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
399 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
400 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
402 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
404 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
405 | C.Implicit infos ->
406 let metasenv',t' = exp_impl metasenv subst context infos in
407 type_of_aux subst metasenv' context t' ugraph
409 let ty',_,subst',metasenv',ugraph1 =
410 type_of_aux subst metasenv context ty ugraph
412 let te',inferredty,subst'',metasenv'',ugraph2 =
413 type_of_aux subst' metasenv' context te ugraph1
416 let subst''',metasenv''',ugraph3 =
417 fo_unif_subst subst'' context metasenv''
418 inferredty ty' ugraph2
420 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
423 enrich localization_tbl te'
426 CicMetaSubst.ppterm_in_context subst'' te'
427 context ^ " has type " ^
428 CicMetaSubst.ppterm_in_context subst'' inferredty
429 context ^ " but is here used with type " ^
430 CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
432 | C.Prod (name,s,t) ->
433 let carr t subst context = CicMetaSubst.apply_subst subst t in
434 let coerce_to_sort in_source tgt_sort t type_to_coerce
435 subst context metasenv uragph
437 if not !insert_coercions then
438 t,type_to_coerce,subst,metasenv,ugraph
440 let coercion_src = carr type_to_coerce subst context in
441 match coercion_src with
443 t,type_to_coerce,subst,metasenv,ugraph
444 | Cic.Meta _ as meta ->
445 t, meta, subst, metasenv, ugraph
446 | Cic.Cast _ as cast ->
447 t, cast, subst, metasenv, ugraph
449 let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
451 CoercGraph.look_for_coercion coercion_src coercion_tgt
454 | CoercGraph.NoCoercion
455 | CoercGraph.NotHandled _ ->
456 enrich localization_tbl t
459 CicMetaSubst.ppterm_in_context subst t context ^
460 " is not a type since it has type " ^
461 CicMetaSubst.ppterm_in_context
462 subst coercion_src context ^ " that is not a sort")))
463 | CoercGraph.NotMetaClosed ->
464 enrich localization_tbl t
467 CicMetaSubst.ppterm_in_context subst t context ^
468 " is not a type since it has type " ^
469 CicMetaSubst.ppterm_in_context
470 subst coercion_src context ^ " that is not a sort")))
471 | CoercGraph.SomeCoercion candidates ->
475 t subst metasenv context ugraph coercion_tgt)
481 enrich localization_tbl t
484 CicMetaSubst.ppterm_in_context
486 " is not a type since it has type " ^
487 CicMetaSubst.ppterm_in_context
488 subst coercion_src context ^
489 " that is not a sort"))))
491 let s',sort1,subst',metasenv',ugraph1 =
492 type_of_aux subst metasenv context s ugraph
494 let s',sort1,subst', metasenv',ugraph1 =
495 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
496 s' sort1 subst' context metasenv' ugraph1
498 let context_for_t = ((Some (name,(C.Decl s')))::context) in
499 let t',sort2,subst'',metasenv'',ugraph2 =
500 type_of_aux subst' metasenv'
501 context_for_t t ugraph1
503 let t',sort2,subst'',metasenv'',ugraph2 =
504 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
505 t' sort2 subst'' context_for_t metasenv'' ugraph2
507 let sop,subst''',metasenv''',ugraph3 =
508 sort_of_prod localization_tbl subst'' metasenv''
509 context (name,s') t' (sort1,sort2) ugraph2
511 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
512 | 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 coercion_src coercion_tgt
528 | CoercGraph.NoCoercion
529 | CoercGraph.NotHandled _ ->
530 enrich localization_tbl s'
533 CicMetaSubst.ppterm_in_context subst s' context ^
534 " is not a type since it has type " ^
535 CicMetaSubst.ppterm_in_context
536 subst coercion_src context ^ " that is not a sort")))
537 | CoercGraph.NotMetaClosed ->
538 enrich localization_tbl s'
541 CicMetaSubst.ppterm_in_context subst s' context ^
542 " is not a type since it has type " ^
543 CicMetaSubst.ppterm_in_context
544 subst coercion_src context ^ " that is not a sort")))
545 | CoercGraph.SomeCoercion candidates ->
549 s' subst' metasenv' context ugraph1 coercion_tgt)
555 enrich localization_tbl s'
558 CicMetaSubst.ppterm_in_context subst s' context ^
559 " is not a type since it has type " ^
560 CicMetaSubst.ppterm_in_context
561 subst coercion_src context ^
562 " that is not a sort")))
564 let context_for_t = ((Some (n,(C.Decl s')))::context) in
565 let t',type2,subst'',metasenv'',ugraph2 =
566 type_of_aux subst' metasenv' context_for_t t ugraph1
568 C.Lambda (n,s',t'),C.Prod (n,s',type2),
569 subst'',metasenv'',ugraph2
571 (* only to check if s is well-typed *)
572 let s',ty,subst',metasenv',ugraph1 =
573 type_of_aux subst metasenv context s ugraph
575 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
577 let t',inferredty,subst'',metasenv'',ugraph2 =
578 type_of_aux subst' metasenv'
579 context_for_t t ugraph1
581 (* One-step LetIn reduction.
582 * Even faster than the previous solution.
583 * Moreover the inferred type is closer to the expected one.
586 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
587 subst'',metasenv'',ugraph2
588 | C.Appl (he::((_::_) as tl)) ->
589 let he',hetype,subst',metasenv',ugraph1 =
590 type_of_aux subst metasenv context he ugraph
592 let tlbody_and_type,subst'',metasenv'',ugraph2 =
593 typeof_list subst' metasenv' context ugraph1 tl
595 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
596 eat_prods true subst'' metasenv'' context
597 he' hetype tlbody_and_type ugraph2
599 let newappl = (C.Appl (coerced_he::coerced_args)) in
600 avoid_double_coercion
601 context subst''' metasenv''' ugraph3 newappl applty
602 | C.Appl _ -> assert false
603 | C.Const (uri,exp_named_subst) ->
604 let exp_named_subst',subst',metasenv',ugraph1 =
605 check_exp_named_subst subst metasenv context
606 exp_named_subst ugraph in
607 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
609 CicSubstitution.subst_vars exp_named_subst' ty_uri
611 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
612 | C.MutInd (uri,i,exp_named_subst) ->
613 let exp_named_subst',subst',metasenv',ugraph1 =
614 check_exp_named_subst subst metasenv context
615 exp_named_subst ugraph
617 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
619 CicSubstitution.subst_vars exp_named_subst' ty_uri in
620 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
621 | C.MutConstruct (uri,i,j,exp_named_subst) ->
622 let exp_named_subst',subst',metasenv',ugraph1 =
623 check_exp_named_subst subst metasenv context
624 exp_named_subst ugraph
627 type_of_mutual_inductive_constr uri i j ugraph1
630 CicSubstitution.subst_vars exp_named_subst' ty_uri
632 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
634 | C.MutCase (uri, i, outtype, term, pl) ->
635 (* first, get the inductive type (and noparams)
636 * in the environment *)
637 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
638 let _ = CicTypeChecker.typecheck uri in
639 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
641 C.InductiveDefinition (l,expl_params,parsno,_) ->
642 List.nth l i , expl_params, parsno, u
644 enrich localization_tbl t
646 (lazy ("Unkown mutual inductive definition " ^
647 U.string_of_uri uri)))
649 let rec count_prod t =
650 match CicReduction.whd ~subst context t with
651 C.Prod (_, _, t) -> 1 + (count_prod t)
654 let no_args = count_prod arity in
655 (* now, create a "generic" MutInd *)
656 let metasenv,left_args =
657 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
659 let metasenv,right_args =
660 let no_right_params = no_args - no_left_params in
661 if no_right_params < 0 then assert false
662 else CicMkImplicit.n_fresh_metas
663 metasenv subst context no_right_params
665 let metasenv,exp_named_subst =
666 CicMkImplicit.fresh_subst metasenv subst context expl_params in
669 C.MutInd (uri,i,exp_named_subst)
672 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
674 (* check consistency with the actual type of term *)
675 let term',actual_type,subst,metasenv,ugraph1 =
676 type_of_aux subst metasenv context term ugraph in
677 let expected_type',_, subst, metasenv,ugraph2 =
678 type_of_aux subst metasenv context expected_type ugraph1
680 let actual_type = CicReduction.whd ~subst context actual_type in
681 let subst,metasenv,ugraph3 =
683 fo_unif_subst subst context metasenv
684 expected_type' actual_type ugraph2
687 enrich localization_tbl term' exn
690 CicMetaSubst.ppterm_in_context subst term'
691 context ^ " has type " ^
692 CicMetaSubst.ppterm_in_context subst actual_type
693 context ^ " but is here used with type " ^
694 CicMetaSubst.ppterm_in_context subst expected_type' context))
696 let rec instantiate_prod t =
700 match CicReduction.whd ~subst context t with
702 instantiate_prod (CicSubstitution.subst he t') tl
705 let arity_instantiated_with_left_args =
706 instantiate_prod arity left_args in
707 (* TODO: check if the sort elimination
708 * is allowed: [(I q1 ... qr)|B] *)
709 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
711 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
713 if left_args = [] then
714 (C.MutConstruct (uri,i,j,exp_named_subst))
717 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
719 let p',actual_type,subst,metasenv,ugraph1 =
720 type_of_aux subst metasenv context p ugraph
722 let constructor',expected_type, subst, metasenv,ugraph2 =
723 type_of_aux subst metasenv context constructor ugraph1
725 let outtypeinstance,subst,metasenv,ugraph3 =
726 check_branch 0 context metasenv subst no_left_params
727 actual_type constructor' expected_type ugraph2
730 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
731 ([],1,[],subst,metasenv,ugraph3) pl
734 (* we are left to check that the outype matches his instances.
735 The easy case is when the outype is specified, that amount
736 to a trivial check. Otherwise, we should guess a type from
740 let outtype,outtypety, subst, metasenv,ugraph4 =
741 type_of_aux subst metasenv context outtype ugraph4 in
744 (let candidate,ugraph5,metasenv,subst =
745 let exp_name_subst, metasenv =
747 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
749 let uris = CicUtil.params_of_obj o in
751 fun uri (acc,metasenv) ->
752 let metasenv',new_meta =
753 CicMkImplicit.mk_implicit metasenv subst context
756 CicMkImplicit.identity_relocation_list_for_metavariable
759 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
763 match left_args,right_args with
764 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
766 let rec mk_right_args =
769 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
771 let right_args_no = List.length right_args in
772 let lifted_left_args =
773 List.map (CicSubstitution.lift right_args_no) left_args
775 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
776 (lifted_left_args @ mk_right_args right_args_no))
779 FreshNamesGenerator.mk_fresh_name ~subst metasenv
780 context Cic.Anonymous ~typ:ty
782 match outtypeinstances with
784 let extended_context =
785 let rec add_right_args =
787 Cic.Prod (name,ty,t) ->
788 Some (name,Cic.Decl ty)::(add_right_args t)
791 (Some (fresh_name,Cic.Decl ty))::
793 (add_right_args arity_instantiated_with_left_args))@
796 let metasenv,new_meta =
797 CicMkImplicit.mk_implicit metasenv subst extended_context
800 CicMkImplicit.identity_relocation_list_for_metavariable
803 let rec add_lambdas b =
805 Cic.Prod (name,ty,t) ->
806 Cic.Lambda (name,ty,(add_lambdas b t))
807 | _ -> Cic.Lambda (fresh_name, ty, b)
810 add_lambdas (Cic.Meta (new_meta,irl))
811 arity_instantiated_with_left_args
813 (Some candidate),ugraph4,metasenv,subst
814 | (constructor_args_no,_,instance,_)::tl ->
816 let instance',subst,metasenv =
817 CicMetaSubst.delift_rels subst metasenv
818 constructor_args_no instance
820 let candidate,ugraph,metasenv,subst =
822 fun (candidate_oty,ugraph,metasenv,subst)
823 (constructor_args_no,_,instance,_) ->
824 match candidate_oty with
825 | None -> None,ugraph,metasenv,subst
828 let instance',subst,metasenv =
829 CicMetaSubst.delift_rels subst metasenv
830 constructor_args_no instance
832 let subst,metasenv,ugraph =
833 fo_unif_subst subst context metasenv
836 candidate_oty,ugraph,metasenv,subst
838 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
839 | CicUnification.UnificationFailure _
840 | CicUnification.Uncertain _ ->
841 None,ugraph,metasenv,subst
842 ) (Some instance',ugraph4,metasenv,subst) tl
845 | None -> None, ugraph,metasenv,subst
847 let rec add_lambdas n b =
849 Cic.Prod (name,ty,t) ->
850 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
852 Cic.Lambda (fresh_name, ty,
853 CicSubstitution.lift (n + 1) t)
856 (add_lambdas 0 t arity_instantiated_with_left_args),
857 ugraph,metasenv,subst
858 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
859 None,ugraph4,metasenv,subst
862 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
864 let subst,metasenv,ugraph =
866 fo_unif_subst subst context metasenv
867 candidate outtype ugraph5
869 exn -> assert false(* unification against a metavariable *)
871 C.MutCase (uri, i, outtype, term', pl'),
872 CicReduction.head_beta_reduce
873 (CicMetaSubst.apply_subst subst
874 (Cic.Appl (outtype::right_args@[term']))),
875 subst,metasenv,ugraph)
876 | _ -> (* easy case *)
877 let tlbody_and_type,subst,metasenv,ugraph4 =
878 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
880 let _,_,_,subst,metasenv,ugraph4 =
881 eat_prods false subst metasenv context
882 outtype outtypety tlbody_and_type ugraph4
884 let _,_, subst, metasenv,ugraph5 =
885 type_of_aux subst metasenv context
886 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
888 let (subst,metasenv,ugraph6) =
890 (fun (subst,metasenv,ugraph)
891 p (constructor_args_no,context,instance,args)
896 CicSubstitution.lift constructor_args_no outtype
898 C.Appl (outtype'::args)
900 CicReduction.whd ~subst context appl
903 fo_unif_subst subst context metasenv instance instance'
907 enrich localization_tbl p exn
910 CicMetaSubst.ppterm_in_context subst p
911 context ^ " has type " ^
912 CicMetaSubst.ppterm_in_context subst instance'
913 context ^ " but is here used with type " ^
914 CicMetaSubst.ppterm_in_context subst instance
916 (subst,metasenv,ugraph5) pl' outtypeinstances
918 C.MutCase (uri, i, outtype, term', pl'),
919 CicReduction.head_beta_reduce
920 (CicMetaSubst.apply_subst subst
921 (C.Appl(outtype::right_args@[term]))),
922 subst,metasenv,ugraph6)
924 let fl_ty',subst,metasenv,types,ugraph1 =
926 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
927 let ty',_,subst',metasenv',ugraph1 =
928 type_of_aux subst metasenv context ty ugraph
930 fl @ [ty'],subst',metasenv',
931 Some (C.Name n,(C.Decl ty')) :: types, ugraph
932 ) ([],subst,metasenv,[],ugraph) fl
934 let len = List.length types in
935 let context' = types@context in
936 let fl_bo',subst,metasenv,ugraph2 =
938 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
939 let bo',ty_of_bo,subst,metasenv,ugraph1 =
940 type_of_aux subst metasenv context' bo ugraph in
941 let expected_ty = CicSubstitution.lift len ty in
942 let subst',metasenv',ugraph' =
944 fo_unif_subst subst context' metasenv
945 ty_of_bo expected_ty ugraph1
948 enrich localization_tbl bo exn
951 CicMetaSubst.ppterm_in_context subst bo
952 context' ^ " has type " ^
953 CicMetaSubst.ppterm_in_context subst ty_of_bo
954 context' ^ " but is here used with type " ^
955 CicMetaSubst.ppterm_in_context subst expected_ty
958 fl @ [bo'] , subst',metasenv',ugraph'
959 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
961 let ty = List.nth fl_ty' i in
962 (* now we have the new ty in fl_ty', the new bo in fl_bo',
963 * and we want the new fl with bo' and ty' injected in the right
966 let rec map3 f l1 l2 l3 =
969 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
972 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
975 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
977 let fl_ty',subst,metasenv,types,ugraph1 =
979 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
980 let ty',_,subst',metasenv',ugraph1 =
981 type_of_aux subst metasenv context ty ugraph
983 fl @ [ty'],subst',metasenv',
984 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
985 ) ([],subst,metasenv,[],ugraph) fl
987 let len = List.length types in
988 let context' = types@context in
989 let fl_bo',subst,metasenv,ugraph2 =
991 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
992 let bo',ty_of_bo,subst,metasenv,ugraph1 =
993 type_of_aux subst metasenv context' bo ugraph in
994 let expected_ty = CicSubstitution.lift len ty in
995 let subst',metasenv',ugraph' =
997 fo_unif_subst subst context' metasenv
998 ty_of_bo expected_ty ugraph1
1001 enrich localization_tbl bo exn
1004 CicMetaSubst.ppterm_in_context subst bo
1005 context' ^ " has type " ^
1006 CicMetaSubst.ppterm_in_context subst ty_of_bo
1007 context' ^ " but is here used with type " ^
1008 CicMetaSubst.ppterm_in_context subst expected_ty
1011 fl @ [bo'],subst',metasenv',ugraph'
1012 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
1014 let ty = List.nth fl_ty' i in
1015 (* now we have the new ty in fl_ty', the new bo in fl_bo',
1016 * and we want the new fl with bo' and ty' injected in the right
1019 let rec map3 f l1 l2 l3 =
1022 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
1025 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
1028 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
1030 relocalize localization_tbl t t';
1033 (* check_metasenv_consistency checks that the "canonical" context of a
1034 metavariable is consitent - up to relocation via the relocation list l -
1035 with the actual context *)
1036 and check_metasenv_consistency
1037 metano subst metasenv context canonical_context l ugraph
1039 let module C = Cic in
1040 let module R = CicReduction in
1041 let module S = CicSubstitution in
1042 let lifted_canonical_context =
1046 | (Some (n,C.Decl t))::tl ->
1047 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
1048 | (Some (n,C.Def (t,None)))::tl ->
1049 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1050 | None::tl -> None::(aux (i+1) tl)
1051 | (Some (n,C.Def (t,Some ty)))::tl ->
1053 C.Def ((S.subst_meta l (S.lift i t)),
1054 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
1056 aux 1 canonical_context
1060 (fun (l,subst,metasenv,ugraph) t ct ->
1063 l @ [None],subst,metasenv,ugraph
1064 | Some t,Some (_,C.Def (ct,_)) ->
1065 let subst',metasenv',ugraph' =
1067 prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
1068 fo_unif_subst subst context metasenv t ct ugraph
1069 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))))))
1071 l @ [Some t],subst',metasenv',ugraph'
1072 | Some t,Some (_,C.Decl ct) ->
1073 let t',inferredty,subst',metasenv',ugraph1 =
1074 type_of_aux subst metasenv context t ugraph
1076 let subst'',metasenv'',ugraph2 =
1079 subst' context metasenv' inferredty ct ugraph1
1080 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))))))
1082 l @ [Some t'], subst'',metasenv'',ugraph2
1084 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
1086 Invalid_argument _ ->
1090 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1091 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
1092 (CicMetaSubst.ppcontext subst canonical_context))))
1094 and check_exp_named_subst metasubst metasenv context tl ugraph =
1095 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1097 [] -> [],metasubst,metasenv,ugraph
1099 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1101 CicSubstitution.subst_vars substs ty_uri in
1102 (* CSC: why was this code here? it is wrong
1103 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1104 Cic.Variable (_,Some bo,_,_) ->
1106 (RefineFailure (lazy
1107 "A variable with a body can not be explicit substituted"))
1108 | Cic.Variable (_,None,_,_) -> ()
1111 (RefineFailure (lazy
1112 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1115 let t',typeoft,metasubst',metasenv',ugraph2 =
1116 type_of_aux metasubst metasenv context t ugraph1 in
1117 let subst = uri,t' in
1118 let metasubst'',metasenv'',ugraph3 =
1121 metasubst' context metasenv' typeoft typeofvar ugraph2
1123 raise (RefineFailure (lazy
1124 ("Wrong Explicit Named Substitution: " ^
1125 CicMetaSubst.ppterm metasubst' typeoft ^
1126 " not unifiable with " ^
1127 CicMetaSubst.ppterm metasubst' typeofvar)))
1129 (* FIXME: no mere tail recursive! *)
1130 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1131 check_exp_named_subst_aux
1132 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1134 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1136 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1139 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1142 let module C = Cic in
1143 let context_for_t2 = (Some (name,C.Decl s))::context in
1144 let t1'' = CicReduction.whd ~subst context t1 in
1145 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1146 match (t1'', t2'') with
1147 (C.Sort s1, C.Sort s2)
1148 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1149 (* different than Coq manual!!! *)
1150 C.Sort s2,subst,metasenv,ugraph
1151 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1152 let t' = CicUniv.fresh() in
1154 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1155 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1156 C.Sort (C.Type t'),subst,metasenv,ugraph2
1158 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1159 | (C.Sort _,C.Sort (C.Type t1)) ->
1160 C.Sort (C.Type t1),subst,metasenv,ugraph
1161 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1162 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1163 (* TODO how can we force the meta to become a sort? If we don't we
1164 * break the invariant that refine produce only well typed terms *)
1165 (* TODO if we check the non meta term and if it is a sort then we
1166 * are likely to know the exact value of the result e.g. if the rhs
1167 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1168 let (metasenv,idx) =
1169 CicMkImplicit.mk_implicit_sort metasenv subst in
1170 let (subst, metasenv,ugraph1) =
1172 fo_unif_subst subst context_for_t2 metasenv
1173 (C.Meta (idx,[])) t2'' ugraph
1174 with _ -> assert false (* unification against a metavariable *)
1176 t2'',subst,metasenv,ugraph1
1179 enrich localization_tbl s
1183 "%s is supposed to be a type, but its type is %s"
1184 (CicMetaSubst.ppterm_in_context subst t context)
1185 (CicMetaSubst.ppterm_in_context subst t2 context))))
1187 enrich localization_tbl t
1191 "%s is supposed to be a type, but its type is %s"
1192 (CicMetaSubst.ppterm_in_context subst s context)
1193 (CicMetaSubst.ppterm_in_context subst t1 context))))
1195 and avoid_double_coercion context subst metasenv ugraph t ty =
1196 if not !pack_coercions then
1197 t,ty,subst,metasenv,ugraph
1199 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1201 let source_carr = CoercGraph.source_of c2 in
1202 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1203 (match CoercGraph.look_for_coercion source_carr tgt_carr
1205 | CoercGraph.SomeCoercion candidates ->
1207 HExtlib.list_findopt
1209 | c when not (CoercGraph.is_composite c) ->
1210 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1215 | Cic.Appl l -> Cic.Appl (l @ [head])
1216 | _ -> Cic.Appl [c;head]
1218 debug_print (lazy ("\nprovo" ^ CicPp.ppterm newt));
1223 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
1224 let newt,_,subst,metasenv,ugraph =
1225 type_of_aux subst metasenv context newt ugraph in
1226 debug_print (lazy "tipa...");
1227 let subst, metasenv, ugraph =
1228 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1229 fo_unif_subst subst context metasenv newt t ugraph
1231 debug_print (lazy "unifica...");
1232 Some (newt, ty, subst, metasenv, ugraph)
1234 | RefineFailure s | Uncertain s when not !pack_coercions->
1235 debug_print s; debug_print (lazy "stop\n");None
1236 | RefineFailure s | Uncertain s ->
1237 debug_print s;debug_print (lazy "goon\n");
1239 let old_pack_coercions = !pack_coercions in
1240 pack_coercions := false; (* to avoid diverging *)
1241 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1242 type_of_aux subst metasenv context c1_c2_implicit ugraph
1244 pack_coercions := old_pack_coercions;
1246 is_a_double_coercion refined_c1_c2_implicit
1252 match refined_c1_c2_implicit with
1253 | Cic.Appl l -> HExtlib.list_last l
1256 let subst, metasenv, ugraph =
1257 try fo_unif_subst subst context metasenv
1259 with RefineFailure s| Uncertain s->
1260 debug_print s;assert false
1262 let subst, metasenv, ugraph =
1263 fo_unif_subst subst context metasenv
1264 refined_c1_c2_implicit t ugraph
1266 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1268 | RefineFailure s | Uncertain s ->
1269 pack_coercions := true;debug_print s;None
1270 | exn -> pack_coercions := true; raise exn))
1273 (match selected with
1277 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1278 t, ty, subst, metasenv, ugraph)
1279 | _ -> t, ty, subst, metasenv, ugraph)
1281 t, ty, subst, metasenv, ugraph
1283 and typeof_list subst metasenv context ugraph l =
1284 let tlbody_and_type,subst,metasenv,ugraph =
1286 (fun x (res,subst,metasenv,ugraph) ->
1287 let x',ty,subst',metasenv',ugraph1 =
1288 type_of_aux subst metasenv context x ugraph
1290 (x', ty)::res,subst',metasenv',ugraph1
1291 ) l ([],subst,metasenv,ugraph)
1293 tlbody_and_type,subst,metasenv,ugraph
1296 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1298 (* aux function to add coercions to funclass *)
1299 let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph =
1301 let pristinemenv = metasenv in
1302 let metasenv,hetype' =
1303 mk_prod_of_metas metasenv context subst args_bo_and_ty
1306 let subst,metasenv,ugraph =
1307 fo_unif_subst_eat_prods
1308 subst context metasenv hetype hetype' ugraph
1310 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1311 with RefineFailure s | Uncertain s as exn
1312 when allow_coercions && !insert_coercions ->
1313 (* {{{ we search a coercion of the head (saturated) to funclass *)
1314 let metasenv = pristinemenv in
1316 ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^
1317 " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype'
1318 (* ^ " cause: " ^ Lazy.force s *)));
1319 let how_many_args_are_needed =
1320 let rec aux n = function
1321 | Cic.Prod(_,_,t) -> aux (n+1) t
1324 aux 0 (CicMetaSubst.apply_subst subst hetype)
1326 let args, remainder =
1327 HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
1329 let args = List.map fst args in
1333 | Cic.Appl l -> Cic.Appl (l@args)
1334 | _ -> Cic.Appl (he::args)
1338 let x,xty,subst,metasenv,ugraph =
1339 type_of_aux subst metasenv context x ugraph
1342 CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty)
1344 let carr_tgt = CoercDb.Fun 0 in
1345 match CoercGraph.look_for_coercion' carr_src carr_tgt with
1346 | CoercGraph.NoCoercion
1347 | CoercGraph.NotMetaClosed
1348 | CoercGraph.NotHandled _ -> raise exn
1349 | CoercGraph.SomeCoercion candidates ->
1351 HExtlib.list_findopt
1353 let t = Cic.Appl [coerc;x] in
1354 debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t));
1356 (* we want this to be available in the error handler fo the
1357 * following (so it has its own try. *)
1358 let t,tty,subst,metasenv,ugraph =
1359 type_of_aux subst metasenv context t ugraph
1362 let metasenv, hetype' =
1363 mk_prod_of_metas metasenv context subst remainder
1366 (" unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^
1367 CicMetaSubst.ppterm subst hetype'));
1368 let subst,metasenv,ugraph =
1369 fo_unif_subst_eat_prods
1370 subst context metasenv tty hetype' ugraph
1372 debug_print (lazy " success!");
1373 Some (subst,metasenv,ugraph,tty,t,remainder)
1375 | Uncertain _ | RefineFailure _
1376 | CicUnification.UnificationFailure _
1377 | CicUnification.Uncertain _ ->
1379 let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
1381 metasenv context subst t tty remainder ugraph
1383 Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
1384 with Uncertain _ | RefineFailure _ -> None
1385 with Uncertain _ | RefineFailure _ -> None)
1388 | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
1389 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1391 more_args_than_expected localization_tbl
1392 subst he context hetype args_bo_and_ty exn
1393 (* }}} end coercion to funclass stuff *)
1394 (* }}} end fix_arity *)
1396 (* aux function to process the type of the head and the args in parallel *)
1397 let rec eat_prods_and_args
1398 pristinemenv metasenv subst context pristinehe he hetype ugraph newargs
1402 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1403 | (hete, hety)::tl ->
1404 match (CicReduction.whd ~subst context hetype) with
1405 | Cic.Prod (n,s,t) ->
1406 let arg,subst,metasenv,ugraph1 =
1408 let subst,metasenv,ugraph1 =
1409 fo_unif_subst_eat_prods2
1410 subst context metasenv hety s ugraph
1412 (hete,hety),subst,metasenv,ugraph1
1413 (* {{{ we search a coercion from hety to s if fails *)
1414 with RefineFailure _ | Uncertain _ as exn
1415 when allow_coercions && !insert_coercions ->
1416 let coer, tgt_carr =
1417 let carr t subst context =
1418 CicReduction.whd ~delta:false
1419 context (CicMetaSubst.apply_subst subst t )
1421 let c_hety = carr hety subst context in
1422 let c_s = carr s subst context in
1423 CoercGraph.look_for_coercion c_hety c_s, c_s
1426 | CoercGraph.NoCoercion
1427 | CoercGraph.NotHandled _ ->
1428 enrich localization_tbl hete exn
1430 (lazy ("The term " ^
1431 CicMetaSubst.ppterm_in_context subst hete
1432 context ^ " has type " ^
1433 CicMetaSubst.ppterm_in_context subst hety
1434 context ^ " but is here used with type " ^
1435 CicMetaSubst.ppterm_in_context subst s context
1436 (* "\nReason: " ^ Lazy.force e*))))
1437 | CoercGraph.NotMetaClosed ->
1438 enrich localization_tbl hete exn
1440 (lazy ("The term " ^
1441 CicMetaSubst.ppterm_in_context subst hete
1442 context ^ " has type " ^
1443 CicMetaSubst.ppterm_in_context subst hety
1444 context ^ " but is here used with type " ^
1445 CicMetaSubst.ppterm_in_context subst s context
1446 (* "\nReason: " ^ Lazy.force e*))))
1447 | CoercGraph.SomeCoercion candidates ->
1449 HExtlib.list_findopt
1452 let t = Cic.Appl[c;hete] in
1453 let newt,newhety,subst,metasenv,ugraph =
1454 type_of_aux subst metasenv context
1457 let newt, newty, subst, metasenv, ugraph =
1458 avoid_double_coercion context subst metasenv
1459 ugraph newt tgt_carr
1461 let subst,metasenv,ugraph1 =
1462 fo_unif_subst subst context metasenv
1465 Some ((newt,newty), subst, metasenv, ugraph)
1466 with Uncertain _ | RefineFailure _ -> None)
1469 (match selected with
1472 enrich localization_tbl hete
1474 (lazy ("The term " ^
1475 CicMetaSubst.ppterm_in_context subst hete
1476 context ^ " has type " ^
1477 CicMetaSubst.ppterm_in_context subst hety
1478 context ^ " but is here used with type " ^
1479 CicMetaSubst.ppterm_in_context subst s context
1480 (* "\nReason: " ^ Lazy.force e*)))) exn))
1482 enrich localization_tbl hete
1484 (lazy ("The term " ^
1485 CicMetaSubst.ppterm_in_context subst hete
1486 context ^ " has type " ^
1487 CicMetaSubst.ppterm_in_context subst hety
1488 context ^ " but is here used with type " ^
1489 CicMetaSubst.ppterm_in_context subst s context
1490 (* "\nReason: " ^ Printexc.to_string exn*)))) exn
1491 (* }}} end coercion stuff *)
1493 eat_prods_and_args pristinemenv metasenv subst context pristinehe he
1494 (CicSubstitution.subst (fst arg) t)
1495 ugraph1 (newargs@[arg]) tl
1498 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1500 pristinemenv context subst he hetype
1501 (newargs@[hete,hety]@tl) ugraph
1503 eat_prods_and_args metasenv
1504 metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
1505 with RefineFailure _ | Uncertain _ as exn ->
1506 (* unable to fix arity *)
1507 more_args_than_expected localization_tbl
1508 subst he context hetype args_bo_and_ty exn
1511 (* first we check if we are in the simple case of a meta closed term *)
1512 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1513 if CicUtil.is_meta_closed hetype then
1514 (* this optimization is to postpone fix_arity (the most common case)*)
1515 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1517 (* this (says CSC) is also useful to infer dependent types *)
1519 fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
1520 with RefineFailure _ | Uncertain _ as exn ->
1521 (* unable to fix arity *)
1522 more_args_than_expected localization_tbl
1523 subst he context hetype args_bo_and_ty exn
1525 let coerced_args,subst,metasenv,he,t,ugraph =
1527 metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
1529 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1532 (* eat prods ends here! *)
1534 let t',ty,subst',metasenv',ugraph1 =
1535 type_of_aux [] metasenv context t ugraph
1537 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1538 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1539 (* Andrea: ho rimesso qui l'applicazione della subst al
1540 metasenv dopo che ho droppato l'invariante che il metsaenv
1541 e' sempre istanziato *)
1542 let substituted_metasenv =
1543 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1545 (* substituted_t,substituted_ty,substituted_metasenv *)
1546 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1548 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1550 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1551 let cleaned_metasenv =
1553 (function (n,context,ty) ->
1554 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1559 | Some (n, Cic.Decl t) ->
1561 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1562 | Some (n, Cic.Def (bo,ty)) ->
1563 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1568 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1570 Some (n, Cic.Def (bo',ty'))
1574 ) substituted_metasenv
1576 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1579 let undebrujin uri typesno tys t =
1582 (fun (name,_,_,_) (i,t) ->
1583 (* here the explicit_named_substituion is assumed to be *)
1585 let t' = Cic.MutInd (uri,i,[]) in
1586 let t = CicSubstitution.subst t' t in
1588 ) tys (typesno - 1,t))
1590 let map_first_n n start f g l =
1591 let rec aux acc k l =
1594 | [] -> raise (Invalid_argument "map_first_n")
1595 | hd :: tl -> f hd k (aux acc (k+1) tl)
1601 (*CSC: this is a very rough approximation; to be finished *)
1602 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1603 let subst,metasenv,ugraph,tys =
1605 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1606 let subst,metasenv,ugraph,cl =
1608 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1609 let rec aux ctx k subst = function
1610 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1611 let subst,metasenv,ugraph,tl =
1613 (subst,metasenv,ugraph,[])
1614 (fun t n (subst,metasenv,ugraph,acc) ->
1615 let subst,metasenv,ugraph =
1617 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1619 subst,metasenv,ugraph,(t::acc))
1620 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1623 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1624 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1625 subst,metasenv,ugraph,t
1626 | Cic.Prod (name,s,t) ->
1627 let ctx = (Some (name,Cic.Decl s))::ctx in
1628 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1629 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1633 (lazy "not well formed constructor type"))
1635 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1636 subst,metasenv,ugraph,(name,ty) :: acc)
1637 cl (subst,metasenv,ugraph,[])
1639 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1640 tys ([],metasenv,ugraph,[])
1642 let substituted_tys =
1644 (fun (name,ind,arity,cl) ->
1646 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1648 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1651 metasenv,ugraph,substituted_tys
1653 let typecheck metasenv uri obj ~localization_tbl =
1654 let ugraph = CicUniv.empty_ugraph in
1656 Cic.Constant (name,Some bo,ty,args,attrs) ->
1657 let bo',boty,metasenv,ugraph =
1658 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1659 let ty',_,metasenv,ugraph =
1660 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1661 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1662 let bo' = CicMetaSubst.apply_subst subst bo' in
1663 let ty' = CicMetaSubst.apply_subst subst ty' in
1664 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1665 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1666 | Cic.Constant (name,None,ty,args,attrs) ->
1667 let ty',_,metasenv,ugraph =
1668 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1670 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1671 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1672 assert (metasenv' = metasenv);
1673 (* Here we do not check the metasenv for correctness *)
1674 let bo',boty,metasenv,ugraph =
1675 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1676 let ty',sort,metasenv,ugraph =
1677 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1681 (* instead of raising Uncertain, let's hope that the meta will become
1684 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
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.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1691 | Cic.Variable _ -> assert false (* not implemented *)
1692 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1693 (*CSC: this code is greately simplified and many many checks are missing *)
1694 (*CSC: e.g. the constructors are not required to build their own types, *)
1695 (*CSC: the arities are not required to have as type a sort, etc. *)
1696 let uri = match uri with Some uri -> uri | None -> assert false in
1697 let typesno = List.length tys in
1698 (* first phase: we fix only the types *)
1699 let metasenv,ugraph,tys =
1701 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1702 let ty',_,metasenv,ugraph =
1703 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1705 metasenv,ugraph,(name,b,ty',cl)::res
1706 ) tys (metasenv,ugraph,[]) in
1708 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1709 (* second phase: we fix only the constructors *)
1710 let metasenv,ugraph,tys =
1712 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1713 let metasenv,ugraph,cl' =
1715 (fun (name,ty) (metasenv,ugraph,res) ->
1717 CicTypeChecker.debrujin_constructor
1718 ~cb:(relocalize localization_tbl) uri typesno ty in
1719 let ty',_,metasenv,ugraph =
1720 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1721 let ty' = undebrujin uri typesno tys ty' in
1722 metasenv,ugraph,(name,ty')::res
1723 ) cl (metasenv,ugraph,[])
1725 metasenv,ugraph,(name,b,ty,cl')::res
1726 ) tys (metasenv,ugraph,[]) in
1727 (* third phase: we check the positivity condition *)
1728 let metasenv,ugraph,tys =
1729 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1731 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1734 (* sara' piu' veloce che raffinare da zero? mah.... *)
1735 let pack_coercion metasenv ctx t =
1736 let module C = Cic in
1737 let rec merge_coercions ctx =
1738 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1740 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1741 | C.Meta (n,subst) ->
1744 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1747 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1748 | C.Prod (name,so,dest) ->
1749 let ctx' = (Some (name,C.Decl so))::ctx in
1750 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1751 | C.Lambda (name,so,dest) ->
1752 let ctx' = (Some (name,C.Decl so))::ctx in
1753 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1754 | C.LetIn (name,so,dest) ->
1755 let _,ty,metasenv,ugraph =
1756 pack_coercions := false;
1757 type_of_aux' metasenv ctx so CicUniv.empty_ugraph in
1758 pack_coercions := true;
1759 let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1760 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1762 let l = List.map (merge_coercions ctx) l in
1764 let b,_,_,_,_ = is_a_double_coercion t in
1765 (* prerr_endline "CANDIDATO!!!!"; *)
1767 let ugraph = CicUniv.empty_ugraph in
1768 let old_insert_coercions = !insert_coercions in
1769 insert_coercions := false;
1770 let newt, _, menv, _ =
1772 type_of_aux' metasenv ctx t ugraph
1773 with RefineFailure _ | Uncertain _ ->
1776 insert_coercions := old_insert_coercions;
1777 if metasenv <> [] || menv = [] then
1780 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1783 | C.Var (uri,exp_named_subst) ->
1784 let exp_named_subst = List.map aux exp_named_subst in
1785 C.Var (uri, exp_named_subst)
1786 | C.Const (uri,exp_named_subst) ->
1787 let exp_named_subst = List.map aux exp_named_subst in
1788 C.Const (uri, exp_named_subst)
1789 | C.MutInd (uri,tyno,exp_named_subst) ->
1790 let exp_named_subst = List.map aux exp_named_subst in
1791 C.MutInd (uri,tyno,exp_named_subst)
1792 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1793 let exp_named_subst = List.map aux exp_named_subst in
1794 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1795 | C.MutCase (uri,tyno,out,te,pl) ->
1796 let pl = List.map (merge_coercions ctx) pl in
1797 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1798 | C.Fix (fno, fl) ->
1801 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1806 (fun (name,idx,ty,bo) ->
1807 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1811 | C.CoFix (fno, fl) ->
1814 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1819 (fun (name,ty,bo) ->
1820 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1825 merge_coercions ctx t
1828 let pack_coercion_metasenv conjectures =
1829 let module C = Cic in
1831 (fun (i, ctx, ty) ->
1837 Some (name, C.Decl t) ->
1838 Some (name, C.Decl (pack_coercion conjectures ctx t))
1839 | Some (name, C.Def (t,None)) ->
1840 Some (name,C.Def (pack_coercion conjectures ctx t,None))
1841 | Some (name, C.Def (t,Some ty)) ->
1842 Some (name, C.Def (pack_coercion conjectures ctx t,
1843 Some (pack_coercion conjectures ctx ty)))
1849 ((i,ctx,pack_coercion conjectures ctx ty))
1853 let pack_coercion_obj obj =
1854 let module C = Cic in
1856 | C.Constant (id, body, ty, params, attrs) ->
1860 | Some body -> Some (pack_coercion [] [] body)
1862 let ty = pack_coercion [] [] ty in
1863 C.Constant (id, body, ty, params, attrs)
1864 | C.Variable (name, body, ty, params, attrs) ->
1868 | Some body -> Some (pack_coercion [] [] body)
1870 let ty = pack_coercion [] [] ty in
1871 C.Variable (name, body, ty, params, attrs)
1872 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1873 let conjectures = pack_coercion_metasenv conjectures in
1874 let body = pack_coercion conjectures [] body in
1875 let ty = pack_coercion conjectures [] ty in
1876 C.CurrentProof (name, conjectures, body, ty, params, attrs)
1877 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1880 (fun (name, ind, arity, cl) ->
1881 let arity = pack_coercion [] [] arity in
1883 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
1885 (name, ind, arity, cl))
1888 C.InductiveDefinition (indtys, params, leftno, attrs)
1893 let type_of_aux' metasenv context term =
1896 type_of_aux' metasenv context term in
1898 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1900 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1903 | RefineFailure msg as e ->
1904 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1906 | Uncertain msg as e ->
1907 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1911 let profiler2 = HExtlib.profile "CicRefine"
1913 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1914 profiler2.HExtlib.profile
1915 (type_of_aux' ?localization_tbl metasenv context term) ugraph
1917 let typecheck ~localization_tbl metasenv uri obj =
1918 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
1920 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
1921 (* vim:set foldmethod=marker: *)