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 (* Cic.Name "pippo" *)
195 FreshNamesGenerator.mk_fresh_name ~subst metasenv
196 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
197 (CicMetaSubst.apply_subst_context subst context')
199 ~typ:(CicMetaSubst.apply_subst subst argty)
201 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
202 FreshNamesGenerator.mk_fresh_name ~subst
203 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
205 let metasenv,target =
206 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
208 metasenv,Cic.Prod (name,meta,target)
210 mk_prod metasenv context' args
213 let rec type_of_constant uri ugraph =
214 let module C = Cic in
215 let module R = CicReduction in
216 let module U = UriManager in
217 let _ = CicTypeChecker.typecheck uri in
220 CicEnvironment.get_cooked_obj ugraph uri
221 with Not_found -> assert false
224 C.Constant (_,_,ty,_,_) -> ty,u
225 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
229 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
231 and type_of_variable uri ugraph =
232 let module C = Cic in
233 let module R = CicReduction in
234 let module U = UriManager in
235 let _ = CicTypeChecker.typecheck uri in
238 CicEnvironment.get_cooked_obj ugraph uri
239 with Not_found -> assert false
242 C.Variable (_,_,ty,_,_) -> ty,u
246 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
248 and type_of_mutual_inductive_defs uri i ugraph =
249 let module C = Cic in
250 let module R = CicReduction in
251 let module U = UriManager in
252 let _ = CicTypeChecker.typecheck uri in
255 CicEnvironment.get_cooked_obj ugraph uri
256 with Not_found -> assert false
259 C.InductiveDefinition (dl,_,_,_) ->
260 let (_,_,arity,_) = List.nth dl i in
265 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
267 and type_of_mutual_inductive_constr uri i j ugraph =
268 let module C = Cic in
269 let module R = CicReduction in
270 let module U = UriManager in
271 let _ = CicTypeChecker.typecheck uri in
274 CicEnvironment.get_cooked_obj ugraph uri
275 with Not_found -> assert false
278 C.InductiveDefinition (dl,_,_,_) ->
279 let (_,_,_,cl) = List.nth dl i in
280 let (_,ty) = List.nth cl (j-1) in
286 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
289 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
291 (* the check_branch function checks if a branch of a case is refinable.
292 It returns a pair (outype_instance,args), a subst and a metasenv.
293 outype_instance is the expected result of applying the case outtype
295 The problem is that outype is in general unknown, and we should
296 try to synthesize it from the above information, that is in general
297 a second order unification problem. *)
299 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
300 let module C = Cic in
301 (* let module R = CicMetaSubst in *)
302 let module R = CicReduction in
303 match R.whd ~subst context expectedtype with
305 (n,context,actualtype, [term]), subst, metasenv, ugraph
306 | C.Appl (C.MutInd (_,_,_)::tl) ->
307 let (_,arguments) = split tl left_args_no in
308 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
309 | C.Prod (name,so,de) ->
310 (* we expect that the actual type of the branch has the due
312 (match R.whd ~subst context actualtype with
313 C.Prod (name',so',de') ->
314 let subst, metasenv, ugraph1 =
315 fo_unif_subst subst context metasenv so so' ugraph in
317 (match CicSubstitution.lift 1 term with
318 C.Appl l -> C.Appl (l@[C.Rel 1])
319 | t -> C.Appl [t ; C.Rel 1]) in
320 (* we should also check that the name variable is anonymous in
321 the actual type de' ?? *)
323 ((Some (name,(C.Decl so)))::context)
324 metasenv subst left_args_no de' term' de ugraph1
325 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
326 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
328 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
331 let rec type_of_aux subst metasenv context t ugraph =
332 let module C = Cic in
333 let module S = CicSubstitution in
334 let module U = UriManager in
335 let (t',_,_,_,_) as res =
340 match List.nth context (n - 1) with
341 Some (_,C.Decl ty) ->
342 t,S.lift n ty,subst,metasenv, ugraph
343 | Some (_,C.Def (_,Some ty)) ->
344 t,S.lift n ty,subst,metasenv, ugraph
345 | Some (_,C.Def (bo,None)) ->
347 (* if it is in the context it must be already well-typed*)
348 CicTypeChecker.type_of_aux' ~subst metasenv context
351 t,ty,subst,metasenv,ugraph
353 enrich localization_tbl t
354 (RefineFailure (lazy "Rel to hidden hypothesis"))
357 enrich localization_tbl t
358 (RefineFailure (lazy "Not a closed term")))
359 | C.Var (uri,exp_named_subst) ->
360 let exp_named_subst',subst',metasenv',ugraph1 =
361 check_exp_named_subst
362 subst metasenv context exp_named_subst ugraph
364 let ty_uri,ugraph1 = type_of_variable uri ugraph in
366 CicSubstitution.subst_vars exp_named_subst' ty_uri
368 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
371 let (canonical_context, term,ty) =
372 CicUtil.lookup_subst n subst
374 let l',subst',metasenv',ugraph1 =
375 check_metasenv_consistency n subst metasenv context
376 canonical_context l ugraph
378 (* trust or check ??? *)
379 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
380 subst', metasenv', ugraph1
381 (* type_of_aux subst metasenv
382 context (CicSubstitution.subst_meta l term) *)
383 with CicUtil.Subst_not_found _ ->
384 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
385 let l',subst',metasenv', ugraph1 =
386 check_metasenv_consistency n subst metasenv context
387 canonical_context l ugraph
389 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
390 subst', metasenv',ugraph1)
391 | C.Sort (C.Type tno) ->
392 let tno' = CicUniv.fresh() in
394 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
395 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
397 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
399 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
400 | C.Implicit infos ->
401 let metasenv',t' = exp_impl metasenv subst context infos in
402 type_of_aux subst metasenv' context t' ugraph
404 let ty',_,subst',metasenv',ugraph1 =
405 type_of_aux subst metasenv context ty ugraph
407 let te',inferredty,subst'',metasenv'',ugraph2 =
408 type_of_aux subst' metasenv' context te ugraph1
410 let (te', ty'), subst''',metasenv''',ugraph3 =
411 coerce_to_something true localization_tbl te' inferredty ty'
412 subst'' metasenv'' context ugraph2
414 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
415 | C.Prod (name,s,t) ->
416 let s',sort1,subst',metasenv',ugraph1 =
417 type_of_aux subst metasenv context s ugraph
419 let s',sort1,subst', metasenv',ugraph1 =
420 coerce_to_sort localization_tbl
421 s' sort1 subst' context metasenv' ugraph1
423 let context_for_t = ((Some (name,(C.Decl s')))::context) in
424 let t',sort2,subst'',metasenv'',ugraph2 =
425 type_of_aux subst' metasenv'
426 context_for_t t ugraph1
428 let t',sort2,subst'',metasenv'',ugraph2 =
429 coerce_to_sort localization_tbl
430 t' sort2 subst'' context_for_t metasenv'' ugraph2
432 let sop,subst''',metasenv''',ugraph3 =
433 sort_of_prod localization_tbl subst'' metasenv''
434 context (name,s') t' (sort1,sort2) ugraph2
436 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
437 | C.Lambda (n,s,t) ->
438 let s',sort1,subst',metasenv',ugraph1 =
439 type_of_aux subst metasenv context s ugraph
441 let s',sort1,subst',metasenv',ugraph1 =
442 coerce_to_sort localization_tbl
443 s' sort1 subst' context metasenv' ugraph1
445 let context_for_t = ((Some (n,(C.Decl s')))::context) in
446 let t',type2,subst'',metasenv'',ugraph2 =
447 type_of_aux subst' metasenv' context_for_t t ugraph1
449 C.Lambda (n,s',t'),C.Prod (n,s',type2),
450 subst'',metasenv'',ugraph2
452 (* only to check if s is well-typed *)
453 let s',ty,subst',metasenv',ugraph1 =
454 type_of_aux subst metasenv context s ugraph
456 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
458 let t',inferredty,subst'',metasenv'',ugraph2 =
459 type_of_aux subst' metasenv'
460 context_for_t t ugraph1
462 (* One-step LetIn reduction.
463 * Even faster than the previous solution.
464 * Moreover the inferred type is closer to the expected one.
467 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
468 subst'',metasenv'',ugraph2
469 | C.Appl (he::((_::_) as tl)) ->
470 let he',hetype,subst',metasenv',ugraph1 =
471 type_of_aux subst metasenv context he ugraph
473 let tlbody_and_type,subst'',metasenv'',ugraph2 =
474 typeof_list subst' metasenv' context ugraph1 tl
476 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
477 eat_prods true subst'' metasenv'' context
478 he' hetype tlbody_and_type ugraph2
480 let newappl = (C.Appl (coerced_he::coerced_args)) in
481 avoid_double_coercion
482 context subst''' metasenv''' ugraph3 newappl applty
483 | C.Appl _ -> assert false
484 | C.Const (uri,exp_named_subst) ->
485 let exp_named_subst',subst',metasenv',ugraph1 =
486 check_exp_named_subst subst metasenv context
487 exp_named_subst ugraph in
488 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
490 CicSubstitution.subst_vars exp_named_subst' ty_uri
492 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
493 | C.MutInd (uri,i,exp_named_subst) ->
494 let exp_named_subst',subst',metasenv',ugraph1 =
495 check_exp_named_subst subst metasenv context
496 exp_named_subst ugraph
498 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
500 CicSubstitution.subst_vars exp_named_subst' ty_uri in
501 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
502 | C.MutConstruct (uri,i,j,exp_named_subst) ->
503 let exp_named_subst',subst',metasenv',ugraph1 =
504 check_exp_named_subst subst metasenv context
505 exp_named_subst ugraph
508 type_of_mutual_inductive_constr uri i j ugraph1
511 CicSubstitution.subst_vars exp_named_subst' ty_uri
513 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
515 | C.MutCase (uri, i, outtype, term, pl) ->
516 (* first, get the inductive type (and noparams)
517 * in the environment *)
518 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
519 let _ = CicTypeChecker.typecheck uri in
520 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
522 C.InductiveDefinition (l,expl_params,parsno,_) ->
523 List.nth l i , expl_params, parsno, u
525 enrich localization_tbl t
527 (lazy ("Unkown mutual inductive definition " ^
528 U.string_of_uri uri)))
530 if List.length constructors <> List.length pl then
531 enrich localization_tbl t
533 (lazy "Wrong number of cases")) ;
534 let rec count_prod t =
535 match CicReduction.whd ~subst context t with
536 C.Prod (_, _, t) -> 1 + (count_prod t)
539 let no_args = count_prod arity in
540 (* now, create a "generic" MutInd *)
541 let metasenv,left_args =
542 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
544 let metasenv,right_args =
545 let no_right_params = no_args - no_left_params in
546 if no_right_params < 0 then assert false
547 else CicMkImplicit.n_fresh_metas
548 metasenv subst context no_right_params
550 let metasenv,exp_named_subst =
551 CicMkImplicit.fresh_subst metasenv subst context expl_params in
554 C.MutInd (uri,i,exp_named_subst)
557 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
559 (* check consistency with the actual type of term *)
560 let term',actual_type,subst,metasenv,ugraph1 =
561 type_of_aux subst metasenv context term ugraph in
562 let expected_type',_, subst, metasenv,ugraph2 =
563 type_of_aux subst metasenv context expected_type ugraph1
565 let actual_type = CicReduction.whd ~subst context actual_type in
566 let subst,metasenv,ugraph3 =
568 fo_unif_subst subst context metasenv
569 expected_type' actual_type ugraph2
572 enrich localization_tbl term' exn
574 lazy ("(10)The term " ^
575 CicMetaSubst.ppterm_in_context ~metasenv subst term'
576 context ^ " has type " ^
577 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
578 context ^ " but is here used with type " ^
579 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
581 let rec instantiate_prod t =
585 match CicReduction.whd ~subst context t with
587 instantiate_prod (CicSubstitution.subst he t') tl
590 let arity_instantiated_with_left_args =
591 instantiate_prod arity left_args in
592 (* TODO: check if the sort elimination
593 * is allowed: [(I q1 ... qr)|B] *)
594 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
596 (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
598 if left_args = [] then
599 (C.MutConstruct (uri,i,j,exp_named_subst))
602 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
604 let p',actual_type,subst,metasenv,ugraph1 =
605 type_of_aux subst metasenv context p ugraph
607 let constructor',expected_type, subst, metasenv,ugraph2 =
608 type_of_aux subst metasenv context constructor ugraph1
610 let outtypeinstance,subst,metasenv,ugraph3 =
612 check_branch 0 context metasenv subst
613 no_left_params actual_type constructor' expected_type
617 enrich localization_tbl constructor'
619 lazy ("(11)The term " ^
620 CicMetaSubst.ppterm_in_context metasenv subst p'
621 context ^ " has type " ^
622 CicMetaSubst.ppterm_in_context metasenv subst actual_type
623 context ^ " but is here used with type " ^
624 CicMetaSubst.ppterm_in_context metasenv subst expected_type
628 outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
629 pl ([],List.length pl,[],subst,metasenv,ugraph3)
632 (* we are left to check that the outype matches his instances.
633 The easy case is when the outype is specified, that amount
634 to a trivial check. Otherwise, we should guess a type from
638 let outtype,outtypety, subst, metasenv,ugraph4 =
639 type_of_aux subst metasenv context outtype ugraph4 in
642 (let candidate,ugraph5,metasenv,subst =
643 let exp_name_subst, metasenv =
645 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
647 let uris = CicUtil.params_of_obj o in
649 fun uri (acc,metasenv) ->
650 let metasenv',new_meta =
651 CicMkImplicit.mk_implicit metasenv subst context
654 CicMkImplicit.identity_relocation_list_for_metavariable
657 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
661 match left_args,right_args with
662 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
664 let rec mk_right_args =
667 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
669 let right_args_no = List.length right_args in
670 let lifted_left_args =
671 List.map (CicSubstitution.lift right_args_no) left_args
673 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
674 (lifted_left_args @ mk_right_args right_args_no))
677 FreshNamesGenerator.mk_fresh_name ~subst metasenv
678 context Cic.Anonymous ~typ:ty
680 match outtypeinstances with
682 let extended_context =
683 let rec add_right_args =
685 Cic.Prod (name,ty,t) ->
686 Some (name,Cic.Decl ty)::(add_right_args t)
689 (Some (fresh_name,Cic.Decl ty))::
691 (add_right_args arity_instantiated_with_left_args))@
694 let metasenv,new_meta =
695 CicMkImplicit.mk_implicit metasenv subst extended_context
698 CicMkImplicit.identity_relocation_list_for_metavariable
701 let rec add_lambdas b =
703 Cic.Prod (name,ty,t) ->
704 Cic.Lambda (name,ty,(add_lambdas b t))
705 | _ -> Cic.Lambda (fresh_name, ty, b)
708 add_lambdas (Cic.Meta (new_meta,irl))
709 arity_instantiated_with_left_args
711 (Some candidate),ugraph4,metasenv,subst
712 | (constructor_args_no,_,instance,_)::tl ->
714 let instance',subst,metasenv =
715 CicMetaSubst.delift_rels subst metasenv
716 constructor_args_no instance
718 let candidate,ugraph,metasenv,subst =
720 fun (candidate_oty,ugraph,metasenv,subst)
721 (constructor_args_no,_,instance,_) ->
722 match candidate_oty with
723 | None -> None,ugraph,metasenv,subst
726 let instance',subst,metasenv =
727 CicMetaSubst.delift_rels subst metasenv
728 constructor_args_no instance
730 let subst,metasenv,ugraph =
731 fo_unif_subst subst context metasenv
734 candidate_oty,ugraph,metasenv,subst
736 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
737 | RefineFailure _ | Uncertain _ ->
738 None,ugraph,metasenv,subst
739 ) (Some instance',ugraph4,metasenv,subst) tl
742 | None -> None, ugraph,metasenv,subst
744 let rec add_lambdas n b =
746 Cic.Prod (name,ty,t) ->
747 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
749 Cic.Lambda (fresh_name, ty,
750 CicSubstitution.lift (n + 1) t)
753 (add_lambdas 0 t arity_instantiated_with_left_args),
754 ugraph,metasenv,subst
755 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
756 None,ugraph4,metasenv,subst
759 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
761 let subst,metasenv,ugraph =
763 fo_unif_subst subst context metasenv
764 candidate outtype ugraph5
766 exn -> assert false(* unification against a metavariable *)
768 C.MutCase (uri, i, outtype, term', pl'),
769 CicReduction.head_beta_reduce
770 (CicMetaSubst.apply_subst subst
771 (Cic.Appl (outtype::right_args@[term']))),
772 subst,metasenv,ugraph)
773 | _ -> (* easy case *)
774 let tlbody_and_type,subst,metasenv,ugraph4 =
775 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
777 let _,_,_,subst,metasenv,ugraph4 =
778 eat_prods false subst metasenv context
779 outtype outtypety tlbody_and_type ugraph4
781 let _,_, subst, metasenv,ugraph5 =
782 type_of_aux subst metasenv context
783 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
785 let (subst,metasenv,ugraph6) =
787 (fun (subst,metasenv,ugraph)
788 p (constructor_args_no,context,instance,args)
793 CicSubstitution.lift constructor_args_no outtype
795 C.Appl (outtype'::args)
797 CicReduction.whd ~subst context appl
800 fo_unif_subst subst context metasenv instance instance'
804 enrich localization_tbl p exn
806 lazy ("(12)The term " ^
807 CicMetaSubst.ppterm_in_context ~metasenv subst p
808 context ^ " has type " ^
809 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
810 context ^ " but is here used with type " ^
811 CicMetaSubst.ppterm_in_context ~metasenv subst instance
813 (subst,metasenv,ugraph5) pl' outtypeinstances
815 C.MutCase (uri, i, outtype, term', pl'),
816 CicReduction.head_beta_reduce
817 (CicMetaSubst.apply_subst subst
818 (C.Appl(outtype::right_args@[term]))),
819 subst,metasenv,ugraph6)
821 let fl_ty',subst,metasenv,types,ugraph1,len =
823 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
824 let ty',_,subst',metasenv',ugraph1 =
825 type_of_aux subst metasenv context ty ugraph
827 fl @ [ty'],subst',metasenv',
828 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
829 :: types, ugraph, len+1
830 ) ([],subst,metasenv,[],ugraph,0) fl
832 let context' = types@context in
833 let fl_bo',subst,metasenv,ugraph2 =
835 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
836 let bo',ty_of_bo,subst,metasenv,ugraph1 =
837 type_of_aux subst metasenv context' bo ugraph in
838 let expected_ty = CicSubstitution.lift len ty in
839 let subst',metasenv',ugraph' =
841 fo_unif_subst subst context' metasenv
842 ty_of_bo expected_ty ugraph1
845 enrich localization_tbl bo exn
847 lazy ("(13)The term " ^
848 CicMetaSubst.ppterm_in_context ~metasenv subst bo
849 context' ^ " has type " ^
850 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
851 context' ^ " but is here used with type " ^
852 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
855 fl @ [bo'] , subst',metasenv',ugraph'
856 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
858 let ty = List.nth fl_ty' i in
859 (* now we have the new ty in fl_ty', the new bo in fl_bo',
860 * and we want the new fl with bo' and ty' injected in the right
863 let rec map3 f l1 l2 l3 =
866 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
869 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
872 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
874 let fl_ty',subst,metasenv,types,ugraph1,len =
876 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
877 let ty',_,subst',metasenv',ugraph1 =
878 type_of_aux subst metasenv context ty ugraph
880 fl @ [ty'],subst',metasenv',
881 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
882 types, ugraph1, len+1
883 ) ([],subst,metasenv,[],ugraph,0) fl
885 let context' = types@context in
886 let fl_bo',subst,metasenv,ugraph2 =
888 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
889 let bo',ty_of_bo,subst,metasenv,ugraph1 =
890 type_of_aux subst metasenv context' bo ugraph in
891 let expected_ty = CicSubstitution.lift len ty in
892 let subst',metasenv',ugraph' =
894 fo_unif_subst subst context' metasenv
895 ty_of_bo expected_ty ugraph1
898 enrich localization_tbl bo exn
900 lazy ("(14)The term " ^
901 CicMetaSubst.ppterm_in_context ~metasenv subst bo
902 context' ^ " has type " ^
903 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
904 context' ^ " but is here used with type " ^
905 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
908 fl @ [bo'],subst',metasenv',ugraph'
909 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
911 let ty = List.nth fl_ty' i in
912 (* now we have the new ty in fl_ty', the new bo in fl_bo',
913 * and we want the new fl with bo' and ty' injected in the right
916 let rec map3 f l1 l2 l3 =
919 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
922 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
925 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
927 relocalize localization_tbl t t';
930 (* check_metasenv_consistency checks that the "canonical" context of a
931 metavariable is consitent - up to relocation via the relocation list l -
932 with the actual context *)
933 and check_metasenv_consistency
934 metano subst metasenv context canonical_context l ugraph
936 let module C = Cic in
937 let module R = CicReduction in
938 let module S = CicSubstitution in
939 let lifted_canonical_context =
943 | (Some (n,C.Decl t))::tl ->
944 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
945 | (Some (n,C.Def (t,None)))::tl ->
946 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
947 | None::tl -> None::(aux (i+1) tl)
948 | (Some (n,C.Def (t,Some ty)))::tl ->
950 C.Def ((S.subst_meta l (S.lift i t)),
951 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
953 aux 1 canonical_context
957 (fun (l,subst,metasenv,ugraph) t ct ->
960 l @ [None],subst,metasenv,ugraph
961 | Some t,Some (_,C.Def (ct,_)) ->
962 let subst',metasenv',ugraph' =
964 (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
965 * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
966 fo_unif_subst subst context metasenv t ct ugraph
967 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))))))
969 l @ [Some t],subst',metasenv',ugraph'
970 | Some t,Some (_,C.Decl ct) ->
971 let t',inferredty,subst',metasenv',ugraph1 =
972 type_of_aux subst metasenv context t ugraph
974 let subst'',metasenv'',ugraph2 =
977 subst' context metasenv' inferredty ct ugraph1
978 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))))))
980 l @ [Some t'], subst'',metasenv'',ugraph2
982 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
984 Invalid_argument _ ->
988 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
989 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
990 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
992 and check_exp_named_subst metasubst metasenv context tl ugraph =
993 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
995 [] -> [],metasubst,metasenv,ugraph
997 let ty_uri,ugraph1 = type_of_variable uri ugraph in
999 CicSubstitution.subst_vars substs ty_uri in
1000 (* CSC: why was this code here? it is wrong
1001 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1002 Cic.Variable (_,Some bo,_,_) ->
1004 (RefineFailure (lazy
1005 "A variable with a body can not be explicit substituted"))
1006 | Cic.Variable (_,None,_,_) -> ()
1009 (RefineFailure (lazy
1010 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1013 let t',typeoft,metasubst',metasenv',ugraph2 =
1014 type_of_aux metasubst metasenv context t ugraph1 in
1015 let subst = uri,t' in
1016 let metasubst'',metasenv'',ugraph3 =
1019 metasubst' context metasenv' typeoft typeofvar ugraph2
1021 raise (RefineFailure (lazy
1022 ("Wrong Explicit Named Substitution: " ^
1023 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1024 " not unifiable with " ^
1025 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1027 (* FIXME: no mere tail recursive! *)
1028 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1029 check_exp_named_subst_aux
1030 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1032 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1034 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1037 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1040 let module C = Cic in
1041 let context_for_t2 = (Some (name,C.Decl s))::context in
1042 let t1'' = CicReduction.whd ~subst context t1 in
1043 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1044 match (t1'', t2'') with
1045 (C.Sort s1, C.Sort s2)
1046 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1047 (* different than Coq manual!!! *)
1048 C.Sort s2,subst,metasenv,ugraph
1049 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1050 let t' = CicUniv.fresh() in
1052 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1053 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1054 C.Sort (C.Type t'),subst,metasenv,ugraph2
1056 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1057 | (C.Sort _,C.Sort (C.Type t1)) ->
1058 C.Sort (C.Type t1),subst,metasenv,ugraph
1059 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1060 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1061 (* TODO how can we force the meta to become a sort? If we don't we
1062 * break the invariant that refine produce only well typed terms *)
1063 (* TODO if we check the non meta term and if it is a sort then we
1064 * are likely to know the exact value of the result e.g. if the rhs
1065 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1066 let (metasenv,idx) =
1067 CicMkImplicit.mk_implicit_sort metasenv subst in
1068 let (subst, metasenv,ugraph1) =
1070 fo_unif_subst subst context_for_t2 metasenv
1071 (C.Meta (idx,[])) t2'' ugraph
1072 with _ -> assert false (* unification against a metavariable *)
1074 t2'',subst,metasenv,ugraph1
1077 enrich localization_tbl s
1081 "%s is supposed to be a type, but its type is %s"
1082 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1083 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1085 enrich localization_tbl t
1089 "%s is supposed to be a type, but its type is %s"
1090 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1091 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1093 and avoid_double_coercion context subst metasenv ugraph t ty =
1094 if not !pack_coercions then
1095 t,ty,subst,metasenv,ugraph
1097 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1099 let source_carr = CoercGraph.source_of c2 in
1100 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1101 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1103 | CoercGraph.SomeCoercion candidates ->
1105 HExtlib.list_findopt
1106 (function (metasenv,last,c) ->
1108 | c when not (CoercGraph.is_composite c) ->
1109 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1112 let subst,metasenv,ugraph =
1113 fo_unif_subst subst context metasenv last head ugraph in
1114 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1119 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1120 let newt,_,subst,metasenv,ugraph =
1121 type_of_aux subst metasenv context c ugraph in
1122 debug_print (lazy "tipa...");
1123 let subst, metasenv, ugraph =
1124 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1125 fo_unif_subst subst context metasenv newt t ugraph
1127 debug_print (lazy "unifica...");
1128 Some (newt, ty, subst, metasenv, ugraph)
1130 | RefineFailure s | Uncertain s when not !pack_coercions->
1131 debug_print s; debug_print (lazy "stop\n");None
1132 | RefineFailure s | Uncertain s ->
1133 debug_print s;debug_print (lazy "goon\n");
1135 let old_pack_coercions = !pack_coercions in
1136 pack_coercions := false; (* to avoid diverging *)
1137 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1138 type_of_aux subst metasenv context c1_c2_implicit ugraph
1140 pack_coercions := old_pack_coercions;
1142 is_a_double_coercion refined_c1_c2_implicit
1148 match refined_c1_c2_implicit with
1149 | Cic.Appl l -> HExtlib.list_last l
1152 let subst, metasenv, ugraph =
1153 try fo_unif_subst subst context metasenv
1155 with RefineFailure s| Uncertain s->
1156 debug_print s;assert false
1158 let subst, metasenv, ugraph =
1159 fo_unif_subst subst context metasenv
1160 refined_c1_c2_implicit t ugraph
1162 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1164 | RefineFailure s | Uncertain s ->
1165 pack_coercions := true;debug_print s;None
1166 | exn -> pack_coercions := true; raise exn))
1169 (match selected with
1173 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1174 t, ty, subst, metasenv, ugraph)
1175 | _ -> t, ty, subst, metasenv, ugraph)
1177 t, ty, subst, metasenv, ugraph
1179 and typeof_list subst metasenv context ugraph l =
1180 let tlbody_and_type,subst,metasenv,ugraph =
1182 (fun x (res,subst,metasenv,ugraph) ->
1183 let x',ty,subst',metasenv',ugraph1 =
1184 type_of_aux subst metasenv context x ugraph
1186 (x', ty)::res,subst',metasenv',ugraph1
1187 ) l ([],subst,metasenv,ugraph)
1189 tlbody_and_type,subst,metasenv,ugraph
1192 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1194 (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1195 let fix_arity n metasenv context subst he hetype ugraph =
1196 let hetype = CicMetaSubst.apply_subst subst hetype in
1197 let src = CoercDb.coerc_carr_of_term hetype in
1198 let tgt = CoercDb.Fun 0 in
1199 match CoercGraph.look_for_coercion' metasenv subst context src tgt with
1200 | CoercGraph.NoCoercion -> []
1201 | CoercGraph.NotMetaClosed
1202 | CoercGraph.NotHandled _ ->
1203 raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1204 | CoercGraph.SomeCoercionToTgt candidates
1205 | CoercGraph.SomeCoercion candidates ->
1207 (fun (metasenv,last,coerc) ->
1209 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1210 let subst,metasenv,ugraph =
1211 fo_unif_subst subst context metasenv last he ugraph in
1212 debug_print (lazy ("New head: "^ pp coerc));
1215 CicTypeChecker.type_of_aux' ~subst metasenv context coerc ugraph in
1216 debug_print (lazy (" has type: "^ pp tty));
1217 Some (coerc,tty,subst,metasenv,ugraph)
1219 | Uncertain _ | RefineFailure _
1220 | HExtlib.Localized (_,Uncertain _)
1221 | HExtlib.Localized (_,RefineFailure _) -> None
1222 | exn -> assert false)
1225 (* aux function to process the type of the head and the args in parallel *)
1226 let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1228 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1229 | (hete, hety)::tl as args ->
1230 match (CicReduction.whd ~subst context hetype) with
1231 | Cic.Prod (n,s,t) ->
1232 let arg,subst,metasenv,ugraph =
1233 coerce_to_something allow_coercions localization_tbl
1234 hete hety s subst metasenv context ugraph in
1236 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1237 ugraph (newargs@[arg]) tl
1240 match he, newargs with
1242 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1243 | _ -> Cic.Appl (he::List.map fst newargs)
1245 (*{{{*) debug_print (lazy
1247 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1248 "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1249 "\n but is applyed to: " ^ String.concat ";"
1250 (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1251 let possible_fixes =
1252 fix_arity (List.length args) metasenv context subst he hetype
1255 HExtlib.list_findopt
1256 (fun (he,hetype,subst,metasenv,ugraph) ->
1257 (* {{{ *)debug_print (lazy ("Try fix: "^
1258 CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1259 debug_print (lazy (" of type: "^
1260 CicMetaSubst.ppterm_in_context
1261 ~metasenv subst hetype context)); (* }}} *)
1263 Some (eat_prods_and_args
1264 metasenv subst context he hetype ugraph [] args)
1266 | RefineFailure _ | Uncertain _
1267 | HExtlib.Localized (_,RefineFailure _)
1268 | HExtlib.Localized (_,Uncertain _) -> None)
1274 (MoreArgsThanExpected
1275 (List.length args, RefineFailure (lazy "")))
1277 (* first we check if we are in the simple case of a meta closed term *)
1278 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1279 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1280 (* this optimization is to postpone fix_arity (the most common case)*)
1281 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1283 (* this (says CSC) is also useful to infer dependent types *)
1284 let pristinemenv = metasenv in
1285 let metasenv,hetype' =
1286 mk_prod_of_metas metasenv context subst args_bo_and_ty
1289 let subst,metasenv,ugraph =
1290 fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1292 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1293 with RefineFailure _ | Uncertain _ ->
1294 subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1296 let coerced_args,subst,metasenv,he,t,ugraph =
1299 metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1301 MoreArgsThanExpected (residuals,exn) ->
1302 more_args_than_expected localization_tbl metasenv
1303 subst he context hetype' residuals args_bo_and_ty exn
1305 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1307 and coerce_to_something
1308 allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1310 let module CS = CicSubstitution in
1311 let module CR = CicReduction in
1312 let cs_subst = CS.subst ~avoid_beta_redexes:true in
1313 let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1314 debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1316 CoercGraph.look_for_coercion metasenv subst context infty expty
1319 | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
1320 "coerce_atom_to_something fails since not meta closed"))
1321 | CoercGraph.NoCoercion
1322 | CoercGraph.SomeCoercionToTgt _
1323 | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
1324 "coerce_atom_to_something fails since no coercions found"))
1325 | CoercGraph.SomeCoercion candidates ->
1326 debug_print (lazy (string_of_int (List.length candidates) ^
1327 " candidates found"));
1328 let uncertain = ref false in
1332 (fun (metasenv,last,c) ->
1334 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1335 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1337 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
1338 "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
1340 debug_print (lazy ("FO_UNIF_SUBST: " ^
1341 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1342 let subst,metasenv,ugraph =
1343 fo_unif_subst subst context metasenv last t ugraph
1345 let newt,newhety,subst,metasenv,ugraph =
1346 type_of_aux subst metasenv context c ugraph in
1347 let newt, newty, subst, metasenv, ugraph =
1348 avoid_double_coercion context subst metasenv ugraph newt expty
1350 let subst,metasenv,ugraph =
1351 fo_unif_subst subst context metasenv newhety expty ugraph in
1352 Some ((newt,newty), subst, metasenv, ugraph)
1354 | Uncertain _ -> uncertain := true; None
1355 | RefineFailure _ -> None)
1360 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1368 | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1369 | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1371 let rec coerce_to_something_aux
1372 t infty expty subst metasenv context ugraph
1375 let subst, metasenv, ugraph =
1376 fo_unif_subst subst context metasenv infty expty ugraph
1378 (t, expty), subst, metasenv, ugraph
1379 with Uncertain _ | RefineFailure _ as exn ->
1380 if not allow_coercions || not !insert_coercions then
1381 enrich localization_tbl t exn
1383 let whd = CicReduction.whd ~delta:false in
1384 let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1385 let infty = clean infty subst context in
1386 let expty = clean expty subst context in
1387 let t = clean t subst context in
1388 (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1389 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1390 CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1391 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1392 let (coerced,_),subst,metasenv,_ as result =
1393 match infty, expty, t with
1394 | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1395 (*{{{*) debug_print (lazy "FIX");
1397 [name,i,_(* infty *),bo] ->
1399 Some (Cic.Name name,Cic.Decl expty)::context in
1400 let (rel1, _), subst, metasenv, ugraph =
1401 coerce_to_something_aux (Cic.Rel 1)
1402 (CS.lift 1 expty) (CS.lift 1 infty) subst
1403 metasenv context_bo ugraph in
1404 let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1405 let (bo,_), subst, metasenv, ugraph =
1406 coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1408 metasenv context_bo ugraph
1410 (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1411 | _ -> assert false (* not implemented yet *)) (*}}}*)
1412 | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1413 (*{{{*) debug_print (lazy "CASE");
1414 (* {{{ helper functions *)
1415 let get_cl_and_left_p uri tyno outty ugraph =
1416 match CicEnvironment.get_obj ugraph uri with
1417 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1420 match CicReduction.whd ~delta:false ctx t with
1421 | Cic.Prod (name,src,tgt) ->
1422 let ctx = Some (name, Cic.Decl src) :: ctx in
1428 let rec skip_lambda_delifting t n =
1431 | Cic.Lambda (_,_,t),n ->
1432 skip_lambda_delifting
1433 (CS.subst (Cic.Implicit None) t) (n - 1)
1436 let get_l_r_p n = function
1437 | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1438 | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1439 HExtlib.split_nth n args
1442 let _, _, ty, cl = List.nth tl tyno in
1443 let pis = count_pis ty in
1444 let rno = pis - leftno in
1445 let t = skip_lambda_delifting outty rno in
1446 let left_p, _ = get_l_r_p leftno t in
1447 let instantiale_with_left cl =
1451 (fun t p -> match t with
1452 | Cic.Prod (_,_,t) ->
1458 let cl = instantiale_with_left (List.map snd cl) in
1459 cl, left_p, leftno, rno, ugraph
1462 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1465 let rec mkr n = function
1466 | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1469 CicReplace.replace_lifting
1470 ~equality:(fun _ -> CicUtil.alpha_equivalence)
1472 ~what:(matched::right_p)
1473 ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1477 | Cic.Lambda (name, src, tgt),_ ->
1478 Cic.Lambda (name, src,
1479 keep_lambdas_and_put_expty
1480 (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1481 (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1484 let eq_uri, eq, eq_refl =
1485 match LibraryObjects.eq_URI () with
1486 | None -> HLog.warn "no default equality"; raise exn
1487 | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1490 metasenv subst context uri tyno cty outty mty m leftno i
1492 let rec aux context outty par k mty m = function
1493 | Cic.Prod (name, src, tgt) ->
1496 (Some (name, Cic.Decl src) :: context)
1497 (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1498 (CS.lift 1 mty) (CS.lift 1 m) tgt
1500 Cic.Prod (name, src, t), k
1503 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1504 if par <> [] then Cic.Appl (k::par) else k
1506 Cic.Prod (Cic.Name "p",
1507 Cic.Appl [eq; mty; m; k],
1509 (CR.head_beta_reduce ~delta:false
1510 (Cic.Appl [outty;k])))),k
1511 | Cic.Appl (Cic.MutInd _::pl) ->
1512 let left_p,right_p = HExtlib.split_nth leftno pl in
1513 let has_rights = right_p <> [] in
1515 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1516 Cic.Appl (k::left_p@par)
1520 CicTypeChecker.type_of_aux' ~subst metasenv context k
1521 CicUniv.oblivion_ugraph
1523 | Cic.Appl (Cic.MutInd _::args),_ ->
1524 snd (HExtlib.split_nth leftno args)
1526 with CicTypeChecker.TypeCheckerFailure _-> assert false
1529 CR.head_beta_reduce ~delta:false
1530 (Cic.Appl (outty ::right_p @ [k])),k
1532 Cic.Prod (Cic.Name "p",
1533 Cic.Appl [eq; mty; m; k],
1535 (CR.head_beta_reduce ~delta:false
1536 (Cic.Appl (outty ::right_p @ [k]))))),k
1539 aux context outty [] 1 mty m cty
1541 let add_lambda_for_refl_m pbo rno mty m k cty =
1542 (* k lives in the right context *)
1543 if rno <> 0 then pbo else
1544 let rec aux mty m = function
1545 | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1546 Cic.Lambda (name,src,
1547 (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1549 Cic.Lambda (Cic.Name "p",
1550 Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1554 let add_pi_for_refl_m new_outty mty m rno =
1555 if rno <> 0 then new_outty else
1556 let rec aux m mty = function
1557 | Cic.Lambda (name, src, tgt) ->
1558 Cic.Lambda (name, src,
1559 aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1562 (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1566 in (* }}} end helper functions *)
1567 (* constructors types with left params already instantiated *)
1568 let outty = CicMetaSubst.apply_subst subst outty in
1569 let cl, left_p, leftno,rno,ugraph =
1570 get_cl_and_left_p uri tyno outty ugraph
1575 CicTypeChecker.type_of_aux' ~subst metasenv context m
1576 CicUniv.oblivion_ugraph
1578 | Cic.MutInd _ as mty,_ -> [], mty
1579 | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
1580 snd (HExtlib.split_nth leftno args), mty
1582 with CicTypeChecker.TypeCheckerFailure _ -> assert false
1585 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1588 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1589 ~metasenv subst new_outty context));
1590 let _,pl,subst,metasenv,ugraph =
1592 (fun cty pbo (i, acc, s, menv, ugraph) ->
1593 (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1594 * (new_)outty right_par (K_i left_par k_par) *)
1596 add_params menv s context uri tyno
1597 cty outty mty m leftno i in
1599 (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1600 ~metasenv subst infty_pbo context));
1601 let expty_pbo, k = (* k is (K_i left_par k_par) *)
1602 add_params menv s context uri tyno
1603 cty new_outty mty m leftno i in
1605 (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1606 ~metasenv subst expty_pbo context));
1607 let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1609 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1610 ~metasenv subst pbo context));
1611 let (pbo, _), subst, metasenv, ugraph =
1612 coerce_to_something_aux pbo infty_pbo expty_pbo
1613 s menv context ugraph
1616 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1617 ~metasenv subst pbo context));
1618 (i-1, pbo::acc, subst, metasenv, ugraph))
1619 cl pl (List.length pl, [], subst, metasenv, ugraph)
1621 let new_outty = add_pi_for_refl_m new_outty mty m rno in
1623 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1624 ~metasenv subst new_outty context));
1627 let refl_m=Cic.Appl[eq_refl;mty;m]in
1628 Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1630 Cic.MutCase(uri,tyno,new_outty,m,pl)
1632 (t, expty), subst, metasenv, ugraph (*}}}*)
1633 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1634 (*{{{*) debug_print (lazy "LAM");
1636 FreshNamesGenerator.mk_fresh_name
1637 ~subst metasenv context ~typ:src2 Cic.Anonymous
1639 let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1640 (* contravariant part: the argument of f:src->ty *)
1641 let (rel1, _), subst, metasenv, ugraph =
1642 coerce_to_something_aux
1643 (Cic.Rel 1) (CS.lift 1 src2)
1644 (CS.lift 1 src) subst metasenv context_src2 ugraph
1646 (* covariant part: the result of f(c x); x:src2; (c x):src *)
1649 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1650 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1652 (* we fix the possible dependency problem in the source ty *)
1653 let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1654 let (bo, _), subst, metasenv, ugraph =
1655 coerce_to_something_aux
1656 bo ty ty2 subst metasenv context_src2 ugraph
1658 let coerced = Cic.Lambda (name_t,src2, bo) in
1659 (coerced, expty), subst, metasenv, ugraph (*}}}*)
1661 (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1662 ~metasenv subst infty context ^ " ==> " ^
1663 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1664 coerce_atom_to_something
1665 t infty expty subst metasenv context ugraph (*}}}*)
1667 debug_print (lazy ("COERCE TO SOMETHING END: "^
1668 CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1672 coerce_to_something_aux t infty expty subst metasenv context ugraph
1673 with Uncertain _ | RefineFailure _ as exn ->
1676 CicMetaSubst.ppterm_in_context metasenv subst t context ^
1677 " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1678 infty context ^ " but is here used with type " ^
1679 CicMetaSubst.ppterm_in_context metasenv subst expty context)
1681 enrich localization_tbl ~f t exn
1683 and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1684 match CicReduction.whd ~delta:false ~subst context infty with
1685 | Cic.Meta _ | Cic.Sort _ ->
1686 t,infty, subst, metasenv, ugraph
1688 debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1689 ~metasenv subst src context));
1690 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1692 let (t, ty_t), subst, metasenv, ugraph =
1693 coerce_to_something true
1694 localization_tbl t src tgt subst metasenv context ugraph
1696 debug_print (lazy ("COERCE TO SORT END: "^
1697 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1698 t, ty_t, subst, metasenv, ugraph
1699 with HExtlib.Localized (_, exn) ->
1701 lazy ("(7)The term " ^
1702 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1703 ^ " is not a type since it has type " ^
1704 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1705 ^ " that is not a sort")
1707 enrich localization_tbl ~f t exn
1710 (* eat prods ends here! *)
1712 let t',ty,subst',metasenv',ugraph1 =
1713 type_of_aux [] metasenv context t ugraph
1715 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1716 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1717 (* Andrea: ho rimesso qui l'applicazione della subst al
1718 metasenv dopo che ho droppato l'invariante che il metsaenv
1719 e' sempre istanziato *)
1720 let substituted_metasenv =
1721 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1723 (* substituted_t,substituted_ty,substituted_metasenv *)
1724 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1726 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1728 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1729 let cleaned_metasenv =
1731 (function (n,context,ty) ->
1732 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1737 | Some (n, Cic.Decl t) ->
1739 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1740 | Some (n, Cic.Def (bo,ty)) ->
1741 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1746 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1748 Some (n, Cic.Def (bo',ty'))
1752 ) substituted_metasenv
1754 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1757 let undebrujin uri typesno tys t =
1760 (fun (name,_,_,_) (i,t) ->
1761 (* here the explicit_named_substituion is assumed to be *)
1763 let t' = Cic.MutInd (uri,i,[]) in
1764 let t = CicSubstitution.subst t' t in
1766 ) tys (typesno - 1,t))
1768 let map_first_n n start f g l =
1769 let rec aux acc k l =
1772 | [] -> raise (Invalid_argument "map_first_n")
1773 | hd :: tl -> f hd k (aux acc (k+1) tl)
1779 (*CSC: this is a very rough approximation; to be finished *)
1780 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1781 let subst,metasenv,ugraph,tys =
1783 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1784 let subst,metasenv,ugraph,cl =
1786 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1787 let rec aux ctx k subst = function
1788 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1789 let subst,metasenv,ugraph,tl =
1791 (subst,metasenv,ugraph,[])
1792 (fun t n (subst,metasenv,ugraph,acc) ->
1793 let subst,metasenv,ugraph =
1795 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1797 subst,metasenv,ugraph,(t::acc))
1798 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1801 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1802 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1803 subst,metasenv,ugraph,t
1804 | Cic.Prod (name,s,t) ->
1805 let ctx = (Some (name,Cic.Decl s))::ctx in
1806 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1807 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1811 (lazy "not well formed constructor type"))
1813 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1814 subst,metasenv,ugraph,(name,ty) :: acc)
1815 cl (subst,metasenv,ugraph,[])
1817 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1818 tys ([],metasenv,ugraph,[])
1820 let substituted_tys =
1822 (fun (name,ind,arity,cl) ->
1824 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1826 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1829 metasenv,ugraph,substituted_tys
1831 let typecheck metasenv uri obj ~localization_tbl =
1832 let ugraph = CicUniv.empty_ugraph in
1834 Cic.Constant (name,Some bo,ty,args,attrs) ->
1835 let bo',boty,metasenv,ugraph =
1836 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1837 let ty',_,metasenv,ugraph =
1838 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1839 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1840 let bo' = CicMetaSubst.apply_subst subst bo' in
1841 let ty' = CicMetaSubst.apply_subst subst ty' in
1842 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1843 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1844 | Cic.Constant (name,None,ty,args,attrs) ->
1845 let ty',_,metasenv,ugraph =
1846 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1848 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1849 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1850 assert (metasenv' = metasenv);
1851 (* Here we do not check the metasenv for correctness *)
1852 let bo',boty,metasenv,ugraph =
1853 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1854 let ty',sort,metasenv,ugraph =
1855 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1859 (* instead of raising Uncertain, let's hope that the meta will become
1862 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1864 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1865 let bo' = CicMetaSubst.apply_subst subst bo' in
1866 let ty' = CicMetaSubst.apply_subst subst ty' in
1867 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1868 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1869 | Cic.Variable _ -> assert false (* not implemented *)
1870 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1871 (*CSC: this code is greately simplified and many many checks are missing *)
1872 (*CSC: e.g. the constructors are not required to build their own types, *)
1873 (*CSC: the arities are not required to have as type a sort, etc. *)
1874 let uri = match uri with Some uri -> uri | None -> assert false in
1875 let typesno = List.length tys in
1876 (* first phase: we fix only the types *)
1877 let metasenv,ugraph,tys =
1879 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1880 let ty',_,metasenv,ugraph =
1881 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1883 metasenv,ugraph,(name,b,ty',cl)::res
1884 ) tys (metasenv,ugraph,[]) in
1886 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1887 (* second phase: we fix only the constructors *)
1888 let saved_menv = metasenv in
1889 let metasenv,ugraph,tys =
1891 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1892 let metasenv,ugraph,cl' =
1894 (fun (name,ty) (metasenv,ugraph,res) ->
1896 CicTypeChecker.debrujin_constructor
1897 ~cb:(relocalize localization_tbl) uri typesno ty in
1898 let ty',_,metasenv,ugraph =
1899 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1900 let ty' = undebrujin uri typesno tys ty' in
1901 metasenv@saved_menv,ugraph,(name,ty')::res
1902 ) cl (metasenv,ugraph,[])
1904 metasenv,ugraph,(name,b,ty,cl')::res
1905 ) tys (metasenv,ugraph,[]) in
1906 (* third phase: we check the positivity condition *)
1907 let metasenv,ugraph,tys =
1908 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1910 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1913 (* sara' piu' veloce che raffinare da zero? mah.... *)
1914 let pack_coercion metasenv ctx t =
1915 let module C = Cic in
1916 let rec merge_coercions ctx =
1917 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1919 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1920 | C.Meta (n,subst) ->
1923 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1926 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1927 | C.Prod (name,so,dest) ->
1928 let ctx' = (Some (name,C.Decl so))::ctx in
1929 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1930 | C.Lambda (name,so,dest) ->
1931 let ctx' = (Some (name,C.Decl so))::ctx in
1932 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1933 | C.LetIn (name,so,dest) ->
1934 let _,ty,metasenv,ugraph =
1935 pack_coercions := false;
1936 type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1937 pack_coercions := true;
1938 let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1939 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1941 let l = List.map (merge_coercions ctx) l in
1943 let b,_,_,_,_ = is_a_double_coercion t in
1945 let ugraph = CicUniv.oblivion_ugraph in
1946 let old_insert_coercions = !insert_coercions in
1947 insert_coercions := false;
1948 let newt, _, menv, _ =
1950 type_of_aux' metasenv ctx t ugraph
1951 with RefineFailure _ | Uncertain _ ->
1954 insert_coercions := old_insert_coercions;
1955 if metasenv <> [] || menv = [] then
1958 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1961 | C.Var (uri,exp_named_subst) ->
1962 let exp_named_subst = List.map aux exp_named_subst in
1963 C.Var (uri, exp_named_subst)
1964 | C.Const (uri,exp_named_subst) ->
1965 let exp_named_subst = List.map aux exp_named_subst in
1966 C.Const (uri, exp_named_subst)
1967 | C.MutInd (uri,tyno,exp_named_subst) ->
1968 let exp_named_subst = List.map aux exp_named_subst in
1969 C.MutInd (uri,tyno,exp_named_subst)
1970 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1971 let exp_named_subst = List.map aux exp_named_subst in
1972 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1973 | C.MutCase (uri,tyno,out,te,pl) ->
1974 let pl = List.map (merge_coercions ctx) pl in
1975 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1976 | C.Fix (fno, fl) ->
1979 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1984 (fun (name,idx,ty,bo) ->
1985 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1989 | C.CoFix (fno, fl) ->
1992 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1997 (fun (name,ty,bo) ->
1998 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
2003 merge_coercions ctx t
2006 let pack_coercion_metasenv conjectures = conjectures (*
2008 TASSI: this code war written when coercions were a toy,
2009 now packing coercions involves unification thus
2010 the metasenv may change, and this pack coercion
2011 does not handle that.
2013 let module C = Cic in
2015 (fun (i, ctx, ty) ->
2021 Some (name, C.Decl t) ->
2022 Some (name, C.Decl (pack_coercion conjectures ctx t))
2023 | Some (name, C.Def (t,None)) ->
2024 Some (name,C.Def (pack_coercion conjectures ctx t,None))
2025 | Some (name, C.Def (t,Some ty)) ->
2026 Some (name, C.Def (pack_coercion conjectures ctx t,
2027 Some (pack_coercion conjectures ctx ty)))
2033 ((i,ctx,pack_coercion conjectures ctx ty))
2038 let pack_coercion_obj obj = obj (*
2040 TASSI: this code war written when coercions were a toy,
2041 now packing coercions involves unification thus
2042 the metasenv may change, and this pack coercion
2043 does not handle that.
2045 let module C = Cic in
2047 | C.Constant (id, body, ty, params, attrs) ->
2051 | Some body -> Some (pack_coercion [] [] body)
2053 let ty = pack_coercion [] [] ty in
2054 C.Constant (id, body, ty, params, attrs)
2055 | C.Variable (name, body, ty, params, attrs) ->
2059 | Some body -> Some (pack_coercion [] [] body)
2061 let ty = pack_coercion [] [] ty in
2062 C.Variable (name, body, ty, params, attrs)
2063 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2064 let conjectures = pack_coercion_metasenv conjectures in
2065 let body = pack_coercion conjectures [] body in
2066 let ty = pack_coercion conjectures [] ty in
2067 C.CurrentProof (name, conjectures, body, ty, params, attrs)
2068 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2071 (fun (name, ind, arity, cl) ->
2072 let arity = pack_coercion [] [] arity in
2074 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2076 (name, ind, arity, cl))
2079 C.InductiveDefinition (indtys, params, leftno, attrs) *)
2084 let type_of_aux' metasenv context term =
2087 type_of_aux' metasenv context term in
2089 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2091 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2094 | RefineFailure msg as e ->
2095 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2097 | Uncertain msg as e ->
2098 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2102 let profiler2 = HExtlib.profile "CicRefine"
2104 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2105 profiler2.HExtlib.profile
2106 (type_of_aux' ?localization_tbl metasenv context term) ugraph
2108 let typecheck ~localization_tbl metasenv uri obj =
2109 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2111 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2112 (* vim:set foldmethod=marker: *)