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
40 if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());;
42 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
44 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
47 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
48 in profiler_eat_prods2.HExtlib.profile foo ()
50 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
51 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
54 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
56 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
59 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
60 in profiler_eat_prods.HExtlib.profile foo ()
62 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
63 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
66 let profiler = HExtlib.profile "CicRefine.fo_unif"
68 let fo_unif_subst subst context metasenv t1 t2 ugraph =
71 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
72 in profiler.HExtlib.profile foo ()
74 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
75 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
78 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
81 RefineFailure msg -> RefineFailure (f msg)
82 | Uncertain msg -> Uncertain (f msg)
83 | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
84 | Sys.Break -> raise exn
85 | _ -> prerr_endline (Printexc.to_string exn); assert false
89 Cic.CicHash.find localization_tbl t
91 prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
94 raise (HExtlib.Localized (loc,exn'))
96 let relocalize localization_tbl oldt newt =
98 let infos = Cic.CicHash.find localization_tbl oldt in
99 Cic.CicHash.remove localization_tbl oldt;
100 Cic.CicHash.add localization_tbl newt infos;
108 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
109 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
112 let exp_impl metasenv subst context =
115 let (metasenv', idx) =
116 CicMkImplicit.mk_implicit_type metasenv subst context in
118 CicMkImplicit.identity_relocation_list_for_metavariable context in
119 metasenv', Cic.Meta (idx, irl)
121 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
122 metasenv', Cic.Meta (idx, [])
124 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
126 CicMkImplicit.identity_relocation_list_for_metavariable context in
127 metasenv', Cic.Meta (idx, irl)
131 let is_a_double_coercion t =
133 let rec aux acc = function
135 | x::tl -> aux (acc@[x]) tl
140 let imp = Cic.Implicit None in
141 let dummyres = false,imp, imp,imp,imp in
143 | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
144 (match last_of tl with
145 | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
146 let sib2,head = last_of tl2 in
147 true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
152 let more_args_than_expected
153 localization_tbl metasenv subst he context hetype' tlbody_and_type exn
157 CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
158 " (that has type "^CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
159 ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
160 " arguments that are more than expected")
162 enrich localization_tbl he ~f:(fun _-> msg) exn
165 let mk_prod_of_metas metasenv context' subst args =
166 let rec mk_prod metasenv context' = function
168 let (metasenv, idx) =
169 CicMkImplicit.mk_implicit_type metasenv subst context'
172 CicMkImplicit.identity_relocation_list_for_metavariable context'
174 metasenv,Cic.Meta (idx, irl)
176 let (metasenv, idx) =
177 CicMkImplicit.mk_implicit_type metasenv subst context'
180 CicMkImplicit.identity_relocation_list_for_metavariable context'
182 let meta = Cic.Meta (idx,irl) in
184 (* The name must be fresh for context. *)
185 (* Nevertheless, argty is well-typed only in context. *)
186 (* Thus I generate a name (name_hint) in context and *)
187 (* then I generate a name --- using the hint name_hint *)
188 (* --- that is fresh in context'. *)
190 (* Cic.Name "pippo" *)
191 FreshNamesGenerator.mk_fresh_name ~subst metasenv
192 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
193 (CicMetaSubst.apply_subst_context subst context')
195 ~typ:(CicMetaSubst.apply_subst subst argty)
197 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
198 FreshNamesGenerator.mk_fresh_name ~subst
199 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
201 let metasenv,target =
202 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
204 metasenv,Cic.Prod (name,meta,target)
206 mk_prod metasenv context' args
209 let rec type_of_constant uri ugraph =
210 let module C = Cic in
211 let module R = CicReduction in
212 let module U = UriManager in
213 let _ = CicTypeChecker.typecheck uri in
216 CicEnvironment.get_cooked_obj ugraph uri
217 with Not_found -> assert false
220 C.Constant (_,_,ty,_,_) -> ty,u
221 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
225 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
227 and type_of_variable uri ugraph =
228 let module C = Cic in
229 let module R = CicReduction in
230 let module U = UriManager in
231 let _ = CicTypeChecker.typecheck uri in
234 CicEnvironment.get_cooked_obj ugraph uri
235 with Not_found -> assert false
238 C.Variable (_,_,ty,_,_) -> ty,u
242 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
244 and type_of_mutual_inductive_defs uri i ugraph =
245 let module C = Cic in
246 let module R = CicReduction in
247 let module U = UriManager in
248 let _ = CicTypeChecker.typecheck uri in
251 CicEnvironment.get_cooked_obj ugraph uri
252 with Not_found -> assert false
255 C.InductiveDefinition (dl,_,_,_) ->
256 let (_,_,arity,_) = List.nth dl i in
261 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
263 and type_of_mutual_inductive_constr uri i j ugraph =
264 let module C = Cic in
265 let module R = CicReduction in
266 let module U = UriManager in
267 let _ = CicTypeChecker.typecheck uri in
270 CicEnvironment.get_cooked_obj ugraph uri
271 with Not_found -> assert false
274 C.InductiveDefinition (dl,_,_,_) ->
275 let (_,_,_,cl) = List.nth dl i in
276 let (_,ty) = List.nth cl (j-1) in
282 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
285 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
287 (* the check_branch function checks if a branch of a case is refinable.
288 It returns a pair (outype_instance,args), a subst and a metasenv.
289 outype_instance is the expected result of applying the case outtype
291 The problem is that outype is in general unknown, and we should
292 try to synthesize it from the above information, that is in general
293 a second order unification problem. *)
295 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
296 let module C = Cic in
297 (* let module R = CicMetaSubst in *)
298 let module R = CicReduction in
299 match R.whd ~subst context expectedtype with
301 (n,context,actualtype, [term]), subst, metasenv, ugraph
302 | C.Appl (C.MutInd (_,_,_)::tl) ->
303 let (_,arguments) = split tl left_args_no in
304 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
305 | C.Prod (name,so,de) ->
306 (* we expect that the actual type of the branch has the due
308 (match R.whd ~subst context actualtype with
309 C.Prod (name',so',de') ->
310 let subst, metasenv, ugraph1 =
311 fo_unif_subst subst context metasenv so so' ugraph in
313 (match CicSubstitution.lift 1 term with
314 C.Appl l -> C.Appl (l@[C.Rel 1])
315 | t -> C.Appl [t ; C.Rel 1]) in
316 (* we should also check that the name variable is anonymous in
317 the actual type de' ?? *)
319 ((Some (name,(C.Decl so)))::context)
320 metasenv subst left_args_no de' term' de ugraph1
321 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
322 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
324 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
327 let rec type_of_aux subst metasenv context t ugraph =
328 let module C = Cic in
329 let module S = CicSubstitution in
330 let module U = UriManager in
332 let try_coercion t subst context ugraph coercion_tgt (metasenv,last,coerced) =
333 let subst,metasenv,ugraph =
334 fo_unif_subst subst context metasenv last t ugraph
337 let newt, tty, subst, metasenv, ugraph =
338 avoid_double_coercion context subst metasenv ugraph coerced
341 Some (newt, tty, subst, metasenv, ugraph)
343 | RefineFailure _ | Uncertain _ -> None
346 let (t',_,_,_,_) as res =
351 match List.nth context (n - 1) with
352 Some (_,C.Decl ty) ->
353 t,S.lift n ty,subst,metasenv, ugraph
354 | Some (_,C.Def (_,Some ty)) ->
355 t,S.lift n ty,subst,metasenv, ugraph
356 | Some (_,C.Def (bo,None)) ->
358 (* if it is in the context it must be already well-typed*)
359 CicTypeChecker.type_of_aux' ~subst metasenv context
362 t,ty,subst,metasenv,ugraph
364 enrich localization_tbl t
365 (RefineFailure (lazy "Rel to hidden hypothesis"))
368 enrich localization_tbl t
369 (RefineFailure (lazy "Not a closed term")))
370 | C.Var (uri,exp_named_subst) ->
371 let exp_named_subst',subst',metasenv',ugraph1 =
372 check_exp_named_subst
373 subst metasenv context exp_named_subst ugraph
375 let ty_uri,ugraph1 = type_of_variable uri ugraph in
377 CicSubstitution.subst_vars exp_named_subst' ty_uri
379 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
382 let (canonical_context, term,ty) =
383 CicUtil.lookup_subst n subst
385 let l',subst',metasenv',ugraph1 =
386 check_metasenv_consistency n subst metasenv context
387 canonical_context l ugraph
389 (* trust or check ??? *)
390 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
391 subst', metasenv', ugraph1
392 (* type_of_aux subst metasenv
393 context (CicSubstitution.subst_meta l term) *)
394 with CicUtil.Subst_not_found _ ->
395 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
396 let l',subst',metasenv', ugraph1 =
397 check_metasenv_consistency n subst metasenv context
398 canonical_context l ugraph
400 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
401 subst', metasenv',ugraph1)
402 | C.Sort (C.Type tno) ->
403 let tno' = CicUniv.fresh() in
405 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
406 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
408 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
410 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
411 | C.Implicit infos ->
412 let metasenv',t' = exp_impl metasenv subst context infos in
413 type_of_aux subst metasenv' context t' ugraph
415 let ty',_,subst',metasenv',ugraph1 =
416 type_of_aux subst metasenv context ty ugraph
418 let te',inferredty,subst'',metasenv'',ugraph2 =
419 type_of_aux subst' metasenv' context te ugraph1
421 let (te', ty'), subst''',metasenv''',ugraph3 =
422 coerce_to_something true localization_tbl te' inferredty ty'
423 subst'' metasenv'' context ugraph2
425 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
426 | C.Prod (name,s,t) ->
427 let s',sort1,subst',metasenv',ugraph1 =
428 type_of_aux subst metasenv context s ugraph
430 let s',sort1,subst', metasenv',ugraph1 =
431 coerce_to_sort localization_tbl
432 s' sort1 subst' context metasenv' ugraph1
434 let context_for_t = ((Some (name,(C.Decl s')))::context) in
435 let t',sort2,subst'',metasenv'',ugraph2 =
436 type_of_aux subst' metasenv'
437 context_for_t t ugraph1
439 let t',sort2,subst'',metasenv'',ugraph2 =
440 coerce_to_sort localization_tbl
441 t' sort2 subst'' context_for_t metasenv'' ugraph2
443 let sop,subst''',metasenv''',ugraph3 =
444 sort_of_prod localization_tbl subst'' metasenv''
445 context (name,s') t' (sort1,sort2) ugraph2
447 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
448 | C.Lambda (n,s,t) ->
449 let s',sort1,subst',metasenv',ugraph1 =
450 type_of_aux subst metasenv context s ugraph
452 let s',sort1,subst',metasenv',ugraph1 =
453 coerce_to_sort localization_tbl
454 s' sort1 subst' context metasenv' ugraph1
456 let context_for_t = ((Some (n,(C.Decl s')))::context) in
457 let t',type2,subst'',metasenv'',ugraph2 =
458 type_of_aux subst' metasenv' context_for_t t ugraph1
460 C.Lambda (n,s',t'),C.Prod (n,s',type2),
461 subst'',metasenv'',ugraph2
463 (* only to check if s is well-typed *)
464 let s',ty,subst',metasenv',ugraph1 =
465 type_of_aux subst metasenv context s ugraph
467 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
469 let t',inferredty,subst'',metasenv'',ugraph2 =
470 type_of_aux subst' metasenv'
471 context_for_t t ugraph1
473 (* One-step LetIn reduction.
474 * Even faster than the previous solution.
475 * Moreover the inferred type is closer to the expected one.
478 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
479 subst'',metasenv'',ugraph2
480 | C.Appl (he::((_::_) as tl)) ->
481 let he',hetype,subst',metasenv',ugraph1 =
482 type_of_aux subst metasenv context he ugraph
484 let tlbody_and_type,subst'',metasenv'',ugraph2 =
485 typeof_list subst' metasenv' context ugraph1 tl
487 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
488 eat_prods true subst'' metasenv'' context
489 he' hetype tlbody_and_type ugraph2
491 let newappl = (C.Appl (coerced_he::coerced_args)) in
492 avoid_double_coercion
493 context subst''' metasenv''' ugraph3 newappl applty
494 | C.Appl _ -> assert false
495 | C.Const (uri,exp_named_subst) ->
496 let exp_named_subst',subst',metasenv',ugraph1 =
497 check_exp_named_subst subst metasenv context
498 exp_named_subst ugraph in
499 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
501 CicSubstitution.subst_vars exp_named_subst' ty_uri
503 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
504 | C.MutInd (uri,i,exp_named_subst) ->
505 let exp_named_subst',subst',metasenv',ugraph1 =
506 check_exp_named_subst subst metasenv context
507 exp_named_subst ugraph
509 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
511 CicSubstitution.subst_vars exp_named_subst' ty_uri in
512 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
513 | C.MutConstruct (uri,i,j,exp_named_subst) ->
514 let exp_named_subst',subst',metasenv',ugraph1 =
515 check_exp_named_subst subst metasenv context
516 exp_named_subst ugraph
519 type_of_mutual_inductive_constr uri i j ugraph1
522 CicSubstitution.subst_vars exp_named_subst' ty_uri
524 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
526 | C.MutCase (uri, i, outtype, term, pl) ->
527 (* first, get the inductive type (and noparams)
528 * in the environment *)
529 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
530 let _ = CicTypeChecker.typecheck uri in
531 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
533 C.InductiveDefinition (l,expl_params,parsno,_) ->
534 List.nth l i , expl_params, parsno, u
536 enrich localization_tbl t
538 (lazy ("Unkown mutual inductive definition " ^
539 U.string_of_uri uri)))
541 let rec count_prod t =
542 match CicReduction.whd ~subst context t with
543 C.Prod (_, _, t) -> 1 + (count_prod t)
546 let no_args = count_prod arity in
547 (* now, create a "generic" MutInd *)
548 let metasenv,left_args =
549 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
551 let metasenv,right_args =
552 let no_right_params = no_args - no_left_params in
553 if no_right_params < 0 then assert false
554 else CicMkImplicit.n_fresh_metas
555 metasenv subst context no_right_params
557 let metasenv,exp_named_subst =
558 CicMkImplicit.fresh_subst metasenv subst context expl_params in
561 C.MutInd (uri,i,exp_named_subst)
564 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
566 (* check consistency with the actual type of term *)
567 let term',actual_type,subst,metasenv,ugraph1 =
568 type_of_aux subst metasenv context term ugraph in
569 let expected_type',_, subst, metasenv,ugraph2 =
570 type_of_aux subst metasenv context expected_type ugraph1
572 let actual_type = CicReduction.whd ~subst context actual_type in
573 let subst,metasenv,ugraph3 =
575 fo_unif_subst subst context metasenv
576 expected_type' actual_type ugraph2
579 enrich localization_tbl term' exn
581 lazy ("(10)The term " ^
582 CicMetaSubst.ppterm_in_context ~metasenv subst term'
583 context ^ " has type " ^
584 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
585 context ^ " but is here used with type " ^
586 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
588 let rec instantiate_prod t =
592 match CicReduction.whd ~subst context t with
594 instantiate_prod (CicSubstitution.subst he t') tl
597 let arity_instantiated_with_left_args =
598 instantiate_prod arity left_args in
599 (* TODO: check if the sort elimination
600 * is allowed: [(I q1 ... qr)|B] *)
601 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
603 (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
605 if left_args = [] then
606 (C.MutConstruct (uri,i,j,exp_named_subst))
609 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
611 let p',actual_type,subst,metasenv,ugraph1 =
612 type_of_aux subst metasenv context p ugraph
614 let constructor',expected_type, subst, metasenv,ugraph2 =
615 type_of_aux subst metasenv context constructor ugraph1
617 let outtypeinstance,subst,metasenv,ugraph3 =
619 check_branch 0 context metasenv subst
620 no_left_params actual_type constructor' expected_type
624 enrich localization_tbl constructor'
626 lazy ("(11)The term " ^
627 CicMetaSubst.ppterm_in_context metasenv subst p'
628 context ^ " has type " ^
629 CicMetaSubst.ppterm_in_context metasenv subst actual_type
630 context ^ " but is here used with type " ^
631 CicMetaSubst.ppterm_in_context metasenv subst expected_type
635 outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
636 pl ([],List.length pl,[],subst,metasenv,ugraph3)
639 (* we are left to check that the outype matches his instances.
640 The easy case is when the outype is specified, that amount
641 to a trivial check. Otherwise, we should guess a type from
645 let outtype,outtypety, subst, metasenv,ugraph4 =
646 type_of_aux subst metasenv context outtype ugraph4 in
649 (let candidate,ugraph5,metasenv,subst =
650 let exp_name_subst, metasenv =
652 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
654 let uris = CicUtil.params_of_obj o in
656 fun uri (acc,metasenv) ->
657 let metasenv',new_meta =
658 CicMkImplicit.mk_implicit metasenv subst context
661 CicMkImplicit.identity_relocation_list_for_metavariable
664 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
668 match left_args,right_args with
669 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
671 let rec mk_right_args =
674 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
676 let right_args_no = List.length right_args in
677 let lifted_left_args =
678 List.map (CicSubstitution.lift right_args_no) left_args
680 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
681 (lifted_left_args @ mk_right_args right_args_no))
684 FreshNamesGenerator.mk_fresh_name ~subst metasenv
685 context Cic.Anonymous ~typ:ty
687 match outtypeinstances with
689 let extended_context =
690 let rec add_right_args =
692 Cic.Prod (name,ty,t) ->
693 Some (name,Cic.Decl ty)::(add_right_args t)
696 (Some (fresh_name,Cic.Decl ty))::
698 (add_right_args arity_instantiated_with_left_args))@
701 let metasenv,new_meta =
702 CicMkImplicit.mk_implicit metasenv subst extended_context
705 CicMkImplicit.identity_relocation_list_for_metavariable
708 let rec add_lambdas b =
710 Cic.Prod (name,ty,t) ->
711 Cic.Lambda (name,ty,(add_lambdas b t))
712 | _ -> Cic.Lambda (fresh_name, ty, b)
715 add_lambdas (Cic.Meta (new_meta,irl))
716 arity_instantiated_with_left_args
718 (Some candidate),ugraph4,metasenv,subst
719 | (constructor_args_no,_,instance,_)::tl ->
721 let instance',subst,metasenv =
722 CicMetaSubst.delift_rels subst metasenv
723 constructor_args_no instance
725 let candidate,ugraph,metasenv,subst =
727 fun (candidate_oty,ugraph,metasenv,subst)
728 (constructor_args_no,_,instance,_) ->
729 match candidate_oty with
730 | None -> None,ugraph,metasenv,subst
733 let instance',subst,metasenv =
734 CicMetaSubst.delift_rels subst metasenv
735 constructor_args_no instance
737 let subst,metasenv,ugraph =
738 fo_unif_subst subst context metasenv
741 candidate_oty,ugraph,metasenv,subst
743 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
744 | RefineFailure _ | Uncertain _ ->
745 None,ugraph,metasenv,subst
746 ) (Some instance',ugraph4,metasenv,subst) tl
749 | None -> None, ugraph,metasenv,subst
751 let rec add_lambdas n b =
753 Cic.Prod (name,ty,t) ->
754 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
756 Cic.Lambda (fresh_name, ty,
757 CicSubstitution.lift (n + 1) t)
760 (add_lambdas 0 t arity_instantiated_with_left_args),
761 ugraph,metasenv,subst
762 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
763 None,ugraph4,metasenv,subst
766 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
768 let subst,metasenv,ugraph =
770 fo_unif_subst subst context metasenv
771 candidate outtype ugraph5
773 exn -> assert false(* unification against a metavariable *)
775 C.MutCase (uri, i, outtype, term', pl'),
776 CicReduction.head_beta_reduce
777 (CicMetaSubst.apply_subst subst
778 (Cic.Appl (outtype::right_args@[term']))),
779 subst,metasenv,ugraph)
780 | _ -> (* easy case *)
781 let tlbody_and_type,subst,metasenv,ugraph4 =
782 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
784 let _,_,_,subst,metasenv,ugraph4 =
785 eat_prods false subst metasenv context
786 outtype outtypety tlbody_and_type ugraph4
788 let _,_, subst, metasenv,ugraph5 =
789 type_of_aux subst metasenv context
790 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
792 let (subst,metasenv,ugraph6) =
794 (fun (subst,metasenv,ugraph)
795 p (constructor_args_no,context,instance,args)
800 CicSubstitution.lift constructor_args_no outtype
802 C.Appl (outtype'::args)
804 CicReduction.whd ~subst context appl
807 fo_unif_subst subst context metasenv instance instance'
811 enrich localization_tbl p exn
813 lazy ("(12)The term " ^
814 CicMetaSubst.ppterm_in_context ~metasenv subst p
815 context ^ " has type " ^
816 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
817 context ^ " but is here used with type " ^
818 CicMetaSubst.ppterm_in_context ~metasenv subst instance
820 (subst,metasenv,ugraph5) pl' outtypeinstances
822 C.MutCase (uri, i, outtype, term', pl'),
823 CicReduction.head_beta_reduce
824 (CicMetaSubst.apply_subst subst
825 (C.Appl(outtype::right_args@[term]))),
826 subst,metasenv,ugraph6)
828 let fl_ty',subst,metasenv,types,ugraph1,len =
830 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
831 let ty',_,subst',metasenv',ugraph1 =
832 type_of_aux subst metasenv context ty ugraph
834 fl @ [ty'],subst',metasenv',
835 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
836 :: types, ugraph, len+1
837 ) ([],subst,metasenv,[],ugraph,0) fl
839 let context' = types@context in
840 let fl_bo',subst,metasenv,ugraph2 =
842 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
843 let bo',ty_of_bo,subst,metasenv,ugraph1 =
844 type_of_aux subst metasenv context' bo ugraph in
845 let expected_ty = CicSubstitution.lift len ty in
846 let subst',metasenv',ugraph' =
848 fo_unif_subst subst context' metasenv
849 ty_of_bo expected_ty ugraph1
852 enrich localization_tbl bo exn
854 lazy ("(13)The term " ^
855 CicMetaSubst.ppterm_in_context ~metasenv subst bo
856 context' ^ " has type " ^
857 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
858 context' ^ " but is here used with type " ^
859 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
862 fl @ [bo'] , subst',metasenv',ugraph'
863 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
865 let ty = List.nth fl_ty' i in
866 (* now we have the new ty in fl_ty', the new bo in fl_bo',
867 * and we want the new fl with bo' and ty' injected in the right
870 let rec map3 f l1 l2 l3 =
873 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
876 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
879 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
881 let fl_ty',subst,metasenv,types,ugraph1,len =
883 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
884 let ty',_,subst',metasenv',ugraph1 =
885 type_of_aux subst metasenv context ty ugraph
887 fl @ [ty'],subst',metasenv',
888 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
889 types, ugraph1, len+1
890 ) ([],subst,metasenv,[],ugraph,0) fl
892 let context' = types@context in
893 let fl_bo',subst,metasenv,ugraph2 =
895 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
896 let bo',ty_of_bo,subst,metasenv,ugraph1 =
897 type_of_aux subst metasenv context' bo ugraph in
898 let expected_ty = CicSubstitution.lift len ty in
899 let subst',metasenv',ugraph' =
901 fo_unif_subst subst context' metasenv
902 ty_of_bo expected_ty ugraph1
905 enrich localization_tbl bo exn
907 lazy ("(14)The term " ^
908 CicMetaSubst.ppterm_in_context ~metasenv subst bo
909 context' ^ " has type " ^
910 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
911 context' ^ " but is here used with type " ^
912 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
915 fl @ [bo'],subst',metasenv',ugraph'
916 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
918 let ty = List.nth fl_ty' i in
919 (* now we have the new ty in fl_ty', the new bo in fl_bo',
920 * and we want the new fl with bo' and ty' injected in the right
923 let rec map3 f l1 l2 l3 =
926 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
929 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
932 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
934 relocalize localization_tbl t t';
937 (* check_metasenv_consistency checks that the "canonical" context of a
938 metavariable is consitent - up to relocation via the relocation list l -
939 with the actual context *)
940 and check_metasenv_consistency
941 metano subst metasenv context canonical_context l ugraph
943 let module C = Cic in
944 let module R = CicReduction in
945 let module S = CicSubstitution in
946 let lifted_canonical_context =
950 | (Some (n,C.Decl t))::tl ->
951 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
952 | (Some (n,C.Def (t,None)))::tl ->
953 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
954 | None::tl -> None::(aux (i+1) tl)
955 | (Some (n,C.Def (t,Some ty)))::tl ->
957 C.Def ((S.subst_meta l (S.lift i t)),
958 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
960 aux 1 canonical_context
964 (fun (l,subst,metasenv,ugraph) t ct ->
967 l @ [None],subst,metasenv,ugraph
968 | Some t,Some (_,C.Def (ct,_)) ->
969 let subst',metasenv',ugraph' =
971 prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
972 fo_unif_subst subst context metasenv t ct ugraph
973 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))))))
975 l @ [Some t],subst',metasenv',ugraph'
976 | Some t,Some (_,C.Decl ct) ->
977 let t',inferredty,subst',metasenv',ugraph1 =
978 type_of_aux subst metasenv context t ugraph
980 let subst'',metasenv'',ugraph2 =
983 subst' context metasenv' inferredty ct ugraph1
984 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))))))
986 l @ [Some t'], subst'',metasenv'',ugraph2
988 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
990 Invalid_argument _ ->
994 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
995 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
996 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
998 and check_exp_named_subst metasubst metasenv context tl ugraph =
999 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1001 [] -> [],metasubst,metasenv,ugraph
1003 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1005 CicSubstitution.subst_vars substs ty_uri in
1006 (* CSC: why was this code here? it is wrong
1007 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1008 Cic.Variable (_,Some bo,_,_) ->
1010 (RefineFailure (lazy
1011 "A variable with a body can not be explicit substituted"))
1012 | Cic.Variable (_,None,_,_) -> ()
1015 (RefineFailure (lazy
1016 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1019 let t',typeoft,metasubst',metasenv',ugraph2 =
1020 type_of_aux metasubst metasenv context t ugraph1 in
1021 let subst = uri,t' in
1022 let metasubst'',metasenv'',ugraph3 =
1025 metasubst' context metasenv' typeoft typeofvar ugraph2
1027 raise (RefineFailure (lazy
1028 ("Wrong Explicit Named Substitution: " ^
1029 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1030 " not unifiable with " ^
1031 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1033 (* FIXME: no mere tail recursive! *)
1034 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1035 check_exp_named_subst_aux
1036 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1038 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1040 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1043 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1046 let module C = Cic in
1047 let context_for_t2 = (Some (name,C.Decl s))::context in
1048 let t1'' = CicReduction.whd ~subst context t1 in
1049 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1050 match (t1'', t2'') with
1051 (C.Sort s1, C.Sort s2)
1052 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1053 (* different than Coq manual!!! *)
1054 C.Sort s2,subst,metasenv,ugraph
1055 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1056 let t' = CicUniv.fresh() in
1058 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1059 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1060 C.Sort (C.Type t'),subst,metasenv,ugraph2
1062 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1063 | (C.Sort _,C.Sort (C.Type t1)) ->
1064 C.Sort (C.Type t1),subst,metasenv,ugraph
1065 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1066 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1067 (* TODO how can we force the meta to become a sort? If we don't we
1068 * break the invariant that refine produce only well typed terms *)
1069 (* TODO if we check the non meta term and if it is a sort then we
1070 * are likely to know the exact value of the result e.g. if the rhs
1071 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1072 let (metasenv,idx) =
1073 CicMkImplicit.mk_implicit_sort metasenv subst in
1074 let (subst, metasenv,ugraph1) =
1076 fo_unif_subst subst context_for_t2 metasenv
1077 (C.Meta (idx,[])) t2'' ugraph
1078 with _ -> assert false (* unification against a metavariable *)
1080 t2'',subst,metasenv,ugraph1
1083 enrich localization_tbl s
1087 "%s is supposed to be a type, but its type is %s"
1088 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1089 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1091 enrich localization_tbl t
1095 "%s is supposed to be a type, but its type is %s"
1096 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1097 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1099 and avoid_double_coercion context subst metasenv ugraph t ty =
1100 if not !pack_coercions then
1101 t,ty,subst,metasenv,ugraph
1103 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1105 let source_carr = CoercGraph.source_of c2 in
1106 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1107 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1109 | CoercGraph.SomeCoercion candidates ->
1111 HExtlib.list_findopt
1112 (function (metasenv,last,c) ->
1114 | c when not (CoercGraph.is_composite c) ->
1115 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1118 let subst,metasenv,ugraph =
1119 fo_unif_subst subst context metasenv last head ugraph in
1120 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1125 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1126 let newt,_,subst,metasenv,ugraph =
1127 type_of_aux subst metasenv context c ugraph in
1128 debug_print (lazy "tipa...");
1129 let subst, metasenv, ugraph =
1130 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1131 fo_unif_subst subst context metasenv newt t ugraph
1133 debug_print (lazy "unifica...");
1134 Some (newt, ty, subst, metasenv, ugraph)
1136 | RefineFailure s | Uncertain s when not !pack_coercions->
1137 debug_print s; debug_print (lazy "stop\n");None
1138 | RefineFailure s | Uncertain s ->
1139 debug_print s;debug_print (lazy "goon\n");
1141 let old_pack_coercions = !pack_coercions in
1142 pack_coercions := false; (* to avoid diverging *)
1143 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1144 type_of_aux subst metasenv context c1_c2_implicit ugraph
1146 pack_coercions := old_pack_coercions;
1148 is_a_double_coercion refined_c1_c2_implicit
1154 match refined_c1_c2_implicit with
1155 | Cic.Appl l -> HExtlib.list_last l
1158 let subst, metasenv, ugraph =
1159 try fo_unif_subst subst context metasenv
1161 with RefineFailure s| Uncertain s->
1162 debug_print s;assert false
1164 let subst, metasenv, ugraph =
1165 fo_unif_subst subst context metasenv
1166 refined_c1_c2_implicit t ugraph
1168 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1170 | RefineFailure s | Uncertain s ->
1171 pack_coercions := true;debug_print s;None
1172 | exn -> pack_coercions := true; raise exn))
1175 (match selected with
1179 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1180 t, ty, subst, metasenv, ugraph)
1181 | _ -> t, ty, subst, metasenv, ugraph)
1183 t, ty, subst, metasenv, ugraph
1185 and typeof_list subst metasenv context ugraph l =
1186 let tlbody_and_type,subst,metasenv,ugraph =
1188 (fun x (res,subst,metasenv,ugraph) ->
1189 let x',ty,subst',metasenv',ugraph1 =
1190 type_of_aux subst metasenv context x ugraph
1192 (x', ty)::res,subst',metasenv',ugraph1
1193 ) l ([],subst,metasenv,ugraph)
1195 tlbody_and_type,subst,metasenv,ugraph
1198 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1200 (* aux function to add coercions to funclass *)
1201 let rec fix_arity metasenv context subst he hetype eaten args_bo_and_ty ugraph =
1203 let pristinemenv = metasenv in
1204 let metasenv,hetype' =
1205 mk_prod_of_metas metasenv context subst args_bo_and_ty
1208 let subst,metasenv,ugraph =
1209 fo_unif_subst_eat_prods
1210 subst context metasenv hetype hetype' ugraph
1212 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1213 with RefineFailure s | Uncertain s as exn
1214 when allow_coercions && !insert_coercions ->
1215 (* {{{ we search a coercion of the head (saturated) to funclass *)
1216 let metasenv = pristinemenv in
1218 ("Fixing arity of: "^CicMetaSubst.ppterm ~metasenv subst hetype ^
1219 " since unif failed with: " ^ CicMetaSubst.ppterm ~metasenv subst hetype'
1220 (* ^ " cause: " ^ Lazy.force s *)));
1221 let how_many_args_are_needed =
1222 let rec aux n = function
1223 | Cic.Prod(_,_,t) -> aux (n+1) t
1226 aux 0 (CicMetaSubst.apply_subst subst hetype)
1228 let args, remainder =
1229 HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
1231 let args = List.map fst (eaten@args) in
1235 | Cic.Appl l -> Cic.Appl (l@args)
1236 | _ -> Cic.Appl (he::args)
1240 let x,xty,subst,metasenv,ugraph =
1241 (*CSC: here unsharing is necessary to avoid an unwanted
1242 relocalization. However, this also shows a great source of
1243 inefficiency: "x" is refined twice (once now and once in the
1244 subsequent eat_prods_and_args). Morevoer, how is divergence avoided?
1246 type_of_aux subst metasenv context (Unshare.unshare x) ugraph
1249 CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty)
1251 let carr_tgt = CoercDb.Fun 0 in
1252 match CoercGraph.look_for_coercion' metasenv subst context carr_src carr_tgt with
1253 | CoercGraph.NoCoercion
1254 | CoercGraph.NotMetaClosed
1255 | CoercGraph.NotHandled _ -> raise exn
1256 | CoercGraph.SomeCoercionToTgt candidates
1257 | CoercGraph.SomeCoercion candidates ->
1259 HExtlib.list_findopt
1260 (fun (metasenv,last,coerc) ->
1261 debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc));
1262 debug_print (lazy ("Last " ^ CicMetaSubst.ppterm ~metasenv subst last));
1263 debug_print (lazy ("x " ^ CicMetaSubst.ppterm ~metasenv subst x));
1264 let subst,metasenv,ugraph =
1265 fo_unif_subst subst context metasenv last x ugraph in
1267 (* we want this to be available in the error handler fo the
1268 * following (so it has its own try. *)
1269 let t,tty,subst,metasenv,ugraph =
1270 type_of_aux subst metasenv context coerc ugraph
1273 let metasenv, hetype' =
1274 mk_prod_of_metas metasenv context subst remainder
1277 (" unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^
1278 CicMetaSubst.ppterm ~metasenv subst hetype'));
1279 let subst,metasenv,ugraph =
1280 fo_unif_subst_eat_prods
1281 subst context metasenv tty hetype' ugraph
1283 debug_print (lazy " success!");
1284 Some (subst,metasenv,ugraph,tty,t,remainder)
1286 | Uncertain _ | RefineFailure _ ->
1288 let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
1290 metasenv context subst t tty [] remainder ugraph
1292 Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
1293 with Uncertain _ | RefineFailure _ -> None
1297 | HExtlib.Localized (_,Uncertain _)
1298 | HExtlib.Localized (_,RefineFailure _) -> None
1299 | exn -> assert false) (* ritornare None, e' un localized *)
1302 | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
1303 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1305 more_args_than_expected localization_tbl metasenv
1306 subst he context hetype args_bo_and_ty exn
1307 (* }}} end coercion to funclass stuff *)
1308 (* }}} end fix_arity *)
1310 (* aux function to process the type of the head and the args in parallel *)
1311 let rec eat_prods_and_args
1312 pristinemenv metasenv subst context pristinehe he hetype ugraph newargs
1316 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1317 | (hete, hety)::tl as rest ->
1318 match (CicReduction.whd ~subst context hetype) with
1319 | Cic.Prod (n,s,t) ->
1320 let arg,subst,metasenv,ugraph =
1321 coerce_to_something allow_coercions localization_tbl
1322 hete hety s subst metasenv context ugraph in
1324 pristinemenv metasenv subst context pristinehe he
1325 (CicSubstitution.subst (fst arg) t)
1326 ugraph (newargs@[arg]) tl
1329 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1331 pristinemenv context subst he hetype
1334 eat_prods_and_args metasenv
1335 metasenv subst context pristinehe he hetype'
1336 ugraph [] args_bo_and_ty
1337 with RefineFailure _ | Uncertain _ as exn ->
1338 (* unable to fix arity *)
1339 more_args_than_expected localization_tbl metasenv
1340 subst he context hetype args_bo_and_ty exn
1343 (* first we check if we are in the simple case of a meta closed term *)
1344 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1345 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1346 (* this optimization is to postpone fix_arity (the most common case)*)
1347 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1349 (* this (says CSC) is also useful to infer dependent types *)
1351 fix_arity metasenv context subst he hetype [] args_bo_and_ty ugraph
1352 with RefineFailure _ | Uncertain _ as exn ->
1353 (* unable to fix arity *)
1354 more_args_than_expected localization_tbl metasenv
1355 subst he context hetype args_bo_and_ty exn
1357 let coerced_args,subst,metasenv,he,t,ugraph =
1359 metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
1361 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1363 and coerce_to_something
1364 allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1366 let module CS = CicSubstitution in
1367 let module CR = CicReduction in
1368 let cs_subst = CS.subst ~avoid_beta_redexes:true in
1369 let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1371 CoercGraph.look_for_coercion metasenv subst context infty expty
1374 | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
1375 "coerce_atom_to_something fails since not meta closed"))
1376 | CoercGraph.NoCoercion
1377 | CoercGraph.SomeCoercionToTgt _
1378 | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
1379 "coerce_atom_to_something fails since no coercions found"))
1380 | CoercGraph.SomeCoercion candidates ->
1381 debug_print (lazy (string_of_int (List.length candidates) ^ "
1382 candidates found"));
1383 let uncertain = ref false in
1385 (* HExtlib.list_findopt *)
1388 (fun (metasenv,last,c) ->
1390 debug_print (lazy ("FO_UNIF_SUBST: " ^
1391 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1393 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1394 debug_print (lazy ("FO_UNIF_SUBST: " ^
1395 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t));
1396 let subst,metasenv,ugraph =
1397 fo_unif_subst subst context metasenv last t ugraph
1400 let newt,newhety,subst,metasenv,ugraph =
1401 type_of_aux subst metasenv context c ugraph in
1402 let newt, newty, subst, metasenv, ugraph =
1403 avoid_double_coercion context subst metasenv ugraph newt expty
1405 let subst,metasenv,ugraph =
1406 fo_unif_subst subst context metasenv newhety expty ugraph in
1407 Some ((newt,newty), subst, metasenv, ugraph)
1409 | Uncertain _ -> uncertain := true; None
1410 | RefineFailure _ -> None)
1415 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1423 | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1424 | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1426 let rec coerce_to_something_aux
1427 t infty expty subst metasenv context ugraph
1430 let subst, metasenv, ugraph =
1431 fo_unif_subst subst context metasenv infty expty ugraph
1433 (t, expty), subst, metasenv, ugraph
1434 with Uncertain _ | RefineFailure _ as exn ->
1435 if not allow_coercions || not !insert_coercions then
1436 enrich localization_tbl t exn
1438 let whd = CicReduction.whd ~delta:false in
1439 let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1440 let infty = clean infty subst context in
1441 let expty = clean expty subst context in
1442 let t = clean t subst context in
1443 debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1444 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1445 CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^ " ==> " ^
1446 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1447 match infty, expty, t with
1448 | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2), Cic.Fix (n,fl) ->
1449 debug_print (lazy "FIX");
1451 [name,i,_(* infty *),bo] ->
1453 Some (Cic.Name name,Cic.Decl expty)::context in
1454 let (rel1, _), subst, metasenv, ugraph =
1455 coerce_to_something_aux (Cic.Rel 1)
1456 (CS.lift 1 expty) (CS.lift 1 infty) subst
1457 metasenv context_bo ugraph in
1458 let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1459 let (bo,_), subst, metasenv, ugraph =
1460 coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1462 metasenv context_bo ugraph
1464 (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1465 | _ -> assert false (* not implemented yet *))
1466 | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1467 debug_print (lazy "CASE");
1468 (* {{{ helper functions *)
1469 let get_cl_and_left_p uri tyno outty ugraph =
1470 match CicEnvironment.get_obj ugraph uri with
1471 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1474 match CicReduction.whd ~delta:false ctx t with
1475 | Cic.Prod (name,src,tgt) ->
1476 let ctx = Some (name, Cic.Decl src) :: ctx in
1482 let rec skip_lambda_delifting t n =
1485 | Cic.Lambda (_,_,t),n ->
1486 skip_lambda_delifting
1487 (CS.subst (Cic.Implicit None) t) (n - 1)
1490 let get_l_r_p n = function
1491 | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1492 | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1493 HExtlib.split_nth n args
1496 let _, _, ty, cl = List.nth tl tyno in
1497 let pis = count_pis ty in
1498 let rno = pis - leftno in
1499 let t = skip_lambda_delifting outty rno in
1500 let left_p, _ = get_l_r_p leftno t in
1501 let instantiale_with_left cl =
1505 (fun t p -> match t with
1506 | Cic.Prod (_,_,t) ->
1512 let cl = instantiale_with_left (List.map snd cl) in
1513 cl, left_p, leftno, rno, ugraph
1516 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1519 let rec mkr n = function
1520 | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1523 CicReplace.replace_lifting
1524 ~equality:(fun _ -> CicUtil.alpha_equivalence)
1526 ~what:(matched::right_p)
1527 ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1531 | Cic.Lambda (name, src, tgt),_ ->
1532 Cic.Lambda (name, src,
1533 keep_lambdas_and_put_expty
1534 (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1535 (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1538 let eq_uri, eq, eq_refl =
1539 match LibraryObjects.eq_URI () with
1540 | None -> HLog.warn "no default equality"; raise exn
1541 | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1544 metasenv subst context uri tyno cty outty mty m leftno i
1546 let rec aux context outty par k mty m = function
1547 | Cic.Prod (name, src, tgt) ->
1550 (Some (name, Cic.Decl src) :: context)
1551 (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1552 (CS.lift 1 mty) (CS.lift 1 m) tgt
1554 Cic.Prod (name, src, t), k
1557 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1558 if par <> [] then Cic.Appl (k::par) else k
1560 Cic.Prod (Cic.Name "p",
1561 Cic.Appl [eq; mty; m; k],
1563 (CR.head_beta_reduce ~delta:false
1564 (Cic.Appl [outty;k])))),k
1565 | Cic.Appl (Cic.MutInd _::pl) ->
1566 let left_p,right_p = HExtlib.split_nth leftno pl in
1567 let has_rights = right_p <> [] in
1569 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1570 Cic.Appl (k::left_p@par)
1574 CicTypeChecker.type_of_aux' ~subst metasenv context k
1575 CicUniv.oblivion_ugraph
1577 | Cic.Appl (Cic.MutInd _::args),_ ->
1578 snd (HExtlib.split_nth leftno args)
1580 with CicTypeChecker.TypeCheckerFailure _ -> assert false
1583 CR.head_beta_reduce ~delta:false
1584 (Cic.Appl (outty ::right_p @ [k])),k
1586 Cic.Prod (Cic.Name "p",
1587 Cic.Appl [eq; mty; m; k],
1589 (CR.head_beta_reduce ~delta:false
1590 (Cic.Appl (outty ::right_p @ [k]))))),k
1593 aux context outty [] 1 mty m cty
1595 let add_lambda_for_refl_m pbo rno mty m k cty =
1596 (* k lives in the right context *)
1597 if rno <> 0 then pbo else
1598 let rec aux mty m = function
1599 | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1600 Cic.Lambda (name,src,
1601 (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1603 Cic.Lambda (Cic.Name "p",
1604 Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1608 let add_pi_for_refl_m new_outty mty m rno =
1609 if rno <> 0 then new_outty else
1610 let rec aux m mty = function
1611 | Cic.Lambda (name, src, tgt) ->
1612 Cic.Lambda (name, src,
1613 aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1616 (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1620 in (* }}} end helper functions *)
1621 (* constructors types with left params already instantiated *)
1622 let outty = CicMetaSubst.apply_subst subst outty in
1623 let cl, left_p, leftno,rno,ugraph =
1624 get_cl_and_left_p uri tyno outty ugraph
1629 CicTypeChecker.type_of_aux' ~subst metasenv context m
1630 CicUniv.oblivion_ugraph
1632 | Cic.MutInd _ as mty,_ -> [], mty
1633 | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
1634 snd (HExtlib.split_nth leftno args), mty
1636 with CicTypeChecker.TypeCheckerFailure _ -> assert false
1639 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1642 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1643 ~metasenv subst new_outty context));
1644 let _,pl,subst,metasenv,ugraph =
1646 (fun cty pbo (i, acc, s, menv, ugraph) ->
1647 (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1648 * (new_)outty right_par (K_i left_par k_par) *)
1650 add_params menv s context uri tyno
1651 cty outty mty m leftno i in
1653 (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1654 ~metasenv subst infty_pbo context));
1655 let expty_pbo, k = (* k is (K_i left_par k_par) *)
1656 add_params menv s context uri tyno
1657 cty new_outty mty m leftno i in
1659 (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1660 ~metasenv subst expty_pbo context));
1661 let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1663 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1664 ~metasenv subst pbo context));
1665 let (pbo, _), subst, metasenv, ugraph =
1666 coerce_to_something_aux pbo infty_pbo expty_pbo
1667 s menv context ugraph
1670 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1671 ~metasenv subst pbo context));
1672 (i-1, pbo::acc, subst, metasenv, ugraph))
1673 cl pl (List.length pl, [], subst, metasenv, ugraph)
1675 let new_outty = add_pi_for_refl_m new_outty mty m rno in
1677 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1678 ~metasenv subst new_outty context));
1681 let refl_m=Cic.Appl[eq_refl;mty;m]in
1682 Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1684 Cic.MutCase(uri,tyno,new_outty,m,pl)
1686 (t, expty), subst, metasenv, ugraph
1687 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1688 debug_print (lazy "LAM");
1690 FreshNamesGenerator.mk_fresh_name
1691 ~subst metasenv context ~typ:src2 Cic.Anonymous
1693 let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1694 (* contravariant part: the argument of f:src->ty *)
1695 let (rel1, _), subst, metasenv, ugraph =
1696 coerce_to_something_aux
1697 (Cic.Rel 1) (CS.lift 1 src2)
1698 (CS.lift 1 src) subst metasenv context_src2 ugraph
1700 (* covariant part: the result of f(c x); x:src2; (c x):src *)
1703 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1704 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1706 (* we fix the possible dependency problem in the source ty *)
1707 let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1708 let (bo, _), subst, metasenv, ugraph =
1709 coerce_to_something_aux
1710 bo ty ty2 subst metasenv context_src2 ugraph
1712 let coerced = Cic.Lambda (name_t,src2, bo) in
1713 debug_print (lazy ("coerced: "^ CicMetaSubst.ppterm_in_context
1714 ~metasenv subst coerced context));
1715 (coerced, expty), subst, metasenv, ugraph
1717 debug_print (lazy ("ATOM: " ^ CicMetaSubst.ppterm_in_context
1718 ~metasenv subst infty context ^ " ==> " ^
1719 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1720 coerce_atom_to_something t infty expty subst metasenv context ugraph
1723 coerce_to_something_aux t infty expty subst metasenv context ugraph
1724 with Uncertain _ | RefineFailure _ as exn ->
1727 CicMetaSubst.ppterm_in_context metasenv subst t context ^
1728 " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1729 infty context ^ " but is here used with type " ^
1730 CicMetaSubst.ppterm_in_context metasenv subst expty context)
1732 enrich localization_tbl ~f t exn
1734 and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1735 match CicReduction.whd ~subst:subst context infty with
1736 | Cic.Meta _ | Cic.Sort _ ->
1737 t,infty, subst, metasenv, ugraph
1739 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1741 let (t, ty_t), subst, metasenv, ugraph =
1742 coerce_to_something true
1743 localization_tbl t src tgt subst metasenv context ugraph
1745 t, ty_t, subst, metasenv, ugraph
1746 with HExtlib.Localized (_, exn) ->
1748 lazy ("(7)The term " ^
1749 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1750 ^ " is not a type since it has type " ^
1751 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1752 ^ " that is not a sort")
1754 enrich localization_tbl ~f t exn
1757 (* eat prods ends here! *)
1759 let t',ty,subst',metasenv',ugraph1 =
1760 type_of_aux [] metasenv context t ugraph
1762 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1763 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1764 (* Andrea: ho rimesso qui l'applicazione della subst al
1765 metasenv dopo che ho droppato l'invariante che il metsaenv
1766 e' sempre istanziato *)
1767 let substituted_metasenv =
1768 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1770 (* substituted_t,substituted_ty,substituted_metasenv *)
1771 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1773 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1775 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1776 let cleaned_metasenv =
1778 (function (n,context,ty) ->
1779 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1784 | Some (n, Cic.Decl t) ->
1786 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1787 | Some (n, Cic.Def (bo,ty)) ->
1788 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1793 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1795 Some (n, Cic.Def (bo',ty'))
1799 ) substituted_metasenv
1801 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1804 let undebrujin uri typesno tys t =
1807 (fun (name,_,_,_) (i,t) ->
1808 (* here the explicit_named_substituion is assumed to be *)
1810 let t' = Cic.MutInd (uri,i,[]) in
1811 let t = CicSubstitution.subst t' t in
1813 ) tys (typesno - 1,t))
1815 let map_first_n n start f g l =
1816 let rec aux acc k l =
1819 | [] -> raise (Invalid_argument "map_first_n")
1820 | hd :: tl -> f hd k (aux acc (k+1) tl)
1826 (*CSC: this is a very rough approximation; to be finished *)
1827 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1828 let subst,metasenv,ugraph,tys =
1830 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1831 let subst,metasenv,ugraph,cl =
1833 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1834 let rec aux ctx k subst = function
1835 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1836 let subst,metasenv,ugraph,tl =
1838 (subst,metasenv,ugraph,[])
1839 (fun t n (subst,metasenv,ugraph,acc) ->
1840 let subst,metasenv,ugraph =
1842 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1844 subst,metasenv,ugraph,(t::acc))
1845 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1848 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1849 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1850 subst,metasenv,ugraph,t
1851 | Cic.Prod (name,s,t) ->
1852 let ctx = (Some (name,Cic.Decl s))::ctx in
1853 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1854 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1858 (lazy "not well formed constructor type"))
1860 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1861 subst,metasenv,ugraph,(name,ty) :: acc)
1862 cl (subst,metasenv,ugraph,[])
1864 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1865 tys ([],metasenv,ugraph,[])
1867 let substituted_tys =
1869 (fun (name,ind,arity,cl) ->
1871 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1873 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1876 metasenv,ugraph,substituted_tys
1878 let typecheck metasenv uri obj ~localization_tbl =
1879 let ugraph = CicUniv.empty_ugraph in
1881 Cic.Constant (name,Some bo,ty,args,attrs) ->
1882 let bo',boty,metasenv,ugraph =
1883 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1884 let ty',_,metasenv,ugraph =
1885 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1886 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1887 let bo' = CicMetaSubst.apply_subst subst bo' in
1888 let ty' = CicMetaSubst.apply_subst subst ty' in
1889 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1890 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1891 | Cic.Constant (name,None,ty,args,attrs) ->
1892 let ty',_,metasenv,ugraph =
1893 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1895 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1896 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1897 assert (metasenv' = metasenv);
1898 (* Here we do not check the metasenv for correctness *)
1899 let bo',boty,metasenv,ugraph =
1900 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1901 let ty',sort,metasenv,ugraph =
1902 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1906 (* instead of raising Uncertain, let's hope that the meta will become
1909 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1911 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1912 let bo' = CicMetaSubst.apply_subst subst bo' in
1913 let ty' = CicMetaSubst.apply_subst subst ty' in
1914 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1915 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1916 | Cic.Variable _ -> assert false (* not implemented *)
1917 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1918 (*CSC: this code is greately simplified and many many checks are missing *)
1919 (*CSC: e.g. the constructors are not required to build their own types, *)
1920 (*CSC: the arities are not required to have as type a sort, etc. *)
1921 let uri = match uri with Some uri -> uri | None -> assert false in
1922 let typesno = List.length tys in
1923 (* first phase: we fix only the types *)
1924 let metasenv,ugraph,tys =
1926 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1927 let ty',_,metasenv,ugraph =
1928 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1930 metasenv,ugraph,(name,b,ty',cl)::res
1931 ) tys (metasenv,ugraph,[]) in
1933 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1934 (* second phase: we fix only the constructors *)
1935 let saved_menv = metasenv in
1936 let metasenv,ugraph,tys =
1938 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1939 let metasenv,ugraph,cl' =
1941 (fun (name,ty) (metasenv,ugraph,res) ->
1943 CicTypeChecker.debrujin_constructor
1944 ~cb:(relocalize localization_tbl) uri typesno ty in
1945 let ty',_,metasenv,ugraph =
1946 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1947 let ty' = undebrujin uri typesno tys ty' in
1948 metasenv@saved_menv,ugraph,(name,ty')::res
1949 ) cl (metasenv,ugraph,[])
1951 metasenv,ugraph,(name,b,ty,cl')::res
1952 ) tys (metasenv,ugraph,[]) in
1953 (* third phase: we check the positivity condition *)
1954 let metasenv,ugraph,tys =
1955 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1957 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1960 (* sara' piu' veloce che raffinare da zero? mah.... *)
1961 let pack_coercion metasenv ctx t =
1962 let module C = Cic in
1963 let rec merge_coercions ctx =
1964 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1966 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1967 | C.Meta (n,subst) ->
1970 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1973 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1974 | C.Prod (name,so,dest) ->
1975 let ctx' = (Some (name,C.Decl so))::ctx in
1976 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1977 | C.Lambda (name,so,dest) ->
1978 let ctx' = (Some (name,C.Decl so))::ctx in
1979 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1980 | C.LetIn (name,so,dest) ->
1981 let _,ty,metasenv,ugraph =
1982 pack_coercions := false;
1983 type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1984 pack_coercions := true;
1985 let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1986 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1988 let l = List.map (merge_coercions ctx) l in
1990 let b,_,_,_,_ = is_a_double_coercion t in
1992 let ugraph = CicUniv.oblivion_ugraph in
1993 let old_insert_coercions = !insert_coercions in
1994 insert_coercions := false;
1995 let newt, _, menv, _ =
1997 type_of_aux' metasenv ctx t ugraph
1998 with RefineFailure _ | Uncertain _ ->
2001 insert_coercions := old_insert_coercions;
2002 if metasenv <> [] || menv = [] then
2005 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
2008 | C.Var (uri,exp_named_subst) ->
2009 let exp_named_subst = List.map aux exp_named_subst in
2010 C.Var (uri, exp_named_subst)
2011 | C.Const (uri,exp_named_subst) ->
2012 let exp_named_subst = List.map aux exp_named_subst in
2013 C.Const (uri, exp_named_subst)
2014 | C.MutInd (uri,tyno,exp_named_subst) ->
2015 let exp_named_subst = List.map aux exp_named_subst in
2016 C.MutInd (uri,tyno,exp_named_subst)
2017 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
2018 let exp_named_subst = List.map aux exp_named_subst in
2019 C.MutConstruct (uri,tyno,consno,exp_named_subst)
2020 | C.MutCase (uri,tyno,out,te,pl) ->
2021 let pl = List.map (merge_coercions ctx) pl in
2022 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
2023 | C.Fix (fno, fl) ->
2026 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2031 (fun (name,idx,ty,bo) ->
2032 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
2036 | C.CoFix (fno, fl) ->
2039 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2044 (fun (name,ty,bo) ->
2045 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
2050 merge_coercions ctx t
2053 let pack_coercion_metasenv conjectures =
2054 let module C = Cic in
2056 (fun (i, ctx, ty) ->
2062 Some (name, C.Decl t) ->
2063 Some (name, C.Decl (pack_coercion conjectures ctx t))
2064 | Some (name, C.Def (t,None)) ->
2065 Some (name,C.Def (pack_coercion conjectures ctx t,None))
2066 | Some (name, C.Def (t,Some ty)) ->
2067 Some (name, C.Def (pack_coercion conjectures ctx t,
2068 Some (pack_coercion conjectures ctx ty)))
2074 ((i,ctx,pack_coercion conjectures ctx ty))
2078 let pack_coercion_obj obj =
2079 let module C = Cic in
2081 | C.Constant (id, body, ty, params, attrs) ->
2085 | Some body -> Some (pack_coercion [] [] body)
2087 let ty = pack_coercion [] [] ty in
2088 C.Constant (id, body, ty, params, attrs)
2089 | C.Variable (name, body, ty, params, attrs) ->
2093 | Some body -> Some (pack_coercion [] [] body)
2095 let ty = pack_coercion [] [] ty in
2096 C.Variable (name, body, ty, params, attrs)
2097 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2098 let conjectures = pack_coercion_metasenv conjectures in
2099 let body = pack_coercion conjectures [] body in
2100 let ty = pack_coercion conjectures [] ty in
2101 C.CurrentProof (name, conjectures, body, ty, params, attrs)
2102 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2105 (fun (name, ind, arity, cl) ->
2106 let arity = pack_coercion [] [] arity in
2108 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2110 (name, ind, arity, cl))
2113 C.InductiveDefinition (indtys, params, leftno, attrs)
2118 let type_of_aux' metasenv context term =
2121 type_of_aux' metasenv context term in
2123 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2125 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2128 | RefineFailure msg as e ->
2129 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2131 | Uncertain msg as e ->
2132 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2136 let profiler2 = HExtlib.profile "CicRefine"
2138 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2139 profiler2.HExtlib.profile
2140 (type_of_aux' ?localization_tbl metasenv context term) ugraph
2142 let typecheck ~localization_tbl metasenv uri obj =
2143 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2145 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2146 (* vim:set foldmethod=marker: *)