1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
30 exception RefineFailure of string Lazy.t;;
31 exception Uncertain of string Lazy.t;;
32 exception AssertFailure of string Lazy.t;;
34 let insert_coercions = ref true
35 let pack_coercions = ref true
37 let debug_print = fun _ -> ();;
38 (*let debug_print x = prerr_endline (Lazy.force x);;*)
40 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
42 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
45 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
46 in profiler_eat_prods2.HExtlib.profile foo ()
48 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
49 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
52 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
54 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
57 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
58 in profiler_eat_prods.HExtlib.profile foo ()
60 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
61 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
64 let profiler = HExtlib.profile "CicRefine.fo_unif"
66 let fo_unif_subst subst context metasenv t1 t2 ugraph =
69 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
70 in profiler.HExtlib.profile foo ()
72 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
73 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
76 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
79 RefineFailure msg -> RefineFailure (f msg)
80 | Uncertain msg -> Uncertain (f msg)
81 | Sys.Break -> raise exn
82 | _ -> assert false in
85 Cic.CicHash.find localization_tbl t
87 prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
90 raise (HExtlib.Localized (loc,exn'))
92 let relocalize localization_tbl oldt newt =
94 let infos = Cic.CicHash.find localization_tbl oldt in
95 Cic.CicHash.remove localization_tbl oldt;
96 Cic.CicHash.add localization_tbl newt infos;
104 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
105 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
108 let exp_impl metasenv subst context =
111 let (metasenv', idx) =
112 CicMkImplicit.mk_implicit_type metasenv subst context in
114 CicMkImplicit.identity_relocation_list_for_metavariable context in
115 metasenv', Cic.Meta (idx, irl)
117 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
118 metasenv', Cic.Meta (idx, [])
120 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
122 CicMkImplicit.identity_relocation_list_for_metavariable context in
123 metasenv', Cic.Meta (idx, irl)
127 let is_a_double_coercion t =
129 let rec aux acc = function
131 | x::tl -> aux (acc@[x]) tl
136 let imp = Cic.Implicit None in
137 let dummyres = false,imp, imp,imp,imp in
139 | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 ->
140 (match last_of tl with
141 | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
142 let sib2,head = last_of tl2 in
143 true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
148 let more_args_than_expected
149 localization_tbl metasenv subst he context hetype' tlbody_and_type exn
153 CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
154 " (that has type "^CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
155 ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
156 " arguments that are more than expected")
158 enrich localization_tbl he ~f:(fun _-> msg) exn
161 let mk_prod_of_metas metasenv context' subst args =
162 let rec mk_prod metasenv context' = function
164 let (metasenv, idx) =
165 CicMkImplicit.mk_implicit_type metasenv subst context'
168 CicMkImplicit.identity_relocation_list_for_metavariable context'
170 metasenv,Cic.Meta (idx, irl)
172 let (metasenv, idx) =
173 CicMkImplicit.mk_implicit_type metasenv subst context'
176 CicMkImplicit.identity_relocation_list_for_metavariable context'
178 let meta = Cic.Meta (idx,irl) in
180 (* The name must be fresh for context. *)
181 (* Nevertheless, argty is well-typed only in context. *)
182 (* Thus I generate a name (name_hint) in context and *)
183 (* then I generate a name --- using the hint name_hint *)
184 (* --- that is fresh in context'. *)
186 (* Cic.Name "pippo" *)
187 FreshNamesGenerator.mk_fresh_name ~subst metasenv
188 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
189 (CicMetaSubst.apply_subst_context subst context')
191 ~typ:(CicMetaSubst.apply_subst subst argty)
193 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
194 FreshNamesGenerator.mk_fresh_name ~subst
195 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
197 let metasenv,target =
198 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
200 metasenv,Cic.Prod (name,meta,target)
202 mk_prod metasenv context' args
205 let rec type_of_constant uri ugraph =
206 let module C = Cic in
207 let module R = CicReduction in
208 let module U = UriManager in
209 let _ = CicTypeChecker.typecheck uri in
212 CicEnvironment.get_cooked_obj ugraph uri
213 with Not_found -> assert false
216 C.Constant (_,_,ty,_,_) -> ty,u
217 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
221 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
223 and type_of_variable uri ugraph =
224 let module C = Cic in
225 let module R = CicReduction in
226 let module U = UriManager in
227 let _ = CicTypeChecker.typecheck uri in
230 CicEnvironment.get_cooked_obj ugraph uri
231 with Not_found -> assert false
234 C.Variable (_,_,ty,_,_) -> ty,u
238 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
240 and type_of_mutual_inductive_defs uri i ugraph =
241 let module C = Cic in
242 let module R = CicReduction in
243 let module U = UriManager in
244 let _ = CicTypeChecker.typecheck uri in
247 CicEnvironment.get_cooked_obj ugraph uri
248 with Not_found -> assert false
251 C.InductiveDefinition (dl,_,_,_) ->
252 let (_,_,arity,_) = List.nth dl i in
257 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
259 and type_of_mutual_inductive_constr uri i j ugraph =
260 let module C = Cic in
261 let module R = CicReduction in
262 let module U = UriManager in
263 let _ = CicTypeChecker.typecheck uri in
266 CicEnvironment.get_cooked_obj ugraph uri
267 with Not_found -> assert false
270 C.InductiveDefinition (dl,_,_,_) ->
271 let (_,_,_,cl) = List.nth dl i in
272 let (_,ty) = List.nth cl (j-1) in
278 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
281 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
283 (* the check_branch function checks if a branch of a case is refinable.
284 It returns a pair (outype_instance,args), a subst and a metasenv.
285 outype_instance is the expected result of applying the case outtype
287 The problem is that outype is in general unknown, and we should
288 try to synthesize it from the above information, that is in general
289 a second order unification problem. *)
291 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
292 let module C = Cic in
293 (* let module R = CicMetaSubst in *)
294 let module R = CicReduction in
295 match R.whd ~subst context expectedtype with
297 (n,context,actualtype, [term]), subst, metasenv, ugraph
298 | C.Appl (C.MutInd (_,_,_)::tl) ->
299 let (_,arguments) = split tl left_args_no in
300 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
301 | C.Prod (name,so,de) ->
302 (* we expect that the actual type of the branch has the due
304 (match R.whd ~subst context actualtype with
305 C.Prod (name',so',de') ->
306 let subst, metasenv, ugraph1 =
307 fo_unif_subst subst context metasenv so so' ugraph in
309 (match CicSubstitution.lift 1 term with
310 C.Appl l -> C.Appl (l@[C.Rel 1])
311 | t -> C.Appl [t ; C.Rel 1]) in
312 (* we should also check that the name variable is anonymous in
313 the actual type de' ?? *)
315 ((Some (name,(C.Decl so)))::context)
316 metasenv subst left_args_no de' term' de ugraph1
317 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
318 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
320 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
323 let rec type_of_aux subst metasenv context t ugraph =
324 let module C = Cic in
325 let module S = CicSubstitution in
326 let module U = UriManager in
327 let try_coercion t subst metasenv context ugraph coercion_tgt c =
330 C.Appl l2 -> C.Appl (l2@[t])
334 let newt,_,subst,metasenv,ugraph =
335 type_of_aux subst metasenv context coerced ugraph
337 let newt, tty, subst, metasenv, ugraph =
338 avoid_double_coercion context subst metasenv ugraph newt coercion_tgt
340 Some (newt, tty, subst, metasenv, ugraph)
342 | RefineFailure _ | Uncertain _ -> None
344 let (t',_,_,_,_) as res =
349 match List.nth context (n - 1) with
350 Some (_,C.Decl ty) ->
351 t,S.lift n ty,subst,metasenv, ugraph
352 | Some (_,C.Def (_,Some ty)) ->
353 t,S.lift n ty,subst,metasenv, ugraph
354 | Some (_,C.Def (bo,None)) ->
356 (* if it is in the context it must be already well-typed*)
357 CicTypeChecker.type_of_aux' ~subst metasenv context
360 t,ty,subst,metasenv,ugraph
362 enrich localization_tbl t
363 (RefineFailure (lazy "Rel to hidden hypothesis"))
366 enrich localization_tbl t
367 (RefineFailure (lazy "Not a closed term")))
368 | C.Var (uri,exp_named_subst) ->
369 let exp_named_subst',subst',metasenv',ugraph1 =
370 check_exp_named_subst
371 subst metasenv context exp_named_subst ugraph
373 let ty_uri,ugraph1 = type_of_variable uri ugraph in
375 CicSubstitution.subst_vars exp_named_subst' ty_uri
377 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
380 let (canonical_context, term,ty) =
381 CicUtil.lookup_subst n subst
383 let l',subst',metasenv',ugraph1 =
384 check_metasenv_consistency n subst metasenv context
385 canonical_context l ugraph
387 (* trust or check ??? *)
388 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
389 subst', metasenv', ugraph1
390 (* type_of_aux subst metasenv
391 context (CicSubstitution.subst_meta l term) *)
392 with CicUtil.Subst_not_found _ ->
393 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
394 let l',subst',metasenv', ugraph1 =
395 check_metasenv_consistency n subst metasenv context
396 canonical_context l ugraph
398 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
399 subst', metasenv',ugraph1)
400 | C.Sort (C.Type tno) ->
401 let tno' = CicUniv.fresh() in
403 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
404 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
406 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
408 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
409 | C.Implicit infos ->
410 let metasenv',t' = exp_impl metasenv subst context infos in
411 type_of_aux subst metasenv' context t' ugraph
413 let ty',_,subst',metasenv',ugraph1 =
414 type_of_aux subst metasenv context ty ugraph
416 let te',inferredty,subst'',metasenv'',ugraph2 =
417 type_of_aux subst' metasenv' context te ugraph1
420 let subst''',metasenv''',ugraph3 =
421 fo_unif_subst subst'' context metasenv''
422 inferredty ty' ugraph2
424 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
427 enrich localization_tbl te'
430 CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
431 context ^ " has type " ^
432 CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty
433 context ^ " but is here used with type " ^
434 CicMetaSubst.ppterm_in_context metasenv'' subst'' ty' context)) exn
436 | C.Prod (name,s,t) ->
437 let carr t subst context = CicMetaSubst.apply_subst subst t in
438 let coerce_to_sort in_source tgt_sort t type_to_coerce
439 subst context metasenv uragph
441 if not !insert_coercions then
442 t,type_to_coerce,subst,metasenv,ugraph
444 let coercion_src = carr type_to_coerce subst context in
445 match coercion_src with
447 t,type_to_coerce,subst,metasenv,ugraph
448 | Cic.Meta _ as meta ->
449 t, meta, subst, metasenv, ugraph
450 | Cic.Cast _ as cast ->
451 t, cast, subst, metasenv, ugraph
453 let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
455 CoercGraph.look_for_coercion coercion_src coercion_tgt
458 | CoercGraph.NoCoercion
459 | CoercGraph.NotHandled _ ->
460 enrich localization_tbl t
463 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
464 " is not a type since it has type " ^
465 CicMetaSubst.ppterm_in_context ~metasenv
466 subst coercion_src context ^ " that is not a sort")))
467 | CoercGraph.NotMetaClosed ->
468 enrich localization_tbl t
471 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
472 " is not a type since it has type " ^
473 CicMetaSubst.ppterm_in_context ~metasenv
474 subst coercion_src context ^ " that is not a sort")))
475 | CoercGraph.SomeCoercion candidates ->
479 t subst metasenv context ugraph coercion_tgt)
485 enrich localization_tbl t
488 CicMetaSubst.ppterm_in_context ~metasenv
490 " is not a type since it has type " ^
491 CicMetaSubst.ppterm_in_context ~metasenv
492 subst coercion_src context ^
493 " that is not a sort"))))
495 let s',sort1,subst',metasenv',ugraph1 =
496 type_of_aux subst metasenv context s ugraph
498 let s',sort1,subst', metasenv',ugraph1 =
499 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
500 s' sort1 subst' context metasenv' ugraph1
502 let context_for_t = ((Some (name,(C.Decl s')))::context) in
503 let t',sort2,subst'',metasenv'',ugraph2 =
504 type_of_aux subst' metasenv'
505 context_for_t t ugraph1
507 let t',sort2,subst'',metasenv'',ugraph2 =
508 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
509 t' sort2 subst'' context_for_t metasenv'' ugraph2
511 let sop,subst''',metasenv''',ugraph3 =
512 sort_of_prod localization_tbl subst'' metasenv''
513 context (name,s') t' (sort1,sort2) ugraph2
515 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
516 | C.Lambda (n,s,t) ->
518 let s',sort1,subst',metasenv',ugraph1 =
519 type_of_aux subst metasenv context s ugraph in
520 let s',sort1,subst',metasenv',ugraph1 =
521 if not !insert_coercions then
522 s',sort1, subst', metasenv', ugraph1
524 match CicReduction.whd ~subst:subst' context sort1 with
525 | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
527 let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
529 CoercGraph.look_for_coercion coercion_src coercion_tgt
532 | CoercGraph.NoCoercion
533 | CoercGraph.NotHandled _ ->
534 enrich localization_tbl s'
537 CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
538 " is not a type since it has type " ^
539 CicMetaSubst.ppterm_in_context ~metasenv
540 subst coercion_src context ^ " that is not a sort")))
541 | CoercGraph.NotMetaClosed ->
542 enrich localization_tbl s'
545 CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
546 " is not a type since it has type " ^
547 CicMetaSubst.ppterm_in_context ~metasenv
548 subst coercion_src context ^ " that is not a sort")))
549 | CoercGraph.SomeCoercion candidates ->
553 s' subst' metasenv' context ugraph1 coercion_tgt)
559 enrich localization_tbl s'
562 CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
563 " is not a type since it has type " ^
564 CicMetaSubst.ppterm_in_context ~metasenv
565 subst coercion_src context ^
566 " that is not a sort")))
568 let context_for_t = ((Some (n,(C.Decl s')))::context) in
569 let t',type2,subst'',metasenv'',ugraph2 =
570 type_of_aux subst' metasenv' context_for_t t ugraph1
572 C.Lambda (n,s',t'),C.Prod (n,s',type2),
573 subst'',metasenv'',ugraph2
575 (* only to check if s is well-typed *)
576 let s',ty,subst',metasenv',ugraph1 =
577 type_of_aux subst metasenv context s ugraph
579 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
581 let t',inferredty,subst'',metasenv'',ugraph2 =
582 type_of_aux subst' metasenv'
583 context_for_t t ugraph1
585 (* One-step LetIn reduction.
586 * Even faster than the previous solution.
587 * Moreover the inferred type is closer to the expected one.
590 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
591 subst'',metasenv'',ugraph2
592 | C.Appl (he::((_::_) as tl)) ->
593 let he',hetype,subst',metasenv',ugraph1 =
594 type_of_aux subst metasenv context he ugraph
596 let tlbody_and_type,subst'',metasenv'',ugraph2 =
597 typeof_list subst' metasenv' context ugraph1 tl
599 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
600 eat_prods true subst'' metasenv'' context
601 he' hetype tlbody_and_type ugraph2
603 let newappl = (C.Appl (coerced_he::coerced_args)) in
604 avoid_double_coercion
605 context subst''' metasenv''' ugraph3 newappl applty
606 | C.Appl _ -> assert false
607 | C.Const (uri,exp_named_subst) ->
608 let exp_named_subst',subst',metasenv',ugraph1 =
609 check_exp_named_subst subst metasenv context
610 exp_named_subst ugraph in
611 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
613 CicSubstitution.subst_vars exp_named_subst' ty_uri
615 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
616 | C.MutInd (uri,i,exp_named_subst) ->
617 let exp_named_subst',subst',metasenv',ugraph1 =
618 check_exp_named_subst subst metasenv context
619 exp_named_subst ugraph
621 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
623 CicSubstitution.subst_vars exp_named_subst' ty_uri in
624 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
625 | C.MutConstruct (uri,i,j,exp_named_subst) ->
626 let exp_named_subst',subst',metasenv',ugraph1 =
627 check_exp_named_subst subst metasenv context
628 exp_named_subst ugraph
631 type_of_mutual_inductive_constr uri i j ugraph1
634 CicSubstitution.subst_vars exp_named_subst' ty_uri
636 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
638 | C.MutCase (uri, i, outtype, term, pl) ->
639 (* first, get the inductive type (and noparams)
640 * in the environment *)
641 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
642 let _ = CicTypeChecker.typecheck uri in
643 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
645 C.InductiveDefinition (l,expl_params,parsno,_) ->
646 List.nth l i , expl_params, parsno, u
648 enrich localization_tbl t
650 (lazy ("Unkown mutual inductive definition " ^
651 U.string_of_uri uri)))
653 let rec count_prod t =
654 match CicReduction.whd ~subst context t with
655 C.Prod (_, _, t) -> 1 + (count_prod t)
658 let no_args = count_prod arity in
659 (* now, create a "generic" MutInd *)
660 let metasenv,left_args =
661 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
663 let metasenv,right_args =
664 let no_right_params = no_args - no_left_params in
665 if no_right_params < 0 then assert false
666 else CicMkImplicit.n_fresh_metas
667 metasenv subst context no_right_params
669 let metasenv,exp_named_subst =
670 CicMkImplicit.fresh_subst metasenv subst context expl_params in
673 C.MutInd (uri,i,exp_named_subst)
676 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
678 (* check consistency with the actual type of term *)
679 let term',actual_type,subst,metasenv,ugraph1 =
680 type_of_aux subst metasenv context term ugraph in
681 let expected_type',_, subst, metasenv,ugraph2 =
682 type_of_aux subst metasenv context expected_type ugraph1
684 let actual_type = CicReduction.whd ~subst context actual_type in
685 let subst,metasenv,ugraph3 =
687 fo_unif_subst subst context metasenv
688 expected_type' actual_type ugraph2
691 enrich localization_tbl term' exn
694 CicMetaSubst.ppterm_in_context ~metasenv subst term'
695 context ^ " has type " ^
696 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
697 context ^ " but is here used with type " ^
698 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
700 let rec instantiate_prod t =
704 match CicReduction.whd ~subst context t with
706 instantiate_prod (CicSubstitution.subst he t') tl
709 let arity_instantiated_with_left_args =
710 instantiate_prod arity left_args in
711 (* TODO: check if the sort elimination
712 * is allowed: [(I q1 ... qr)|B] *)
713 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
715 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
717 if left_args = [] then
718 (C.MutConstruct (uri,i,j,exp_named_subst))
721 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
723 let p',actual_type,subst,metasenv,ugraph1 =
724 type_of_aux subst metasenv context p ugraph
726 let constructor',expected_type, subst, metasenv,ugraph2 =
727 type_of_aux subst metasenv context constructor ugraph1
729 let outtypeinstance,subst,metasenv,ugraph3 =
730 check_branch 0 context metasenv subst no_left_params
731 actual_type constructor' expected_type ugraph2
734 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
735 ([],1,[],subst,metasenv,ugraph3) pl
738 (* we are left to check that the outype matches his instances.
739 The easy case is when the outype is specified, that amount
740 to a trivial check. Otherwise, we should guess a type from
744 let outtype,outtypety, subst, metasenv,ugraph4 =
745 type_of_aux subst metasenv context outtype ugraph4 in
748 (let candidate,ugraph5,metasenv,subst =
749 let exp_name_subst, metasenv =
751 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
753 let uris = CicUtil.params_of_obj o in
755 fun uri (acc,metasenv) ->
756 let metasenv',new_meta =
757 CicMkImplicit.mk_implicit metasenv subst context
760 CicMkImplicit.identity_relocation_list_for_metavariable
763 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
767 match left_args,right_args with
768 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
770 let rec mk_right_args =
773 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
775 let right_args_no = List.length right_args in
776 let lifted_left_args =
777 List.map (CicSubstitution.lift right_args_no) left_args
779 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
780 (lifted_left_args @ mk_right_args right_args_no))
783 FreshNamesGenerator.mk_fresh_name ~subst metasenv
784 context Cic.Anonymous ~typ:ty
786 match outtypeinstances with
788 let extended_context =
789 let rec add_right_args =
791 Cic.Prod (name,ty,t) ->
792 Some (name,Cic.Decl ty)::(add_right_args t)
795 (Some (fresh_name,Cic.Decl ty))::
797 (add_right_args arity_instantiated_with_left_args))@
800 let metasenv,new_meta =
801 CicMkImplicit.mk_implicit metasenv subst extended_context
804 CicMkImplicit.identity_relocation_list_for_metavariable
807 let rec add_lambdas b =
809 Cic.Prod (name,ty,t) ->
810 Cic.Lambda (name,ty,(add_lambdas b t))
811 | _ -> Cic.Lambda (fresh_name, ty, b)
814 add_lambdas (Cic.Meta (new_meta,irl))
815 arity_instantiated_with_left_args
817 (Some candidate),ugraph4,metasenv,subst
818 | (constructor_args_no,_,instance,_)::tl ->
820 let instance',subst,metasenv =
821 CicMetaSubst.delift_rels subst metasenv
822 constructor_args_no instance
824 let candidate,ugraph,metasenv,subst =
826 fun (candidate_oty,ugraph,metasenv,subst)
827 (constructor_args_no,_,instance,_) ->
828 match candidate_oty with
829 | None -> None,ugraph,metasenv,subst
832 let instance',subst,metasenv =
833 CicMetaSubst.delift_rels subst metasenv
834 constructor_args_no instance
836 let subst,metasenv,ugraph =
837 fo_unif_subst subst context metasenv
840 candidate_oty,ugraph,metasenv,subst
842 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
843 | CicUnification.UnificationFailure _
844 | CicUnification.Uncertain _ ->
845 None,ugraph,metasenv,subst
846 ) (Some instance',ugraph4,metasenv,subst) tl
849 | None -> None, ugraph,metasenv,subst
851 let rec add_lambdas n b =
853 Cic.Prod (name,ty,t) ->
854 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
856 Cic.Lambda (fresh_name, ty,
857 CicSubstitution.lift (n + 1) t)
860 (add_lambdas 0 t arity_instantiated_with_left_args),
861 ugraph,metasenv,subst
862 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
863 None,ugraph4,metasenv,subst
866 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
868 let subst,metasenv,ugraph =
870 fo_unif_subst subst context metasenv
871 candidate outtype ugraph5
873 exn -> assert false(* unification against a metavariable *)
875 C.MutCase (uri, i, outtype, term', pl'),
876 CicReduction.head_beta_reduce
877 (CicMetaSubst.apply_subst subst
878 (Cic.Appl (outtype::right_args@[term']))),
879 subst,metasenv,ugraph)
880 | _ -> (* easy case *)
881 let tlbody_and_type,subst,metasenv,ugraph4 =
882 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
884 let _,_,_,subst,metasenv,ugraph4 =
885 eat_prods false subst metasenv context
886 outtype outtypety tlbody_and_type ugraph4
888 let _,_, subst, metasenv,ugraph5 =
889 type_of_aux subst metasenv context
890 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
892 let (subst,metasenv,ugraph6) =
894 (fun (subst,metasenv,ugraph)
895 p (constructor_args_no,context,instance,args)
900 CicSubstitution.lift constructor_args_no outtype
902 C.Appl (outtype'::args)
904 CicReduction.whd ~subst context appl
907 fo_unif_subst subst context metasenv instance instance'
911 enrich localization_tbl p exn
914 CicMetaSubst.ppterm_in_context ~metasenv subst p
915 context ^ " has type " ^
916 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
917 context ^ " but is here used with type " ^
918 CicMetaSubst.ppterm_in_context ~metasenv subst instance
920 (subst,metasenv,ugraph5) pl' outtypeinstances
922 C.MutCase (uri, i, outtype, term', pl'),
923 CicReduction.head_beta_reduce
924 (CicMetaSubst.apply_subst subst
925 (C.Appl(outtype::right_args@[term]))),
926 subst,metasenv,ugraph6)
928 let fl_ty',subst,metasenv,types,ugraph1 =
930 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
931 let ty',_,subst',metasenv',ugraph1 =
932 type_of_aux subst metasenv context ty ugraph
934 fl @ [ty'],subst',metasenv',
935 Some (C.Name n,(C.Decl ty')) :: types, ugraph
936 ) ([],subst,metasenv,[],ugraph) fl
938 let len = List.length types in
939 let context' = types@context in
940 let fl_bo',subst,metasenv,ugraph2 =
942 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
943 let bo',ty_of_bo,subst,metasenv,ugraph1 =
944 type_of_aux subst metasenv context' bo ugraph in
945 let expected_ty = CicSubstitution.lift len ty in
946 let subst',metasenv',ugraph' =
948 fo_unif_subst subst context' metasenv
949 ty_of_bo expected_ty ugraph1
952 enrich localization_tbl bo exn
955 CicMetaSubst.ppterm_in_context ~metasenv subst bo
956 context' ^ " has type " ^
957 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
958 context' ^ " but is here used with type " ^
959 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
962 fl @ [bo'] , subst',metasenv',ugraph'
963 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
965 let ty = List.nth fl_ty' i in
966 (* now we have the new ty in fl_ty', the new bo in fl_bo',
967 * and we want the new fl with bo' and ty' injected in the right
970 let rec map3 f l1 l2 l3 =
973 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
976 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
979 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
981 let fl_ty',subst,metasenv,types,ugraph1 =
983 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
984 let ty',_,subst',metasenv',ugraph1 =
985 type_of_aux subst metasenv context ty ugraph
987 fl @ [ty'],subst',metasenv',
988 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
989 ) ([],subst,metasenv,[],ugraph) fl
991 let len = List.length types in
992 let context' = types@context in
993 let fl_bo',subst,metasenv,ugraph2 =
995 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
996 let bo',ty_of_bo,subst,metasenv,ugraph1 =
997 type_of_aux subst metasenv context' bo ugraph in
998 let expected_ty = CicSubstitution.lift len ty in
999 let subst',metasenv',ugraph' =
1001 fo_unif_subst subst context' metasenv
1002 ty_of_bo expected_ty ugraph1
1005 enrich localization_tbl bo exn
1008 CicMetaSubst.ppterm_in_context ~metasenv subst bo
1009 context' ^ " has type " ^
1010 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
1011 context' ^ " but is here used with type " ^
1012 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
1015 fl @ [bo'],subst',metasenv',ugraph'
1016 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
1018 let ty = List.nth fl_ty' i in
1019 (* now we have the new ty in fl_ty', the new bo in fl_bo',
1020 * and we want the new fl with bo' and ty' injected in the right
1023 let rec map3 f l1 l2 l3 =
1026 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
1029 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
1032 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
1034 relocalize localization_tbl t t';
1037 (* check_metasenv_consistency checks that the "canonical" context of a
1038 metavariable is consitent - up to relocation via the relocation list l -
1039 with the actual context *)
1040 and check_metasenv_consistency
1041 metano subst metasenv context canonical_context l ugraph
1043 let module C = Cic in
1044 let module R = CicReduction in
1045 let module S = CicSubstitution in
1046 let lifted_canonical_context =
1050 | (Some (n,C.Decl t))::tl ->
1051 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
1052 | (Some (n,C.Def (t,None)))::tl ->
1053 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1054 | None::tl -> None::(aux (i+1) tl)
1055 | (Some (n,C.Def (t,Some ty)))::tl ->
1057 C.Def ((S.subst_meta l (S.lift i t)),
1058 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
1060 aux 1 canonical_context
1064 (fun (l,subst,metasenv,ugraph) t ct ->
1067 l @ [None],subst,metasenv,ugraph
1068 | Some t,Some (_,C.Def (ct,_)) ->
1069 let subst',metasenv',ugraph' =
1071 prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
1072 fo_unif_subst subst context metasenv t ct ugraph
1073 with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
1075 l @ [Some t],subst',metasenv',ugraph'
1076 | Some t,Some (_,C.Decl ct) ->
1077 let t',inferredty,subst',metasenv',ugraph1 =
1078 type_of_aux subst metasenv context t ugraph
1080 let subst'',metasenv'',ugraph2 =
1083 subst' context metasenv' inferredty ct ugraph1
1084 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))))))
1086 l @ [Some t'], subst'',metasenv'',ugraph2
1088 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
1090 Invalid_argument _ ->
1094 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1095 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1096 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1098 and check_exp_named_subst metasubst metasenv context tl ugraph =
1099 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1101 [] -> [],metasubst,metasenv,ugraph
1103 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1105 CicSubstitution.subst_vars substs ty_uri in
1106 (* CSC: why was this code here? it is wrong
1107 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1108 Cic.Variable (_,Some bo,_,_) ->
1110 (RefineFailure (lazy
1111 "A variable with a body can not be explicit substituted"))
1112 | Cic.Variable (_,None,_,_) -> ()
1115 (RefineFailure (lazy
1116 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1119 let t',typeoft,metasubst',metasenv',ugraph2 =
1120 type_of_aux metasubst metasenv context t ugraph1 in
1121 let subst = uri,t' in
1122 let metasubst'',metasenv'',ugraph3 =
1125 metasubst' context metasenv' typeoft typeofvar ugraph2
1127 raise (RefineFailure (lazy
1128 ("Wrong Explicit Named Substitution: " ^
1129 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1130 " not unifiable with " ^
1131 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1133 (* FIXME: no mere tail recursive! *)
1134 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1135 check_exp_named_subst_aux
1136 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1138 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1140 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1143 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1146 let module C = Cic in
1147 let context_for_t2 = (Some (name,C.Decl s))::context in
1148 let t1'' = CicReduction.whd ~subst context t1 in
1149 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1150 match (t1'', t2'') with
1151 (C.Sort s1, C.Sort s2)
1152 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1153 (* different than Coq manual!!! *)
1154 C.Sort s2,subst,metasenv,ugraph
1155 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1156 let t' = CicUniv.fresh() in
1158 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1159 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1160 C.Sort (C.Type t'),subst,metasenv,ugraph2
1162 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1163 | (C.Sort _,C.Sort (C.Type t1)) ->
1164 C.Sort (C.Type t1),subst,metasenv,ugraph
1165 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1166 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1167 (* TODO how can we force the meta to become a sort? If we don't we
1168 * break the invariant that refine produce only well typed terms *)
1169 (* TODO if we check the non meta term and if it is a sort then we
1170 * are likely to know the exact value of the result e.g. if the rhs
1171 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1172 let (metasenv,idx) =
1173 CicMkImplicit.mk_implicit_sort metasenv subst in
1174 let (subst, metasenv,ugraph1) =
1176 fo_unif_subst subst context_for_t2 metasenv
1177 (C.Meta (idx,[])) t2'' ugraph
1178 with _ -> assert false (* unification against a metavariable *)
1180 t2'',subst,metasenv,ugraph1
1183 enrich localization_tbl s
1187 "%s is supposed to be a type, but its type is %s"
1188 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1189 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1191 enrich localization_tbl t
1195 "%s is supposed to be a type, but its type is %s"
1196 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1197 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1199 and avoid_double_coercion context subst metasenv ugraph t ty =
1200 if not !pack_coercions then
1201 t,ty,subst,metasenv,ugraph
1203 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1205 let source_carr = CoercGraph.source_of c2 in
1206 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1207 (match CoercGraph.look_for_coercion source_carr tgt_carr
1209 | CoercGraph.SomeCoercion candidates ->
1211 HExtlib.list_findopt
1213 | c when not (CoercGraph.is_composite c) ->
1214 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1219 | Cic.Appl l -> Cic.Appl (l @ [head])
1220 | _ -> Cic.Appl [c;head]
1222 debug_print (lazy ("\nprovo" ^ CicPp.ppterm newt));
1227 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
1228 let newt,_,subst,metasenv,ugraph =
1229 type_of_aux subst metasenv context newt ugraph in
1230 debug_print (lazy "tipa...");
1231 let subst, metasenv, ugraph =
1232 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1233 fo_unif_subst subst context metasenv newt t ugraph
1235 debug_print (lazy "unifica...");
1236 Some (newt, ty, subst, metasenv, ugraph)
1238 | RefineFailure s | Uncertain s when not !pack_coercions->
1239 debug_print s; debug_print (lazy "stop\n");None
1240 | RefineFailure s | Uncertain s ->
1241 debug_print s;debug_print (lazy "goon\n");
1243 let old_pack_coercions = !pack_coercions in
1244 pack_coercions := false; (* to avoid diverging *)
1245 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1246 type_of_aux subst metasenv context c1_c2_implicit ugraph
1248 pack_coercions := old_pack_coercions;
1250 is_a_double_coercion refined_c1_c2_implicit
1256 match refined_c1_c2_implicit with
1257 | Cic.Appl l -> HExtlib.list_last l
1260 let subst, metasenv, ugraph =
1261 try fo_unif_subst subst context metasenv
1263 with RefineFailure s| Uncertain s->
1264 debug_print s;assert false
1266 let subst, metasenv, ugraph =
1267 fo_unif_subst subst context metasenv
1268 refined_c1_c2_implicit t ugraph
1270 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1272 | RefineFailure s | Uncertain s ->
1273 pack_coercions := true;debug_print s;None
1274 | exn -> pack_coercions := true; raise exn))
1277 (match selected with
1281 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1282 t, ty, subst, metasenv, ugraph)
1283 | _ -> t, ty, subst, metasenv, ugraph)
1285 t, ty, subst, metasenv, ugraph
1287 and typeof_list subst metasenv context ugraph l =
1288 let tlbody_and_type,subst,metasenv,ugraph =
1290 (fun x (res,subst,metasenv,ugraph) ->
1291 let x',ty,subst',metasenv',ugraph1 =
1292 type_of_aux subst metasenv context x ugraph
1294 (x', ty)::res,subst',metasenv',ugraph1
1295 ) l ([],subst,metasenv,ugraph)
1297 tlbody_and_type,subst,metasenv,ugraph
1300 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1302 (* aux function to add coercions to funclass *)
1303 let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph =
1305 let pristinemenv = metasenv in
1306 let metasenv,hetype' =
1307 mk_prod_of_metas metasenv context subst args_bo_and_ty
1310 let subst,metasenv,ugraph =
1311 fo_unif_subst_eat_prods
1312 subst context metasenv hetype hetype' ugraph
1314 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1315 with RefineFailure s | Uncertain s as exn
1316 when allow_coercions && !insert_coercions ->
1317 (* {{{ we search a coercion of the head (saturated) to funclass *)
1318 let metasenv = pristinemenv in
1320 ("Fixing arity of: "^CicMetaSubst.ppterm ~metasenv subst hetype ^
1321 " since unif failed with: " ^ CicMetaSubst.ppterm ~metasenv subst hetype'
1322 (* ^ " cause: " ^ Lazy.force s *)));
1323 let how_many_args_are_needed =
1324 let rec aux n = function
1325 | Cic.Prod(_,_,t) -> aux (n+1) t
1328 aux 0 (CicMetaSubst.apply_subst subst hetype)
1330 let args, remainder =
1331 HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
1333 let args = List.map fst args in
1337 | Cic.Appl l -> Cic.Appl (l@args)
1338 | _ -> Cic.Appl (he::args)
1342 let x,xty,subst,metasenv,ugraph =
1343 type_of_aux subst metasenv context x ugraph
1346 CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty)
1348 let carr_tgt = CoercDb.Fun 0 in
1349 match CoercGraph.look_for_coercion' carr_src carr_tgt with
1350 | CoercGraph.NoCoercion
1351 | CoercGraph.NotMetaClosed
1352 | CoercGraph.NotHandled _ -> raise exn
1353 | CoercGraph.SomeCoercion candidates ->
1355 HExtlib.list_findopt
1357 let t = Cic.Appl [coerc;x] in
1358 debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst t));
1360 (* we want this to be available in the error handler fo the
1361 * following (so it has its own try. *)
1362 let t,tty,subst,metasenv,ugraph =
1363 type_of_aux subst metasenv context t ugraph
1366 let metasenv, hetype' =
1367 mk_prod_of_metas metasenv context subst remainder
1370 (" unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^
1371 CicMetaSubst.ppterm ~metasenv subst hetype'));
1372 let subst,metasenv,ugraph =
1373 fo_unif_subst_eat_prods
1374 subst context metasenv tty hetype' ugraph
1376 debug_print (lazy " success!");
1377 Some (subst,metasenv,ugraph,tty,t,remainder)
1379 | Uncertain _ | RefineFailure _
1380 | CicUnification.UnificationFailure _
1381 | CicUnification.Uncertain _ ->
1383 let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
1385 metasenv context subst t tty remainder ugraph
1387 Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
1388 with Uncertain _ | RefineFailure _ -> None
1389 with Uncertain _ | RefineFailure _ -> None
1390 | exn -> assert false) (* ritornare None, e' un localized *)
1393 | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
1394 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1396 more_args_than_expected localization_tbl metasenv
1397 subst he context hetype args_bo_and_ty exn
1398 (* }}} end coercion to funclass stuff *)
1399 (* }}} end fix_arity *)
1401 (* aux function to process the type of the head and the args in parallel *)
1402 let rec eat_prods_and_args
1403 pristinemenv metasenv subst context pristinehe he hetype ugraph newargs
1407 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1408 | (hete, hety)::tl ->
1409 match (CicReduction.whd ~subst context hetype) with
1410 | Cic.Prod (n,s,t) ->
1411 let arg,subst,metasenv,ugraph1 =
1413 let subst,metasenv,ugraph1 =
1414 fo_unif_subst_eat_prods2
1415 subst context metasenv hety s ugraph
1417 (hete,hety),subst,metasenv,ugraph1
1418 (* {{{ we search a coercion from hety to s if fails *)
1419 with RefineFailure _ | Uncertain _ as exn
1420 when allow_coercions && !insert_coercions ->
1421 let coer, tgt_carr =
1422 let carr t subst context =
1423 CicReduction.whd ~delta:false
1424 context (CicMetaSubst.apply_subst subst t )
1426 let c_hety = carr hety subst context in
1427 let c_s = carr s subst context in
1428 CoercGraph.look_for_coercion c_hety c_s, c_s
1431 | CoercGraph.NoCoercion
1432 | CoercGraph.NotHandled _ ->
1433 enrich localization_tbl hete exn
1435 (lazy ("The term " ^
1436 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1437 context ^ " has type " ^
1438 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1439 context ^ " but is here used with type " ^
1440 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1441 (* "\nReason: " ^ Lazy.force e*))))
1442 | CoercGraph.NotMetaClosed ->
1443 enrich localization_tbl hete exn
1445 (lazy ("The term " ^
1446 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1447 context ^ " has type " ^
1448 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1449 context ^ " but is here used with type " ^
1450 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1451 (* "\nReason: " ^ Lazy.force e*))))
1452 | CoercGraph.SomeCoercion candidates ->
1454 HExtlib.list_findopt
1457 let t = Cic.Appl[c;hete] in
1458 let newt,newhety,subst,metasenv,ugraph =
1459 type_of_aux subst metasenv context
1462 let newt, newty, subst, metasenv, ugraph =
1463 avoid_double_coercion context subst metasenv
1464 ugraph newt tgt_carr
1466 let subst,metasenv,ugraph1 =
1467 fo_unif_subst subst context metasenv
1470 Some ((newt,newty), subst, metasenv, ugraph)
1471 with Uncertain _ | RefineFailure _ -> None)
1474 (match selected with
1477 enrich localization_tbl hete
1479 (lazy ("The term " ^
1480 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1481 context ^ " has type " ^
1482 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1483 context ^ " but is here used with type " ^
1484 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1485 (* "\nReason: " ^ Lazy.force e*)))) exn))
1487 enrich localization_tbl hete
1489 (lazy ("The term " ^
1490 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1491 context ^ " has type " ^
1492 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1493 context ^ " but is here used with type " ^
1494 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1495 (* "\nReason: " ^ Printexc.to_string exn*)))) exn
1496 (* }}} end coercion stuff *)
1498 eat_prods_and_args pristinemenv metasenv subst context pristinehe he
1499 (CicSubstitution.subst (fst arg) t)
1500 ugraph1 (newargs@[arg]) tl
1503 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1505 pristinemenv context subst he hetype
1506 (newargs@[hete,hety]@tl) ugraph
1508 eat_prods_and_args metasenv
1509 metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
1510 with RefineFailure _ | Uncertain _ as exn ->
1511 (* unable to fix arity *)
1512 more_args_than_expected localization_tbl metasenv
1513 subst he context hetype args_bo_and_ty exn
1516 (* first we check if we are in the simple case of a meta closed term *)
1517 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1518 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1519 (* this optimization is to postpone fix_arity (the most common case)*)
1520 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1522 (* this (says CSC) is also useful to infer dependent types *)
1524 fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
1525 with RefineFailure _ | Uncertain _ as exn ->
1526 (* unable to fix arity *)
1527 more_args_than_expected localization_tbl metasenv
1528 subst he context hetype args_bo_and_ty exn
1530 let coerced_args,subst,metasenv,he,t,ugraph =
1532 metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
1534 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1537 (* eat prods ends here! *)
1539 let t',ty,subst',metasenv',ugraph1 =
1540 type_of_aux [] metasenv context t ugraph
1542 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1543 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1544 (* Andrea: ho rimesso qui l'applicazione della subst al
1545 metasenv dopo che ho droppato l'invariante che il metsaenv
1546 e' sempre istanziato *)
1547 let substituted_metasenv =
1548 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1550 (* substituted_t,substituted_ty,substituted_metasenv *)
1551 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1553 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1555 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1556 let cleaned_metasenv =
1558 (function (n,context,ty) ->
1559 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1564 | Some (n, Cic.Decl t) ->
1566 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1567 | Some (n, Cic.Def (bo,ty)) ->
1568 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1573 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1575 Some (n, Cic.Def (bo',ty'))
1579 ) substituted_metasenv
1581 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1584 let undebrujin uri typesno tys t =
1587 (fun (name,_,_,_) (i,t) ->
1588 (* here the explicit_named_substituion is assumed to be *)
1590 let t' = Cic.MutInd (uri,i,[]) in
1591 let t = CicSubstitution.subst t' t in
1593 ) tys (typesno - 1,t))
1595 let map_first_n n start f g l =
1596 let rec aux acc k l =
1599 | [] -> raise (Invalid_argument "map_first_n")
1600 | hd :: tl -> f hd k (aux acc (k+1) tl)
1606 (*CSC: this is a very rough approximation; to be finished *)
1607 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1608 let subst,metasenv,ugraph,tys =
1610 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1611 let subst,metasenv,ugraph,cl =
1613 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1614 let rec aux ctx k subst = function
1615 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1616 let subst,metasenv,ugraph,tl =
1618 (subst,metasenv,ugraph,[])
1619 (fun t n (subst,metasenv,ugraph,acc) ->
1620 let subst,metasenv,ugraph =
1622 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1624 subst,metasenv,ugraph,(t::acc))
1625 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1628 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1629 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1630 subst,metasenv,ugraph,t
1631 | Cic.Prod (name,s,t) ->
1632 let ctx = (Some (name,Cic.Decl s))::ctx in
1633 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1634 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1638 (lazy "not well formed constructor type"))
1640 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1641 subst,metasenv,ugraph,(name,ty) :: acc)
1642 cl (subst,metasenv,ugraph,[])
1644 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1645 tys ([],metasenv,ugraph,[])
1647 let substituted_tys =
1649 (fun (name,ind,arity,cl) ->
1651 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1653 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1656 metasenv,ugraph,substituted_tys
1658 let typecheck metasenv uri obj ~localization_tbl =
1659 let ugraph = CicUniv.empty_ugraph in
1661 Cic.Constant (name,Some bo,ty,args,attrs) ->
1662 let bo',boty,metasenv,ugraph =
1663 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1664 let ty',_,metasenv,ugraph =
1665 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1666 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1667 let bo' = CicMetaSubst.apply_subst subst bo' in
1668 let ty' = CicMetaSubst.apply_subst subst ty' in
1669 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1670 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1671 | Cic.Constant (name,None,ty,args,attrs) ->
1672 let ty',_,metasenv,ugraph =
1673 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1675 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1676 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1677 assert (metasenv' = metasenv);
1678 (* Here we do not check the metasenv for correctness *)
1679 let bo',boty,metasenv,ugraph =
1680 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1681 let ty',sort,metasenv,ugraph =
1682 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1686 (* instead of raising Uncertain, let's hope that the meta will become
1689 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1691 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1692 let bo' = CicMetaSubst.apply_subst subst bo' in
1693 let ty' = CicMetaSubst.apply_subst subst ty' in
1694 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1695 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1696 | Cic.Variable _ -> assert false (* not implemented *)
1697 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1698 (*CSC: this code is greately simplified and many many checks are missing *)
1699 (*CSC: e.g. the constructors are not required to build their own types, *)
1700 (*CSC: the arities are not required to have as type a sort, etc. *)
1701 let uri = match uri with Some uri -> uri | None -> assert false in
1702 let typesno = List.length tys in
1703 (* first phase: we fix only the types *)
1704 let metasenv,ugraph,tys =
1706 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1707 let ty',_,metasenv,ugraph =
1708 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1710 metasenv,ugraph,(name,b,ty',cl)::res
1711 ) tys (metasenv,ugraph,[]) in
1713 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1714 (* second phase: we fix only the constructors *)
1715 let metasenv,ugraph,tys =
1717 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1718 let metasenv,ugraph,cl' =
1720 (fun (name,ty) (metasenv,ugraph,res) ->
1722 CicTypeChecker.debrujin_constructor
1723 ~cb:(relocalize localization_tbl) uri typesno ty in
1724 let ty',_,metasenv,ugraph =
1725 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1726 let ty' = undebrujin uri typesno tys ty' in
1727 metasenv,ugraph,(name,ty')::res
1728 ) cl (metasenv,ugraph,[])
1730 metasenv,ugraph,(name,b,ty,cl')::res
1731 ) tys (metasenv,ugraph,[]) in
1732 (* third phase: we check the positivity condition *)
1733 let metasenv,ugraph,tys =
1734 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1736 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1739 (* sara' piu' veloce che raffinare da zero? mah.... *)
1740 let pack_coercion metasenv ctx t =
1741 let module C = Cic in
1742 let rec merge_coercions ctx =
1743 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1745 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1746 | C.Meta (n,subst) ->
1749 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1752 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1753 | C.Prod (name,so,dest) ->
1754 let ctx' = (Some (name,C.Decl so))::ctx in
1755 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1756 | C.Lambda (name,so,dest) ->
1757 let ctx' = (Some (name,C.Decl so))::ctx in
1758 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1759 | C.LetIn (name,so,dest) ->
1760 let _,ty,metasenv,ugraph =
1761 pack_coercions := false;
1762 type_of_aux' metasenv ctx so CicUniv.empty_ugraph in
1763 pack_coercions := true;
1764 let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1765 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1767 let l = List.map (merge_coercions ctx) l in
1769 let b,_,_,_,_ = is_a_double_coercion t in
1770 (* prerr_endline "CANDIDATO!!!!"; *)
1772 let ugraph = CicUniv.empty_ugraph in
1773 let old_insert_coercions = !insert_coercions in
1774 insert_coercions := false;
1775 let newt, _, menv, _ =
1777 type_of_aux' metasenv ctx t ugraph
1778 with RefineFailure _ | Uncertain _ ->
1781 insert_coercions := old_insert_coercions;
1782 if metasenv <> [] || menv = [] then
1785 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1788 | C.Var (uri,exp_named_subst) ->
1789 let exp_named_subst = List.map aux exp_named_subst in
1790 C.Var (uri, exp_named_subst)
1791 | C.Const (uri,exp_named_subst) ->
1792 let exp_named_subst = List.map aux exp_named_subst in
1793 C.Const (uri, exp_named_subst)
1794 | C.MutInd (uri,tyno,exp_named_subst) ->
1795 let exp_named_subst = List.map aux exp_named_subst in
1796 C.MutInd (uri,tyno,exp_named_subst)
1797 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1798 let exp_named_subst = List.map aux exp_named_subst in
1799 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1800 | C.MutCase (uri,tyno,out,te,pl) ->
1801 let pl = List.map (merge_coercions ctx) pl in
1802 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1803 | C.Fix (fno, fl) ->
1806 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1811 (fun (name,idx,ty,bo) ->
1812 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1816 | C.CoFix (fno, fl) ->
1819 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1824 (fun (name,ty,bo) ->
1825 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1830 merge_coercions ctx t
1833 let pack_coercion_metasenv conjectures =
1834 let module C = Cic in
1836 (fun (i, ctx, ty) ->
1842 Some (name, C.Decl t) ->
1843 Some (name, C.Decl (pack_coercion conjectures ctx t))
1844 | Some (name, C.Def (t,None)) ->
1845 Some (name,C.Def (pack_coercion conjectures ctx t,None))
1846 | Some (name, C.Def (t,Some ty)) ->
1847 Some (name, C.Def (pack_coercion conjectures ctx t,
1848 Some (pack_coercion conjectures ctx ty)))
1854 ((i,ctx,pack_coercion conjectures ctx ty))
1858 let pack_coercion_obj obj =
1859 let module C = Cic in
1861 | C.Constant (id, body, ty, params, attrs) ->
1865 | Some body -> Some (pack_coercion [] [] body)
1867 let ty = pack_coercion [] [] ty in
1868 C.Constant (id, body, ty, params, attrs)
1869 | C.Variable (name, body, ty, params, attrs) ->
1873 | Some body -> Some (pack_coercion [] [] body)
1875 let ty = pack_coercion [] [] ty in
1876 C.Variable (name, body, ty, params, attrs)
1877 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1878 let conjectures = pack_coercion_metasenv conjectures in
1879 let body = pack_coercion conjectures [] body in
1880 let ty = pack_coercion conjectures [] ty in
1881 C.CurrentProof (name, conjectures, body, ty, params, attrs)
1882 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1885 (fun (name, ind, arity, cl) ->
1886 let arity = pack_coercion [] [] arity in
1888 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
1890 (name, ind, arity, cl))
1893 C.InductiveDefinition (indtys, params, leftno, attrs)
1898 let type_of_aux' metasenv context term =
1901 type_of_aux' metasenv context term in
1903 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1905 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1908 | RefineFailure msg as e ->
1909 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1911 | Uncertain msg as e ->
1912 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1916 let profiler2 = HExtlib.profile "CicRefine"
1918 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1919 profiler2.HExtlib.profile
1920 (type_of_aux' ?localization_tbl metasenv context term) ugraph
1922 let typecheck ~localization_tbl metasenv uri obj =
1923 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
1925 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
1926 (* vim:set foldmethod=marker: *)