1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
30 exception RefineFailure of string Lazy.t;;
31 exception Uncertain of string Lazy.t;;
32 exception AssertFailure of string Lazy.t;;
34 (* for internal use only; the integer is the number of surplus arguments *)
35 exception MoreArgsThanExpected of int * exn;;
37 let insert_coercions = ref true
38 let pack_coercions = ref true
43 if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());;
45 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
47 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
50 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
51 in profiler_eat_prods2.HExtlib.profile foo ()
53 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
54 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
57 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
59 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
62 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
63 in profiler_eat_prods.HExtlib.profile foo ()
65 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
66 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
69 let profiler = HExtlib.profile "CicRefine.fo_unif"
71 let fo_unif_subst subst context metasenv t1 t2 ugraph =
74 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
75 in profiler.HExtlib.profile foo ()
77 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
78 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
81 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
84 RefineFailure msg -> RefineFailure (f msg)
85 | Uncertain msg -> Uncertain (f msg)
86 | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
87 | Sys.Break -> raise exn
88 | _ -> prerr_endline (Printexc.to_string exn); assert false
92 Cic.CicHash.find localization_tbl t
94 HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
97 raise (HExtlib.Localized (loc,exn'))
99 let relocalize localization_tbl oldt newt =
101 let infos = Cic.CicHash.find localization_tbl oldt in
102 Cic.CicHash.remove localization_tbl oldt;
103 Cic.CicHash.add localization_tbl newt infos;
111 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
112 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
115 let exp_impl metasenv subst context =
118 let (metasenv', idx) =
119 CicMkImplicit.mk_implicit_type metasenv subst context in
121 CicMkImplicit.identity_relocation_list_for_metavariable context in
122 metasenv', Cic.Meta (idx, irl)
124 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
125 metasenv', Cic.Meta (idx, [])
127 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
129 CicMkImplicit.identity_relocation_list_for_metavariable context in
130 metasenv', Cic.Meta (idx, irl)
134 let is_a_double_coercion t =
136 let rec aux acc = function
138 | x::tl -> aux (acc@[x]) tl
143 let imp = Cic.Implicit None in
144 let dummyres = false,imp, imp,imp,imp in
146 | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
147 (match last_of tl with
148 | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
149 let sib2,head = last_of tl2 in
150 true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
155 let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
157 let len = List.length tlbody_and_type in
160 CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
161 " (that has type "^ CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
162 ") is here applied to " ^ string_of_int len ^
163 " arguments but here it can handle only up to " ^
164 string_of_int (len - residuals) ^ " arguments")
166 enrich localization_tbl he ~f:(fun _-> msg) exn
169 let mk_prod_of_metas metasenv context subst args =
170 let rec mk_prod metasenv context' = function
172 let (metasenv, idx) =
173 CicMkImplicit.mk_implicit_type metasenv subst context'
176 CicMkImplicit.identity_relocation_list_for_metavariable context'
178 metasenv,Cic.Meta (idx, irl)
180 let (metasenv, idx) =
181 CicMkImplicit.mk_implicit_type metasenv subst context'
184 CicMkImplicit.identity_relocation_list_for_metavariable context'
186 let meta = Cic.Meta (idx,irl) in
188 (* The name must be fresh for context. *)
189 (* Nevertheless, argty is well-typed only in context. *)
190 (* Thus I generate a name (name_hint) in context and *)
191 (* then I generate a name --- using the hint name_hint *)
192 (* --- that is fresh in context'. *)
194 FreshNamesGenerator.mk_fresh_name ~subst metasenv
195 (CicMetaSubst.apply_subst_context subst context)
197 ~typ:(CicMetaSubst.apply_subst subst argty)
199 FreshNamesGenerator.mk_fresh_name ~subst
200 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
202 let metasenv,target =
203 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
205 metasenv,Cic.Prod (name,meta,target)
207 mk_prod metasenv context args
210 let rec type_of_constant uri ugraph =
211 let module C = Cic in
212 let module R = CicReduction in
213 let module U = UriManager in
214 let _ = CicTypeChecker.typecheck uri in
217 CicEnvironment.get_cooked_obj ugraph uri
218 with Not_found -> assert false
221 C.Constant (_,_,ty,_,_) -> ty,u
222 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
226 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
228 and type_of_variable uri ugraph =
229 let module C = Cic in
230 let module R = CicReduction in
231 let module U = UriManager in
232 let _ = CicTypeChecker.typecheck uri in
235 CicEnvironment.get_cooked_obj ugraph uri
236 with Not_found -> assert false
239 C.Variable (_,_,ty,_,_) -> ty,u
243 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
245 and type_of_mutual_inductive_defs uri i ugraph =
246 let module C = Cic in
247 let module R = CicReduction in
248 let module U = UriManager in
249 let _ = CicTypeChecker.typecheck uri in
252 CicEnvironment.get_cooked_obj ugraph uri
253 with Not_found -> assert false
256 C.InductiveDefinition (dl,_,_,_) ->
257 let (_,_,arity,_) = List.nth dl i in
262 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
264 and type_of_mutual_inductive_constr uri i j ugraph =
265 let module C = Cic in
266 let module R = CicReduction in
267 let module U = UriManager in
268 let _ = CicTypeChecker.typecheck uri in
271 CicEnvironment.get_cooked_obj ugraph uri
272 with Not_found -> assert false
275 C.InductiveDefinition (dl,_,_,_) ->
276 let (_,_,_,cl) = List.nth dl i in
277 let (_,ty) = List.nth cl (j-1) in
283 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
286 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
288 (* the check_branch function checks if a branch of a case is refinable.
289 It returns a pair (outype_instance,args), a subst and a metasenv.
290 outype_instance is the expected result of applying the case outtype
292 The problem is that outype is in general unknown, and we should
293 try to synthesize it from the above information, that is in general
294 a second order unification problem. *)
296 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
297 let module C = Cic in
298 (* let module R = CicMetaSubst in *)
299 let module R = CicReduction in
300 match R.whd ~subst context expectedtype with
302 (n,context,actualtype, [term]), subst, metasenv, ugraph
303 | C.Appl (C.MutInd (_,_,_)::tl) ->
304 let (_,arguments) = split tl left_args_no in
305 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
306 | C.Prod (name,so,de) ->
307 (* we expect that the actual type of the branch has the due
309 (match R.whd ~subst context actualtype with
310 C.Prod (name',so',de') ->
311 let subst, metasenv, ugraph1 =
312 fo_unif_subst subst context metasenv so so' ugraph in
314 (match CicSubstitution.lift 1 term with
315 C.Appl l -> C.Appl (l@[C.Rel 1])
316 | t -> C.Appl [t ; C.Rel 1]) in
317 (* we should also check that the name variable is anonymous in
318 the actual type de' ?? *)
320 ((Some (name,(C.Decl so)))::context)
321 metasenv subst left_args_no de' term' de ugraph1
322 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
323 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
325 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
328 let rec type_of_aux subst metasenv context t ugraph =
329 let module C = Cic in
330 let module S = CicSubstitution in
331 let module U = UriManager in
332 let (t',_,_,_,_) as res =
337 match List.nth context (n - 1) with
338 Some (_,C.Decl ty) ->
339 t,S.lift n ty,subst,metasenv, ugraph
340 | Some (_,C.Def (_,Some ty)) ->
341 t,S.lift n ty,subst,metasenv, ugraph
342 | Some (_,C.Def (bo,None)) ->
344 (* if it is in the context it must be already well-typed*)
345 CicTypeChecker.type_of_aux' ~subst metasenv context
348 t,ty,subst,metasenv,ugraph
350 enrich localization_tbl t
351 (RefineFailure (lazy "Rel to hidden hypothesis"))
354 enrich localization_tbl t
355 (RefineFailure (lazy "Not a closed term")))
356 | C.Var (uri,exp_named_subst) ->
357 let exp_named_subst',subst',metasenv',ugraph1 =
358 check_exp_named_subst
359 subst metasenv context exp_named_subst ugraph
361 let ty_uri,ugraph1 = type_of_variable uri ugraph in
363 CicSubstitution.subst_vars exp_named_subst' ty_uri
365 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
368 let (canonical_context, term,ty) =
369 CicUtil.lookup_subst n subst
371 let l',subst',metasenv',ugraph1 =
372 check_metasenv_consistency n subst metasenv context
373 canonical_context l ugraph
375 (* trust or check ??? *)
376 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
377 subst', metasenv', ugraph1
378 (* type_of_aux subst metasenv
379 context (CicSubstitution.subst_meta l term) *)
380 with CicUtil.Subst_not_found _ ->
381 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
382 let l',subst',metasenv', ugraph1 =
383 check_metasenv_consistency n subst metasenv context
384 canonical_context l ugraph
386 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
387 subst', metasenv',ugraph1)
388 | C.Sort (C.Type tno) ->
389 let tno' = CicUniv.fresh() in
391 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
392 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
394 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
396 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
397 | C.Implicit infos ->
398 let metasenv',t' = exp_impl metasenv subst context infos in
399 type_of_aux subst metasenv' context t' ugraph
401 let ty',_,subst',metasenv',ugraph1 =
402 type_of_aux subst metasenv context ty ugraph
404 let te',inferredty,subst'',metasenv'',ugraph2 =
405 type_of_aux subst' metasenv' context te ugraph1
407 let (te', ty'), subst''',metasenv''',ugraph3 =
408 coerce_to_something true localization_tbl te' inferredty ty'
409 subst'' metasenv'' context ugraph2
411 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
412 | C.Prod (name,s,t) ->
413 let s',sort1,subst',metasenv',ugraph1 =
414 type_of_aux subst metasenv context s ugraph
416 let s',sort1,subst', metasenv',ugraph1 =
417 coerce_to_sort localization_tbl
418 s' sort1 subst' context metasenv' ugraph1
420 let context_for_t = ((Some (name,(C.Decl s')))::context) in
421 let t',sort2,subst'',metasenv'',ugraph2 =
422 type_of_aux subst' metasenv'
423 context_for_t t ugraph1
425 let t',sort2,subst'',metasenv'',ugraph2 =
426 coerce_to_sort localization_tbl
427 t' sort2 subst'' context_for_t metasenv'' ugraph2
429 let sop,subst''',metasenv''',ugraph3 =
430 sort_of_prod localization_tbl subst'' metasenv''
431 context (name,s') t' (sort1,sort2) ugraph2
433 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
434 | C.Lambda (n,s,t) ->
435 let s',sort1,subst',metasenv',ugraph1 =
436 type_of_aux subst metasenv context s ugraph
438 let s',sort1,subst',metasenv',ugraph1 =
439 coerce_to_sort localization_tbl
440 s' sort1 subst' context metasenv' ugraph1
442 let context_for_t = ((Some (n,(C.Decl s')))::context) in
443 let t',type2,subst'',metasenv'',ugraph2 =
444 type_of_aux subst' metasenv' context_for_t t ugraph1
446 C.Lambda (n,s',t'),C.Prod (n,s',type2),
447 subst'',metasenv'',ugraph2
449 (* only to check if s is well-typed *)
450 let s',ty,subst',metasenv',ugraph1 =
451 type_of_aux subst metasenv context s ugraph
453 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
455 let t',inferredty,subst'',metasenv'',ugraph2 =
456 type_of_aux subst' metasenv'
457 context_for_t t ugraph1
459 (* One-step LetIn reduction.
460 * Even faster than the previous solution.
461 * Moreover the inferred type is closer to the expected one.
464 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
465 subst'',metasenv'',ugraph2
466 | C.Appl (he::((_::_) as tl)) ->
467 let he',hetype,subst',metasenv',ugraph1 =
468 type_of_aux subst metasenv context he ugraph
470 let tlbody_and_type,subst'',metasenv'',ugraph2 =
471 typeof_list subst' metasenv' context ugraph1 tl
473 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
474 eat_prods true subst'' metasenv'' context
475 he' hetype tlbody_and_type ugraph2
477 let newappl = (C.Appl (coerced_he::coerced_args)) in
478 avoid_double_coercion
479 context subst''' metasenv''' ugraph3 newappl applty
480 | C.Appl _ -> assert false
481 | C.Const (uri,exp_named_subst) ->
482 let exp_named_subst',subst',metasenv',ugraph1 =
483 check_exp_named_subst subst metasenv context
484 exp_named_subst ugraph in
485 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
487 CicSubstitution.subst_vars exp_named_subst' ty_uri
489 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
490 | C.MutInd (uri,i,exp_named_subst) ->
491 let exp_named_subst',subst',metasenv',ugraph1 =
492 check_exp_named_subst subst metasenv context
493 exp_named_subst ugraph
495 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
497 CicSubstitution.subst_vars exp_named_subst' ty_uri in
498 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
499 | C.MutConstruct (uri,i,j,exp_named_subst) ->
500 let exp_named_subst',subst',metasenv',ugraph1 =
501 check_exp_named_subst subst metasenv context
502 exp_named_subst ugraph
505 type_of_mutual_inductive_constr uri i j ugraph1
508 CicSubstitution.subst_vars exp_named_subst' ty_uri
510 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
512 | C.MutCase (uri, i, outtype, term, pl) ->
513 (* first, get the inductive type (and noparams)
514 * in the environment *)
515 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
516 let _ = CicTypeChecker.typecheck uri in
517 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
519 C.InductiveDefinition (l,expl_params,parsno,_) ->
520 List.nth l i , expl_params, parsno, u
522 enrich localization_tbl t
524 (lazy ("Unkown mutual inductive definition " ^
525 U.string_of_uri uri)))
527 if List.length constructors <> List.length pl then
528 enrich localization_tbl t
530 (lazy "Wrong number of cases")) ;
531 let rec count_prod t =
532 match CicReduction.whd ~subst context t with
533 C.Prod (_, _, t) -> 1 + (count_prod t)
536 let no_args = count_prod arity in
537 (* now, create a "generic" MutInd *)
538 let metasenv,left_args =
539 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
541 let metasenv,right_args =
542 let no_right_params = no_args - no_left_params in
543 if no_right_params < 0 then assert false
544 else CicMkImplicit.n_fresh_metas
545 metasenv subst context no_right_params
547 let metasenv,exp_named_subst =
548 CicMkImplicit.fresh_subst metasenv subst context expl_params in
551 C.MutInd (uri,i,exp_named_subst)
554 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
556 (* check consistency with the actual type of term *)
557 let term',actual_type,subst,metasenv,ugraph1 =
558 type_of_aux subst metasenv context term ugraph in
559 let expected_type',_, subst, metasenv,ugraph2 =
560 type_of_aux subst metasenv context expected_type ugraph1
562 let actual_type = CicReduction.whd ~subst context actual_type in
563 let subst,metasenv,ugraph3 =
565 fo_unif_subst subst context metasenv
566 expected_type' actual_type ugraph2
569 enrich localization_tbl term' exn
572 CicMetaSubst.ppterm_in_context ~metasenv subst term'
573 context ^ " has type " ^
574 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
575 context ^ " but is here used with type " ^
576 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
578 let rec instantiate_prod t =
582 match CicReduction.whd ~subst context t with
584 instantiate_prod (CicSubstitution.subst he t') tl
587 let arity_instantiated_with_left_args =
588 instantiate_prod arity left_args in
589 (* TODO: check if the sort elimination
590 * is allowed: [(I q1 ... qr)|B] *)
591 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
593 (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
595 if left_args = [] then
596 (C.MutConstruct (uri,i,j,exp_named_subst))
599 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
601 let p',actual_type,subst,metasenv,ugraph1 =
602 type_of_aux subst metasenv context p ugraph
604 let constructor',expected_type, subst, metasenv,ugraph2 =
605 type_of_aux subst metasenv context constructor ugraph1
607 let outtypeinstance,subst,metasenv,ugraph3 =
609 check_branch 0 context metasenv subst
610 no_left_params actual_type constructor' expected_type
614 enrich localization_tbl constructor'
617 CicMetaSubst.ppterm_in_context metasenv subst p'
618 context ^ " has type " ^
619 CicMetaSubst.ppterm_in_context metasenv subst actual_type
620 context ^ " but is here used with type " ^
621 CicMetaSubst.ppterm_in_context metasenv subst expected_type
625 outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
626 pl ([],List.length pl,[],subst,metasenv,ugraph3)
629 (* we are left to check that the outype matches his instances.
630 The easy case is when the outype is specified, that amount
631 to a trivial check. Otherwise, we should guess a type from
635 let outtype,outtypety, subst, metasenv,ugraph4 =
636 type_of_aux subst metasenv context outtype ugraph4 in
639 (let candidate,ugraph5,metasenv,subst =
640 let exp_name_subst, metasenv =
642 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
644 let uris = CicUtil.params_of_obj o in
646 fun uri (acc,metasenv) ->
647 let metasenv',new_meta =
648 CicMkImplicit.mk_implicit metasenv subst context
651 CicMkImplicit.identity_relocation_list_for_metavariable
654 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
658 match left_args,right_args with
659 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
661 let rec mk_right_args =
664 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
666 let right_args_no = List.length right_args in
667 let lifted_left_args =
668 List.map (CicSubstitution.lift right_args_no) left_args
670 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
671 (lifted_left_args @ mk_right_args right_args_no))
674 FreshNamesGenerator.mk_fresh_name ~subst metasenv
675 context Cic.Anonymous ~typ:ty
677 match outtypeinstances with
679 let extended_context =
680 let rec add_right_args =
682 Cic.Prod (name,ty,t) ->
683 Some (name,Cic.Decl ty)::(add_right_args t)
686 (Some (fresh_name,Cic.Decl ty))::
688 (add_right_args arity_instantiated_with_left_args))@
691 let metasenv,new_meta =
692 CicMkImplicit.mk_implicit metasenv subst extended_context
695 CicMkImplicit.identity_relocation_list_for_metavariable
698 let rec add_lambdas b =
700 Cic.Prod (name,ty,t) ->
701 Cic.Lambda (name,ty,(add_lambdas b t))
702 | _ -> Cic.Lambda (fresh_name, ty, b)
705 add_lambdas (Cic.Meta (new_meta,irl))
706 arity_instantiated_with_left_args
708 (Some candidate),ugraph4,metasenv,subst
709 | (constructor_args_no,_,instance,_)::tl ->
711 let instance',subst,metasenv =
712 CicMetaSubst.delift_rels subst metasenv
713 constructor_args_no instance
715 let candidate,ugraph,metasenv,subst =
717 fun (candidate_oty,ugraph,metasenv,subst)
718 (constructor_args_no,_,instance,_) ->
719 match candidate_oty with
720 | None -> None,ugraph,metasenv,subst
723 let instance',subst,metasenv =
724 CicMetaSubst.delift_rels subst metasenv
725 constructor_args_no instance
727 let subst,metasenv,ugraph =
728 fo_unif_subst subst context metasenv
731 candidate_oty,ugraph,metasenv,subst
733 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
734 | RefineFailure _ | Uncertain _ ->
735 None,ugraph,metasenv,subst
736 ) (Some instance',ugraph4,metasenv,subst) tl
739 | None -> None, ugraph,metasenv,subst
741 let rec add_lambdas n b =
743 Cic.Prod (name,ty,t) ->
744 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
746 Cic.Lambda (fresh_name, ty,
747 CicSubstitution.lift (n + 1) t)
750 (add_lambdas 0 t arity_instantiated_with_left_args),
751 ugraph,metasenv,subst
752 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
753 None,ugraph4,metasenv,subst
756 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
758 let subst,metasenv,ugraph =
760 fo_unif_subst subst context metasenv
761 candidate outtype ugraph5
763 exn -> assert false(* unification against a metavariable *)
765 C.MutCase (uri, i, outtype, term', pl'),
766 CicReduction.head_beta_reduce
767 (CicMetaSubst.apply_subst subst
768 (Cic.Appl (outtype::right_args@[term']))),
769 subst,metasenv,ugraph)
770 | _ -> (* easy case *)
771 let tlbody_and_type,subst,metasenv,ugraph4 =
772 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
774 let _,_,_,subst,metasenv,ugraph4 =
775 eat_prods false subst metasenv context
776 outtype outtypety tlbody_and_type ugraph4
778 let _,_, subst, metasenv,ugraph5 =
779 type_of_aux subst metasenv context
780 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
782 let (subst,metasenv,ugraph6) =
784 (fun (subst,metasenv,ugraph)
785 p (constructor_args_no,context,instance,args)
790 CicSubstitution.lift constructor_args_no outtype
792 C.Appl (outtype'::args)
794 CicReduction.whd ~subst context appl
797 fo_unif_subst subst context metasenv instance instance'
801 enrich localization_tbl p exn
804 CicMetaSubst.ppterm_in_context ~metasenv subst p
805 context ^ " has type " ^
806 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
807 context ^ " but is here used with type " ^
808 CicMetaSubst.ppterm_in_context ~metasenv subst instance
810 (subst,metasenv,ugraph5) pl' outtypeinstances
812 C.MutCase (uri, i, outtype, term', pl'),
813 CicReduction.head_beta_reduce
814 (CicMetaSubst.apply_subst subst
815 (C.Appl(outtype::right_args@[term]))),
816 subst,metasenv,ugraph6)
818 let fl_ty',subst,metasenv,types,ugraph1,len =
820 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
821 let ty',_,subst',metasenv',ugraph1 =
822 type_of_aux subst metasenv context ty ugraph
824 fl @ [ty'],subst',metasenv',
825 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
826 :: types, ugraph, len+1
827 ) ([],subst,metasenv,[],ugraph,0) fl
829 let context' = types@context in
830 let fl_bo',subst,metasenv,ugraph2 =
832 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
833 let bo',ty_of_bo,subst,metasenv,ugraph1 =
834 type_of_aux subst metasenv context' bo ugraph in
835 let expected_ty = CicSubstitution.lift len ty in
836 let subst',metasenv',ugraph' =
838 fo_unif_subst subst context' metasenv
839 ty_of_bo expected_ty ugraph1
842 enrich localization_tbl bo exn
845 CicMetaSubst.ppterm_in_context ~metasenv subst bo
846 context' ^ " has type " ^
847 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
848 context' ^ " but is here used with type " ^
849 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
852 fl @ [bo'] , subst',metasenv',ugraph'
853 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
855 let ty = List.nth fl_ty' i in
856 (* now we have the new ty in fl_ty', the new bo in fl_bo',
857 * and we want the new fl with bo' and ty' injected in the right
860 let rec map3 f l1 l2 l3 =
863 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
866 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
869 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
871 let fl_ty',subst,metasenv,types,ugraph1,len =
873 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
874 let ty',_,subst',metasenv',ugraph1 =
875 type_of_aux subst metasenv context ty ugraph
877 fl @ [ty'],subst',metasenv',
878 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
879 types, ugraph1, len+1
880 ) ([],subst,metasenv,[],ugraph,0) fl
882 let context' = types@context in
883 let fl_bo',subst,metasenv,ugraph2 =
885 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
886 let bo',ty_of_bo,subst,metasenv,ugraph1 =
887 type_of_aux subst metasenv context' bo ugraph in
888 let expected_ty = CicSubstitution.lift len ty in
889 let subst',metasenv',ugraph' =
891 fo_unif_subst subst context' metasenv
892 ty_of_bo expected_ty ugraph1
895 enrich localization_tbl bo exn
898 CicMetaSubst.ppterm_in_context ~metasenv subst bo
899 context' ^ " has type " ^
900 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
901 context' ^ " but is here used with type " ^
902 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
905 fl @ [bo'],subst',metasenv',ugraph'
906 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
908 let ty = List.nth fl_ty' i in
909 (* now we have the new ty in fl_ty', the new bo in fl_bo',
910 * and we want the new fl with bo' and ty' injected in the right
913 let rec map3 f l1 l2 l3 =
916 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
919 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
922 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
924 relocalize localization_tbl t t';
927 (* check_metasenv_consistency checks that the "canonical" context of a
928 metavariable is consitent - up to relocation via the relocation list l -
929 with the actual context *)
930 and check_metasenv_consistency
931 metano subst metasenv context canonical_context l ugraph
933 let module C = Cic in
934 let module R = CicReduction in
935 let module S = CicSubstitution in
936 let lifted_canonical_context =
940 | (Some (n,C.Decl t))::tl ->
941 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
942 | (Some (n,C.Def (t,None)))::tl ->
943 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
944 | None::tl -> None::(aux (i+1) tl)
945 | (Some (n,C.Def (t,Some ty)))::tl ->
947 C.Def ((S.subst_meta l (S.lift i t)),
948 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
950 aux 1 canonical_context
954 (fun (l,subst,metasenv,ugraph) t ct ->
957 l @ [None],subst,metasenv,ugraph
958 | Some t,Some (_,C.Def (ct,_)) ->
959 (*CSC: the following optimization is to avoid a possibly
960 expensive reduction that can be easily avoided and
961 that is quite frequent. However, this is better
962 handled using levels to control reduction *)
967 match List.nth context (n - 1) with
968 Some (_,C.Def (te,_)) -> S.lift n te
974 let subst',metasenv',ugraph' =
976 (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
977 * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
978 fo_unif_subst subst context metasenv optimized_t ct ugraph
979 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 optimized_t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
981 l @ [Some t],subst',metasenv',ugraph'
982 | Some t,Some (_,C.Decl ct) ->
983 let t',inferredty,subst',metasenv',ugraph1 =
984 type_of_aux subst metasenv context t ugraph
986 let subst'',metasenv'',ugraph2 =
989 subst' context metasenv' inferredty ct ugraph1
990 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))))))
992 l @ [Some t'], subst'',metasenv'',ugraph2
994 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
996 Invalid_argument _ ->
1000 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1001 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1002 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1004 and check_exp_named_subst metasubst metasenv context tl ugraph =
1005 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1007 [] -> [],metasubst,metasenv,ugraph
1009 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1011 CicSubstitution.subst_vars substs ty_uri in
1012 (* CSC: why was this code here? it is wrong
1013 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1014 Cic.Variable (_,Some bo,_,_) ->
1016 (RefineFailure (lazy
1017 "A variable with a body can not be explicit substituted"))
1018 | Cic.Variable (_,None,_,_) -> ()
1021 (RefineFailure (lazy
1022 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1025 let t',typeoft,metasubst',metasenv',ugraph2 =
1026 type_of_aux metasubst metasenv context t ugraph1 in
1027 let subst = uri,t' in
1028 let metasubst'',metasenv'',ugraph3 =
1031 metasubst' context metasenv' typeoft typeofvar ugraph2
1033 raise (RefineFailure (lazy
1034 ("Wrong Explicit Named Substitution: " ^
1035 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1036 " not unifiable with " ^
1037 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1039 (* FIXME: no mere tail recursive! *)
1040 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1041 check_exp_named_subst_aux
1042 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1044 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1046 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1049 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1052 let module C = Cic in
1053 let context_for_t2 = (Some (name,C.Decl s))::context in
1054 let t1'' = CicReduction.whd ~subst context t1 in
1055 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1056 match (t1'', t2'') with
1057 (C.Sort s1, C.Sort s2)
1058 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1059 (* different than Coq manual!!! *)
1060 C.Sort s2,subst,metasenv,ugraph
1061 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1062 let t' = CicUniv.fresh() in
1064 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1065 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1066 C.Sort (C.Type t'),subst,metasenv,ugraph2
1068 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1069 | (C.Sort _,C.Sort (C.Type t1)) ->
1070 C.Sort (C.Type t1),subst,metasenv,ugraph
1071 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1072 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1073 (* TODO how can we force the meta to become a sort? If we don't we
1074 * break the invariant that refine produce only well typed terms *)
1075 (* TODO if we check the non meta term and if it is a sort then we
1076 * are likely to know the exact value of the result e.g. if the rhs
1077 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1078 let (metasenv,idx) =
1079 CicMkImplicit.mk_implicit_sort metasenv subst in
1080 let (subst, metasenv,ugraph1) =
1082 fo_unif_subst subst context_for_t2 metasenv
1083 (C.Meta (idx,[])) t2'' ugraph
1084 with _ -> assert false (* unification against a metavariable *)
1086 t2'',subst,metasenv,ugraph1
1089 enrich localization_tbl s
1093 "%s is supposed to be a type, but its type is %s"
1094 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1095 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1097 enrich localization_tbl t
1101 "%s is supposed to be a type, but its type is %s"
1102 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1103 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1105 and avoid_double_coercion context subst metasenv ugraph t ty =
1106 if not !pack_coercions then
1107 t,ty,subst,metasenv,ugraph
1109 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1111 let source_carr = CoercGraph.source_of c2 in
1112 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1113 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1115 | CoercGraph.SomeCoercion candidates ->
1117 HExtlib.list_findopt
1118 (function (metasenv,last,c) ->
1120 | c when not (CoercGraph.is_composite c) ->
1121 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1124 let subst,metasenv,ugraph =
1125 fo_unif_subst subst context metasenv last head ugraph in
1126 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1131 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1132 let newt,_,subst,metasenv,ugraph =
1133 type_of_aux subst metasenv context c ugraph in
1134 debug_print (lazy "tipa...");
1135 let subst, metasenv, ugraph =
1136 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1137 fo_unif_subst subst context metasenv newt t ugraph
1139 debug_print (lazy "unifica...");
1140 Some (newt, ty, subst, metasenv, ugraph)
1142 | RefineFailure s | Uncertain s when not !pack_coercions->
1143 debug_print s; debug_print (lazy "stop\n");None
1144 | RefineFailure s | Uncertain s ->
1145 debug_print s;debug_print (lazy "goon\n");
1147 let old_pack_coercions = !pack_coercions in
1148 pack_coercions := false; (* to avoid diverging *)
1149 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1150 type_of_aux subst metasenv context c1_c2_implicit ugraph
1152 pack_coercions := old_pack_coercions;
1154 is_a_double_coercion refined_c1_c2_implicit
1160 match refined_c1_c2_implicit with
1161 | Cic.Appl l -> HExtlib.list_last l
1164 let subst, metasenv, ugraph =
1165 try fo_unif_subst subst context metasenv
1167 with RefineFailure s| Uncertain s->
1168 debug_print s;assert false
1170 let subst, metasenv, ugraph =
1171 fo_unif_subst subst context metasenv
1172 refined_c1_c2_implicit t ugraph
1174 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1176 | RefineFailure s | Uncertain s ->
1177 pack_coercions := true;debug_print s;None
1178 | exn -> pack_coercions := true; raise exn))
1181 (match selected with
1185 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1186 t, ty, subst, metasenv, ugraph)
1187 | _ -> t, ty, subst, metasenv, ugraph)
1189 t, ty, subst, metasenv, ugraph
1191 and typeof_list subst metasenv context ugraph l =
1192 let tlbody_and_type,subst,metasenv,ugraph =
1194 (fun x (res,subst,metasenv,ugraph) ->
1195 let x',ty,subst',metasenv',ugraph1 =
1196 type_of_aux subst metasenv context x ugraph
1198 (x', ty)::res,subst',metasenv',ugraph1
1199 ) l ([],subst,metasenv,ugraph)
1201 tlbody_and_type,subst,metasenv,ugraph
1204 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1206 (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1207 let fix_arity n metasenv context subst he hetype ugraph =
1208 let hetype = CicMetaSubst.apply_subst subst hetype in
1209 let src = CoercDb.coerc_carr_of_term hetype in
1210 let tgt = CoercDb.Fun 0 in
1211 match CoercGraph.look_for_coercion' metasenv subst context src tgt with
1212 | CoercGraph.NoCoercion -> []
1213 | CoercGraph.NotMetaClosed
1214 | CoercGraph.NotHandled _ ->
1215 raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1216 | CoercGraph.SomeCoercionToTgt candidates
1217 | CoercGraph.SomeCoercion candidates ->
1219 (fun (metasenv,last,coerc) ->
1221 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1223 let subst,metasenv,ugraph =
1224 fo_unif_subst subst context metasenv last he ugraph in
1225 debug_print (lazy ("New head: "^ pp coerc));
1227 CicTypeChecker.type_of_aux' ~subst metasenv context coerc
1230 debug_print (lazy (" has type: "^ pp tty));
1231 Some (coerc,tty,subst,metasenv,ugraph)
1233 | Uncertain _ | RefineFailure _
1234 | HExtlib.Localized (_,Uncertain _)
1235 | HExtlib.Localized (_,RefineFailure _) -> None
1236 | exn -> assert false)
1239 (* aux function to process the type of the head and the args in parallel *)
1240 let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1242 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1243 | (hete, hety)::tl as args ->
1244 match (CicReduction.whd ~subst context hetype) with
1245 | Cic.Prod (n,s,t) ->
1246 let arg,subst,metasenv,ugraph =
1247 coerce_to_something allow_coercions localization_tbl
1248 hete hety s subst metasenv context ugraph in
1250 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1251 ugraph (newargs@[arg]) tl
1254 match he, newargs with
1256 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1257 | _ -> Cic.Appl (he::List.map fst newargs)
1259 (*{{{*) debug_print (lazy
1261 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1262 "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1263 "\n but is applyed to: " ^ String.concat ";"
1264 (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1265 let possible_fixes =
1266 fix_arity (List.length args) metasenv context subst he hetype
1269 HExtlib.list_findopt
1270 (fun (he,hetype,subst,metasenv,ugraph) ->
1271 (* {{{ *)debug_print (lazy ("Try fix: "^
1272 CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1273 debug_print (lazy (" of type: "^
1274 CicMetaSubst.ppterm_in_context
1275 ~metasenv subst hetype context)); (* }}} *)
1277 Some (eat_prods_and_args
1278 metasenv subst context he hetype ugraph [] args)
1280 | RefineFailure _ | Uncertain _
1281 | HExtlib.Localized (_,RefineFailure _)
1282 | HExtlib.Localized (_,Uncertain _) -> None)
1288 (MoreArgsThanExpected
1289 (List.length args, RefineFailure (lazy "")))
1291 (* first we check if we are in the simple case of a meta closed term *)
1292 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1293 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1294 (* this optimization is to postpone fix_arity (the most common case)*)
1295 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1297 (* this (says CSC) is also useful to infer dependent types *)
1298 let pristinemenv = metasenv in
1299 let metasenv,hetype' =
1300 mk_prod_of_metas metasenv context subst args_bo_and_ty
1303 let subst,metasenv,ugraph =
1304 fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1306 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1307 with RefineFailure _ | Uncertain _ ->
1308 subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1310 let coerced_args,subst,metasenv,he,t,ugraph =
1313 metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1315 MoreArgsThanExpected (residuals,exn) ->
1316 more_args_than_expected localization_tbl metasenv
1317 subst he context hetype' residuals args_bo_and_ty exn
1319 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1321 and coerce_to_something
1322 allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1324 let module CS = CicSubstitution in
1325 let module CR = CicReduction in
1326 let cs_subst = CS.subst ~avoid_beta_redexes:true in
1327 let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1328 debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1330 CoercGraph.look_for_coercion metasenv subst context infty expty
1333 | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
1334 "coerce_atom_to_something fails since not meta closed"))
1335 | CoercGraph.NoCoercion
1336 | CoercGraph.SomeCoercionToTgt _
1337 | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
1338 "coerce_atom_to_something fails since no coercions found"))
1339 | CoercGraph.SomeCoercion candidates ->
1340 debug_print (lazy (string_of_int (List.length candidates) ^
1341 " candidates found"));
1342 let uncertain = ref false in
1346 (fun (metasenv,last,c) ->
1348 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1349 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1351 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
1352 "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
1354 debug_print (lazy ("FO_UNIF_SUBST: " ^
1355 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1356 let subst,metasenv,ugraph =
1357 fo_unif_subst subst context metasenv last t ugraph
1359 let newt,newhety,subst,metasenv,ugraph =
1360 type_of_aux subst metasenv context c ugraph in
1361 let newt, newty, subst, metasenv, ugraph =
1362 avoid_double_coercion context subst metasenv ugraph newt expty
1364 let subst,metasenv,ugraph =
1365 fo_unif_subst subst context metasenv newhety expty ugraph in
1366 Some ((newt,newty), subst, metasenv, ugraph)
1368 | Uncertain _ -> uncertain := true; None
1369 | RefineFailure _ -> None)
1374 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1382 | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1383 | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1385 let rec coerce_to_something_aux
1386 t infty expty subst metasenv context ugraph
1389 let subst, metasenv, ugraph =
1390 fo_unif_subst subst context metasenv infty expty ugraph
1392 (t, expty), subst, metasenv, ugraph
1393 with (Uncertain _ | RefineFailure _ as exn)
1394 when allow_coercions && !insert_coercions ->
1395 let whd = CicReduction.whd ~delta:false in
1396 let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1397 let infty = clean infty subst context in
1398 let expty = clean expty subst context in
1399 let t = clean t subst context in
1400 (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1401 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1402 CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1403 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1404 let (coerced,_),subst,metasenv,_ as result =
1405 match infty, expty, t with
1406 | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1407 (*{{{*) debug_print (lazy "FIX");
1409 [name,i,_(* infty *),bo] ->
1411 Some (Cic.Name name,Cic.Decl expty)::context in
1412 let (rel1, _), subst, metasenv, ugraph =
1413 coerce_to_something_aux (Cic.Rel 1)
1414 (CS.lift 1 expty) (CS.lift 1 infty) subst
1415 metasenv context_bo ugraph in
1416 let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1417 let (bo,_), subst, metasenv, ugraph =
1418 coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1420 metasenv context_bo ugraph
1422 (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1423 | _ -> assert false (* not implemented yet *)) (*}}}*)
1424 | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1425 (*{{{*) debug_print (lazy "CASE");
1426 (* {{{ helper functions *)
1427 let get_cl_and_left_p uri tyno outty ugraph =
1428 match CicEnvironment.get_obj ugraph uri with
1429 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1432 match CicReduction.whd ~delta:false ctx t with
1433 | Cic.Prod (name,src,tgt) ->
1434 let ctx = Some (name, Cic.Decl src) :: ctx in
1440 let rec skip_lambda_delifting t n =
1443 | Cic.Lambda (_,_,t),n ->
1444 skip_lambda_delifting
1445 (CS.subst (Cic.Implicit None) t) (n - 1)
1448 let get_l_r_p n = function
1449 | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1450 | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1451 HExtlib.split_nth n args
1454 let _, _, ty, cl = List.nth tl tyno in
1455 let pis = count_pis ty in
1456 let rno = pis - leftno in
1457 let t = skip_lambda_delifting outty rno in
1458 let left_p, _ = get_l_r_p leftno t in
1459 let instantiale_with_left cl =
1463 (fun t p -> match t with
1464 | Cic.Prod (_,_,t) ->
1470 let cl = instantiale_with_left (List.map snd cl) in
1471 cl, left_p, leftno, rno, ugraph
1474 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1477 let rec mkr n = function
1478 | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1481 CicReplace.replace_lifting
1482 ~equality:(fun _ -> CicUtil.alpha_equivalence)
1484 ~what:(matched::right_p)
1485 ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1489 | Cic.Lambda (name, src, tgt),_ ->
1490 Cic.Lambda (name, src,
1491 keep_lambdas_and_put_expty
1492 (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1493 (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1496 let eq_uri, eq, eq_refl =
1497 match LibraryObjects.eq_URI () with
1498 | None -> HLog.warn "no default equality"; raise exn
1499 | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1502 metasenv subst context uri tyno cty outty mty m leftno i
1504 let rec aux context outty par k mty m = function
1505 | Cic.Prod (name, src, tgt) ->
1508 (Some (name, Cic.Decl src) :: context)
1509 (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1510 (CS.lift 1 mty) (CS.lift 1 m) tgt
1512 Cic.Prod (name, src, t), k
1515 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1516 if par <> [] then Cic.Appl (k::par) else k
1518 Cic.Prod (Cic.Name "p",
1519 Cic.Appl [eq; mty; m; k],
1521 (CR.head_beta_reduce ~delta:false
1522 (Cic.Appl [outty;k])))),k
1523 | Cic.Appl (Cic.MutInd _::pl) ->
1524 let left_p,right_p = HExtlib.split_nth leftno pl in
1525 let has_rights = right_p <> [] in
1527 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1528 Cic.Appl (k::left_p@par)
1532 CicTypeChecker.type_of_aux' ~subst metasenv context k
1533 CicUniv.oblivion_ugraph
1535 | Cic.Appl (Cic.MutInd _::args),_ ->
1536 snd (HExtlib.split_nth leftno args)
1538 with CicTypeChecker.TypeCheckerFailure _-> assert false
1541 CR.head_beta_reduce ~delta:false
1542 (Cic.Appl (outty ::right_p @ [k])),k
1544 Cic.Prod (Cic.Name "p",
1545 Cic.Appl [eq; mty; m; k],
1547 (CR.head_beta_reduce ~delta:false
1548 (Cic.Appl (outty ::right_p @ [k]))))),k
1551 aux context outty [] 1 mty m cty
1553 let add_lambda_for_refl_m pbo rno mty m k cty =
1554 (* k lives in the right context *)
1555 if rno <> 0 then pbo else
1556 let rec aux mty m = function
1557 | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1558 Cic.Lambda (name,src,
1559 (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1561 Cic.Lambda (Cic.Name "p",
1562 Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1566 let add_pi_for_refl_m new_outty mty m rno =
1567 if rno <> 0 then new_outty else
1568 let rec aux m mty = function
1569 | Cic.Lambda (name, src, tgt) ->
1570 Cic.Lambda (name, src,
1571 aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1574 (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1578 in (* }}} end helper functions *)
1579 (* constructors types with left params already instantiated *)
1580 let outty = CicMetaSubst.apply_subst subst outty in
1581 let cl, left_p, leftno,rno,ugraph =
1582 get_cl_and_left_p uri tyno outty ugraph
1587 CicTypeChecker.type_of_aux' ~subst metasenv context m
1588 CicUniv.oblivion_ugraph
1590 | Cic.MutInd _ as mty,_ -> [], mty
1591 | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
1592 snd (HExtlib.split_nth leftno args), mty
1594 with CicTypeChecker.TypeCheckerFailure _ -> assert false
1597 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1600 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1601 ~metasenv subst new_outty context));
1602 let _,pl,subst,metasenv,ugraph =
1604 (fun cty pbo (i, acc, s, menv, ugraph) ->
1605 (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1606 * (new_)outty right_par (K_i left_par k_par) *)
1608 add_params menv s context uri tyno
1609 cty outty mty m leftno i in
1611 (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1612 ~metasenv subst infty_pbo context));
1613 let expty_pbo, k = (* k is (K_i left_par k_par) *)
1614 add_params menv s context uri tyno
1615 cty new_outty mty m leftno i in
1617 (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1618 ~metasenv subst expty_pbo context));
1619 let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1621 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1622 ~metasenv subst pbo context));
1623 let (pbo, _), subst, metasenv, ugraph =
1624 coerce_to_something_aux pbo infty_pbo expty_pbo
1625 s menv context ugraph
1628 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1629 ~metasenv subst pbo context));
1630 (i-1, pbo::acc, subst, metasenv, ugraph))
1631 cl pl (List.length pl, [], subst, metasenv, ugraph)
1633 let new_outty = add_pi_for_refl_m new_outty mty m rno in
1635 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1636 ~metasenv subst new_outty context));
1639 let refl_m=Cic.Appl[eq_refl;mty;m]in
1640 Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1642 Cic.MutCase(uri,tyno,new_outty,m,pl)
1644 (t, expty), subst, metasenv, ugraph (*}}}*)
1645 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1646 (*{{{*) debug_print (lazy "LAM");
1648 FreshNamesGenerator.mk_fresh_name
1649 ~subst metasenv context ~typ:src2 Cic.Anonymous
1651 let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1652 (* contravariant part: the argument of f:src->ty *)
1653 let (rel1, _), subst, metasenv, ugraph =
1654 coerce_to_something_aux
1655 (Cic.Rel 1) (CS.lift 1 src2)
1656 (CS.lift 1 src) subst metasenv context_src2 ugraph
1658 (* covariant part: the result of f(c x); x:src2; (c x):src *)
1661 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1662 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1664 (* we fix the possible dependency problem in the source ty *)
1665 let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1666 let (bo, _), subst, metasenv, ugraph =
1667 coerce_to_something_aux
1668 bo ty ty2 subst metasenv context_src2 ugraph
1670 let coerced = Cic.Lambda (name_t,src2, bo) in
1671 (coerced, expty), subst, metasenv, ugraph (*}}}*)
1673 (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1674 ~metasenv subst infty context ^ " ==> " ^
1675 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1676 coerce_atom_to_something
1677 t infty expty subst metasenv context ugraph (*}}}*)
1679 debug_print (lazy ("COERCE TO SOMETHING END: "^
1680 CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1684 coerce_to_something_aux t infty expty subst metasenv context ugraph
1685 with Uncertain _ | RefineFailure _ as exn ->
1688 CicMetaSubst.ppterm_in_context metasenv subst t context ^
1689 " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1690 infty context ^ " but is here used with type " ^
1691 CicMetaSubst.ppterm_in_context metasenv subst expty context)
1693 enrich localization_tbl ~f t exn
1695 and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1696 match CicReduction.whd ~delta:false ~subst context infty with
1697 | Cic.Meta _ | Cic.Sort _ ->
1698 t,infty, subst, metasenv, ugraph
1700 debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1701 ~metasenv subst src context));
1702 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1704 let (t, ty_t), subst, metasenv, ugraph =
1705 coerce_to_something true
1706 localization_tbl t src tgt subst metasenv context ugraph
1708 debug_print (lazy ("COERCE TO SORT END: "^
1709 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1710 t, ty_t, subst, metasenv, ugraph
1711 with HExtlib.Localized (_, exn) ->
1713 lazy ("(7)The term " ^
1714 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1715 ^ " is not a type since it has type " ^
1716 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1717 ^ " that is not a sort")
1719 enrich localization_tbl ~f t exn
1722 (* eat prods ends here! *)
1724 let t',ty,subst',metasenv',ugraph1 =
1725 type_of_aux [] metasenv context t ugraph
1727 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1728 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1729 (* Andrea: ho rimesso qui l'applicazione della subst al
1730 metasenv dopo che ho droppato l'invariante che il metsaenv
1731 e' sempre istanziato *)
1732 let substituted_metasenv =
1733 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1735 (* substituted_t,substituted_ty,substituted_metasenv *)
1736 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1738 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1740 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1741 let cleaned_metasenv =
1743 (function (n,context,ty) ->
1744 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1749 | Some (n, Cic.Decl t) ->
1751 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1752 | Some (n, Cic.Def (bo,ty)) ->
1753 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1758 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1760 Some (n, Cic.Def (bo',ty'))
1764 ) substituted_metasenv
1766 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1769 let undebrujin uri typesno tys t =
1772 (fun (name,_,_,_) (i,t) ->
1773 (* here the explicit_named_substituion is assumed to be *)
1775 let t' = Cic.MutInd (uri,i,[]) in
1776 let t = CicSubstitution.subst t' t in
1778 ) tys (typesno - 1,t))
1780 let map_first_n n start f g l =
1781 let rec aux acc k l =
1784 | [] -> raise (Invalid_argument "map_first_n")
1785 | hd :: tl -> f hd k (aux acc (k+1) tl)
1791 (*CSC: this is a very rough approximation; to be finished *)
1792 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1793 let subst,metasenv,ugraph,tys =
1795 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1796 let subst,metasenv,ugraph,cl =
1798 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1799 let rec aux ctx k subst = function
1800 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1801 let subst,metasenv,ugraph,tl =
1803 (subst,metasenv,ugraph,[])
1804 (fun t n (subst,metasenv,ugraph,acc) ->
1805 let subst,metasenv,ugraph =
1807 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1809 subst,metasenv,ugraph,(t::acc))
1810 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1813 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1814 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1815 subst,metasenv,ugraph,t
1816 | Cic.Prod (name,s,t) ->
1817 let ctx = (Some (name,Cic.Decl s))::ctx in
1818 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1819 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1823 (lazy "not well formed constructor type"))
1825 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1826 subst,metasenv,ugraph,(name,ty) :: acc)
1827 cl (subst,metasenv,ugraph,[])
1829 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1830 tys ([],metasenv,ugraph,[])
1832 let substituted_tys =
1834 (fun (name,ind,arity,cl) ->
1836 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1838 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1841 metasenv,ugraph,substituted_tys
1843 let typecheck metasenv uri obj ~localization_tbl =
1844 let ugraph = CicUniv.empty_ugraph in
1846 Cic.Constant (name,Some bo,ty,args,attrs) ->
1847 (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
1848 since type_of_aux' destroys localization information (which are
1849 preserved by type_of_aux *)
1852 Cic.CicHash.find localization_tbl bo
1854 HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
1856 let bo',boty,metasenv,ugraph =
1857 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1858 let ty',_,metasenv,ugraph =
1859 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1860 let subst,metasenv,ugraph =
1862 fo_unif_subst [] [] metasenv boty ty' ugraph
1865 | Uncertain _ as exn ->
1868 CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
1870 CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
1871 " but is here used with type " ^
1872 CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
1876 RefineFailure _ -> RefineFailure msg
1877 | Uncertain _ -> Uncertain msg
1880 raise (HExtlib.Localized (loc exn',exn'))
1882 let bo' = CicMetaSubst.apply_subst subst bo' in
1883 let ty' = CicMetaSubst.apply_subst subst ty' in
1884 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1885 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1886 | Cic.Constant (name,None,ty,args,attrs) ->
1887 let ty',_,metasenv,ugraph =
1888 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1890 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1891 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1892 assert (metasenv' = metasenv);
1893 (* Here we do not check the metasenv for correctness *)
1894 let bo',boty,metasenv,ugraph =
1895 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1896 let ty',sort,metasenv,ugraph =
1897 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1901 (* instead of raising Uncertain, let's hope that the meta will become
1904 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1906 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1907 let bo' = CicMetaSubst.apply_subst subst bo' in
1908 let ty' = CicMetaSubst.apply_subst subst ty' in
1909 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1910 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1911 | Cic.Variable _ -> assert false (* not implemented *)
1912 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1913 (*CSC: this code is greately simplified and many many checks are missing *)
1914 (*CSC: e.g. the constructors are not required to build their own types, *)
1915 (*CSC: the arities are not required to have as type a sort, etc. *)
1916 let uri = match uri with Some uri -> uri | None -> assert false in
1917 let typesno = List.length tys in
1918 (* first phase: we fix only the types *)
1919 let metasenv,ugraph,tys =
1921 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1922 let ty',_,metasenv,ugraph =
1923 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1925 metasenv,ugraph,(name,b,ty',cl)::res
1926 ) tys (metasenv,ugraph,[]) in
1928 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1929 (* second phase: we fix only the constructors *)
1930 let saved_menv = metasenv in
1931 let metasenv,ugraph,tys =
1933 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1934 let metasenv,ugraph,cl' =
1936 (fun (name,ty) (metasenv,ugraph,res) ->
1938 CicTypeChecker.debrujin_constructor
1939 ~cb:(relocalize localization_tbl) uri typesno ty in
1940 let ty',_,metasenv,ugraph =
1941 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1942 let ty' = undebrujin uri typesno tys ty' in
1943 metasenv@saved_menv,ugraph,(name,ty')::res
1944 ) cl (metasenv,ugraph,[])
1946 metasenv,ugraph,(name,b,ty,cl')::res
1947 ) tys (metasenv,ugraph,[]) in
1948 (* third phase: we check the positivity condition *)
1949 let metasenv,ugraph,tys =
1950 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1952 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1955 (* sara' piu' veloce che raffinare da zero? mah.... *)
1956 let pack_coercion metasenv ctx t =
1957 let module C = Cic in
1958 let rec merge_coercions ctx =
1959 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1961 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1962 | C.Meta (n,subst) ->
1965 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1968 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1969 | C.Prod (name,so,dest) ->
1970 let ctx' = (Some (name,C.Decl so))::ctx in
1971 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1972 | C.Lambda (name,so,dest) ->
1973 let ctx' = (Some (name,C.Decl so))::ctx in
1974 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1975 | C.LetIn (name,so,dest) ->
1976 let _,ty,metasenv,ugraph =
1977 pack_coercions := false;
1978 type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1979 pack_coercions := true;
1980 let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1981 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1983 let l = List.map (merge_coercions ctx) l in
1985 let b,_,_,_,_ = is_a_double_coercion t in
1987 let ugraph = CicUniv.oblivion_ugraph in
1988 let old_insert_coercions = !insert_coercions in
1989 insert_coercions := false;
1990 let newt, _, menv, _ =
1992 type_of_aux' metasenv ctx t ugraph
1993 with RefineFailure _ | Uncertain _ ->
1996 insert_coercions := old_insert_coercions;
1997 if metasenv <> [] || menv = [] then
2000 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
2003 | C.Var (uri,exp_named_subst) ->
2004 let exp_named_subst = List.map aux exp_named_subst in
2005 C.Var (uri, exp_named_subst)
2006 | C.Const (uri,exp_named_subst) ->
2007 let exp_named_subst = List.map aux exp_named_subst in
2008 C.Const (uri, exp_named_subst)
2009 | C.MutInd (uri,tyno,exp_named_subst) ->
2010 let exp_named_subst = List.map aux exp_named_subst in
2011 C.MutInd (uri,tyno,exp_named_subst)
2012 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
2013 let exp_named_subst = List.map aux exp_named_subst in
2014 C.MutConstruct (uri,tyno,consno,exp_named_subst)
2015 | C.MutCase (uri,tyno,out,te,pl) ->
2016 let pl = List.map (merge_coercions ctx) pl in
2017 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
2018 | C.Fix (fno, fl) ->
2021 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2026 (fun (name,idx,ty,bo) ->
2027 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
2031 | C.CoFix (fno, fl) ->
2034 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2039 (fun (name,ty,bo) ->
2040 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
2045 merge_coercions ctx t
2048 let pack_coercion_metasenv conjectures = conjectures (*
2050 TASSI: this code war written when coercions were a toy,
2051 now packing coercions involves unification thus
2052 the metasenv may change, and this pack coercion
2053 does not handle that.
2055 let module C = Cic in
2057 (fun (i, ctx, ty) ->
2063 Some (name, C.Decl t) ->
2064 Some (name, C.Decl (pack_coercion conjectures ctx t))
2065 | Some (name, C.Def (t,None)) ->
2066 Some (name,C.Def (pack_coercion conjectures ctx t,None))
2067 | Some (name, C.Def (t,Some ty)) ->
2068 Some (name, C.Def (pack_coercion conjectures ctx t,
2069 Some (pack_coercion conjectures ctx ty)))
2075 ((i,ctx,pack_coercion conjectures ctx ty))
2080 let pack_coercion_obj obj = obj (*
2082 TASSI: this code war written when coercions were a toy,
2083 now packing coercions involves unification thus
2084 the metasenv may change, and this pack coercion
2085 does not handle that.
2087 let module C = Cic in
2089 | C.Constant (id, body, ty, params, attrs) ->
2093 | Some body -> Some (pack_coercion [] [] body)
2095 let ty = pack_coercion [] [] ty in
2096 C.Constant (id, body, ty, params, attrs)
2097 | C.Variable (name, body, ty, params, attrs) ->
2101 | Some body -> Some (pack_coercion [] [] body)
2103 let ty = pack_coercion [] [] ty in
2104 C.Variable (name, body, ty, params, attrs)
2105 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2106 let conjectures = pack_coercion_metasenv conjectures in
2107 let body = pack_coercion conjectures [] body in
2108 let ty = pack_coercion conjectures [] ty in
2109 C.CurrentProof (name, conjectures, body, ty, params, attrs)
2110 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2113 (fun (name, ind, arity, cl) ->
2114 let arity = pack_coercion [] [] arity in
2116 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2118 (name, ind, arity, cl))
2121 C.InductiveDefinition (indtys, params, leftno, attrs) *)
2126 let type_of_aux' metasenv context term =
2129 type_of_aux' metasenv context term in
2131 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2133 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2136 | RefineFailure msg as e ->
2137 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2139 | Uncertain msg as e ->
2140 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2144 let profiler2 = HExtlib.profile "CicRefine"
2146 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2147 profiler2.HExtlib.profile
2148 (type_of_aux' ?localization_tbl metasenv context term) ugraph
2150 let typecheck ~localization_tbl metasenv uri obj =
2151 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2153 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2154 (* vim:set foldmethod=marker: *)