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 Impossible of int;;
29 exception NotRefinable of string;;
30 exception Uncertain of string;;
31 exception WrongUriToConstant of string;;
32 exception WrongUriToVariable of string;;
33 exception ListTooShort;;
34 exception WrongUriToMutualInductiveDefinitions of string;;
35 exception RelToHiddenHypothesis;;
36 exception MetasenvInconsistency;;
37 exception WrongArgumentNumber;;
41 let rec debug_aux t i =
43 let module U = UriManager in
44 CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
47 raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
48 (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
51 let debug_print = prerr_endline
56 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
57 | (_,_) -> raise ListTooShort
60 let rec type_of_constant uri =
62 let module R = CicReduction in
63 let module U = UriManager in
64 match CicEnvironment.get_cooked_obj uri with
65 C.Constant (_,_,ty,_) -> ty
66 | C.CurrentProof (_,_,_,ty,_) -> ty
67 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
69 and type_of_variable uri =
71 let module R = CicReduction in
72 let module U = UriManager in
73 match CicEnvironment.get_cooked_obj uri with
74 C.Variable (_,_,ty,_) -> ty
75 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
77 and type_of_mutual_inductive_defs uri i =
79 let module R = CicReduction in
80 let module U = UriManager in
81 match CicEnvironment.get_cooked_obj uri with
82 C.InductiveDefinition (dl,_,_) ->
83 let (_,_,arity,_) = List.nth dl i in
85 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
87 and type_of_mutual_inductive_constr uri i j =
89 let module R = CicReduction in
90 let module U = UriManager in
91 match CicEnvironment.get_cooked_obj uri with
92 C.InductiveDefinition (dl,_,_) ->
93 let (_,_,_,cl) = List.nth dl i in
94 let (_,ty) = List.nth cl (j-1) in
96 | _ -> raise (WrongUriToMutualInductiveDefinitions (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 let module Un = CicUnification in
112 match R.whd subst context expectedtype with
114 (n,context,actualtype, [term]), subst, metasenv
115 | C.Appl (C.MutInd (_,_,_)::tl) ->
116 let (_,arguments) = split tl left_args_no in
117 (n,context,actualtype, arguments@[term]), subst, metasenv
118 | C.Prod (name,so,de) ->
119 (* we expect that the actual type of the branch has the due
121 (match R.whd subst context actualtype with
122 C.Prod (name',so',de') ->
123 let subst, metasenv =
124 Un.fo_unif_subst subst context metasenv so so' in
126 (match CicSubstitution.lift 1 term with
127 C.Appl l -> C.Appl (l@[C.Rel 1])
128 | t -> C.Appl [t ; C.Rel 1]) in
129 (* we should also check that the name variable is anonymous in
130 the actual type de' ?? *)
131 check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de
132 | _ -> raise WrongArgumentNumber)
133 | _ -> raise (NotRefinable "Prod or MutInd expected")
135 and type_of_aux' metasenv context t =
136 let rec type_of_aux subst metasenv context =
137 let module C = Cic in
138 let module S = CicSubstitution in
139 let module U = UriManager in
140 let module Un = CicUnification in
144 match List.nth context (n - 1) with
145 Some (_,C.Decl t) -> S.lift n t,subst,metasenv
146 | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
147 | Some (_,C.Def (bo,None)) ->
148 type_of_aux subst metasenv context (S.lift n bo)
149 | None -> raise RelToHiddenHypothesis
151 _ -> raise (NotRefinable "Not a close term")
153 | C.Var (uri,exp_named_subst) ->
155 let subst',metasenv' =
156 check_exp_named_subst subst metasenv context exp_named_subst in
158 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
163 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
164 let subst',metasenv' =
165 check_metasenv_consistency subst metasenv context canonical_context l
167 CicSubstitution.lift_meta l ty, subst', metasenv'
169 C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
171 | C.Implicit -> raise (Impossible 21)
173 let _,subst',metasenv' =
174 type_of_aux subst metasenv context ty in
175 let inferredty,subst'',metasenv'' =
176 type_of_aux subst' metasenv' context te
179 let subst''',metasenv''' =
180 Un.fo_unif_subst subst'' context metasenv'' inferredty ty
182 ty,subst''',metasenv'''
184 _ -> raise (NotRefinable "Cast"))
185 | C.Prod (name,s,t) ->
186 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
187 let sort2,subst'',metasenv'' =
188 type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
190 sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
191 | C.Lambda (n,s,t) ->
192 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
193 let type2,subst'',metasenv'' =
194 type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
196 let sort2,subst''',metasenv''' =
197 type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
199 (* only to check if the product is well-typed *)
200 let _,subst'''',metasenv'''' =
201 sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
203 C.Prod (n,s,type2),subst'''',metasenv''''
205 (* only to check if s is well-typed *)
206 let ty,subst',metasenv' = type_of_aux subst metasenv context s in
207 let inferredty,subst'',metasenv'' =
208 type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
210 (* One-step LetIn reduction. Even faster than the previous solution.
211 Moreover the inferred type is closer to the expected one. *)
212 CicSubstitution.subst s inferredty,subst',metasenv'
213 | C.Appl (he::tl) when List.length tl > 0 ->
214 let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
215 let tlbody_and_type,subst'',metasenv'' =
217 (fun x (res,subst,metasenv) ->
218 let ty,subst',metasenv' =
219 type_of_aux subst metasenv context x
221 (x, ty)::res,subst',metasenv'
222 ) tl ([],subst',metasenv')
224 eat_prods subst'' metasenv'' context hetype tlbody_and_type
225 | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
226 | C.Const (uri,exp_named_subst) ->
228 let subst',metasenv' =
229 check_exp_named_subst subst metasenv context exp_named_subst in
231 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
235 | C.MutInd (uri,i,exp_named_subst) ->
237 let subst',metasenv' =
238 check_exp_named_subst subst metasenv context exp_named_subst in
240 CicSubstitution.subst_vars exp_named_subst
241 (type_of_mutual_inductive_defs uri i)
245 | C.MutConstruct (uri,i,j,exp_named_subst) ->
246 let subst',metasenv' =
247 check_exp_named_subst subst metasenv context exp_named_subst in
249 CicSubstitution.subst_vars exp_named_subst
250 (type_of_mutual_inductive_constr uri i j)
253 | C.MutCase (uri, i, outtype, term, pl) ->
254 (* first, get the inductive type (and noparams) in the environment *)
255 let (_,b,arity,constructors), expl_params, no_left_params =
256 match CicEnvironment.get_cooked_obj ~trust:true uri with
257 C.InductiveDefinition (l,expl_params,parsno) ->
258 List.nth l i , expl_params, parsno
261 (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
262 let rec count_prod t =
263 match CicMetaSubst.whd subst context t with
264 C.Prod (_, _, t) -> 1 + (count_prod t)
266 let no_args = count_prod arity in
267 (* now, create a "generic" MutInd *)
268 let metasenv,left_args =
269 CicMkImplicit.n_fresh_metas metasenv context no_left_params in
270 let metasenv,right_args =
271 let no_right_params = no_args - no_left_params in
272 if no_right_params < 0 then assert false
273 else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
274 let metasenv,exp_named_subst =
275 CicMkImplicit.fresh_subst metasenv context expl_params in
278 C.MutInd (uri,i,exp_named_subst)
280 C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
282 (* check consistency with the actual type of term *)
283 let actual_type,subst,metasenv =
284 type_of_aux subst metasenv context term in
285 let _, subst, metasenv =
286 type_of_aux subst metasenv context expected_type
288 let actual_type = CicMetaSubst.whd subst context actual_type in
290 Un.fo_unif_subst subst context metasenv expected_type actual_type
292 (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
293 let (_,outtypeinstances,subst,metasenv) =
295 (fun (j,outtypeinstances,subst,metasenv) p ->
297 if left_args = [] then
298 (C.MutConstruct (uri,i,j,exp_named_subst))
300 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
302 let actual_type,subst,metasenv =
303 type_of_aux subst metasenv context p in
304 let expected_type, subst, metasenv =
305 type_of_aux subst metasenv context constructor in
306 let outtypeinstance,subst,metasenv =
308 0 context metasenv subst
309 no_left_params actual_type constructor expected_type in
310 (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
311 (1,[],subst,metasenv) pl in
312 (* we are left to check that the outype matches his instances.
313 The easy case is when the outype is specified, that amount
314 to a trivial check. Otherwise, we should guess a type from
317 let _, subst, metasenv =
318 type_of_aux subst metasenv context
319 (C.Appl ((outtype :: right_args) @ [term]))
321 let (subst,metasenv) =
323 (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
327 CicSubstitution.lift constructor_args_no outtype
329 C.Appl (outtype'::args)
332 (* if appl is not well typed then the type_of below solves the
334 let (_, subst, metasenv) =
335 type_of_aux subst metasenv context appl
338 CicMetaSubst.whd subst context appl
340 Un.fo_unif_subst subst context metasenv instance instance')
341 (subst,metasenv) outtypeinstances in
342 CicMetaSubst.whd subst
343 context (C.Appl(outtype::right_args@[term])),subst,metasenv
345 let subst,metasenv,types =
347 (fun (subst,metasenv,types) (n,_,ty,_) ->
348 let _,subst',metasenv' = type_of_aux subst metasenv context ty in
349 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
350 ) (subst,metasenv,[]) fl
352 let len = List.length types in
353 let context' = types@context in
356 (fun (subst,metasenv) (name,x,ty,bo) ->
357 let ty_of_bo,subst,metasenv =
358 type_of_aux subst metasenv context' bo
360 Un.fo_unif_subst subst context' metasenv
361 ty_of_bo (CicMetaSubst.lift subst len ty)
362 ) (subst,metasenv) fl in
363 let (_,_,ty,_) = List.nth fl i in
366 let subst,metasenv,types =
368 (fun (subst,metasenv,types) (n,ty,_) ->
369 let _,subst',metasenv' = type_of_aux subst metasenv context ty in
370 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
371 ) (subst,metasenv,[]) fl
373 let len = List.length types in
374 let context' = types@context in
377 (fun (subst,metasenv) (name,ty,bo) ->
378 let ty_of_bo,subst,metasenv =
379 type_of_aux subst metasenv context' bo
381 Un.fo_unif_subst subst context' metasenv
382 ty_of_bo (CicMetaSubst.lift subst len ty)
383 ) (subst,metasenv) fl in
385 let (_,ty,_) = List.nth fl i in
388 (* check_metasenv_consistency checks that the "canonical" context of a
389 metavariable is consitent - up to relocation via the relocation list l -
390 with the actual context *)
391 and check_metasenv_consistency subst metasenv context canonical_context l =
392 let module C = Cic in
393 let module R = CicReduction in
394 let module S = CicSubstitution in
395 let lifted_canonical_context =
399 | (Some (n,C.Decl t))::tl ->
400 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
401 | (Some (n,C.Def (t,None)))::tl ->
402 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
403 | None::tl -> None::(aux (i+1) tl)
404 | (Some (n,C.Def (t,Some ty)))::tl ->
406 C.Def ((S.lift_meta l (S.lift i t)),
407 Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
409 aux 1 canonical_context
412 (fun (subst,metasenv) t ct ->
416 | Some t,Some (_,C.Def (ct,_)) ->
418 CicUnification.fo_unif_subst subst context metasenv t ct
419 with _ -> raise MetasenvInconsistency)
420 | Some t,Some (_,C.Decl ct) ->
421 let inferredty,subst',metasenv' =
422 type_of_aux subst metasenv context t
425 CicUnification.fo_unif_subst
426 subst' context metasenv' inferredty ct
427 with _ -> raise MetasenvInconsistency)
429 raise MetasenvInconsistency
430 ) (subst,metasenv) l lifted_canonical_context
432 and check_exp_named_subst metasubst metasenv context =
433 let rec check_exp_named_subst_aux metasubst metasenv substs =
435 [] -> metasubst,metasenv
436 | ((uri,t) as subst)::tl ->
438 CicSubstitution.subst_vars substs (type_of_variable uri) in
439 (match CicEnvironment.get_cooked_obj ~trust:false uri with
440 Cic.Variable (_,Some bo,_,_) ->
443 "A variable with a body can not be explicit substituted")
444 | Cic.Variable (_,None,_,_) -> ()
445 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
447 let typeoft,metasubst',metasenv' =
448 type_of_aux metasubst metasenv context t
451 let metasubst'',metasenv'' =
452 CicUnification.fo_unif_subst
453 metasubst' context metasenv' typeoft typeofvar
455 check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
457 raise (NotRefinable "Wrong Explicit Named Substitution")
459 check_exp_named_subst_aux metasubst metasenv []
461 and sort_of_prod subst metasenv context (name,s) (t1, t2) =
462 let module C = Cic in
463 (* ti could be a metavariable in the domain of the substitution *)
464 let t1' = CicMetaSubst.apply_subst subst t1 in
465 let t2' = CicMetaSubst.apply_subst subst t2 in
466 let t1'' = CicMetaSubst.whd subst context t1' in
468 CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) t2'
470 match (t1'', t2'') with
471 (C.Sort s1, C.Sort s2)
472 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
473 C.Sort s2,subst,metasenv
474 | (C.Sort s1, C.Sort s2) ->
475 (*CSC manca la gestione degli universi!!! *)
476 C.Sort C.Type,subst,metasenv
477 | (C.Meta _,_) | (_,C.Meta _) ->
478 (* TODO how can we force the meta to become a sort? If we don't we
479 * brake the invariant that refine produce only well typed terms *)
480 (* TODO if we check the non meta term and if it is a sort then we are
481 * likely to know the exact value of the result e.g. if the rhs is a
482 * Sort (Prop | Set | CProp) then the result is the rhs *)
483 let (metasenv, idx) = CicMkImplicit.mk_implicit metasenv context in
485 CicMkImplicit.identity_relocation_list_for_metavariable context
487 C.Meta (idx, irl), subst, metasenv
489 raise (NotRefinable (sprintf
490 "Two types were expected, found %s of type %s and %s of type %s"
491 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
492 (CicPp.ppterm t2'')))
494 and eat_prods subst metasenv context hetype tlbody_and_type =
495 (* TODO to be reviewed *)
497 (fun (resty, subst, metasenv) (arg, argty) ->
498 let context' = Some (Cic.Anonymous, Cic.Decl argty) :: context in
499 let (metasenv, idx) = CicMkImplicit.mk_implicit metasenv context' in
501 CicMkImplicit.identity_relocation_list_for_metavariable context'
503 let newmeta = Cic.Meta (idx, irl) in
504 let prod = Cic.Prod (Cic.Anonymous, argty, newmeta) in
505 let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
506 let (subst, metasenv) =
507 CicUnification.fo_unif_subst subst context metasenv resty prod
509 (CicMetaSubst.subst subst arg newmeta, subst, metasenv))
510 (hetype, subst, metasenv) tlbody_and_type
513 let ty,subst',metasenv' =
514 type_of_aux [] metasenv context t
516 (* we get rid of the metavariables that have been instantiated *)
519 (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst'))
522 CicMetaSubst.apply_subst subst' t,
523 CicMetaSubst.apply_subst subst' ty,
528 let type_of_aux' metasenv context term =
530 let (t,ty,s,m) = type_of_aux' metasenv context term in
532 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
535 ("@@@ REFINE SUCCESSFUL (subst):\n" ^ CicMetaSubst.ppsubst s);
537 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
541 | CicUnification.AssertFailure msg as e ->
542 debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
545 | CicUnification.UnificationFailure msg as e ->
546 debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
550 debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;