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))
390 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
391 | C.Implicit infos ->
392 let metasenv',t' = exp_impl metasenv subst context infos in
393 type_of_aux subst metasenv' context t' ugraph
395 let ty',_,subst',metasenv',ugraph1 =
396 type_of_aux subst metasenv context ty ugraph
398 let te',inferredty,subst'',metasenv'',ugraph2 =
399 type_of_aux subst' metasenv' context te ugraph1
401 let (te', ty'), subst''',metasenv''',ugraph3 =
402 coerce_to_something true localization_tbl te' inferredty ty'
403 subst'' metasenv'' context ugraph2
405 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
406 | C.Prod (name,s,t) ->
407 let s',sort1,subst',metasenv',ugraph1 =
408 type_of_aux subst metasenv context s ugraph
410 let s',sort1,subst', metasenv',ugraph1 =
411 coerce_to_sort localization_tbl
412 s' sort1 subst' context metasenv' ugraph1
414 let context_for_t = ((Some (name,(C.Decl s')))::context) in
415 let t',sort2,subst'',metasenv'',ugraph2 =
416 type_of_aux subst' metasenv'
417 context_for_t t ugraph1
419 let t',sort2,subst'',metasenv'',ugraph2 =
420 coerce_to_sort localization_tbl
421 t' sort2 subst'' context_for_t metasenv'' ugraph2
423 let sop,subst''',metasenv''',ugraph3 =
424 sort_of_prod localization_tbl subst'' metasenv''
425 context (name,s') t' (sort1,sort2) ugraph2
427 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
428 | C.Lambda (n,s,t) ->
429 let s',sort1,subst',metasenv',ugraph1 =
430 type_of_aux subst metasenv context s ugraph
432 let s',sort1,subst',metasenv',ugraph1 =
433 coerce_to_sort localization_tbl
434 s' sort1 subst' context metasenv' ugraph1
436 let context_for_t = ((Some (n,(C.Decl s')))::context) in
437 let t',type2,subst'',metasenv'',ugraph2 =
438 type_of_aux subst' metasenv' context_for_t t ugraph1
440 C.Lambda (n,s',t'),C.Prod (n,s',type2),
441 subst'',metasenv'',ugraph2
442 | C.LetIn (n,s,ty,t) ->
443 (* only to check if s is well-typed *)
444 let s',ty',subst',metasenv',ugraph1 =
445 type_of_aux subst metasenv context s ugraph in
446 let ty,_,subst',metasenv',ugraph1 =
447 type_of_aux subst' metasenv' context ty ugraph1 in
448 let subst',metasenv',ugraph1 =
450 fo_unif_subst subst' context metasenv'
454 enrich localization_tbl s' exn
457 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
458 context ^ " has type " ^
459 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
460 context ^ " but is here used with type " ^
461 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
464 let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
466 let t',inferredty,subst'',metasenv'',ugraph2 =
467 type_of_aux subst' metasenv'
468 context_for_t t ugraph1
470 (* One-step LetIn reduction.
471 * Even faster than the previous solution.
472 * Moreover the inferred type is closer to the expected one.
474 C.LetIn (n,s',ty,t'),
475 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
476 subst'',metasenv'',ugraph2
477 | C.Appl (he::((_::_) as tl)) ->
478 let he',hetype,subst',metasenv',ugraph1 =
479 type_of_aux subst metasenv context he ugraph
481 let tlbody_and_type,subst'',metasenv'',ugraph2 =
482 typeof_list subst' metasenv' context ugraph1 tl
484 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
485 eat_prods true subst'' metasenv'' context
486 he' hetype tlbody_and_type ugraph2
488 let newappl = (C.Appl (coerced_he::coerced_args)) in
489 avoid_double_coercion
490 context subst''' metasenv''' ugraph3 newappl applty
491 | C.Appl _ -> assert false
492 | C.Const (uri,exp_named_subst) ->
493 let exp_named_subst',subst',metasenv',ugraph1 =
494 check_exp_named_subst subst metasenv context
495 exp_named_subst ugraph in
496 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
498 CicSubstitution.subst_vars exp_named_subst' ty_uri
500 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
501 | C.MutInd (uri,i,exp_named_subst) ->
502 let exp_named_subst',subst',metasenv',ugraph1 =
503 check_exp_named_subst subst metasenv context
504 exp_named_subst ugraph
506 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
508 CicSubstitution.subst_vars exp_named_subst' ty_uri in
509 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
510 | C.MutConstruct (uri,i,j,exp_named_subst) ->
511 let exp_named_subst',subst',metasenv',ugraph1 =
512 check_exp_named_subst subst metasenv context
513 exp_named_subst ugraph
516 type_of_mutual_inductive_constr uri i j ugraph1
519 CicSubstitution.subst_vars exp_named_subst' ty_uri
521 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
523 | C.MutCase (uri, i, outtype, term, pl) ->
524 (* first, get the inductive type (and noparams)
525 * in the environment *)
526 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
527 let _ = CicTypeChecker.typecheck uri in
528 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
530 C.InductiveDefinition (l,expl_params,parsno,_) ->
531 List.nth l i , expl_params, parsno, u
533 enrich localization_tbl t
535 (lazy ("Unkown mutual inductive definition " ^
536 U.string_of_uri uri)))
538 if List.length constructors <> List.length pl then
539 enrich localization_tbl t
541 (lazy "Wrong number of cases")) ;
542 let rec count_prod t =
543 match CicReduction.whd ~subst context t with
544 C.Prod (_, _, t) -> 1 + (count_prod t)
547 let no_args = count_prod arity in
548 (* now, create a "generic" MutInd *)
549 let metasenv,left_args =
550 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
552 let metasenv,right_args =
553 let no_right_params = no_args - no_left_params in
554 if no_right_params < 0 then assert false
555 else CicMkImplicit.n_fresh_metas
556 metasenv subst context no_right_params
558 let metasenv,exp_named_subst =
559 CicMkImplicit.fresh_subst metasenv subst context expl_params in
562 C.MutInd (uri,i,exp_named_subst)
565 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
567 (* check consistency with the actual type of term *)
568 let term',actual_type,subst,metasenv,ugraph1 =
569 type_of_aux subst metasenv context term ugraph in
570 let expected_type',_, subst, metasenv,ugraph2 =
571 type_of_aux subst metasenv context expected_type ugraph1
573 let actual_type = CicReduction.whd ~subst context actual_type in
574 let subst,metasenv,ugraph3 =
576 fo_unif_subst subst context metasenv
577 expected_type' actual_type ugraph2
580 enrich localization_tbl term' exn
583 CicMetaSubst.ppterm_in_context ~metasenv subst term'
584 context ^ " has type " ^
585 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
586 context ^ " but is here used with type " ^
587 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type'
590 let rec instantiate_prod t =
594 match CicReduction.whd ~subst context t with
596 instantiate_prod (CicSubstitution.subst he t') tl
599 let arity_instantiated_with_left_args =
600 instantiate_prod arity left_args in
601 (* TODO: check if the sort elimination
602 * is allowed: [(I q1 ... qr)|B] *)
603 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
605 (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
607 if left_args = [] then
608 (C.MutConstruct (uri,i,j,exp_named_subst))
611 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
613 let p',actual_type,subst,metasenv,ugraph1 =
614 type_of_aux subst metasenv context p ugraph
616 let constructor',expected_type, subst, metasenv,ugraph2 =
617 type_of_aux subst metasenv context constructor ugraph1
619 let outtypeinstance,subst,metasenv,ugraph3 =
621 check_branch 0 context metasenv subst
622 no_left_params actual_type constructor' expected_type
626 enrich localization_tbl constructor'
629 CicMetaSubst.ppterm_in_context metasenv subst p'
630 context ^ " has type " ^
631 CicMetaSubst.ppterm_in_context metasenv subst actual_type
632 context ^ " but is here used with type " ^
633 CicMetaSubst.ppterm_in_context metasenv subst expected_type
637 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
638 pl ([],List.length pl,[],subst,metasenv,ugraph3)
641 (* we are left to check that the outype matches his instances.
642 The easy case is when the outype is specified, that amount
643 to a trivial check. Otherwise, we should guess a type from
647 let outtype,outtypety, subst, metasenv,ugraph4 =
648 type_of_aux subst metasenv context outtype ugraph4 in
651 (let candidate,ugraph5,metasenv,subst =
652 let exp_name_subst, metasenv =
654 CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
656 let uris = CicUtil.params_of_obj o in
658 fun uri (acc,metasenv) ->
659 let metasenv',new_meta =
660 CicMkImplicit.mk_implicit metasenv subst context
663 CicMkImplicit.identity_relocation_list_for_metavariable
666 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
670 match left_args,right_args with
671 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
673 let rec mk_right_args =
676 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
678 let right_args_no = List.length right_args in
679 let lifted_left_args =
680 List.map (CicSubstitution.lift right_args_no) left_args
682 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
683 (lifted_left_args @ mk_right_args right_args_no))
686 FreshNamesGenerator.mk_fresh_name ~subst metasenv
687 context Cic.Anonymous ~typ:ty
689 match outtypeinstances with
691 let extended_context =
692 let rec add_right_args =
694 Cic.Prod (name,ty,t) ->
695 Some (name,Cic.Decl ty)::(add_right_args t)
698 (Some (fresh_name,Cic.Decl ty))::
700 (add_right_args arity_instantiated_with_left_args))@
703 let metasenv,new_meta =
704 CicMkImplicit.mk_implicit metasenv subst extended_context
707 CicMkImplicit.identity_relocation_list_for_metavariable
710 let rec add_lambdas b =
712 Cic.Prod (name,ty,t) ->
713 Cic.Lambda (name,ty,(add_lambdas b t))
714 | _ -> Cic.Lambda (fresh_name, ty, b)
717 add_lambdas (Cic.Meta (new_meta,irl))
718 arity_instantiated_with_left_args
720 (Some candidate),ugraph4,metasenv,subst
721 | (constructor_args_no,_,instance,_)::tl ->
723 let instance',subst,metasenv =
724 CicMetaSubst.delift_rels subst metasenv
725 constructor_args_no instance
727 let candidate,ugraph,metasenv,subst =
729 fun (candidate_oty,ugraph,metasenv,subst)
730 (constructor_args_no,_,instance,_) ->
731 match candidate_oty with
732 | None -> None,ugraph,metasenv,subst
735 let instance',subst,metasenv =
736 CicMetaSubst.delift_rels subst metasenv
737 constructor_args_no instance
739 let subst,metasenv,ugraph =
740 fo_unif_subst subst context metasenv
743 candidate_oty,ugraph,metasenv,subst
745 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
746 | RefineFailure _ | Uncertain _ ->
747 None,ugraph,metasenv,subst
748 ) (Some instance',ugraph4,metasenv,subst) tl
751 | None -> None, ugraph,metasenv,subst
753 let rec add_lambdas n b =
755 Cic.Prod (name,ty,t) ->
756 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
758 Cic.Lambda (fresh_name, ty,
759 CicSubstitution.lift (n + 1) t)
762 (add_lambdas 0 t arity_instantiated_with_left_args),
763 ugraph,metasenv,subst
764 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
765 None,ugraph4,metasenv,subst
768 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
770 let subst,metasenv,ugraph =
772 fo_unif_subst subst context metasenv
773 candidate outtype ugraph5
775 exn -> assert false(* unification against a metavariable *)
777 C.MutCase (uri, i, outtype, term', pl'),
778 CicReduction.head_beta_reduce
779 (CicMetaSubst.apply_subst subst
780 (Cic.Appl (outtype::right_args@[term']))),
781 subst,metasenv,ugraph)
782 | _ -> (* easy case *)
783 let tlbody_and_type,subst,metasenv,ugraph4 =
784 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
786 let _,_,_,subst,metasenv,ugraph4 =
787 eat_prods false subst metasenv context
788 outtype outtypety tlbody_and_type ugraph4
790 let _,_, subst, metasenv,ugraph5 =
791 type_of_aux subst metasenv context
792 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
794 let (subst,metasenv,ugraph6) =
796 (fun (subst,metasenv,ugraph)
797 p (constructor_args_no,context,instance,args)
802 CicSubstitution.lift constructor_args_no outtype
804 C.Appl (outtype'::args)
806 CicReduction.head_beta_reduce ~delta:false
807 ~upto:(List.length args) appl
810 fo_unif_subst subst context metasenv instance instance'
814 enrich localization_tbl p exn
817 CicMetaSubst.ppterm_in_context ~metasenv subst p
818 context ^ " has type " ^
819 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
820 context ^ " but is here used with type " ^
821 CicMetaSubst.ppterm_in_context ~metasenv subst instance
823 (subst,metasenv,ugraph5) pl' outtypeinstances
825 C.MutCase (uri, i, outtype, term', pl'),
826 CicReduction.head_beta_reduce
827 (CicMetaSubst.apply_subst subst
828 (C.Appl(outtype::right_args@[term']))),
829 subst,metasenv,ugraph6)
831 let fl_ty',subst,metasenv,types,ugraph1,len =
833 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
834 let ty',_,subst',metasenv',ugraph1 =
835 type_of_aux subst metasenv context ty ugraph
837 fl @ [ty'],subst',metasenv',
838 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
839 :: types, ugraph, len+1
840 ) ([],subst,metasenv,[],ugraph,0) fl
842 let context' = types@context in
843 let fl_bo',subst,metasenv,ugraph2 =
845 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
846 let bo',ty_of_bo,subst,metasenv,ugraph1 =
847 type_of_aux subst metasenv context' bo ugraph in
848 let expected_ty = CicSubstitution.lift len ty in
849 let subst',metasenv',ugraph' =
851 fo_unif_subst subst context' metasenv
852 ty_of_bo expected_ty ugraph1
855 enrich localization_tbl bo exn
858 CicMetaSubst.ppterm_in_context ~metasenv subst bo
859 context' ^ " has type " ^
860 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
861 context' ^ " but is here used with type " ^
862 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
865 fl @ [bo'] , subst',metasenv',ugraph'
866 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
868 let ty = List.nth fl_ty' i in
869 (* now we have the new ty in fl_ty', the new bo in fl_bo',
870 * and we want the new fl with bo' and ty' injected in the right
873 let rec map3 f l1 l2 l3 =
876 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
879 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
882 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
884 let fl_ty',subst,metasenv,types,ugraph1,len =
886 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
887 let ty',_,subst',metasenv',ugraph1 =
888 type_of_aux subst metasenv context ty ugraph
890 fl @ [ty'],subst',metasenv',
891 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
892 types, ugraph1, len+1
893 ) ([],subst,metasenv,[],ugraph,0) fl
895 let context' = types@context in
896 let fl_bo',subst,metasenv,ugraph2 =
898 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
899 let bo',ty_of_bo,subst,metasenv,ugraph1 =
900 type_of_aux subst metasenv context' bo ugraph in
901 let expected_ty = CicSubstitution.lift len ty in
902 let subst',metasenv',ugraph' =
904 fo_unif_subst subst context' metasenv
905 ty_of_bo expected_ty ugraph1
908 enrich localization_tbl bo exn
911 CicMetaSubst.ppterm_in_context ~metasenv subst bo
912 context' ^ " has type " ^
913 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
914 context' ^ " but is here used with type " ^
915 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
918 fl @ [bo'],subst',metasenv',ugraph'
919 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
921 let ty = List.nth fl_ty' i in
922 (* now we have the new ty in fl_ty', the new bo in fl_bo',
923 * and we want the new fl with bo' and ty' injected in the right
926 let rec map3 f l1 l2 l3 =
929 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
932 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
935 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
937 relocalize localization_tbl t t';
940 (* check_metasenv_consistency checks that the "canonical" context of a
941 metavariable is consitent - up to relocation via the relocation list l -
942 with the actual context *)
943 and check_metasenv_consistency
944 metano subst metasenv context canonical_context l ugraph
946 let module C = Cic in
947 let module R = CicReduction in
948 let module S = CicSubstitution in
949 let lifted_canonical_context =
953 | (Some (n,C.Decl t))::tl ->
954 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
955 | None::tl -> None::(aux (i+1) tl)
956 | (Some (n,C.Def (t,ty)))::tl ->
960 (S.subst_meta l (S.lift i t),
961 S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
963 aux 1 canonical_context
967 (fun (l,subst,metasenv,ugraph) t ct ->
970 l @ [None],subst,metasenv,ugraph
971 | Some t,Some (_,C.Def (ct,_)) ->
972 (*CSC: the following optimization is to avoid a possibly
973 expensive reduction that can be easily avoided and
974 that is quite frequent. However, this is better
975 handled using levels to control reduction *)
980 match List.nth context (n - 1) with
981 Some (_,C.Def (te,_)) -> S.lift n te
987 let subst',metasenv',ugraph' =
989 (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
990 * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
991 fo_unif_subst subst context metasenv optimized_t ct ugraph
992 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))))))
994 l @ [Some t],subst',metasenv',ugraph'
995 | Some t,Some (_,C.Decl ct) ->
996 let t',inferredty,subst',metasenv',ugraph1 =
997 type_of_aux subst metasenv context t ugraph
999 let subst'',metasenv'',ugraph2 =
1002 subst' context metasenv' inferredty ct ugraph1
1003 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))))))
1005 l @ [Some t'], subst'',metasenv'',ugraph2
1007 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
1009 Invalid_argument _ ->
1013 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1014 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1015 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1017 and check_exp_named_subst metasubst metasenv context tl ugraph =
1018 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1020 [] -> [],metasubst,metasenv,ugraph
1022 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1024 CicSubstitution.subst_vars substs ty_uri in
1025 (* CSC: why was this code here? it is wrong
1026 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1027 Cic.Variable (_,Some bo,_,_) ->
1029 (RefineFailure (lazy
1030 "A variable with a body can not be explicit substituted"))
1031 | Cic.Variable (_,None,_,_) -> ()
1034 (RefineFailure (lazy
1035 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1038 let t',typeoft,metasubst',metasenv',ugraph2 =
1039 type_of_aux metasubst metasenv context t ugraph1 in
1040 let subst = uri,t' in
1041 let metasubst'',metasenv'',ugraph3 =
1044 metasubst' context metasenv' typeoft typeofvar ugraph2
1046 raise (RefineFailure (lazy
1047 ("Wrong Explicit Named Substitution: " ^
1048 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1049 " not unifiable with " ^
1050 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1052 (* FIXME: no mere tail recursive! *)
1053 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1054 check_exp_named_subst_aux
1055 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1057 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1059 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1062 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1065 let module C = Cic in
1066 let context_for_t2 = (Some (name,C.Decl s))::context in
1067 let t1'' = CicReduction.whd ~subst context t1 in
1068 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1069 match (t1'', t2'') with
1070 | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) ->
1071 (* different than Coq manual!!! *)
1072 C.Sort s2,subst,metasenv,ugraph
1073 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1074 let t' = CicUniv.fresh() in
1076 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1077 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1078 C.Sort (C.Type t'),subst,metasenv,ugraph2
1080 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1081 | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
1082 let t' = CicUniv.fresh() in
1084 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1085 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1086 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1088 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1089 | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
1090 let t' = CicUniv.fresh() in
1092 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1093 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1094 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1096 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1097 | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
1098 let t' = CicUniv.fresh() in
1100 let ugraph1 = CicUniv.add_gt t' t1 ugraph in
1101 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1102 C.Sort (C.Type t'),subst,metasenv,ugraph2
1104 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1105 | (C.Sort _,C.Sort (C.Type t1)) ->
1106 C.Sort (C.Type t1),subst,metasenv,ugraph
1107 | (C.Sort _,C.Sort (C.CProp t1)) ->
1108 C.Sort (C.CProp t1),subst,metasenv,ugraph
1109 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1110 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1111 (* TODO how can we force the meta to become a sort? If we don't we
1112 * break the invariant that refine produce only well typed terms *)
1113 (* TODO if we check the non meta term and if it is a sort then we
1114 * are likely to know the exact value of the result e.g. if the rhs
1115 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1116 let (metasenv,idx) =
1117 CicMkImplicit.mk_implicit_sort metasenv subst in
1118 let (subst, metasenv,ugraph1) =
1120 fo_unif_subst subst context_for_t2 metasenv
1121 (C.Meta (idx,[])) t2'' ugraph
1122 with _ -> assert false (* unification against a metavariable *)
1124 t2'',subst,metasenv,ugraph1
1127 enrich localization_tbl s
1131 "%s is supposed to be a type, but its type is %s"
1132 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1133 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1135 enrich localization_tbl t
1139 "%s is supposed to be a type, but its type is %s"
1140 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1141 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1143 and avoid_double_coercion context subst metasenv ugraph t ty =
1144 if not !pack_coercions then
1145 t,ty,subst,metasenv,ugraph
1147 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1149 let source_carr = CoercGraph.source_of c2 in
1150 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1151 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1153 | CoercGraph.SomeCoercion candidates ->
1155 HExtlib.list_findopt
1156 (function (metasenv,last,c) ->
1158 | c when not (CoercGraph.is_composite c) ->
1159 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1162 let subst,metasenv,ugraph =
1163 fo_unif_subst subst context metasenv last head ugraph in
1164 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1169 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1170 let newt,_,subst,metasenv,ugraph =
1171 type_of_aux subst metasenv context c ugraph in
1172 debug_print (lazy "tipa...");
1173 let subst, metasenv, ugraph =
1174 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1175 fo_unif_subst subst context metasenv newt t ugraph
1177 debug_print (lazy "unifica...");
1178 Some (newt, ty, subst, metasenv, ugraph)
1180 | RefineFailure s | Uncertain s when not !pack_coercions->
1181 debug_print s; debug_print (lazy "stop\n");None
1182 | RefineFailure s | Uncertain s ->
1183 debug_print s;debug_print (lazy "goon\n");
1185 let old_pack_coercions = !pack_coercions in
1186 pack_coercions := false; (* to avoid diverging *)
1187 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1188 type_of_aux subst metasenv context c1_c2_implicit ugraph
1190 pack_coercions := old_pack_coercions;
1192 is_a_double_coercion refined_c1_c2_implicit
1198 match refined_c1_c2_implicit with
1199 | Cic.Appl l -> HExtlib.list_last l
1202 let subst, metasenv, ugraph =
1203 try fo_unif_subst subst context metasenv
1205 with RefineFailure s| Uncertain s->
1206 debug_print s;assert false
1208 let subst, metasenv, ugraph =
1209 fo_unif_subst subst context metasenv
1210 refined_c1_c2_implicit t ugraph
1212 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1214 | RefineFailure s | Uncertain s ->
1215 pack_coercions := true;debug_print s;None
1216 | exn -> pack_coercions := true; raise exn))
1219 (match selected with
1223 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1224 t, ty, subst, metasenv, ugraph)
1225 | _ -> t, ty, subst, metasenv, ugraph)
1227 t, ty, subst, metasenv, ugraph
1229 and typeof_list subst metasenv context ugraph l =
1230 let tlbody_and_type,subst,metasenv,ugraph =
1232 (fun x (res,subst,metasenv,ugraph) ->
1233 let x',ty,subst',metasenv',ugraph1 =
1234 type_of_aux subst metasenv context x ugraph
1236 (x', ty)::res,subst',metasenv',ugraph1
1237 ) l ([],subst,metasenv,ugraph)
1239 tlbody_and_type,subst,metasenv,ugraph
1242 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1244 (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1245 let fix_arity n metasenv context subst he hetype ugraph =
1246 let hetype = CicMetaSubst.apply_subst subst hetype in
1247 let src = CoercDb.coerc_carr_of_term hetype 0 in
1248 let tgt = CoercDb.coerc_carr_of_term (Cic.Implicit None) 1 in
1249 match CoercGraph.look_for_coercion' metasenv subst context src tgt with
1250 | CoercGraph.NoCoercion -> []
1251 | CoercGraph.NotHandled ->
1252 raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1253 | CoercGraph.SomeCoercionToTgt candidates
1254 | CoercGraph.SomeCoercion candidates ->
1256 (fun (metasenv,last,coerc) ->
1258 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1260 let subst,metasenv,ugraph =
1261 fo_unif_subst subst context metasenv last he ugraph in
1262 debug_print (lazy ("New head: "^ pp coerc));
1264 CicTypeChecker.type_of_aux' ~subst metasenv context coerc
1267 debug_print (lazy (" has type: "^ pp tty));
1268 Some (coerc,tty,subst,metasenv,ugraph)
1270 | Uncertain _ | RefineFailure _
1271 | HExtlib.Localized (_,Uncertain _)
1272 | HExtlib.Localized (_,RefineFailure _) -> None
1273 | exn -> assert false)
1276 (* aux function to process the type of the head and the args in parallel *)
1277 let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1279 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1280 | (hete, hety)::tl as args ->
1281 match (CicReduction.whd ~subst context hetype) with
1282 | Cic.Prod (n,s,t) ->
1283 let arg,subst,metasenv,ugraph =
1284 coerce_to_something allow_coercions localization_tbl
1285 hete hety s subst metasenv context ugraph in
1287 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1288 ugraph (newargs@[arg]) tl
1291 match he, newargs with
1293 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1294 | _ -> Cic.Appl (he::List.map fst newargs)
1296 (*{{{*) debug_print (lazy
1298 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1299 "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1300 "\n but is applyed to: " ^ String.concat ";"
1301 (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1302 let possible_fixes =
1303 fix_arity (List.length args) metasenv context subst he hetype
1306 HExtlib.list_findopt
1307 (fun (he,hetype,subst,metasenv,ugraph) ->
1308 (* {{{ *)debug_print (lazy ("Try fix: "^
1309 CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1310 debug_print (lazy (" of type: "^
1311 CicMetaSubst.ppterm_in_context
1312 ~metasenv subst hetype context)); (* }}} *)
1314 Some (eat_prods_and_args
1315 metasenv subst context he hetype ugraph [] args)
1317 | RefineFailure _ | Uncertain _
1318 | HExtlib.Localized (_,RefineFailure _)
1319 | HExtlib.Localized (_,Uncertain _) -> None)
1325 (MoreArgsThanExpected
1326 (List.length args, RefineFailure (lazy "")))
1328 (* first we check if we are in the simple case of a meta closed term *)
1329 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1330 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1331 (* this optimization is to postpone fix_arity (the most common case)*)
1332 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1334 (* this (says CSC) is also useful to infer dependent types *)
1335 let pristinemenv = metasenv in
1336 let metasenv,hetype' =
1337 mk_prod_of_metas metasenv context subst args_bo_and_ty
1340 let subst,metasenv,ugraph =
1341 fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1343 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1344 with RefineFailure _ | Uncertain _ ->
1345 subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1347 let coerced_args,subst,metasenv,he,t,ugraph =
1350 metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1352 MoreArgsThanExpected (residuals,exn) ->
1353 more_args_than_expected localization_tbl metasenv
1354 subst he context hetype' residuals args_bo_and_ty exn
1356 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1358 and coerce_to_something
1359 allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1361 let module CS = CicSubstitution in
1362 let module CR = CicReduction in
1363 let cs_subst = CS.subst ~avoid_beta_redexes:true in
1364 let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1365 debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1367 CoercGraph.look_for_coercion metasenv subst context infty expty
1370 | CoercGraph.NoCoercion
1371 | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy
1372 "coerce_atom_to_something fails since no coercions found"))
1373 | CoercGraph.NotHandled when
1374 not (CicUtil.is_meta_closed infty) ||
1375 not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy
1376 "coerce_atom_to_something fails since carriers have metas"))
1377 | CoercGraph.NotHandled -> raise (RefineFailure (lazy
1378 "coerce_atom_to_something fails since no coercions found"))
1379 | CoercGraph.SomeCoercion candidates ->
1380 debug_print (lazy (string_of_int (List.length candidates) ^
1381 " candidates found"));
1382 let uncertain = ref false in
1386 (fun (metasenv,last,c) ->
1388 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1389 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1391 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
1392 "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
1394 debug_print (lazy ("FO_UNIF_SUBST: " ^
1395 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1396 let subst,metasenv,ugraph =
1397 fo_unif_subst subst context metasenv last t ugraph
1399 let newt,newhety,subst,metasenv,ugraph =
1400 type_of_aux subst metasenv context c ugraph in
1401 let newt, newty, subst, metasenv, ugraph =
1402 avoid_double_coercion context subst metasenv ugraph newt expty
1404 let subst,metasenv,ugraph =
1405 fo_unif_subst subst context metasenv newhety expty ugraph in
1406 Some ((newt,newty), subst, metasenv, ugraph)
1408 | Uncertain _ -> uncertain := true; None
1409 | RefineFailure _ -> None)
1414 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1422 | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1423 | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1425 let rec coerce_to_something_aux
1426 t infty expty subst metasenv context ugraph
1429 let subst, metasenv, ugraph =
1430 fo_unif_subst subst context metasenv infty expty ugraph
1432 (t, expty), subst, metasenv, ugraph
1433 with (Uncertain _ | RefineFailure _ as exn)
1434 when allow_coercions && !insert_coercions ->
1435 let whd = CicReduction.whd ~delta:false in
1436 let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1437 let infty = clean infty subst context in
1438 let expty = clean expty subst context in
1439 let t = clean t subst context in
1440 (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1441 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1442 CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1443 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1444 let (coerced,_),subst,metasenv,_ as result =
1445 match infty, expty, t with
1446 | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1447 (*{{{*) debug_print (lazy "FIX");
1449 [name,i,_(* infty *),bo] ->
1451 Some (Cic.Name name,Cic.Decl expty)::context in
1452 let (rel1, _), subst, metasenv, ugraph =
1453 coerce_to_something_aux (Cic.Rel 1)
1454 (CS.lift 1 expty) (CS.lift 1 infty) subst
1455 metasenv context_bo ugraph in
1456 let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1457 let (bo,_), subst, metasenv, ugraph =
1458 coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1460 metasenv context_bo ugraph
1462 (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1463 | _ -> assert false (* not implemented yet *)) (*}}}*)
1464 | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1465 (*{{{*) debug_print (lazy "CASE");
1466 (* {{{ helper functions *)
1467 let get_cl_and_left_p uri tyno outty ugraph =
1468 match CicEnvironment.get_obj ugraph uri with
1469 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1472 match CicReduction.whd ~delta:false ctx t with
1473 | Cic.Prod (name,src,tgt) ->
1474 let ctx = Some (name, Cic.Decl src) :: ctx in
1480 let rec skip_lambda_delifting t n =
1483 | Cic.Lambda (_,_,t),n ->
1484 skip_lambda_delifting
1485 (CS.subst (Cic.Implicit None) t) (n - 1)
1488 let get_l_r_p n = function
1489 | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1490 | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1491 HExtlib.split_nth n args
1494 let _, _, ty, cl = List.nth tl tyno in
1495 let pis = count_pis ty in
1496 let rno = pis - leftno in
1497 let t = skip_lambda_delifting outty rno in
1498 let left_p, _ = get_l_r_p leftno t in
1499 let instantiale_with_left cl =
1503 (fun t p -> match t with
1504 | Cic.Prod (_,_,t) ->
1510 let cl = instantiale_with_left (List.map snd cl) in
1511 cl, left_p, leftno, rno, ugraph
1514 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1517 let rec mkr n = function
1518 | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1521 CicReplace.replace_lifting
1522 ~equality:(fun _ -> CicUtil.alpha_equivalence)
1524 ~what:(matched::right_p)
1525 ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1529 | Cic.Lambda (name, src, tgt),_ ->
1530 Cic.Lambda (name, src,
1531 keep_lambdas_and_put_expty
1532 (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1533 (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1536 let eq_uri, eq, eq_refl =
1537 match LibraryObjects.eq_URI () with
1538 | None -> HLog.warn "no default equality"; raise exn
1539 | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1542 metasenv subst context uri tyno cty outty mty m leftno i
1544 let rec aux context outty par k mty m = function
1545 | Cic.Prod (name, src, tgt) ->
1548 (Some (name, Cic.Decl src) :: context)
1549 (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1550 (CS.lift 1 mty) (CS.lift 1 m) tgt
1552 Cic.Prod (name, src, t), k
1555 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1556 if par <> [] then Cic.Appl (k::par) else k
1558 Cic.Prod (Cic.Name "p",
1559 Cic.Appl [eq; mty; m; k],
1561 (CR.head_beta_reduce ~delta:false
1562 (Cic.Appl [outty;k])))),k
1563 | Cic.Appl (Cic.MutInd _::pl) ->
1564 let left_p,right_p = HExtlib.split_nth leftno pl in
1565 let has_rights = right_p <> [] in
1567 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1568 Cic.Appl (k::left_p@par)
1572 CicTypeChecker.type_of_aux' ~subst metasenv context k
1573 CicUniv.oblivion_ugraph
1575 | Cic.Appl (Cic.MutInd _::args),_ ->
1576 snd (HExtlib.split_nth leftno args)
1578 with CicTypeChecker.TypeCheckerFailure _-> assert false
1581 CR.head_beta_reduce ~delta:false
1582 (Cic.Appl (outty ::right_p @ [k])),k
1584 Cic.Prod (Cic.Name "p",
1585 Cic.Appl [eq; mty; m; k],
1587 (CR.head_beta_reduce ~delta:false
1588 (Cic.Appl (outty ::right_p @ [k]))))),k
1591 aux context outty [] 1 mty m cty
1593 let add_lambda_for_refl_m pbo rno mty m k cty =
1594 (* k lives in the right context *)
1595 if rno <> 0 then pbo else
1596 let rec aux mty m = function
1597 | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1598 Cic.Lambda (name,src,
1599 (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1601 Cic.Lambda (Cic.Name "p",
1602 Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1606 let add_pi_for_refl_m new_outty mty m rno =
1607 if rno <> 0 then new_outty else
1608 let rec aux m mty = function
1609 | Cic.Lambda (name, src, tgt) ->
1610 Cic.Lambda (name, src,
1611 aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1614 (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1618 in (* }}} end helper functions *)
1619 (* constructors types with left params already instantiated *)
1620 let outty = CicMetaSubst.apply_subst subst outty in
1621 let cl, left_p, leftno,rno,ugraph =
1622 get_cl_and_left_p uri tyno outty ugraph
1627 CicTypeChecker.type_of_aux' ~subst metasenv context m
1628 CicUniv.oblivion_ugraph
1630 | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty
1631 | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
1632 snd (HExtlib.split_nth leftno args), mty
1634 with CicTypeChecker.TypeCheckerFailure _ ->
1635 raise (AssertFailure(lazy "already ill-typed matched term"))
1638 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1641 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1642 ~metasenv subst new_outty context));
1643 let _,pl,subst,metasenv,ugraph =
1645 (fun cty pbo (i, acc, s, menv, ugraph) ->
1646 (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1647 * (new_)outty right_par (K_i left_par k_par) *)
1649 add_params menv s context uri tyno
1650 cty outty mty m leftno i in
1652 (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1653 ~metasenv subst infty_pbo context));
1654 let expty_pbo, k = (* k is (K_i left_par k_par) *)
1655 add_params menv s context uri tyno
1656 cty new_outty mty m leftno i in
1658 (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1659 ~metasenv subst expty_pbo context));
1660 let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1662 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1663 ~metasenv subst pbo context));
1664 let (pbo, _), subst, metasenv, ugraph =
1665 coerce_to_something_aux pbo infty_pbo expty_pbo
1666 s menv context ugraph
1669 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1670 ~metasenv subst pbo context));
1671 (i-1, pbo::acc, subst, metasenv, ugraph))
1672 cl pl (List.length pl, [], subst, metasenv, ugraph)
1674 let new_outty = add_pi_for_refl_m new_outty mty m rno in
1676 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1677 ~metasenv subst new_outty context));
1680 let refl_m=Cic.Appl[eq_refl;mty;m]in
1681 Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1683 Cic.MutCase(uri,tyno,new_outty,m,pl)
1685 (t, expty), subst, metasenv, ugraph (*}}}*)
1686 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1687 (*{{{*) debug_print (lazy "LAM");
1689 FreshNamesGenerator.mk_fresh_name
1690 ~subst metasenv context ~typ:src2 Cic.Anonymous
1692 let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1693 (* contravariant part: the argument of f:src->ty *)
1694 let (rel1, _), subst, metasenv, ugraph =
1695 coerce_to_something_aux
1696 (Cic.Rel 1) (CS.lift 1 src2)
1697 (CS.lift 1 src) subst metasenv context_src2 ugraph
1699 (* covariant part: the result of f(c x); x:src2; (c x):src *)
1702 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1703 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1705 (* we fix the possible dependency problem in the source ty *)
1706 let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1707 let (bo, _), subst, metasenv, ugraph =
1708 coerce_to_something_aux
1709 bo ty ty2 subst metasenv context_src2 ugraph
1711 let coerced = Cic.Lambda (name_t,src2, bo) in
1712 (coerced, expty), subst, metasenv, ugraph (*}}}*)
1714 (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1715 ~metasenv subst infty context ^ " ==> " ^
1716 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1717 coerce_atom_to_something
1718 t infty expty subst metasenv context ugraph (*}}}*)
1720 debug_print (lazy ("COERCE TO SOMETHING END: "^
1721 CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1725 coerce_to_something_aux t infty expty subst metasenv context ugraph
1726 with Uncertain _ | RefineFailure _ as exn ->
1729 CicMetaSubst.ppterm_in_context metasenv subst t context ^
1730 " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1731 infty context ^ " but is here used with type " ^
1732 CicMetaSubst.ppterm_in_context metasenv subst expty context)
1734 enrich localization_tbl ~f t exn
1736 and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1737 match CicReduction.whd ~delta:false ~subst context infty with
1738 | Cic.Meta _ | Cic.Sort _ ->
1739 t,infty, subst, metasenv, ugraph
1741 debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1742 ~metasenv subst src context));
1743 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1745 let (t, ty_t), subst, metasenv, ugraph =
1746 coerce_to_something true
1747 localization_tbl t src tgt subst metasenv context ugraph
1749 debug_print (lazy ("COERCE TO SORT END: "^
1750 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1751 t, ty_t, subst, metasenv, ugraph
1752 with HExtlib.Localized (_, exn) ->
1754 lazy ("(7)The term " ^
1755 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1756 ^ " is not a type since it has type " ^
1757 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1758 ^ " that is not a sort")
1760 enrich localization_tbl ~f t exn
1763 (* eat prods ends here! *)
1765 let t',ty,subst',metasenv',ugraph1 =
1766 type_of_aux [] metasenv context t ugraph
1768 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1769 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1770 (* Andrea: ho rimesso qui l'applicazione della subst al
1771 metasenv dopo che ho droppato l'invariante che il metsaenv
1772 e' sempre istanziato *)
1773 let substituted_metasenv =
1774 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1776 (* substituted_t,substituted_ty,substituted_metasenv *)
1777 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1779 if clean_dummy_dependent_types then
1780 FreshNamesGenerator.clean_dummy_dependent_types substituted_t
1781 else substituted_t in
1783 if clean_dummy_dependent_types then
1784 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty
1785 else substituted_ty in
1786 let cleaned_metasenv =
1787 if clean_dummy_dependent_types then
1789 (function (n,context,ty) ->
1790 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1795 | Some (n, Cic.Decl t) ->
1797 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1798 | Some (n, Cic.Def (bo,ty)) ->
1799 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1800 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
1802 Some (n, Cic.Def (bo',ty'))
1806 ) substituted_metasenv
1808 substituted_metasenv
1810 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1813 let undebrujin uri typesno tys t =
1816 (fun (name,_,_,_) (i,t) ->
1817 (* here the explicit_named_substituion is assumed to be *)
1819 let t' = Cic.MutInd (uri,i,[]) in
1820 let t = CicSubstitution.subst t' t in
1822 ) tys (typesno - 1,t))
1824 let map_first_n n start f g l =
1825 let rec aux acc k l =
1828 | [] -> raise (Invalid_argument "map_first_n")
1829 | hd :: tl -> f hd k (aux acc (k+1) tl)
1835 (*CSC: this is a very rough approximation; to be finished *)
1836 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1837 let subst,metasenv,ugraph,tys =
1839 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1840 let subst,metasenv,ugraph,cl =
1842 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1843 let rec aux ctx k subst = function
1844 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1845 let subst,metasenv,ugraph,tl =
1847 (subst,metasenv,ugraph,[])
1848 (fun t n (subst,metasenv,ugraph,acc) ->
1849 let subst,metasenv,ugraph =
1851 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1853 subst,metasenv,ugraph,(t::acc))
1854 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1857 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1858 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1859 subst,metasenv,ugraph,t
1860 | Cic.Prod (name,s,t) ->
1861 let ctx = (Some (name,Cic.Decl s))::ctx in
1862 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1863 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1867 (lazy "not well formed constructor type"))
1869 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1870 subst,metasenv,ugraph,(name,ty) :: acc)
1871 cl (subst,metasenv,ugraph,[])
1873 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1874 tys ([],metasenv,ugraph,[])
1876 let substituted_tys =
1878 (fun (name,ind,arity,cl) ->
1880 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1882 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1885 metasenv,ugraph,substituted_tys
1887 let typecheck metasenv uri obj ~localization_tbl =
1888 let ugraph = CicUniv.oblivion_ugraph in
1890 Cic.Constant (name,Some bo,ty,args,attrs) ->
1891 (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
1892 since type_of_aux' destroys localization information (which are
1893 preserved by type_of_aux *)
1896 Cic.CicHash.find localization_tbl bo
1898 HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
1900 let bo',boty,metasenv,ugraph =
1901 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1902 let ty',_,metasenv,ugraph =
1903 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1904 let subst,metasenv,ugraph =
1906 fo_unif_subst [] [] metasenv boty ty' ugraph
1909 | Uncertain _ as exn ->
1912 CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
1914 CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
1915 " but is here used with type " ^
1916 CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
1920 RefineFailure _ -> RefineFailure msg
1921 | Uncertain _ -> Uncertain msg
1924 raise (HExtlib.Localized (loc exn',exn'))
1926 let bo' = CicMetaSubst.apply_subst subst bo' in
1927 let ty' = CicMetaSubst.apply_subst subst ty' in
1928 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1929 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1930 | Cic.Constant (name,None,ty,args,attrs) ->
1931 let ty',_,metasenv,ugraph =
1932 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1934 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1935 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1936 assert (metasenv' = metasenv);
1937 (* Here we do not check the metasenv for correctness *)
1938 let bo',boty,metasenv,ugraph =
1939 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1940 let ty',sort,metasenv,ugraph =
1941 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1945 (* instead of raising Uncertain, let's hope that the meta will become
1948 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1950 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1951 let bo' = CicMetaSubst.apply_subst subst bo' in
1952 let ty' = CicMetaSubst.apply_subst subst ty' in
1953 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1954 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1955 | Cic.Variable _ -> assert false (* not implemented *)
1956 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1957 (*CSC: this code is greately simplified and many many checks are missing *)
1958 (*CSC: e.g. the constructors are not required to build their own types, *)
1959 (*CSC: the arities are not required to have as type a sort, etc. *)
1960 let uri = match uri with Some uri -> uri | None -> assert false in
1961 let typesno = List.length tys in
1962 (* first phase: we fix only the types *)
1963 let metasenv,ugraph,tys =
1965 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1966 let ty',_,metasenv,ugraph =
1967 (* clean_dummy_dependent_types: false to avoid cleaning the names
1968 of the left products, that must be identical to those of the
1969 constructors; however, non-left products should probably be
1971 type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl
1972 metasenv [] ty ugraph
1974 metasenv,ugraph,(name,b,ty',cl)::res
1975 ) tys (metasenv,ugraph,[]) in
1977 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1978 (* second phase: we fix only the constructors *)
1979 let saved_menv = metasenv in
1980 let metasenv,ugraph,tys =
1982 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1983 let metasenv,ugraph,cl' =
1985 (fun (name,ty) (metasenv,ugraph,res) ->
1987 CicTypeChecker.debrujin_constructor
1988 ~cb:(relocalize localization_tbl) uri typesno [] ty in
1989 let ty',_,metasenv,ugraph =
1990 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1991 let ty' = undebrujin uri typesno tys ty' in
1992 metasenv@saved_menv,ugraph,(name,ty')::res
1993 ) cl (metasenv,ugraph,[])
1995 metasenv,ugraph,(name,b,ty,cl')::res
1996 ) tys (metasenv,ugraph,[]) in
1997 (* third phase: we check the positivity condition *)
1998 let metasenv,ugraph,tys =
1999 are_all_occurrences_positive metasenv ugraph uri tys paramsno
2001 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
2004 (* sara' piu' veloce che raffinare da zero? mah.... *)
2005 let pack_coercion metasenv ctx t =
2006 let module C = Cic in
2007 let rec merge_coercions ctx =
2008 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
2010 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
2011 | C.Meta (n,subst) ->
2014 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
2017 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
2018 | C.Prod (name,so,dest) ->
2019 let ctx' = (Some (name,C.Decl so))::ctx in
2020 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
2021 | C.Lambda (name,so,dest) ->
2022 let ctx' = (Some (name,C.Decl so))::ctx in
2023 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
2024 | C.LetIn (name,so,ty,dest) ->
2025 let ctx' = Some (name,(C.Def (so,ty)))::ctx in
2027 (name, merge_coercions ctx so, merge_coercions ctx ty,
2028 merge_coercions ctx' dest)
2030 let l = List.map (merge_coercions ctx) l in
2032 let b,_,_,_,_ = is_a_double_coercion t in
2034 let ugraph = CicUniv.oblivion_ugraph in
2035 let old_insert_coercions = !insert_coercions in
2036 insert_coercions := false;
2037 let newt, _, menv, _ =
2039 type_of_aux' metasenv ctx t ugraph
2040 with RefineFailure _ | Uncertain _ ->
2043 insert_coercions := old_insert_coercions;
2044 if metasenv <> [] || menv = [] then
2047 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
2050 | C.Var (uri,exp_named_subst) ->
2051 let exp_named_subst = List.map aux exp_named_subst in
2052 C.Var (uri, exp_named_subst)
2053 | C.Const (uri,exp_named_subst) ->
2054 let exp_named_subst = List.map aux exp_named_subst in
2055 C.Const (uri, exp_named_subst)
2056 | C.MutInd (uri,tyno,exp_named_subst) ->
2057 let exp_named_subst = List.map aux exp_named_subst in
2058 C.MutInd (uri,tyno,exp_named_subst)
2059 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
2060 let exp_named_subst = List.map aux exp_named_subst in
2061 C.MutConstruct (uri,tyno,consno,exp_named_subst)
2062 | C.MutCase (uri,tyno,out,te,pl) ->
2063 let pl = List.map (merge_coercions ctx) pl in
2064 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
2065 | C.Fix (fno, fl) ->
2068 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2073 (fun (name,idx,ty,bo) ->
2074 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
2078 | C.CoFix (fno, fl) ->
2081 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2086 (fun (name,ty,bo) ->
2087 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
2092 merge_coercions ctx t
2095 let pack_coercion_metasenv conjectures = conjectures (*
2097 TASSI: this code war written when coercions were a toy,
2098 now packing coercions involves unification thus
2099 the metasenv may change, and this pack coercion
2100 does not handle that.
2102 let module C = Cic in
2104 (fun (i, ctx, ty) ->
2110 Some (name, C.Decl t) ->
2111 Some (name, C.Decl (pack_coercion conjectures ctx t))
2112 | Some (name, C.Def (t,None)) ->
2113 Some (name,C.Def (pack_coercion conjectures ctx t,None))
2114 | Some (name, C.Def (t,Some ty)) ->
2115 Some (name, C.Def (pack_coercion conjectures ctx t,
2116 Some (pack_coercion conjectures ctx ty)))
2122 ((i,ctx,pack_coercion conjectures ctx ty))
2127 let pack_coercion_obj obj = obj (*
2129 TASSI: this code war written when coercions were a toy,
2130 now packing coercions involves unification thus
2131 the metasenv may change, and this pack coercion
2132 does not handle that.
2134 let module C = Cic in
2136 | C.Constant (id, body, ty, params, attrs) ->
2140 | Some body -> Some (pack_coercion [] [] body)
2142 let ty = pack_coercion [] [] ty in
2143 C.Constant (id, body, ty, params, attrs)
2144 | C.Variable (name, body, ty, params, attrs) ->
2148 | Some body -> Some (pack_coercion [] [] body)
2150 let ty = pack_coercion [] [] ty in
2151 C.Variable (name, body, ty, params, attrs)
2152 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2153 let conjectures = pack_coercion_metasenv conjectures in
2154 let body = pack_coercion conjectures [] body in
2155 let ty = pack_coercion conjectures [] ty in
2156 C.CurrentProof (name, conjectures, body, ty, params, attrs)
2157 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2160 (fun (name, ind, arity, cl) ->
2161 let arity = pack_coercion [] [] arity in
2163 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2165 (name, ind, arity, cl))
2168 C.InductiveDefinition (indtys, params, leftno, attrs) *)
2173 let type_of_aux' metasenv context term =
2176 type_of_aux' metasenv context term in
2178 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2180 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2183 | RefineFailure msg as e ->
2184 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2186 | Uncertain msg as e ->
2187 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2191 let profiler2 = HExtlib.profile "CicRefine"
2193 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2194 profiler2.HExtlib.profile
2195 (type_of_aux' ?localization_tbl metasenv context term) ugraph
2197 let typecheck ~localization_tbl metasenv uri obj =
2198 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2200 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2201 (* vim:set foldmethod=marker: *)