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 HLog.debug ("!!! 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 FreshNamesGenerator.mk_fresh_name ~subst metasenv
195 (CicMetaSubst.apply_subst_context subst context)
197 ~typ:(CicMetaSubst.apply_subst subst argty)
199 FreshNamesGenerator.mk_fresh_name ~subst
200 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
202 let metasenv,target =
203 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
205 metasenv,Cic.Prod (name,meta,target)
207 mk_prod metasenv context args
210 let rec type_of_constant uri ugraph =
211 let module C = Cic in
212 let module R = CicReduction in
213 let module U = UriManager in
214 let _ = CicTypeChecker.typecheck uri in
217 CicEnvironment.get_cooked_obj ugraph uri
218 with Not_found -> assert false
221 C.Constant (_,_,ty,_,_) -> ty,u
222 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
226 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
228 and type_of_variable uri ugraph =
229 let module C = Cic in
230 let module R = CicReduction in
231 let module U = UriManager in
232 let _ = CicTypeChecker.typecheck uri in
235 CicEnvironment.get_cooked_obj ugraph uri
236 with Not_found -> assert false
239 C.Variable (_,_,ty,_,_) -> ty,u
243 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
245 and type_of_mutual_inductive_defs uri i ugraph =
246 let module C = Cic in
247 let module R = CicReduction in
248 let module U = UriManager in
249 let _ = CicTypeChecker.typecheck uri in
252 CicEnvironment.get_cooked_obj ugraph uri
253 with Not_found -> assert false
256 C.InductiveDefinition (dl,_,_,_) ->
257 let (_,_,arity,_) = List.nth dl i in
262 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
264 and type_of_mutual_inductive_constr uri i j ugraph =
265 let module C = Cic in
266 let module R = CicReduction in
267 let module U = UriManager in
268 let _ = CicTypeChecker.typecheck uri in
271 CicEnvironment.get_cooked_obj ugraph uri
272 with Not_found -> assert false
275 C.InductiveDefinition (dl,_,_,_) ->
276 let (_,_,_,cl) = List.nth dl i in
277 let (_,ty) = List.nth cl (j-1) in
283 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
286 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
288 (* the check_branch function checks if a branch of a case is refinable.
289 It returns a pair (outype_instance,args), a subst and a metasenv.
290 outype_instance is the expected result of applying the case outtype
292 The problem is that outype is in general unknown, and we should
293 try to synthesize it from the above information, that is in general
294 a second order unification problem. *)
296 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
297 let module C = Cic in
298 (* let module R = CicMetaSubst in *)
299 let module R = CicReduction in
300 match R.whd ~subst context expectedtype with
302 (n,context,actualtype, [term]), subst, metasenv, ugraph
303 | C.Appl (C.MutInd (_,_,_)::tl) ->
304 let (_,arguments) = split tl left_args_no in
305 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
306 | C.Prod (name,so,de) ->
307 (* we expect that the actual type of the branch has the due
309 (match R.whd ~subst context actualtype with
310 C.Prod (name',so',de') ->
311 let subst, metasenv, ugraph1 =
312 fo_unif_subst subst context metasenv so so' ugraph in
314 (match CicSubstitution.lift 1 term with
315 C.Appl l -> C.Appl (l@[C.Rel 1])
316 | t -> C.Appl [t ; C.Rel 1]) in
317 (* we should also check that the name variable is anonymous in
318 the actual type de' ?? *)
320 ((Some (name,(C.Decl so)))::context)
321 metasenv subst left_args_no de' term' de ugraph1
322 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
323 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
325 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
328 let rec type_of_aux subst metasenv context t ugraph =
329 let module C = Cic in
330 let module S = CicSubstitution in
331 let module U = UriManager in
332 let (t',_,_,_,_) as res =
337 match List.nth context (n - 1) with
338 Some (_,C.Decl ty) ->
339 t,S.lift n ty,subst,metasenv, ugraph
340 | Some (_,C.Def (_,Some ty)) ->
341 t,S.lift n ty,subst,metasenv, ugraph
342 | Some (_,C.Def (bo,None)) ->
344 (* if it is in the context it must be already well-typed*)
345 CicTypeChecker.type_of_aux' ~subst metasenv context
348 t,ty,subst,metasenv,ugraph
350 enrich localization_tbl t
351 (RefineFailure (lazy "Rel to hidden hypothesis"))
354 enrich localization_tbl t
355 (RefineFailure (lazy "Not a closed term")))
356 | C.Var (uri,exp_named_subst) ->
357 let exp_named_subst',subst',metasenv',ugraph1 =
358 check_exp_named_subst
359 subst metasenv context exp_named_subst ugraph
361 let ty_uri,ugraph1 = type_of_variable uri ugraph in
363 CicSubstitution.subst_vars exp_named_subst' ty_uri
365 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
368 let (canonical_context, term,ty) =
369 CicUtil.lookup_subst n subst
371 let l',subst',metasenv',ugraph1 =
372 check_metasenv_consistency n subst metasenv context
373 canonical_context l ugraph
375 (* trust or check ??? *)
376 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
377 subst', metasenv', ugraph1
378 (* type_of_aux subst metasenv
379 context (CicSubstitution.subst_meta l term) *)
380 with CicUtil.Subst_not_found _ ->
381 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
382 let l',subst',metasenv', ugraph1 =
383 check_metasenv_consistency n subst metasenv context
384 canonical_context l ugraph
386 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
387 subst', metasenv',ugraph1)
388 | C.Sort (C.Type tno) ->
389 let tno' = CicUniv.fresh() in
391 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
392 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
394 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
396 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
397 | C.Implicit infos ->
398 let metasenv',t' = exp_impl metasenv subst context infos in
399 type_of_aux subst metasenv' context t' ugraph
401 let ty',_,subst',metasenv',ugraph1 =
402 type_of_aux subst metasenv context ty ugraph
404 let te',inferredty,subst'',metasenv'',ugraph2 =
405 type_of_aux subst' metasenv' context te ugraph1
407 let (te', ty'), subst''',metasenv''',ugraph3 =
408 coerce_to_something true localization_tbl te' inferredty ty'
409 subst'' metasenv'' context ugraph2
411 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
412 | C.Prod (name,s,t) ->
413 let s',sort1,subst',metasenv',ugraph1 =
414 type_of_aux subst metasenv context s ugraph
416 let s',sort1,subst', metasenv',ugraph1 =
417 coerce_to_sort localization_tbl
418 s' sort1 subst' context metasenv' ugraph1
420 let context_for_t = ((Some (name,(C.Decl s')))::context) in
421 let t',sort2,subst'',metasenv'',ugraph2 =
422 type_of_aux subst' metasenv'
423 context_for_t t ugraph1
425 let t',sort2,subst'',metasenv'',ugraph2 =
426 coerce_to_sort localization_tbl
427 t' sort2 subst'' context_for_t metasenv'' ugraph2
429 let sop,subst''',metasenv''',ugraph3 =
430 sort_of_prod localization_tbl subst'' metasenv''
431 context (name,s') t' (sort1,sort2) ugraph2
433 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
434 | C.Lambda (n,s,t) ->
435 let s',sort1,subst',metasenv',ugraph1 =
436 type_of_aux subst metasenv context s ugraph
438 let s',sort1,subst',metasenv',ugraph1 =
439 coerce_to_sort localization_tbl
440 s' sort1 subst' context metasenv' ugraph1
442 let context_for_t = ((Some (n,(C.Decl s')))::context) in
443 let t',type2,subst'',metasenv'',ugraph2 =
444 type_of_aux subst' metasenv' context_for_t t ugraph1
446 C.Lambda (n,s',t'),C.Prod (n,s',type2),
447 subst'',metasenv'',ugraph2
449 (* only to check if s is well-typed *)
450 let s',ty,subst',metasenv',ugraph1 =
451 type_of_aux subst metasenv context s ugraph
453 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
455 let t',inferredty,subst'',metasenv'',ugraph2 =
456 type_of_aux subst' metasenv'
457 context_for_t t ugraph1
459 (* One-step LetIn reduction.
460 * Even faster than the previous solution.
461 * Moreover the inferred type is closer to the expected one.
464 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
465 subst'',metasenv'',ugraph2
466 | C.Appl (he::((_::_) as tl)) ->
467 let he',hetype,subst',metasenv',ugraph1 =
468 type_of_aux subst metasenv context he ugraph
470 let tlbody_and_type,subst'',metasenv'',ugraph2 =
471 typeof_list subst' metasenv' context ugraph1 tl
473 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
474 eat_prods true subst'' metasenv'' context
475 he' hetype tlbody_and_type ugraph2
477 let newappl = (C.Appl (coerced_he::coerced_args)) in
478 avoid_double_coercion
479 context subst''' metasenv''' ugraph3 newappl applty
480 | C.Appl _ -> assert false
481 | C.Const (uri,exp_named_subst) ->
482 let exp_named_subst',subst',metasenv',ugraph1 =
483 check_exp_named_subst subst metasenv context
484 exp_named_subst ugraph in
485 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
487 CicSubstitution.subst_vars exp_named_subst' ty_uri
489 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
490 | C.MutInd (uri,i,exp_named_subst) ->
491 let exp_named_subst',subst',metasenv',ugraph1 =
492 check_exp_named_subst subst metasenv context
493 exp_named_subst ugraph
495 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
497 CicSubstitution.subst_vars exp_named_subst' ty_uri in
498 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
499 | C.MutConstruct (uri,i,j,exp_named_subst) ->
500 let exp_named_subst',subst',metasenv',ugraph1 =
501 check_exp_named_subst subst metasenv context
502 exp_named_subst ugraph
505 type_of_mutual_inductive_constr uri i j ugraph1
508 CicSubstitution.subst_vars exp_named_subst' ty_uri
510 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
512 | C.MutCase (uri, i, outtype, term, pl) ->
513 (* first, get the inductive type (and noparams)
514 * in the environment *)
515 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
516 let _ = CicTypeChecker.typecheck uri in
517 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
519 C.InductiveDefinition (l,expl_params,parsno,_) ->
520 List.nth l i , expl_params, parsno, u
522 enrich localization_tbl t
524 (lazy ("Unkown mutual inductive definition " ^
525 U.string_of_uri uri)))
527 if List.length constructors <> List.length pl then
528 enrich localization_tbl t
530 (lazy "Wrong number of cases")) ;
531 let rec count_prod t =
532 match CicReduction.whd ~subst context t with
533 C.Prod (_, _, t) -> 1 + (count_prod t)
536 let no_args = count_prod arity in
537 (* now, create a "generic" MutInd *)
538 let metasenv,left_args =
539 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
541 let metasenv,right_args =
542 let no_right_params = no_args - no_left_params in
543 if no_right_params < 0 then assert false
544 else CicMkImplicit.n_fresh_metas
545 metasenv subst context no_right_params
547 let metasenv,exp_named_subst =
548 CicMkImplicit.fresh_subst metasenv subst context expl_params in
551 C.MutInd (uri,i,exp_named_subst)
554 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
556 (* check consistency with the actual type of term *)
557 let term',actual_type,subst,metasenv,ugraph1 =
558 type_of_aux subst metasenv context term ugraph in
559 let expected_type',_, subst, metasenv,ugraph2 =
560 type_of_aux subst metasenv context expected_type ugraph1
562 let actual_type = CicReduction.whd ~subst context actual_type in
563 let subst,metasenv,ugraph3 =
565 fo_unif_subst subst context metasenv
566 expected_type' actual_type ugraph2
569 enrich localization_tbl term' exn
572 CicMetaSubst.ppterm_in_context ~metasenv subst term'
573 context ^ " has type " ^
574 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
575 context ^ " but is here used with type " ^
576 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
578 let rec instantiate_prod t =
582 match CicReduction.whd ~subst context t with
584 instantiate_prod (CicSubstitution.subst he t') tl
587 let arity_instantiated_with_left_args =
588 instantiate_prod arity left_args in
589 (* TODO: check if the sort elimination
590 * is allowed: [(I q1 ... qr)|B] *)
591 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
593 (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
595 if left_args = [] then
596 (C.MutConstruct (uri,i,j,exp_named_subst))
599 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
601 let p',actual_type,subst,metasenv,ugraph1 =
602 type_of_aux subst metasenv context p ugraph
604 let constructor',expected_type, subst, metasenv,ugraph2 =
605 type_of_aux subst metasenv context constructor ugraph1
607 let outtypeinstance,subst,metasenv,ugraph3 =
609 check_branch 0 context metasenv subst
610 no_left_params actual_type constructor' expected_type
614 enrich localization_tbl constructor'
617 CicMetaSubst.ppterm_in_context metasenv subst p'
618 context ^ " has type " ^
619 CicMetaSubst.ppterm_in_context metasenv subst actual_type
620 context ^ " but is here used with type " ^
621 CicMetaSubst.ppterm_in_context metasenv subst expected_type
625 outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
626 pl ([],List.length pl,[],subst,metasenv,ugraph3)
629 (* we are left to check that the outype matches his instances.
630 The easy case is when the outype is specified, that amount
631 to a trivial check. Otherwise, we should guess a type from
635 let outtype,outtypety, subst, metasenv,ugraph4 =
636 type_of_aux subst metasenv context outtype ugraph4 in
639 (let candidate,ugraph5,metasenv,subst =
640 let exp_name_subst, metasenv =
642 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
644 let uris = CicUtil.params_of_obj o in
646 fun uri (acc,metasenv) ->
647 let metasenv',new_meta =
648 CicMkImplicit.mk_implicit metasenv subst context
651 CicMkImplicit.identity_relocation_list_for_metavariable
654 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
658 match left_args,right_args with
659 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
661 let rec mk_right_args =
664 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
666 let right_args_no = List.length right_args in
667 let lifted_left_args =
668 List.map (CicSubstitution.lift right_args_no) left_args
670 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
671 (lifted_left_args @ mk_right_args right_args_no))
674 FreshNamesGenerator.mk_fresh_name ~subst metasenv
675 context Cic.Anonymous ~typ:ty
677 match outtypeinstances with
679 let extended_context =
680 let rec add_right_args =
682 Cic.Prod (name,ty,t) ->
683 Some (name,Cic.Decl ty)::(add_right_args t)
686 (Some (fresh_name,Cic.Decl ty))::
688 (add_right_args arity_instantiated_with_left_args))@
691 let metasenv,new_meta =
692 CicMkImplicit.mk_implicit metasenv subst extended_context
695 CicMkImplicit.identity_relocation_list_for_metavariable
698 let rec add_lambdas b =
700 Cic.Prod (name,ty,t) ->
701 Cic.Lambda (name,ty,(add_lambdas b t))
702 | _ -> Cic.Lambda (fresh_name, ty, b)
705 add_lambdas (Cic.Meta (new_meta,irl))
706 arity_instantiated_with_left_args
708 (Some candidate),ugraph4,metasenv,subst
709 | (constructor_args_no,_,instance,_)::tl ->
711 let instance',subst,metasenv =
712 CicMetaSubst.delift_rels subst metasenv
713 constructor_args_no instance
715 let candidate,ugraph,metasenv,subst =
717 fun (candidate_oty,ugraph,metasenv,subst)
718 (constructor_args_no,_,instance,_) ->
719 match candidate_oty with
720 | None -> None,ugraph,metasenv,subst
723 let instance',subst,metasenv =
724 CicMetaSubst.delift_rels subst metasenv
725 constructor_args_no instance
727 let subst,metasenv,ugraph =
728 fo_unif_subst subst context metasenv
731 candidate_oty,ugraph,metasenv,subst
733 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
734 | RefineFailure _ | Uncertain _ ->
735 None,ugraph,metasenv,subst
736 ) (Some instance',ugraph4,metasenv,subst) tl
739 | None -> None, ugraph,metasenv,subst
741 let rec add_lambdas n b =
743 Cic.Prod (name,ty,t) ->
744 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
746 Cic.Lambda (fresh_name, ty,
747 CicSubstitution.lift (n + 1) t)
750 (add_lambdas 0 t arity_instantiated_with_left_args),
751 ugraph,metasenv,subst
752 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
753 None,ugraph4,metasenv,subst
756 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
758 let subst,metasenv,ugraph =
760 fo_unif_subst subst context metasenv
761 candidate outtype ugraph5
763 exn -> assert false(* unification against a metavariable *)
765 C.MutCase (uri, i, outtype, term', pl'),
766 CicReduction.head_beta_reduce
767 (CicMetaSubst.apply_subst subst
768 (Cic.Appl (outtype::right_args@[term']))),
769 subst,metasenv,ugraph)
770 | _ -> (* easy case *)
771 let tlbody_and_type,subst,metasenv,ugraph4 =
772 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
774 let _,_,_,subst,metasenv,ugraph4 =
775 eat_prods false subst metasenv context
776 outtype outtypety tlbody_and_type ugraph4
778 let _,_, subst, metasenv,ugraph5 =
779 type_of_aux subst metasenv context
780 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
782 let (subst,metasenv,ugraph6) =
784 (fun (subst,metasenv,ugraph)
785 p (constructor_args_no,context,instance,args)
790 CicSubstitution.lift constructor_args_no outtype
792 C.Appl (outtype'::args)
794 CicReduction.whd ~subst context appl
797 fo_unif_subst subst context metasenv instance instance'
801 enrich localization_tbl p exn
804 CicMetaSubst.ppterm_in_context ~metasenv subst p
805 context ^ " has type " ^
806 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
807 context ^ " but is here used with type " ^
808 CicMetaSubst.ppterm_in_context ~metasenv subst instance
810 (subst,metasenv,ugraph5) pl' outtypeinstances
812 C.MutCase (uri, i, outtype, term', pl'),
813 CicReduction.head_beta_reduce
814 (CicMetaSubst.apply_subst subst
815 (C.Appl(outtype::right_args@[term]))),
816 subst,metasenv,ugraph6)
818 let fl_ty',subst,metasenv,types,ugraph1,len =
820 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
821 let ty',_,subst',metasenv',ugraph1 =
822 type_of_aux subst metasenv context ty ugraph
824 fl @ [ty'],subst',metasenv',
825 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
826 :: types, ugraph, len+1
827 ) ([],subst,metasenv,[],ugraph,0) fl
829 let context' = types@context in
830 let fl_bo',subst,metasenv,ugraph2 =
832 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
833 let bo',ty_of_bo,subst,metasenv,ugraph1 =
834 type_of_aux subst metasenv context' bo ugraph in
835 let expected_ty = CicSubstitution.lift len ty in
836 let subst',metasenv',ugraph' =
838 fo_unif_subst subst context' metasenv
839 ty_of_bo expected_ty ugraph1
842 enrich localization_tbl bo exn
845 CicMetaSubst.ppterm_in_context ~metasenv subst bo
846 context' ^ " has type " ^
847 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
848 context' ^ " but is here used with type " ^
849 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
852 fl @ [bo'] , subst',metasenv',ugraph'
853 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
855 let ty = List.nth fl_ty' i in
856 (* now we have the new ty in fl_ty', the new bo in fl_bo',
857 * and we want the new fl with bo' and ty' injected in the right
860 let rec map3 f l1 l2 l3 =
863 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
866 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
869 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
871 let fl_ty',subst,metasenv,types,ugraph1,len =
873 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
874 let ty',_,subst',metasenv',ugraph1 =
875 type_of_aux subst metasenv context ty ugraph
877 fl @ [ty'],subst',metasenv',
878 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
879 types, ugraph1, len+1
880 ) ([],subst,metasenv,[],ugraph,0) fl
882 let context' = types@context in
883 let fl_bo',subst,metasenv,ugraph2 =
885 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
886 let bo',ty_of_bo,subst,metasenv,ugraph1 =
887 type_of_aux subst metasenv context' bo ugraph in
888 let expected_ty = CicSubstitution.lift len ty in
889 let subst',metasenv',ugraph' =
891 fo_unif_subst subst context' metasenv
892 ty_of_bo expected_ty ugraph1
895 enrich localization_tbl bo exn
898 CicMetaSubst.ppterm_in_context ~metasenv subst bo
899 context' ^ " has type " ^
900 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
901 context' ^ " but is here used with type " ^
902 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
905 fl @ [bo'],subst',metasenv',ugraph'
906 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
908 let ty = List.nth fl_ty' i in
909 (* now we have the new ty in fl_ty', the new bo in fl_bo',
910 * and we want the new fl with bo' and ty' injected in the right
913 let rec map3 f l1 l2 l3 =
916 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
919 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
922 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
924 relocalize localization_tbl t t';
927 (* check_metasenv_consistency checks that the "canonical" context of a
928 metavariable is consitent - up to relocation via the relocation list l -
929 with the actual context *)
930 and check_metasenv_consistency
931 metano subst metasenv context canonical_context l ugraph
933 let module C = Cic in
934 let module R = CicReduction in
935 let module S = CicSubstitution in
936 let lifted_canonical_context =
940 | (Some (n,C.Decl t))::tl ->
941 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
942 | (Some (n,C.Def (t,None)))::tl ->
943 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
944 | None::tl -> None::(aux (i+1) tl)
945 | (Some (n,C.Def (t,Some ty)))::tl ->
947 C.Def ((S.subst_meta l (S.lift i t)),
948 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
950 aux 1 canonical_context
954 (fun (l,subst,metasenv,ugraph) t ct ->
957 l @ [None],subst,metasenv,ugraph
958 | Some t,Some (_,C.Def (ct,_)) ->
959 let subst',metasenv',ugraph' =
961 (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
962 * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
963 fo_unif_subst subst context metasenv t ct ugraph
964 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))))))
966 l @ [Some t],subst',metasenv',ugraph'
967 | Some t,Some (_,C.Decl ct) ->
968 let t',inferredty,subst',metasenv',ugraph1 =
969 type_of_aux subst metasenv context t ugraph
971 let subst'',metasenv'',ugraph2 =
974 subst' context metasenv' inferredty ct ugraph1
975 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))))))
977 l @ [Some t'], subst'',metasenv'',ugraph2
979 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
981 Invalid_argument _ ->
985 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
986 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
987 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
989 and check_exp_named_subst metasubst metasenv context tl ugraph =
990 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
992 [] -> [],metasubst,metasenv,ugraph
994 let ty_uri,ugraph1 = type_of_variable uri ugraph in
996 CicSubstitution.subst_vars substs ty_uri in
997 (* CSC: why was this code here? it is wrong
998 (match CicEnvironment.get_cooked_obj ~trust:false uri with
999 Cic.Variable (_,Some bo,_,_) ->
1001 (RefineFailure (lazy
1002 "A variable with a body can not be explicit substituted"))
1003 | Cic.Variable (_,None,_,_) -> ()
1006 (RefineFailure (lazy
1007 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1010 let t',typeoft,metasubst',metasenv',ugraph2 =
1011 type_of_aux metasubst metasenv context t ugraph1 in
1012 let subst = uri,t' in
1013 let metasubst'',metasenv'',ugraph3 =
1016 metasubst' context metasenv' typeoft typeofvar ugraph2
1018 raise (RefineFailure (lazy
1019 ("Wrong Explicit Named Substitution: " ^
1020 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1021 " not unifiable with " ^
1022 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1024 (* FIXME: no mere tail recursive! *)
1025 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1026 check_exp_named_subst_aux
1027 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1029 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1031 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1034 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1037 let module C = Cic in
1038 let context_for_t2 = (Some (name,C.Decl s))::context in
1039 let t1'' = CicReduction.whd ~subst context t1 in
1040 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1041 match (t1'', t2'') with
1042 (C.Sort s1, C.Sort s2)
1043 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1044 (* different than Coq manual!!! *)
1045 C.Sort s2,subst,metasenv,ugraph
1046 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1047 let t' = CicUniv.fresh() in
1049 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1050 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1051 C.Sort (C.Type t'),subst,metasenv,ugraph2
1053 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1054 | (C.Sort _,C.Sort (C.Type t1)) ->
1055 C.Sort (C.Type t1),subst,metasenv,ugraph
1056 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1057 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1058 (* TODO how can we force the meta to become a sort? If we don't we
1059 * break the invariant that refine produce only well typed terms *)
1060 (* TODO if we check the non meta term and if it is a sort then we
1061 * are likely to know the exact value of the result e.g. if the rhs
1062 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1063 let (metasenv,idx) =
1064 CicMkImplicit.mk_implicit_sort metasenv subst in
1065 let (subst, metasenv,ugraph1) =
1067 fo_unif_subst subst context_for_t2 metasenv
1068 (C.Meta (idx,[])) t2'' ugraph
1069 with _ -> assert false (* unification against a metavariable *)
1071 t2'',subst,metasenv,ugraph1
1074 enrich localization_tbl s
1078 "%s is supposed to be a type, but its type is %s"
1079 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1080 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1082 enrich localization_tbl t
1086 "%s is supposed to be a type, but its type is %s"
1087 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1088 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1090 and avoid_double_coercion context subst metasenv ugraph t ty =
1091 if not !pack_coercions then
1092 t,ty,subst,metasenv,ugraph
1094 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1096 let source_carr = CoercGraph.source_of c2 in
1097 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1098 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1100 | CoercGraph.SomeCoercion candidates ->
1102 HExtlib.list_findopt
1103 (function (metasenv,last,c) ->
1105 | c when not (CoercGraph.is_composite c) ->
1106 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1109 let subst,metasenv,ugraph =
1110 fo_unif_subst subst context metasenv last head ugraph in
1111 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1116 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1117 let newt,_,subst,metasenv,ugraph =
1118 type_of_aux subst metasenv context c ugraph in
1119 debug_print (lazy "tipa...");
1120 let subst, metasenv, ugraph =
1121 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1122 fo_unif_subst subst context metasenv newt t ugraph
1124 debug_print (lazy "unifica...");
1125 Some (newt, ty, subst, metasenv, ugraph)
1127 | RefineFailure s | Uncertain s when not !pack_coercions->
1128 debug_print s; debug_print (lazy "stop\n");None
1129 | RefineFailure s | Uncertain s ->
1130 debug_print s;debug_print (lazy "goon\n");
1132 let old_pack_coercions = !pack_coercions in
1133 pack_coercions := false; (* to avoid diverging *)
1134 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1135 type_of_aux subst metasenv context c1_c2_implicit ugraph
1137 pack_coercions := old_pack_coercions;
1139 is_a_double_coercion refined_c1_c2_implicit
1145 match refined_c1_c2_implicit with
1146 | Cic.Appl l -> HExtlib.list_last l
1149 let subst, metasenv, ugraph =
1150 try fo_unif_subst subst context metasenv
1152 with RefineFailure s| Uncertain s->
1153 debug_print s;assert false
1155 let subst, metasenv, ugraph =
1156 fo_unif_subst subst context metasenv
1157 refined_c1_c2_implicit t ugraph
1159 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1161 | RefineFailure s | Uncertain s ->
1162 pack_coercions := true;debug_print s;None
1163 | exn -> pack_coercions := true; raise exn))
1166 (match selected with
1170 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1171 t, ty, subst, metasenv, ugraph)
1172 | _ -> t, ty, subst, metasenv, ugraph)
1174 t, ty, subst, metasenv, ugraph
1176 and typeof_list subst metasenv context ugraph l =
1177 let tlbody_and_type,subst,metasenv,ugraph =
1179 (fun x (res,subst,metasenv,ugraph) ->
1180 let x',ty,subst',metasenv',ugraph1 =
1181 type_of_aux subst metasenv context x ugraph
1183 (x', ty)::res,subst',metasenv',ugraph1
1184 ) l ([],subst,metasenv,ugraph)
1186 tlbody_and_type,subst,metasenv,ugraph
1189 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1191 (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1192 let fix_arity n metasenv context subst he hetype ugraph =
1193 let hetype = CicMetaSubst.apply_subst subst hetype in
1194 let src = CoercDb.coerc_carr_of_term hetype in
1195 let tgt = CoercDb.Fun 0 in
1196 match CoercGraph.look_for_coercion' metasenv subst context src tgt with
1197 | CoercGraph.NoCoercion -> []
1198 | CoercGraph.NotMetaClosed
1199 | CoercGraph.NotHandled _ ->
1200 raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1201 | CoercGraph.SomeCoercionToTgt candidates
1202 | CoercGraph.SomeCoercion candidates ->
1204 (fun (metasenv,last,coerc) ->
1206 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1208 let subst,metasenv,ugraph =
1209 fo_unif_subst subst context metasenv last he ugraph in
1210 debug_print (lazy ("New head: "^ pp coerc));
1212 CicTypeChecker.type_of_aux' ~subst metasenv context coerc
1215 debug_print (lazy (" has type: "^ pp tty));
1216 Some (coerc,tty,subst,metasenv,ugraph)
1218 | Uncertain _ | RefineFailure _
1219 | HExtlib.Localized (_,Uncertain _)
1220 | HExtlib.Localized (_,RefineFailure _) -> None
1221 | exn -> assert false)
1224 (* aux function to process the type of the head and the args in parallel *)
1225 let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1227 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1228 | (hete, hety)::tl as args ->
1229 match (CicReduction.whd ~subst context hetype) with
1230 | Cic.Prod (n,s,t) ->
1231 let arg,subst,metasenv,ugraph =
1232 coerce_to_something allow_coercions localization_tbl
1233 hete hety s subst metasenv context ugraph in
1235 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1236 ugraph (newargs@[arg]) tl
1239 match he, newargs with
1241 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1242 | _ -> Cic.Appl (he::List.map fst newargs)
1244 (*{{{*) debug_print (lazy
1246 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1247 "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1248 "\n but is applyed to: " ^ String.concat ";"
1249 (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1250 let possible_fixes =
1251 fix_arity (List.length args) metasenv context subst he hetype
1254 HExtlib.list_findopt
1255 (fun (he,hetype,subst,metasenv,ugraph) ->
1256 (* {{{ *)debug_print (lazy ("Try fix: "^
1257 CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1258 debug_print (lazy (" of type: "^
1259 CicMetaSubst.ppterm_in_context
1260 ~metasenv subst hetype context)); (* }}} *)
1262 Some (eat_prods_and_args
1263 metasenv subst context he hetype ugraph [] args)
1265 | RefineFailure _ | Uncertain _
1266 | HExtlib.Localized (_,RefineFailure _)
1267 | HExtlib.Localized (_,Uncertain _) -> None)
1273 (MoreArgsThanExpected
1274 (List.length args, RefineFailure (lazy "")))
1276 (* first we check if we are in the simple case of a meta closed term *)
1277 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1278 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1279 (* this optimization is to postpone fix_arity (the most common case)*)
1280 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1282 (* this (says CSC) is also useful to infer dependent types *)
1283 let pristinemenv = metasenv in
1284 let metasenv,hetype' =
1285 mk_prod_of_metas metasenv context subst args_bo_and_ty
1288 let subst,metasenv,ugraph =
1289 fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1291 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1292 with RefineFailure _ | Uncertain _ ->
1293 subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1295 let coerced_args,subst,metasenv,he,t,ugraph =
1298 metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1300 MoreArgsThanExpected (residuals,exn) ->
1301 more_args_than_expected localization_tbl metasenv
1302 subst he context hetype' residuals args_bo_and_ty exn
1304 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1306 and coerce_to_something
1307 allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1309 let module CS = CicSubstitution in
1310 let module CR = CicReduction in
1311 let cs_subst = CS.subst ~avoid_beta_redexes:true in
1312 let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1313 debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1315 CoercGraph.look_for_coercion metasenv subst context infty expty
1318 | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
1319 "coerce_atom_to_something fails since not meta closed"))
1320 | CoercGraph.NoCoercion
1321 | CoercGraph.SomeCoercionToTgt _
1322 | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
1323 "coerce_atom_to_something fails since no coercions found"))
1324 | CoercGraph.SomeCoercion candidates ->
1325 debug_print (lazy (string_of_int (List.length candidates) ^
1326 " candidates found"));
1327 let uncertain = ref false in
1331 (fun (metasenv,last,c) ->
1333 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1334 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1336 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
1337 "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
1339 debug_print (lazy ("FO_UNIF_SUBST: " ^
1340 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1341 let subst,metasenv,ugraph =
1342 fo_unif_subst subst context metasenv last t ugraph
1344 let newt,newhety,subst,metasenv,ugraph =
1345 type_of_aux subst metasenv context c ugraph in
1346 let newt, newty, subst, metasenv, ugraph =
1347 avoid_double_coercion context subst metasenv ugraph newt expty
1349 let subst,metasenv,ugraph =
1350 fo_unif_subst subst context metasenv newhety expty ugraph in
1351 Some ((newt,newty), subst, metasenv, ugraph)
1353 | Uncertain _ -> uncertain := true; None
1354 | RefineFailure _ -> None)
1359 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1367 | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1368 | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1370 let rec coerce_to_something_aux
1371 t infty expty subst metasenv context ugraph
1374 let subst, metasenv, ugraph =
1375 fo_unif_subst subst context metasenv infty expty ugraph
1377 (t, expty), subst, metasenv, ugraph
1378 with (Uncertain _ | RefineFailure _ as exn)
1379 when allow_coercions && !insert_coercions ->
1380 let whd = CicReduction.whd ~delta:false in
1381 let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1382 let infty = clean infty subst context in
1383 let expty = clean expty subst context in
1384 let t = clean t subst context in
1385 (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1386 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1387 CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1388 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1389 let (coerced,_),subst,metasenv,_ as result =
1390 match infty, expty, t with
1391 | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1392 (*{{{*) debug_print (lazy "FIX");
1394 [name,i,_(* infty *),bo] ->
1396 Some (Cic.Name name,Cic.Decl expty)::context in
1397 let (rel1, _), subst, metasenv, ugraph =
1398 coerce_to_something_aux (Cic.Rel 1)
1399 (CS.lift 1 expty) (CS.lift 1 infty) subst
1400 metasenv context_bo ugraph in
1401 let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1402 let (bo,_), subst, metasenv, ugraph =
1403 coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1405 metasenv context_bo ugraph
1407 (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1408 | _ -> assert false (* not implemented yet *)) (*}}}*)
1409 | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1410 (*{{{*) debug_print (lazy "CASE");
1411 (* {{{ helper functions *)
1412 let get_cl_and_left_p uri tyno outty ugraph =
1413 match CicEnvironment.get_obj ugraph uri with
1414 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1417 match CicReduction.whd ~delta:false ctx t with
1418 | Cic.Prod (name,src,tgt) ->
1419 let ctx = Some (name, Cic.Decl src) :: ctx in
1425 let rec skip_lambda_delifting t n =
1428 | Cic.Lambda (_,_,t),n ->
1429 skip_lambda_delifting
1430 (CS.subst (Cic.Implicit None) t) (n - 1)
1433 let get_l_r_p n = function
1434 | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1435 | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1436 HExtlib.split_nth n args
1439 let _, _, ty, cl = List.nth tl tyno in
1440 let pis = count_pis ty in
1441 let rno = pis - leftno in
1442 let t = skip_lambda_delifting outty rno in
1443 let left_p, _ = get_l_r_p leftno t in
1444 let instantiale_with_left cl =
1448 (fun t p -> match t with
1449 | Cic.Prod (_,_,t) ->
1455 let cl = instantiale_with_left (List.map snd cl) in
1456 cl, left_p, leftno, rno, ugraph
1459 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1462 let rec mkr n = function
1463 | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1466 CicReplace.replace_lifting
1467 ~equality:(fun _ -> CicUtil.alpha_equivalence)
1469 ~what:(matched::right_p)
1470 ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1474 | Cic.Lambda (name, src, tgt),_ ->
1475 Cic.Lambda (name, src,
1476 keep_lambdas_and_put_expty
1477 (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1478 (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1481 let eq_uri, eq, eq_refl =
1482 match LibraryObjects.eq_URI () with
1483 | None -> HLog.warn "no default equality"; raise exn
1484 | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1487 metasenv subst context uri tyno cty outty mty m leftno i
1489 let rec aux context outty par k mty m = function
1490 | Cic.Prod (name, src, tgt) ->
1493 (Some (name, Cic.Decl src) :: context)
1494 (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1495 (CS.lift 1 mty) (CS.lift 1 m) tgt
1497 Cic.Prod (name, src, t), k
1500 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1501 if par <> [] then Cic.Appl (k::par) else k
1503 Cic.Prod (Cic.Name "p",
1504 Cic.Appl [eq; mty; m; k],
1506 (CR.head_beta_reduce ~delta:false
1507 (Cic.Appl [outty;k])))),k
1508 | Cic.Appl (Cic.MutInd _::pl) ->
1509 let left_p,right_p = HExtlib.split_nth leftno pl in
1510 let has_rights = right_p <> [] in
1512 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1513 Cic.Appl (k::left_p@par)
1517 CicTypeChecker.type_of_aux' ~subst metasenv context k
1518 CicUniv.oblivion_ugraph
1520 | Cic.Appl (Cic.MutInd _::args),_ ->
1521 snd (HExtlib.split_nth leftno args)
1523 with CicTypeChecker.TypeCheckerFailure _-> assert false
1526 CR.head_beta_reduce ~delta:false
1527 (Cic.Appl (outty ::right_p @ [k])),k
1529 Cic.Prod (Cic.Name "p",
1530 Cic.Appl [eq; mty; m; k],
1532 (CR.head_beta_reduce ~delta:false
1533 (Cic.Appl (outty ::right_p @ [k]))))),k
1536 aux context outty [] 1 mty m cty
1538 let add_lambda_for_refl_m pbo rno mty m k cty =
1539 (* k lives in the right context *)
1540 if rno <> 0 then pbo else
1541 let rec aux mty m = function
1542 | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1543 Cic.Lambda (name,src,
1544 (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1546 Cic.Lambda (Cic.Name "p",
1547 Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1551 let add_pi_for_refl_m new_outty mty m rno =
1552 if rno <> 0 then new_outty else
1553 let rec aux m mty = function
1554 | Cic.Lambda (name, src, tgt) ->
1555 Cic.Lambda (name, src,
1556 aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1559 (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1563 in (* }}} end helper functions *)
1564 (* constructors types with left params already instantiated *)
1565 let outty = CicMetaSubst.apply_subst subst outty in
1566 let cl, left_p, leftno,rno,ugraph =
1567 get_cl_and_left_p uri tyno outty ugraph
1572 CicTypeChecker.type_of_aux' ~subst metasenv context m
1573 CicUniv.oblivion_ugraph
1575 | Cic.MutInd _ as mty,_ -> [], mty
1576 | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
1577 snd (HExtlib.split_nth leftno args), mty
1579 with CicTypeChecker.TypeCheckerFailure _ -> assert false
1582 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1585 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1586 ~metasenv subst new_outty context));
1587 let _,pl,subst,metasenv,ugraph =
1589 (fun cty pbo (i, acc, s, menv, ugraph) ->
1590 (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1591 * (new_)outty right_par (K_i left_par k_par) *)
1593 add_params menv s context uri tyno
1594 cty outty mty m leftno i in
1596 (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1597 ~metasenv subst infty_pbo context));
1598 let expty_pbo, k = (* k is (K_i left_par k_par) *)
1599 add_params menv s context uri tyno
1600 cty new_outty mty m leftno i in
1602 (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1603 ~metasenv subst expty_pbo context));
1604 let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1606 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1607 ~metasenv subst pbo context));
1608 let (pbo, _), subst, metasenv, ugraph =
1609 coerce_to_something_aux pbo infty_pbo expty_pbo
1610 s menv context ugraph
1613 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1614 ~metasenv subst pbo context));
1615 (i-1, pbo::acc, subst, metasenv, ugraph))
1616 cl pl (List.length pl, [], subst, metasenv, ugraph)
1618 let new_outty = add_pi_for_refl_m new_outty mty m rno in
1620 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1621 ~metasenv subst new_outty context));
1624 let refl_m=Cic.Appl[eq_refl;mty;m]in
1625 Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1627 Cic.MutCase(uri,tyno,new_outty,m,pl)
1629 (t, expty), subst, metasenv, ugraph (*}}}*)
1630 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1631 (*{{{*) debug_print (lazy "LAM");
1633 FreshNamesGenerator.mk_fresh_name
1634 ~subst metasenv context ~typ:src2 Cic.Anonymous
1636 let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1637 (* contravariant part: the argument of f:src->ty *)
1638 let (rel1, _), subst, metasenv, ugraph =
1639 coerce_to_something_aux
1640 (Cic.Rel 1) (CS.lift 1 src2)
1641 (CS.lift 1 src) subst metasenv context_src2 ugraph
1643 (* covariant part: the result of f(c x); x:src2; (c x):src *)
1646 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1647 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1649 (* we fix the possible dependency problem in the source ty *)
1650 let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1651 let (bo, _), subst, metasenv, ugraph =
1652 coerce_to_something_aux
1653 bo ty ty2 subst metasenv context_src2 ugraph
1655 let coerced = Cic.Lambda (name_t,src2, bo) in
1656 (coerced, expty), subst, metasenv, ugraph (*}}}*)
1658 (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1659 ~metasenv subst infty context ^ " ==> " ^
1660 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1661 coerce_atom_to_something
1662 t infty expty subst metasenv context ugraph (*}}}*)
1664 debug_print (lazy ("COERCE TO SOMETHING END: "^
1665 CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1669 coerce_to_something_aux t infty expty subst metasenv context ugraph
1670 with Uncertain _ | RefineFailure _ as exn ->
1673 CicMetaSubst.ppterm_in_context metasenv subst t context ^
1674 " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1675 infty context ^ " but is here used with type " ^
1676 CicMetaSubst.ppterm_in_context metasenv subst expty context)
1678 enrich localization_tbl ~f t exn
1680 and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1681 match CicReduction.whd ~delta:false ~subst context infty with
1682 | Cic.Meta _ | Cic.Sort _ ->
1683 t,infty, subst, metasenv, ugraph
1685 debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1686 ~metasenv subst src context));
1687 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1689 let (t, ty_t), subst, metasenv, ugraph =
1690 coerce_to_something true
1691 localization_tbl t src tgt subst metasenv context ugraph
1693 debug_print (lazy ("COERCE TO SORT END: "^
1694 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1695 t, ty_t, subst, metasenv, ugraph
1696 with HExtlib.Localized (_, exn) ->
1698 lazy ("(7)The term " ^
1699 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1700 ^ " is not a type since it has type " ^
1701 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1702 ^ " that is not a sort")
1704 enrich localization_tbl ~f t exn
1707 (* eat prods ends here! *)
1709 let t',ty,subst',metasenv',ugraph1 =
1710 type_of_aux [] metasenv context t ugraph
1712 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1713 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1714 (* Andrea: ho rimesso qui l'applicazione della subst al
1715 metasenv dopo che ho droppato l'invariante che il metsaenv
1716 e' sempre istanziato *)
1717 let substituted_metasenv =
1718 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1720 (* substituted_t,substituted_ty,substituted_metasenv *)
1721 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1723 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1725 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1726 let cleaned_metasenv =
1728 (function (n,context,ty) ->
1729 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1734 | Some (n, Cic.Decl t) ->
1736 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1737 | Some (n, Cic.Def (bo,ty)) ->
1738 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1743 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1745 Some (n, Cic.Def (bo',ty'))
1749 ) substituted_metasenv
1751 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1754 let undebrujin uri typesno tys t =
1757 (fun (name,_,_,_) (i,t) ->
1758 (* here the explicit_named_substituion is assumed to be *)
1760 let t' = Cic.MutInd (uri,i,[]) in
1761 let t = CicSubstitution.subst t' t in
1763 ) tys (typesno - 1,t))
1765 let map_first_n n start f g l =
1766 let rec aux acc k l =
1769 | [] -> raise (Invalid_argument "map_first_n")
1770 | hd :: tl -> f hd k (aux acc (k+1) tl)
1776 (*CSC: this is a very rough approximation; to be finished *)
1777 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1778 let subst,metasenv,ugraph,tys =
1780 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1781 let subst,metasenv,ugraph,cl =
1783 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1784 let rec aux ctx k subst = function
1785 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1786 let subst,metasenv,ugraph,tl =
1788 (subst,metasenv,ugraph,[])
1789 (fun t n (subst,metasenv,ugraph,acc) ->
1790 let subst,metasenv,ugraph =
1792 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1794 subst,metasenv,ugraph,(t::acc))
1795 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1798 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1799 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1800 subst,metasenv,ugraph,t
1801 | Cic.Prod (name,s,t) ->
1802 let ctx = (Some (name,Cic.Decl s))::ctx in
1803 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1804 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1808 (lazy "not well formed constructor type"))
1810 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1811 subst,metasenv,ugraph,(name,ty) :: acc)
1812 cl (subst,metasenv,ugraph,[])
1814 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1815 tys ([],metasenv,ugraph,[])
1817 let substituted_tys =
1819 (fun (name,ind,arity,cl) ->
1821 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1823 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1826 metasenv,ugraph,substituted_tys
1828 let typecheck metasenv uri obj ~localization_tbl =
1829 let ugraph = CicUniv.empty_ugraph in
1831 Cic.Constant (name,Some bo,ty,args,attrs) ->
1832 (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
1833 since type_of_aux' destroys localization information (which are
1834 preserved by type_of_aux *)
1837 Cic.CicHash.find localization_tbl bo
1839 HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
1841 let bo',boty,metasenv,ugraph =
1842 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1843 let ty',_,metasenv,ugraph =
1844 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1845 let subst,metasenv,ugraph =
1847 fo_unif_subst [] [] metasenv boty ty' ugraph
1850 | Uncertain _ as exn ->
1853 CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
1855 CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
1856 " but is here used with type " ^
1857 CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
1861 RefineFailure _ -> RefineFailure msg
1862 | Uncertain _ -> Uncertain msg
1865 raise (HExtlib.Localized (loc exn',exn'))
1867 let bo' = CicMetaSubst.apply_subst subst bo' in
1868 let ty' = CicMetaSubst.apply_subst subst ty' in
1869 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1870 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1871 | Cic.Constant (name,None,ty,args,attrs) ->
1872 let ty',_,metasenv,ugraph =
1873 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1875 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1876 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1877 assert (metasenv' = metasenv);
1878 (* Here we do not check the metasenv for correctness *)
1879 let bo',boty,metasenv,ugraph =
1880 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1881 let ty',sort,metasenv,ugraph =
1882 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1886 (* instead of raising Uncertain, let's hope that the meta will become
1889 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1891 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1892 let bo' = CicMetaSubst.apply_subst subst bo' in
1893 let ty' = CicMetaSubst.apply_subst subst ty' in
1894 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1895 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1896 | Cic.Variable _ -> assert false (* not implemented *)
1897 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1898 (*CSC: this code is greately simplified and many many checks are missing *)
1899 (*CSC: e.g. the constructors are not required to build their own types, *)
1900 (*CSC: the arities are not required to have as type a sort, etc. *)
1901 let uri = match uri with Some uri -> uri | None -> assert false in
1902 let typesno = List.length tys in
1903 (* first phase: we fix only the types *)
1904 let metasenv,ugraph,tys =
1906 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1907 let ty',_,metasenv,ugraph =
1908 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1910 metasenv,ugraph,(name,b,ty',cl)::res
1911 ) tys (metasenv,ugraph,[]) in
1913 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1914 (* second phase: we fix only the constructors *)
1915 let saved_menv = metasenv in
1916 let metasenv,ugraph,tys =
1918 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1919 let metasenv,ugraph,cl' =
1921 (fun (name,ty) (metasenv,ugraph,res) ->
1923 CicTypeChecker.debrujin_constructor
1924 ~cb:(relocalize localization_tbl) uri typesno ty in
1925 let ty',_,metasenv,ugraph =
1926 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1927 let ty' = undebrujin uri typesno tys ty' in
1928 metasenv@saved_menv,ugraph,(name,ty')::res
1929 ) cl (metasenv,ugraph,[])
1931 metasenv,ugraph,(name,b,ty,cl')::res
1932 ) tys (metasenv,ugraph,[]) in
1933 (* third phase: we check the positivity condition *)
1934 let metasenv,ugraph,tys =
1935 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1937 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1940 (* sara' piu' veloce che raffinare da zero? mah.... *)
1941 let pack_coercion metasenv ctx t =
1942 let module C = Cic in
1943 let rec merge_coercions ctx =
1944 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1946 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1947 | C.Meta (n,subst) ->
1950 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1953 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1954 | C.Prod (name,so,dest) ->
1955 let ctx' = (Some (name,C.Decl so))::ctx in
1956 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1957 | C.Lambda (name,so,dest) ->
1958 let ctx' = (Some (name,C.Decl so))::ctx in
1959 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1960 | C.LetIn (name,so,dest) ->
1961 let _,ty,metasenv,ugraph =
1962 pack_coercions := false;
1963 type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1964 pack_coercions := true;
1965 let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1966 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1968 let l = List.map (merge_coercions ctx) l in
1970 let b,_,_,_,_ = is_a_double_coercion t in
1972 let ugraph = CicUniv.oblivion_ugraph in
1973 let old_insert_coercions = !insert_coercions in
1974 insert_coercions := false;
1975 let newt, _, menv, _ =
1977 type_of_aux' metasenv ctx t ugraph
1978 with RefineFailure _ | Uncertain _ ->
1981 insert_coercions := old_insert_coercions;
1982 if metasenv <> [] || menv = [] then
1985 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1988 | C.Var (uri,exp_named_subst) ->
1989 let exp_named_subst = List.map aux exp_named_subst in
1990 C.Var (uri, exp_named_subst)
1991 | C.Const (uri,exp_named_subst) ->
1992 let exp_named_subst = List.map aux exp_named_subst in
1993 C.Const (uri, exp_named_subst)
1994 | C.MutInd (uri,tyno,exp_named_subst) ->
1995 let exp_named_subst = List.map aux exp_named_subst in
1996 C.MutInd (uri,tyno,exp_named_subst)
1997 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1998 let exp_named_subst = List.map aux exp_named_subst in
1999 C.MutConstruct (uri,tyno,consno,exp_named_subst)
2000 | C.MutCase (uri,tyno,out,te,pl) ->
2001 let pl = List.map (merge_coercions ctx) pl in
2002 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
2003 | C.Fix (fno, fl) ->
2006 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2011 (fun (name,idx,ty,bo) ->
2012 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
2016 | C.CoFix (fno, fl) ->
2019 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2024 (fun (name,ty,bo) ->
2025 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
2030 merge_coercions ctx t
2033 let pack_coercion_metasenv conjectures = conjectures (*
2035 TASSI: this code war written when coercions were a toy,
2036 now packing coercions involves unification thus
2037 the metasenv may change, and this pack coercion
2038 does not handle that.
2040 let module C = Cic in
2042 (fun (i, ctx, ty) ->
2048 Some (name, C.Decl t) ->
2049 Some (name, C.Decl (pack_coercion conjectures ctx t))
2050 | Some (name, C.Def (t,None)) ->
2051 Some (name,C.Def (pack_coercion conjectures ctx t,None))
2052 | Some (name, C.Def (t,Some ty)) ->
2053 Some (name, C.Def (pack_coercion conjectures ctx t,
2054 Some (pack_coercion conjectures ctx ty)))
2060 ((i,ctx,pack_coercion conjectures ctx ty))
2065 let pack_coercion_obj obj = obj (*
2067 TASSI: this code war written when coercions were a toy,
2068 now packing coercions involves unification thus
2069 the metasenv may change, and this pack coercion
2070 does not handle that.
2072 let module C = Cic in
2074 | C.Constant (id, body, ty, params, attrs) ->
2078 | Some body -> Some (pack_coercion [] [] body)
2080 let ty = pack_coercion [] [] ty in
2081 C.Constant (id, body, ty, params, attrs)
2082 | C.Variable (name, body, ty, params, attrs) ->
2086 | Some body -> Some (pack_coercion [] [] body)
2088 let ty = pack_coercion [] [] ty in
2089 C.Variable (name, body, ty, params, attrs)
2090 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2091 let conjectures = pack_coercion_metasenv conjectures in
2092 let body = pack_coercion conjectures [] body in
2093 let ty = pack_coercion conjectures [] ty in
2094 C.CurrentProof (name, conjectures, body, ty, params, attrs)
2095 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2098 (fun (name, ind, arity, cl) ->
2099 let arity = pack_coercion [] [] arity in
2101 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2103 (name, ind, arity, cl))
2106 C.InductiveDefinition (indtys, params, leftno, attrs) *)
2111 let type_of_aux' metasenv context term =
2114 type_of_aux' metasenv context term in
2116 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2118 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2121 | RefineFailure msg as e ->
2122 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2124 | Uncertain msg as e ->
2125 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2129 let profiler2 = HExtlib.profile "CicRefine"
2131 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2132 profiler2.HExtlib.profile
2133 (type_of_aux' ?localization_tbl metasenv context term) ugraph
2135 let typecheck ~localization_tbl metasenv uri obj =
2136 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2138 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2139 (* vim:set foldmethod=marker: *)