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
148 let subst, metasenv, ugraph =
149 fo_unif_subst subst context metasenv newt t ugraph
154 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm (Cic.Appl (c::args))));
155 Cic.Appl (c::args), ty, subst, metasenv, ugraph
158 prerr_endline ("#### Coercion not packed (Refine_failure): " ^
159 CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args)));
162 prerr_endline ("#### Coercion not packed (Uncercatin case): " ^
163 CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args)));
165 | _ -> assert false) (* the composite coercion must exist *)
167 t, ty, subst, metasenv, ugraph
169 let rec type_of_constant uri ugraph =
170 let module C = Cic in
171 let module R = CicReduction in
172 let module U = UriManager in
173 let _ = CicTypeChecker.typecheck uri in
176 CicEnvironment.get_cooked_obj ugraph uri
177 with Not_found -> assert false
180 C.Constant (_,_,ty,_,_) -> ty,u
181 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
185 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
187 and type_of_variable uri ugraph =
188 let module C = Cic in
189 let module R = CicReduction in
190 let module U = UriManager in
191 let _ = CicTypeChecker.typecheck uri in
194 CicEnvironment.get_cooked_obj ugraph uri
195 with Not_found -> assert false
198 C.Variable (_,_,ty,_,_) -> ty,u
202 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
204 and type_of_mutual_inductive_defs uri i ugraph =
205 let module C = Cic in
206 let module R = CicReduction in
207 let module U = UriManager in
208 let _ = CicTypeChecker.typecheck uri in
211 CicEnvironment.get_cooked_obj ugraph uri
212 with Not_found -> assert false
215 C.InductiveDefinition (dl,_,_,_) ->
216 let (_,_,arity,_) = List.nth dl i in
221 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
223 and type_of_mutual_inductive_constr uri i j ugraph =
224 let module C = Cic in
225 let module R = CicReduction in
226 let module U = UriManager in
227 let _ = CicTypeChecker.typecheck uri in
230 CicEnvironment.get_cooked_obj ugraph uri
231 with Not_found -> assert false
234 C.InductiveDefinition (dl,_,_,_) ->
235 let (_,_,_,cl) = List.nth dl i in
236 let (_,ty) = List.nth cl (j-1) in
242 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
245 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
247 (* the check_branch function checks if a branch of a case is refinable.
248 It returns a pair (outype_instance,args), a subst and a metasenv.
249 outype_instance is the expected result of applying the case outtype
251 The problem is that outype is in general unknown, and we should
252 try to synthesize it from the above information, that is in general
253 a second order unification problem. *)
255 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
256 let module C = Cic in
257 (* let module R = CicMetaSubst in *)
258 let module R = CicReduction in
259 match R.whd ~subst context expectedtype with
261 (n,context,actualtype, [term]), subst, metasenv, ugraph
262 | C.Appl (C.MutInd (_,_,_)::tl) ->
263 let (_,arguments) = split tl left_args_no in
264 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
265 | C.Prod (name,so,de) ->
266 (* we expect that the actual type of the branch has the due
268 (match R.whd ~subst context actualtype with
269 C.Prod (name',so',de') ->
270 let subst, metasenv, ugraph1 =
271 fo_unif_subst subst context metasenv so so' ugraph in
273 (match CicSubstitution.lift 1 term with
274 C.Appl l -> C.Appl (l@[C.Rel 1])
275 | t -> C.Appl [t ; C.Rel 1]) in
276 (* we should also check that the name variable is anonymous in
277 the actual type de' ?? *)
279 ((Some (name,(C.Decl so)))::context)
280 metasenv subst left_args_no de' term' de ugraph1
281 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
282 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
284 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
287 let rec type_of_aux subst metasenv context t ugraph =
288 let module C = Cic in
289 let module S = CicSubstitution in
290 let module U = UriManager in
291 let (t',_,_,_,_) as res =
296 match List.nth context (n - 1) with
297 Some (_,C.Decl ty) ->
298 t,S.lift n ty,subst,metasenv, ugraph
299 | Some (_,C.Def (_,Some ty)) ->
300 t,S.lift n ty,subst,metasenv, ugraph
301 | Some (_,C.Def (bo,None)) ->
303 (* if it is in the context it must be already well-typed*)
304 CicTypeChecker.type_of_aux' ~subst metasenv context
307 t,ty,subst,metasenv,ugraph
309 enrich localization_tbl t
310 (RefineFailure (lazy "Rel to hidden hypothesis"))
313 enrich localization_tbl t
314 (RefineFailure (lazy "Not a close term")))
315 | C.Var (uri,exp_named_subst) ->
316 let exp_named_subst',subst',metasenv',ugraph1 =
317 check_exp_named_subst
318 subst metasenv context exp_named_subst ugraph
320 let ty_uri,ugraph1 = type_of_variable uri ugraph in
322 CicSubstitution.subst_vars exp_named_subst' ty_uri
324 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
327 let (canonical_context, term,ty) =
328 CicUtil.lookup_subst n subst
330 let l',subst',metasenv',ugraph1 =
331 check_metasenv_consistency n subst metasenv context
332 canonical_context l ugraph
334 (* trust or check ??? *)
335 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
336 subst', metasenv', ugraph1
337 (* type_of_aux subst metasenv
338 context (CicSubstitution.subst_meta l term) *)
339 with CicUtil.Subst_not_found _ ->
340 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
341 let l',subst',metasenv', ugraph1 =
342 check_metasenv_consistency n subst metasenv context
343 canonical_context l ugraph
345 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
346 subst', metasenv',ugraph1)
347 | C.Sort (C.Type tno) ->
348 let tno' = CicUniv.fresh() in
349 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
350 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
352 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
353 | C.Implicit infos ->
354 let metasenv',t' = exp_impl metasenv subst context infos in
355 type_of_aux subst metasenv' context t' ugraph
357 let ty',_,subst',metasenv',ugraph1 =
358 type_of_aux subst metasenv context ty ugraph
360 let te',inferredty,subst'',metasenv'',ugraph2 =
361 type_of_aux subst' metasenv' context te ugraph1
364 let subst''',metasenv''',ugraph3 =
365 fo_unif_subst subst'' context metasenv''
366 inferredty ty' ugraph2
368 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
371 enrich localization_tbl te'
374 CicMetaSubst.ppterm_in_context subst'' te'
375 context ^ " has type " ^
376 CicMetaSubst.ppterm_in_context subst'' inferredty
377 context ^ " but is here used with type " ^
378 CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
380 | C.Prod (name,s,t) ->
381 let carr t subst context = CicMetaSubst.apply_subst subst t in
382 let coerce_to_sort in_source tgt_sort t type_to_coerce
383 subst context metasenv uragph
385 if not !insert_coercions then
386 t,type_to_coerce,subst,metasenv,ugraph
388 let coercion_src = carr type_to_coerce subst context in
389 match coercion_src with
391 t,type_to_coerce,subst,metasenv,ugraph
392 | Cic.Meta _ as meta ->
393 t, meta, subst, metasenv, ugraph
394 | Cic.Cast _ as cast ->
395 t, cast, subst, metasenv, ugraph
397 let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
398 let search = CoercGraph.look_for_coercion in
399 let boh = search coercion_src coercion_tgt in
401 | CoercGraph.NoCoercion
402 | CoercGraph.NotHandled _ ->
403 enrich localization_tbl t
406 CicMetaSubst.ppterm_in_context subst t context ^
407 " is not a type since it has type " ^
408 CicMetaSubst.ppterm_in_context
409 subst coercion_src context ^ " that is not a sort")))
410 | CoercGraph.NotMetaClosed ->
411 enrich localization_tbl t
414 CicMetaSubst.ppterm_in_context subst t context ^
415 " is not a type since it has type " ^
416 CicMetaSubst.ppterm_in_context
417 subst coercion_src context ^ " that is not a sort")))
418 | CoercGraph.SomeCoercion c ->
419 let newt, tty, subst, metasenv, ugraph =
420 avoid_double_coercion context
421 subst metasenv ugraph
422 (Cic.Appl[c;t]) coercion_tgt
424 newt, tty, subst, metasenv, ugraph)
426 let s',sort1,subst',metasenv',ugraph1 =
427 type_of_aux subst metasenv context s ugraph
429 let s',sort1,subst', metasenv',ugraph1 =
430 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
431 s' sort1 subst' context metasenv' ugraph1
433 let context_for_t = ((Some (name,(C.Decl s')))::context) in
434 let t',sort2,subst'',metasenv'',ugraph2 =
435 type_of_aux subst' metasenv'
436 context_for_t t ugraph1
438 let t',sort2,subst'',metasenv'',ugraph2 =
439 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
440 t' sort2 subst'' context_for_t metasenv'' ugraph2
442 let sop,subst''',metasenv''',ugraph3 =
443 sort_of_prod subst'' metasenv''
444 context (name,s') (sort1,sort2) ugraph2
446 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
447 | C.Lambda (n,s,t) ->
449 let s',sort1,subst',metasenv',ugraph1 =
450 type_of_aux subst metasenv context s ugraph in
451 let s',sort1,subst',metasenv',ugraph1 =
452 if not !insert_coercions then
453 s',sort1, subst', metasenv', ugraph1
455 match CicReduction.whd ~subst:subst' context sort1 with
456 | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
458 let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
459 let search = CoercGraph.look_for_coercion in
460 let boh = search coercion_src coercion_tgt in
462 | CoercGraph.SomeCoercion c ->
463 let newt, tty, subst', metasenv', ugraph1 =
464 avoid_double_coercion context
465 subst' metasenv' ugraph1
466 (Cic.Appl[c;s']) coercion_tgt
468 newt, tty, subst', metasenv', ugraph1
469 | CoercGraph.NoCoercion
470 | CoercGraph.NotHandled _ ->
471 enrich localization_tbl s'
474 CicMetaSubst.ppterm_in_context subst s' context ^
475 " is not a type since it has type " ^
476 CicMetaSubst.ppterm_in_context
477 subst coercion_src context ^ " that is not a sort")))
478 | CoercGraph.NotMetaClosed ->
479 enrich localization_tbl s'
482 CicMetaSubst.ppterm_in_context subst s' context ^
483 " is not a type since it has type " ^
484 CicMetaSubst.ppterm_in_context
485 subst coercion_src context ^ " that is not a sort")))
487 let context_for_t = ((Some (n,(C.Decl s')))::context) in
488 let t',type2,subst'',metasenv'',ugraph2 =
489 type_of_aux subst' metasenv' context_for_t t ugraph1
491 C.Lambda (n,s',t'),C.Prod (n,s',type2),
492 subst'',metasenv'',ugraph2
494 (* only to check if s is well-typed *)
495 let s',ty,subst',metasenv',ugraph1 =
496 type_of_aux subst metasenv context s ugraph
498 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
500 let t',inferredty,subst'',metasenv'',ugraph2 =
501 type_of_aux subst' metasenv'
502 context_for_t t ugraph1
504 (* One-step LetIn reduction.
505 * Even faster than the previous solution.
506 * Moreover the inferred type is closer to the expected one.
508 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
509 subst'',metasenv'',ugraph2
510 | C.Appl (he::((_::_) as tl)) ->
511 let he',hetype,subst',metasenv',ugraph1 =
512 type_of_aux subst metasenv context he ugraph
514 let tlbody_and_type,subst'',metasenv'',ugraph2 =
516 (fun x (res,subst,metasenv,ugraph) ->
517 let x',ty,subst',metasenv',ugraph1 =
518 type_of_aux subst metasenv context x ugraph
520 (x', ty)::res,subst',metasenv',ugraph1
521 ) tl ([],subst',metasenv',ugraph1)
523 let tl',applty,subst''',metasenv''',ugraph3 =
524 eat_prods true subst'' metasenv'' context
525 he hetype tlbody_and_type ugraph2
527 avoid_double_coercion context
528 subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
529 | C.Appl _ -> assert false
530 | C.Const (uri,exp_named_subst) ->
531 let exp_named_subst',subst',metasenv',ugraph1 =
532 check_exp_named_subst subst metasenv context
533 exp_named_subst ugraph in
534 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
536 CicSubstitution.subst_vars exp_named_subst' ty_uri
538 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
539 | C.MutInd (uri,i,exp_named_subst) ->
540 let exp_named_subst',subst',metasenv',ugraph1 =
541 check_exp_named_subst subst metasenv context
542 exp_named_subst ugraph
544 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
546 CicSubstitution.subst_vars exp_named_subst' ty_uri in
547 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
548 | C.MutConstruct (uri,i,j,exp_named_subst) ->
549 let exp_named_subst',subst',metasenv',ugraph1 =
550 check_exp_named_subst subst metasenv context
551 exp_named_subst ugraph
554 type_of_mutual_inductive_constr uri i j ugraph1
557 CicSubstitution.subst_vars exp_named_subst' ty_uri
559 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
561 | C.MutCase (uri, i, outtype, term, pl) ->
562 (* first, get the inductive type (and noparams)
563 * in the environment *)
564 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
565 let _ = CicTypeChecker.typecheck uri in
566 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
568 C.InductiveDefinition (l,expl_params,parsno,_) ->
569 List.nth l i , expl_params, parsno, u
571 enrich localization_tbl t
573 (lazy ("Unkown mutual inductive definition " ^
574 U.string_of_uri uri)))
576 let rec count_prod t =
577 match CicReduction.whd ~subst context t with
578 C.Prod (_, _, t) -> 1 + (count_prod t)
581 let no_args = count_prod arity in
582 (* now, create a "generic" MutInd *)
583 let metasenv,left_args =
584 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
586 let metasenv,right_args =
587 let no_right_params = no_args - no_left_params in
588 if no_right_params < 0 then assert false
589 else CicMkImplicit.n_fresh_metas
590 metasenv subst context no_right_params
592 let metasenv,exp_named_subst =
593 CicMkImplicit.fresh_subst metasenv subst context expl_params in
596 C.MutInd (uri,i,exp_named_subst)
599 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
601 (* check consistency with the actual type of term *)
602 let term',actual_type,subst,metasenv,ugraph1 =
603 type_of_aux subst metasenv context term ugraph in
604 let expected_type',_, subst, metasenv,ugraph2 =
605 type_of_aux subst metasenv context expected_type ugraph1
607 let actual_type = CicReduction.whd ~subst context actual_type in
608 let subst,metasenv,ugraph3 =
610 fo_unif_subst subst context metasenv
611 expected_type' actual_type ugraph2
614 enrich localization_tbl term' exn
617 CicMetaSubst.ppterm_in_context subst term'
618 context ^ " has type " ^
619 CicMetaSubst.ppterm_in_context subst actual_type
620 context ^ " but is here used with type " ^
621 CicMetaSubst.ppterm_in_context subst expected_type' context))
623 let rec instantiate_prod t =
627 match CicReduction.whd ~subst context t with
629 instantiate_prod (CicSubstitution.subst he t') tl
632 let arity_instantiated_with_left_args =
633 instantiate_prod arity left_args in
634 (* TODO: check if the sort elimination
635 * is allowed: [(I q1 ... qr)|B] *)
636 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
638 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
640 if left_args = [] then
641 (C.MutConstruct (uri,i,j,exp_named_subst))
644 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
646 let p',actual_type,subst,metasenv,ugraph1 =
647 type_of_aux subst metasenv context p ugraph
649 let constructor',expected_type, subst, metasenv,ugraph2 =
650 type_of_aux subst metasenv context constructor ugraph1
652 let outtypeinstance,subst,metasenv,ugraph3 =
653 check_branch 0 context metasenv subst no_left_params
654 actual_type constructor' expected_type ugraph2
657 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
658 ([],1,[],subst,metasenv,ugraph3) pl
661 (* we are left to check that the outype matches his instances.
662 The easy case is when the outype is specified, that amount
663 to a trivial check. Otherwise, we should guess a type from
667 let outtype,outtypety, subst, metasenv,ugraph4 =
668 type_of_aux subst metasenv context outtype ugraph4 in
671 (let candidate,ugraph5,metasenv,subst =
672 let exp_name_subst, metasenv =
674 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
676 let uris = CicUtil.params_of_obj o in
678 fun uri (acc,metasenv) ->
679 let metasenv',new_meta =
680 CicMkImplicit.mk_implicit metasenv subst context
683 CicMkImplicit.identity_relocation_list_for_metavariable
686 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
690 match left_args,right_args with
691 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
693 let rec mk_right_args =
696 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
698 let right_args_no = List.length right_args in
699 let lifted_left_args =
700 List.map (CicSubstitution.lift right_args_no) left_args
702 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
703 (lifted_left_args @ mk_right_args right_args_no))
706 FreshNamesGenerator.mk_fresh_name ~subst metasenv
707 context Cic.Anonymous ~typ:ty
709 match outtypeinstances with
711 let extended_context =
712 let rec add_right_args =
714 Cic.Prod (name,ty,t) ->
715 Some (name,Cic.Decl ty)::(add_right_args t)
718 (Some (fresh_name,Cic.Decl ty))::
720 (add_right_args arity_instantiated_with_left_args))@
723 let metasenv,new_meta =
724 CicMkImplicit.mk_implicit metasenv subst extended_context
727 CicMkImplicit.identity_relocation_list_for_metavariable
730 let rec add_lambdas b =
732 Cic.Prod (name,ty,t) ->
733 Cic.Lambda (name,ty,(add_lambdas b t))
734 | _ -> Cic.Lambda (fresh_name, ty, b)
737 add_lambdas (Cic.Meta (new_meta,irl))
738 arity_instantiated_with_left_args
740 (Some candidate),ugraph4,metasenv,subst
741 | (constructor_args_no,_,instance,_)::tl ->
743 let instance',subst,metasenv =
744 CicMetaSubst.delift_rels subst metasenv
745 constructor_args_no instance
747 let candidate,ugraph,metasenv,subst =
749 fun (candidate_oty,ugraph,metasenv,subst)
750 (constructor_args_no,_,instance,_) ->
751 match candidate_oty with
752 | None -> None,ugraph,metasenv,subst
755 let instance',subst,metasenv =
756 CicMetaSubst.delift_rels subst metasenv
757 constructor_args_no instance
759 let subst,metasenv,ugraph =
760 fo_unif_subst subst context metasenv
763 candidate_oty,ugraph,metasenv,subst
765 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
766 | CicUnification.UnificationFailure _
767 | CicUnification.Uncertain _ ->
768 None,ugraph,metasenv,subst
769 ) (Some instance',ugraph4,metasenv,subst) tl
772 | None -> None, ugraph,metasenv,subst
774 let rec add_lambdas n b =
776 Cic.Prod (name,ty,t) ->
777 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
779 Cic.Lambda (fresh_name, ty,
780 CicSubstitution.lift (n + 1) t)
783 (add_lambdas 0 t arity_instantiated_with_left_args),
784 ugraph,metasenv,subst
785 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
786 None,ugraph4,metasenv,subst
789 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
791 let subst,metasenv,ugraph =
793 fo_unif_subst subst context metasenv
794 candidate outtype ugraph5
796 exn -> assert false(* unification against a metavariable *)
798 C.MutCase (uri, i, outtype, term', pl'),
799 CicReduction.head_beta_reduce
800 (CicMetaSubst.apply_subst subst
801 (Cic.Appl (outtype::right_args@[term']))),
802 subst,metasenv,ugraph)
803 | _ -> (* easy case *)
804 let tlbody_and_type,subst,metasenv,ugraph4 =
806 (fun x (res,subst,metasenv,ugraph) ->
807 let x',ty,subst',metasenv',ugraph1 =
808 type_of_aux subst metasenv context x ugraph
810 (x', ty)::res,subst',metasenv',ugraph1
811 ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
813 let _,_,subst,metasenv,ugraph4 =
814 eat_prods false subst metasenv context
815 outtype outtypety tlbody_and_type ugraph4
817 let _,_, subst, metasenv,ugraph5 =
818 type_of_aux subst metasenv context
819 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
821 let (subst,metasenv,ugraph6) =
823 (fun (subst,metasenv,ugraph)
824 p (constructor_args_no,context,instance,args)
829 CicSubstitution.lift constructor_args_no outtype
831 C.Appl (outtype'::args)
833 CicReduction.whd ~subst context appl
836 fo_unif_subst subst context metasenv instance instance'
840 enrich localization_tbl p exn
843 CicMetaSubst.ppterm_in_context subst p
844 context ^ " has type " ^
845 CicMetaSubst.ppterm_in_context subst instance'
846 context ^ " but is here used with type " ^
847 CicMetaSubst.ppterm_in_context subst instance
849 (subst,metasenv,ugraph5) pl' outtypeinstances
851 C.MutCase (uri, i, outtype, term', pl'),
852 CicReduction.head_beta_reduce
853 (CicMetaSubst.apply_subst subst
854 (C.Appl(outtype::right_args@[term]))),
855 subst,metasenv,ugraph6)
857 let fl_ty',subst,metasenv,types,ugraph1 =
859 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
860 let ty',_,subst',metasenv',ugraph1 =
861 type_of_aux subst metasenv context ty ugraph
863 fl @ [ty'],subst',metasenv',
864 Some (C.Name n,(C.Decl ty')) :: types, ugraph
865 ) ([],subst,metasenv,[],ugraph) fl
867 let len = List.length types in
868 let context' = types@context in
869 let fl_bo',subst,metasenv,ugraph2 =
871 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
872 let bo',ty_of_bo,subst,metasenv,ugraph1 =
873 type_of_aux subst metasenv context' bo ugraph in
874 let expected_ty = CicSubstitution.lift len ty in
875 let subst',metasenv',ugraph' =
877 fo_unif_subst subst context' metasenv
878 ty_of_bo expected_ty ugraph1
881 enrich localization_tbl bo exn
884 CicMetaSubst.ppterm_in_context subst bo
885 context' ^ " has type " ^
886 CicMetaSubst.ppterm_in_context subst ty_of_bo
887 context' ^ " but is here used with type " ^
888 CicMetaSubst.ppterm_in_context subst expected_ty
891 fl @ [bo'] , subst',metasenv',ugraph'
892 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
894 let ty = List.nth fl_ty' i in
895 (* now we have the new ty in fl_ty', the new bo in fl_bo',
896 * and we want the new fl with bo' and ty' injected in the right
899 let rec map3 f l1 l2 l3 =
902 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
905 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
908 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
910 let fl_ty',subst,metasenv,types,ugraph1 =
912 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
913 let ty',_,subst',metasenv',ugraph1 =
914 type_of_aux subst metasenv context ty ugraph
916 fl @ [ty'],subst',metasenv',
917 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
918 ) ([],subst,metasenv,[],ugraph) fl
920 let len = List.length types in
921 let context' = types@context in
922 let fl_bo',subst,metasenv,ugraph2 =
924 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
925 let bo',ty_of_bo,subst,metasenv,ugraph1 =
926 type_of_aux subst metasenv context' bo ugraph in
927 let expected_ty = CicSubstitution.lift len ty in
928 let subst',metasenv',ugraph' =
930 fo_unif_subst subst context' metasenv
931 ty_of_bo expected_ty ugraph1
934 enrich localization_tbl bo exn
937 CicMetaSubst.ppterm_in_context subst bo
938 context' ^ " has type " ^
939 CicMetaSubst.ppterm_in_context subst ty_of_bo
940 context' ^ " but is here used with type " ^
941 CicMetaSubst.ppterm_in_context subst expected_ty
944 fl @ [bo'],subst',metasenv',ugraph'
945 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
947 let ty = List.nth fl_ty' i in
948 (* now we have the new ty in fl_ty', the new bo in fl_bo',
949 * and we want the new fl with bo' and ty' injected in the right
952 let rec map3 f l1 l2 l3 =
955 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
958 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
961 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
963 relocalize localization_tbl t t';
966 (* check_metasenv_consistency checks that the "canonical" context of a
967 metavariable is consitent - up to relocation via the relocation list l -
968 with the actual context *)
969 and check_metasenv_consistency
970 metano subst metasenv context canonical_context l ugraph
972 let module C = Cic in
973 let module R = CicReduction in
974 let module S = CicSubstitution in
975 let lifted_canonical_context =
979 | (Some (n,C.Decl t))::tl ->
980 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
981 | (Some (n,C.Def (t,None)))::tl ->
982 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
983 | None::tl -> None::(aux (i+1) tl)
984 | (Some (n,C.Def (t,Some ty)))::tl ->
986 C.Def ((S.subst_meta l (S.lift i t)),
987 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
989 aux 1 canonical_context
993 (fun (l,subst,metasenv,ugraph) t ct ->
996 l @ [None],subst,metasenv,ugraph
997 | Some t,Some (_,C.Def (ct,_)) ->
998 let subst',metasenv',ugraph' =
1000 fo_unif_subst subst context metasenv t ct ugraph
1001 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))))))
1003 l @ [Some t],subst',metasenv',ugraph'
1004 | Some t,Some (_,C.Decl ct) ->
1005 let t',inferredty,subst',metasenv',ugraph1 =
1006 type_of_aux subst metasenv context t ugraph
1008 let subst'',metasenv'',ugraph2 =
1011 subst' context metasenv' inferredty ct ugraph1
1012 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))))))
1014 l @ [Some t'], subst'',metasenv'',ugraph2
1016 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
1018 Invalid_argument _ ->
1022 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1023 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
1024 (CicMetaSubst.ppcontext subst canonical_context))))
1026 and check_exp_named_subst metasubst metasenv context tl ugraph =
1027 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1029 [] -> [],metasubst,metasenv,ugraph
1031 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1033 CicSubstitution.subst_vars substs ty_uri in
1034 (* CSC: why was this code here? it is wrong
1035 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1036 Cic.Variable (_,Some bo,_,_) ->
1038 (RefineFailure (lazy
1039 "A variable with a body can not be explicit substituted"))
1040 | Cic.Variable (_,None,_,_) -> ()
1043 (RefineFailure (lazy
1044 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1047 let t',typeoft,metasubst',metasenv',ugraph2 =
1048 type_of_aux metasubst metasenv context t ugraph1 in
1049 let subst = uri,t' in
1050 let metasubst'',metasenv'',ugraph3 =
1053 metasubst' context metasenv' typeoft typeofvar ugraph2
1055 raise (RefineFailure (lazy
1056 ("Wrong Explicit Named Substitution: " ^
1057 CicMetaSubst.ppterm metasubst' typeoft ^
1058 " not unifiable with " ^
1059 CicMetaSubst.ppterm metasubst' typeofvar)))
1061 (* FIXME: no mere tail recursive! *)
1062 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1063 check_exp_named_subst_aux
1064 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1066 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1068 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1071 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
1072 let module C = Cic in
1073 let context_for_t2 = (Some (name,C.Decl s))::context in
1074 let t1'' = CicReduction.whd ~subst context t1 in
1075 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1076 match (t1'', t2'') with
1077 (C.Sort s1, C.Sort s2)
1078 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1079 (* different than Coq manual!!! *)
1080 C.Sort s2,subst,metasenv,ugraph
1081 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1082 let t' = CicUniv.fresh() in
1083 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1084 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1085 C.Sort (C.Type t'),subst,metasenv,ugraph2
1086 | (C.Sort _,C.Sort (C.Type t1)) ->
1087 C.Sort (C.Type t1),subst,metasenv,ugraph
1088 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1089 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1090 (* TODO how can we force the meta to become a sort? If we don't we
1091 * break the invariant that refine produce only well typed terms *)
1092 (* TODO if we check the non meta term and if it is a sort then we
1093 * are likely to know the exact value of the result e.g. if the rhs
1094 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1095 let (metasenv,idx) =
1096 CicMkImplicit.mk_implicit_sort metasenv subst in
1097 let (subst, metasenv,ugraph1) =
1099 fo_unif_subst subst context_for_t2 metasenv
1100 (C.Meta (idx,[])) t2'' ugraph
1101 with _ -> assert false (* unification against a metavariable *)
1103 t2'',subst,metasenv,ugraph1
1109 ("Two sorts were expected, found %s " ^^
1110 "(that reduces to %s) and %s (that reduces to %s)")
1111 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
1112 (CicPp.ppterm t2''))))
1115 allow_coercions subst metasenv context he hetype tlbody_and_type ugraph
1117 let rec mk_prod metasenv context' =
1120 let (metasenv, idx) =
1121 CicMkImplicit.mk_implicit_type metasenv subst context'
1124 CicMkImplicit.identity_relocation_list_for_metavariable context'
1126 metasenv,Cic.Meta (idx, irl)
1128 let (metasenv, idx) =
1129 CicMkImplicit.mk_implicit_type metasenv subst context'
1132 CicMkImplicit.identity_relocation_list_for_metavariable context'
1134 let meta = Cic.Meta (idx,irl) in
1136 (* The name must be fresh for context. *)
1137 (* Nevertheless, argty is well-typed only in context. *)
1138 (* Thus I generate a name (name_hint) in context and *)
1139 (* then I generate a name --- using the hint name_hint *)
1140 (* --- that is fresh in context'. *)
1142 (* Cic.Name "pippo" *)
1143 FreshNamesGenerator.mk_fresh_name ~subst metasenv
1144 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
1145 (CicMetaSubst.apply_subst_context subst context)
1147 ~typ:(CicMetaSubst.apply_subst subst argty)
1149 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
1150 FreshNamesGenerator.mk_fresh_name ~subst
1151 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
1153 let metasenv,target =
1154 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
1156 metasenv,Cic.Prod (name,meta,target)
1158 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
1159 let (subst, metasenv,ugraph1) =
1161 fo_unif_subst subst context metasenv hetype hetype' ugraph
1163 enrich localization_tbl he
1165 (lazy ("The term " ^
1166 CicMetaSubst.ppterm_in_context subst he
1167 context ^ "(that has type " ^
1168 CicMetaSubst.ppterm_in_context subst hetype
1169 context ^ ") is here applied to " ^
1170 string_of_int (List.length tlbody_and_type) ^
1171 " arguments that are more than expected"
1172 (* "\nReason: " ^ Lazy.force exn*)))) exn
1174 let rec eat_prods metasenv subst context hetype ugraph =
1176 | [] -> [],metasenv,subst,hetype,ugraph
1177 | (hete, hety)::tl ->
1180 let arg,subst,metasenv,ugraph1 =
1182 let subst,metasenv,ugraph1 =
1183 fo_unif_subst subst context metasenv hety s ugraph
1185 hete,subst,metasenv,ugraph1
1186 with exn when allow_coercions && !insert_coercions ->
1187 (* we search a coercion from hety to s *)
1188 let coer, tgt_carr =
1189 let carr t subst context =
1190 CicMetaSubst.apply_subst subst t
1192 let c_hety = carr hety subst context in
1193 let c_s = carr s subst context in
1194 CoercGraph.look_for_coercion c_hety c_s, c_s
1197 | CoercGraph.NoCoercion
1198 | CoercGraph.NotHandled _ ->
1199 enrich localization_tbl hete
1201 (lazy ("The term " ^
1202 CicMetaSubst.ppterm_in_context subst hete
1203 context ^ " has type " ^
1204 CicMetaSubst.ppterm_in_context subst hety
1205 context ^ " but is here used with type " ^
1206 CicMetaSubst.ppterm_in_context subst s context
1207 (* "\nReason: " ^ Lazy.force e*))))
1208 | CoercGraph.NotMetaClosed ->
1209 enrich localization_tbl hete
1211 (lazy ("The term " ^
1212 CicMetaSubst.ppterm_in_context subst hete
1213 context ^ " has type " ^
1214 CicMetaSubst.ppterm_in_context subst hety
1215 context ^ " but is here used with type " ^
1216 CicMetaSubst.ppterm_in_context subst s context
1217 (* "\nReason: " ^ Lazy.force e*))))
1218 | CoercGraph.SomeCoercion c ->
1219 let newt, _, subst, metasenv, ugraph =
1220 avoid_double_coercion context
1221 subst metasenv ugraph
1222 (Cic.Appl[c;hete]) tgt_carr in
1224 let newty,newhety,subst,metasenv,ugraph =
1225 type_of_aux subst metasenv context newt ugraph in
1226 let subst,metasenv,ugraph1 =
1227 fo_unif_subst subst context metasenv
1230 newt, subst, metasenv, ugraph
1232 enrich localization_tbl hete
1234 (lazy ("The term " ^
1235 CicMetaSubst.ppterm_in_context subst hete
1236 context ^ " has type " ^
1237 CicMetaSubst.ppterm_in_context subst hety
1238 context ^ " but is here used with type " ^
1239 CicMetaSubst.ppterm_in_context subst s context
1240 (* "\nReason: " ^ Lazy.force e*)))) exn)
1242 enrich localization_tbl hete
1244 (lazy ("The term " ^
1245 CicMetaSubst.ppterm_in_context subst hete
1246 context ^ " has type " ^
1247 CicMetaSubst.ppterm_in_context subst hety
1248 context ^ " but is here used with type " ^
1249 CicMetaSubst.ppterm_in_context subst s context
1250 (* "\nReason: " ^ Lazy.force e*)))) exn
1252 let coerced_args,metasenv',subst',t',ugraph2 =
1253 eat_prods metasenv subst context
1254 (CicSubstitution.subst arg t) ugraph1 tl
1256 arg::coerced_args,metasenv',subst',t',ugraph2
1260 let coerced_args,metasenv,subst,t,ugraph2 =
1261 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
1263 coerced_args,t,subst,metasenv,ugraph2
1266 (* eat prods ends here! *)
1268 let t',ty,subst',metasenv',ugraph1 =
1269 type_of_aux [] metasenv context t ugraph
1271 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1272 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1273 (* Andrea: ho rimesso qui l'applicazione della subst al
1274 metasenv dopo che ho droppato l'invariante che il metsaenv
1275 e' sempre istanziato *)
1276 let substituted_metasenv =
1277 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1279 (* substituted_t,substituted_ty,substituted_metasenv *)
1280 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1282 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1284 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1285 let cleaned_metasenv =
1287 (function (n,context,ty) ->
1288 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1293 | Some (n, Cic.Decl t) ->
1295 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1296 | Some (n, Cic.Def (bo,ty)) ->
1297 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1302 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1304 Some (n, Cic.Def (bo',ty'))
1308 ) substituted_metasenv
1310 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1313 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1315 type_of_aux' ?localization_tbl metasenv context term ugraph
1317 CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
1319 let undebrujin uri typesno tys t =
1322 (fun (name,_,_,_) (i,t) ->
1323 (* here the explicit_named_substituion is assumed to be *)
1325 let t' = Cic.MutInd (uri,i,[]) in
1326 let t = CicSubstitution.subst t' t in
1328 ) tys (typesno - 1,t))
1330 let map_first_n n start f g l =
1331 let rec aux acc k l =
1334 | [] -> raise (Invalid_argument "map_first_n")
1335 | hd :: tl -> f hd k (aux acc (k+1) tl)
1341 (*CSC: this is a very rough approximation; to be finished *)
1342 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1343 let subst,metasenv,ugraph,tys =
1345 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1346 let subst,metasenv,ugraph,cl =
1348 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1349 let rec aux ctx k subst = function
1350 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1351 let subst,metasenv,ugraph,tl =
1353 (subst,metasenv,ugraph,[])
1354 (fun t n (subst,metasenv,ugraph,acc) ->
1355 let subst,metasenv,ugraph =
1357 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1359 subst,metasenv,ugraph,(t::acc))
1360 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1363 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1364 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1365 subst,metasenv,ugraph,t
1366 | Cic.Prod (name,s,t) ->
1367 let ctx = (Some (name,Cic.Decl s))::ctx in
1368 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1369 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1373 (lazy "not well formed constructor type"))
1375 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1376 subst,metasenv,ugraph,(name,ty) :: acc)
1377 cl (subst,metasenv,ugraph,[])
1379 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1380 tys ([],metasenv,ugraph,[])
1382 let substituted_tys =
1384 (fun (name,ind,arity,cl) ->
1386 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1388 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1391 metasenv,ugraph,substituted_tys
1393 let typecheck metasenv uri obj ~localization_tbl =
1394 let ugraph = CicUniv.empty_ugraph in
1396 Cic.Constant (name,Some bo,ty,args,attrs) ->
1397 let bo',boty,metasenv,ugraph =
1398 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1399 let ty',_,metasenv,ugraph =
1400 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1401 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1402 let bo' = CicMetaSubst.apply_subst subst bo' in
1403 let ty' = CicMetaSubst.apply_subst subst ty' in
1404 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1405 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1406 | Cic.Constant (name,None,ty,args,attrs) ->
1407 let ty',_,metasenv,ugraph =
1408 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1410 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1411 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1412 assert (metasenv' = metasenv);
1413 (* Here we do not check the metasenv for correctness *)
1414 let bo',boty,metasenv,ugraph =
1415 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1416 let ty',sort,metasenv,ugraph =
1417 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1421 (* instead of raising Uncertain, let's hope that the meta will become
1424 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1426 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1427 let bo' = CicMetaSubst.apply_subst subst bo' in
1428 let ty' = CicMetaSubst.apply_subst subst ty' in
1429 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1430 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1431 | Cic.Variable _ -> assert false (* not implemented *)
1432 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1433 (*CSC: this code is greately simplified and many many checks are missing *)
1434 (*CSC: e.g. the constructors are not required to build their own types, *)
1435 (*CSC: the arities are not required to have as type a sort, etc. *)
1436 let uri = match uri with Some uri -> uri | None -> assert false in
1437 let typesno = List.length tys in
1438 (* first phase: we fix only the types *)
1439 let metasenv,ugraph,tys =
1441 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1442 let ty',_,metasenv,ugraph =
1443 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1445 metasenv,ugraph,(name,b,ty',cl)::res
1446 ) tys (metasenv,ugraph,[]) in
1448 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1449 (* second phase: we fix only the constructors *)
1450 let metasenv,ugraph,tys =
1452 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1453 let metasenv,ugraph,cl' =
1455 (fun (name,ty) (metasenv,ugraph,res) ->
1457 CicTypeChecker.debrujin_constructor
1458 ~cb:(relocalize localization_tbl) uri typesno ty in
1459 let ty',_,metasenv,ugraph =
1460 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1461 let ty' = undebrujin uri typesno tys ty' in
1462 metasenv,ugraph,(name,ty')::res
1463 ) cl (metasenv,ugraph,[])
1465 metasenv,ugraph,(name,b,ty,cl')::res
1466 ) tys (metasenv,ugraph,[]) in
1467 (* third phase: we check the positivity condition *)
1468 let metasenv,ugraph,tys =
1469 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1471 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1474 (* sara' piu' veloce che raffinare da zero? mah.... *)
1475 let pack_coercion metasenv t =
1476 let module C = Cic in
1477 let rec merge_coercions ctx =
1478 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1480 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1481 | C.Meta (n,subst) ->
1484 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1487 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1488 | C.Prod (name,so,dest) ->
1489 let ctx' = (Some (name,C.Decl so))::ctx in
1490 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1491 | C.Lambda (name,so,dest) ->
1492 let ctx' = (Some (name,C.Decl so))::ctx in
1493 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1494 | C.LetIn (name,so,dest) ->
1495 let ctx' = Some (name,(C.Def (so,None)))::ctx in
1496 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1498 let b,_,_,_ = is_a_double_coercion t in
1499 (* prerr_endline "CANDIDATO!!!!"; *)
1502 let ugraph = CicUniv.empty_ugraph in
1503 let old_insert_coercions = !insert_coercions in
1504 insert_coercions := false;
1505 let newt, _, menv, _ =
1507 type_of_aux' metasenv ctx t ugraph
1508 with RefineFailure _ | Uncertain _ ->
1509 prerr_endline (CicPp.ppterm t);
1512 insert_coercions := old_insert_coercions;
1513 if metasenv <> [] || menv = [] then
1516 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1521 | C.Appl l -> C.Appl (List.map (merge_coercions ctx) l)
1522 | _ -> assert false)
1523 | C.Var (uri,exp_named_subst) ->
1524 let exp_named_subst = List.map aux exp_named_subst in
1525 C.Var (uri, exp_named_subst)
1526 | C.Const (uri,exp_named_subst) ->
1527 let exp_named_subst = List.map aux exp_named_subst in
1528 C.Const (uri, exp_named_subst)
1529 | C.MutInd (uri,tyno,exp_named_subst) ->
1530 let exp_named_subst = List.map aux exp_named_subst in
1531 C.MutInd (uri,tyno,exp_named_subst)
1532 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1533 let exp_named_subst = List.map aux exp_named_subst in
1534 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1535 | C.MutCase (uri,tyno,out,te,pl) ->
1536 let pl = List.map (merge_coercions ctx) pl in
1537 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1538 | C.Fix (fno, fl) ->
1541 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1546 (fun (name,idx,ty,bo) ->
1547 (name,idx,merge_coercions ctx ty,merge_coercions ctx bo))
1551 | C.CoFix (fno, fl) ->
1554 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1559 (fun (name,ty,bo) ->
1560 (name, merge_coercions ctx ty, merge_coercions ctx bo))
1565 merge_coercions [] t
1568 let pack_coercion_obj obj =
1569 let module C = Cic in
1571 | C.Constant (id, body, ty, params, attrs) ->
1575 | Some body -> Some (pack_coercion [] body)
1577 let ty = pack_coercion [] ty in
1578 C.Constant (id, body, ty, params, attrs)
1579 | C.Variable (name, body, ty, params, attrs) ->
1583 | Some body -> Some (pack_coercion [] body)
1585 let ty = pack_coercion [] ty in
1586 C.Variable (name, body, ty, params, attrs)
1587 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1590 (fun (i, ctx, ty) ->
1594 | Some (name, C.Decl t) ->
1595 Some (name, C.Decl (pack_coercion conjectures t))
1596 | Some (name, C.Def (t,None)) ->
1597 Some (name, C.Def (pack_coercion conjectures t, None))
1598 | Some (name, C.Def (t,Some ty)) ->
1599 Some (name, C.Def (pack_coercion conjectures t,
1600 Some (pack_coercion conjectures ty)))
1604 ((i,ctx,pack_coercion conjectures ty)))
1607 let body = pack_coercion conjectures body in
1608 let ty = pack_coercion conjectures ty in
1609 C.CurrentProof (name, conjectures, body, ty, params, attrs)
1610 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1613 (fun (name, ind, arity, cl) ->
1614 let arity = pack_coercion [] arity in
1616 List.map (fun (name, ty) -> (name,pack_coercion [] ty)) cl
1618 (name, ind, arity, cl))
1621 C.InductiveDefinition (indtys, params, leftno, attrs)
1626 let type_of_aux' metasenv context term =
1629 type_of_aux' metasenv context term in
1631 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1633 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1636 | RefineFailure msg as e ->
1637 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1639 | Uncertain msg as e ->
1640 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1644 let profiler2 = HExtlib.profile "CicRefine"
1646 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1647 profiler2.HExtlib.profile
1648 (type_of_aux' ?localization_tbl metasenv context term) ugraph
1650 let typecheck ~localization_tbl metasenv uri obj =
1651 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj