1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
30 exception RefineFailure of string Lazy.t;;
31 exception Uncertain of string Lazy.t;;
32 exception AssertFailure of string Lazy.t;;
34 let insert_coercions = ref true
35 let pack_coercions = ref true
37 let debug_print = fun _ -> ();;
38 (*let debug_print x = prerr_endline (Lazy.force x);;*)
40 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
42 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
45 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
46 in profiler_eat_prods2.HExtlib.profile foo ()
48 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
49 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
52 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
54 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
57 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
58 in profiler_eat_prods.HExtlib.profile foo ()
60 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
61 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
64 let profiler = HExtlib.profile "CicRefine.fo_unif"
66 let fo_unif_subst subst context metasenv t1 t2 ugraph =
69 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
70 in profiler.HExtlib.profile foo ()
72 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
73 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
76 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
79 RefineFailure msg -> RefineFailure (f msg)
80 | Uncertain msg -> Uncertain (f msg)
81 | Sys.Break -> raise exn
82 | _ -> assert false in
85 Cic.CicHash.find localization_tbl t
87 prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
90 raise (HExtlib.Localized (loc,exn'))
92 let relocalize localization_tbl oldt newt =
94 let infos = Cic.CicHash.find localization_tbl oldt in
95 Cic.CicHash.remove localization_tbl oldt;
96 Cic.CicHash.add localization_tbl newt infos;
104 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
105 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
108 let exp_impl metasenv subst context =
111 let (metasenv', idx) =
112 CicMkImplicit.mk_implicit_type metasenv subst context in
114 CicMkImplicit.identity_relocation_list_for_metavariable context in
115 metasenv', Cic.Meta (idx, irl)
117 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
118 metasenv', Cic.Meta (idx, [])
120 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
122 CicMkImplicit.identity_relocation_list_for_metavariable context in
123 metasenv', Cic.Meta (idx, irl)
127 let is_a_double_coercion t =
129 let rec aux acc = function
131 | x::tl -> aux (acc@[x]) tl
136 let imp = Cic.Implicit None in
137 let dummyres = false,imp, imp,imp,imp in
139 | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 ->
140 (match last_of tl with
141 | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
142 let sib2,head = last_of tl2 in
143 true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
148 let more_args_than_expected
149 localization_tbl subst he context hetype' tlbody_and_type exn
153 CicMetaSubst.ppterm_in_context subst he context ^
154 " (that has type "^CicMetaSubst.ppterm_in_context subst hetype' context ^
155 ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
156 " arguments that are more than expected")
158 enrich localization_tbl he ~f:(fun _-> msg) exn
161 let mk_prod_of_metas metasenv context' subst args =
162 let rec mk_prod metasenv context' = function
164 let (metasenv, idx) =
165 CicMkImplicit.mk_implicit_type metasenv subst context'
168 CicMkImplicit.identity_relocation_list_for_metavariable context'
170 metasenv,Cic.Meta (idx, irl)
172 let (metasenv, idx) =
173 CicMkImplicit.mk_implicit_type metasenv subst context'
176 CicMkImplicit.identity_relocation_list_for_metavariable context'
178 let meta = Cic.Meta (idx,irl) in
180 (* The name must be fresh for context. *)
181 (* Nevertheless, argty is well-typed only in context. *)
182 (* Thus I generate a name (name_hint) in context and *)
183 (* then I generate a name --- using the hint name_hint *)
184 (* --- that is fresh in context'. *)
186 (* Cic.Name "pippo" *)
187 FreshNamesGenerator.mk_fresh_name ~subst metasenv
188 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
189 (CicMetaSubst.apply_subst_context subst context')
191 ~typ:(CicMetaSubst.apply_subst subst argty)
193 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
194 FreshNamesGenerator.mk_fresh_name ~subst
195 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
197 let metasenv,target =
198 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
200 metasenv,Cic.Prod (name,meta,target)
202 mk_prod metasenv context' args
205 let rec type_of_constant uri ugraph =
206 let module C = Cic in
207 let module R = CicReduction in
208 let module U = UriManager in
209 let _ = CicTypeChecker.typecheck uri in
212 CicEnvironment.get_cooked_obj ugraph uri
213 with Not_found -> assert false
216 C.Constant (_,_,ty,_,_) -> ty,u
217 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
221 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
223 and type_of_variable uri ugraph =
224 let module C = Cic in
225 let module R = CicReduction in
226 let module U = UriManager in
227 let _ = CicTypeChecker.typecheck uri in
230 CicEnvironment.get_cooked_obj ugraph uri
231 with Not_found -> assert false
234 C.Variable (_,_,ty,_,_) -> ty,u
238 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
240 and type_of_mutual_inductive_defs uri i ugraph =
241 let module C = Cic in
242 let module R = CicReduction in
243 let module U = UriManager in
244 let _ = CicTypeChecker.typecheck uri in
247 CicEnvironment.get_cooked_obj ugraph uri
248 with Not_found -> assert false
251 C.InductiveDefinition (dl,_,_,_) ->
252 let (_,_,arity,_) = List.nth dl i in
257 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
259 and type_of_mutual_inductive_constr uri i j ugraph =
260 let module C = Cic in
261 let module R = CicReduction in
262 let module U = UriManager in
263 let _ = CicTypeChecker.typecheck uri in
266 CicEnvironment.get_cooked_obj ugraph uri
267 with Not_found -> assert false
270 C.InductiveDefinition (dl,_,_,_) ->
271 let (_,_,_,cl) = List.nth dl i in
272 let (_,ty) = List.nth cl (j-1) in
278 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
281 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
283 (* the check_branch function checks if a branch of a case is refinable.
284 It returns a pair (outype_instance,args), a subst and a metasenv.
285 outype_instance is the expected result of applying the case outtype
287 The problem is that outype is in general unknown, and we should
288 try to synthesize it from the above information, that is in general
289 a second order unification problem. *)
291 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
292 let module C = Cic in
293 (* let module R = CicMetaSubst in *)
294 let module R = CicReduction in
295 match R.whd ~subst context expectedtype with
297 (n,context,actualtype, [term]), subst, metasenv, ugraph
298 | C.Appl (C.MutInd (_,_,_)::tl) ->
299 let (_,arguments) = split tl left_args_no in
300 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
301 | C.Prod (name,so,de) ->
302 (* we expect that the actual type of the branch has the due
304 (match R.whd ~subst context actualtype with
305 C.Prod (name',so',de') ->
306 let subst, metasenv, ugraph1 =
307 fo_unif_subst subst context metasenv so so' ugraph in
309 (match CicSubstitution.lift 1 term with
310 C.Appl l -> C.Appl (l@[C.Rel 1])
311 | t -> C.Appl [t ; C.Rel 1]) in
312 (* we should also check that the name variable is anonymous in
313 the actual type de' ?? *)
315 ((Some (name,(C.Decl so)))::context)
316 metasenv subst left_args_no de' term' de ugraph1
317 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
318 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
320 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
323 let rec type_of_aux subst metasenv context t ugraph =
324 let module C = Cic in
325 let module S = CicSubstitution in
326 let module U = UriManager in
327 let try_coercion t subst metasenv context ugraph coercion_tgt c =
328 let coerced = C.Appl[c;t] in
330 let newt,_,subst,metasenv,ugraph =
331 type_of_aux subst metasenv context coerced ugraph
333 let newt, tty, subst, metasenv, ugraph =
334 avoid_double_coercion context subst metasenv ugraph newt coercion_tgt
336 Some (newt, tty, subst, metasenv, ugraph)
338 | RefineFailure _ | Uncertain _ -> None
340 let (t',_,_,_,_) as res =
345 match List.nth context (n - 1) with
346 Some (_,C.Decl ty) ->
347 t,S.lift n ty,subst,metasenv, ugraph
348 | Some (_,C.Def (_,Some ty)) ->
349 t,S.lift n ty,subst,metasenv, ugraph
350 | Some (_,C.Def (bo,None)) ->
352 (* if it is in the context it must be already well-typed*)
353 CicTypeChecker.type_of_aux' ~subst metasenv context
356 t,ty,subst,metasenv,ugraph
358 enrich localization_tbl t
359 (RefineFailure (lazy "Rel to hidden hypothesis"))
362 enrich localization_tbl t
363 (RefineFailure (lazy "Not a closed term")))
364 | C.Var (uri,exp_named_subst) ->
365 let exp_named_subst',subst',metasenv',ugraph1 =
366 check_exp_named_subst
367 subst metasenv context exp_named_subst ugraph
369 let ty_uri,ugraph1 = type_of_variable uri ugraph in
371 CicSubstitution.subst_vars exp_named_subst' ty_uri
373 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
376 let (canonical_context, term,ty) =
377 CicUtil.lookup_subst n subst
379 let l',subst',metasenv',ugraph1 =
380 check_metasenv_consistency n subst metasenv context
381 canonical_context l ugraph
383 (* trust or check ??? *)
384 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
385 subst', metasenv', ugraph1
386 (* type_of_aux subst metasenv
387 context (CicSubstitution.subst_meta l term) *)
388 with CicUtil.Subst_not_found _ ->
389 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
390 let l',subst',metasenv', ugraph1 =
391 check_metasenv_consistency n subst metasenv context
392 canonical_context l ugraph
394 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
395 subst', metasenv',ugraph1)
396 | C.Sort (C.Type tno) ->
397 let tno' = CicUniv.fresh() in
398 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
399 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
401 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
402 | C.Implicit infos ->
403 let metasenv',t' = exp_impl metasenv subst context infos in
404 type_of_aux subst metasenv' context t' ugraph
406 let ty',_,subst',metasenv',ugraph1 =
407 type_of_aux subst metasenv context ty ugraph
409 let te',inferredty,subst'',metasenv'',ugraph2 =
410 type_of_aux subst' metasenv' context te ugraph1
413 let subst''',metasenv''',ugraph3 =
414 fo_unif_subst subst'' context metasenv''
415 inferredty ty' ugraph2
417 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
420 enrich localization_tbl te'
423 CicMetaSubst.ppterm_in_context subst'' te'
424 context ^ " has type " ^
425 CicMetaSubst.ppterm_in_context subst'' inferredty
426 context ^ " but is here used with type " ^
427 CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
429 | C.Prod (name,s,t) ->
430 let carr t subst context = CicMetaSubst.apply_subst subst t in
431 let coerce_to_sort in_source tgt_sort t type_to_coerce
432 subst context metasenv uragph
434 if not !insert_coercions then
435 t,type_to_coerce,subst,metasenv,ugraph
437 let coercion_src = carr type_to_coerce subst context in
438 match coercion_src with
440 t,type_to_coerce,subst,metasenv,ugraph
441 | Cic.Meta _ as meta ->
442 t, meta, subst, metasenv, ugraph
443 | Cic.Cast _ as cast ->
444 t, cast, subst, metasenv, ugraph
446 let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
448 CoercGraph.look_for_coercion coercion_src coercion_tgt
451 | CoercGraph.NoCoercion
452 | CoercGraph.NotHandled _ ->
453 enrich localization_tbl t
456 CicMetaSubst.ppterm_in_context subst t context ^
457 " is not a type since it has type " ^
458 CicMetaSubst.ppterm_in_context
459 subst coercion_src context ^ " that is not a sort")))
460 | CoercGraph.NotMetaClosed ->
461 enrich localization_tbl t
464 CicMetaSubst.ppterm_in_context subst t context ^
465 " is not a type since it has type " ^
466 CicMetaSubst.ppterm_in_context
467 subst coercion_src context ^ " that is not a sort")))
468 | CoercGraph.SomeCoercion candidates ->
472 t subst metasenv context ugraph coercion_tgt)
478 enrich localization_tbl t
481 CicMetaSubst.ppterm_in_context
483 " is not a type since it has type " ^
484 CicMetaSubst.ppterm_in_context
485 subst coercion_src context ^
486 " that is not a sort"))))
488 let s',sort1,subst',metasenv',ugraph1 =
489 type_of_aux subst metasenv context s ugraph
491 let s',sort1,subst', metasenv',ugraph1 =
492 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
493 s' sort1 subst' context metasenv' ugraph1
495 let context_for_t = ((Some (name,(C.Decl s')))::context) in
496 let t',sort2,subst'',metasenv'',ugraph2 =
497 type_of_aux subst' metasenv'
498 context_for_t t ugraph1
500 let t',sort2,subst'',metasenv'',ugraph2 =
501 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
502 t' sort2 subst'' context_for_t metasenv'' ugraph2
504 let sop,subst''',metasenv''',ugraph3 =
505 sort_of_prod subst'' metasenv''
506 context (name,s') (sort1,sort2) ugraph2
508 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
509 | C.Lambda (n,s,t) ->
511 let s',sort1,subst',metasenv',ugraph1 =
512 type_of_aux subst metasenv context s ugraph in
513 let s',sort1,subst',metasenv',ugraph1 =
514 if not !insert_coercions then
515 s',sort1, subst', metasenv', ugraph1
517 match CicReduction.whd ~subst:subst' context sort1 with
518 | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
520 let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
522 CoercGraph.look_for_coercion coercion_src coercion_tgt
525 | CoercGraph.NoCoercion
526 | CoercGraph.NotHandled _ ->
527 enrich localization_tbl s'
530 CicMetaSubst.ppterm_in_context subst s' context ^
531 " is not a type since it has type " ^
532 CicMetaSubst.ppterm_in_context
533 subst coercion_src context ^ " that is not a sort")))
534 | CoercGraph.NotMetaClosed ->
535 enrich localization_tbl s'
538 CicMetaSubst.ppterm_in_context subst s' context ^
539 " is not a type since it has type " ^
540 CicMetaSubst.ppterm_in_context
541 subst coercion_src context ^ " that is not a sort")))
542 | CoercGraph.SomeCoercion candidates ->
546 s' subst' metasenv' context ugraph1 coercion_tgt)
552 enrich localization_tbl s'
555 CicMetaSubst.ppterm_in_context subst s' context ^
556 " is not a type since it has type " ^
557 CicMetaSubst.ppterm_in_context
558 subst coercion_src context ^
559 " that is not a sort")))
561 let context_for_t = ((Some (n,(C.Decl s')))::context) in
562 let t',type2,subst'',metasenv'',ugraph2 =
563 type_of_aux subst' metasenv' context_for_t t ugraph1
565 C.Lambda (n,s',t'),C.Prod (n,s',type2),
566 subst'',metasenv'',ugraph2
568 (* only to check if s is well-typed *)
569 let s',ty,subst',metasenv',ugraph1 =
570 type_of_aux subst metasenv context s ugraph
572 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
574 let t',inferredty,subst'',metasenv'',ugraph2 =
575 type_of_aux subst' metasenv'
576 context_for_t t ugraph1
578 (* One-step LetIn reduction.
579 * Even faster than the previous solution.
580 * Moreover the inferred type is closer to the expected one.
583 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
584 subst'',metasenv'',ugraph2
585 | C.Appl (he::((_::_) as tl)) ->
586 let he',hetype,subst',metasenv',ugraph1 =
587 type_of_aux subst metasenv context he ugraph
589 let tlbody_and_type,subst'',metasenv'',ugraph2 =
590 typeof_list subst' metasenv' context ugraph1 tl
592 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
593 eat_prods true subst'' metasenv'' context
594 he' hetype tlbody_and_type ugraph2
596 let newappl = (C.Appl (coerced_he::coerced_args)) in
597 avoid_double_coercion
598 context subst''' metasenv''' ugraph3 newappl applty
599 | C.Appl _ -> assert false
600 | C.Const (uri,exp_named_subst) ->
601 let exp_named_subst',subst',metasenv',ugraph1 =
602 check_exp_named_subst subst metasenv context
603 exp_named_subst ugraph in
604 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
606 CicSubstitution.subst_vars exp_named_subst' ty_uri
608 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
609 | C.MutInd (uri,i,exp_named_subst) ->
610 let exp_named_subst',subst',metasenv',ugraph1 =
611 check_exp_named_subst subst metasenv context
612 exp_named_subst ugraph
614 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
616 CicSubstitution.subst_vars exp_named_subst' ty_uri in
617 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
618 | C.MutConstruct (uri,i,j,exp_named_subst) ->
619 let exp_named_subst',subst',metasenv',ugraph1 =
620 check_exp_named_subst subst metasenv context
621 exp_named_subst ugraph
624 type_of_mutual_inductive_constr uri i j ugraph1
627 CicSubstitution.subst_vars exp_named_subst' ty_uri
629 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
631 | C.MutCase (uri, i, outtype, term, pl) ->
632 (* first, get the inductive type (and noparams)
633 * in the environment *)
634 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
635 let _ = CicTypeChecker.typecheck uri in
636 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
638 C.InductiveDefinition (l,expl_params,parsno,_) ->
639 List.nth l i , expl_params, parsno, u
641 enrich localization_tbl t
643 (lazy ("Unkown mutual inductive definition " ^
644 U.string_of_uri uri)))
646 let rec count_prod t =
647 match CicReduction.whd ~subst context t with
648 C.Prod (_, _, t) -> 1 + (count_prod t)
651 let no_args = count_prod arity in
652 (* now, create a "generic" MutInd *)
653 let metasenv,left_args =
654 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
656 let metasenv,right_args =
657 let no_right_params = no_args - no_left_params in
658 if no_right_params < 0 then assert false
659 else CicMkImplicit.n_fresh_metas
660 metasenv subst context no_right_params
662 let metasenv,exp_named_subst =
663 CicMkImplicit.fresh_subst metasenv subst context expl_params in
666 C.MutInd (uri,i,exp_named_subst)
669 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
671 (* check consistency with the actual type of term *)
672 let term',actual_type,subst,metasenv,ugraph1 =
673 type_of_aux subst metasenv context term ugraph in
674 let expected_type',_, subst, metasenv,ugraph2 =
675 type_of_aux subst metasenv context expected_type ugraph1
677 let actual_type = CicReduction.whd ~subst context actual_type in
678 let subst,metasenv,ugraph3 =
680 fo_unif_subst subst context metasenv
681 expected_type' actual_type ugraph2
684 enrich localization_tbl term' exn
687 CicMetaSubst.ppterm_in_context subst term'
688 context ^ " has type " ^
689 CicMetaSubst.ppterm_in_context subst actual_type
690 context ^ " but is here used with type " ^
691 CicMetaSubst.ppterm_in_context subst expected_type' context))
693 let rec instantiate_prod t =
697 match CicReduction.whd ~subst context t with
699 instantiate_prod (CicSubstitution.subst he t') tl
702 let arity_instantiated_with_left_args =
703 instantiate_prod arity left_args in
704 (* TODO: check if the sort elimination
705 * is allowed: [(I q1 ... qr)|B] *)
706 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
708 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
710 if left_args = [] then
711 (C.MutConstruct (uri,i,j,exp_named_subst))
714 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
716 let p',actual_type,subst,metasenv,ugraph1 =
717 type_of_aux subst metasenv context p ugraph
719 let constructor',expected_type, subst, metasenv,ugraph2 =
720 type_of_aux subst metasenv context constructor ugraph1
722 let outtypeinstance,subst,metasenv,ugraph3 =
723 check_branch 0 context metasenv subst no_left_params
724 actual_type constructor' expected_type ugraph2
727 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
728 ([],1,[],subst,metasenv,ugraph3) pl
731 (* we are left to check that the outype matches his instances.
732 The easy case is when the outype is specified, that amount
733 to a trivial check. Otherwise, we should guess a type from
737 let outtype,outtypety, subst, metasenv,ugraph4 =
738 type_of_aux subst metasenv context outtype ugraph4 in
741 (let candidate,ugraph5,metasenv,subst =
742 let exp_name_subst, metasenv =
744 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
746 let uris = CicUtil.params_of_obj o in
748 fun uri (acc,metasenv) ->
749 let metasenv',new_meta =
750 CicMkImplicit.mk_implicit metasenv subst context
753 CicMkImplicit.identity_relocation_list_for_metavariable
756 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
760 match left_args,right_args with
761 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
763 let rec mk_right_args =
766 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
768 let right_args_no = List.length right_args in
769 let lifted_left_args =
770 List.map (CicSubstitution.lift right_args_no) left_args
772 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
773 (lifted_left_args @ mk_right_args right_args_no))
776 FreshNamesGenerator.mk_fresh_name ~subst metasenv
777 context Cic.Anonymous ~typ:ty
779 match outtypeinstances with
781 let extended_context =
782 let rec add_right_args =
784 Cic.Prod (name,ty,t) ->
785 Some (name,Cic.Decl ty)::(add_right_args t)
788 (Some (fresh_name,Cic.Decl ty))::
790 (add_right_args arity_instantiated_with_left_args))@
793 let metasenv,new_meta =
794 CicMkImplicit.mk_implicit metasenv subst extended_context
797 CicMkImplicit.identity_relocation_list_for_metavariable
800 let rec add_lambdas b =
802 Cic.Prod (name,ty,t) ->
803 Cic.Lambda (name,ty,(add_lambdas b t))
804 | _ -> Cic.Lambda (fresh_name, ty, b)
807 add_lambdas (Cic.Meta (new_meta,irl))
808 arity_instantiated_with_left_args
810 (Some candidate),ugraph4,metasenv,subst
811 | (constructor_args_no,_,instance,_)::tl ->
813 let instance',subst,metasenv =
814 CicMetaSubst.delift_rels subst metasenv
815 constructor_args_no instance
817 let candidate,ugraph,metasenv,subst =
819 fun (candidate_oty,ugraph,metasenv,subst)
820 (constructor_args_no,_,instance,_) ->
821 match candidate_oty with
822 | None -> None,ugraph,metasenv,subst
825 let instance',subst,metasenv =
826 CicMetaSubst.delift_rels subst metasenv
827 constructor_args_no instance
829 let subst,metasenv,ugraph =
830 fo_unif_subst subst context metasenv
833 candidate_oty,ugraph,metasenv,subst
835 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
836 | CicUnification.UnificationFailure _
837 | CicUnification.Uncertain _ ->
838 None,ugraph,metasenv,subst
839 ) (Some instance',ugraph4,metasenv,subst) tl
842 | None -> None, ugraph,metasenv,subst
844 let rec add_lambdas n b =
846 Cic.Prod (name,ty,t) ->
847 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
849 Cic.Lambda (fresh_name, ty,
850 CicSubstitution.lift (n + 1) t)
853 (add_lambdas 0 t arity_instantiated_with_left_args),
854 ugraph,metasenv,subst
855 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
856 None,ugraph4,metasenv,subst
859 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
861 let subst,metasenv,ugraph =
863 fo_unif_subst subst context metasenv
864 candidate outtype ugraph5
866 exn -> assert false(* unification against a metavariable *)
868 C.MutCase (uri, i, outtype, term', pl'),
869 CicReduction.head_beta_reduce
870 (CicMetaSubst.apply_subst subst
871 (Cic.Appl (outtype::right_args@[term']))),
872 subst,metasenv,ugraph)
873 | _ -> (* easy case *)
874 let tlbody_and_type,subst,metasenv,ugraph4 =
875 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
877 let _,_,_,subst,metasenv,ugraph4 =
878 eat_prods false subst metasenv context
879 outtype outtypety tlbody_and_type ugraph4
881 let _,_, subst, metasenv,ugraph5 =
882 type_of_aux subst metasenv context
883 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
885 let (subst,metasenv,ugraph6) =
887 (fun (subst,metasenv,ugraph)
888 p (constructor_args_no,context,instance,args)
893 CicSubstitution.lift constructor_args_no outtype
895 C.Appl (outtype'::args)
897 CicReduction.whd ~subst context appl
900 fo_unif_subst subst context metasenv instance instance'
904 enrich localization_tbl p exn
907 CicMetaSubst.ppterm_in_context subst p
908 context ^ " has type " ^
909 CicMetaSubst.ppterm_in_context subst instance'
910 context ^ " but is here used with type " ^
911 CicMetaSubst.ppterm_in_context subst instance
913 (subst,metasenv,ugraph5) pl' outtypeinstances
915 C.MutCase (uri, i, outtype, term', pl'),
916 CicReduction.head_beta_reduce
917 (CicMetaSubst.apply_subst subst
918 (C.Appl(outtype::right_args@[term]))),
919 subst,metasenv,ugraph6)
921 let fl_ty',subst,metasenv,types,ugraph1 =
923 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
924 let ty',_,subst',metasenv',ugraph1 =
925 type_of_aux subst metasenv context ty ugraph
927 fl @ [ty'],subst',metasenv',
928 Some (C.Name n,(C.Decl ty')) :: types, ugraph
929 ) ([],subst,metasenv,[],ugraph) fl
931 let len = List.length types in
932 let context' = types@context in
933 let fl_bo',subst,metasenv,ugraph2 =
935 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
936 let bo',ty_of_bo,subst,metasenv,ugraph1 =
937 type_of_aux subst metasenv context' bo ugraph in
938 let expected_ty = CicSubstitution.lift len ty in
939 let subst',metasenv',ugraph' =
941 fo_unif_subst subst context' metasenv
942 ty_of_bo expected_ty ugraph1
945 enrich localization_tbl bo exn
948 CicMetaSubst.ppterm_in_context subst bo
949 context' ^ " has type " ^
950 CicMetaSubst.ppterm_in_context subst ty_of_bo
951 context' ^ " but is here used with type " ^
952 CicMetaSubst.ppterm_in_context subst expected_ty
955 fl @ [bo'] , subst',metasenv',ugraph'
956 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
958 let ty = List.nth fl_ty' i in
959 (* now we have the new ty in fl_ty', the new bo in fl_bo',
960 * and we want the new fl with bo' and ty' injected in the right
963 let rec map3 f l1 l2 l3 =
966 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
969 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
972 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
974 let fl_ty',subst,metasenv,types,ugraph1 =
976 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
977 let ty',_,subst',metasenv',ugraph1 =
978 type_of_aux subst metasenv context ty ugraph
980 fl @ [ty'],subst',metasenv',
981 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
982 ) ([],subst,metasenv,[],ugraph) fl
984 let len = List.length types in
985 let context' = types@context in
986 let fl_bo',subst,metasenv,ugraph2 =
988 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
989 let bo',ty_of_bo,subst,metasenv,ugraph1 =
990 type_of_aux subst metasenv context' bo ugraph in
991 let expected_ty = CicSubstitution.lift len ty in
992 let subst',metasenv',ugraph' =
994 fo_unif_subst subst context' metasenv
995 ty_of_bo expected_ty ugraph1
998 enrich localization_tbl bo exn
1001 CicMetaSubst.ppterm_in_context subst bo
1002 context' ^ " has type " ^
1003 CicMetaSubst.ppterm_in_context subst ty_of_bo
1004 context' ^ " but is here used with type " ^
1005 CicMetaSubst.ppterm_in_context subst expected_ty
1008 fl @ [bo'],subst',metasenv',ugraph'
1009 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
1011 let ty = List.nth fl_ty' i in
1012 (* now we have the new ty in fl_ty', the new bo in fl_bo',
1013 * and we want the new fl with bo' and ty' injected in the right
1016 let rec map3 f l1 l2 l3 =
1019 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
1022 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
1025 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
1027 relocalize localization_tbl t t';
1030 (* check_metasenv_consistency checks that the "canonical" context of a
1031 metavariable is consitent - up to relocation via the relocation list l -
1032 with the actual context *)
1033 and check_metasenv_consistency
1034 metano subst metasenv context canonical_context l ugraph
1036 let module C = Cic in
1037 let module R = CicReduction in
1038 let module S = CicSubstitution in
1039 let lifted_canonical_context =
1043 | (Some (n,C.Decl t))::tl ->
1044 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
1045 | (Some (n,C.Def (t,None)))::tl ->
1046 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1047 | None::tl -> None::(aux (i+1) tl)
1048 | (Some (n,C.Def (t,Some ty)))::tl ->
1050 C.Def ((S.subst_meta l (S.lift i t)),
1051 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
1053 aux 1 canonical_context
1057 (fun (l,subst,metasenv,ugraph) t ct ->
1060 l @ [None],subst,metasenv,ugraph
1061 | Some t,Some (_,C.Def (ct,_)) ->
1062 let subst',metasenv',ugraph' =
1064 prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
1065 fo_unif_subst subst context metasenv t ct ugraph
1066 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 subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
1068 l @ [Some t],subst',metasenv',ugraph'
1069 | Some t,Some (_,C.Decl ct) ->
1070 let t',inferredty,subst',metasenv',ugraph1 =
1071 type_of_aux subst metasenv context t ugraph
1073 let subst'',metasenv'',ugraph2 =
1076 subst' context metasenv' inferredty ct ugraph1
1077 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 subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
1079 l @ [Some t'], subst'',metasenv'',ugraph2
1081 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 subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
1083 Invalid_argument _ ->
1087 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1088 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
1089 (CicMetaSubst.ppcontext subst canonical_context))))
1091 and check_exp_named_subst metasubst metasenv context tl ugraph =
1092 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1094 [] -> [],metasubst,metasenv,ugraph
1096 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1098 CicSubstitution.subst_vars substs ty_uri in
1099 (* CSC: why was this code here? it is wrong
1100 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1101 Cic.Variable (_,Some bo,_,_) ->
1103 (RefineFailure (lazy
1104 "A variable with a body can not be explicit substituted"))
1105 | Cic.Variable (_,None,_,_) -> ()
1108 (RefineFailure (lazy
1109 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1112 let t',typeoft,metasubst',metasenv',ugraph2 =
1113 type_of_aux metasubst metasenv context t ugraph1 in
1114 let subst = uri,t' in
1115 let metasubst'',metasenv'',ugraph3 =
1118 metasubst' context metasenv' typeoft typeofvar ugraph2
1120 raise (RefineFailure (lazy
1121 ("Wrong Explicit Named Substitution: " ^
1122 CicMetaSubst.ppterm metasubst' typeoft ^
1123 " not unifiable with " ^
1124 CicMetaSubst.ppterm metasubst' typeofvar)))
1126 (* FIXME: no mere tail recursive! *)
1127 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1128 check_exp_named_subst_aux
1129 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1131 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1133 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1136 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
1137 let module C = Cic in
1138 let context_for_t2 = (Some (name,C.Decl s))::context in
1139 let t1'' = CicReduction.whd ~subst context t1 in
1140 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1141 match (t1'', t2'') with
1142 (C.Sort s1, C.Sort s2)
1143 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1144 (* different than Coq manual!!! *)
1145 C.Sort s2,subst,metasenv,ugraph
1146 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1147 let t' = CicUniv.fresh() in
1148 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1149 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1150 C.Sort (C.Type t'),subst,metasenv,ugraph2
1151 | (C.Sort _,C.Sort (C.Type t1)) ->
1152 C.Sort (C.Type t1),subst,metasenv,ugraph
1153 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1154 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1155 (* TODO how can we force the meta to become a sort? If we don't we
1156 * break the invariant that refine produce only well typed terms *)
1157 (* TODO if we check the non meta term and if it is a sort then we
1158 * are likely to know the exact value of the result e.g. if the rhs
1159 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1160 let (metasenv,idx) =
1161 CicMkImplicit.mk_implicit_sort metasenv subst in
1162 let (subst, metasenv,ugraph1) =
1164 fo_unif_subst subst context_for_t2 metasenv
1165 (C.Meta (idx,[])) t2'' ugraph
1166 with _ -> assert false (* unification against a metavariable *)
1168 t2'',subst,metasenv,ugraph1
1174 ("Two sorts were expected, found %s " ^^
1175 "(that reduces to %s) and %s (that reduces to %s)")
1176 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
1177 (CicPp.ppterm t2''))))
1179 and avoid_double_coercion context subst metasenv ugraph t ty =
1180 if not !pack_coercions then
1181 t,ty,subst,metasenv,ugraph
1183 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1185 let source_carr = CoercGraph.source_of c2 in
1186 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1187 (match CoercGraph.look_for_coercion source_carr tgt_carr
1189 | CoercGraph.SomeCoercion candidates ->
1191 HExtlib.list_findopt
1193 | c when not (CoercGraph.is_composite c) ->
1194 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1199 | Cic.Appl l -> Cic.Appl (l @ [head])
1200 | _ -> Cic.Appl [c;head]
1202 debug_print (lazy ("\nprovo" ^ CicPp.ppterm newt));
1207 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
1208 let newt,_,subst,metasenv,ugraph =
1209 type_of_aux subst metasenv context newt ugraph in
1210 debug_print (lazy "tipa...");
1211 let subst, metasenv, ugraph =
1212 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1213 fo_unif_subst subst context metasenv newt t ugraph
1215 debug_print (lazy "unifica...");
1216 Some (newt, ty, subst, metasenv, ugraph)
1218 | RefineFailure s | Uncertain s when not !pack_coercions->
1219 debug_print s; debug_print (lazy "stop\n");None
1220 | RefineFailure s | Uncertain s ->
1221 debug_print s;debug_print (lazy "goon\n");
1223 let old_pack_coercions = !pack_coercions in
1224 pack_coercions := false; (* to avoid diverging *)
1225 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1226 type_of_aux subst metasenv context c1_c2_implicit ugraph
1228 pack_coercions := old_pack_coercions;
1230 is_a_double_coercion refined_c1_c2_implicit
1236 match refined_c1_c2_implicit with
1237 | Cic.Appl l -> HExtlib.list_last l
1240 let subst, metasenv, ugraph =
1241 try fo_unif_subst subst context metasenv
1243 with RefineFailure s| Uncertain s->
1244 debug_print s;assert false
1246 let subst, metasenv, ugraph =
1247 fo_unif_subst subst context metasenv
1248 refined_c1_c2_implicit t ugraph
1250 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1252 | RefineFailure s | Uncertain s ->
1253 pack_coercions := true;debug_print s;None
1254 | exn -> pack_coercions := true; raise exn))
1257 (match selected with
1261 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1262 t, ty, subst, metasenv, ugraph)
1263 | _ -> t, ty, subst, metasenv, ugraph)
1265 t, ty, subst, metasenv, ugraph
1267 and typeof_list subst metasenv context ugraph l =
1268 let tlbody_and_type,subst,metasenv,ugraph =
1270 (fun x (res,subst,metasenv,ugraph) ->
1271 let x',ty,subst',metasenv',ugraph1 =
1272 type_of_aux subst metasenv context x ugraph
1274 (x', ty)::res,subst',metasenv',ugraph1
1275 ) l ([],subst,metasenv,ugraph)
1277 tlbody_and_type,subst,metasenv,ugraph
1280 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1282 (* aux function to add coercions to funclass *)
1283 let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph =
1285 let pristinemenv = metasenv in
1286 let metasenv,hetype' =
1287 mk_prod_of_metas metasenv context subst args_bo_and_ty
1290 let subst,metasenv,ugraph =
1291 fo_unif_subst_eat_prods
1292 subst context metasenv hetype hetype' ugraph
1294 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1295 with RefineFailure s | Uncertain s as exn
1296 when allow_coercions && !insert_coercions ->
1297 (* {{{ we search a coercion of the head (saturated) to funclass *)
1298 let metasenv = pristinemenv in
1300 ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^
1301 " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype'
1302 (* ^ " cause: " ^ Lazy.force s *)));
1303 let how_many_args_are_needed =
1304 let rec aux n = function
1305 | Cic.Prod(_,_,t) -> aux (n+1) t
1308 aux 0 (CicMetaSubst.apply_subst subst hetype)
1310 let args, remainder =
1311 HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
1313 let args = List.map fst args in
1317 | Cic.Appl l -> Cic.Appl (l@args)
1318 | _ -> Cic.Appl (he::args)
1322 let x,xty,subst,metasenv,ugraph =
1323 type_of_aux subst metasenv context x ugraph
1326 CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty)
1328 let carr_tgt = CoercDb.Fun 0 in
1329 match CoercGraph.look_for_coercion' carr_src carr_tgt with
1330 | CoercGraph.NoCoercion
1331 | CoercGraph.NotMetaClosed
1332 | CoercGraph.NotHandled _ -> raise exn
1333 | CoercGraph.SomeCoercion candidates ->
1335 HExtlib.list_findopt
1337 let t = Cic.Appl [coerc;x] in
1338 debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t));
1340 (* we want this to be available in the error handler fo the
1341 * following (so it has its own try. *)
1342 let t,tty,subst,metasenv,ugraph =
1343 type_of_aux subst metasenv context t ugraph
1346 let metasenv, hetype' =
1347 mk_prod_of_metas metasenv context subst remainder
1350 (" unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^
1351 CicMetaSubst.ppterm subst hetype'));
1352 let subst,metasenv,ugraph =
1353 fo_unif_subst_eat_prods
1354 subst context metasenv tty hetype' ugraph
1356 debug_print (lazy " success!");
1357 Some (subst,metasenv,ugraph,tty,t,remainder)
1359 | Uncertain _ | RefineFailure _
1360 | CicUnification.UnificationFailure _
1361 | CicUnification.Uncertain _ ->
1363 let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
1365 metasenv context subst t tty remainder ugraph
1367 Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
1368 with Uncertain _ | RefineFailure _ -> None
1369 with Uncertain _ | RefineFailure _ -> None)
1372 | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
1373 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1375 more_args_than_expected localization_tbl
1376 subst he context hetype args_bo_and_ty exn
1377 (* }}} end coercion to funclass stuff *)
1378 (* }}} end fix_arity *)
1380 (* aux function to process the type of the head and the args in parallel *)
1381 let rec eat_prods_and_args
1382 pristinemenv metasenv subst context pristinehe he hetype ugraph newargs
1386 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1387 | (hete, hety)::tl ->
1388 match (CicReduction.whd ~subst context hetype) with
1389 | Cic.Prod (n,s,t) ->
1390 let arg,subst,metasenv,ugraph1 =
1392 let subst,metasenv,ugraph1 =
1393 fo_unif_subst_eat_prods2
1394 subst context metasenv hety s ugraph
1396 (hete,hety),subst,metasenv,ugraph1
1397 (* {{{ we search a coercion from hety to s if fails *)
1398 with RefineFailure _ | Uncertain _ as exn
1399 when allow_coercions && !insert_coercions ->
1400 let coer, tgt_carr =
1401 let carr t subst context =
1402 CicReduction.whd ~delta:false
1403 context (CicMetaSubst.apply_subst subst t )
1405 let c_hety = carr hety subst context in
1406 let c_s = carr s subst context in
1407 CoercGraph.look_for_coercion c_hety c_s, c_s
1410 | CoercGraph.NoCoercion
1411 | CoercGraph.NotHandled _ ->
1412 enrich localization_tbl hete
1414 (lazy ("The term " ^
1415 CicMetaSubst.ppterm_in_context subst hete
1416 context ^ " has type " ^
1417 CicMetaSubst.ppterm_in_context subst hety
1418 context ^ " but is here used with type " ^
1419 CicMetaSubst.ppterm_in_context subst s context
1420 (* "\nReason: " ^ Lazy.force e*))))
1421 | CoercGraph.NotMetaClosed ->
1422 enrich localization_tbl hete
1424 (lazy ("The term " ^
1425 CicMetaSubst.ppterm_in_context subst hete
1426 context ^ " has type " ^
1427 CicMetaSubst.ppterm_in_context subst hety
1428 context ^ " but is here used with type " ^
1429 CicMetaSubst.ppterm_in_context subst s context
1430 (* "\nReason: " ^ Lazy.force e*))))
1431 | CoercGraph.SomeCoercion candidates ->
1433 HExtlib.list_findopt
1436 let t = Cic.Appl[c;hete] in
1437 let newt,newhety,subst,metasenv,ugraph =
1438 type_of_aux subst metasenv context
1441 let newt, newty, subst, metasenv, ugraph =
1442 avoid_double_coercion context subst metasenv
1443 ugraph newt tgt_carr
1445 let subst,metasenv,ugraph1 =
1446 fo_unif_subst subst context metasenv
1449 Some ((newt,newty), subst, metasenv, ugraph)
1450 with Uncertain _ | RefineFailure _ -> None)
1453 (match selected with
1456 enrich localization_tbl hete
1458 (lazy ("The term " ^
1459 CicMetaSubst.ppterm_in_context subst hete
1460 context ^ " has type " ^
1461 CicMetaSubst.ppterm_in_context subst hety
1462 context ^ " but is here used with type " ^
1463 CicMetaSubst.ppterm_in_context subst s context
1464 (* "\nReason: " ^ Lazy.force e*)))) exn))
1466 enrich localization_tbl hete
1468 (lazy ("The term " ^
1469 CicMetaSubst.ppterm_in_context subst hete
1470 context ^ " has type " ^
1471 CicMetaSubst.ppterm_in_context subst hety
1472 context ^ " but is here used with type " ^
1473 CicMetaSubst.ppterm_in_context subst s context
1474 (* "\nReason: " ^ Printexc.to_string exn*)))) exn
1475 (* }}} end coercion stuff *)
1477 eat_prods_and_args pristinemenv metasenv subst context pristinehe he
1478 (CicSubstitution.subst (fst arg) t)
1479 ugraph1 (newargs@[arg]) tl
1482 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1484 pristinemenv context subst he hetype
1485 (newargs@[hete,hety]@tl) ugraph
1487 eat_prods_and_args metasenv
1488 metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
1489 with RefineFailure _ | Uncertain _ as exn ->
1490 (* unable to fix arity *)
1491 more_args_than_expected localization_tbl
1492 subst he context hetype args_bo_and_ty exn
1495 (* first we check if we are in the simple case of a meta closed term *)
1496 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1497 if CicUtil.is_meta_closed hetype then
1498 (* this optimization is to postpone fix_arity (the most common case)*)
1499 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1501 (* this (says CSC) is also useful to infer dependent types *)
1503 fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
1504 with RefineFailure _ | Uncertain _ as exn ->
1505 (* unable to fix arity *)
1506 more_args_than_expected localization_tbl
1507 subst he context hetype args_bo_and_ty exn
1509 let coerced_args,subst,metasenv,he,t,ugraph =
1511 metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
1513 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1516 (* eat prods ends here! *)
1518 let t',ty,subst',metasenv',ugraph1 =
1519 type_of_aux [] metasenv context t ugraph
1521 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1522 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1523 (* Andrea: ho rimesso qui l'applicazione della subst al
1524 metasenv dopo che ho droppato l'invariante che il metsaenv
1525 e' sempre istanziato *)
1526 let substituted_metasenv =
1527 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1529 (* substituted_t,substituted_ty,substituted_metasenv *)
1530 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1532 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1534 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1535 let cleaned_metasenv =
1537 (function (n,context,ty) ->
1538 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1543 | Some (n, Cic.Decl t) ->
1545 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1546 | Some (n, Cic.Def (bo,ty)) ->
1547 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1552 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1554 Some (n, Cic.Def (bo',ty'))
1558 ) substituted_metasenv
1560 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1563 let undebrujin uri typesno tys t =
1566 (fun (name,_,_,_) (i,t) ->
1567 (* here the explicit_named_substituion is assumed to be *)
1569 let t' = Cic.MutInd (uri,i,[]) in
1570 let t = CicSubstitution.subst t' t in
1572 ) tys (typesno - 1,t))
1574 let map_first_n n start f g l =
1575 let rec aux acc k l =
1578 | [] -> raise (Invalid_argument "map_first_n")
1579 | hd :: tl -> f hd k (aux acc (k+1) tl)
1585 (*CSC: this is a very rough approximation; to be finished *)
1586 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1587 let subst,metasenv,ugraph,tys =
1589 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1590 let subst,metasenv,ugraph,cl =
1592 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1593 let rec aux ctx k subst = function
1594 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1595 let subst,metasenv,ugraph,tl =
1597 (subst,metasenv,ugraph,[])
1598 (fun t n (subst,metasenv,ugraph,acc) ->
1599 let subst,metasenv,ugraph =
1601 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1603 subst,metasenv,ugraph,(t::acc))
1604 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1607 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1608 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1609 subst,metasenv,ugraph,t
1610 | Cic.Prod (name,s,t) ->
1611 let ctx = (Some (name,Cic.Decl s))::ctx in
1612 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1613 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1617 (lazy "not well formed constructor type"))
1619 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1620 subst,metasenv,ugraph,(name,ty) :: acc)
1621 cl (subst,metasenv,ugraph,[])
1623 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1624 tys ([],metasenv,ugraph,[])
1626 let substituted_tys =
1628 (fun (name,ind,arity,cl) ->
1630 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1632 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1635 metasenv,ugraph,substituted_tys
1637 let typecheck metasenv uri obj ~localization_tbl =
1638 let ugraph = CicUniv.empty_ugraph in
1640 Cic.Constant (name,Some bo,ty,args,attrs) ->
1641 let bo',boty,metasenv,ugraph =
1642 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1643 let ty',_,metasenv,ugraph =
1644 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1645 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1646 let bo' = CicMetaSubst.apply_subst subst bo' in
1647 let ty' = CicMetaSubst.apply_subst subst ty' in
1648 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1649 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1650 | Cic.Constant (name,None,ty,args,attrs) ->
1651 let ty',_,metasenv,ugraph =
1652 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1654 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1655 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1656 assert (metasenv' = metasenv);
1657 (* Here we do not check the metasenv for correctness *)
1658 let bo',boty,metasenv,ugraph =
1659 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1660 let ty',sort,metasenv,ugraph =
1661 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1665 (* instead of raising Uncertain, let's hope that the meta will become
1668 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1670 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1671 let bo' = CicMetaSubst.apply_subst subst bo' in
1672 let ty' = CicMetaSubst.apply_subst subst ty' in
1673 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1674 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1675 | Cic.Variable _ -> assert false (* not implemented *)
1676 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1677 (*CSC: this code is greately simplified and many many checks are missing *)
1678 (*CSC: e.g. the constructors are not required to build their own types, *)
1679 (*CSC: the arities are not required to have as type a sort, etc. *)
1680 let uri = match uri with Some uri -> uri | None -> assert false in
1681 let typesno = List.length tys in
1682 (* first phase: we fix only the types *)
1683 let metasenv,ugraph,tys =
1685 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1686 let ty',_,metasenv,ugraph =
1687 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1689 metasenv,ugraph,(name,b,ty',cl)::res
1690 ) tys (metasenv,ugraph,[]) in
1692 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1693 (* second phase: we fix only the constructors *)
1694 let metasenv,ugraph,tys =
1696 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1697 let metasenv,ugraph,cl' =
1699 (fun (name,ty) (metasenv,ugraph,res) ->
1701 CicTypeChecker.debrujin_constructor
1702 ~cb:(relocalize localization_tbl) uri typesno ty in
1703 let ty',_,metasenv,ugraph =
1704 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1705 let ty' = undebrujin uri typesno tys ty' in
1706 metasenv,ugraph,(name,ty')::res
1707 ) cl (metasenv,ugraph,[])
1709 metasenv,ugraph,(name,b,ty,cl')::res
1710 ) tys (metasenv,ugraph,[]) in
1711 (* third phase: we check the positivity condition *)
1712 let metasenv,ugraph,tys =
1713 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1715 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1718 (* sara' piu' veloce che raffinare da zero? mah.... *)
1719 let pack_coercion metasenv ctx t =
1720 let module C = Cic in
1721 let rec merge_coercions ctx =
1722 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1724 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1725 | C.Meta (n,subst) ->
1728 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1731 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1732 | C.Prod (name,so,dest) ->
1733 let ctx' = (Some (name,C.Decl so))::ctx in
1734 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1735 | C.Lambda (name,so,dest) ->
1736 let ctx' = (Some (name,C.Decl so))::ctx in
1737 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1738 | C.LetIn (name,so,dest) ->
1739 let _,ty,metasenv,ugraph =
1740 pack_coercions := false;
1741 type_of_aux' metasenv ctx so CicUniv.empty_ugraph in
1742 pack_coercions := true;
1743 let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1744 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1746 let l = List.map (merge_coercions ctx) l in
1748 let b,_,_,_,_ = is_a_double_coercion t in
1749 (* prerr_endline "CANDIDATO!!!!"; *)
1751 let ugraph = CicUniv.empty_ugraph in
1752 let old_insert_coercions = !insert_coercions in
1753 insert_coercions := false;
1754 let newt, _, menv, _ =
1756 type_of_aux' metasenv ctx t ugraph
1757 with RefineFailure _ | Uncertain _ ->
1760 insert_coercions := old_insert_coercions;
1761 if metasenv <> [] || menv = [] then
1764 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1767 | C.Var (uri,exp_named_subst) ->
1768 let exp_named_subst = List.map aux exp_named_subst in
1769 C.Var (uri, exp_named_subst)
1770 | C.Const (uri,exp_named_subst) ->
1771 let exp_named_subst = List.map aux exp_named_subst in
1772 C.Const (uri, exp_named_subst)
1773 | C.MutInd (uri,tyno,exp_named_subst) ->
1774 let exp_named_subst = List.map aux exp_named_subst in
1775 C.MutInd (uri,tyno,exp_named_subst)
1776 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1777 let exp_named_subst = List.map aux exp_named_subst in
1778 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1779 | C.MutCase (uri,tyno,out,te,pl) ->
1780 let pl = List.map (merge_coercions ctx) pl in
1781 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1782 | C.Fix (fno, fl) ->
1785 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1790 (fun (name,idx,ty,bo) ->
1791 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1795 | C.CoFix (fno, fl) ->
1798 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1803 (fun (name,ty,bo) ->
1804 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1809 merge_coercions ctx t
1812 let pack_coercion_obj obj =
1813 let module C = Cic in
1815 | C.Constant (id, body, ty, params, attrs) ->
1819 | Some body -> Some (pack_coercion [] [] body)
1821 let ty = pack_coercion [] [] ty in
1822 C.Constant (id, body, ty, params, attrs)
1823 | C.Variable (name, body, ty, params, attrs) ->
1827 | Some body -> Some (pack_coercion [] [] body)
1829 let ty = pack_coercion [] [] ty in
1830 C.Variable (name, body, ty, params, attrs)
1831 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1834 (fun (i, ctx, ty) ->
1840 Some (name, C.Decl t) ->
1841 Some (name, C.Decl (pack_coercion conjectures ctx t))
1842 | Some (name, C.Def (t,None)) ->
1843 Some (name,C.Def (pack_coercion conjectures ctx t,None))
1844 | Some (name, C.Def (t,Some ty)) ->
1845 Some (name, C.Def (pack_coercion conjectures ctx t,
1846 Some (pack_coercion conjectures ctx ty)))
1852 ((i,ctx,pack_coercion conjectures ctx ty))
1855 let body = pack_coercion conjectures [] body in
1856 let ty = pack_coercion conjectures [] ty in
1857 C.CurrentProof (name, conjectures, body, ty, params, attrs)
1858 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1861 (fun (name, ind, arity, cl) ->
1862 let arity = pack_coercion [] [] arity in
1864 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
1866 (name, ind, arity, cl))
1869 C.InductiveDefinition (indtys, params, leftno, attrs)
1874 let type_of_aux' metasenv context term =
1877 type_of_aux' metasenv context term in
1879 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1881 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1884 | RefineFailure msg as e ->
1885 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1887 | Uncertain msg as e ->
1888 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1892 let profiler2 = HExtlib.profile "CicRefine"
1894 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1895 profiler2.HExtlib.profile
1896 (type_of_aux' ?localization_tbl metasenv context term) ugraph
1898 let typecheck ~localization_tbl metasenv uri obj =
1899 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
1901 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
1902 (* vim:set foldmethod=marker: *)