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
36 let debug_print = fun _ -> ()
38 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
40 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
43 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
44 in profiler_eat_prods2.HExtlib.profile foo ()
46 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
47 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
50 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
52 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
55 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
56 in profiler_eat_prods.HExtlib.profile foo ()
58 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
59 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
62 let profiler = HExtlib.profile "CicRefine.fo_unif"
64 let fo_unif_subst subst context metasenv t1 t2 ugraph =
67 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
68 in profiler.HExtlib.profile foo ()
70 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
71 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
74 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
77 RefineFailure msg -> RefineFailure (f msg)
78 | Uncertain msg -> Uncertain (f msg)
79 | _ -> assert false in
82 Cic.CicHash.find localization_tbl t
84 prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
87 raise (HExtlib.Localized (loc,exn'))
89 let relocalize localization_tbl oldt newt =
91 let infos = Cic.CicHash.find localization_tbl oldt in
92 Cic.CicHash.remove localization_tbl oldt;
93 Cic.CicHash.add localization_tbl newt infos;
101 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
102 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
105 let exp_impl metasenv subst context =
108 let (metasenv', idx) =
109 CicMkImplicit.mk_implicit_type metasenv subst context in
111 CicMkImplicit.identity_relocation_list_for_metavariable context in
112 metasenv', Cic.Meta (idx, irl)
114 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
115 metasenv', Cic.Meta (idx, [])
117 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
119 CicMkImplicit.identity_relocation_list_for_metavariable context in
120 metasenv', Cic.Meta (idx, irl)
124 let is_a_double_coercion t =
126 let rec aux = function
134 false, Cic.Implicit None, Cic.Implicit None, Cic.Implicit None
137 | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 ->
138 (match last_of tl with
139 | Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
140 let head = last_of tl2 in
145 let rec type_of_constant uri ugraph =
146 let module C = Cic in
147 let module R = CicReduction in
148 let module U = UriManager in
149 let _ = CicTypeChecker.typecheck uri in
152 CicEnvironment.get_cooked_obj ugraph uri
153 with Not_found -> assert false
156 C.Constant (_,_,ty,_,_) -> ty,u
157 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
161 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
163 and type_of_variable uri ugraph =
164 let module C = Cic in
165 let module R = CicReduction in
166 let module U = UriManager in
167 let _ = CicTypeChecker.typecheck uri in
170 CicEnvironment.get_cooked_obj ugraph uri
171 with Not_found -> assert false
174 C.Variable (_,_,ty,_,_) -> ty,u
178 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
180 and type_of_mutual_inductive_defs uri i ugraph =
181 let module C = Cic in
182 let module R = CicReduction in
183 let module U = UriManager in
184 let _ = CicTypeChecker.typecheck uri in
187 CicEnvironment.get_cooked_obj ugraph uri
188 with Not_found -> assert false
191 C.InductiveDefinition (dl,_,_,_) ->
192 let (_,_,arity,_) = List.nth dl i in
197 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
199 and type_of_mutual_inductive_constr uri i j ugraph =
200 let module C = Cic in
201 let module R = CicReduction in
202 let module U = UriManager in
203 let _ = CicTypeChecker.typecheck uri in
206 CicEnvironment.get_cooked_obj ugraph uri
207 with Not_found -> assert false
210 C.InductiveDefinition (dl,_,_,_) ->
211 let (_,_,_,cl) = List.nth dl i in
212 let (_,ty) = List.nth cl (j-1) in
218 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
221 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
223 (* the check_branch function checks if a branch of a case is refinable.
224 It returns a pair (outype_instance,args), a subst and a metasenv.
225 outype_instance is the expected result of applying the case outtype
227 The problem is that outype is in general unknown, and we should
228 try to synthesize it from the above information, that is in general
229 a second order unification problem. *)
231 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
232 let module C = Cic in
233 (* let module R = CicMetaSubst in *)
234 let module R = CicReduction in
235 match R.whd ~subst context expectedtype with
237 (n,context,actualtype, [term]), subst, metasenv, ugraph
238 | C.Appl (C.MutInd (_,_,_)::tl) ->
239 let (_,arguments) = split tl left_args_no in
240 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
241 | C.Prod (name,so,de) ->
242 (* we expect that the actual type of the branch has the due
244 (match R.whd ~subst context actualtype with
245 C.Prod (name',so',de') ->
246 let subst, metasenv, ugraph1 =
247 fo_unif_subst subst context metasenv so so' ugraph in
249 (match CicSubstitution.lift 1 term with
250 C.Appl l -> C.Appl (l@[C.Rel 1])
251 | t -> C.Appl [t ; C.Rel 1]) in
252 (* we should also check that the name variable is anonymous in
253 the actual type de' ?? *)
255 ((Some (name,(C.Decl so)))::context)
256 metasenv subst left_args_no de' term' de ugraph1
257 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
258 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
260 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
263 let rec type_of_aux subst metasenv context t ugraph =
264 let try_coercion t subst metasenv context ugraph coercion_tgt c =
265 let coerced = Cic.Appl[c;t] in
267 let newt,_,subst,metasenv,ugraph =
268 type_of_aux subst metasenv context coerced ugraph
270 let newt, tty, subst, metasenv, ugraph =
271 avoid_double_coercion context subst metasenv ugraph newt coercion_tgt
273 Some (newt, tty, subst, metasenv, ugraph)
275 | RefineFailure _ | Uncertain _ -> None
277 let module C = Cic in
278 let module S = CicSubstitution in
279 let module U = UriManager in
280 let (t',_,_,_,_) as res =
285 match List.nth context (n - 1) with
286 Some (_,C.Decl ty) ->
287 t,S.lift n ty,subst,metasenv, ugraph
288 | Some (_,C.Def (_,Some ty)) ->
289 t,S.lift n ty,subst,metasenv, ugraph
290 | Some (_,C.Def (bo,None)) ->
292 (* if it is in the context it must be already well-typed*)
293 CicTypeChecker.type_of_aux' ~subst metasenv context
296 t,ty,subst,metasenv,ugraph
298 enrich localization_tbl t
299 (RefineFailure (lazy "Rel to hidden hypothesis"))
302 enrich localization_tbl t
303 (RefineFailure (lazy "Not a close term")))
304 | C.Var (uri,exp_named_subst) ->
305 let exp_named_subst',subst',metasenv',ugraph1 =
306 check_exp_named_subst
307 subst metasenv context exp_named_subst ugraph
309 let ty_uri,ugraph1 = type_of_variable uri ugraph in
311 CicSubstitution.subst_vars exp_named_subst' ty_uri
313 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
316 let (canonical_context, term,ty) =
317 CicUtil.lookup_subst n subst
319 let l',subst',metasenv',ugraph1 =
320 check_metasenv_consistency n subst metasenv context
321 canonical_context l ugraph
323 (* trust or check ??? *)
324 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
325 subst', metasenv', ugraph1
326 (* type_of_aux subst metasenv
327 context (CicSubstitution.subst_meta l term) *)
328 with CicUtil.Subst_not_found _ ->
329 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
330 let l',subst',metasenv', ugraph1 =
331 check_metasenv_consistency n subst metasenv context
332 canonical_context l ugraph
334 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
335 subst', metasenv',ugraph1)
336 | C.Sort (C.Type tno) ->
337 let tno' = CicUniv.fresh() in
338 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
339 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
341 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
342 | C.Implicit infos ->
343 let metasenv',t' = exp_impl metasenv subst context infos in
344 type_of_aux subst metasenv' context t' ugraph
346 let ty',_,subst',metasenv',ugraph1 =
347 type_of_aux subst metasenv context ty ugraph
349 let te',inferredty,subst'',metasenv'',ugraph2 =
350 type_of_aux subst' metasenv' context te ugraph1
353 let subst''',metasenv''',ugraph3 =
354 fo_unif_subst subst'' context metasenv''
355 inferredty ty' ugraph2
357 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
360 enrich localization_tbl te'
363 CicMetaSubst.ppterm_in_context subst'' te'
364 context ^ " has type " ^
365 CicMetaSubst.ppterm_in_context subst'' inferredty
366 context ^ " but is here used with type " ^
367 CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
369 | C.Prod (name,s,t) ->
370 let carr t subst context = CicMetaSubst.apply_subst subst t in
371 let coerce_to_sort in_source tgt_sort t type_to_coerce
372 subst context metasenv uragph
374 if not !insert_coercions then
375 t,type_to_coerce,subst,metasenv,ugraph
377 let coercion_src = carr type_to_coerce subst context in
378 match coercion_src with
380 t,type_to_coerce,subst,metasenv,ugraph
381 | Cic.Meta _ as meta ->
382 t, meta, subst, metasenv, ugraph
383 | Cic.Cast _ as cast ->
384 t, cast, subst, metasenv, ugraph
386 let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
388 CoercGraph.look_for_coercion coercion_src coercion_tgt
391 | CoercGraph.NoCoercion
392 | CoercGraph.NotHandled _ ->
393 enrich localization_tbl t
396 CicMetaSubst.ppterm_in_context subst t context ^
397 " is not a type since it has type " ^
398 CicMetaSubst.ppterm_in_context
399 subst coercion_src context ^ " that is not a sort")))
400 | CoercGraph.NotMetaClosed ->
401 enrich localization_tbl t
404 CicMetaSubst.ppterm_in_context subst t context ^
405 " is not a type since it has type " ^
406 CicMetaSubst.ppterm_in_context
407 subst coercion_src context ^ " that is not a sort")))
408 | CoercGraph.SomeCoercion candidates ->
412 t subst metasenv context ugraph coercion_tgt)
418 enrich localization_tbl t
421 CicMetaSubst.ppterm_in_context
423 " is not a type since it has type " ^
424 CicMetaSubst.ppterm_in_context
425 subst coercion_src context ^
426 " that is not a sort"))))
428 let s',sort1,subst',metasenv',ugraph1 =
429 type_of_aux subst metasenv context s ugraph
431 let s',sort1,subst', metasenv',ugraph1 =
432 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
433 s' sort1 subst' context metasenv' ugraph1
435 let context_for_t = ((Some (name,(C.Decl s')))::context) in
436 let t',sort2,subst'',metasenv'',ugraph2 =
437 type_of_aux subst' metasenv'
438 context_for_t t ugraph1
440 let t',sort2,subst'',metasenv'',ugraph2 =
441 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
442 t' sort2 subst'' context_for_t metasenv'' ugraph2
444 let sop,subst''',metasenv''',ugraph3 =
445 sort_of_prod subst'' metasenv''
446 context (name,s') (sort1,sort2) ugraph2
448 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
449 | C.Lambda (n,s,t) ->
451 let s',sort1,subst',metasenv',ugraph1 =
452 type_of_aux subst metasenv context s ugraph in
453 let s',sort1,subst',metasenv',ugraph1 =
454 if not !insert_coercions then
455 s',sort1, subst', metasenv', ugraph1
457 match CicReduction.whd ~subst:subst' context sort1 with
458 | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
460 let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
462 CoercGraph.look_for_coercion coercion_src coercion_tgt
465 | CoercGraph.NoCoercion
466 | CoercGraph.NotHandled _ ->
467 enrich localization_tbl s'
470 CicMetaSubst.ppterm_in_context subst s' context ^
471 " is not a type since it has type " ^
472 CicMetaSubst.ppterm_in_context
473 subst coercion_src context ^ " that is not a sort")))
474 | CoercGraph.NotMetaClosed ->
475 enrich localization_tbl s'
478 CicMetaSubst.ppterm_in_context subst s' context ^
479 " is not a type since it has type " ^
480 CicMetaSubst.ppterm_in_context
481 subst coercion_src context ^ " that is not a sort")))
482 | CoercGraph.SomeCoercion candidates ->
486 s' subst' metasenv' context ugraph1 coercion_tgt)
492 enrich localization_tbl s'
495 CicMetaSubst.ppterm_in_context subst s' context ^
496 " is not a type since it has type " ^
497 CicMetaSubst.ppterm_in_context
498 subst coercion_src context ^
499 " that is not a sort")))
501 let context_for_t = ((Some (n,(C.Decl s')))::context) in
502 let t',type2,subst'',metasenv'',ugraph2 =
503 type_of_aux subst' metasenv' context_for_t t ugraph1
505 C.Lambda (n,s',t'),C.Prod (n,s',type2),
506 subst'',metasenv'',ugraph2
508 (* only to check if s is well-typed *)
509 let s',ty,subst',metasenv',ugraph1 =
510 type_of_aux subst metasenv context s ugraph
512 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
514 let t',inferredty,subst'',metasenv'',ugraph2 =
515 type_of_aux subst' metasenv'
516 context_for_t t ugraph1
518 (* One-step LetIn reduction.
519 * Even faster than the previous solution.
520 * Moreover the inferred type is closer to the expected one.
522 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
523 subst'',metasenv'',ugraph2
524 | C.Appl (he::((_::_) as tl)) ->
525 let he',hetype,subst',metasenv',ugraph1 =
526 type_of_aux subst metasenv context he ugraph
528 let tlbody_and_type,subst'',metasenv'',ugraph2 =
530 (fun x (res,subst,metasenv,ugraph) ->
531 let x',ty,subst',metasenv',ugraph1 =
532 type_of_aux subst metasenv context x ugraph
534 (x', ty)::res,subst',metasenv',ugraph1
535 ) tl ([],subst',metasenv',ugraph1)
537 let tl',applty,subst''',metasenv''',ugraph3 =
538 eat_prods true subst'' metasenv'' context
539 he' hetype tlbody_and_type ugraph2
541 avoid_double_coercion context
542 subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
543 | C.Appl _ -> assert false
544 | C.Const (uri,exp_named_subst) ->
545 let exp_named_subst',subst',metasenv',ugraph1 =
546 check_exp_named_subst subst metasenv context
547 exp_named_subst ugraph in
548 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
550 CicSubstitution.subst_vars exp_named_subst' ty_uri
552 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
553 | C.MutInd (uri,i,exp_named_subst) ->
554 let exp_named_subst',subst',metasenv',ugraph1 =
555 check_exp_named_subst subst metasenv context
556 exp_named_subst ugraph
558 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
560 CicSubstitution.subst_vars exp_named_subst' ty_uri in
561 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
562 | C.MutConstruct (uri,i,j,exp_named_subst) ->
563 let exp_named_subst',subst',metasenv',ugraph1 =
564 check_exp_named_subst subst metasenv context
565 exp_named_subst ugraph
568 type_of_mutual_inductive_constr uri i j ugraph1
571 CicSubstitution.subst_vars exp_named_subst' ty_uri
573 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
575 | C.MutCase (uri, i, outtype, term, pl) ->
576 (* first, get the inductive type (and noparams)
577 * in the environment *)
578 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
579 let _ = CicTypeChecker.typecheck uri in
580 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
582 C.InductiveDefinition (l,expl_params,parsno,_) ->
583 List.nth l i , expl_params, parsno, u
585 enrich localization_tbl t
587 (lazy ("Unkown mutual inductive definition " ^
588 U.string_of_uri uri)))
590 let rec count_prod t =
591 match CicReduction.whd ~subst context t with
592 C.Prod (_, _, t) -> 1 + (count_prod t)
595 let no_args = count_prod arity in
596 (* now, create a "generic" MutInd *)
597 let metasenv,left_args =
598 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
600 let metasenv,right_args =
601 let no_right_params = no_args - no_left_params in
602 if no_right_params < 0 then assert false
603 else CicMkImplicit.n_fresh_metas
604 metasenv subst context no_right_params
606 let metasenv,exp_named_subst =
607 CicMkImplicit.fresh_subst metasenv subst context expl_params in
610 C.MutInd (uri,i,exp_named_subst)
613 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
615 (* check consistency with the actual type of term *)
616 let term',actual_type,subst,metasenv,ugraph1 =
617 type_of_aux subst metasenv context term ugraph in
618 let expected_type',_, subst, metasenv,ugraph2 =
619 type_of_aux subst metasenv context expected_type ugraph1
621 let actual_type = CicReduction.whd ~subst context actual_type in
622 let subst,metasenv,ugraph3 =
624 fo_unif_subst subst context metasenv
625 expected_type' actual_type ugraph2
628 enrich localization_tbl term' exn
631 CicMetaSubst.ppterm_in_context subst term'
632 context ^ " has type " ^
633 CicMetaSubst.ppterm_in_context subst actual_type
634 context ^ " but is here used with type " ^
635 CicMetaSubst.ppterm_in_context subst expected_type' context))
637 let rec instantiate_prod t =
641 match CicReduction.whd ~subst context t with
643 instantiate_prod (CicSubstitution.subst he t') tl
646 let arity_instantiated_with_left_args =
647 instantiate_prod arity left_args in
648 (* TODO: check if the sort elimination
649 * is allowed: [(I q1 ... qr)|B] *)
650 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
652 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
654 if left_args = [] then
655 (C.MutConstruct (uri,i,j,exp_named_subst))
658 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
660 let p',actual_type,subst,metasenv,ugraph1 =
661 type_of_aux subst metasenv context p ugraph
663 let constructor',expected_type, subst, metasenv,ugraph2 =
664 type_of_aux subst metasenv context constructor ugraph1
666 let outtypeinstance,subst,metasenv,ugraph3 =
667 check_branch 0 context metasenv subst no_left_params
668 actual_type constructor' expected_type ugraph2
671 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
672 ([],1,[],subst,metasenv,ugraph3) pl
675 (* we are left to check that the outype matches his instances.
676 The easy case is when the outype is specified, that amount
677 to a trivial check. Otherwise, we should guess a type from
681 let outtype,outtypety, subst, metasenv,ugraph4 =
682 type_of_aux subst metasenv context outtype ugraph4 in
685 (let candidate,ugraph5,metasenv,subst =
686 let exp_name_subst, metasenv =
688 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
690 let uris = CicUtil.params_of_obj o in
692 fun uri (acc,metasenv) ->
693 let metasenv',new_meta =
694 CicMkImplicit.mk_implicit metasenv subst context
697 CicMkImplicit.identity_relocation_list_for_metavariable
700 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
704 match left_args,right_args with
705 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
707 let rec mk_right_args =
710 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
712 let right_args_no = List.length right_args in
713 let lifted_left_args =
714 List.map (CicSubstitution.lift right_args_no) left_args
716 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
717 (lifted_left_args @ mk_right_args right_args_no))
720 FreshNamesGenerator.mk_fresh_name ~subst metasenv
721 context Cic.Anonymous ~typ:ty
723 match outtypeinstances with
725 let extended_context =
726 let rec add_right_args =
728 Cic.Prod (name,ty,t) ->
729 Some (name,Cic.Decl ty)::(add_right_args t)
732 (Some (fresh_name,Cic.Decl ty))::
734 (add_right_args arity_instantiated_with_left_args))@
737 let metasenv,new_meta =
738 CicMkImplicit.mk_implicit metasenv subst extended_context
741 CicMkImplicit.identity_relocation_list_for_metavariable
744 let rec add_lambdas b =
746 Cic.Prod (name,ty,t) ->
747 Cic.Lambda (name,ty,(add_lambdas b t))
748 | _ -> Cic.Lambda (fresh_name, ty, b)
751 add_lambdas (Cic.Meta (new_meta,irl))
752 arity_instantiated_with_left_args
754 (Some candidate),ugraph4,metasenv,subst
755 | (constructor_args_no,_,instance,_)::tl ->
757 let instance',subst,metasenv =
758 CicMetaSubst.delift_rels subst metasenv
759 constructor_args_no instance
761 let candidate,ugraph,metasenv,subst =
763 fun (candidate_oty,ugraph,metasenv,subst)
764 (constructor_args_no,_,instance,_) ->
765 match candidate_oty with
766 | None -> None,ugraph,metasenv,subst
769 let instance',subst,metasenv =
770 CicMetaSubst.delift_rels subst metasenv
771 constructor_args_no instance
773 let subst,metasenv,ugraph =
774 fo_unif_subst subst context metasenv
777 candidate_oty,ugraph,metasenv,subst
779 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
780 | CicUnification.UnificationFailure _
781 | CicUnification.Uncertain _ ->
782 None,ugraph,metasenv,subst
783 ) (Some instance',ugraph4,metasenv,subst) tl
786 | None -> None, ugraph,metasenv,subst
788 let rec add_lambdas n b =
790 Cic.Prod (name,ty,t) ->
791 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
793 Cic.Lambda (fresh_name, ty,
794 CicSubstitution.lift (n + 1) t)
797 (add_lambdas 0 t arity_instantiated_with_left_args),
798 ugraph,metasenv,subst
799 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
800 None,ugraph4,metasenv,subst
803 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
805 let subst,metasenv,ugraph =
807 fo_unif_subst subst context metasenv
808 candidate outtype ugraph5
810 exn -> assert false(* unification against a metavariable *)
812 C.MutCase (uri, i, outtype, term', pl'),
813 CicReduction.head_beta_reduce
814 (CicMetaSubst.apply_subst subst
815 (Cic.Appl (outtype::right_args@[term']))),
816 subst,metasenv,ugraph)
817 | _ -> (* easy case *)
818 let tlbody_and_type,subst,metasenv,ugraph4 =
820 (fun x (res,subst,metasenv,ugraph) ->
821 let x',ty,subst',metasenv',ugraph1 =
822 type_of_aux subst metasenv context x ugraph
824 (x', ty)::res,subst',metasenv',ugraph1
825 ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
827 let _,_,subst,metasenv,ugraph4 =
828 eat_prods false subst metasenv context
829 outtype outtypety tlbody_and_type ugraph4
831 let _,_, subst, metasenv,ugraph5 =
832 type_of_aux subst metasenv context
833 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
835 let (subst,metasenv,ugraph6) =
837 (fun (subst,metasenv,ugraph)
838 p (constructor_args_no,context,instance,args)
843 CicSubstitution.lift constructor_args_no outtype
845 C.Appl (outtype'::args)
847 CicReduction.whd ~subst context appl
850 fo_unif_subst subst context metasenv instance instance'
854 enrich localization_tbl p exn
857 CicMetaSubst.ppterm_in_context subst p
858 context ^ " has type " ^
859 CicMetaSubst.ppterm_in_context subst instance'
860 context ^ " but is here used with type " ^
861 CicMetaSubst.ppterm_in_context subst instance
863 (subst,metasenv,ugraph5) pl' outtypeinstances
865 C.MutCase (uri, i, outtype, term', pl'),
866 CicReduction.head_beta_reduce
867 (CicMetaSubst.apply_subst subst
868 (C.Appl(outtype::right_args@[term]))),
869 subst,metasenv,ugraph6)
871 let fl_ty',subst,metasenv,types,ugraph1 =
873 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
874 let ty',_,subst',metasenv',ugraph1 =
875 type_of_aux subst metasenv context ty ugraph
877 fl @ [ty'],subst',metasenv',
878 Some (C.Name n,(C.Decl ty')) :: types, ugraph
879 ) ([],subst,metasenv,[],ugraph) fl
881 let len = List.length types in
882 let context' = types@context in
883 let fl_bo',subst,metasenv,ugraph2 =
885 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
886 let bo',ty_of_bo,subst,metasenv,ugraph1 =
887 type_of_aux subst metasenv context' bo ugraph in
888 let expected_ty = CicSubstitution.lift len ty in
889 let subst',metasenv',ugraph' =
891 fo_unif_subst subst context' metasenv
892 ty_of_bo expected_ty ugraph1
895 enrich localization_tbl bo exn
898 CicMetaSubst.ppterm_in_context subst bo
899 context' ^ " has type " ^
900 CicMetaSubst.ppterm_in_context subst ty_of_bo
901 context' ^ " but is here used with type " ^
902 CicMetaSubst.ppterm_in_context subst expected_ty
905 fl @ [bo'] , subst',metasenv',ugraph'
906 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
908 let ty = List.nth fl_ty' i in
909 (* now we have the new ty in fl_ty', the new bo in fl_bo',
910 * and we want the new fl with bo' and ty' injected in the right
913 let rec map3 f l1 l2 l3 =
916 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
919 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
922 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
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, ugraph1
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,_,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,ty,bo) -> (name,ty',bo') )
975 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
977 relocalize localization_tbl t t';
980 (* check_metasenv_consistency checks that the "canonical" context of a
981 metavariable is consitent - up to relocation via the relocation list l -
982 with the actual context *)
983 and check_metasenv_consistency
984 metano subst metasenv context canonical_context l ugraph
986 let module C = Cic in
987 let module R = CicReduction in
988 let module S = CicSubstitution in
989 let lifted_canonical_context =
993 | (Some (n,C.Decl t))::tl ->
994 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
995 | (Some (n,C.Def (t,None)))::tl ->
996 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
997 | None::tl -> None::(aux (i+1) tl)
998 | (Some (n,C.Def (t,Some ty)))::tl ->
1000 C.Def ((S.subst_meta l (S.lift i t)),
1001 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
1003 aux 1 canonical_context
1007 (fun (l,subst,metasenv,ugraph) t ct ->
1010 l @ [None],subst,metasenv,ugraph
1011 | Some t,Some (_,C.Def (ct,_)) ->
1012 let subst',metasenv',ugraph' =
1014 fo_unif_subst subst context metasenv t ct ugraph
1015 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))))))
1017 l @ [Some t],subst',metasenv',ugraph'
1018 | Some t,Some (_,C.Decl ct) ->
1019 let t',inferredty,subst',metasenv',ugraph1 =
1020 type_of_aux subst metasenv context t ugraph
1022 let subst'',metasenv'',ugraph2 =
1025 subst' context metasenv' inferredty ct ugraph1
1026 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))))))
1028 l @ [Some t'], subst'',metasenv'',ugraph2
1030 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
1032 Invalid_argument _ ->
1036 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1037 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
1038 (CicMetaSubst.ppcontext subst canonical_context))))
1040 and check_exp_named_subst metasubst metasenv context tl ugraph =
1041 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1043 [] -> [],metasubst,metasenv,ugraph
1045 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1047 CicSubstitution.subst_vars substs ty_uri in
1048 (* CSC: why was this code here? it is wrong
1049 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1050 Cic.Variable (_,Some bo,_,_) ->
1052 (RefineFailure (lazy
1053 "A variable with a body can not be explicit substituted"))
1054 | Cic.Variable (_,None,_,_) -> ()
1057 (RefineFailure (lazy
1058 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1061 let t',typeoft,metasubst',metasenv',ugraph2 =
1062 type_of_aux metasubst metasenv context t ugraph1 in
1063 let subst = uri,t' in
1064 let metasubst'',metasenv'',ugraph3 =
1067 metasubst' context metasenv' typeoft typeofvar ugraph2
1069 raise (RefineFailure (lazy
1070 ("Wrong Explicit Named Substitution: " ^
1071 CicMetaSubst.ppterm metasubst' typeoft ^
1072 " not unifiable with " ^
1073 CicMetaSubst.ppterm metasubst' typeofvar)))
1075 (* FIXME: no mere tail recursive! *)
1076 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1077 check_exp_named_subst_aux
1078 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1080 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1082 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1085 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
1086 let module C = Cic in
1087 let context_for_t2 = (Some (name,C.Decl s))::context in
1088 let t1'' = CicReduction.whd ~subst context t1 in
1089 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1090 match (t1'', t2'') with
1091 (C.Sort s1, C.Sort s2)
1092 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1093 (* different than Coq manual!!! *)
1094 C.Sort s2,subst,metasenv,ugraph
1095 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1096 let t' = CicUniv.fresh() in
1097 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1098 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1099 C.Sort (C.Type t'),subst,metasenv,ugraph2
1100 | (C.Sort _,C.Sort (C.Type t1)) ->
1101 C.Sort (C.Type t1),subst,metasenv,ugraph
1102 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1103 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1104 (* TODO how can we force the meta to become a sort? If we don't we
1105 * break the invariant that refine produce only well typed terms *)
1106 (* TODO if we check the non meta term and if it is a sort then we
1107 * are likely to know the exact value of the result e.g. if the rhs
1108 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1109 let (metasenv,idx) =
1110 CicMkImplicit.mk_implicit_sort metasenv subst in
1111 let (subst, metasenv,ugraph1) =
1113 fo_unif_subst subst context_for_t2 metasenv
1114 (C.Meta (idx,[])) t2'' ugraph
1115 with _ -> assert false (* unification against a metavariable *)
1117 t2'',subst,metasenv,ugraph1
1123 ("Two sorts were expected, found %s " ^^
1124 "(that reduces to %s) and %s (that reduces to %s)")
1125 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
1126 (CicPp.ppterm t2''))))
1128 and avoid_double_coercion context subst metasenv ugraph t ty =
1129 let b, c1, c2, head = is_a_double_coercion t in
1131 let source_carr = CoercGraph.source_of c2 in
1132 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1133 (match CoercGraph.look_for_coercion source_carr tgt_carr
1135 | CoercGraph.SomeCoercion candidates ->
1137 HExtlib.list_findopt
1141 | Cic.Appl l -> Cic.Appl (l @ [head])
1142 | _ -> Cic.Appl [c;head]
1145 let newt,_,subst,metasenv,ugraph =
1146 type_of_aux subst metasenv context newt ugraph in
1147 let subst, metasenv, ugraph =
1148 fo_unif_subst subst context metasenv newt t ugraph
1153 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
1154 Some (newt, ty, subst, metasenv, ugraph)
1155 with RefineFailure _ | Uncertain _ -> None))
1158 (match selected with
1161 prerr_endline ("#### Coercion not packed: " ^ CicPp.ppterm t);
1163 | _ -> assert false) (* the composite coercion must exist *)
1165 t, ty, subst, metasenv, ugraph
1168 allow_coercions subst metasenv context he hetype tlbody_and_type ugraph
1170 let rec mk_prod metasenv context' =
1173 let (metasenv, idx) =
1174 CicMkImplicit.mk_implicit_type metasenv subst context'
1177 CicMkImplicit.identity_relocation_list_for_metavariable context'
1179 metasenv,Cic.Meta (idx, irl)
1181 let (metasenv, idx) =
1182 CicMkImplicit.mk_implicit_type metasenv subst context'
1185 CicMkImplicit.identity_relocation_list_for_metavariable context'
1187 let meta = Cic.Meta (idx,irl) in
1189 (* The name must be fresh for context. *)
1190 (* Nevertheless, argty is well-typed only in context. *)
1191 (* Thus I generate a name (name_hint) in context and *)
1192 (* then I generate a name --- using the hint name_hint *)
1193 (* --- that is fresh in context'. *)
1195 (* Cic.Name "pippo" *)
1196 FreshNamesGenerator.mk_fresh_name ~subst metasenv
1197 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
1198 (CicMetaSubst.apply_subst_context subst context)
1200 ~typ:(CicMetaSubst.apply_subst subst argty)
1202 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
1203 FreshNamesGenerator.mk_fresh_name ~subst
1204 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
1206 let metasenv,target =
1207 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
1209 metasenv,Cic.Prod (name,meta,target)
1211 let ((subst,metasenv,ugraph1),hetype') =
1212 if CicUtil.is_meta_closed hetype then
1213 (subst,metasenv,ugraph),hetype
1215 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
1217 fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph, hetype'
1219 enrich localization_tbl he
1221 (lazy ("The term " ^
1222 CicMetaSubst.ppterm_in_context subst he
1223 context ^ " (that has type " ^
1224 CicMetaSubst.ppterm_in_context subst hetype
1225 context ^ ") is here applied to " ^
1226 string_of_int (List.length tlbody_and_type) ^
1227 " arguments that are more than expected"
1228 (* "\nReason: " ^ Lazy.force exn*)))) exn
1230 let rec eat_prods metasenv subst context hetype ugraph =
1232 | [] -> [],metasenv,subst,hetype,ugraph
1233 | (hete, hety)::tl ->
1234 (match (CicReduction.whd ~subst context hetype) with
1236 let arg,subst,metasenv,ugraph1 =
1238 let subst,metasenv,ugraph1 =
1239 fo_unif_subst_eat_prods2 subst context metasenv hety s ugraph
1241 hete,subst,metasenv,ugraph1
1242 with exn when allow_coercions && !insert_coercions ->
1243 (* we search a coercion from hety to s *)
1244 let coer, tgt_carr =
1245 let carr t subst context =
1246 CicReduction.whd ~delta:false
1247 context (CicMetaSubst.apply_subst subst t )
1249 let c_hety = carr hety subst context in
1250 let c_s = carr s subst context in
1251 CoercGraph.look_for_coercion c_hety c_s, c_s
1254 | CoercGraph.NoCoercion
1255 | CoercGraph.NotHandled _ ->
1256 enrich localization_tbl hete
1258 (lazy ("The term " ^
1259 CicMetaSubst.ppterm_in_context subst hete
1260 context ^ " has type " ^
1261 CicMetaSubst.ppterm_in_context subst hety
1262 context ^ " but is here used with type " ^
1263 CicMetaSubst.ppterm_in_context subst s context
1264 (* "\nReason: " ^ Lazy.force e*))))
1265 | CoercGraph.NotMetaClosed ->
1266 enrich localization_tbl hete
1268 (lazy ("The term " ^
1269 CicMetaSubst.ppterm_in_context subst hete
1270 context ^ " has type " ^
1271 CicMetaSubst.ppterm_in_context subst hety
1272 context ^ " but is here used with type " ^
1273 CicMetaSubst.ppterm_in_context subst s context
1274 (* "\nReason: " ^ Lazy.force e*))))
1275 | CoercGraph.SomeCoercion candidates ->
1277 HExtlib.list_findopt
1280 let t = Cic.Appl[c;hete] in
1281 let newt,newhety,subst,metasenv,ugraph =
1282 type_of_aux subst metasenv context
1285 let newt, _, subst, metasenv, ugraph =
1286 avoid_double_coercion context subst metasenv
1287 ugraph newt tgt_carr
1289 let subst,metasenv,ugraph1 =
1290 fo_unif_subst subst context metasenv
1293 Some (newt, subst, metasenv, ugraph)
1294 with Uncertain _ | RefineFailure _ -> None)
1297 (match selected with
1300 enrich localization_tbl hete
1302 (lazy ("The term " ^
1303 CicMetaSubst.ppterm_in_context subst hete
1304 context ^ " has type " ^
1305 CicMetaSubst.ppterm_in_context subst hety
1306 context ^ " but is here used with type " ^
1307 CicMetaSubst.ppterm_in_context subst s context
1308 (* "\nReason: " ^ Lazy.force e*)))) exn))
1310 enrich localization_tbl hete
1312 (lazy ("The term " ^
1313 CicMetaSubst.ppterm_in_context subst hete
1314 context ^ " has type " ^
1315 CicMetaSubst.ppterm_in_context subst hety
1316 context ^ " but is here used with type " ^
1317 CicMetaSubst.ppterm_in_context subst s context
1318 (* "\nReason: " ^ Lazy.force e*)))) exn
1320 let coerced_args,metasenv',subst',t',ugraph2 =
1321 eat_prods metasenv subst context
1322 (CicSubstitution.subst arg t) ugraph1 tl
1324 arg::coerced_args,metasenv',subst',t',ugraph2
1326 raise (RefineFailure
1327 (lazy ("The term " ^
1328 CicMetaSubst.ppterm_in_context subst he
1329 context ^ " (that has type " ^
1330 CicMetaSubst.ppterm_in_context subst hetype'
1331 context ^ ") is here applied to " ^
1332 string_of_int (List.length tlbody_and_type) ^
1333 " arguments that are more than expected"))))
1335 let coerced_args,metasenv,subst,t,ugraph2 =
1336 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
1338 coerced_args,t,subst,metasenv,ugraph2
1341 (* eat prods ends here! *)
1343 let t',ty,subst',metasenv',ugraph1 =
1344 type_of_aux [] metasenv context t ugraph
1346 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1347 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1348 (* Andrea: ho rimesso qui l'applicazione della subst al
1349 metasenv dopo che ho droppato l'invariante che il metsaenv
1350 e' sempre istanziato *)
1351 let substituted_metasenv =
1352 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1354 (* substituted_t,substituted_ty,substituted_metasenv *)
1355 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1357 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1359 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1360 let cleaned_metasenv =
1362 (function (n,context,ty) ->
1363 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1368 | Some (n, Cic.Decl t) ->
1370 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1371 | Some (n, Cic.Def (bo,ty)) ->
1372 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1377 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1379 Some (n, Cic.Def (bo',ty'))
1383 ) substituted_metasenv
1385 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1388 let undebrujin uri typesno tys t =
1391 (fun (name,_,_,_) (i,t) ->
1392 (* here the explicit_named_substituion is assumed to be *)
1394 let t' = Cic.MutInd (uri,i,[]) in
1395 let t = CicSubstitution.subst t' t in
1397 ) tys (typesno - 1,t))
1399 let map_first_n n start f g l =
1400 let rec aux acc k l =
1403 | [] -> raise (Invalid_argument "map_first_n")
1404 | hd :: tl -> f hd k (aux acc (k+1) tl)
1410 (*CSC: this is a very rough approximation; to be finished *)
1411 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1412 let subst,metasenv,ugraph,tys =
1414 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1415 let subst,metasenv,ugraph,cl =
1417 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1418 let rec aux ctx k subst = function
1419 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1420 let subst,metasenv,ugraph,tl =
1422 (subst,metasenv,ugraph,[])
1423 (fun t n (subst,metasenv,ugraph,acc) ->
1424 let subst,metasenv,ugraph =
1426 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1428 subst,metasenv,ugraph,(t::acc))
1429 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1432 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1433 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1434 subst,metasenv,ugraph,t
1435 | Cic.Prod (name,s,t) ->
1436 let ctx = (Some (name,Cic.Decl s))::ctx in
1437 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1438 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1442 (lazy "not well formed constructor type"))
1444 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1445 subst,metasenv,ugraph,(name,ty) :: acc)
1446 cl (subst,metasenv,ugraph,[])
1448 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1449 tys ([],metasenv,ugraph,[])
1451 let substituted_tys =
1453 (fun (name,ind,arity,cl) ->
1455 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1457 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1460 metasenv,ugraph,substituted_tys
1462 let typecheck metasenv uri obj ~localization_tbl =
1463 let ugraph = CicUniv.empty_ugraph in
1465 Cic.Constant (name,Some bo,ty,args,attrs) ->
1466 let bo',boty,metasenv,ugraph =
1467 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1468 let ty',_,metasenv,ugraph =
1469 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1470 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1471 let bo' = CicMetaSubst.apply_subst subst bo' in
1472 let ty' = CicMetaSubst.apply_subst subst ty' in
1473 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1474 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1475 | Cic.Constant (name,None,ty,args,attrs) ->
1476 let ty',_,metasenv,ugraph =
1477 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1479 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1480 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1481 assert (metasenv' = metasenv);
1482 (* Here we do not check the metasenv for correctness *)
1483 let bo',boty,metasenv,ugraph =
1484 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1485 let ty',sort,metasenv,ugraph =
1486 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1490 (* instead of raising Uncertain, let's hope that the meta will become
1493 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1495 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1496 let bo' = CicMetaSubst.apply_subst subst bo' in
1497 let ty' = CicMetaSubst.apply_subst subst ty' in
1498 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1499 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1500 | Cic.Variable _ -> assert false (* not implemented *)
1501 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1502 (*CSC: this code is greately simplified and many many checks are missing *)
1503 (*CSC: e.g. the constructors are not required to build their own types, *)
1504 (*CSC: the arities are not required to have as type a sort, etc. *)
1505 let uri = match uri with Some uri -> uri | None -> assert false in
1506 let typesno = List.length tys in
1507 (* first phase: we fix only the types *)
1508 let metasenv,ugraph,tys =
1510 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1511 let ty',_,metasenv,ugraph =
1512 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1514 metasenv,ugraph,(name,b,ty',cl)::res
1515 ) tys (metasenv,ugraph,[]) in
1517 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1518 (* second phase: we fix only the constructors *)
1519 let metasenv,ugraph,tys =
1521 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1522 let metasenv,ugraph,cl' =
1524 (fun (name,ty) (metasenv,ugraph,res) ->
1526 CicTypeChecker.debrujin_constructor
1527 ~cb:(relocalize localization_tbl) uri typesno ty in
1528 let ty',_,metasenv,ugraph =
1529 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1530 let ty' = undebrujin uri typesno tys ty' in
1531 metasenv,ugraph,(name,ty')::res
1532 ) cl (metasenv,ugraph,[])
1534 metasenv,ugraph,(name,b,ty,cl')::res
1535 ) tys (metasenv,ugraph,[]) in
1536 (* third phase: we check the positivity condition *)
1537 let metasenv,ugraph,tys =
1538 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1540 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1543 (* sara' piu' veloce che raffinare da zero? mah.... *)
1544 let pack_coercion metasenv ctx t =
1545 let module C = Cic in
1546 let rec merge_coercions ctx =
1547 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1549 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1550 | C.Meta (n,subst) ->
1553 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1556 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1557 | C.Prod (name,so,dest) ->
1558 let ctx' = (Some (name,C.Decl so))::ctx in
1559 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1560 | C.Lambda (name,so,dest) ->
1561 let ctx' = (Some (name,C.Decl so))::ctx in
1562 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1563 | C.LetIn (name,so,dest) ->
1564 let ctx' = Some (name,(C.Def (so,None)))::ctx in
1565 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1567 let l = List.map (merge_coercions ctx) l in
1569 let b,_,_,_ = is_a_double_coercion t in
1570 (* prerr_endline "CANDIDATO!!!!"; *)
1572 let ugraph = CicUniv.empty_ugraph in
1573 let old_insert_coercions = !insert_coercions in
1574 insert_coercions := false;
1575 let newt, _, menv, _ =
1577 type_of_aux' metasenv ctx t ugraph
1578 with RefineFailure _ | Uncertain _ ->
1579 prerr_endline (CicPp.ppterm t);
1582 insert_coercions := old_insert_coercions;
1583 if metasenv <> [] || menv = [] then
1586 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1589 | C.Var (uri,exp_named_subst) ->
1590 let exp_named_subst = List.map aux exp_named_subst in
1591 C.Var (uri, exp_named_subst)
1592 | C.Const (uri,exp_named_subst) ->
1593 let exp_named_subst = List.map aux exp_named_subst in
1594 C.Const (uri, exp_named_subst)
1595 | C.MutInd (uri,tyno,exp_named_subst) ->
1596 let exp_named_subst = List.map aux exp_named_subst in
1597 C.MutInd (uri,tyno,exp_named_subst)
1598 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1599 let exp_named_subst = List.map aux exp_named_subst in
1600 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1601 | C.MutCase (uri,tyno,out,te,pl) ->
1602 let pl = List.map (merge_coercions ctx) pl in
1603 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1604 | C.Fix (fno, fl) ->
1607 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1612 (fun (name,idx,ty,bo) ->
1613 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1617 | C.CoFix (fno, fl) ->
1620 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1625 (fun (name,ty,bo) ->
1626 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1631 merge_coercions ctx t
1634 let pack_coercion_obj obj =
1635 let module C = Cic in
1637 | C.Constant (id, body, ty, params, attrs) ->
1641 | Some body -> Some (pack_coercion [] [] body)
1643 let ty = pack_coercion [] [] ty in
1644 C.Constant (id, body, ty, params, attrs)
1645 | C.Variable (name, body, ty, params, attrs) ->
1649 | Some body -> Some (pack_coercion [] [] body)
1651 let ty = pack_coercion [] [] ty in
1652 C.Variable (name, body, ty, params, attrs)
1653 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1656 (fun (i, ctx, ty) ->
1662 Some (name, C.Decl t) ->
1663 Some (name, C.Decl (pack_coercion conjectures ctx t))
1664 | Some (name, C.Def (t,None)) ->
1665 Some (name,C.Def (pack_coercion conjectures ctx t,None))
1666 | Some (name, C.Def (t,Some ty)) ->
1667 Some (name, C.Def (pack_coercion conjectures ctx t,
1668 Some (pack_coercion conjectures ctx ty)))
1674 ((i,ctx,pack_coercion conjectures ctx ty))
1677 let body = pack_coercion conjectures [] body in
1678 let ty = pack_coercion conjectures [] ty in
1679 C.CurrentProof (name, conjectures, body, ty, params, attrs)
1680 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1683 (fun (name, ind, arity, cl) ->
1684 let arity = pack_coercion [] [] arity in
1686 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
1688 (name, ind, arity, cl))
1691 C.InductiveDefinition (indtys, params, leftno, attrs)
1696 let type_of_aux' metasenv context term =
1699 type_of_aux' metasenv context term in
1701 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1703 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1706 | RefineFailure msg as e ->
1707 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1709 | Uncertain msg as e ->
1710 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1714 let profiler2 = HExtlib.profile "CicRefine"
1716 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1717 profiler2.HExtlib.profile
1718 (type_of_aux' ?localization_tbl metasenv context term) ugraph
1720 let typecheck ~localization_tbl metasenv uri obj =
1721 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
1723 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;