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.head_beta_reduce ~delta:false
805 ~upto:(List.length args) appl
808 fo_unif_subst subst context metasenv instance instance'
812 enrich localization_tbl p exn
815 CicMetaSubst.ppterm_in_context ~metasenv subst p
816 context ^ " has type " ^
817 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
818 context ^ " but is here used with type " ^
819 CicMetaSubst.ppterm_in_context ~metasenv subst instance
821 (subst,metasenv,ugraph5) pl' outtypeinstances
823 C.MutCase (uri, i, outtype, term', pl'),
824 CicReduction.head_beta_reduce
825 (CicMetaSubst.apply_subst subst
826 (C.Appl(outtype::right_args@[term']))),
827 subst,metasenv,ugraph6)
829 let fl_ty',subst,metasenv,types,ugraph1,len =
831 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
832 let ty',_,subst',metasenv',ugraph1 =
833 type_of_aux subst metasenv context ty ugraph
835 fl @ [ty'],subst',metasenv',
836 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
837 :: types, ugraph, len+1
838 ) ([],subst,metasenv,[],ugraph,0) fl
840 let context' = types@context in
841 let fl_bo',subst,metasenv,ugraph2 =
843 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
844 let bo',ty_of_bo,subst,metasenv,ugraph1 =
845 type_of_aux subst metasenv context' bo ugraph in
846 let expected_ty = CicSubstitution.lift len ty in
847 let subst',metasenv',ugraph' =
849 fo_unif_subst subst context' metasenv
850 ty_of_bo expected_ty ugraph1
853 enrich localization_tbl bo exn
856 CicMetaSubst.ppterm_in_context ~metasenv subst bo
857 context' ^ " has type " ^
858 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
859 context' ^ " but is here used with type " ^
860 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
863 fl @ [bo'] , subst',metasenv',ugraph'
864 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
866 let ty = List.nth fl_ty' i in
867 (* now we have the new ty in fl_ty', the new bo in fl_bo',
868 * and we want the new fl with bo' and ty' injected in the right
871 let rec map3 f l1 l2 l3 =
874 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
877 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
880 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
882 let fl_ty',subst,metasenv,types,ugraph1,len =
884 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
885 let ty',_,subst',metasenv',ugraph1 =
886 type_of_aux subst metasenv context ty ugraph
888 fl @ [ty'],subst',metasenv',
889 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
890 types, ugraph1, len+1
891 ) ([],subst,metasenv,[],ugraph,0) fl
893 let context' = types@context in
894 let fl_bo',subst,metasenv,ugraph2 =
896 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
897 let bo',ty_of_bo,subst,metasenv,ugraph1 =
898 type_of_aux subst metasenv context' bo ugraph in
899 let expected_ty = CicSubstitution.lift len ty in
900 let subst',metasenv',ugraph' =
902 fo_unif_subst subst context' metasenv
903 ty_of_bo expected_ty ugraph1
906 enrich localization_tbl bo exn
909 CicMetaSubst.ppterm_in_context ~metasenv subst bo
910 context' ^ " has type " ^
911 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
912 context' ^ " but is here used with type " ^
913 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
916 fl @ [bo'],subst',metasenv',ugraph'
917 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
919 let ty = List.nth fl_ty' i in
920 (* now we have the new ty in fl_ty', the new bo in fl_bo',
921 * and we want the new fl with bo' and ty' injected in the right
924 let rec map3 f l1 l2 l3 =
927 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
930 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
933 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
935 relocalize localization_tbl t t';
938 (* check_metasenv_consistency checks that the "canonical" context of a
939 metavariable is consitent - up to relocation via the relocation list l -
940 with the actual context *)
941 and check_metasenv_consistency
942 metano subst metasenv context canonical_context l ugraph
944 let module C = Cic in
945 let module R = CicReduction in
946 let module S = CicSubstitution in
947 let lifted_canonical_context =
951 | (Some (n,C.Decl t))::tl ->
952 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
953 | None::tl -> None::(aux (i+1) tl)
954 | (Some (n,C.Def (t,ty)))::tl ->
958 (S.subst_meta l (S.lift i t),
959 S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
961 aux 1 canonical_context
965 (fun (l,subst,metasenv,ugraph) t ct ->
968 l @ [None],subst,metasenv,ugraph
969 | Some t,Some (_,C.Def (ct,_)) ->
970 (*CSC: the following optimization is to avoid a possibly
971 expensive reduction that can be easily avoided and
972 that is quite frequent. However, this is better
973 handled using levels to control reduction *)
978 match List.nth context (n - 1) with
979 Some (_,C.Def (te,_)) -> S.lift n te
985 let subst',metasenv',ugraph' =
987 (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
988 * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
989 fo_unif_subst subst context metasenv optimized_t ct ugraph
990 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))))))
992 l @ [Some t],subst',metasenv',ugraph'
993 | Some t,Some (_,C.Decl ct) ->
994 let t',inferredty,subst',metasenv',ugraph1 =
995 type_of_aux subst metasenv context t ugraph
997 let subst'',metasenv'',ugraph2 =
1000 subst' context metasenv' inferredty ct ugraph1
1001 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))))))
1003 l @ [Some t'], subst'',metasenv'',ugraph2
1005 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
1007 Invalid_argument _ ->
1011 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1012 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1013 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1015 and check_exp_named_subst metasubst metasenv context tl ugraph =
1016 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1018 [] -> [],metasubst,metasenv,ugraph
1020 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1022 CicSubstitution.subst_vars substs ty_uri in
1023 (* CSC: why was this code here? it is wrong
1024 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1025 Cic.Variable (_,Some bo,_,_) ->
1027 (RefineFailure (lazy
1028 "A variable with a body can not be explicit substituted"))
1029 | Cic.Variable (_,None,_,_) -> ()
1032 (RefineFailure (lazy
1033 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1036 let t',typeoft,metasubst',metasenv',ugraph2 =
1037 type_of_aux metasubst metasenv context t ugraph1 in
1038 let subst = uri,t' in
1039 let metasubst'',metasenv'',ugraph3 =
1042 metasubst' context metasenv' typeoft typeofvar ugraph2
1044 raise (RefineFailure (lazy
1045 ("Wrong Explicit Named Substitution: " ^
1046 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1047 " not unifiable with " ^
1048 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1050 (* FIXME: no mere tail recursive! *)
1051 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1052 check_exp_named_subst_aux
1053 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1055 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1057 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1060 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1063 let module C = Cic in
1064 let context_for_t2 = (Some (name,C.Decl s))::context in
1065 let t1'' = CicReduction.whd ~subst context t1 in
1066 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1067 match (t1'', t2'') with
1068 | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) ->
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.CProp t1), C.Sort (C.CProp t2)) ->
1080 let t' = CicUniv.fresh() in
1082 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1083 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1084 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1086 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1087 | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
1088 let t' = CicUniv.fresh() in
1090 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1091 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1092 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1094 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1095 | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
1096 let t' = CicUniv.fresh() in
1098 let ugraph1 = CicUniv.add_gt t' t1 ugraph in
1099 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1100 C.Sort (C.Type t'),subst,metasenv,ugraph2
1102 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1103 | (C.Sort _,C.Sort (C.Type t1)) ->
1104 C.Sort (C.Type t1),subst,metasenv,ugraph
1105 | (C.Sort _,C.Sort (C.CProp t1)) ->
1106 C.Sort (C.CProp t1),subst,metasenv,ugraph
1107 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1108 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1109 (* TODO how can we force the meta to become a sort? If we don't we
1110 * break the invariant that refine produce only well typed terms *)
1111 (* TODO if we check the non meta term and if it is a sort then we
1112 * are likely to know the exact value of the result e.g. if the rhs
1113 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1114 let (metasenv,idx) =
1115 CicMkImplicit.mk_implicit_sort metasenv subst in
1116 let (subst, metasenv,ugraph1) =
1118 fo_unif_subst subst context_for_t2 metasenv
1119 (C.Meta (idx,[])) t2'' ugraph
1120 with _ -> assert false (* unification against a metavariable *)
1122 t2'',subst,metasenv,ugraph1
1125 enrich localization_tbl s
1129 "%s is supposed to be a type, but its type is %s"
1130 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1131 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1133 enrich localization_tbl t
1137 "%s is supposed to be a type, but its type is %s"
1138 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1139 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1141 and avoid_double_coercion context subst metasenv ugraph t ty =
1142 if not !pack_coercions then
1143 t,ty,subst,metasenv,ugraph
1145 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1147 let source_carr = CoercGraph.source_of c2 in
1148 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1149 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1151 | CoercGraph.SomeCoercion candidates ->
1153 HExtlib.list_findopt
1154 (function (metasenv,last,c) ->
1156 | c when not (CoercGraph.is_composite c) ->
1157 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1160 let subst,metasenv,ugraph =
1161 fo_unif_subst subst context metasenv last head ugraph in
1162 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1167 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1168 let newt,_,subst,metasenv,ugraph =
1169 type_of_aux subst metasenv context c ugraph in
1170 debug_print (lazy "tipa...");
1171 let subst, metasenv, ugraph =
1172 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1173 fo_unif_subst subst context metasenv newt t ugraph
1175 debug_print (lazy "unifica...");
1176 Some (newt, ty, subst, metasenv, ugraph)
1178 | RefineFailure s | Uncertain s when not !pack_coercions->
1179 debug_print s; debug_print (lazy "stop\n");None
1180 | RefineFailure s | Uncertain s ->
1181 debug_print s;debug_print (lazy "goon\n");
1183 let old_pack_coercions = !pack_coercions in
1184 pack_coercions := false; (* to avoid diverging *)
1185 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1186 type_of_aux subst metasenv context c1_c2_implicit ugraph
1188 pack_coercions := old_pack_coercions;
1190 is_a_double_coercion refined_c1_c2_implicit
1196 match refined_c1_c2_implicit with
1197 | Cic.Appl l -> HExtlib.list_last l
1200 let subst, metasenv, ugraph =
1201 try fo_unif_subst subst context metasenv
1203 with RefineFailure s| Uncertain s->
1204 debug_print s;assert false
1206 let subst, metasenv, ugraph =
1207 fo_unif_subst subst context metasenv
1208 refined_c1_c2_implicit t ugraph
1210 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1212 | RefineFailure s | Uncertain s ->
1213 pack_coercions := true;debug_print s;None
1214 | exn -> pack_coercions := true; raise exn))
1217 (match selected with
1221 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1222 t, ty, subst, metasenv, ugraph)
1223 | _ -> t, ty, subst, metasenv, ugraph)
1225 t, ty, subst, metasenv, ugraph
1227 and typeof_list subst metasenv context ugraph l =
1228 let tlbody_and_type,subst,metasenv,ugraph =
1230 (fun x (res,subst,metasenv,ugraph) ->
1231 let x',ty,subst',metasenv',ugraph1 =
1232 type_of_aux subst metasenv context x ugraph
1234 (x', ty)::res,subst',metasenv',ugraph1
1235 ) l ([],subst,metasenv,ugraph)
1237 tlbody_and_type,subst,metasenv,ugraph
1240 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1242 (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1243 let fix_arity n metasenv context subst he hetype ugraph =
1244 let hetype = CicMetaSubst.apply_subst subst hetype in
1245 let src = CoercDb.coerc_carr_of_term hetype in
1246 let tgt = CoercDb.Fun 0 in
1247 match CoercGraph.look_for_coercion' metasenv subst context src tgt with
1248 | CoercGraph.NoCoercion -> []
1249 | CoercGraph.NotMetaClosed
1250 | CoercGraph.NotHandled _ ->
1251 raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1252 | CoercGraph.SomeCoercionToTgt candidates
1253 | CoercGraph.SomeCoercion candidates ->
1255 (fun (metasenv,last,coerc) ->
1257 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1259 let subst,metasenv,ugraph =
1260 fo_unif_subst subst context metasenv last he ugraph in
1261 debug_print (lazy ("New head: "^ pp coerc));
1263 CicTypeChecker.type_of_aux' ~subst metasenv context coerc
1266 debug_print (lazy (" has type: "^ pp tty));
1267 Some (coerc,tty,subst,metasenv,ugraph)
1269 | Uncertain _ | RefineFailure _
1270 | HExtlib.Localized (_,Uncertain _)
1271 | HExtlib.Localized (_,RefineFailure _) -> None
1272 | exn -> assert false)
1275 (* aux function to process the type of the head and the args in parallel *)
1276 let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1278 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1279 | (hete, hety)::tl as args ->
1280 match (CicReduction.whd ~subst context hetype) with
1281 | Cic.Prod (n,s,t) ->
1282 let arg,subst,metasenv,ugraph =
1283 coerce_to_something allow_coercions localization_tbl
1284 hete hety s subst metasenv context ugraph in
1286 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1287 ugraph (newargs@[arg]) tl
1290 match he, newargs with
1292 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1293 | _ -> Cic.Appl (he::List.map fst newargs)
1295 (*{{{*) debug_print (lazy
1297 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1298 "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1299 "\n but is applyed to: " ^ String.concat ";"
1300 (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1301 let possible_fixes =
1302 fix_arity (List.length args) metasenv context subst he hetype
1305 HExtlib.list_findopt
1306 (fun (he,hetype,subst,metasenv,ugraph) ->
1307 (* {{{ *)debug_print (lazy ("Try fix: "^
1308 CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1309 debug_print (lazy (" of type: "^
1310 CicMetaSubst.ppterm_in_context
1311 ~metasenv subst hetype context)); (* }}} *)
1313 Some (eat_prods_and_args
1314 metasenv subst context he hetype ugraph [] args)
1316 | RefineFailure _ | Uncertain _
1317 | HExtlib.Localized (_,RefineFailure _)
1318 | HExtlib.Localized (_,Uncertain _) -> None)
1324 (MoreArgsThanExpected
1325 (List.length args, RefineFailure (lazy "")))
1327 (* first we check if we are in the simple case of a meta closed term *)
1328 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1329 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1330 (* this optimization is to postpone fix_arity (the most common case)*)
1331 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1333 (* this (says CSC) is also useful to infer dependent types *)
1334 let pristinemenv = metasenv in
1335 let metasenv,hetype' =
1336 mk_prod_of_metas metasenv context subst args_bo_and_ty
1339 let subst,metasenv,ugraph =
1340 fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1342 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1343 with RefineFailure _ | Uncertain _ ->
1344 subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1346 let coerced_args,subst,metasenv,he,t,ugraph =
1349 metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1351 MoreArgsThanExpected (residuals,exn) ->
1352 more_args_than_expected localization_tbl metasenv
1353 subst he context hetype' residuals args_bo_and_ty exn
1355 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1357 and coerce_to_something
1358 allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1360 let module CS = CicSubstitution in
1361 let module CR = CicReduction in
1362 let cs_subst = CS.subst ~avoid_beta_redexes:true in
1363 let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1364 debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1366 CoercGraph.look_for_coercion metasenv subst context infty expty
1369 | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
1370 "coerce_atom_to_something fails since not meta closed"))
1371 | CoercGraph.NoCoercion
1372 | CoercGraph.SomeCoercionToTgt _
1373 | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
1374 "coerce_atom_to_something fails since no coercions found"))
1375 | CoercGraph.SomeCoercion candidates ->
1376 debug_print (lazy (string_of_int (List.length candidates) ^
1377 " candidates found"));
1378 let uncertain = ref false in
1382 (fun (metasenv,last,c) ->
1384 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1385 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1387 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
1388 "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
1390 debug_print (lazy ("FO_UNIF_SUBST: " ^
1391 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1392 let subst,metasenv,ugraph =
1393 fo_unif_subst subst context metasenv last t ugraph
1395 let newt,newhety,subst,metasenv,ugraph =
1396 type_of_aux subst metasenv context c ugraph in
1397 let newt, newty, subst, metasenv, ugraph =
1398 avoid_double_coercion context subst metasenv ugraph newt expty
1400 let subst,metasenv,ugraph =
1401 fo_unif_subst subst context metasenv newhety expty ugraph in
1402 Some ((newt,newty), subst, metasenv, ugraph)
1404 | Uncertain _ -> uncertain := true; None
1405 | RefineFailure _ -> None)
1410 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1418 | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1419 | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1421 let rec coerce_to_something_aux
1422 t infty expty subst metasenv context ugraph
1425 let subst, metasenv, ugraph =
1426 fo_unif_subst subst context metasenv infty expty ugraph
1428 (t, expty), subst, metasenv, ugraph
1429 with (Uncertain _ | RefineFailure _ as exn)
1430 when allow_coercions && !insert_coercions ->
1431 let whd = CicReduction.whd ~delta:false in
1432 let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1433 let infty = clean infty subst context in
1434 let expty = clean expty subst context in
1435 let t = clean t subst context in
1436 (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1437 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1438 CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1439 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1440 let (coerced,_),subst,metasenv,_ as result =
1441 match infty, expty, t with
1442 | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1443 (*{{{*) debug_print (lazy "FIX");
1445 [name,i,_(* infty *),bo] ->
1447 Some (Cic.Name name,Cic.Decl expty)::context in
1448 let (rel1, _), subst, metasenv, ugraph =
1449 coerce_to_something_aux (Cic.Rel 1)
1450 (CS.lift 1 expty) (CS.lift 1 infty) subst
1451 metasenv context_bo ugraph in
1452 let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1453 let (bo,_), subst, metasenv, ugraph =
1454 coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1456 metasenv context_bo ugraph
1458 (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1459 | _ -> assert false (* not implemented yet *)) (*}}}*)
1460 | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1461 (*{{{*) debug_print (lazy "CASE");
1462 (* {{{ helper functions *)
1463 let get_cl_and_left_p uri tyno outty ugraph =
1464 match CicEnvironment.get_obj ugraph uri with
1465 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1468 match CicReduction.whd ~delta:false ctx t with
1469 | Cic.Prod (name,src,tgt) ->
1470 let ctx = Some (name, Cic.Decl src) :: ctx in
1476 let rec skip_lambda_delifting t n =
1479 | Cic.Lambda (_,_,t),n ->
1480 skip_lambda_delifting
1481 (CS.subst (Cic.Implicit None) t) (n - 1)
1484 let get_l_r_p n = function
1485 | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1486 | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1487 HExtlib.split_nth n args
1490 let _, _, ty, cl = List.nth tl tyno in
1491 let pis = count_pis ty in
1492 let rno = pis - leftno in
1493 let t = skip_lambda_delifting outty rno in
1494 let left_p, _ = get_l_r_p leftno t in
1495 let instantiale_with_left cl =
1499 (fun t p -> match t with
1500 | Cic.Prod (_,_,t) ->
1506 let cl = instantiale_with_left (List.map snd cl) in
1507 cl, left_p, leftno, rno, ugraph
1510 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1513 let rec mkr n = function
1514 | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1517 CicReplace.replace_lifting
1518 ~equality:(fun _ -> CicUtil.alpha_equivalence)
1520 ~what:(matched::right_p)
1521 ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1525 | Cic.Lambda (name, src, tgt),_ ->
1526 Cic.Lambda (name, src,
1527 keep_lambdas_and_put_expty
1528 (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1529 (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1532 let eq_uri, eq, eq_refl =
1533 match LibraryObjects.eq_URI () with
1534 | None -> HLog.warn "no default equality"; raise exn
1535 | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1538 metasenv subst context uri tyno cty outty mty m leftno i
1540 let rec aux context outty par k mty m = function
1541 | Cic.Prod (name, src, tgt) ->
1544 (Some (name, Cic.Decl src) :: context)
1545 (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1546 (CS.lift 1 mty) (CS.lift 1 m) tgt
1548 Cic.Prod (name, src, t), k
1551 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1552 if par <> [] then Cic.Appl (k::par) else 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;k])))),k
1559 | Cic.Appl (Cic.MutInd _::pl) ->
1560 let left_p,right_p = HExtlib.split_nth leftno pl in
1561 let has_rights = right_p <> [] in
1563 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1564 Cic.Appl (k::left_p@par)
1568 CicTypeChecker.type_of_aux' ~subst metasenv context k
1569 CicUniv.oblivion_ugraph
1571 | Cic.Appl (Cic.MutInd _::args),_ ->
1572 snd (HExtlib.split_nth leftno args)
1574 with CicTypeChecker.TypeCheckerFailure _-> assert false
1577 CR.head_beta_reduce ~delta:false
1578 (Cic.Appl (outty ::right_p @ [k])),k
1580 Cic.Prod (Cic.Name "p",
1581 Cic.Appl [eq; mty; m; k],
1583 (CR.head_beta_reduce ~delta:false
1584 (Cic.Appl (outty ::right_p @ [k]))))),k
1587 aux context outty [] 1 mty m cty
1589 let add_lambda_for_refl_m pbo rno mty m k cty =
1590 (* k lives in the right context *)
1591 if rno <> 0 then pbo else
1592 let rec aux mty m = function
1593 | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1594 Cic.Lambda (name,src,
1595 (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1597 Cic.Lambda (Cic.Name "p",
1598 Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1602 let add_pi_for_refl_m new_outty mty m rno =
1603 if rno <> 0 then new_outty else
1604 let rec aux m mty = function
1605 | Cic.Lambda (name, src, tgt) ->
1606 Cic.Lambda (name, src,
1607 aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1610 (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1614 in (* }}} end helper functions *)
1615 (* constructors types with left params already instantiated *)
1616 let outty = CicMetaSubst.apply_subst subst outty in
1617 let cl, left_p, leftno,rno,ugraph =
1618 get_cl_and_left_p uri tyno outty ugraph
1623 CicTypeChecker.type_of_aux' ~subst metasenv context m
1624 CicUniv.oblivion_ugraph
1626 | Cic.MutInd _ as mty,_ -> [], mty
1627 | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
1628 snd (HExtlib.split_nth leftno args), mty
1630 with CicTypeChecker.TypeCheckerFailure _ -> assert false
1633 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1636 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1637 ~metasenv subst new_outty context));
1638 let _,pl,subst,metasenv,ugraph =
1640 (fun cty pbo (i, acc, s, menv, ugraph) ->
1641 (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1642 * (new_)outty right_par (K_i left_par k_par) *)
1644 add_params menv s context uri tyno
1645 cty outty mty m leftno i in
1647 (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1648 ~metasenv subst infty_pbo context));
1649 let expty_pbo, k = (* k is (K_i left_par k_par) *)
1650 add_params menv s context uri tyno
1651 cty new_outty mty m leftno i in
1653 (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1654 ~metasenv subst expty_pbo context));
1655 let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1657 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1658 ~metasenv subst pbo context));
1659 let (pbo, _), subst, metasenv, ugraph =
1660 coerce_to_something_aux pbo infty_pbo expty_pbo
1661 s menv context ugraph
1664 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1665 ~metasenv subst pbo context));
1666 (i-1, pbo::acc, subst, metasenv, ugraph))
1667 cl pl (List.length pl, [], subst, metasenv, ugraph)
1669 let new_outty = add_pi_for_refl_m new_outty mty m rno in
1671 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1672 ~metasenv subst new_outty context));
1675 let refl_m=Cic.Appl[eq_refl;mty;m]in
1676 Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1678 Cic.MutCase(uri,tyno,new_outty,m,pl)
1680 (t, expty), subst, metasenv, ugraph (*}}}*)
1681 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1682 (*{{{*) debug_print (lazy "LAM");
1684 FreshNamesGenerator.mk_fresh_name
1685 ~subst metasenv context ~typ:src2 Cic.Anonymous
1687 let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1688 (* contravariant part: the argument of f:src->ty *)
1689 let (rel1, _), subst, metasenv, ugraph =
1690 coerce_to_something_aux
1691 (Cic.Rel 1) (CS.lift 1 src2)
1692 (CS.lift 1 src) subst metasenv context_src2 ugraph
1694 (* covariant part: the result of f(c x); x:src2; (c x):src *)
1697 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1698 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1700 (* we fix the possible dependency problem in the source ty *)
1701 let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1702 let (bo, _), subst, metasenv, ugraph =
1703 coerce_to_something_aux
1704 bo ty ty2 subst metasenv context_src2 ugraph
1706 let coerced = Cic.Lambda (name_t,src2, bo) in
1707 (coerced, expty), subst, metasenv, ugraph (*}}}*)
1709 (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1710 ~metasenv subst infty context ^ " ==> " ^
1711 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1712 coerce_atom_to_something
1713 t infty expty subst metasenv context ugraph (*}}}*)
1715 debug_print (lazy ("COERCE TO SOMETHING END: "^
1716 CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1720 coerce_to_something_aux t infty expty subst metasenv context ugraph
1721 with Uncertain _ | RefineFailure _ as exn ->
1724 CicMetaSubst.ppterm_in_context metasenv subst t context ^
1725 " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1726 infty context ^ " but is here used with type " ^
1727 CicMetaSubst.ppterm_in_context metasenv subst expty context)
1729 enrich localization_tbl ~f t exn
1731 and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1732 match CicReduction.whd ~delta:false ~subst context infty with
1733 | Cic.Meta _ | Cic.Sort _ ->
1734 t,infty, subst, metasenv, ugraph
1736 debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1737 ~metasenv subst src context));
1738 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1740 let (t, ty_t), subst, metasenv, ugraph =
1741 coerce_to_something true
1742 localization_tbl t src tgt subst metasenv context ugraph
1744 debug_print (lazy ("COERCE TO SORT END: "^
1745 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1746 t, ty_t, subst, metasenv, ugraph
1747 with HExtlib.Localized (_, exn) ->
1749 lazy ("(7)The term " ^
1750 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1751 ^ " is not a type since it has type " ^
1752 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1753 ^ " that is not a sort")
1755 enrich localization_tbl ~f t exn
1758 (* eat prods ends here! *)
1760 let t',ty,subst',metasenv',ugraph1 =
1761 type_of_aux [] metasenv context t ugraph
1763 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1764 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1765 (* Andrea: ho rimesso qui l'applicazione della subst al
1766 metasenv dopo che ho droppato l'invariante che il metsaenv
1767 e' sempre istanziato *)
1768 let substituted_metasenv =
1769 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1771 (* substituted_t,substituted_ty,substituted_metasenv *)
1772 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1774 if clean_dummy_dependent_types then
1775 FreshNamesGenerator.clean_dummy_dependent_types substituted_t
1776 else substituted_t in
1778 if clean_dummy_dependent_types then
1779 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty
1780 else substituted_ty in
1781 let cleaned_metasenv =
1782 if clean_dummy_dependent_types then
1784 (function (n,context,ty) ->
1785 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1790 | Some (n, Cic.Decl t) ->
1792 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1793 | Some (n, Cic.Def (bo,ty)) ->
1794 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1795 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
1797 Some (n, Cic.Def (bo',ty'))
1801 ) substituted_metasenv
1803 substituted_metasenv
1805 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1808 let undebrujin uri typesno tys t =
1811 (fun (name,_,_,_) (i,t) ->
1812 (* here the explicit_named_substituion is assumed to be *)
1814 let t' = Cic.MutInd (uri,i,[]) in
1815 let t = CicSubstitution.subst t' t in
1817 ) tys (typesno - 1,t))
1819 let map_first_n n start f g l =
1820 let rec aux acc k l =
1823 | [] -> raise (Invalid_argument "map_first_n")
1824 | hd :: tl -> f hd k (aux acc (k+1) tl)
1830 (*CSC: this is a very rough approximation; to be finished *)
1831 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1832 let subst,metasenv,ugraph,tys =
1834 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1835 let subst,metasenv,ugraph,cl =
1837 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1838 let rec aux ctx k subst = function
1839 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1840 let subst,metasenv,ugraph,tl =
1842 (subst,metasenv,ugraph,[])
1843 (fun t n (subst,metasenv,ugraph,acc) ->
1844 let subst,metasenv,ugraph =
1846 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1848 subst,metasenv,ugraph,(t::acc))
1849 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1852 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1853 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1854 subst,metasenv,ugraph,t
1855 | Cic.Prod (name,s,t) ->
1856 let ctx = (Some (name,Cic.Decl s))::ctx in
1857 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1858 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1862 (lazy "not well formed constructor type"))
1864 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1865 subst,metasenv,ugraph,(name,ty) :: acc)
1866 cl (subst,metasenv,ugraph,[])
1868 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1869 tys ([],metasenv,ugraph,[])
1871 let substituted_tys =
1873 (fun (name,ind,arity,cl) ->
1875 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1877 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1880 metasenv,ugraph,substituted_tys
1882 let typecheck metasenv uri obj ~localization_tbl =
1883 let ugraph = CicUniv.oblivion_ugraph in
1885 Cic.Constant (name,Some bo,ty,args,attrs) ->
1886 (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
1887 since type_of_aux' destroys localization information (which are
1888 preserved by type_of_aux *)
1891 Cic.CicHash.find localization_tbl bo
1893 HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
1895 let bo',boty,metasenv,ugraph =
1896 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1897 let ty',_,metasenv,ugraph =
1898 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1899 let subst,metasenv,ugraph =
1901 fo_unif_subst [] [] metasenv boty ty' ugraph
1904 | Uncertain _ as exn ->
1907 CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
1909 CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
1910 " but is here used with type " ^
1911 CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
1915 RefineFailure _ -> RefineFailure msg
1916 | Uncertain _ -> Uncertain msg
1919 raise (HExtlib.Localized (loc exn',exn'))
1921 let bo' = CicMetaSubst.apply_subst subst bo' in
1922 let ty' = CicMetaSubst.apply_subst subst ty' in
1923 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1924 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1925 | Cic.Constant (name,None,ty,args,attrs) ->
1926 let ty',_,metasenv,ugraph =
1927 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1929 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1930 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1931 assert (metasenv' = metasenv);
1932 (* Here we do not check the metasenv for correctness *)
1933 let bo',boty,metasenv,ugraph =
1934 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1935 let ty',sort,metasenv,ugraph =
1936 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1940 (* instead of raising Uncertain, let's hope that the meta will become
1943 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1945 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1946 let bo' = CicMetaSubst.apply_subst subst bo' in
1947 let ty' = CicMetaSubst.apply_subst subst ty' in
1948 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1949 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1950 | Cic.Variable _ -> assert false (* not implemented *)
1951 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1952 (*CSC: this code is greately simplified and many many checks are missing *)
1953 (*CSC: e.g. the constructors are not required to build their own types, *)
1954 (*CSC: the arities are not required to have as type a sort, etc. *)
1955 let uri = match uri with Some uri -> uri | None -> assert false in
1956 let typesno = List.length tys in
1957 (* first phase: we fix only the types *)
1958 let metasenv,ugraph,tys =
1960 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1961 let ty',_,metasenv,ugraph =
1962 (* clean_dummy_dependent_types: false to avoid cleaning the names
1963 of the left products, that must be identical to those of the
1964 constructors; however, non-left products should probably be
1966 type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl
1967 metasenv [] ty ugraph
1969 metasenv,ugraph,(name,b,ty',cl)::res
1970 ) tys (metasenv,ugraph,[]) in
1972 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1973 (* second phase: we fix only the constructors *)
1974 let saved_menv = metasenv in
1975 let metasenv,ugraph,tys =
1977 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1978 let metasenv,ugraph,cl' =
1980 (fun (name,ty) (metasenv,ugraph,res) ->
1982 CicTypeChecker.debrujin_constructor
1983 ~cb:(relocalize localization_tbl) uri typesno [] ty in
1984 let ty',_,metasenv,ugraph =
1985 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1986 let ty' = undebrujin uri typesno tys ty' in
1987 metasenv@saved_menv,ugraph,(name,ty')::res
1988 ) cl (metasenv,ugraph,[])
1990 metasenv,ugraph,(name,b,ty,cl')::res
1991 ) tys (metasenv,ugraph,[]) in
1992 (* third phase: we check the positivity condition *)
1993 let metasenv,ugraph,tys =
1994 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1996 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1999 (* sara' piu' veloce che raffinare da zero? mah.... *)
2000 let pack_coercion metasenv ctx t =
2001 let module C = Cic in
2002 let rec merge_coercions ctx =
2003 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
2005 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
2006 | C.Meta (n,subst) ->
2009 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
2012 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
2013 | C.Prod (name,so,dest) ->
2014 let ctx' = (Some (name,C.Decl so))::ctx in
2015 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
2016 | C.Lambda (name,so,dest) ->
2017 let ctx' = (Some (name,C.Decl so))::ctx in
2018 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
2019 | C.LetIn (name,so,ty,dest) ->
2020 let ctx' = Some (name,(C.Def (so,ty)))::ctx in
2022 (name, merge_coercions ctx so, merge_coercions ctx ty,
2023 merge_coercions ctx' dest)
2025 let l = List.map (merge_coercions ctx) l in
2027 let b,_,_,_,_ = is_a_double_coercion t in
2029 let ugraph = CicUniv.oblivion_ugraph in
2030 let old_insert_coercions = !insert_coercions in
2031 insert_coercions := false;
2032 let newt, _, menv, _ =
2034 type_of_aux' metasenv ctx t ugraph
2035 with RefineFailure _ | Uncertain _ ->
2038 insert_coercions := old_insert_coercions;
2039 if metasenv <> [] || menv = [] then
2042 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
2045 | C.Var (uri,exp_named_subst) ->
2046 let exp_named_subst = List.map aux exp_named_subst in
2047 C.Var (uri, exp_named_subst)
2048 | C.Const (uri,exp_named_subst) ->
2049 let exp_named_subst = List.map aux exp_named_subst in
2050 C.Const (uri, exp_named_subst)
2051 | C.MutInd (uri,tyno,exp_named_subst) ->
2052 let exp_named_subst = List.map aux exp_named_subst in
2053 C.MutInd (uri,tyno,exp_named_subst)
2054 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
2055 let exp_named_subst = List.map aux exp_named_subst in
2056 C.MutConstruct (uri,tyno,consno,exp_named_subst)
2057 | C.MutCase (uri,tyno,out,te,pl) ->
2058 let pl = List.map (merge_coercions ctx) pl in
2059 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
2060 | C.Fix (fno, fl) ->
2063 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2068 (fun (name,idx,ty,bo) ->
2069 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
2073 | C.CoFix (fno, fl) ->
2076 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2081 (fun (name,ty,bo) ->
2082 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
2087 merge_coercions ctx t
2090 let pack_coercion_metasenv conjectures = conjectures (*
2092 TASSI: this code war written when coercions were a toy,
2093 now packing coercions involves unification thus
2094 the metasenv may change, and this pack coercion
2095 does not handle that.
2097 let module C = Cic in
2099 (fun (i, ctx, ty) ->
2105 Some (name, C.Decl t) ->
2106 Some (name, C.Decl (pack_coercion conjectures ctx t))
2107 | Some (name, C.Def (t,None)) ->
2108 Some (name,C.Def (pack_coercion conjectures ctx t,None))
2109 | Some (name, C.Def (t,Some ty)) ->
2110 Some (name, C.Def (pack_coercion conjectures ctx t,
2111 Some (pack_coercion conjectures ctx ty)))
2117 ((i,ctx,pack_coercion conjectures ctx ty))
2122 let pack_coercion_obj obj = obj (*
2124 TASSI: this code war written when coercions were a toy,
2125 now packing coercions involves unification thus
2126 the metasenv may change, and this pack coercion
2127 does not handle that.
2129 let module C = Cic in
2131 | C.Constant (id, body, ty, params, attrs) ->
2135 | Some body -> Some (pack_coercion [] [] body)
2137 let ty = pack_coercion [] [] ty in
2138 C.Constant (id, body, ty, params, attrs)
2139 | C.Variable (name, body, ty, params, attrs) ->
2143 | Some body -> Some (pack_coercion [] [] body)
2145 let ty = pack_coercion [] [] ty in
2146 C.Variable (name, body, ty, params, attrs)
2147 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2148 let conjectures = pack_coercion_metasenv conjectures in
2149 let body = pack_coercion conjectures [] body in
2150 let ty = pack_coercion conjectures [] ty in
2151 C.CurrentProof (name, conjectures, body, ty, params, attrs)
2152 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2155 (fun (name, ind, arity, cl) ->
2156 let arity = pack_coercion [] [] arity in
2158 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2160 (name, ind, arity, cl))
2163 C.InductiveDefinition (indtys, params, leftno, attrs) *)
2168 let type_of_aux' metasenv context term =
2171 type_of_aux' metasenv context term in
2173 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2175 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2178 | RefineFailure msg as e ->
2179 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2181 | Uncertain msg as e ->
2182 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2186 let profiler2 = HExtlib.profile "CicRefine"
2188 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2189 profiler2.HExtlib.profile
2190 (type_of_aux' ?localization_tbl metasenv context term) ugraph
2192 let typecheck ~localization_tbl metasenv uri obj =
2193 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2195 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2196 (* vim:set foldmethod=marker: *)