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/.
28 exception RefineFailure of string Lazy.t;;
29 exception Uncertain of string Lazy.t;;
30 exception AssertFailure of string Lazy.t;;
32 let debug_print = fun _ -> ()
34 let profiler = HExtlib.profile "CicRefine.fo_unif"
36 let fo_unif_subst subst context metasenv t1 t2 ugraph =
39 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
40 in profiler.HExtlib.profile foo ()
42 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
43 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
46 let enrich localization_tbl t f exn =
49 RefineFailure msg -> RefineFailure (f msg)
50 | Uncertain msg -> Uncertain (f msg)
51 | _ -> assert false in
54 Cic.CicHash.find localization_tbl t
56 (* prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); *)
59 raise (HExtlib.Localized (loc,exn'))
61 let relocalize localization_tbl oldt newt =
63 let infos = Cic.CicHash.find localization_tbl oldt in
64 Cic.CicHash.remove localization_tbl oldt;
65 Cic.CicHash.add localization_tbl newt infos;
73 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
74 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
77 let exp_impl metasenv subst context =
80 let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
81 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
82 metasenv', Cic.Meta (idx, irl)
84 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
85 metasenv', Cic.Meta (idx, [])
87 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
88 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
89 metasenv', Cic.Meta (idx, irl)
93 let rec type_of_constant uri ugraph =
95 let module R = CicReduction in
96 let module U = UriManager in
97 let _ = CicTypeChecker.typecheck uri in
100 CicEnvironment.get_cooked_obj ugraph uri
101 with Not_found -> assert false
104 C.Constant (_,_,ty,_,_) -> ty,u
105 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
108 (RefineFailure (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
110 and type_of_variable uri ugraph =
111 let module C = Cic in
112 let module R = CicReduction in
113 let module U = UriManager in
114 let _ = CicTypeChecker.typecheck uri in
117 CicEnvironment.get_cooked_obj ugraph uri
118 with Not_found -> assert false
121 C.Variable (_,_,ty,_,_) -> ty,u
125 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
127 and type_of_mutual_inductive_defs uri i ugraph =
128 let module C = Cic in
129 let module R = CicReduction in
130 let module U = UriManager in
131 let _ = CicTypeChecker.typecheck uri in
134 CicEnvironment.get_cooked_obj ugraph uri
135 with Not_found -> assert false
138 C.InductiveDefinition (dl,_,_,_) ->
139 let (_,_,arity,_) = List.nth dl i in
144 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
146 and type_of_mutual_inductive_constr uri i j ugraph =
147 let module C = Cic in
148 let module R = CicReduction in
149 let module U = UriManager in
150 let _ = CicTypeChecker.typecheck uri in
153 CicEnvironment.get_cooked_obj ugraph uri
154 with Not_found -> assert false
157 C.InductiveDefinition (dl,_,_,_) ->
158 let (_,_,_,cl) = List.nth dl i in
159 let (_,ty) = List.nth cl (j-1) in
165 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
168 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
170 (* the check_branch function checks if a branch of a case is refinable.
171 It returns a pair (outype_instance,args), a subst and a metasenv.
172 outype_instance is the expected result of applying the case outtype
174 The problem is that outype is in general unknown, and we should
175 try to synthesize it from the above information, that is in general
176 a second order unification problem. *)
178 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
179 let module C = Cic in
180 (* let module R = CicMetaSubst in *)
181 let module R = CicReduction in
182 match R.whd ~subst context expectedtype with
184 (n,context,actualtype, [term]), subst, metasenv, ugraph
185 | C.Appl (C.MutInd (_,_,_)::tl) ->
186 let (_,arguments) = split tl left_args_no in
187 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
188 | C.Prod (name,so,de) ->
189 (* we expect that the actual type of the branch has the due
191 (match R.whd ~subst context actualtype with
192 C.Prod (name',so',de') ->
193 let subst, metasenv, ugraph1 =
194 fo_unif_subst subst context metasenv so so' ugraph in
196 (match CicSubstitution.lift 1 term with
197 C.Appl l -> C.Appl (l@[C.Rel 1])
198 | t -> C.Appl [t ; C.Rel 1]) in
199 (* we should also check that the name variable is anonymous in
200 the actual type de' ?? *)
202 ((Some (name,(C.Decl so)))::context)
203 metasenv subst left_args_no de' term' de ugraph1
204 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
205 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
207 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
210 let rec type_of_aux subst metasenv context t ugraph =
211 let module C = Cic in
212 let module S = CicSubstitution in
213 let module U = UriManager in
214 let (t',_,_,_,_) as res =
219 match List.nth context (n - 1) with
220 Some (_,C.Decl ty) ->
221 t,S.lift n ty,subst,metasenv, ugraph
222 | Some (_,C.Def (_,Some ty)) ->
223 t,S.lift n ty,subst,metasenv, ugraph
224 | Some (_,C.Def (bo,None)) ->
226 (* if it is in the context it must be already well-typed*)
227 CicTypeChecker.type_of_aux' ~subst metasenv context
230 t,ty,subst,metasenv,ugraph
231 | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis"))
233 _ -> raise (RefineFailure (lazy "Not a close term")))
234 | C.Var (uri,exp_named_subst) ->
235 let exp_named_subst',subst',metasenv',ugraph1 =
236 check_exp_named_subst
237 subst metasenv context exp_named_subst ugraph
239 let ty_uri,ugraph1 = type_of_variable uri ugraph in
241 CicSubstitution.subst_vars exp_named_subst' ty_uri
243 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
246 let (canonical_context, term,ty) =
247 CicUtil.lookup_subst n subst
249 let l',subst',metasenv',ugraph1 =
250 check_metasenv_consistency n subst metasenv context
251 canonical_context l ugraph
253 (* trust or check ??? *)
254 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
255 subst', metasenv', ugraph1
256 (* type_of_aux subst metasenv
257 context (CicSubstitution.subst_meta l term) *)
258 with CicUtil.Subst_not_found _ ->
259 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
260 let l',subst',metasenv', ugraph1 =
261 check_metasenv_consistency n subst metasenv context
262 canonical_context l ugraph
264 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
265 subst', metasenv',ugraph1)
266 | C.Sort (C.Type tno) ->
267 let tno' = CicUniv.fresh() in
268 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
269 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
271 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
272 | C.Implicit infos ->
273 let metasenv',t' = exp_impl metasenv subst context infos in
274 type_of_aux subst metasenv' context t' ugraph
276 let ty',_,subst',metasenv',ugraph1 =
277 type_of_aux subst metasenv context ty ugraph
279 let te',inferredty,subst'',metasenv'',ugraph2 =
280 type_of_aux subst' metasenv' context te ugraph1
282 let subst''',metasenv''',ugraph3 =
283 fo_unif_subst subst'' context metasenv''
284 inferredty ty' ugraph2
286 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
287 | C.Prod (name,s,t) ->
288 let carr t subst context = CicMetaSubst.apply_subst subst t in
290 in_source tgt_sort t type_to_coerce subst ctx metasenv uragph
292 let coercion_src = carr type_to_coerce subst ctx in
293 match coercion_src with
295 t,type_to_coerce,subst,metasenv,ugraph
297 | Cic.Meta _ as meta when not in_source ->
298 let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
299 let subst, metasenv, ugraph =
301 subst ctx metasenv meta coercion_tgt ugraph
303 t, Cic.Sort tgt_sort, subst, metasenv, ugraph
305 | Cic.Meta _ as meta ->
306 t, meta, subst, metasenv, ugraph
307 | Cic.Cast _ as cast ->
308 t, cast, subst, metasenv, ugraph
310 let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
311 let search = CoercGraph.look_for_coercion in
312 let boh = search coercion_src coercion_tgt in
314 | CoercGraph.NoCoercion
315 | CoercGraph.NotHandled _ ->
317 (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
318 | CoercGraph.NotMetaClosed ->
320 (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
321 | CoercGraph.SomeCoercion c ->
322 Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
324 let s',sort1,subst',metasenv',ugraph1 =
325 type_of_aux subst metasenv context s ugraph
327 let s',sort1,subst', metasenv',ugraph1 =
328 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
329 s' sort1 subst' context metasenv' ugraph1
331 let context_for_t = ((Some (name,(C.Decl s')))::context) in
332 let t',sort2,subst'',metasenv'',ugraph2 =
333 type_of_aux subst' metasenv'
334 context_for_t t ugraph1
336 let t',sort2,subst'',metasenv'',ugraph2 =
337 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
338 t' sort2 subst'' context_for_t metasenv'' ugraph2
340 let sop,subst''',metasenv''',ugraph3 =
341 sort_of_prod subst'' metasenv''
342 context (name,s') (sort1,sort2) ugraph2
344 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
345 | C.Lambda (n,s,t) ->
347 let s',sort1,subst',metasenv',ugraph1 =
348 type_of_aux subst metasenv context s ugraph in
350 match CicReduction.whd ~subst:subst' context sort1 with
352 | C.Sort _ -> s',sort1
354 let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh ())) in
355 let search = CoercGraph.look_for_coercion in
356 let boh = search coercion_src coercion_tgt in
358 | CoercGraph.SomeCoercion c ->
359 Cic.Appl [c;s'], coercion_tgt
360 | CoercGraph.NoCoercion
361 | CoercGraph.NotHandled _
362 | CoercGraph.NotMetaClosed ->
363 raise (RefineFailure (lazy (sprintf
364 "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1))))
366 let context_for_t = ((Some (n,(C.Decl s')))::context) in
367 let t',type2,subst'',metasenv'',ugraph2 =
368 type_of_aux subst' metasenv' context_for_t t ugraph1
370 C.Lambda (n,s',t'),C.Prod (n,s',type2),
371 subst'',metasenv'',ugraph2
373 (* only to check if s is well-typed *)
374 let s',ty,subst',metasenv',ugraph1 =
375 type_of_aux subst metasenv context s ugraph
377 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
379 let t',inferredty,subst'',metasenv'',ugraph2 =
380 type_of_aux subst' metasenv'
381 context_for_t t ugraph1
383 (* One-step LetIn reduction.
384 * Even faster than the previous solution.
385 * Moreover the inferred type is closer to the expected one.
387 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
388 subst'',metasenv'',ugraph2
389 | C.Appl (he::((_::_) as tl)) ->
390 let he',hetype,subst',metasenv',ugraph1 =
391 type_of_aux subst metasenv context he ugraph
393 let tlbody_and_type,subst'',metasenv'',ugraph2 =
395 (fun x (res,subst,metasenv,ugraph) ->
396 let x',ty,subst',metasenv',ugraph1 =
397 type_of_aux subst metasenv context x ugraph
399 (x', ty)::res,subst',metasenv',ugraph1
400 ) tl ([],subst',metasenv',ugraph1)
402 let tl',applty,subst''',metasenv''',ugraph3 =
403 eat_prods true subst'' metasenv'' context
404 hetype tlbody_and_type ugraph2
406 C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
407 | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
408 | C.Const (uri,exp_named_subst) ->
409 let exp_named_subst',subst',metasenv',ugraph1 =
410 check_exp_named_subst subst metasenv context
411 exp_named_subst ugraph in
412 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
414 CicSubstitution.subst_vars exp_named_subst' ty_uri
416 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
417 | C.MutInd (uri,i,exp_named_subst) ->
418 let exp_named_subst',subst',metasenv',ugraph1 =
419 check_exp_named_subst subst metasenv context
420 exp_named_subst ugraph
422 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
424 CicSubstitution.subst_vars exp_named_subst' ty_uri in
425 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
426 | C.MutConstruct (uri,i,j,exp_named_subst) ->
427 let exp_named_subst',subst',metasenv',ugraph1 =
428 check_exp_named_subst subst metasenv context
429 exp_named_subst ugraph
432 type_of_mutual_inductive_constr uri i j ugraph1
435 CicSubstitution.subst_vars exp_named_subst' ty_uri
437 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
439 | C.MutCase (uri, i, outtype, term, pl) ->
440 (* first, get the inductive type (and noparams)
441 * in the environment *)
442 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
443 let _ = CicTypeChecker.typecheck uri in
444 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
446 C.InductiveDefinition (l,expl_params,parsno,_) ->
447 List.nth l i , expl_params, parsno, u
451 (lazy ("Unkown mutual inductive definition " ^
452 U.string_of_uri uri)))
454 let rec count_prod t =
455 match CicReduction.whd ~subst context t with
456 C.Prod (_, _, t) -> 1 + (count_prod t)
459 let no_args = count_prod arity in
460 (* now, create a "generic" MutInd *)
461 let metasenv,left_args =
462 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
464 let metasenv,right_args =
465 let no_right_params = no_args - no_left_params in
466 if no_right_params < 0 then assert false
467 else CicMkImplicit.n_fresh_metas
468 metasenv subst context no_right_params
470 let metasenv,exp_named_subst =
471 CicMkImplicit.fresh_subst metasenv subst context expl_params in
474 C.MutInd (uri,i,exp_named_subst)
477 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
479 (* check consistency with the actual type of term *)
480 let term',actual_type,subst,metasenv,ugraph1 =
481 type_of_aux subst metasenv context term ugraph in
482 let expected_type',_, subst, metasenv,ugraph2 =
483 type_of_aux subst metasenv context expected_type ugraph1
485 let actual_type = CicReduction.whd ~subst context actual_type in
486 let subst,metasenv,ugraph3 =
487 fo_unif_subst subst context metasenv
488 expected_type' actual_type ugraph2
490 let rec instantiate_prod t =
494 match CicReduction.whd ~subst context t with
496 instantiate_prod (CicSubstitution.subst he t') tl
499 let arity_instantiated_with_left_args =
500 instantiate_prod arity left_args in
501 (* TODO: check if the sort elimination
502 * is allowed: [(I q1 ... qr)|B] *)
503 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
505 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
507 if left_args = [] then
508 (C.MutConstruct (uri,i,j,exp_named_subst))
511 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
513 let p',actual_type,subst,metasenv,ugraph1 =
514 type_of_aux subst metasenv context p ugraph
516 let constructor',expected_type, subst, metasenv,ugraph2 =
517 type_of_aux subst metasenv context constructor ugraph1
519 let outtypeinstance,subst,metasenv,ugraph3 =
520 check_branch 0 context metasenv subst no_left_params
521 actual_type constructor' expected_type ugraph2
524 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
525 ([],1,[],subst,metasenv,ugraph3) pl
528 (* we are left to check that the outype matches his instances.
529 The easy case is when the outype is specified, that amount
530 to a trivial check. Otherwise, we should guess a type from
534 let outtype,outtypety, subst, metasenv,ugraph4 =
535 type_of_aux subst metasenv context outtype ugraph4 in
538 (let candidate,ugraph5,metasenv,subst =
539 let exp_name_subst, metasenv =
541 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
543 let uris = CicUtil.params_of_obj o in
545 fun uri (acc,metasenv) ->
546 let metasenv',new_meta =
547 CicMkImplicit.mk_implicit metasenv subst context
550 CicMkImplicit.identity_relocation_list_for_metavariable
553 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
557 match left_args,right_args with
558 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
560 let rec mk_right_args =
563 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
565 let right_args_no = List.length right_args in
566 let lifted_left_args =
567 List.map (CicSubstitution.lift right_args_no) left_args
569 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
570 (lifted_left_args @ mk_right_args right_args_no))
573 FreshNamesGenerator.mk_fresh_name ~subst metasenv
574 context Cic.Anonymous ~typ:ty
576 match outtypeinstances with
578 let extended_context =
579 let rec add_right_args =
581 Cic.Prod (name,ty,t) ->
582 Some (name,Cic.Decl ty)::(add_right_args t)
585 (Some (fresh_name,Cic.Decl ty))::
587 (add_right_args arity_instantiated_with_left_args))@
590 let metasenv,new_meta =
591 CicMkImplicit.mk_implicit metasenv subst extended_context
594 CicMkImplicit.identity_relocation_list_for_metavariable
597 let rec add_lambdas b =
599 Cic.Prod (name,ty,t) ->
600 Cic.Lambda (name,ty,(add_lambdas b t))
601 | _ -> Cic.Lambda (fresh_name, ty, b)
604 add_lambdas (Cic.Meta (new_meta,irl))
605 arity_instantiated_with_left_args
607 (Some candidate),ugraph4,metasenv,subst
608 | (constructor_args_no,_,instance,_)::tl ->
610 let instance',subst,metasenv =
611 CicMetaSubst.delift_rels subst metasenv
612 constructor_args_no instance
614 let candidate,ugraph,metasenv,subst =
616 fun (candidate_oty,ugraph,metasenv,subst)
617 (constructor_args_no,_,instance,_) ->
618 match candidate_oty with
619 | None -> None,ugraph,metasenv,subst
622 let instance',subst,metasenv =
623 CicMetaSubst.delift_rels subst metasenv
624 constructor_args_no instance
626 let subst,metasenv,ugraph =
627 fo_unif_subst subst context metasenv
630 candidate_oty,ugraph,metasenv,subst
632 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
633 | CicUnification.UnificationFailure _
634 | CicUnification.Uncertain _ ->
635 None,ugraph,metasenv,subst
636 ) (Some instance',ugraph4,metasenv,subst) tl
639 | None -> None, ugraph,metasenv,subst
641 let rec add_lambdas n b =
643 Cic.Prod (name,ty,t) ->
644 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
646 Cic.Lambda (fresh_name, ty,
647 CicSubstitution.lift (n + 1) t)
650 (add_lambdas 0 t arity_instantiated_with_left_args),
651 ugraph,metasenv,subst
652 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
653 None,ugraph4,metasenv,subst
656 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
658 let subst,metasenv,ugraph =
659 fo_unif_subst subst context metasenv
660 candidate outtype ugraph5
662 C.MutCase (uri, i, outtype, term', pl'),
663 CicReduction.head_beta_reduce
664 (CicMetaSubst.apply_subst subst
665 (Cic.Appl (outtype::right_args@[term']))),
666 subst,metasenv,ugraph)
667 | _ -> (* easy case *)
668 let tlbody_and_type,subst,metasenv,ugraph4 =
670 (fun x (res,subst,metasenv,ugraph) ->
671 let x',ty,subst',metasenv',ugraph1 =
672 type_of_aux subst metasenv context x ugraph
674 (x', ty)::res,subst',metasenv',ugraph1
675 ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
677 let _,_,subst,metasenv,ugraph4 =
678 eat_prods false subst metasenv context
679 outtypety tlbody_and_type ugraph4
681 let _,_, subst, metasenv,ugraph5 =
682 type_of_aux subst metasenv context
683 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
685 let (subst,metasenv,ugraph6) =
687 (fun (subst,metasenv,ugraph)
688 (constructor_args_no,context,instance,args) ->
692 CicSubstitution.lift constructor_args_no outtype
694 C.Appl (outtype'::args)
696 CicReduction.whd ~subst context appl
698 fo_unif_subst subst context metasenv
699 instance instance' ugraph)
700 (subst,metasenv,ugraph5) outtypeinstances
702 C.MutCase (uri, i, outtype, term', pl'),
703 CicReduction.head_beta_reduce
704 (CicMetaSubst.apply_subst subst
705 (C.Appl(outtype::right_args@[term]))),
706 subst,metasenv,ugraph6)
708 let fl_ty',subst,metasenv,types,ugraph1 =
710 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
711 let ty',_,subst',metasenv',ugraph1 =
712 type_of_aux subst metasenv context ty ugraph
714 fl @ [ty'],subst',metasenv',
715 Some (C.Name n,(C.Decl ty')) :: types, ugraph
716 ) ([],subst,metasenv,[],ugraph) fl
718 let len = List.length types in
719 let context' = types@context in
720 let fl_bo',subst,metasenv,ugraph2 =
722 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
723 let bo',ty_of_bo,subst,metasenv,ugraph1 =
724 type_of_aux subst metasenv context' bo ugraph
726 let subst',metasenv',ugraph' =
727 fo_unif_subst subst context' metasenv
728 ty_of_bo (CicSubstitution.lift len ty) ugraph1
730 fl @ [bo'] , subst',metasenv',ugraph'
731 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
733 let ty = List.nth fl_ty' i in
734 (* now we have the new ty in fl_ty', the new bo in fl_bo',
735 * and we want the new fl with bo' and ty' injected in the right
738 let rec map3 f l1 l2 l3 =
741 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
744 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
747 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
749 let fl_ty',subst,metasenv,types,ugraph1 =
751 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
752 let ty',_,subst',metasenv',ugraph1 =
753 type_of_aux subst metasenv context ty ugraph
755 fl @ [ty'],subst',metasenv',
756 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
757 ) ([],subst,metasenv,[],ugraph) fl
759 let len = List.length types in
760 let context' = types@context in
761 let fl_bo',subst,metasenv,ugraph2 =
763 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
764 let bo',ty_of_bo,subst,metasenv,ugraph1 =
765 type_of_aux subst metasenv context' bo ugraph
767 let subst',metasenv',ugraph' =
768 fo_unif_subst subst context' metasenv
769 ty_of_bo (CicSubstitution.lift len ty) ugraph1
771 fl @ [bo'],subst',metasenv',ugraph'
772 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
774 let ty = List.nth fl_ty' i in
775 (* now we have the new ty in fl_ty', the new bo in fl_bo',
776 * and we want the new fl with bo' and ty' injected in the right
779 let rec map3 f l1 l2 l3 =
782 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
785 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
788 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
790 relocalize localization_tbl t t';
793 (* check_metasenv_consistency checks that the "canonical" context of a
794 metavariable is consitent - up to relocation via the relocation list l -
795 with the actual context *)
796 and check_metasenv_consistency
797 metano subst metasenv context canonical_context l ugraph
799 let module C = Cic in
800 let module R = CicReduction in
801 let module S = CicSubstitution in
802 let lifted_canonical_context =
806 | (Some (n,C.Decl t))::tl ->
807 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
808 | (Some (n,C.Def (t,None)))::tl ->
809 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
810 | None::tl -> None::(aux (i+1) tl)
811 | (Some (n,C.Def (t,Some ty)))::tl ->
813 C.Def ((S.subst_meta l (S.lift i t)),
814 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
816 aux 1 canonical_context
820 (fun (l,subst,metasenv,ugraph) t ct ->
823 l @ [None],subst,metasenv,ugraph
824 | Some t,Some (_,C.Def (ct,_)) ->
825 let subst',metasenv',ugraph' =
827 fo_unif_subst subst context metasenv t ct ugraph
828 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))))))
830 l @ [Some t],subst',metasenv',ugraph'
831 | Some t,Some (_,C.Decl ct) ->
832 let t',inferredty,subst',metasenv',ugraph1 =
833 type_of_aux subst metasenv context t ugraph
835 let subst'',metasenv'',ugraph2 =
838 subst' context metasenv' inferredty ct ugraph1
839 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))))))
841 l @ [Some t'], subst'',metasenv'',ugraph2
843 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
845 Invalid_argument _ ->
849 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
850 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
851 (CicMetaSubst.ppcontext subst canonical_context))))
853 and check_exp_named_subst metasubst metasenv context tl ugraph =
854 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
856 [] -> [],metasubst,metasenv,ugraph
858 let ty_uri,ugraph1 = type_of_variable uri ugraph in
860 CicSubstitution.subst_vars substs ty_uri in
861 (* CSC: why was this code here? it is wrong
862 (match CicEnvironment.get_cooked_obj ~trust:false uri with
863 Cic.Variable (_,Some bo,_,_) ->
866 "A variable with a body can not be explicit substituted"))
867 | Cic.Variable (_,None,_,_) -> ()
871 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
874 let t',typeoft,metasubst',metasenv',ugraph2 =
875 type_of_aux metasubst metasenv context t ugraph1 in
876 let subst = uri,t' in
877 let metasubst'',metasenv'',ugraph3 =
880 metasubst' context metasenv' typeoft typeofvar ugraph2
882 raise (RefineFailure (lazy
883 ("Wrong Explicit Named Substitution: " ^
884 CicMetaSubst.ppterm metasubst' typeoft ^
885 " not unifiable with " ^
886 CicMetaSubst.ppterm metasubst' typeofvar)))
888 (* FIXME: no mere tail recursive! *)
889 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
890 check_exp_named_subst_aux
891 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
893 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
895 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
898 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
899 let module C = Cic in
900 let context_for_t2 = (Some (name,C.Decl s))::context in
901 let t1'' = CicReduction.whd ~subst context t1 in
902 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
903 match (t1'', t2'') with
904 (C.Sort s1, C.Sort s2)
905 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
906 (* different than Coq manual!!! *)
907 C.Sort s2,subst,metasenv,ugraph
908 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
909 let t' = CicUniv.fresh() in
910 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
911 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
912 C.Sort (C.Type t'),subst,metasenv,ugraph2
913 | (C.Sort _,C.Sort (C.Type t1)) ->
914 C.Sort (C.Type t1),subst,metasenv,ugraph
915 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
916 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
917 (* TODO how can we force the meta to become a sort? If we don't we
918 * brake the invariant that refine produce only well typed terms *)
919 (* TODO if we check the non meta term and if it is a sort then we
920 * are likely to know the exact value of the result e.g. if the rhs
921 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
923 CicMkImplicit.mk_implicit_sort metasenv subst in
924 let (subst, metasenv,ugraph1) =
925 fo_unif_subst subst context_for_t2 metasenv
926 (C.Meta (idx,[])) t2'' ugraph
928 t2'',subst,metasenv,ugraph1
934 ("Two sorts were expected, found %s " ^^
935 "(that reduces to %s) and %s (that reduces to %s)")
936 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
937 (CicPp.ppterm t2''))))
940 allow_coercions subst metasenv context hetype tlbody_and_type ugraph
942 let rec mk_prod metasenv context =
945 let (metasenv, idx) =
946 CicMkImplicit.mk_implicit_type metasenv subst context
949 CicMkImplicit.identity_relocation_list_for_metavariable context
951 metasenv,Cic.Meta (idx, irl)
953 let (metasenv, idx) =
954 CicMkImplicit.mk_implicit_type metasenv subst context
957 CicMkImplicit.identity_relocation_list_for_metavariable context
959 let meta = Cic.Meta (idx,irl) in
961 (* The name must be fresh for context. *)
962 (* Nevertheless, argty is well-typed only in context. *)
963 (* Thus I generate a name (name_hint) in context and *)
964 (* then I generate a name --- using the hint name_hint *)
965 (* --- that is fresh in (context'@context). *)
967 (* Cic.Name "pippo" *)
968 FreshNamesGenerator.mk_fresh_name ~subst metasenv
969 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
970 (CicMetaSubst.apply_subst_context subst context)
972 ~typ:(CicMetaSubst.apply_subst subst argty)
974 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
975 FreshNamesGenerator.mk_fresh_name ~subst
976 [] context name_hint ~typ:(Cic.Sort Cic.Prop)
978 let metasenv,target =
979 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
981 metasenv,Cic.Prod (name,meta,target)
983 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
984 let (subst, metasenv,ugraph1) =
986 fo_unif_subst subst context metasenv hetype hetype' ugraph
988 debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
989 (CicPp.ppterm hetype)
990 (CicPp.ppterm hetype')
991 (CicMetaSubst.ppmetasenv [] metasenv)
992 (CicMetaSubst.ppsubst subst)));
996 let rec eat_prods metasenv subst context hetype ugraph =
998 | [] -> [],metasenv,subst,hetype,ugraph
999 | (hete, hety)::tl ->
1002 let arg,subst,metasenv,ugraph1 =
1004 let subst,metasenv,ugraph1 =
1005 fo_unif_subst subst context metasenv hety s ugraph
1007 hete,subst,metasenv,ugraph1
1008 with exn when allow_coercions ->
1009 (* we search a coercion from hety to s *)
1011 let carr t subst context =
1012 CicMetaSubst.apply_subst subst t
1014 let c_hety = carr hety subst context in
1015 let c_s = carr s subst context in
1016 CoercGraph.look_for_coercion c_hety c_s
1019 | CoercGraph.NoCoercion
1020 | CoercGraph.NotHandled _ ->
1023 CicMetaSubst.ppterm_in_context subst hete
1024 context ^ " has type " ^
1025 CicMetaSubst.ppterm_in_context subst hety
1026 context ^ " but is here used with type " ^
1027 CicMetaSubst.ppterm_in_context subst s context
1028 (* "\nReason: " ^ Lazy.force e*))
1030 enrich localization_tbl hete msg exn
1031 | CoercGraph.NotMetaClosed ->
1032 raise (Uncertain (lazy "Coercions on meta"))
1033 | CoercGraph.SomeCoercion c ->
1034 (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
1036 let coerced_args,metasenv',subst',t',ugraph2 =
1037 eat_prods metasenv subst context
1038 (CicSubstitution.subst arg t) ugraph1 tl
1040 arg::coerced_args,metasenv',subst',t',ugraph2
1044 let coerced_args,metasenv,subst,t,ugraph2 =
1045 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
1047 coerced_args,t,subst,metasenv,ugraph2
1050 (* eat prods ends here! *)
1052 let t',ty,subst',metasenv',ugraph1 =
1053 type_of_aux [] metasenv context t ugraph
1055 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1056 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1057 (* Andrea: ho rimesso qui l'applicazione della subst al
1058 metasenv dopo che ho droppato l'invariante che il metsaenv
1059 e' sempre istanziato *)
1060 let substituted_metasenv =
1061 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1063 (* substituted_t,substituted_ty,substituted_metasenv *)
1064 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1066 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1068 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1069 let cleaned_metasenv =
1071 (function (n,context,ty) ->
1072 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1077 | Some (n, Cic.Decl t) ->
1079 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1080 | Some (n, Cic.Def (bo,ty)) ->
1081 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1086 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1088 Some (n, Cic.Def (bo',ty'))
1092 ) substituted_metasenv
1094 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1097 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1099 type_of_aux' ?localization_tbl metasenv context term ugraph
1101 CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
1103 let undebrujin uri typesno tys t =
1106 (fun (name,_,_,_) (i,t) ->
1107 (* here the explicit_named_substituion is assumed to be *)
1109 let t' = Cic.MutInd (uri,i,[]) in
1110 let t = CicSubstitution.subst t' t in
1112 ) tys (typesno - 1,t))
1114 let map_first_n n start f g l =
1115 let rec aux acc k l =
1118 | [] -> raise (Invalid_argument "map_first_n")
1119 | hd :: tl -> f hd k (aux acc (k+1) tl)
1125 (*CSC: this is a very rough approximation; to be finished *)
1126 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1127 let subst,metasenv,ugraph,tys =
1129 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1130 let subst,metasenv,ugraph,cl =
1132 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1133 let rec aux ctx k subst = function
1134 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1135 let subst,metasenv,ugraph,tl =
1137 (subst,metasenv,ugraph,[])
1138 (fun t n (subst,metasenv,ugraph,acc) ->
1139 let subst,metasenv,ugraph =
1141 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1143 subst,metasenv,ugraph,(t::acc))
1144 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1147 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1148 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1149 subst,metasenv,ugraph,t
1150 | Cic.Prod (name,s,t) ->
1151 let ctx = (Some (name,Cic.Decl s))::ctx in
1152 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1153 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1157 (lazy "not well formed constructor type"))
1159 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1160 subst,metasenv,ugraph,(name,ty) :: acc)
1161 cl (subst,metasenv,ugraph,[])
1163 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1164 tys ([],metasenv,ugraph,[])
1166 let substituted_tys =
1168 (fun (name,ind,arity,cl) ->
1170 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1172 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1175 metasenv,ugraph,substituted_tys
1177 let typecheck metasenv uri obj ~localization_tbl =
1178 let ugraph = CicUniv.empty_ugraph in
1180 Cic.Constant (name,Some bo,ty,args,attrs) ->
1181 let bo',boty,metasenv,ugraph =
1182 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1183 let ty',_,metasenv,ugraph =
1184 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1185 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1186 let bo' = CicMetaSubst.apply_subst subst bo' in
1187 let ty' = CicMetaSubst.apply_subst subst ty' in
1188 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1189 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1190 | Cic.Constant (name,None,ty,args,attrs) ->
1191 let ty',_,metasenv,ugraph =
1192 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1194 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1195 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1196 assert (metasenv' = metasenv);
1197 (* Here we do not check the metasenv for correctness *)
1198 let bo',boty,metasenv,ugraph =
1199 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1200 let ty',sort,metasenv,ugraph =
1201 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1205 (* instead of raising Uncertain, let's hope that the meta will become
1208 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1210 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1211 let bo' = CicMetaSubst.apply_subst subst bo' in
1212 let ty' = CicMetaSubst.apply_subst subst ty' in
1213 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1214 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1215 | Cic.Variable _ -> assert false (* not implemented *)
1216 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1217 (*CSC: this code is greately simplified and many many checks are missing *)
1218 (*CSC: e.g. the constructors are not required to build their own types, *)
1219 (*CSC: the arities are not required to have as type a sort, etc. *)
1220 let uri = match uri with Some uri -> uri | None -> assert false in
1221 let typesno = List.length tys in
1222 (* first phase: we fix only the types *)
1223 let metasenv,ugraph,tys =
1225 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1226 let ty',_,metasenv,ugraph =
1227 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1229 metasenv,ugraph,(name,b,ty',cl)::res
1230 ) tys (metasenv,ugraph,[]) in
1232 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1233 (* second phase: we fix only the constructors *)
1234 let metasenv,ugraph,tys =
1236 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1237 let metasenv,ugraph,cl' =
1239 (fun (name,ty) (metasenv,ugraph,res) ->
1240 let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
1241 let ty',_,metasenv,ugraph =
1242 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1243 let ty' = undebrujin uri typesno tys ty' in
1244 metasenv,ugraph,(name,ty')::res
1245 ) cl (metasenv,ugraph,[])
1247 metasenv,ugraph,(name,b,ty,cl')::res
1248 ) tys (metasenv,ugraph,[]) in
1249 (* third phase: we check the positivity condition *)
1250 let metasenv,ugraph,tys =
1251 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1253 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1256 let type_of_aux' metasenv context term =
1259 type_of_aux' metasenv context term in
1261 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1263 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1266 | RefineFailure msg as e ->
1267 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1269 | Uncertain msg as e ->
1270 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1274 let profiler2 = HExtlib.profile "CicRefine"
1276 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1277 profiler2.HExtlib.profile
1278 (type_of_aux' ?localization_tbl metasenv context term) ugraph
1280 let typecheck ~localization_tbl metasenv uri obj =
1281 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj