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_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
40 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
43 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
44 in profiler_eat_prods2.HExtlib.profile foo ()
46 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
47 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
50 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
52 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
55 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
56 in profiler_eat_prods.HExtlib.profile foo ()
58 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
59 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
62 let profiler = HExtlib.profile "CicRefine.fo_unif"
64 let fo_unif_subst subst context metasenv t1 t2 ugraph =
67 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
68 in profiler.HExtlib.profile foo ()
70 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
71 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
74 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
77 RefineFailure msg -> RefineFailure (f msg)
78 | Uncertain msg -> Uncertain (f msg)
79 | _ -> assert false in
82 Cic.CicHash.find localization_tbl t
84 prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
87 raise (HExtlib.Localized (loc,exn'))
89 let relocalize localization_tbl oldt newt =
91 let infos = Cic.CicHash.find localization_tbl oldt in
92 Cic.CicHash.remove localization_tbl oldt;
93 Cic.CicHash.add localization_tbl newt infos;
101 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
102 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
105 let exp_impl metasenv subst context =
108 let (metasenv', idx) =
109 CicMkImplicit.mk_implicit_type metasenv subst context in
111 CicMkImplicit.identity_relocation_list_for_metavariable context in
112 metasenv', Cic.Meta (idx, irl)
114 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
115 metasenv', Cic.Meta (idx, [])
117 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
119 CicMkImplicit.identity_relocation_list_for_metavariable context in
120 metasenv', Cic.Meta (idx, irl)
124 let is_a_double_coercion t =
126 let rec aux = function
134 false, Cic.Implicit None, Cic.Implicit None, Cic.Implicit None
137 | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 ->
138 (match last_of tl with
139 | Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
140 let head = last_of tl2 in
145 let rec type_of_constant uri ugraph =
146 let module C = Cic in
147 let module R = CicReduction in
148 let module U = UriManager in
149 let _ = CicTypeChecker.typecheck uri in
152 CicEnvironment.get_cooked_obj ugraph uri
153 with Not_found -> assert false
156 C.Constant (_,_,ty,_,_) -> ty,u
157 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
161 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
163 and type_of_variable uri ugraph =
164 let module C = Cic in
165 let module R = CicReduction in
166 let module U = UriManager in
167 let _ = CicTypeChecker.typecheck uri in
170 CicEnvironment.get_cooked_obj ugraph uri
171 with Not_found -> assert false
174 C.Variable (_,_,ty,_,_) -> ty,u
178 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
180 and type_of_mutual_inductive_defs uri i ugraph =
181 let module C = Cic in
182 let module R = CicReduction in
183 let module U = UriManager in
184 let _ = CicTypeChecker.typecheck uri in
187 CicEnvironment.get_cooked_obj ugraph uri
188 with Not_found -> assert false
191 C.InductiveDefinition (dl,_,_,_) ->
192 let (_,_,arity,_) = List.nth dl i in
197 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
199 and type_of_mutual_inductive_constr uri i j ugraph =
200 let module C = Cic in
201 let module R = CicReduction in
202 let module U = UriManager in
203 let _ = CicTypeChecker.typecheck uri in
206 CicEnvironment.get_cooked_obj ugraph uri
207 with Not_found -> assert false
210 C.InductiveDefinition (dl,_,_,_) ->
211 let (_,_,_,cl) = List.nth dl i in
212 let (_,ty) = List.nth cl (j-1) in
218 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
221 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
223 (* the check_branch function checks if a branch of a case is refinable.
224 It returns a pair (outype_instance,args), a subst and a metasenv.
225 outype_instance is the expected result of applying the case outtype
227 The problem is that outype is in general unknown, and we should
228 try to synthesize it from the above information, that is in general
229 a second order unification problem. *)
231 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
232 let module C = Cic in
233 (* let module R = CicMetaSubst in *)
234 let module R = CicReduction in
235 match R.whd ~subst context expectedtype with
237 (n,context,actualtype, [term]), subst, metasenv, ugraph
238 | C.Appl (C.MutInd (_,_,_)::tl) ->
239 let (_,arguments) = split tl left_args_no in
240 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
241 | C.Prod (name,so,de) ->
242 (* we expect that the actual type of the branch has the due
244 (match R.whd ~subst context actualtype with
245 C.Prod (name',so',de') ->
246 let subst, metasenv, ugraph1 =
247 fo_unif_subst subst context metasenv so so' ugraph in
249 (match CicSubstitution.lift 1 term with
250 C.Appl l -> C.Appl (l@[C.Rel 1])
251 | t -> C.Appl [t ; C.Rel 1]) in
252 (* we should also check that the name variable is anonymous in
253 the actual type de' ?? *)
255 ((Some (name,(C.Decl so)))::context)
256 metasenv subst left_args_no de' term' de ugraph1
257 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
258 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
260 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
263 let rec type_of_aux subst metasenv context t ugraph =
264 let module C = Cic in
265 let module S = CicSubstitution in
266 let module U = UriManager in
267 let (t',_,_,_,_) as res =
272 match List.nth context (n - 1) with
273 Some (_,C.Decl ty) ->
274 t,S.lift n ty,subst,metasenv, ugraph
275 | Some (_,C.Def (_,Some ty)) ->
276 t,S.lift n ty,subst,metasenv, ugraph
277 | Some (_,C.Def (bo,None)) ->
279 (* if it is in the context it must be already well-typed*)
280 CicTypeChecker.type_of_aux' ~subst metasenv context
283 t,ty,subst,metasenv,ugraph
285 enrich localization_tbl t
286 (RefineFailure (lazy "Rel to hidden hypothesis"))
289 enrich localization_tbl t
290 (RefineFailure (lazy "Not a close term")))
291 | C.Var (uri,exp_named_subst) ->
292 let exp_named_subst',subst',metasenv',ugraph1 =
293 check_exp_named_subst
294 subst metasenv context exp_named_subst ugraph
296 let ty_uri,ugraph1 = type_of_variable uri ugraph in
298 CicSubstitution.subst_vars exp_named_subst' ty_uri
300 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
303 let (canonical_context, term,ty) =
304 CicUtil.lookup_subst n subst
306 let l',subst',metasenv',ugraph1 =
307 check_metasenv_consistency n subst metasenv context
308 canonical_context l ugraph
310 (* trust or check ??? *)
311 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
312 subst', metasenv', ugraph1
313 (* type_of_aux subst metasenv
314 context (CicSubstitution.subst_meta l term) *)
315 with CicUtil.Subst_not_found _ ->
316 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
317 let l',subst',metasenv', ugraph1 =
318 check_metasenv_consistency n subst metasenv context
319 canonical_context l ugraph
321 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
322 subst', metasenv',ugraph1)
323 | C.Sort (C.Type tno) ->
324 let tno' = CicUniv.fresh() in
325 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
326 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
328 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
329 | C.Implicit infos ->
330 let metasenv',t' = exp_impl metasenv subst context infos in
331 type_of_aux subst metasenv' context t' ugraph
333 let ty',_,subst',metasenv',ugraph1 =
334 type_of_aux subst metasenv context ty ugraph
336 let te',inferredty,subst'',metasenv'',ugraph2 =
337 type_of_aux subst' metasenv' context te ugraph1
340 let subst''',metasenv''',ugraph3 =
341 fo_unif_subst subst'' context metasenv''
342 inferredty ty' ugraph2
344 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
347 enrich localization_tbl te'
350 CicMetaSubst.ppterm_in_context subst'' te'
351 context ^ " has type " ^
352 CicMetaSubst.ppterm_in_context subst'' inferredty
353 context ^ " but is here used with type " ^
354 CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
356 | C.Prod (name,s,t) ->
357 let carr t subst context = CicMetaSubst.apply_subst subst t in
358 let coerce_to_sort in_source tgt_sort t type_to_coerce
359 subst context metasenv uragph
361 if not !insert_coercions then
362 t,type_to_coerce,subst,metasenv,ugraph
364 let coercion_src = carr type_to_coerce subst context in
365 match coercion_src with
367 t,type_to_coerce,subst,metasenv,ugraph
368 | Cic.Meta _ as meta ->
369 t, meta, subst, metasenv, ugraph
370 | Cic.Cast _ as cast ->
371 t, cast, subst, metasenv, ugraph
373 let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
375 CoercGraph.look_for_coercion coercion_src coercion_tgt
378 | CoercGraph.NoCoercion
379 | CoercGraph.NotHandled _ ->
380 enrich localization_tbl t
383 CicMetaSubst.ppterm_in_context subst t context ^
384 " is not a type since it has type " ^
385 CicMetaSubst.ppterm_in_context
386 subst coercion_src context ^ " that is not a sort")))
387 | CoercGraph.NotMetaClosed ->
388 enrich localization_tbl t
391 CicMetaSubst.ppterm_in_context subst t context ^
392 " is not a type since it has type " ^
393 CicMetaSubst.ppterm_in_context
394 subst coercion_src context ^ " that is not a sort")))
395 | CoercGraph.SomeCoercion c ->
396 let newt,_,subst,metasenv,ugraph =
397 type_of_aux subst metasenv context (Cic.Appl[c;t])
399 let newt, tty, subst, metasenv, ugraph =
400 avoid_double_coercion context subst metasenv ugraph
403 newt, tty, subst, metasenv, ugraph)
405 let s',sort1,subst',metasenv',ugraph1 =
406 type_of_aux subst metasenv context s ugraph
408 let s',sort1,subst', metasenv',ugraph1 =
409 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
410 s' sort1 subst' context metasenv' ugraph1
412 let context_for_t = ((Some (name,(C.Decl s')))::context) in
413 let t',sort2,subst'',metasenv'',ugraph2 =
414 type_of_aux subst' metasenv'
415 context_for_t t ugraph1
417 let t',sort2,subst'',metasenv'',ugraph2 =
418 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
419 t' sort2 subst'' context_for_t metasenv'' ugraph2
421 let sop,subst''',metasenv''',ugraph3 =
422 sort_of_prod subst'' metasenv''
423 context (name,s') (sort1,sort2) ugraph2
425 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
426 | C.Lambda (n,s,t) ->
428 let s',sort1,subst',metasenv',ugraph1 =
429 type_of_aux subst metasenv context s ugraph in
430 let s',sort1,subst',metasenv',ugraph1 =
431 if not !insert_coercions then
432 s',sort1, subst', metasenv', ugraph1
434 match CicReduction.whd ~subst:subst' context sort1 with
435 | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
437 let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
439 CoercGraph.look_for_coercion coercion_src coercion_tgt
442 | CoercGraph.SomeCoercion c ->
443 let newt,_,subst',metasenv',ugraph1 =
444 type_of_aux subst' metasenv' context (Cic.Appl[c;s'])
446 let newt, tty, subst', metasenv', ugraph1 =
447 avoid_double_coercion context subst' metasenv'
448 ugraph1 newt coercion_tgt
450 newt, tty, subst', metasenv', ugraph1
451 | CoercGraph.NoCoercion
452 | CoercGraph.NotHandled _ ->
453 enrich localization_tbl s'
456 CicMetaSubst.ppterm_in_context subst s' context ^
457 " is not a type since it has type " ^
458 CicMetaSubst.ppterm_in_context
459 subst coercion_src context ^ " that is not a sort")))
460 | CoercGraph.NotMetaClosed ->
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")))
469 let context_for_t = ((Some (n,(C.Decl s')))::context) in
470 let t',type2,subst'',metasenv'',ugraph2 =
471 type_of_aux subst' metasenv' context_for_t t ugraph1
473 C.Lambda (n,s',t'),C.Prod (n,s',type2),
474 subst'',metasenv'',ugraph2
476 (* only to check if s is well-typed *)
477 let s',ty,subst',metasenv',ugraph1 =
478 type_of_aux subst metasenv context s ugraph
480 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
482 let t',inferredty,subst'',metasenv'',ugraph2 =
483 type_of_aux subst' metasenv'
484 context_for_t t ugraph1
486 (* One-step LetIn reduction.
487 * Even faster than the previous solution.
488 * Moreover the inferred type is closer to the expected one.
490 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
491 subst'',metasenv'',ugraph2
492 | C.Appl (he::((_::_) as tl)) ->
493 let he',hetype,subst',metasenv',ugraph1 =
494 type_of_aux subst metasenv context he ugraph
496 let tlbody_and_type,subst'',metasenv'',ugraph2 =
498 (fun x (res,subst,metasenv,ugraph) ->
499 let x',ty,subst',metasenv',ugraph1 =
500 type_of_aux subst metasenv context x ugraph
502 (x', ty)::res,subst',metasenv',ugraph1
503 ) tl ([],subst',metasenv',ugraph1)
505 let tl',applty,subst''',metasenv''',ugraph3 =
506 eat_prods true subst'' metasenv'' context
507 he' hetype tlbody_and_type ugraph2
509 avoid_double_coercion context
510 subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
511 | C.Appl _ -> assert false
512 | C.Const (uri,exp_named_subst) ->
513 let exp_named_subst',subst',metasenv',ugraph1 =
514 check_exp_named_subst subst metasenv context
515 exp_named_subst ugraph in
516 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
518 CicSubstitution.subst_vars exp_named_subst' ty_uri
520 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
521 | C.MutInd (uri,i,exp_named_subst) ->
522 let exp_named_subst',subst',metasenv',ugraph1 =
523 check_exp_named_subst subst metasenv context
524 exp_named_subst ugraph
526 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
528 CicSubstitution.subst_vars exp_named_subst' ty_uri in
529 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
530 | C.MutConstruct (uri,i,j,exp_named_subst) ->
531 let exp_named_subst',subst',metasenv',ugraph1 =
532 check_exp_named_subst subst metasenv context
533 exp_named_subst ugraph
536 type_of_mutual_inductive_constr uri i j ugraph1
539 CicSubstitution.subst_vars exp_named_subst' ty_uri
541 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
543 | C.MutCase (uri, i, outtype, term, pl) ->
544 (* first, get the inductive type (and noparams)
545 * in the environment *)
546 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
547 let _ = CicTypeChecker.typecheck uri in
548 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
550 C.InductiveDefinition (l,expl_params,parsno,_) ->
551 List.nth l i , expl_params, parsno, u
553 enrich localization_tbl t
555 (lazy ("Unkown mutual inductive definition " ^
556 U.string_of_uri uri)))
558 let rec count_prod t =
559 match CicReduction.whd ~subst context t with
560 C.Prod (_, _, t) -> 1 + (count_prod t)
563 let no_args = count_prod arity in
564 (* now, create a "generic" MutInd *)
565 let metasenv,left_args =
566 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
568 let metasenv,right_args =
569 let no_right_params = no_args - no_left_params in
570 if no_right_params < 0 then assert false
571 else CicMkImplicit.n_fresh_metas
572 metasenv subst context no_right_params
574 let metasenv,exp_named_subst =
575 CicMkImplicit.fresh_subst metasenv subst context expl_params in
578 C.MutInd (uri,i,exp_named_subst)
581 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
583 (* check consistency with the actual type of term *)
584 let term',actual_type,subst,metasenv,ugraph1 =
585 type_of_aux subst metasenv context term ugraph in
586 let expected_type',_, subst, metasenv,ugraph2 =
587 type_of_aux subst metasenv context expected_type ugraph1
589 let actual_type = CicReduction.whd ~subst context actual_type in
590 let subst,metasenv,ugraph3 =
592 fo_unif_subst subst context metasenv
593 expected_type' actual_type ugraph2
596 enrich localization_tbl term' exn
599 CicMetaSubst.ppterm_in_context subst term'
600 context ^ " has type " ^
601 CicMetaSubst.ppterm_in_context subst actual_type
602 context ^ " but is here used with type " ^
603 CicMetaSubst.ppterm_in_context subst expected_type' context))
605 let rec instantiate_prod t =
609 match CicReduction.whd ~subst context t with
611 instantiate_prod (CicSubstitution.subst he t') tl
614 let arity_instantiated_with_left_args =
615 instantiate_prod arity left_args in
616 (* TODO: check if the sort elimination
617 * is allowed: [(I q1 ... qr)|B] *)
618 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
620 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
622 if left_args = [] then
623 (C.MutConstruct (uri,i,j,exp_named_subst))
626 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
628 let p',actual_type,subst,metasenv,ugraph1 =
629 type_of_aux subst metasenv context p ugraph
631 let constructor',expected_type, subst, metasenv,ugraph2 =
632 type_of_aux subst metasenv context constructor ugraph1
634 let outtypeinstance,subst,metasenv,ugraph3 =
635 check_branch 0 context metasenv subst no_left_params
636 actual_type constructor' expected_type ugraph2
639 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
640 ([],1,[],subst,metasenv,ugraph3) pl
643 (* we are left to check that the outype matches his instances.
644 The easy case is when the outype is specified, that amount
645 to a trivial check. Otherwise, we should guess a type from
649 let outtype,outtypety, subst, metasenv,ugraph4 =
650 type_of_aux subst metasenv context outtype ugraph4 in
653 (let candidate,ugraph5,metasenv,subst =
654 let exp_name_subst, metasenv =
656 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
658 let uris = CicUtil.params_of_obj o in
660 fun uri (acc,metasenv) ->
661 let metasenv',new_meta =
662 CicMkImplicit.mk_implicit metasenv subst context
665 CicMkImplicit.identity_relocation_list_for_metavariable
668 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
672 match left_args,right_args with
673 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
675 let rec mk_right_args =
678 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
680 let right_args_no = List.length right_args in
681 let lifted_left_args =
682 List.map (CicSubstitution.lift right_args_no) left_args
684 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
685 (lifted_left_args @ mk_right_args right_args_no))
688 FreshNamesGenerator.mk_fresh_name ~subst metasenv
689 context Cic.Anonymous ~typ:ty
691 match outtypeinstances with
693 let extended_context =
694 let rec add_right_args =
696 Cic.Prod (name,ty,t) ->
697 Some (name,Cic.Decl ty)::(add_right_args t)
700 (Some (fresh_name,Cic.Decl ty))::
702 (add_right_args arity_instantiated_with_left_args))@
705 let metasenv,new_meta =
706 CicMkImplicit.mk_implicit metasenv subst extended_context
709 CicMkImplicit.identity_relocation_list_for_metavariable
712 let rec add_lambdas b =
714 Cic.Prod (name,ty,t) ->
715 Cic.Lambda (name,ty,(add_lambdas b t))
716 | _ -> Cic.Lambda (fresh_name, ty, b)
719 add_lambdas (Cic.Meta (new_meta,irl))
720 arity_instantiated_with_left_args
722 (Some candidate),ugraph4,metasenv,subst
723 | (constructor_args_no,_,instance,_)::tl ->
725 let instance',subst,metasenv =
726 CicMetaSubst.delift_rels subst metasenv
727 constructor_args_no instance
729 let candidate,ugraph,metasenv,subst =
731 fun (candidate_oty,ugraph,metasenv,subst)
732 (constructor_args_no,_,instance,_) ->
733 match candidate_oty with
734 | None -> None,ugraph,metasenv,subst
737 let instance',subst,metasenv =
738 CicMetaSubst.delift_rels subst metasenv
739 constructor_args_no instance
741 let subst,metasenv,ugraph =
742 fo_unif_subst subst context metasenv
745 candidate_oty,ugraph,metasenv,subst
747 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
748 | CicUnification.UnificationFailure _
749 | CicUnification.Uncertain _ ->
750 None,ugraph,metasenv,subst
751 ) (Some instance',ugraph4,metasenv,subst) tl
754 | None -> None, ugraph,metasenv,subst
756 let rec add_lambdas n b =
758 Cic.Prod (name,ty,t) ->
759 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
761 Cic.Lambda (fresh_name, ty,
762 CicSubstitution.lift (n + 1) t)
765 (add_lambdas 0 t arity_instantiated_with_left_args),
766 ugraph,metasenv,subst
767 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
768 None,ugraph4,metasenv,subst
771 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
773 let subst,metasenv,ugraph =
775 fo_unif_subst subst context metasenv
776 candidate outtype ugraph5
778 exn -> assert false(* unification against a metavariable *)
780 C.MutCase (uri, i, outtype, term', pl'),
781 CicReduction.head_beta_reduce
782 (CicMetaSubst.apply_subst subst
783 (Cic.Appl (outtype::right_args@[term']))),
784 subst,metasenv,ugraph)
785 | _ -> (* easy case *)
786 let tlbody_and_type,subst,metasenv,ugraph4 =
788 (fun x (res,subst,metasenv,ugraph) ->
789 let x',ty,subst',metasenv',ugraph1 =
790 type_of_aux subst metasenv context x ugraph
792 (x', ty)::res,subst',metasenv',ugraph1
793 ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
795 let _,_,subst,metasenv,ugraph4 =
796 eat_prods false subst metasenv context
797 outtype outtypety tlbody_and_type ugraph4
799 let _,_, subst, metasenv,ugraph5 =
800 type_of_aux subst metasenv context
801 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
803 let (subst,metasenv,ugraph6) =
805 (fun (subst,metasenv,ugraph)
806 p (constructor_args_no,context,instance,args)
811 CicSubstitution.lift constructor_args_no outtype
813 C.Appl (outtype'::args)
815 CicReduction.whd ~subst context appl
818 fo_unif_subst subst context metasenv instance instance'
822 enrich localization_tbl p exn
825 CicMetaSubst.ppterm_in_context subst p
826 context ^ " has type " ^
827 CicMetaSubst.ppterm_in_context subst instance'
828 context ^ " but is here used with type " ^
829 CicMetaSubst.ppterm_in_context subst instance
831 (subst,metasenv,ugraph5) pl' outtypeinstances
833 C.MutCase (uri, i, outtype, term', pl'),
834 CicReduction.head_beta_reduce
835 (CicMetaSubst.apply_subst subst
836 (C.Appl(outtype::right_args@[term]))),
837 subst,metasenv,ugraph6)
839 let fl_ty',subst,metasenv,types,ugraph1 =
841 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
842 let ty',_,subst',metasenv',ugraph1 =
843 type_of_aux subst metasenv context ty ugraph
845 fl @ [ty'],subst',metasenv',
846 Some (C.Name n,(C.Decl ty')) :: types, ugraph
847 ) ([],subst,metasenv,[],ugraph) fl
849 let len = List.length types in
850 let context' = types@context in
851 let fl_bo',subst,metasenv,ugraph2 =
853 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
854 let bo',ty_of_bo,subst,metasenv,ugraph1 =
855 type_of_aux subst metasenv context' bo ugraph in
856 let expected_ty = CicSubstitution.lift len ty in
857 let subst',metasenv',ugraph' =
859 fo_unif_subst subst context' metasenv
860 ty_of_bo expected_ty ugraph1
863 enrich localization_tbl bo exn
866 CicMetaSubst.ppterm_in_context subst bo
867 context' ^ " has type " ^
868 CicMetaSubst.ppterm_in_context subst ty_of_bo
869 context' ^ " but is here used with type " ^
870 CicMetaSubst.ppterm_in_context subst expected_ty
873 fl @ [bo'] , subst',metasenv',ugraph'
874 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
876 let ty = List.nth fl_ty' i in
877 (* now we have the new ty in fl_ty', the new bo in fl_bo',
878 * and we want the new fl with bo' and ty' injected in the right
881 let rec map3 f l1 l2 l3 =
884 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
887 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
890 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
892 let fl_ty',subst,metasenv,types,ugraph1 =
894 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
895 let ty',_,subst',metasenv',ugraph1 =
896 type_of_aux subst metasenv context ty ugraph
898 fl @ [ty'],subst',metasenv',
899 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
900 ) ([],subst,metasenv,[],ugraph) fl
902 let len = List.length types in
903 let context' = types@context in
904 let fl_bo',subst,metasenv,ugraph2 =
906 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
907 let bo',ty_of_bo,subst,metasenv,ugraph1 =
908 type_of_aux subst metasenv context' bo ugraph in
909 let expected_ty = CicSubstitution.lift len ty in
910 let subst',metasenv',ugraph' =
912 fo_unif_subst subst context' metasenv
913 ty_of_bo expected_ty ugraph1
916 enrich localization_tbl bo exn
919 CicMetaSubst.ppterm_in_context subst bo
920 context' ^ " has type " ^
921 CicMetaSubst.ppterm_in_context subst ty_of_bo
922 context' ^ " but is here used with type " ^
923 CicMetaSubst.ppterm_in_context subst expected_ty
926 fl @ [bo'],subst',metasenv',ugraph'
927 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
929 let ty = List.nth fl_ty' i in
930 (* now we have the new ty in fl_ty', the new bo in fl_bo',
931 * and we want the new fl with bo' and ty' injected in the right
934 let rec map3 f l1 l2 l3 =
937 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
940 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
943 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
945 relocalize localization_tbl t t';
948 (* check_metasenv_consistency checks that the "canonical" context of a
949 metavariable is consitent - up to relocation via the relocation list l -
950 with the actual context *)
951 and check_metasenv_consistency
952 metano subst metasenv context canonical_context l ugraph
954 let module C = Cic in
955 let module R = CicReduction in
956 let module S = CicSubstitution in
957 let lifted_canonical_context =
961 | (Some (n,C.Decl t))::tl ->
962 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
963 | (Some (n,C.Def (t,None)))::tl ->
964 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
965 | None::tl -> None::(aux (i+1) tl)
966 | (Some (n,C.Def (t,Some ty)))::tl ->
968 C.Def ((S.subst_meta l (S.lift i t)),
969 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
971 aux 1 canonical_context
975 (fun (l,subst,metasenv,ugraph) t ct ->
978 l @ [None],subst,metasenv,ugraph
979 | Some t,Some (_,C.Def (ct,_)) ->
980 let subst',metasenv',ugraph' =
982 fo_unif_subst subst context metasenv t ct ugraph
983 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))))))
985 l @ [Some t],subst',metasenv',ugraph'
986 | Some t,Some (_,C.Decl ct) ->
987 let t',inferredty,subst',metasenv',ugraph1 =
988 type_of_aux subst metasenv context t ugraph
990 let subst'',metasenv'',ugraph2 =
993 subst' context metasenv' inferredty ct ugraph1
994 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))))))
996 l @ [Some t'], subst'',metasenv'',ugraph2
998 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
1000 Invalid_argument _ ->
1004 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1005 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
1006 (CicMetaSubst.ppcontext subst canonical_context))))
1008 and check_exp_named_subst metasubst metasenv context tl ugraph =
1009 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1011 [] -> [],metasubst,metasenv,ugraph
1013 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1015 CicSubstitution.subst_vars substs ty_uri in
1016 (* CSC: why was this code here? it is wrong
1017 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1018 Cic.Variable (_,Some bo,_,_) ->
1020 (RefineFailure (lazy
1021 "A variable with a body can not be explicit substituted"))
1022 | Cic.Variable (_,None,_,_) -> ()
1025 (RefineFailure (lazy
1026 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1029 let t',typeoft,metasubst',metasenv',ugraph2 =
1030 type_of_aux metasubst metasenv context t ugraph1 in
1031 let subst = uri,t' in
1032 let metasubst'',metasenv'',ugraph3 =
1035 metasubst' context metasenv' typeoft typeofvar ugraph2
1037 raise (RefineFailure (lazy
1038 ("Wrong Explicit Named Substitution: " ^
1039 CicMetaSubst.ppterm metasubst' typeoft ^
1040 " not unifiable with " ^
1041 CicMetaSubst.ppterm metasubst' typeofvar)))
1043 (* FIXME: no mere tail recursive! *)
1044 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1045 check_exp_named_subst_aux
1046 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1048 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1050 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1053 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
1054 let module C = Cic in
1055 let context_for_t2 = (Some (name,C.Decl s))::context in
1056 let t1'' = CicReduction.whd ~subst context t1 in
1057 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1058 match (t1'', t2'') with
1059 (C.Sort s1, C.Sort s2)
1060 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1061 (* different than Coq manual!!! *)
1062 C.Sort s2,subst,metasenv,ugraph
1063 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1064 let t' = CicUniv.fresh() in
1065 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1066 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1067 C.Sort (C.Type t'),subst,metasenv,ugraph2
1068 | (C.Sort _,C.Sort (C.Type t1)) ->
1069 C.Sort (C.Type t1),subst,metasenv,ugraph
1070 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1071 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1072 (* TODO how can we force the meta to become a sort? If we don't we
1073 * break the invariant that refine produce only well typed terms *)
1074 (* TODO if we check the non meta term and if it is a sort then we
1075 * are likely to know the exact value of the result e.g. if the rhs
1076 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1077 let (metasenv,idx) =
1078 CicMkImplicit.mk_implicit_sort metasenv subst in
1079 let (subst, metasenv,ugraph1) =
1081 fo_unif_subst subst context_for_t2 metasenv
1082 (C.Meta (idx,[])) t2'' ugraph
1083 with _ -> assert false (* unification against a metavariable *)
1085 t2'',subst,metasenv,ugraph1
1091 ("Two sorts were expected, found %s " ^^
1092 "(that reduces to %s) and %s (that reduces to %s)")
1093 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
1094 (CicPp.ppterm t2''))))
1096 and avoid_double_coercion context subst metasenv ugraph t ty =
1097 let b, c1, c2, head = is_a_double_coercion t in
1099 let source_carr = CoercGraph.source_of c2 in
1100 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1101 (match CoercGraph.look_for_coercion source_carr tgt_carr
1103 | CoercGraph.SomeCoercion c ->
1106 Cic.Appl l -> Cic.Appl (l @ [head])
1107 | _ -> Cic.Appl [c;head]
1110 let newt,_,subst,metasenv,ugraph =
1111 type_of_aux subst metasenv context newt ugraph in
1112 let subst, metasenv, ugraph =
1113 fo_unif_subst subst context metasenv newt t ugraph
1118 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
1119 newt, ty, subst, metasenv, ugraph
1122 prerr_endline ("#### Coercion not packed (Refine_failure): " ^
1123 CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
1126 prerr_endline ("#### Coercion not packed (Uncerctain case): " ^
1127 CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
1129 | _ -> assert false) (* the composite coercion must exist *)
1131 t, ty, subst, metasenv, ugraph
1134 allow_coercions subst metasenv context he hetype tlbody_and_type ugraph
1136 let rec mk_prod metasenv context' =
1139 let (metasenv, idx) =
1140 CicMkImplicit.mk_implicit_type metasenv subst context'
1143 CicMkImplicit.identity_relocation_list_for_metavariable context'
1145 metasenv,Cic.Meta (idx, irl)
1147 let (metasenv, idx) =
1148 CicMkImplicit.mk_implicit_type metasenv subst context'
1151 CicMkImplicit.identity_relocation_list_for_metavariable context'
1153 let meta = Cic.Meta (idx,irl) in
1155 (* The name must be fresh for context. *)
1156 (* Nevertheless, argty is well-typed only in context. *)
1157 (* Thus I generate a name (name_hint) in context and *)
1158 (* then I generate a name --- using the hint name_hint *)
1159 (* --- that is fresh in context'. *)
1161 (* Cic.Name "pippo" *)
1162 FreshNamesGenerator.mk_fresh_name ~subst metasenv
1163 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
1164 (CicMetaSubst.apply_subst_context subst context)
1166 ~typ:(CicMetaSubst.apply_subst subst argty)
1168 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
1169 FreshNamesGenerator.mk_fresh_name ~subst
1170 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
1172 let metasenv,target =
1173 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
1175 metasenv,Cic.Prod (name,meta,target)
1177 let ((subst,metasenv,ugraph1),hetype') =
1178 if CicUtil.is_meta_closed hetype then
1179 (subst,metasenv,ugraph),hetype
1181 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
1183 fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph, hetype'
1185 enrich localization_tbl he
1187 (lazy ("The term " ^
1188 CicMetaSubst.ppterm_in_context subst he
1189 context ^ " (that has type " ^
1190 CicMetaSubst.ppterm_in_context subst hetype
1191 context ^ ") is here applied to " ^
1192 string_of_int (List.length tlbody_and_type) ^
1193 " arguments that are more than expected"
1194 (* "\nReason: " ^ Lazy.force exn*)))) exn
1196 let rec eat_prods metasenv subst context hetype ugraph =
1198 | [] -> [],metasenv,subst,hetype,ugraph
1199 | (hete, hety)::tl ->
1200 (match (CicReduction.whd ~subst context hetype) with
1202 let arg,subst,metasenv,ugraph1 =
1204 let subst,metasenv,ugraph1 =
1205 fo_unif_subst_eat_prods2 subst context metasenv hety s ugraph
1207 hete,subst,metasenv,ugraph1
1208 with exn when allow_coercions && !insert_coercions ->
1209 (* we search a coercion from hety to s *)
1210 let coer, tgt_carr =
1211 let carr t subst context =
1212 CicReduction.whd ~delta:false
1213 context (CicMetaSubst.apply_subst subst t )
1215 let c_hety = carr hety subst context in
1216 let c_s = carr s subst context in
1217 CoercGraph.look_for_coercion c_hety c_s, c_s
1220 | CoercGraph.NoCoercion
1221 | CoercGraph.NotHandled _ ->
1222 enrich localization_tbl hete
1224 (lazy ("The term " ^
1225 CicMetaSubst.ppterm_in_context subst hete
1226 context ^ " has type " ^
1227 CicMetaSubst.ppterm_in_context subst hety
1228 context ^ " but is here used with type " ^
1229 CicMetaSubst.ppterm_in_context subst s context
1230 (* "\nReason: " ^ Lazy.force e*))))
1231 | CoercGraph.NotMetaClosed ->
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*))))
1241 | CoercGraph.SomeCoercion c ->
1243 let newt,newhety,subst,metasenv,ugraph =
1244 type_of_aux subst metasenv context
1245 (Cic.Appl[c;hete]) ugraph in
1246 let newt, _, subst, metasenv, ugraph =
1247 avoid_double_coercion context subst metasenv
1248 ugraph newt tgt_carr in
1249 let subst,metasenv,ugraph1 =
1250 fo_unif_subst subst context metasenv
1253 newt, subst, metasenv, ugraph
1255 enrich localization_tbl hete
1257 (lazy ("The term " ^
1258 CicMetaSubst.ppterm_in_context subst hete
1259 context ^ " has type " ^
1260 CicMetaSubst.ppterm_in_context subst hety
1261 context ^ " but is here used with type " ^
1262 CicMetaSubst.ppterm_in_context subst s context
1263 (* "\nReason: " ^ Lazy.force e*)))) exn)
1265 enrich localization_tbl hete
1267 (lazy ("The term " ^
1268 CicMetaSubst.ppterm_in_context subst hete
1269 context ^ " has type " ^
1270 CicMetaSubst.ppterm_in_context subst hety
1271 context ^ " but is here used with type " ^
1272 CicMetaSubst.ppterm_in_context subst s context
1273 (* "\nReason: " ^ Lazy.force e*)))) exn
1275 let coerced_args,metasenv',subst',t',ugraph2 =
1276 eat_prods metasenv subst context
1277 (CicSubstitution.subst arg t) ugraph1 tl
1279 arg::coerced_args,metasenv',subst',t',ugraph2
1281 raise (RefineFailure
1282 (lazy ("The term " ^
1283 CicMetaSubst.ppterm_in_context subst he
1284 context ^ " (that has type " ^
1285 CicMetaSubst.ppterm_in_context subst hetype'
1286 context ^ ") is here applied to " ^
1287 string_of_int (List.length tlbody_and_type) ^
1288 " arguments that are more than expected"))))
1290 let coerced_args,metasenv,subst,t,ugraph2 =
1291 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
1293 coerced_args,t,subst,metasenv,ugraph2
1296 (* eat prods ends here! *)
1298 let t',ty,subst',metasenv',ugraph1 =
1299 type_of_aux [] metasenv context t ugraph
1301 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1302 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1303 (* Andrea: ho rimesso qui l'applicazione della subst al
1304 metasenv dopo che ho droppato l'invariante che il metsaenv
1305 e' sempre istanziato *)
1306 let substituted_metasenv =
1307 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1309 (* substituted_t,substituted_ty,substituted_metasenv *)
1310 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1312 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1314 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1315 let cleaned_metasenv =
1317 (function (n,context,ty) ->
1318 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1323 | Some (n, Cic.Decl t) ->
1325 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1326 | Some (n, Cic.Def (bo,ty)) ->
1327 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1332 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1334 Some (n, Cic.Def (bo',ty'))
1338 ) substituted_metasenv
1340 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1343 let undebrujin uri typesno tys t =
1346 (fun (name,_,_,_) (i,t) ->
1347 (* here the explicit_named_substituion is assumed to be *)
1349 let t' = Cic.MutInd (uri,i,[]) in
1350 let t = CicSubstitution.subst t' t in
1352 ) tys (typesno - 1,t))
1354 let map_first_n n start f g l =
1355 let rec aux acc k l =
1358 | [] -> raise (Invalid_argument "map_first_n")
1359 | hd :: tl -> f hd k (aux acc (k+1) tl)
1365 (*CSC: this is a very rough approximation; to be finished *)
1366 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1367 let subst,metasenv,ugraph,tys =
1369 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1370 let subst,metasenv,ugraph,cl =
1372 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1373 let rec aux ctx k subst = function
1374 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1375 let subst,metasenv,ugraph,tl =
1377 (subst,metasenv,ugraph,[])
1378 (fun t n (subst,metasenv,ugraph,acc) ->
1379 let subst,metasenv,ugraph =
1381 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1383 subst,metasenv,ugraph,(t::acc))
1384 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1387 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1388 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1389 subst,metasenv,ugraph,t
1390 | Cic.Prod (name,s,t) ->
1391 let ctx = (Some (name,Cic.Decl s))::ctx in
1392 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1393 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1397 (lazy "not well formed constructor type"))
1399 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1400 subst,metasenv,ugraph,(name,ty) :: acc)
1401 cl (subst,metasenv,ugraph,[])
1403 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1404 tys ([],metasenv,ugraph,[])
1406 let substituted_tys =
1408 (fun (name,ind,arity,cl) ->
1410 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1412 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1415 metasenv,ugraph,substituted_tys
1417 let typecheck metasenv uri obj ~localization_tbl =
1418 let ugraph = CicUniv.empty_ugraph in
1420 Cic.Constant (name,Some bo,ty,args,attrs) ->
1421 let bo',boty,metasenv,ugraph =
1422 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1423 let ty',_,metasenv,ugraph =
1424 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1425 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1426 let bo' = CicMetaSubst.apply_subst subst bo' in
1427 let ty' = CicMetaSubst.apply_subst subst ty' in
1428 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1429 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1430 | Cic.Constant (name,None,ty,args,attrs) ->
1431 let ty',_,metasenv,ugraph =
1432 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1434 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1435 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1436 assert (metasenv' = metasenv);
1437 (* Here we do not check the metasenv for correctness *)
1438 let bo',boty,metasenv,ugraph =
1439 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1440 let ty',sort,metasenv,ugraph =
1441 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1445 (* instead of raising Uncertain, let's hope that the meta will become
1448 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1450 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1451 let bo' = CicMetaSubst.apply_subst subst bo' in
1452 let ty' = CicMetaSubst.apply_subst subst ty' in
1453 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1454 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1455 | Cic.Variable _ -> assert false (* not implemented *)
1456 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1457 (*CSC: this code is greately simplified and many many checks are missing *)
1458 (*CSC: e.g. the constructors are not required to build their own types, *)
1459 (*CSC: the arities are not required to have as type a sort, etc. *)
1460 let uri = match uri with Some uri -> uri | None -> assert false in
1461 let typesno = List.length tys in
1462 (* first phase: we fix only the types *)
1463 let metasenv,ugraph,tys =
1465 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1466 let ty',_,metasenv,ugraph =
1467 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1469 metasenv,ugraph,(name,b,ty',cl)::res
1470 ) tys (metasenv,ugraph,[]) in
1472 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1473 (* second phase: we fix only the constructors *)
1474 let metasenv,ugraph,tys =
1476 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1477 let metasenv,ugraph,cl' =
1479 (fun (name,ty) (metasenv,ugraph,res) ->
1481 CicTypeChecker.debrujin_constructor
1482 ~cb:(relocalize localization_tbl) uri typesno ty in
1483 let ty',_,metasenv,ugraph =
1484 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1485 let ty' = undebrujin uri typesno tys ty' in
1486 metasenv,ugraph,(name,ty')::res
1487 ) cl (metasenv,ugraph,[])
1489 metasenv,ugraph,(name,b,ty,cl')::res
1490 ) tys (metasenv,ugraph,[]) in
1491 (* third phase: we check the positivity condition *)
1492 let metasenv,ugraph,tys =
1493 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1495 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1498 (* sara' piu' veloce che raffinare da zero? mah.... *)
1499 let pack_coercion metasenv ctx t =
1500 let module C = Cic in
1501 let rec merge_coercions ctx =
1502 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1504 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1505 | C.Meta (n,subst) ->
1508 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1511 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1512 | C.Prod (name,so,dest) ->
1513 let ctx' = (Some (name,C.Decl so))::ctx in
1514 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1515 | C.Lambda (name,so,dest) ->
1516 let ctx' = (Some (name,C.Decl so))::ctx in
1517 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1518 | C.LetIn (name,so,dest) ->
1519 let ctx' = Some (name,(C.Def (so,None)))::ctx in
1520 C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1522 let l = List.map (merge_coercions ctx) l in
1524 let b,_,_,_ = is_a_double_coercion t in
1525 (* prerr_endline "CANDIDATO!!!!"; *)
1527 let ugraph = CicUniv.empty_ugraph in
1528 let old_insert_coercions = !insert_coercions in
1529 insert_coercions := false;
1530 let newt, _, menv, _ =
1532 type_of_aux' metasenv ctx t ugraph
1533 with RefineFailure _ | Uncertain _ ->
1534 prerr_endline (CicPp.ppterm t);
1537 insert_coercions := old_insert_coercions;
1538 if metasenv <> [] || menv = [] then
1541 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1544 | C.Var (uri,exp_named_subst) ->
1545 let exp_named_subst = List.map aux exp_named_subst in
1546 C.Var (uri, exp_named_subst)
1547 | C.Const (uri,exp_named_subst) ->
1548 let exp_named_subst = List.map aux exp_named_subst in
1549 C.Const (uri, exp_named_subst)
1550 | C.MutInd (uri,tyno,exp_named_subst) ->
1551 let exp_named_subst = List.map aux exp_named_subst in
1552 C.MutInd (uri,tyno,exp_named_subst)
1553 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1554 let exp_named_subst = List.map aux exp_named_subst in
1555 C.MutConstruct (uri,tyno,consno,exp_named_subst)
1556 | C.MutCase (uri,tyno,out,te,pl) ->
1557 let pl = List.map (merge_coercions ctx) pl in
1558 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1559 | C.Fix (fno, fl) ->
1562 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1567 (fun (name,idx,ty,bo) ->
1568 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1572 | C.CoFix (fno, fl) ->
1575 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1580 (fun (name,ty,bo) ->
1581 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1586 merge_coercions ctx t
1589 let pack_coercion_obj obj =
1590 let module C = Cic in
1592 | C.Constant (id, body, ty, params, attrs) ->
1596 | Some body -> Some (pack_coercion [] [] body)
1598 let ty = pack_coercion [] [] ty in
1599 C.Constant (id, body, ty, params, attrs)
1600 | C.Variable (name, body, ty, params, attrs) ->
1604 | Some body -> Some (pack_coercion [] [] body)
1606 let ty = pack_coercion [] [] ty in
1607 C.Variable (name, body, ty, params, attrs)
1608 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1611 (fun (i, ctx, ty) ->
1617 Some (name, C.Decl t) ->
1618 Some (name, C.Decl (pack_coercion conjectures ctx t))
1619 | Some (name, C.Def (t,None)) ->
1620 Some (name,C.Def (pack_coercion conjectures ctx t,None))
1621 | Some (name, C.Def (t,Some ty)) ->
1622 Some (name, C.Def (pack_coercion conjectures ctx t,
1623 Some (pack_coercion conjectures ctx ty)))
1629 ((i,ctx,pack_coercion conjectures ctx ty))
1632 let body = pack_coercion conjectures [] body in
1633 let ty = pack_coercion conjectures [] ty in
1634 C.CurrentProof (name, conjectures, body, ty, params, attrs)
1635 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1638 (fun (name, ind, arity, cl) ->
1639 let arity = pack_coercion [] [] arity in
1641 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
1643 (name, ind, arity, cl))
1646 C.InductiveDefinition (indtys, params, leftno, attrs)
1651 let type_of_aux' metasenv context term =
1654 type_of_aux' metasenv context term in
1656 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1658 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1661 | RefineFailure msg as e ->
1662 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1664 | Uncertain msg as e ->
1665 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1669 let profiler2 = HExtlib.profile "CicRefine"
1671 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1672 profiler2.HExtlib.profile
1673 (type_of_aux' ?localization_tbl metasenv context term) ugraph
1675 let typecheck ~localization_tbl metasenv uri obj =
1676 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
1678 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;