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;;
29 exception Uncertain of string;;
30 exception AssertFailure of string;;
32 let debug_print = prerr_endline
34 let fo_unif_subst subst context metasenv t1 t2 =
36 CicUnification.fo_unif_subst subst context metasenv t1 t2
38 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
39 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
45 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
46 | (_,_) -> raise (AssertFailure "split: list too short")
49 let rec type_of_constant uri =
51 let module R = CicReduction in
52 let module U = UriManager in
53 match CicEnvironment.get_cooked_obj uri with
54 C.Constant (_,_,ty,_) -> ty
55 | C.CurrentProof (_,_,_,ty,_) -> ty
58 (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri))
60 and type_of_variable uri =
62 let module R = CicReduction in
63 let module U = UriManager in
64 match CicEnvironment.get_cooked_obj uri with
65 C.Variable (_,_,ty,_) -> ty
69 ("Unknown variable definition " ^ UriManager.string_of_uri uri))
71 and type_of_mutual_inductive_defs uri i =
73 let module R = CicReduction in
74 let module U = UriManager in
75 match CicEnvironment.get_cooked_obj uri with
76 C.InductiveDefinition (dl,_,_) ->
77 let (_,_,arity,_) = List.nth dl i in
82 ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
84 and type_of_mutual_inductive_constr uri i j =
86 let module R = CicReduction in
87 let module U = UriManager in
88 match CicEnvironment.get_cooked_obj uri with
89 C.InductiveDefinition (dl,_,_) ->
90 let (_,_,_,cl) = List.nth dl i in
91 let (_,ty) = List.nth cl (j-1) in
96 ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
98 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
100 (* the check_branch function checks if a branch of a case is refinable.
101 It returns a pair (outype_instance,args), a subst and a metasenv.
102 outype_instance is the expected result of applying the case outtype
104 The problem is that outype is in general unknown, and we should
105 try to synthesize it from the above information, that is in general
106 a second order unification problem. *)
108 and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
109 let module C = Cic in
110 let module R = CicMetaSubst in
111 match R.whd subst context expectedtype with
113 (n,context,actualtype, [term]), subst, metasenv
114 | C.Appl (C.MutInd (_,_,_)::tl) ->
115 let (_,arguments) = split tl left_args_no in
116 (n,context,actualtype, arguments@[term]), subst, metasenv
117 | C.Prod (name,so,de) ->
118 (* we expect that the actual type of the branch has the due
120 (match R.whd subst context actualtype with
121 C.Prod (name',so',de') ->
122 let subst, metasenv =
123 fo_unif_subst subst context metasenv so so' in
125 (match CicSubstitution.lift 1 term with
126 C.Appl l -> C.Appl (l@[C.Rel 1])
127 | t -> C.Appl [t ; C.Rel 1]) in
128 (* we should also check that the name variable is anonymous in
129 the actual type de' ?? *)
130 check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de
131 | _ -> raise (AssertFailure "Wrong number of arguments"))
132 | _ -> raise (AssertFailure "Prod or MutInd expected")
134 and type_of_aux' metasenv context t =
135 let rec type_of_aux subst metasenv context =
136 let module C = Cic in
137 let module S = CicSubstitution in
138 let module U = UriManager in
142 match List.nth context (n - 1) with
143 Some (_,C.Decl t) -> S.lift n t,subst,metasenv
144 | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
145 | Some (_,C.Def (bo,None)) ->
146 type_of_aux subst metasenv context (S.lift n bo)
147 | None -> raise (RefineFailure "Rel to hidden hypothesis")
149 _ -> raise (RefineFailure "Not a close term")
151 | C.Var (uri,exp_named_subst) ->
152 let subst',metasenv' =
153 check_exp_named_subst subst metasenv context exp_named_subst in
155 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
159 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
160 let subst',metasenv' =
161 check_metasenv_consistency n subst metasenv context canonical_context l
163 CicSubstitution.lift_meta l ty, subst', metasenv'
165 C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
167 | C.Implicit _ -> raise (AssertFailure "21")
169 let _,subst',metasenv' =
170 type_of_aux subst metasenv context ty in
171 let inferredty,subst'',metasenv'' =
172 type_of_aux subst' metasenv' context te
175 let subst''',metasenv''' =
176 fo_unif_subst subst'' context metasenv'' inferredty ty
178 ty,subst''',metasenv'''
180 _ -> raise (RefineFailure "Cast"))
181 | C.Prod (name,s,t) ->
182 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
183 let sort2,subst'',metasenv'' =
184 type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
186 sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
187 | C.Lambda (n,s,t) ->
188 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
189 (match CicMetaSubst.whd subst' context sort1 with
193 raise (RefineFailure (sprintf
194 "Not well-typed lambda-abstraction: the source %s should be a type;
195 instead it is a term of type %s" (CicPp.ppterm s)
196 (CicPp.ppterm sort1)))
198 let type2,subst'',metasenv'' =
199 type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
201 C.Prod (n,s,type2),subst'',metasenv''
203 (* only to check if s is well-typed *)
204 let ty,subst',metasenv' = type_of_aux subst metasenv context s in
205 let inferredty,subst'',metasenv'' =
206 type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
208 (* One-step LetIn reduction. Even faster than the previous solution.
209 Moreover the inferred type is closer to the expected one. *)
210 CicSubstitution.subst s inferredty,subst',metasenv'
211 | C.Appl (he::tl) when List.length tl > 0 ->
212 let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
213 let tlbody_and_type,subst'',metasenv'' =
215 (fun x (res,subst,metasenv) ->
216 let ty,subst',metasenv' =
217 type_of_aux subst metasenv context x
219 (x, ty)::res,subst',metasenv'
220 ) tl ([],subst',metasenv')
222 eat_prods subst'' metasenv'' context hetype tlbody_and_type
223 | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
224 | C.Const (uri,exp_named_subst) ->
225 let subst',metasenv' =
226 check_exp_named_subst subst metasenv context exp_named_subst in
228 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
231 | C.MutInd (uri,i,exp_named_subst) ->
232 let subst',metasenv' =
233 check_exp_named_subst subst metasenv context exp_named_subst in
235 CicSubstitution.subst_vars exp_named_subst
236 (type_of_mutual_inductive_defs uri i)
239 | C.MutConstruct (uri,i,j,exp_named_subst) ->
240 let subst',metasenv' =
241 check_exp_named_subst subst metasenv context exp_named_subst in
243 CicSubstitution.subst_vars exp_named_subst
244 (type_of_mutual_inductive_constr uri i j)
247 | C.MutCase (uri, i, outtype, term, pl) ->
248 (* first, get the inductive type (and noparams) in the environment *)
249 let (_,b,arity,constructors), expl_params, no_left_params =
250 match CicEnvironment.get_cooked_obj ~trust:true uri with
251 C.InductiveDefinition (l,expl_params,parsno) ->
252 List.nth l i , expl_params, parsno
256 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
257 let rec count_prod t =
258 match CicMetaSubst.whd subst context t with
259 C.Prod (_, _, t) -> 1 + (count_prod t)
261 let no_args = count_prod arity in
262 (* now, create a "generic" MutInd *)
263 let metasenv,left_args =
264 CicMkImplicit.n_fresh_metas metasenv context no_left_params in
265 let metasenv,right_args =
266 let no_right_params = no_args - no_left_params in
267 if no_right_params < 0 then assert false
268 else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
269 let metasenv,exp_named_subst =
270 CicMkImplicit.fresh_subst metasenv context expl_params in
273 C.MutInd (uri,i,exp_named_subst)
275 C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
277 (* check consistency with the actual type of term *)
278 let actual_type,subst,metasenv =
279 type_of_aux subst metasenv context term in
280 let _, subst, metasenv =
281 type_of_aux subst metasenv context expected_type
283 let actual_type = CicMetaSubst.whd subst context actual_type in
285 fo_unif_subst subst context metasenv expected_type actual_type
287 (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
288 let (_,outtypeinstances,subst,metasenv) =
290 (fun (j,outtypeinstances,subst,metasenv) p ->
292 if left_args = [] then
293 (C.MutConstruct (uri,i,j,exp_named_subst))
295 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
297 let actual_type,subst,metasenv =
298 type_of_aux subst metasenv context p in
299 let expected_type, subst, metasenv =
300 type_of_aux subst metasenv context constructor in
301 let outtypeinstance,subst,metasenv =
303 0 context metasenv subst
304 no_left_params actual_type constructor expected_type in
305 (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
306 (1,[],subst,metasenv) pl in
307 (* we are left to check that the outype matches his instances.
308 The easy case is when the outype is specified, that amount
309 to a trivial check. Otherwise, we should guess a type from
313 let _, subst, metasenv =
314 type_of_aux subst metasenv context
315 (C.Appl ((outtype :: right_args) @ [term]))
317 let (subst,metasenv) =
319 (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
323 CicSubstitution.lift constructor_args_no outtype
325 C.Appl (outtype'::args)
328 (* if appl is not well typed then the type_of below solves the
330 let (_, subst, metasenv) =
331 type_of_aux subst metasenv context appl
334 CicMetaSubst.whd subst context appl
336 fo_unif_subst subst context metasenv instance instance')
337 (subst,metasenv) outtypeinstances in
338 CicMetaSubst.whd subst
339 context (C.Appl(outtype::right_args@[term])),subst,metasenv
341 let subst,metasenv,types =
343 (fun (subst,metasenv,types) (n,_,ty,_) ->
344 let _,subst',metasenv' = type_of_aux subst metasenv context ty in
345 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
346 ) (subst,metasenv,[]) fl
348 let len = List.length types in
349 let context' = types@context in
352 (fun (subst,metasenv) (name,x,ty,bo) ->
353 let ty_of_bo,subst,metasenv =
354 type_of_aux subst metasenv context' bo
356 fo_unif_subst subst context' metasenv
357 ty_of_bo (CicMetaSubst.lift subst len ty)
358 ) (subst,metasenv) fl in
359 let (_,_,ty,_) = List.nth fl i in
362 let subst,metasenv,types =
364 (fun (subst,metasenv,types) (n,ty,_) ->
365 let _,subst',metasenv' = type_of_aux subst metasenv context ty in
366 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
367 ) (subst,metasenv,[]) fl
369 let len = List.length types in
370 let context' = types@context in
373 (fun (subst,metasenv) (name,ty,bo) ->
374 let ty_of_bo,subst,metasenv =
375 type_of_aux subst metasenv context' bo
377 fo_unif_subst subst context' metasenv
378 ty_of_bo (CicMetaSubst.lift subst len ty)
379 ) (subst,metasenv) fl in
381 let (_,ty,_) = List.nth fl i in
384 (* check_metasenv_consistency checks that the "canonical" context of a
385 metavariable is consitent - up to relocation via the relocation list l -
386 with the actual context *)
387 and check_metasenv_consistency
388 metano subst metasenv context canonical_context l
390 let module C = Cic in
391 let module R = CicReduction in
392 let module S = CicSubstitution in
393 let lifted_canonical_context =
397 | (Some (n,C.Decl t))::tl ->
398 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
399 | (Some (n,C.Def (t,None)))::tl ->
400 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
401 | None::tl -> None::(aux (i+1) tl)
402 | (Some (n,C.Def (t,Some ty)))::tl ->
404 C.Def ((S.lift_meta l (S.lift i t)),
405 Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
407 aux 1 canonical_context
411 (fun (subst,metasenv) t ct ->
415 | Some t,Some (_,C.Def (ct,_)) ->
417 fo_unif_subst subst context metasenv t ct
418 with e -> raise (RefineFailure (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 -> msg | _ -> (Printexc.to_string e)))))
419 | Some t,Some (_,C.Decl ct) ->
420 let inferredty,subst',metasenv' =
421 type_of_aux subst metasenv context t
425 subst' context metasenv' inferredty ct
426 with e -> raise (RefineFailure (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 -> msg | _ -> (Printexc.to_string e)))))
428 raise (RefineFailure (sprintf
429 "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"
430 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
431 (CicMetaSubst.ppcontext subst canonical_context)))
432 ) (subst,metasenv) l lifted_canonical_context
434 Invalid_argument _ ->
438 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
439 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
440 (CicMetaSubst.ppcontext subst canonical_context)))
442 and check_exp_named_subst metasubst metasenv context =
443 let rec check_exp_named_subst_aux metasubst metasenv substs =
445 [] -> metasubst,metasenv
446 | ((uri,t) as subst)::tl ->
448 CicSubstitution.subst_vars substs (type_of_variable uri) in
449 (match CicEnvironment.get_cooked_obj ~trust:false uri with
450 Cic.Variable (_,Some bo,_,_) ->
453 "A variable with a body can not be explicit substituted")
454 | Cic.Variable (_,None,_,_) -> ()
458 ("Unkown variable definition " ^ UriManager.string_of_uri uri))
460 let typeoft,metasubst',metasenv' =
461 type_of_aux metasubst metasenv context t
464 let metasubst'',metasenv'' =
465 fo_unif_subst metasubst' context metasenv' typeoft typeofvar
467 check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
469 raise (RefineFailure "Wrong Explicit Named Substitution")
471 check_exp_named_subst_aux metasubst metasenv []
473 and sort_of_prod subst metasenv context (name,s) (t1, t2) =
474 let module C = Cic in
475 let context_for_t2 = (Some (name,C.Decl s))::context in
476 let t1'' = CicMetaSubst.whd subst context t1 in
477 let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in
478 match (t1'', t2'') with
479 (C.Sort s1, C.Sort s2)
480 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
481 C.Sort s2,subst,metasenv
482 | (C.Sort s1, C.Sort s2) ->
483 (*CSC manca la gestione degli universi!!! *)
484 C.Sort C.Type,subst,metasenv
485 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
486 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
487 (* TODO how can we force the meta to become a sort? If we don't we
488 * brake the invariant that refine produce only well typed terms *)
489 (* TODO if we check the non meta term and if it is a sort then we are
490 * likely to know the exact value of the result e.g. if the rhs is a
491 * Sort (Prop | Set | CProp) then the result is the rhs *)
493 CicMkImplicit.mk_implicit_sort metasenv in
494 let (subst, metasenv) =
495 fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
499 raise (RefineFailure (sprintf
500 "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
501 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
502 (CicPp.ppterm t2'')))
504 and eat_prods subst metasenv context hetype tlbody_and_type =
505 let rec mk_prod metasenv context =
508 let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
510 CicMkImplicit.identity_relocation_list_for_metavariable context
512 metasenv,Cic.Meta (idx, irl)
514 let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
516 CicMkImplicit.identity_relocation_list_for_metavariable context
518 let meta = Cic.Meta (idx,irl) in
520 (* The name must be fresh for context. *)
521 (* Nevertheless, argty is well-typed only in context. *)
522 (* Thus I generate a name (name_hint) in context and *)
523 (* then I generate a name --- using the hint name_hint *)
524 (* --- that is fresh in (context'@context). *)
526 FreshNamesGenerator.mk_fresh_name
527 (CicMetaSubst.apply_subst_metasenv subst metasenv)
528 (CicMetaSubst.apply_subst_context subst context)
530 (CicMetaSubst.apply_subst subst argty)
532 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
533 FreshNamesGenerator.mk_fresh_name
534 [] context name_hint (Cic.Sort Cic.Prop)
536 let metasenv,target =
537 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
539 metasenv,Cic.Prod (name,meta,target)
541 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
542 let (subst, metasenv) =
543 fo_unif_subst subst context metasenv hetype hetype'
545 let rec eat_prods metasenv subst context hetype =
547 [] -> metasenv,subst,hetype
548 | (hete, hety)::tl ->
552 fo_unif_subst subst context metasenv hety s
554 eat_prods metasenv subst context
555 (CicMetaSubst.subst subst hete t) tl
559 let metasenv,subst,t =
560 eat_prods metasenv subst context hetype' tlbody_and_type
564 let rec aux context' args (resty,subst,metasenv) =
566 [] -> resty,subst,metasenv
572 | Some t -> Some (CicMetaSubst.lift subst 1 t)
574 let argty' = CicMetaSubst.lift subst (List.length args) argty in
576 (* The name must be fresh for (context'@context). *)
577 (* Nevertheless, argty is well-typed only in context. *)
578 (* Thus I generate a name (name_hint) in context and *)
579 (* then I generate a name --- using the hint name_hint *)
580 (* --- that is fresh in (context'@context). *)
582 FreshNamesGenerator.mk_fresh_name
583 (CicMetaSubst.apply_subst_metasenv subst metasenv)
584 (CicMetaSubst.apply_subst_context subst context)
586 (CicMetaSubst.apply_subst subst argty)
588 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
589 FreshNamesGenerator.mk_fresh_name
590 [] (context'@context) name_hint (Cic.Sort Cic.Prop)
592 let context'' = Some (name, Cic.Decl argty') :: context' in
593 let (metasenv, idx) =
594 CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
596 (Some (Cic.Rel 1))::args' @
597 (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
600 let newmeta = Cic.Meta (idx, irl) in
601 let prod = Cic.Prod (name, argty, newmeta) in
602 let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
603 let (subst, metasenv) =
604 fo_unif_subst subst context metasenv resty prod
606 aux context'' (Some arg :: args)
607 (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
609 aux [] [] (hetype,subst,metasenv) tlbody_and_type
612 let ty,subst',metasenv' =
613 type_of_aux [] metasenv context t
615 let substituted_t = CicMetaSubst.apply_subst subst' t in
616 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
617 let substituted_metasenv =
618 CicMetaSubst.apply_subst_metasenv subst' metasenv'
621 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
623 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
624 let cleaned_metasenv =
626 (function (n,context,ty) ->
627 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
632 | Some (n, Cic.Decl t) ->
634 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
635 | Some (n, Cic.Def (bo,ty)) ->
636 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
641 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
643 Some (n, Cic.Def (bo',ty'))
647 ) substituted_metasenv
649 (cleaned_t,cleaned_ty,cleaned_metasenv)
654 let type_of_aux' metasenv context term =
656 let (t,ty,m) = type_of_aux' metasenv context term in
658 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
661 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
665 | RefineFailure msg as e ->
666 debug_print ("@@@ REFINE FAILED: " ^ msg);
668 | Uncertain msg as e ->
669 debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);