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 let insert_coercions = ref true
36 let debug_print = fun _ -> ()
38 let profiler = HExtlib.profile "CicRefine.fo_unif"
40 let fo_unif_subst subst context metasenv t1 t2 ugraph =
43 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
44 in profiler.HExtlib.profile foo ()
46 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
47 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
50 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
53 RefineFailure msg -> RefineFailure (f msg)
54 | Uncertain msg -> Uncertain (f msg)
55 | _ -> assert false in
58 Cic.CicHash.find localization_tbl t
60 prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
63 raise (HExtlib.Localized (loc,exn'))
65 let relocalize localization_tbl oldt newt =
67 let infos = Cic.CicHash.find localization_tbl oldt in
68 Cic.CicHash.remove localization_tbl oldt;
69 Cic.CicHash.add localization_tbl newt infos;
77 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
78 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
81 let exp_impl metasenv subst context =
84 let (metasenv', idx) =
85 CicMkImplicit.mk_implicit_type metasenv subst context in
87 CicMkImplicit.identity_relocation_list_for_metavariable context in
88 metasenv', Cic.Meta (idx, irl)
90 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
91 metasenv', Cic.Meta (idx, [])
93 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
95 CicMkImplicit.identity_relocation_list_for_metavariable context in
96 metasenv', Cic.Meta (idx, irl)
100 let is_a_double_coercion t =
102 let rec aux = function
110 false, Cic.Implicit None, Cic.Implicit None, Cic.Implicit None
113 | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 ->
114 (match last_of tl with
115 | Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
116 let head = last_of tl2 in
121 let avoid_double_coercion context subst metasenv ugraph t ty =
124 let ty,_=CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in
125 let rec count_pi = function
126 | Cic.Prod (_,_,t) -> 1 + count_pi t
130 with Invalid_argument _ -> assert false (* all coercions have an uri *)
132 let rec mk_implicits tail = function
134 | n -> Cic.Implicit None :: mk_implicits tail (n-1)
136 let b, c1, c2, head = is_a_double_coercion t in
138 let source_carr = CoercGraph.source_of c2 in
139 let tgt_carr = CicMetaSubst.apply_subst subst ty in
140 (match CoercGraph.look_for_coercion source_carr tgt_carr
142 | CoercGraph.SomeCoercion c ->
143 let arity = arity_of c in
144 let args = mk_implicits head (arity - 1) in
145 let c_bo = CicUtil.term_of_uri (CicUtil.uri_of_term c) in
146 let newt = Cic.Appl (c_bo::args) in
147 let subst, metasenv, ugraph =
148 CicUnification.fo_unif_subst subst context metasenv newt t ugraph
153 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm (Cic.Appl (c::args))));
154 Cic.Appl (c::args), ty, subst, metasenv, ugraph
155 | _ -> assert false) (* the composite coercion must exist *)
157 t, ty, subst, metasenv, ugraph
159 let rec type_of_constant uri ugraph =
160 let module C = Cic in
161 let module R = CicReduction in
162 let module U = UriManager in
163 let _ = CicTypeChecker.typecheck uri in
166 CicEnvironment.get_cooked_obj ugraph uri
167 with Not_found -> assert false
170 C.Constant (_,_,ty,_,_) -> ty,u
171 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
175 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
177 and type_of_variable uri ugraph =
178 let module C = Cic in
179 let module R = CicReduction in
180 let module U = UriManager in
181 let _ = CicTypeChecker.typecheck uri in
184 CicEnvironment.get_cooked_obj ugraph uri
185 with Not_found -> assert false
188 C.Variable (_,_,ty,_,_) -> ty,u
192 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
194 and type_of_mutual_inductive_defs uri i ugraph =
195 let module C = Cic in
196 let module R = CicReduction in
197 let module U = UriManager in
198 let _ = CicTypeChecker.typecheck uri in
201 CicEnvironment.get_cooked_obj ugraph uri
202 with Not_found -> assert false
205 C.InductiveDefinition (dl,_,_,_) ->
206 let (_,_,arity,_) = List.nth dl i in
211 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
213 and type_of_mutual_inductive_constr uri i j ugraph =
214 let module C = Cic in
215 let module R = CicReduction in
216 let module U = UriManager in
217 let _ = CicTypeChecker.typecheck uri in
220 CicEnvironment.get_cooked_obj ugraph uri
221 with Not_found -> assert false
224 C.InductiveDefinition (dl,_,_,_) ->
225 let (_,_,_,cl) = List.nth dl i in
226 let (_,ty) = List.nth cl (j-1) in
232 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
235 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
237 (* the check_branch function checks if a branch of a case is refinable.
238 It returns a pair (outype_instance,args), a subst and a metasenv.
239 outype_instance is the expected result of applying the case outtype
241 The problem is that outype is in general unknown, and we should
242 try to synthesize it from the above information, that is in general
243 a second order unification problem. *)
245 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
246 let module C = Cic in
247 (* let module R = CicMetaSubst in *)
248 let module R = CicReduction in
249 match R.whd ~subst context expectedtype with
251 (n,context,actualtype, [term]), subst, metasenv, ugraph
252 | C.Appl (C.MutInd (_,_,_)::tl) ->
253 let (_,arguments) = split tl left_args_no in
254 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
255 | C.Prod (name,so,de) ->
256 (* we expect that the actual type of the branch has the due
258 (match R.whd ~subst context actualtype with
259 C.Prod (name',so',de') ->
260 let subst, metasenv, ugraph1 =
261 fo_unif_subst subst context metasenv so so' ugraph in
263 (match CicSubstitution.lift 1 term with
264 C.Appl l -> C.Appl (l@[C.Rel 1])
265 | t -> C.Appl [t ; C.Rel 1]) in
266 (* we should also check that the name variable is anonymous in
267 the actual type de' ?? *)
269 ((Some (name,(C.Decl so)))::context)
270 metasenv subst left_args_no de' term' de ugraph1
271 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
272 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
274 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
277 let rec type_of_aux subst metasenv context t ugraph =
278 let module C = Cic in
279 let module S = CicSubstitution in
280 let module U = UriManager in
281 let (t',_,_,_,_) as res =
286 match List.nth context (n - 1) with
287 Some (_,C.Decl ty) ->
288 t,S.lift n ty,subst,metasenv, ugraph
289 | Some (_,C.Def (_,Some ty)) ->
290 t,S.lift n ty,subst,metasenv, ugraph
291 | Some (_,C.Def (bo,None)) ->
293 (* if it is in the context it must be already well-typed*)
294 CicTypeChecker.type_of_aux' ~subst metasenv context
297 t,ty,subst,metasenv,ugraph
299 enrich localization_tbl t
300 (RefineFailure (lazy "Rel to hidden hypothesis"))
303 enrich localization_tbl t
304 (RefineFailure (lazy "Not a close term")))
305 | C.Var (uri,exp_named_subst) ->
306 let exp_named_subst',subst',metasenv',ugraph1 =
307 check_exp_named_subst
308 subst metasenv context exp_named_subst ugraph
310 let ty_uri,ugraph1 = type_of_variable uri ugraph in
312 CicSubstitution.subst_vars exp_named_subst' ty_uri
314 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
317 let (canonical_context, term,ty) =
318 CicUtil.lookup_subst n subst
320 let l',subst',metasenv',ugraph1 =
321 check_metasenv_consistency n subst metasenv context
322 canonical_context l ugraph
324 (* trust or check ??? *)
325 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
326 subst', metasenv', ugraph1
327 (* type_of_aux subst metasenv
328 context (CicSubstitution.subst_meta l term) *)
329 with CicUtil.Subst_not_found _ ->
330 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
331 let l',subst',metasenv', ugraph1 =
332 check_metasenv_consistency n subst metasenv context
333 canonical_context l ugraph
335 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
336 subst', metasenv',ugraph1)
337 | C.Sort (C.Type tno) ->
338 let tno' = CicUniv.fresh() in
339 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
340 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
342 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
343 | C.Implicit infos ->
344 let metasenv',t' = exp_impl metasenv subst context infos in
345 type_of_aux subst metasenv' context t' ugraph
347 let ty',_,subst',metasenv',ugraph1 =
348 type_of_aux subst metasenv context ty ugraph
350 let te',inferredty,subst'',metasenv'',ugraph2 =
351 type_of_aux subst' metasenv' context te ugraph1
354 let subst''',metasenv''',ugraph3 =
355 fo_unif_subst subst'' context metasenv''
356 inferredty ty' ugraph2
358 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
361 enrich localization_tbl te'
364 CicMetaSubst.ppterm_in_context subst'' te'
365 context ^ " has type " ^
366 CicMetaSubst.ppterm_in_context subst'' inferredty
367 context ^ " but is here used with type " ^
368 CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
370 | C.Prod (name,s,t) ->
371 let carr t subst context = CicMetaSubst.apply_subst subst t in
372 let coerce_to_sort in_source tgt_sort t type_to_coerce
373 subst context metasenv uragph
375 if not !insert_coercions then
376 t,type_to_coerce,subst,metasenv,ugraph
378 let coercion_src = carr type_to_coerce subst context in
379 match coercion_src with
381 t,type_to_coerce,subst,metasenv,ugraph
382 | Cic.Meta _ as meta ->
383 t, meta, subst, metasenv, ugraph
384 | Cic.Cast _ as cast ->
385 t, cast, subst, metasenv, ugraph
387 let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
388 let search = CoercGraph.look_for_coercion in
389 let boh = search coercion_src coercion_tgt in
391 | CoercGraph.NoCoercion
392 | CoercGraph.NotHandled _ ->
393 enrich localization_tbl t
396 CicMetaSubst.ppterm_in_context subst t context ^
397 " is not a type since it has type " ^
398 CicMetaSubst.ppterm_in_context
399 subst coercion_src context ^ " that is not a sort")))
400 | CoercGraph.NotMetaClosed ->
401 enrich localization_tbl t
404 CicMetaSubst.ppterm_in_context subst t context ^
405 " is not a type since it has type " ^
406 CicMetaSubst.ppterm_in_context
407 subst coercion_src context ^ " that is not a sort")))
408 | CoercGraph.SomeCoercion c ->
409 let newt, tty, subst, metasenv, ugraph =
410 avoid_double_coercion context
411 subst metasenv ugraph
412 (Cic.Appl[c;t]) coercion_tgt
414 newt, tty, subst, metasenv, ugraph)
416 let s',sort1,subst',metasenv',ugraph1 =
417 type_of_aux subst metasenv context s ugraph
419 let s',sort1,subst', metasenv',ugraph1 =
420 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
421 s' sort1 subst' context metasenv' ugraph1
423 let context_for_t = ((Some (name,(C.Decl s')))::context) in
424 let t',sort2,subst'',metasenv'',ugraph2 =
425 type_of_aux subst' metasenv'
426 context_for_t t ugraph1
428 let t',sort2,subst'',metasenv'',ugraph2 =
429 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
430 t' sort2 subst'' context_for_t metasenv'' ugraph2
432 let sop,subst''',metasenv''',ugraph3 =
433 sort_of_prod subst'' metasenv''
434 context (name,s') (sort1,sort2) ugraph2
436 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
437 | C.Lambda (n,s,t) ->
439 let s',sort1,subst',metasenv',ugraph1 =
440 type_of_aux subst metasenv context s ugraph in
441 let s',sort1,subst',metasenv',ugraph1 =
442 if not !insert_coercions then
443 s',sort1, subst', metasenv', ugraph1
445 match CicReduction.whd ~subst:subst' context sort1 with
446 | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
448 let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
449 let search = CoercGraph.look_for_coercion in
450 let boh = search coercion_src coercion_tgt in
452 | CoercGraph.SomeCoercion c ->
453 let newt, tty, subst', metasenv', ugraph1 =
454 avoid_double_coercion context
455 subst' metasenv' ugraph1
456 (Cic.Appl[c;s']) coercion_tgt
458 newt, tty, subst', metasenv', ugraph1
459 | CoercGraph.NoCoercion
460 | CoercGraph.NotHandled _ ->
461 enrich localization_tbl s'
464 CicMetaSubst.ppterm_in_context subst s' context ^
465 " is not a type since it has type " ^
466 CicMetaSubst.ppterm_in_context
467 subst coercion_src context ^ " that is not a sort")))
468 | CoercGraph.NotMetaClosed ->
469 enrich localization_tbl s'
472 CicMetaSubst.ppterm_in_context subst s' context ^
473 " is not a type since it has type " ^
474 CicMetaSubst.ppterm_in_context
475 subst coercion_src context ^ " that is not a sort")))
477 let context_for_t = ((Some (n,(C.Decl s')))::context) in
478 let t',type2,subst'',metasenv'',ugraph2 =
479 type_of_aux subst' metasenv' context_for_t t ugraph1
481 C.Lambda (n,s',t'),C.Prod (n,s',type2),
482 subst'',metasenv'',ugraph2
484 (* only to check if s is well-typed *)
485 let s',ty,subst',metasenv',ugraph1 =
486 type_of_aux subst metasenv context s ugraph
488 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
490 let t',inferredty,subst'',metasenv'',ugraph2 =
491 type_of_aux subst' metasenv'
492 context_for_t t ugraph1
494 (* One-step LetIn reduction.
495 * Even faster than the previous solution.
496 * Moreover the inferred type is closer to the expected one.
498 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
499 subst'',metasenv'',ugraph2
500 | C.Appl (he::((_::_) as tl)) ->
501 let he',hetype,subst',metasenv',ugraph1 =
502 type_of_aux subst metasenv context he ugraph
504 let tlbody_and_type,subst'',metasenv'',ugraph2 =
506 (fun x (res,subst,metasenv,ugraph) ->
507 let x',ty,subst',metasenv',ugraph1 =
508 type_of_aux subst metasenv context x ugraph
510 (x', ty)::res,subst',metasenv',ugraph1
511 ) tl ([],subst',metasenv',ugraph1)
513 let tl',applty,subst''',metasenv''',ugraph3 =
514 eat_prods true subst'' metasenv'' context
515 hetype tlbody_and_type ugraph2
517 avoid_double_coercion context
518 subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
519 | C.Appl _ -> assert false
520 | C.Const (uri,exp_named_subst) ->
521 let exp_named_subst',subst',metasenv',ugraph1 =
522 check_exp_named_subst subst metasenv context
523 exp_named_subst ugraph in
524 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
526 CicSubstitution.subst_vars exp_named_subst' ty_uri
528 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
529 | C.MutInd (uri,i,exp_named_subst) ->
530 let exp_named_subst',subst',metasenv',ugraph1 =
531 check_exp_named_subst subst metasenv context
532 exp_named_subst ugraph
534 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
536 CicSubstitution.subst_vars exp_named_subst' ty_uri in
537 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
538 | C.MutConstruct (uri,i,j,exp_named_subst) ->
539 let exp_named_subst',subst',metasenv',ugraph1 =
540 check_exp_named_subst subst metasenv context
541 exp_named_subst ugraph
544 type_of_mutual_inductive_constr uri i j ugraph1
547 CicSubstitution.subst_vars exp_named_subst' ty_uri
549 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
551 | C.MutCase (uri, i, outtype, term, pl) ->
552 (* first, get the inductive type (and noparams)
553 * in the environment *)
554 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
555 let _ = CicTypeChecker.typecheck uri in
556 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
558 C.InductiveDefinition (l,expl_params,parsno,_) ->
559 List.nth l i , expl_params, parsno, u
561 enrich localization_tbl t
563 (lazy ("Unkown mutual inductive definition " ^
564 U.string_of_uri uri)))
566 let rec count_prod t =
567 match CicReduction.whd ~subst context t with
568 C.Prod (_, _, t) -> 1 + (count_prod t)
571 let no_args = count_prod arity in
572 (* now, create a "generic" MutInd *)
573 let metasenv,left_args =
574 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
576 let metasenv,right_args =
577 let no_right_params = no_args - no_left_params in
578 if no_right_params < 0 then assert false
579 else CicMkImplicit.n_fresh_metas
580 metasenv subst context no_right_params
582 let metasenv,exp_named_subst =
583 CicMkImplicit.fresh_subst metasenv subst context expl_params in
586 C.MutInd (uri,i,exp_named_subst)
589 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
591 (* check consistency with the actual type of term *)
592 let term',actual_type,subst,metasenv,ugraph1 =
593 type_of_aux subst metasenv context term ugraph in
594 let expected_type',_, subst, metasenv,ugraph2 =
595 type_of_aux subst metasenv context expected_type ugraph1
597 let actual_type = CicReduction.whd ~subst context actual_type in
598 let subst,metasenv,ugraph3 =
600 fo_unif_subst subst context metasenv
601 expected_type' actual_type ugraph2
604 enrich localization_tbl term' exn
607 CicMetaSubst.ppterm_in_context subst term'
608 context ^ " has type " ^
609 CicMetaSubst.ppterm_in_context subst actual_type
610 context ^ " but is here used with type " ^
611 CicMetaSubst.ppterm_in_context subst expected_type' context))
613 let rec instantiate_prod t =
617 match CicReduction.whd ~subst context t with
619 instantiate_prod (CicSubstitution.subst he t') tl
622 let arity_instantiated_with_left_args =
623 instantiate_prod arity left_args in
624 (* TODO: check if the sort elimination
625 * is allowed: [(I q1 ... qr)|B] *)
626 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
628 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
630 if left_args = [] then
631 (C.MutConstruct (uri,i,j,exp_named_subst))
634 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
636 let p',actual_type,subst,metasenv,ugraph1 =
637 type_of_aux subst metasenv context p ugraph
639 let constructor',expected_type, subst, metasenv,ugraph2 =
640 type_of_aux subst metasenv context constructor ugraph1
642 let outtypeinstance,subst,metasenv,ugraph3 =
643 check_branch 0 context metasenv subst no_left_params
644 actual_type constructor' expected_type ugraph2
647 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
648 ([],1,[],subst,metasenv,ugraph3) pl
651 (* we are left to check that the outype matches his instances.
652 The easy case is when the outype is specified, that amount
653 to a trivial check. Otherwise, we should guess a type from
657 let outtype,outtypety, subst, metasenv,ugraph4 =
658 type_of_aux subst metasenv context outtype ugraph4 in
661 (let candidate,ugraph5,metasenv,subst =
662 let exp_name_subst, metasenv =
664 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
666 let uris = CicUtil.params_of_obj o in
668 fun uri (acc,metasenv) ->
669 let metasenv',new_meta =
670 CicMkImplicit.mk_implicit metasenv subst context
673 CicMkImplicit.identity_relocation_list_for_metavariable
676 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
680 match left_args,right_args with
681 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
683 let rec mk_right_args =
686 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
688 let right_args_no = List.length right_args in
689 let lifted_left_args =
690 List.map (CicSubstitution.lift right_args_no) left_args
692 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
693 (lifted_left_args @ mk_right_args right_args_no))
696 FreshNamesGenerator.mk_fresh_name ~subst metasenv
697 context Cic.Anonymous ~typ:ty
699 match outtypeinstances with
701 let extended_context =
702 let rec add_right_args =
704 Cic.Prod (name,ty,t) ->
705 Some (name,Cic.Decl ty)::(add_right_args t)
708 (Some (fresh_name,Cic.Decl ty))::
710 (add_right_args arity_instantiated_with_left_args))@
713 let metasenv,new_meta =
714 CicMkImplicit.mk_implicit metasenv subst extended_context
717 CicMkImplicit.identity_relocation_list_for_metavariable
720 let rec add_lambdas b =
722 Cic.Prod (name,ty,t) ->
723 Cic.Lambda (name,ty,(add_lambdas b t))
724 | _ -> Cic.Lambda (fresh_name, ty, b)
727 add_lambdas (Cic.Meta (new_meta,irl))
728 arity_instantiated_with_left_args
730 (Some candidate),ugraph4,metasenv,subst
731 | (constructor_args_no,_,instance,_)::tl ->
733 let instance',subst,metasenv =
734 CicMetaSubst.delift_rels subst metasenv
735 constructor_args_no instance
737 let candidate,ugraph,metasenv,subst =
739 fun (candidate_oty,ugraph,metasenv,subst)
740 (constructor_args_no,_,instance,_) ->
741 match candidate_oty with
742 | None -> None,ugraph,metasenv,subst
745 let instance',subst,metasenv =
746 CicMetaSubst.delift_rels subst metasenv
747 constructor_args_no instance
749 let subst,metasenv,ugraph =
750 fo_unif_subst subst context metasenv
753 candidate_oty,ugraph,metasenv,subst
755 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
756 | CicUnification.UnificationFailure _
757 | CicUnification.Uncertain _ ->
758 None,ugraph,metasenv,subst
759 ) (Some instance',ugraph4,metasenv,subst) tl
762 | None -> None, ugraph,metasenv,subst
764 let rec add_lambdas n b =
766 Cic.Prod (name,ty,t) ->
767 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
769 Cic.Lambda (fresh_name, ty,
770 CicSubstitution.lift (n + 1) t)
773 (add_lambdas 0 t arity_instantiated_with_left_args),
774 ugraph,metasenv,subst
775 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
776 None,ugraph4,metasenv,subst
779 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
781 let subst,metasenv,ugraph =
782 fo_unif_subst subst context metasenv
783 candidate outtype ugraph5
785 C.MutCase (uri, i, outtype, term', pl'),
786 CicReduction.head_beta_reduce
787 (CicMetaSubst.apply_subst subst
788 (Cic.Appl (outtype::right_args@[term']))),
789 subst,metasenv,ugraph)
790 | _ -> (* easy case *)
791 let tlbody_and_type,subst,metasenv,ugraph4 =
793 (fun x (res,subst,metasenv,ugraph) ->
794 let x',ty,subst',metasenv',ugraph1 =
795 type_of_aux subst metasenv context x ugraph
797 (x', ty)::res,subst',metasenv',ugraph1
798 ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
800 let _,_,subst,metasenv,ugraph4 =
801 eat_prods false subst metasenv context
802 outtypety tlbody_and_type ugraph4
804 let _,_, subst, metasenv,ugraph5 =
805 type_of_aux subst metasenv context
806 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
808 let (subst,metasenv,ugraph6) =
810 (fun (subst,metasenv,ugraph)
811 (constructor_args_no,context,instance,args) ->
815 CicSubstitution.lift constructor_args_no outtype
817 C.Appl (outtype'::args)
819 CicReduction.whd ~subst context appl
821 fo_unif_subst subst context metasenv
822 instance instance' ugraph)
823 (subst,metasenv,ugraph5) 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 =
833 (fun (fl,subst,metasenv,types,ugraph) (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 ty')) :: types, ugraph
839 ) ([],subst,metasenv,[],ugraph) fl
841 let len = List.length types in
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
849 let subst',metasenv',ugraph' =
850 fo_unif_subst subst context' metasenv
851 ty_of_bo (CicSubstitution.lift len ty) ugraph1
853 fl @ [bo'] , subst',metasenv',ugraph'
854 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
856 let ty = List.nth fl_ty' i in
857 (* now we have the new ty in fl_ty', the new bo in fl_bo',
858 * and we want the new fl with bo' and ty' injected in the right
861 let rec map3 f l1 l2 l3 =
864 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
867 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
870 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
872 let fl_ty',subst,metasenv,types,ugraph1 =
874 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
875 let ty',_,subst',metasenv',ugraph1 =
876 type_of_aux subst metasenv context ty ugraph
878 fl @ [ty'],subst',metasenv',
879 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
880 ) ([],subst,metasenv,[],ugraph) fl
882 let len = List.length types in
883 let context' = types@context in
884 let fl_bo',subst,metasenv,ugraph2 =
886 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
887 let bo',ty_of_bo,subst,metasenv,ugraph1 =
888 type_of_aux subst metasenv context' bo ugraph
890 let subst',metasenv',ugraph' =
891 fo_unif_subst subst context' metasenv
892 ty_of_bo (CicSubstitution.lift len ty) ugraph1
894 fl @ [bo'],subst',metasenv',ugraph'
895 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
897 let ty = List.nth fl_ty' i in
898 (* now we have the new ty in fl_ty', the new bo in fl_bo',
899 * and we want the new fl with bo' and ty' injected in the right
902 let rec map3 f l1 l2 l3 =
905 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
908 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
911 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
913 relocalize localization_tbl t t';
916 (* check_metasenv_consistency checks that the "canonical" context of a
917 metavariable is consitent - up to relocation via the relocation list l -
918 with the actual context *)
919 and check_metasenv_consistency
920 metano subst metasenv context canonical_context l ugraph
922 let module C = Cic in
923 let module R = CicReduction in
924 let module S = CicSubstitution in
925 let lifted_canonical_context =
929 | (Some (n,C.Decl t))::tl ->
930 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
931 | (Some (n,C.Def (t,None)))::tl ->
932 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
933 | None::tl -> None::(aux (i+1) tl)
934 | (Some (n,C.Def (t,Some ty)))::tl ->
936 C.Def ((S.subst_meta l (S.lift i t)),
937 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
939 aux 1 canonical_context
943 (fun (l,subst,metasenv,ugraph) t ct ->
946 l @ [None],subst,metasenv,ugraph
947 | Some t,Some (_,C.Def (ct,_)) ->
948 let subst',metasenv',ugraph' =
950 fo_unif_subst subst context metasenv t ct ugraph
951 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 subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
953 l @ [Some t],subst',metasenv',ugraph'
954 | Some t,Some (_,C.Decl ct) ->
955 let t',inferredty,subst',metasenv',ugraph1 =
956 type_of_aux subst metasenv context t ugraph
958 let subst'',metasenv'',ugraph2 =
961 subst' context metasenv' inferredty ct ugraph1
962 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 subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
964 l @ [Some t'], subst'',metasenv'',ugraph2
966 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 subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
968 Invalid_argument _ ->
972 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
973 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
974 (CicMetaSubst.ppcontext subst canonical_context))))
976 and check_exp_named_subst metasubst metasenv context tl ugraph =
977 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
979 [] -> [],metasubst,metasenv,ugraph
981 let ty_uri,ugraph1 = type_of_variable uri ugraph in
983 CicSubstitution.subst_vars substs ty_uri in
984 (* CSC: why was this code here? it is wrong
985 (match CicEnvironment.get_cooked_obj ~trust:false uri with
986 Cic.Variable (_,Some bo,_,_) ->
989 "A variable with a body can not be explicit substituted"))
990 | Cic.Variable (_,None,_,_) -> ()
994 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
997 let t',typeoft,metasubst',metasenv',ugraph2 =
998 type_of_aux metasubst metasenv context t ugraph1 in
999 let subst = uri,t' in
1000 let metasubst'',metasenv'',ugraph3 =
1003 metasubst' context metasenv' typeoft typeofvar ugraph2
1005 raise (RefineFailure (lazy
1006 ("Wrong Explicit Named Substitution: " ^
1007 CicMetaSubst.ppterm metasubst' typeoft ^
1008 " not unifiable with " ^
1009 CicMetaSubst.ppterm metasubst' typeofvar)))
1011 (* FIXME: no mere tail recursive! *)
1012 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1013 check_exp_named_subst_aux
1014 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1016 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1018 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1021 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
1022 let module C = Cic in
1023 let context_for_t2 = (Some (name,C.Decl s))::context in
1024 let t1'' = CicReduction.whd ~subst context t1 in
1025 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1026 match (t1'', t2'') with
1027 (C.Sort s1, C.Sort s2)
1028 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1029 (* different than Coq manual!!! *)
1030 C.Sort s2,subst,metasenv,ugraph
1031 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1032 let t' = CicUniv.fresh() in
1033 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1034 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1035 C.Sort (C.Type t'),subst,metasenv,ugraph2
1036 | (C.Sort _,C.Sort (C.Type t1)) ->
1037 C.Sort (C.Type t1),subst,metasenv,ugraph
1038 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1039 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1040 (* TODO how can we force the meta to become a sort? If we don't we
1041 * brake the invariant that refine produce only well typed terms *)
1042 (* TODO if we check the non meta term and if it is a sort then we
1043 * are likely to know the exact value of the result e.g. if the rhs
1044 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1045 let (metasenv,idx) =
1046 CicMkImplicit.mk_implicit_sort metasenv subst in
1047 let (subst, metasenv,ugraph1) =
1048 fo_unif_subst subst context_for_t2 metasenv
1049 (C.Meta (idx,[])) t2'' ugraph
1051 t2'',subst,metasenv,ugraph1
1057 ("Two sorts were expected, found %s " ^^
1058 "(that reduces to %s) and %s (that reduces to %s)")
1059 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
1060 (CicPp.ppterm t2''))))
1063 allow_coercions subst metasenv context hetype tlbody_and_type ugraph
1065 let rec mk_prod metasenv context' =
1068 let (metasenv, idx) =
1069 CicMkImplicit.mk_implicit_type metasenv subst context'
1072 CicMkImplicit.identity_relocation_list_for_metavariable context'
1074 metasenv,Cic.Meta (idx, irl)
1076 let (metasenv, idx) =
1077 CicMkImplicit.mk_implicit_type metasenv subst context'
1080 CicMkImplicit.identity_relocation_list_for_metavariable context'
1082 let meta = Cic.Meta (idx,irl) in
1084 (* The name must be fresh for context. *)
1085 (* Nevertheless, argty is well-typed only in context. *)
1086 (* Thus I generate a name (name_hint) in context and *)
1087 (* then I generate a name --- using the hint name_hint *)
1088 (* --- that is fresh in context'. *)
1090 (* Cic.Name "pippo" *)
1091 FreshNamesGenerator.mk_fresh_name ~subst metasenv
1092 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
1093 (CicMetaSubst.apply_subst_context subst context)
1095 ~typ:(CicMetaSubst.apply_subst subst argty)
1097 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
1098 FreshNamesGenerator.mk_fresh_name ~subst
1099 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
1101 let metasenv,target =
1102 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
1104 metasenv,Cic.Prod (name,meta,target)
1106 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
1107 let (subst, metasenv,ugraph1) =
1109 fo_unif_subst subst context metasenv hetype hetype' ugraph
1112 (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
1113 (CicPp.ppterm hetype)
1114 (CicPp.ppterm hetype')
1115 (CicMetaSubst.ppmetasenv [] metasenv)
1116 (CicMetaSubst.ppsubst subst)));
1120 let rec eat_prods metasenv subst context hetype ugraph =
1122 | [] -> [],metasenv,subst,hetype,ugraph
1123 | (hete, hety)::tl ->
1126 let arg,subst,metasenv,ugraph1 =
1128 let subst,metasenv,ugraph1 =
1129 fo_unif_subst subst context metasenv hety s ugraph
1131 hete,subst,metasenv,ugraph1
1132 with exn when allow_coercions && !insert_coercions ->
1133 (* we search a coercion from hety to s *)
1134 let coer, tgt_carr =
1135 let carr t subst context =
1136 CicMetaSubst.apply_subst subst t
1138 let c_hety = carr hety subst context in
1139 let c_s = carr s subst context in
1140 CoercGraph.look_for_coercion c_hety c_s, c_s
1143 | CoercGraph.NoCoercion
1144 | CoercGraph.NotHandled _ ->
1145 enrich localization_tbl hete
1147 (lazy ("The term " ^
1148 CicMetaSubst.ppterm_in_context subst hete
1149 context ^ " has type " ^
1150 CicMetaSubst.ppterm_in_context subst hety
1151 context ^ " but is here used with type " ^
1152 CicMetaSubst.ppterm_in_context subst s context
1153 (* "\nReason: " ^ Lazy.force e*))))
1154 | CoercGraph.NotMetaClosed ->
1155 enrich localization_tbl hete
1157 (lazy ("The term " ^
1158 CicMetaSubst.ppterm_in_context subst hete
1159 context ^ " has type " ^
1160 CicMetaSubst.ppterm_in_context subst hety
1161 context ^ " but is here used with type " ^
1162 CicMetaSubst.ppterm_in_context subst s context
1163 (* "\nReason: " ^ Lazy.force e*))))
1164 | CoercGraph.SomeCoercion c ->
1165 let newt, _, subst, metasenv, ugraph =
1166 avoid_double_coercion context
1167 subst metasenv ugraph
1168 (Cic.Appl[c;hete]) tgt_carr in
1170 let newty,newhety,subst,metasenv,ugraph =
1171 type_of_aux subst metasenv context newt ugraph in
1172 let subst,metasenv,ugraph1 =
1173 fo_unif_subst subst context metasenv
1176 newt, subst, metasenv, ugraph
1178 enrich localization_tbl hete
1180 (lazy ("The term " ^
1181 CicMetaSubst.ppterm_in_context subst hete
1182 context ^ " has type " ^
1183 CicMetaSubst.ppterm_in_context subst hety
1184 context ^ " but is here used with type " ^
1185 CicMetaSubst.ppterm_in_context subst s context
1186 (* "\nReason: " ^ Lazy.force e*)))) exn)
1188 enrich localization_tbl hete
1190 (lazy ("The term " ^
1191 CicMetaSubst.ppterm_in_context subst hete
1192 context ^ " has type " ^
1193 CicMetaSubst.ppterm_in_context subst hety
1194 context ^ " but is here used with type " ^
1195 CicMetaSubst.ppterm_in_context subst s context
1196 (* "\nReason: " ^ Lazy.force e*)))) exn
1198 let coerced_args,metasenv',subst',t',ugraph2 =
1199 eat_prods metasenv subst context
1200 (CicSubstitution.subst arg t) ugraph1 tl
1202 arg::coerced_args,metasenv',subst',t',ugraph2
1206 let coerced_args,metasenv,subst,t,ugraph2 =
1207 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
1209 coerced_args,t,subst,metasenv,ugraph2
1212 (* eat prods ends here! *)
1214 let t',ty,subst',metasenv',ugraph1 =
1215 type_of_aux [] metasenv context t ugraph
1217 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1218 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1219 (* Andrea: ho rimesso qui l'applicazione della subst al
1220 metasenv dopo che ho droppato l'invariante che il metsaenv
1221 e' sempre istanziato *)
1222 let substituted_metasenv =
1223 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1225 (* substituted_t,substituted_ty,substituted_metasenv *)
1226 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1228 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1230 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1231 let cleaned_metasenv =
1233 (function (n,context,ty) ->
1234 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1239 | Some (n, Cic.Decl t) ->
1241 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1242 | Some (n, Cic.Def (bo,ty)) ->
1243 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1248 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1250 Some (n, Cic.Def (bo',ty'))
1254 ) substituted_metasenv
1256 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1259 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1261 type_of_aux' ?localization_tbl metasenv context term ugraph
1263 CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
1265 let undebrujin uri typesno tys t =
1268 (fun (name,_,_,_) (i,t) ->
1269 (* here the explicit_named_substituion is assumed to be *)
1271 let t' = Cic.MutInd (uri,i,[]) in
1272 let t = CicSubstitution.subst t' t in
1274 ) tys (typesno - 1,t))
1276 let map_first_n n start f g l =
1277 let rec aux acc k l =
1280 | [] -> raise (Invalid_argument "map_first_n")
1281 | hd :: tl -> f hd k (aux acc (k+1) tl)
1287 (*CSC: this is a very rough approximation; to be finished *)
1288 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1289 let subst,metasenv,ugraph,tys =
1291 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1292 let subst,metasenv,ugraph,cl =
1294 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1295 let rec aux ctx k subst = function
1296 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1297 let subst,metasenv,ugraph,tl =
1299 (subst,metasenv,ugraph,[])
1300 (fun t n (subst,metasenv,ugraph,acc) ->
1301 let subst,metasenv,ugraph =
1303 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1305 subst,metasenv,ugraph,(t::acc))
1306 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1309 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1310 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1311 subst,metasenv,ugraph,t
1312 | Cic.Prod (name,s,t) ->
1313 let ctx = (Some (name,Cic.Decl s))::ctx in
1314 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1315 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1319 (lazy "not well formed constructor type"))
1321 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1322 subst,metasenv,ugraph,(name,ty) :: acc)
1323 cl (subst,metasenv,ugraph,[])
1325 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1326 tys ([],metasenv,ugraph,[])
1328 let substituted_tys =
1330 (fun (name,ind,arity,cl) ->
1332 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1334 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1337 metasenv,ugraph,substituted_tys
1339 let typecheck metasenv uri obj ~localization_tbl =
1340 let ugraph = CicUniv.empty_ugraph in
1342 Cic.Constant (name,Some bo,ty,args,attrs) ->
1343 let bo',boty,metasenv,ugraph =
1344 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1345 let ty',_,metasenv,ugraph =
1346 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1347 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1348 let bo' = CicMetaSubst.apply_subst subst bo' in
1349 let ty' = CicMetaSubst.apply_subst subst ty' in
1350 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1351 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1352 | Cic.Constant (name,None,ty,args,attrs) ->
1353 let ty',_,metasenv,ugraph =
1354 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1356 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1357 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1358 assert (metasenv' = metasenv);
1359 (* Here we do not check the metasenv for correctness *)
1360 let bo',boty,metasenv,ugraph =
1361 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1362 let ty',sort,metasenv,ugraph =
1363 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1367 (* instead of raising Uncertain, let's hope that the meta will become
1370 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1372 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1373 let bo' = CicMetaSubst.apply_subst subst bo' in
1374 let ty' = CicMetaSubst.apply_subst subst ty' in
1375 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1376 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1377 | Cic.Variable _ -> assert false (* not implemented *)
1378 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1379 (*CSC: this code is greately simplified and many many checks are missing *)
1380 (*CSC: e.g. the constructors are not required to build their own types, *)
1381 (*CSC: the arities are not required to have as type a sort, etc. *)
1382 let uri = match uri with Some uri -> uri | None -> assert false in
1383 let typesno = List.length tys in
1384 (* first phase: we fix only the types *)
1385 let metasenv,ugraph,tys =
1387 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1388 let ty',_,metasenv,ugraph =
1389 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1391 metasenv,ugraph,(name,b,ty',cl)::res
1392 ) tys (metasenv,ugraph,[]) in
1394 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1395 (* second phase: we fix only the constructors *)
1396 let metasenv,ugraph,tys =
1398 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1399 let metasenv,ugraph,cl' =
1401 (fun (name,ty) (metasenv,ugraph,res) ->
1403 CicTypeChecker.debrujin_constructor
1404 ~cb:(relocalize localization_tbl) uri typesno ty in
1405 let ty',_,metasenv,ugraph =
1406 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1407 let ty' = undebrujin uri typesno tys ty' in
1408 metasenv,ugraph,(name,ty')::res
1409 ) cl (metasenv,ugraph,[])
1411 metasenv,ugraph,(name,b,ty,cl')::res
1412 ) tys (metasenv,ugraph,[]) in
1413 (* third phase: we check the positivity condition *)
1414 let metasenv,ugraph,tys =
1415 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1417 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1420 (* sara' piu' veloce che raffinare da zero? mah.... *)
1421 let pack_coercion metasenv t =
1422 let module C = Cic in
1423 let rec merge_coercions ctx =
1424 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1426 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1427 | C.Meta (n,subst) ->
1430 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1433 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1434 | C.Prod (name,so,dest) ->
1435 let ctx' = (Some (name,C.Decl so))::ctx in
1436 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1437 | C.Lambda (name,so,dest) ->
1438 let ctx' = (Some (name,C.Decl so))::ctx in
1439 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1440 | C.LetIn (name,so,dest) ->
1441 let ctx' = Some (name,(C.Def (so,None)))::ctx in
1442 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1444 let b,_,_,_ = is_a_double_coercion t in
1445 (* prerr_endline "CANDIDATO!!!!"; *)
1448 let ugraph = CicUniv.empty_ugraph in
1449 let old_insert_coercions = !insert_coercions in
1450 insert_coercions := false;
1451 let newt, _, menv, _ =
1453 type_of_aux' metasenv ctx t ugraph
1454 with RefineFailure _ | Uncertain _ ->
1455 prerr_endline (CicPp.ppterm t);
1458 insert_coercions := old_insert_coercions;
1459 if metasenv <> [] || menv = [] then
1462 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1467 | C.Appl l -> C.Appl (List.map (merge_coercions ctx) l)
1468 | _ -> assert false)
1469 | C.Var (uri,exp_named_subst) ->
1470 let exp_named_subst = List.map aux exp_named_subst in
1471 C.Var (uri, exp_named_subst)
1472 | C.Const (uri,exp_named_subst) ->
1473 let exp_named_subst = List.map aux exp_named_subst in
1474 C.Const (uri, exp_named_subst)
1475 | C.MutInd (uri,tyno,exp_named_subst) ->
1476 let exp_named_subst = List.map aux exp_named_subst in
1477 C.MutInd (uri,tyno,exp_named_subst)
1478 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1479 let exp_named_subst = List.map aux exp_named_subst in
1480 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1481 | C.MutCase (uri,tyno,out,te,pl) ->
1482 let pl = List.map (merge_coercions ctx) pl in
1483 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1484 | C.Fix (fno, fl) ->
1487 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1492 (fun (name,idx,ty,bo) ->
1493 (name,idx,merge_coercions ctx ty,merge_coercions ctx bo))
1497 | C.CoFix (fno, fl) ->
1500 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1505 (fun (name,ty,bo) ->
1506 (name, merge_coercions ctx ty, merge_coercions ctx bo))
1511 merge_coercions [] t
1514 let pack_coercion_obj obj =
1515 let module C = Cic in
1517 | C.Constant (id, body, ty, params, attrs) ->
1521 | Some body -> Some (pack_coercion [] body)
1523 let ty = pack_coercion [] ty in
1524 C.Constant (id, body, ty, params, attrs)
1525 | C.Variable (name, body, ty, params, attrs) ->
1529 | Some body -> Some (pack_coercion [] body)
1531 let ty = pack_coercion [] ty in
1532 C.Variable (name, body, ty, params, attrs)
1533 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1536 (fun (i, ctx, ty) ->
1540 | Some (name, C.Decl t) ->
1541 Some (name, C.Decl (pack_coercion conjectures t))
1542 | Some (name, C.Def (t,None)) ->
1543 Some (name, C.Def (pack_coercion conjectures t, None))
1544 | Some (name, C.Def (t,Some ty)) ->
1545 Some (name, C.Def (pack_coercion conjectures t,
1546 Some (pack_coercion conjectures ty)))
1550 ((i,ctx,pack_coercion conjectures ty)))
1553 let body = pack_coercion conjectures body in
1554 let ty = pack_coercion conjectures ty in
1555 C.CurrentProof (name, conjectures, body, ty, params, attrs)
1556 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1559 (fun (name, ind, arity, cl) ->
1560 let arity = pack_coercion [] arity in
1562 List.map (fun (name, ty) -> (name,pack_coercion [] ty)) cl
1564 (name, ind, arity, cl))
1567 C.InductiveDefinition (indtys, params, leftno, attrs)
1572 let type_of_aux' metasenv context term =
1575 type_of_aux' metasenv context term in
1577 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1579 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1582 | RefineFailure msg as e ->
1583 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1585 | Uncertain msg as e ->
1586 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1590 let profiler2 = HExtlib.profile "CicRefine"
1592 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1593 profiler2.HExtlib.profile
1594 (type_of_aux' ?localization_tbl metasenv context term) ugraph
1596 let typecheck ~localization_tbl metasenv uri obj =
1597 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj