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
1207 let subst,metasenv,ugraph =
1208 fo_unif_subst subst context metasenv last he ugraph in
1209 debug_print (lazy ("New head: "^ pp coerc));
1212 CicTypeChecker.type_of_aux' ~subst metasenv context coerc ugraph in
1213 debug_print (lazy (" has type: "^ pp tty));
1214 Some (coerc,tty,subst,metasenv,ugraph)
1216 | Uncertain _ | RefineFailure _
1217 | HExtlib.Localized (_,Uncertain _)
1218 | HExtlib.Localized (_,RefineFailure _) -> None
1219 | exn -> assert false)
1222 (* aux function to process the type of the head and the args in parallel *)
1223 let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1225 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1226 | (hete, hety)::tl as args ->
1227 match (CicReduction.whd ~subst context hetype) with
1228 | Cic.Prod (n,s,t) ->
1229 let arg,subst,metasenv,ugraph =
1230 coerce_to_something allow_coercions localization_tbl
1231 hete hety s subst metasenv context ugraph in
1233 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1234 ugraph (newargs@[arg]) tl
1237 match he, newargs with
1239 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1240 | _ -> Cic.Appl (he::List.map fst newargs)
1242 (*{{{*) debug_print (lazy
1244 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1245 "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1246 "\n but is applyed to: " ^ String.concat ";"
1247 (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1248 let possible_fixes =
1249 fix_arity (List.length args) metasenv context subst he hetype
1252 HExtlib.list_findopt
1253 (fun (he,hetype,subst,metasenv,ugraph) ->
1254 (* {{{ *)debug_print (lazy ("Try fix: "^
1255 CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1256 debug_print (lazy (" of type: "^
1257 CicMetaSubst.ppterm_in_context
1258 ~metasenv subst hetype context)); (* }}} *)
1260 Some (eat_prods_and_args
1261 metasenv subst context he hetype ugraph [] args)
1263 | RefineFailure _ | Uncertain _
1264 | HExtlib.Localized (_,RefineFailure _)
1265 | HExtlib.Localized (_,Uncertain _) -> None)
1271 (MoreArgsThanExpected
1272 (List.length args, RefineFailure (lazy "")))
1274 (* first we check if we are in the simple case of a meta closed term *)
1275 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1276 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1277 (* this optimization is to postpone fix_arity (the most common case)*)
1278 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1280 (* this (says CSC) is also useful to infer dependent types *)
1281 let pristinemenv = metasenv in
1282 let metasenv,hetype' =
1283 mk_prod_of_metas metasenv context subst args_bo_and_ty
1286 let subst,metasenv,ugraph =
1287 fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1289 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1290 with RefineFailure _ | Uncertain _ ->
1291 subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1293 let coerced_args,subst,metasenv,he,t,ugraph =
1296 metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1298 MoreArgsThanExpected (residuals,exn) ->
1299 more_args_than_expected localization_tbl metasenv
1300 subst he context hetype' residuals args_bo_and_ty exn
1302 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1304 and coerce_to_something
1305 allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1307 let module CS = CicSubstitution in
1308 let module CR = CicReduction in
1309 let cs_subst = CS.subst ~avoid_beta_redexes:true in
1310 let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1311 debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1313 CoercGraph.look_for_coercion metasenv subst context infty expty
1316 | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
1317 "coerce_atom_to_something fails since not meta closed"))
1318 | CoercGraph.NoCoercion
1319 | CoercGraph.SomeCoercionToTgt _
1320 | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
1321 "coerce_atom_to_something fails since no coercions found"))
1322 | CoercGraph.SomeCoercion candidates ->
1323 debug_print (lazy (string_of_int (List.length candidates) ^
1324 " candidates found"));
1325 let uncertain = ref false in
1329 (fun (metasenv,last,c) ->
1331 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1332 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1334 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
1335 "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
1337 debug_print (lazy ("FO_UNIF_SUBST: " ^
1338 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1339 let subst,metasenv,ugraph =
1340 fo_unif_subst subst context metasenv last t ugraph
1342 let newt,newhety,subst,metasenv,ugraph =
1343 type_of_aux subst metasenv context c ugraph in
1344 let newt, newty, subst, metasenv, ugraph =
1345 avoid_double_coercion context subst metasenv ugraph newt expty
1347 let subst,metasenv,ugraph =
1348 fo_unif_subst subst context metasenv newhety expty ugraph in
1349 Some ((newt,newty), subst, metasenv, ugraph)
1351 | Uncertain _ -> uncertain := true; None
1352 | RefineFailure _ -> None)
1357 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1365 | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1366 | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1368 let rec coerce_to_something_aux
1369 t infty expty subst metasenv context ugraph
1372 let subst, metasenv, ugraph =
1373 fo_unif_subst subst context metasenv infty expty ugraph
1375 (t, expty), subst, metasenv, ugraph
1376 with (Uncertain _ | RefineFailure _ as exn)
1377 when allow_coercions && !insert_coercions ->
1378 let whd = CicReduction.whd ~delta:false in
1379 let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1380 let infty = clean infty subst context in
1381 let expty = clean expty subst context in
1382 let t = clean t subst context in
1383 (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1384 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1385 CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1386 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1387 let (coerced,_),subst,metasenv,_ as result =
1388 match infty, expty, t with
1389 | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1390 (*{{{*) debug_print (lazy "FIX");
1392 [name,i,_(* infty *),bo] ->
1394 Some (Cic.Name name,Cic.Decl expty)::context in
1395 let (rel1, _), subst, metasenv, ugraph =
1396 coerce_to_something_aux (Cic.Rel 1)
1397 (CS.lift 1 expty) (CS.lift 1 infty) subst
1398 metasenv context_bo ugraph in
1399 let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1400 let (bo,_), subst, metasenv, ugraph =
1401 coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1403 metasenv context_bo ugraph
1405 (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1406 | _ -> assert false (* not implemented yet *)) (*}}}*)
1407 | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1408 (*{{{*) debug_print (lazy "CASE");
1409 (* {{{ helper functions *)
1410 let get_cl_and_left_p uri tyno outty ugraph =
1411 match CicEnvironment.get_obj ugraph uri with
1412 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1415 match CicReduction.whd ~delta:false ctx t with
1416 | Cic.Prod (name,src,tgt) ->
1417 let ctx = Some (name, Cic.Decl src) :: ctx in
1423 let rec skip_lambda_delifting t n =
1426 | Cic.Lambda (_,_,t),n ->
1427 skip_lambda_delifting
1428 (CS.subst (Cic.Implicit None) t) (n - 1)
1431 let get_l_r_p n = function
1432 | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1433 | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1434 HExtlib.split_nth n args
1437 let _, _, ty, cl = List.nth tl tyno in
1438 let pis = count_pis ty in
1439 let rno = pis - leftno in
1440 let t = skip_lambda_delifting outty rno in
1441 let left_p, _ = get_l_r_p leftno t in
1442 let instantiale_with_left cl =
1446 (fun t p -> match t with
1447 | Cic.Prod (_,_,t) ->
1453 let cl = instantiale_with_left (List.map snd cl) in
1454 cl, left_p, leftno, rno, ugraph
1457 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1460 let rec mkr n = function
1461 | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1464 CicReplace.replace_lifting
1465 ~equality:(fun _ -> CicUtil.alpha_equivalence)
1467 ~what:(matched::right_p)
1468 ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1472 | Cic.Lambda (name, src, tgt),_ ->
1473 Cic.Lambda (name, src,
1474 keep_lambdas_and_put_expty
1475 (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1476 (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1479 let eq_uri, eq, eq_refl =
1480 match LibraryObjects.eq_URI () with
1481 | None -> HLog.warn "no default equality"; raise exn
1482 | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1485 metasenv subst context uri tyno cty outty mty m leftno i
1487 let rec aux context outty par k mty m = function
1488 | Cic.Prod (name, src, tgt) ->
1491 (Some (name, Cic.Decl src) :: context)
1492 (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1493 (CS.lift 1 mty) (CS.lift 1 m) tgt
1495 Cic.Prod (name, src, t), k
1498 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1499 if par <> [] then Cic.Appl (k::par) else k
1501 Cic.Prod (Cic.Name "p",
1502 Cic.Appl [eq; mty; m; k],
1504 (CR.head_beta_reduce ~delta:false
1505 (Cic.Appl [outty;k])))),k
1506 | Cic.Appl (Cic.MutInd _::pl) ->
1507 let left_p,right_p = HExtlib.split_nth leftno pl in
1508 let has_rights = right_p <> [] in
1510 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1511 Cic.Appl (k::left_p@par)
1515 CicTypeChecker.type_of_aux' ~subst metasenv context k
1516 CicUniv.oblivion_ugraph
1518 | Cic.Appl (Cic.MutInd _::args),_ ->
1519 snd (HExtlib.split_nth leftno args)
1521 with CicTypeChecker.TypeCheckerFailure _-> assert false
1524 CR.head_beta_reduce ~delta:false
1525 (Cic.Appl (outty ::right_p @ [k])),k
1527 Cic.Prod (Cic.Name "p",
1528 Cic.Appl [eq; mty; m; k],
1530 (CR.head_beta_reduce ~delta:false
1531 (Cic.Appl (outty ::right_p @ [k]))))),k
1534 aux context outty [] 1 mty m cty
1536 let add_lambda_for_refl_m pbo rno mty m k cty =
1537 (* k lives in the right context *)
1538 if rno <> 0 then pbo else
1539 let rec aux mty m = function
1540 | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1541 Cic.Lambda (name,src,
1542 (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1544 Cic.Lambda (Cic.Name "p",
1545 Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1549 let add_pi_for_refl_m new_outty mty m rno =
1550 if rno <> 0 then new_outty else
1551 let rec aux m mty = function
1552 | Cic.Lambda (name, src, tgt) ->
1553 Cic.Lambda (name, src,
1554 aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1557 (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1561 in (* }}} end helper functions *)
1562 (* constructors types with left params already instantiated *)
1563 let outty = CicMetaSubst.apply_subst subst outty in
1564 let cl, left_p, leftno,rno,ugraph =
1565 get_cl_and_left_p uri tyno outty ugraph
1570 CicTypeChecker.type_of_aux' ~subst metasenv context m
1571 CicUniv.oblivion_ugraph
1573 | Cic.MutInd _ as mty,_ -> [], mty
1574 | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
1575 snd (HExtlib.split_nth leftno args), mty
1577 with CicTypeChecker.TypeCheckerFailure _ -> assert false
1580 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1583 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1584 ~metasenv subst new_outty context));
1585 let _,pl,subst,metasenv,ugraph =
1587 (fun cty pbo (i, acc, s, menv, ugraph) ->
1588 (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1589 * (new_)outty right_par (K_i left_par k_par) *)
1591 add_params menv s context uri tyno
1592 cty outty mty m leftno i in
1594 (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1595 ~metasenv subst infty_pbo context));
1596 let expty_pbo, k = (* k is (K_i left_par k_par) *)
1597 add_params menv s context uri tyno
1598 cty new_outty mty m leftno i in
1600 (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1601 ~metasenv subst expty_pbo context));
1602 let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1604 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1605 ~metasenv subst pbo context));
1606 let (pbo, _), subst, metasenv, ugraph =
1607 coerce_to_something_aux pbo infty_pbo expty_pbo
1608 s menv context ugraph
1611 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1612 ~metasenv subst pbo context));
1613 (i-1, pbo::acc, subst, metasenv, ugraph))
1614 cl pl (List.length pl, [], subst, metasenv, ugraph)
1616 let new_outty = add_pi_for_refl_m new_outty mty m rno in
1618 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1619 ~metasenv subst new_outty context));
1622 let refl_m=Cic.Appl[eq_refl;mty;m]in
1623 Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1625 Cic.MutCase(uri,tyno,new_outty,m,pl)
1627 (t, expty), subst, metasenv, ugraph (*}}}*)
1628 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1629 (*{{{*) debug_print (lazy "LAM");
1631 FreshNamesGenerator.mk_fresh_name
1632 ~subst metasenv context ~typ:src2 Cic.Anonymous
1634 let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1635 (* contravariant part: the argument of f:src->ty *)
1636 let (rel1, _), subst, metasenv, ugraph =
1637 coerce_to_something_aux
1638 (Cic.Rel 1) (CS.lift 1 src2)
1639 (CS.lift 1 src) subst metasenv context_src2 ugraph
1641 (* covariant part: the result of f(c x); x:src2; (c x):src *)
1644 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1645 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1647 (* we fix the possible dependency problem in the source ty *)
1648 let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1649 let (bo, _), subst, metasenv, ugraph =
1650 coerce_to_something_aux
1651 bo ty ty2 subst metasenv context_src2 ugraph
1653 let coerced = Cic.Lambda (name_t,src2, bo) in
1654 (coerced, expty), subst, metasenv, ugraph (*}}}*)
1656 (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1657 ~metasenv subst infty context ^ " ==> " ^
1658 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1659 coerce_atom_to_something
1660 t infty expty subst metasenv context ugraph (*}}}*)
1662 debug_print (lazy ("COERCE TO SOMETHING END: "^
1663 CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1667 coerce_to_something_aux t infty expty subst metasenv context ugraph
1668 with Uncertain _ | RefineFailure _ as exn ->
1671 CicMetaSubst.ppterm_in_context metasenv subst t context ^
1672 " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1673 infty context ^ " but is here used with type " ^
1674 CicMetaSubst.ppterm_in_context metasenv subst expty context)
1676 enrich localization_tbl ~f t exn
1678 and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1679 match CicReduction.whd ~delta:false ~subst context infty with
1680 | Cic.Meta _ | Cic.Sort _ ->
1681 t,infty, subst, metasenv, ugraph
1683 debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1684 ~metasenv subst src context));
1685 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1687 let (t, ty_t), subst, metasenv, ugraph =
1688 coerce_to_something true
1689 localization_tbl t src tgt subst metasenv context ugraph
1691 debug_print (lazy ("COERCE TO SORT END: "^
1692 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1693 t, ty_t, subst, metasenv, ugraph
1694 with HExtlib.Localized (_, exn) ->
1696 lazy ("(7)The term " ^
1697 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1698 ^ " is not a type since it has type " ^
1699 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1700 ^ " that is not a sort")
1702 enrich localization_tbl ~f t exn
1705 (* eat prods ends here! *)
1707 let t',ty,subst',metasenv',ugraph1 =
1708 type_of_aux [] metasenv context t ugraph
1710 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1711 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1712 (* Andrea: ho rimesso qui l'applicazione della subst al
1713 metasenv dopo che ho droppato l'invariante che il metsaenv
1714 e' sempre istanziato *)
1715 let substituted_metasenv =
1716 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1718 (* substituted_t,substituted_ty,substituted_metasenv *)
1719 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1721 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1723 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1724 let cleaned_metasenv =
1726 (function (n,context,ty) ->
1727 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1732 | Some (n, Cic.Decl t) ->
1734 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1735 | Some (n, Cic.Def (bo,ty)) ->
1736 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1741 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1743 Some (n, Cic.Def (bo',ty'))
1747 ) substituted_metasenv
1749 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1752 let undebrujin uri typesno tys t =
1755 (fun (name,_,_,_) (i,t) ->
1756 (* here the explicit_named_substituion is assumed to be *)
1758 let t' = Cic.MutInd (uri,i,[]) in
1759 let t = CicSubstitution.subst t' t in
1761 ) tys (typesno - 1,t))
1763 let map_first_n n start f g l =
1764 let rec aux acc k l =
1767 | [] -> raise (Invalid_argument "map_first_n")
1768 | hd :: tl -> f hd k (aux acc (k+1) tl)
1774 (*CSC: this is a very rough approximation; to be finished *)
1775 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1776 let subst,metasenv,ugraph,tys =
1778 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1779 let subst,metasenv,ugraph,cl =
1781 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1782 let rec aux ctx k subst = function
1783 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1784 let subst,metasenv,ugraph,tl =
1786 (subst,metasenv,ugraph,[])
1787 (fun t n (subst,metasenv,ugraph,acc) ->
1788 let subst,metasenv,ugraph =
1790 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1792 subst,metasenv,ugraph,(t::acc))
1793 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1796 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1797 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1798 subst,metasenv,ugraph,t
1799 | Cic.Prod (name,s,t) ->
1800 let ctx = (Some (name,Cic.Decl s))::ctx in
1801 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1802 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1806 (lazy "not well formed constructor type"))
1808 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1809 subst,metasenv,ugraph,(name,ty) :: acc)
1810 cl (subst,metasenv,ugraph,[])
1812 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1813 tys ([],metasenv,ugraph,[])
1815 let substituted_tys =
1817 (fun (name,ind,arity,cl) ->
1819 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1821 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1824 metasenv,ugraph,substituted_tys
1826 let typecheck metasenv uri obj ~localization_tbl =
1827 let ugraph = CicUniv.empty_ugraph in
1829 Cic.Constant (name,Some bo,ty,args,attrs) ->
1830 let bo',boty,metasenv,ugraph =
1831 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1832 let ty',_,metasenv,ugraph =
1833 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1834 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1835 let bo' = CicMetaSubst.apply_subst subst bo' in
1836 let ty' = CicMetaSubst.apply_subst subst ty' in
1837 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1838 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1839 | Cic.Constant (name,None,ty,args,attrs) ->
1840 let ty',_,metasenv,ugraph =
1841 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1843 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1844 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1845 assert (metasenv' = metasenv);
1846 (* Here we do not check the metasenv for correctness *)
1847 let bo',boty,metasenv,ugraph =
1848 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1849 let ty',sort,metasenv,ugraph =
1850 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1854 (* instead of raising Uncertain, let's hope that the meta will become
1857 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1859 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1860 let bo' = CicMetaSubst.apply_subst subst bo' in
1861 let ty' = CicMetaSubst.apply_subst subst ty' in
1862 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1863 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1864 | Cic.Variable _ -> assert false (* not implemented *)
1865 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1866 (*CSC: this code is greately simplified and many many checks are missing *)
1867 (*CSC: e.g. the constructors are not required to build their own types, *)
1868 (*CSC: the arities are not required to have as type a sort, etc. *)
1869 let uri = match uri with Some uri -> uri | None -> assert false in
1870 let typesno = List.length tys in
1871 (* first phase: we fix only the types *)
1872 let metasenv,ugraph,tys =
1874 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1875 let ty',_,metasenv,ugraph =
1876 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1878 metasenv,ugraph,(name,b,ty',cl)::res
1879 ) tys (metasenv,ugraph,[]) in
1881 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1882 (* second phase: we fix only the constructors *)
1883 let saved_menv = metasenv in
1884 let metasenv,ugraph,tys =
1886 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1887 let metasenv,ugraph,cl' =
1889 (fun (name,ty) (metasenv,ugraph,res) ->
1891 CicTypeChecker.debrujin_constructor
1892 ~cb:(relocalize localization_tbl) uri typesno ty in
1893 let ty',_,metasenv,ugraph =
1894 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1895 let ty' = undebrujin uri typesno tys ty' in
1896 metasenv@saved_menv,ugraph,(name,ty')::res
1897 ) cl (metasenv,ugraph,[])
1899 metasenv,ugraph,(name,b,ty,cl')::res
1900 ) tys (metasenv,ugraph,[]) in
1901 (* third phase: we check the positivity condition *)
1902 let metasenv,ugraph,tys =
1903 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1905 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1908 (* sara' piu' veloce che raffinare da zero? mah.... *)
1909 let pack_coercion metasenv ctx t =
1910 let module C = Cic in
1911 let rec merge_coercions ctx =
1912 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1914 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1915 | C.Meta (n,subst) ->
1918 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1921 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1922 | C.Prod (name,so,dest) ->
1923 let ctx' = (Some (name,C.Decl so))::ctx in
1924 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1925 | C.Lambda (name,so,dest) ->
1926 let ctx' = (Some (name,C.Decl so))::ctx in
1927 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1928 | C.LetIn (name,so,dest) ->
1929 let _,ty,metasenv,ugraph =
1930 pack_coercions := false;
1931 type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1932 pack_coercions := true;
1933 let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1934 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1936 let l = List.map (merge_coercions ctx) l in
1938 let b,_,_,_,_ = is_a_double_coercion t in
1940 let ugraph = CicUniv.oblivion_ugraph in
1941 let old_insert_coercions = !insert_coercions in
1942 insert_coercions := false;
1943 let newt, _, menv, _ =
1945 type_of_aux' metasenv ctx t ugraph
1946 with RefineFailure _ | Uncertain _ ->
1949 insert_coercions := old_insert_coercions;
1950 if metasenv <> [] || menv = [] then
1953 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1956 | C.Var (uri,exp_named_subst) ->
1957 let exp_named_subst = List.map aux exp_named_subst in
1958 C.Var (uri, exp_named_subst)
1959 | C.Const (uri,exp_named_subst) ->
1960 let exp_named_subst = List.map aux exp_named_subst in
1961 C.Const (uri, exp_named_subst)
1962 | C.MutInd (uri,tyno,exp_named_subst) ->
1963 let exp_named_subst = List.map aux exp_named_subst in
1964 C.MutInd (uri,tyno,exp_named_subst)
1965 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1966 let exp_named_subst = List.map aux exp_named_subst in
1967 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1968 | C.MutCase (uri,tyno,out,te,pl) ->
1969 let pl = List.map (merge_coercions ctx) pl in
1970 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1971 | C.Fix (fno, fl) ->
1974 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1979 (fun (name,idx,ty,bo) ->
1980 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1984 | C.CoFix (fno, fl) ->
1987 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1992 (fun (name,ty,bo) ->
1993 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1998 merge_coercions ctx t
2001 let pack_coercion_metasenv conjectures = conjectures (*
2003 TASSI: this code war written when coercions were a toy,
2004 now packing coercions involves unification thus
2005 the metasenv may change, and this pack coercion
2006 does not handle that.
2008 let module C = Cic in
2010 (fun (i, ctx, ty) ->
2016 Some (name, C.Decl t) ->
2017 Some (name, C.Decl (pack_coercion conjectures ctx t))
2018 | Some (name, C.Def (t,None)) ->
2019 Some (name,C.Def (pack_coercion conjectures ctx t,None))
2020 | Some (name, C.Def (t,Some ty)) ->
2021 Some (name, C.Def (pack_coercion conjectures ctx t,
2022 Some (pack_coercion conjectures ctx ty)))
2028 ((i,ctx,pack_coercion conjectures ctx ty))
2033 let pack_coercion_obj obj = obj (*
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 | C.Constant (id, body, ty, params, attrs) ->
2046 | Some body -> Some (pack_coercion [] [] body)
2048 let ty = pack_coercion [] [] ty in
2049 C.Constant (id, body, ty, params, attrs)
2050 | C.Variable (name, body, ty, params, attrs) ->
2054 | Some body -> Some (pack_coercion [] [] body)
2056 let ty = pack_coercion [] [] ty in
2057 C.Variable (name, body, ty, params, attrs)
2058 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2059 let conjectures = pack_coercion_metasenv conjectures in
2060 let body = pack_coercion conjectures [] body in
2061 let ty = pack_coercion conjectures [] ty in
2062 C.CurrentProof (name, conjectures, body, ty, params, attrs)
2063 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2066 (fun (name, ind, arity, cl) ->
2067 let arity = pack_coercion [] [] arity in
2069 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2071 (name, ind, arity, cl))
2074 C.InductiveDefinition (indtys, params, leftno, attrs) *)
2079 let type_of_aux' metasenv context term =
2082 type_of_aux' metasenv context term in
2084 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2086 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2089 | RefineFailure msg as e ->
2090 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2092 | Uncertain msg as e ->
2093 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2097 let profiler2 = HExtlib.profile "CicRefine"
2099 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2100 profiler2.HExtlib.profile
2101 (type_of_aux' ?localization_tbl metasenv context term) ugraph
2103 let typecheck ~localization_tbl metasenv uri obj =
2104 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2106 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2107 (* vim:set foldmethod=marker: *)