1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
30 exception RefineFailure of string Lazy.t;;
31 exception Uncertain of string Lazy.t;;
32 exception AssertFailure of string Lazy.t;;
34 let insert_coercions = ref true
35 let pack_coercions = ref true
37 let debug_print = fun _ -> ();;
38 (*let debug_print x = prerr_endline (Lazy.force x);;*)
40 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
42 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
45 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
46 in profiler_eat_prods2.HExtlib.profile foo ()
48 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
49 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
52 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
54 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
57 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
58 in profiler_eat_prods.HExtlib.profile foo ()
60 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
61 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
64 let profiler = HExtlib.profile "CicRefine.fo_unif"
66 let fo_unif_subst subst context metasenv t1 t2 ugraph =
69 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
70 in profiler.HExtlib.profile foo ()
72 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
73 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
76 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
79 RefineFailure msg -> RefineFailure (f msg)
80 | Uncertain msg -> Uncertain (f msg)
81 | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
82 | Sys.Break -> raise exn
83 | _ -> prerr_endline (Printexc.to_string exn); assert false
87 Cic.CicHash.find localization_tbl t
89 prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
92 raise (HExtlib.Localized (loc,exn'))
94 let relocalize localization_tbl oldt newt =
96 let infos = Cic.CicHash.find localization_tbl oldt in
97 Cic.CicHash.remove localization_tbl oldt;
98 Cic.CicHash.add localization_tbl newt infos;
106 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
107 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
110 let exp_impl metasenv subst context =
113 let (metasenv', idx) =
114 CicMkImplicit.mk_implicit_type metasenv subst context in
116 CicMkImplicit.identity_relocation_list_for_metavariable context in
117 metasenv', Cic.Meta (idx, irl)
119 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
120 metasenv', Cic.Meta (idx, [])
122 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
124 CicMkImplicit.identity_relocation_list_for_metavariable context in
125 metasenv', Cic.Meta (idx, irl)
129 let is_a_double_coercion t =
131 let rec aux acc = function
133 | x::tl -> aux (acc@[x]) tl
138 let imp = Cic.Implicit None in
139 let dummyres = false,imp, imp,imp,imp in
141 | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
142 (match last_of tl with
143 | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
144 let sib2,head = last_of tl2 in
145 true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
150 let more_args_than_expected
151 localization_tbl metasenv subst he context hetype' tlbody_and_type exn
155 CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
156 " (that has type "^CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
157 ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
158 " arguments that are more than expected")
160 enrich localization_tbl he ~f:(fun _-> msg) exn
163 let mk_prod_of_metas metasenv context' subst args =
164 let rec mk_prod metasenv context' = function
166 let (metasenv, idx) =
167 CicMkImplicit.mk_implicit_type metasenv subst context'
170 CicMkImplicit.identity_relocation_list_for_metavariable context'
172 metasenv,Cic.Meta (idx, irl)
174 let (metasenv, idx) =
175 CicMkImplicit.mk_implicit_type metasenv subst context'
178 CicMkImplicit.identity_relocation_list_for_metavariable context'
180 let meta = Cic.Meta (idx,irl) in
182 (* The name must be fresh for context. *)
183 (* Nevertheless, argty is well-typed only in context. *)
184 (* Thus I generate a name (name_hint) in context and *)
185 (* then I generate a name --- using the hint name_hint *)
186 (* --- that is fresh in context'. *)
188 (* Cic.Name "pippo" *)
189 FreshNamesGenerator.mk_fresh_name ~subst metasenv
190 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
191 (CicMetaSubst.apply_subst_context subst context')
193 ~typ:(CicMetaSubst.apply_subst subst argty)
195 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
196 FreshNamesGenerator.mk_fresh_name ~subst
197 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
199 let metasenv,target =
200 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
202 metasenv,Cic.Prod (name,meta,target)
204 mk_prod metasenv context' args
207 let rec type_of_constant uri ugraph =
208 let module C = Cic in
209 let module R = CicReduction in
210 let module U = UriManager in
211 let _ = CicTypeChecker.typecheck uri in
214 CicEnvironment.get_cooked_obj ugraph uri
215 with Not_found -> assert false
218 C.Constant (_,_,ty,_,_) -> ty,u
219 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
223 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
225 and type_of_variable uri ugraph =
226 let module C = Cic in
227 let module R = CicReduction in
228 let module U = UriManager in
229 let _ = CicTypeChecker.typecheck uri in
232 CicEnvironment.get_cooked_obj ugraph uri
233 with Not_found -> assert false
236 C.Variable (_,_,ty,_,_) -> ty,u
240 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
242 and type_of_mutual_inductive_defs uri i ugraph =
243 let module C = Cic in
244 let module R = CicReduction in
245 let module U = UriManager in
246 let _ = CicTypeChecker.typecheck uri in
249 CicEnvironment.get_cooked_obj ugraph uri
250 with Not_found -> assert false
253 C.InductiveDefinition (dl,_,_,_) ->
254 let (_,_,arity,_) = List.nth dl i in
259 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
261 and type_of_mutual_inductive_constr uri i j ugraph =
262 let module C = Cic in
263 let module R = CicReduction in
264 let module U = UriManager in
265 let _ = CicTypeChecker.typecheck uri in
268 CicEnvironment.get_cooked_obj ugraph uri
269 with Not_found -> assert false
272 C.InductiveDefinition (dl,_,_,_) ->
273 let (_,_,_,cl) = List.nth dl i in
274 let (_,ty) = List.nth cl (j-1) in
280 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
283 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
285 (* the check_branch function checks if a branch of a case is refinable.
286 It returns a pair (outype_instance,args), a subst and a metasenv.
287 outype_instance is the expected result of applying the case outtype
289 The problem is that outype is in general unknown, and we should
290 try to synthesize it from the above information, that is in general
291 a second order unification problem. *)
293 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
294 let module C = Cic in
295 (* let module R = CicMetaSubst in *)
296 let module R = CicReduction in
297 match R.whd ~subst context expectedtype with
299 (n,context,actualtype, [term]), subst, metasenv, ugraph
300 | C.Appl (C.MutInd (_,_,_)::tl) ->
301 let (_,arguments) = split tl left_args_no in
302 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
303 | C.Prod (name,so,de) ->
304 (* we expect that the actual type of the branch has the due
306 (match R.whd ~subst context actualtype with
307 C.Prod (name',so',de') ->
308 let subst, metasenv, ugraph1 =
309 fo_unif_subst subst context metasenv so so' ugraph in
311 (match CicSubstitution.lift 1 term with
312 C.Appl l -> C.Appl (l@[C.Rel 1])
313 | t -> C.Appl [t ; C.Rel 1]) in
314 (* we should also check that the name variable is anonymous in
315 the actual type de' ?? *)
317 ((Some (name,(C.Decl so)))::context)
318 metasenv subst left_args_no de' term' de ugraph1
319 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
320 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
322 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
325 let rec type_of_aux subst metasenv context t ugraph =
326 let module C = Cic in
327 let module S = CicSubstitution in
328 let module U = UriManager in
330 let try_coercion t subst context ugraph coercion_tgt (metasenv,last,coerced) =
331 let subst,metasenv,ugraph =
332 fo_unif_subst subst context metasenv last t ugraph
335 let newt, tty, subst, metasenv, ugraph =
336 avoid_double_coercion context subst metasenv ugraph coerced
339 Some (newt, tty, subst, metasenv, ugraph)
341 | RefineFailure _ | Uncertain _ -> None
344 let (t',_,_,_,_) as res =
349 match List.nth context (n - 1) with
350 Some (_,C.Decl ty) ->
351 t,S.lift n ty,subst,metasenv, ugraph
352 | Some (_,C.Def (_,Some ty)) ->
353 t,S.lift n ty,subst,metasenv, ugraph
354 | Some (_,C.Def (bo,None)) ->
356 (* if it is in the context it must be already well-typed*)
357 CicTypeChecker.type_of_aux' ~subst metasenv context
360 t,ty,subst,metasenv,ugraph
362 enrich localization_tbl t
363 (RefineFailure (lazy "Rel to hidden hypothesis"))
366 enrich localization_tbl t
367 (RefineFailure (lazy "Not a closed term")))
368 | C.Var (uri,exp_named_subst) ->
369 let exp_named_subst',subst',metasenv',ugraph1 =
370 check_exp_named_subst
371 subst metasenv context exp_named_subst ugraph
373 let ty_uri,ugraph1 = type_of_variable uri ugraph in
375 CicSubstitution.subst_vars exp_named_subst' ty_uri
377 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
380 let (canonical_context, term,ty) =
381 CicUtil.lookup_subst n subst
383 let l',subst',metasenv',ugraph1 =
384 check_metasenv_consistency n subst metasenv context
385 canonical_context l ugraph
387 (* trust or check ??? *)
388 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
389 subst', metasenv', ugraph1
390 (* type_of_aux subst metasenv
391 context (CicSubstitution.subst_meta l term) *)
392 with CicUtil.Subst_not_found _ ->
393 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
394 let l',subst',metasenv', ugraph1 =
395 check_metasenv_consistency n subst metasenv context
396 canonical_context l ugraph
398 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
399 subst', metasenv',ugraph1)
400 | C.Sort (C.Type tno) ->
401 let tno' = CicUniv.fresh() in
403 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
404 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
406 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
408 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
409 | C.Implicit infos ->
410 let metasenv',t' = exp_impl metasenv subst context infos in
411 type_of_aux subst metasenv' context t' ugraph
413 let ty',_,subst',metasenv',ugraph1 =
414 type_of_aux subst metasenv context ty ugraph
416 let te',inferredty,subst'',metasenv'',ugraph2 =
417 type_of_aux subst' metasenv' context te ugraph1
420 let subst''',metasenv''',ugraph3 =
421 fo_unif_subst subst'' context metasenv''
422 inferredty ty' ugraph2
424 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
426 | Uncertain _ | RefineFailure _ ->
428 RefineFailure (lazy ("(3)The term " ^
429 CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
430 context ^ " has type " ^
431 CicMetaSubst.ppterm_in_context metasenv''
432 subst'' inferredty context ^
433 " but is here used with type " ^
434 CicMetaSubst.ppterm_in_context
435 metasenv'' subst'' ty' context))
438 let (te, ty), subst, metasenv, ugraph =
439 coerce_to_something te' inferredty ty'
440 subst'' metasenv'' context exn ugraph2
442 C.Cast (te, ty'), ty', subst, metasenv, ugraph
443 with exn -> enrich localization_tbl te' exn)
444 | C.Prod (name,s,t) ->
445 let s',sort1,subst',metasenv',ugraph1 =
446 type_of_aux subst metasenv context s ugraph
448 let s',sort1,subst', metasenv',ugraph1 =
449 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
450 s' sort1 subst' context metasenv' ugraph1
452 let context_for_t = ((Some (name,(C.Decl s')))::context) in
453 let t',sort2,subst'',metasenv'',ugraph2 =
454 type_of_aux subst' metasenv'
455 context_for_t t ugraph1
457 let t',sort2,subst'',metasenv'',ugraph2 =
458 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
459 t' sort2 subst'' context_for_t metasenv'' ugraph2
461 let sop,subst''',metasenv''',ugraph3 =
462 sort_of_prod localization_tbl subst'' metasenv''
463 context (name,s') t' (sort1,sort2) ugraph2
465 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
466 | C.Lambda (n,s,t) ->
467 let s',sort1,subst',metasenv',ugraph1 =
468 type_of_aux subst metasenv context s ugraph
470 let s',sort1,subst',metasenv',ugraph1 =
471 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
472 s' sort1 subst' context metasenv' ugraph1
474 let context_for_t = ((Some (n,(C.Decl s')))::context) in
475 let t',type2,subst'',metasenv'',ugraph2 =
476 type_of_aux subst' metasenv' context_for_t t ugraph1
478 C.Lambda (n,s',t'),C.Prod (n,s',type2),
479 subst'',metasenv'',ugraph2
481 (* only to check if s is well-typed *)
482 let s',ty,subst',metasenv',ugraph1 =
483 type_of_aux subst metasenv context s ugraph
485 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
487 let t',inferredty,subst'',metasenv'',ugraph2 =
488 type_of_aux subst' metasenv'
489 context_for_t t ugraph1
491 (* One-step LetIn reduction.
492 * Even faster than the previous solution.
493 * Moreover the inferred type is closer to the expected one.
496 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
497 subst'',metasenv'',ugraph2
498 | C.Appl (he::((_::_) as tl)) ->
499 let he',hetype,subst',metasenv',ugraph1 =
500 type_of_aux subst metasenv context he ugraph
502 let tlbody_and_type,subst'',metasenv'',ugraph2 =
503 typeof_list subst' metasenv' context ugraph1 tl
505 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
506 eat_prods true subst'' metasenv'' context
507 he' hetype tlbody_and_type ugraph2
509 let newappl = (C.Appl (coerced_he::coerced_args)) in
510 avoid_double_coercion
511 context subst''' metasenv''' ugraph3 newappl applty
512 | C.Appl _ -> assert false
513 | C.Const (uri,exp_named_subst) ->
514 let exp_named_subst',subst',metasenv',ugraph1 =
515 check_exp_named_subst subst metasenv context
516 exp_named_subst ugraph in
517 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
519 CicSubstitution.subst_vars exp_named_subst' ty_uri
521 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
522 | C.MutInd (uri,i,exp_named_subst) ->
523 let exp_named_subst',subst',metasenv',ugraph1 =
524 check_exp_named_subst subst metasenv context
525 exp_named_subst ugraph
527 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
529 CicSubstitution.subst_vars exp_named_subst' ty_uri in
530 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
531 | C.MutConstruct (uri,i,j,exp_named_subst) ->
532 let exp_named_subst',subst',metasenv',ugraph1 =
533 check_exp_named_subst subst metasenv context
534 exp_named_subst ugraph
537 type_of_mutual_inductive_constr uri i j ugraph1
540 CicSubstitution.subst_vars exp_named_subst' ty_uri
542 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
544 | C.MutCase (uri, i, outtype, term, pl) ->
545 (* first, get the inductive type (and noparams)
546 * in the environment *)
547 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
548 let _ = CicTypeChecker.typecheck uri in
549 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
551 C.InductiveDefinition (l,expl_params,parsno,_) ->
552 List.nth l i , expl_params, parsno, u
554 enrich localization_tbl t
556 (lazy ("Unkown mutual inductive definition " ^
557 U.string_of_uri uri)))
559 let rec count_prod t =
560 match CicReduction.whd ~subst context t with
561 C.Prod (_, _, t) -> 1 + (count_prod t)
564 let no_args = count_prod arity in
565 (* now, create a "generic" MutInd *)
566 let metasenv,left_args =
567 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
569 let metasenv,right_args =
570 let no_right_params = no_args - no_left_params in
571 if no_right_params < 0 then assert false
572 else CicMkImplicit.n_fresh_metas
573 metasenv subst context no_right_params
575 let metasenv,exp_named_subst =
576 CicMkImplicit.fresh_subst metasenv subst context expl_params in
579 C.MutInd (uri,i,exp_named_subst)
582 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
584 (* check consistency with the actual type of term *)
585 let term',actual_type,subst,metasenv,ugraph1 =
586 type_of_aux subst metasenv context term ugraph in
587 let expected_type',_, subst, metasenv,ugraph2 =
588 type_of_aux subst metasenv context expected_type ugraph1
590 let actual_type = CicReduction.whd ~subst context actual_type in
591 let subst,metasenv,ugraph3 =
593 fo_unif_subst subst context metasenv
594 expected_type' actual_type ugraph2
597 enrich localization_tbl term' exn
599 lazy ("(10)The term " ^
600 CicMetaSubst.ppterm_in_context ~metasenv subst term'
601 context ^ " has type " ^
602 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
603 context ^ " but is here used with type " ^
604 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
606 let rec instantiate_prod t =
610 match CicReduction.whd ~subst context t with
612 instantiate_prod (CicSubstitution.subst he t') tl
615 let arity_instantiated_with_left_args =
616 instantiate_prod arity left_args in
617 (* TODO: check if the sort elimination
618 * is allowed: [(I q1 ... qr)|B] *)
619 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
621 (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
623 if left_args = [] then
624 (C.MutConstruct (uri,i,j,exp_named_subst))
627 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
629 let p',actual_type,subst,metasenv,ugraph1 =
630 type_of_aux subst metasenv context p ugraph
632 let constructor',expected_type, subst, metasenv,ugraph2 =
633 type_of_aux subst metasenv context constructor ugraph1
635 let outtypeinstance,subst,metasenv,ugraph3 =
637 check_branch 0 context metasenv subst
638 no_left_params actual_type constructor' expected_type
642 enrich localization_tbl constructor'
644 lazy ("(11)The term " ^
645 CicMetaSubst.ppterm_in_context metasenv subst p'
646 context ^ " has type " ^
647 CicMetaSubst.ppterm_in_context metasenv subst actual_type
648 context ^ " but is here used with type " ^
649 CicMetaSubst.ppterm_in_context metasenv subst expected_type
653 outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
654 pl ([],List.length pl,[],subst,metasenv,ugraph3)
657 (* we are left to check that the outype matches his instances.
658 The easy case is when the outype is specified, that amount
659 to a trivial check. Otherwise, we should guess a type from
663 let outtype,outtypety, subst, metasenv,ugraph4 =
664 type_of_aux subst metasenv context outtype ugraph4 in
667 (let candidate,ugraph5,metasenv,subst =
668 let exp_name_subst, metasenv =
670 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
672 let uris = CicUtil.params_of_obj o in
674 fun uri (acc,metasenv) ->
675 let metasenv',new_meta =
676 CicMkImplicit.mk_implicit metasenv subst context
679 CicMkImplicit.identity_relocation_list_for_metavariable
682 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
686 match left_args,right_args with
687 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
689 let rec mk_right_args =
692 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
694 let right_args_no = List.length right_args in
695 let lifted_left_args =
696 List.map (CicSubstitution.lift right_args_no) left_args
698 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
699 (lifted_left_args @ mk_right_args right_args_no))
702 FreshNamesGenerator.mk_fresh_name ~subst metasenv
703 context Cic.Anonymous ~typ:ty
705 match outtypeinstances with
707 let extended_context =
708 let rec add_right_args =
710 Cic.Prod (name,ty,t) ->
711 Some (name,Cic.Decl ty)::(add_right_args t)
714 (Some (fresh_name,Cic.Decl ty))::
716 (add_right_args arity_instantiated_with_left_args))@
719 let metasenv,new_meta =
720 CicMkImplicit.mk_implicit metasenv subst extended_context
723 CicMkImplicit.identity_relocation_list_for_metavariable
726 let rec add_lambdas b =
728 Cic.Prod (name,ty,t) ->
729 Cic.Lambda (name,ty,(add_lambdas b t))
730 | _ -> Cic.Lambda (fresh_name, ty, b)
733 add_lambdas (Cic.Meta (new_meta,irl))
734 arity_instantiated_with_left_args
736 (Some candidate),ugraph4,metasenv,subst
737 | (constructor_args_no,_,instance,_)::tl ->
739 let instance',subst,metasenv =
740 CicMetaSubst.delift_rels subst metasenv
741 constructor_args_no instance
743 let candidate,ugraph,metasenv,subst =
745 fun (candidate_oty,ugraph,metasenv,subst)
746 (constructor_args_no,_,instance,_) ->
747 match candidate_oty with
748 | None -> None,ugraph,metasenv,subst
751 let instance',subst,metasenv =
752 CicMetaSubst.delift_rels subst metasenv
753 constructor_args_no instance
755 let subst,metasenv,ugraph =
756 fo_unif_subst subst context metasenv
759 candidate_oty,ugraph,metasenv,subst
761 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
762 | RefineFailure _ | Uncertain _ ->
763 None,ugraph,metasenv,subst
764 ) (Some instance',ugraph4,metasenv,subst) tl
767 | None -> None, ugraph,metasenv,subst
769 let rec add_lambdas n b =
771 Cic.Prod (name,ty,t) ->
772 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
774 Cic.Lambda (fresh_name, ty,
775 CicSubstitution.lift (n + 1) t)
778 (add_lambdas 0 t arity_instantiated_with_left_args),
779 ugraph,metasenv,subst
780 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
781 None,ugraph4,metasenv,subst
784 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
786 let subst,metasenv,ugraph =
788 fo_unif_subst subst context metasenv
789 candidate outtype ugraph5
791 exn -> assert false(* unification against a metavariable *)
793 C.MutCase (uri, i, outtype, term', pl'),
794 CicReduction.head_beta_reduce
795 (CicMetaSubst.apply_subst subst
796 (Cic.Appl (outtype::right_args@[term']))),
797 subst,metasenv,ugraph)
798 | _ -> (* easy case *)
799 let tlbody_and_type,subst,metasenv,ugraph4 =
800 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
802 let _,_,_,subst,metasenv,ugraph4 =
803 eat_prods false subst metasenv context
804 outtype outtypety tlbody_and_type ugraph4
806 let _,_, subst, metasenv,ugraph5 =
807 type_of_aux subst metasenv context
808 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
810 let (subst,metasenv,ugraph6) =
812 (fun (subst,metasenv,ugraph)
813 p (constructor_args_no,context,instance,args)
818 CicSubstitution.lift constructor_args_no outtype
820 C.Appl (outtype'::args)
822 CicReduction.whd ~subst context appl
825 fo_unif_subst subst context metasenv instance instance'
829 enrich localization_tbl p exn
831 lazy ("(12)The term " ^
832 CicMetaSubst.ppterm_in_context ~metasenv subst p
833 context ^ " has type " ^
834 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
835 context ^ " but is here used with type " ^
836 CicMetaSubst.ppterm_in_context ~metasenv subst instance
838 (subst,metasenv,ugraph5) pl' outtypeinstances
840 C.MutCase (uri, i, outtype, term', pl'),
841 CicReduction.head_beta_reduce
842 (CicMetaSubst.apply_subst subst
843 (C.Appl(outtype::right_args@[term]))),
844 subst,metasenv,ugraph6)
846 let fl_ty',subst,metasenv,types,ugraph1,len =
848 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
849 let ty',_,subst',metasenv',ugraph1 =
850 type_of_aux subst metasenv context ty ugraph
852 fl @ [ty'],subst',metasenv',
853 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
854 :: types, ugraph, len+1
855 ) ([],subst,metasenv,[],ugraph,0) fl
857 let context' = types@context in
858 let fl_bo',subst,metasenv,ugraph2 =
860 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
861 let bo',ty_of_bo,subst,metasenv,ugraph1 =
862 type_of_aux subst metasenv context' bo ugraph in
863 let expected_ty = CicSubstitution.lift len ty in
864 let subst',metasenv',ugraph' =
866 fo_unif_subst subst context' metasenv
867 ty_of_bo expected_ty ugraph1
870 enrich localization_tbl bo exn
872 lazy ("(13)The term " ^
873 CicMetaSubst.ppterm_in_context ~metasenv subst bo
874 context' ^ " has type " ^
875 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
876 context' ^ " but is here used with type " ^
877 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
880 fl @ [bo'] , subst',metasenv',ugraph'
881 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
883 let ty = List.nth fl_ty' i in
884 (* now we have the new ty in fl_ty', the new bo in fl_bo',
885 * and we want the new fl with bo' and ty' injected in the right
888 let rec map3 f l1 l2 l3 =
891 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
894 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
897 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
899 let fl_ty',subst,metasenv,types,ugraph1,len =
901 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
902 let ty',_,subst',metasenv',ugraph1 =
903 type_of_aux subst metasenv context ty ugraph
905 fl @ [ty'],subst',metasenv',
906 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
907 types, ugraph1, len+1
908 ) ([],subst,metasenv,[],ugraph,0) fl
910 let context' = types@context in
911 let fl_bo',subst,metasenv,ugraph2 =
913 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
914 let bo',ty_of_bo,subst,metasenv,ugraph1 =
915 type_of_aux subst metasenv context' bo ugraph in
916 let expected_ty = CicSubstitution.lift len ty in
917 let subst',metasenv',ugraph' =
919 fo_unif_subst subst context' metasenv
920 ty_of_bo expected_ty ugraph1
923 enrich localization_tbl bo exn
925 lazy ("(14)The term " ^
926 CicMetaSubst.ppterm_in_context ~metasenv subst bo
927 context' ^ " has type " ^
928 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
929 context' ^ " but is here used with type " ^
930 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
933 fl @ [bo'],subst',metasenv',ugraph'
934 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
936 let ty = List.nth fl_ty' i in
937 (* now we have the new ty in fl_ty', the new bo in fl_bo',
938 * and we want the new fl with bo' and ty' injected in the right
941 let rec map3 f l1 l2 l3 =
944 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
947 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
950 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
952 relocalize localization_tbl t t';
955 (* check_metasenv_consistency checks that the "canonical" context of a
956 metavariable is consitent - up to relocation via the relocation list l -
957 with the actual context *)
958 and check_metasenv_consistency
959 metano subst metasenv context canonical_context l ugraph
961 let module C = Cic in
962 let module R = CicReduction in
963 let module S = CicSubstitution in
964 let lifted_canonical_context =
968 | (Some (n,C.Decl t))::tl ->
969 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
970 | (Some (n,C.Def (t,None)))::tl ->
971 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
972 | None::tl -> None::(aux (i+1) tl)
973 | (Some (n,C.Def (t,Some ty)))::tl ->
975 C.Def ((S.subst_meta l (S.lift i t)),
976 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
978 aux 1 canonical_context
982 (fun (l,subst,metasenv,ugraph) t ct ->
985 l @ [None],subst,metasenv,ugraph
986 | Some t,Some (_,C.Def (ct,_)) ->
987 let subst',metasenv',ugraph' =
989 prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
990 fo_unif_subst subst context metasenv t ct ugraph
991 with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
993 l @ [Some t],subst',metasenv',ugraph'
994 | Some t,Some (_,C.Decl ct) ->
995 let t',inferredty,subst',metasenv',ugraph1 =
996 type_of_aux subst metasenv context t ugraph
998 let subst'',metasenv'',ugraph2 =
1001 subst' context metasenv' inferredty ct ugraph1
1002 with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
1004 l @ [Some t'], subst'',metasenv'',ugraph2
1006 raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
1008 Invalid_argument _ ->
1012 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1013 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1014 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1016 and check_exp_named_subst metasubst metasenv context tl ugraph =
1017 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1019 [] -> [],metasubst,metasenv,ugraph
1021 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1023 CicSubstitution.subst_vars substs ty_uri in
1024 (* CSC: why was this code here? it is wrong
1025 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1026 Cic.Variable (_,Some bo,_,_) ->
1028 (RefineFailure (lazy
1029 "A variable with a body can not be explicit substituted"))
1030 | Cic.Variable (_,None,_,_) -> ()
1033 (RefineFailure (lazy
1034 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1037 let t',typeoft,metasubst',metasenv',ugraph2 =
1038 type_of_aux metasubst metasenv context t ugraph1 in
1039 let subst = uri,t' in
1040 let metasubst'',metasenv'',ugraph3 =
1043 metasubst' context metasenv' typeoft typeofvar ugraph2
1045 raise (RefineFailure (lazy
1046 ("Wrong Explicit Named Substitution: " ^
1047 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1048 " not unifiable with " ^
1049 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1051 (* FIXME: no mere tail recursive! *)
1052 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1053 check_exp_named_subst_aux
1054 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1056 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1058 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1061 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1064 let module C = Cic in
1065 let context_for_t2 = (Some (name,C.Decl s))::context in
1066 let t1'' = CicReduction.whd ~subst context t1 in
1067 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1068 match (t1'', t2'') with
1069 (C.Sort s1, C.Sort s2)
1070 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1071 (* different than Coq manual!!! *)
1072 C.Sort s2,subst,metasenv,ugraph
1073 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1074 let t' = CicUniv.fresh() in
1076 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1077 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1078 C.Sort (C.Type t'),subst,metasenv,ugraph2
1080 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1081 | (C.Sort _,C.Sort (C.Type t1)) ->
1082 C.Sort (C.Type t1),subst,metasenv,ugraph
1083 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1084 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1085 (* TODO how can we force the meta to become a sort? If we don't we
1086 * break the invariant that refine produce only well typed terms *)
1087 (* TODO if we check the non meta term and if it is a sort then we
1088 * are likely to know the exact value of the result e.g. if the rhs
1089 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1090 let (metasenv,idx) =
1091 CicMkImplicit.mk_implicit_sort metasenv subst in
1092 let (subst, metasenv,ugraph1) =
1094 fo_unif_subst subst context_for_t2 metasenv
1095 (C.Meta (idx,[])) t2'' ugraph
1096 with _ -> assert false (* unification against a metavariable *)
1098 t2'',subst,metasenv,ugraph1
1101 enrich localization_tbl s
1105 "%s is supposed to be a type, but its type is %s"
1106 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1107 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1109 enrich localization_tbl t
1113 "%s is supposed to be a type, but its type is %s"
1114 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1115 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1117 and avoid_double_coercion context subst metasenv ugraph t ty =
1118 if not !pack_coercions then
1119 t,ty,subst,metasenv,ugraph
1121 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1123 let source_carr = CoercGraph.source_of c2 in
1124 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1125 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1127 | CoercGraph.SomeCoercion candidates ->
1129 HExtlib.list_findopt
1130 (function (metasenv,last,c) ->
1132 | c when not (CoercGraph.is_composite c) ->
1133 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1136 let subst,metasenv,ugraph =
1137 fo_unif_subst subst context metasenv last head ugraph in
1138 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1143 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1144 let newt,_,subst,metasenv,ugraph =
1145 type_of_aux subst metasenv context c ugraph in
1146 debug_print (lazy "tipa...");
1147 let subst, metasenv, ugraph =
1148 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1149 fo_unif_subst subst context metasenv newt t ugraph
1151 debug_print (lazy "unifica...");
1152 Some (newt, ty, subst, metasenv, ugraph)
1154 | RefineFailure s | Uncertain s when not !pack_coercions->
1155 debug_print s; debug_print (lazy "stop\n");None
1156 | RefineFailure s | Uncertain s ->
1157 debug_print s;debug_print (lazy "goon\n");
1159 let old_pack_coercions = !pack_coercions in
1160 pack_coercions := false; (* to avoid diverging *)
1161 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1162 type_of_aux subst metasenv context c1_c2_implicit ugraph
1164 pack_coercions := old_pack_coercions;
1166 is_a_double_coercion refined_c1_c2_implicit
1172 match refined_c1_c2_implicit with
1173 | Cic.Appl l -> HExtlib.list_last l
1176 let subst, metasenv, ugraph =
1177 try fo_unif_subst subst context metasenv
1179 with RefineFailure s| Uncertain s->
1180 debug_print s;assert false
1182 let subst, metasenv, ugraph =
1183 fo_unif_subst subst context metasenv
1184 refined_c1_c2_implicit t ugraph
1186 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1188 | RefineFailure s | Uncertain s ->
1189 pack_coercions := true;debug_print s;None
1190 | exn -> pack_coercions := true; raise exn))
1193 (match selected with
1197 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1198 t, ty, subst, metasenv, ugraph)
1199 | _ -> t, ty, subst, metasenv, ugraph)
1201 t, ty, subst, metasenv, ugraph
1203 and typeof_list subst metasenv context ugraph l =
1204 let tlbody_and_type,subst,metasenv,ugraph =
1206 (fun x (res,subst,metasenv,ugraph) ->
1207 let x',ty,subst',metasenv',ugraph1 =
1208 type_of_aux subst metasenv context x ugraph
1210 (x', ty)::res,subst',metasenv',ugraph1
1211 ) l ([],subst,metasenv,ugraph)
1213 tlbody_and_type,subst,metasenv,ugraph
1216 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1218 (* aux function to add coercions to funclass *)
1219 let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph =
1221 let pristinemenv = metasenv in
1222 let metasenv,hetype' =
1223 mk_prod_of_metas metasenv context subst args_bo_and_ty
1226 let subst,metasenv,ugraph =
1227 fo_unif_subst_eat_prods
1228 subst context metasenv hetype hetype' ugraph
1230 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1231 with RefineFailure s | Uncertain s as exn
1232 when allow_coercions && !insert_coercions ->
1233 (* {{{ we search a coercion of the head (saturated) to funclass *)
1234 let metasenv = pristinemenv in
1236 ("Fixing arity of: "^CicMetaSubst.ppterm ~metasenv subst hetype ^
1237 " since unif failed with: " ^ CicMetaSubst.ppterm ~metasenv subst hetype'
1238 (* ^ " cause: " ^ Lazy.force s *)));
1239 let how_many_args_are_needed =
1240 let rec aux n = function
1241 | Cic.Prod(_,_,t) -> aux (n+1) t
1244 aux 0 (CicMetaSubst.apply_subst subst hetype)
1246 let args, remainder =
1247 HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
1249 let args = List.map fst args in
1253 | Cic.Appl l -> Cic.Appl (l@args)
1254 | _ -> Cic.Appl (he::args)
1258 let x,xty,subst,metasenv,ugraph =
1259 (*CSC: here unsharing is necessary to avoid an unwanted
1260 relocalization. However, this also shows a great source of
1261 inefficiency: "x" is refined twice (once now and once in the
1262 subsequent eat_prods_and_args). Morevoer, how is divergence avoided?
1264 type_of_aux subst metasenv context (Unshare.unshare x) ugraph
1267 CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty)
1269 let carr_tgt = CoercDb.Fun 0 in
1270 match CoercGraph.look_for_coercion' metasenv subst context carr_src carr_tgt with
1271 | CoercGraph.NoCoercion
1272 | CoercGraph.NotMetaClosed
1273 | CoercGraph.NotHandled _ -> raise exn
1274 | CoercGraph.SomeCoercionToTgt candidates
1275 | CoercGraph.SomeCoercion candidates ->
1277 HExtlib.list_findopt
1278 (fun (metasenv,last,coerc) ->
1279 let subst,metasenv,ugraph =
1280 fo_unif_subst subst context metasenv last x ugraph in
1281 debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc));
1283 (* we want this to be available in the error handler fo the
1284 * following (so it has its own try. *)
1285 let t,tty,subst,metasenv,ugraph =
1286 type_of_aux subst metasenv context coerc ugraph
1289 let metasenv, hetype' =
1290 mk_prod_of_metas metasenv context subst remainder
1293 (" unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^
1294 CicMetaSubst.ppterm ~metasenv subst hetype'));
1295 let subst,metasenv,ugraph =
1296 fo_unif_subst_eat_prods
1297 subst context metasenv tty hetype' ugraph
1299 debug_print (lazy " success!");
1300 Some (subst,metasenv,ugraph,tty,t,remainder)
1302 | Uncertain _ | RefineFailure _ ->
1304 let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
1306 metasenv context subst t tty remainder ugraph
1308 Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
1309 with Uncertain _ | RefineFailure _ -> None
1313 | HExtlib.Localized (_,Uncertain _)
1314 | HExtlib.Localized (_,RefineFailure _) -> None
1315 | exn -> assert false) (* ritornare None, e' un localized *)
1318 | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
1319 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1321 more_args_than_expected localization_tbl metasenv
1322 subst he context hetype args_bo_and_ty exn
1323 (* }}} end coercion to funclass stuff *)
1324 (* }}} end fix_arity *)
1326 (* aux function to process the type of the head and the args in parallel *)
1327 let rec eat_prods_and_args
1328 pristinemenv metasenv subst context pristinehe he hetype ugraph newargs
1332 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1333 | (hete, hety)::tl ->
1334 match (CicReduction.whd ~subst context hetype) with
1335 | Cic.Prod (n,s,t) ->
1336 let arg,subst,metasenv,ugraph1 =
1339 let subst,metasenv,ugraph1 =
1340 fo_unif_subst_eat_prods2
1341 subst context metasenv hety s ugraph
1343 (hete,hety),subst,metasenv,ugraph1
1344 with RefineFailure _ | Uncertain _ as exn
1345 when allow_coercions && !insert_coercions ->
1347 hete hety s subst metasenv context exn ugraph)
1349 enrich localization_tbl hete
1351 (lazy ("(2)The term " ^
1352 CicMetaSubst.ppterm_in_context ~metasenv subst hete
1353 context ^ " has type " ^
1354 CicMetaSubst.ppterm_in_context ~metasenv subst hety
1355 context ^ " but is here used with type " ^
1356 CicMetaSubst.ppterm_in_context
1357 ~metasenv subst s context
1358 (* "\nReason: " ^ Printexc.to_string exn*)))) exn
1360 eat_prods_and_args pristinemenv metasenv subst context pristinehe he
1361 (CicSubstitution.subst (fst arg) t)
1362 ugraph1 (newargs@[arg]) tl
1365 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1367 pristinemenv context subst he hetype
1368 (newargs@[hete,hety]@tl) ugraph
1370 eat_prods_and_args metasenv
1371 metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
1372 with RefineFailure _ | Uncertain _ as exn ->
1373 (* unable to fix arity *)
1374 more_args_than_expected localization_tbl metasenv
1375 subst he context hetype args_bo_and_ty exn
1378 (* first we check if we are in the simple case of a meta closed term *)
1379 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1380 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1381 (* this optimization is to postpone fix_arity (the most common case)*)
1382 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1384 (* this (says CSC) is also useful to infer dependent types *)
1386 fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
1387 with RefineFailure _ | Uncertain _ as exn ->
1388 (* unable to fix arity *)
1389 more_args_than_expected localization_tbl metasenv
1390 subst he context hetype args_bo_and_ty exn
1392 let coerced_args,subst,metasenv,he,t,ugraph =
1394 metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
1396 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1398 and coerce_to_something t infty expty subst metasenv context exn ugraph =
1399 if not !insert_coercions then
1402 let clean t subst context =
1403 CicReduction.whd ~delta:false context (CicMetaSubst.apply_subst subst t)
1405 let infty = clean infty subst context in
1406 let expty = clean expty subst context in
1407 match infty, expty with
1408 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2) ->
1409 (* covariant part *)
1410 let name_con = Cic.Name "name_con" in
1411 let name_t, ty_s_bo, bo =
1413 | Cic.Lambda (name, src, bo) -> name, src, bo
1414 | _ -> name_con, src, Cic.Appl [CicSubstitution.lift 1 t ; Cic.Rel 1]
1416 let context_bo = (Some (name_t, Cic.Decl ty_s_bo)) :: context in
1417 let (bo, _), subst, metasenv, ugraph =
1418 coerce_to_something bo ty ty2 subst metasenv context_bo exn ugraph
1420 (* contravariant part *)
1421 let context_rel1 = (Some (name_t, Cic.Decl src2) :: context) in
1422 let (rel1, _), subst, metasenv, ugraph =
1423 coerce_to_something (Cic.Rel 1) (CicSubstitution.lift 1 src2)
1424 (CicSubstitution.lift 1 src) subst metasenv context_rel1 exn
1428 Cic.Lambda (name_t,src2,
1429 CicSubstitution.subst rel1 (CicSubstitution.lift_from 2 1 bo))
1431 (coerced, expty), subst, metasenv, ugraph
1433 coerce_atom_to_something t infty expty subst metasenv context exn ugraph
1435 and coerce_atom_to_something t infty expty subst metasenv context exn ugraph =
1437 CoercGraph.look_for_coercion metasenv subst context infty expty
1440 | CoercGraph.NotMetaClosed ->
1442 | RefineFailure s -> raise (Uncertain s)
1443 | HExtlib.Localized _ -> assert false
1445 | CoercGraph.NoCoercion
1446 | CoercGraph.SomeCoercionToTgt _
1447 | CoercGraph.NotHandled _ ->
1449 | CoercGraph.SomeCoercion candidates ->
1451 HExtlib.list_findopt
1452 (fun (metasenv,last,c) ->
1454 let subst,metasenv,ugraph =
1455 fo_unif_subst subst context metasenv last t
1457 let newt,newhety,subst,metasenv,ugraph =
1458 type_of_aux subst metasenv context
1461 let newt, newty, subst, metasenv, ugraph =
1462 avoid_double_coercion context subst metasenv
1465 let subst,metasenv,ugraph1 =
1466 fo_unif_subst subst context metasenv
1467 newhety expty ugraph
1469 Some ((newt,newty), subst, metasenv, ugraph)
1470 with Uncertain _ | RefineFailure _ -> None)
1478 in_source tgt_sort t type_to_coerce subst context metasenv uragph =
1479 match CicReduction.whd ~subst:subst context type_to_coerce with
1480 | Cic.Meta _ | Cic.Sort _ ->
1481 t,type_to_coerce, subst, metasenv, ugraph
1483 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1485 RefineFailure (lazy ("(7)The term " ^
1486 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1487 ^ " is not a type since it has type " ^
1488 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1489 ^ " that is not a sort"))
1492 let (t, ty_t), subst, metasenv, ugraph =
1493 coerce_to_something t src tgt
1494 subst metasenv context exn ugraph
1496 t, ty_t, subst, metasenv, ugraph
1497 with exn -> enrich localization_tbl t exn
1500 (* eat prods ends here! *)
1502 let t',ty,subst',metasenv',ugraph1 =
1503 type_of_aux [] metasenv context t ugraph
1505 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1506 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1507 (* Andrea: ho rimesso qui l'applicazione della subst al
1508 metasenv dopo che ho droppato l'invariante che il metsaenv
1509 e' sempre istanziato *)
1510 let substituted_metasenv =
1511 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1513 (* substituted_t,substituted_ty,substituted_metasenv *)
1514 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1516 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1518 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1519 let cleaned_metasenv =
1521 (function (n,context,ty) ->
1522 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1527 | Some (n, Cic.Decl t) ->
1529 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1530 | Some (n, Cic.Def (bo,ty)) ->
1531 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1536 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1538 Some (n, Cic.Def (bo',ty'))
1542 ) substituted_metasenv
1544 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1547 let undebrujin uri typesno tys t =
1550 (fun (name,_,_,_) (i,t) ->
1551 (* here the explicit_named_substituion is assumed to be *)
1553 let t' = Cic.MutInd (uri,i,[]) in
1554 let t = CicSubstitution.subst t' t in
1556 ) tys (typesno - 1,t))
1558 let map_first_n n start f g l =
1559 let rec aux acc k l =
1562 | [] -> raise (Invalid_argument "map_first_n")
1563 | hd :: tl -> f hd k (aux acc (k+1) tl)
1569 (*CSC: this is a very rough approximation; to be finished *)
1570 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1571 let subst,metasenv,ugraph,tys =
1573 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1574 let subst,metasenv,ugraph,cl =
1576 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1577 let rec aux ctx k subst = function
1578 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1579 let subst,metasenv,ugraph,tl =
1581 (subst,metasenv,ugraph,[])
1582 (fun t n (subst,metasenv,ugraph,acc) ->
1583 let subst,metasenv,ugraph =
1585 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1587 subst,metasenv,ugraph,(t::acc))
1588 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1591 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1592 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1593 subst,metasenv,ugraph,t
1594 | Cic.Prod (name,s,t) ->
1595 let ctx = (Some (name,Cic.Decl s))::ctx in
1596 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1597 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1601 (lazy "not well formed constructor type"))
1603 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1604 subst,metasenv,ugraph,(name,ty) :: acc)
1605 cl (subst,metasenv,ugraph,[])
1607 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1608 tys ([],metasenv,ugraph,[])
1610 let substituted_tys =
1612 (fun (name,ind,arity,cl) ->
1614 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1616 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1619 metasenv,ugraph,substituted_tys
1621 let typecheck metasenv uri obj ~localization_tbl =
1622 let ugraph = CicUniv.empty_ugraph in
1624 Cic.Constant (name,Some bo,ty,args,attrs) ->
1625 let bo',boty,metasenv,ugraph =
1626 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1627 let ty',_,metasenv,ugraph =
1628 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1629 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1630 let bo' = CicMetaSubst.apply_subst subst bo' in
1631 let ty' = CicMetaSubst.apply_subst subst ty' in
1632 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1633 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1634 | Cic.Constant (name,None,ty,args,attrs) ->
1635 let ty',_,metasenv,ugraph =
1636 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1638 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1639 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1640 assert (metasenv' = metasenv);
1641 (* Here we do not check the metasenv for correctness *)
1642 let bo',boty,metasenv,ugraph =
1643 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1644 let ty',sort,metasenv,ugraph =
1645 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1649 (* instead of raising Uncertain, let's hope that the meta will become
1652 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1654 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1655 let bo' = CicMetaSubst.apply_subst subst bo' in
1656 let ty' = CicMetaSubst.apply_subst subst ty' in
1657 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1658 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1659 | Cic.Variable _ -> assert false (* not implemented *)
1660 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1661 (*CSC: this code is greately simplified and many many checks are missing *)
1662 (*CSC: e.g. the constructors are not required to build their own types, *)
1663 (*CSC: the arities are not required to have as type a sort, etc. *)
1664 let uri = match uri with Some uri -> uri | None -> assert false in
1665 let typesno = List.length tys in
1666 (* first phase: we fix only the types *)
1667 let metasenv,ugraph,tys =
1669 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1670 let ty',_,metasenv,ugraph =
1671 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1673 metasenv,ugraph,(name,b,ty',cl)::res
1674 ) tys (metasenv,ugraph,[]) in
1676 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1677 (* second phase: we fix only the constructors *)
1678 let saved_menv = metasenv in
1679 let metasenv,ugraph,tys =
1681 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1682 let metasenv,ugraph,cl' =
1684 (fun (name,ty) (metasenv,ugraph,res) ->
1686 CicTypeChecker.debrujin_constructor
1687 ~cb:(relocalize localization_tbl) uri typesno ty in
1688 let ty',_,metasenv,ugraph =
1689 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1690 let ty' = undebrujin uri typesno tys ty' in
1691 metasenv@saved_menv,ugraph,(name,ty')::res
1692 ) cl (metasenv,ugraph,[])
1694 metasenv,ugraph,(name,b,ty,cl')::res
1695 ) tys (metasenv,ugraph,[]) in
1696 (* third phase: we check the positivity condition *)
1697 let metasenv,ugraph,tys =
1698 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1700 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1703 (* sara' piu' veloce che raffinare da zero? mah.... *)
1704 let pack_coercion metasenv ctx t =
1705 let module C = Cic in
1706 let rec merge_coercions ctx =
1707 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1709 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1710 | C.Meta (n,subst) ->
1713 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1716 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1717 | C.Prod (name,so,dest) ->
1718 let ctx' = (Some (name,C.Decl so))::ctx in
1719 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1720 | C.Lambda (name,so,dest) ->
1721 let ctx' = (Some (name,C.Decl so))::ctx in
1722 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1723 | C.LetIn (name,so,dest) ->
1724 let _,ty,metasenv,ugraph =
1725 pack_coercions := false;
1726 type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1727 pack_coercions := true;
1728 let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1729 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1731 let l = List.map (merge_coercions ctx) l in
1733 let b,_,_,_,_ = is_a_double_coercion t in
1735 let ugraph = CicUniv.oblivion_ugraph in
1736 let old_insert_coercions = !insert_coercions in
1737 insert_coercions := false;
1738 let newt, _, menv, _ =
1740 type_of_aux' metasenv ctx t ugraph
1741 with RefineFailure _ | Uncertain _ ->
1744 insert_coercions := old_insert_coercions;
1745 if metasenv <> [] || menv = [] then
1748 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1751 | C.Var (uri,exp_named_subst) ->
1752 let exp_named_subst = List.map aux exp_named_subst in
1753 C.Var (uri, exp_named_subst)
1754 | C.Const (uri,exp_named_subst) ->
1755 let exp_named_subst = List.map aux exp_named_subst in
1756 C.Const (uri, exp_named_subst)
1757 | C.MutInd (uri,tyno,exp_named_subst) ->
1758 let exp_named_subst = List.map aux exp_named_subst in
1759 C.MutInd (uri,tyno,exp_named_subst)
1760 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1761 let exp_named_subst = List.map aux exp_named_subst in
1762 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1763 | C.MutCase (uri,tyno,out,te,pl) ->
1764 let pl = List.map (merge_coercions ctx) pl in
1765 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1766 | C.Fix (fno, fl) ->
1769 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1774 (fun (name,idx,ty,bo) ->
1775 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1779 | C.CoFix (fno, fl) ->
1782 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1787 (fun (name,ty,bo) ->
1788 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1793 merge_coercions ctx t
1796 let pack_coercion_metasenv conjectures =
1797 let module C = Cic in
1799 (fun (i, ctx, ty) ->
1805 Some (name, C.Decl t) ->
1806 Some (name, C.Decl (pack_coercion conjectures ctx t))
1807 | Some (name, C.Def (t,None)) ->
1808 Some (name,C.Def (pack_coercion conjectures ctx t,None))
1809 | Some (name, C.Def (t,Some ty)) ->
1810 Some (name, C.Def (pack_coercion conjectures ctx t,
1811 Some (pack_coercion conjectures ctx ty)))
1817 ((i,ctx,pack_coercion conjectures ctx ty))
1821 let pack_coercion_obj obj =
1822 let module C = Cic in
1824 | C.Constant (id, body, ty, params, attrs) ->
1828 | Some body -> Some (pack_coercion [] [] body)
1830 let ty = pack_coercion [] [] ty in
1831 C.Constant (id, body, ty, params, attrs)
1832 | C.Variable (name, body, ty, params, attrs) ->
1836 | Some body -> Some (pack_coercion [] [] body)
1838 let ty = pack_coercion [] [] ty in
1839 C.Variable (name, body, ty, params, attrs)
1840 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1841 let conjectures = pack_coercion_metasenv conjectures in
1842 let body = pack_coercion conjectures [] body in
1843 let ty = pack_coercion conjectures [] ty in
1844 C.CurrentProof (name, conjectures, body, ty, params, attrs)
1845 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1848 (fun (name, ind, arity, cl) ->
1849 let arity = pack_coercion [] [] arity in
1851 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
1853 (name, ind, arity, cl))
1856 C.InductiveDefinition (indtys, params, leftno, attrs)
1861 let type_of_aux' metasenv context term =
1864 type_of_aux' metasenv context term in
1866 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1868 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1871 | RefineFailure msg as e ->
1872 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1874 | Uncertain msg as e ->
1875 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1879 let profiler2 = HExtlib.profile "CicRefine"
1881 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1882 profiler2.HExtlib.profile
1883 (type_of_aux' ?localization_tbl metasenv context term) ugraph
1885 let typecheck ~localization_tbl metasenv uri obj =
1886 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
1888 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
1889 (* vim:set foldmethod=marker: *)