1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
30 exception RefineFailure of string Lazy.t;;
31 exception Uncertain of string Lazy.t;;
32 exception AssertFailure of string Lazy.t;;
34 let insert_coercions = ref true
35 let pack_coercions = ref true
40 if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());;
42 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
44 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
47 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
48 in profiler_eat_prods2.HExtlib.profile foo ()
50 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
51 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
54 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
56 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
59 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
60 in profiler_eat_prods.HExtlib.profile foo ()
62 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
63 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
66 let profiler = HExtlib.profile "CicRefine.fo_unif"
68 let fo_unif_subst subst context metasenv t1 t2 ugraph =
71 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
72 in profiler.HExtlib.profile foo ()
74 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
75 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
78 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
81 RefineFailure msg -> RefineFailure (f msg)
82 | Uncertain msg -> Uncertain (f msg)
83 | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
84 | Sys.Break -> raise exn
85 | _ -> prerr_endline (Printexc.to_string exn); assert false
89 Cic.CicHash.find localization_tbl t
91 prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
94 raise (HExtlib.Localized (loc,exn'))
96 let relocalize localization_tbl oldt newt =
98 let infos = Cic.CicHash.find localization_tbl oldt in
99 Cic.CicHash.remove localization_tbl oldt;
100 Cic.CicHash.add localization_tbl newt infos;
108 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
109 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
112 let exp_impl metasenv subst context =
115 let (metasenv', idx) =
116 CicMkImplicit.mk_implicit_type metasenv subst context in
118 CicMkImplicit.identity_relocation_list_for_metavariable context in
119 metasenv', Cic.Meta (idx, irl)
121 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
122 metasenv', Cic.Meta (idx, [])
124 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
126 CicMkImplicit.identity_relocation_list_for_metavariable context in
127 metasenv', Cic.Meta (idx, irl)
131 let is_a_double_coercion t =
133 let rec aux acc = function
135 | x::tl -> aux (acc@[x]) tl
140 let imp = Cic.Implicit None in
141 let dummyres = false,imp, imp,imp,imp in
143 | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
144 (match last_of tl with
145 | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
146 let sib2,head = last_of tl2 in
147 true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
152 let more_args_than_expected
153 localization_tbl metasenv subst he context hetype' tlbody_and_type exn
157 CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
158 " (that has type "^CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
159 ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
160 " arguments that are more than expected")
162 enrich localization_tbl he ~f:(fun _-> msg) exn
165 let mk_prod_of_metas metasenv context' subst args =
166 let rec mk_prod metasenv context' = function
168 let (metasenv, idx) =
169 CicMkImplicit.mk_implicit_type metasenv subst context'
172 CicMkImplicit.identity_relocation_list_for_metavariable context'
174 metasenv,Cic.Meta (idx, irl)
176 let (metasenv, idx) =
177 CicMkImplicit.mk_implicit_type metasenv subst context'
180 CicMkImplicit.identity_relocation_list_for_metavariable context'
182 let meta = Cic.Meta (idx,irl) in
184 (* The name must be fresh for context. *)
185 (* Nevertheless, argty is well-typed only in context. *)
186 (* Thus I generate a name (name_hint) in context and *)
187 (* then I generate a name --- using the hint name_hint *)
188 (* --- that is fresh in context'. *)
190 (* Cic.Name "pippo" *)
191 FreshNamesGenerator.mk_fresh_name ~subst metasenv
192 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
193 (CicMetaSubst.apply_subst_context subst context')
195 ~typ:(CicMetaSubst.apply_subst subst argty)
197 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
198 FreshNamesGenerator.mk_fresh_name ~subst
199 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
201 let metasenv,target =
202 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
204 metasenv,Cic.Prod (name,meta,target)
206 mk_prod metasenv context' args
209 let rec type_of_constant uri ugraph =
210 let module C = Cic in
211 let module R = CicReduction in
212 let module U = UriManager in
213 let _ = CicTypeChecker.typecheck uri in
216 CicEnvironment.get_cooked_obj ugraph uri
217 with Not_found -> assert false
220 C.Constant (_,_,ty,_,_) -> ty,u
221 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
225 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
227 and type_of_variable uri ugraph =
228 let module C = Cic in
229 let module R = CicReduction in
230 let module U = UriManager in
231 let _ = CicTypeChecker.typecheck uri in
234 CicEnvironment.get_cooked_obj ugraph uri
235 with Not_found -> assert false
238 C.Variable (_,_,ty,_,_) -> ty,u
242 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
244 and type_of_mutual_inductive_defs uri i ugraph =
245 let module C = Cic in
246 let module R = CicReduction in
247 let module U = UriManager in
248 let _ = CicTypeChecker.typecheck uri in
251 CicEnvironment.get_cooked_obj ugraph uri
252 with Not_found -> assert false
255 C.InductiveDefinition (dl,_,_,_) ->
256 let (_,_,arity,_) = List.nth dl i in
261 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
263 and type_of_mutual_inductive_constr uri i j ugraph =
264 let module C = Cic in
265 let module R = CicReduction in
266 let module U = UriManager in
267 let _ = CicTypeChecker.typecheck uri in
270 CicEnvironment.get_cooked_obj ugraph uri
271 with Not_found -> assert false
274 C.InductiveDefinition (dl,_,_,_) ->
275 let (_,_,_,cl) = List.nth dl i in
276 let (_,ty) = List.nth cl (j-1) in
282 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
285 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
287 (* the check_branch function checks if a branch of a case is refinable.
288 It returns a pair (outype_instance,args), a subst and a metasenv.
289 outype_instance is the expected result of applying the case outtype
291 The problem is that outype is in general unknown, and we should
292 try to synthesize it from the above information, that is in general
293 a second order unification problem. *)
295 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
296 let module C = Cic in
297 (* let module R = CicMetaSubst in *)
298 let module R = CicReduction in
299 match R.whd ~subst context expectedtype with
301 (n,context,actualtype, [term]), subst, metasenv, ugraph
302 | C.Appl (C.MutInd (_,_,_)::tl) ->
303 let (_,arguments) = split tl left_args_no in
304 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
305 | C.Prod (name,so,de) ->
306 (* we expect that the actual type of the branch has the due
308 (match R.whd ~subst context actualtype with
309 C.Prod (name',so',de') ->
310 let subst, metasenv, ugraph1 =
311 fo_unif_subst subst context metasenv so so' ugraph in
313 (match CicSubstitution.lift 1 term with
314 C.Appl l -> C.Appl (l@[C.Rel 1])
315 | t -> C.Appl [t ; C.Rel 1]) in
316 (* we should also check that the name variable is anonymous in
317 the actual type de' ?? *)
319 ((Some (name,(C.Decl so)))::context)
320 metasenv subst left_args_no de' term' de ugraph1
321 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
322 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
324 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
327 let rec type_of_aux subst metasenv context t ugraph =
328 let module C = Cic in
329 let module S = CicSubstitution in
330 let module U = UriManager in
331 let (t',_,_,_,_) as res =
336 match List.nth context (n - 1) with
337 Some (_,C.Decl ty) ->
338 t,S.lift n ty,subst,metasenv, ugraph
339 | Some (_,C.Def (_,Some ty)) ->
340 t,S.lift n ty,subst,metasenv, ugraph
341 | Some (_,C.Def (bo,None)) ->
343 (* if it is in the context it must be already well-typed*)
344 CicTypeChecker.type_of_aux' ~subst metasenv context
347 t,ty,subst,metasenv,ugraph
349 enrich localization_tbl t
350 (RefineFailure (lazy "Rel to hidden hypothesis"))
353 enrich localization_tbl t
354 (RefineFailure (lazy "Not a closed term")))
355 | C.Var (uri,exp_named_subst) ->
356 let exp_named_subst',subst',metasenv',ugraph1 =
357 check_exp_named_subst
358 subst metasenv context exp_named_subst ugraph
360 let ty_uri,ugraph1 = type_of_variable uri ugraph in
362 CicSubstitution.subst_vars exp_named_subst' ty_uri
364 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
367 let (canonical_context, term,ty) =
368 CicUtil.lookup_subst n subst
370 let l',subst',metasenv',ugraph1 =
371 check_metasenv_consistency n subst metasenv context
372 canonical_context l ugraph
374 (* trust or check ??? *)
375 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
376 subst', metasenv', ugraph1
377 (* type_of_aux subst metasenv
378 context (CicSubstitution.subst_meta l term) *)
379 with CicUtil.Subst_not_found _ ->
380 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
381 let l',subst',metasenv', ugraph1 =
382 check_metasenv_consistency n subst metasenv context
383 canonical_context l ugraph
385 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
386 subst', metasenv',ugraph1)
387 | C.Sort (C.Type tno) ->
388 let tno' = CicUniv.fresh() in
390 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
391 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
393 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
395 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
396 | C.Implicit infos ->
397 let metasenv',t' = exp_impl metasenv subst context infos in
398 type_of_aux subst metasenv' context t' ugraph
400 let ty',_,subst',metasenv',ugraph1 =
401 type_of_aux subst metasenv context ty ugraph
403 let te',inferredty,subst'',metasenv'',ugraph2 =
404 type_of_aux subst' metasenv' context te ugraph1
406 let (te', ty'), subst''',metasenv''',ugraph3 =
407 coerce_to_something true localization_tbl te' inferredty ty'
408 subst'' metasenv'' context ugraph2
410 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
411 | C.Prod (name,s,t) ->
412 let s',sort1,subst',metasenv',ugraph1 =
413 type_of_aux subst metasenv context s ugraph
415 let s',sort1,subst', metasenv',ugraph1 =
416 coerce_to_sort localization_tbl
417 s' sort1 subst' context metasenv' ugraph1
419 let context_for_t = ((Some (name,(C.Decl s')))::context) in
420 let t',sort2,subst'',metasenv'',ugraph2 =
421 type_of_aux subst' metasenv'
422 context_for_t t ugraph1
424 let t',sort2,subst'',metasenv'',ugraph2 =
425 coerce_to_sort localization_tbl
426 t' sort2 subst'' context_for_t metasenv'' ugraph2
428 let sop,subst''',metasenv''',ugraph3 =
429 sort_of_prod localization_tbl subst'' metasenv''
430 context (name,s') t' (sort1,sort2) ugraph2
432 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
433 | C.Lambda (n,s,t) ->
434 let s',sort1,subst',metasenv',ugraph1 =
435 type_of_aux subst metasenv context s ugraph
437 let s',sort1,subst',metasenv',ugraph1 =
438 coerce_to_sort localization_tbl
439 s' sort1 subst' context metasenv' ugraph1
441 let context_for_t = ((Some (n,(C.Decl s')))::context) in
442 let t',type2,subst'',metasenv'',ugraph2 =
443 type_of_aux subst' metasenv' context_for_t t ugraph1
445 C.Lambda (n,s',t'),C.Prod (n,s',type2),
446 subst'',metasenv'',ugraph2
448 (* only to check if s is well-typed *)
449 let s',ty,subst',metasenv',ugraph1 =
450 type_of_aux subst metasenv context s ugraph
452 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
454 let t',inferredty,subst'',metasenv'',ugraph2 =
455 type_of_aux subst' metasenv'
456 context_for_t t ugraph1
458 (* One-step LetIn reduction.
459 * Even faster than the previous solution.
460 * Moreover the inferred type is closer to the expected one.
463 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
464 subst'',metasenv'',ugraph2
465 | C.Appl (he::((_::_) as tl)) ->
466 let he',hetype,subst',metasenv',ugraph1 =
467 type_of_aux subst metasenv context he ugraph
469 let tlbody_and_type,subst'',metasenv'',ugraph2 =
470 typeof_list subst' metasenv' context ugraph1 tl
472 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
473 eat_prods true subst'' metasenv'' context
474 he' hetype tlbody_and_type ugraph2
476 let newappl = (C.Appl (coerced_he::coerced_args)) in
477 avoid_double_coercion
478 context subst''' metasenv''' ugraph3 newappl applty
479 | C.Appl _ -> assert false
480 | C.Const (uri,exp_named_subst) ->
481 let exp_named_subst',subst',metasenv',ugraph1 =
482 check_exp_named_subst subst metasenv context
483 exp_named_subst ugraph in
484 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
486 CicSubstitution.subst_vars exp_named_subst' ty_uri
488 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
489 | C.MutInd (uri,i,exp_named_subst) ->
490 let exp_named_subst',subst',metasenv',ugraph1 =
491 check_exp_named_subst subst metasenv context
492 exp_named_subst ugraph
494 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
496 CicSubstitution.subst_vars exp_named_subst' ty_uri in
497 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
498 | C.MutConstruct (uri,i,j,exp_named_subst) ->
499 let exp_named_subst',subst',metasenv',ugraph1 =
500 check_exp_named_subst subst metasenv context
501 exp_named_subst ugraph
504 type_of_mutual_inductive_constr uri i j ugraph1
507 CicSubstitution.subst_vars exp_named_subst' ty_uri
509 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
511 | C.MutCase (uri, i, outtype, term, pl) ->
512 (* first, get the inductive type (and noparams)
513 * in the environment *)
514 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
515 let _ = CicTypeChecker.typecheck uri in
516 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
518 C.InductiveDefinition (l,expl_params,parsno,_) ->
519 List.nth l i , expl_params, parsno, u
521 enrich localization_tbl t
523 (lazy ("Unkown mutual inductive definition " ^
524 U.string_of_uri uri)))
526 let rec count_prod t =
527 match CicReduction.whd ~subst context t with
528 C.Prod (_, _, t) -> 1 + (count_prod t)
531 let no_args = count_prod arity in
532 (* now, create a "generic" MutInd *)
533 let metasenv,left_args =
534 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
536 let metasenv,right_args =
537 let no_right_params = no_args - no_left_params in
538 if no_right_params < 0 then assert false
539 else CicMkImplicit.n_fresh_metas
540 metasenv subst context no_right_params
542 let metasenv,exp_named_subst =
543 CicMkImplicit.fresh_subst metasenv subst context expl_params in
546 C.MutInd (uri,i,exp_named_subst)
549 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
551 (* check consistency with the actual type of term *)
552 let term',actual_type,subst,metasenv,ugraph1 =
553 type_of_aux subst metasenv context term ugraph in
554 let expected_type',_, subst, metasenv,ugraph2 =
555 type_of_aux subst metasenv context expected_type ugraph1
557 let actual_type = CicReduction.whd ~subst context actual_type in
558 let subst,metasenv,ugraph3 =
560 fo_unif_subst subst context metasenv
561 expected_type' actual_type ugraph2
564 enrich localization_tbl term' exn
566 lazy ("(10)The term " ^
567 CicMetaSubst.ppterm_in_context ~metasenv subst term'
568 context ^ " has type " ^
569 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
570 context ^ " but is here used with type " ^
571 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
573 let rec instantiate_prod t =
577 match CicReduction.whd ~subst context t with
579 instantiate_prod (CicSubstitution.subst he t') tl
582 let arity_instantiated_with_left_args =
583 instantiate_prod arity left_args in
584 (* TODO: check if the sort elimination
585 * is allowed: [(I q1 ... qr)|B] *)
586 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
588 (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
590 if left_args = [] then
591 (C.MutConstruct (uri,i,j,exp_named_subst))
594 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
596 let p',actual_type,subst,metasenv,ugraph1 =
597 type_of_aux subst metasenv context p ugraph
599 let constructor',expected_type, subst, metasenv,ugraph2 =
600 type_of_aux subst metasenv context constructor ugraph1
602 let outtypeinstance,subst,metasenv,ugraph3 =
604 check_branch 0 context metasenv subst
605 no_left_params actual_type constructor' expected_type
609 enrich localization_tbl constructor'
611 lazy ("(11)The term " ^
612 CicMetaSubst.ppterm_in_context metasenv subst p'
613 context ^ " has type " ^
614 CicMetaSubst.ppterm_in_context metasenv subst actual_type
615 context ^ " but is here used with type " ^
616 CicMetaSubst.ppterm_in_context metasenv subst expected_type
620 outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
621 pl ([],List.length pl,[],subst,metasenv,ugraph3)
624 (* we are left to check that the outype matches his instances.
625 The easy case is when the outype is specified, that amount
626 to a trivial check. Otherwise, we should guess a type from
630 let outtype,outtypety, subst, metasenv,ugraph4 =
631 type_of_aux subst metasenv context outtype ugraph4 in
634 (let candidate,ugraph5,metasenv,subst =
635 let exp_name_subst, metasenv =
637 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
639 let uris = CicUtil.params_of_obj o in
641 fun uri (acc,metasenv) ->
642 let metasenv',new_meta =
643 CicMkImplicit.mk_implicit metasenv subst context
646 CicMkImplicit.identity_relocation_list_for_metavariable
649 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
653 match left_args,right_args with
654 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
656 let rec mk_right_args =
659 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
661 let right_args_no = List.length right_args in
662 let lifted_left_args =
663 List.map (CicSubstitution.lift right_args_no) left_args
665 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
666 (lifted_left_args @ mk_right_args right_args_no))
669 FreshNamesGenerator.mk_fresh_name ~subst metasenv
670 context Cic.Anonymous ~typ:ty
672 match outtypeinstances with
674 let extended_context =
675 let rec add_right_args =
677 Cic.Prod (name,ty,t) ->
678 Some (name,Cic.Decl ty)::(add_right_args t)
681 (Some (fresh_name,Cic.Decl ty))::
683 (add_right_args arity_instantiated_with_left_args))@
686 let metasenv,new_meta =
687 CicMkImplicit.mk_implicit metasenv subst extended_context
690 CicMkImplicit.identity_relocation_list_for_metavariable
693 let rec add_lambdas b =
695 Cic.Prod (name,ty,t) ->
696 Cic.Lambda (name,ty,(add_lambdas b t))
697 | _ -> Cic.Lambda (fresh_name, ty, b)
700 add_lambdas (Cic.Meta (new_meta,irl))
701 arity_instantiated_with_left_args
703 (Some candidate),ugraph4,metasenv,subst
704 | (constructor_args_no,_,instance,_)::tl ->
706 let instance',subst,metasenv =
707 CicMetaSubst.delift_rels subst metasenv
708 constructor_args_no instance
710 let candidate,ugraph,metasenv,subst =
712 fun (candidate_oty,ugraph,metasenv,subst)
713 (constructor_args_no,_,instance,_) ->
714 match candidate_oty with
715 | None -> None,ugraph,metasenv,subst
718 let instance',subst,metasenv =
719 CicMetaSubst.delift_rels subst metasenv
720 constructor_args_no instance
722 let subst,metasenv,ugraph =
723 fo_unif_subst subst context metasenv
726 candidate_oty,ugraph,metasenv,subst
728 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
729 | RefineFailure _ | Uncertain _ ->
730 None,ugraph,metasenv,subst
731 ) (Some instance',ugraph4,metasenv,subst) tl
734 | None -> None, ugraph,metasenv,subst
736 let rec add_lambdas n b =
738 Cic.Prod (name,ty,t) ->
739 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
741 Cic.Lambda (fresh_name, ty,
742 CicSubstitution.lift (n + 1) t)
745 (add_lambdas 0 t arity_instantiated_with_left_args),
746 ugraph,metasenv,subst
747 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
748 None,ugraph4,metasenv,subst
751 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
753 let subst,metasenv,ugraph =
755 fo_unif_subst subst context metasenv
756 candidate outtype ugraph5
758 exn -> assert false(* unification against a metavariable *)
760 C.MutCase (uri, i, outtype, term', pl'),
761 CicReduction.head_beta_reduce
762 (CicMetaSubst.apply_subst subst
763 (Cic.Appl (outtype::right_args@[term']))),
764 subst,metasenv,ugraph)
765 | _ -> (* easy case *)
766 let tlbody_and_type,subst,metasenv,ugraph4 =
767 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
769 let _,_,_,subst,metasenv,ugraph4 =
770 eat_prods false subst metasenv context
771 outtype outtypety tlbody_and_type ugraph4
773 let _,_, subst, metasenv,ugraph5 =
774 type_of_aux subst metasenv context
775 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
777 let (subst,metasenv,ugraph6) =
779 (fun (subst,metasenv,ugraph)
780 p (constructor_args_no,context,instance,args)
785 CicSubstitution.lift constructor_args_no outtype
787 C.Appl (outtype'::args)
789 CicReduction.whd ~subst context appl
792 fo_unif_subst subst context metasenv instance instance'
796 enrich localization_tbl p exn
798 lazy ("(12)The term " ^
799 CicMetaSubst.ppterm_in_context ~metasenv subst p
800 context ^ " has type " ^
801 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
802 context ^ " but is here used with type " ^
803 CicMetaSubst.ppterm_in_context ~metasenv subst instance
805 (subst,metasenv,ugraph5) pl' outtypeinstances
807 C.MutCase (uri, i, outtype, term', pl'),
808 CicReduction.head_beta_reduce
809 (CicMetaSubst.apply_subst subst
810 (C.Appl(outtype::right_args@[term]))),
811 subst,metasenv,ugraph6)
813 let fl_ty',subst,metasenv,types,ugraph1,len =
815 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
816 let ty',_,subst',metasenv',ugraph1 =
817 type_of_aux subst metasenv context ty ugraph
819 fl @ [ty'],subst',metasenv',
820 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
821 :: types, ugraph, len+1
822 ) ([],subst,metasenv,[],ugraph,0) fl
824 let context' = types@context in
825 let fl_bo',subst,metasenv,ugraph2 =
827 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
828 let bo',ty_of_bo,subst,metasenv,ugraph1 =
829 type_of_aux subst metasenv context' bo ugraph in
830 let expected_ty = CicSubstitution.lift len ty in
831 let subst',metasenv',ugraph' =
833 fo_unif_subst subst context' metasenv
834 ty_of_bo expected_ty ugraph1
837 enrich localization_tbl bo exn
839 lazy ("(13)The term " ^
840 CicMetaSubst.ppterm_in_context ~metasenv subst bo
841 context' ^ " has type " ^
842 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
843 context' ^ " but is here used with type " ^
844 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
847 fl @ [bo'] , subst',metasenv',ugraph'
848 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
850 let ty = List.nth fl_ty' i in
851 (* now we have the new ty in fl_ty', the new bo in fl_bo',
852 * and we want the new fl with bo' and ty' injected in the right
855 let rec map3 f l1 l2 l3 =
858 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
861 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
864 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
866 let fl_ty',subst,metasenv,types,ugraph1,len =
868 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
869 let ty',_,subst',metasenv',ugraph1 =
870 type_of_aux subst metasenv context ty ugraph
872 fl @ [ty'],subst',metasenv',
873 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
874 types, ugraph1, len+1
875 ) ([],subst,metasenv,[],ugraph,0) fl
877 let context' = types@context in
878 let fl_bo',subst,metasenv,ugraph2 =
880 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
881 let bo',ty_of_bo,subst,metasenv,ugraph1 =
882 type_of_aux subst metasenv context' bo ugraph in
883 let expected_ty = CicSubstitution.lift len ty in
884 let subst',metasenv',ugraph' =
886 fo_unif_subst subst context' metasenv
887 ty_of_bo expected_ty ugraph1
890 enrich localization_tbl bo exn
892 lazy ("(14)The term " ^
893 CicMetaSubst.ppterm_in_context ~metasenv subst bo
894 context' ^ " has type " ^
895 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
896 context' ^ " but is here used with type " ^
897 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
900 fl @ [bo'],subst',metasenv',ugraph'
901 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
903 let ty = List.nth fl_ty' i in
904 (* now we have the new ty in fl_ty', the new bo in fl_bo',
905 * and we want the new fl with bo' and ty' injected in the right
908 let rec map3 f l1 l2 l3 =
911 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
914 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
917 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
919 relocalize localization_tbl t t';
922 (* check_metasenv_consistency checks that the "canonical" context of a
923 metavariable is consitent - up to relocation via the relocation list l -
924 with the actual context *)
925 and check_metasenv_consistency
926 metano subst metasenv context canonical_context l ugraph
928 let module C = Cic in
929 let module R = CicReduction in
930 let module S = CicSubstitution in
931 let lifted_canonical_context =
935 | (Some (n,C.Decl t))::tl ->
936 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
937 | (Some (n,C.Def (t,None)))::tl ->
938 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
939 | None::tl -> None::(aux (i+1) tl)
940 | (Some (n,C.Def (t,Some ty)))::tl ->
942 C.Def ((S.subst_meta l (S.lift i t)),
943 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
945 aux 1 canonical_context
949 (fun (l,subst,metasenv,ugraph) t ct ->
952 l @ [None],subst,metasenv,ugraph
953 | Some t,Some (_,C.Def (ct,_)) ->
954 let subst',metasenv',ugraph' =
956 prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
957 fo_unif_subst subst context metasenv t ct ugraph
958 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))))))
960 l @ [Some t],subst',metasenv',ugraph'
961 | Some t,Some (_,C.Decl ct) ->
962 let t',inferredty,subst',metasenv',ugraph1 =
963 type_of_aux subst metasenv context t ugraph
965 let subst'',metasenv'',ugraph2 =
968 subst' context metasenv' inferredty ct ugraph1
969 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))))))
971 l @ [Some t'], subst'',metasenv'',ugraph2
973 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
975 Invalid_argument _ ->
979 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
980 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
981 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
983 and check_exp_named_subst metasubst metasenv context tl ugraph =
984 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
986 [] -> [],metasubst,metasenv,ugraph
988 let ty_uri,ugraph1 = type_of_variable uri ugraph in
990 CicSubstitution.subst_vars substs ty_uri in
991 (* CSC: why was this code here? it is wrong
992 (match CicEnvironment.get_cooked_obj ~trust:false uri with
993 Cic.Variable (_,Some bo,_,_) ->
996 "A variable with a body can not be explicit substituted"))
997 | Cic.Variable (_,None,_,_) -> ()
1000 (RefineFailure (lazy
1001 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1004 let t',typeoft,metasubst',metasenv',ugraph2 =
1005 type_of_aux metasubst metasenv context t ugraph1 in
1006 let subst = uri,t' in
1007 let metasubst'',metasenv'',ugraph3 =
1010 metasubst' context metasenv' typeoft typeofvar ugraph2
1012 raise (RefineFailure (lazy
1013 ("Wrong Explicit Named Substitution: " ^
1014 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1015 " not unifiable with " ^
1016 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1018 (* FIXME: no mere tail recursive! *)
1019 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1020 check_exp_named_subst_aux
1021 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1023 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1025 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1028 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1031 let module C = Cic in
1032 let context_for_t2 = (Some (name,C.Decl s))::context in
1033 let t1'' = CicReduction.whd ~subst context t1 in
1034 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1035 match (t1'', t2'') with
1036 (C.Sort s1, C.Sort s2)
1037 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1038 (* different than Coq manual!!! *)
1039 C.Sort s2,subst,metasenv,ugraph
1040 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1041 let t' = CicUniv.fresh() in
1043 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1044 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1045 C.Sort (C.Type t'),subst,metasenv,ugraph2
1047 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1048 | (C.Sort _,C.Sort (C.Type t1)) ->
1049 C.Sort (C.Type t1),subst,metasenv,ugraph
1050 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1051 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1052 (* TODO how can we force the meta to become a sort? If we don't we
1053 * break the invariant that refine produce only well typed terms *)
1054 (* TODO if we check the non meta term and if it is a sort then we
1055 * are likely to know the exact value of the result e.g. if the rhs
1056 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1057 let (metasenv,idx) =
1058 CicMkImplicit.mk_implicit_sort metasenv subst in
1059 let (subst, metasenv,ugraph1) =
1061 fo_unif_subst subst context_for_t2 metasenv
1062 (C.Meta (idx,[])) t2'' ugraph
1063 with _ -> assert false (* unification against a metavariable *)
1065 t2'',subst,metasenv,ugraph1
1068 enrich localization_tbl s
1072 "%s is supposed to be a type, but its type is %s"
1073 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1074 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1076 enrich localization_tbl t
1080 "%s is supposed to be a type, but its type is %s"
1081 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1082 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1084 and avoid_double_coercion context subst metasenv ugraph t ty =
1085 if not !pack_coercions then
1086 t,ty,subst,metasenv,ugraph
1088 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1090 let source_carr = CoercGraph.source_of c2 in
1091 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1092 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1094 | CoercGraph.SomeCoercion candidates ->
1096 HExtlib.list_findopt
1097 (function (metasenv,last,c) ->
1099 | c when not (CoercGraph.is_composite c) ->
1100 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1103 let subst,metasenv,ugraph =
1104 fo_unif_subst subst context metasenv last head ugraph in
1105 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1110 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1111 let newt,_,subst,metasenv,ugraph =
1112 type_of_aux subst metasenv context c ugraph in
1113 debug_print (lazy "tipa...");
1114 let subst, metasenv, ugraph =
1115 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1116 fo_unif_subst subst context metasenv newt t ugraph
1118 debug_print (lazy "unifica...");
1119 Some (newt, ty, subst, metasenv, ugraph)
1121 | RefineFailure s | Uncertain s when not !pack_coercions->
1122 debug_print s; debug_print (lazy "stop\n");None
1123 | RefineFailure s | Uncertain s ->
1124 debug_print s;debug_print (lazy "goon\n");
1126 let old_pack_coercions = !pack_coercions in
1127 pack_coercions := false; (* to avoid diverging *)
1128 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1129 type_of_aux subst metasenv context c1_c2_implicit ugraph
1131 pack_coercions := old_pack_coercions;
1133 is_a_double_coercion refined_c1_c2_implicit
1139 match refined_c1_c2_implicit with
1140 | Cic.Appl l -> HExtlib.list_last l
1143 let subst, metasenv, ugraph =
1144 try fo_unif_subst subst context metasenv
1146 with RefineFailure s| Uncertain s->
1147 debug_print s;assert false
1149 let subst, metasenv, ugraph =
1150 fo_unif_subst subst context metasenv
1151 refined_c1_c2_implicit t ugraph
1153 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1155 | RefineFailure s | Uncertain s ->
1156 pack_coercions := true;debug_print s;None
1157 | exn -> pack_coercions := true; raise exn))
1160 (match selected with
1164 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1165 t, ty, subst, metasenv, ugraph)
1166 | _ -> t, ty, subst, metasenv, ugraph)
1168 t, ty, subst, metasenv, ugraph
1170 and typeof_list subst metasenv context ugraph l =
1171 let tlbody_and_type,subst,metasenv,ugraph =
1173 (fun x (res,subst,metasenv,ugraph) ->
1174 let x',ty,subst',metasenv',ugraph1 =
1175 type_of_aux subst metasenv context x ugraph
1177 (x', ty)::res,subst',metasenv',ugraph1
1178 ) l ([],subst,metasenv,ugraph)
1180 tlbody_and_type,subst,metasenv,ugraph
1183 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1185 (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1186 let fix_arity exn metasenv context subst he hetype ugraph =
1187 let hetype = CicMetaSubst.apply_subst subst hetype in
1188 let src = CoercDb.coerc_carr_of_term hetype in
1189 let tgt = CoercDb.Fun 0 in
1190 match CoercGraph.look_for_coercion' metasenv subst context src tgt with
1191 | CoercGraph.NoCoercion
1192 | CoercGraph.NotMetaClosed
1193 | CoercGraph.NotHandled _ -> raise exn
1194 | CoercGraph.SomeCoercionToTgt candidates
1195 | CoercGraph.SomeCoercion candidates ->
1197 (fun (metasenv,last,coerc) ->
1199 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1200 let subst,metasenv,ugraph =
1201 fo_unif_subst subst context metasenv last he ugraph in
1202 debug_print (lazy ("New head: "^ pp coerc));
1204 let t,tty,subst,metasenv,ugraph =
1205 type_of_aux subst metasenv context coerc ugraph in
1206 (*{{{*)debug_print (lazy (" refined: "^ pp t));
1207 debug_print (lazy (" has type: "^ pp tty));(*}}}*)
1208 Some (t,tty,subst,metasenv,ugraph)
1210 | Uncertain _ | RefineFailure _
1211 | HExtlib.Localized (_,Uncertain _)
1212 | HExtlib.Localized (_,RefineFailure _) -> None
1213 | exn -> assert false)
1216 (* aux function to process the type of the head and the args in parallel *)
1217 let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1219 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1220 | (hete, hety)::tl as args ->
1221 match (CicReduction.whd ~subst context hetype) with
1222 | Cic.Prod (n,s,t) ->
1223 let arg,subst,metasenv,ugraph =
1224 coerce_to_something allow_coercions localization_tbl
1225 hete hety s subst metasenv context ugraph in
1227 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1228 ugraph (newargs@[arg]) tl
1231 match he, newargs with
1233 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1234 | _ -> Cic.Appl (he::List.map fst newargs)
1236 (*{{{*) debug_print (lazy
1238 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1239 "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1240 "\n but is applyed to: " ^ String.concat ";"
1241 (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1242 let exn = RefineFailure (lazy ("more args than expected")) in
1243 let possible_fixes =
1244 fix_arity exn metasenv context subst he hetype ugraph in
1246 HExtlib.list_findopt
1247 (fun (he,hetype,subst,metasenv,ugraph) ->
1248 (* {{{ *)debug_print (lazy ("Try fix: "^
1249 CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1250 debug_print (lazy (" of type: "^
1251 CicMetaSubst.ppterm_in_context
1252 ~metasenv subst hetype context)); (* }}} *)
1254 Some (eat_prods_and_args
1255 metasenv subst context he hetype ugraph [] args)
1256 with RefineFailure _ | Uncertain _ -> None)
1261 more_args_than_expected localization_tbl metasenv
1262 subst he context hetype args_bo_and_ty exn
1264 (* first we check if we are in the simple case of a meta closed term *)
1265 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1266 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1267 (* this optimization is to postpone fix_arity (the most common case)*)
1268 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1270 (* this (says CSC) is also useful to infer dependent types *)
1271 let pristinemenv = metasenv in
1272 let metasenv,hetype' =
1273 mk_prod_of_metas metasenv context subst args_bo_and_ty
1276 let subst,metasenv,ugraph =
1277 fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1279 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1280 with RefineFailure _ | Uncertain _ ->
1281 subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1283 let coerced_args,subst,metasenv,he,t,ugraph =
1285 metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1287 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1289 and coerce_to_something
1290 allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1292 let module CS = CicSubstitution in
1293 let module CR = CicReduction in
1294 let cs_subst = CS.subst ~avoid_beta_redexes:true in
1295 let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1296 debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1298 CoercGraph.look_for_coercion metasenv subst context infty expty
1301 | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
1302 "coerce_atom_to_something fails since not meta closed"))
1303 | CoercGraph.NoCoercion
1304 | CoercGraph.SomeCoercionToTgt _
1305 | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
1306 "coerce_atom_to_something fails since no coercions found"))
1307 | CoercGraph.SomeCoercion candidates ->
1308 debug_print (lazy (string_of_int (List.length candidates) ^
1309 " candidates found"));
1310 let uncertain = ref false in
1314 (fun (metasenv,last,c) ->
1316 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1317 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1319 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1320 debug_print (lazy ("FO_UNIF_SUBST: " ^
1321 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1322 let subst,metasenv,ugraph =
1323 fo_unif_subst subst context metasenv last t ugraph
1325 let newt,newhety,subst,metasenv,ugraph =
1326 type_of_aux subst metasenv context c ugraph in
1327 let newt, newty, subst, metasenv, ugraph =
1328 avoid_double_coercion context subst metasenv ugraph newt expty
1330 let subst,metasenv,ugraph =
1331 fo_unif_subst subst context metasenv newhety expty ugraph in
1332 Some ((newt,newty), subst, metasenv, ugraph)
1334 | Uncertain _ -> uncertain := true; None
1335 | RefineFailure _ -> None)
1340 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1348 | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1349 | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1351 let rec coerce_to_something_aux
1352 t infty expty subst metasenv context ugraph
1355 let subst, metasenv, ugraph =
1356 fo_unif_subst subst context metasenv infty expty ugraph
1358 (t, expty), subst, metasenv, ugraph
1359 with Uncertain _ | RefineFailure _ as exn ->
1360 if not allow_coercions || not !insert_coercions then
1361 enrich localization_tbl t exn
1363 let whd = CicReduction.whd ~delta:false in
1364 let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1365 let infty = clean infty subst context in
1366 let expty = clean expty subst context in
1367 let t = clean t subst context in
1368 (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1369 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1370 CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1371 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1372 let (coerced,_),subst,metasenv,_ as result =
1373 match infty, expty, t with
1374 | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1375 (*{{{*) debug_print (lazy "FIX");
1377 [name,i,_(* infty *),bo] ->
1379 Some (Cic.Name name,Cic.Decl expty)::context in
1380 let (rel1, _), subst, metasenv, ugraph =
1381 coerce_to_something_aux (Cic.Rel 1)
1382 (CS.lift 1 expty) (CS.lift 1 infty) subst
1383 metasenv context_bo ugraph in
1384 let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1385 let (bo,_), subst, metasenv, ugraph =
1386 coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1388 metasenv context_bo ugraph
1390 (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1391 | _ -> assert false (* not implemented yet *)) (*}}}*)
1392 | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1393 (*{{{*) debug_print (lazy "CASE");
1394 (* {{{ helper functions *)
1395 let get_cl_and_left_p uri tyno outty ugraph =
1396 match CicEnvironment.get_obj ugraph uri with
1397 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1400 match CicReduction.whd ~delta:false ctx t with
1401 | Cic.Prod (name,src,tgt) ->
1402 let ctx = Some (name, Cic.Decl src) :: ctx in
1408 let rec skip_lambda_delifting t n =
1411 | Cic.Lambda (_,_,t),n ->
1412 skip_lambda_delifting
1413 (CS.subst (Cic.Implicit None) t) (n - 1)
1416 let get_l_r_p n = function
1417 | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1418 | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1419 HExtlib.split_nth n args
1422 let _, _, ty, cl = List.nth tl tyno in
1423 let pis = count_pis ty in
1424 let rno = pis - leftno in
1425 let t = skip_lambda_delifting outty rno in
1426 let left_p, _ = get_l_r_p leftno t in
1427 let instantiale_with_left cl =
1431 (fun t p -> match t with
1432 | Cic.Prod (_,_,t) ->
1438 let cl = instantiale_with_left (List.map snd cl) in
1439 cl, left_p, leftno, rno, ugraph
1442 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1445 let rec mkr n = function
1446 | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1449 CicReplace.replace_lifting
1450 ~equality:(fun _ -> CicUtil.alpha_equivalence)
1452 ~what:(matched::right_p)
1453 ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1457 | Cic.Lambda (name, src, tgt),_ ->
1458 Cic.Lambda (name, src,
1459 keep_lambdas_and_put_expty
1460 (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1461 (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1464 let eq_uri, eq, eq_refl =
1465 match LibraryObjects.eq_URI () with
1466 | None -> HLog.warn "no default equality"; raise exn
1467 | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1470 metasenv subst context uri tyno cty outty mty m leftno i
1472 let rec aux context outty par k mty m = function
1473 | Cic.Prod (name, src, tgt) ->
1476 (Some (name, Cic.Decl src) :: context)
1477 (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1478 (CS.lift 1 mty) (CS.lift 1 m) tgt
1480 Cic.Prod (name, src, t), k
1483 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1484 if par <> [] then Cic.Appl (k::par) else k
1486 Cic.Prod (Cic.Name "p",
1487 Cic.Appl [eq; mty; m; k],
1489 (CR.head_beta_reduce ~delta:false
1490 (Cic.Appl [outty;k])))),k
1491 | Cic.Appl (Cic.MutInd _::pl) ->
1492 let left_p,right_p = HExtlib.split_nth leftno pl in
1493 let has_rights = right_p <> [] in
1495 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1496 Cic.Appl (k::left_p@par)
1500 CicTypeChecker.type_of_aux' ~subst metasenv context k
1501 CicUniv.oblivion_ugraph
1503 | Cic.Appl (Cic.MutInd _::args),_ ->
1504 snd (HExtlib.split_nth leftno args)
1506 with CicTypeChecker.TypeCheckerFailure _-> assert false
1509 CR.head_beta_reduce ~delta:false
1510 (Cic.Appl (outty ::right_p @ [k])),k
1512 Cic.Prod (Cic.Name "p",
1513 Cic.Appl [eq; mty; m; k],
1515 (CR.head_beta_reduce ~delta:false
1516 (Cic.Appl (outty ::right_p @ [k]))))),k
1519 aux context outty [] 1 mty m cty
1521 let add_lambda_for_refl_m pbo rno mty m k cty =
1522 (* k lives in the right context *)
1523 if rno <> 0 then pbo else
1524 let rec aux mty m = function
1525 | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1526 Cic.Lambda (name,src,
1527 (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1529 Cic.Lambda (Cic.Name "p",
1530 Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1534 let add_pi_for_refl_m new_outty mty m rno =
1535 if rno <> 0 then new_outty else
1536 let rec aux m mty = function
1537 | Cic.Lambda (name, src, tgt) ->
1538 Cic.Lambda (name, src,
1539 aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1542 (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1546 in (* }}} end helper functions *)
1547 (* constructors types with left params already instantiated *)
1548 let outty = CicMetaSubst.apply_subst subst outty in
1549 let cl, left_p, leftno,rno,ugraph =
1550 get_cl_and_left_p uri tyno outty ugraph
1555 CicTypeChecker.type_of_aux' ~subst metasenv context m
1556 CicUniv.oblivion_ugraph
1558 | Cic.MutInd _ as mty,_ -> [], mty
1559 | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
1560 snd (HExtlib.split_nth leftno args), mty
1562 with CicTypeChecker.TypeCheckerFailure _ -> assert false
1565 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1568 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1569 ~metasenv subst new_outty context));
1570 let _,pl,subst,metasenv,ugraph =
1572 (fun cty pbo (i, acc, s, menv, ugraph) ->
1573 (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1574 * (new_)outty right_par (K_i left_par k_par) *)
1576 add_params menv s context uri tyno
1577 cty outty mty m leftno i in
1579 (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1580 ~metasenv subst infty_pbo context));
1581 let expty_pbo, k = (* k is (K_i left_par k_par) *)
1582 add_params menv s context uri tyno
1583 cty new_outty mty m leftno i in
1585 (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1586 ~metasenv subst expty_pbo context));
1587 let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1589 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1590 ~metasenv subst pbo context));
1591 let (pbo, _), subst, metasenv, ugraph =
1592 coerce_to_something_aux pbo infty_pbo expty_pbo
1593 s menv context ugraph
1596 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1597 ~metasenv subst pbo context));
1598 (i-1, pbo::acc, subst, metasenv, ugraph))
1599 cl pl (List.length pl, [], subst, metasenv, ugraph)
1601 let new_outty = add_pi_for_refl_m new_outty mty m rno in
1603 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1604 ~metasenv subst new_outty context));
1607 let refl_m=Cic.Appl[eq_refl;mty;m]in
1608 Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1610 Cic.MutCase(uri,tyno,new_outty,m,pl)
1612 (t, expty), subst, metasenv, ugraph (*}}}*)
1613 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1614 (*{{{*) debug_print (lazy "LAM");
1616 FreshNamesGenerator.mk_fresh_name
1617 ~subst metasenv context ~typ:src2 Cic.Anonymous
1619 let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1620 (* contravariant part: the argument of f:src->ty *)
1621 let (rel1, _), subst, metasenv, ugraph =
1622 coerce_to_something_aux
1623 (Cic.Rel 1) (CS.lift 1 src2)
1624 (CS.lift 1 src) subst metasenv context_src2 ugraph
1626 (* covariant part: the result of f(c x); x:src2; (c x):src *)
1629 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1630 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1632 (* we fix the possible dependency problem in the source ty *)
1633 let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1634 let (bo, _), subst, metasenv, ugraph =
1635 coerce_to_something_aux
1636 bo ty ty2 subst metasenv context_src2 ugraph
1638 let coerced = Cic.Lambda (name_t,src2, bo) in
1639 (coerced, expty), subst, metasenv, ugraph (*}}}*)
1641 (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1642 ~metasenv subst infty context ^ " ==> " ^
1643 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1644 coerce_atom_to_something
1645 t infty expty subst metasenv context ugraph (*}}}*)
1647 debug_print (lazy ("COERCE TO SOMETHING END: "^
1648 CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1652 coerce_to_something_aux t infty expty subst metasenv context ugraph
1653 with Uncertain _ | RefineFailure _ as exn ->
1656 CicMetaSubst.ppterm_in_context metasenv subst t context ^
1657 " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1658 infty context ^ " but is here used with type " ^
1659 CicMetaSubst.ppterm_in_context metasenv subst expty context)
1661 enrich localization_tbl ~f t exn
1663 and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1664 match CicReduction.whd ~delta:false ~subst context infty with
1665 | Cic.Meta _ | Cic.Sort _ ->
1666 t,infty, subst, metasenv, ugraph
1668 debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1669 ~metasenv subst src context));
1670 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1672 let (t, ty_t), subst, metasenv, ugraph =
1673 coerce_to_something true
1674 localization_tbl t src tgt subst metasenv context ugraph
1676 debug_print (lazy ("COERCE TO SORT END: "^
1677 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1678 t, ty_t, subst, metasenv, ugraph
1679 with HExtlib.Localized (_, exn) ->
1681 lazy ("(7)The term " ^
1682 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1683 ^ " is not a type since it has type " ^
1684 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1685 ^ " that is not a sort")
1687 enrich localization_tbl ~f t exn
1690 (* eat prods ends here! *)
1692 let t',ty,subst',metasenv',ugraph1 =
1693 type_of_aux [] metasenv context t ugraph
1695 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1696 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1697 (* Andrea: ho rimesso qui l'applicazione della subst al
1698 metasenv dopo che ho droppato l'invariante che il metsaenv
1699 e' sempre istanziato *)
1700 let substituted_metasenv =
1701 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1703 (* substituted_t,substituted_ty,substituted_metasenv *)
1704 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1706 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1708 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1709 let cleaned_metasenv =
1711 (function (n,context,ty) ->
1712 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1717 | Some (n, Cic.Decl t) ->
1719 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1720 | Some (n, Cic.Def (bo,ty)) ->
1721 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1726 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1728 Some (n, Cic.Def (bo',ty'))
1732 ) substituted_metasenv
1734 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1737 let undebrujin uri typesno tys t =
1740 (fun (name,_,_,_) (i,t) ->
1741 (* here the explicit_named_substituion is assumed to be *)
1743 let t' = Cic.MutInd (uri,i,[]) in
1744 let t = CicSubstitution.subst t' t in
1746 ) tys (typesno - 1,t))
1748 let map_first_n n start f g l =
1749 let rec aux acc k l =
1752 | [] -> raise (Invalid_argument "map_first_n")
1753 | hd :: tl -> f hd k (aux acc (k+1) tl)
1759 (*CSC: this is a very rough approximation; to be finished *)
1760 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1761 let subst,metasenv,ugraph,tys =
1763 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1764 let subst,metasenv,ugraph,cl =
1766 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1767 let rec aux ctx k subst = function
1768 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1769 let subst,metasenv,ugraph,tl =
1771 (subst,metasenv,ugraph,[])
1772 (fun t n (subst,metasenv,ugraph,acc) ->
1773 let subst,metasenv,ugraph =
1775 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1777 subst,metasenv,ugraph,(t::acc))
1778 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1781 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1782 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1783 subst,metasenv,ugraph,t
1784 | Cic.Prod (name,s,t) ->
1785 let ctx = (Some (name,Cic.Decl s))::ctx in
1786 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1787 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1791 (lazy "not well formed constructor type"))
1793 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1794 subst,metasenv,ugraph,(name,ty) :: acc)
1795 cl (subst,metasenv,ugraph,[])
1797 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1798 tys ([],metasenv,ugraph,[])
1800 let substituted_tys =
1802 (fun (name,ind,arity,cl) ->
1804 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1806 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1809 metasenv,ugraph,substituted_tys
1811 let typecheck metasenv uri obj ~localization_tbl =
1812 let ugraph = CicUniv.empty_ugraph in
1814 Cic.Constant (name,Some bo,ty,args,attrs) ->
1815 let bo',boty,metasenv,ugraph =
1816 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1817 let ty',_,metasenv,ugraph =
1818 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1819 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1820 let bo' = CicMetaSubst.apply_subst subst bo' in
1821 let ty' = CicMetaSubst.apply_subst subst ty' in
1822 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1823 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1824 | Cic.Constant (name,None,ty,args,attrs) ->
1825 let ty',_,metasenv,ugraph =
1826 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1828 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1829 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1830 assert (metasenv' = metasenv);
1831 (* Here we do not check the metasenv for correctness *)
1832 let bo',boty,metasenv,ugraph =
1833 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1834 let ty',sort,metasenv,ugraph =
1835 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1839 (* instead of raising Uncertain, let's hope that the meta will become
1842 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1844 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1845 let bo' = CicMetaSubst.apply_subst subst bo' in
1846 let ty' = CicMetaSubst.apply_subst subst ty' in
1847 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1848 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1849 | Cic.Variable _ -> assert false (* not implemented *)
1850 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1851 (*CSC: this code is greately simplified and many many checks are missing *)
1852 (*CSC: e.g. the constructors are not required to build their own types, *)
1853 (*CSC: the arities are not required to have as type a sort, etc. *)
1854 let uri = match uri with Some uri -> uri | None -> assert false in
1855 let typesno = List.length tys in
1856 (* first phase: we fix only the types *)
1857 let metasenv,ugraph,tys =
1859 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1860 let ty',_,metasenv,ugraph =
1861 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1863 metasenv,ugraph,(name,b,ty',cl)::res
1864 ) tys (metasenv,ugraph,[]) in
1866 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1867 (* second phase: we fix only the constructors *)
1868 let saved_menv = metasenv in
1869 let metasenv,ugraph,tys =
1871 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1872 let metasenv,ugraph,cl' =
1874 (fun (name,ty) (metasenv,ugraph,res) ->
1876 CicTypeChecker.debrujin_constructor
1877 ~cb:(relocalize localization_tbl) uri typesno ty in
1878 let ty',_,metasenv,ugraph =
1879 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1880 let ty' = undebrujin uri typesno tys ty' in
1881 metasenv@saved_menv,ugraph,(name,ty')::res
1882 ) cl (metasenv,ugraph,[])
1884 metasenv,ugraph,(name,b,ty,cl')::res
1885 ) tys (metasenv,ugraph,[]) in
1886 (* third phase: we check the positivity condition *)
1887 let metasenv,ugraph,tys =
1888 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1890 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1893 (* sara' piu' veloce che raffinare da zero? mah.... *)
1894 let pack_coercion metasenv ctx t =
1895 let module C = Cic in
1896 let rec merge_coercions ctx =
1897 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1899 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1900 | C.Meta (n,subst) ->
1903 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1906 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1907 | C.Prod (name,so,dest) ->
1908 let ctx' = (Some (name,C.Decl so))::ctx in
1909 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1910 | C.Lambda (name,so,dest) ->
1911 let ctx' = (Some (name,C.Decl so))::ctx in
1912 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1913 | C.LetIn (name,so,dest) ->
1914 let _,ty,metasenv,ugraph =
1915 pack_coercions := false;
1916 type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1917 pack_coercions := true;
1918 let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1919 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1921 let l = List.map (merge_coercions ctx) l in
1923 let b,_,_,_,_ = is_a_double_coercion t in
1925 let ugraph = CicUniv.oblivion_ugraph in
1926 let old_insert_coercions = !insert_coercions in
1927 insert_coercions := false;
1928 let newt, _, menv, _ =
1930 type_of_aux' metasenv ctx t ugraph
1931 with RefineFailure _ | Uncertain _ ->
1934 insert_coercions := old_insert_coercions;
1935 if metasenv <> [] || menv = [] then
1938 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1941 | C.Var (uri,exp_named_subst) ->
1942 let exp_named_subst = List.map aux exp_named_subst in
1943 C.Var (uri, exp_named_subst)
1944 | C.Const (uri,exp_named_subst) ->
1945 let exp_named_subst = List.map aux exp_named_subst in
1946 C.Const (uri, exp_named_subst)
1947 | C.MutInd (uri,tyno,exp_named_subst) ->
1948 let exp_named_subst = List.map aux exp_named_subst in
1949 C.MutInd (uri,tyno,exp_named_subst)
1950 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1951 let exp_named_subst = List.map aux exp_named_subst in
1952 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1953 | C.MutCase (uri,tyno,out,te,pl) ->
1954 let pl = List.map (merge_coercions ctx) pl in
1955 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1956 | C.Fix (fno, fl) ->
1959 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1964 (fun (name,idx,ty,bo) ->
1965 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1969 | C.CoFix (fno, fl) ->
1972 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1977 (fun (name,ty,bo) ->
1978 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1983 merge_coercions ctx t
1986 let pack_coercion_metasenv conjectures =
1987 let module C = Cic in
1989 (fun (i, ctx, ty) ->
1995 Some (name, C.Decl t) ->
1996 Some (name, C.Decl (pack_coercion conjectures ctx t))
1997 | Some (name, C.Def (t,None)) ->
1998 Some (name,C.Def (pack_coercion conjectures ctx t,None))
1999 | Some (name, C.Def (t,Some ty)) ->
2000 Some (name, C.Def (pack_coercion conjectures ctx t,
2001 Some (pack_coercion conjectures ctx ty)))
2007 ((i,ctx,pack_coercion conjectures ctx ty))
2011 let pack_coercion_obj obj =
2012 let module C = Cic in
2014 | C.Constant (id, body, ty, params, attrs) ->
2018 | Some body -> Some (pack_coercion [] [] body)
2020 let ty = pack_coercion [] [] ty in
2021 C.Constant (id, body, ty, params, attrs)
2022 | C.Variable (name, body, ty, params, attrs) ->
2026 | Some body -> Some (pack_coercion [] [] body)
2028 let ty = pack_coercion [] [] ty in
2029 C.Variable (name, body, ty, params, attrs)
2030 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2031 let conjectures = pack_coercion_metasenv conjectures in
2032 let body = pack_coercion conjectures [] body in
2033 let ty = pack_coercion conjectures [] ty in
2034 C.CurrentProof (name, conjectures, body, ty, params, attrs)
2035 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2038 (fun (name, ind, arity, cl) ->
2039 let arity = pack_coercion [] [] arity in
2041 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2043 (name, ind, arity, cl))
2046 C.InductiveDefinition (indtys, params, leftno, attrs)
2051 let type_of_aux' metasenv context term =
2054 type_of_aux' metasenv context term in
2056 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2058 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2061 | RefineFailure msg as e ->
2062 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2064 | Uncertain msg as e ->
2065 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2069 let profiler2 = HExtlib.profile "CicRefine"
2071 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2072 profiler2.HExtlib.profile
2073 (type_of_aux' ?localization_tbl metasenv context term) ugraph
2075 let typecheck ~localization_tbl metasenv uri obj =
2076 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2078 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2079 (* vim:set foldmethod=marker: *)