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 let insert_coercions = ref true
35 let pack_coercions = ref true
37 let debug_print = fun _ -> ();;
38 (*let debug_print x = prerr_endline (Lazy.force x);;*)
40 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
42 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
45 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
46 in profiler_eat_prods2.HExtlib.profile foo ()
48 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
49 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
52 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
54 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
57 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
58 in profiler_eat_prods.HExtlib.profile foo ()
60 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
61 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
64 let profiler = HExtlib.profile "CicRefine.fo_unif"
66 let fo_unif_subst subst context metasenv t1 t2 ugraph =
69 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
70 in profiler.HExtlib.profile foo ()
72 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
73 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
76 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
79 RefineFailure msg -> RefineFailure (f msg)
80 | Uncertain msg -> Uncertain (f msg)
81 | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
82 | Sys.Break -> raise exn
83 | _ -> prerr_endline (Printexc.to_string exn); assert false
87 Cic.CicHash.find localization_tbl t
89 prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
92 raise (HExtlib.Localized (loc,exn'))
94 let relocalize localization_tbl oldt newt =
96 let infos = Cic.CicHash.find localization_tbl oldt in
97 Cic.CicHash.remove localization_tbl oldt;
98 Cic.CicHash.add localization_tbl newt infos;
106 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
107 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
110 let exp_impl metasenv subst context =
113 let (metasenv', idx) =
114 CicMkImplicit.mk_implicit_type metasenv subst context in
116 CicMkImplicit.identity_relocation_list_for_metavariable context in
117 metasenv', Cic.Meta (idx, irl)
119 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
120 metasenv', Cic.Meta (idx, [])
122 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
124 CicMkImplicit.identity_relocation_list_for_metavariable context in
125 metasenv', Cic.Meta (idx, irl)
129 let is_a_double_coercion t =
131 let rec aux acc = function
133 | x::tl -> aux (acc@[x]) tl
138 let imp = Cic.Implicit None in
139 let dummyres = false,imp, imp,imp,imp in
141 | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
142 (match last_of tl with
143 | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
144 let sib2,head = last_of tl2 in
145 true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
150 let more_args_than_expected
151 localization_tbl metasenv subst he context hetype' tlbody_and_type exn
155 CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
156 " (that has type "^CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
157 ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
158 " arguments that are more than expected")
160 enrich localization_tbl he ~f:(fun _-> msg) exn
163 let mk_prod_of_metas metasenv context' subst args =
164 let rec mk_prod metasenv context' = function
166 let (metasenv, idx) =
167 CicMkImplicit.mk_implicit_type metasenv subst context'
170 CicMkImplicit.identity_relocation_list_for_metavariable context'
172 metasenv,Cic.Meta (idx, irl)
174 let (metasenv, idx) =
175 CicMkImplicit.mk_implicit_type metasenv subst context'
178 CicMkImplicit.identity_relocation_list_for_metavariable context'
180 let meta = Cic.Meta (idx,irl) in
182 (* The name must be fresh for context. *)
183 (* Nevertheless, argty is well-typed only in context. *)
184 (* Thus I generate a name (name_hint) in context and *)
185 (* then I generate a name --- using the hint name_hint *)
186 (* --- that is fresh in context'. *)
188 (* Cic.Name "pippo" *)
189 FreshNamesGenerator.mk_fresh_name ~subst metasenv
190 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
191 (CicMetaSubst.apply_subst_context subst context')
193 ~typ:(CicMetaSubst.apply_subst subst argty)
195 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
196 FreshNamesGenerator.mk_fresh_name ~subst
197 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
199 let metasenv,target =
200 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
202 metasenv,Cic.Prod (name,meta,target)
204 mk_prod metasenv context' args
207 let rec type_of_constant uri ugraph =
208 let module C = Cic in
209 let module R = CicReduction in
210 let module U = UriManager in
211 let _ = CicTypeChecker.typecheck uri in
214 CicEnvironment.get_cooked_obj ugraph uri
215 with Not_found -> assert false
218 C.Constant (_,_,ty,_,_) -> ty,u
219 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
223 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
225 and type_of_variable uri ugraph =
226 let module C = Cic in
227 let module R = CicReduction in
228 let module U = UriManager in
229 let _ = CicTypeChecker.typecheck uri in
232 CicEnvironment.get_cooked_obj ugraph uri
233 with Not_found -> assert false
236 C.Variable (_,_,ty,_,_) -> ty,u
240 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
242 and type_of_mutual_inductive_defs uri i ugraph =
243 let module C = Cic in
244 let module R = CicReduction in
245 let module U = UriManager in
246 let _ = CicTypeChecker.typecheck uri in
249 CicEnvironment.get_cooked_obj ugraph uri
250 with Not_found -> assert false
253 C.InductiveDefinition (dl,_,_,_) ->
254 let (_,_,arity,_) = List.nth dl i in
259 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
261 and type_of_mutual_inductive_constr uri i j ugraph =
262 let module C = Cic in
263 let module R = CicReduction in
264 let module U = UriManager in
265 let _ = CicTypeChecker.typecheck uri in
268 CicEnvironment.get_cooked_obj ugraph uri
269 with Not_found -> assert false
272 C.InductiveDefinition (dl,_,_,_) ->
273 let (_,_,_,cl) = List.nth dl i in
274 let (_,ty) = List.nth cl (j-1) in
280 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
283 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
285 (* the check_branch function checks if a branch of a case is refinable.
286 It returns a pair (outype_instance,args), a subst and a metasenv.
287 outype_instance is the expected result of applying the case outtype
289 The problem is that outype is in general unknown, and we should
290 try to synthesize it from the above information, that is in general
291 a second order unification problem. *)
293 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
294 let module C = Cic in
295 (* let module R = CicMetaSubst in *)
296 let module R = CicReduction in
297 match R.whd ~subst context expectedtype with
299 (n,context,actualtype, [term]), subst, metasenv, ugraph
300 | C.Appl (C.MutInd (_,_,_)::tl) ->
301 let (_,arguments) = split tl left_args_no in
302 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
303 | C.Prod (name,so,de) ->
304 (* we expect that the actual type of the branch has the due
306 (match R.whd ~subst context actualtype with
307 C.Prod (name',so',de') ->
308 let subst, metasenv, ugraph1 =
309 fo_unif_subst subst context metasenv so so' ugraph in
311 (match CicSubstitution.lift 1 term with
312 C.Appl l -> C.Appl (l@[C.Rel 1])
313 | t -> C.Appl [t ; C.Rel 1]) in
314 (* we should also check that the name variable is anonymous in
315 the actual type de' ?? *)
317 ((Some (name,(C.Decl so)))::context)
318 metasenv subst left_args_no de' term' de ugraph1
319 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
320 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
322 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
325 let rec type_of_aux subst metasenv context t ugraph =
326 let module C = Cic in
327 let module S = CicSubstitution in
328 let module U = UriManager in
330 let try_coercion t subst context ugraph coercion_tgt (metasenv,last,coerced) =
331 let subst,metasenv,ugraph =
332 fo_unif_subst subst context metasenv last t ugraph
335 let newt, tty, subst, metasenv, ugraph =
336 avoid_double_coercion context subst metasenv ugraph coerced
339 Some (newt, tty, subst, metasenv, ugraph)
341 | RefineFailure _ | Uncertain _ -> None
344 let (t',_,_,_,_) as res =
349 match List.nth context (n - 1) with
350 Some (_,C.Decl ty) ->
351 t,S.lift n ty,subst,metasenv, ugraph
352 | Some (_,C.Def (_,Some ty)) ->
353 t,S.lift n ty,subst,metasenv, ugraph
354 | Some (_,C.Def (bo,None)) ->
356 (* if it is in the context it must be already well-typed*)
357 CicTypeChecker.type_of_aux' ~subst metasenv context
360 t,ty,subst,metasenv,ugraph
362 enrich localization_tbl t
363 (RefineFailure (lazy "Rel to hidden hypothesis"))
366 enrich localization_tbl t
367 (RefineFailure (lazy "Not a closed term")))
368 | C.Var (uri,exp_named_subst) ->
369 let exp_named_subst',subst',metasenv',ugraph1 =
370 check_exp_named_subst
371 subst metasenv context exp_named_subst ugraph
373 let ty_uri,ugraph1 = type_of_variable uri ugraph in
375 CicSubstitution.subst_vars exp_named_subst' ty_uri
377 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
380 let (canonical_context, term,ty) =
381 CicUtil.lookup_subst n subst
383 let l',subst',metasenv',ugraph1 =
384 check_metasenv_consistency n subst metasenv context
385 canonical_context l ugraph
387 (* trust or check ??? *)
388 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
389 subst', metasenv', ugraph1
390 (* type_of_aux subst metasenv
391 context (CicSubstitution.subst_meta l term) *)
392 with CicUtil.Subst_not_found _ ->
393 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
394 let l',subst',metasenv', ugraph1 =
395 check_metasenv_consistency n subst metasenv context
396 canonical_context l ugraph
398 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
399 subst', metasenv',ugraph1)
400 | C.Sort (C.Type tno) ->
401 let tno' = CicUniv.fresh() in
403 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
404 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
406 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
408 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
409 | C.Implicit infos ->
410 let metasenv',t' = exp_impl metasenv subst context infos in
411 type_of_aux subst metasenv' context t' ugraph
413 let ty',_,subst',metasenv',ugraph1 =
414 type_of_aux subst metasenv context ty ugraph
416 let te',inferredty,subst'',metasenv'',ugraph2 =
417 type_of_aux subst' metasenv' context te ugraph1
419 let (te', ty'), subst''',metasenv''',ugraph3 =
420 coerce_to_something true localization_tbl te' inferredty ty'
421 subst'' metasenv'' context ugraph2
423 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
424 | C.Prod (name,s,t) ->
425 let s',sort1,subst',metasenv',ugraph1 =
426 type_of_aux subst metasenv context s ugraph
428 let s',sort1,subst', metasenv',ugraph1 =
429 coerce_to_sort localization_tbl
430 s' sort1 subst' context metasenv' ugraph1
432 let context_for_t = ((Some (name,(C.Decl s')))::context) in
433 let t',sort2,subst'',metasenv'',ugraph2 =
434 type_of_aux subst' metasenv'
435 context_for_t t ugraph1
437 let t',sort2,subst'',metasenv'',ugraph2 =
438 coerce_to_sort localization_tbl
439 t' sort2 subst'' context_for_t metasenv'' ugraph2
441 let sop,subst''',metasenv''',ugraph3 =
442 sort_of_prod localization_tbl subst'' metasenv''
443 context (name,s') t' (sort1,sort2) ugraph2
445 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
446 | C.Lambda (n,s,t) ->
447 let s',sort1,subst',metasenv',ugraph1 =
448 type_of_aux subst metasenv context s ugraph
450 let s',sort1,subst',metasenv',ugraph1 =
451 coerce_to_sort localization_tbl
452 s' sort1 subst' context metasenv' ugraph1
454 let context_for_t = ((Some (n,(C.Decl s')))::context) in
455 let t',type2,subst'',metasenv'',ugraph2 =
456 type_of_aux subst' metasenv' context_for_t t ugraph1
458 C.Lambda (n,s',t'),C.Prod (n,s',type2),
459 subst'',metasenv'',ugraph2
461 (* only to check if s is well-typed *)
462 let s',ty,subst',metasenv',ugraph1 =
463 type_of_aux subst metasenv context s ugraph
465 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
467 let t',inferredty,subst'',metasenv'',ugraph2 =
468 type_of_aux subst' metasenv'
469 context_for_t t ugraph1
471 (* One-step LetIn reduction.
472 * Even faster than the previous solution.
473 * Moreover the inferred type is closer to the expected one.
476 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
477 subst'',metasenv'',ugraph2
478 | C.Appl (he::((_::_) as tl)) ->
479 let he',hetype,subst',metasenv',ugraph1 =
480 type_of_aux subst metasenv context he ugraph
482 let tlbody_and_type,subst'',metasenv'',ugraph2 =
483 typeof_list subst' metasenv' context ugraph1 tl
485 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
486 eat_prods true subst'' metasenv'' context
487 he' hetype tlbody_and_type ugraph2
489 let newappl = (C.Appl (coerced_he::coerced_args)) in
490 avoid_double_coercion
491 context subst''' metasenv''' ugraph3 newappl applty
492 | C.Appl _ -> assert false
493 | C.Const (uri,exp_named_subst) ->
494 let exp_named_subst',subst',metasenv',ugraph1 =
495 check_exp_named_subst subst metasenv context
496 exp_named_subst ugraph in
497 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
499 CicSubstitution.subst_vars exp_named_subst' ty_uri
501 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
502 | C.MutInd (uri,i,exp_named_subst) ->
503 let exp_named_subst',subst',metasenv',ugraph1 =
504 check_exp_named_subst subst metasenv context
505 exp_named_subst ugraph
507 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
509 CicSubstitution.subst_vars exp_named_subst' ty_uri in
510 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
511 | C.MutConstruct (uri,i,j,exp_named_subst) ->
512 let exp_named_subst',subst',metasenv',ugraph1 =
513 check_exp_named_subst subst metasenv context
514 exp_named_subst ugraph
517 type_of_mutual_inductive_constr uri i j ugraph1
520 CicSubstitution.subst_vars exp_named_subst' ty_uri
522 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
524 | C.MutCase (uri, i, outtype, term, pl) ->
525 (* first, get the inductive type (and noparams)
526 * in the environment *)
527 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
528 let _ = CicTypeChecker.typecheck uri in
529 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
531 C.InductiveDefinition (l,expl_params,parsno,_) ->
532 List.nth l i , expl_params, parsno, u
534 enrich localization_tbl t
536 (lazy ("Unkown mutual inductive definition " ^
537 U.string_of_uri uri)))
539 let rec count_prod t =
540 match CicReduction.whd ~subst context t with
541 C.Prod (_, _, t) -> 1 + (count_prod t)
544 let no_args = count_prod arity in
545 (* now, create a "generic" MutInd *)
546 let metasenv,left_args =
547 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
549 let metasenv,right_args =
550 let no_right_params = no_args - no_left_params in
551 if no_right_params < 0 then assert false
552 else CicMkImplicit.n_fresh_metas
553 metasenv subst context no_right_params
555 let metasenv,exp_named_subst =
556 CicMkImplicit.fresh_subst metasenv subst context expl_params in
559 C.MutInd (uri,i,exp_named_subst)
562 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
564 (* check consistency with the actual type of term *)
565 let term',actual_type,subst,metasenv,ugraph1 =
566 type_of_aux subst metasenv context term ugraph in
567 let expected_type',_, subst, metasenv,ugraph2 =
568 type_of_aux subst metasenv context expected_type ugraph1
570 let actual_type = CicReduction.whd ~subst context actual_type in
571 let subst,metasenv,ugraph3 =
573 fo_unif_subst subst context metasenv
574 expected_type' actual_type ugraph2
577 enrich localization_tbl term' exn
579 lazy ("(10)The term " ^
580 CicMetaSubst.ppterm_in_context ~metasenv subst term'
581 context ^ " has type " ^
582 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
583 context ^ " but is here used with type " ^
584 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
586 let rec instantiate_prod t =
590 match CicReduction.whd ~subst context t with
592 instantiate_prod (CicSubstitution.subst he t') tl
595 let arity_instantiated_with_left_args =
596 instantiate_prod arity left_args in
597 (* TODO: check if the sort elimination
598 * is allowed: [(I q1 ... qr)|B] *)
599 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
601 (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
603 if left_args = [] then
604 (C.MutConstruct (uri,i,j,exp_named_subst))
607 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
609 let p',actual_type,subst,metasenv,ugraph1 =
610 type_of_aux subst metasenv context p ugraph
612 let constructor',expected_type, subst, metasenv,ugraph2 =
613 type_of_aux subst metasenv context constructor ugraph1
615 let outtypeinstance,subst,metasenv,ugraph3 =
617 check_branch 0 context metasenv subst
618 no_left_params actual_type constructor' expected_type
622 enrich localization_tbl constructor'
624 lazy ("(11)The term " ^
625 CicMetaSubst.ppterm_in_context metasenv subst p'
626 context ^ " has type " ^
627 CicMetaSubst.ppterm_in_context metasenv subst actual_type
628 context ^ " but is here used with type " ^
629 CicMetaSubst.ppterm_in_context metasenv subst expected_type
633 outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
634 pl ([],List.length pl,[],subst,metasenv,ugraph3)
637 (* we are left to check that the outype matches his instances.
638 The easy case is when the outype is specified, that amount
639 to a trivial check. Otherwise, we should guess a type from
643 let outtype,outtypety, subst, metasenv,ugraph4 =
644 type_of_aux subst metasenv context outtype ugraph4 in
647 (let candidate,ugraph5,metasenv,subst =
648 let exp_name_subst, metasenv =
650 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
652 let uris = CicUtil.params_of_obj o in
654 fun uri (acc,metasenv) ->
655 let metasenv',new_meta =
656 CicMkImplicit.mk_implicit metasenv subst context
659 CicMkImplicit.identity_relocation_list_for_metavariable
662 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
666 match left_args,right_args with
667 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
669 let rec mk_right_args =
672 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
674 let right_args_no = List.length right_args in
675 let lifted_left_args =
676 List.map (CicSubstitution.lift right_args_no) left_args
678 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
679 (lifted_left_args @ mk_right_args right_args_no))
682 FreshNamesGenerator.mk_fresh_name ~subst metasenv
683 context Cic.Anonymous ~typ:ty
685 match outtypeinstances with
687 let extended_context =
688 let rec add_right_args =
690 Cic.Prod (name,ty,t) ->
691 Some (name,Cic.Decl ty)::(add_right_args t)
694 (Some (fresh_name,Cic.Decl ty))::
696 (add_right_args arity_instantiated_with_left_args))@
699 let metasenv,new_meta =
700 CicMkImplicit.mk_implicit metasenv subst extended_context
703 CicMkImplicit.identity_relocation_list_for_metavariable
706 let rec add_lambdas b =
708 Cic.Prod (name,ty,t) ->
709 Cic.Lambda (name,ty,(add_lambdas b t))
710 | _ -> Cic.Lambda (fresh_name, ty, b)
713 add_lambdas (Cic.Meta (new_meta,irl))
714 arity_instantiated_with_left_args
716 (Some candidate),ugraph4,metasenv,subst
717 | (constructor_args_no,_,instance,_)::tl ->
719 let instance',subst,metasenv =
720 CicMetaSubst.delift_rels subst metasenv
721 constructor_args_no instance
723 let candidate,ugraph,metasenv,subst =
725 fun (candidate_oty,ugraph,metasenv,subst)
726 (constructor_args_no,_,instance,_) ->
727 match candidate_oty with
728 | None -> None,ugraph,metasenv,subst
731 let instance',subst,metasenv =
732 CicMetaSubst.delift_rels subst metasenv
733 constructor_args_no instance
735 let subst,metasenv,ugraph =
736 fo_unif_subst subst context metasenv
739 candidate_oty,ugraph,metasenv,subst
741 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
742 | RefineFailure _ | Uncertain _ ->
743 None,ugraph,metasenv,subst
744 ) (Some instance',ugraph4,metasenv,subst) tl
747 | None -> None, ugraph,metasenv,subst
749 let rec add_lambdas n b =
751 Cic.Prod (name,ty,t) ->
752 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
754 Cic.Lambda (fresh_name, ty,
755 CicSubstitution.lift (n + 1) t)
758 (add_lambdas 0 t arity_instantiated_with_left_args),
759 ugraph,metasenv,subst
760 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
761 None,ugraph4,metasenv,subst
764 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
766 let subst,metasenv,ugraph =
768 fo_unif_subst subst context metasenv
769 candidate outtype ugraph5
771 exn -> assert false(* unification against a metavariable *)
773 C.MutCase (uri, i, outtype, term', pl'),
774 CicReduction.head_beta_reduce
775 (CicMetaSubst.apply_subst subst
776 (Cic.Appl (outtype::right_args@[term']))),
777 subst,metasenv,ugraph)
778 | _ -> (* easy case *)
779 let tlbody_and_type,subst,metasenv,ugraph4 =
780 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
782 let _,_,_,subst,metasenv,ugraph4 =
783 eat_prods false subst metasenv context
784 outtype outtypety tlbody_and_type ugraph4
786 let _,_, subst, metasenv,ugraph5 =
787 type_of_aux subst metasenv context
788 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
790 let (subst,metasenv,ugraph6) =
792 (fun (subst,metasenv,ugraph)
793 p (constructor_args_no,context,instance,args)
798 CicSubstitution.lift constructor_args_no outtype
800 C.Appl (outtype'::args)
802 CicReduction.whd ~subst context appl
805 fo_unif_subst subst context metasenv instance instance'
809 enrich localization_tbl p exn
811 lazy ("(12)The term " ^
812 CicMetaSubst.ppterm_in_context ~metasenv subst p
813 context ^ " has type " ^
814 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
815 context ^ " but is here used with type " ^
816 CicMetaSubst.ppterm_in_context ~metasenv subst instance
818 (subst,metasenv,ugraph5) pl' outtypeinstances
820 C.MutCase (uri, i, outtype, term', pl'),
821 CicReduction.head_beta_reduce
822 (CicMetaSubst.apply_subst subst
823 (C.Appl(outtype::right_args@[term]))),
824 subst,metasenv,ugraph6)
826 let fl_ty',subst,metasenv,types,ugraph1,len =
828 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
829 let ty',_,subst',metasenv',ugraph1 =
830 type_of_aux subst metasenv context ty ugraph
832 fl @ [ty'],subst',metasenv',
833 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
834 :: types, ugraph, len+1
835 ) ([],subst,metasenv,[],ugraph,0) fl
837 let context' = types@context in
838 let fl_bo',subst,metasenv,ugraph2 =
840 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
841 let bo',ty_of_bo,subst,metasenv,ugraph1 =
842 type_of_aux subst metasenv context' bo ugraph in
843 let expected_ty = CicSubstitution.lift len ty in
844 let subst',metasenv',ugraph' =
846 fo_unif_subst subst context' metasenv
847 ty_of_bo expected_ty ugraph1
850 enrich localization_tbl bo exn
852 lazy ("(13)The term " ^
853 CicMetaSubst.ppterm_in_context ~metasenv subst bo
854 context' ^ " has type " ^
855 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
856 context' ^ " but is here used with type " ^
857 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
860 fl @ [bo'] , subst',metasenv',ugraph'
861 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
863 let ty = List.nth fl_ty' i in
864 (* now we have the new ty in fl_ty', the new bo in fl_bo',
865 * and we want the new fl with bo' and ty' injected in the right
868 let rec map3 f l1 l2 l3 =
871 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
874 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
877 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
879 let fl_ty',subst,metasenv,types,ugraph1,len =
881 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
882 let ty',_,subst',metasenv',ugraph1 =
883 type_of_aux subst metasenv context ty ugraph
885 fl @ [ty'],subst',metasenv',
886 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
887 types, ugraph1, len+1
888 ) ([],subst,metasenv,[],ugraph,0) fl
890 let context' = types@context in
891 let fl_bo',subst,metasenv,ugraph2 =
893 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
894 let bo',ty_of_bo,subst,metasenv,ugraph1 =
895 type_of_aux subst metasenv context' bo ugraph in
896 let expected_ty = CicSubstitution.lift len ty in
897 let subst',metasenv',ugraph' =
899 fo_unif_subst subst context' metasenv
900 ty_of_bo expected_ty ugraph1
903 enrich localization_tbl bo exn
905 lazy ("(14)The term " ^
906 CicMetaSubst.ppterm_in_context ~metasenv subst bo
907 context' ^ " has type " ^
908 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
909 context' ^ " but is here used with type " ^
910 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
913 fl @ [bo'],subst',metasenv',ugraph'
914 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
916 let ty = List.nth fl_ty' i in
917 (* now we have the new ty in fl_ty', the new bo in fl_bo',
918 * and we want the new fl with bo' and ty' injected in the right
921 let rec map3 f l1 l2 l3 =
924 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
927 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
930 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
932 relocalize localization_tbl t t';
935 (* check_metasenv_consistency checks that the "canonical" context of a
936 metavariable is consitent - up to relocation via the relocation list l -
937 with the actual context *)
938 and check_metasenv_consistency
939 metano subst metasenv context canonical_context l ugraph
941 let module C = Cic in
942 let module R = CicReduction in
943 let module S = CicSubstitution in
944 let lifted_canonical_context =
948 | (Some (n,C.Decl t))::tl ->
949 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
950 | (Some (n,C.Def (t,None)))::tl ->
951 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
952 | None::tl -> None::(aux (i+1) tl)
953 | (Some (n,C.Def (t,Some ty)))::tl ->
955 C.Def ((S.subst_meta l (S.lift i t)),
956 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
958 aux 1 canonical_context
962 (fun (l,subst,metasenv,ugraph) t ct ->
965 l @ [None],subst,metasenv,ugraph
966 | Some t,Some (_,C.Def (ct,_)) ->
967 let subst',metasenv',ugraph' =
969 prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
970 fo_unif_subst subst context metasenv t ct ugraph
971 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))))))
973 l @ [Some t],subst',metasenv',ugraph'
974 | Some t,Some (_,C.Decl ct) ->
975 let t',inferredty,subst',metasenv',ugraph1 =
976 type_of_aux subst metasenv context t ugraph
978 let subst'',metasenv'',ugraph2 =
981 subst' context metasenv' inferredty ct ugraph1
982 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))))))
984 l @ [Some t'], subst'',metasenv'',ugraph2
986 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
988 Invalid_argument _ ->
992 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
993 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
994 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
996 and check_exp_named_subst metasubst metasenv context tl ugraph =
997 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
999 [] -> [],metasubst,metasenv,ugraph
1001 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1003 CicSubstitution.subst_vars substs ty_uri in
1004 (* CSC: why was this code here? it is wrong
1005 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1006 Cic.Variable (_,Some bo,_,_) ->
1008 (RefineFailure (lazy
1009 "A variable with a body can not be explicit substituted"))
1010 | Cic.Variable (_,None,_,_) -> ()
1013 (RefineFailure (lazy
1014 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1017 let t',typeoft,metasubst',metasenv',ugraph2 =
1018 type_of_aux metasubst metasenv context t ugraph1 in
1019 let subst = uri,t' in
1020 let metasubst'',metasenv'',ugraph3 =
1023 metasubst' context metasenv' typeoft typeofvar ugraph2
1025 raise (RefineFailure (lazy
1026 ("Wrong Explicit Named Substitution: " ^
1027 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1028 " not unifiable with " ^
1029 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1031 (* FIXME: no mere tail recursive! *)
1032 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1033 check_exp_named_subst_aux
1034 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1036 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1038 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1041 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1044 let module C = Cic in
1045 let context_for_t2 = (Some (name,C.Decl s))::context in
1046 let t1'' = CicReduction.whd ~subst context t1 in
1047 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1048 match (t1'', t2'') with
1049 (C.Sort s1, C.Sort s2)
1050 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1051 (* different than Coq manual!!! *)
1052 C.Sort s2,subst,metasenv,ugraph
1053 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1054 let t' = CicUniv.fresh() in
1056 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1057 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1058 C.Sort (C.Type t'),subst,metasenv,ugraph2
1060 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1061 | (C.Sort _,C.Sort (C.Type t1)) ->
1062 C.Sort (C.Type t1),subst,metasenv,ugraph
1063 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1064 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1065 (* TODO how can we force the meta to become a sort? If we don't we
1066 * break the invariant that refine produce only well typed terms *)
1067 (* TODO if we check the non meta term and if it is a sort then we
1068 * are likely to know the exact value of the result e.g. if the rhs
1069 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1070 let (metasenv,idx) =
1071 CicMkImplicit.mk_implicit_sort metasenv subst in
1072 let (subst, metasenv,ugraph1) =
1074 fo_unif_subst subst context_for_t2 metasenv
1075 (C.Meta (idx,[])) t2'' ugraph
1076 with _ -> assert false (* unification against a metavariable *)
1078 t2'',subst,metasenv,ugraph1
1081 enrich localization_tbl s
1085 "%s is supposed to be a type, but its type is %s"
1086 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1087 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1089 enrich localization_tbl t
1093 "%s is supposed to be a type, but its type is %s"
1094 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1095 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1097 and avoid_double_coercion context subst metasenv ugraph t ty =
1098 if not !pack_coercions then
1099 t,ty,subst,metasenv,ugraph
1101 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1103 let source_carr = CoercGraph.source_of c2 in
1104 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1105 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1107 | CoercGraph.SomeCoercion candidates ->
1109 HExtlib.list_findopt
1110 (function (metasenv,last,c) ->
1112 | c when not (CoercGraph.is_composite c) ->
1113 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1116 let subst,metasenv,ugraph =
1117 fo_unif_subst subst context metasenv last head ugraph in
1118 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1123 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1124 let newt,_,subst,metasenv,ugraph =
1125 type_of_aux subst metasenv context c ugraph in
1126 debug_print (lazy "tipa...");
1127 let subst, metasenv, ugraph =
1128 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1129 fo_unif_subst subst context metasenv newt t ugraph
1131 debug_print (lazy "unifica...");
1132 Some (newt, ty, subst, metasenv, ugraph)
1134 | RefineFailure s | Uncertain s when not !pack_coercions->
1135 debug_print s; debug_print (lazy "stop\n");None
1136 | RefineFailure s | Uncertain s ->
1137 debug_print s;debug_print (lazy "goon\n");
1139 let old_pack_coercions = !pack_coercions in
1140 pack_coercions := false; (* to avoid diverging *)
1141 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1142 type_of_aux subst metasenv context c1_c2_implicit ugraph
1144 pack_coercions := old_pack_coercions;
1146 is_a_double_coercion refined_c1_c2_implicit
1152 match refined_c1_c2_implicit with
1153 | Cic.Appl l -> HExtlib.list_last l
1156 let subst, metasenv, ugraph =
1157 try fo_unif_subst subst context metasenv
1159 with RefineFailure s| Uncertain s->
1160 debug_print s;assert false
1162 let subst, metasenv, ugraph =
1163 fo_unif_subst subst context metasenv
1164 refined_c1_c2_implicit t ugraph
1166 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1168 | RefineFailure s | Uncertain s ->
1169 pack_coercions := true;debug_print s;None
1170 | exn -> pack_coercions := true; raise exn))
1173 (match selected with
1177 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1178 t, ty, subst, metasenv, ugraph)
1179 | _ -> t, ty, subst, metasenv, ugraph)
1181 t, ty, subst, metasenv, ugraph
1183 and typeof_list subst metasenv context ugraph l =
1184 let tlbody_and_type,subst,metasenv,ugraph =
1186 (fun x (res,subst,metasenv,ugraph) ->
1187 let x',ty,subst',metasenv',ugraph1 =
1188 type_of_aux subst metasenv context x ugraph
1190 (x', ty)::res,subst',metasenv',ugraph1
1191 ) l ([],subst,metasenv,ugraph)
1193 tlbody_and_type,subst,metasenv,ugraph
1196 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1198 (* aux function to add coercions to funclass *)
1199 let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph =
1201 let pristinemenv = metasenv in
1202 let metasenv,hetype' =
1203 mk_prod_of_metas metasenv context subst args_bo_and_ty
1206 let subst,metasenv,ugraph =
1207 fo_unif_subst_eat_prods
1208 subst context metasenv hetype hetype' ugraph
1210 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1211 with RefineFailure s | Uncertain s as exn
1212 when allow_coercions && !insert_coercions ->
1213 (* {{{ we search a coercion of the head (saturated) to funclass *)
1214 let metasenv = pristinemenv in
1216 ("Fixing arity of: "^CicMetaSubst.ppterm ~metasenv subst hetype ^
1217 " since unif failed with: " ^ CicMetaSubst.ppterm ~metasenv subst hetype'
1218 (* ^ " cause: " ^ Lazy.force s *)));
1219 let how_many_args_are_needed =
1220 let rec aux n = function
1221 | Cic.Prod(_,_,t) -> aux (n+1) t
1224 aux 0 (CicMetaSubst.apply_subst subst hetype)
1226 let args, remainder =
1227 HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
1229 let args = List.map fst args in
1233 | Cic.Appl l -> Cic.Appl (l@args)
1234 | _ -> Cic.Appl (he::args)
1238 let x,xty,subst,metasenv,ugraph =
1239 (*CSC: here unsharing is necessary to avoid an unwanted
1240 relocalization. However, this also shows a great source of
1241 inefficiency: "x" is refined twice (once now and once in the
1242 subsequent eat_prods_and_args). Morevoer, how is divergence avoided?
1244 type_of_aux subst metasenv context (Unshare.unshare x) ugraph
1247 CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty)
1249 let carr_tgt = CoercDb.Fun 0 in
1250 match CoercGraph.look_for_coercion' metasenv subst context carr_src carr_tgt with
1251 | CoercGraph.NoCoercion
1252 | CoercGraph.NotMetaClosed
1253 | CoercGraph.NotHandled _ -> raise exn
1254 | CoercGraph.SomeCoercionToTgt candidates
1255 | CoercGraph.SomeCoercion candidates ->
1257 HExtlib.list_findopt
1258 (fun (metasenv,last,coerc) ->
1259 let subst,metasenv,ugraph =
1260 fo_unif_subst subst context metasenv last x ugraph in
1261 debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc));
1263 (* we want this to be available in the error handler fo the
1264 * following (so it has its own try. *)
1265 let t,tty,subst,metasenv,ugraph =
1266 type_of_aux subst metasenv context coerc ugraph
1269 let metasenv, hetype' =
1270 mk_prod_of_metas metasenv context subst remainder
1273 (" unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^
1274 CicMetaSubst.ppterm ~metasenv subst hetype'));
1275 let subst,metasenv,ugraph =
1276 fo_unif_subst_eat_prods
1277 subst context metasenv tty hetype' ugraph
1279 debug_print (lazy " success!");
1280 Some (subst,metasenv,ugraph,tty,t,remainder)
1282 | Uncertain _ | RefineFailure _ ->
1284 let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
1286 metasenv context subst t tty remainder ugraph
1288 Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
1289 with Uncertain _ | RefineFailure _ -> None
1293 | HExtlib.Localized (_,Uncertain _)
1294 | HExtlib.Localized (_,RefineFailure _) -> None
1295 | exn -> assert false) (* ritornare None, e' un localized *)
1298 | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
1299 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1301 more_args_than_expected localization_tbl metasenv
1302 subst he context hetype args_bo_and_ty exn
1303 (* }}} end coercion to funclass stuff *)
1304 (* }}} end fix_arity *)
1306 (* aux function to process the type of the head and the args in parallel *)
1307 let rec eat_prods_and_args
1308 pristinemenv metasenv subst context pristinehe he hetype ugraph newargs
1312 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1313 | (hete, hety)::tl ->
1314 match (CicReduction.whd ~subst context hetype) with
1315 | Cic.Prod (n,s,t) ->
1316 let arg,subst,metasenv,ugraph =
1317 coerce_to_something allow_coercions localization_tbl
1318 hete hety s subst metasenv context ugraph in
1320 pristinemenv metasenv subst context pristinehe he
1321 (CicSubstitution.subst (fst arg) t)
1322 ugraph (newargs@[arg]) tl
1325 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1327 pristinemenv context subst he hetype
1328 (newargs@[hete,hety]@tl) ugraph
1330 eat_prods_and_args metasenv
1331 metasenv subst context pristinehe he hetype'
1332 ugraph [] args_bo_and_ty
1333 with RefineFailure _ | Uncertain _ as exn ->
1334 (* unable to fix arity *)
1335 more_args_than_expected localization_tbl metasenv
1336 subst he context hetype args_bo_and_ty exn
1339 (* first we check if we are in the simple case of a meta closed term *)
1340 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1341 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1342 (* this optimization is to postpone fix_arity (the most common case)*)
1343 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1345 (* this (says CSC) is also useful to infer dependent types *)
1347 fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
1348 with RefineFailure _ | Uncertain _ as exn ->
1349 (* unable to fix arity *)
1350 more_args_than_expected localization_tbl metasenv
1351 subst he context hetype args_bo_and_ty exn
1353 let coerced_args,subst,metasenv,he,t,ugraph =
1355 metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
1357 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1359 and coerce_to_something
1360 allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1362 let module CS = CicSubstitution in
1363 let module CR = CicReduction in
1364 let cs_subst = CS.subst ~avoid_beta_redexes:true in
1365 let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1367 CoercGraph.look_for_coercion metasenv subst context infty expty
1370 | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
1371 "coerce_atom_to_something fails since not meta closed"))
1372 | CoercGraph.NoCoercion
1373 | CoercGraph.SomeCoercionToTgt _
1374 | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
1375 "coerce_atom_to_something fails since no coercions found"))
1376 | CoercGraph.SomeCoercion candidates ->
1377 let uncertain = ref false in
1379 (* HExtlib.list_findopt *)
1382 (fun (metasenv,last,c) ->
1384 let subst,metasenv,ugraph =
1385 fo_unif_subst subst context metasenv last t ugraph in
1386 let newt,newhety,subst,metasenv,ugraph =
1387 type_of_aux subst metasenv context c ugraph in
1388 let newt, newty, subst, metasenv, ugraph =
1389 avoid_double_coercion context subst metasenv ugraph newt expty
1391 let subst,metasenv,ugraph =
1392 fo_unif_subst subst context metasenv newhety expty ugraph in
1393 Some ((newt,newty), subst, metasenv, ugraph)
1395 | Uncertain _ -> uncertain := true; None
1396 | RefineFailure _ -> None)
1401 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1409 | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1410 | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1412 let rec coerce_to_something_aux
1413 t infty expty subst metasenv context ugraph
1416 let subst, metasenv, ugraph =
1417 fo_unif_subst subst context metasenv infty expty ugraph
1419 (t, expty), subst, metasenv, ugraph
1420 with Uncertain _ | RefineFailure _ as exn ->
1421 if not allow_coercions || not !insert_coercions then
1422 enrich localization_tbl t exn
1424 let whd = CicReduction.whd ~delta:false in
1425 let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1426 let infty = clean infty subst context in
1427 let expty = clean expty subst context in
1428 match infty, expty, t with
1429 | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2), Cic.Fix (n,fl) ->
1431 [name,i,_(* infty *),bo] ->
1433 Some (Cic.Name name,Cic.Decl expty)::context in
1434 let (rel1, _), subst, metasenv, ugraph =
1435 coerce_to_something_aux (Cic.Rel 1)
1436 (CS.lift 1 expty) (CS.lift 1 infty) subst
1437 metasenv context_bo ugraph in
1438 let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1439 let (bo,_), subst, metasenv, ugraph =
1440 coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1442 metasenv context_bo ugraph
1444 (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1445 | _ -> assert false (* not implemented yet *))
1446 | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1447 (* move this stuff away *)
1448 let get_cl_and_left_p uri tyno outty ugraph =
1449 match CicEnvironment.get_obj ugraph uri with
1450 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1453 match CicReduction.whd ~delta:false ctx t with
1454 | Cic.Prod (name,src,tgt) ->
1455 let ctx = Some (name, Cic.Decl src) :: ctx in
1461 let rec skip_lambda_delifting t n =
1464 | Cic.Lambda (_,_,t),n ->
1465 skip_lambda_delifting
1466 (CS.subst (Cic.Implicit None) t) (n - 1)
1469 let get_l_r_p n = function
1470 | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1471 | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1472 HExtlib.split_nth n args
1475 let _, _, ty, cl = List.nth tl tyno in
1476 let pis = count_pis ty in
1477 let rno = pis - leftno in
1478 let t = skip_lambda_delifting outty rno in
1479 let left_p, _ = get_l_r_p leftno t in
1480 let instantiale_with_left cl =
1484 (fun t p -> match t with
1485 | Cic.Prod (_,_,t) ->
1491 let cl = instantiale_with_left (List.map snd cl) in
1492 cl, left_p, leftno, rno, ugraph
1495 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1498 let rec mkr n = function
1499 | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1502 CicReplace.replace_lifting
1503 ~equality:(fun _ -> CicUtil.alpha_equivalence)
1505 ~what:(matched::right_p)
1506 ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1510 | Cic.Lambda (name, src, tgt),_ ->
1511 Cic.Lambda (name, src,
1512 keep_lambdas_and_put_expty
1513 (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1514 (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1518 metasenv subst context uri tyno cty outty leftno i
1520 let mytl = function [] -> [] | _::tl -> tl in
1521 let rec aux context outty par k = function
1522 | Cic.Prod (name, src, tgt) ->
1523 Cic.Prod (name, src,
1525 (Some (name, Cic.Decl src) :: context)
1526 (CS.lift 1 outty) (Cic.Rel k::par) (k+1) tgt)
1528 let par = mytl par in
1530 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1531 if par <> [] then Cic.Appl (k::par) else k
1533 CR.head_beta_reduce ~delta:false
1534 (Cic.Appl [outty;k])
1535 | Cic.Appl (Cic.MutInd _::pl) ->
1536 let left_p,_ = HExtlib.split_nth leftno pl in
1538 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1539 Cic.Appl (k::left_p@par)
1543 CicTypeChecker.type_of_aux' ~subst metasenv context k
1544 CicUniv.oblivion_ugraph
1546 | Cic.Appl (Cic.MutInd _::args),_ ->
1547 snd (HExtlib.split_nth leftno args)
1549 with CicTypeChecker.TypeCheckerFailure _ -> assert false
1551 CR.head_beta_reduce ~delta:false
1552 (Cic.Appl (outty ::right_p @ [k]))
1555 aux context outty [] 1 cty
1557 (* constructors types with left params already instantiated *)
1558 let outty = CicMetaSubst.apply_subst subst outty in
1559 let cl, left_p, leftno,rno,ugraph =
1560 get_cl_and_left_p uri tyno outty ugraph
1565 CicTypeChecker.type_of_aux' ~subst metasenv context m
1566 CicUniv.oblivion_ugraph
1568 | Cic.MutInd _,_ -> []
1569 | Cic.Appl (Cic.MutInd _::args),_ ->
1570 snd (HExtlib.split_nth leftno args)
1572 with CicTypeChecker.TypeCheckerFailure _ ->
1574 function 0 -> [] | n -> Cic.Implicit None :: foo (n-1)
1579 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1581 let _,pl,subst,metasenv,ugraph =
1583 (fun cty pbo (i, acc, s, m, ugraph) ->
1584 (* Pi k_par, (naw_)outty right_par (K_i left_par k_par) *)
1586 add_params m s context uri tyno cty outty leftno i in
1588 add_params m s context uri tyno cty new_outty leftno i in
1589 let (pbo, _), subst, metasenv, ugraph =
1590 coerce_to_something_aux pbo infty_pbo expty_pbo
1593 (i-1, pbo::acc, subst, metasenv, ugraph))
1594 cl pl (List.length pl, [], subst, metasenv, ugraph)
1596 let t = Cic.MutCase(uri, tyno, new_outty, m, pl) in
1597 (t, expty), subst, metasenv, ugraph
1598 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1600 FreshNamesGenerator.mk_fresh_name
1601 ~subst metasenv context Cic.Anonymous ~typ:src2
1603 let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1604 (* contravariant part: the argument of f:src->ty *)
1605 let (rel1, _), subst, metasenv, ugraph =
1606 coerce_to_something_aux
1607 (Cic.Rel 1) (CS.lift 1 src2)
1608 (CS.lift 1 src) subst metasenv context_src2 ugraph
1610 (* covariant part: the result of f(c x); x:src2; (c x):src *)
1613 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1614 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1616 (* we fix the possible dependency problem in the source ty *)
1617 let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1618 let (bo, _), subst, metasenv, ugraph =
1619 coerce_to_something_aux
1620 bo ty ty2 subst metasenv context_src2 ugraph
1622 let coerced = Cic.Lambda (name_t,src2, bo) in
1623 debug_print (lazy ("coerced: "^ CicMetaSubst.ppterm_in_context
1624 ~metasenv subst coerced context));
1625 (coerced, expty), subst, metasenv, ugraph
1627 coerce_atom_to_something t infty expty subst metasenv context ugraph
1630 coerce_to_something_aux t infty expty subst metasenv context ugraph
1631 with Uncertain _ | RefineFailure _ as exn ->
1634 CicMetaSubst.ppterm_in_context metasenv subst t context ^
1635 " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1636 infty context ^ " but is here used with type " ^
1637 CicMetaSubst.ppterm_in_context metasenv subst expty context)
1639 enrich localization_tbl ~f t exn
1641 and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1642 match CicReduction.whd ~subst:subst context infty with
1643 | Cic.Meta _ | Cic.Sort _ ->
1644 t,infty, subst, metasenv, ugraph
1646 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1648 let (t, ty_t), subst, metasenv, ugraph =
1649 coerce_to_something true
1650 localization_tbl t src tgt subst metasenv context ugraph
1652 t, ty_t, subst, metasenv, ugraph
1653 with HExtlib.Localized (_, exn) ->
1655 lazy ("(7)The term " ^
1656 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1657 ^ " is not a type since it has type " ^
1658 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1659 ^ " that is not a sort")
1661 enrich localization_tbl ~f t exn
1664 (* eat prods ends here! *)
1666 let t',ty,subst',metasenv',ugraph1 =
1667 type_of_aux [] metasenv context t ugraph
1669 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1670 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1671 (* Andrea: ho rimesso qui l'applicazione della subst al
1672 metasenv dopo che ho droppato l'invariante che il metsaenv
1673 e' sempre istanziato *)
1674 let substituted_metasenv =
1675 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1677 (* substituted_t,substituted_ty,substituted_metasenv *)
1678 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1680 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1682 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1683 let cleaned_metasenv =
1685 (function (n,context,ty) ->
1686 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1691 | Some (n, Cic.Decl t) ->
1693 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1694 | Some (n, Cic.Def (bo,ty)) ->
1695 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1700 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1702 Some (n, Cic.Def (bo',ty'))
1706 ) substituted_metasenv
1708 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1711 let undebrujin uri typesno tys t =
1714 (fun (name,_,_,_) (i,t) ->
1715 (* here the explicit_named_substituion is assumed to be *)
1717 let t' = Cic.MutInd (uri,i,[]) in
1718 let t = CicSubstitution.subst t' t in
1720 ) tys (typesno - 1,t))
1722 let map_first_n n start f g l =
1723 let rec aux acc k l =
1726 | [] -> raise (Invalid_argument "map_first_n")
1727 | hd :: tl -> f hd k (aux acc (k+1) tl)
1733 (*CSC: this is a very rough approximation; to be finished *)
1734 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1735 let subst,metasenv,ugraph,tys =
1737 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1738 let subst,metasenv,ugraph,cl =
1740 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1741 let rec aux ctx k subst = function
1742 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1743 let subst,metasenv,ugraph,tl =
1745 (subst,metasenv,ugraph,[])
1746 (fun t n (subst,metasenv,ugraph,acc) ->
1747 let subst,metasenv,ugraph =
1749 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1751 subst,metasenv,ugraph,(t::acc))
1752 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1755 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1756 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1757 subst,metasenv,ugraph,t
1758 | Cic.Prod (name,s,t) ->
1759 let ctx = (Some (name,Cic.Decl s))::ctx in
1760 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1761 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1765 (lazy "not well formed constructor type"))
1767 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1768 subst,metasenv,ugraph,(name,ty) :: acc)
1769 cl (subst,metasenv,ugraph,[])
1771 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1772 tys ([],metasenv,ugraph,[])
1774 let substituted_tys =
1776 (fun (name,ind,arity,cl) ->
1778 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1780 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1783 metasenv,ugraph,substituted_tys
1785 let typecheck metasenv uri obj ~localization_tbl =
1786 let ugraph = CicUniv.empty_ugraph in
1788 Cic.Constant (name,Some bo,ty,args,attrs) ->
1789 let bo',boty,metasenv,ugraph =
1790 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1791 let ty',_,metasenv,ugraph =
1792 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1793 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1794 let bo' = CicMetaSubst.apply_subst subst bo' in
1795 let ty' = CicMetaSubst.apply_subst subst ty' in
1796 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1797 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1798 | Cic.Constant (name,None,ty,args,attrs) ->
1799 let ty',_,metasenv,ugraph =
1800 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1802 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1803 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1804 assert (metasenv' = metasenv);
1805 (* Here we do not check the metasenv for correctness *)
1806 let bo',boty,metasenv,ugraph =
1807 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1808 let ty',sort,metasenv,ugraph =
1809 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1813 (* instead of raising Uncertain, let's hope that the meta will become
1816 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1818 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1819 let bo' = CicMetaSubst.apply_subst subst bo' in
1820 let ty' = CicMetaSubst.apply_subst subst ty' in
1821 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1822 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1823 | Cic.Variable _ -> assert false (* not implemented *)
1824 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1825 (*CSC: this code is greately simplified and many many checks are missing *)
1826 (*CSC: e.g. the constructors are not required to build their own types, *)
1827 (*CSC: the arities are not required to have as type a sort, etc. *)
1828 let uri = match uri with Some uri -> uri | None -> assert false in
1829 let typesno = List.length tys in
1830 (* first phase: we fix only the types *)
1831 let metasenv,ugraph,tys =
1833 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1834 let ty',_,metasenv,ugraph =
1835 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1837 metasenv,ugraph,(name,b,ty',cl)::res
1838 ) tys (metasenv,ugraph,[]) in
1840 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1841 (* second phase: we fix only the constructors *)
1842 let saved_menv = metasenv in
1843 let metasenv,ugraph,tys =
1845 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1846 let metasenv,ugraph,cl' =
1848 (fun (name,ty) (metasenv,ugraph,res) ->
1850 CicTypeChecker.debrujin_constructor
1851 ~cb:(relocalize localization_tbl) uri typesno ty in
1852 let ty',_,metasenv,ugraph =
1853 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1854 let ty' = undebrujin uri typesno tys ty' in
1855 metasenv@saved_menv,ugraph,(name,ty')::res
1856 ) cl (metasenv,ugraph,[])
1858 metasenv,ugraph,(name,b,ty,cl')::res
1859 ) tys (metasenv,ugraph,[]) in
1860 (* third phase: we check the positivity condition *)
1861 let metasenv,ugraph,tys =
1862 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1864 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1867 (* sara' piu' veloce che raffinare da zero? mah.... *)
1868 let pack_coercion metasenv ctx t =
1869 let module C = Cic in
1870 let rec merge_coercions ctx =
1871 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1873 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1874 | C.Meta (n,subst) ->
1877 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1880 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1881 | C.Prod (name,so,dest) ->
1882 let ctx' = (Some (name,C.Decl so))::ctx in
1883 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1884 | C.Lambda (name,so,dest) ->
1885 let ctx' = (Some (name,C.Decl so))::ctx in
1886 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1887 | C.LetIn (name,so,dest) ->
1888 let _,ty,metasenv,ugraph =
1889 pack_coercions := false;
1890 type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1891 pack_coercions := true;
1892 let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1893 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1895 let l = List.map (merge_coercions ctx) l in
1897 let b,_,_,_,_ = is_a_double_coercion t in
1899 let ugraph = CicUniv.oblivion_ugraph in
1900 let old_insert_coercions = !insert_coercions in
1901 insert_coercions := false;
1902 let newt, _, menv, _ =
1904 type_of_aux' metasenv ctx t ugraph
1905 with RefineFailure _ | Uncertain _ ->
1908 insert_coercions := old_insert_coercions;
1909 if metasenv <> [] || menv = [] then
1912 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1915 | C.Var (uri,exp_named_subst) ->
1916 let exp_named_subst = List.map aux exp_named_subst in
1917 C.Var (uri, exp_named_subst)
1918 | C.Const (uri,exp_named_subst) ->
1919 let exp_named_subst = List.map aux exp_named_subst in
1920 C.Const (uri, exp_named_subst)
1921 | C.MutInd (uri,tyno,exp_named_subst) ->
1922 let exp_named_subst = List.map aux exp_named_subst in
1923 C.MutInd (uri,tyno,exp_named_subst)
1924 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1925 let exp_named_subst = List.map aux exp_named_subst in
1926 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1927 | C.MutCase (uri,tyno,out,te,pl) ->
1928 let pl = List.map (merge_coercions ctx) pl in
1929 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1930 | C.Fix (fno, fl) ->
1933 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1938 (fun (name,idx,ty,bo) ->
1939 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1943 | C.CoFix (fno, fl) ->
1946 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1951 (fun (name,ty,bo) ->
1952 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1957 merge_coercions ctx t
1960 let pack_coercion_metasenv conjectures =
1961 let module C = Cic in
1963 (fun (i, ctx, ty) ->
1969 Some (name, C.Decl t) ->
1970 Some (name, C.Decl (pack_coercion conjectures ctx t))
1971 | Some (name, C.Def (t,None)) ->
1972 Some (name,C.Def (pack_coercion conjectures ctx t,None))
1973 | Some (name, C.Def (t,Some ty)) ->
1974 Some (name, C.Def (pack_coercion conjectures ctx t,
1975 Some (pack_coercion conjectures ctx ty)))
1981 ((i,ctx,pack_coercion conjectures ctx ty))
1985 let pack_coercion_obj obj =
1986 let module C = Cic in
1988 | C.Constant (id, body, ty, params, attrs) ->
1992 | Some body -> Some (pack_coercion [] [] body)
1994 let ty = pack_coercion [] [] ty in
1995 C.Constant (id, body, ty, params, attrs)
1996 | C.Variable (name, body, ty, params, attrs) ->
2000 | Some body -> Some (pack_coercion [] [] body)
2002 let ty = pack_coercion [] [] ty in
2003 C.Variable (name, body, ty, params, attrs)
2004 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2005 let conjectures = pack_coercion_metasenv conjectures in
2006 let body = pack_coercion conjectures [] body in
2007 let ty = pack_coercion conjectures [] ty in
2008 C.CurrentProof (name, conjectures, body, ty, params, attrs)
2009 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2012 (fun (name, ind, arity, cl) ->
2013 let arity = pack_coercion [] [] arity in
2015 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2017 (name, ind, arity, cl))
2020 C.InductiveDefinition (indtys, params, leftno, attrs)
2025 let type_of_aux' metasenv context term =
2028 type_of_aux' metasenv context term in
2030 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2032 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2035 | RefineFailure msg as e ->
2036 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2038 | Uncertain msg as e ->
2039 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2043 let profiler2 = HExtlib.profile "CicRefine"
2045 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2046 profiler2.HExtlib.profile
2047 (type_of_aux' ?localization_tbl metasenv context term) ugraph
2049 let typecheck ~localization_tbl metasenv uri obj =
2050 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2052 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2053 (* vim:set foldmethod=marker: *)