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.NotHandled _ ->
458 enrich localization_tbl t
460 (lazy ("(4)The term " ^
461 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
462 " is not a type since it has type " ^
463 CicMetaSubst.ppterm_in_context ~metasenv
464 subst coercion_src context ^ " that is not a sort")))
465 | CoercGraph.NotMetaClosed ->
466 enrich localization_tbl t
468 (lazy ("(5)The term " ^
469 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
470 " is not a type since it has type " ^
471 CicMetaSubst.ppterm_in_context ~metasenv
472 subst coercion_src context ^ " that is not a sort")))
473 | CoercGraph.SomeCoercion candidates ->
476 (try_coercion t subst context ugraph coercion_tgt)
482 enrich localization_tbl t
484 (lazy ("(6)The term " ^
485 CicMetaSubst.ppterm_in_context ~metasenv
487 " is not a type since it has type " ^
488 CicMetaSubst.ppterm_in_context ~metasenv
489 subst coercion_src context ^
490 " that is not a sort"))))
492 let s',sort1,subst',metasenv',ugraph1 =
493 type_of_aux subst metasenv context s ugraph
495 let s',sort1,subst', metasenv',ugraph1 =
496 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
497 s' sort1 subst' context metasenv' ugraph1
499 let context_for_t = ((Some (name,(C.Decl s')))::context) in
500 let t',sort2,subst'',metasenv'',ugraph2 =
501 type_of_aux subst' metasenv'
502 context_for_t t ugraph1
504 let t',sort2,subst'',metasenv'',ugraph2 =
505 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
506 t' sort2 subst'' context_for_t metasenv'' ugraph2
508 let sop,subst''',metasenv''',ugraph3 =
509 sort_of_prod localization_tbl subst'' metasenv''
510 context (name,s') t' (sort1,sort2) ugraph2
512 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
513 | C.Lambda (n,s,t) ->
514 let s',sort1,subst',metasenv',ugraph1 =
515 type_of_aux subst metasenv context s ugraph in
516 let s',sort1,subst',metasenv',ugraph1 =
517 if not !insert_coercions then
518 s',sort1, subst', metasenv', ugraph1
520 match CicReduction.whd ~subst:subst' context sort1 with
521 | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
523 let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
525 CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
528 | CoercGraph.NoCoercion
529 | CoercGraph.NotHandled _ ->
530 enrich localization_tbl s'
532 (lazy ("(7)The term " ^
533 CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
534 " is not a type since it has type " ^
535 CicMetaSubst.ppterm_in_context ~metasenv
536 subst coercion_src context ^ " that is not a sort")))
537 | CoercGraph.NotMetaClosed ->
538 enrich localization_tbl s'
540 (lazy ("(8)The term " ^
541 CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
542 " is not a type since it has type " ^
543 CicMetaSubst.ppterm_in_context ~metasenv
544 subst coercion_src context ^ " that is not a sort")))
545 | CoercGraph.SomeCoercion candidates ->
548 (try_coercion s' subst' context ugraph1 coercion_tgt)
554 enrich localization_tbl s'
556 (lazy ("(9)The term " ^
557 CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
558 " is not a type since it has type " ^
559 CicMetaSubst.ppterm_in_context ~metasenv
560 subst coercion_src context ^
561 " that is not a sort")))
563 let context_for_t = ((Some (n,(C.Decl s')))::context) in
564 let t',type2,subst'',metasenv'',ugraph2 =
565 type_of_aux subst' metasenv' context_for_t t ugraph1
567 C.Lambda (n,s',t'),C.Prod (n,s',type2),
568 subst'',metasenv'',ugraph2
570 (* only to check if s is well-typed *)
571 let s',ty,subst',metasenv',ugraph1 =
572 type_of_aux subst metasenv context s ugraph
574 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
576 let t',inferredty,subst'',metasenv'',ugraph2 =
577 type_of_aux subst' metasenv'
578 context_for_t t ugraph1
580 (* One-step LetIn reduction.
581 * Even faster than the previous solution.
582 * Moreover the inferred type is closer to the expected one.
585 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
586 subst'',metasenv'',ugraph2
587 | C.Appl (he::((_::_) as tl)) ->
588 let he',hetype,subst',metasenv',ugraph1 =
589 type_of_aux subst metasenv context he ugraph
591 let tlbody_and_type,subst'',metasenv'',ugraph2 =
592 typeof_list subst' metasenv' context ugraph1 tl
594 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
595 eat_prods true subst'' metasenv'' context
596 he' hetype tlbody_and_type ugraph2
598 let newappl = (C.Appl (coerced_he::coerced_args)) in
599 avoid_double_coercion
600 context subst''' metasenv''' ugraph3 newappl applty
601 | C.Appl _ -> assert false
602 | C.Const (uri,exp_named_subst) ->
603 let exp_named_subst',subst',metasenv',ugraph1 =
604 check_exp_named_subst subst metasenv context
605 exp_named_subst ugraph in
606 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
608 CicSubstitution.subst_vars exp_named_subst' ty_uri
610 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
611 | C.MutInd (uri,i,exp_named_subst) ->
612 let exp_named_subst',subst',metasenv',ugraph1 =
613 check_exp_named_subst subst metasenv context
614 exp_named_subst ugraph
616 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
618 CicSubstitution.subst_vars exp_named_subst' ty_uri in
619 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
620 | C.MutConstruct (uri,i,j,exp_named_subst) ->
621 let exp_named_subst',subst',metasenv',ugraph1 =
622 check_exp_named_subst subst metasenv context
623 exp_named_subst ugraph
626 type_of_mutual_inductive_constr uri i j ugraph1
629 CicSubstitution.subst_vars exp_named_subst' ty_uri
631 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
633 | C.MutCase (uri, i, outtype, term, pl) ->
634 (* first, get the inductive type (and noparams)
635 * in the environment *)
636 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
637 let _ = CicTypeChecker.typecheck uri in
638 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
640 C.InductiveDefinition (l,expl_params,parsno,_) ->
641 List.nth l i , expl_params, parsno, u
643 enrich localization_tbl t
645 (lazy ("Unkown mutual inductive definition " ^
646 U.string_of_uri uri)))
648 let rec count_prod t =
649 match CicReduction.whd ~subst context t with
650 C.Prod (_, _, t) -> 1 + (count_prod t)
653 let no_args = count_prod arity in
654 (* now, create a "generic" MutInd *)
655 let metasenv,left_args =
656 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
658 let metasenv,right_args =
659 let no_right_params = no_args - no_left_params in
660 if no_right_params < 0 then assert false
661 else CicMkImplicit.n_fresh_metas
662 metasenv subst context no_right_params
664 let metasenv,exp_named_subst =
665 CicMkImplicit.fresh_subst metasenv subst context expl_params in
668 C.MutInd (uri,i,exp_named_subst)
671 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
673 (* check consistency with the actual type of term *)
674 let term',actual_type,subst,metasenv,ugraph1 =
675 type_of_aux subst metasenv context term ugraph in
676 let expected_type',_, subst, metasenv,ugraph2 =
677 type_of_aux subst metasenv context expected_type ugraph1
679 let actual_type = CicReduction.whd ~subst context actual_type in
680 let subst,metasenv,ugraph3 =
682 fo_unif_subst subst context metasenv
683 expected_type' actual_type ugraph2
686 prerr_endline (CicMetaSubst.ppmetasenv subst metasenv);
687 prerr_endline (CicMetaSubst.ppsubst subst ~metasenv);
688 enrich localization_tbl term' exn
690 lazy ("(10)The term " ^
691 CicMetaSubst.ppterm_in_context ~metasenv subst term'
692 context ^ " has type " ^
693 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
694 context ^ " but is here used with type " ^
695 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
697 let rec instantiate_prod t =
701 match CicReduction.whd ~subst context t with
703 instantiate_prod (CicSubstitution.subst he t') tl
706 let arity_instantiated_with_left_args =
707 instantiate_prod arity left_args in
708 (* TODO: check if the sort elimination
709 * is allowed: [(I q1 ... qr)|B] *)
710 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
712 (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
714 if left_args = [] then
715 (C.MutConstruct (uri,i,j,exp_named_subst))
718 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
720 let p',actual_type,subst,metasenv,ugraph1 =
721 type_of_aux subst metasenv context p ugraph
723 let constructor',expected_type, subst, metasenv,ugraph2 =
724 type_of_aux subst metasenv context constructor ugraph1
726 let outtypeinstance,subst,metasenv,ugraph3 =
728 check_branch 0 context metasenv subst
729 no_left_params actual_type constructor' expected_type
733 enrich localization_tbl constructor'
735 lazy ("(11)The term " ^
736 CicMetaSubst.ppterm_in_context metasenv subst p'
737 context ^ " has type " ^
738 CicMetaSubst.ppterm_in_context metasenv subst actual_type
739 context ^ " but is here used with type " ^
740 CicMetaSubst.ppterm_in_context metasenv subst expected_type
744 outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
745 pl ([],List.length pl,[],subst,metasenv,ugraph3)
748 (* we are left to check that the outype matches his instances.
749 The easy case is when the outype is specified, that amount
750 to a trivial check. Otherwise, we should guess a type from
754 let outtype,outtypety, subst, metasenv,ugraph4 =
755 type_of_aux subst metasenv context outtype ugraph4 in
758 (let candidate,ugraph5,metasenv,subst =
759 let exp_name_subst, metasenv =
761 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
763 let uris = CicUtil.params_of_obj o in
765 fun uri (acc,metasenv) ->
766 let metasenv',new_meta =
767 CicMkImplicit.mk_implicit metasenv subst context
770 CicMkImplicit.identity_relocation_list_for_metavariable
773 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
777 match left_args,right_args with
778 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
780 let rec mk_right_args =
783 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
785 let right_args_no = List.length right_args in
786 let lifted_left_args =
787 List.map (CicSubstitution.lift right_args_no) left_args
789 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
790 (lifted_left_args @ mk_right_args right_args_no))
793 FreshNamesGenerator.mk_fresh_name ~subst metasenv
794 context Cic.Anonymous ~typ:ty
796 match outtypeinstances with
798 let extended_context =
799 let rec add_right_args =
801 Cic.Prod (name,ty,t) ->
802 Some (name,Cic.Decl ty)::(add_right_args t)
805 (Some (fresh_name,Cic.Decl ty))::
807 (add_right_args arity_instantiated_with_left_args))@
810 let metasenv,new_meta =
811 CicMkImplicit.mk_implicit metasenv subst extended_context
814 CicMkImplicit.identity_relocation_list_for_metavariable
817 let rec add_lambdas b =
819 Cic.Prod (name,ty,t) ->
820 Cic.Lambda (name,ty,(add_lambdas b t))
821 | _ -> Cic.Lambda (fresh_name, ty, b)
824 add_lambdas (Cic.Meta (new_meta,irl))
825 arity_instantiated_with_left_args
827 (Some candidate),ugraph4,metasenv,subst
828 | (constructor_args_no,_,instance,_)::tl ->
830 let instance',subst,metasenv =
831 CicMetaSubst.delift_rels subst metasenv
832 constructor_args_no instance
834 let candidate,ugraph,metasenv,subst =
836 fun (candidate_oty,ugraph,metasenv,subst)
837 (constructor_args_no,_,instance,_) ->
838 match candidate_oty with
839 | None -> None,ugraph,metasenv,subst
842 let instance',subst,metasenv =
843 CicMetaSubst.delift_rels subst metasenv
844 constructor_args_no instance
846 let subst,metasenv,ugraph =
847 fo_unif_subst subst context metasenv
850 candidate_oty,ugraph,metasenv,subst
852 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
853 | CicUnification.UnificationFailure _
854 | CicUnification.Uncertain _ ->
855 None,ugraph,metasenv,subst
856 ) (Some instance',ugraph4,metasenv,subst) tl
859 | None -> None, ugraph,metasenv,subst
861 let rec add_lambdas n b =
863 Cic.Prod (name,ty,t) ->
864 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
866 Cic.Lambda (fresh_name, ty,
867 CicSubstitution.lift (n + 1) t)
870 (add_lambdas 0 t arity_instantiated_with_left_args),
871 ugraph,metasenv,subst
872 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
873 None,ugraph4,metasenv,subst
876 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
878 let subst,metasenv,ugraph =
880 fo_unif_subst subst context metasenv
881 candidate outtype ugraph5
883 exn -> assert false(* unification against a metavariable *)
885 C.MutCase (uri, i, outtype, term', pl'),
886 CicReduction.head_beta_reduce
887 (CicMetaSubst.apply_subst subst
888 (Cic.Appl (outtype::right_args@[term']))),
889 subst,metasenv,ugraph)
890 | _ -> (* easy case *)
891 let tlbody_and_type,subst,metasenv,ugraph4 =
892 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
894 let _,_,_,subst,metasenv,ugraph4 =
895 eat_prods false subst metasenv context
896 outtype outtypety tlbody_and_type ugraph4
898 let _,_, subst, metasenv,ugraph5 =
899 type_of_aux subst metasenv context
900 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
902 let (subst,metasenv,ugraph6) =
904 (fun (subst,metasenv,ugraph)
905 p (constructor_args_no,context,instance,args)
910 CicSubstitution.lift constructor_args_no outtype
912 C.Appl (outtype'::args)
914 CicReduction.whd ~subst context appl
917 fo_unif_subst subst context metasenv instance instance'
921 enrich localization_tbl p exn
923 lazy ("(12)The term " ^
924 CicMetaSubst.ppterm_in_context ~metasenv subst p
925 context ^ " has type " ^
926 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
927 context ^ " but is here used with type " ^
928 CicMetaSubst.ppterm_in_context ~metasenv subst instance
930 (subst,metasenv,ugraph5) pl' outtypeinstances
932 C.MutCase (uri, i, outtype, term', pl'),
933 CicReduction.head_beta_reduce
934 (CicMetaSubst.apply_subst subst
935 (C.Appl(outtype::right_args@[term]))),
936 subst,metasenv,ugraph6)
938 let fl_ty',subst,metasenv,types,ugraph1,len =
940 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
941 let ty',_,subst',metasenv',ugraph1 =
942 type_of_aux subst metasenv context ty ugraph
944 fl @ [ty'],subst',metasenv',
945 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
946 :: types, ugraph, len+1
947 ) ([],subst,metasenv,[],ugraph,0) fl
949 let context' = types@context in
950 let fl_bo',subst,metasenv,ugraph2 =
952 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
953 let bo',ty_of_bo,subst,metasenv,ugraph1 =
954 type_of_aux subst metasenv context' bo ugraph in
955 let expected_ty = CicSubstitution.lift len ty in
956 let subst',metasenv',ugraph' =
958 fo_unif_subst subst context' metasenv
959 ty_of_bo expected_ty ugraph1
962 enrich localization_tbl bo exn
964 lazy ("(13)The term " ^
965 CicMetaSubst.ppterm_in_context ~metasenv subst bo
966 context' ^ " has type " ^
967 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
968 context' ^ " but is here used with type " ^
969 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
972 fl @ [bo'] , subst',metasenv',ugraph'
973 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
975 let ty = List.nth fl_ty' i in
976 (* now we have the new ty in fl_ty', the new bo in fl_bo',
977 * and we want the new fl with bo' and ty' injected in the right
980 let rec map3 f l1 l2 l3 =
983 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
986 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
989 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
991 let fl_ty',subst,metasenv,types,ugraph1,len =
993 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
994 let ty',_,subst',metasenv',ugraph1 =
995 type_of_aux subst metasenv context ty ugraph
997 fl @ [ty'],subst',metasenv',
998 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
999 types, ugraph1, len+1
1000 ) ([],subst,metasenv,[],ugraph,0) fl
1002 let context' = types@context in
1003 let fl_bo',subst,metasenv,ugraph2 =
1005 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
1006 let bo',ty_of_bo,subst,metasenv,ugraph1 =
1007 type_of_aux subst metasenv context' bo ugraph in
1008 let expected_ty = CicSubstitution.lift len ty in
1009 let subst',metasenv',ugraph' =
1011 fo_unif_subst subst context' metasenv
1012 ty_of_bo expected_ty ugraph1
1015 enrich localization_tbl bo exn
1017 lazy ("(14)The term " ^
1018 CicMetaSubst.ppterm_in_context ~metasenv subst bo
1019 context' ^ " has type " ^
1020 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
1021 context' ^ " but is here used with type " ^
1022 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
1025 fl @ [bo'],subst',metasenv',ugraph'
1026 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
1028 let ty = List.nth fl_ty' i in
1029 (* now we have the new ty in fl_ty', the new bo in fl_bo',
1030 * and we want the new fl with bo' and ty' injected in the right
1033 let rec map3 f l1 l2 l3 =
1036 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
1039 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
1042 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
1044 relocalize localization_tbl t t';
1047 (* check_metasenv_consistency checks that the "canonical" context of a
1048 metavariable is consitent - up to relocation via the relocation list l -
1049 with the actual context *)
1050 and check_metasenv_consistency
1051 metano subst metasenv context canonical_context l ugraph
1053 let module C = Cic in
1054 let module R = CicReduction in
1055 let module S = CicSubstitution in
1056 let lifted_canonical_context =
1060 | (Some (n,C.Decl t))::tl ->
1061 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
1062 | (Some (n,C.Def (t,None)))::tl ->
1063 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1064 | None::tl -> None::(aux (i+1) tl)
1065 | (Some (n,C.Def (t,Some ty)))::tl ->
1067 C.Def ((S.subst_meta l (S.lift i t)),
1068 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
1070 aux 1 canonical_context
1074 (fun (l,subst,metasenv,ugraph) t ct ->
1077 l @ [None],subst,metasenv,ugraph
1078 | Some t,Some (_,C.Def (ct,_)) ->
1079 let subst',metasenv',ugraph' =
1081 prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
1082 fo_unif_subst subst context metasenv t ct ugraph
1083 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))))))
1085 l @ [Some t],subst',metasenv',ugraph'
1086 | Some t,Some (_,C.Decl ct) ->
1087 let t',inferredty,subst',metasenv',ugraph1 =
1088 type_of_aux subst metasenv context t ugraph
1090 let subst'',metasenv'',ugraph2 =
1093 subst' context metasenv' inferredty ct ugraph1
1094 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))))))
1096 l @ [Some t'], subst'',metasenv'',ugraph2
1098 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
1100 Invalid_argument _ ->
1104 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1105 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1106 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1108 and check_exp_named_subst metasubst metasenv context tl ugraph =
1109 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1111 [] -> [],metasubst,metasenv,ugraph
1113 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1115 CicSubstitution.subst_vars substs ty_uri in
1116 (* CSC: why was this code here? it is wrong
1117 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1118 Cic.Variable (_,Some bo,_,_) ->
1120 (RefineFailure (lazy
1121 "A variable with a body can not be explicit substituted"))
1122 | Cic.Variable (_,None,_,_) -> ()
1125 (RefineFailure (lazy
1126 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1129 let t',typeoft,metasubst',metasenv',ugraph2 =
1130 type_of_aux metasubst metasenv context t ugraph1 in
1131 let subst = uri,t' in
1132 let metasubst'',metasenv'',ugraph3 =
1135 metasubst' context metasenv' typeoft typeofvar ugraph2
1137 raise (RefineFailure (lazy
1138 ("Wrong Explicit Named Substitution: " ^
1139 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1140 " not unifiable with " ^
1141 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1143 (* FIXME: no mere tail recursive! *)
1144 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1145 check_exp_named_subst_aux
1146 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1148 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1150 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1153 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1156 let module C = Cic in
1157 let context_for_t2 = (Some (name,C.Decl s))::context in
1158 let t1'' = CicReduction.whd ~subst context t1 in
1159 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1160 match (t1'', t2'') with
1161 (C.Sort s1, C.Sort s2)
1162 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1163 (* different than Coq manual!!! *)
1164 C.Sort s2,subst,metasenv,ugraph
1165 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1166 let t' = CicUniv.fresh() in
1168 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1169 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1170 C.Sort (C.Type t'),subst,metasenv,ugraph2
1172 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1173 | (C.Sort _,C.Sort (C.Type t1)) ->
1174 C.Sort (C.Type t1),subst,metasenv,ugraph
1175 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1176 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1177 (* TODO how can we force the meta to become a sort? If we don't we
1178 * break the invariant that refine produce only well typed terms *)
1179 (* TODO if we check the non meta term and if it is a sort then we
1180 * are likely to know the exact value of the result e.g. if the rhs
1181 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1182 let (metasenv,idx) =
1183 CicMkImplicit.mk_implicit_sort metasenv subst in
1184 let (subst, metasenv,ugraph1) =
1186 fo_unif_subst subst context_for_t2 metasenv
1187 (C.Meta (idx,[])) t2'' ugraph
1188 with _ -> assert false (* unification against a metavariable *)
1190 t2'',subst,metasenv,ugraph1
1193 enrich localization_tbl s
1197 "%s is supposed to be a type, but its type is %s"
1198 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1199 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1201 enrich localization_tbl t
1205 "%s is supposed to be a type, but its type is %s"
1206 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1207 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1209 and avoid_double_coercion context subst metasenv ugraph t ty =
1210 if not !pack_coercions then
1211 t,ty,subst,metasenv,ugraph
1213 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1215 let source_carr = CoercGraph.source_of c2 in
1216 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1217 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1219 | CoercGraph.SomeCoercion candidates ->
1221 HExtlib.list_findopt
1222 (function (metasenv,last,c) ->
1224 | c when not (CoercGraph.is_composite c) ->
1225 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1228 let subst,metasenv,ugraph =
1229 fo_unif_subst subst context metasenv last head ugraph in
1230 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1235 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1236 let newt,_,subst,metasenv,ugraph =
1237 type_of_aux subst metasenv context c ugraph in
1238 debug_print (lazy "tipa...");
1239 let subst, metasenv, ugraph =
1240 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1241 fo_unif_subst subst context metasenv newt t ugraph
1243 debug_print (lazy "unifica...");
1244 Some (newt, ty, subst, metasenv, ugraph)
1246 | RefineFailure s | Uncertain s when not !pack_coercions->
1247 debug_print s; debug_print (lazy "stop\n");None
1248 | RefineFailure s | Uncertain s ->
1249 debug_print s;debug_print (lazy "goon\n");
1251 let old_pack_coercions = !pack_coercions in
1252 pack_coercions := false; (* to avoid diverging *)
1253 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1254 type_of_aux subst metasenv context c1_c2_implicit ugraph
1256 pack_coercions := old_pack_coercions;
1258 is_a_double_coercion refined_c1_c2_implicit
1264 match refined_c1_c2_implicit with
1265 | Cic.Appl l -> HExtlib.list_last l
1268 let subst, metasenv, ugraph =
1269 try fo_unif_subst subst context metasenv
1271 with RefineFailure s| Uncertain s->
1272 debug_print s;assert false
1274 let subst, metasenv, ugraph =
1275 fo_unif_subst subst context metasenv
1276 refined_c1_c2_implicit t ugraph
1278 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1280 | RefineFailure s | Uncertain s ->
1281 pack_coercions := true;debug_print s;None
1282 | exn -> pack_coercions := true; raise exn))
1285 (match selected with
1289 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1290 t, ty, subst, metasenv, ugraph)
1291 | _ -> t, ty, subst, metasenv, ugraph)
1293 t, ty, subst, metasenv, ugraph
1295 and typeof_list subst metasenv context ugraph l =
1296 let tlbody_and_type,subst,metasenv,ugraph =
1298 (fun x (res,subst,metasenv,ugraph) ->
1299 let x',ty,subst',metasenv',ugraph1 =
1300 type_of_aux subst metasenv context x ugraph
1302 (x', ty)::res,subst',metasenv',ugraph1
1303 ) l ([],subst,metasenv,ugraph)
1305 tlbody_and_type,subst,metasenv,ugraph
1308 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1310 (* aux function to add coercions to funclass *)
1311 let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph =
1313 let pristinemenv = metasenv in
1314 let metasenv,hetype' =
1315 mk_prod_of_metas metasenv context subst args_bo_and_ty
1318 let subst,metasenv,ugraph =
1319 fo_unif_subst_eat_prods
1320 subst context metasenv hetype hetype' ugraph
1322 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1323 with RefineFailure s | Uncertain s as exn
1324 when allow_coercions && !insert_coercions ->
1325 (* {{{ we search a coercion of the head (saturated) to funclass *)
1326 let metasenv = pristinemenv in
1328 ("Fixing arity of: "^CicMetaSubst.ppterm ~metasenv subst hetype ^
1329 " since unif failed with: " ^ CicMetaSubst.ppterm ~metasenv subst hetype'
1330 (* ^ " cause: " ^ Lazy.force s *)));
1331 let how_many_args_are_needed =
1332 let rec aux n = function
1333 | Cic.Prod(_,_,t) -> aux (n+1) t
1336 aux 0 (CicMetaSubst.apply_subst subst hetype)
1338 let args, remainder =
1339 HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
1341 let args = List.map fst args in
1345 | Cic.Appl l -> Cic.Appl (l@args)
1346 | _ -> Cic.Appl (he::args)
1350 let x,xty,subst,metasenv,ugraph =
1351 (*CSC: here unsharing is necessary to avoid an unwanted
1352 relocalization. However, this also shows a great source of
1353 inefficiency: "x" is refined twice (once now and once in the
1354 subsequent eat_prods_and_args). Morevoer, how is divergence avoided?
1356 type_of_aux subst metasenv context (Unshare.unshare x) ugraph
1359 CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty)
1361 let carr_tgt = CoercDb.Fun 0 in
1362 match CoercGraph.look_for_coercion' metasenv subst context carr_src carr_tgt with
1363 | CoercGraph.NoCoercion
1364 | CoercGraph.NotMetaClosed
1365 | CoercGraph.NotHandled _ -> raise exn
1366 | CoercGraph.SomeCoercion candidates ->
1368 HExtlib.list_findopt
1369 (fun (metasenv,last,coerc) ->
1370 let subst,metasenv,ugraph =
1371 fo_unif_subst subst context metasenv last x ugraph in
1372 debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc));
1374 (* we want this to be available in the error handler fo the
1375 * following (so it has its own try. *)
1376 let t,tty,subst,metasenv,ugraph =
1377 type_of_aux subst metasenv context coerc ugraph
1380 let metasenv, hetype' =
1381 mk_prod_of_metas metasenv context subst remainder
1384 (" unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^
1385 CicMetaSubst.ppterm ~metasenv subst hetype'));
1386 let subst,metasenv,ugraph =
1387 fo_unif_subst_eat_prods
1388 subst context metasenv tty hetype' ugraph
1390 debug_print (lazy " success!");
1391 Some (subst,metasenv,ugraph,tty,t,remainder)
1393 | Uncertain _ | RefineFailure _
1394 | CicUnification.UnificationFailure _
1395 | CicUnification.Uncertain _ ->
1397 let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
1399 metasenv context subst t tty remainder ugraph
1401 Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
1402 with Uncertain _ | RefineFailure _ -> None
1406 | HExtlib.Localized (_,Uncertain _)
1407 | HExtlib.Localized (_,RefineFailure _) -> None
1408 | exn -> assert false) (* ritornare None, e' un localized *)
1411 | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
1412 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1414 more_args_than_expected localization_tbl metasenv
1415 subst he context hetype args_bo_and_ty exn
1416 (* }}} end coercion to funclass stuff *)
1417 (* }}} end fix_arity *)
1419 (* aux function to process the type of the head and the args in parallel *)
1420 let rec eat_prods_and_args
1421 pristinemenv metasenv subst context pristinehe he hetype ugraph newargs
1425 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1426 | (hete, hety)::tl ->
1427 match (CicReduction.whd ~subst context hetype) with
1428 | Cic.Prod (n,s,t) ->
1429 let arg,subst,metasenv,ugraph1 =
1431 let subst,metasenv,ugraph1 =
1432 fo_unif_subst_eat_prods2
1433 subst context metasenv hety s ugraph
1435 (hete,hety),subst,metasenv,ugraph1
1436 (* {{{ we search a coercion from hety to s if fails *)
1437 with RefineFailure _ | Uncertain _ as exn
1438 when allow_coercions && !insert_coercions ->
1439 let coer, tgt_carr =
1440 let carr t subst context =
1441 CicReduction.whd ~delta:false
1442 context (CicMetaSubst.apply_subst subst t )
1444 let c_hety = carr hety subst context in
1445 let c_s = carr s subst context in
1446 CoercGraph.look_for_coercion metasenv subst context c_hety c_s, c_s
1449 | CoercGraph.NoCoercion
1450 | CoercGraph.NotHandled _ ->
1451 enrich localization_tbl hete exn
1453 (lazy ("(15)The term " ^
1454 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1455 context ^ " has type " ^
1456 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1457 context ^ " but is here used with type " ^
1458 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1459 (* "\nReason: " ^ Lazy.force e*))))
1460 | CoercGraph.NotMetaClosed ->
1461 enrich localization_tbl hete exn
1463 (lazy ("(16)The term " ^
1464 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1465 context ^ " has type " ^
1466 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1467 context ^ " but is here used with type " ^
1468 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1469 (* "\nReason: " ^ Lazy.force e*))))
1470 | CoercGraph.SomeCoercion candidates ->
1472 HExtlib.list_findopt
1473 (fun (metasenv,last,c) ->
1475 let subst,metasenv,ugraph =
1476 fo_unif_subst subst context metasenv last hete
1478 let newt,newhety,subst,metasenv,ugraph =
1479 type_of_aux subst metasenv context
1482 let newt, newty, subst, metasenv, ugraph =
1483 avoid_double_coercion context subst metasenv
1484 ugraph newt tgt_carr
1486 let subst,metasenv,ugraph1 =
1487 fo_unif_subst subst context metasenv
1490 Some ((newt,newty), subst, metasenv, ugraph)
1491 with Uncertain _ | RefineFailure _ -> None)
1494 (match selected with
1497 enrich localization_tbl hete
1499 (lazy ("(1)The term " ^
1500 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1501 context ^ " has type " ^
1502 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1503 context ^ " but is here used with type " ^
1504 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1505 (* "\nReason: " ^ Lazy.force e*)))) exn))
1507 enrich localization_tbl hete
1509 (lazy ("(2)The term " ^
1510 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1511 context ^ " has type " ^
1512 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1513 context ^ " but is here used with type " ^
1514 CicMetaSubst.ppterm_in_context ~metasenv subst s context
1515 (* "\nReason: " ^ Printexc.to_string exn*)))) exn
1516 (* }}} end coercion stuff *)
1518 eat_prods_and_args pristinemenv metasenv subst context pristinehe he
1519 (CicSubstitution.subst (fst arg) t)
1520 ugraph1 (newargs@[arg]) tl
1523 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1525 pristinemenv context subst he hetype
1526 (newargs@[hete,hety]@tl) ugraph
1528 eat_prods_and_args metasenv
1529 metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
1530 with RefineFailure _ | Uncertain _ as exn ->
1531 (* unable to fix arity *)
1532 more_args_than_expected localization_tbl metasenv
1533 subst he context hetype args_bo_and_ty exn
1536 (* first we check if we are in the simple case of a meta closed term *)
1537 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1538 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1539 (* this optimization is to postpone fix_arity (the most common case)*)
1540 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1542 (* this (says CSC) is also useful to infer dependent types *)
1544 fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
1545 with RefineFailure _ | Uncertain _ as exn ->
1546 (* unable to fix arity *)
1547 more_args_than_expected localization_tbl metasenv
1548 subst he context hetype args_bo_and_ty exn
1550 let coerced_args,subst,metasenv,he,t,ugraph =
1552 metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
1554 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1557 (* eat prods ends here! *)
1559 let t',ty,subst',metasenv',ugraph1 =
1560 type_of_aux [] metasenv context t ugraph
1562 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1563 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1564 (* Andrea: ho rimesso qui l'applicazione della subst al
1565 metasenv dopo che ho droppato l'invariante che il metsaenv
1566 e' sempre istanziato *)
1567 let substituted_metasenv =
1568 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1570 (* substituted_t,substituted_ty,substituted_metasenv *)
1571 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1573 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1575 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1576 let cleaned_metasenv =
1578 (function (n,context,ty) ->
1579 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1584 | Some (n, Cic.Decl t) ->
1586 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1587 | Some (n, Cic.Def (bo,ty)) ->
1588 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1593 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1595 Some (n, Cic.Def (bo',ty'))
1599 ) substituted_metasenv
1601 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1604 let undebrujin uri typesno tys t =
1607 (fun (name,_,_,_) (i,t) ->
1608 (* here the explicit_named_substituion is assumed to be *)
1610 let t' = Cic.MutInd (uri,i,[]) in
1611 let t = CicSubstitution.subst t' t in
1613 ) tys (typesno - 1,t))
1615 let map_first_n n start f g l =
1616 let rec aux acc k l =
1619 | [] -> raise (Invalid_argument "map_first_n")
1620 | hd :: tl -> f hd k (aux acc (k+1) tl)
1626 (*CSC: this is a very rough approximation; to be finished *)
1627 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1628 let subst,metasenv,ugraph,tys =
1630 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1631 let subst,metasenv,ugraph,cl =
1633 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1634 let rec aux ctx k subst = function
1635 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1636 let subst,metasenv,ugraph,tl =
1638 (subst,metasenv,ugraph,[])
1639 (fun t n (subst,metasenv,ugraph,acc) ->
1640 let subst,metasenv,ugraph =
1642 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1644 subst,metasenv,ugraph,(t::acc))
1645 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1648 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1649 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1650 subst,metasenv,ugraph,t
1651 | Cic.Prod (name,s,t) ->
1652 let ctx = (Some (name,Cic.Decl s))::ctx in
1653 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1654 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1658 (lazy "not well formed constructor type"))
1660 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1661 subst,metasenv,ugraph,(name,ty) :: acc)
1662 cl (subst,metasenv,ugraph,[])
1664 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1665 tys ([],metasenv,ugraph,[])
1667 let substituted_tys =
1669 (fun (name,ind,arity,cl) ->
1671 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1673 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1676 metasenv,ugraph,substituted_tys
1678 let typecheck metasenv uri obj ~localization_tbl =
1679 let ugraph = CicUniv.empty_ugraph in
1681 Cic.Constant (name,Some bo,ty,args,attrs) ->
1682 let bo',boty,metasenv,ugraph =
1683 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1684 let ty',_,metasenv,ugraph =
1685 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1686 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1687 let bo' = CicMetaSubst.apply_subst subst bo' in
1688 let ty' = CicMetaSubst.apply_subst subst ty' in
1689 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1690 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1691 | Cic.Constant (name,None,ty,args,attrs) ->
1692 let ty',_,metasenv,ugraph =
1693 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1695 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1696 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1697 assert (metasenv' = metasenv);
1698 (* Here we do not check the metasenv for correctness *)
1699 let bo',boty,metasenv,ugraph =
1700 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1701 let ty',sort,metasenv,ugraph =
1702 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1706 (* instead of raising Uncertain, let's hope that the meta will become
1709 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1711 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1712 let bo' = CicMetaSubst.apply_subst subst bo' in
1713 let ty' = CicMetaSubst.apply_subst subst ty' in
1714 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1715 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1716 | Cic.Variable _ -> assert false (* not implemented *)
1717 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1718 (*CSC: this code is greately simplified and many many checks are missing *)
1719 (*CSC: e.g. the constructors are not required to build their own types, *)
1720 (*CSC: the arities are not required to have as type a sort, etc. *)
1721 let uri = match uri with Some uri -> uri | None -> assert false in
1722 let typesno = List.length tys in
1723 (* first phase: we fix only the types *)
1724 let metasenv,ugraph,tys =
1726 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1727 let ty',_,metasenv,ugraph =
1728 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1730 metasenv,ugraph,(name,b,ty',cl)::res
1731 ) tys (metasenv,ugraph,[]) in
1733 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1734 (* second phase: we fix only the constructors *)
1735 let saved_menv = metasenv in
1736 let metasenv,ugraph,tys =
1738 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1739 let metasenv,ugraph,cl' =
1741 (fun (name,ty) (metasenv,ugraph,res) ->
1743 CicTypeChecker.debrujin_constructor
1744 ~cb:(relocalize localization_tbl) uri typesno ty in
1745 let ty',_,metasenv,ugraph =
1746 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1747 let ty' = undebrujin uri typesno tys ty' in
1748 metasenv@saved_menv,ugraph,(name,ty')::res
1749 ) cl (metasenv,ugraph,[])
1751 metasenv,ugraph,(name,b,ty,cl')::res
1752 ) tys (metasenv,ugraph,[]) in
1753 (* third phase: we check the positivity condition *)
1754 let metasenv,ugraph,tys =
1755 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1757 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1760 (* sara' piu' veloce che raffinare da zero? mah.... *)
1761 let pack_coercion metasenv ctx t =
1762 let module C = Cic in
1763 let rec merge_coercions ctx =
1764 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1766 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1767 | C.Meta (n,subst) ->
1770 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1773 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1774 | C.Prod (name,so,dest) ->
1775 let ctx' = (Some (name,C.Decl so))::ctx in
1776 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1777 | C.Lambda (name,so,dest) ->
1778 let ctx' = (Some (name,C.Decl so))::ctx in
1779 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1780 | C.LetIn (name,so,dest) ->
1781 let _,ty,metasenv,ugraph =
1782 pack_coercions := false;
1783 type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1784 pack_coercions := true;
1785 let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1786 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1788 let l = List.map (merge_coercions ctx) l in
1790 let b,_,_,_,_ = is_a_double_coercion t in
1791 (* prerr_endline "CANDIDATO!!!!"; *)
1793 let ugraph = CicUniv.oblivion_ugraph in
1794 let old_insert_coercions = !insert_coercions in
1795 insert_coercions := false;
1796 let newt, _, menv, _ =
1798 type_of_aux' metasenv ctx t ugraph
1799 with RefineFailure _ | Uncertain _ ->
1802 insert_coercions := old_insert_coercions;
1803 if metasenv <> [] || menv = [] then
1806 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1809 | C.Var (uri,exp_named_subst) ->
1810 let exp_named_subst = List.map aux exp_named_subst in
1811 C.Var (uri, exp_named_subst)
1812 | C.Const (uri,exp_named_subst) ->
1813 let exp_named_subst = List.map aux exp_named_subst in
1814 C.Const (uri, exp_named_subst)
1815 | C.MutInd (uri,tyno,exp_named_subst) ->
1816 let exp_named_subst = List.map aux exp_named_subst in
1817 C.MutInd (uri,tyno,exp_named_subst)
1818 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1819 let exp_named_subst = List.map aux exp_named_subst in
1820 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1821 | C.MutCase (uri,tyno,out,te,pl) ->
1822 let pl = List.map (merge_coercions ctx) pl in
1823 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1824 | C.Fix (fno, fl) ->
1827 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1832 (fun (name,idx,ty,bo) ->
1833 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1837 | C.CoFix (fno, fl) ->
1840 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1845 (fun (name,ty,bo) ->
1846 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1851 merge_coercions ctx t
1854 let pack_coercion_metasenv conjectures =
1855 let module C = Cic in
1857 (fun (i, ctx, ty) ->
1863 Some (name, C.Decl t) ->
1864 Some (name, C.Decl (pack_coercion conjectures ctx t))
1865 | Some (name, C.Def (t,None)) ->
1866 Some (name,C.Def (pack_coercion conjectures ctx t,None))
1867 | Some (name, C.Def (t,Some ty)) ->
1868 Some (name, C.Def (pack_coercion conjectures ctx t,
1869 Some (pack_coercion conjectures ctx ty)))
1875 ((i,ctx,pack_coercion conjectures ctx ty))
1879 let pack_coercion_obj obj =
1880 let module C = Cic in
1882 | C.Constant (id, body, ty, params, attrs) ->
1886 | Some body -> Some (pack_coercion [] [] body)
1888 let ty = pack_coercion [] [] ty in
1889 C.Constant (id, body, ty, params, attrs)
1890 | C.Variable (name, body, ty, params, attrs) ->
1894 | Some body -> Some (pack_coercion [] [] body)
1896 let ty = pack_coercion [] [] ty in
1897 C.Variable (name, body, ty, params, attrs)
1898 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1899 let conjectures = pack_coercion_metasenv conjectures in
1900 let body = pack_coercion conjectures [] body in
1901 let ty = pack_coercion conjectures [] ty in
1902 C.CurrentProof (name, conjectures, body, ty, params, attrs)
1903 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1906 (fun (name, ind, arity, cl) ->
1907 let arity = pack_coercion [] [] arity in
1909 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
1911 (name, ind, arity, cl))
1914 C.InductiveDefinition (indtys, params, leftno, attrs)
1919 let type_of_aux' metasenv context term =
1922 type_of_aux' metasenv context term in
1924 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1926 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1929 | RefineFailure msg as e ->
1930 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1932 | Uncertain msg as e ->
1933 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1937 let profiler2 = HExtlib.profile "CicRefine"
1939 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1940 profiler2.HExtlib.profile
1941 (type_of_aux' ?localization_tbl metasenv context term) ugraph
1943 let typecheck ~localization_tbl metasenv uri obj =
1944 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
1946 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
1947 (* vim:set foldmethod=marker: *)