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)
49 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
50 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
53 let rec type_of_constant uri ugraph =
55 let module R = CicReduction in
56 let module U = UriManager in
57 let _ = CicTypeChecker.typecheck uri in
60 CicEnvironment.get_cooked_obj ugraph uri
61 with Not_found -> assert false
64 C.Constant (_,_,ty,_,_) -> ty,u
65 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
68 (RefineFailure (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
70 and type_of_variable uri ugraph =
72 let module R = CicReduction in
73 let module U = UriManager in
74 let _ = CicTypeChecker.typecheck uri in
77 CicEnvironment.get_cooked_obj ugraph uri
78 with Not_found -> assert false
81 C.Variable (_,_,ty,_,_) -> ty,u
85 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
87 and type_of_mutual_inductive_defs uri i ugraph =
89 let module R = CicReduction in
90 let module U = UriManager in
91 let _ = CicTypeChecker.typecheck uri in
94 CicEnvironment.get_cooked_obj ugraph uri
95 with Not_found -> assert false
98 C.InductiveDefinition (dl,_,_,_) ->
99 let (_,_,arity,_) = List.nth dl i in
104 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
106 and type_of_mutual_inductive_constr uri i j 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.InductiveDefinition (dl,_,_,_) ->
118 let (_,_,_,cl) = List.nth dl i in
119 let (_,ty) = List.nth cl (j-1) in
124 (lazy ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
127 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
129 (* the check_branch function checks if a branch of a case is refinable.
130 It returns a pair (outype_instance,args), a subst and a metasenv.
131 outype_instance is the expected result of applying the case outtype
133 The problem is that outype is in general unknown, and we should
134 try to synthesize it from the above information, that is in general
135 a second order unification problem. *)
137 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
138 let module C = Cic in
139 (* let module R = CicMetaSubst in *)
140 let module R = CicReduction in
141 match R.whd ~subst context expectedtype with
143 (n,context,actualtype, [term]), subst, metasenv, ugraph
144 | C.Appl (C.MutInd (_,_,_)::tl) ->
145 let (_,arguments) = split tl left_args_no in
146 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
147 | C.Prod (name,so,de) ->
148 (* we expect that the actual type of the branch has the due
150 (match R.whd ~subst context actualtype with
151 C.Prod (name',so',de') ->
152 let subst, metasenv, ugraph1 =
153 fo_unif_subst subst context metasenv so so' ugraph in
155 (match CicSubstitution.lift 1 term with
156 C.Appl l -> C.Appl (l@[C.Rel 1])
157 | t -> C.Appl [t ; C.Rel 1]) in
158 (* we should also check that the name variable is anonymous in
159 the actual type de' ?? *)
161 ((Some (name,(C.Decl so)))::context)
162 metasenv subst left_args_no de' term' de ugraph1
163 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
164 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
166 and type_of_aux' metasenv context t ugraph =
167 let rec type_of_aux subst metasenv context t ugraph =
168 let module C = Cic in
169 let module S = CicSubstitution in
170 let module U = UriManager in
175 match List.nth context (n - 1) with
176 Some (_,C.Decl ty) ->
177 t,S.lift n ty,subst,metasenv, ugraph
178 | Some (_,C.Def (_,Some ty)) ->
179 t,S.lift n ty,subst,metasenv, ugraph
180 | Some (_,C.Def (bo,None)) ->
182 (* if it is in the context it must be already well-typed*)
183 CicTypeChecker.type_of_aux' ~subst metasenv context
186 t,ty,subst,metasenv,ugraph
187 | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis"))
189 _ -> raise (RefineFailure (lazy "Not a close term"))
191 | C.Var (uri,exp_named_subst) ->
192 let exp_named_subst',subst',metasenv',ugraph1 =
193 check_exp_named_subst
194 subst metasenv context exp_named_subst ugraph
196 let ty_uri,ugraph1 = type_of_variable uri ugraph in
198 CicSubstitution.subst_vars exp_named_subst' ty_uri
200 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
203 let (canonical_context, term,ty) =
204 CicUtil.lookup_subst n subst
206 let l',subst',metasenv',ugraph1 =
207 check_metasenv_consistency n subst metasenv context
208 canonical_context l ugraph
210 (* trust or check ??? *)
211 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
212 subst', metasenv', ugraph1
213 (* type_of_aux subst metasenv
214 context (CicSubstitution.subst_meta l term) *)
215 with CicUtil.Subst_not_found _ ->
216 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
217 let l',subst',metasenv', ugraph1 =
218 check_metasenv_consistency n subst metasenv context
219 canonical_context l ugraph
221 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
222 subst', metasenv',ugraph1)
223 | C.Sort (C.Type tno) ->
224 let tno' = CicUniv.fresh() in
225 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
226 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
228 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
229 | C.Implicit _ -> raise (AssertFailure (lazy "21"))
231 let ty',_,subst',metasenv',ugraph1 =
232 type_of_aux subst metasenv context ty ugraph
234 let te',inferredty,subst'',metasenv'',ugraph2 =
235 type_of_aux subst' metasenv' context te ugraph1
238 let subst''',metasenv''',ugraph3 =
239 fo_unif_subst subst'' context metasenv''
240 inferredty ty ugraph2
242 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
244 _ -> raise (RefineFailure (lazy "Cast")))
245 | C.Prod (name,s,t) ->
246 let s',sort1,subst',metasenv',ugraph1 =
247 type_of_aux subst metasenv context s ugraph
249 let t',sort2,subst'',metasenv'',ugraph2 =
250 type_of_aux subst' metasenv'
251 ((Some (name,(C.Decl s')))::context) t ugraph1
254 let sop,subst''',metasenv''',ugraph3 =
255 sort_of_prod subst'' metasenv''
256 context (name,s') (sort1,sort2) ugraph2
258 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
260 | RefineFailure _ as exn ->
261 (* given [t] of type [type_to_coerce] returns
262 * a term that has type [tgt_sort] eventually
263 * derived from (coercion [t]) *)
264 let refined_target = t' in
265 let sort_of_refined_target = sort2 in
266 let carr t subst context = CicMetaSubst.apply_subst subst t in
267 let coerce_to_sort tgt_sort t type_to_coerce subst ctx =
268 match type_to_coerce with
271 let coercion_src = carr type_to_coerce subst ctx in
272 let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
273 let search = CoercGraph.look_for_coercion in
274 (match search coercion_src coercion_tgt with
275 | CoercGraph.NoCoercion
276 | CoercGraph.NotHandled _ -> raise exn
277 | CoercGraph.NotMetaClosed ->
278 raise (Uncertain (lazy "Coercions on metas"))
279 | CoercGraph.SomeCoercion c -> Cic.Appl [c;t])
281 (* this is probably not the best... *)
282 let tgt_sort_for_pi_source = Cic.Type(CicUniv.fresh()) in
283 let tgt_sort_for_pi_target = Cic.Type(CicUniv.fresh()) in
285 coerce_to_sort tgt_sort_for_pi_source s sort1 subst context
287 let context_with_new_src =
288 ((Some (name,(C.Decl new_src)))::context)
292 tgt_sort_for_pi_target
293 refined_target sort_of_refined_target
294 subst context_with_new_src
296 let newprod = C.Prod (name,new_src,new_tgt) in
297 let _,sort_of_refined_prod,subst,metasenv,ugraph3 =
298 type_of_aux subst metasenv context newprod ugraph2
300 (* this if for a coercion on the tail of the arrow *)
302 match sort_of_refined_target with
303 | Cic.Sort _ -> refined_target
306 C.Prod(name,new_src,new_target),
307 sort_of_refined_prod,subst,metasenv,ugraph3)
308 | C.Lambda (n,s,t) ->
309 let s',sort1,subst',metasenv',ugraph1 =
310 type_of_aux subst metasenv context s ugraph
312 (match CicReduction.whd ~subst:subst' context sort1 with
316 raise (RefineFailure (lazy (sprintf
317 "Not well-typed lambda-abstraction: the source %s should be a type;
318 instead it is a term of type %s" (CicPp.ppterm s)
319 (CicPp.ppterm sort1))))
321 let t',type2,subst'',metasenv'',ugraph2 =
322 type_of_aux subst' metasenv'
323 ((Some (n,(C.Decl s')))::context) t ugraph1
325 C.Lambda (n,s',t'),C.Prod (n,s',type2),
326 subst'',metasenv'',ugraph2
328 (* only to check if s is well-typed *)
329 let s',ty,subst',metasenv',ugraph1 =
330 type_of_aux subst metasenv context s ugraph
332 let t',inferredty,subst'',metasenv'',ugraph2 =
333 type_of_aux subst' metasenv'
334 ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1
336 (* One-step LetIn reduction.
337 * Even faster than the previous solution.
338 * Moreover the inferred type is closer to the expected one.
340 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
341 subst'',metasenv'',ugraph2
342 | C.Appl (he::((_::_) as tl)) ->
343 let he',hetype,subst',metasenv',ugraph1 =
344 type_of_aux subst metasenv context he ugraph
346 let tlbody_and_type,subst'',metasenv'',ugraph2 =
348 (fun x (res,subst,metasenv,ugraph) ->
349 let x',ty,subst',metasenv',ugraph1 =
350 type_of_aux subst metasenv context x ugraph
352 (x', ty)::res,subst',metasenv',ugraph1
353 ) tl ([],subst',metasenv',ugraph1)
355 let tl',applty,subst''',metasenv''',ugraph3 =
356 eat_prods subst'' metasenv'' context
357 hetype tlbody_and_type ugraph2
359 C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
360 | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
361 | C.Const (uri,exp_named_subst) ->
362 let exp_named_subst',subst',metasenv',ugraph1 =
363 check_exp_named_subst subst metasenv context
364 exp_named_subst ugraph in
365 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
367 CicSubstitution.subst_vars exp_named_subst' ty_uri
369 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
370 | C.MutInd (uri,i,exp_named_subst) ->
371 let exp_named_subst',subst',metasenv',ugraph1 =
372 check_exp_named_subst subst metasenv context
373 exp_named_subst ugraph
375 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
377 CicSubstitution.subst_vars exp_named_subst' ty_uri in
378 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
379 | C.MutConstruct (uri,i,j,exp_named_subst) ->
380 let exp_named_subst',subst',metasenv',ugraph1 =
381 check_exp_named_subst subst metasenv context
382 exp_named_subst ugraph
385 type_of_mutual_inductive_constr uri i j ugraph1
388 CicSubstitution.subst_vars exp_named_subst' ty_uri
390 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
392 | C.MutCase (uri, i, outtype, term, pl) ->
393 (* first, get the inductive type (and noparams)
394 * in the environment *)
395 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
396 let _ = CicTypeChecker.typecheck uri in
397 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
399 C.InductiveDefinition (l,expl_params,parsno,_) ->
400 List.nth l i , expl_params, parsno, u
404 (lazy ("Unkown mutual inductive definition " ^
405 U.string_of_uri uri)))
407 let rec count_prod t =
408 match CicReduction.whd ~subst context t with
409 C.Prod (_, _, t) -> 1 + (count_prod t)
412 let no_args = count_prod arity in
413 (* now, create a "generic" MutInd *)
414 let metasenv,left_args =
415 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
417 let metasenv,right_args =
418 let no_right_params = no_args - no_left_params in
419 if no_right_params < 0 then assert false
420 else CicMkImplicit.n_fresh_metas
421 metasenv subst context no_right_params
423 let metasenv,exp_named_subst =
424 CicMkImplicit.fresh_subst metasenv subst context expl_params in
427 C.MutInd (uri,i,exp_named_subst)
430 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
432 (* check consistency with the actual type of term *)
433 let term',actual_type,subst,metasenv,ugraph1 =
434 type_of_aux subst metasenv context term ugraph in
435 let expected_type',_, subst, metasenv,ugraph2 =
436 type_of_aux subst metasenv context expected_type ugraph1
438 let actual_type = CicReduction.whd ~subst context actual_type in
439 let subst,metasenv,ugraph3 =
440 fo_unif_subst subst context metasenv
441 expected_type' actual_type ugraph2
443 let rec instantiate_prod t =
447 match CicReduction.whd ~subst context t with
449 instantiate_prod (CicSubstitution.subst he t') tl
452 let arity_instantiated_with_left_args =
453 instantiate_prod arity left_args in
454 (* TODO: check if the sort elimination
455 * is allowed: [(I q1 ... qr)|B] *)
456 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
458 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
460 if left_args = [] then
461 (C.MutConstruct (uri,i,j,exp_named_subst))
464 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
466 let p',actual_type,subst,metasenv,ugraph1 =
467 type_of_aux subst metasenv context p ugraph
469 let constructor',expected_type, subst, metasenv,ugraph2 =
470 type_of_aux subst metasenv context constructor ugraph1
472 let outtypeinstance,subst,metasenv,ugraph3 =
473 check_branch 0 context metasenv subst no_left_params
474 actual_type constructor' expected_type ugraph2
477 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
478 ([],1,[],subst,metasenv,ugraph3) pl
481 (* we are left to check that the outype matches his instances.
482 The easy case is when the outype is specified, that amount
483 to a trivial check. Otherwise, we should guess a type from
489 (let candidate,ugraph5,metasenv,subst =
490 let exp_name_subst, metasenv =
492 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
494 let uris = CicUtil.params_of_obj o in
496 fun uri (acc,metasenv) ->
497 let metasenv',new_meta =
498 CicMkImplicit.mk_implicit metasenv subst context
501 CicMkImplicit.identity_relocation_list_for_metavariable
504 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
508 match left_args,right_args with
509 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
511 let rec mk_right_args =
514 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
516 let right_args_no = List.length right_args in
517 let lifted_left_args =
518 List.map (CicSubstitution.lift right_args_no) left_args
520 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
521 (lifted_left_args @ mk_right_args right_args_no))
524 FreshNamesGenerator.mk_fresh_name ~subst metasenv
525 context Cic.Anonymous ~typ:ty
527 match outtypeinstances with
529 let extended_context =
530 let rec add_right_args =
532 Cic.Prod (name,ty,t) ->
533 Some (name,Cic.Decl ty)::(add_right_args t)
536 (Some (fresh_name,Cic.Decl ty))::
538 (add_right_args arity_instantiated_with_left_args))@
541 let metasenv,new_meta =
542 CicMkImplicit.mk_implicit metasenv subst extended_context
545 CicMkImplicit.identity_relocation_list_for_metavariable
548 let rec add_lambdas b =
550 Cic.Prod (name,ty,t) ->
551 Cic.Lambda (name,ty,(add_lambdas b t))
552 | _ -> Cic.Lambda (fresh_name, ty, b)
555 add_lambdas (Cic.Meta (new_meta,irl))
556 arity_instantiated_with_left_args
558 (Some candidate),ugraph4,metasenv,subst
559 | (constructor_args_no,_,instance,_)::tl ->
561 let instance',subst,metasenv =
562 CicMetaSubst.delift_rels subst metasenv
563 constructor_args_no instance
565 let candidate,ugraph,metasenv,subst =
567 fun (candidate_oty,ugraph,metasenv,subst)
568 (constructor_args_no,_,instance,_) ->
569 match candidate_oty with
570 | None -> None,ugraph,metasenv,subst
573 let instance',subst,metasenv =
574 CicMetaSubst.delift_rels subst metasenv
575 constructor_args_no instance
577 let subst,metasenv,ugraph =
578 fo_unif_subst subst context metasenv
581 candidate_oty,ugraph,metasenv,subst
583 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
584 | CicUnification.UnificationFailure _
585 | CicUnification.Uncertain _ ->
586 None,ugraph,metasenv,subst
587 ) (Some instance',ugraph4,metasenv,subst) tl
590 | None -> None, ugraph,metasenv,subst
592 let rec add_lambdas n b =
594 Cic.Prod (name,ty,t) ->
595 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
597 Cic.Lambda (fresh_name, ty,
598 CicSubstitution.lift (n + 1) t)
601 (add_lambdas 0 t arity_instantiated_with_left_args),
602 ugraph,metasenv,subst
603 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
604 None,ugraph4,metasenv,subst
607 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
609 let subst,metasenv,ugraph =
610 fo_unif_subst subst context metasenv
611 candidate outtype ugraph5
613 C.MutCase (uri, i, outtype, term', pl'),
614 CicReduction.head_beta_reduce
615 (CicMetaSubst.apply_subst subst
616 (Cic.Appl (outtype::right_args@[term']))),
617 subst,metasenv,ugraph)
618 | _ -> (* easy case *)
619 let _,_, subst, metasenv,ugraph5 =
620 type_of_aux subst metasenv context
621 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
623 let (subst,metasenv,ugraph6) =
625 (fun (subst,metasenv,ugraph)
626 (constructor_args_no,context,instance,args) ->
630 CicSubstitution.lift constructor_args_no outtype
632 C.Appl (outtype'::args)
634 CicReduction.whd ~subst context appl
636 fo_unif_subst subst context metasenv
637 instance instance' ugraph)
638 (subst,metasenv,ugraph5) outtypeinstances
640 C.MutCase (uri, i, outtype, term', pl'),
641 CicReduction.head_beta_reduce
642 (CicMetaSubst.apply_subst subst
643 (C.Appl(outtype::right_args@[term]))),
644 subst,metasenv,ugraph6)
646 let fl_ty',subst,metasenv,types,ugraph1 =
648 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
649 let ty',_,subst',metasenv',ugraph1 =
650 type_of_aux subst metasenv context ty ugraph
652 fl @ [ty'],subst',metasenv',
653 Some (C.Name n,(C.Decl ty')) :: types, ugraph
654 ) ([],subst,metasenv,[],ugraph) fl
656 let len = List.length types in
657 let context' = types@context in
658 let fl_bo',subst,metasenv,ugraph2 =
660 (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
661 let bo',ty_of_bo,subst,metasenv,ugraph1 =
662 type_of_aux subst metasenv context' bo ugraph
664 let subst',metasenv',ugraph' =
665 fo_unif_subst subst context' metasenv
666 ty_of_bo (CicSubstitution.lift len ty) ugraph1
668 fl @ [bo'] , subst',metasenv',ugraph'
669 ) ([],subst,metasenv,ugraph1) fl
671 let (_,_,ty,_) = List.nth fl i in
672 (* now we have the new ty in fl_ty', the new bo in fl_bo',
673 * and we want the new fl with bo' and ty' injected in the right
676 let rec map3 f l1 l2 l3 =
679 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
682 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
685 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
687 let fl_ty',subst,metasenv,types,ugraph1 =
689 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
690 let ty',_,subst',metasenv',ugraph1 =
691 type_of_aux subst metasenv context ty ugraph
693 fl @ [ty'],subst',metasenv',
694 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
695 ) ([],subst,metasenv,[],ugraph) fl
697 let len = List.length types in
698 let context' = types@context in
699 let fl_bo',subst,metasenv,ugraph2 =
701 (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
702 let bo',ty_of_bo,subst,metasenv,ugraph1 =
703 type_of_aux subst metasenv context' bo ugraph
705 let subst',metasenv',ugraph' =
706 fo_unif_subst subst context' metasenv
707 ty_of_bo (CicSubstitution.lift len ty) ugraph1
709 fl @ [bo'],subst',metasenv',ugraph'
710 ) ([],subst,metasenv,ugraph1) fl
712 let (_,ty,_) = List.nth fl i in
713 (* now we have the new ty in fl_ty', the new bo in fl_bo',
714 * and we want the new fl with bo' and ty' injected in the right
717 let rec map3 f l1 l2 l3 =
720 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
723 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
726 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
728 (* check_metasenv_consistency checks that the "canonical" context of a
729 metavariable is consitent - up to relocation via the relocation list l -
730 with the actual context *)
731 and check_metasenv_consistency
732 metano subst metasenv context canonical_context l ugraph
734 let module C = Cic in
735 let module R = CicReduction in
736 let module S = CicSubstitution in
737 let lifted_canonical_context =
741 | (Some (n,C.Decl t))::tl ->
742 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
743 | (Some (n,C.Def (t,None)))::tl ->
744 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
745 | None::tl -> None::(aux (i+1) tl)
746 | (Some (n,C.Def (t,Some ty)))::tl ->
748 C.Def ((S.subst_meta l (S.lift i t)),
749 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
751 aux 1 canonical_context
755 (fun (l,subst,metasenv,ugraph) t ct ->
758 l @ [None],subst,metasenv,ugraph
759 | Some t,Some (_,C.Def (ct,_)) ->
760 let subst',metasenv',ugraph' =
762 fo_unif_subst subst context metasenv t ct ugraph
763 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))))))
765 l @ [Some t],subst',metasenv',ugraph'
766 | Some t,Some (_,C.Decl ct) ->
767 let t',inferredty,subst',metasenv',ugraph1 =
768 type_of_aux subst metasenv context t ugraph
770 let subst'',metasenv'',ugraph2 =
773 subst' context metasenv' inferredty ct ugraph1
774 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 | _ -> (Printexc.to_string e))))))
776 l @ [Some t'], subst'',metasenv'',ugraph2
778 raise (RefineFailure (lazy (sprintf
779 "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"
780 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
781 (CicMetaSubst.ppcontext subst canonical_context))))
782 ) ([],subst,metasenv,ugraph) l lifted_canonical_context
784 Invalid_argument _ ->
788 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
789 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
790 (CicMetaSubst.ppcontext subst canonical_context))))
792 and check_exp_named_subst metasubst metasenv context tl ugraph =
793 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
795 [] -> [],metasubst,metasenv,ugraph
796 | ((uri,t) as subst)::tl ->
797 let ty_uri,ugraph1 = type_of_variable uri ugraph in
799 CicSubstitution.subst_vars substs ty_uri in
800 (* CSC: why was this code here? it is wrong
801 (match CicEnvironment.get_cooked_obj ~trust:false uri with
802 Cic.Variable (_,Some bo,_,_) ->
804 (RefineFailure (Reason
805 "A variable with a body can not be explicit substituted"))
806 | Cic.Variable (_,None,_,_) -> ()
809 (RefineFailure (Reason
810 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
813 let t',typeoft,metasubst',metasenv',ugraph2 =
814 type_of_aux metasubst metasenv context t ugraph1
816 let metasubst'',metasenv'',ugraph3 =
819 metasubst' context metasenv' typeoft typeofvar ugraph2
821 raise (RefineFailure (lazy
822 ("Wrong Explicit Named Substitution: " ^
823 CicMetaSubst.ppterm metasubst' typeoft ^
824 " not unifiable with " ^
825 CicMetaSubst.ppterm metasubst' typeofvar)))
827 (* FIXME: no mere tail recursive! *)
828 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
829 check_exp_named_subst_aux
830 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
832 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
834 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
837 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
838 let module C = Cic in
839 let context_for_t2 = (Some (name,C.Decl s))::context in
840 let t1'' = CicReduction.whd ~subst context t1 in
841 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
842 match (t1'', t2'') with
843 (C.Sort s1, C.Sort s2)
844 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
845 (* different than Coq manual!!! *)
846 C.Sort s2,subst,metasenv,ugraph
847 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
848 let t' = CicUniv.fresh() in
849 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
850 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
851 C.Sort (C.Type t'),subst,metasenv,ugraph2
852 | (C.Sort _,C.Sort (C.Type t1)) ->
853 C.Sort (C.Type t1),subst,metasenv,ugraph
854 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
855 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
856 (* TODO how can we force the meta to become a sort? If we don't we
857 * brake the invariant that refine produce only well typed terms *)
858 (* TODO if we check the non meta term and if it is a sort then we
859 * are likely to know the exact value of the result e.g. if the rhs
860 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
862 CicMkImplicit.mk_implicit_sort metasenv subst in
863 let (subst, metasenv,ugraph1) =
864 fo_unif_subst subst context_for_t2 metasenv
865 (C.Meta (idx,[])) t2'' ugraph
867 t2'',subst,metasenv,ugraph1
873 ("Two sorts were expected, found %s " ^^
874 "(that reduces to %s) and %s (that reduces to %s)")
875 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
876 (CicPp.ppterm t2''))))
878 and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
879 let rec mk_prod metasenv context =
882 let (metasenv, idx) =
883 CicMkImplicit.mk_implicit_type metasenv subst context
886 CicMkImplicit.identity_relocation_list_for_metavariable context
888 metasenv,Cic.Meta (idx, irl)
890 let (metasenv, idx) =
891 CicMkImplicit.mk_implicit_type metasenv subst context
894 CicMkImplicit.identity_relocation_list_for_metavariable context
896 let meta = Cic.Meta (idx,irl) in
898 (* The name must be fresh for context. *)
899 (* Nevertheless, argty is well-typed only in context. *)
900 (* Thus I generate a name (name_hint) in context and *)
901 (* then I generate a name --- using the hint name_hint *)
902 (* --- that is fresh in (context'@context). *)
904 (* Cic.Name "pippo" *)
905 FreshNamesGenerator.mk_fresh_name ~subst metasenv
906 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
907 (CicMetaSubst.apply_subst_context subst context)
909 ~typ:(CicMetaSubst.apply_subst subst argty)
911 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
912 FreshNamesGenerator.mk_fresh_name ~subst
913 [] context name_hint ~typ:(Cic.Sort Cic.Prop)
915 let metasenv,target =
916 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
918 metasenv,Cic.Prod (name,meta,target)
920 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
921 let (subst, metasenv,ugraph1) =
923 fo_unif_subst subst context metasenv hetype hetype' ugraph
925 debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
926 (CicPp.ppterm hetype)
927 (CicPp.ppterm hetype')
928 (CicMetaSubst.ppmetasenv [] metasenv)
929 (CicMetaSubst.ppsubst subst)));
933 let rec eat_prods metasenv subst context hetype ugraph =
935 | [] -> [],metasenv,subst,hetype,ugraph
936 | (hete, hety)::tl ->
939 let arg,subst,metasenv,ugraph1 =
941 let subst,metasenv,ugraph1 =
942 fo_unif_subst subst context metasenv hety s ugraph
944 hete,subst,metasenv,ugraph1
946 (* we search a coercion from hety to s *)
948 let carr t subst context =
949 CicMetaSubst.apply_subst subst t
951 let c_hety = carr hety subst context in
952 let c_s = carr s subst context in
953 CoercGraph.look_for_coercion c_hety c_s
956 | CoercGraph.NoCoercion
957 | CoercGraph.NotHandled _ -> raise exn
958 | CoercGraph.NotMetaClosed ->
959 raise (Uncertain (lazy "Coercions on meta"))
960 | CoercGraph.SomeCoercion c ->
961 (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
963 let coerced_args,metasenv',subst',t',ugraph2 =
964 eat_prods metasenv subst context
965 (* (CicMetaSubst.subst subst hete t) tl *)
966 (CicSubstitution.subst hete t) ugraph1 tl
968 arg::coerced_args,metasenv',subst',t',ugraph2
972 let coerced_args,metasenv,subst,t,ugraph2 =
973 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
975 coerced_args,t,subst,metasenv,ugraph2
978 (* eat prods ends here! *)
980 let t',ty,subst',metasenv',ugraph1 =
981 type_of_aux [] metasenv context t ugraph
983 let substituted_t = CicMetaSubst.apply_subst subst' t' in
984 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
985 (* Andrea: ho rimesso qui l'applicazione della subst al
986 metasenv dopo che ho droppato l'invariante che il metsaenv
987 e' sempre istanziato *)
988 let substituted_metasenv =
989 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
991 (* substituted_t,substituted_ty,substituted_metasenv *)
992 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
994 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
996 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
997 let cleaned_metasenv =
999 (function (n,context,ty) ->
1000 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1005 | Some (n, Cic.Decl t) ->
1007 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1008 | Some (n, Cic.Def (bo,ty)) ->
1009 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1014 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1016 Some (n, Cic.Def (bo',ty'))
1020 ) substituted_metasenv
1022 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1025 let type_of_aux' metasenv context term ugraph =
1027 type_of_aux' metasenv context term ugraph
1029 CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
1031 (*CSC: this is a very very rough approximation; to be finished *)
1032 let are_all_occurrences_positive uri =
1034 (*CSC: here we should do a whd; but can we do that? *)
1036 Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> ()
1037 | Cic.MutInd (uri',_,_) when uri = uri' -> ()
1038 | Cic.Prod (_,_,t) -> aux t
1039 | _ -> raise (RefineFailure (lazy "not well formed constructor type"))
1043 let typecheck metasenv uri obj =
1044 let ugraph = CicUniv.empty_ugraph in
1046 Cic.Constant (name,Some bo,ty,args,attrs) ->
1047 let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
1048 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1049 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1050 let bo' = CicMetaSubst.apply_subst subst bo' in
1051 let ty' = CicMetaSubst.apply_subst subst ty' in
1052 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1053 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1054 | Cic.Constant (name,None,ty,args,attrs) ->
1055 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1056 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1057 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1058 assert (metasenv' = metasenv);
1059 (* Here we do not check the metasenv for correctness *)
1060 let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
1061 let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1065 (* instead of raising Uncertain, let's hope that the meta will become
1068 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1070 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1071 let bo' = CicMetaSubst.apply_subst subst bo' in
1072 let ty' = CicMetaSubst.apply_subst subst ty' in
1073 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1074 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1075 | Cic.Variable _ -> assert false (* not implemented *)
1076 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1077 (*CSC: this code is greately simplified and many many checks are missing *)
1078 (*CSC: e.g. the constructors are not required to build their own types, *)
1079 (*CSC: the arities are not required to have as type a sort, etc. *)
1080 let uri = match uri with Some uri -> uri | None -> assert false in
1081 let typesno = List.length tys in
1082 (* first phase: we fix only the types *)
1083 let metasenv,ugraph,tys =
1085 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1086 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1087 metasenv,ugraph,(name,b,ty',cl)::res
1088 ) tys (metasenv,ugraph,[]) in
1090 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1091 (* second phase: we fix only the constructors *)
1092 let metasenv,ugraph,tys =
1094 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1095 let metasenv,ugraph,cl' =
1097 (fun (name,ty) (metasenv,ugraph,res) ->
1098 let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
1099 let ty',_,metasenv,ugraph =
1100 type_of_aux' metasenv con_context ty ugraph in
1104 (fun (name,_,_,_) (i,t) ->
1105 (* here the explicit_named_substituion is assumed to be *)
1107 let t' = Cic.MutInd (uri,i,[]) in
1108 let t = CicSubstitution.subst t' t in
1110 ) tys (typesno - 1,t)) in
1111 let ty' = undebrujin ty' in
1112 metasenv,ugraph,(name,ty')::res
1113 ) cl (metasenv,ugraph,[])
1115 metasenv,ugraph,(name,b,ty,cl')::res
1116 ) tys (metasenv,ugraph,[]) in
1117 (* third phase: we check the positivity condition *)
1120 List.iter (fun (_,ty) -> are_all_occurrences_positive uri ty) cl
1122 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1125 let type_of_aux' metasenv context term =
1128 type_of_aux' metasenv context term in
1130 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1132 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1135 | RefineFailure msg as e ->
1136 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1138 | Uncertain msg as e ->
1139 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1143 let profiler2 = HExtlib.profile "CicRefine"
1145 let type_of_aux' metasenv context term ugraph =
1146 profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph
1148 let typecheck metasenv uri obj =
1149 profiler2.HExtlib.profile (typecheck metasenv uri) obj