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 CoercDb.is_a_coercion' c1 ->
140 (match last_of tl with
141 | sib1,Cic.Appl (c2::tl2) when CoercDb.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 context ugraph coercion_tgt (metasenv,last,coerced) =
328 let subst,metasenv,ugraph =
329 fo_unif_subst subst context metasenv last t ugraph
332 let newt, tty, subst, metasenv, ugraph =
333 avoid_double_coercion context subst metasenv ugraph coerced
336 Some (newt, tty, subst, metasenv, ugraph)
338 | RefineFailure _ | Uncertain _ -> None
340 let (t',_,_,_,_) as res =
345 match List.nth context (n - 1) with
346 Some (_,C.Decl ty) ->
347 t,S.lift n ty,subst,metasenv, ugraph
348 | Some (_,C.Def (_,Some ty)) ->
349 t,S.lift n ty,subst,metasenv, ugraph
350 | Some (_,C.Def (bo,None)) ->
352 (* if it is in the context it must be already well-typed*)
353 CicTypeChecker.type_of_aux' ~subst metasenv context
356 t,ty,subst,metasenv,ugraph
358 enrich localization_tbl t
359 (RefineFailure (lazy "Rel to hidden hypothesis"))
362 enrich localization_tbl t
363 (RefineFailure (lazy "Not a closed term")))
364 | C.Var (uri,exp_named_subst) ->
365 let exp_named_subst',subst',metasenv',ugraph1 =
366 check_exp_named_subst
367 subst metasenv context exp_named_subst ugraph
369 let ty_uri,ugraph1 = type_of_variable uri ugraph in
371 CicSubstitution.subst_vars exp_named_subst' ty_uri
373 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
376 let (canonical_context, term,ty) =
377 CicUtil.lookup_subst n subst
379 let l',subst',metasenv',ugraph1 =
380 check_metasenv_consistency n subst metasenv context
381 canonical_context l ugraph
383 (* trust or check ??? *)
384 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
385 subst', metasenv', ugraph1
386 (* type_of_aux subst metasenv
387 context (CicSubstitution.subst_meta l term) *)
388 with CicUtil.Subst_not_found _ ->
389 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
390 let l',subst',metasenv', ugraph1 =
391 check_metasenv_consistency n subst metasenv context
392 canonical_context l ugraph
394 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
395 subst', metasenv',ugraph1)
396 | C.Sort (C.Type tno) ->
397 let tno' = CicUniv.fresh() in
399 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
400 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
402 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
404 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
405 | C.Implicit infos ->
406 let metasenv',t' = exp_impl metasenv subst context infos in
407 type_of_aux subst metasenv' context t' ugraph
409 let ty',_,subst',metasenv',ugraph1 =
410 type_of_aux subst metasenv context ty ugraph
412 let te',inferredty,subst'',metasenv'',ugraph2 =
413 type_of_aux subst' metasenv' context te ugraph1
416 let subst''',metasenv''',ugraph3 =
417 fo_unif_subst subst'' context metasenv''
418 inferredty ty' ugraph2
420 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
423 enrich localization_tbl te'
426 CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
427 context ^ " has type " ^
428 CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty
429 context ^ " but is here used with type " ^
430 CicMetaSubst.ppterm_in_context metasenv'' subst'' ty' context)) exn
432 | C.Prod (name,s,t) ->
433 let carr t subst context = CicMetaSubst.apply_subst subst t in
434 let coerce_to_sort in_source tgt_sort t type_to_coerce
435 subst context metasenv uragph
437 if not !insert_coercions then
438 t,type_to_coerce,subst,metasenv,ugraph
440 let coercion_src = carr type_to_coerce subst context in
441 match coercion_src with
443 t,type_to_coerce,subst,metasenv,ugraph
444 | Cic.Meta _ as meta ->
445 t, meta, subst, metasenv, ugraph
446 | Cic.Cast _ as cast ->
447 t, cast, subst, metasenv, ugraph
449 let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
451 CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
454 | CoercGraph.NoCoercion
455 | CoercGraph.NotHandled _ ->
456 enrich localization_tbl t
459 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
460 " is not a type since it has type " ^
461 CicMetaSubst.ppterm_in_context ~metasenv
462 subst coercion_src context ^ " that is not a sort")))
463 | CoercGraph.NotMetaClosed ->
464 enrich localization_tbl t
467 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
468 " is not a type since it has type " ^
469 CicMetaSubst.ppterm_in_context ~metasenv
470 subst coercion_src context ^ " that is not a sort")))
471 | CoercGraph.SomeCoercion candidates ->
474 (try_coercion t subst context ugraph coercion_tgt)
480 enrich localization_tbl t
483 CicMetaSubst.ppterm_in_context ~metasenv
485 " is not a type since it has type " ^
486 CicMetaSubst.ppterm_in_context ~metasenv
487 subst coercion_src context ^
488 " that is not a sort"))))
490 let s',sort1,subst',metasenv',ugraph1 =
491 type_of_aux subst metasenv context s ugraph
493 let s',sort1,subst', metasenv',ugraph1 =
494 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
495 s' sort1 subst' context metasenv' ugraph1
497 let context_for_t = ((Some (name,(C.Decl s')))::context) in
498 let t',sort2,subst'',metasenv'',ugraph2 =
499 type_of_aux subst' metasenv'
500 context_for_t t ugraph1
502 let t',sort2,subst'',metasenv'',ugraph2 =
503 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
504 t' sort2 subst'' context_for_t metasenv'' ugraph2
506 let sop,subst''',metasenv''',ugraph3 =
507 sort_of_prod localization_tbl subst'' metasenv''
508 context (name,s') t' (sort1,sort2) ugraph2
510 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
511 | C.Lambda (n,s,t) ->
513 let s',sort1,subst',metasenv',ugraph1 =
514 type_of_aux subst metasenv context s ugraph in
515 let s',sort1,subst',metasenv',ugraph1 =
516 if not !insert_coercions then
517 s',sort1, subst', metasenv', ugraph1
519 match CicReduction.whd ~subst:subst' context sort1 with
520 | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
522 let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
524 CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
527 | CoercGraph.NoCoercion
528 | CoercGraph.NotHandled _ ->
529 enrich localization_tbl s'
532 CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
533 " is not a type since it has type " ^
534 CicMetaSubst.ppterm_in_context ~metasenv
535 subst coercion_src context ^ " that is not a sort")))
536 | CoercGraph.NotMetaClosed ->
537 enrich localization_tbl s'
540 CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
541 " is not a type since it has type " ^
542 CicMetaSubst.ppterm_in_context ~metasenv
543 subst coercion_src context ^ " that is not a sort")))
544 | CoercGraph.SomeCoercion candidates ->
547 (try_coercion s' subst' context ugraph1 coercion_tgt)
553 enrich localization_tbl s'
556 CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
557 " is not a type since it has type " ^
558 CicMetaSubst.ppterm_in_context ~metasenv
559 subst coercion_src context ^
560 " that is not a sort")))
562 let context_for_t = ((Some (n,(C.Decl s')))::context) in
563 let t',type2,subst'',metasenv'',ugraph2 =
564 type_of_aux subst' metasenv' context_for_t t ugraph1
566 C.Lambda (n,s',t'),C.Prod (n,s',type2),
567 subst'',metasenv'',ugraph2
569 (* only to check if s is well-typed *)
570 let s',ty,subst',metasenv',ugraph1 =
571 type_of_aux subst metasenv context s ugraph
573 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
575 let t',inferredty,subst'',metasenv'',ugraph2 =
576 type_of_aux subst' metasenv'
577 context_for_t t ugraph1
579 (* One-step LetIn reduction.
580 * Even faster than the previous solution.
581 * Moreover the inferred type is closer to the expected one.
584 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
585 subst'',metasenv'',ugraph2
586 | C.Appl (he::((_::_) as tl)) ->
587 let he',hetype,subst',metasenv',ugraph1 =
588 type_of_aux subst metasenv context he ugraph
590 let tlbody_and_type,subst'',metasenv'',ugraph2 =
591 typeof_list subst' metasenv' context ugraph1 tl
593 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
594 eat_prods true subst'' metasenv'' context
595 he' hetype tlbody_and_type ugraph2
597 let newappl = (C.Appl (coerced_he::coerced_args)) in
598 avoid_double_coercion
599 context subst''' metasenv''' ugraph3 newappl applty
600 | C.Appl _ -> assert false
601 | C.Const (uri,exp_named_subst) ->
602 let exp_named_subst',subst',metasenv',ugraph1 =
603 check_exp_named_subst subst metasenv context
604 exp_named_subst ugraph in
605 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
607 CicSubstitution.subst_vars exp_named_subst' ty_uri
609 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
610 | C.MutInd (uri,i,exp_named_subst) ->
611 let exp_named_subst',subst',metasenv',ugraph1 =
612 check_exp_named_subst subst metasenv context
613 exp_named_subst ugraph
615 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
617 CicSubstitution.subst_vars exp_named_subst' ty_uri in
618 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
619 | C.MutConstruct (uri,i,j,exp_named_subst) ->
620 let exp_named_subst',subst',metasenv',ugraph1 =
621 check_exp_named_subst subst metasenv context
622 exp_named_subst ugraph
625 type_of_mutual_inductive_constr uri i j ugraph1
628 CicSubstitution.subst_vars exp_named_subst' ty_uri
630 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
632 | C.MutCase (uri, i, outtype, term, pl) ->
633 (* first, get the inductive type (and noparams)
634 * in the environment *)
635 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
636 let _ = CicTypeChecker.typecheck uri in
637 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
639 C.InductiveDefinition (l,expl_params,parsno,_) ->
640 List.nth l i , expl_params, parsno, u
642 enrich localization_tbl t
644 (lazy ("Unkown mutual inductive definition " ^
645 U.string_of_uri uri)))
647 let rec count_prod t =
648 match CicReduction.whd ~subst context t with
649 C.Prod (_, _, t) -> 1 + (count_prod t)
652 let no_args = count_prod arity in
653 (* now, create a "generic" MutInd *)
654 let metasenv,left_args =
655 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
657 let metasenv,right_args =
658 let no_right_params = no_args - no_left_params in
659 if no_right_params < 0 then assert false
660 else CicMkImplicit.n_fresh_metas
661 metasenv subst context no_right_params
663 let metasenv,exp_named_subst =
664 CicMkImplicit.fresh_subst metasenv subst context expl_params in
667 C.MutInd (uri,i,exp_named_subst)
670 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
672 (* check consistency with the actual type of term *)
673 let term',actual_type,subst,metasenv,ugraph1 =
674 type_of_aux subst metasenv context term ugraph in
675 let expected_type',_, subst, metasenv,ugraph2 =
676 type_of_aux subst metasenv context expected_type ugraph1
678 let actual_type = CicReduction.whd ~subst context actual_type in
679 let subst,metasenv,ugraph3 =
681 fo_unif_subst subst context metasenv
682 expected_type' actual_type ugraph2
685 enrich localization_tbl term' exn
688 CicMetaSubst.ppterm_in_context ~metasenv subst term'
689 context ^ " has type " ^
690 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
691 context ^ " but is here used with type " ^
692 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
694 let rec instantiate_prod t =
698 match CicReduction.whd ~subst context t with
700 instantiate_prod (CicSubstitution.subst he t') tl
703 let arity_instantiated_with_left_args =
704 instantiate_prod arity left_args in
705 (* TODO: check if the sort elimination
706 * is allowed: [(I q1 ... qr)|B] *)
707 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
709 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
711 if left_args = [] then
712 (C.MutConstruct (uri,i,j,exp_named_subst))
715 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
717 let p',actual_type,subst,metasenv,ugraph1 =
718 type_of_aux subst metasenv context p ugraph
720 let constructor',expected_type, subst, metasenv,ugraph2 =
721 type_of_aux subst metasenv context constructor ugraph1
723 let outtypeinstance,subst,metasenv,ugraph3 =
724 check_branch 0 context metasenv subst no_left_params
725 actual_type constructor' expected_type ugraph2
728 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
729 ([],1,[],subst,metasenv,ugraph3) pl
732 (* we are left to check that the outype matches his instances.
733 The easy case is when the outype is specified, that amount
734 to a trivial check. Otherwise, we should guess a type from
738 let outtype,outtypety, subst, metasenv,ugraph4 =
739 type_of_aux subst metasenv context outtype ugraph4 in
742 (let candidate,ugraph5,metasenv,subst =
743 let exp_name_subst, metasenv =
745 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
747 let uris = CicUtil.params_of_obj o in
749 fun uri (acc,metasenv) ->
750 let metasenv',new_meta =
751 CicMkImplicit.mk_implicit metasenv subst context
754 CicMkImplicit.identity_relocation_list_for_metavariable
757 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
761 match left_args,right_args with
762 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
764 let rec mk_right_args =
767 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
769 let right_args_no = List.length right_args in
770 let lifted_left_args =
771 List.map (CicSubstitution.lift right_args_no) left_args
773 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
774 (lifted_left_args @ mk_right_args right_args_no))
777 FreshNamesGenerator.mk_fresh_name ~subst metasenv
778 context Cic.Anonymous ~typ:ty
780 match outtypeinstances with
782 let extended_context =
783 let rec add_right_args =
785 Cic.Prod (name,ty,t) ->
786 Some (name,Cic.Decl ty)::(add_right_args t)
789 (Some (fresh_name,Cic.Decl ty))::
791 (add_right_args arity_instantiated_with_left_args))@
794 let metasenv,new_meta =
795 CicMkImplicit.mk_implicit metasenv subst extended_context
798 CicMkImplicit.identity_relocation_list_for_metavariable
801 let rec add_lambdas b =
803 Cic.Prod (name,ty,t) ->
804 Cic.Lambda (name,ty,(add_lambdas b t))
805 | _ -> Cic.Lambda (fresh_name, ty, b)
808 add_lambdas (Cic.Meta (new_meta,irl))
809 arity_instantiated_with_left_args
811 (Some candidate),ugraph4,metasenv,subst
812 | (constructor_args_no,_,instance,_)::tl ->
814 let instance',subst,metasenv =
815 CicMetaSubst.delift_rels subst metasenv
816 constructor_args_no instance
818 let candidate,ugraph,metasenv,subst =
820 fun (candidate_oty,ugraph,metasenv,subst)
821 (constructor_args_no,_,instance,_) ->
822 match candidate_oty with
823 | None -> None,ugraph,metasenv,subst
826 let instance',subst,metasenv =
827 CicMetaSubst.delift_rels subst metasenv
828 constructor_args_no instance
830 let subst,metasenv,ugraph =
831 fo_unif_subst subst context metasenv
834 candidate_oty,ugraph,metasenv,subst
836 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
837 | CicUnification.UnificationFailure _
838 | CicUnification.Uncertain _ ->
839 None,ugraph,metasenv,subst
840 ) (Some instance',ugraph4,metasenv,subst) tl
843 | None -> None, ugraph,metasenv,subst
845 let rec add_lambdas n b =
847 Cic.Prod (name,ty,t) ->
848 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
850 Cic.Lambda (fresh_name, ty,
851 CicSubstitution.lift (n + 1) t)
854 (add_lambdas 0 t arity_instantiated_with_left_args),
855 ugraph,metasenv,subst
856 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
857 None,ugraph4,metasenv,subst
860 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
862 let subst,metasenv,ugraph =
864 fo_unif_subst subst context metasenv
865 candidate outtype ugraph5
867 exn -> assert false(* unification against a metavariable *)
869 C.MutCase (uri, i, outtype, term', pl'),
870 CicReduction.head_beta_reduce
871 (CicMetaSubst.apply_subst subst
872 (Cic.Appl (outtype::right_args@[term']))),
873 subst,metasenv,ugraph)
874 | _ -> (* easy case *)
875 let tlbody_and_type,subst,metasenv,ugraph4 =
876 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
878 let _,_,_,subst,metasenv,ugraph4 =
879 eat_prods false subst metasenv context
880 outtype outtypety tlbody_and_type ugraph4
882 let _,_, subst, metasenv,ugraph5 =
883 type_of_aux subst metasenv context
884 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
886 let (subst,metasenv,ugraph6) =
888 (fun (subst,metasenv,ugraph)
889 p (constructor_args_no,context,instance,args)
894 CicSubstitution.lift constructor_args_no outtype
896 C.Appl (outtype'::args)
898 CicReduction.whd ~subst context appl
901 fo_unif_subst subst context metasenv instance instance'
905 enrich localization_tbl p exn
908 CicMetaSubst.ppterm_in_context ~metasenv subst p
909 context ^ " has type " ^
910 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
911 context ^ " but is here used with type " ^
912 CicMetaSubst.ppterm_in_context ~metasenv subst instance
914 (subst,metasenv,ugraph5) pl' outtypeinstances
916 C.MutCase (uri, i, outtype, term', pl'),
917 CicReduction.head_beta_reduce
918 (CicMetaSubst.apply_subst subst
919 (C.Appl(outtype::right_args@[term]))),
920 subst,metasenv,ugraph6)
922 let fl_ty',subst,metasenv,types,ugraph1 =
924 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
925 let ty',_,subst',metasenv',ugraph1 =
926 type_of_aux subst metasenv context ty ugraph
928 fl @ [ty'],subst',metasenv',
929 Some (C.Name n,(C.Decl ty')) :: types, ugraph
930 ) ([],subst,metasenv,[],ugraph) fl
932 let len = List.length types in
933 let context' = types@context in
934 let fl_bo',subst,metasenv,ugraph2 =
936 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
937 let bo',ty_of_bo,subst,metasenv,ugraph1 =
938 type_of_aux subst metasenv context' bo ugraph in
939 let expected_ty = CicSubstitution.lift len ty in
940 let subst',metasenv',ugraph' =
942 fo_unif_subst subst context' metasenv
943 ty_of_bo expected_ty ugraph1
946 enrich localization_tbl bo exn
949 CicMetaSubst.ppterm_in_context ~metasenv subst bo
950 context' ^ " has type " ^
951 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
952 context' ^ " but is here used with type " ^
953 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
956 fl @ [bo'] , subst',metasenv',ugraph'
957 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
959 let ty = List.nth fl_ty' i in
960 (* now we have the new ty in fl_ty', the new bo in fl_bo',
961 * and we want the new fl with bo' and ty' injected in the right
964 let rec map3 f l1 l2 l3 =
967 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
970 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
973 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
975 let fl_ty',subst,metasenv,types,ugraph1 =
977 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
978 let ty',_,subst',metasenv',ugraph1 =
979 type_of_aux subst metasenv context ty ugraph
981 fl @ [ty'],subst',metasenv',
982 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
983 ) ([],subst,metasenv,[],ugraph) fl
985 let len = List.length types in
986 let context' = types@context in
987 let fl_bo',subst,metasenv,ugraph2 =
989 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
990 let bo',ty_of_bo,subst,metasenv,ugraph1 =
991 type_of_aux subst metasenv context' bo ugraph in
992 let expected_ty = CicSubstitution.lift len ty in
993 let subst',metasenv',ugraph' =
995 fo_unif_subst subst context' metasenv
996 ty_of_bo expected_ty ugraph1
999 enrich localization_tbl bo exn
1002 CicMetaSubst.ppterm_in_context ~metasenv subst bo
1003 context' ^ " has type " ^
1004 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
1005 context' ^ " but is here used with type " ^
1006 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
1009 fl @ [bo'],subst',metasenv',ugraph'
1010 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
1012 let ty = List.nth fl_ty' i in
1013 (* now we have the new ty in fl_ty', the new bo in fl_bo',
1014 * and we want the new fl with bo' and ty' injected in the right
1017 let rec map3 f l1 l2 l3 =
1020 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
1023 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
1026 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
1028 relocalize localization_tbl t t';
1031 (* check_metasenv_consistency checks that the "canonical" context of a
1032 metavariable is consitent - up to relocation via the relocation list l -
1033 with the actual context *)
1034 and check_metasenv_consistency
1035 metano subst metasenv context canonical_context l ugraph
1037 let module C = Cic in
1038 let module R = CicReduction in
1039 let module S = CicSubstitution in
1040 let lifted_canonical_context =
1044 | (Some (n,C.Decl t))::tl ->
1045 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
1046 | (Some (n,C.Def (t,None)))::tl ->
1047 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1048 | None::tl -> None::(aux (i+1) tl)
1049 | (Some (n,C.Def (t,Some ty)))::tl ->
1051 C.Def ((S.subst_meta l (S.lift i t)),
1052 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
1054 aux 1 canonical_context
1058 (fun (l,subst,metasenv,ugraph) t ct ->
1061 l @ [None],subst,metasenv,ugraph
1062 | Some t,Some (_,C.Def (ct,_)) ->
1063 let subst',metasenv',ugraph' =
1065 prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
1066 fo_unif_subst subst context metasenv t ct ugraph
1067 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))))))
1069 l @ [Some t],subst',metasenv',ugraph'
1070 | Some t,Some (_,C.Decl ct) ->
1071 let t',inferredty,subst',metasenv',ugraph1 =
1072 type_of_aux subst metasenv context t ugraph
1074 let subst'',metasenv'',ugraph2 =
1077 subst' context metasenv' inferredty ct ugraph1
1078 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))))))
1080 l @ [Some t'], subst'',metasenv'',ugraph2
1082 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
1084 Invalid_argument _ ->
1088 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1089 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1090 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1092 and check_exp_named_subst metasubst metasenv context tl ugraph =
1093 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1095 [] -> [],metasubst,metasenv,ugraph
1097 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1099 CicSubstitution.subst_vars substs ty_uri in
1100 (* CSC: why was this code here? it is wrong
1101 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1102 Cic.Variable (_,Some bo,_,_) ->
1104 (RefineFailure (lazy
1105 "A variable with a body can not be explicit substituted"))
1106 | Cic.Variable (_,None,_,_) -> ()
1109 (RefineFailure (lazy
1110 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1113 let t',typeoft,metasubst',metasenv',ugraph2 =
1114 type_of_aux metasubst metasenv context t ugraph1 in
1115 let subst = uri,t' in
1116 let metasubst'',metasenv'',ugraph3 =
1119 metasubst' context metasenv' typeoft typeofvar ugraph2
1121 raise (RefineFailure (lazy
1122 ("Wrong Explicit Named Substitution: " ^
1123 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1124 " not unifiable with " ^
1125 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1127 (* FIXME: no mere tail recursive! *)
1128 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1129 check_exp_named_subst_aux
1130 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1132 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1134 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1137 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1140 let module C = Cic in
1141 let context_for_t2 = (Some (name,C.Decl s))::context in
1142 let t1'' = CicReduction.whd ~subst context t1 in
1143 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1144 match (t1'', t2'') with
1145 (C.Sort s1, C.Sort s2)
1146 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1147 (* different than Coq manual!!! *)
1148 C.Sort s2,subst,metasenv,ugraph
1149 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1150 let t' = CicUniv.fresh() in
1152 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1153 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1154 C.Sort (C.Type t'),subst,metasenv,ugraph2
1156 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1157 | (C.Sort _,C.Sort (C.Type t1)) ->
1158 C.Sort (C.Type t1),subst,metasenv,ugraph
1159 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1160 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1161 (* TODO how can we force the meta to become a sort? If we don't we
1162 * break the invariant that refine produce only well typed terms *)
1163 (* TODO if we check the non meta term and if it is a sort then we
1164 * are likely to know the exact value of the result e.g. if the rhs
1165 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1166 let (metasenv,idx) =
1167 CicMkImplicit.mk_implicit_sort metasenv subst in
1168 let (subst, metasenv,ugraph1) =
1170 fo_unif_subst subst context_for_t2 metasenv
1171 (C.Meta (idx,[])) t2'' ugraph
1172 with _ -> assert false (* unification against a metavariable *)
1174 t2'',subst,metasenv,ugraph1
1177 enrich localization_tbl s
1181 "%s is supposed to be a type, but its type is %s"
1182 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1183 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1185 enrich localization_tbl t
1189 "%s is supposed to be a type, but its type is %s"
1190 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1191 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1193 and avoid_double_coercion context subst metasenv ugraph t ty =
1194 if not !pack_coercions then
1195 t,ty,subst,metasenv,ugraph
1197 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1199 let source_carr = CoercGraph.source_of c2 in
1200 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1201 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1203 | CoercGraph.SomeCoercion candidates ->
1205 HExtlib.list_findopt
1206 (function (metasenv,last,c) ->
1208 | c when not (CoercGraph.is_composite c) ->
1209 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1212 let subst,metasenv,ugraph =
1213 fo_unif_subst subst context metasenv last head ugraph in
1214 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1219 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1220 let newt,_,subst,metasenv,ugraph =
1221 type_of_aux subst metasenv context c ugraph in
1222 debug_print (lazy "tipa...");
1223 let subst, metasenv, ugraph =
1224 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1225 fo_unif_subst subst context metasenv newt t ugraph
1227 debug_print (lazy "unifica...");
1228 Some (newt, ty, subst, metasenv, ugraph)
1230 | RefineFailure s | Uncertain s when not !pack_coercions->
1231 debug_print s; debug_print (lazy "stop\n");None
1232 | RefineFailure s | Uncertain s ->
1233 debug_print s;debug_print (lazy "goon\n");
1235 let old_pack_coercions = !pack_coercions in
1236 pack_coercions := false; (* to avoid diverging *)
1237 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1238 type_of_aux subst metasenv context c1_c2_implicit ugraph
1240 pack_coercions := old_pack_coercions;
1242 is_a_double_coercion refined_c1_c2_implicit
1248 match refined_c1_c2_implicit with
1249 | Cic.Appl l -> HExtlib.list_last l
1252 let subst, metasenv, ugraph =
1253 try fo_unif_subst subst context metasenv
1255 with RefineFailure s| Uncertain s->
1256 debug_print s;assert false
1258 let subst, metasenv, ugraph =
1259 fo_unif_subst subst context metasenv
1260 refined_c1_c2_implicit t ugraph
1262 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1264 | RefineFailure s | Uncertain s ->
1265 pack_coercions := true;debug_print s;None
1266 | exn -> pack_coercions := true; raise exn))
1269 (match selected with
1273 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1274 t, ty, subst, metasenv, ugraph)
1275 | _ -> t, ty, subst, metasenv, ugraph)
1277 t, ty, subst, metasenv, ugraph
1279 and typeof_list subst metasenv context ugraph l =
1280 let tlbody_and_type,subst,metasenv,ugraph =
1282 (fun x (res,subst,metasenv,ugraph) ->
1283 let x',ty,subst',metasenv',ugraph1 =
1284 type_of_aux subst metasenv context x ugraph
1286 (x', ty)::res,subst',metasenv',ugraph1
1287 ) l ([],subst,metasenv,ugraph)
1289 tlbody_and_type,subst,metasenv,ugraph
1292 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1294 (* aux function to add coercions to funclass *)
1295 let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph =
1297 let pristinemenv = metasenv in
1298 let metasenv,hetype' =
1299 mk_prod_of_metas metasenv context subst args_bo_and_ty
1302 let subst,metasenv,ugraph =
1303 fo_unif_subst_eat_prods
1304 subst context metasenv hetype hetype' ugraph
1306 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1307 with RefineFailure s | Uncertain s as exn
1308 when allow_coercions && !insert_coercions ->
1309 (* {{{ we search a coercion of the head (saturated) to funclass *)
1310 let metasenv = pristinemenv in
1312 ("Fixing arity of: "^CicMetaSubst.ppterm ~metasenv subst hetype ^
1313 " since unif failed with: " ^ CicMetaSubst.ppterm ~metasenv subst hetype'
1314 (* ^ " cause: " ^ Lazy.force s *)));
1315 let how_many_args_are_needed =
1316 let rec aux n = function
1317 | Cic.Prod(_,_,t) -> aux (n+1) t
1320 aux 0 (CicMetaSubst.apply_subst subst hetype)
1322 let args, remainder =
1323 HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
1325 let args = List.map fst args in
1329 | Cic.Appl l -> Cic.Appl (l@args)
1330 | _ -> Cic.Appl (he::args)
1334 let x,xty,subst,metasenv,ugraph =
1335 (*CSC: here unsharing is necessary to avoid an unwanted
1336 relocalization. However, this also shows a great source of
1337 inefficiency: "x" is refined twice (once now and once in the
1338 subsequent eat_prods_and_args). Morevoer, how is divergence avoided?
1340 type_of_aux subst metasenv context (Unshare.unshare x) ugraph
1343 CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty)
1345 let carr_tgt = CoercDb.Fun 0 in
1346 match CoercGraph.look_for_coercion' metasenv subst context carr_src carr_tgt with
1347 | CoercGraph.NoCoercion
1348 | CoercGraph.NotMetaClosed
1349 | CoercGraph.NotHandled _ -> raise exn
1350 | CoercGraph.SomeCoercion candidates ->
1352 HExtlib.list_findopt
1353 (fun (metasenv,last,coerc) ->
1354 let subst,metasenv,ugraph =
1355 fo_unif_subst subst context metasenv last x ugraph in
1356 debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc));
1358 (* we want this to be available in the error handler fo the
1359 * following (so it has its own try. *)
1360 let t,tty,subst,metasenv,ugraph =
1361 type_of_aux subst metasenv context coerc ugraph
1364 let metasenv, hetype' =
1365 mk_prod_of_metas metasenv context subst remainder
1368 (" unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^
1369 CicMetaSubst.ppterm ~metasenv subst hetype'));
1370 let subst,metasenv,ugraph =
1371 fo_unif_subst_eat_prods
1372 subst context metasenv tty hetype' ugraph
1374 debug_print (lazy " success!");
1375 Some (subst,metasenv,ugraph,tty,t,remainder)
1377 | Uncertain _ | RefineFailure _
1378 | CicUnification.UnificationFailure _
1379 | CicUnification.Uncertain _ ->
1381 let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
1383 metasenv context subst t tty remainder ugraph
1385 Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
1386 with Uncertain _ | RefineFailure _ -> None
1390 | HExtlib.Localized (_,Uncertain _)
1391 | HExtlib.Localized (_,RefineFailure _) -> None
1392 | exn -> assert false) (* ritornare None, e' un localized *)
1395 | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
1396 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1398 more_args_than_expected localization_tbl metasenv
1399 subst he context hetype args_bo_and_ty exn
1400 (* }}} end coercion to funclass stuff *)
1401 (* }}} end fix_arity *)
1403 (* aux function to process the type of the head and the args in parallel *)
1404 let rec eat_prods_and_args
1405 pristinemenv metasenv subst context pristinehe he hetype ugraph newargs
1409 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1410 | (hete, hety)::tl ->
1411 match (CicReduction.whd ~subst context hetype) with
1412 | Cic.Prod (n,s,t) ->
1413 let arg,subst,metasenv,ugraph1 =
1415 let subst,metasenv,ugraph1 =
1416 fo_unif_subst_eat_prods2
1417 subst context metasenv hety s ugraph
1419 (hete,hety),subst,metasenv,ugraph1
1420 (* {{{ we search a coercion from hety to s if fails *)
1421 with RefineFailure _ | Uncertain _ as exn
1422 when allow_coercions && !insert_coercions ->
1423 let coer, tgt_carr =
1424 let carr t subst context =
1425 CicReduction.whd ~delta:false
1426 context (CicMetaSubst.apply_subst subst t )
1428 let c_hety = carr hety subst context in
1429 let c_s = carr s subst context in
1430 CoercGraph.look_for_coercion metasenv subst context c_hety c_s, c_s
1433 | CoercGraph.NoCoercion
1434 | CoercGraph.NotHandled _ ->
1435 enrich localization_tbl hete exn
1437 (lazy ("The term " ^
1438 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1439 context ^ " has type " ^
1440 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1441 context ^ " but is here used with type " ^
1442 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1443 (* "\nReason: " ^ Lazy.force e*))))
1444 | CoercGraph.NotMetaClosed ->
1445 enrich localization_tbl hete exn
1447 (lazy ("The term " ^
1448 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1449 context ^ " has type " ^
1450 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1451 context ^ " but is here used with type " ^
1452 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1453 (* "\nReason: " ^ Lazy.force e*))))
1454 | CoercGraph.SomeCoercion candidates ->
1456 HExtlib.list_findopt
1457 (fun (metasenv,last,c) ->
1459 let subst,metasenv,ugraph =
1460 fo_unif_subst subst context metasenv last hete
1462 let newt,newhety,subst,metasenv,ugraph =
1463 type_of_aux subst metasenv context
1466 let newt, newty, subst, metasenv, ugraph =
1467 avoid_double_coercion context subst metasenv
1468 ugraph newt tgt_carr
1470 let subst,metasenv,ugraph1 =
1471 fo_unif_subst subst context metasenv
1474 Some ((newt,newty), subst, metasenv, ugraph)
1475 with Uncertain _ | RefineFailure _ -> None)
1478 (match selected with
1481 enrich localization_tbl hete
1483 (lazy ("The term " ^
1484 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1485 context ^ " has type " ^
1486 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1487 context ^ " but is here used with type " ^
1488 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1489 (* "\nReason: " ^ Lazy.force e*)))) exn))
1491 enrich localization_tbl hete
1493 (lazy ("The term " ^
1494 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1495 context ^ " has type " ^
1496 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1497 context ^ " but is here used with type " ^
1498 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1499 (* "\nReason: " ^ Printexc.to_string exn*)))) exn
1500 (* }}} end coercion stuff *)
1502 eat_prods_and_args pristinemenv metasenv subst context pristinehe he
1503 (CicSubstitution.subst (fst arg) t)
1504 ugraph1 (newargs@[arg]) tl
1507 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1509 pristinemenv context subst he hetype
1510 (newargs@[hete,hety]@tl) ugraph
1512 eat_prods_and_args metasenv
1513 metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
1514 with RefineFailure _ | Uncertain _ as exn ->
1515 (* unable to fix arity *)
1516 more_args_than_expected localization_tbl metasenv
1517 subst he context hetype args_bo_and_ty exn
1520 (* first we check if we are in the simple case of a meta closed term *)
1521 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1522 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1523 (* this optimization is to postpone fix_arity (the most common case)*)
1524 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1526 (* this (says CSC) is also useful to infer dependent types *)
1528 fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
1529 with RefineFailure _ | Uncertain _ as exn ->
1530 (* unable to fix arity *)
1531 more_args_than_expected localization_tbl metasenv
1532 subst he context hetype args_bo_and_ty exn
1534 let coerced_args,subst,metasenv,he,t,ugraph =
1536 metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
1538 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1541 (* eat prods ends here! *)
1543 let t',ty,subst',metasenv',ugraph1 =
1544 type_of_aux [] metasenv context t ugraph
1546 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1547 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1548 (* Andrea: ho rimesso qui l'applicazione della subst al
1549 metasenv dopo che ho droppato l'invariante che il metsaenv
1550 e' sempre istanziato *)
1551 let substituted_metasenv =
1552 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1554 (* substituted_t,substituted_ty,substituted_metasenv *)
1555 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1557 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1559 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1560 let cleaned_metasenv =
1562 (function (n,context,ty) ->
1563 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1568 | Some (n, Cic.Decl t) ->
1570 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1571 | Some (n, Cic.Def (bo,ty)) ->
1572 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1577 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1579 Some (n, Cic.Def (bo',ty'))
1583 ) substituted_metasenv
1585 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1588 let undebrujin uri typesno tys t =
1591 (fun (name,_,_,_) (i,t) ->
1592 (* here the explicit_named_substituion is assumed to be *)
1594 let t' = Cic.MutInd (uri,i,[]) in
1595 let t = CicSubstitution.subst t' t in
1597 ) tys (typesno - 1,t))
1599 let map_first_n n start f g l =
1600 let rec aux acc k l =
1603 | [] -> raise (Invalid_argument "map_first_n")
1604 | hd :: tl -> f hd k (aux acc (k+1) tl)
1610 (*CSC: this is a very rough approximation; to be finished *)
1611 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1612 let subst,metasenv,ugraph,tys =
1614 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1615 let subst,metasenv,ugraph,cl =
1617 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1618 let rec aux ctx k subst = function
1619 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1620 let subst,metasenv,ugraph,tl =
1622 (subst,metasenv,ugraph,[])
1623 (fun t n (subst,metasenv,ugraph,acc) ->
1624 let subst,metasenv,ugraph =
1626 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1628 subst,metasenv,ugraph,(t::acc))
1629 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1632 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1633 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1634 subst,metasenv,ugraph,t
1635 | Cic.Prod (name,s,t) ->
1636 let ctx = (Some (name,Cic.Decl s))::ctx in
1637 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1638 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1642 (lazy "not well formed constructor type"))
1644 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1645 subst,metasenv,ugraph,(name,ty) :: acc)
1646 cl (subst,metasenv,ugraph,[])
1648 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1649 tys ([],metasenv,ugraph,[])
1651 let substituted_tys =
1653 (fun (name,ind,arity,cl) ->
1655 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1657 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1660 metasenv,ugraph,substituted_tys
1662 let typecheck metasenv uri obj ~localization_tbl =
1663 let ugraph = CicUniv.empty_ugraph in
1665 Cic.Constant (name,Some bo,ty,args,attrs) ->
1666 let bo',boty,metasenv,ugraph =
1667 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1668 let ty',_,metasenv,ugraph =
1669 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1670 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1671 let bo' = CicMetaSubst.apply_subst subst bo' in
1672 let ty' = CicMetaSubst.apply_subst subst ty' in
1673 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1674 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1675 | Cic.Constant (name,None,ty,args,attrs) ->
1676 let ty',_,metasenv,ugraph =
1677 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1679 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1680 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1681 assert (metasenv' = metasenv);
1682 (* Here we do not check the metasenv for correctness *)
1683 let bo',boty,metasenv,ugraph =
1684 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1685 let ty',sort,metasenv,ugraph =
1686 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1690 (* instead of raising Uncertain, let's hope that the meta will become
1693 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1695 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1696 let bo' = CicMetaSubst.apply_subst subst bo' in
1697 let ty' = CicMetaSubst.apply_subst subst ty' in
1698 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1699 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1700 | Cic.Variable _ -> assert false (* not implemented *)
1701 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1702 (*CSC: this code is greately simplified and many many checks are missing *)
1703 (*CSC: e.g. the constructors are not required to build their own types, *)
1704 (*CSC: the arities are not required to have as type a sort, etc. *)
1705 let uri = match uri with Some uri -> uri | None -> assert false in
1706 let typesno = List.length tys in
1707 (* first phase: we fix only the types *)
1708 let metasenv,ugraph,tys =
1710 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1711 let ty',_,metasenv,ugraph =
1712 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1714 metasenv,ugraph,(name,b,ty',cl)::res
1715 ) tys (metasenv,ugraph,[]) in
1717 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1718 (* second phase: we fix only the constructors *)
1719 let metasenv,ugraph,tys =
1721 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1722 let metasenv,ugraph,cl' =
1724 (fun (name,ty) (metasenv,ugraph,res) ->
1726 CicTypeChecker.debrujin_constructor
1727 ~cb:(relocalize localization_tbl) uri typesno ty in
1728 let ty',_,metasenv,ugraph =
1729 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1730 let ty' = undebrujin uri typesno tys ty' in
1731 metasenv,ugraph,(name,ty')::res
1732 ) cl (metasenv,ugraph,[])
1734 metasenv,ugraph,(name,b,ty,cl')::res
1735 ) tys (metasenv,ugraph,[]) in
1736 (* third phase: we check the positivity condition *)
1737 let metasenv,ugraph,tys =
1738 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1740 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1743 (* sara' piu' veloce che raffinare da zero? mah.... *)
1744 let pack_coercion metasenv ctx t =
1745 let module C = Cic in
1746 let rec merge_coercions ctx =
1747 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1749 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1750 | C.Meta (n,subst) ->
1753 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1756 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1757 | C.Prod (name,so,dest) ->
1758 let ctx' = (Some (name,C.Decl so))::ctx in
1759 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1760 | C.Lambda (name,so,dest) ->
1761 let ctx' = (Some (name,C.Decl so))::ctx in
1762 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1763 | C.LetIn (name,so,dest) ->
1764 let _,ty,metasenv,ugraph =
1765 pack_coercions := false;
1766 type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1767 pack_coercions := true;
1768 let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1769 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1771 let l = List.map (merge_coercions ctx) l in
1773 let b,_,_,_,_ = is_a_double_coercion t in
1774 (* prerr_endline "CANDIDATO!!!!"; *)
1776 let ugraph = CicUniv.oblivion_ugraph in
1777 let old_insert_coercions = !insert_coercions in
1778 insert_coercions := false;
1779 let newt, _, menv, _ =
1781 type_of_aux' metasenv ctx t ugraph
1782 with RefineFailure _ | Uncertain _ ->
1785 insert_coercions := old_insert_coercions;
1786 if metasenv <> [] || menv = [] then
1789 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1792 | C.Var (uri,exp_named_subst) ->
1793 let exp_named_subst = List.map aux exp_named_subst in
1794 C.Var (uri, exp_named_subst)
1795 | C.Const (uri,exp_named_subst) ->
1796 let exp_named_subst = List.map aux exp_named_subst in
1797 C.Const (uri, exp_named_subst)
1798 | C.MutInd (uri,tyno,exp_named_subst) ->
1799 let exp_named_subst = List.map aux exp_named_subst in
1800 C.MutInd (uri,tyno,exp_named_subst)
1801 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1802 let exp_named_subst = List.map aux exp_named_subst in
1803 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1804 | C.MutCase (uri,tyno,out,te,pl) ->
1805 let pl = List.map (merge_coercions ctx) pl in
1806 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1807 | C.Fix (fno, fl) ->
1810 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1815 (fun (name,idx,ty,bo) ->
1816 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1820 | C.CoFix (fno, fl) ->
1823 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1828 (fun (name,ty,bo) ->
1829 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1834 merge_coercions ctx t
1837 let pack_coercion_metasenv conjectures =
1838 let module C = Cic in
1840 (fun (i, ctx, ty) ->
1846 Some (name, C.Decl t) ->
1847 Some (name, C.Decl (pack_coercion conjectures ctx t))
1848 | Some (name, C.Def (t,None)) ->
1849 Some (name,C.Def (pack_coercion conjectures ctx t,None))
1850 | Some (name, C.Def (t,Some ty)) ->
1851 Some (name, C.Def (pack_coercion conjectures ctx t,
1852 Some (pack_coercion conjectures ctx ty)))
1858 ((i,ctx,pack_coercion conjectures ctx ty))
1862 let pack_coercion_obj obj =
1863 let module C = Cic in
1865 | C.Constant (id, body, ty, params, attrs) ->
1869 | Some body -> Some (pack_coercion [] [] body)
1871 let ty = pack_coercion [] [] ty in
1872 C.Constant (id, body, ty, params, attrs)
1873 | C.Variable (name, body, ty, params, attrs) ->
1877 | Some body -> Some (pack_coercion [] [] body)
1879 let ty = pack_coercion [] [] ty in
1880 C.Variable (name, body, ty, params, attrs)
1881 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1882 let conjectures = pack_coercion_metasenv conjectures in
1883 let body = pack_coercion conjectures [] body in
1884 let ty = pack_coercion conjectures [] ty in
1885 C.CurrentProof (name, conjectures, body, ty, params, attrs)
1886 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1889 (fun (name, ind, arity, cl) ->
1890 let arity = pack_coercion [] [] arity in
1892 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
1894 (name, ind, arity, cl))
1897 C.InductiveDefinition (indtys, params, leftno, attrs)
1902 let type_of_aux' metasenv context term =
1905 type_of_aux' metasenv context term in
1907 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1909 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1912 | RefineFailure msg as e ->
1913 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1915 | Uncertain msg as e ->
1916 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1920 let profiler2 = HExtlib.profile "CicRefine"
1922 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1923 profiler2.HExtlib.profile
1924 (type_of_aux' ?localization_tbl metasenv context term) ugraph
1926 let typecheck ~localization_tbl metasenv uri obj =
1927 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
1929 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
1930 (* vim:set foldmethod=marker: *)