1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
30 exception RefineFailure of string Lazy.t;;
31 exception Uncertain of string Lazy.t;;
32 exception AssertFailure of string Lazy.t;;
34 (* for internal use only; the integer is the number of surplus arguments *)
35 exception MoreArgsThanExpected of int * exn;;
37 let insert_coercions = ref true
38 let pack_coercions = ref true
43 if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());;
45 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
47 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
50 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
51 in profiler_eat_prods2.HExtlib.profile foo ()
53 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
54 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
57 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
59 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
62 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
63 in profiler_eat_prods.HExtlib.profile foo ()
65 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
66 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
69 let profiler = HExtlib.profile "CicRefine.fo_unif"
71 let fo_unif_subst subst context metasenv t1 t2 ugraph =
74 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
75 in profiler.HExtlib.profile foo ()
77 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
78 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
81 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
84 RefineFailure msg -> RefineFailure (f msg)
85 | Uncertain msg -> Uncertain (f msg)
86 | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
87 | Sys.Break -> raise exn
88 | _ -> prerr_endline (Printexc.to_string exn); assert false
92 Cic.CicHash.find localization_tbl t
94 prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
97 raise (HExtlib.Localized (loc,exn'))
99 let relocalize localization_tbl oldt newt =
101 let infos = Cic.CicHash.find localization_tbl oldt in
102 Cic.CicHash.remove localization_tbl oldt;
103 Cic.CicHash.add localization_tbl newt infos;
111 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
112 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
115 let exp_impl metasenv subst context =
118 let (metasenv', idx) =
119 CicMkImplicit.mk_implicit_type metasenv subst context in
121 CicMkImplicit.identity_relocation_list_for_metavariable context in
122 metasenv', Cic.Meta (idx, irl)
124 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
125 metasenv', Cic.Meta (idx, [])
127 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
129 CicMkImplicit.identity_relocation_list_for_metavariable context in
130 metasenv', Cic.Meta (idx, irl)
134 let is_a_double_coercion t =
136 let rec aux acc = function
138 | x::tl -> aux (acc@[x]) tl
143 let imp = Cic.Implicit None in
144 let dummyres = false,imp, imp,imp,imp in
146 | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
147 (match last_of tl with
148 | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
149 let sib2,head = last_of tl2 in
150 true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
155 let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
157 let len = List.length tlbody_and_type in
160 CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
161 " (that has type "^ CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
162 ") is here applied to " ^ string_of_int len ^
163 " arguments but here it can handle only up to " ^
164 string_of_int (len - residuals) ^ " arguments")
166 enrich localization_tbl he ~f:(fun _-> msg) exn
169 let mk_prod_of_metas metasenv context' subst args =
170 let rec mk_prod metasenv context' = function
172 let (metasenv, idx) =
173 CicMkImplicit.mk_implicit_type metasenv subst context'
176 CicMkImplicit.identity_relocation_list_for_metavariable context'
178 metasenv,Cic.Meta (idx, irl)
180 let (metasenv, idx) =
181 CicMkImplicit.mk_implicit_type metasenv subst context'
184 CicMkImplicit.identity_relocation_list_for_metavariable context'
186 let meta = Cic.Meta (idx,irl) in
188 (* The name must be fresh for context. *)
189 (* Nevertheless, argty is well-typed only in context. *)
190 (* Thus I generate a name (name_hint) in context and *)
191 (* then I generate a name --- using the hint name_hint *)
192 (* --- that is fresh in context'. *)
194 (* Cic.Name "pippo" *)
195 FreshNamesGenerator.mk_fresh_name ~subst metasenv
196 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
197 (CicMetaSubst.apply_subst_context subst context')
199 ~typ:(CicMetaSubst.apply_subst subst argty)
201 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
202 FreshNamesGenerator.mk_fresh_name ~subst
203 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
205 let metasenv,target =
206 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
208 metasenv,Cic.Prod (name,meta,target)
210 mk_prod metasenv context' args
213 let rec type_of_constant uri ugraph =
214 let module C = Cic in
215 let module R = CicReduction in
216 let module U = UriManager in
217 let _ = CicTypeChecker.typecheck uri in
220 CicEnvironment.get_cooked_obj ugraph uri
221 with Not_found -> assert false
224 C.Constant (_,_,ty,_,_) -> ty,u
225 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
229 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
231 and type_of_variable uri ugraph =
232 let module C = Cic in
233 let module R = CicReduction in
234 let module U = UriManager in
235 let _ = CicTypeChecker.typecheck uri in
238 CicEnvironment.get_cooked_obj ugraph uri
239 with Not_found -> assert false
242 C.Variable (_,_,ty,_,_) -> ty,u
246 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
248 and type_of_mutual_inductive_defs uri i ugraph =
249 let module C = Cic in
250 let module R = CicReduction in
251 let module U = UriManager in
252 let _ = CicTypeChecker.typecheck uri in
255 CicEnvironment.get_cooked_obj ugraph uri
256 with Not_found -> assert false
259 C.InductiveDefinition (dl,_,_,_) ->
260 let (_,_,arity,_) = List.nth dl i in
265 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
267 and type_of_mutual_inductive_constr uri i j ugraph =
268 let module C = Cic in
269 let module R = CicReduction in
270 let module U = UriManager in
271 let _ = CicTypeChecker.typecheck uri in
274 CicEnvironment.get_cooked_obj ugraph uri
275 with Not_found -> assert false
278 C.InductiveDefinition (dl,_,_,_) ->
279 let (_,_,_,cl) = List.nth dl i in
280 let (_,ty) = List.nth cl (j-1) in
286 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
289 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
291 (* the check_branch function checks if a branch of a case is refinable.
292 It returns a pair (outype_instance,args), a subst and a metasenv.
293 outype_instance is the expected result of applying the case outtype
295 The problem is that outype is in general unknown, and we should
296 try to synthesize it from the above information, that is in general
297 a second order unification problem. *)
299 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
300 let module C = Cic in
301 (* let module R = CicMetaSubst in *)
302 let module R = CicReduction in
303 match R.whd ~subst context expectedtype with
305 (n,context,actualtype, [term]), subst, metasenv, ugraph
306 | C.Appl (C.MutInd (_,_,_)::tl) ->
307 let (_,arguments) = split tl left_args_no in
308 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
309 | C.Prod (name,so,de) ->
310 (* we expect that the actual type of the branch has the due
312 (match R.whd ~subst context actualtype with
313 C.Prod (name',so',de') ->
314 let subst, metasenv, ugraph1 =
315 fo_unif_subst subst context metasenv so so' ugraph in
317 (match CicSubstitution.lift 1 term with
318 C.Appl l -> C.Appl (l@[C.Rel 1])
319 | t -> C.Appl [t ; C.Rel 1]) in
320 (* we should also check that the name variable is anonymous in
321 the actual type de' ?? *)
323 ((Some (name,(C.Decl so)))::context)
324 metasenv subst left_args_no de' term' de ugraph1
325 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
326 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
328 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
331 let rec type_of_aux subst metasenv context t ugraph =
332 let module C = Cic in
333 let module S = CicSubstitution in
334 let module U = UriManager in
335 let (t',_,_,_,_) as res =
340 match List.nth context (n - 1) with
341 Some (_,C.Decl ty) ->
342 t,S.lift n ty,subst,metasenv, ugraph
343 | Some (_,C.Def (_,Some ty)) ->
344 t,S.lift n ty,subst,metasenv, ugraph
345 | Some (_,C.Def (bo,None)) ->
347 (* if it is in the context it must be already well-typed*)
348 CicTypeChecker.type_of_aux' ~subst metasenv context
351 t,ty,subst,metasenv,ugraph
353 enrich localization_tbl t
354 (RefineFailure (lazy "Rel to hidden hypothesis"))
357 enrich localization_tbl t
358 (RefineFailure (lazy "Not a closed term")))
359 | C.Var (uri,exp_named_subst) ->
360 let exp_named_subst',subst',metasenv',ugraph1 =
361 check_exp_named_subst
362 subst metasenv context exp_named_subst ugraph
364 let ty_uri,ugraph1 = type_of_variable uri ugraph in
366 CicSubstitution.subst_vars exp_named_subst' ty_uri
368 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
371 let (canonical_context, term,ty) =
372 CicUtil.lookup_subst n subst
374 let l',subst',metasenv',ugraph1 =
375 check_metasenv_consistency n subst metasenv context
376 canonical_context l ugraph
378 (* trust or check ??? *)
379 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
380 subst', metasenv', ugraph1
381 (* type_of_aux subst metasenv
382 context (CicSubstitution.subst_meta l term) *)
383 with CicUtil.Subst_not_found _ ->
384 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
385 let l',subst',metasenv', ugraph1 =
386 check_metasenv_consistency n subst metasenv context
387 canonical_context l ugraph
389 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
390 subst', metasenv',ugraph1)
391 | C.Sort (C.Type tno) ->
392 let tno' = CicUniv.fresh() in
394 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
395 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
397 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
399 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
400 | C.Implicit infos ->
401 let metasenv',t' = exp_impl metasenv subst context infos in
402 type_of_aux subst metasenv' context t' ugraph
404 let ty',_,subst',metasenv',ugraph1 =
405 type_of_aux subst metasenv context ty ugraph
407 let te',inferredty,subst'',metasenv'',ugraph2 =
408 type_of_aux subst' metasenv' context te ugraph1
410 let (te', ty'), subst''',metasenv''',ugraph3 =
411 coerce_to_something true localization_tbl te' inferredty ty'
412 subst'' metasenv'' context ugraph2
414 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
415 | C.Prod (name,s,t) ->
416 let s',sort1,subst',metasenv',ugraph1 =
417 type_of_aux subst metasenv context s ugraph
419 let s',sort1,subst', metasenv',ugraph1 =
420 coerce_to_sort localization_tbl
421 s' sort1 subst' context metasenv' ugraph1
423 let context_for_t = ((Some (name,(C.Decl s')))::context) in
424 let t',sort2,subst'',metasenv'',ugraph2 =
425 type_of_aux subst' metasenv'
426 context_for_t t ugraph1
428 let t',sort2,subst'',metasenv'',ugraph2 =
429 coerce_to_sort localization_tbl
430 t' sort2 subst'' context_for_t metasenv'' ugraph2
432 let sop,subst''',metasenv''',ugraph3 =
433 sort_of_prod localization_tbl subst'' metasenv''
434 context (name,s') t' (sort1,sort2) ugraph2
436 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
437 | C.Lambda (n,s,t) ->
438 let s',sort1,subst',metasenv',ugraph1 =
439 type_of_aux subst metasenv context s ugraph
441 let s',sort1,subst',metasenv',ugraph1 =
442 coerce_to_sort localization_tbl
443 s' sort1 subst' context metasenv' ugraph1
445 let context_for_t = ((Some (n,(C.Decl s')))::context) in
446 let t',type2,subst'',metasenv'',ugraph2 =
447 type_of_aux subst' metasenv' context_for_t t ugraph1
449 C.Lambda (n,s',t'),C.Prod (n,s',type2),
450 subst'',metasenv'',ugraph2
452 (* only to check if s is well-typed *)
453 let s',ty,subst',metasenv',ugraph1 =
454 type_of_aux subst metasenv context s ugraph
456 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
458 let t',inferredty,subst'',metasenv'',ugraph2 =
459 type_of_aux subst' metasenv'
460 context_for_t t ugraph1
462 (* One-step LetIn reduction.
463 * Even faster than the previous solution.
464 * Moreover the inferred type is closer to the expected one.
467 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
468 subst'',metasenv'',ugraph2
469 | C.Appl (he::((_::_) as tl)) ->
470 let he',hetype,subst',metasenv',ugraph1 =
471 type_of_aux subst metasenv context he ugraph
473 let tlbody_and_type,subst'',metasenv'',ugraph2 =
474 typeof_list subst' metasenv' context ugraph1 tl
476 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
477 eat_prods true subst'' metasenv'' context
478 he' hetype tlbody_and_type ugraph2
480 let newappl = (C.Appl (coerced_he::coerced_args)) in
481 avoid_double_coercion
482 context subst''' metasenv''' ugraph3 newappl applty
483 | C.Appl _ -> assert false
484 | C.Const (uri,exp_named_subst) ->
485 let exp_named_subst',subst',metasenv',ugraph1 =
486 check_exp_named_subst subst metasenv context
487 exp_named_subst ugraph in
488 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
490 CicSubstitution.subst_vars exp_named_subst' ty_uri
492 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
493 | C.MutInd (uri,i,exp_named_subst) ->
494 let exp_named_subst',subst',metasenv',ugraph1 =
495 check_exp_named_subst subst metasenv context
496 exp_named_subst ugraph
498 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
500 CicSubstitution.subst_vars exp_named_subst' ty_uri in
501 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
502 | C.MutConstruct (uri,i,j,exp_named_subst) ->
503 let exp_named_subst',subst',metasenv',ugraph1 =
504 check_exp_named_subst subst metasenv context
505 exp_named_subst ugraph
508 type_of_mutual_inductive_constr uri i j ugraph1
511 CicSubstitution.subst_vars exp_named_subst' ty_uri
513 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
515 | C.MutCase (uri, i, outtype, term, pl) ->
516 (* first, get the inductive type (and noparams)
517 * in the environment *)
518 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
519 let _ = CicTypeChecker.typecheck uri in
520 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
522 C.InductiveDefinition (l,expl_params,parsno,_) ->
523 List.nth l i , expl_params, parsno, u
525 enrich localization_tbl t
527 (lazy ("Unkown mutual inductive definition " ^
528 U.string_of_uri uri)))
530 let rec count_prod t =
531 match CicReduction.whd ~subst context t with
532 C.Prod (_, _, t) -> 1 + (count_prod t)
535 let no_args = count_prod arity in
536 (* now, create a "generic" MutInd *)
537 let metasenv,left_args =
538 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
540 let metasenv,right_args =
541 let no_right_params = no_args - no_left_params in
542 if no_right_params < 0 then assert false
543 else CicMkImplicit.n_fresh_metas
544 metasenv subst context no_right_params
546 let metasenv,exp_named_subst =
547 CicMkImplicit.fresh_subst metasenv subst context expl_params in
550 C.MutInd (uri,i,exp_named_subst)
553 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
555 (* check consistency with the actual type of term *)
556 let term',actual_type,subst,metasenv,ugraph1 =
557 type_of_aux subst metasenv context term ugraph in
558 let expected_type',_, subst, metasenv,ugraph2 =
559 type_of_aux subst metasenv context expected_type ugraph1
561 let actual_type = CicReduction.whd ~subst context actual_type in
562 let subst,metasenv,ugraph3 =
564 fo_unif_subst subst context metasenv
565 expected_type' actual_type ugraph2
568 enrich localization_tbl term' exn
570 lazy ("(10)The term " ^
571 CicMetaSubst.ppterm_in_context ~metasenv subst term'
572 context ^ " has type " ^
573 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
574 context ^ " but is here used with type " ^
575 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
577 let rec instantiate_prod t =
581 match CicReduction.whd ~subst context t with
583 instantiate_prod (CicSubstitution.subst he t') tl
586 let arity_instantiated_with_left_args =
587 instantiate_prod arity left_args in
588 (* TODO: check if the sort elimination
589 * is allowed: [(I q1 ... qr)|B] *)
590 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
592 (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
594 if left_args = [] then
595 (C.MutConstruct (uri,i,j,exp_named_subst))
598 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
600 let p',actual_type,subst,metasenv,ugraph1 =
601 type_of_aux subst metasenv context p ugraph
603 let constructor',expected_type, subst, metasenv,ugraph2 =
604 type_of_aux subst metasenv context constructor ugraph1
606 let outtypeinstance,subst,metasenv,ugraph3 =
608 check_branch 0 context metasenv subst
609 no_left_params actual_type constructor' expected_type
613 enrich localization_tbl constructor'
615 lazy ("(11)The term " ^
616 CicMetaSubst.ppterm_in_context metasenv subst p'
617 context ^ " has type " ^
618 CicMetaSubst.ppterm_in_context metasenv subst actual_type
619 context ^ " but is here used with type " ^
620 CicMetaSubst.ppterm_in_context metasenv subst expected_type
624 outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
625 pl ([],List.length pl,[],subst,metasenv,ugraph3)
628 (* we are left to check that the outype matches his instances.
629 The easy case is when the outype is specified, that amount
630 to a trivial check. Otherwise, we should guess a type from
634 let outtype,outtypety, subst, metasenv,ugraph4 =
635 type_of_aux subst metasenv context outtype ugraph4 in
638 (let candidate,ugraph5,metasenv,subst =
639 let exp_name_subst, metasenv =
641 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
643 let uris = CicUtil.params_of_obj o in
645 fun uri (acc,metasenv) ->
646 let metasenv',new_meta =
647 CicMkImplicit.mk_implicit metasenv subst context
650 CicMkImplicit.identity_relocation_list_for_metavariable
653 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
657 match left_args,right_args with
658 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
660 let rec mk_right_args =
663 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
665 let right_args_no = List.length right_args in
666 let lifted_left_args =
667 List.map (CicSubstitution.lift right_args_no) left_args
669 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
670 (lifted_left_args @ mk_right_args right_args_no))
673 FreshNamesGenerator.mk_fresh_name ~subst metasenv
674 context Cic.Anonymous ~typ:ty
676 match outtypeinstances with
678 let extended_context =
679 let rec add_right_args =
681 Cic.Prod (name,ty,t) ->
682 Some (name,Cic.Decl ty)::(add_right_args t)
685 (Some (fresh_name,Cic.Decl ty))::
687 (add_right_args arity_instantiated_with_left_args))@
690 let metasenv,new_meta =
691 CicMkImplicit.mk_implicit metasenv subst extended_context
694 CicMkImplicit.identity_relocation_list_for_metavariable
697 let rec add_lambdas b =
699 Cic.Prod (name,ty,t) ->
700 Cic.Lambda (name,ty,(add_lambdas b t))
701 | _ -> Cic.Lambda (fresh_name, ty, b)
704 add_lambdas (Cic.Meta (new_meta,irl))
705 arity_instantiated_with_left_args
707 (Some candidate),ugraph4,metasenv,subst
708 | (constructor_args_no,_,instance,_)::tl ->
710 let instance',subst,metasenv =
711 CicMetaSubst.delift_rels subst metasenv
712 constructor_args_no instance
714 let candidate,ugraph,metasenv,subst =
716 fun (candidate_oty,ugraph,metasenv,subst)
717 (constructor_args_no,_,instance,_) ->
718 match candidate_oty with
719 | None -> None,ugraph,metasenv,subst
722 let instance',subst,metasenv =
723 CicMetaSubst.delift_rels subst metasenv
724 constructor_args_no instance
726 let subst,metasenv,ugraph =
727 fo_unif_subst subst context metasenv
730 candidate_oty,ugraph,metasenv,subst
732 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
733 | RefineFailure _ | Uncertain _ ->
734 None,ugraph,metasenv,subst
735 ) (Some instance',ugraph4,metasenv,subst) tl
738 | None -> None, ugraph,metasenv,subst
740 let rec add_lambdas n b =
742 Cic.Prod (name,ty,t) ->
743 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
745 Cic.Lambda (fresh_name, ty,
746 CicSubstitution.lift (n + 1) t)
749 (add_lambdas 0 t arity_instantiated_with_left_args),
750 ugraph,metasenv,subst
751 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
752 None,ugraph4,metasenv,subst
755 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
757 let subst,metasenv,ugraph =
759 fo_unif_subst subst context metasenv
760 candidate outtype ugraph5
762 exn -> assert false(* unification against a metavariable *)
764 C.MutCase (uri, i, outtype, term', pl'),
765 CicReduction.head_beta_reduce
766 (CicMetaSubst.apply_subst subst
767 (Cic.Appl (outtype::right_args@[term']))),
768 subst,metasenv,ugraph)
769 | _ -> (* easy case *)
770 let tlbody_and_type,subst,metasenv,ugraph4 =
771 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
773 let _,_,_,subst,metasenv,ugraph4 =
774 eat_prods false subst metasenv context
775 outtype outtypety tlbody_and_type ugraph4
777 let _,_, subst, metasenv,ugraph5 =
778 type_of_aux subst metasenv context
779 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
781 let (subst,metasenv,ugraph6) =
783 (fun (subst,metasenv,ugraph)
784 p (constructor_args_no,context,instance,args)
789 CicSubstitution.lift constructor_args_no outtype
791 C.Appl (outtype'::args)
793 CicReduction.whd ~subst context appl
796 fo_unif_subst subst context metasenv instance instance'
800 enrich localization_tbl p exn
802 lazy ("(12)The term " ^
803 CicMetaSubst.ppterm_in_context ~metasenv subst p
804 context ^ " has type " ^
805 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
806 context ^ " but is here used with type " ^
807 CicMetaSubst.ppterm_in_context ~metasenv subst instance
809 (subst,metasenv,ugraph5) pl' outtypeinstances
811 C.MutCase (uri, i, outtype, term', pl'),
812 CicReduction.head_beta_reduce
813 (CicMetaSubst.apply_subst subst
814 (C.Appl(outtype::right_args@[term]))),
815 subst,metasenv,ugraph6)
817 let fl_ty',subst,metasenv,types,ugraph1,len =
819 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
820 let ty',_,subst',metasenv',ugraph1 =
821 type_of_aux subst metasenv context ty ugraph
823 fl @ [ty'],subst',metasenv',
824 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
825 :: types, ugraph, len+1
826 ) ([],subst,metasenv,[],ugraph,0) fl
828 let context' = types@context in
829 let fl_bo',subst,metasenv,ugraph2 =
831 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
832 let bo',ty_of_bo,subst,metasenv,ugraph1 =
833 type_of_aux subst metasenv context' bo ugraph in
834 let expected_ty = CicSubstitution.lift len ty in
835 let subst',metasenv',ugraph' =
837 fo_unif_subst subst context' metasenv
838 ty_of_bo expected_ty ugraph1
841 enrich localization_tbl bo exn
843 lazy ("(13)The term " ^
844 CicMetaSubst.ppterm_in_context ~metasenv subst bo
845 context' ^ " has type " ^
846 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
847 context' ^ " but is here used with type " ^
848 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
851 fl @ [bo'] , subst',metasenv',ugraph'
852 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
854 let ty = List.nth fl_ty' i in
855 (* now we have the new ty in fl_ty', the new bo in fl_bo',
856 * and we want the new fl with bo' and ty' injected in the right
859 let rec map3 f l1 l2 l3 =
862 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
865 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
868 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
870 let fl_ty',subst,metasenv,types,ugraph1,len =
872 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
873 let ty',_,subst',metasenv',ugraph1 =
874 type_of_aux subst metasenv context ty ugraph
876 fl @ [ty'],subst',metasenv',
877 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
878 types, ugraph1, len+1
879 ) ([],subst,metasenv,[],ugraph,0) fl
881 let context' = types@context in
882 let fl_bo',subst,metasenv,ugraph2 =
884 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
885 let bo',ty_of_bo,subst,metasenv,ugraph1 =
886 type_of_aux subst metasenv context' bo ugraph in
887 let expected_ty = CicSubstitution.lift len ty in
888 let subst',metasenv',ugraph' =
890 fo_unif_subst subst context' metasenv
891 ty_of_bo expected_ty ugraph1
894 enrich localization_tbl bo exn
896 lazy ("(14)The term " ^
897 CicMetaSubst.ppterm_in_context ~metasenv subst bo
898 context' ^ " has type " ^
899 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
900 context' ^ " but is here used with type " ^
901 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
904 fl @ [bo'],subst',metasenv',ugraph'
905 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
907 let ty = List.nth fl_ty' i in
908 (* now we have the new ty in fl_ty', the new bo in fl_bo',
909 * and we want the new fl with bo' and ty' injected in the right
912 let rec map3 f l1 l2 l3 =
915 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
918 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
921 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
923 relocalize localization_tbl t t';
926 (* check_metasenv_consistency checks that the "canonical" context of a
927 metavariable is consitent - up to relocation via the relocation list l -
928 with the actual context *)
929 and check_metasenv_consistency
930 metano subst metasenv context canonical_context l ugraph
932 let module C = Cic in
933 let module R = CicReduction in
934 let module S = CicSubstitution in
935 let lifted_canonical_context =
939 | (Some (n,C.Decl t))::tl ->
940 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
941 | (Some (n,C.Def (t,None)))::tl ->
942 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
943 | None::tl -> None::(aux (i+1) tl)
944 | (Some (n,C.Def (t,Some ty)))::tl ->
946 C.Def ((S.subst_meta l (S.lift i t)),
947 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
949 aux 1 canonical_context
953 (fun (l,subst,metasenv,ugraph) t ct ->
956 l @ [None],subst,metasenv,ugraph
957 | Some t,Some (_,C.Def (ct,_)) ->
958 let subst',metasenv',ugraph' =
960 prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
961 fo_unif_subst subst context metasenv t ct ugraph
962 with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
964 l @ [Some t],subst',metasenv',ugraph'
965 | Some t,Some (_,C.Decl ct) ->
966 let t',inferredty,subst',metasenv',ugraph1 =
967 type_of_aux subst metasenv context t ugraph
969 let subst'',metasenv'',ugraph2 =
972 subst' context metasenv' inferredty ct ugraph1
973 with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
975 l @ [Some t'], subst'',metasenv'',ugraph2
977 raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
979 Invalid_argument _ ->
983 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
984 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
985 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
987 and check_exp_named_subst metasubst metasenv context tl ugraph =
988 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
990 [] -> [],metasubst,metasenv,ugraph
992 let ty_uri,ugraph1 = type_of_variable uri ugraph in
994 CicSubstitution.subst_vars substs ty_uri in
995 (* CSC: why was this code here? it is wrong
996 (match CicEnvironment.get_cooked_obj ~trust:false uri with
997 Cic.Variable (_,Some bo,_,_) ->
1000 "A variable with a body can not be explicit substituted"))
1001 | Cic.Variable (_,None,_,_) -> ()
1004 (RefineFailure (lazy
1005 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1008 let t',typeoft,metasubst',metasenv',ugraph2 =
1009 type_of_aux metasubst metasenv context t ugraph1 in
1010 let subst = uri,t' in
1011 let metasubst'',metasenv'',ugraph3 =
1014 metasubst' context metasenv' typeoft typeofvar ugraph2
1016 raise (RefineFailure (lazy
1017 ("Wrong Explicit Named Substitution: " ^
1018 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1019 " not unifiable with " ^
1020 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1022 (* FIXME: no mere tail recursive! *)
1023 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1024 check_exp_named_subst_aux
1025 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1027 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1029 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1032 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1035 let module C = Cic in
1036 let context_for_t2 = (Some (name,C.Decl s))::context in
1037 let t1'' = CicReduction.whd ~subst context t1 in
1038 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1039 match (t1'', t2'') with
1040 (C.Sort s1, C.Sort s2)
1041 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1042 (* different than Coq manual!!! *)
1043 C.Sort s2,subst,metasenv,ugraph
1044 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1045 let t' = CicUniv.fresh() in
1047 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1048 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1049 C.Sort (C.Type t'),subst,metasenv,ugraph2
1051 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1052 | (C.Sort _,C.Sort (C.Type t1)) ->
1053 C.Sort (C.Type t1),subst,metasenv,ugraph
1054 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1055 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1056 (* TODO how can we force the meta to become a sort? If we don't we
1057 * break the invariant that refine produce only well typed terms *)
1058 (* TODO if we check the non meta term and if it is a sort then we
1059 * are likely to know the exact value of the result e.g. if the rhs
1060 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1061 let (metasenv,idx) =
1062 CicMkImplicit.mk_implicit_sort metasenv subst in
1063 let (subst, metasenv,ugraph1) =
1065 fo_unif_subst subst context_for_t2 metasenv
1066 (C.Meta (idx,[])) t2'' ugraph
1067 with _ -> assert false (* unification against a metavariable *)
1069 t2'',subst,metasenv,ugraph1
1072 enrich localization_tbl s
1076 "%s is supposed to be a type, but its type is %s"
1077 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1078 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1080 enrich localization_tbl t
1084 "%s is supposed to be a type, but its type is %s"
1085 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1086 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1088 and avoid_double_coercion context subst metasenv ugraph t ty =
1089 if not !pack_coercions then
1090 t,ty,subst,metasenv,ugraph
1092 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1094 let source_carr = CoercGraph.source_of c2 in
1095 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1096 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1098 | CoercGraph.SomeCoercion candidates ->
1100 HExtlib.list_findopt
1101 (function (metasenv,last,c) ->
1103 | c when not (CoercGraph.is_composite c) ->
1104 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1107 let subst,metasenv,ugraph =
1108 fo_unif_subst subst context metasenv last head ugraph in
1109 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1114 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1115 let newt,_,subst,metasenv,ugraph =
1116 type_of_aux subst metasenv context c ugraph in
1117 debug_print (lazy "tipa...");
1118 let subst, metasenv, ugraph =
1119 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1120 fo_unif_subst subst context metasenv newt t ugraph
1122 debug_print (lazy "unifica...");
1123 Some (newt, ty, subst, metasenv, ugraph)
1125 | RefineFailure s | Uncertain s when not !pack_coercions->
1126 debug_print s; debug_print (lazy "stop\n");None
1127 | RefineFailure s | Uncertain s ->
1128 debug_print s;debug_print (lazy "goon\n");
1130 let old_pack_coercions = !pack_coercions in
1131 pack_coercions := false; (* to avoid diverging *)
1132 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1133 type_of_aux subst metasenv context c1_c2_implicit ugraph
1135 pack_coercions := old_pack_coercions;
1137 is_a_double_coercion refined_c1_c2_implicit
1143 match refined_c1_c2_implicit with
1144 | Cic.Appl l -> HExtlib.list_last l
1147 let subst, metasenv, ugraph =
1148 try fo_unif_subst subst context metasenv
1150 with RefineFailure s| Uncertain s->
1151 debug_print s;assert false
1153 let subst, metasenv, ugraph =
1154 fo_unif_subst subst context metasenv
1155 refined_c1_c2_implicit t ugraph
1157 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1159 | RefineFailure s | Uncertain s ->
1160 pack_coercions := true;debug_print s;None
1161 | exn -> pack_coercions := true; raise exn))
1164 (match selected with
1168 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1169 t, ty, subst, metasenv, ugraph)
1170 | _ -> t, ty, subst, metasenv, ugraph)
1172 t, ty, subst, metasenv, ugraph
1174 and typeof_list subst metasenv context ugraph l =
1175 let tlbody_and_type,subst,metasenv,ugraph =
1177 (fun x (res,subst,metasenv,ugraph) ->
1178 let x',ty,subst',metasenv',ugraph1 =
1179 type_of_aux subst metasenv context x ugraph
1181 (x', ty)::res,subst',metasenv',ugraph1
1182 ) l ([],subst,metasenv,ugraph)
1184 tlbody_and_type,subst,metasenv,ugraph
1187 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1189 (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1190 let fix_arity n metasenv context subst he hetype ugraph =
1191 let hetype = CicMetaSubst.apply_subst subst hetype in
1192 let src = CoercDb.coerc_carr_of_term hetype in
1193 let tgt = CoercDb.Fun 0 in
1194 match CoercGraph.look_for_coercion' metasenv subst context src tgt with
1195 | CoercGraph.NoCoercion -> []
1196 | CoercGraph.NotMetaClosed
1197 | CoercGraph.NotHandled _ ->
1198 raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1199 | CoercGraph.SomeCoercionToTgt candidates
1200 | CoercGraph.SomeCoercion candidates ->
1202 (fun (metasenv,last,coerc) ->
1204 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1205 let subst,metasenv,ugraph =
1206 fo_unif_subst subst context metasenv last he ugraph in
1207 debug_print (lazy ("New head: "^ pp coerc));
1210 CicTypeChecker.type_of_aux' ~subst metasenv context coerc ugraph in
1211 debug_print (lazy (" has type: "^ pp tty));
1212 Some (coerc,tty,subst,metasenv,ugraph)
1214 | Uncertain _ | RefineFailure _
1215 | HExtlib.Localized (_,Uncertain _)
1216 | HExtlib.Localized (_,RefineFailure _) -> None
1217 | exn -> assert false)
1220 (* aux function to process the type of the head and the args in parallel *)
1221 let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1223 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1224 | (hete, hety)::tl as args ->
1225 match (CicReduction.whd ~subst context hetype) with
1226 | Cic.Prod (n,s,t) ->
1227 let arg,subst,metasenv,ugraph =
1228 coerce_to_something allow_coercions localization_tbl
1229 hete hety s subst metasenv context ugraph in
1231 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1232 ugraph (newargs@[arg]) tl
1235 match he, newargs with
1237 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1238 | _ -> Cic.Appl (he::List.map fst newargs)
1240 (*{{{*) debug_print (lazy
1242 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1243 "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1244 "\n but is applyed to: " ^ String.concat ";"
1245 (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1246 let possible_fixes =
1247 fix_arity (List.length args) metasenv context subst he hetype
1250 HExtlib.list_findopt
1251 (fun (he,hetype,subst,metasenv,ugraph) ->
1252 (* {{{ *)debug_print (lazy ("Try fix: "^
1253 CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1254 debug_print (lazy (" of type: "^
1255 CicMetaSubst.ppterm_in_context
1256 ~metasenv subst hetype context)); (* }}} *)
1258 Some (eat_prods_and_args
1259 metasenv subst context he hetype ugraph [] args)
1261 | RefineFailure _ | Uncertain _
1262 | HExtlib.Localized (_,RefineFailure _)
1263 | HExtlib.Localized (_,Uncertain _) -> None)
1269 (MoreArgsThanExpected
1270 (List.length args, RefineFailure (lazy "")))
1272 (* first we check if we are in the simple case of a meta closed term *)
1273 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1274 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1275 (* this optimization is to postpone fix_arity (the most common case)*)
1276 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1278 (* this (says CSC) is also useful to infer dependent types *)
1279 let pristinemenv = metasenv in
1280 let metasenv,hetype' =
1281 mk_prod_of_metas metasenv context subst args_bo_and_ty
1284 let subst,metasenv,ugraph =
1285 fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1287 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1288 with RefineFailure _ | Uncertain _ ->
1289 subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1291 let coerced_args,subst,metasenv,he,t,ugraph =
1294 metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1296 MoreArgsThanExpected (residuals,exn) ->
1297 more_args_than_expected localization_tbl metasenv
1298 subst he context hetype' residuals args_bo_and_ty exn
1300 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1302 and coerce_to_something
1303 allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1305 let module CS = CicSubstitution in
1306 let module CR = CicReduction in
1307 let cs_subst = CS.subst ~avoid_beta_redexes:true in
1308 let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1309 debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1311 CoercGraph.look_for_coercion metasenv subst context infty expty
1314 | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
1315 "coerce_atom_to_something fails since not meta closed"))
1316 | CoercGraph.NoCoercion
1317 | CoercGraph.SomeCoercionToTgt _
1318 | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
1319 "coerce_atom_to_something fails since no coercions found"))
1320 | CoercGraph.SomeCoercion candidates ->
1321 debug_print (lazy (string_of_int (List.length candidates) ^
1322 " candidates found"));
1323 let uncertain = ref false in
1327 (fun (metasenv,last,c) ->
1329 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1330 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1332 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1333 debug_print (lazy ("FO_UNIF_SUBST: " ^
1334 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1335 let subst,metasenv,ugraph =
1336 fo_unif_subst subst context metasenv last t ugraph
1338 let newt,newhety,subst,metasenv,ugraph =
1339 type_of_aux subst metasenv context c ugraph in
1340 let newt, newty, subst, metasenv, ugraph =
1341 avoid_double_coercion context subst metasenv ugraph newt expty
1343 let subst,metasenv,ugraph =
1344 fo_unif_subst subst context metasenv newhety expty ugraph in
1345 Some ((newt,newty), subst, metasenv, ugraph)
1347 | Uncertain _ -> uncertain := true; None
1348 | RefineFailure _ -> None)
1353 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1361 | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1362 | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1364 let rec coerce_to_something_aux
1365 t infty expty subst metasenv context ugraph
1368 let subst, metasenv, ugraph =
1369 fo_unif_subst subst context metasenv infty expty ugraph
1371 (t, expty), subst, metasenv, ugraph
1372 with Uncertain _ | RefineFailure _ as exn ->
1373 if not allow_coercions || not !insert_coercions then
1374 enrich localization_tbl t exn
1376 let whd = CicReduction.whd ~delta:false in
1377 let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1378 let infty = clean infty subst context in
1379 let expty = clean expty subst context in
1380 let t = clean t subst context in
1381 (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1382 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1383 CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1384 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1385 let (coerced,_),subst,metasenv,_ as result =
1386 match infty, expty, t with
1387 | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1388 (*{{{*) debug_print (lazy "FIX");
1390 [name,i,_(* infty *),bo] ->
1392 Some (Cic.Name name,Cic.Decl expty)::context in
1393 let (rel1, _), subst, metasenv, ugraph =
1394 coerce_to_something_aux (Cic.Rel 1)
1395 (CS.lift 1 expty) (CS.lift 1 infty) subst
1396 metasenv context_bo ugraph in
1397 let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1398 let (bo,_), subst, metasenv, ugraph =
1399 coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1401 metasenv context_bo ugraph
1403 (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1404 | _ -> assert false (* not implemented yet *)) (*}}}*)
1405 | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1406 (*{{{*) debug_print (lazy "CASE");
1407 (* {{{ helper functions *)
1408 let get_cl_and_left_p uri tyno outty ugraph =
1409 match CicEnvironment.get_obj ugraph uri with
1410 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1413 match CicReduction.whd ~delta:false ctx t with
1414 | Cic.Prod (name,src,tgt) ->
1415 let ctx = Some (name, Cic.Decl src) :: ctx in
1421 let rec skip_lambda_delifting t n =
1424 | Cic.Lambda (_,_,t),n ->
1425 skip_lambda_delifting
1426 (CS.subst (Cic.Implicit None) t) (n - 1)
1429 let get_l_r_p n = function
1430 | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1431 | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1432 HExtlib.split_nth n args
1435 let _, _, ty, cl = List.nth tl tyno in
1436 let pis = count_pis ty in
1437 let rno = pis - leftno in
1438 let t = skip_lambda_delifting outty rno in
1439 let left_p, _ = get_l_r_p leftno t in
1440 let instantiale_with_left cl =
1444 (fun t p -> match t with
1445 | Cic.Prod (_,_,t) ->
1451 let cl = instantiale_with_left (List.map snd cl) in
1452 cl, left_p, leftno, rno, ugraph
1455 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1458 let rec mkr n = function
1459 | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1462 CicReplace.replace_lifting
1463 ~equality:(fun _ -> CicUtil.alpha_equivalence)
1465 ~what:(matched::right_p)
1466 ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1470 | Cic.Lambda (name, src, tgt),_ ->
1471 Cic.Lambda (name, src,
1472 keep_lambdas_and_put_expty
1473 (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1474 (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1477 let eq_uri, eq, eq_refl =
1478 match LibraryObjects.eq_URI () with
1479 | None -> HLog.warn "no default equality"; raise exn
1480 | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1483 metasenv subst context uri tyno cty outty mty m leftno i
1485 let rec aux context outty par k mty m = function
1486 | Cic.Prod (name, src, tgt) ->
1489 (Some (name, Cic.Decl src) :: context)
1490 (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1491 (CS.lift 1 mty) (CS.lift 1 m) tgt
1493 Cic.Prod (name, src, t), k
1496 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1497 if par <> [] then Cic.Appl (k::par) else k
1499 Cic.Prod (Cic.Name "p",
1500 Cic.Appl [eq; mty; m; k],
1502 (CR.head_beta_reduce ~delta:false
1503 (Cic.Appl [outty;k])))),k
1504 | Cic.Appl (Cic.MutInd _::pl) ->
1505 let left_p,right_p = HExtlib.split_nth leftno pl in
1506 let has_rights = right_p <> [] in
1508 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1509 Cic.Appl (k::left_p@par)
1513 CicTypeChecker.type_of_aux' ~subst metasenv context k
1514 CicUniv.oblivion_ugraph
1516 | Cic.Appl (Cic.MutInd _::args),_ ->
1517 snd (HExtlib.split_nth leftno args)
1519 with CicTypeChecker.TypeCheckerFailure _-> assert false
1522 CR.head_beta_reduce ~delta:false
1523 (Cic.Appl (outty ::right_p @ [k])),k
1525 Cic.Prod (Cic.Name "p",
1526 Cic.Appl [eq; mty; m; k],
1528 (CR.head_beta_reduce ~delta:false
1529 (Cic.Appl (outty ::right_p @ [k]))))),k
1532 aux context outty [] 1 mty m cty
1534 let add_lambda_for_refl_m pbo rno mty m k cty =
1535 (* k lives in the right context *)
1536 if rno <> 0 then pbo else
1537 let rec aux mty m = function
1538 | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1539 Cic.Lambda (name,src,
1540 (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1542 Cic.Lambda (Cic.Name "p",
1543 Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1547 let add_pi_for_refl_m new_outty mty m rno =
1548 if rno <> 0 then new_outty else
1549 let rec aux m mty = function
1550 | Cic.Lambda (name, src, tgt) ->
1551 Cic.Lambda (name, src,
1552 aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1555 (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1559 in (* }}} end helper functions *)
1560 (* constructors types with left params already instantiated *)
1561 let outty = CicMetaSubst.apply_subst subst outty in
1562 let cl, left_p, leftno,rno,ugraph =
1563 get_cl_and_left_p uri tyno outty ugraph
1568 CicTypeChecker.type_of_aux' ~subst metasenv context m
1569 CicUniv.oblivion_ugraph
1571 | Cic.MutInd _ as mty,_ -> [], mty
1572 | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
1573 snd (HExtlib.split_nth leftno args), mty
1575 with CicTypeChecker.TypeCheckerFailure _ -> assert false
1578 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1581 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1582 ~metasenv subst new_outty context));
1583 let _,pl,subst,metasenv,ugraph =
1585 (fun cty pbo (i, acc, s, menv, ugraph) ->
1586 (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1587 * (new_)outty right_par (K_i left_par k_par) *)
1589 add_params menv s context uri tyno
1590 cty outty mty m leftno i in
1592 (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1593 ~metasenv subst infty_pbo context));
1594 let expty_pbo, k = (* k is (K_i left_par k_par) *)
1595 add_params menv s context uri tyno
1596 cty new_outty mty m leftno i in
1598 (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1599 ~metasenv subst expty_pbo context));
1600 let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1602 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1603 ~metasenv subst pbo context));
1604 let (pbo, _), subst, metasenv, ugraph =
1605 coerce_to_something_aux pbo infty_pbo expty_pbo
1606 s menv context ugraph
1609 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1610 ~metasenv subst pbo context));
1611 (i-1, pbo::acc, subst, metasenv, ugraph))
1612 cl pl (List.length pl, [], subst, metasenv, ugraph)
1614 let new_outty = add_pi_for_refl_m new_outty mty m rno in
1616 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1617 ~metasenv subst new_outty context));
1620 let refl_m=Cic.Appl[eq_refl;mty;m]in
1621 Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1623 Cic.MutCase(uri,tyno,new_outty,m,pl)
1625 (t, expty), subst, metasenv, ugraph (*}}}*)
1626 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1627 (*{{{*) debug_print (lazy "LAM");
1629 FreshNamesGenerator.mk_fresh_name
1630 ~subst metasenv context ~typ:src2 Cic.Anonymous
1632 let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1633 (* contravariant part: the argument of f:src->ty *)
1634 let (rel1, _), subst, metasenv, ugraph =
1635 coerce_to_something_aux
1636 (Cic.Rel 1) (CS.lift 1 src2)
1637 (CS.lift 1 src) subst metasenv context_src2 ugraph
1639 (* covariant part: the result of f(c x); x:src2; (c x):src *)
1642 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1643 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1645 (* we fix the possible dependency problem in the source ty *)
1646 let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1647 let (bo, _), subst, metasenv, ugraph =
1648 coerce_to_something_aux
1649 bo ty ty2 subst metasenv context_src2 ugraph
1651 let coerced = Cic.Lambda (name_t,src2, bo) in
1652 (coerced, expty), subst, metasenv, ugraph (*}}}*)
1654 (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1655 ~metasenv subst infty context ^ " ==> " ^
1656 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1657 coerce_atom_to_something
1658 t infty expty subst metasenv context ugraph (*}}}*)
1660 debug_print (lazy ("COERCE TO SOMETHING END: "^
1661 CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1665 coerce_to_something_aux t infty expty subst metasenv context ugraph
1666 with Uncertain _ | RefineFailure _ as exn ->
1669 CicMetaSubst.ppterm_in_context metasenv subst t context ^
1670 " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1671 infty context ^ " but is here used with type " ^
1672 CicMetaSubst.ppterm_in_context metasenv subst expty context)
1674 enrich localization_tbl ~f t exn
1676 and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1677 match CicReduction.whd ~delta:false ~subst context infty with
1678 | Cic.Meta _ | Cic.Sort _ ->
1679 t,infty, subst, metasenv, ugraph
1681 debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1682 ~metasenv subst src context));
1683 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1685 let (t, ty_t), subst, metasenv, ugraph =
1686 coerce_to_something true
1687 localization_tbl t src tgt subst metasenv context ugraph
1689 debug_print (lazy ("COERCE TO SORT END: "^
1690 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1691 t, ty_t, subst, metasenv, ugraph
1692 with HExtlib.Localized (_, exn) ->
1694 lazy ("(7)The term " ^
1695 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1696 ^ " is not a type since it has type " ^
1697 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1698 ^ " that is not a sort")
1700 enrich localization_tbl ~f t exn
1703 (* eat prods ends here! *)
1705 let t',ty,subst',metasenv',ugraph1 =
1706 type_of_aux [] metasenv context t ugraph
1708 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1709 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1710 (* Andrea: ho rimesso qui l'applicazione della subst al
1711 metasenv dopo che ho droppato l'invariante che il metsaenv
1712 e' sempre istanziato *)
1713 let substituted_metasenv =
1714 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1716 (* substituted_t,substituted_ty,substituted_metasenv *)
1717 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1719 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1721 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1722 let cleaned_metasenv =
1724 (function (n,context,ty) ->
1725 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1730 | Some (n, Cic.Decl t) ->
1732 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1733 | Some (n, Cic.Def (bo,ty)) ->
1734 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1739 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1741 Some (n, Cic.Def (bo',ty'))
1745 ) substituted_metasenv
1747 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1750 let undebrujin uri typesno tys t =
1753 (fun (name,_,_,_) (i,t) ->
1754 (* here the explicit_named_substituion is assumed to be *)
1756 let t' = Cic.MutInd (uri,i,[]) in
1757 let t = CicSubstitution.subst t' t in
1759 ) tys (typesno - 1,t))
1761 let map_first_n n start f g l =
1762 let rec aux acc k l =
1765 | [] -> raise (Invalid_argument "map_first_n")
1766 | hd :: tl -> f hd k (aux acc (k+1) tl)
1772 (*CSC: this is a very rough approximation; to be finished *)
1773 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1774 let subst,metasenv,ugraph,tys =
1776 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1777 let subst,metasenv,ugraph,cl =
1779 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1780 let rec aux ctx k subst = function
1781 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1782 let subst,metasenv,ugraph,tl =
1784 (subst,metasenv,ugraph,[])
1785 (fun t n (subst,metasenv,ugraph,acc) ->
1786 let subst,metasenv,ugraph =
1788 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1790 subst,metasenv,ugraph,(t::acc))
1791 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1794 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1795 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1796 subst,metasenv,ugraph,t
1797 | Cic.Prod (name,s,t) ->
1798 let ctx = (Some (name,Cic.Decl s))::ctx in
1799 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1800 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1804 (lazy "not well formed constructor type"))
1806 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1807 subst,metasenv,ugraph,(name,ty) :: acc)
1808 cl (subst,metasenv,ugraph,[])
1810 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1811 tys ([],metasenv,ugraph,[])
1813 let substituted_tys =
1815 (fun (name,ind,arity,cl) ->
1817 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1819 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1822 metasenv,ugraph,substituted_tys
1824 let typecheck metasenv uri obj ~localization_tbl =
1825 let ugraph = CicUniv.empty_ugraph in
1827 Cic.Constant (name,Some bo,ty,args,attrs) ->
1828 let bo',boty,metasenv,ugraph =
1829 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1830 let ty',_,metasenv,ugraph =
1831 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1832 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1833 let bo' = CicMetaSubst.apply_subst subst bo' in
1834 let ty' = CicMetaSubst.apply_subst subst ty' in
1835 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1836 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1837 | Cic.Constant (name,None,ty,args,attrs) ->
1838 let ty',_,metasenv,ugraph =
1839 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1841 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1842 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1843 assert (metasenv' = metasenv);
1844 (* Here we do not check the metasenv for correctness *)
1845 let bo',boty,metasenv,ugraph =
1846 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1847 let ty',sort,metasenv,ugraph =
1848 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1852 (* instead of raising Uncertain, let's hope that the meta will become
1855 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1857 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1858 let bo' = CicMetaSubst.apply_subst subst bo' in
1859 let ty' = CicMetaSubst.apply_subst subst ty' in
1860 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1861 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1862 | Cic.Variable _ -> assert false (* not implemented *)
1863 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1864 (*CSC: this code is greately simplified and many many checks are missing *)
1865 (*CSC: e.g. the constructors are not required to build their own types, *)
1866 (*CSC: the arities are not required to have as type a sort, etc. *)
1867 let uri = match uri with Some uri -> uri | None -> assert false in
1868 let typesno = List.length tys in
1869 (* first phase: we fix only the types *)
1870 let metasenv,ugraph,tys =
1872 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1873 let ty',_,metasenv,ugraph =
1874 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1876 metasenv,ugraph,(name,b,ty',cl)::res
1877 ) tys (metasenv,ugraph,[]) in
1879 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1880 (* second phase: we fix only the constructors *)
1881 let saved_menv = metasenv in
1882 let metasenv,ugraph,tys =
1884 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1885 let metasenv,ugraph,cl' =
1887 (fun (name,ty) (metasenv,ugraph,res) ->
1889 CicTypeChecker.debrujin_constructor
1890 ~cb:(relocalize localization_tbl) uri typesno ty in
1891 let ty',_,metasenv,ugraph =
1892 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1893 let ty' = undebrujin uri typesno tys ty' in
1894 metasenv@saved_menv,ugraph,(name,ty')::res
1895 ) cl (metasenv,ugraph,[])
1897 metasenv,ugraph,(name,b,ty,cl')::res
1898 ) tys (metasenv,ugraph,[]) in
1899 (* third phase: we check the positivity condition *)
1900 let metasenv,ugraph,tys =
1901 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1903 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1906 (* sara' piu' veloce che raffinare da zero? mah.... *)
1907 let pack_coercion metasenv ctx t =
1908 let module C = Cic in
1909 let rec merge_coercions ctx =
1910 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1912 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1913 | C.Meta (n,subst) ->
1916 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1919 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1920 | C.Prod (name,so,dest) ->
1921 let ctx' = (Some (name,C.Decl so))::ctx in
1922 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1923 | C.Lambda (name,so,dest) ->
1924 let ctx' = (Some (name,C.Decl so))::ctx in
1925 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1926 | C.LetIn (name,so,dest) ->
1927 let _,ty,metasenv,ugraph =
1928 pack_coercions := false;
1929 type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1930 pack_coercions := true;
1931 let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1932 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1934 let l = List.map (merge_coercions ctx) l in
1936 let b,_,_,_,_ = is_a_double_coercion t in
1938 let ugraph = CicUniv.oblivion_ugraph in
1939 let old_insert_coercions = !insert_coercions in
1940 insert_coercions := false;
1941 let newt, _, menv, _ =
1943 type_of_aux' metasenv ctx t ugraph
1944 with RefineFailure _ | Uncertain _ ->
1947 insert_coercions := old_insert_coercions;
1948 if metasenv <> [] || menv = [] then
1951 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1954 | C.Var (uri,exp_named_subst) ->
1955 let exp_named_subst = List.map aux exp_named_subst in
1956 C.Var (uri, exp_named_subst)
1957 | C.Const (uri,exp_named_subst) ->
1958 let exp_named_subst = List.map aux exp_named_subst in
1959 C.Const (uri, exp_named_subst)
1960 | C.MutInd (uri,tyno,exp_named_subst) ->
1961 let exp_named_subst = List.map aux exp_named_subst in
1962 C.MutInd (uri,tyno,exp_named_subst)
1963 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1964 let exp_named_subst = List.map aux exp_named_subst in
1965 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1966 | C.MutCase (uri,tyno,out,te,pl) ->
1967 let pl = List.map (merge_coercions ctx) pl in
1968 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1969 | C.Fix (fno, fl) ->
1972 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1977 (fun (name,idx,ty,bo) ->
1978 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1982 | C.CoFix (fno, fl) ->
1985 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1990 (fun (name,ty,bo) ->
1991 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1996 merge_coercions ctx t
1999 let pack_coercion_metasenv conjectures = conjectures (*
2001 TASSI: this code war written when coercions were a toy,
2002 now packing coercions involves unification thus
2003 the metasenv may change, and this pack coercion
2004 does not handle that.
2006 let module C = Cic in
2008 (fun (i, ctx, ty) ->
2014 Some (name, C.Decl t) ->
2015 Some (name, C.Decl (pack_coercion conjectures ctx t))
2016 | Some (name, C.Def (t,None)) ->
2017 Some (name,C.Def (pack_coercion conjectures ctx t,None))
2018 | Some (name, C.Def (t,Some ty)) ->
2019 Some (name, C.Def (pack_coercion conjectures ctx t,
2020 Some (pack_coercion conjectures ctx ty)))
2026 ((i,ctx,pack_coercion conjectures ctx ty))
2031 let pack_coercion_obj obj = obj (*
2033 TASSI: this code war written when coercions were a toy,
2034 now packing coercions involves unification thus
2035 the metasenv may change, and this pack coercion
2036 does not handle that.
2038 let module C = Cic in
2040 | C.Constant (id, body, ty, params, attrs) ->
2044 | Some body -> Some (pack_coercion [] [] body)
2046 let ty = pack_coercion [] [] ty in
2047 C.Constant (id, body, ty, params, attrs)
2048 | C.Variable (name, body, ty, params, attrs) ->
2052 | Some body -> Some (pack_coercion [] [] body)
2054 let ty = pack_coercion [] [] ty in
2055 C.Variable (name, body, ty, params, attrs)
2056 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2057 let conjectures = pack_coercion_metasenv conjectures in
2058 let body = pack_coercion conjectures [] body in
2059 let ty = pack_coercion conjectures [] ty in
2060 C.CurrentProof (name, conjectures, body, ty, params, attrs)
2061 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2064 (fun (name, ind, arity, cl) ->
2065 let arity = pack_coercion [] [] arity in
2067 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2069 (name, ind, arity, cl))
2072 C.InductiveDefinition (indtys, params, leftno, attrs) *)
2077 let type_of_aux' metasenv context term =
2080 type_of_aux' metasenv context term in
2082 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2084 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2087 | RefineFailure msg as e ->
2088 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2090 | Uncertain msg as e ->
2091 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2095 let profiler2 = HExtlib.profile "CicRefine"
2097 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2098 profiler2.HExtlib.profile
2099 (type_of_aux' ?localization_tbl metasenv context term) ugraph
2101 let typecheck ~localization_tbl metasenv uri obj =
2102 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2104 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2105 (* vim:set foldmethod=marker: *)