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 =
135 let rec subst_nth n x l =
138 | 0, _::tl -> x :: tl
139 | n, hd::tl -> hd :: subst_nth (n-1) x tl
141 let imp = Cic.Implicit None in
142 let dummyres = false,imp, imp,imp,imp in
145 (match CoercGraph.coerced_arg l1 with
146 | Some (Cic.Appl l2, pos1) ->
147 (match CoercGraph.coerced_arg l2 with
149 true, List.hd l1, List.hd l2, x,
150 Cic.Appl (subst_nth (pos1 + 1)
151 (Cic.Appl (subst_nth (pos2+1) imp l2)) l1)
157 let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
159 let len = List.length tlbody_and_type in
162 CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
163 " (that has type "^ CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
164 ") is here applied to " ^ string_of_int len ^
165 " arguments but here it can handle only up to " ^
166 string_of_int (len - residuals) ^ " arguments")
168 enrich localization_tbl he ~f:(fun _-> msg) exn
171 let mk_prod_of_metas metasenv context subst args =
172 let rec mk_prod metasenv context' = function
174 let (metasenv, idx) =
175 CicMkImplicit.mk_implicit_type metasenv subst context'
178 CicMkImplicit.identity_relocation_list_for_metavariable context'
180 metasenv,Cic.Meta (idx, irl)
182 let (metasenv, idx) =
183 CicMkImplicit.mk_implicit_type metasenv subst context'
186 CicMkImplicit.identity_relocation_list_for_metavariable context'
188 let meta = Cic.Meta (idx,irl) in
190 (* The name must be fresh for context. *)
191 (* Nevertheless, argty is well-typed only in context. *)
192 (* Thus I generate a name (name_hint) in context and *)
193 (* then I generate a name --- using the hint name_hint *)
194 (* --- that is fresh in context'. *)
196 FreshNamesGenerator.mk_fresh_name ~subst metasenv
197 (CicMetaSubst.apply_subst_context subst context)
199 ~typ:(CicMetaSubst.apply_subst subst argty)
201 FreshNamesGenerator.mk_fresh_name ~subst
202 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
204 let metasenv,target =
205 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
207 metasenv,Cic.Prod (name,meta,target)
209 mk_prod metasenv context args
212 let rec type_of_constant uri ugraph =
213 let module C = Cic in
214 let module R = CicReduction in
215 let module U = UriManager in
216 let _ = CicTypeChecker.typecheck uri in
219 CicEnvironment.get_cooked_obj ugraph uri
220 with Not_found -> assert false
223 C.Constant (_,_,ty,_,_) -> ty,u
224 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
228 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
230 and type_of_variable uri ugraph =
231 let module C = Cic in
232 let module R = CicReduction in
233 let module U = UriManager in
234 let _ = CicTypeChecker.typecheck uri in
237 CicEnvironment.get_cooked_obj ugraph uri
238 with Not_found -> assert false
241 C.Variable (_,_,ty,_,_) -> ty,u
245 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
247 and type_of_mutual_inductive_defs uri i ugraph =
248 let module C = Cic in
249 let module R = CicReduction in
250 let module U = UriManager in
251 let _ = CicTypeChecker.typecheck uri in
254 CicEnvironment.get_cooked_obj ugraph uri
255 with Not_found -> assert false
258 C.InductiveDefinition (dl,_,_,_) ->
259 let (_,_,arity,_) = List.nth dl i in
264 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
266 and type_of_mutual_inductive_constr uri i j ugraph =
267 let module C = Cic in
268 let module R = CicReduction in
269 let module U = UriManager in
270 let _ = CicTypeChecker.typecheck uri in
273 CicEnvironment.get_cooked_obj ugraph uri
274 with Not_found -> assert false
277 C.InductiveDefinition (dl,_,_,_) ->
278 let (_,_,_,cl) = List.nth dl i in
279 let (_,ty) = List.nth cl (j-1) in
285 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
288 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
290 (* the check_branch function checks if a branch of a case is refinable.
291 It returns a pair (outype_instance,args), a subst and a metasenv.
292 outype_instance is the expected result of applying the case outtype
294 The problem is that outype is in general unknown, and we should
295 try to synthesize it from the above information, that is in general
296 a second order unification problem. *)
298 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
299 let module C = Cic in
300 let module R = CicReduction in
301 match R.whd ~subst context expectedtype with
303 (n,context,actualtype, [term]), subst, metasenv, ugraph
304 | C.Appl (C.MutInd (_,_,_)::tl) ->
305 let (_,arguments) = split tl left_args_no in
306 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
307 | C.Prod (_,so,de) ->
308 (* we expect that the actual type of the branch has the due
310 (match R.whd ~subst context actualtype with
311 C.Prod (name',so',de') ->
312 let subst, metasenv, ugraph1 =
313 fo_unif_subst subst context metasenv so so' ugraph in
315 (match CicSubstitution.lift 1 term with
316 C.Appl l -> C.Appl (l@[C.Rel 1])
317 | t -> C.Appl [t ; C.Rel 1]) in
318 (* we should also check that the name variable is anonymous in
319 the actual type de' ?? *)
321 ((Some (name',(C.Decl so)))::context)
322 metasenv subst left_args_no de' term' de ugraph1
323 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
324 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
326 and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
329 let rec type_of_aux subst metasenv context t ugraph =
330 let module C = Cic in
331 let module S = CicSubstitution in
332 let module U = UriManager in
333 let (t',_,_,_,_) as res =
338 match List.nth context (n - 1) with
339 Some (_,C.Decl ty) ->
340 t,S.lift n ty,subst,metasenv, ugraph
341 | Some (_,C.Def (_,ty)) ->
342 t,S.lift n ty,subst,metasenv, ugraph
344 enrich localization_tbl t
345 (RefineFailure (lazy "Rel to hidden hypothesis"))
348 enrich localization_tbl t
349 (RefineFailure (lazy "Not a closed term")))
350 | C.Var (uri,exp_named_subst) ->
351 let exp_named_subst',subst',metasenv',ugraph1 =
352 check_exp_named_subst
353 subst metasenv context exp_named_subst ugraph
355 let ty_uri,ugraph1 = type_of_variable uri ugraph in
357 CicSubstitution.subst_vars exp_named_subst' ty_uri
359 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
362 let (canonical_context, term,ty) =
363 CicUtil.lookup_subst n subst
365 let l',subst',metasenv',ugraph1 =
366 check_metasenv_consistency n subst metasenv context
367 canonical_context l ugraph
369 (* trust or check ??? *)
370 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
371 subst', metasenv', ugraph1
372 (* type_of_aux subst metasenv
373 context (CicSubstitution.subst_meta l term) *)
374 with CicUtil.Subst_not_found _ ->
375 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
376 let l',subst',metasenv', ugraph1 =
377 check_metasenv_consistency n subst metasenv context
378 canonical_context l ugraph
380 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
381 subst', metasenv',ugraph1)
382 | C.Sort (C.Type tno) ->
383 let tno' = CicUniv.fresh() in
385 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
386 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
388 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
389 | C.Sort (C.CProp tno) ->
390 let tno' = CicUniv.fresh() in
392 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
393 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
395 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
396 | C.Sort (C.Prop|C.Set) ->
397 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
398 | C.Implicit infos ->
399 let metasenv',t' = exp_impl metasenv subst context infos in
400 type_of_aux subst metasenv' context t' ugraph
402 let ty',_,subst',metasenv',ugraph1 =
403 type_of_aux subst metasenv context ty ugraph
405 let te',inferredty,subst'',metasenv'',ugraph2 =
406 type_of_aux subst' metasenv' context te ugraph1
408 let (te', ty'), subst''',metasenv''',ugraph3 =
409 coerce_to_something true localization_tbl te' inferredty ty'
410 subst'' metasenv'' context ugraph2
412 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
413 | C.Prod (name,s,t) ->
414 let s',sort1,subst',metasenv',ugraph1 =
415 type_of_aux subst metasenv context s ugraph
417 let s',sort1,subst', metasenv',ugraph1 =
418 coerce_to_sort localization_tbl
419 s' sort1 subst' context metasenv' ugraph1
421 let context_for_t = ((Some (name,(C.Decl s')))::context) in
422 let t',sort2,subst'',metasenv'',ugraph2 =
423 type_of_aux subst' metasenv'
424 context_for_t t ugraph1
426 let t',sort2,subst'',metasenv'',ugraph2 =
427 coerce_to_sort localization_tbl
428 t' sort2 subst'' context_for_t metasenv'' ugraph2
430 let sop,subst''',metasenv''',ugraph3 =
431 sort_of_prod localization_tbl subst'' metasenv''
432 context (name,s') t' (sort1,sort2) ugraph2
434 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
435 | C.Lambda (n,s,t) ->
436 let s',sort1,subst',metasenv',ugraph1 =
437 type_of_aux subst metasenv context s ugraph
439 let s',sort1,subst',metasenv',ugraph1 =
440 coerce_to_sort localization_tbl
441 s' sort1 subst' context metasenv' ugraph1
443 let context_for_t = ((Some (n,(C.Decl s')))::context) in
444 let t',type2,subst'',metasenv'',ugraph2 =
445 type_of_aux subst' metasenv' context_for_t t ugraph1
447 C.Lambda (n,s',t'),C.Prod (n,s',type2),
448 subst'',metasenv'',ugraph2
449 | C.LetIn (n,s,ty,t) ->
450 (* only to check if s is well-typed *)
451 let s',ty',subst',metasenv',ugraph1 =
452 type_of_aux subst metasenv context s ugraph in
453 let ty,_,subst',metasenv',ugraph1 =
454 type_of_aux subst' metasenv' context ty ugraph1 in
455 let subst',metasenv',ugraph1 =
457 fo_unif_subst subst' context metasenv'
461 enrich localization_tbl s' exn
464 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
465 context ^ " has type " ^
466 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
467 context ^ " but is here used with type " ^
468 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
471 let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
473 let t',inferredty,subst'',metasenv'',ugraph2 =
474 type_of_aux subst' metasenv'
475 context_for_t t ugraph1
477 (* One-step LetIn reduction.
478 * Even faster than the previous solution.
479 * Moreover the inferred type is closer to the expected one.
481 C.LetIn (n,s',ty,t'),
482 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
483 subst'',metasenv'',ugraph2
484 | C.Appl (he::((_::_) as tl)) ->
485 let he',hetype,subst',metasenv',ugraph1 =
486 type_of_aux subst metasenv context he ugraph
488 let tlbody_and_type,subst'',metasenv'',ugraph2 =
489 typeof_list subst' metasenv' context ugraph1 tl
491 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
492 eat_prods true subst'' metasenv'' context
493 he' hetype tlbody_and_type ugraph2
495 let newappl = (C.Appl (coerced_he::coerced_args)) in
496 avoid_double_coercion
497 context subst''' metasenv''' ugraph3 newappl applty
498 | C.Appl _ -> assert false
499 | C.Const (uri,exp_named_subst) ->
500 let exp_named_subst',subst',metasenv',ugraph1 =
501 check_exp_named_subst subst metasenv context
502 exp_named_subst ugraph in
503 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
505 CicSubstitution.subst_vars exp_named_subst' ty_uri
507 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
508 | C.MutInd (uri,i,exp_named_subst) ->
509 let exp_named_subst',subst',metasenv',ugraph1 =
510 check_exp_named_subst subst metasenv context
511 exp_named_subst ugraph
513 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
515 CicSubstitution.subst_vars exp_named_subst' ty_uri in
516 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
517 | C.MutConstruct (uri,i,j,exp_named_subst) ->
518 let exp_named_subst',subst',metasenv',ugraph1 =
519 check_exp_named_subst subst metasenv context
520 exp_named_subst ugraph
523 type_of_mutual_inductive_constr uri i j ugraph1
526 CicSubstitution.subst_vars exp_named_subst' ty_uri
528 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
530 | C.MutCase (uri, i, outtype, term, pl) ->
531 (* first, get the inductive type (and noparams)
532 * in the environment *)
533 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
534 let _ = CicTypeChecker.typecheck uri in
535 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
537 C.InductiveDefinition (l,expl_params,parsno,_) ->
538 List.nth l i , expl_params, parsno, u
540 enrich localization_tbl t
542 (lazy ("Unkown mutual inductive definition " ^
543 U.string_of_uri uri)))
545 if List.length constructors <> List.length pl then
546 enrich localization_tbl t
548 (lazy "Wrong number of cases")) ;
549 let rec count_prod t =
550 match CicReduction.whd ~subst context t with
551 C.Prod (_, _, t) -> 1 + (count_prod t)
554 let no_args = count_prod arity in
555 (* now, create a "generic" MutInd *)
556 let metasenv,left_args =
557 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
559 let metasenv,right_args =
560 let no_right_params = no_args - no_left_params in
561 if no_right_params < 0 then assert false
562 else CicMkImplicit.n_fresh_metas
563 metasenv subst context no_right_params
565 let metasenv,exp_named_subst =
566 CicMkImplicit.fresh_subst metasenv subst context expl_params in
569 C.MutInd (uri,i,exp_named_subst)
572 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
574 (* check consistency with the actual type of term *)
575 let term',actual_type,subst,metasenv,ugraph1 =
576 type_of_aux subst metasenv context term ugraph in
577 let expected_type',_, subst, metasenv,ugraph2 =
578 type_of_aux subst metasenv context expected_type ugraph1
580 let actual_type = CicReduction.whd ~subst context actual_type in
581 let subst,metasenv,ugraph3 =
583 fo_unif_subst subst context metasenv
584 expected_type' actual_type ugraph2
587 enrich localization_tbl term' exn
590 CicMetaSubst.ppterm_in_context ~metasenv subst term'
591 context ^ " has type " ^
592 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
593 context ^ " but is here used with type " ^
594 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type'
597 let rec instantiate_prod t =
601 match CicReduction.whd ~subst context t with
603 instantiate_prod (CicSubstitution.subst he t') tl
606 let arity_instantiated_with_left_args =
607 instantiate_prod arity left_args in
608 (* TODO: check if the sort elimination
609 * is allowed: [(I q1 ... qr)|B] *)
610 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
612 (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
614 if left_args = [] then
615 (C.MutConstruct (uri,i,j,exp_named_subst))
618 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
620 let p',actual_type,subst,metasenv,ugraph1 =
621 type_of_aux subst metasenv context p ugraph
623 let constructor',expected_type, subst, metasenv,ugraph2 =
624 type_of_aux subst metasenv context constructor ugraph1
626 let outtypeinstance,subst,metasenv,ugraph3 =
628 check_branch 0 context metasenv subst
629 no_left_params actual_type constructor' expected_type
633 enrich localization_tbl constructor'
636 CicMetaSubst.ppterm_in_context metasenv subst p'
637 context ^ " has type " ^
638 CicMetaSubst.ppterm_in_context metasenv subst actual_type
639 context ^ " but is here used with type " ^
640 CicMetaSubst.ppterm_in_context metasenv subst expected_type
644 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
645 pl ([],List.length pl,[],subst,metasenv,ugraph3)
648 (* we are left to check that the outype matches his instances.
649 The easy case is when the outype is specified, that amount
650 to a trivial check. Otherwise, we should guess a type from
654 let outtype,outtypety, subst, metasenv,ugraph4 =
655 type_of_aux subst metasenv context outtype ugraph4 in
658 (let candidate,ugraph5,metasenv,subst =
659 let exp_name_subst, metasenv =
661 CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
663 let uris = CicUtil.params_of_obj o in
665 fun uri (acc,metasenv) ->
666 let metasenv',new_meta =
667 CicMkImplicit.mk_implicit metasenv subst context
670 CicMkImplicit.identity_relocation_list_for_metavariable
673 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
677 match left_args,right_args with
678 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
680 let rec mk_right_args =
683 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
685 let right_args_no = List.length right_args in
686 let lifted_left_args =
687 List.map (CicSubstitution.lift right_args_no) left_args
689 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
690 (lifted_left_args @ mk_right_args right_args_no))
693 FreshNamesGenerator.mk_fresh_name ~subst metasenv
694 context Cic.Anonymous ~typ:ty
696 match outtypeinstances with
698 let extended_context =
699 let rec add_right_args =
701 Cic.Prod (name,ty,t) ->
702 Some (name,Cic.Decl ty)::(add_right_args t)
705 (Some (fresh_name,Cic.Decl ty))::
707 (add_right_args arity_instantiated_with_left_args))@
710 let metasenv,new_meta =
711 CicMkImplicit.mk_implicit metasenv subst extended_context
714 CicMkImplicit.identity_relocation_list_for_metavariable
717 let rec add_lambdas b =
719 Cic.Prod (name,ty,t) ->
720 Cic.Lambda (name,ty,(add_lambdas b t))
721 | _ -> Cic.Lambda (fresh_name, ty, b)
724 add_lambdas (Cic.Meta (new_meta,irl))
725 arity_instantiated_with_left_args
727 (Some candidate),ugraph4,metasenv,subst
728 | (constructor_args_no,_,instance,_)::tl ->
730 let instance',subst,metasenv =
731 CicMetaSubst.delift_rels subst metasenv
732 constructor_args_no instance
734 let candidate,ugraph,metasenv,subst =
736 fun (candidate_oty,ugraph,metasenv,subst)
737 (constructor_args_no,_,instance,_) ->
738 match candidate_oty with
739 | None -> None,ugraph,metasenv,subst
742 let instance',subst,metasenv =
743 CicMetaSubst.delift_rels subst metasenv
744 constructor_args_no instance
746 let subst,metasenv,ugraph =
747 fo_unif_subst subst context metasenv
750 candidate_oty,ugraph,metasenv,subst
752 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
753 | RefineFailure _ | Uncertain _ ->
754 None,ugraph,metasenv,subst
755 ) (Some instance',ugraph4,metasenv,subst) tl
758 | None -> None, ugraph,metasenv,subst
760 let rec add_lambdas n b =
762 Cic.Prod (name,ty,t) ->
763 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
765 Cic.Lambda (fresh_name, ty,
766 CicSubstitution.lift (n + 1) t)
769 (add_lambdas 0 t arity_instantiated_with_left_args),
770 ugraph,metasenv,subst
771 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
772 None,ugraph4,metasenv,subst
775 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
777 let subst,metasenv,ugraph =
779 fo_unif_subst subst context metasenv
780 candidate outtype ugraph5
782 exn -> assert false(* unification against a metavariable *)
784 C.MutCase (uri, i, outtype, term', pl'),
785 CicReduction.head_beta_reduce
786 (CicMetaSubst.apply_subst subst
787 (Cic.Appl (outtype::right_args@[term']))),
788 subst,metasenv,ugraph)
789 | _ -> (* easy case *)
790 let tlbody_and_type,subst,metasenv,ugraph4 =
791 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
793 let _,_,_,subst,metasenv,ugraph4 =
794 eat_prods false subst metasenv context
795 outtype outtypety tlbody_and_type ugraph4
797 let _,_, subst, metasenv,ugraph5 =
798 type_of_aux subst metasenv context
799 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
801 let (subst,metasenv,ugraph6) =
803 (fun (subst,metasenv,ugraph)
804 p (constructor_args_no,context,instance,args)
809 CicSubstitution.lift constructor_args_no outtype
811 C.Appl (outtype'::args)
813 CicReduction.head_beta_reduce ~delta:false
814 ~upto:(List.length args) appl
817 fo_unif_subst subst context metasenv instance instance'
821 enrich localization_tbl p exn
824 CicMetaSubst.ppterm_in_context ~metasenv subst p
825 context ^ " has type " ^
826 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
827 context ^ " but is here used with type " ^
828 CicMetaSubst.ppterm_in_context ~metasenv subst instance
830 (subst,metasenv,ugraph5) pl' outtypeinstances
832 C.MutCase (uri, i, outtype, term', pl'),
833 CicReduction.head_beta_reduce
834 (CicMetaSubst.apply_subst subst
835 (C.Appl(outtype::right_args@[term']))),
836 subst,metasenv,ugraph6)
838 let fl_ty',subst,metasenv,types,ugraph1,len =
840 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
841 let ty',_,subst',metasenv',ugraph1 =
842 type_of_aux subst metasenv context ty ugraph
844 fl @ [ty'],subst',metasenv',
845 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
846 :: types, ugraph, len+1
847 ) ([],subst,metasenv,[],ugraph,0) fl
849 let context' = types@context in
850 let fl_bo',subst,metasenv,ugraph2 =
852 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
853 let bo',ty_of_bo,subst,metasenv,ugraph1 =
854 type_of_aux subst metasenv context' bo ugraph in
855 let expected_ty = CicSubstitution.lift len ty in
856 let subst',metasenv',ugraph' =
858 fo_unif_subst subst context' metasenv
859 ty_of_bo expected_ty ugraph1
862 enrich localization_tbl bo exn
865 CicMetaSubst.ppterm_in_context ~metasenv subst bo
866 context' ^ " has type " ^
867 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
868 context' ^ " but is here used with type " ^
869 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
872 fl @ [bo'] , subst',metasenv',ugraph'
873 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
875 let ty = List.nth fl_ty' i in
876 (* now we have the new ty in fl_ty', the new bo in fl_bo',
877 * and we want the new fl with bo' and ty' injected in the right
880 let rec map3 f l1 l2 l3 =
883 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
886 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
889 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
891 let fl_ty',subst,metasenv,types,ugraph1,len =
893 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
894 let ty',_,subst',metasenv',ugraph1 =
895 type_of_aux subst metasenv context ty ugraph
897 fl @ [ty'],subst',metasenv',
898 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
899 types, ugraph1, len+1
900 ) ([],subst,metasenv,[],ugraph,0) fl
902 let context' = types@context in
903 let fl_bo',subst,metasenv,ugraph2 =
905 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
906 let bo',ty_of_bo,subst,metasenv,ugraph1 =
907 type_of_aux subst metasenv context' bo ugraph in
908 let expected_ty = CicSubstitution.lift len ty in
909 let subst',metasenv',ugraph' =
911 fo_unif_subst subst context' metasenv
912 ty_of_bo expected_ty ugraph1
915 enrich localization_tbl bo exn
918 CicMetaSubst.ppterm_in_context ~metasenv subst bo
919 context' ^ " has type " ^
920 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
921 context' ^ " but is here used with type " ^
922 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
925 fl @ [bo'],subst',metasenv',ugraph'
926 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
928 let ty = List.nth fl_ty' i in
929 (* now we have the new ty in fl_ty', the new bo in fl_bo',
930 * and we want the new fl with bo' and ty' injected in the right
933 let rec map3 f l1 l2 l3 =
936 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
939 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
942 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
944 relocalize localization_tbl t t';
947 (* check_metasenv_consistency checks that the "canonical" context of a
948 metavariable is consitent - up to relocation via the relocation list l -
949 with the actual context *)
950 and check_metasenv_consistency
951 metano subst metasenv context canonical_context l ugraph
953 let module C = Cic in
954 let module R = CicReduction in
955 let module S = CicSubstitution in
956 let lifted_canonical_context =
960 | (Some (n,C.Decl t))::tl ->
961 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
962 | None::tl -> None::(aux (i+1) tl)
963 | (Some (n,C.Def (t,ty)))::tl ->
967 (S.subst_meta l (S.lift i t),
968 S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
970 aux 1 canonical_context
974 (fun (l,subst,metasenv,ugraph) t ct ->
977 l @ [None],subst,metasenv,ugraph
978 | Some t,Some (_,C.Def (ct,_)) ->
979 (*CSC: the following optimization is to avoid a possibly
980 expensive reduction that can be easily avoided and
981 that is quite frequent. However, this is better
982 handled using levels to control reduction *)
987 match List.nth context (n - 1) with
988 Some (_,C.Def (te,_)) -> S.lift n te
994 let subst',metasenv',ugraph' =
996 (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
997 * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
998 fo_unif_subst subst context metasenv optimized_t ct ugraph
999 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))))))
1001 l @ [Some t],subst',metasenv',ugraph'
1002 | Some t,Some (_,C.Decl ct) ->
1003 let t',inferredty,subst',metasenv',ugraph1 =
1004 type_of_aux subst metasenv context t ugraph
1006 let subst'',metasenv'',ugraph2 =
1009 subst' context metasenv' inferredty ct ugraph1
1010 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))))))
1012 l @ [Some t'], subst'',metasenv'',ugraph2
1014 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
1016 Invalid_argument _ ->
1020 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1021 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1022 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1024 and check_exp_named_subst metasubst metasenv context tl ugraph =
1025 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1027 [] -> [],metasubst,metasenv,ugraph
1029 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1031 CicSubstitution.subst_vars substs ty_uri in
1032 (* CSC: why was this code here? it is wrong
1033 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1034 Cic.Variable (_,Some bo,_,_) ->
1036 (RefineFailure (lazy
1037 "A variable with a body can not be explicit substituted"))
1038 | Cic.Variable (_,None,_,_) -> ()
1041 (RefineFailure (lazy
1042 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1045 let t',typeoft,metasubst',metasenv',ugraph2 =
1046 type_of_aux metasubst metasenv context t ugraph1 in
1047 let subst = uri,t' in
1048 let metasubst'',metasenv'',ugraph3 =
1051 metasubst' context metasenv' typeoft typeofvar ugraph2
1053 raise (RefineFailure (lazy
1054 ("Wrong Explicit Named Substitution: " ^
1055 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1056 " not unifiable with " ^
1057 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1059 (* FIXME: no mere tail recursive! *)
1060 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1061 check_exp_named_subst_aux
1062 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1064 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1066 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1069 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1072 let module C = Cic in
1073 let context_for_t2 = (Some (name,C.Decl s))::context in
1074 let t1'' = CicReduction.whd ~subst context t1 in
1075 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1076 match (t1'', t2'') with
1077 | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) ->
1078 (* different than Coq manual!!! *)
1079 C.Sort s2,subst,metasenv,ugraph
1080 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1081 let t' = CicUniv.fresh() in
1083 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1084 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1085 C.Sort (C.Type t'),subst,metasenv,ugraph2
1087 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1088 | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
1089 let t' = CicUniv.fresh() in
1091 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1092 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1093 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1095 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1096 | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
1097 let t' = CicUniv.fresh() in
1099 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1100 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1101 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1103 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1104 | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
1105 let t' = CicUniv.fresh() in
1107 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1108 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1109 C.Sort (C.Type t'),subst,metasenv,ugraph2
1111 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1112 | (C.Sort _,C.Sort (C.Type t1)) ->
1113 C.Sort (C.Type t1),subst,metasenv,ugraph
1114 | (C.Sort _,C.Sort (C.CProp t1)) ->
1115 C.Sort (C.CProp t1),subst,metasenv,ugraph
1116 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1117 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1118 (* TODO how can we force the meta to become a sort? If we don't we
1119 * break the invariant that refine produce only well typed terms *)
1120 (* TODO if we check the non meta term and if it is a sort then we
1121 * are likely to know the exact value of the result e.g. if the rhs
1122 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1123 let (metasenv,idx) =
1124 CicMkImplicit.mk_implicit_sort metasenv subst in
1125 let (subst, metasenv,ugraph1) =
1127 fo_unif_subst subst context_for_t2 metasenv
1128 (C.Meta (idx,[])) t2'' ugraph
1129 with _ -> assert false (* unification against a metavariable *)
1131 t2'',subst,metasenv,ugraph1
1134 enrich localization_tbl s
1138 "%s is supposed to be a type, but its type is %s"
1139 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1140 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1142 enrich localization_tbl t
1146 "%s is supposed to be a type, but its type is %s"
1147 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1148 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1150 and avoid_double_coercion context subst metasenv ugraph t ty =
1151 if not !pack_coercions then
1152 t,ty,subst,metasenv,ugraph
1154 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1156 let source_carr = CoercGraph.source_of c2 in
1157 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1158 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1160 | CoercGraph.SomeCoercion candidates ->
1162 HExtlib.list_findopt
1163 (function (metasenv,last,c) ->
1165 | c when not (CoercGraph.is_composite c) ->
1166 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1169 let subst,metasenv,ugraph =
1170 fo_unif_subst subst context metasenv last head ugraph in
1171 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1176 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1177 let newt,_,subst,metasenv,ugraph =
1178 type_of_aux subst metasenv context c ugraph in
1179 debug_print (lazy "tipa...");
1180 let subst, metasenv, ugraph =
1181 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1182 fo_unif_subst subst context metasenv newt t ugraph
1184 debug_print (lazy "unifica...");
1185 Some (newt, ty, subst, metasenv, ugraph)
1187 | RefineFailure s | Uncertain s when not !pack_coercions->
1188 debug_print s; debug_print (lazy "stop\n");None
1189 | RefineFailure s | Uncertain s ->
1190 debug_print s;debug_print (lazy "goon\n");
1192 let old_pack_coercions = !pack_coercions in
1193 pack_coercions := false; (* to avoid diverging *)
1194 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1195 type_of_aux subst metasenv context c1_c2_implicit ugraph
1197 pack_coercions := old_pack_coercions;
1199 is_a_double_coercion refined_c1_c2_implicit
1205 match refined_c1_c2_implicit with
1206 | Cic.Appl l -> HExtlib.list_last l
1209 let subst, metasenv, ugraph =
1210 try fo_unif_subst subst context metasenv
1212 with RefineFailure s| Uncertain s->
1213 debug_print s;assert false
1215 let subst, metasenv, ugraph =
1216 fo_unif_subst subst context metasenv
1217 refined_c1_c2_implicit t ugraph
1219 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1221 | RefineFailure s | Uncertain s ->
1222 pack_coercions := true;debug_print s;None
1223 | exn -> pack_coercions := true; raise exn))
1226 (match selected with
1230 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1231 t, ty, subst, metasenv, ugraph)
1232 | _ -> t, ty, subst, metasenv, ugraph)
1234 t, ty, subst, metasenv, ugraph
1236 and typeof_list subst metasenv context ugraph l =
1237 let tlbody_and_type,subst,metasenv,ugraph =
1239 (fun x (res,subst,metasenv,ugraph) ->
1240 let x',ty,subst',metasenv',ugraph1 =
1241 type_of_aux subst metasenv context x ugraph
1243 (x', ty)::res,subst',metasenv',ugraph1
1244 ) l ([],subst,metasenv,ugraph)
1246 tlbody_and_type,subst,metasenv,ugraph
1249 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1251 (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1252 let fix_arity n metasenv context subst he hetype ugraph =
1253 let hetype = CicMetaSubst.apply_subst subst hetype in
1254 (* instead of a dummy functional type we may create the real product
1255 * using args_bo_and_ty, but since coercions lookup ignores the
1256 * actual ariety we opt for the simple solution *)
1257 let fty = Cic.Prod(Cic.Anonymous, Cic.Sort Cic.Prop, Cic.Sort Cic.Prop) in
1258 match CoercGraph.look_for_coercion metasenv subst context hetype fty with
1259 | CoercGraph.NoCoercion -> []
1260 | CoercGraph.NotHandled ->
1261 raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1262 | CoercGraph.SomeCoercionToTgt candidates
1263 | CoercGraph.SomeCoercion candidates ->
1265 (fun (metasenv,last,coerc) ->
1267 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1269 let subst,metasenv,ugraph =
1270 fo_unif_subst subst context metasenv last he ugraph in
1271 debug_print (lazy ("New head: "^ pp coerc));
1273 CicTypeChecker.type_of_aux' ~subst metasenv context coerc
1276 debug_print (lazy (" has type: "^ pp tty));
1277 Some (coerc,tty,subst,metasenv,ugraph)
1279 | Uncertain _ | RefineFailure _
1280 | HExtlib.Localized (_,Uncertain _)
1281 | HExtlib.Localized (_,RefineFailure _) -> None
1282 | exn -> assert false)
1285 (* aux function to process the type of the head and the args in parallel *)
1286 let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1288 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1289 | (hete, hety)::tl as args ->
1290 match (CicReduction.whd ~subst context hetype) with
1291 | Cic.Prod (n,s,t) ->
1292 let arg,subst,metasenv,ugraph =
1293 coerce_to_something allow_coercions localization_tbl
1294 hete hety s subst metasenv context ugraph in
1296 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1297 ugraph (newargs@[arg]) tl
1300 match he, newargs with
1302 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1303 | _ -> Cic.Appl (he::List.map fst newargs)
1305 (*{{{*) debug_print (lazy
1307 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1308 "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1309 "\n but is applyed to: " ^ String.concat ";"
1310 (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1311 let error = ref None in
1312 let possible_fixes =
1313 fix_arity (List.length args) metasenv context subst he hetype
1316 HExtlib.list_findopt
1317 (fun (he,hetype,subst,metasenv,ugraph) ->
1318 (* {{{ *)debug_print (lazy ("Try fix: "^
1319 CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1320 debug_print (lazy (" of type: "^
1321 CicMetaSubst.ppterm_in_context
1322 ~metasenv subst hetype context)); (* }}} *)
1324 Some (eat_prods_and_args
1325 metasenv subst context he hetype ugraph [] args)
1327 | RefineFailure _ | Uncertain _
1328 | HExtlib.Localized (_,RefineFailure _)
1329 | HExtlib.Localized (_,Uncertain _) as exn ->
1330 error := Some exn; None)
1338 (MoreArgsThanExpected
1339 (List.length args, RefineFailure (lazy "")))
1340 | Some exn -> raise exn
1342 (* first we check if we are in the simple case of a meta closed term *)
1343 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1344 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1345 (* this optimization is to postpone fix_arity (the most common case)*)
1346 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1348 (* this (says CSC) is also useful to infer dependent types *)
1349 let pristinemenv = metasenv in
1350 let metasenv,hetype' =
1351 mk_prod_of_metas metasenv context subst args_bo_and_ty
1354 let subst,metasenv,ugraph =
1355 fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1357 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1358 with RefineFailure _ | Uncertain _ ->
1359 subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1361 let coerced_args,subst,metasenv,he,t,ugraph =
1364 metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1366 MoreArgsThanExpected (residuals,exn) ->
1367 more_args_than_expected localization_tbl metasenv
1368 subst he context hetype' residuals args_bo_and_ty exn
1370 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1372 and coerce_to_something
1373 allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1375 let module CS = CicSubstitution in
1376 let module CR = CicReduction in
1377 let cs_subst = CS.subst ~avoid_beta_redexes:true in
1378 let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1379 debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1381 CoercGraph.look_for_coercion metasenv subst context infty expty
1384 | CoercGraph.NoCoercion
1385 | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy
1386 "coerce_atom_to_something fails since no coercions found"))
1387 | CoercGraph.NotHandled when
1388 not (CicUtil.is_meta_closed infty) ||
1389 not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy
1390 "coerce_atom_to_something fails since carriers have metas"))
1391 | CoercGraph.NotHandled -> raise (RefineFailure (lazy
1392 "coerce_atom_to_something fails since no coercions found"))
1393 | CoercGraph.SomeCoercion candidates ->
1394 debug_print (lazy (string_of_int (List.length candidates) ^
1395 " candidates found"));
1396 let uncertain = ref false in
1400 (fun (metasenv,last,c) ->
1402 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1403 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1405 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
1406 "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
1408 debug_print (lazy ("FO_UNIF_SUBST: " ^
1409 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1410 let subst,metasenv,ugraph =
1411 fo_unif_subst subst context metasenv last t ugraph
1413 let newt,newhety,subst,metasenv,ugraph =
1414 type_of_aux subst metasenv context c ugraph in
1415 let newt, newty, subst, metasenv, ugraph =
1416 avoid_double_coercion context subst metasenv ugraph newt expty
1418 let subst,metasenv,ugraph =
1419 fo_unif_subst subst context metasenv newhety expty ugraph in
1420 Some ((newt,newty), subst, metasenv, ugraph)
1422 | Uncertain _ -> uncertain := true; None
1423 | RefineFailure _ -> None)
1428 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1436 | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1437 | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1439 let rec coerce_to_something_aux
1440 t infty expty subst metasenv context ugraph
1443 let subst, metasenv, ugraph =
1444 fo_unif_subst subst context metasenv infty expty ugraph
1446 (t, expty), subst, metasenv, ugraph
1447 with (Uncertain _ | RefineFailure _ as exn)
1448 when allow_coercions && !insert_coercions ->
1449 let whd = CicReduction.whd ~delta:false in
1450 let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1451 let infty = clean infty subst context in
1452 let expty = clean expty subst context in
1453 let t = clean t subst context in
1454 (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1455 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1456 CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1457 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1458 let (coerced,_),subst,metasenv,_ as result =
1459 match infty, expty, t with
1460 | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1461 (*{{{*) debug_print (lazy "FIX");
1463 [name,i,_(* infty *),bo] ->
1465 Some (Cic.Name name,Cic.Decl expty)::context in
1466 let (rel1, _), subst, metasenv, ugraph =
1467 coerce_to_something_aux (Cic.Rel 1)
1468 (CS.lift 1 expty) (CS.lift 1 infty) subst
1469 metasenv context_bo ugraph in
1470 let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1471 let (bo,_), subst, metasenv, ugraph =
1472 coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1474 metasenv context_bo ugraph
1476 (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1477 | _ -> assert false (* not implemented yet *)) (*}}}*)
1478 | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1479 (*{{{*) debug_print (lazy "CASE");
1480 (* {{{ helper functions *)
1481 let get_cl_and_left_p uri tyno outty ugraph =
1482 match CicEnvironment.get_obj ugraph uri with
1483 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1486 match CicReduction.whd ~delta:false ctx t with
1487 | Cic.Prod (name,src,tgt) ->
1488 let ctx = Some (name, Cic.Decl src) :: ctx in
1494 let rec skip_lambda_delifting t n =
1497 | Cic.Lambda (_,_,t),n ->
1498 skip_lambda_delifting
1499 (CS.subst (Cic.Implicit None) t) (n - 1)
1502 let get_l_r_p n = function
1503 | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1504 | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1505 HExtlib.split_nth n args
1508 let _, _, ty, cl = List.nth tl tyno in
1509 let pis = count_pis ty in
1510 let rno = pis - leftno in
1511 let t = skip_lambda_delifting outty rno in
1512 let left_p, _ = get_l_r_p leftno t in
1513 let instantiale_with_left cl =
1517 (fun t p -> match t with
1518 | Cic.Prod (_,_,t) ->
1524 let cl = instantiale_with_left (List.map snd cl) in
1525 cl, left_p, leftno, rno, ugraph
1528 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1531 let rec mkr n = function
1532 | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1535 CicReplace.replace_lifting
1536 ~equality:(fun _ -> CicUtil.alpha_equivalence)
1538 ~what:(matched::right_p)
1539 ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1543 | Cic.Lambda (name, src, tgt),_ ->
1544 Cic.Lambda (name, src,
1545 keep_lambdas_and_put_expty
1546 (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1547 (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1550 let eq_uri, eq, eq_refl =
1551 match LibraryObjects.eq_URI () with
1552 | None -> HLog.warn "no default equality"; raise exn
1553 | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1556 metasenv subst context uri tyno cty outty mty m leftno i
1558 let rec aux context outty par k mty m = function
1559 | Cic.Prod (name, src, tgt) ->
1562 (Some (name, Cic.Decl src) :: context)
1563 (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1564 (CS.lift 1 mty) (CS.lift 1 m) tgt
1566 Cic.Prod (name, src, t), k
1569 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1570 if par <> [] then Cic.Appl (k::par) else k
1572 Cic.Prod (Cic.Name "p",
1573 Cic.Appl [eq; mty; m; k],
1575 (CR.head_beta_reduce ~delta:false
1576 (Cic.Appl [outty;k])))),k
1577 | Cic.Appl (Cic.MutInd _::pl) ->
1578 let left_p,right_p = HExtlib.split_nth leftno pl in
1579 let has_rights = right_p <> [] in
1581 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1582 Cic.Appl (k::left_p@par)
1586 CicTypeChecker.type_of_aux' ~subst metasenv context k
1587 CicUniv.oblivion_ugraph
1589 | Cic.Appl (Cic.MutInd _::args),_ ->
1590 snd (HExtlib.split_nth leftno args)
1592 with CicTypeChecker.TypeCheckerFailure _-> assert false
1595 CR.head_beta_reduce ~delta:false
1596 (Cic.Appl (outty ::right_p @ [k])),k
1598 Cic.Prod (Cic.Name "p",
1599 Cic.Appl [eq; mty; m; k],
1601 (CR.head_beta_reduce ~delta:false
1602 (Cic.Appl (outty ::right_p @ [k]))))),k
1605 aux context outty [] 1 mty m cty
1607 let add_lambda_for_refl_m pbo rno mty m k cty =
1608 (* k lives in the right context *)
1609 if rno <> 0 then pbo else
1610 let rec aux mty m = function
1611 | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1612 Cic.Lambda (name,src,
1613 (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1615 Cic.Lambda (Cic.Name "p",
1616 Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1620 let add_pi_for_refl_m new_outty mty m rno =
1621 if rno <> 0 then new_outty else
1622 let rec aux m mty = function
1623 | Cic.Lambda (name, src, tgt) ->
1624 Cic.Lambda (name, src,
1625 aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1628 (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1632 in (* }}} end helper functions *)
1633 (* constructors types with left params already instantiated *)
1634 let outty = CicMetaSubst.apply_subst subst outty in
1635 let cl, left_p, leftno,rno,ugraph =
1636 get_cl_and_left_p uri tyno outty ugraph
1641 CicTypeChecker.type_of_aux' ~subst metasenv context m
1642 CicUniv.oblivion_ugraph
1644 | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty
1645 | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
1646 snd (HExtlib.split_nth leftno args), mty
1648 with CicTypeChecker.TypeCheckerFailure _ ->
1649 raise (AssertFailure(lazy "already ill-typed matched term"))
1652 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1655 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1656 ~metasenv subst new_outty context));
1657 let _,pl,subst,metasenv,ugraph =
1659 (fun cty pbo (i, acc, s, menv, ugraph) ->
1660 (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1661 * (new_)outty right_par (K_i left_par k_par) *)
1663 add_params menv s context uri tyno
1664 cty outty mty m leftno i in
1666 (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1667 ~metasenv subst infty_pbo context));
1668 let expty_pbo, k = (* k is (K_i left_par k_par) *)
1669 add_params menv s context uri tyno
1670 cty new_outty mty m leftno i in
1672 (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1673 ~metasenv subst expty_pbo context));
1674 let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1676 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1677 ~metasenv subst pbo context));
1678 let (pbo, _), subst, metasenv, ugraph =
1679 coerce_to_something_aux pbo infty_pbo expty_pbo
1680 s menv context ugraph
1683 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1684 ~metasenv subst pbo context));
1685 (i-1, pbo::acc, subst, metasenv, ugraph))
1686 cl pl (List.length pl, [], subst, metasenv, ugraph)
1688 let new_outty = add_pi_for_refl_m new_outty mty m rno in
1690 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1691 ~metasenv subst new_outty context));
1694 let refl_m=Cic.Appl[eq_refl;mty;m]in
1695 Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1697 Cic.MutCase(uri,tyno,new_outty,m,pl)
1699 (t, expty), subst, metasenv, ugraph (*}}}*)
1700 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1701 (*{{{*) debug_print (lazy "LAM");
1703 FreshNamesGenerator.mk_fresh_name
1704 ~subst metasenv context ~typ:src2 Cic.Anonymous
1706 let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1707 (* contravariant part: the argument of f:src->ty *)
1708 let (rel1, _), subst, metasenv, ugraph =
1709 coerce_to_something_aux
1710 (Cic.Rel 1) (CS.lift 1 src2)
1711 (CS.lift 1 src) subst metasenv context_src2 ugraph
1713 (* covariant part: the result of f(c x); x:src2; (c x):src *)
1716 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1717 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1719 (* we fix the possible dependency problem in the source ty *)
1720 let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1721 let (bo, _), subst, metasenv, ugraph =
1722 coerce_to_something_aux
1723 bo ty ty2 subst metasenv context_src2 ugraph
1725 let coerced = Cic.Lambda (name_t,src2, bo) in
1726 (coerced, expty), subst, metasenv, ugraph (*}}}*)
1728 (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1729 ~metasenv subst infty context ^ " ==> " ^
1730 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1731 coerce_atom_to_something
1732 t infty expty subst metasenv context ugraph (*}}}*)
1734 debug_print (lazy ("COERCE TO SOMETHING END: "^
1735 CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1739 coerce_to_something_aux t infty expty subst metasenv context ugraph
1740 with Uncertain _ | RefineFailure _ as exn ->
1743 CicMetaSubst.ppterm_in_context metasenv subst t context ^
1744 " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1745 infty context ^ " but is here used with type " ^
1746 CicMetaSubst.ppterm_in_context metasenv subst expty context)
1748 enrich localization_tbl ~f t exn
1750 and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1751 match CicReduction.whd ~delta:false ~subst context infty with
1752 | Cic.Meta _ | Cic.Sort _ ->
1753 t,infty, subst, metasenv, ugraph
1755 debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1756 ~metasenv subst src context));
1757 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1759 let (t, ty_t), subst, metasenv, ugraph =
1760 coerce_to_something true
1761 localization_tbl t src tgt subst metasenv context ugraph
1763 debug_print (lazy ("COERCE TO SORT END: "^
1764 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1765 t, ty_t, subst, metasenv, ugraph
1766 with HExtlib.Localized (_, exn) ->
1768 lazy ("(7)The term " ^
1769 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1770 ^ " is not a type since it has type " ^
1771 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1772 ^ " that is not a sort")
1774 enrich localization_tbl ~f t exn
1777 (* eat prods ends here! *)
1779 let t',ty,subst',metasenv',ugraph1 =
1780 type_of_aux [] metasenv context t ugraph
1782 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1783 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1784 (* Andrea: ho rimesso qui l'applicazione della subst al
1785 metasenv dopo che ho droppato l'invariante che il metsaenv
1786 e' sempre istanziato *)
1787 let substituted_metasenv =
1788 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1790 (* substituted_t,substituted_ty,substituted_metasenv *)
1791 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1793 if clean_dummy_dependent_types then
1794 FreshNamesGenerator.clean_dummy_dependent_types substituted_t
1795 else substituted_t in
1797 if clean_dummy_dependent_types then
1798 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty
1799 else substituted_ty in
1800 let cleaned_metasenv =
1801 if clean_dummy_dependent_types then
1803 (function (n,context,ty) ->
1804 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1809 | Some (n, Cic.Decl t) ->
1811 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1812 | Some (n, Cic.Def (bo,ty)) ->
1813 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1814 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
1816 Some (n, Cic.Def (bo',ty'))
1820 ) substituted_metasenv
1822 substituted_metasenv
1824 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1827 let undebrujin uri typesno tys t =
1830 (fun (name,_,_,_) (i,t) ->
1831 (* here the explicit_named_substituion is assumed to be *)
1833 let t' = Cic.MutInd (uri,i,[]) in
1834 let t = CicSubstitution.subst t' t in
1836 ) tys (typesno - 1,t))
1838 let map_first_n n start f g l =
1839 let rec aux acc k l =
1842 | [] -> raise (Invalid_argument "map_first_n")
1843 | hd :: tl -> f hd k (aux acc (k+1) tl)
1849 (*CSC: this is a very rough approximation; to be finished *)
1850 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1851 let subst,metasenv,ugraph,tys =
1853 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1854 let subst,metasenv,ugraph,cl =
1856 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1857 let rec aux ctx k subst = function
1858 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1859 let subst,metasenv,ugraph,tl =
1861 (subst,metasenv,ugraph,[])
1862 (fun t n (subst,metasenv,ugraph,acc) ->
1863 let subst,metasenv,ugraph =
1865 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1867 subst,metasenv,ugraph,(t::acc))
1868 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1871 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1872 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1873 subst,metasenv,ugraph,t
1874 | Cic.Prod (name,s,t) ->
1875 let ctx = (Some (name,Cic.Decl s))::ctx in
1876 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1877 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1881 (lazy "not well formed constructor type"))
1883 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1884 subst,metasenv,ugraph,(name,ty) :: acc)
1885 cl (subst,metasenv,ugraph,[])
1887 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1888 tys ([],metasenv,ugraph,[])
1890 let substituted_tys =
1892 (fun (name,ind,arity,cl) ->
1894 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1896 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1899 metasenv,ugraph,substituted_tys
1901 let typecheck metasenv uri obj ~localization_tbl =
1902 let ugraph = CicUniv.oblivion_ugraph in
1904 Cic.Constant (name,Some bo,ty,args,attrs) ->
1905 (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
1906 since type_of_aux' destroys localization information (which are
1907 preserved by type_of_aux *)
1910 Cic.CicHash.find localization_tbl bo
1912 HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
1914 let bo',boty,metasenv,ugraph =
1915 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1916 let ty',_,metasenv,ugraph =
1917 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1918 let subst,metasenv,ugraph =
1920 fo_unif_subst [] [] metasenv boty ty' ugraph
1923 | Uncertain _ as exn ->
1926 CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
1928 CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
1929 " but is here used with type " ^
1930 CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
1934 RefineFailure _ -> RefineFailure msg
1935 | Uncertain _ -> Uncertain msg
1938 raise (HExtlib.Localized (loc exn',exn'))
1940 let bo' = CicMetaSubst.apply_subst subst bo' in
1941 let ty' = CicMetaSubst.apply_subst subst ty' in
1942 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1943 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1944 | Cic.Constant (name,None,ty,args,attrs) ->
1945 let ty',_,metasenv,ugraph =
1946 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1948 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1949 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1950 assert (metasenv' = metasenv);
1951 (* Here we do not check the metasenv for correctness *)
1952 let bo',boty,metasenv,ugraph =
1953 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1954 let ty',sort,metasenv,ugraph =
1955 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1959 (* instead of raising Uncertain, let's hope that the meta will become
1962 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1964 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1965 let bo' = CicMetaSubst.apply_subst subst bo' in
1966 let ty' = CicMetaSubst.apply_subst subst ty' in
1967 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1968 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1969 | Cic.Variable _ -> assert false (* not implemented *)
1970 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1971 (*CSC: this code is greately simplified and many many checks are missing *)
1972 (*CSC: e.g. the constructors are not required to build their own types, *)
1973 (*CSC: the arities are not required to have as type a sort, etc. *)
1974 let uri = match uri with Some uri -> uri | None -> assert false in
1975 let typesno = List.length tys in
1976 (* first phase: we fix only the types *)
1977 let metasenv,ugraph,tys =
1979 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1980 let ty',_,metasenv,ugraph =
1981 (* clean_dummy_dependent_types: false to avoid cleaning the names
1982 of the left products, that must be identical to those of the
1983 constructors; however, non-left products should probably be
1985 type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl
1986 metasenv [] ty ugraph
1988 metasenv,ugraph,(name,b,ty',cl)::res
1989 ) tys (metasenv,ugraph,[]) in
1991 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1992 (* second phase: we fix only the constructors *)
1993 let saved_menv = metasenv in
1994 let metasenv,ugraph,tys =
1996 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1997 let metasenv,ugraph,cl' =
1999 (fun (name,ty) (metasenv,ugraph,res) ->
2001 CicTypeChecker.debrujin_constructor
2002 ~cb:(relocalize localization_tbl) uri typesno [] ty in
2003 let ty',_,metasenv,ugraph =
2004 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
2005 let ty' = undebrujin uri typesno tys ty' in
2006 metasenv@saved_menv,ugraph,(name,ty')::res
2007 ) cl (metasenv,ugraph,[])
2009 metasenv,ugraph,(name,b,ty,cl')::res
2010 ) tys (metasenv,ugraph,[]) in
2011 (* third phase: we check the positivity condition *)
2012 let metasenv,ugraph,tys =
2013 are_all_occurrences_positive metasenv ugraph uri tys paramsno
2015 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
2018 (* sara' piu' veloce che raffinare da zero? mah.... *)
2019 let pack_coercion metasenv ctx t =
2020 let module C = Cic in
2021 let rec merge_coercions ctx =
2022 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
2024 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
2025 | C.Meta (n,subst) ->
2028 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
2031 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
2032 | C.Prod (name,so,dest) ->
2033 let ctx' = (Some (name,C.Decl so))::ctx in
2034 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
2035 | C.Lambda (name,so,dest) ->
2036 let ctx' = (Some (name,C.Decl so))::ctx in
2037 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
2038 | C.LetIn (name,so,ty,dest) ->
2039 let ctx' = Some (name,(C.Def (so,ty)))::ctx in
2041 (name, merge_coercions ctx so, merge_coercions ctx ty,
2042 merge_coercions ctx' dest)
2044 let l = List.map (merge_coercions ctx) l in
2046 let b,_,_,_,_ = is_a_double_coercion t in
2048 let ugraph = CicUniv.oblivion_ugraph in
2049 let old_insert_coercions = !insert_coercions in
2050 insert_coercions := false;
2051 let newt, _, menv, _ =
2053 type_of_aux' metasenv ctx t ugraph
2054 with RefineFailure _ | Uncertain _ ->
2057 insert_coercions := old_insert_coercions;
2058 if metasenv <> [] || menv = [] then
2061 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
2064 | C.Var (uri,exp_named_subst) ->
2065 let exp_named_subst = List.map aux exp_named_subst in
2066 C.Var (uri, exp_named_subst)
2067 | C.Const (uri,exp_named_subst) ->
2068 let exp_named_subst = List.map aux exp_named_subst in
2069 C.Const (uri, exp_named_subst)
2070 | C.MutInd (uri,tyno,exp_named_subst) ->
2071 let exp_named_subst = List.map aux exp_named_subst in
2072 C.MutInd (uri,tyno,exp_named_subst)
2073 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
2074 let exp_named_subst = List.map aux exp_named_subst in
2075 C.MutConstruct (uri,tyno,consno,exp_named_subst)
2076 | C.MutCase (uri,tyno,out,te,pl) ->
2077 let pl = List.map (merge_coercions ctx) pl in
2078 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
2079 | C.Fix (fno, fl) ->
2082 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2087 (fun (name,idx,ty,bo) ->
2088 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
2092 | C.CoFix (fno, fl) ->
2095 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2100 (fun (name,ty,bo) ->
2101 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
2106 merge_coercions ctx t
2109 let pack_coercion_metasenv conjectures = conjectures (*
2111 TASSI: this code war written when coercions were a toy,
2112 now packing coercions involves unification thus
2113 the metasenv may change, and this pack coercion
2114 does not handle that.
2116 let module C = Cic in
2118 (fun (i, ctx, ty) ->
2124 Some (name, C.Decl t) ->
2125 Some (name, C.Decl (pack_coercion conjectures ctx t))
2126 | Some (name, C.Def (t,None)) ->
2127 Some (name,C.Def (pack_coercion conjectures ctx t,None))
2128 | Some (name, C.Def (t,Some ty)) ->
2129 Some (name, C.Def (pack_coercion conjectures ctx t,
2130 Some (pack_coercion conjectures ctx ty)))
2136 ((i,ctx,pack_coercion conjectures ctx ty))
2141 let pack_coercion_obj obj = obj (*
2143 TASSI: this code war written when coercions were a toy,
2144 now packing coercions involves unification thus
2145 the metasenv may change, and this pack coercion
2146 does not handle that.
2148 let module C = Cic in
2150 | C.Constant (id, body, ty, params, attrs) ->
2154 | Some body -> Some (pack_coercion [] [] body)
2156 let ty = pack_coercion [] [] ty in
2157 C.Constant (id, body, ty, params, attrs)
2158 | C.Variable (name, body, ty, params, attrs) ->
2162 | Some body -> Some (pack_coercion [] [] body)
2164 let ty = pack_coercion [] [] ty in
2165 C.Variable (name, body, ty, params, attrs)
2166 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2167 let conjectures = pack_coercion_metasenv conjectures in
2168 let body = pack_coercion conjectures [] body in
2169 let ty = pack_coercion conjectures [] ty in
2170 C.CurrentProof (name, conjectures, body, ty, params, attrs)
2171 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2174 (fun (name, ind, arity, cl) ->
2175 let arity = pack_coercion [] [] arity in
2177 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2179 (name, ind, arity, cl))
2182 C.InductiveDefinition (indtys, params, leftno, attrs) *)
2187 let type_of_aux' metasenv context term =
2190 type_of_aux' metasenv context term in
2192 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2194 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2197 | RefineFailure msg as e ->
2198 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2200 | Uncertain msg as e ->
2201 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2205 let profiler2 = HExtlib.profile "CicRefine"
2207 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2208 profiler2.HExtlib.profile
2209 (type_of_aux' ?localization_tbl metasenv context term) ugraph
2211 let typecheck ~localization_tbl metasenv uri obj =
2212 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2214 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2215 (* vim:set foldmethod=marker: *)