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 Uncertain of string;;
29 exception WrongUriToConstant of string;;
30 exception WrongUriToVariable of string;;
31 exception WrongUriToMutualInductiveDefinitions of string;;
32 exception RelToHiddenHypothesis;;
33 exception MetasenvInconsistency;;
34 exception MutCaseFixAndCofixRefineNotImplemented;;
35 exception FreeMetaFound of int;;
39 let rec debug_aux t i =
41 let module U = UriManager in
42 CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
45 raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
46 (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
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
56 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
58 and type_of_variable uri =
60 let module R = CicReduction in
61 let module U = UriManager in
62 match CicEnvironment.get_cooked_obj uri with
63 C.Variable (_,_,ty,_) -> ty
64 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
66 and type_of_mutual_inductive_defs uri i =
68 let module R = CicReduction in
69 let module U = UriManager in
70 match CicEnvironment.get_cooked_obj uri with
71 C.InductiveDefinition (dl,_,_) ->
72 let (_,_,arity,_) = List.nth dl i in
74 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
76 and type_of_mutual_inductive_constr uri i j =
78 let module R = CicReduction in
79 let module U = UriManager in
80 match CicEnvironment.get_cooked_obj uri with
81 C.InductiveDefinition (dl,_,_) ->
82 let (_,_,_,cl) = List.nth dl i in
83 let (_,ty) = List.nth cl (j-1) in
85 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
87 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
88 and type_of_aux' metasenv context t =
89 let rec type_of_aux subst metasenv context =
91 let module S = CicSubstitution in
92 let module U = UriManager in
93 let module Un = CicUnification in
97 match List.nth context (n - 1) with
98 Some (_,C.Decl t) -> S.lift n t,subst,metasenv
99 | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
100 | Some (_,C.Def (bo,None)) ->
101 prerr_endline "##### DA INVESTIGARE E CAPIRE" ;
102 type_of_aux subst metasenv context (S.lift n bo)
103 | None -> raise RelToHiddenHypothesis
105 _ -> raise (NotRefinable "Not a close term")
107 | C.Var (uri,exp_named_subst) ->
109 let subst',metasenv' =
110 check_exp_named_subst subst metasenv context exp_named_subst in
112 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
117 let (_,canonical_context,ty) =
119 List.find (function (m,_,_) -> n = m) metasenv
121 Not_found -> raise (FreeMetaFound n)
123 let subst',metasenv' =
124 check_metasenv_consistency subst metasenv context canonical_context l
126 CicSubstitution.lift_meta l ty, subst', metasenv'
128 C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
130 | C.Implicit -> raise (Impossible 21)
132 let _,subst',metasenv' =
133 type_of_aux subst metasenv context ty in
134 let inferredty,subst'',metasenv'' =
135 type_of_aux subst' metasenv' context ty
138 let subst''',metasenv''' =
139 Un.fo_unif_subst subst'' context metasenv'' inferredty ty
141 ty,subst''',metasenv'''
143 _ -> raise (NotRefinable "Cast"))
144 | C.Prod (name,s,t) ->
145 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
146 let sort2,subst'',metasenv'' =
147 type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
149 sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
150 | C.Lambda (n,s,t) ->
151 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
152 let type2,subst'',metasenv'' =
153 type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
155 let sort2,subst''',metasenv''' =
156 type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
158 (* only to check if the product is well-typed *)
159 let _,subst'''',metasenv'''' =
160 sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
162 C.Prod (n,s,type2),subst'''',metasenv''''
164 (* only to check if s is well-typed *)
165 let ty,subst',metasenv' = type_of_aux subst metasenv context s in
166 let inferredty,subst'',metasenv'' =
167 type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
169 (* One-step LetIn reduction. Even faster than the previous solution.
170 Moreover the inferred type is closer to the expected one. *)
171 CicSubstitution.subst s inferredty,subst',metasenv'
172 | C.Appl (he::tl) when List.length tl > 0 ->
173 let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
174 let tlbody_and_type,subst'',metasenv'' =
176 (fun x (res,subst,metasenv) ->
177 let ty,subst',metasenv' =
178 type_of_aux subst metasenv context x
180 (x, ty)::res,subst',metasenv'
181 ) tl ([],subst',metasenv')
183 eat_prods subst'' metasenv'' context hetype tlbody_and_type
184 | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
185 | C.Const (uri,exp_named_subst) ->
187 let subst',metasenv' =
188 check_exp_named_subst subst metasenv context exp_named_subst in
190 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
194 | C.MutInd (uri,i,exp_named_subst) ->
196 let subst',metasenv' =
197 check_exp_named_subst subst metasenv context exp_named_subst in
199 CicSubstitution.subst_vars exp_named_subst
200 (type_of_mutual_inductive_defs uri i)
204 | C.MutConstruct (uri,i,j,exp_named_subst) ->
205 let subst',metasenv' =
206 check_exp_named_subst subst metasenv context exp_named_subst in
208 CicSubstitution.subst_vars exp_named_subst
209 (type_of_mutual_inductive_constr uri i j)
214 | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
216 (* check_metasenv_consistency checks that the "canonical" context of a
217 metavariable is consitent - up to relocation via the relocation list l -
218 with the actual context *)
219 and check_metasenv_consistency subst metasenv context canonical_context l =
220 let module C = Cic in
221 let module R = CicReduction in
222 let module S = CicSubstitution in
223 let lifted_canonical_context =
227 | (Some (n,C.Decl t))::tl ->
228 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
229 | (Some (n,C.Def (t,None)))::tl ->
230 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
231 | None::tl -> None::(aux (i+1) tl)
232 | (Some (_,C.Def (_,Some _)))::_ -> assert false
234 aux 1 canonical_context
237 (fun (subst,metasenv) t ct ->
239 _,None -> subst,metasenv
240 | Some t,Some (_,C.Def (ct,_)) ->
242 CicUnification.fo_unif_subst subst context metasenv t ct
243 with _ -> raise MetasenvInconsistency)
244 | Some t,Some (_,C.Decl ct) ->
245 let inferredty,subst',metasenv' =
246 type_of_aux subst metasenv context t
249 CicUnification.fo_unif_subst subst context metasenv inferredty ct
250 with _ -> raise MetasenvInconsistency)
251 | _, _ -> raise MetasenvInconsistency
252 ) (subst,metasenv) l lifted_canonical_context
254 and check_exp_named_subst metasubst metasenv context =
255 let rec check_exp_named_subst_aux metasubst metasenv substs =
257 [] -> metasubst,metasenv
258 | ((uri,t) as subst)::tl ->
260 CicSubstitution.subst_vars substs (type_of_variable uri) in
261 (match CicEnvironment.get_cooked_obj ~trust:false uri with
262 Cic.Variable (_,Some bo,_,_) ->
265 "A variable with a body can not be explicit substituted")
266 | Cic.Variable (_,None,_,_) -> ()
267 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
269 let typeoft,metasubst',metasenv' =
270 type_of_aux metasubst metasenv context t
273 let metasubst'',metasenv'' =
274 CicUnification.fo_unif_subst
275 metasubst' context metasenv' typeoft typeofvar
277 check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
279 raise (NotRefinable "Wrong Explicit Named Substitution")
281 check_exp_named_subst_aux metasubst metasenv []
283 and sort_of_prod subst metasenv context (name,s) (t1, t2) =
284 let module C = Cic in
285 (* ti could be a metavariable in the domain of the substitution *)
286 let subst',metasenv' = CicUnification.unwind_subst metasenv subst in
287 let t1' = CicUnification.apply_subst subst' t1 in
288 let t2' = CicUnification.apply_subst subst' t2 in
289 let t1'' = CicReduction.whd context t1' in
290 let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' in
291 match (t1'', t2'') with
292 (C.Sort s1, C.Sort s2)
293 when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
294 C.Sort s2,subst',metasenv'
295 | (C.Sort s1, C.Sort s2) ->
296 (*CSC manca la gestione degli universi!!! *)
297 C.Sort C.Type,subst',metasenv'
302 ("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^
307 ("Prod: sort1= "^ CicPp.ppterm t1'' ^ " ; sort2= "^ CicPp.ppterm t2''))
309 and eat_prods subst metasenv context hetype =
311 [] -> hetype,subst,metasenv
312 | (hete, hety)::tl ->
313 (match (CicReduction.whd context hetype) with
315 let subst',metasenv' =
317 CicUnification.fo_unif_subst subst context metasenv s hety
319 raise (NotRefinable "Appl: wrong parameter-type")
321 CicReduction.fdebug := -1 ;
322 eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
326 ("Prod expected, " ^ CicPp.ppterm t ^ " found"))
327 | _ -> raise (NotRefinable "Appl: wrong Prod-type")
330 let ty,subst',metasenv' =
331 type_of_aux [] metasenv context t
333 let subst'',metasenv'' = CicUnification.unwind_subst metasenv' subst' in
334 (* we get rid of the metavariables that have been instantiated *)
337 (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst''))
340 CicUnification.apply_subst subst'' t,
341 CicUnification.apply_subst subst'' ty,
346 let type_of_aux' metasenv context term =
349 type_of_aux' metasenv context term
353 prerr_endline ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
356 prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
358 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
364 prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
366 prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;