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;;
30 exception Impossible of int;;
31 exception NotRefinable of string;;
32 exception Uncertain of string;;
33 exception WrongUriToConstant of string;;
34 exception WrongUriToVariable of string;;
35 exception ListTooShort;;
36 exception WrongUriToMutualInductiveDefinitions of string;;
37 exception RelToHiddenHypothesis;;
38 exception WrongArgumentNumber;;
42 let rec debug_aux t i =
44 let module U = UriManager in
45 CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
48 raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
49 (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
52 let debug_print = prerr_endline
57 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
58 | (_,_) -> raise ListTooShort
61 let rec type_of_constant uri =
63 let module R = CicReduction in
64 let module U = UriManager in
65 match CicEnvironment.get_cooked_obj uri with
66 C.Constant (_,_,ty,_) -> ty
67 | C.CurrentProof (_,_,_,ty,_) -> ty
68 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
70 and type_of_variable uri =
72 let module R = CicReduction in
73 let module U = UriManager in
74 match CicEnvironment.get_cooked_obj uri with
75 C.Variable (_,_,ty,_) -> ty
76 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
78 and type_of_mutual_inductive_defs uri i =
80 let module R = CicReduction in
81 let module U = UriManager in
82 match CicEnvironment.get_cooked_obj uri with
83 C.InductiveDefinition (dl,_,_) ->
84 let (_,_,arity,_) = List.nth dl i in
86 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
88 and type_of_mutual_inductive_constr uri i j =
90 let module R = CicReduction in
91 let module U = UriManager in
92 match CicEnvironment.get_cooked_obj uri with
93 C.InductiveDefinition (dl,_,_) ->
94 let (_,_,_,cl) = List.nth dl i in
95 let (_,ty) = List.nth cl (j-1) in
97 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
99 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
101 (* the check_branch function checks if a branch of a case is refinable.
102 It returns a pair (outype_instance,args), a subst and a metasenv.
103 outype_instance is the expected result of applying the case outtype
105 The problem is that outype is in general unknown, and we should
106 try to synthesize it from the above information, that is in general
107 a second order unification problem. *)
109 and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
110 let module C = Cic in
111 let module R = CicMetaSubst in
112 let module Un = CicUnification in
113 match R.whd subst context expectedtype with
115 (n,context,actualtype, [term]), subst, metasenv
116 | C.Appl (C.MutInd (_,_,_)::tl) ->
117 let (_,arguments) = split tl left_args_no in
118 (n,context,actualtype, arguments@[term]), subst, metasenv
119 | C.Prod (name,so,de) ->
120 (* we expect that the actual type of the branch has the due
122 (match R.whd subst context actualtype with
123 C.Prod (name',so',de') ->
124 let subst, metasenv =
125 Un.fo_unif_subst subst context metasenv so so' in
127 (match CicSubstitution.lift 1 term with
128 C.Appl l -> C.Appl (l@[C.Rel 1])
129 | t -> C.Appl [t ; C.Rel 1]) in
130 (* we should also check that the name variable is anonymous in
131 the actual type de' ?? *)
132 check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de
133 | _ -> raise WrongArgumentNumber)
134 | _ -> raise (NotRefinable "Prod or MutInd expected")
136 and type_of_aux' metasenv context t =
137 let rec type_of_aux subst metasenv context =
138 let module C = Cic in
139 let module S = CicSubstitution in
140 let module U = UriManager in
141 let module Un = CicUnification in
145 match List.nth context (n - 1) with
146 Some (_,C.Decl t) -> S.lift n t,subst,metasenv
147 | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
148 | Some (_,C.Def (bo,None)) ->
149 type_of_aux subst metasenv context (S.lift n bo)
150 | None -> raise RelToHiddenHypothesis
152 _ -> raise (NotRefinable "Not a close term")
154 | C.Var (uri,exp_named_subst) ->
156 let subst',metasenv' =
157 check_exp_named_subst subst metasenv context exp_named_subst in
159 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
164 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
165 let subst',metasenv' =
166 check_metasenv_consistency n subst metasenv context canonical_context l
168 CicSubstitution.lift_meta l ty, subst', metasenv'
170 C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
172 | C.Implicit -> raise (Impossible 21)
174 let _,subst',metasenv' =
175 type_of_aux subst metasenv context ty in
176 let inferredty,subst'',metasenv'' =
177 type_of_aux subst' metasenv' context te
180 let subst''',metasenv''' =
181 Un.fo_unif_subst subst'' context metasenv'' inferredty ty
183 ty,subst''',metasenv'''
185 _ -> raise (NotRefinable "Cast"))
186 | C.Prod (name,s,t) ->
187 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
188 let sort2,subst'',metasenv'' =
189 type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
191 sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2),
193 | C.Lambda (n,s,t) ->
194 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
195 let type2,subst'',metasenv'' =
196 type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
198 let sort2,subst''',metasenv''' =
199 type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
201 (* only to check if the product is well-typed *)
203 sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
205 C.Prod (n,s,type2),subst''',metasenv'''
207 (* only to check if s is well-typed *)
208 let ty,subst',metasenv' = type_of_aux subst metasenv context s in
209 let inferredty,subst'',metasenv'' =
210 type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
212 (* One-step LetIn reduction. Even faster than the previous solution.
213 Moreover the inferred type is closer to the expected one. *)
214 CicSubstitution.subst s inferredty,subst',metasenv'
215 | C.Appl (he::tl) when List.length tl > 0 ->
216 let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
217 let tlbody_and_type,subst'',metasenv'' =
219 (fun x (res,subst,metasenv) ->
220 let ty,subst',metasenv' =
221 type_of_aux subst metasenv context x
223 (x, ty)::res,subst',metasenv'
224 ) tl ([],subst',metasenv')
226 eat_prods subst'' metasenv'' context hetype tlbody_and_type
227 | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
228 | C.Const (uri,exp_named_subst) ->
230 let subst',metasenv' =
231 check_exp_named_subst subst metasenv context exp_named_subst in
233 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
237 | C.MutInd (uri,i,exp_named_subst) ->
239 let subst',metasenv' =
240 check_exp_named_subst subst metasenv context exp_named_subst in
242 CicSubstitution.subst_vars exp_named_subst
243 (type_of_mutual_inductive_defs uri i)
247 | C.MutConstruct (uri,i,j,exp_named_subst) ->
248 let subst',metasenv' =
249 check_exp_named_subst subst metasenv context exp_named_subst in
251 CicSubstitution.subst_vars exp_named_subst
252 (type_of_mutual_inductive_constr uri i j)
255 | C.MutCase (uri, i, outtype, term, pl) ->
256 (* first, get the inductive type (and noparams) in the environment *)
257 let (_,b,arity,constructors), expl_params, no_left_params =
258 match CicEnvironment.get_cooked_obj ~trust:true uri with
259 C.InductiveDefinition (l,expl_params,parsno) ->
260 List.nth l i , expl_params, parsno
263 (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
264 let rec count_prod t =
265 match CicMetaSubst.whd subst context t with
266 C.Prod (_, _, t) -> 1 + (count_prod t)
268 let no_args = count_prod arity in
269 (* now, create a "generic" MutInd *)
270 let metasenv,left_args =
271 CicMkImplicit.n_fresh_metas metasenv context no_left_params in
272 let metasenv,right_args =
273 let no_right_params = no_args - no_left_params in
274 if no_right_params < 0 then assert false
275 else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
276 let metasenv,exp_named_subst =
277 CicMkImplicit.fresh_subst metasenv context expl_params in
280 C.MutInd (uri,i,exp_named_subst)
282 C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
284 (* check consistency with the actual type of term *)
285 let actual_type,subst,metasenv =
286 type_of_aux subst metasenv context term in
287 let _, subst, metasenv =
288 type_of_aux subst metasenv context expected_type
290 let actual_type = CicMetaSubst.whd subst context actual_type in
292 Un.fo_unif_subst subst context metasenv expected_type actual_type
294 (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
295 let (_,outtypeinstances,subst,metasenv) =
297 (fun (j,outtypeinstances,subst,metasenv) p ->
299 if left_args = [] then
300 (C.MutConstruct (uri,i,j,exp_named_subst))
302 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
304 let actual_type,subst,metasenv =
305 type_of_aux subst metasenv context p in
306 let expected_type, subst, metasenv =
307 type_of_aux subst metasenv context constructor in
308 let outtypeinstance,subst,metasenv =
310 0 context metasenv subst
311 no_left_params actual_type constructor expected_type in
312 (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
313 (1,[],subst,metasenv) pl in
314 (* we are left to check that the outype matches his instances.
315 The easy case is when the outype is specified, that amount
316 to a trivial check. Otherwise, we should guess a type from
319 let _, subst, metasenv =
320 type_of_aux subst metasenv context
321 (C.Appl ((outtype :: right_args) @ [term]))
323 let (subst,metasenv) =
325 (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
329 CicSubstitution.lift constructor_args_no outtype
331 C.Appl (outtype'::args)
334 (* if appl is not well typed then the type_of below solves the
336 let (_, subst, metasenv) =
337 type_of_aux subst metasenv context appl
340 CicMetaSubst.whd subst context appl
342 Un.fo_unif_subst subst context metasenv instance instance')
343 (subst,metasenv) outtypeinstances in
344 CicMetaSubst.whd subst
345 context (C.Appl(outtype::right_args@[term])),subst,metasenv
347 let subst,metasenv,types =
349 (fun (subst,metasenv,types) (n,_,ty,_) ->
350 let _,subst',metasenv' = type_of_aux subst metasenv context ty in
351 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
352 ) (subst,metasenv,[]) fl
354 let len = List.length types in
355 let context' = types@context in
358 (fun (subst,metasenv) (name,x,ty,bo) ->
359 let ty_of_bo,subst,metasenv =
360 type_of_aux subst metasenv context' bo
362 Un.fo_unif_subst subst context' metasenv
363 ty_of_bo (CicMetaSubst.lift subst len ty)
364 ) (subst,metasenv) fl in
365 let (_,_,ty,_) = List.nth fl i in
368 let subst,metasenv,types =
370 (fun (subst,metasenv,types) (n,ty,_) ->
371 let _,subst',metasenv' = type_of_aux subst metasenv context ty in
372 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
373 ) (subst,metasenv,[]) fl
375 let len = List.length types in
376 let context' = types@context in
379 (fun (subst,metasenv) (name,ty,bo) ->
380 let ty_of_bo,subst,metasenv =
381 type_of_aux subst metasenv context' bo
383 Un.fo_unif_subst subst context' metasenv
384 ty_of_bo (CicMetaSubst.lift subst len ty)
385 ) (subst,metasenv) fl in
387 let (_,ty,_) = List.nth fl i in
390 (* check_metasenv_consistency checks that the "canonical" context of a
391 metavariable is consitent - up to relocation via the relocation list l -
392 with the actual context *)
393 and check_metasenv_consistency
394 metano subst metasenv context canonical_context l
396 let module C = Cic in
397 let module R = CicReduction in
398 let module S = CicSubstitution in
399 let lifted_canonical_context =
403 | (Some (n,C.Decl t))::tl ->
404 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
405 | (Some (n,C.Def (t,None)))::tl ->
406 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
407 | None::tl -> None::(aux (i+1) tl)
408 | (Some (n,C.Def (t,Some ty)))::tl ->
410 C.Def ((S.lift_meta l (S.lift i t)),
411 Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
413 aux 1 canonical_context
416 (fun (subst,metasenv) t ct ->
420 | Some t,Some (_,C.Def (ct,_)) ->
422 CicUnification.fo_unif_subst subst context metasenv t ct
423 with _ -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct))))
424 | Some t,Some (_,C.Decl ct) ->
425 let inferredty,subst',metasenv' =
426 type_of_aux subst metasenv context t
429 CicUnification.fo_unif_subst
430 subst' context metasenv' inferredty ct
431 with _ -> raise (NotRefinable (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" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct))))
433 raise (NotRefinable (sprintf
434 "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"
435 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
436 (CicMetaSubst.ppcontext subst canonical_context)))
437 ) (subst,metasenv) l lifted_canonical_context
439 and check_exp_named_subst metasubst metasenv context =
440 let rec check_exp_named_subst_aux metasubst metasenv substs =
442 [] -> metasubst,metasenv
443 | ((uri,t) as subst)::tl ->
445 CicSubstitution.subst_vars substs (type_of_variable uri) in
446 (match CicEnvironment.get_cooked_obj ~trust:false uri with
447 Cic.Variable (_,Some bo,_,_) ->
450 "A variable with a body can not be explicit substituted")
451 | Cic.Variable (_,None,_,_) -> ()
452 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
454 let typeoft,metasubst',metasenv' =
455 type_of_aux metasubst metasenv context t
458 let metasubst'',metasenv'' =
459 CicUnification.fo_unif_subst
460 metasubst' context metasenv' typeoft typeofvar
462 check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
464 raise (NotRefinable "Wrong Explicit Named Substitution")
466 check_exp_named_subst_aux metasubst metasenv []
468 and sort_of_prod subst metasenv context (name,s) (t1, t2) =
469 let module C = Cic in
470 let t1'' = CicMetaSubst.whd subst context t1 in
471 let t2'' = CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) t2 in
472 match (t1'', t2'') with
473 (C.Sort s1, C.Sort s2)
474 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
476 | (C.Sort s1, C.Sort s2) ->
477 (*CSC manca la gestione degli universi!!! *)
479 | (C.Meta _,_) | (_,C.Meta _) ->
480 (* TODO how can we force the meta to become a sort? If we don't we
481 * brake the invariant that refine produce only well typed terms *)
482 (* TODO if we check the non meta term and if it is a sort then we are
483 * likely to know the exact value of the result e.g. if the rhs is a
484 * Sort (Prop | Set | CProp) then the result is the rhs *)
488 raise (NotRefinable (sprintf
489 "Two types were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
490 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
491 (CicPp.ppterm t2'')))
493 and eat_prods subst metasenv context hetype tlbody_and_type =
494 let rec aux context' args (resty,subst,metasenv) =
496 [] -> resty,subst,metasenv
502 | Some t -> Some (CicMetaSubst.lift subst 1 t)
504 let argty' = CicMetaSubst.lift subst (List.length args) argty in
505 let context'' = Some (Cic.Anonymous, Cic.Decl argty') :: context' in
506 let (metasenv, idx) =
507 CicMkImplicit.mk_implicit metasenv (context'' @ context) in
509 (Some (Cic.Rel 1))::args' @
510 (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
513 let newmeta = Cic.Meta (idx, irl) in
514 let prod = Cic.Prod (Cic.Anonymous, argty, newmeta) in
515 let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
516 let (subst, metasenv) =
517 CicUnification.fo_unif_subst subst context metasenv resty prod
519 aux context'' (Some arg :: args)
520 (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
522 aux [] [] (hetype,subst,metasenv) tlbody_and_type
525 let ty,subst',metasenv' =
526 type_of_aux [] metasenv context t
528 (CicMetaSubst.apply_subst subst' t,
529 CicMetaSubst.apply_subst subst' ty,
530 CicMetaSubst.apply_subst_metasenv subst' metasenv')
534 let type_of_aux' metasenv context term =
536 let (t,ty,m) = type_of_aux' metasenv context term in
538 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
541 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
545 | CicUnification.AssertFailure msg as e ->
546 debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
549 | CicUnification.UnificationFailure msg as e ->
550 debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
554 debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;