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/.
26 exception Impossible of int;;
27 exception NotRefinable of string;;
28 exception WrongUriToConstant of string;;
29 exception WrongUriToVariable of string;;
30 exception WrongUriToMutualInductiveDefinitions of string;;
31 exception RelToHiddenHypothesis;;
32 exception MetasenvInconsistency;;
33 exception MutCaseFixAndCofixRefineNotImplemented;;
34 exception FreeMetaFound of int;;
38 let rec debug_aux t i =
40 let module U = UriManager in
41 CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
44 raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
45 (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
48 let rec type_of_constant uri =
50 let module R = CicReduction in
51 let module U = UriManager in
52 match CicEnvironment.get_cooked_obj uri with
53 C.Constant (_,_,ty,_) -> ty
54 | C.CurrentProof (_,_,_,ty,_) -> ty
55 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
57 and type_of_variable uri =
59 let module R = CicReduction in
60 let module U = UriManager in
61 match CicEnvironment.get_cooked_obj uri with
62 C.Variable (_,_,ty,_) -> ty
63 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
65 and type_of_mutual_inductive_defs uri i =
67 let module R = CicReduction in
68 let module U = UriManager in
69 match CicEnvironment.get_cooked_obj uri with
70 C.InductiveDefinition (dl,_,_) ->
71 let (_,_,arity,_) = List.nth dl i in
73 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
75 and type_of_mutual_inductive_constr uri i j =
77 let module R = CicReduction in
78 let module U = UriManager in
79 match CicEnvironment.get_cooked_obj uri with
80 C.InductiveDefinition (dl,_,_) ->
81 let (_,_,_,cl) = List.nth dl i in
82 let (_,ty) = List.nth cl (j-1) in
84 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
86 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
87 and type_of_aux' metasenv context t =
88 let rec type_of_aux subst metasenv context =
90 let module S = CicSubstitution in
91 let module U = UriManager in
92 let module Un = CicUnification in
96 match List.nth context (n - 1) with
97 Some (_,C.Decl t) -> S.lift n t,subst,metasenv
98 | Some (_,C.Def bo) ->
99 type_of_aux subst metasenv context (S.lift n bo)
100 | None -> raise RelToHiddenHypothesis
102 _ -> raise (NotRefinable "Not a close term")
104 | C.Var (uri,exp_named_subst) ->
106 let subst',metasenv' =
107 check_exp_named_subst subst metasenv context exp_named_subst in
109 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
114 let (_,canonical_context,ty) =
116 List.find (function (m,_,_) -> n = m) metasenv
118 Not_found -> raise (FreeMetaFound n)
120 let subst',metasenv' =
121 check_metasenv_consistency subst metasenv context canonical_context l
123 CicSubstitution.lift_meta l ty, subst', metasenv'
125 C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
127 | C.Implicit -> raise (Impossible 21)
129 let _,subst',metasenv' =
130 type_of_aux subst metasenv context ty in
131 let inferredty,subst'',metasenv'' =
132 type_of_aux subst' metasenv' context ty
135 let subst''',metasenv''' =
136 Un.fo_unif_subst subst'' context metasenv'' inferredty ty
138 ty,subst''',metasenv'''
140 _ -> raise (NotRefinable "Cast"))
141 | C.Prod (name,s,t) ->
142 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
143 let sort2,subst'',metasenv'' =
144 type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
146 sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
147 | C.Lambda (n,s,t) ->
148 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
149 let type2,subst'',metasenv'' =
150 type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
152 let sort2,subst''',metasenv''' =
153 type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
155 (* only to check if the product is well-typed *)
156 let _,subst'''',metasenv'''' =
157 sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
159 C.Prod (n,s,type2),subst'''',metasenv''''
161 (* only to check if s is well-typed *)
162 let _,subst',metasenv' = type_of_aux subst metasenv context s in
163 let inferredty,subst'',metasenv'' =
164 type_of_aux subst' metasenv' ((Some (n,(C.Def s)))::context) t
166 (* One-step LetIn reduction. Even faster than the previous solution.
167 Moreover the inferred type is closer to the expected one. *)
168 CicSubstitution.subst s inferredty,subst',metasenv'
169 | C.Appl (he::tl) when List.length tl > 0 ->
170 let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
171 let tlbody_and_type,subst'',metasenv'' =
173 (fun x (res,subst,metasenv) ->
174 let ty,subst',metasenv' =
175 type_of_aux subst metasenv context x
177 (x, ty)::res,subst',metasenv'
178 ) tl ([],subst',metasenv')
180 eat_prods subst'' metasenv'' context hetype tlbody_and_type
181 | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
182 | C.Const (uri,exp_named_subst) ->
184 let subst',metasenv' =
185 check_exp_named_subst subst metasenv context exp_named_subst in
187 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
191 | C.MutInd (uri,i,exp_named_subst) ->
193 let subst',metasenv' =
194 check_exp_named_subst subst metasenv context exp_named_subst in
196 CicSubstitution.subst_vars exp_named_subst
197 (type_of_mutual_inductive_defs uri i)
201 | C.MutConstruct (uri,i,j,exp_named_subst) ->
202 let subst',metasenv' =
203 check_exp_named_subst subst metasenv context exp_named_subst in
205 CicSubstitution.subst_vars exp_named_subst
206 (type_of_mutual_inductive_constr uri i j)
211 | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
213 (* check_metasenv_consistency checks that the "canonical" context of a
214 metavariable is consitent - up to relocation via the relocation list l -
215 with the actual context *)
216 and check_metasenv_consistency subst metasenv context canonical_context l =
217 let module C = Cic in
218 let module R = CicReduction in
219 let module S = CicSubstitution in
220 let lifted_canonical_context =
224 | (Some (n,C.Decl t))::tl ->
225 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
226 | (Some (n,C.Def t))::tl ->
227 (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
228 | None::tl -> None::(aux (i+1) tl)
230 aux 1 canonical_context
233 (fun (subst,metasenv) t ct ->
235 _,None -> subst,metasenv
236 | Some t,Some (_,C.Def ct) ->
238 CicUnification.fo_unif_subst subst context metasenv t ct
239 with _ -> raise MetasenvInconsistency)
240 | Some t,Some (_,C.Decl ct) ->
241 let inferredty,subst',metasenv' =
242 type_of_aux subst metasenv context t
245 CicUnification.fo_unif_subst subst context metasenv inferredty ct
246 with _ -> raise MetasenvInconsistency)
247 | _, _ -> raise MetasenvInconsistency
248 ) (subst,metasenv) l lifted_canonical_context
250 and check_exp_named_subst metasubst metasenv context =
251 let rec check_exp_named_subst_aux metasubst metasenv substs =
253 [] -> metasubst,metasenv
254 | ((uri,t) as subst)::tl ->
256 CicSubstitution.subst_vars substs (type_of_variable uri) in
257 (match CicEnvironment.get_cooked_obj ~trust:false uri with
258 Cic.Variable (_,Some bo,_,_) ->
261 "A variable with a body can not be explicit substituted")
262 | Cic.Variable (_,None,_,_) -> ()
263 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
265 let typeoft,metasubst',metasenv' =
266 type_of_aux metasubst metasenv context t
269 let metasubst'',metasenv'' =
270 CicUnification.fo_unif_subst
271 metasubst' context metasenv' typeoft typeofvar
273 check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
275 raise (NotRefinable "Wrong Explicit Named Substitution")
277 check_exp_named_subst_aux metasubst metasenv []
279 and sort_of_prod subst metasenv context (name,s) (t1, t2) =
280 let module C = Cic in
281 (* ti could be a metavariable in the domain of the substitution *)
282 let subst',metasenv' = CicUnification.unwind_subst metasenv subst in
283 let t1' = CicUnification.apply_subst subst' t1 in
284 let t2' = CicUnification.apply_subst subst' t2 in
285 let t1'' = CicReduction.whd context t1' in
286 let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' in
287 match (t1'', t2'') with
288 (C.Sort s1, C.Sort s2)
289 when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
290 C.Sort s2,subst',metasenv'
291 | (C.Sort s1, C.Sort s2) ->
292 (*CSC manca la gestione degli universi!!! *)
293 C.Sort C.Type,subst',metasenv'
297 ("Prod: sort1= "^ CicPp.ppterm t1'' ^ " ; sort2= "^ CicPp.ppterm t2''))
299 and eat_prods subst metasenv context hetype =
301 [] -> hetype,subst,metasenv
302 | (hete, hety)::tl ->
303 (match (CicReduction.whd context hetype) with
305 let subst',metasenv' =
307 CicUnification.fo_unif_subst subst context metasenv s hety
309 raise (NotRefinable "Appl: wrong parameter-type")
311 CicReduction.fdebug := -1 ;
312 eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
313 | _ -> raise (NotRefinable "Appl: wrong Prod-type")
316 let ty,subst',metasenv' =
317 type_of_aux [] metasenv context t
319 let subst'',metasenv'' = CicUnification.unwind_subst metasenv' subst' in
320 (* we get rid of the metavariables that have been instantiated *)
323 (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst''))
326 CicUnification.apply_subst subst'' t,
327 CicUnification.apply_subst subst'' ty,
332 let type_of_aux' metasenv context term =
335 type_of_aux' metasenv context term
339 prerr_endline ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
342 prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
344 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
350 prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
352 prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;