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 | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
82 | Sys.Break -> raise exn
83 | _ -> prerr_endline (Printexc.to_string exn); assert false
87 Cic.CicHash.find localization_tbl t
89 prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
92 raise (HExtlib.Localized (loc,exn'))
94 let relocalize localization_tbl oldt newt =
96 let infos = Cic.CicHash.find localization_tbl oldt in
97 Cic.CicHash.remove localization_tbl oldt;
98 Cic.CicHash.add localization_tbl newt infos;
106 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
107 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
110 let exp_impl metasenv subst context =
113 let (metasenv', idx) =
114 CicMkImplicit.mk_implicit_type metasenv subst context in
116 CicMkImplicit.identity_relocation_list_for_metavariable context in
117 metasenv', Cic.Meta (idx, irl)
119 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
120 metasenv', Cic.Meta (idx, [])
122 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
124 CicMkImplicit.identity_relocation_list_for_metavariable context in
125 metasenv', Cic.Meta (idx, irl)
129 let is_a_double_coercion t =
131 let rec aux acc = function
133 | x::tl -> aux (acc@[x]) tl
138 let imp = Cic.Implicit None in
139 let dummyres = false,imp, imp,imp,imp in
141 | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
142 (match last_of tl with
143 | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
144 let sib2,head = last_of tl2 in
145 true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
150 let more_args_than_expected
151 localization_tbl metasenv subst he context hetype' tlbody_and_type exn
155 CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
156 " (that has type "^CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
157 ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
158 " arguments that are more than expected")
160 enrich localization_tbl he ~f:(fun _-> msg) exn
163 let mk_prod_of_metas metasenv context' subst args =
164 let rec mk_prod metasenv context' = function
166 let (metasenv, idx) =
167 CicMkImplicit.mk_implicit_type metasenv subst context'
170 CicMkImplicit.identity_relocation_list_for_metavariable context'
172 metasenv,Cic.Meta (idx, irl)
174 let (metasenv, idx) =
175 CicMkImplicit.mk_implicit_type metasenv subst context'
178 CicMkImplicit.identity_relocation_list_for_metavariable context'
180 let meta = Cic.Meta (idx,irl) in
182 (* The name must be fresh for context. *)
183 (* Nevertheless, argty is well-typed only in context. *)
184 (* Thus I generate a name (name_hint) in context and *)
185 (* then I generate a name --- using the hint name_hint *)
186 (* --- that is fresh in context'. *)
188 (* Cic.Name "pippo" *)
189 FreshNamesGenerator.mk_fresh_name ~subst metasenv
190 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
191 (CicMetaSubst.apply_subst_context subst context')
193 ~typ:(CicMetaSubst.apply_subst subst argty)
195 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
196 FreshNamesGenerator.mk_fresh_name ~subst
197 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
199 let metasenv,target =
200 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
202 metasenv,Cic.Prod (name,meta,target)
204 mk_prod metasenv context' args
207 let rec type_of_constant uri ugraph =
208 let module C = Cic in
209 let module R = CicReduction in
210 let module U = UriManager in
211 let _ = CicTypeChecker.typecheck uri in
214 CicEnvironment.get_cooked_obj ugraph uri
215 with Not_found -> assert false
218 C.Constant (_,_,ty,_,_) -> ty,u
219 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
223 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
225 and type_of_variable uri ugraph =
226 let module C = Cic in
227 let module R = CicReduction in
228 let module U = UriManager in
229 let _ = CicTypeChecker.typecheck uri in
232 CicEnvironment.get_cooked_obj ugraph uri
233 with Not_found -> assert false
236 C.Variable (_,_,ty,_,_) -> ty,u
240 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
242 and type_of_mutual_inductive_defs uri i ugraph =
243 let module C = Cic in
244 let module R = CicReduction in
245 let module U = UriManager in
246 let _ = CicTypeChecker.typecheck uri in
249 CicEnvironment.get_cooked_obj ugraph uri
250 with Not_found -> assert false
253 C.InductiveDefinition (dl,_,_,_) ->
254 let (_,_,arity,_) = List.nth dl i in
259 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
261 and type_of_mutual_inductive_constr uri i j ugraph =
262 let module C = Cic in
263 let module R = CicReduction in
264 let module U = UriManager in
265 let _ = CicTypeChecker.typecheck uri in
268 CicEnvironment.get_cooked_obj ugraph uri
269 with Not_found -> assert false
272 C.InductiveDefinition (dl,_,_,_) ->
273 let (_,_,_,cl) = List.nth dl i in
274 let (_,ty) = List.nth cl (j-1) in
280 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
283 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
285 (* the check_branch function checks if a branch of a case is refinable.
286 It returns a pair (outype_instance,args), a subst and a metasenv.
287 outype_instance is the expected result of applying the case outtype
289 The problem is that outype is in general unknown, and we should
290 try to synthesize it from the above information, that is in general
291 a second order unification problem. *)
293 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
294 let module C = Cic in
295 (* let module R = CicMetaSubst in *)
296 let module R = CicReduction in
297 match R.whd ~subst context expectedtype with
299 (n,context,actualtype, [term]), subst, metasenv, ugraph
300 | C.Appl (C.MutInd (_,_,_)::tl) ->
301 let (_,arguments) = split tl left_args_no in
302 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
303 | C.Prod (name,so,de) ->
304 (* we expect that the actual type of the branch has the due
306 (match R.whd ~subst context actualtype with
307 C.Prod (name',so',de') ->
308 let subst, metasenv, ugraph1 =
309 fo_unif_subst subst context metasenv so so' ugraph in
311 (match CicSubstitution.lift 1 term with
312 C.Appl l -> C.Appl (l@[C.Rel 1])
313 | t -> C.Appl [t ; C.Rel 1]) in
314 (* we should also check that the name variable is anonymous in
315 the actual type de' ?? *)
317 ((Some (name,(C.Decl so)))::context)
318 metasenv subst left_args_no de' term' de ugraph1
319 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
320 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
322 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
325 let rec type_of_aux subst metasenv context t ugraph =
326 let module C = Cic in
327 let module S = CicSubstitution in
328 let module U = UriManager in
329 let try_coercion t subst context ugraph coercion_tgt (metasenv,last,coerced) =
330 let subst,metasenv,ugraph =
331 fo_unif_subst subst context metasenv last t ugraph
334 let newt, tty, subst, metasenv, ugraph =
335 avoid_double_coercion context subst metasenv ugraph coerced
338 Some (newt, tty, subst, metasenv, ugraph)
340 | RefineFailure _ | Uncertain _ -> None
342 let (t',_,_,_,_) as res =
347 match List.nth context (n - 1) with
348 Some (_,C.Decl ty) ->
349 t,S.lift n ty,subst,metasenv, ugraph
350 | Some (_,C.Def (_,Some ty)) ->
351 t,S.lift n ty,subst,metasenv, ugraph
352 | Some (_,C.Def (bo,None)) ->
354 (* if it is in the context it must be already well-typed*)
355 CicTypeChecker.type_of_aux' ~subst metasenv context
358 t,ty,subst,metasenv,ugraph
360 enrich localization_tbl t
361 (RefineFailure (lazy "Rel to hidden hypothesis"))
364 enrich localization_tbl t
365 (RefineFailure (lazy "Not a closed term")))
366 | C.Var (uri,exp_named_subst) ->
367 let exp_named_subst',subst',metasenv',ugraph1 =
368 check_exp_named_subst
369 subst metasenv context exp_named_subst ugraph
371 let ty_uri,ugraph1 = type_of_variable uri ugraph in
373 CicSubstitution.subst_vars exp_named_subst' ty_uri
375 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
378 let (canonical_context, term,ty) =
379 CicUtil.lookup_subst n subst
381 let l',subst',metasenv',ugraph1 =
382 check_metasenv_consistency n subst metasenv context
383 canonical_context l ugraph
385 (* trust or check ??? *)
386 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
387 subst', metasenv', ugraph1
388 (* type_of_aux subst metasenv
389 context (CicSubstitution.subst_meta l term) *)
390 with CicUtil.Subst_not_found _ ->
391 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
392 let l',subst',metasenv', ugraph1 =
393 check_metasenv_consistency n subst metasenv context
394 canonical_context l ugraph
396 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
397 subst', metasenv',ugraph1)
398 | C.Sort (C.Type tno) ->
399 let tno' = CicUniv.fresh() in
401 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
402 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
404 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
406 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
407 | C.Implicit infos ->
408 let metasenv',t' = exp_impl metasenv subst context infos in
409 type_of_aux subst metasenv' context t' ugraph
411 let ty',_,subst',metasenv',ugraph1 =
412 type_of_aux subst metasenv context ty ugraph
414 let te',inferredty,subst'',metasenv'',ugraph2 =
415 type_of_aux subst' metasenv' context te ugraph1
418 let subst''',metasenv''',ugraph3 =
419 fo_unif_subst subst'' context metasenv''
420 inferredty ty' ugraph2
422 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
425 enrich localization_tbl te'
427 lazy ("(3)The term " ^
428 CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
429 context ^ " has type " ^
430 CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty
431 context ^ " but is here used with type " ^
432 CicMetaSubst.ppterm_in_context metasenv'' subst'' ty' context)) exn
434 | C.Prod (name,s,t) ->
435 let carr t subst context = CicMetaSubst.apply_subst subst t in
436 let coerce_to_sort in_source tgt_sort t type_to_coerce
437 subst context metasenv uragph
439 if not !insert_coercions then
440 t,type_to_coerce,subst,metasenv,ugraph
442 let coercion_src = carr type_to_coerce subst context in
443 match coercion_src with
445 t,type_to_coerce,subst,metasenv,ugraph
446 | Cic.Meta _ as meta ->
447 t, meta, subst, metasenv, ugraph
448 | Cic.Cast _ as cast ->
449 t, cast, subst, metasenv, ugraph
451 let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
453 CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
456 | CoercGraph.NoCoercion
457 | CoercGraph.SomeCoercionToTgt _
458 | CoercGraph.NotHandled _ ->
459 enrich localization_tbl t
461 (lazy ("(4)The term " ^
462 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
463 " is not a type since it has type " ^
464 CicMetaSubst.ppterm_in_context ~metasenv
465 subst coercion_src context ^ " that is not a sort")))
466 | CoercGraph.NotMetaClosed ->
467 enrich localization_tbl t
469 (lazy ("(5)The term " ^
470 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
471 " is not a type since it has type " ^
472 CicMetaSubst.ppterm_in_context ~metasenv
473 subst coercion_src context ^ " that is not a sort")))
474 | CoercGraph.SomeCoercion candidates ->
477 (try_coercion t subst context ugraph coercion_tgt)
483 enrich localization_tbl t
485 (lazy ("(6)The term " ^
486 CicMetaSubst.ppterm_in_context ~metasenv
488 " is not a type since it has type " ^
489 CicMetaSubst.ppterm_in_context ~metasenv
490 subst coercion_src context ^
491 " that is not a sort"))))
493 let s',sort1,subst',metasenv',ugraph1 =
494 type_of_aux subst metasenv context s ugraph
496 let s',sort1,subst', metasenv',ugraph1 =
497 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
498 s' sort1 subst' context metasenv' ugraph1
500 let context_for_t = ((Some (name,(C.Decl s')))::context) in
501 let t',sort2,subst'',metasenv'',ugraph2 =
502 type_of_aux subst' metasenv'
503 context_for_t t ugraph1
505 let t',sort2,subst'',metasenv'',ugraph2 =
506 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
507 t' sort2 subst'' context_for_t metasenv'' ugraph2
509 let sop,subst''',metasenv''',ugraph3 =
510 sort_of_prod localization_tbl subst'' metasenv''
511 context (name,s') t' (sort1,sort2) ugraph2
513 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
514 | C.Lambda (n,s,t) ->
515 let s',sort1,subst',metasenv',ugraph1 =
516 type_of_aux subst metasenv context s ugraph in
517 let s',sort1,subst',metasenv',ugraph1 =
518 if not !insert_coercions then
519 s',sort1, subst', metasenv', ugraph1
521 match CicReduction.whd ~subst:subst' context sort1 with
522 | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
524 let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
526 CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
529 | CoercGraph.NoCoercion
530 | CoercGraph.SomeCoercionToTgt _
531 | CoercGraph.NotHandled _ ->
532 enrich localization_tbl s'
534 (lazy ("(7)The term " ^
535 CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
536 " is not a type since it has type " ^
537 CicMetaSubst.ppterm_in_context ~metasenv
538 subst coercion_src context ^ " that is not a sort")))
539 | CoercGraph.NotMetaClosed ->
540 enrich localization_tbl s'
542 (lazy ("(8)The term " ^
543 CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
544 " is not a type since it has type " ^
545 CicMetaSubst.ppterm_in_context ~metasenv
546 subst coercion_src context ^ " that is not a sort")))
547 | CoercGraph.SomeCoercion candidates ->
550 (try_coercion s' subst' context ugraph1 coercion_tgt)
556 enrich localization_tbl s'
558 (lazy ("(9)The term " ^
559 CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
560 " is not a type since it has type " ^
561 CicMetaSubst.ppterm_in_context ~metasenv
562 subst coercion_src context ^
563 " that is not a sort")))
565 let context_for_t = ((Some (n,(C.Decl s')))::context) in
566 let t',type2,subst'',metasenv'',ugraph2 =
567 type_of_aux subst' metasenv' context_for_t t ugraph1
569 C.Lambda (n,s',t'),C.Prod (n,s',type2),
570 subst'',metasenv'',ugraph2
572 (* only to check if s is well-typed *)
573 let s',ty,subst',metasenv',ugraph1 =
574 type_of_aux subst metasenv context s ugraph
576 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
578 let t',inferredty,subst'',metasenv'',ugraph2 =
579 type_of_aux subst' metasenv'
580 context_for_t t ugraph1
582 (* One-step LetIn reduction.
583 * Even faster than the previous solution.
584 * Moreover the inferred type is closer to the expected one.
587 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
588 subst'',metasenv'',ugraph2
589 | C.Appl (he::((_::_) as tl)) ->
590 let he',hetype,subst',metasenv',ugraph1 =
591 type_of_aux subst metasenv context he ugraph
593 let tlbody_and_type,subst'',metasenv'',ugraph2 =
594 typeof_list subst' metasenv' context ugraph1 tl
596 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
597 eat_prods true subst'' metasenv'' context
598 he' hetype tlbody_and_type ugraph2
600 let newappl = (C.Appl (coerced_he::coerced_args)) in
601 avoid_double_coercion
602 context subst''' metasenv''' ugraph3 newappl applty
603 | C.Appl _ -> assert false
604 | C.Const (uri,exp_named_subst) ->
605 let exp_named_subst',subst',metasenv',ugraph1 =
606 check_exp_named_subst subst metasenv context
607 exp_named_subst ugraph in
608 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
610 CicSubstitution.subst_vars exp_named_subst' ty_uri
612 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
613 | C.MutInd (uri,i,exp_named_subst) ->
614 let exp_named_subst',subst',metasenv',ugraph1 =
615 check_exp_named_subst subst metasenv context
616 exp_named_subst ugraph
618 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
620 CicSubstitution.subst_vars exp_named_subst' ty_uri in
621 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
622 | C.MutConstruct (uri,i,j,exp_named_subst) ->
623 let exp_named_subst',subst',metasenv',ugraph1 =
624 check_exp_named_subst subst metasenv context
625 exp_named_subst ugraph
628 type_of_mutual_inductive_constr uri i j ugraph1
631 CicSubstitution.subst_vars exp_named_subst' ty_uri
633 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
635 | C.MutCase (uri, i, outtype, term, pl) ->
636 (* first, get the inductive type (and noparams)
637 * in the environment *)
638 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
639 let _ = CicTypeChecker.typecheck uri in
640 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
642 C.InductiveDefinition (l,expl_params,parsno,_) ->
643 List.nth l i , expl_params, parsno, u
645 enrich localization_tbl t
647 (lazy ("Unkown mutual inductive definition " ^
648 U.string_of_uri uri)))
650 let rec count_prod t =
651 match CicReduction.whd ~subst context t with
652 C.Prod (_, _, t) -> 1 + (count_prod t)
655 let no_args = count_prod arity in
656 (* now, create a "generic" MutInd *)
657 let metasenv,left_args =
658 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
660 let metasenv,right_args =
661 let no_right_params = no_args - no_left_params in
662 if no_right_params < 0 then assert false
663 else CicMkImplicit.n_fresh_metas
664 metasenv subst context no_right_params
666 let metasenv,exp_named_subst =
667 CicMkImplicit.fresh_subst metasenv subst context expl_params in
670 C.MutInd (uri,i,exp_named_subst)
673 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
675 (* check consistency with the actual type of term *)
676 let term',actual_type,subst,metasenv,ugraph1 =
677 type_of_aux subst metasenv context term ugraph in
678 let expected_type',_, subst, metasenv,ugraph2 =
679 type_of_aux subst metasenv context expected_type ugraph1
681 let actual_type = CicReduction.whd ~subst context actual_type in
682 let subst,metasenv,ugraph3 =
684 fo_unif_subst subst context metasenv
685 expected_type' actual_type ugraph2
688 prerr_endline (CicMetaSubst.ppmetasenv subst metasenv);
689 prerr_endline (CicMetaSubst.ppsubst subst ~metasenv);
690 enrich localization_tbl term' exn
692 lazy ("(10)The term " ^
693 CicMetaSubst.ppterm_in_context ~metasenv subst term'
694 context ^ " has type " ^
695 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
696 context ^ " but is here used with type " ^
697 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
699 let rec instantiate_prod t =
703 match CicReduction.whd ~subst context t with
705 instantiate_prod (CicSubstitution.subst he t') tl
708 let arity_instantiated_with_left_args =
709 instantiate_prod arity left_args in
710 (* TODO: check if the sort elimination
711 * is allowed: [(I q1 ... qr)|B] *)
712 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
714 (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
716 if left_args = [] then
717 (C.MutConstruct (uri,i,j,exp_named_subst))
720 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
722 let p',actual_type,subst,metasenv,ugraph1 =
723 type_of_aux subst metasenv context p ugraph
725 let constructor',expected_type, subst, metasenv,ugraph2 =
726 type_of_aux subst metasenv context constructor ugraph1
728 let outtypeinstance,subst,metasenv,ugraph3 =
730 check_branch 0 context metasenv subst
731 no_left_params actual_type constructor' expected_type
735 enrich localization_tbl constructor'
737 lazy ("(11)The term " ^
738 CicMetaSubst.ppterm_in_context metasenv subst p'
739 context ^ " has type " ^
740 CicMetaSubst.ppterm_in_context metasenv subst actual_type
741 context ^ " but is here used with type " ^
742 CicMetaSubst.ppterm_in_context metasenv subst expected_type
746 outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
747 pl ([],List.length pl,[],subst,metasenv,ugraph3)
750 (* we are left to check that the outype matches his instances.
751 The easy case is when the outype is specified, that amount
752 to a trivial check. Otherwise, we should guess a type from
756 let outtype,outtypety, subst, metasenv,ugraph4 =
757 type_of_aux subst metasenv context outtype ugraph4 in
760 (let candidate,ugraph5,metasenv,subst =
761 let exp_name_subst, metasenv =
763 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
765 let uris = CicUtil.params_of_obj o in
767 fun uri (acc,metasenv) ->
768 let metasenv',new_meta =
769 CicMkImplicit.mk_implicit metasenv subst context
772 CicMkImplicit.identity_relocation_list_for_metavariable
775 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
779 match left_args,right_args with
780 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
782 let rec mk_right_args =
785 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
787 let right_args_no = List.length right_args in
788 let lifted_left_args =
789 List.map (CicSubstitution.lift right_args_no) left_args
791 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
792 (lifted_left_args @ mk_right_args right_args_no))
795 FreshNamesGenerator.mk_fresh_name ~subst metasenv
796 context Cic.Anonymous ~typ:ty
798 match outtypeinstances with
800 let extended_context =
801 let rec add_right_args =
803 Cic.Prod (name,ty,t) ->
804 Some (name,Cic.Decl ty)::(add_right_args t)
807 (Some (fresh_name,Cic.Decl ty))::
809 (add_right_args arity_instantiated_with_left_args))@
812 let metasenv,new_meta =
813 CicMkImplicit.mk_implicit metasenv subst extended_context
816 CicMkImplicit.identity_relocation_list_for_metavariable
819 let rec add_lambdas b =
821 Cic.Prod (name,ty,t) ->
822 Cic.Lambda (name,ty,(add_lambdas b t))
823 | _ -> Cic.Lambda (fresh_name, ty, b)
826 add_lambdas (Cic.Meta (new_meta,irl))
827 arity_instantiated_with_left_args
829 (Some candidate),ugraph4,metasenv,subst
830 | (constructor_args_no,_,instance,_)::tl ->
832 let instance',subst,metasenv =
833 CicMetaSubst.delift_rels subst metasenv
834 constructor_args_no instance
836 let candidate,ugraph,metasenv,subst =
838 fun (candidate_oty,ugraph,metasenv,subst)
839 (constructor_args_no,_,instance,_) ->
840 match candidate_oty with
841 | None -> None,ugraph,metasenv,subst
844 let instance',subst,metasenv =
845 CicMetaSubst.delift_rels subst metasenv
846 constructor_args_no instance
848 let subst,metasenv,ugraph =
849 fo_unif_subst subst context metasenv
852 candidate_oty,ugraph,metasenv,subst
854 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
855 | CicUnification.UnificationFailure _
856 | CicUnification.Uncertain _ ->
857 None,ugraph,metasenv,subst
858 ) (Some instance',ugraph4,metasenv,subst) tl
861 | None -> None, ugraph,metasenv,subst
863 let rec add_lambdas n b =
865 Cic.Prod (name,ty,t) ->
866 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
868 Cic.Lambda (fresh_name, ty,
869 CicSubstitution.lift (n + 1) t)
872 (add_lambdas 0 t arity_instantiated_with_left_args),
873 ugraph,metasenv,subst
874 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
875 None,ugraph4,metasenv,subst
878 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
880 let subst,metasenv,ugraph =
882 fo_unif_subst subst context metasenv
883 candidate outtype ugraph5
885 exn -> assert false(* unification against a metavariable *)
887 C.MutCase (uri, i, outtype, term', pl'),
888 CicReduction.head_beta_reduce
889 (CicMetaSubst.apply_subst subst
890 (Cic.Appl (outtype::right_args@[term']))),
891 subst,metasenv,ugraph)
892 | _ -> (* easy case *)
893 let tlbody_and_type,subst,metasenv,ugraph4 =
894 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
896 let _,_,_,subst,metasenv,ugraph4 =
897 eat_prods false subst metasenv context
898 outtype outtypety tlbody_and_type ugraph4
900 let _,_, subst, metasenv,ugraph5 =
901 type_of_aux subst metasenv context
902 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
904 let (subst,metasenv,ugraph6) =
906 (fun (subst,metasenv,ugraph)
907 p (constructor_args_no,context,instance,args)
912 CicSubstitution.lift constructor_args_no outtype
914 C.Appl (outtype'::args)
916 CicReduction.whd ~subst context appl
919 fo_unif_subst subst context metasenv instance instance'
923 enrich localization_tbl p exn
925 lazy ("(12)The term " ^
926 CicMetaSubst.ppterm_in_context ~metasenv subst p
927 context ^ " has type " ^
928 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
929 context ^ " but is here used with type " ^
930 CicMetaSubst.ppterm_in_context ~metasenv subst instance
932 (subst,metasenv,ugraph5) pl' outtypeinstances
934 C.MutCase (uri, i, outtype, term', pl'),
935 CicReduction.head_beta_reduce
936 (CicMetaSubst.apply_subst subst
937 (C.Appl(outtype::right_args@[term]))),
938 subst,metasenv,ugraph6)
940 let fl_ty',subst,metasenv,types,ugraph1,len =
942 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
943 let ty',_,subst',metasenv',ugraph1 =
944 type_of_aux subst metasenv context ty ugraph
946 fl @ [ty'],subst',metasenv',
947 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
948 :: types, ugraph, len+1
949 ) ([],subst,metasenv,[],ugraph,0) fl
951 let context' = types@context in
952 let fl_bo',subst,metasenv,ugraph2 =
954 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
955 let bo',ty_of_bo,subst,metasenv,ugraph1 =
956 type_of_aux subst metasenv context' bo ugraph in
957 let expected_ty = CicSubstitution.lift len ty in
958 let subst',metasenv',ugraph' =
960 fo_unif_subst subst context' metasenv
961 ty_of_bo expected_ty ugraph1
964 enrich localization_tbl bo exn
966 lazy ("(13)The term " ^
967 CicMetaSubst.ppterm_in_context ~metasenv subst bo
968 context' ^ " has type " ^
969 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
970 context' ^ " but is here used with type " ^
971 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
974 fl @ [bo'] , subst',metasenv',ugraph'
975 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
977 let ty = List.nth fl_ty' i in
978 (* now we have the new ty in fl_ty', the new bo in fl_bo',
979 * and we want the new fl with bo' and ty' injected in the right
982 let rec map3 f l1 l2 l3 =
985 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
988 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
991 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
993 let fl_ty',subst,metasenv,types,ugraph1,len =
995 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
996 let ty',_,subst',metasenv',ugraph1 =
997 type_of_aux subst metasenv context ty ugraph
999 fl @ [ty'],subst',metasenv',
1000 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
1001 types, ugraph1, len+1
1002 ) ([],subst,metasenv,[],ugraph,0) fl
1004 let context' = types@context in
1005 let fl_bo',subst,metasenv,ugraph2 =
1007 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
1008 let bo',ty_of_bo,subst,metasenv,ugraph1 =
1009 type_of_aux subst metasenv context' bo ugraph in
1010 let expected_ty = CicSubstitution.lift len ty in
1011 let subst',metasenv',ugraph' =
1013 fo_unif_subst subst context' metasenv
1014 ty_of_bo expected_ty ugraph1
1017 enrich localization_tbl bo exn
1019 lazy ("(14)The term " ^
1020 CicMetaSubst.ppterm_in_context ~metasenv subst bo
1021 context' ^ " has type " ^
1022 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
1023 context' ^ " but is here used with type " ^
1024 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
1027 fl @ [bo'],subst',metasenv',ugraph'
1028 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
1030 let ty = List.nth fl_ty' i in
1031 (* now we have the new ty in fl_ty', the new bo in fl_bo',
1032 * and we want the new fl with bo' and ty' injected in the right
1035 let rec map3 f l1 l2 l3 =
1038 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
1041 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
1044 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
1046 relocalize localization_tbl t t';
1049 (* check_metasenv_consistency checks that the "canonical" context of a
1050 metavariable is consitent - up to relocation via the relocation list l -
1051 with the actual context *)
1052 and check_metasenv_consistency
1053 metano subst metasenv context canonical_context l ugraph
1055 let module C = Cic in
1056 let module R = CicReduction in
1057 let module S = CicSubstitution in
1058 let lifted_canonical_context =
1062 | (Some (n,C.Decl t))::tl ->
1063 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
1064 | (Some (n,C.Def (t,None)))::tl ->
1065 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1066 | None::tl -> None::(aux (i+1) tl)
1067 | (Some (n,C.Def (t,Some ty)))::tl ->
1069 C.Def ((S.subst_meta l (S.lift i t)),
1070 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
1072 aux 1 canonical_context
1076 (fun (l,subst,metasenv,ugraph) t ct ->
1079 l @ [None],subst,metasenv,ugraph
1080 | Some t,Some (_,C.Def (ct,_)) ->
1081 let subst',metasenv',ugraph' =
1083 prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
1084 fo_unif_subst subst context metasenv t ct ugraph
1085 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))))))
1087 l @ [Some t],subst',metasenv',ugraph'
1088 | Some t,Some (_,C.Decl ct) ->
1089 let t',inferredty,subst',metasenv',ugraph1 =
1090 type_of_aux subst metasenv context t ugraph
1092 let subst'',metasenv'',ugraph2 =
1095 subst' context metasenv' inferredty ct ugraph1
1096 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))))))
1098 l @ [Some t'], subst'',metasenv'',ugraph2
1100 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
1102 Invalid_argument _ ->
1106 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1107 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1108 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1110 and check_exp_named_subst metasubst metasenv context tl ugraph =
1111 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1113 [] -> [],metasubst,metasenv,ugraph
1115 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1117 CicSubstitution.subst_vars substs ty_uri in
1118 (* CSC: why was this code here? it is wrong
1119 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1120 Cic.Variable (_,Some bo,_,_) ->
1122 (RefineFailure (lazy
1123 "A variable with a body can not be explicit substituted"))
1124 | Cic.Variable (_,None,_,_) -> ()
1127 (RefineFailure (lazy
1128 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1131 let t',typeoft,metasubst',metasenv',ugraph2 =
1132 type_of_aux metasubst metasenv context t ugraph1 in
1133 let subst = uri,t' in
1134 let metasubst'',metasenv'',ugraph3 =
1137 metasubst' context metasenv' typeoft typeofvar ugraph2
1139 raise (RefineFailure (lazy
1140 ("Wrong Explicit Named Substitution: " ^
1141 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1142 " not unifiable with " ^
1143 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1145 (* FIXME: no mere tail recursive! *)
1146 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1147 check_exp_named_subst_aux
1148 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1150 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1152 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1155 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1158 let module C = Cic in
1159 let context_for_t2 = (Some (name,C.Decl s))::context in
1160 let t1'' = CicReduction.whd ~subst context t1 in
1161 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1162 match (t1'', t2'') with
1163 (C.Sort s1, C.Sort s2)
1164 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1165 (* different than Coq manual!!! *)
1166 C.Sort s2,subst,metasenv,ugraph
1167 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1168 let t' = CicUniv.fresh() in
1170 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1171 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1172 C.Sort (C.Type t'),subst,metasenv,ugraph2
1174 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1175 | (C.Sort _,C.Sort (C.Type t1)) ->
1176 C.Sort (C.Type t1),subst,metasenv,ugraph
1177 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1178 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1179 (* TODO how can we force the meta to become a sort? If we don't we
1180 * break the invariant that refine produce only well typed terms *)
1181 (* TODO if we check the non meta term and if it is a sort then we
1182 * are likely to know the exact value of the result e.g. if the rhs
1183 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1184 let (metasenv,idx) =
1185 CicMkImplicit.mk_implicit_sort metasenv subst in
1186 let (subst, metasenv,ugraph1) =
1188 fo_unif_subst subst context_for_t2 metasenv
1189 (C.Meta (idx,[])) t2'' ugraph
1190 with _ -> assert false (* unification against a metavariable *)
1192 t2'',subst,metasenv,ugraph1
1195 enrich localization_tbl s
1199 "%s is supposed to be a type, but its type is %s"
1200 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1201 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1203 enrich localization_tbl t
1207 "%s is supposed to be a type, but its type is %s"
1208 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1209 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1211 and avoid_double_coercion context subst metasenv ugraph t ty =
1212 if not !pack_coercions then
1213 t,ty,subst,metasenv,ugraph
1215 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1217 let source_carr = CoercGraph.source_of c2 in
1218 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1219 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1221 | CoercGraph.SomeCoercion candidates ->
1223 HExtlib.list_findopt
1224 (function (metasenv,last,c) ->
1226 | c when not (CoercGraph.is_composite c) ->
1227 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1230 let subst,metasenv,ugraph =
1231 fo_unif_subst subst context metasenv last head ugraph in
1232 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1237 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1238 let newt,_,subst,metasenv,ugraph =
1239 type_of_aux subst metasenv context c ugraph in
1240 debug_print (lazy "tipa...");
1241 let subst, metasenv, ugraph =
1242 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1243 fo_unif_subst subst context metasenv newt t ugraph
1245 debug_print (lazy "unifica...");
1246 Some (newt, ty, subst, metasenv, ugraph)
1248 | RefineFailure s | Uncertain s when not !pack_coercions->
1249 debug_print s; debug_print (lazy "stop\n");None
1250 | RefineFailure s | Uncertain s ->
1251 debug_print s;debug_print (lazy "goon\n");
1253 let old_pack_coercions = !pack_coercions in
1254 pack_coercions := false; (* to avoid diverging *)
1255 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1256 type_of_aux subst metasenv context c1_c2_implicit ugraph
1258 pack_coercions := old_pack_coercions;
1260 is_a_double_coercion refined_c1_c2_implicit
1266 match refined_c1_c2_implicit with
1267 | Cic.Appl l -> HExtlib.list_last l
1270 let subst, metasenv, ugraph =
1271 try fo_unif_subst subst context metasenv
1273 with RefineFailure s| Uncertain s->
1274 debug_print s;assert false
1276 let subst, metasenv, ugraph =
1277 fo_unif_subst subst context metasenv
1278 refined_c1_c2_implicit t ugraph
1280 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1282 | RefineFailure s | Uncertain s ->
1283 pack_coercions := true;debug_print s;None
1284 | exn -> pack_coercions := true; raise exn))
1287 (match selected with
1291 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1292 t, ty, subst, metasenv, ugraph)
1293 | _ -> t, ty, subst, metasenv, ugraph)
1295 t, ty, subst, metasenv, ugraph
1297 and typeof_list subst metasenv context ugraph l =
1298 let tlbody_and_type,subst,metasenv,ugraph =
1300 (fun x (res,subst,metasenv,ugraph) ->
1301 let x',ty,subst',metasenv',ugraph1 =
1302 type_of_aux subst metasenv context x ugraph
1304 (x', ty)::res,subst',metasenv',ugraph1
1305 ) l ([],subst,metasenv,ugraph)
1307 tlbody_and_type,subst,metasenv,ugraph
1310 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1312 (* aux function to add coercions to funclass *)
1313 let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph =
1315 let pristinemenv = metasenv in
1316 let metasenv,hetype' =
1317 mk_prod_of_metas metasenv context subst args_bo_and_ty
1320 let subst,metasenv,ugraph =
1321 fo_unif_subst_eat_prods
1322 subst context metasenv hetype hetype' ugraph
1324 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1325 with RefineFailure s | Uncertain s as exn
1326 when allow_coercions && !insert_coercions ->
1327 (* {{{ we search a coercion of the head (saturated) to funclass *)
1328 let metasenv = pristinemenv in
1330 ("Fixing arity of: "^CicMetaSubst.ppterm ~metasenv subst hetype ^
1331 " since unif failed with: " ^ CicMetaSubst.ppterm ~metasenv subst hetype'
1332 (* ^ " cause: " ^ Lazy.force s *)));
1333 let how_many_args_are_needed =
1334 let rec aux n = function
1335 | Cic.Prod(_,_,t) -> aux (n+1) t
1338 aux 0 (CicMetaSubst.apply_subst subst hetype)
1340 let args, remainder =
1341 HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
1343 let args = List.map fst args in
1347 | Cic.Appl l -> Cic.Appl (l@args)
1348 | _ -> Cic.Appl (he::args)
1352 let x,xty,subst,metasenv,ugraph =
1353 (*CSC: here unsharing is necessary to avoid an unwanted
1354 relocalization. However, this also shows a great source of
1355 inefficiency: "x" is refined twice (once now and once in the
1356 subsequent eat_prods_and_args). Morevoer, how is divergence avoided?
1358 type_of_aux subst metasenv context (Unshare.unshare x) ugraph
1361 CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty)
1363 let carr_tgt = CoercDb.Fun 0 in
1364 match CoercGraph.look_for_coercion' metasenv subst context carr_src carr_tgt with
1365 | CoercGraph.NoCoercion
1366 | CoercGraph.NotMetaClosed
1367 | CoercGraph.NotHandled _ -> raise exn
1368 | CoercGraph.SomeCoercionToTgt candidates
1369 | CoercGraph.SomeCoercion candidates ->
1371 HExtlib.list_findopt
1372 (fun (metasenv,last,coerc) ->
1373 let subst,metasenv,ugraph =
1374 fo_unif_subst subst context metasenv last x ugraph in
1375 debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc));
1377 (* we want this to be available in the error handler fo the
1378 * following (so it has its own try. *)
1379 let t,tty,subst,metasenv,ugraph =
1380 type_of_aux subst metasenv context coerc ugraph
1383 let metasenv, hetype' =
1384 mk_prod_of_metas metasenv context subst remainder
1387 (" unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^
1388 CicMetaSubst.ppterm ~metasenv subst hetype'));
1389 let subst,metasenv,ugraph =
1390 fo_unif_subst_eat_prods
1391 subst context metasenv tty hetype' ugraph
1393 debug_print (lazy " success!");
1394 Some (subst,metasenv,ugraph,tty,t,remainder)
1396 | Uncertain _ | RefineFailure _
1397 | CicUnification.UnificationFailure _
1398 | CicUnification.Uncertain _ ->
1400 let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
1402 metasenv context subst t tty remainder ugraph
1404 Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
1405 with Uncertain _ | RefineFailure _ -> None
1409 | HExtlib.Localized (_,Uncertain _)
1410 | HExtlib.Localized (_,RefineFailure _) -> None
1411 | exn -> assert false) (* ritornare None, e' un localized *)
1414 | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
1415 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1417 more_args_than_expected localization_tbl metasenv
1418 subst he context hetype args_bo_and_ty exn
1419 (* }}} end coercion to funclass stuff *)
1420 (* }}} end fix_arity *)
1422 (* aux function to process the type of the head and the args in parallel *)
1423 let rec eat_prods_and_args
1424 pristinemenv metasenv subst context pristinehe he hetype ugraph newargs
1428 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1429 | (hete, hety)::tl ->
1430 match (CicReduction.whd ~subst context hetype) with
1431 | Cic.Prod (n,s,t) ->
1432 let arg,subst,metasenv,ugraph1 =
1434 let subst,metasenv,ugraph1 =
1435 fo_unif_subst_eat_prods2
1436 subst context metasenv hety s ugraph
1438 (hete,hety),subst,metasenv,ugraph1
1439 (* {{{ we search a coercion from hety to s if fails *)
1440 with RefineFailure _ | Uncertain _ as exn
1441 when allow_coercions && !insert_coercions ->
1442 let coer, tgt_carr =
1443 let carr t subst context =
1444 CicReduction.whd ~delta:false
1445 context (CicMetaSubst.apply_subst subst t )
1447 let c_hety = carr hety subst context in
1448 let c_s = carr s subst context in
1449 CoercGraph.look_for_coercion metasenv subst context c_hety c_s, c_s
1452 | CoercGraph.NoCoercion
1453 | CoercGraph.SomeCoercionToTgt _
1454 | CoercGraph.NotHandled _ ->
1455 enrich localization_tbl hete exn
1457 (lazy ("(15)The term " ^
1458 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1459 context ^ " has type " ^
1460 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1461 context ^ " but is here used with type " ^
1462 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1463 (* "\nReason: " ^ Lazy.force e*))))
1464 | CoercGraph.NotMetaClosed ->
1465 enrich localization_tbl hete exn
1467 (lazy ("(16)The term " ^
1468 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1469 context ^ " has type " ^
1470 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1471 context ^ " but is here used with type " ^
1472 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1473 (* "\nReason: " ^ Lazy.force e*))))
1474 | CoercGraph.SomeCoercion candidates ->
1476 HExtlib.list_findopt
1477 (fun (metasenv,last,c) ->
1479 let subst,metasenv,ugraph =
1480 fo_unif_subst subst context metasenv last hete
1482 let newt,newhety,subst,metasenv,ugraph =
1483 type_of_aux subst metasenv context
1486 let newt, newty, subst, metasenv, ugraph =
1487 avoid_double_coercion context subst metasenv
1488 ugraph newt tgt_carr
1490 let subst,metasenv,ugraph1 =
1491 fo_unif_subst subst context metasenv
1494 Some ((newt,newty), subst, metasenv, ugraph)
1495 with Uncertain _ | RefineFailure _ -> None)
1498 (match selected with
1501 enrich localization_tbl hete
1503 (lazy ("(1)The term " ^
1504 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1505 context ^ " has type " ^
1506 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1507 context ^ " but is here used with type " ^
1508 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1509 (* "\nReason: " ^ Lazy.force e*)))) exn))
1511 enrich localization_tbl hete
1513 (lazy ("(2)The term " ^
1514 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1515 context ^ " has type " ^
1516 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1517 context ^ " but is here used with type " ^
1518 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1519 (* "\nReason: " ^ Printexc.to_string exn*)))) exn
1520 (* }}} end coercion stuff *)
1522 eat_prods_and_args pristinemenv metasenv subst context pristinehe he
1523 (CicSubstitution.subst (fst arg) t)
1524 ugraph1 (newargs@[arg]) tl
1527 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1529 pristinemenv context subst he hetype
1530 (newargs@[hete,hety]@tl) ugraph
1532 eat_prods_and_args metasenv
1533 metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
1534 with RefineFailure _ | Uncertain _ as exn ->
1535 (* unable to fix arity *)
1536 more_args_than_expected localization_tbl metasenv
1537 subst he context hetype args_bo_and_ty exn
1540 (* first we check if we are in the simple case of a meta closed term *)
1541 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1542 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1543 (* this optimization is to postpone fix_arity (the most common case)*)
1544 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1546 (* this (says CSC) is also useful to infer dependent types *)
1548 fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
1549 with RefineFailure _ | Uncertain _ as exn ->
1550 (* unable to fix arity *)
1551 more_args_than_expected localization_tbl metasenv
1552 subst he context hetype args_bo_and_ty exn
1554 let coerced_args,subst,metasenv,he,t,ugraph =
1556 metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
1558 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1561 (* eat prods ends here! *)
1563 let t',ty,subst',metasenv',ugraph1 =
1564 type_of_aux [] metasenv context t ugraph
1566 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1567 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1568 (* Andrea: ho rimesso qui l'applicazione della subst al
1569 metasenv dopo che ho droppato l'invariante che il metsaenv
1570 e' sempre istanziato *)
1571 let substituted_metasenv =
1572 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1574 (* substituted_t,substituted_ty,substituted_metasenv *)
1575 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1577 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1579 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1580 let cleaned_metasenv =
1582 (function (n,context,ty) ->
1583 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1588 | Some (n, Cic.Decl t) ->
1590 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1591 | Some (n, Cic.Def (bo,ty)) ->
1592 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1597 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1599 Some (n, Cic.Def (bo',ty'))
1603 ) substituted_metasenv
1605 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1608 let undebrujin uri typesno tys t =
1611 (fun (name,_,_,_) (i,t) ->
1612 (* here the explicit_named_substituion is assumed to be *)
1614 let t' = Cic.MutInd (uri,i,[]) in
1615 let t = CicSubstitution.subst t' t in
1617 ) tys (typesno - 1,t))
1619 let map_first_n n start f g l =
1620 let rec aux acc k l =
1623 | [] -> raise (Invalid_argument "map_first_n")
1624 | hd :: tl -> f hd k (aux acc (k+1) tl)
1630 (*CSC: this is a very rough approximation; to be finished *)
1631 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1632 let subst,metasenv,ugraph,tys =
1634 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1635 let subst,metasenv,ugraph,cl =
1637 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1638 let rec aux ctx k subst = function
1639 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1640 let subst,metasenv,ugraph,tl =
1642 (subst,metasenv,ugraph,[])
1643 (fun t n (subst,metasenv,ugraph,acc) ->
1644 let subst,metasenv,ugraph =
1646 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1648 subst,metasenv,ugraph,(t::acc))
1649 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1652 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1653 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1654 subst,metasenv,ugraph,t
1655 | Cic.Prod (name,s,t) ->
1656 let ctx = (Some (name,Cic.Decl s))::ctx in
1657 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1658 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1662 (lazy "not well formed constructor type"))
1664 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1665 subst,metasenv,ugraph,(name,ty) :: acc)
1666 cl (subst,metasenv,ugraph,[])
1668 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1669 tys ([],metasenv,ugraph,[])
1671 let substituted_tys =
1673 (fun (name,ind,arity,cl) ->
1675 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1677 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1680 metasenv,ugraph,substituted_tys
1682 let typecheck metasenv uri obj ~localization_tbl =
1683 let ugraph = CicUniv.empty_ugraph in
1685 Cic.Constant (name,Some bo,ty,args,attrs) ->
1686 let bo',boty,metasenv,ugraph =
1687 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1688 let ty',_,metasenv,ugraph =
1689 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1690 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1691 let bo' = CicMetaSubst.apply_subst subst bo' in
1692 let ty' = CicMetaSubst.apply_subst subst ty' in
1693 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1694 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1695 | Cic.Constant (name,None,ty,args,attrs) ->
1696 let ty',_,metasenv,ugraph =
1697 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1699 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1700 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1701 assert (metasenv' = metasenv);
1702 (* Here we do not check the metasenv for correctness *)
1703 let bo',boty,metasenv,ugraph =
1704 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1705 let ty',sort,metasenv,ugraph =
1706 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1710 (* instead of raising Uncertain, let's hope that the meta will become
1713 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1715 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1716 let bo' = CicMetaSubst.apply_subst subst bo' in
1717 let ty' = CicMetaSubst.apply_subst subst ty' in
1718 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1719 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1720 | Cic.Variable _ -> assert false (* not implemented *)
1721 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1722 (*CSC: this code is greately simplified and many many checks are missing *)
1723 (*CSC: e.g. the constructors are not required to build their own types, *)
1724 (*CSC: the arities are not required to have as type a sort, etc. *)
1725 let uri = match uri with Some uri -> uri | None -> assert false in
1726 let typesno = List.length tys in
1727 (* first phase: we fix only the types *)
1728 let metasenv,ugraph,tys =
1730 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1731 let ty',_,metasenv,ugraph =
1732 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1734 metasenv,ugraph,(name,b,ty',cl)::res
1735 ) tys (metasenv,ugraph,[]) in
1737 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1738 (* second phase: we fix only the constructors *)
1739 let saved_menv = metasenv in
1740 let metasenv,ugraph,tys =
1742 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1743 let metasenv,ugraph,cl' =
1745 (fun (name,ty) (metasenv,ugraph,res) ->
1747 CicTypeChecker.debrujin_constructor
1748 ~cb:(relocalize localization_tbl) uri typesno ty in
1749 let ty',_,metasenv,ugraph =
1750 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1751 let ty' = undebrujin uri typesno tys ty' in
1752 metasenv@saved_menv,ugraph,(name,ty')::res
1753 ) cl (metasenv,ugraph,[])
1755 metasenv,ugraph,(name,b,ty,cl')::res
1756 ) tys (metasenv,ugraph,[]) in
1757 (* third phase: we check the positivity condition *)
1758 let metasenv,ugraph,tys =
1759 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1761 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1764 (* sara' piu' veloce che raffinare da zero? mah.... *)
1765 let pack_coercion metasenv ctx t =
1766 let module C = Cic in
1767 let rec merge_coercions ctx =
1768 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1770 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1771 | C.Meta (n,subst) ->
1774 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1777 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1778 | C.Prod (name,so,dest) ->
1779 let ctx' = (Some (name,C.Decl so))::ctx in
1780 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1781 | C.Lambda (name,so,dest) ->
1782 let ctx' = (Some (name,C.Decl so))::ctx in
1783 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1784 | C.LetIn (name,so,dest) ->
1785 let _,ty,metasenv,ugraph =
1786 pack_coercions := false;
1787 type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1788 pack_coercions := true;
1789 let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1790 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1792 let l = List.map (merge_coercions ctx) l in
1794 let b,_,_,_,_ = is_a_double_coercion t in
1795 (* prerr_endline "CANDIDATO!!!!"; *)
1797 let ugraph = CicUniv.oblivion_ugraph in
1798 let old_insert_coercions = !insert_coercions in
1799 insert_coercions := false;
1800 let newt, _, menv, _ =
1802 type_of_aux' metasenv ctx t ugraph
1803 with RefineFailure _ | Uncertain _ ->
1806 insert_coercions := old_insert_coercions;
1807 if metasenv <> [] || menv = [] then
1810 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1813 | C.Var (uri,exp_named_subst) ->
1814 let exp_named_subst = List.map aux exp_named_subst in
1815 C.Var (uri, exp_named_subst)
1816 | C.Const (uri,exp_named_subst) ->
1817 let exp_named_subst = List.map aux exp_named_subst in
1818 C.Const (uri, exp_named_subst)
1819 | C.MutInd (uri,tyno,exp_named_subst) ->
1820 let exp_named_subst = List.map aux exp_named_subst in
1821 C.MutInd (uri,tyno,exp_named_subst)
1822 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1823 let exp_named_subst = List.map aux exp_named_subst in
1824 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1825 | C.MutCase (uri,tyno,out,te,pl) ->
1826 let pl = List.map (merge_coercions ctx) pl in
1827 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1828 | C.Fix (fno, fl) ->
1831 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1836 (fun (name,idx,ty,bo) ->
1837 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1841 | C.CoFix (fno, fl) ->
1844 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1849 (fun (name,ty,bo) ->
1850 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1855 merge_coercions ctx t
1858 let pack_coercion_metasenv conjectures =
1859 let module C = Cic in
1861 (fun (i, ctx, ty) ->
1867 Some (name, C.Decl t) ->
1868 Some (name, C.Decl (pack_coercion conjectures ctx t))
1869 | Some (name, C.Def (t,None)) ->
1870 Some (name,C.Def (pack_coercion conjectures ctx t,None))
1871 | Some (name, C.Def (t,Some ty)) ->
1872 Some (name, C.Def (pack_coercion conjectures ctx t,
1873 Some (pack_coercion conjectures ctx ty)))
1879 ((i,ctx,pack_coercion conjectures ctx ty))
1883 let pack_coercion_obj obj =
1884 let module C = Cic in
1886 | C.Constant (id, body, ty, params, attrs) ->
1890 | Some body -> Some (pack_coercion [] [] body)
1892 let ty = pack_coercion [] [] ty in
1893 C.Constant (id, body, ty, params, attrs)
1894 | C.Variable (name, body, ty, params, attrs) ->
1898 | Some body -> Some (pack_coercion [] [] body)
1900 let ty = pack_coercion [] [] ty in
1901 C.Variable (name, body, ty, params, attrs)
1902 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1903 let conjectures = pack_coercion_metasenv conjectures in
1904 let body = pack_coercion conjectures [] body in
1905 let ty = pack_coercion conjectures [] ty in
1906 C.CurrentProof (name, conjectures, body, ty, params, attrs)
1907 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1910 (fun (name, ind, arity, cl) ->
1911 let arity = pack_coercion [] [] arity in
1913 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
1915 (name, ind, arity, cl))
1918 C.InductiveDefinition (indtys, params, leftno, attrs)
1923 let type_of_aux' metasenv context term =
1926 type_of_aux' metasenv context term in
1928 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1930 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1933 | RefineFailure msg as e ->
1934 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1936 | Uncertain msg as e ->
1937 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1941 let profiler2 = HExtlib.profile "CicRefine"
1943 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1944 profiler2.HExtlib.profile
1945 (type_of_aux' ?localization_tbl metasenv context term) ugraph
1947 let typecheck ~localization_tbl metasenv uri obj =
1948 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
1950 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
1951 (* vim:set foldmethod=marker: *)