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 (_,ty)) ->
341 t,S.lift n ty,subst,metasenv, ugraph
343 enrich localization_tbl t
344 (RefineFailure (lazy "Rel to hidden hypothesis"))
347 enrich localization_tbl t
348 (RefineFailure (lazy "Not a closed term")))
349 | C.Var (uri,exp_named_subst) ->
350 let exp_named_subst',subst',metasenv',ugraph1 =
351 check_exp_named_subst
352 subst metasenv context exp_named_subst ugraph
354 let ty_uri,ugraph1 = type_of_variable uri ugraph in
356 CicSubstitution.subst_vars exp_named_subst' ty_uri
358 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
361 let (canonical_context, term,ty) =
362 CicUtil.lookup_subst n subst
364 let l',subst',metasenv',ugraph1 =
365 check_metasenv_consistency n subst metasenv context
366 canonical_context l ugraph
368 (* trust or check ??? *)
369 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
370 subst', metasenv', ugraph1
371 (* type_of_aux subst metasenv
372 context (CicSubstitution.subst_meta l term) *)
373 with CicUtil.Subst_not_found _ ->
374 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
375 let l',subst',metasenv', ugraph1 =
376 check_metasenv_consistency n subst metasenv context
377 canonical_context l ugraph
379 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
380 subst', metasenv',ugraph1)
381 | C.Sort (C.Type tno) ->
382 let tno' = CicUniv.fresh() in
384 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
385 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
387 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
389 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
390 | C.Implicit infos ->
391 let metasenv',t' = exp_impl metasenv subst context infos in
392 type_of_aux subst metasenv' context t' ugraph
394 let ty',_,subst',metasenv',ugraph1 =
395 type_of_aux subst metasenv context ty ugraph
397 let te',inferredty,subst'',metasenv'',ugraph2 =
398 type_of_aux subst' metasenv' context te ugraph1
400 let (te', ty'), subst''',metasenv''',ugraph3 =
401 coerce_to_something true localization_tbl te' inferredty ty'
402 subst'' metasenv'' context ugraph2
404 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
405 | C.Prod (name,s,t) ->
406 let s',sort1,subst',metasenv',ugraph1 =
407 type_of_aux subst metasenv context s ugraph
409 let s',sort1,subst', metasenv',ugraph1 =
410 coerce_to_sort localization_tbl
411 s' sort1 subst' context metasenv' ugraph1
413 let context_for_t = ((Some (name,(C.Decl s')))::context) in
414 let t',sort2,subst'',metasenv'',ugraph2 =
415 type_of_aux subst' metasenv'
416 context_for_t t ugraph1
418 let t',sort2,subst'',metasenv'',ugraph2 =
419 coerce_to_sort localization_tbl
420 t' sort2 subst'' context_for_t metasenv'' ugraph2
422 let sop,subst''',metasenv''',ugraph3 =
423 sort_of_prod localization_tbl subst'' metasenv''
424 context (name,s') t' (sort1,sort2) ugraph2
426 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
427 | C.Lambda (n,s,t) ->
428 let s',sort1,subst',metasenv',ugraph1 =
429 type_of_aux subst metasenv context s ugraph
431 let s',sort1,subst',metasenv',ugraph1 =
432 coerce_to_sort localization_tbl
433 s' sort1 subst' context metasenv' ugraph1
435 let context_for_t = ((Some (n,(C.Decl s')))::context) in
436 let t',type2,subst'',metasenv'',ugraph2 =
437 type_of_aux subst' metasenv' context_for_t t ugraph1
439 C.Lambda (n,s',t'),C.Prod (n,s',type2),
440 subst'',metasenv'',ugraph2
441 | C.LetIn (n,s,ty,t) ->
442 (* only to check if s is well-typed *)
443 let s',ty',subst',metasenv',ugraph1 =
444 type_of_aux subst metasenv context s ugraph in
445 let ty,_,subst',metasenv',ugraph1 =
446 type_of_aux subst' metasenv' context ty ugraph1 in
447 let subst',metasenv',ugraph1 =
449 fo_unif_subst subst' context metasenv'
453 enrich localization_tbl s' exn
456 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
457 context ^ " has type " ^
458 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
459 context ^ " but is here used with type " ^
460 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
463 let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
465 let t',inferredty,subst'',metasenv'',ugraph2 =
466 type_of_aux subst' metasenv'
467 context_for_t t ugraph1
469 (* One-step LetIn reduction.
470 * Even faster than the previous solution.
471 * Moreover the inferred type is closer to the expected one.
473 C.LetIn (n,s',ty,t'),
474 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
475 subst'',metasenv'',ugraph2
476 | C.Appl (he::((_::_) as tl)) ->
477 let he',hetype,subst',metasenv',ugraph1 =
478 type_of_aux subst metasenv context he ugraph
480 let tlbody_and_type,subst'',metasenv'',ugraph2 =
481 typeof_list subst' metasenv' context ugraph1 tl
483 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
484 eat_prods true subst'' metasenv'' context
485 he' hetype tlbody_and_type ugraph2
487 let newappl = (C.Appl (coerced_he::coerced_args)) in
488 avoid_double_coercion
489 context subst''' metasenv''' ugraph3 newappl applty
490 | C.Appl _ -> assert false
491 | C.Const (uri,exp_named_subst) ->
492 let exp_named_subst',subst',metasenv',ugraph1 =
493 check_exp_named_subst subst metasenv context
494 exp_named_subst ugraph in
495 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
497 CicSubstitution.subst_vars exp_named_subst' ty_uri
499 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
500 | C.MutInd (uri,i,exp_named_subst) ->
501 let exp_named_subst',subst',metasenv',ugraph1 =
502 check_exp_named_subst subst metasenv context
503 exp_named_subst ugraph
505 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
507 CicSubstitution.subst_vars exp_named_subst' ty_uri in
508 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
509 | C.MutConstruct (uri,i,j,exp_named_subst) ->
510 let exp_named_subst',subst',metasenv',ugraph1 =
511 check_exp_named_subst subst metasenv context
512 exp_named_subst ugraph
515 type_of_mutual_inductive_constr uri i j ugraph1
518 CicSubstitution.subst_vars exp_named_subst' ty_uri
520 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
522 | C.MutCase (uri, i, outtype, term, pl) ->
523 (* first, get the inductive type (and noparams)
524 * in the environment *)
525 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
526 let _ = CicTypeChecker.typecheck uri in
527 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
529 C.InductiveDefinition (l,expl_params,parsno,_) ->
530 List.nth l i , expl_params, parsno, u
532 enrich localization_tbl t
534 (lazy ("Unkown mutual inductive definition " ^
535 U.string_of_uri uri)))
537 if List.length constructors <> List.length pl then
538 enrich localization_tbl t
540 (lazy "Wrong number of cases")) ;
541 let rec count_prod t =
542 match CicReduction.whd ~subst context t with
543 C.Prod (_, _, t) -> 1 + (count_prod t)
546 let no_args = count_prod arity in
547 (* now, create a "generic" MutInd *)
548 let metasenv,left_args =
549 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
551 let metasenv,right_args =
552 let no_right_params = no_args - no_left_params in
553 if no_right_params < 0 then assert false
554 else CicMkImplicit.n_fresh_metas
555 metasenv subst context no_right_params
557 let metasenv,exp_named_subst =
558 CicMkImplicit.fresh_subst metasenv subst context expl_params in
561 C.MutInd (uri,i,exp_named_subst)
564 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
566 (* check consistency with the actual type of term *)
567 let term',actual_type,subst,metasenv,ugraph1 =
568 type_of_aux subst metasenv context term ugraph in
569 let expected_type',_, subst, metasenv,ugraph2 =
570 type_of_aux subst metasenv context expected_type ugraph1
572 let actual_type = CicReduction.whd ~subst context actual_type in
573 let subst,metasenv,ugraph3 =
575 fo_unif_subst subst context metasenv
576 expected_type' actual_type ugraph2
579 enrich localization_tbl term' exn
582 CicMetaSubst.ppterm_in_context ~metasenv subst term'
583 context ^ " has type " ^
584 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
585 context ^ " but is here used with type " ^
586 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
588 let rec instantiate_prod t =
592 match CicReduction.whd ~subst context t with
594 instantiate_prod (CicSubstitution.subst he t') tl
597 let arity_instantiated_with_left_args =
598 instantiate_prod arity left_args in
599 (* TODO: check if the sort elimination
600 * is allowed: [(I q1 ... qr)|B] *)
601 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
603 (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
605 if left_args = [] then
606 (C.MutConstruct (uri,i,j,exp_named_subst))
609 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
611 let p',actual_type,subst,metasenv,ugraph1 =
612 type_of_aux subst metasenv context p ugraph
614 let constructor',expected_type, subst, metasenv,ugraph2 =
615 type_of_aux subst metasenv context constructor ugraph1
617 let outtypeinstance,subst,metasenv,ugraph3 =
619 check_branch 0 context metasenv subst
620 no_left_params actual_type constructor' expected_type
624 enrich localization_tbl constructor'
627 CicMetaSubst.ppterm_in_context metasenv subst p'
628 context ^ " has type " ^
629 CicMetaSubst.ppterm_in_context metasenv subst actual_type
630 context ^ " but is here used with type " ^
631 CicMetaSubst.ppterm_in_context metasenv subst expected_type
635 outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
636 pl ([],List.length pl,[],subst,metasenv,ugraph3)
639 (* we are left to check that the outype matches his instances.
640 The easy case is when the outype is specified, that amount
641 to a trivial check. Otherwise, we should guess a type from
645 let outtype,outtypety, subst, metasenv,ugraph4 =
646 type_of_aux subst metasenv context outtype ugraph4 in
649 (let candidate,ugraph5,metasenv,subst =
650 let exp_name_subst, metasenv =
652 CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
654 let uris = CicUtil.params_of_obj o in
656 fun uri (acc,metasenv) ->
657 let metasenv',new_meta =
658 CicMkImplicit.mk_implicit metasenv subst context
661 CicMkImplicit.identity_relocation_list_for_metavariable
664 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
668 match left_args,right_args with
669 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
671 let rec mk_right_args =
674 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
676 let right_args_no = List.length right_args in
677 let lifted_left_args =
678 List.map (CicSubstitution.lift right_args_no) left_args
680 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
681 (lifted_left_args @ mk_right_args right_args_no))
684 FreshNamesGenerator.mk_fresh_name ~subst metasenv
685 context Cic.Anonymous ~typ:ty
687 match outtypeinstances with
689 let extended_context =
690 let rec add_right_args =
692 Cic.Prod (name,ty,t) ->
693 Some (name,Cic.Decl ty)::(add_right_args t)
696 (Some (fresh_name,Cic.Decl ty))::
698 (add_right_args arity_instantiated_with_left_args))@
701 let metasenv,new_meta =
702 CicMkImplicit.mk_implicit metasenv subst extended_context
705 CicMkImplicit.identity_relocation_list_for_metavariable
708 let rec add_lambdas b =
710 Cic.Prod (name,ty,t) ->
711 Cic.Lambda (name,ty,(add_lambdas b t))
712 | _ -> Cic.Lambda (fresh_name, ty, b)
715 add_lambdas (Cic.Meta (new_meta,irl))
716 arity_instantiated_with_left_args
718 (Some candidate),ugraph4,metasenv,subst
719 | (constructor_args_no,_,instance,_)::tl ->
721 let instance',subst,metasenv =
722 CicMetaSubst.delift_rels subst metasenv
723 constructor_args_no instance
725 let candidate,ugraph,metasenv,subst =
727 fun (candidate_oty,ugraph,metasenv,subst)
728 (constructor_args_no,_,instance,_) ->
729 match candidate_oty with
730 | None -> None,ugraph,metasenv,subst
733 let instance',subst,metasenv =
734 CicMetaSubst.delift_rels subst metasenv
735 constructor_args_no instance
737 let subst,metasenv,ugraph =
738 fo_unif_subst subst context metasenv
741 candidate_oty,ugraph,metasenv,subst
743 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
744 | RefineFailure _ | Uncertain _ ->
745 None,ugraph,metasenv,subst
746 ) (Some instance',ugraph4,metasenv,subst) tl
749 | None -> None, ugraph,metasenv,subst
751 let rec add_lambdas n b =
753 Cic.Prod (name,ty,t) ->
754 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
756 Cic.Lambda (fresh_name, ty,
757 CicSubstitution.lift (n + 1) t)
760 (add_lambdas 0 t arity_instantiated_with_left_args),
761 ugraph,metasenv,subst
762 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
763 None,ugraph4,metasenv,subst
766 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
768 let subst,metasenv,ugraph =
770 fo_unif_subst subst context metasenv
771 candidate outtype ugraph5
773 exn -> assert false(* unification against a metavariable *)
775 C.MutCase (uri, i, outtype, term', pl'),
776 CicReduction.head_beta_reduce
777 (CicMetaSubst.apply_subst subst
778 (Cic.Appl (outtype::right_args@[term']))),
779 subst,metasenv,ugraph)
780 | _ -> (* easy case *)
781 let tlbody_and_type,subst,metasenv,ugraph4 =
782 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
784 let _,_,_,subst,metasenv,ugraph4 =
785 eat_prods false subst metasenv context
786 outtype outtypety tlbody_and_type ugraph4
788 let _,_, subst, metasenv,ugraph5 =
789 type_of_aux subst metasenv context
790 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
792 let (subst,metasenv,ugraph6) =
794 (fun (subst,metasenv,ugraph)
795 p (constructor_args_no,context,instance,args)
800 CicSubstitution.lift constructor_args_no outtype
802 C.Appl (outtype'::args)
804 CicReduction.whd ~subst context appl
807 fo_unif_subst subst context metasenv instance instance'
811 enrich localization_tbl p exn
814 CicMetaSubst.ppterm_in_context ~metasenv subst p
815 context ^ " has type " ^
816 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
817 context ^ " but is here used with type " ^
818 CicMetaSubst.ppterm_in_context ~metasenv subst instance
820 (subst,metasenv,ugraph5) pl' outtypeinstances
822 C.MutCase (uri, i, outtype, term', pl'),
823 CicReduction.head_beta_reduce
824 (CicMetaSubst.apply_subst subst
825 (C.Appl(outtype::right_args@[term]))),
826 subst,metasenv,ugraph6)
828 let fl_ty',subst,metasenv,types,ugraph1,len =
830 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
831 let ty',_,subst',metasenv',ugraph1 =
832 type_of_aux subst metasenv context ty ugraph
834 fl @ [ty'],subst',metasenv',
835 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
836 :: types, ugraph, len+1
837 ) ([],subst,metasenv,[],ugraph,0) fl
839 let context' = types@context in
840 let fl_bo',subst,metasenv,ugraph2 =
842 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
843 let bo',ty_of_bo,subst,metasenv,ugraph1 =
844 type_of_aux subst metasenv context' bo ugraph in
845 let expected_ty = CicSubstitution.lift len ty in
846 let subst',metasenv',ugraph' =
848 fo_unif_subst subst context' metasenv
849 ty_of_bo expected_ty ugraph1
852 enrich localization_tbl bo exn
855 CicMetaSubst.ppterm_in_context ~metasenv subst bo
856 context' ^ " has type " ^
857 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
858 context' ^ " but is here used with type " ^
859 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
862 fl @ [bo'] , subst',metasenv',ugraph'
863 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
865 let ty = List.nth fl_ty' i in
866 (* now we have the new ty in fl_ty', the new bo in fl_bo',
867 * and we want the new fl with bo' and ty' injected in the right
870 let rec map3 f l1 l2 l3 =
873 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
876 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
879 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
881 let fl_ty',subst,metasenv,types,ugraph1,len =
883 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
884 let ty',_,subst',metasenv',ugraph1 =
885 type_of_aux subst metasenv context ty ugraph
887 fl @ [ty'],subst',metasenv',
888 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
889 types, ugraph1, len+1
890 ) ([],subst,metasenv,[],ugraph,0) fl
892 let context' = types@context in
893 let fl_bo',subst,metasenv,ugraph2 =
895 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
896 let bo',ty_of_bo,subst,metasenv,ugraph1 =
897 type_of_aux subst metasenv context' bo ugraph in
898 let expected_ty = CicSubstitution.lift len ty in
899 let subst',metasenv',ugraph' =
901 fo_unif_subst subst context' metasenv
902 ty_of_bo expected_ty ugraph1
905 enrich localization_tbl bo exn
908 CicMetaSubst.ppterm_in_context ~metasenv subst bo
909 context' ^ " has type " ^
910 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
911 context' ^ " but is here used with type " ^
912 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
915 fl @ [bo'],subst',metasenv',ugraph'
916 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
918 let ty = List.nth fl_ty' i in
919 (* now we have the new ty in fl_ty', the new bo in fl_bo',
920 * and we want the new fl with bo' and ty' injected in the right
923 let rec map3 f l1 l2 l3 =
926 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
929 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
932 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
934 relocalize localization_tbl t t';
937 (* check_metasenv_consistency checks that the "canonical" context of a
938 metavariable is consitent - up to relocation via the relocation list l -
939 with the actual context *)
940 and check_metasenv_consistency
941 metano subst metasenv context canonical_context l ugraph
943 let module C = Cic in
944 let module R = CicReduction in
945 let module S = CicSubstitution in
946 let lifted_canonical_context =
950 | (Some (n,C.Decl t))::tl ->
951 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
952 | None::tl -> None::(aux (i+1) tl)
953 | (Some (n,C.Def (t,ty)))::tl ->
957 (S.subst_meta l (S.lift i t),
958 S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
960 aux 1 canonical_context
964 (fun (l,subst,metasenv,ugraph) t ct ->
967 l @ [None],subst,metasenv,ugraph
968 | Some t,Some (_,C.Def (ct,_)) ->
969 (*CSC: the following optimization is to avoid a possibly
970 expensive reduction that can be easily avoided and
971 that is quite frequent. However, this is better
972 handled using levels to control reduction *)
977 match List.nth context (n - 1) with
978 Some (_,C.Def (te,_)) -> S.lift n te
984 let subst',metasenv',ugraph' =
986 (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
987 * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
988 fo_unif_subst subst context metasenv optimized_t ct ugraph
989 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))))))
991 l @ [Some t],subst',metasenv',ugraph'
992 | Some t,Some (_,C.Decl ct) ->
993 let t',inferredty,subst',metasenv',ugraph1 =
994 type_of_aux subst metasenv context t ugraph
996 let subst'',metasenv'',ugraph2 =
999 subst' context metasenv' inferredty ct ugraph1
1000 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))))))
1002 l @ [Some t'], subst'',metasenv'',ugraph2
1004 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
1006 Invalid_argument _ ->
1010 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1011 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1012 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1014 and check_exp_named_subst metasubst metasenv context tl ugraph =
1015 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1017 [] -> [],metasubst,metasenv,ugraph
1019 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1021 CicSubstitution.subst_vars substs ty_uri in
1022 (* CSC: why was this code here? it is wrong
1023 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1024 Cic.Variable (_,Some bo,_,_) ->
1026 (RefineFailure (lazy
1027 "A variable with a body can not be explicit substituted"))
1028 | Cic.Variable (_,None,_,_) -> ()
1031 (RefineFailure (lazy
1032 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1035 let t',typeoft,metasubst',metasenv',ugraph2 =
1036 type_of_aux metasubst metasenv context t ugraph1 in
1037 let subst = uri,t' in
1038 let metasubst'',metasenv'',ugraph3 =
1041 metasubst' context metasenv' typeoft typeofvar ugraph2
1043 raise (RefineFailure (lazy
1044 ("Wrong Explicit Named Substitution: " ^
1045 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1046 " not unifiable with " ^
1047 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1049 (* FIXME: no mere tail recursive! *)
1050 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1051 check_exp_named_subst_aux
1052 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1054 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1056 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1059 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1062 let module C = Cic in
1063 let context_for_t2 = (Some (name,C.Decl s))::context in
1064 let t1'' = CicReduction.whd ~subst context t1 in
1065 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1066 match (t1'', t2'') with
1067 (C.Sort s1, C.Sort s2)
1068 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1069 (* different than Coq manual!!! *)
1070 C.Sort s2,subst,metasenv,ugraph
1071 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1072 let t' = CicUniv.fresh() in
1074 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1075 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1076 C.Sort (C.Type t'),subst,metasenv,ugraph2
1078 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1079 | (C.Sort _,C.Sort (C.Type t1)) ->
1080 C.Sort (C.Type t1),subst,metasenv,ugraph
1081 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1082 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1083 (* TODO how can we force the meta to become a sort? If we don't we
1084 * break the invariant that refine produce only well typed terms *)
1085 (* TODO if we check the non meta term and if it is a sort then we
1086 * are likely to know the exact value of the result e.g. if the rhs
1087 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1088 let (metasenv,idx) =
1089 CicMkImplicit.mk_implicit_sort metasenv subst in
1090 let (subst, metasenv,ugraph1) =
1092 fo_unif_subst subst context_for_t2 metasenv
1093 (C.Meta (idx,[])) t2'' ugraph
1094 with _ -> assert false (* unification against a metavariable *)
1096 t2'',subst,metasenv,ugraph1
1099 enrich localization_tbl s
1103 "%s is supposed to be a type, but its type is %s"
1104 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1105 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1107 enrich localization_tbl t
1111 "%s is supposed to be a type, but its type is %s"
1112 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1113 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1115 and avoid_double_coercion context subst metasenv ugraph t ty =
1116 if not !pack_coercions then
1117 t,ty,subst,metasenv,ugraph
1119 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1121 let source_carr = CoercGraph.source_of c2 in
1122 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1123 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1125 | CoercGraph.SomeCoercion candidates ->
1127 HExtlib.list_findopt
1128 (function (metasenv,last,c) ->
1130 | c when not (CoercGraph.is_composite c) ->
1131 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1134 let subst,metasenv,ugraph =
1135 fo_unif_subst subst context metasenv last head ugraph in
1136 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1141 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1142 let newt,_,subst,metasenv,ugraph =
1143 type_of_aux subst metasenv context c ugraph in
1144 debug_print (lazy "tipa...");
1145 let subst, metasenv, ugraph =
1146 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1147 fo_unif_subst subst context metasenv newt t ugraph
1149 debug_print (lazy "unifica...");
1150 Some (newt, ty, subst, metasenv, ugraph)
1152 | RefineFailure s | Uncertain s when not !pack_coercions->
1153 debug_print s; debug_print (lazy "stop\n");None
1154 | RefineFailure s | Uncertain s ->
1155 debug_print s;debug_print (lazy "goon\n");
1157 let old_pack_coercions = !pack_coercions in
1158 pack_coercions := false; (* to avoid diverging *)
1159 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1160 type_of_aux subst metasenv context c1_c2_implicit ugraph
1162 pack_coercions := old_pack_coercions;
1164 is_a_double_coercion refined_c1_c2_implicit
1170 match refined_c1_c2_implicit with
1171 | Cic.Appl l -> HExtlib.list_last l
1174 let subst, metasenv, ugraph =
1175 try fo_unif_subst subst context metasenv
1177 with RefineFailure s| Uncertain s->
1178 debug_print s;assert false
1180 let subst, metasenv, ugraph =
1181 fo_unif_subst subst context metasenv
1182 refined_c1_c2_implicit t ugraph
1184 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1186 | RefineFailure s | Uncertain s ->
1187 pack_coercions := true;debug_print s;None
1188 | exn -> pack_coercions := true; raise exn))
1191 (match selected with
1195 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1196 t, ty, subst, metasenv, ugraph)
1197 | _ -> t, ty, subst, metasenv, ugraph)
1199 t, ty, subst, metasenv, ugraph
1201 and typeof_list subst metasenv context ugraph l =
1202 let tlbody_and_type,subst,metasenv,ugraph =
1204 (fun x (res,subst,metasenv,ugraph) ->
1205 let x',ty,subst',metasenv',ugraph1 =
1206 type_of_aux subst metasenv context x ugraph
1208 (x', ty)::res,subst',metasenv',ugraph1
1209 ) l ([],subst,metasenv,ugraph)
1211 tlbody_and_type,subst,metasenv,ugraph
1214 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1216 (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1217 let fix_arity n metasenv context subst he hetype ugraph =
1218 let hetype = CicMetaSubst.apply_subst subst hetype in
1219 let src = CoercDb.coerc_carr_of_term hetype in
1220 let tgt = CoercDb.Fun 0 in
1221 match CoercGraph.look_for_coercion' metasenv subst context src tgt with
1222 | CoercGraph.NoCoercion -> []
1223 | CoercGraph.NotMetaClosed
1224 | CoercGraph.NotHandled _ ->
1225 raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1226 | CoercGraph.SomeCoercionToTgt candidates
1227 | CoercGraph.SomeCoercion candidates ->
1229 (fun (metasenv,last,coerc) ->
1231 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1233 let subst,metasenv,ugraph =
1234 fo_unif_subst subst context metasenv last he ugraph in
1235 debug_print (lazy ("New head: "^ pp coerc));
1237 CicTypeChecker.type_of_aux' ~subst metasenv context coerc
1240 debug_print (lazy (" has type: "^ pp tty));
1241 Some (coerc,tty,subst,metasenv,ugraph)
1243 | Uncertain _ | RefineFailure _
1244 | HExtlib.Localized (_,Uncertain _)
1245 | HExtlib.Localized (_,RefineFailure _) -> None
1246 | exn -> assert false)
1249 (* aux function to process the type of the head and the args in parallel *)
1250 let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1252 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1253 | (hete, hety)::tl as args ->
1254 match (CicReduction.whd ~subst context hetype) with
1255 | Cic.Prod (n,s,t) ->
1256 let arg,subst,metasenv,ugraph =
1257 coerce_to_something allow_coercions localization_tbl
1258 hete hety s subst metasenv context ugraph in
1260 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1261 ugraph (newargs@[arg]) tl
1264 match he, newargs with
1266 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1267 | _ -> Cic.Appl (he::List.map fst newargs)
1269 (*{{{*) debug_print (lazy
1271 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1272 "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1273 "\n but is applyed to: " ^ String.concat ";"
1274 (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1275 let possible_fixes =
1276 fix_arity (List.length args) metasenv context subst he hetype
1279 HExtlib.list_findopt
1280 (fun (he,hetype,subst,metasenv,ugraph) ->
1281 (* {{{ *)debug_print (lazy ("Try fix: "^
1282 CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1283 debug_print (lazy (" of type: "^
1284 CicMetaSubst.ppterm_in_context
1285 ~metasenv subst hetype context)); (* }}} *)
1287 Some (eat_prods_and_args
1288 metasenv subst context he hetype ugraph [] args)
1290 | RefineFailure _ | Uncertain _
1291 | HExtlib.Localized (_,RefineFailure _)
1292 | HExtlib.Localized (_,Uncertain _) -> None)
1298 (MoreArgsThanExpected
1299 (List.length args, RefineFailure (lazy "")))
1301 (* first we check if we are in the simple case of a meta closed term *)
1302 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1303 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1304 (* this optimization is to postpone fix_arity (the most common case)*)
1305 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1307 (* this (says CSC) is also useful to infer dependent types *)
1308 let pristinemenv = metasenv in
1309 let metasenv,hetype' =
1310 mk_prod_of_metas metasenv context subst args_bo_and_ty
1313 let subst,metasenv,ugraph =
1314 fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1316 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1317 with RefineFailure _ | Uncertain _ ->
1318 subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1320 let coerced_args,subst,metasenv,he,t,ugraph =
1323 metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1325 MoreArgsThanExpected (residuals,exn) ->
1326 more_args_than_expected localization_tbl metasenv
1327 subst he context hetype' residuals args_bo_and_ty exn
1329 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1331 and coerce_to_something
1332 allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1334 let module CS = CicSubstitution in
1335 let module CR = CicReduction in
1336 let cs_subst = CS.subst ~avoid_beta_redexes:true in
1337 let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1338 debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1340 CoercGraph.look_for_coercion metasenv subst context infty expty
1343 | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
1344 "coerce_atom_to_something fails since not meta closed"))
1345 | CoercGraph.NoCoercion
1346 | CoercGraph.SomeCoercionToTgt _
1347 | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
1348 "coerce_atom_to_something fails since no coercions found"))
1349 | CoercGraph.SomeCoercion candidates ->
1350 debug_print (lazy (string_of_int (List.length candidates) ^
1351 " candidates found"));
1352 let uncertain = ref false in
1356 (fun (metasenv,last,c) ->
1358 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1359 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1361 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
1362 "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
1364 debug_print (lazy ("FO_UNIF_SUBST: " ^
1365 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1366 let subst,metasenv,ugraph =
1367 fo_unif_subst subst context metasenv last t ugraph
1369 let newt,newhety,subst,metasenv,ugraph =
1370 type_of_aux subst metasenv context c ugraph in
1371 let newt, newty, subst, metasenv, ugraph =
1372 avoid_double_coercion context subst metasenv ugraph newt expty
1374 let subst,metasenv,ugraph =
1375 fo_unif_subst subst context metasenv newhety expty ugraph in
1376 Some ((newt,newty), subst, metasenv, ugraph)
1378 | Uncertain _ -> uncertain := true; None
1379 | RefineFailure _ -> None)
1384 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1392 | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1393 | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1395 let rec coerce_to_something_aux
1396 t infty expty subst metasenv context ugraph
1399 let subst, metasenv, ugraph =
1400 fo_unif_subst subst context metasenv infty expty ugraph
1402 (t, expty), subst, metasenv, ugraph
1403 with (Uncertain _ | RefineFailure _ as exn)
1404 when allow_coercions && !insert_coercions ->
1405 let whd = CicReduction.whd ~delta:false in
1406 let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1407 let infty = clean infty subst context in
1408 let expty = clean expty subst context in
1409 let t = clean t subst context in
1410 (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1411 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1412 CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1413 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1414 let (coerced,_),subst,metasenv,_ as result =
1415 match infty, expty, t with
1416 | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1417 (*{{{*) debug_print (lazy "FIX");
1419 [name,i,_(* infty *),bo] ->
1421 Some (Cic.Name name,Cic.Decl expty)::context in
1422 let (rel1, _), subst, metasenv, ugraph =
1423 coerce_to_something_aux (Cic.Rel 1)
1424 (CS.lift 1 expty) (CS.lift 1 infty) subst
1425 metasenv context_bo ugraph in
1426 let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1427 let (bo,_), subst, metasenv, ugraph =
1428 coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1430 metasenv context_bo ugraph
1432 (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1433 | _ -> assert false (* not implemented yet *)) (*}}}*)
1434 | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1435 (*{{{*) debug_print (lazy "CASE");
1436 (* {{{ helper functions *)
1437 let get_cl_and_left_p uri tyno outty ugraph =
1438 match CicEnvironment.get_obj ugraph uri with
1439 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1442 match CicReduction.whd ~delta:false ctx t with
1443 | Cic.Prod (name,src,tgt) ->
1444 let ctx = Some (name, Cic.Decl src) :: ctx in
1450 let rec skip_lambda_delifting t n =
1453 | Cic.Lambda (_,_,t),n ->
1454 skip_lambda_delifting
1455 (CS.subst (Cic.Implicit None) t) (n - 1)
1458 let get_l_r_p n = function
1459 | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1460 | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1461 HExtlib.split_nth n args
1464 let _, _, ty, cl = List.nth tl tyno in
1465 let pis = count_pis ty in
1466 let rno = pis - leftno in
1467 let t = skip_lambda_delifting outty rno in
1468 let left_p, _ = get_l_r_p leftno t in
1469 let instantiale_with_left cl =
1473 (fun t p -> match t with
1474 | Cic.Prod (_,_,t) ->
1480 let cl = instantiale_with_left (List.map snd cl) in
1481 cl, left_p, leftno, rno, ugraph
1484 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1487 let rec mkr n = function
1488 | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1491 CicReplace.replace_lifting
1492 ~equality:(fun _ -> CicUtil.alpha_equivalence)
1494 ~what:(matched::right_p)
1495 ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1499 | Cic.Lambda (name, src, tgt),_ ->
1500 Cic.Lambda (name, src,
1501 keep_lambdas_and_put_expty
1502 (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1503 (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1506 let eq_uri, eq, eq_refl =
1507 match LibraryObjects.eq_URI () with
1508 | None -> HLog.warn "no default equality"; raise exn
1509 | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1512 metasenv subst context uri tyno cty outty mty m leftno i
1514 let rec aux context outty par k mty m = function
1515 | Cic.Prod (name, src, tgt) ->
1518 (Some (name, Cic.Decl src) :: context)
1519 (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1520 (CS.lift 1 mty) (CS.lift 1 m) tgt
1522 Cic.Prod (name, src, t), k
1525 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1526 if par <> [] then Cic.Appl (k::par) else k
1528 Cic.Prod (Cic.Name "p",
1529 Cic.Appl [eq; mty; m; k],
1531 (CR.head_beta_reduce ~delta:false
1532 (Cic.Appl [outty;k])))),k
1533 | Cic.Appl (Cic.MutInd _::pl) ->
1534 let left_p,right_p = HExtlib.split_nth leftno pl in
1535 let has_rights = right_p <> [] in
1537 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1538 Cic.Appl (k::left_p@par)
1542 CicTypeChecker.type_of_aux' ~subst metasenv context k
1543 CicUniv.oblivion_ugraph
1545 | Cic.Appl (Cic.MutInd _::args),_ ->
1546 snd (HExtlib.split_nth leftno args)
1548 with CicTypeChecker.TypeCheckerFailure _-> assert false
1551 CR.head_beta_reduce ~delta:false
1552 (Cic.Appl (outty ::right_p @ [k])),k
1554 Cic.Prod (Cic.Name "p",
1555 Cic.Appl [eq; mty; m; k],
1557 (CR.head_beta_reduce ~delta:false
1558 (Cic.Appl (outty ::right_p @ [k]))))),k
1561 aux context outty [] 1 mty m cty
1563 let add_lambda_for_refl_m pbo rno mty m k cty =
1564 (* k lives in the right context *)
1565 if rno <> 0 then pbo else
1566 let rec aux mty m = function
1567 | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1568 Cic.Lambda (name,src,
1569 (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1571 Cic.Lambda (Cic.Name "p",
1572 Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1576 let add_pi_for_refl_m new_outty mty m rno =
1577 if rno <> 0 then new_outty else
1578 let rec aux m mty = function
1579 | Cic.Lambda (name, src, tgt) ->
1580 Cic.Lambda (name, src,
1581 aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1584 (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1588 in (* }}} end helper functions *)
1589 (* constructors types with left params already instantiated *)
1590 let outty = CicMetaSubst.apply_subst subst outty in
1591 let cl, left_p, leftno,rno,ugraph =
1592 get_cl_and_left_p uri tyno outty ugraph
1597 CicTypeChecker.type_of_aux' ~subst metasenv context m
1598 CicUniv.oblivion_ugraph
1600 | Cic.MutInd _ as mty,_ -> [], mty
1601 | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
1602 snd (HExtlib.split_nth leftno args), mty
1604 with CicTypeChecker.TypeCheckerFailure _ -> assert false
1607 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1610 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1611 ~metasenv subst new_outty context));
1612 let _,pl,subst,metasenv,ugraph =
1614 (fun cty pbo (i, acc, s, menv, ugraph) ->
1615 (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1616 * (new_)outty right_par (K_i left_par k_par) *)
1618 add_params menv s context uri tyno
1619 cty outty mty m leftno i in
1621 (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1622 ~metasenv subst infty_pbo context));
1623 let expty_pbo, k = (* k is (K_i left_par k_par) *)
1624 add_params menv s context uri tyno
1625 cty new_outty mty m leftno i in
1627 (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1628 ~metasenv subst expty_pbo context));
1629 let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1631 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1632 ~metasenv subst pbo context));
1633 let (pbo, _), subst, metasenv, ugraph =
1634 coerce_to_something_aux pbo infty_pbo expty_pbo
1635 s menv context ugraph
1638 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1639 ~metasenv subst pbo context));
1640 (i-1, pbo::acc, subst, metasenv, ugraph))
1641 cl pl (List.length pl, [], subst, metasenv, ugraph)
1643 let new_outty = add_pi_for_refl_m new_outty mty m rno in
1645 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1646 ~metasenv subst new_outty context));
1649 let refl_m=Cic.Appl[eq_refl;mty;m]in
1650 Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1652 Cic.MutCase(uri,tyno,new_outty,m,pl)
1654 (t, expty), subst, metasenv, ugraph (*}}}*)
1655 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1656 (*{{{*) debug_print (lazy "LAM");
1658 FreshNamesGenerator.mk_fresh_name
1659 ~subst metasenv context ~typ:src2 Cic.Anonymous
1661 let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1662 (* contravariant part: the argument of f:src->ty *)
1663 let (rel1, _), subst, metasenv, ugraph =
1664 coerce_to_something_aux
1665 (Cic.Rel 1) (CS.lift 1 src2)
1666 (CS.lift 1 src) subst metasenv context_src2 ugraph
1668 (* covariant part: the result of f(c x); x:src2; (c x):src *)
1671 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1672 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1674 (* we fix the possible dependency problem in the source ty *)
1675 let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1676 let (bo, _), subst, metasenv, ugraph =
1677 coerce_to_something_aux
1678 bo ty ty2 subst metasenv context_src2 ugraph
1680 let coerced = Cic.Lambda (name_t,src2, bo) in
1681 (coerced, expty), subst, metasenv, ugraph (*}}}*)
1683 (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1684 ~metasenv subst infty context ^ " ==> " ^
1685 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1686 coerce_atom_to_something
1687 t infty expty subst metasenv context ugraph (*}}}*)
1689 debug_print (lazy ("COERCE TO SOMETHING END: "^
1690 CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1694 coerce_to_something_aux t infty expty subst metasenv context ugraph
1695 with Uncertain _ | RefineFailure _ as exn ->
1698 CicMetaSubst.ppterm_in_context metasenv subst t context ^
1699 " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1700 infty context ^ " but is here used with type " ^
1701 CicMetaSubst.ppterm_in_context metasenv subst expty context)
1703 enrich localization_tbl ~f t exn
1705 and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1706 match CicReduction.whd ~delta:false ~subst context infty with
1707 | Cic.Meta _ | Cic.Sort _ ->
1708 t,infty, subst, metasenv, ugraph
1710 debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1711 ~metasenv subst src context));
1712 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1714 let (t, ty_t), subst, metasenv, ugraph =
1715 coerce_to_something true
1716 localization_tbl t src tgt subst metasenv context ugraph
1718 debug_print (lazy ("COERCE TO SORT END: "^
1719 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1720 t, ty_t, subst, metasenv, ugraph
1721 with HExtlib.Localized (_, exn) ->
1723 lazy ("(7)The term " ^
1724 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1725 ^ " is not a type since it has type " ^
1726 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1727 ^ " that is not a sort")
1729 enrich localization_tbl ~f t exn
1732 (* eat prods ends here! *)
1734 let t',ty,subst',metasenv',ugraph1 =
1735 type_of_aux [] metasenv context t ugraph
1737 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1738 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1739 (* Andrea: ho rimesso qui l'applicazione della subst al
1740 metasenv dopo che ho droppato l'invariante che il metsaenv
1741 e' sempre istanziato *)
1742 let substituted_metasenv =
1743 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1745 (* substituted_t,substituted_ty,substituted_metasenv *)
1746 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1748 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1750 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1751 let cleaned_metasenv =
1753 (function (n,context,ty) ->
1754 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1759 | Some (n, Cic.Decl t) ->
1761 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1762 | Some (n, Cic.Def (bo,ty)) ->
1763 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1764 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
1766 Some (n, Cic.Def (bo',ty'))
1770 ) substituted_metasenv
1772 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1775 let undebrujin uri typesno tys t =
1778 (fun (name,_,_,_) (i,t) ->
1779 (* here the explicit_named_substituion is assumed to be *)
1781 let t' = Cic.MutInd (uri,i,[]) in
1782 let t = CicSubstitution.subst t' t in
1784 ) tys (typesno - 1,t))
1786 let map_first_n n start f g l =
1787 let rec aux acc k l =
1790 | [] -> raise (Invalid_argument "map_first_n")
1791 | hd :: tl -> f hd k (aux acc (k+1) tl)
1797 (*CSC: this is a very rough approximation; to be finished *)
1798 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1799 let subst,metasenv,ugraph,tys =
1801 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1802 let subst,metasenv,ugraph,cl =
1804 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1805 let rec aux ctx k subst = function
1806 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1807 let subst,metasenv,ugraph,tl =
1809 (subst,metasenv,ugraph,[])
1810 (fun t n (subst,metasenv,ugraph,acc) ->
1811 let subst,metasenv,ugraph =
1813 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1815 subst,metasenv,ugraph,(t::acc))
1816 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1819 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1820 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1821 subst,metasenv,ugraph,t
1822 | Cic.Prod (name,s,t) ->
1823 let ctx = (Some (name,Cic.Decl s))::ctx in
1824 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1825 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1829 (lazy "not well formed constructor type"))
1831 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1832 subst,metasenv,ugraph,(name,ty) :: acc)
1833 cl (subst,metasenv,ugraph,[])
1835 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1836 tys ([],metasenv,ugraph,[])
1838 let substituted_tys =
1840 (fun (name,ind,arity,cl) ->
1842 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1844 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1847 metasenv,ugraph,substituted_tys
1849 let typecheck metasenv uri obj ~localization_tbl =
1850 let ugraph = CicUniv.oblivion_ugraph in
1852 Cic.Constant (name,Some bo,ty,args,attrs) ->
1853 (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
1854 since type_of_aux' destroys localization information (which are
1855 preserved by type_of_aux *)
1858 Cic.CicHash.find localization_tbl bo
1860 HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
1862 let bo',boty,metasenv,ugraph =
1863 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1864 let ty',_,metasenv,ugraph =
1865 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1866 let subst,metasenv,ugraph =
1868 fo_unif_subst [] [] metasenv boty ty' ugraph
1871 | Uncertain _ as exn ->
1874 CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
1876 CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
1877 " but is here used with type " ^
1878 CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
1882 RefineFailure _ -> RefineFailure msg
1883 | Uncertain _ -> Uncertain msg
1886 raise (HExtlib.Localized (loc exn',exn'))
1888 let bo' = CicMetaSubst.apply_subst subst bo' in
1889 let ty' = CicMetaSubst.apply_subst subst ty' in
1890 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1891 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1892 | Cic.Constant (name,None,ty,args,attrs) ->
1893 let ty',_,metasenv,ugraph =
1894 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1896 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1897 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1898 assert (metasenv' = metasenv);
1899 (* Here we do not check the metasenv for correctness *)
1900 let bo',boty,metasenv,ugraph =
1901 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1902 let ty',sort,metasenv,ugraph =
1903 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1907 (* instead of raising Uncertain, let's hope that the meta will become
1910 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1912 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1913 let bo' = CicMetaSubst.apply_subst subst bo' in
1914 let ty' = CicMetaSubst.apply_subst subst ty' in
1915 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1916 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1917 | Cic.Variable _ -> assert false (* not implemented *)
1918 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1919 (*CSC: this code is greately simplified and many many checks are missing *)
1920 (*CSC: e.g. the constructors are not required to build their own types, *)
1921 (*CSC: the arities are not required to have as type a sort, etc. *)
1922 let uri = match uri with Some uri -> uri | None -> assert false in
1923 let typesno = List.length tys in
1924 (* first phase: we fix only the types *)
1925 let metasenv,ugraph,tys =
1927 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1928 let ty',_,metasenv,ugraph =
1929 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1931 metasenv,ugraph,(name,b,ty',cl)::res
1932 ) tys (metasenv,ugraph,[]) in
1934 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1935 (* second phase: we fix only the constructors *)
1936 let saved_menv = metasenv in
1937 let metasenv,ugraph,tys =
1939 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1940 let metasenv,ugraph,cl' =
1942 (fun (name,ty) (metasenv,ugraph,res) ->
1944 CicTypeChecker.debrujin_constructor
1945 ~cb:(relocalize localization_tbl) uri typesno [] ty in
1946 let ty',_,metasenv,ugraph =
1947 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1948 let ty' = undebrujin uri typesno tys ty' in
1949 metasenv@saved_menv,ugraph,(name,ty')::res
1950 ) cl (metasenv,ugraph,[])
1952 metasenv,ugraph,(name,b,ty,cl')::res
1953 ) tys (metasenv,ugraph,[]) in
1954 (* third phase: we check the positivity condition *)
1955 let metasenv,ugraph,tys =
1956 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1958 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1961 (* sara' piu' veloce che raffinare da zero? mah.... *)
1962 let pack_coercion metasenv ctx t =
1963 let module C = Cic in
1964 let rec merge_coercions ctx =
1965 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1967 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1968 | C.Meta (n,subst) ->
1971 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1974 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1975 | C.Prod (name,so,dest) ->
1976 let ctx' = (Some (name,C.Decl so))::ctx in
1977 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1978 | C.Lambda (name,so,dest) ->
1979 let ctx' = (Some (name,C.Decl so))::ctx in
1980 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1981 | C.LetIn (name,so,ty,dest) ->
1982 let ctx' = Some (name,(C.Def (so,ty)))::ctx in
1984 (name, merge_coercions ctx so, merge_coercions ctx ty,
1985 merge_coercions ctx' dest)
1987 let l = List.map (merge_coercions ctx) l in
1989 let b,_,_,_,_ = is_a_double_coercion t in
1991 let ugraph = CicUniv.oblivion_ugraph in
1992 let old_insert_coercions = !insert_coercions in
1993 insert_coercions := false;
1994 let newt, _, menv, _ =
1996 type_of_aux' metasenv ctx t ugraph
1997 with RefineFailure _ | Uncertain _ ->
2000 insert_coercions := old_insert_coercions;
2001 if metasenv <> [] || menv = [] then
2004 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
2007 | C.Var (uri,exp_named_subst) ->
2008 let exp_named_subst = List.map aux exp_named_subst in
2009 C.Var (uri, exp_named_subst)
2010 | C.Const (uri,exp_named_subst) ->
2011 let exp_named_subst = List.map aux exp_named_subst in
2012 C.Const (uri, exp_named_subst)
2013 | C.MutInd (uri,tyno,exp_named_subst) ->
2014 let exp_named_subst = List.map aux exp_named_subst in
2015 C.MutInd (uri,tyno,exp_named_subst)
2016 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
2017 let exp_named_subst = List.map aux exp_named_subst in
2018 C.MutConstruct (uri,tyno,consno,exp_named_subst)
2019 | C.MutCase (uri,tyno,out,te,pl) ->
2020 let pl = List.map (merge_coercions ctx) pl in
2021 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
2022 | C.Fix (fno, fl) ->
2025 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2030 (fun (name,idx,ty,bo) ->
2031 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
2035 | C.CoFix (fno, fl) ->
2038 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2043 (fun (name,ty,bo) ->
2044 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
2049 merge_coercions ctx t
2052 let pack_coercion_metasenv conjectures = conjectures (*
2054 TASSI: this code war written when coercions were a toy,
2055 now packing coercions involves unification thus
2056 the metasenv may change, and this pack coercion
2057 does not handle that.
2059 let module C = Cic in
2061 (fun (i, ctx, ty) ->
2067 Some (name, C.Decl t) ->
2068 Some (name, C.Decl (pack_coercion conjectures ctx t))
2069 | Some (name, C.Def (t,None)) ->
2070 Some (name,C.Def (pack_coercion conjectures ctx t,None))
2071 | Some (name, C.Def (t,Some ty)) ->
2072 Some (name, C.Def (pack_coercion conjectures ctx t,
2073 Some (pack_coercion conjectures ctx ty)))
2079 ((i,ctx,pack_coercion conjectures ctx ty))
2084 let pack_coercion_obj obj = obj (*
2086 TASSI: this code war written when coercions were a toy,
2087 now packing coercions involves unification thus
2088 the metasenv may change, and this pack coercion
2089 does not handle that.
2091 let module C = Cic in
2093 | C.Constant (id, body, ty, params, attrs) ->
2097 | Some body -> Some (pack_coercion [] [] body)
2099 let ty = pack_coercion [] [] ty in
2100 C.Constant (id, body, ty, params, attrs)
2101 | C.Variable (name, body, ty, params, attrs) ->
2105 | Some body -> Some (pack_coercion [] [] body)
2107 let ty = pack_coercion [] [] ty in
2108 C.Variable (name, body, ty, params, attrs)
2109 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2110 let conjectures = pack_coercion_metasenv conjectures in
2111 let body = pack_coercion conjectures [] body in
2112 let ty = pack_coercion conjectures [] ty in
2113 C.CurrentProof (name, conjectures, body, ty, params, attrs)
2114 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2117 (fun (name, ind, arity, cl) ->
2118 let arity = pack_coercion [] [] arity in
2120 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2122 (name, ind, arity, cl))
2125 C.InductiveDefinition (indtys, params, leftno, attrs) *)
2130 let type_of_aux' metasenv context term =
2133 type_of_aux' metasenv context term in
2135 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2137 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2140 | RefineFailure msg as e ->
2141 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2143 | Uncertain msg as e ->
2144 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2148 let profiler2 = HExtlib.profile "CicRefine"
2150 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2151 profiler2.HExtlib.profile
2152 (type_of_aux' ?localization_tbl metasenv context term) ugraph
2154 let typecheck ~localization_tbl metasenv uri obj =
2155 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2157 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2158 (* vim:set foldmethod=marker: *)