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 loc f exn =
49 RefineFailure msg -> RefineFailure (f msg)
50 | Uncertain msg -> Uncertain (f msg)
55 | Some loc -> raise (HExtlib.Localized (loc,exn'))
57 let relocalize localization_tbl oldt newt =
59 let infos = Cic.CicHash.find localization_tbl oldt in
60 Cic.CicHash.remove localization_tbl oldt;
61 Cic.CicHash.add localization_tbl newt infos;
69 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
70 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
73 let exp_impl metasenv subst context =
76 let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
77 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
78 metasenv', Cic.Meta (idx, irl)
80 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
81 metasenv', Cic.Meta (idx, [])
83 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
84 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
85 metasenv', Cic.Meta (idx, irl)
89 let rec type_of_constant uri ugraph =
91 let module R = CicReduction in
92 let module U = UriManager in
93 let _ = CicTypeChecker.typecheck uri in
96 CicEnvironment.get_cooked_obj ugraph uri
97 with Not_found -> assert false
100 C.Constant (_,_,ty,_,_) -> ty,u
101 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
104 (RefineFailure (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
106 and type_of_variable uri ugraph =
107 let module C = Cic in
108 let module R = CicReduction in
109 let module U = UriManager in
110 let _ = CicTypeChecker.typecheck uri in
113 CicEnvironment.get_cooked_obj ugraph uri
114 with Not_found -> assert false
117 C.Variable (_,_,ty,_,_) -> ty,u
121 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
123 and type_of_mutual_inductive_defs uri i ugraph =
124 let module C = Cic in
125 let module R = CicReduction in
126 let module U = UriManager in
127 let _ = CicTypeChecker.typecheck uri in
130 CicEnvironment.get_cooked_obj ugraph uri
131 with Not_found -> assert false
134 C.InductiveDefinition (dl,_,_,_) ->
135 let (_,_,arity,_) = List.nth dl i in
140 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
142 and type_of_mutual_inductive_constr uri i j ugraph =
143 let module C = Cic in
144 let module R = CicReduction in
145 let module U = UriManager in
146 let _ = CicTypeChecker.typecheck uri in
149 CicEnvironment.get_cooked_obj ugraph uri
150 with Not_found -> assert false
153 C.InductiveDefinition (dl,_,_,_) ->
154 let (_,_,_,cl) = List.nth dl i in
155 let (_,ty) = List.nth cl (j-1) in
161 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
164 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
166 (* the check_branch function checks if a branch of a case is refinable.
167 It returns a pair (outype_instance,args), a subst and a metasenv.
168 outype_instance is the expected result of applying the case outtype
170 The problem is that outype is in general unknown, and we should
171 try to synthesize it from the above information, that is in general
172 a second order unification problem. *)
174 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
175 let module C = Cic in
176 (* let module R = CicMetaSubst in *)
177 let module R = CicReduction in
178 match R.whd ~subst context expectedtype with
180 (n,context,actualtype, [term]), subst, metasenv, ugraph
181 | C.Appl (C.MutInd (_,_,_)::tl) ->
182 let (_,arguments) = split tl left_args_no in
183 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
184 | C.Prod (name,so,de) ->
185 (* we expect that the actual type of the branch has the due
187 (match R.whd ~subst context actualtype with
188 C.Prod (name',so',de') ->
189 let subst, metasenv, ugraph1 =
190 fo_unif_subst subst context metasenv so so' ugraph in
192 (match CicSubstitution.lift 1 term with
193 C.Appl l -> C.Appl (l@[C.Rel 1])
194 | t -> C.Appl [t ; C.Rel 1]) in
195 (* we should also check that the name variable is anonymous in
196 the actual type de' ?? *)
198 ((Some (name,(C.Decl so)))::context)
199 metasenv subst left_args_no de' term' de ugraph1
200 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
201 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
203 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
206 let rec type_of_aux subst metasenv context t ugraph =
207 let module C = Cic in
208 let module S = CicSubstitution in
209 let module U = UriManager in
210 (* this stops on binders, so we have to call it every time *)
215 match List.nth context (n - 1) with
216 Some (_,C.Decl ty) ->
217 t,S.lift n ty,subst,metasenv, ugraph
218 | Some (_,C.Def (_,Some ty)) ->
219 t,S.lift n ty,subst,metasenv, ugraph
220 | Some (_,C.Def (bo,None)) ->
222 (* if it is in the context it must be already well-typed*)
223 CicTypeChecker.type_of_aux' ~subst metasenv context
226 t,ty,subst,metasenv,ugraph
227 | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis"))
229 _ -> raise (RefineFailure (lazy "Not a close term")))
230 | C.Var (uri,exp_named_subst) ->
231 let exp_named_subst',subst',metasenv',ugraph1 =
232 check_exp_named_subst
233 subst metasenv context exp_named_subst ugraph
235 let ty_uri,ugraph1 = type_of_variable uri ugraph in
237 CicSubstitution.subst_vars exp_named_subst' ty_uri
239 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
242 let (canonical_context, term,ty) =
243 CicUtil.lookup_subst n subst
245 let l',subst',metasenv',ugraph1 =
246 check_metasenv_consistency n subst metasenv context
247 canonical_context l ugraph
249 (* trust or check ??? *)
250 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
251 subst', metasenv', ugraph1
252 (* type_of_aux subst metasenv
253 context (CicSubstitution.subst_meta l term) *)
254 with CicUtil.Subst_not_found _ ->
255 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
256 let l',subst',metasenv', ugraph1 =
257 check_metasenv_consistency n subst metasenv context
258 canonical_context l ugraph
260 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
261 subst', metasenv',ugraph1)
262 | C.Sort (C.Type tno) ->
263 let tno' = CicUniv.fresh() in
264 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
265 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
267 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
268 | C.Implicit infos ->
269 let metasenv',t' = exp_impl metasenv subst context infos in
270 type_of_aux subst metasenv' context t' ugraph
272 let ty',_,subst',metasenv',ugraph1 =
273 type_of_aux subst metasenv context ty ugraph
275 let te',inferredty,subst'',metasenv'',ugraph2 =
276 type_of_aux subst' metasenv' context te ugraph1
278 let subst''',metasenv''',ugraph3 =
279 fo_unif_subst subst'' context metasenv''
280 inferredty ty' ugraph2
282 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
283 | C.Prod (name,s,t) ->
284 let carr t subst context = CicMetaSubst.apply_subst subst t in
286 in_source tgt_sort t type_to_coerce subst ctx metasenv uragph
288 let coercion_src = carr type_to_coerce subst ctx in
289 match coercion_src with
291 t,type_to_coerce,subst,metasenv,ugraph
293 | Cic.Meta _ as meta when not in_source ->
294 let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
295 let subst, metasenv, ugraph =
297 subst ctx metasenv meta coercion_tgt ugraph
299 t, Cic.Sort tgt_sort, subst, metasenv, ugraph
301 | Cic.Meta _ as meta ->
302 t, meta, subst, metasenv, ugraph
303 | Cic.Cast _ as cast ->
304 t, cast, subst, metasenv, ugraph
306 let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
307 let search = CoercGraph.look_for_coercion in
308 let boh = search coercion_src coercion_tgt in
310 | CoercGraph.NoCoercion
311 | CoercGraph.NotHandled _ ->
313 (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
314 | CoercGraph.NotMetaClosed ->
316 (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
317 | CoercGraph.SomeCoercion c ->
318 Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
320 let s',sort1,subst',metasenv',ugraph1 =
321 type_of_aux subst metasenv context s ugraph
323 let s',sort1,subst', metasenv',ugraph1 =
324 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
325 s' sort1 subst' context metasenv' ugraph1
327 let context_for_t = ((Some (name,(C.Decl s')))::context) in
328 let t',sort2,subst'',metasenv'',ugraph2 =
329 type_of_aux subst' metasenv'
330 context_for_t t ugraph1
332 let t',sort2,subst'',metasenv'',ugraph2 =
333 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
334 t' sort2 subst'' context_for_t metasenv'' ugraph2
336 let sop,subst''',metasenv''',ugraph3 =
337 sort_of_prod subst'' metasenv''
338 context (name,s') (sort1,sort2) ugraph2
340 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
341 | C.Lambda (n,s,t) ->
343 let s',sort1,subst',metasenv',ugraph1 =
344 type_of_aux subst metasenv context s ugraph in
346 match CicReduction.whd ~subst:subst' context sort1 with
348 | C.Sort _ -> s',sort1
350 let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh ())) in
351 let search = CoercGraph.look_for_coercion in
352 let boh = search coercion_src coercion_tgt in
354 | CoercGraph.SomeCoercion c ->
355 Cic.Appl [c;s'], coercion_tgt
356 | CoercGraph.NoCoercion
357 | CoercGraph.NotHandled _
358 | CoercGraph.NotMetaClosed ->
359 raise (RefineFailure (lazy (sprintf
360 "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))))
362 let context_for_t = ((Some (n,(C.Decl s')))::context) in
363 let t',type2,subst'',metasenv'',ugraph2 =
364 type_of_aux subst' metasenv' context_for_t t ugraph1
366 C.Lambda (n,s',t'),C.Prod (n,s',type2),
367 subst'',metasenv'',ugraph2
369 (* only to check if s is well-typed *)
370 let s',ty,subst',metasenv',ugraph1 =
371 type_of_aux subst metasenv context s ugraph
373 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
375 let t',inferredty,subst'',metasenv'',ugraph2 =
376 type_of_aux subst' metasenv'
377 context_for_t t ugraph1
379 (* One-step LetIn reduction.
380 * Even faster than the previous solution.
381 * Moreover the inferred type is closer to the expected one.
383 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
384 subst'',metasenv'',ugraph2
385 | C.Appl (he::((_::_) as tl)) ->
386 let he',hetype,subst',metasenv',ugraph1 =
387 type_of_aux subst metasenv context he ugraph
389 let tlbody_and_type,subst'',metasenv'',ugraph2 =
391 (fun x (res,subst,metasenv,ugraph) ->
392 let x',ty,subst',metasenv',ugraph1 =
393 type_of_aux subst metasenv context x ugraph
395 relocalize localization_tbl x x';
396 (x', ty)::res,subst',metasenv',ugraph1
397 ) tl ([],subst',metasenv',ugraph1)
399 let tl',applty,subst''',metasenv''',ugraph3 =
400 eat_prods true subst'' metasenv'' context
401 hetype tlbody_and_type ugraph2
403 C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
404 | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
405 | C.Const (uri,exp_named_subst) ->
406 let exp_named_subst',subst',metasenv',ugraph1 =
407 check_exp_named_subst subst metasenv context
408 exp_named_subst ugraph in
409 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
411 CicSubstitution.subst_vars exp_named_subst' ty_uri
413 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
414 | C.MutInd (uri,i,exp_named_subst) ->
415 let exp_named_subst',subst',metasenv',ugraph1 =
416 check_exp_named_subst subst metasenv context
417 exp_named_subst ugraph
419 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
421 CicSubstitution.subst_vars exp_named_subst' ty_uri in
422 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
423 | C.MutConstruct (uri,i,j,exp_named_subst) ->
424 let exp_named_subst',subst',metasenv',ugraph1 =
425 check_exp_named_subst subst metasenv context
426 exp_named_subst ugraph
429 type_of_mutual_inductive_constr uri i j ugraph1
432 CicSubstitution.subst_vars exp_named_subst' ty_uri
434 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
436 | C.MutCase (uri, i, outtype, term, pl) ->
437 (* first, get the inductive type (and noparams)
438 * in the environment *)
439 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
440 let _ = CicTypeChecker.typecheck uri in
441 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
443 C.InductiveDefinition (l,expl_params,parsno,_) ->
444 List.nth l i , expl_params, parsno, u
448 (lazy ("Unkown mutual inductive definition " ^
449 U.string_of_uri uri)))
451 let rec count_prod t =
452 match CicReduction.whd ~subst context t with
453 C.Prod (_, _, t) -> 1 + (count_prod t)
456 let no_args = count_prod arity in
457 (* now, create a "generic" MutInd *)
458 let metasenv,left_args =
459 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
461 let metasenv,right_args =
462 let no_right_params = no_args - no_left_params in
463 if no_right_params < 0 then assert false
464 else CicMkImplicit.n_fresh_metas
465 metasenv subst context no_right_params
467 let metasenv,exp_named_subst =
468 CicMkImplicit.fresh_subst metasenv subst context expl_params in
471 C.MutInd (uri,i,exp_named_subst)
474 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
476 (* check consistency with the actual type of term *)
477 let term',actual_type,subst,metasenv,ugraph1 =
478 type_of_aux subst metasenv context term ugraph in
479 let expected_type',_, subst, metasenv,ugraph2 =
480 type_of_aux subst metasenv context expected_type ugraph1
482 let actual_type = CicReduction.whd ~subst context actual_type in
483 let subst,metasenv,ugraph3 =
484 fo_unif_subst subst context metasenv
485 expected_type' actual_type ugraph2
487 let rec instantiate_prod t =
491 match CicReduction.whd ~subst context t with
493 instantiate_prod (CicSubstitution.subst he t') tl
496 let arity_instantiated_with_left_args =
497 instantiate_prod arity left_args in
498 (* TODO: check if the sort elimination
499 * is allowed: [(I q1 ... qr)|B] *)
500 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
502 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
504 if left_args = [] then
505 (C.MutConstruct (uri,i,j,exp_named_subst))
508 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
510 let p',actual_type,subst,metasenv,ugraph1 =
511 type_of_aux subst metasenv context p ugraph
513 let constructor',expected_type, subst, metasenv,ugraph2 =
514 type_of_aux subst metasenv context constructor ugraph1
516 let outtypeinstance,subst,metasenv,ugraph3 =
517 check_branch 0 context metasenv subst no_left_params
518 actual_type constructor' expected_type ugraph2
521 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
522 ([],1,[],subst,metasenv,ugraph3) pl
525 (* we are left to check that the outype matches his instances.
526 The easy case is when the outype is specified, that amount
527 to a trivial check. Otherwise, we should guess a type from
533 (let candidate,ugraph5,metasenv,subst =
534 let exp_name_subst, metasenv =
536 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
538 let uris = CicUtil.params_of_obj o in
540 fun uri (acc,metasenv) ->
541 let metasenv',new_meta =
542 CicMkImplicit.mk_implicit metasenv subst context
545 CicMkImplicit.identity_relocation_list_for_metavariable
548 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
552 match left_args,right_args with
553 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
555 let rec mk_right_args =
558 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
560 let right_args_no = List.length right_args in
561 let lifted_left_args =
562 List.map (CicSubstitution.lift right_args_no) left_args
564 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
565 (lifted_left_args @ mk_right_args right_args_no))
568 FreshNamesGenerator.mk_fresh_name ~subst metasenv
569 context Cic.Anonymous ~typ:ty
571 match outtypeinstances with
573 let extended_context =
574 let rec add_right_args =
576 Cic.Prod (name,ty,t) ->
577 Some (name,Cic.Decl ty)::(add_right_args t)
580 (Some (fresh_name,Cic.Decl ty))::
582 (add_right_args arity_instantiated_with_left_args))@
585 let metasenv,new_meta =
586 CicMkImplicit.mk_implicit metasenv subst extended_context
589 CicMkImplicit.identity_relocation_list_for_metavariable
592 let rec add_lambdas b =
594 Cic.Prod (name,ty,t) ->
595 Cic.Lambda (name,ty,(add_lambdas b t))
596 | _ -> Cic.Lambda (fresh_name, ty, b)
599 add_lambdas (Cic.Meta (new_meta,irl))
600 arity_instantiated_with_left_args
602 (Some candidate),ugraph4,metasenv,subst
603 | (constructor_args_no,_,instance,_)::tl ->
605 let instance',subst,metasenv =
606 CicMetaSubst.delift_rels subst metasenv
607 constructor_args_no instance
609 let candidate,ugraph,metasenv,subst =
611 fun (candidate_oty,ugraph,metasenv,subst)
612 (constructor_args_no,_,instance,_) ->
613 match candidate_oty with
614 | None -> None,ugraph,metasenv,subst
617 let instance',subst,metasenv =
618 CicMetaSubst.delift_rels subst metasenv
619 constructor_args_no instance
621 let subst,metasenv,ugraph =
622 fo_unif_subst subst context metasenv
625 candidate_oty,ugraph,metasenv,subst
627 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
628 | CicUnification.UnificationFailure _
629 | CicUnification.Uncertain _ ->
630 None,ugraph,metasenv,subst
631 ) (Some instance',ugraph4,metasenv,subst) tl
634 | None -> None, ugraph,metasenv,subst
636 let rec add_lambdas n b =
638 Cic.Prod (name,ty,t) ->
639 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
641 Cic.Lambda (fresh_name, ty,
642 CicSubstitution.lift (n + 1) t)
645 (add_lambdas 0 t arity_instantiated_with_left_args),
646 ugraph,metasenv,subst
647 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
648 None,ugraph4,metasenv,subst
651 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
653 let subst,metasenv,ugraph =
654 fo_unif_subst subst context metasenv
655 candidate outtype ugraph5
657 C.MutCase (uri, i, outtype, term', pl'),
658 CicReduction.head_beta_reduce
659 (CicMetaSubst.apply_subst subst
660 (Cic.Appl (outtype::right_args@[term']))),
661 subst,metasenv,ugraph)
662 | _ -> (* easy case *)
663 let outtype,outtypety, subst, metasenv,ugraph4 =
664 type_of_aux subst metasenv context outtype ugraph4
666 let tlbody_and_type,subst,metasenv,ugraph4 =
668 (fun x (res,subst,metasenv,ugraph) ->
669 let x',ty,subst',metasenv',ugraph1 =
670 type_of_aux subst metasenv context x ugraph
672 (x', ty)::res,subst',metasenv',ugraph1
673 ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
675 let _,_,subst,metasenv,ugraph4 =
676 eat_prods false subst metasenv context
677 outtypety tlbody_and_type ugraph4
679 let _,_, subst, metasenv,ugraph5 =
680 type_of_aux subst metasenv context
681 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
683 let (subst,metasenv,ugraph6) =
685 (fun (subst,metasenv,ugraph)
686 (constructor_args_no,context,instance,args) ->
690 CicSubstitution.lift constructor_args_no outtype
692 C.Appl (outtype'::args)
694 CicReduction.whd ~subst context appl
696 fo_unif_subst subst context metasenv
697 instance instance' ugraph)
698 (subst,metasenv,ugraph5) outtypeinstances
700 C.MutCase (uri, i, outtype, term', pl'),
701 CicReduction.head_beta_reduce
702 (CicMetaSubst.apply_subst subst
703 (C.Appl(outtype::right_args@[term]))),
704 subst,metasenv,ugraph6)
706 let fl_ty',subst,metasenv,types,ugraph1 =
708 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
709 let ty',_,subst',metasenv',ugraph1 =
710 type_of_aux subst metasenv context ty ugraph
712 fl @ [ty'],subst',metasenv',
713 Some (C.Name n,(C.Decl ty')) :: types, ugraph
714 ) ([],subst,metasenv,[],ugraph) fl
716 let len = List.length types in
717 let context' = types@context in
718 let fl_bo',subst,metasenv,ugraph2 =
720 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
721 let bo',ty_of_bo,subst,metasenv,ugraph1 =
722 type_of_aux subst metasenv context' bo ugraph
724 let subst',metasenv',ugraph' =
725 fo_unif_subst subst context' metasenv
726 ty_of_bo (CicSubstitution.lift len ty) ugraph1
728 fl @ [bo'] , subst',metasenv',ugraph'
729 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
731 let ty = List.nth fl_ty' i in
732 (* now we have the new ty in fl_ty', the new bo in fl_bo',
733 * and we want the new fl with bo' and ty' injected in the right
736 let rec map3 f l1 l2 l3 =
739 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
742 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
745 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
747 let fl_ty',subst,metasenv,types,ugraph1 =
749 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
750 let ty',_,subst',metasenv',ugraph1 =
751 type_of_aux subst metasenv context ty ugraph
753 fl @ [ty'],subst',metasenv',
754 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
755 ) ([],subst,metasenv,[],ugraph) fl
757 let len = List.length types in
758 let context' = types@context in
759 let fl_bo',subst,metasenv,ugraph2 =
761 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
762 let bo',ty_of_bo,subst,metasenv,ugraph1 =
763 type_of_aux subst metasenv context' bo ugraph
765 let subst',metasenv',ugraph' =
766 fo_unif_subst subst context' metasenv
767 ty_of_bo (CicSubstitution.lift len ty) ugraph1
769 fl @ [bo'],subst',metasenv',ugraph'
770 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
772 let ty = List.nth fl_ty' i in
773 (* now we have the new ty in fl_ty', the new bo in fl_bo',
774 * and we want the new fl with bo' and ty' injected in the right
777 let rec map3 f l1 l2 l3 =
780 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
783 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
786 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
788 (* check_metasenv_consistency checks that the "canonical" context of a
789 metavariable is consitent - up to relocation via the relocation list l -
790 with the actual context *)
791 and check_metasenv_consistency
792 metano subst metasenv context canonical_context l ugraph
794 let module C = Cic in
795 let module R = CicReduction in
796 let module S = CicSubstitution in
797 let lifted_canonical_context =
801 | (Some (n,C.Decl t))::tl ->
802 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
803 | (Some (n,C.Def (t,None)))::tl ->
804 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
805 | None::tl -> None::(aux (i+1) tl)
806 | (Some (n,C.Def (t,Some ty)))::tl ->
808 C.Def ((S.subst_meta l (S.lift i t)),
809 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
811 aux 1 canonical_context
815 (fun (l,subst,metasenv,ugraph) t ct ->
818 l @ [None],subst,metasenv,ugraph
819 | Some t,Some (_,C.Def (ct,_)) ->
820 let subst',metasenv',ugraph' =
822 fo_unif_subst subst context metasenv t ct ugraph
823 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))))))
825 l @ [Some t],subst',metasenv',ugraph'
826 | Some t,Some (_,C.Decl ct) ->
827 let t',inferredty,subst',metasenv',ugraph1 =
828 type_of_aux subst metasenv context t ugraph
830 let subst'',metasenv'',ugraph2 =
833 subst' context metasenv' inferredty ct ugraph1
834 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))))))
836 l @ [Some t'], subst'',metasenv'',ugraph2
838 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
840 Invalid_argument _ ->
844 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
845 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
846 (CicMetaSubst.ppcontext subst canonical_context))))
848 and check_exp_named_subst metasubst metasenv context tl ugraph =
849 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
851 [] -> [],metasubst,metasenv,ugraph
852 | ((uri,t) as subst)::tl ->
853 let ty_uri,ugraph1 = type_of_variable uri ugraph in
855 CicSubstitution.subst_vars substs ty_uri in
856 (* CSC: why was this code here? it is wrong
857 (match CicEnvironment.get_cooked_obj ~trust:false uri with
858 Cic.Variable (_,Some bo,_,_) ->
861 "A variable with a body can not be explicit substituted"))
862 | Cic.Variable (_,None,_,_) -> ()
866 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
869 let t',typeoft,metasubst',metasenv',ugraph2 =
870 type_of_aux metasubst metasenv context t ugraph1
872 let metasubst'',metasenv'',ugraph3 =
875 metasubst' context metasenv' typeoft typeofvar ugraph2
877 raise (RefineFailure (lazy
878 ("Wrong Explicit Named Substitution: " ^
879 CicMetaSubst.ppterm metasubst' typeoft ^
880 " not unifiable with " ^
881 CicMetaSubst.ppterm metasubst' typeofvar)))
883 (* FIXME: no mere tail recursive! *)
884 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
885 check_exp_named_subst_aux
886 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
888 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
890 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
893 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
894 let module C = Cic in
895 let context_for_t2 = (Some (name,C.Decl s))::context in
896 let t1'' = CicReduction.whd ~subst context t1 in
897 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
898 match (t1'', t2'') with
899 (C.Sort s1, C.Sort s2)
900 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
901 (* different than Coq manual!!! *)
902 C.Sort s2,subst,metasenv,ugraph
903 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
904 let t' = CicUniv.fresh() in
905 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
906 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
907 C.Sort (C.Type t'),subst,metasenv,ugraph2
908 | (C.Sort _,C.Sort (C.Type t1)) ->
909 C.Sort (C.Type t1),subst,metasenv,ugraph
910 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
911 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
912 (* TODO how can we force the meta to become a sort? If we don't we
913 * brake the invariant that refine produce only well typed terms *)
914 (* TODO if we check the non meta term and if it is a sort then we
915 * are likely to know the exact value of the result e.g. if the rhs
916 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
918 CicMkImplicit.mk_implicit_sort metasenv subst in
919 let (subst, metasenv,ugraph1) =
920 fo_unif_subst subst context_for_t2 metasenv
921 (C.Meta (idx,[])) t2'' ugraph
923 t2'',subst,metasenv,ugraph1
929 ("Two sorts were expected, found %s " ^^
930 "(that reduces to %s) and %s (that reduces to %s)")
931 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
932 (CicPp.ppterm t2''))))
935 allow_coercions subst metasenv context hetype tlbody_and_type ugraph
937 let rec mk_prod metasenv context =
940 let (metasenv, idx) =
941 CicMkImplicit.mk_implicit_type metasenv subst context
944 CicMkImplicit.identity_relocation_list_for_metavariable context
946 metasenv,Cic.Meta (idx, irl)
948 let (metasenv, idx) =
949 CicMkImplicit.mk_implicit_type metasenv subst context
952 CicMkImplicit.identity_relocation_list_for_metavariable context
954 let meta = Cic.Meta (idx,irl) in
956 (* The name must be fresh for context. *)
957 (* Nevertheless, argty is well-typed only in context. *)
958 (* Thus I generate a name (name_hint) in context and *)
959 (* then I generate a name --- using the hint name_hint *)
960 (* --- that is fresh in (context'@context). *)
962 (* Cic.Name "pippo" *)
963 FreshNamesGenerator.mk_fresh_name ~subst metasenv
964 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
965 (CicMetaSubst.apply_subst_context subst context)
967 ~typ:(CicMetaSubst.apply_subst subst argty)
969 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
970 FreshNamesGenerator.mk_fresh_name ~subst
971 [] context name_hint ~typ:(Cic.Sort Cic.Prop)
973 let metasenv,target =
974 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
976 metasenv,Cic.Prod (name,meta,target)
978 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
979 let (subst, metasenv,ugraph1) =
981 fo_unif_subst subst context metasenv hetype hetype' ugraph
983 debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
984 (CicPp.ppterm hetype)
985 (CicPp.ppterm hetype')
986 (CicMetaSubst.ppmetasenv [] metasenv)
987 (CicMetaSubst.ppsubst subst)));
991 let rec eat_prods metasenv subst context hetype ugraph =
993 | [] -> [],metasenv,subst,hetype,ugraph
994 | (hete, hety)::tl ->
997 let arg,subst,metasenv,ugraph1 =
999 let subst,metasenv,ugraph1 =
1000 fo_unif_subst subst context metasenv hety s ugraph
1002 hete,subst,metasenv,ugraph1
1003 with exn when allow_coercions ->
1004 (* we search a coercion from hety to s *)
1006 let carr t subst context =
1007 CicMetaSubst.apply_subst subst t
1009 let c_hety = carr hety subst context in
1010 let c_s = carr s subst context in
1011 CoercGraph.look_for_coercion c_hety c_s
1014 | CoercGraph.NoCoercion
1015 | CoercGraph.NotHandled _ ->
1018 CicMetaSubst.ppterm_in_context subst hete
1019 context ^ " has type " ^
1020 CicMetaSubst.ppterm_in_context subst hety
1021 context ^ " but is here used with type " ^
1022 CicMetaSubst.ppterm_in_context subst s context
1023 (* "\nReason: " ^ Lazy.force e*))
1026 (try Some (Cic.CicHash.find localization_tbl hete) with Not_found -> prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm hete); None)
1028 | CoercGraph.NotMetaClosed ->
1029 raise (Uncertain (lazy "Coercions on meta"))
1030 | CoercGraph.SomeCoercion c ->
1031 (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
1033 let coerced_args,metasenv',subst',t',ugraph2 =
1034 eat_prods metasenv subst context
1035 (CicSubstitution.subst arg t) ugraph1 tl
1037 arg::coerced_args,metasenv',subst',t',ugraph2
1041 let coerced_args,metasenv,subst,t,ugraph2 =
1042 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
1044 coerced_args,t,subst,metasenv,ugraph2
1047 (* eat prods ends here! *)
1049 let t',ty,subst',metasenv',ugraph1 =
1050 type_of_aux [] metasenv context t ugraph
1052 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1053 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1054 (* Andrea: ho rimesso qui l'applicazione della subst al
1055 metasenv dopo che ho droppato l'invariante che il metsaenv
1056 e' sempre istanziato *)
1057 let substituted_metasenv =
1058 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1060 (* substituted_t,substituted_ty,substituted_metasenv *)
1061 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1063 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1065 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1066 let cleaned_metasenv =
1068 (function (n,context,ty) ->
1069 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1074 | Some (n, Cic.Decl t) ->
1076 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1077 | Some (n, Cic.Def (bo,ty)) ->
1078 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1083 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1085 Some (n, Cic.Def (bo',ty'))
1089 ) substituted_metasenv
1091 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1094 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1096 type_of_aux' ?localization_tbl metasenv context term ugraph
1098 CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
1100 let undebrujin uri typesno tys t =
1103 (fun (name,_,_,_) (i,t) ->
1104 (* here the explicit_named_substituion is assumed to be *)
1106 let t' = Cic.MutInd (uri,i,[]) in
1107 let t = CicSubstitution.subst t' t in
1109 ) tys (typesno - 1,t))
1111 let map_first_n n start f g l =
1112 let rec aux acc k l =
1115 | [] -> raise (Invalid_argument "map_first_n")
1116 | hd :: tl -> f hd k (aux acc (k+1) tl)
1122 (*CSC: this is a very rough approximation; to be finished *)
1123 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1124 let number_of_types = List.length tys in
1125 let subst,metasenv,ugraph,tys =
1127 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1128 let subst,metasenv,ugraph,cl =
1130 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1131 let rec aux ctx k subst = function
1132 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1133 let subst,metasenv,ugraph,tl =
1135 (subst,metasenv,ugraph,[])
1136 (fun t n (subst,metasenv,ugraph,acc) ->
1137 let subst,metasenv,ugraph =
1139 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1141 subst,metasenv,ugraph,(t::acc))
1142 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1145 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1146 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1147 subst,metasenv,ugraph,t
1148 | Cic.Prod (name,s,t) ->
1149 let ctx = (Some (name,Cic.Decl s))::ctx in
1150 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1151 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1155 (lazy "not well formed constructor type"))
1157 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1158 subst,metasenv,ugraph,(name,ty) :: acc)
1159 cl (subst,metasenv,ugraph,[])
1161 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1162 tys ([],metasenv,ugraph,[])
1164 let substituted_tys =
1166 (fun (name,ind,arity,cl) ->
1168 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1170 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1173 metasenv,ugraph,substituted_tys
1175 let typecheck metasenv uri obj ~localization_tbl =
1176 let ugraph = CicUniv.empty_ugraph in
1178 Cic.Constant (name,Some bo,ty,args,attrs) ->
1179 let bo',boty,metasenv,ugraph =
1180 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1181 let ty',_,metasenv,ugraph =
1182 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1183 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1184 let bo' = CicMetaSubst.apply_subst subst bo' in
1185 let ty' = CicMetaSubst.apply_subst subst ty' in
1186 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1187 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1188 | Cic.Constant (name,None,ty,args,attrs) ->
1189 let ty',_,metasenv,ugraph =
1190 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1192 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1193 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1194 assert (metasenv' = metasenv);
1195 (* Here we do not check the metasenv for correctness *)
1196 let bo',boty,metasenv,ugraph =
1197 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1198 let ty',sort,metasenv,ugraph =
1199 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1203 (* instead of raising Uncertain, let's hope that the meta will become
1206 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1208 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1209 let bo' = CicMetaSubst.apply_subst subst bo' in
1210 let ty' = CicMetaSubst.apply_subst subst ty' in
1211 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1212 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1213 | Cic.Variable _ -> assert false (* not implemented *)
1214 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1215 (*CSC: this code is greately simplified and many many checks are missing *)
1216 (*CSC: e.g. the constructors are not required to build their own types, *)
1217 (*CSC: the arities are not required to have as type a sort, etc. *)
1218 let uri = match uri with Some uri -> uri | None -> assert false in
1219 let typesno = List.length tys in
1220 (* first phase: we fix only the types *)
1221 let metasenv,ugraph,tys =
1223 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1224 let ty',_,metasenv,ugraph =
1225 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1227 metasenv,ugraph,(name,b,ty',cl)::res
1228 ) tys (metasenv,ugraph,[]) in
1230 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1231 (* second phase: we fix only the constructors *)
1232 let metasenv,ugraph,tys =
1234 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1235 let metasenv,ugraph,cl' =
1237 (fun (name,ty) (metasenv,ugraph,res) ->
1238 let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
1239 let ty',_,metasenv,ugraph =
1240 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1241 let ty' = undebrujin uri typesno tys ty' in
1242 metasenv,ugraph,(name,ty')::res
1243 ) cl (metasenv,ugraph,[])
1245 metasenv,ugraph,(name,b,ty,cl')::res
1246 ) tys (metasenv,ugraph,[]) in
1247 (* third phase: we check the positivity condition *)
1248 let metasenv,ugraph,tys =
1249 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1251 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1254 let type_of_aux' metasenv context term =
1257 type_of_aux' metasenv context term in
1259 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1261 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1264 | RefineFailure msg as e ->
1265 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1267 | Uncertain msg as e ->
1268 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1272 let profiler2 = HExtlib.profile "CicRefine"
1274 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1275 profiler2.HExtlib.profile
1276 (type_of_aux' ?localization_tbl metasenv context term) ugraph
1278 let typecheck ~localization_tbl metasenv uri obj =
1279 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj