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 (* for internal use only; the integer is the number of surplus arguments *)
35 exception MoreArgsThanExpected of int * exn;;
37 let insert_coercions = ref true
38 let pack_coercions = ref true
43 if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());;
45 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
47 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
50 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
51 in profiler_eat_prods2.HExtlib.profile foo ()
53 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
54 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
57 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
59 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
62 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
63 in profiler_eat_prods.HExtlib.profile foo ()
65 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
66 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
69 let profiler = HExtlib.profile "CicRefine.fo_unif"
71 let fo_unif_subst subst context metasenv t1 t2 ugraph =
74 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
75 in profiler.HExtlib.profile foo ()
77 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
78 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
81 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
84 RefineFailure msg -> RefineFailure (f msg)
85 | Uncertain msg -> Uncertain (f msg)
86 | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
87 | Sys.Break -> raise exn
88 | _ -> prerr_endline (Printexc.to_string exn); assert false
92 Cic.CicHash.find localization_tbl t
94 HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
97 raise (HExtlib.Localized (loc,exn'))
99 let relocalize localization_tbl oldt newt =
101 let infos = Cic.CicHash.find localization_tbl oldt in
102 Cic.CicHash.remove localization_tbl oldt;
103 Cic.CicHash.add localization_tbl newt infos;
111 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
112 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
115 let exp_impl metasenv subst context =
118 let (metasenv', idx) =
119 CicMkImplicit.mk_implicit_type metasenv subst context in
121 CicMkImplicit.identity_relocation_list_for_metavariable context in
122 metasenv', Cic.Meta (idx, irl)
124 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
125 metasenv', Cic.Meta (idx, [])
127 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
129 CicMkImplicit.identity_relocation_list_for_metavariable context in
130 metasenv', Cic.Meta (idx, irl)
134 let is_a_double_coercion t =
136 let rec aux acc = function
138 | x::tl -> aux (acc@[x]) tl
143 let imp = Cic.Implicit None in
144 let dummyres = false,imp, imp,imp,imp in
146 | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
147 (match last_of tl with
148 | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
149 let sib2,head = last_of tl2 in
150 true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
155 let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
157 let len = List.length tlbody_and_type in
160 CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
161 " (that has type "^ CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
162 ") is here applied to " ^ string_of_int len ^
163 " arguments but here it can handle only up to " ^
164 string_of_int (len - residuals) ^ " arguments")
166 enrich localization_tbl he ~f:(fun _-> msg) exn
169 let mk_prod_of_metas metasenv context subst args =
170 let rec mk_prod metasenv context' = function
172 let (metasenv, idx) =
173 CicMkImplicit.mk_implicit_type metasenv subst context'
176 CicMkImplicit.identity_relocation_list_for_metavariable context'
178 metasenv,Cic.Meta (idx, irl)
180 let (metasenv, idx) =
181 CicMkImplicit.mk_implicit_type metasenv subst context'
184 CicMkImplicit.identity_relocation_list_for_metavariable context'
186 let meta = Cic.Meta (idx,irl) in
188 (* The name must be fresh for context. *)
189 (* Nevertheless, argty is well-typed only in context. *)
190 (* Thus I generate a name (name_hint) in context and *)
191 (* then I generate a name --- using the hint name_hint *)
192 (* --- that is fresh in context'. *)
194 FreshNamesGenerator.mk_fresh_name ~subst metasenv
195 (CicMetaSubst.apply_subst_context subst context)
197 ~typ:(CicMetaSubst.apply_subst subst argty)
199 FreshNamesGenerator.mk_fresh_name ~subst
200 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
202 let metasenv,target =
203 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
205 metasenv,Cic.Prod (name,meta,target)
207 mk_prod metasenv context args
210 let rec type_of_constant uri ugraph =
211 let module C = Cic in
212 let module R = CicReduction in
213 let module U = UriManager in
214 let _ = CicTypeChecker.typecheck uri in
217 CicEnvironment.get_cooked_obj ugraph uri
218 with Not_found -> assert false
221 C.Constant (_,_,ty,_,_) -> ty,u
222 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
226 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
228 and type_of_variable uri ugraph =
229 let module C = Cic in
230 let module R = CicReduction in
231 let module U = UriManager in
232 let _ = CicTypeChecker.typecheck uri in
235 CicEnvironment.get_cooked_obj ugraph uri
236 with Not_found -> assert false
239 C.Variable (_,_,ty,_,_) -> ty,u
243 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
245 and type_of_mutual_inductive_defs uri i ugraph =
246 let module C = Cic in
247 let module R = CicReduction in
248 let module U = UriManager in
249 let _ = CicTypeChecker.typecheck uri in
252 CicEnvironment.get_cooked_obj ugraph uri
253 with Not_found -> assert false
256 C.InductiveDefinition (dl,_,_,_) ->
257 let (_,_,arity,_) = List.nth dl i in
262 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
264 and type_of_mutual_inductive_constr uri i j ugraph =
265 let module C = Cic in
266 let module R = CicReduction in
267 let module U = UriManager in
268 let _ = CicTypeChecker.typecheck uri in
271 CicEnvironment.get_cooked_obj ugraph uri
272 with Not_found -> assert false
275 C.InductiveDefinition (dl,_,_,_) ->
276 let (_,_,_,cl) = List.nth dl i in
277 let (_,ty) = List.nth cl (j-1) in
283 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
286 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
288 (* the check_branch function checks if a branch of a case is refinable.
289 It returns a pair (outype_instance,args), a subst and a metasenv.
290 outype_instance is the expected result of applying the case outtype
292 The problem is that outype is in general unknown, and we should
293 try to synthesize it from the above information, that is in general
294 a second order unification problem. *)
296 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
297 let module C = Cic 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 (_,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' ?(clean_dummy_dependent_types=true) ?(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
331 let (t',_,_,_,_) as res =
336 match List.nth context (n - 1) with
337 Some (_,C.Decl ty) ->
338 t,S.lift n ty,subst,metasenv, ugraph
339 | Some (_,C.Def (_,ty)) ->
340 t,S.lift n ty,subst,metasenv, ugraph
342 enrich localization_tbl t
343 (RefineFailure (lazy "Rel to hidden hypothesis"))
346 enrich localization_tbl t
347 (RefineFailure (lazy "Not a closed term")))
348 | C.Var (uri,exp_named_subst) ->
349 let exp_named_subst',subst',metasenv',ugraph1 =
350 check_exp_named_subst
351 subst metasenv context exp_named_subst ugraph
353 let ty_uri,ugraph1 = type_of_variable uri ugraph in
355 CicSubstitution.subst_vars exp_named_subst' ty_uri
357 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
360 let (canonical_context, term,ty) =
361 CicUtil.lookup_subst n subst
363 let l',subst',metasenv',ugraph1 =
364 check_metasenv_consistency n subst metasenv context
365 canonical_context l ugraph
367 (* trust or check ??? *)
368 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
369 subst', metasenv', ugraph1
370 (* type_of_aux subst metasenv
371 context (CicSubstitution.subst_meta l term) *)
372 with CicUtil.Subst_not_found _ ->
373 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
374 let l',subst',metasenv', ugraph1 =
375 check_metasenv_consistency n subst metasenv context
376 canonical_context l ugraph
378 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
379 subst', metasenv',ugraph1)
380 | C.Sort (C.Type tno) ->
381 let tno' = CicUniv.fresh() in
383 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
384 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
386 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
388 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
389 | C.Implicit infos ->
390 let metasenv',t' = exp_impl metasenv subst context infos in
391 type_of_aux subst metasenv' context t' ugraph
393 let ty',_,subst',metasenv',ugraph1 =
394 type_of_aux subst metasenv context ty ugraph
396 let te',inferredty,subst'',metasenv'',ugraph2 =
397 type_of_aux subst' metasenv' context te ugraph1
399 let (te', ty'), subst''',metasenv''',ugraph3 =
400 coerce_to_something true localization_tbl te' inferredty ty'
401 subst'' metasenv'' context ugraph2
403 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
404 | C.Prod (name,s,t) ->
405 let s',sort1,subst',metasenv',ugraph1 =
406 type_of_aux subst metasenv context s ugraph
408 let s',sort1,subst', metasenv',ugraph1 =
409 coerce_to_sort localization_tbl
410 s' sort1 subst' context metasenv' ugraph1
412 let context_for_t = ((Some (name,(C.Decl s')))::context) in
413 let t',sort2,subst'',metasenv'',ugraph2 =
414 type_of_aux subst' metasenv'
415 context_for_t t ugraph1
417 let t',sort2,subst'',metasenv'',ugraph2 =
418 coerce_to_sort localization_tbl
419 t' sort2 subst'' context_for_t metasenv'' ugraph2
421 let sop,subst''',metasenv''',ugraph3 =
422 sort_of_prod localization_tbl subst'' metasenv''
423 context (name,s') t' (sort1,sort2) ugraph2
425 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
426 | C.Lambda (n,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 (n,(C.Decl s')))::context) in
435 let t',type2,subst'',metasenv'',ugraph2 =
436 type_of_aux subst' metasenv' context_for_t t ugraph1
438 C.Lambda (n,s',t'),C.Prod (n,s',type2),
439 subst'',metasenv'',ugraph2
440 | C.LetIn (n,s,ty,t) ->
441 (* only to check if s is well-typed *)
442 let s',ty',subst',metasenv',ugraph1 =
443 type_of_aux subst metasenv context s ugraph in
444 let ty,_,subst',metasenv',ugraph1 =
445 type_of_aux subst' metasenv' context ty ugraph1 in
446 let subst',metasenv',ugraph1 =
448 fo_unif_subst subst' context metasenv'
452 enrich localization_tbl s' exn
455 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
456 context ^ " has type " ^
457 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
458 context ^ " but is here used with type " ^
459 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
462 let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
464 let t',inferredty,subst'',metasenv'',ugraph2 =
465 type_of_aux subst' metasenv'
466 context_for_t t ugraph1
468 (* One-step LetIn reduction.
469 * Even faster than the previous solution.
470 * Moreover the inferred type is closer to the expected one.
472 C.LetIn (n,s',ty,t'),
473 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
474 subst'',metasenv'',ugraph2
475 | C.Appl (he::((_::_) as tl)) ->
476 let he',hetype,subst',metasenv',ugraph1 =
477 type_of_aux subst metasenv context he ugraph
479 let tlbody_and_type,subst'',metasenv'',ugraph2 =
480 typeof_list subst' metasenv' context ugraph1 tl
482 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
483 eat_prods true subst'' metasenv'' context
484 he' hetype tlbody_and_type ugraph2
486 let newappl = (C.Appl (coerced_he::coerced_args)) in
487 avoid_double_coercion
488 context subst''' metasenv''' ugraph3 newappl applty
489 | C.Appl _ -> assert false
490 | C.Const (uri,exp_named_subst) ->
491 let exp_named_subst',subst',metasenv',ugraph1 =
492 check_exp_named_subst subst metasenv context
493 exp_named_subst ugraph in
494 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
496 CicSubstitution.subst_vars exp_named_subst' ty_uri
498 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
499 | C.MutInd (uri,i,exp_named_subst) ->
500 let exp_named_subst',subst',metasenv',ugraph1 =
501 check_exp_named_subst subst metasenv context
502 exp_named_subst ugraph
504 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
506 CicSubstitution.subst_vars exp_named_subst' ty_uri in
507 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
508 | C.MutConstruct (uri,i,j,exp_named_subst) ->
509 let exp_named_subst',subst',metasenv',ugraph1 =
510 check_exp_named_subst subst metasenv context
511 exp_named_subst ugraph
514 type_of_mutual_inductive_constr uri i j ugraph1
517 CicSubstitution.subst_vars exp_named_subst' ty_uri
519 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
521 | C.MutCase (uri, i, outtype, term, pl) ->
522 (* first, get the inductive type (and noparams)
523 * in the environment *)
524 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
525 let _ = CicTypeChecker.typecheck uri in
526 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
528 C.InductiveDefinition (l,expl_params,parsno,_) ->
529 List.nth l i , expl_params, parsno, u
531 enrich localization_tbl t
533 (lazy ("Unkown mutual inductive definition " ^
534 U.string_of_uri uri)))
536 if List.length constructors <> List.length pl then
537 enrich localization_tbl t
539 (lazy "Wrong number of cases")) ;
540 let rec count_prod t =
541 match CicReduction.whd ~subst context t with
542 C.Prod (_, _, t) -> 1 + (count_prod t)
545 let no_args = count_prod arity in
546 (* now, create a "generic" MutInd *)
547 let metasenv,left_args =
548 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
550 let metasenv,right_args =
551 let no_right_params = no_args - no_left_params in
552 if no_right_params < 0 then assert false
553 else CicMkImplicit.n_fresh_metas
554 metasenv subst context no_right_params
556 let metasenv,exp_named_subst =
557 CicMkImplicit.fresh_subst metasenv subst context expl_params in
560 C.MutInd (uri,i,exp_named_subst)
563 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
565 (* check consistency with the actual type of term *)
566 let term',actual_type,subst,metasenv,ugraph1 =
567 type_of_aux subst metasenv context term ugraph in
568 let expected_type',_, subst, metasenv,ugraph2 =
569 type_of_aux subst metasenv context expected_type ugraph1
571 let actual_type = CicReduction.whd ~subst context actual_type in
572 let subst,metasenv,ugraph3 =
574 fo_unif_subst subst context metasenv
575 expected_type' actual_type ugraph2
578 enrich localization_tbl term' exn
581 CicMetaSubst.ppterm_in_context ~metasenv subst term'
582 context ^ " has type " ^
583 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
584 context ^ " but is here used with type " ^
585 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type'
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'
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 outtypeinstance::outtypeinstances,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.oblivion_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
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
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
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 | None::tl -> None::(aux (i+1) tl)
953 | (Some (n,C.Def (t,ty)))::tl ->
957 (S.subst_meta l (S.lift i t),
958 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 (*CSC: the following optimization is to avoid a possibly
970 expensive reduction that can be easily avoided and
971 that is quite frequent. However, this is better
972 handled using levels to control reduction *)
977 match List.nth context (n - 1) with
978 Some (_,C.Def (te,_)) -> S.lift n te
984 let subst',metasenv',ugraph' =
986 (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
987 * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
988 fo_unif_subst subst context metasenv optimized_t ct ugraph
989 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 optimized_t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
991 l @ [Some t],subst',metasenv',ugraph'
992 | Some t,Some (_,C.Decl ct) ->
993 let t',inferredty,subst',metasenv',ugraph1 =
994 type_of_aux subst metasenv context t ugraph
996 let subst'',metasenv'',ugraph2 =
999 subst' context metasenv' inferredty ct ugraph1
1000 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))))))
1002 l @ [Some t'], subst'',metasenv'',ugraph2
1004 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
1006 Invalid_argument _ ->
1010 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1011 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1012 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1014 and check_exp_named_subst metasubst metasenv context tl ugraph =
1015 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1017 [] -> [],metasubst,metasenv,ugraph
1019 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1021 CicSubstitution.subst_vars substs ty_uri in
1022 (* CSC: why was this code here? it is wrong
1023 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1024 Cic.Variable (_,Some bo,_,_) ->
1026 (RefineFailure (lazy
1027 "A variable with a body can not be explicit substituted"))
1028 | Cic.Variable (_,None,_,_) -> ()
1031 (RefineFailure (lazy
1032 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1035 let t',typeoft,metasubst',metasenv',ugraph2 =
1036 type_of_aux metasubst metasenv context t ugraph1 in
1037 let subst = uri,t' in
1038 let metasubst'',metasenv'',ugraph3 =
1041 metasubst' context metasenv' typeoft typeofvar ugraph2
1043 raise (RefineFailure (lazy
1044 ("Wrong Explicit Named Substitution: " ^
1045 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1046 " not unifiable with " ^
1047 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1049 (* FIXME: no mere tail recursive! *)
1050 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1051 check_exp_named_subst_aux
1052 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1054 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1056 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1059 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1062 let module C = Cic in
1063 let context_for_t2 = (Some (name,C.Decl s))::context in
1064 let t1'' = CicReduction.whd ~subst context t1 in
1065 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1066 match (t1'', t2'') with
1067 (C.Sort s1, C.Sort s2)
1068 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1069 (* different than Coq manual!!! *)
1070 C.Sort s2,subst,metasenv,ugraph
1071 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1072 let t' = CicUniv.fresh() in
1074 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1075 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1076 C.Sort (C.Type t'),subst,metasenv,ugraph2
1078 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1079 | (C.Sort _,C.Sort (C.Type t1)) ->
1080 C.Sort (C.Type t1),subst,metasenv,ugraph
1081 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1082 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1083 (* TODO how can we force the meta to become a sort? If we don't we
1084 * break the invariant that refine produce only well typed terms *)
1085 (* TODO if we check the non meta term and if it is a sort then we
1086 * are likely to know the exact value of the result e.g. if the rhs
1087 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1088 let (metasenv,idx) =
1089 CicMkImplicit.mk_implicit_sort metasenv subst in
1090 let (subst, metasenv,ugraph1) =
1092 fo_unif_subst subst context_for_t2 metasenv
1093 (C.Meta (idx,[])) t2'' ugraph
1094 with _ -> assert false (* unification against a metavariable *)
1096 t2'',subst,metasenv,ugraph1
1099 enrich localization_tbl s
1103 "%s is supposed to be a type, but its type is %s"
1104 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1105 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1107 enrich localization_tbl t
1111 "%s is supposed to be a type, but its type is %s"
1112 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1113 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1115 and avoid_double_coercion context subst metasenv ugraph t ty =
1116 if not !pack_coercions then
1117 t,ty,subst,metasenv,ugraph
1119 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1121 let source_carr = CoercGraph.source_of c2 in
1122 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1123 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1125 | CoercGraph.SomeCoercion candidates ->
1127 HExtlib.list_findopt
1128 (function (metasenv,last,c) ->
1130 | c when not (CoercGraph.is_composite c) ->
1131 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1134 let subst,metasenv,ugraph =
1135 fo_unif_subst subst context metasenv last head ugraph in
1136 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1141 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1142 let newt,_,subst,metasenv,ugraph =
1143 type_of_aux subst metasenv context c ugraph in
1144 debug_print (lazy "tipa...");
1145 let subst, metasenv, ugraph =
1146 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1147 fo_unif_subst subst context metasenv newt t ugraph
1149 debug_print (lazy "unifica...");
1150 Some (newt, ty, subst, metasenv, ugraph)
1152 | RefineFailure s | Uncertain s when not !pack_coercions->
1153 debug_print s; debug_print (lazy "stop\n");None
1154 | RefineFailure s | Uncertain s ->
1155 debug_print s;debug_print (lazy "goon\n");
1157 let old_pack_coercions = !pack_coercions in
1158 pack_coercions := false; (* to avoid diverging *)
1159 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1160 type_of_aux subst metasenv context c1_c2_implicit ugraph
1162 pack_coercions := old_pack_coercions;
1164 is_a_double_coercion refined_c1_c2_implicit
1170 match refined_c1_c2_implicit with
1171 | Cic.Appl l -> HExtlib.list_last l
1174 let subst, metasenv, ugraph =
1175 try fo_unif_subst subst context metasenv
1177 with RefineFailure s| Uncertain s->
1178 debug_print s;assert false
1180 let subst, metasenv, ugraph =
1181 fo_unif_subst subst context metasenv
1182 refined_c1_c2_implicit t ugraph
1184 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1186 | RefineFailure s | Uncertain s ->
1187 pack_coercions := true;debug_print s;None
1188 | exn -> pack_coercions := true; raise exn))
1191 (match selected with
1195 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1196 t, ty, subst, metasenv, ugraph)
1197 | _ -> t, ty, subst, metasenv, ugraph)
1199 t, ty, subst, metasenv, ugraph
1201 and typeof_list subst metasenv context ugraph l =
1202 let tlbody_and_type,subst,metasenv,ugraph =
1204 (fun x (res,subst,metasenv,ugraph) ->
1205 let x',ty,subst',metasenv',ugraph1 =
1206 type_of_aux subst metasenv context x ugraph
1208 (x', ty)::res,subst',metasenv',ugraph1
1209 ) l ([],subst,metasenv,ugraph)
1211 tlbody_and_type,subst,metasenv,ugraph
1214 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1216 (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1217 let fix_arity n metasenv context subst he hetype ugraph =
1218 let hetype = CicMetaSubst.apply_subst subst hetype in
1219 let src = CoercDb.coerc_carr_of_term hetype in
1220 let tgt = CoercDb.Fun 0 in
1221 match CoercGraph.look_for_coercion' metasenv subst context src tgt with
1222 | CoercGraph.NoCoercion -> []
1223 | CoercGraph.NotMetaClosed
1224 | CoercGraph.NotHandled _ ->
1225 raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1226 | CoercGraph.SomeCoercionToTgt candidates
1227 | CoercGraph.SomeCoercion candidates ->
1229 (fun (metasenv,last,coerc) ->
1231 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1233 let subst,metasenv,ugraph =
1234 fo_unif_subst subst context metasenv last he ugraph in
1235 debug_print (lazy ("New head: "^ pp coerc));
1237 CicTypeChecker.type_of_aux' ~subst metasenv context coerc
1240 debug_print (lazy (" has type: "^ pp tty));
1241 Some (coerc,tty,subst,metasenv,ugraph)
1243 | Uncertain _ | RefineFailure _
1244 | HExtlib.Localized (_,Uncertain _)
1245 | HExtlib.Localized (_,RefineFailure _) -> None
1246 | exn -> assert false)
1249 (* aux function to process the type of the head and the args in parallel *)
1250 let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1252 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1253 | (hete, hety)::tl as args ->
1254 match (CicReduction.whd ~subst context hetype) with
1255 | Cic.Prod (n,s,t) ->
1256 let arg,subst,metasenv,ugraph =
1257 coerce_to_something allow_coercions localization_tbl
1258 hete hety s subst metasenv context ugraph in
1260 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1261 ugraph (newargs@[arg]) tl
1264 match he, newargs with
1266 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1267 | _ -> Cic.Appl (he::List.map fst newargs)
1269 (*{{{*) debug_print (lazy
1271 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1272 "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1273 "\n but is applyed to: " ^ String.concat ";"
1274 (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1275 let possible_fixes =
1276 fix_arity (List.length args) metasenv context subst he hetype
1279 HExtlib.list_findopt
1280 (fun (he,hetype,subst,metasenv,ugraph) ->
1281 (* {{{ *)debug_print (lazy ("Try fix: "^
1282 CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1283 debug_print (lazy (" of type: "^
1284 CicMetaSubst.ppterm_in_context
1285 ~metasenv subst hetype context)); (* }}} *)
1287 Some (eat_prods_and_args
1288 metasenv subst context he hetype ugraph [] args)
1290 | RefineFailure _ | Uncertain _
1291 | HExtlib.Localized (_,RefineFailure _)
1292 | HExtlib.Localized (_,Uncertain _) -> None)
1298 (MoreArgsThanExpected
1299 (List.length args, RefineFailure (lazy "")))
1301 (* first we check if we are in the simple case of a meta closed term *)
1302 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1303 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1304 (* this optimization is to postpone fix_arity (the most common case)*)
1305 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1307 (* this (says CSC) is also useful to infer dependent types *)
1308 let pristinemenv = metasenv in
1309 let metasenv,hetype' =
1310 mk_prod_of_metas metasenv context subst args_bo_and_ty
1313 let subst,metasenv,ugraph =
1314 fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1316 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1317 with RefineFailure _ | Uncertain _ ->
1318 subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1320 let coerced_args,subst,metasenv,he,t,ugraph =
1323 metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1325 MoreArgsThanExpected (residuals,exn) ->
1326 more_args_than_expected localization_tbl metasenv
1327 subst he context hetype' residuals args_bo_and_ty exn
1329 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1331 and coerce_to_something
1332 allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1334 let module CS = CicSubstitution in
1335 let module CR = CicReduction in
1336 let cs_subst = CS.subst ~avoid_beta_redexes:true in
1337 let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1338 debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1340 CoercGraph.look_for_coercion metasenv subst context infty expty
1343 | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
1344 "coerce_atom_to_something fails since not meta closed"))
1345 | CoercGraph.NoCoercion
1346 | CoercGraph.SomeCoercionToTgt _
1347 | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
1348 "coerce_atom_to_something fails since no coercions found"))
1349 | CoercGraph.SomeCoercion candidates ->
1350 debug_print (lazy (string_of_int (List.length candidates) ^
1351 " candidates found"));
1352 let uncertain = ref false in
1356 (fun (metasenv,last,c) ->
1358 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1359 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1361 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
1362 "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
1364 debug_print (lazy ("FO_UNIF_SUBST: " ^
1365 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1366 let subst,metasenv,ugraph =
1367 fo_unif_subst subst context metasenv last t ugraph
1369 let newt,newhety,subst,metasenv,ugraph =
1370 type_of_aux subst metasenv context c ugraph in
1371 let newt, newty, subst, metasenv, ugraph =
1372 avoid_double_coercion context subst metasenv ugraph newt expty
1374 let subst,metasenv,ugraph =
1375 fo_unif_subst subst context metasenv newhety expty ugraph in
1376 Some ((newt,newty), subst, metasenv, ugraph)
1378 | Uncertain _ -> uncertain := true; None
1379 | RefineFailure _ -> None)
1384 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1392 | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1393 | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1395 let rec coerce_to_something_aux
1396 t infty expty subst metasenv context ugraph
1399 let subst, metasenv, ugraph =
1400 fo_unif_subst subst context metasenv infty expty ugraph
1402 (t, expty), subst, metasenv, ugraph
1403 with (Uncertain _ | RefineFailure _ as exn)
1404 when allow_coercions && !insert_coercions ->
1405 let whd = CicReduction.whd ~delta:false in
1406 let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1407 let infty = clean infty subst context in
1408 let expty = clean expty subst context in
1409 let t = clean t subst context in
1410 (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1411 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1412 CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1413 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1414 let (coerced,_),subst,metasenv,_ as result =
1415 match infty, expty, t with
1416 | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1417 (*{{{*) debug_print (lazy "FIX");
1419 [name,i,_(* infty *),bo] ->
1421 Some (Cic.Name name,Cic.Decl expty)::context in
1422 let (rel1, _), subst, metasenv, ugraph =
1423 coerce_to_something_aux (Cic.Rel 1)
1424 (CS.lift 1 expty) (CS.lift 1 infty) subst
1425 metasenv context_bo ugraph in
1426 let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1427 let (bo,_), subst, metasenv, ugraph =
1428 coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1430 metasenv context_bo ugraph
1432 (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1433 | _ -> assert false (* not implemented yet *)) (*}}}*)
1434 | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1435 (*{{{*) debug_print (lazy "CASE");
1436 (* {{{ helper functions *)
1437 let get_cl_and_left_p uri tyno outty ugraph =
1438 match CicEnvironment.get_obj ugraph uri with
1439 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1442 match CicReduction.whd ~delta:false ctx t with
1443 | Cic.Prod (name,src,tgt) ->
1444 let ctx = Some (name, Cic.Decl src) :: ctx in
1450 let rec skip_lambda_delifting t n =
1453 | Cic.Lambda (_,_,t),n ->
1454 skip_lambda_delifting
1455 (CS.subst (Cic.Implicit None) t) (n - 1)
1458 let get_l_r_p n = function
1459 | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1460 | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1461 HExtlib.split_nth n args
1464 let _, _, ty, cl = List.nth tl tyno in
1465 let pis = count_pis ty in
1466 let rno = pis - leftno in
1467 let t = skip_lambda_delifting outty rno in
1468 let left_p, _ = get_l_r_p leftno t in
1469 let instantiale_with_left cl =
1473 (fun t p -> match t with
1474 | Cic.Prod (_,_,t) ->
1480 let cl = instantiale_with_left (List.map snd cl) in
1481 cl, left_p, leftno, rno, ugraph
1484 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1487 let rec mkr n = function
1488 | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1491 CicReplace.replace_lifting
1492 ~equality:(fun _ -> CicUtil.alpha_equivalence)
1494 ~what:(matched::right_p)
1495 ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1499 | Cic.Lambda (name, src, tgt),_ ->
1500 Cic.Lambda (name, src,
1501 keep_lambdas_and_put_expty
1502 (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1503 (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1506 let eq_uri, eq, eq_refl =
1507 match LibraryObjects.eq_URI () with
1508 | None -> HLog.warn "no default equality"; raise exn
1509 | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1512 metasenv subst context uri tyno cty outty mty m leftno i
1514 let rec aux context outty par k mty m = function
1515 | Cic.Prod (name, src, tgt) ->
1518 (Some (name, Cic.Decl src) :: context)
1519 (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1520 (CS.lift 1 mty) (CS.lift 1 m) tgt
1522 Cic.Prod (name, src, t), k
1525 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1526 if par <> [] then Cic.Appl (k::par) else k
1528 Cic.Prod (Cic.Name "p",
1529 Cic.Appl [eq; mty; m; k],
1531 (CR.head_beta_reduce ~delta:false
1532 (Cic.Appl [outty;k])))),k
1533 | Cic.Appl (Cic.MutInd _::pl) ->
1534 let left_p,right_p = HExtlib.split_nth leftno pl in
1535 let has_rights = right_p <> [] in
1537 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1538 Cic.Appl (k::left_p@par)
1542 CicTypeChecker.type_of_aux' ~subst metasenv context k
1543 CicUniv.oblivion_ugraph
1545 | Cic.Appl (Cic.MutInd _::args),_ ->
1546 snd (HExtlib.split_nth leftno args)
1548 with CicTypeChecker.TypeCheckerFailure _-> assert false
1551 CR.head_beta_reduce ~delta:false
1552 (Cic.Appl (outty ::right_p @ [k])),k
1554 Cic.Prod (Cic.Name "p",
1555 Cic.Appl [eq; mty; m; k],
1557 (CR.head_beta_reduce ~delta:false
1558 (Cic.Appl (outty ::right_p @ [k]))))),k
1561 aux context outty [] 1 mty m cty
1563 let add_lambda_for_refl_m pbo rno mty m k cty =
1564 (* k lives in the right context *)
1565 if rno <> 0 then pbo else
1566 let rec aux mty m = function
1567 | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1568 Cic.Lambda (name,src,
1569 (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1571 Cic.Lambda (Cic.Name "p",
1572 Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1576 let add_pi_for_refl_m new_outty mty m rno =
1577 if rno <> 0 then new_outty else
1578 let rec aux m mty = function
1579 | Cic.Lambda (name, src, tgt) ->
1580 Cic.Lambda (name, src,
1581 aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1584 (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1588 in (* }}} end helper functions *)
1589 (* constructors types with left params already instantiated *)
1590 let outty = CicMetaSubst.apply_subst subst outty in
1591 let cl, left_p, leftno,rno,ugraph =
1592 get_cl_and_left_p uri tyno outty ugraph
1597 CicTypeChecker.type_of_aux' ~subst metasenv context m
1598 CicUniv.oblivion_ugraph
1600 | Cic.MutInd _ as mty,_ -> [], mty
1601 | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
1602 snd (HExtlib.split_nth leftno args), mty
1604 with CicTypeChecker.TypeCheckerFailure _ -> assert false
1607 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1610 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1611 ~metasenv subst new_outty context));
1612 let _,pl,subst,metasenv,ugraph =
1614 (fun cty pbo (i, acc, s, menv, ugraph) ->
1615 (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1616 * (new_)outty right_par (K_i left_par k_par) *)
1618 add_params menv s context uri tyno
1619 cty outty mty m leftno i in
1621 (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1622 ~metasenv subst infty_pbo context));
1623 let expty_pbo, k = (* k is (K_i left_par k_par) *)
1624 add_params menv s context uri tyno
1625 cty new_outty mty m leftno i in
1627 (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1628 ~metasenv subst expty_pbo context));
1629 let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1631 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1632 ~metasenv subst pbo context));
1633 let (pbo, _), subst, metasenv, ugraph =
1634 coerce_to_something_aux pbo infty_pbo expty_pbo
1635 s menv context ugraph
1638 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1639 ~metasenv subst pbo context));
1640 (i-1, pbo::acc, subst, metasenv, ugraph))
1641 cl pl (List.length pl, [], subst, metasenv, ugraph)
1643 let new_outty = add_pi_for_refl_m new_outty mty m rno in
1645 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1646 ~metasenv subst new_outty context));
1649 let refl_m=Cic.Appl[eq_refl;mty;m]in
1650 Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1652 Cic.MutCase(uri,tyno,new_outty,m,pl)
1654 (t, expty), subst, metasenv, ugraph (*}}}*)
1655 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1656 (*{{{*) debug_print (lazy "LAM");
1658 FreshNamesGenerator.mk_fresh_name
1659 ~subst metasenv context ~typ:src2 Cic.Anonymous
1661 let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1662 (* contravariant part: the argument of f:src->ty *)
1663 let (rel1, _), subst, metasenv, ugraph =
1664 coerce_to_something_aux
1665 (Cic.Rel 1) (CS.lift 1 src2)
1666 (CS.lift 1 src) subst metasenv context_src2 ugraph
1668 (* covariant part: the result of f(c x); x:src2; (c x):src *)
1671 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1672 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1674 (* we fix the possible dependency problem in the source ty *)
1675 let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1676 let (bo, _), subst, metasenv, ugraph =
1677 coerce_to_something_aux
1678 bo ty ty2 subst metasenv context_src2 ugraph
1680 let coerced = Cic.Lambda (name_t,src2, bo) in
1681 (coerced, expty), subst, metasenv, ugraph (*}}}*)
1683 (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1684 ~metasenv subst infty context ^ " ==> " ^
1685 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1686 coerce_atom_to_something
1687 t infty expty subst metasenv context ugraph (*}}}*)
1689 debug_print (lazy ("COERCE TO SOMETHING END: "^
1690 CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1694 coerce_to_something_aux t infty expty subst metasenv context ugraph
1695 with Uncertain _ | RefineFailure _ as exn ->
1698 CicMetaSubst.ppterm_in_context metasenv subst t context ^
1699 " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1700 infty context ^ " but is here used with type " ^
1701 CicMetaSubst.ppterm_in_context metasenv subst expty context)
1703 enrich localization_tbl ~f t exn
1705 and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1706 match CicReduction.whd ~delta:false ~subst context infty with
1707 | Cic.Meta _ | Cic.Sort _ ->
1708 t,infty, subst, metasenv, ugraph
1710 debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1711 ~metasenv subst src context));
1712 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1714 let (t, ty_t), subst, metasenv, ugraph =
1715 coerce_to_something true
1716 localization_tbl t src tgt subst metasenv context ugraph
1718 debug_print (lazy ("COERCE TO SORT END: "^
1719 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1720 t, ty_t, subst, metasenv, ugraph
1721 with HExtlib.Localized (_, exn) ->
1723 lazy ("(7)The term " ^
1724 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1725 ^ " is not a type since it has type " ^
1726 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1727 ^ " that is not a sort")
1729 enrich localization_tbl ~f t exn
1732 (* eat prods ends here! *)
1734 let t',ty,subst',metasenv',ugraph1 =
1735 type_of_aux [] metasenv context t ugraph
1737 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1738 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1739 (* Andrea: ho rimesso qui l'applicazione della subst al
1740 metasenv dopo che ho droppato l'invariante che il metsaenv
1741 e' sempre istanziato *)
1742 let substituted_metasenv =
1743 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1745 (* substituted_t,substituted_ty,substituted_metasenv *)
1746 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1748 if clean_dummy_dependent_types then
1749 FreshNamesGenerator.clean_dummy_dependent_types substituted_t
1750 else substituted_t in
1752 if clean_dummy_dependent_types then
1753 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty
1754 else substituted_ty in
1755 let cleaned_metasenv =
1756 if clean_dummy_dependent_types then
1758 (function (n,context,ty) ->
1759 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1764 | Some (n, Cic.Decl t) ->
1766 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1767 | Some (n, Cic.Def (bo,ty)) ->
1768 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1769 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
1771 Some (n, Cic.Def (bo',ty'))
1775 ) substituted_metasenv
1777 substituted_metasenv
1779 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1782 let undebrujin uri typesno tys t =
1785 (fun (name,_,_,_) (i,t) ->
1786 (* here the explicit_named_substituion is assumed to be *)
1788 let t' = Cic.MutInd (uri,i,[]) in
1789 let t = CicSubstitution.subst t' t in
1791 ) tys (typesno - 1,t))
1793 let map_first_n n start f g l =
1794 let rec aux acc k l =
1797 | [] -> raise (Invalid_argument "map_first_n")
1798 | hd :: tl -> f hd k (aux acc (k+1) tl)
1804 (*CSC: this is a very rough approximation; to be finished *)
1805 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1806 let subst,metasenv,ugraph,tys =
1808 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1809 let subst,metasenv,ugraph,cl =
1811 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1812 let rec aux ctx k subst = function
1813 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1814 let subst,metasenv,ugraph,tl =
1816 (subst,metasenv,ugraph,[])
1817 (fun t n (subst,metasenv,ugraph,acc) ->
1818 let subst,metasenv,ugraph =
1820 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1822 subst,metasenv,ugraph,(t::acc))
1823 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1826 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1827 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1828 subst,metasenv,ugraph,t
1829 | Cic.Prod (name,s,t) ->
1830 let ctx = (Some (name,Cic.Decl s))::ctx in
1831 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1832 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1836 (lazy "not well formed constructor type"))
1838 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1839 subst,metasenv,ugraph,(name,ty) :: acc)
1840 cl (subst,metasenv,ugraph,[])
1842 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1843 tys ([],metasenv,ugraph,[])
1845 let substituted_tys =
1847 (fun (name,ind,arity,cl) ->
1849 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1851 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1854 metasenv,ugraph,substituted_tys
1856 let typecheck metasenv uri obj ~localization_tbl =
1857 let ugraph = CicUniv.oblivion_ugraph in
1859 Cic.Constant (name,Some bo,ty,args,attrs) ->
1860 (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
1861 since type_of_aux' destroys localization information (which are
1862 preserved by type_of_aux *)
1865 Cic.CicHash.find localization_tbl bo
1867 HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
1869 let bo',boty,metasenv,ugraph =
1870 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1871 let ty',_,metasenv,ugraph =
1872 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1873 let subst,metasenv,ugraph =
1875 fo_unif_subst [] [] metasenv boty ty' ugraph
1878 | Uncertain _ as exn ->
1881 CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
1883 CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
1884 " but is here used with type " ^
1885 CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
1889 RefineFailure _ -> RefineFailure msg
1890 | Uncertain _ -> Uncertain msg
1893 raise (HExtlib.Localized (loc exn',exn'))
1895 let bo' = CicMetaSubst.apply_subst subst bo' in
1896 let ty' = CicMetaSubst.apply_subst subst ty' in
1897 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1898 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1899 | Cic.Constant (name,None,ty,args,attrs) ->
1900 let ty',_,metasenv,ugraph =
1901 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1903 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1904 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1905 assert (metasenv' = metasenv);
1906 (* Here we do not check the metasenv for correctness *)
1907 let bo',boty,metasenv,ugraph =
1908 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1909 let ty',sort,metasenv,ugraph =
1910 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1914 (* instead of raising Uncertain, let's hope that the meta will become
1917 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1919 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1920 let bo' = CicMetaSubst.apply_subst subst bo' in
1921 let ty' = CicMetaSubst.apply_subst subst ty' in
1922 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1923 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1924 | Cic.Variable _ -> assert false (* not implemented *)
1925 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1926 (*CSC: this code is greately simplified and many many checks are missing *)
1927 (*CSC: e.g. the constructors are not required to build their own types, *)
1928 (*CSC: the arities are not required to have as type a sort, etc. *)
1929 let uri = match uri with Some uri -> uri | None -> assert false in
1930 let typesno = List.length tys in
1931 (* first phase: we fix only the types *)
1932 let metasenv,ugraph,tys =
1934 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1935 let ty',_,metasenv,ugraph =
1936 (* clean_dummy_dependent_types: false to avoid cleaning the names
1937 of the left products, that must be identical to those of the
1938 constructors; however, non-left products should probably be
1940 type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl
1941 metasenv [] ty ugraph
1943 metasenv,ugraph,(name,b,ty',cl)::res
1944 ) tys (metasenv,ugraph,[]) in
1946 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1947 (* second phase: we fix only the constructors *)
1948 let saved_menv = metasenv in
1949 let metasenv,ugraph,tys =
1951 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1952 let metasenv,ugraph,cl' =
1954 (fun (name,ty) (metasenv,ugraph,res) ->
1956 CicTypeChecker.debrujin_constructor
1957 ~cb:(relocalize localization_tbl) uri typesno [] ty in
1958 let ty',_,metasenv,ugraph =
1959 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1960 let ty' = undebrujin uri typesno tys ty' in
1961 metasenv@saved_menv,ugraph,(name,ty')::res
1962 ) cl (metasenv,ugraph,[])
1964 metasenv,ugraph,(name,b,ty,cl')::res
1965 ) tys (metasenv,ugraph,[]) in
1966 (* third phase: we check the positivity condition *)
1967 let metasenv,ugraph,tys =
1968 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1970 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1973 (* sara' piu' veloce che raffinare da zero? mah.... *)
1974 let pack_coercion metasenv ctx t =
1975 let module C = Cic in
1976 let rec merge_coercions ctx =
1977 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1979 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1980 | C.Meta (n,subst) ->
1983 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1986 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1987 | C.Prod (name,so,dest) ->
1988 let ctx' = (Some (name,C.Decl so))::ctx in
1989 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1990 | C.Lambda (name,so,dest) ->
1991 let ctx' = (Some (name,C.Decl so))::ctx in
1992 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1993 | C.LetIn (name,so,ty,dest) ->
1994 let ctx' = Some (name,(C.Def (so,ty)))::ctx in
1996 (name, merge_coercions ctx so, merge_coercions ctx ty,
1997 merge_coercions ctx' dest)
1999 let l = List.map (merge_coercions ctx) l in
2001 let b,_,_,_,_ = is_a_double_coercion t in
2003 let ugraph = CicUniv.oblivion_ugraph in
2004 let old_insert_coercions = !insert_coercions in
2005 insert_coercions := false;
2006 let newt, _, menv, _ =
2008 type_of_aux' metasenv ctx t ugraph
2009 with RefineFailure _ | Uncertain _ ->
2012 insert_coercions := old_insert_coercions;
2013 if metasenv <> [] || menv = [] then
2016 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
2019 | C.Var (uri,exp_named_subst) ->
2020 let exp_named_subst = List.map aux exp_named_subst in
2021 C.Var (uri, exp_named_subst)
2022 | C.Const (uri,exp_named_subst) ->
2023 let exp_named_subst = List.map aux exp_named_subst in
2024 C.Const (uri, exp_named_subst)
2025 | C.MutInd (uri,tyno,exp_named_subst) ->
2026 let exp_named_subst = List.map aux exp_named_subst in
2027 C.MutInd (uri,tyno,exp_named_subst)
2028 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
2029 let exp_named_subst = List.map aux exp_named_subst in
2030 C.MutConstruct (uri,tyno,consno,exp_named_subst)
2031 | C.MutCase (uri,tyno,out,te,pl) ->
2032 let pl = List.map (merge_coercions ctx) pl in
2033 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
2034 | C.Fix (fno, fl) ->
2037 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2042 (fun (name,idx,ty,bo) ->
2043 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
2047 | C.CoFix (fno, fl) ->
2050 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2055 (fun (name,ty,bo) ->
2056 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
2061 merge_coercions ctx t
2064 let pack_coercion_metasenv conjectures = conjectures (*
2066 TASSI: this code war written when coercions were a toy,
2067 now packing coercions involves unification thus
2068 the metasenv may change, and this pack coercion
2069 does not handle that.
2071 let module C = Cic in
2073 (fun (i, ctx, ty) ->
2079 Some (name, C.Decl t) ->
2080 Some (name, C.Decl (pack_coercion conjectures ctx t))
2081 | Some (name, C.Def (t,None)) ->
2082 Some (name,C.Def (pack_coercion conjectures ctx t,None))
2083 | Some (name, C.Def (t,Some ty)) ->
2084 Some (name, C.Def (pack_coercion conjectures ctx t,
2085 Some (pack_coercion conjectures ctx ty)))
2091 ((i,ctx,pack_coercion conjectures ctx ty))
2096 let pack_coercion_obj obj = obj (*
2098 TASSI: this code war written when coercions were a toy,
2099 now packing coercions involves unification thus
2100 the metasenv may change, and this pack coercion
2101 does not handle that.
2103 let module C = Cic in
2105 | C.Constant (id, body, ty, params, attrs) ->
2109 | Some body -> Some (pack_coercion [] [] body)
2111 let ty = pack_coercion [] [] ty in
2112 C.Constant (id, body, ty, params, attrs)
2113 | C.Variable (name, body, ty, params, attrs) ->
2117 | Some body -> Some (pack_coercion [] [] body)
2119 let ty = pack_coercion [] [] ty in
2120 C.Variable (name, body, ty, params, attrs)
2121 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2122 let conjectures = pack_coercion_metasenv conjectures in
2123 let body = pack_coercion conjectures [] body in
2124 let ty = pack_coercion conjectures [] ty in
2125 C.CurrentProof (name, conjectures, body, ty, params, attrs)
2126 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2129 (fun (name, ind, arity, cl) ->
2130 let arity = pack_coercion [] [] arity in
2132 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2134 (name, ind, arity, cl))
2137 C.InductiveDefinition (indtys, params, leftno, attrs) *)
2142 let type_of_aux' metasenv context term =
2145 type_of_aux' metasenv context term in
2147 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2149 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2152 | RefineFailure msg as e ->
2153 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2155 | Uncertain msg as e ->
2156 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2160 let profiler2 = HExtlib.profile "CicRefine"
2162 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2163 profiler2.HExtlib.profile
2164 (type_of_aux' ?localization_tbl metasenv context term) ugraph
2166 let typecheck ~localization_tbl metasenv uri obj =
2167 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2169 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2170 (* vim:set foldmethod=marker: *)