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 rec count_prods context ty =
409 match CicReduction.whd context ~subst:subst'' ty with
410 | Cic.Prod (n,s,t) ->
411 1 + count_prods (Some (n,Cic.Decl s)::context) t
414 let exp_prods = count_prods context ty' in
415 let inf_prods = count_prods context inferredty in
416 let te', inferredty, metasenv'', subst'', ugraph2 =
417 let rec aux t m s ug it = function
420 match CicReduction.whd context ~subst:s it with
421 | Cic.Prod (_,src,tgt) ->
422 let newmeta, metaty, s, m, ug =
423 type_of_aux s m context (Cic.Implicit None) ug
426 fo_unif_subst s context m metaty src ug
430 | Cic.Appl l -> Cic.Appl (l @ [newmeta])
431 | _ -> Cic.Appl [t;newmeta]
433 aux t m s ug (CicSubstitution.subst newmeta tgt) (n-1)
436 aux te' metasenv'' subst'' ugraph2 inferredty
437 (max 0 (inf_prods - exp_prods))
439 let (te', ty'), subst''',metasenv''',ugraph3 =
440 coerce_to_something true localization_tbl te' inferredty ty'
441 subst'' metasenv'' context ugraph2
443 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
444 | C.Prod (name,s,t) ->
445 let s',sort1,subst',metasenv',ugraph1 =
446 type_of_aux subst metasenv context s ugraph
448 let s',sort1,subst', metasenv',ugraph1 =
449 coerce_to_sort localization_tbl
450 s' sort1 subst' context metasenv' ugraph1
452 let context_for_t = ((Some (name,(C.Decl s')))::context) in
453 let t',sort2,subst'',metasenv'',ugraph2 =
454 type_of_aux subst' metasenv'
455 context_for_t t ugraph1
457 let t',sort2,subst'',metasenv'',ugraph2 =
458 coerce_to_sort localization_tbl
459 t' sort2 subst'' context_for_t metasenv'' ugraph2
461 let sop,subst''',metasenv''',ugraph3 =
462 sort_of_prod localization_tbl subst'' metasenv''
463 context (name,s') t' (sort1,sort2) ugraph2
465 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
466 | C.Lambda (n,s,t) ->
467 let s',sort1,subst',metasenv',ugraph1 =
468 type_of_aux subst metasenv context s ugraph
470 let s',sort1,subst',metasenv',ugraph1 =
471 coerce_to_sort localization_tbl
472 s' sort1 subst' context metasenv' ugraph1
474 let context_for_t = ((Some (n,(C.Decl s')))::context) in
475 let t',type2,subst'',metasenv'',ugraph2 =
476 type_of_aux subst' metasenv' context_for_t t ugraph1
478 C.Lambda (n,s',t'),C.Prod (n,s',type2),
479 subst'',metasenv'',ugraph2
480 | C.LetIn (n,s,ty,t) ->
481 (* only to check if s is well-typed *)
482 let s',ty',subst',metasenv',ugraph1 =
483 type_of_aux subst metasenv context s ugraph in
484 let ty,_,subst',metasenv',ugraph1 =
485 type_of_aux subst' metasenv' context ty ugraph1 in
486 let subst',metasenv',ugraph1 =
488 fo_unif_subst subst' context metasenv'
492 enrich localization_tbl s' exn
495 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
496 context ^ " has type " ^
497 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
498 context ^ " but is here used with type " ^
499 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
502 let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
504 let t',inferredty,subst'',metasenv'',ugraph2 =
505 type_of_aux subst' metasenv'
506 context_for_t t ugraph1
508 (* One-step LetIn reduction.
509 * Even faster than the previous solution.
510 * Moreover the inferred type is closer to the expected one.
512 C.LetIn (n,s',ty,t'),
513 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
514 subst'',metasenv'',ugraph2
515 | C.Appl (he::((_::_) as tl)) ->
516 let he',hetype,subst',metasenv',ugraph1 =
517 type_of_aux subst metasenv context he ugraph
519 let tlbody_and_type,subst'',metasenv'',ugraph2 =
520 typeof_list subst' metasenv' context ugraph1 tl
522 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
523 eat_prods true subst'' metasenv'' context
524 he' hetype tlbody_and_type ugraph2
526 let newappl = (C.Appl (coerced_he::coerced_args)) in
527 avoid_double_coercion
528 context subst''' metasenv''' ugraph3 newappl applty
529 | C.Appl _ -> assert false
530 | C.Const (uri,exp_named_subst) ->
531 let exp_named_subst',subst',metasenv',ugraph1 =
532 check_exp_named_subst subst metasenv context
533 exp_named_subst ugraph in
534 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
536 CicSubstitution.subst_vars exp_named_subst' ty_uri
538 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
539 | C.MutInd (uri,i,exp_named_subst) ->
540 let exp_named_subst',subst',metasenv',ugraph1 =
541 check_exp_named_subst subst metasenv context
542 exp_named_subst ugraph
544 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
546 CicSubstitution.subst_vars exp_named_subst' ty_uri in
547 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
548 | C.MutConstruct (uri,i,j,exp_named_subst) ->
549 let exp_named_subst',subst',metasenv',ugraph1 =
550 check_exp_named_subst subst metasenv context
551 exp_named_subst ugraph
554 type_of_mutual_inductive_constr uri i j ugraph1
557 CicSubstitution.subst_vars exp_named_subst' ty_uri
559 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
561 | C.MutCase (uri, i, outtype, term, pl) ->
562 (* first, get the inductive type (and noparams)
563 * in the environment *)
564 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
565 let _ = CicTypeChecker.typecheck uri in
566 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
568 C.InductiveDefinition (l,expl_params,parsno,_) ->
569 List.nth l i , expl_params, parsno, u
571 enrich localization_tbl t
573 (lazy ("Unkown mutual inductive definition " ^
574 U.string_of_uri uri)))
576 if List.length constructors <> List.length pl then
577 enrich localization_tbl t
579 (lazy "Wrong number of cases")) ;
580 let rec count_prod t =
581 match CicReduction.whd ~subst context t with
582 C.Prod (_, _, t) -> 1 + (count_prod t)
585 let no_args = count_prod arity in
586 (* now, create a "generic" MutInd *)
587 let metasenv,left_args =
588 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
590 let metasenv,right_args =
591 let no_right_params = no_args - no_left_params in
592 if no_right_params < 0 then assert false
593 else CicMkImplicit.n_fresh_metas
594 metasenv subst context no_right_params
596 let metasenv,exp_named_subst =
597 CicMkImplicit.fresh_subst metasenv subst context expl_params in
600 C.MutInd (uri,i,exp_named_subst)
603 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
605 (* check consistency with the actual type of term *)
606 let term',actual_type,subst,metasenv,ugraph1 =
607 type_of_aux subst metasenv context term ugraph in
608 let expected_type',_, subst, metasenv,ugraph2 =
609 type_of_aux subst metasenv context expected_type ugraph1
611 let actual_type = CicReduction.whd ~subst context actual_type in
612 let subst,metasenv,ugraph3 =
614 fo_unif_subst subst context metasenv
615 expected_type' actual_type ugraph2
618 enrich localization_tbl term' exn
621 CicMetaSubst.ppterm_in_context ~metasenv subst term'
622 context ^ " has type " ^
623 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
624 context ^ " but is here used with type " ^
625 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type'
628 let rec instantiate_prod t =
632 match CicReduction.whd ~subst context t with
634 instantiate_prod (CicSubstitution.subst he t') tl
637 let arity_instantiated_with_left_args =
638 instantiate_prod arity left_args in
639 (* TODO: check if the sort elimination
640 * is allowed: [(I q1 ... qr)|B] *)
641 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
643 (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
645 if left_args = [] then
646 (C.MutConstruct (uri,i,j,exp_named_subst))
649 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
651 let p',actual_type,subst,metasenv,ugraph1 =
652 type_of_aux subst metasenv context p ugraph
654 let constructor',expected_type, subst, metasenv,ugraph2 =
655 type_of_aux subst metasenv context constructor ugraph1
657 let outtypeinstance,subst,metasenv,ugraph3 =
659 check_branch 0 context metasenv subst
660 no_left_params actual_type constructor' expected_type
664 enrich localization_tbl constructor'
667 CicMetaSubst.ppterm_in_context metasenv subst p'
668 context ^ " has type " ^
669 CicMetaSubst.ppterm_in_context metasenv subst actual_type
670 context ^ " but is here used with type " ^
671 CicMetaSubst.ppterm_in_context metasenv subst expected_type
675 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
676 pl ([],List.length pl,[],subst,metasenv,ugraph3)
679 (* we are left to check that the outype matches his instances.
680 The easy case is when the outype is specified, that amount
681 to a trivial check. Otherwise, we should guess a type from
685 let outtype,outtypety, subst, metasenv,ugraph4 =
686 type_of_aux subst metasenv context outtype ugraph4 in
689 (let candidate,ugraph5,metasenv,subst =
690 let exp_name_subst, metasenv =
692 CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
694 let uris = CicUtil.params_of_obj o in
696 fun uri (acc,metasenv) ->
697 let metasenv',new_meta =
698 CicMkImplicit.mk_implicit metasenv subst context
701 CicMkImplicit.identity_relocation_list_for_metavariable
704 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
708 match left_args,right_args with
709 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
711 let rec mk_right_args =
714 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
716 let right_args_no = List.length right_args in
717 let lifted_left_args =
718 List.map (CicSubstitution.lift right_args_no) left_args
720 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
721 (lifted_left_args @ mk_right_args right_args_no))
724 FreshNamesGenerator.mk_fresh_name ~subst metasenv
725 context Cic.Anonymous ~typ:ty
727 match outtypeinstances with
729 let extended_context =
730 let rec add_right_args =
732 Cic.Prod (name,ty,t) ->
733 Some (name,Cic.Decl ty)::(add_right_args t)
736 (Some (fresh_name,Cic.Decl ty))::
738 (add_right_args arity_instantiated_with_left_args))@
741 let metasenv,new_meta =
742 CicMkImplicit.mk_implicit metasenv subst extended_context
745 CicMkImplicit.identity_relocation_list_for_metavariable
748 let rec add_lambdas b =
750 Cic.Prod (name,ty,t) ->
751 Cic.Lambda (name,ty,(add_lambdas b t))
752 | _ -> Cic.Lambda (fresh_name, ty, b)
755 add_lambdas (Cic.Meta (new_meta,irl))
756 arity_instantiated_with_left_args
758 (Some candidate),ugraph4,metasenv,subst
759 | (constructor_args_no,_,instance,_)::tl ->
761 let instance',subst,metasenv =
762 CicMetaSubst.delift_rels subst metasenv
763 constructor_args_no instance
765 let candidate,ugraph,metasenv,subst =
767 fun (candidate_oty,ugraph,metasenv,subst)
768 (constructor_args_no,_,instance,_) ->
769 match candidate_oty with
770 | None -> None,ugraph,metasenv,subst
773 let instance',subst,metasenv =
774 CicMetaSubst.delift_rels subst metasenv
775 constructor_args_no instance
777 let subst,metasenv,ugraph =
778 fo_unif_subst subst context metasenv
781 candidate_oty,ugraph,metasenv,subst
783 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
784 | RefineFailure _ | Uncertain _ ->
785 None,ugraph,metasenv,subst
786 ) (Some instance',ugraph4,metasenv,subst) tl
789 | None -> None, ugraph,metasenv,subst
791 let rec add_lambdas n b =
793 Cic.Prod (name,ty,t) ->
794 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
796 Cic.Lambda (fresh_name, ty,
797 CicSubstitution.lift (n + 1) t)
800 (add_lambdas 0 t arity_instantiated_with_left_args),
801 ugraph,metasenv,subst
802 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
803 None,ugraph4,metasenv,subst
806 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
808 let subst,metasenv,ugraph =
810 fo_unif_subst subst context metasenv
811 candidate outtype ugraph5
813 exn -> assert false(* unification against a metavariable *)
815 C.MutCase (uri, i, outtype, term', pl'),
816 CicReduction.head_beta_reduce
817 (CicMetaSubst.apply_subst subst
818 (Cic.Appl (outtype::right_args@[term']))),
819 subst,metasenv,ugraph)
820 | _ -> (* easy case *)
821 let tlbody_and_type,subst,metasenv,ugraph4 =
822 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
824 let _,_,_,subst,metasenv,ugraph4 =
825 eat_prods false subst metasenv context
826 outtype outtypety tlbody_and_type ugraph4
828 let _,_, subst, metasenv,ugraph5 =
829 type_of_aux subst metasenv context
830 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
832 let (subst,metasenv,ugraph6) =
834 (fun (subst,metasenv,ugraph)
835 p (constructor_args_no,context,instance,args)
840 CicSubstitution.lift constructor_args_no outtype
842 C.Appl (outtype'::args)
844 CicReduction.head_beta_reduce ~delta:false
845 ~upto:(List.length args) appl
848 fo_unif_subst subst context metasenv instance instance'
852 enrich localization_tbl p exn
855 CicMetaSubst.ppterm_in_context ~metasenv subst p
856 context ^ " has type " ^
857 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
858 context ^ " but is here used with type " ^
859 CicMetaSubst.ppterm_in_context ~metasenv subst instance
861 (subst,metasenv,ugraph5) pl' outtypeinstances
863 C.MutCase (uri, i, outtype, term', pl'),
864 CicReduction.head_beta_reduce
865 (CicMetaSubst.apply_subst subst
866 (C.Appl(outtype::right_args@[term']))),
867 subst,metasenv,ugraph6)
869 let fl_ty',subst,metasenv,types,ugraph1,len =
871 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
872 let ty',_,subst',metasenv',ugraph1 =
873 type_of_aux subst metasenv context ty ugraph
875 fl @ [ty'],subst',metasenv',
876 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
877 :: types, ugraph, len+1
878 ) ([],subst,metasenv,[],ugraph,0) fl
880 let context' = types@context in
881 let fl_bo',subst,metasenv,ugraph2 =
883 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
884 let bo',ty_of_bo,subst,metasenv,ugraph1 =
885 type_of_aux subst metasenv context' bo ugraph in
886 let expected_ty = CicSubstitution.lift len ty in
887 let subst',metasenv',ugraph' =
889 fo_unif_subst subst context' metasenv
890 ty_of_bo expected_ty ugraph1
893 enrich localization_tbl bo exn
896 CicMetaSubst.ppterm_in_context ~metasenv subst bo
897 context' ^ " has type " ^
898 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
899 context' ^ " but is here used with type " ^
900 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
903 fl @ [bo'] , subst',metasenv',ugraph'
904 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
906 let ty = List.nth fl_ty' i in
907 (* now we have the new ty in fl_ty', the new bo in fl_bo',
908 * and we want the new fl with bo' and ty' injected in the right
911 let rec map3 f l1 l2 l3 =
914 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
917 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
920 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
922 let fl_ty',subst,metasenv,types,ugraph1,len =
924 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
925 let ty',_,subst',metasenv',ugraph1 =
926 type_of_aux subst metasenv context ty ugraph
928 fl @ [ty'],subst',metasenv',
929 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
930 types, ugraph1, len+1
931 ) ([],subst,metasenv,[],ugraph,0) fl
933 let context' = types@context in
934 let fl_bo',subst,metasenv,ugraph2 =
936 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
937 let bo',ty_of_bo,subst,metasenv,ugraph1 =
938 type_of_aux subst metasenv context' bo ugraph in
939 let expected_ty = CicSubstitution.lift len ty in
940 let subst',metasenv',ugraph' =
942 fo_unif_subst subst context' metasenv
943 ty_of_bo expected_ty ugraph1
946 enrich localization_tbl bo exn
949 CicMetaSubst.ppterm_in_context ~metasenv subst bo
950 context' ^ " has type " ^
951 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
952 context' ^ " but is here used with type " ^
953 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
956 fl @ [bo'],subst',metasenv',ugraph'
957 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
959 let ty = List.nth fl_ty' i in
960 (* now we have the new ty in fl_ty', the new bo in fl_bo',
961 * and we want the new fl with bo' and ty' injected in the right
964 let rec map3 f l1 l2 l3 =
967 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
970 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
973 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
975 relocalize localization_tbl t t';
978 (* check_metasenv_consistency checks that the "canonical" context of a
979 metavariable is consitent - up to relocation via the relocation list l -
980 with the actual context *)
981 and check_metasenv_consistency
982 metano subst metasenv context canonical_context l ugraph
984 let module C = Cic in
985 let module R = CicReduction in
986 let module S = CicSubstitution in
987 let lifted_canonical_context =
991 | (Some (n,C.Decl t))::tl ->
992 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
993 | None::tl -> None::(aux (i+1) tl)
994 | (Some (n,C.Def (t,ty)))::tl ->
998 (S.subst_meta l (S.lift i t),
999 S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
1001 aux 1 canonical_context
1005 (fun (l,subst,metasenv,ugraph) t ct ->
1008 l @ [None],subst,metasenv,ugraph
1009 | Some t,Some (_,C.Def (ct,_)) ->
1010 (*CSC: the following optimization is to avoid a possibly
1011 expensive reduction that can be easily avoided and
1012 that is quite frequent. However, this is better
1013 handled using levels to control reduction *)
1018 match List.nth context (n - 1) with
1019 Some (_,C.Def (te,_)) -> S.lift n te
1025 let subst',metasenv',ugraph' =
1027 (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
1028 * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
1029 fo_unif_subst subst context metasenv optimized_t ct ugraph
1030 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))))))
1032 l @ [Some t],subst',metasenv',ugraph'
1033 | Some t,Some (_,C.Decl ct) ->
1034 let t',inferredty,subst',metasenv',ugraph1 =
1035 type_of_aux subst metasenv context t ugraph
1037 let subst'',metasenv'',ugraph2 =
1040 subst' context metasenv' inferredty ct ugraph1
1041 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))))))
1043 l @ [Some t'], subst'',metasenv'',ugraph2
1045 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
1047 Invalid_argument _ ->
1051 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1052 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1053 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1055 and check_exp_named_subst metasubst metasenv context tl ugraph =
1056 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1058 [] -> [],metasubst,metasenv,ugraph
1060 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1062 CicSubstitution.subst_vars substs ty_uri in
1063 (* CSC: why was this code here? it is wrong
1064 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1065 Cic.Variable (_,Some bo,_,_) ->
1067 (RefineFailure (lazy
1068 "A variable with a body can not be explicit substituted"))
1069 | Cic.Variable (_,None,_,_) -> ()
1072 (RefineFailure (lazy
1073 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1076 let t',typeoft,metasubst',metasenv',ugraph2 =
1077 type_of_aux metasubst metasenv context t ugraph1 in
1078 let subst = uri,t' in
1079 let metasubst'',metasenv'',ugraph3 =
1082 metasubst' context metasenv' typeoft typeofvar ugraph2
1084 raise (RefineFailure (lazy
1085 ("Wrong Explicit Named Substitution: " ^
1086 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1087 " not unifiable with " ^
1088 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1090 (* FIXME: no mere tail recursive! *)
1091 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1092 check_exp_named_subst_aux
1093 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1095 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1097 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1100 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1103 let module C = Cic in
1104 let context_for_t2 = (Some (name,C.Decl s))::context in
1105 let t1'' = CicReduction.whd ~subst context t1 in
1106 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1107 match (t1'', t2'') with
1108 | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) ->
1109 (* different than Coq manual!!! *)
1110 C.Sort s2,subst,metasenv,ugraph
1111 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1112 let t' = CicUniv.fresh() in
1114 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1115 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1116 C.Sort (C.Type t'),subst,metasenv,ugraph2
1118 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1119 | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
1120 let t' = CicUniv.fresh() in
1122 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1123 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1124 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1126 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1127 | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
1128 let t' = CicUniv.fresh() in
1130 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1131 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1132 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1134 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1135 | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
1136 let t' = CicUniv.fresh() in
1138 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1139 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1140 C.Sort (C.Type t'),subst,metasenv,ugraph2
1142 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1143 | (C.Sort _,C.Sort (C.Type t1)) ->
1144 C.Sort (C.Type t1),subst,metasenv,ugraph
1145 | (C.Sort _,C.Sort (C.CProp t1)) ->
1146 C.Sort (C.CProp t1),subst,metasenv,ugraph
1147 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1148 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1149 (* TODO how can we force the meta to become a sort? If we don't we
1150 * break the invariant that refine produce only well typed terms *)
1151 (* TODO if we check the non meta term and if it is a sort then we
1152 * are likely to know the exact value of the result e.g. if the rhs
1153 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1154 let (metasenv,idx) =
1155 CicMkImplicit.mk_implicit_sort metasenv subst in
1156 let (subst, metasenv,ugraph1) =
1158 fo_unif_subst subst context_for_t2 metasenv
1159 (C.Meta (idx,[])) t2'' ugraph
1160 with _ -> assert false (* unification against a metavariable *)
1162 t2'',subst,metasenv,ugraph1
1165 enrich localization_tbl s
1169 "%s is supposed to be a type, but its type is %s"
1170 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1171 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1173 enrich localization_tbl t
1177 "%s is supposed to be a type, but its type is %s"
1178 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1179 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1181 and avoid_double_coercion context subst metasenv ugraph t ty =
1182 if not !pack_coercions then
1183 t,ty,subst,metasenv,ugraph
1185 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1187 let source_carr = CoercGraph.source_of c2 in
1188 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1189 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1191 | CoercGraph.SomeCoercion candidates ->
1193 HExtlib.list_findopt
1194 (fun (metasenv,last,c) _ ->
1195 let subst,metasenv,ugraph =
1196 fo_unif_subst subst context metasenv last head ugraph in
1197 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1202 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1203 let newt,_,subst,metasenv,ugraph =
1204 type_of_aux subst metasenv context c ugraph in
1205 debug_print (lazy "tipa...");
1206 let subst, metasenv, ugraph =
1207 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1208 fo_unif_subst subst context metasenv newt t ugraph
1210 debug_print (lazy "unifica...");
1211 Some (newt, ty, subst, metasenv, ugraph)
1213 | RefineFailure s | Uncertain s when not !pack_coercions->
1214 debug_print s; debug_print (lazy "stop\n");None
1215 | RefineFailure s | Uncertain s ->
1216 debug_print s;debug_print (lazy "goon\n");
1218 let old_pack_coercions = !pack_coercions in
1219 pack_coercions := false; (* to avoid diverging *)
1220 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1221 type_of_aux subst metasenv context c1_c2_implicit ugraph
1223 pack_coercions := old_pack_coercions;
1225 is_a_double_coercion refined_c1_c2_implicit
1231 match refined_c1_c2_implicit with
1232 | Cic.Appl l -> HExtlib.list_last l
1235 let subst, metasenv, ugraph =
1236 try fo_unif_subst subst context metasenv
1238 with RefineFailure s| Uncertain s->
1239 debug_print s;assert false
1241 let subst, metasenv, ugraph =
1242 fo_unif_subst subst context metasenv
1243 refined_c1_c2_implicit t ugraph
1245 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1247 | RefineFailure s | Uncertain s ->
1248 pack_coercions := true;debug_print s;None
1249 | exn -> pack_coercions := true; raise exn))
1252 (match selected with
1256 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1257 t, ty, subst, metasenv, ugraph)
1258 | _ -> t, ty, subst, metasenv, ugraph)
1260 t, ty, subst, metasenv, ugraph
1262 and typeof_list subst metasenv context ugraph l =
1263 let tlbody_and_type,subst,metasenv,ugraph =
1265 (fun x (res,subst,metasenv,ugraph) ->
1266 let x',ty,subst',metasenv',ugraph1 =
1267 type_of_aux subst metasenv context x ugraph
1269 (x', ty)::res,subst',metasenv',ugraph1
1270 ) l ([],subst,metasenv,ugraph)
1272 tlbody_and_type,subst,metasenv,ugraph
1275 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1277 (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1278 let fix_arity n metasenv context subst he hetype ugraph =
1279 let hetype = CicMetaSubst.apply_subst subst hetype in
1280 (* instead of a dummy functional type we may create the real product
1281 * using args_bo_and_ty, but since coercions lookup ignores the
1282 * actual ariety we opt for the simple solution *)
1283 let fty = Cic.Prod(Cic.Anonymous, Cic.Sort Cic.Prop, Cic.Sort Cic.Prop) in
1284 match CoercGraph.look_for_coercion metasenv subst context hetype fty with
1285 | CoercGraph.NoCoercion -> []
1286 | CoercGraph.NotHandled ->
1287 raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1288 | CoercGraph.SomeCoercionToTgt candidates
1289 | CoercGraph.SomeCoercion candidates ->
1291 (fun (metasenv,last,coerc) ->
1293 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1295 let subst,metasenv,ugraph =
1296 fo_unif_subst subst context metasenv last he ugraph in
1297 debug_print (lazy ("New head: "^ pp coerc));
1299 CicTypeChecker.type_of_aux' ~subst metasenv context coerc
1302 debug_print (lazy (" has type: "^ pp tty));
1303 Some (coerc,tty,subst,metasenv,ugraph)
1305 | Uncertain _ | RefineFailure _
1306 | HExtlib.Localized (_,Uncertain _)
1307 | HExtlib.Localized (_,RefineFailure _) -> None
1308 | exn -> assert false)
1311 (* aux function to process the type of the head and the args in parallel *)
1312 let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1314 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1315 | (hete, hety)::tl as args ->
1316 match (CicReduction.whd ~subst context hetype) with
1317 | Cic.Prod (n,s,t) ->
1318 let arg,subst,metasenv,ugraph =
1319 coerce_to_something allow_coercions localization_tbl
1320 hete hety s subst metasenv context ugraph in
1322 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1323 ugraph (newargs@[arg]) tl
1326 match he, newargs with
1328 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1329 | _ -> Cic.Appl (he::List.map fst newargs)
1331 (*{{{*) debug_print (lazy
1333 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1334 "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1335 "\n but is applyed to: " ^ String.concat ";"
1336 (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1337 let error = ref None in
1338 let possible_fixes =
1339 fix_arity (List.length args) metasenv context subst he hetype
1342 HExtlib.list_findopt
1343 (fun (he,hetype,subst,metasenv,ugraph) _ ->
1344 (* {{{ *)debug_print (lazy ("Try fix: "^
1345 CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1346 debug_print (lazy (" of type: "^
1347 CicMetaSubst.ppterm_in_context
1348 ~metasenv subst hetype context)); (* }}} *)
1350 Some (eat_prods_and_args
1351 metasenv subst context he hetype ugraph [] args)
1353 | RefineFailure _ | Uncertain _
1354 | HExtlib.Localized (_,RefineFailure _)
1355 | HExtlib.Localized (_,Uncertain _) as exn ->
1356 error := Some exn; None)
1364 (MoreArgsThanExpected
1365 (List.length args, RefineFailure (lazy "")))
1366 | Some exn -> raise exn
1368 (* first we check if we are in the simple case of a meta closed term *)
1369 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1370 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1371 (* this optimization is to postpone fix_arity (the most common case)*)
1372 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1374 (* this (says CSC) is also useful to infer dependent types *)
1375 let pristinemenv = metasenv in
1376 let metasenv,hetype' =
1377 mk_prod_of_metas metasenv context subst args_bo_and_ty
1380 let subst,metasenv,ugraph =
1381 fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1383 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1384 with RefineFailure _ | Uncertain _ ->
1385 subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1387 let coerced_args,subst,metasenv,he,t,ugraph =
1390 metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1392 MoreArgsThanExpected (residuals,exn) ->
1393 more_args_than_expected localization_tbl metasenv
1394 subst he context hetype' residuals args_bo_and_ty exn
1396 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1398 and coerce_to_something
1399 allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1401 let module CS = CicSubstitution in
1402 let module CR = CicReduction in
1403 let cs_subst = CS.subst ~avoid_beta_redexes:true in
1404 let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1405 debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1407 CoercGraph.look_for_coercion metasenv subst context infty expty
1410 | CoercGraph.NoCoercion
1411 | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy
1412 "coerce_atom_to_something fails since no coercions found"))
1413 | CoercGraph.NotHandled when
1414 not (CicUtil.is_meta_closed infty) ||
1415 not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy
1416 "coerce_atom_to_something fails since carriers have metas"))
1417 | CoercGraph.NotHandled -> raise (RefineFailure (lazy
1418 "coerce_atom_to_something fails since no coercions found"))
1419 | CoercGraph.SomeCoercion candidates ->
1420 debug_print (lazy (string_of_int (List.length candidates) ^
1421 " candidates found"));
1422 let uncertain = ref false in
1426 (fun (metasenv,last,c) ->
1428 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1429 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1431 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
1432 "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
1434 debug_print (lazy ("FO_UNIF_SUBST: " ^
1435 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1436 let subst,metasenv,ugraph =
1437 fo_unif_subst subst context metasenv last t ugraph
1439 let newt,newhety,subst,metasenv,ugraph =
1440 type_of_aux subst metasenv context c ugraph in
1441 let newt, newty, subst, metasenv, ugraph =
1442 avoid_double_coercion context subst metasenv ugraph newt
1445 let subst,metasenv,ugraph =
1446 fo_unif_subst subst context metasenv newhety expty ugraph
1449 CicReduction.are_convertible
1450 ~subst ~metasenv context infty expty ugraph
1453 Some ((t,infty), subst, metasenv, ugraph)
1455 let newt = (* unfold coercion if `Variant *)
1457 | Cic.Appl (hd::args) ->
1458 let uri = CicUtil.uri_of_term hd in
1460 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
1462 | Cic.Constant (_,Some t,_,[],attrs),_
1463 when List.exists ((=) (`Flavour `Variant)) attrs ->
1468 Some ((newt,newty), subst, metasenv, ugraph)
1470 | Uncertain _ -> uncertain := true; None
1471 | RefineFailure _ -> None)
1476 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1484 | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1485 | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1487 let rec coerce_to_something_aux
1488 t infty expty subst metasenv context ugraph
1491 let subst, metasenv, ugraph =
1492 fo_unif_subst subst context metasenv infty expty ugraph
1494 (t, expty), subst, metasenv, ugraph
1495 with (Uncertain _ | RefineFailure _ as exn)
1496 when allow_coercions && !insert_coercions ->
1497 let whd = CicReduction.whd ~delta:false in
1498 let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1499 let infty = clean infty subst context in
1500 let expty = clean expty subst context in
1501 let t = clean t subst context in
1502 (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1503 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1504 CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1505 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1506 let (coerced,_),subst,metasenv,_ as result =
1507 match infty, expty, t with
1508 | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1509 (*{{{*) debug_print (lazy "FIX");
1511 [name,i,_(* infty *),bo] ->
1513 Some (Cic.Name name,Cic.Decl expty)::context in
1514 let (rel1, _), subst, metasenv, ugraph =
1515 coerce_to_something_aux (Cic.Rel 1)
1516 (CS.lift 1 expty) (CS.lift 1 infty) subst
1517 metasenv context_bo ugraph in
1518 let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1519 let (bo,_), subst, metasenv, ugraph =
1520 coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1522 metasenv context_bo ugraph
1524 (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1525 | _ -> assert false (* not implemented yet *)) (*}}}*)
1526 | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1527 (*{{{*) debug_print (lazy "CASE");
1528 (* {{{ helper functions *)
1529 let get_cl_and_left_p uri tyno outty ugraph =
1530 match CicEnvironment.get_obj ugraph uri with
1531 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1534 match CicReduction.whd ~delta:false ctx t with
1535 | Cic.Prod (name,src,tgt) ->
1536 let ctx = Some (name, Cic.Decl src) :: ctx in
1542 let rec skip_lambda_delifting t n =
1545 | Cic.Lambda (_,_,t),n ->
1546 skip_lambda_delifting
1547 (CS.subst (Cic.Implicit None) t) (n - 1)
1550 let get_l_r_p n = function
1551 | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1552 | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1553 HExtlib.split_nth n args
1556 let _, _, ty, cl = List.nth tl tyno in
1557 let pis = count_pis ty in
1558 let rno = pis - leftno in
1559 let t = skip_lambda_delifting outty rno in
1560 let left_p, _ = get_l_r_p leftno t in
1561 let instantiale_with_left cl =
1565 (fun t p -> match t with
1566 | Cic.Prod (_,_,t) ->
1572 let cl = instantiale_with_left (List.map snd cl) in
1573 cl, left_p, leftno, rno, ugraph
1576 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1579 let rec mkr n = function
1580 | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1583 CicReplace.replace_lifting
1584 ~equality:(fun _ -> CicUtil.alpha_equivalence)
1586 ~what:(matched::right_p)
1587 ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1591 | Cic.Lambda (name, src, tgt),_ ->
1592 Cic.Lambda (name, src,
1593 keep_lambdas_and_put_expty
1594 (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1595 (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1598 let eq_uri, eq, eq_refl =
1599 match LibraryObjects.eq_URI () with
1600 | None -> HLog.warn "no default equality"; raise exn
1601 | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1604 metasenv subst context uri tyno cty outty mty m leftno i
1606 let rec aux context outty par k mty m = function
1607 | Cic.Prod (name, src, tgt) ->
1610 (Some (name, Cic.Decl src) :: context)
1611 (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1612 (CS.lift 1 mty) (CS.lift 1 m) tgt
1614 Cic.Prod (name, src, t), k
1617 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1618 if par <> [] then Cic.Appl (k::par) else k
1620 Cic.Prod (Cic.Name "p",
1621 Cic.Appl [eq; mty; m; k],
1623 (CR.head_beta_reduce ~delta:false
1624 (Cic.Appl [outty;k])))),k
1625 | Cic.Appl (Cic.MutInd _::pl) ->
1626 let left_p,right_p = HExtlib.split_nth leftno pl in
1627 let has_rights = right_p <> [] in
1629 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1630 Cic.Appl (k::left_p@par)
1634 CicTypeChecker.type_of_aux' ~subst metasenv context k
1635 CicUniv.oblivion_ugraph
1637 | Cic.Appl (Cic.MutInd _::args),_ ->
1638 snd (HExtlib.split_nth leftno args)
1640 with CicTypeChecker.TypeCheckerFailure _-> assert false
1643 CR.head_beta_reduce ~delta:false
1644 (Cic.Appl (outty ::right_p @ [k])),k
1646 Cic.Prod (Cic.Name "p",
1647 Cic.Appl [eq; mty; m; k],
1649 (CR.head_beta_reduce ~delta:false
1650 (Cic.Appl (outty ::right_p @ [k]))))),k
1653 aux context outty [] 1 mty m cty
1655 let add_lambda_for_refl_m pbo rno mty m k cty =
1656 (* k lives in the right context *)
1657 if rno <> 0 then pbo else
1658 let rec aux mty m = function
1659 | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1660 Cic.Lambda (name,src,
1661 (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1663 Cic.Lambda (Cic.Name "p",
1664 Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1668 let add_pi_for_refl_m new_outty mty m rno =
1669 if rno <> 0 then new_outty else
1670 let rec aux m mty = function
1671 | Cic.Lambda (name, src, tgt) ->
1672 Cic.Lambda (name, src,
1673 aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1676 (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1680 in (* }}} end helper functions *)
1681 (* constructors types with left params already instantiated *)
1682 let outty = CicMetaSubst.apply_subst subst outty in
1683 let cl, left_p, leftno,rno,ugraph =
1684 get_cl_and_left_p uri tyno outty ugraph
1689 CicTypeChecker.type_of_aux' ~subst metasenv context m
1690 CicUniv.oblivion_ugraph
1692 | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty
1693 | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
1694 snd (HExtlib.split_nth leftno args), mty
1696 with CicTypeChecker.TypeCheckerFailure _ ->
1697 raise (AssertFailure(lazy "already ill-typed matched term"))
1700 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1703 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1704 ~metasenv subst new_outty context));
1705 let _,pl,subst,metasenv,ugraph =
1707 (fun cty pbo (i, acc, s, menv, ugraph) ->
1708 (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1709 * (new_)outty right_par (K_i left_par k_par) *)
1711 add_params menv s context uri tyno
1712 cty outty mty m leftno i in
1714 (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1715 ~metasenv subst infty_pbo context));
1716 let expty_pbo, k = (* k is (K_i left_par k_par) *)
1717 add_params menv s context uri tyno
1718 cty new_outty mty m leftno i in
1720 (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1721 ~metasenv subst expty_pbo context));
1722 let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1724 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1725 ~metasenv subst pbo context));
1726 let (pbo, _), subst, metasenv, ugraph =
1727 coerce_to_something_aux pbo infty_pbo expty_pbo
1728 s menv context ugraph
1731 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1732 ~metasenv subst pbo context));
1733 (i-1, pbo::acc, subst, metasenv, ugraph))
1734 cl pl (List.length pl, [], subst, metasenv, ugraph)
1736 let new_outty = add_pi_for_refl_m new_outty mty m rno in
1738 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1739 ~metasenv subst new_outty context));
1742 let refl_m=Cic.Appl[eq_refl;mty;m]in
1743 Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1745 Cic.MutCase(uri,tyno,new_outty,m,pl)
1747 (t, expty), subst, metasenv, ugraph (*}}}*)
1748 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1749 (*{{{*) debug_print (lazy "LAM");
1751 FreshNamesGenerator.mk_fresh_name
1752 ~subst metasenv context ~typ:src2 Cic.Anonymous
1754 let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1755 (* contravariant part: the argument of f:src->ty *)
1756 let (rel1, _), subst, metasenv, ugraph =
1757 coerce_to_something_aux
1758 (Cic.Rel 1) (CS.lift 1 src2)
1759 (CS.lift 1 src) subst metasenv context_src2 ugraph
1761 (* covariant part: the result of f(c x); x:src2; (c x):src *)
1764 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1765 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1767 (* we fix the possible dependency problem in the source ty *)
1768 let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1769 let (bo, _), subst, metasenv, ugraph =
1770 coerce_to_something_aux
1771 bo ty ty2 subst metasenv context_src2 ugraph
1773 let coerced = Cic.Lambda (name_t,src2, bo) in
1774 (coerced, expty), subst, metasenv, ugraph (*}}}*)
1776 (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1777 ~metasenv subst infty context ^ " ==> " ^
1778 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1779 coerce_atom_to_something
1780 t infty expty subst metasenv context ugraph (*}}}*)
1782 debug_print (lazy ("COERCE TO SOMETHING END: "^
1783 CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1787 coerce_to_something_aux t infty expty subst metasenv context ugraph
1788 with Uncertain _ | RefineFailure _ as exn ->
1791 CicMetaSubst.ppterm_in_context metasenv subst t context ^
1792 " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1793 infty context ^ " but is here used with type " ^
1794 CicMetaSubst.ppterm_in_context metasenv subst expty context)
1796 enrich localization_tbl ~f t exn
1798 and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1799 match CicReduction.whd ~delta:false ~subst context infty with
1800 | Cic.Meta _ | Cic.Sort _ ->
1801 t,infty, subst, metasenv, ugraph
1803 debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1804 ~metasenv subst src context));
1805 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1807 let (t, ty_t), subst, metasenv, ugraph =
1808 coerce_to_something true
1809 localization_tbl t src tgt subst metasenv context ugraph
1811 debug_print (lazy ("COERCE TO SORT END: "^
1812 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1813 t, ty_t, subst, metasenv, ugraph
1814 with HExtlib.Localized (_, exn) ->
1816 lazy ("(7)The term " ^
1817 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1818 ^ " is not a type since it has type " ^
1819 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1820 ^ " that is not a sort")
1822 enrich localization_tbl ~f t exn
1825 (* eat prods ends here! *)
1827 let t',ty,subst',metasenv',ugraph1 =
1828 type_of_aux [] metasenv context t ugraph
1830 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1831 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1832 (* Andrea: ho rimesso qui l'applicazione della subst al
1833 metasenv dopo che ho droppato l'invariante che il metsaenv
1834 e' sempre istanziato *)
1835 let substituted_metasenv =
1836 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1838 (* substituted_t,substituted_ty,substituted_metasenv *)
1839 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1841 if clean_dummy_dependent_types then
1842 FreshNamesGenerator.clean_dummy_dependent_types substituted_t
1843 else substituted_t in
1845 if clean_dummy_dependent_types then
1846 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty
1847 else substituted_ty in
1848 let cleaned_metasenv =
1849 if clean_dummy_dependent_types then
1851 (function (n,context,ty) ->
1852 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1857 | Some (n, Cic.Decl t) ->
1859 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1860 | Some (n, Cic.Def (bo,ty)) ->
1861 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1862 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
1864 Some (n, Cic.Def (bo',ty'))
1868 ) substituted_metasenv
1870 substituted_metasenv
1872 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1875 let undebrujin uri typesno tys t =
1878 (fun (name,_,_,_) (i,t) ->
1879 (* here the explicit_named_substituion is assumed to be *)
1881 let t' = Cic.MutInd (uri,i,[]) in
1882 let t = CicSubstitution.subst t' t in
1884 ) tys (typesno - 1,t))
1886 let map_first_n n start f g l =
1887 let rec aux acc k l =
1890 | [] -> raise (Invalid_argument "map_first_n")
1891 | hd :: tl -> f hd k (aux acc (k+1) tl)
1897 (*CSC: this is a very rough approximation; to be finished *)
1898 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1899 let subst,metasenv,ugraph,tys =
1901 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1902 let subst,metasenv,ugraph,cl =
1904 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1905 let rec aux ctx k subst = function
1906 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1907 let subst,metasenv,ugraph,tl =
1909 (subst,metasenv,ugraph,[])
1910 (fun t n (subst,metasenv,ugraph,acc) ->
1911 let subst,metasenv,ugraph =
1913 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1915 subst,metasenv,ugraph,(t::acc))
1916 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1919 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1920 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1921 subst,metasenv,ugraph,t
1922 | Cic.Prod (name,s,t) ->
1923 let ctx = (Some (name,Cic.Decl s))::ctx in
1924 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1925 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1929 (lazy "not well formed constructor type"))
1931 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1932 subst,metasenv,ugraph,(name,ty) :: acc)
1933 cl (subst,metasenv,ugraph,[])
1935 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1936 tys ([],metasenv,ugraph,[])
1938 let substituted_tys =
1940 (fun (name,ind,arity,cl) ->
1942 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1944 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1947 metasenv,ugraph,substituted_tys
1949 let typecheck metasenv uri obj ~localization_tbl =
1950 let ugraph = CicUniv.oblivion_ugraph in
1952 Cic.Constant (name,Some bo,ty,args,attrs) ->
1953 (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
1954 since type_of_aux' destroys localization information (which are
1955 preserved by type_of_aux *)
1958 Cic.CicHash.find localization_tbl bo
1960 HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
1962 let bo',boty,metasenv,ugraph =
1963 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1964 let ty',_,metasenv,ugraph =
1965 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1966 let subst,metasenv,ugraph =
1968 fo_unif_subst [] [] metasenv boty ty' ugraph
1971 | Uncertain _ as exn ->
1974 CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
1976 CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
1977 " but is here used with type " ^
1978 CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
1982 RefineFailure _ -> RefineFailure msg
1983 | Uncertain _ -> Uncertain msg
1986 raise (HExtlib.Localized (loc exn',exn'))
1988 let bo' = CicMetaSubst.apply_subst subst bo' in
1989 let ty' = CicMetaSubst.apply_subst subst ty' in
1990 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1991 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1992 | Cic.Constant (name,None,ty,args,attrs) ->
1993 let ty',sort,metasenv,ugraph =
1994 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1996 (match CicReduction.whd [] sort with
1998 | Cic.Meta _ -> Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1999 | _ -> raise (RefineFailure (lazy "")))
2000 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
2001 assert (metasenv' = metasenv);
2002 (* Here we do not check the metasenv for correctness *)
2003 let bo',boty,metasenv,ugraph =
2004 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
2005 let ty',sort,metasenv,ugraph =
2006 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
2008 match CicReduction.whd ~delta:true [] sort with
2010 (* instead of raising Uncertain, let's hope that the meta will become
2013 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
2015 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
2016 let bo' = CicMetaSubst.apply_subst subst bo' in
2017 let ty' = CicMetaSubst.apply_subst subst ty' in
2018 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
2019 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
2020 | Cic.Variable _ -> assert false (* not implemented *)
2021 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
2022 (*CSC: this code is greately simplified and many many checks are missing *)
2023 (*CSC: e.g. the constructors are not required to build their own types, *)
2024 (*CSC: the arities are not required to have as type a sort, etc. *)
2025 let uri = match uri with Some uri -> uri | None -> assert false in
2026 let typesno = List.length tys in
2027 (* first phase: we fix only the types *)
2028 let metasenv,ugraph,tys =
2030 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
2031 let ty',_,metasenv,ugraph =
2032 (* clean_dummy_dependent_types: false to avoid cleaning the names
2033 of the left products, that must be identical to those of the
2034 constructors; however, non-left products should probably be
2036 type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl
2037 metasenv [] ty ugraph
2039 metasenv,ugraph,(name,b,ty',cl)::res
2040 ) tys (metasenv,ugraph,[]) in
2042 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
2043 (* second phase: we fix only the constructors *)
2044 let saved_menv = metasenv in
2045 let metasenv,ugraph,tys =
2047 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
2048 let metasenv,ugraph,cl' =
2050 (fun (name,ty) (metasenv,ugraph,res) ->
2052 CicTypeChecker.debrujin_constructor
2053 ~cb:(relocalize localization_tbl) uri typesno [] ty in
2054 let ty',_,metasenv,ugraph =
2055 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
2056 let ty' = undebrujin uri typesno tys ty' in
2057 metasenv@saved_menv,ugraph,(name,ty')::res
2058 ) cl (metasenv,ugraph,[])
2060 metasenv,ugraph,(name,b,ty,cl')::res
2061 ) tys (metasenv,ugraph,[]) in
2062 (* third phase: we check the positivity condition *)
2063 let metasenv,ugraph,tys =
2064 are_all_occurrences_positive metasenv ugraph uri tys paramsno
2066 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
2069 (* sara' piu' veloce che raffinare da zero? mah.... *)
2070 let pack_coercion metasenv ctx t =
2071 let module C = Cic in
2072 let rec merge_coercions ctx =
2073 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
2075 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
2076 | C.Meta (n,subst) ->
2079 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
2082 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
2083 | C.Prod (name,so,dest) ->
2084 let ctx' = (Some (name,C.Decl so))::ctx in
2085 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
2086 | C.Lambda (name,so,dest) ->
2087 let ctx' = (Some (name,C.Decl so))::ctx in
2088 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
2089 | C.LetIn (name,so,ty,dest) ->
2090 let ctx' = Some (name,(C.Def (so,ty)))::ctx in
2092 (name, merge_coercions ctx so, merge_coercions ctx ty,
2093 merge_coercions ctx' dest)
2095 let l = List.map (merge_coercions ctx) l in
2097 let b,_,_,_,_ = is_a_double_coercion t in
2099 let ugraph = CicUniv.oblivion_ugraph in
2100 let old_insert_coercions = !insert_coercions in
2101 insert_coercions := false;
2102 let newt, _, menv, _ =
2104 type_of_aux' metasenv ctx t ugraph
2105 with RefineFailure _ | Uncertain _ ->
2108 insert_coercions := old_insert_coercions;
2109 if metasenv <> [] || menv = [] then
2112 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
2115 | C.Var (uri,exp_named_subst) ->
2116 let exp_named_subst = List.map aux exp_named_subst in
2117 C.Var (uri, exp_named_subst)
2118 | C.Const (uri,exp_named_subst) ->
2119 let exp_named_subst = List.map aux exp_named_subst in
2120 C.Const (uri, exp_named_subst)
2121 | C.MutInd (uri,tyno,exp_named_subst) ->
2122 let exp_named_subst = List.map aux exp_named_subst in
2123 C.MutInd (uri,tyno,exp_named_subst)
2124 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
2125 let exp_named_subst = List.map aux exp_named_subst in
2126 C.MutConstruct (uri,tyno,consno,exp_named_subst)
2127 | C.MutCase (uri,tyno,out,te,pl) ->
2128 let pl = List.map (merge_coercions ctx) pl in
2129 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
2130 | C.Fix (fno, fl) ->
2133 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2138 (fun (name,idx,ty,bo) ->
2139 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
2143 | C.CoFix (fno, fl) ->
2146 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2151 (fun (name,ty,bo) ->
2152 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
2157 merge_coercions ctx t
2160 let pack_coercion_metasenv conjectures = conjectures (*
2162 TASSI: this code war written when coercions were a toy,
2163 now packing coercions involves unification thus
2164 the metasenv may change, and this pack coercion
2165 does not handle that.
2167 let module C = Cic in
2169 (fun (i, ctx, ty) ->
2175 Some (name, C.Decl t) ->
2176 Some (name, C.Decl (pack_coercion conjectures ctx t))
2177 | Some (name, C.Def (t,None)) ->
2178 Some (name,C.Def (pack_coercion conjectures ctx t,None))
2179 | Some (name, C.Def (t,Some ty)) ->
2180 Some (name, C.Def (pack_coercion conjectures ctx t,
2181 Some (pack_coercion conjectures ctx ty)))
2187 ((i,ctx,pack_coercion conjectures ctx ty))
2192 let pack_coercion_obj obj = obj (*
2194 TASSI: this code war written when coercions were a toy,
2195 now packing coercions involves unification thus
2196 the metasenv may change, and this pack coercion
2197 does not handle that.
2199 let module C = Cic in
2201 | C.Constant (id, body, ty, params, attrs) ->
2205 | Some body -> Some (pack_coercion [] [] body)
2207 let ty = pack_coercion [] [] ty in
2208 C.Constant (id, body, ty, params, attrs)
2209 | C.Variable (name, body, ty, params, attrs) ->
2213 | Some body -> Some (pack_coercion [] [] body)
2215 let ty = pack_coercion [] [] ty in
2216 C.Variable (name, body, ty, params, attrs)
2217 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2218 let conjectures = pack_coercion_metasenv conjectures in
2219 let body = pack_coercion conjectures [] body in
2220 let ty = pack_coercion conjectures [] ty in
2221 C.CurrentProof (name, conjectures, body, ty, params, attrs)
2222 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2225 (fun (name, ind, arity, cl) ->
2226 let arity = pack_coercion [] [] arity in
2228 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2230 (name, ind, arity, cl))
2233 C.InductiveDefinition (indtys, params, leftno, attrs) *)
2238 let type_of_aux' metasenv context term =
2241 type_of_aux' metasenv context term in
2243 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2245 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2248 | RefineFailure msg as e ->
2249 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2251 | Uncertain msg as e ->
2252 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2256 let profiler2 = HExtlib.profile "CicRefine"
2258 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2259 profiler2.HExtlib.profile
2260 (type_of_aux' ?localization_tbl metasenv context term) ugraph
2262 let typecheck ~localization_tbl metasenv uri obj =
2263 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2265 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2266 (* vim:set foldmethod=marker: *)