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 NotWellTyped of string;;
28 exception WrongUriToConstant of string;;
29 exception WrongUriToVariable of string;;
30 exception WrongUriToMutualInductiveDefinitions of string;;
31 exception ListTooShort;;
32 exception RelToHiddenHypothesis;;
34 type types = {synthesized : Cic.term ; expected : Cic.term};;
39 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
40 | (_,_) -> raise ListTooShort
43 let cooked_type_of_constant uri cookingsno =
45 let module R = CicReduction in
46 let module U = UriManager in
48 match CicEnvironment.is_type_checked uri cookingsno with
49 CicEnvironment.CheckedObj cobj -> cobj
50 | CicEnvironment.UncheckedObj uobj ->
51 raise (NotWellTyped "Reference to an unchecked constant")
54 C.Definition (_,_,ty,_) -> ty
55 | C.Axiom (_,ty,_) -> ty
56 | C.CurrentProof (_,_,_,ty) -> ty
57 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
60 let type_of_variable uri =
62 let module R = CicReduction in
63 let module U = UriManager in
64 (* 0 because a variable is never cooked => no partial cooking at one level *)
65 match CicEnvironment.is_type_checked uri 0 with
66 CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty
67 | CicEnvironment.UncheckedObj (C.Variable _) ->
68 raise (NotWellTyped "Reference to an unchecked variable")
69 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
72 let cooked_type_of_mutual_inductive_defs uri cookingsno i =
74 let module R = CicReduction in
75 let module U = UriManager in
77 match CicEnvironment.is_type_checked uri cookingsno with
78 CicEnvironment.CheckedObj cobj -> cobj
79 | CicEnvironment.UncheckedObj uobj ->
80 raise (NotWellTyped "Reference to an unchecked inductive type")
83 C.InductiveDefinition (dl,_,_) ->
84 let (_,_,arity,_) = List.nth dl i in
86 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
89 let cooked_type_of_mutual_inductive_constr uri cookingsno i j =
91 let module R = CicReduction in
92 let module U = UriManager in
94 match CicEnvironment.is_type_checked uri cookingsno with
95 CicEnvironment.CheckedObj cobj -> cobj
96 | CicEnvironment.UncheckedObj uobj ->
97 raise (NotWellTyped "Reference to an unchecked constructor")
100 C.InductiveDefinition (dl,_,_) ->
101 let (_,_,_,cl) = List.nth dl i in
102 let (_,ty,_) = List.nth cl (j-1) in
104 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
112 let hash = Hashtbl.hash
116 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
117 let rec type_of_aux' subterms_to_types metasenv context t =
118 (* Coscoy's double type-inference algorithm *)
119 (* It computes the inner-types of every subterm of [t], *)
120 (* even when they are not needed to compute the types *)
121 (* of other terms. *)
122 let rec type_of_aux context t =
123 let module C = Cic in
124 let module R = CicReduction in
125 let module S = CicSubstitution in
126 let module U = UriManager in
131 match List.nth context (n - 1) with
132 Some (_,C.Decl t) -> S.lift n t
133 | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
134 | None -> raise RelToHiddenHypothesis
136 _ -> raise (NotWellTyped "Not a close term")
138 | C.Var uri -> type_of_variable uri
140 (* Let's visit all the subterms that will not be visited later *)
143 (function None -> () | Some t -> ignore (type_of_aux context t)) l
145 let (_,canonical_context,ty) =
146 List.find (function (m,_,_) -> n = m) metasenv
148 (* Checks suppressed *)
149 CicSubstitution.lift_meta l ty
150 | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
151 | C.Implicit -> raise (Impossible 21)
153 (* Let's visit all the subterms that will not be visited later *)
154 let _ = type_of_aux context te in
155 let _ = type_of_aux context ty in
156 (* Checks suppressed *)
158 | C.Prod (name,s,t) ->
159 let sort1 = type_of_aux context s
160 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
161 sort_of_prod context (name,s) (sort1,sort2)
162 | C.Lambda (n,s,t) ->
163 (* Let's visit all the subterms that will not be visited later *)
164 let _ = type_of_aux context s in
165 let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
166 (* Checks suppressed *)
169 (* Let's visit all the subterms that will not be visited later *)
170 let _ = type_of_aux context s in
171 (* Checks suppressed *)
172 C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)
173 | C.Appl (he::tl) when List.length tl > 0 ->
174 let hetype = type_of_aux context he
175 and tlbody_and_type =
176 List.map (fun x -> (x, type_of_aux context x)) tl
178 eat_prods context hetype tlbody_and_type
179 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
180 | C.Const (uri,cookingsno) ->
181 cooked_type_of_constant uri cookingsno
182 | C.Abst _ -> raise (Impossible 22)
183 | C.MutInd (uri,cookingsno,i) ->
184 cooked_type_of_mutual_inductive_defs uri cookingsno i
185 | C.MutConstruct (uri,cookingsno,i,j) ->
186 let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j in
188 | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
189 (* Let's visit all the subterms that will not be visited later *)
190 let _ = List.map (type_of_aux context) pl in
191 let outsort = type_of_aux context outtype in
192 let (need_dummy, k) =
193 let rec guess_args context t =
194 match CicReduction.whd context t with
195 C.Sort _ -> (true, 0)
196 | C.Prod (name, s, t) ->
197 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
199 (* last prod before sort *)
200 match CicReduction.whd context s with
201 (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
202 C.MutInd (uri',_,i') when U.eq uri' uri && i' = i ->
204 | C.Appl ((C.MutInd (uri',_,i')) :: _)
205 when U.eq uri' uri && i' = i -> (false, 1)
209 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
211 (*CSC whd non serve dopo type_of_aux ? *)
212 let (b, k) = guess_args context outsort in
213 if not b then (b, k - 1) else (b, k)
216 match R.whd context (type_of_aux context term) with
217 (*CSC manca il caso dei CAST *)
218 C.MutInd (uri',_,i') ->
219 (* Checks suppressed *)
221 | C.Appl (C.MutInd (uri',_,i') :: tl) ->
222 split tl (List.length tl - k)
224 raise (NotWellTyped "MutCase: the term is not an inductive one")
226 (* Checks suppressed *)
227 if not need_dummy then
228 C.Appl ((outtype::arguments)@[term])
229 else if arguments = [] then
232 C.Appl (outtype::arguments)
234 (* Let's visit all the subterms that will not be visited later *)
239 let _ = type_of_aux context ty in
240 (Some (C.Name n,(C.Decl ty)))
247 (fun (_,_,_,bo) -> ignore (type_of_aux context' bo))
249 (* Checks suppressed *)
250 let (_,_,ty,_) = List.nth fl i in
253 (* Let's visit all the subterms that will not be visited later *)
258 let _ = type_of_aux context ty in
259 (Some (C.Name n,(C.Decl ty)))
266 (fun (_,_,bo) -> ignore (type_of_aux context' bo))
268 (* Checks suppressed *)
269 let (_,ty,_) = List.nth fl i in
272 (*CSC: Is whd the right thing to do? Or should full beta *)
273 (*CSC: reduction be more appropriate? *)
274 (*CSC: Nota: whd fa troppo (esempio: fa anche iota) e full beta sembra molto *)
275 (*CSC: costosa quando fatta ogni passo. Fare solo un passo? *)
276 let synthesized' = CicReduction.whd context synthesized in
277 CicHash.add subterms_to_types t
278 {synthesized = synthesized' ; expected = Cic.Implicit} ;
281 and sort_of_prod context (name,s) (t1, t2) =
282 let module C = Cic in
283 let t1' = CicReduction.whd context t1 in
284 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
285 match (t1', t2') with
286 (C.Sort s1, C.Sort s2)
287 when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
289 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
293 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
295 and eat_prods context hetype =
296 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
300 | (hete, hety)::tl ->
301 (match (CicReduction.whd context hetype) with
303 (* Checks suppressed *)
304 eat_prods context (CicSubstitution.subst hete t) tl
305 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
309 type_of_aux context t
312 let double_type_of metasenv context t =
313 let subterms_to_types = CicHash.create 503 in
314 ignore (type_of_aux' subterms_to_types metasenv context t) ;