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/.
27 {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
31 let res = "i" ^ string_of_int !seed in
36 let fresh_id seed ids_to_terms ids_to_father_ids =
38 let res = gen_id seed in
39 Hashtbl.add ids_to_father_ids res father ;
40 Hashtbl.add ids_to_terms res t ;
44 exception NotEnoughElements;;
45 exception NameExpected;;
47 (*CSC: cut&paste da cicPp.ml *)
48 (* get_nth l n returns the nth element of the list l if it exists or *)
49 (* raises NotEnoughElements if l has less than n elements *)
53 | (n, he::tail) when n > 1 -> get_nth tail (n-1)
54 | (_,_) -> raise NotEnoughElements
57 let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
58 ids_to_inner_types metasenv context idrefs t expectedty
60 let module D = DoubleTypeInference in
61 let module T = CicTypeChecker in
63 let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in
65 D.double_type_of metasenv context t expectedty
67 let rec aux computeinnertypes father context idrefs tt =
68 let fresh_id'' = fresh_id' father tt in
69 (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
70 let aux' = aux computeinnertypes (Some fresh_id'') in
71 (* First of all we compute the inner type and the inner sort *)
72 (* of the term. They may be useful in what follows. *)
73 (*CSC: This is a very inefficient way of computing inner types *)
74 (*CSC: and inner sorts: very deep terms have their types/sorts *)
75 (*CSC: computed again and again. *)
76 let string_of_sort t =
77 match CicReduction.whd context t with
78 C.Sort C.Prop -> "Prop"
79 | C.Sort C.Set -> "Set"
80 | C.Sort C.Type -> "Type"
83 let ainnertypes,innertype,innersort,expected_available =
84 (*CSC: Here we need the algorithm for Coscoy's double type-inference *)
85 (*CSC: (expected type + inferred type). Just for now we use the usual *)
86 (*CSC: type-inference, but the result is very poor. As a very weak *)
87 (*CSC: patch, I apply whd to the computed type. Full beta *)
88 (*CSC: reduction would be a much better option. *)
89 let {D.synthesized = synthesized; D.expected = expected} =
90 if computeinnertypes then
91 D.CicHash.find terms_to_types tt
93 (* We are already in an inner-type and Coscoy's double *)
94 (* type inference algorithm has not been applied. *)
96 CicReduction.whd context (T.type_of_aux' metasenv context tt) ;
99 let innersort = T.type_of_aux' metasenv context synthesized in
100 let ainnertypes,expected_available =
101 if computeinnertypes then
102 let annexpected,expected_available =
105 | Some expectedty' ->
107 (aux false (Some fresh_id'') context idrefs expectedty'),
112 aux false (Some fresh_id'') context idrefs synthesized ;
113 annexpected = annexpected
114 }, expected_available
118 ainnertypes,synthesized, string_of_sort innersort, expected_available
120 let add_inner_type id =
121 match ainnertypes with
123 | Some ainnertypes -> Hashtbl.add ids_to_inner_types id ainnertypes
128 match get_nth context n with
129 (Some (C.Name s,_)) -> s
130 | _ -> raise NameExpected
132 Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
133 if innersort = "Prop" && expected_available then
134 add_inner_type fresh_id'' ;
135 C.ARel (fresh_id'', List.nth idrefs (n-1), n, id)
136 | C.Var (uri,exp_named_subst) ->
137 Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
138 if innersort = "Prop" && expected_available then
139 add_inner_type fresh_id'' ;
140 let exp_named_subst' =
142 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
144 C.AVar (fresh_id'', uri,exp_named_subst')
146 let (_,canonical_context,_) =
147 List.find (function (m,_,_) -> n = m) metasenv
149 Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
150 if innersort = "Prop" && expected_available then
151 add_inner_type fresh_id'' ;
152 C.AMeta (fresh_id'', n,
157 | _, Some t -> Some (aux' context idrefs t)
158 | Some _, None -> assert false (* due to typing rules *))
159 canonical_context l))
160 | C.Sort s -> C.ASort (fresh_id'', s)
161 | C.Implicit -> C.AImplicit (fresh_id'')
163 Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
164 if innersort = "Prop" then
165 add_inner_type fresh_id'' ;
166 C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t)
168 Hashtbl.add ids_to_inner_sorts fresh_id''
169 (string_of_sort innertype) ;
171 (fresh_id'', n, aux' context idrefs s,
172 aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t)
173 | C.Lambda (n,s,t) ->
174 Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
175 if innersort = "Prop" then
177 let father_is_lambda =
181 match Hashtbl.find ids_to_terms father' with
185 if (not father_is_lambda) || expected_available then
186 add_inner_type fresh_id''
189 (fresh_id'',n, aux' context idrefs s,
190 aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
192 Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
193 if innersort = "Prop" then
194 add_inner_type fresh_id'' ;
196 (fresh_id'', n, aux' context idrefs s,
197 aux' ((Some (n, C.Def s))::context) (fresh_id''::idrefs) t)
199 Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
200 if innersort = "Prop" then
201 add_inner_type fresh_id'' ;
202 C.AAppl (fresh_id'', List.map (aux' context idrefs) l)
203 | C.Const (uri,exp_named_subst) ->
204 Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
205 if innersort = "Prop" && expected_available then
206 add_inner_type fresh_id'' ;
207 let exp_named_subst' =
209 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
211 C.AConst (fresh_id'', uri, exp_named_subst')
212 | C.MutInd (uri,tyno,exp_named_subst) ->
213 let exp_named_subst' =
215 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
217 C.AMutInd (fresh_id'', uri, tyno, exp_named_subst')
218 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
219 Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
220 if innersort = "Prop" && expected_available then
221 add_inner_type fresh_id'' ;
222 let exp_named_subst' =
224 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
226 C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst')
227 | C.MutCase (uri, tyno, outty, term, patterns) ->
228 Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
229 if innersort = "Prop" then
230 add_inner_type fresh_id'' ;
231 C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty,
232 aux' context idrefs term, List.map (aux' context idrefs) patterns)
233 | C.Fix (funno, funs) ->
235 List.map (function _ -> gen_id seed) funs in
236 let new_idrefs = List.rev fresh_idrefs @ idrefs in
238 List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs
240 Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
241 if innersort = "Prop" then
242 add_inner_type fresh_id'' ;
243 C.AFix (fresh_id'', funno,
245 (fun id (name, indidx, ty, bo) ->
246 (id, name, indidx, aux' context idrefs ty,
247 aux' (tys@context) new_idrefs bo)
250 | C.CoFix (funno, funs) ->
252 List.map (function _ -> gen_id seed) funs in
253 let new_idrefs = List.rev fresh_idrefs @ idrefs in
255 List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs
257 Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
258 if innersort = "Prop" then
259 add_inner_type fresh_id'' ;
260 C.ACoFix (fresh_id'', funno,
262 (fun id (name, ty, bo) ->
263 (id, name, aux' context idrefs ty,
264 aux' (tys@context) new_idrefs bo)
268 aux true None context idrefs t
271 let acic_of_cic_context metasenv context idrefs t =
272 let ids_to_terms = Hashtbl.create 503 in
273 let ids_to_father_ids = Hashtbl.create 503 in
274 let ids_to_inner_sorts = Hashtbl.create 503 in
275 let ids_to_inner_types = Hashtbl.create 503 in
277 acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
278 ids_to_inner_types metasenv context idrefs t,
279 ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
282 let acic_object_of_cic_object obj =
283 let module C = Cic in
284 let ids_to_terms = Hashtbl.create 503 in
285 let ids_to_father_ids = Hashtbl.create 503 in
286 let ids_to_inner_sorts = Hashtbl.create 503 in
287 let ids_to_inner_types = Hashtbl.create 503 in
288 let ids_to_conjectures = Hashtbl.create 11 in
289 let ids_to_hypotheses = Hashtbl.create 127 in
290 let hypotheses_seed = ref 0 in
291 let conjectures_seed = ref 0 in
293 let acic_term_of_cic_term_context' =
294 acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
295 ids_to_inner_types in
296 let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] [] in
299 C.Constant (id,Some bo,ty,params) ->
300 let abo = acic_term_of_cic_term' bo (Some ty) in
301 let aty = acic_term_of_cic_term' ty None in
303 ("mettereaposto",Some "mettereaposto2",id,Some abo,aty, params)
304 | C.Constant (id,None,ty,params) ->
305 let aty = acic_term_of_cic_term' ty None in
307 ("mettereaposto",None,id,None,aty, params)
308 | C.Variable (id,bo,ty,params) ->
312 | Some bo -> Some (acic_term_of_cic_term' bo (Some ty))
314 let aty = acic_term_of_cic_term' ty None in
316 ("mettereaposto",id,abo,aty, params)
317 | C.CurrentProof (id,conjectures,bo,ty,params) ->
320 (function (i,canonical_context,term) as conjecture ->
321 let cid = "c" ^ string_of_int !conjectures_seed in
322 Hashtbl.add ids_to_conjectures cid conjecture ;
323 incr conjectures_seed ;
324 let idrefs',revacanonical_context =
325 let rec aux context idrefs =
329 let hid = "h" ^ string_of_int !hypotheses_seed in
330 let new_idrefs = hid::idrefs in
331 Hashtbl.add ids_to_hypotheses hid hyp ;
332 incr hypotheses_seed ;
334 (Some (n,C.Decl t)) ->
335 let final_idrefs,atl =
336 aux (hyp::context) new_idrefs tl in
338 acic_term_of_cic_term_context'
339 conjectures context idrefs t None
341 final_idrefs,(hid,Some (n,C.ADecl at))::atl
342 | (Some (n,C.Def t)) ->
343 let final_idrefs,atl =
344 aux (hyp::context) new_idrefs tl in
346 acic_term_of_cic_term_context'
347 conjectures context idrefs t None
349 final_idrefs,(hid,Some (n,C.ADef at))::atl
351 let final_idrefs,atl =
352 aux (hyp::context) new_idrefs tl
354 final_idrefs,(hid,None)::atl
356 aux [] [] (List.rev canonical_context)
359 acic_term_of_cic_term_context' conjectures
360 canonical_context idrefs' term None
362 (cid,i,(List.rev revacanonical_context),aterm)
365 acic_term_of_cic_term_context' conjectures [] [] bo (Some ty) in
366 let aty = acic_term_of_cic_term_context' conjectures [] [] ty None in
368 ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params)
369 | C.InductiveDefinition (tys,params,paramsno) ->
372 (fun (name,_,arity,_) -> Some (C.Name name, C.Decl arity)) tys in
373 let idrefs = List.map (function _ -> gen_id seed) tys in
376 (fun id (name,inductive,ty,cons) ->
379 (function (name,ty) ->
381 acic_term_of_cic_term_context' [] context idrefs ty None)
384 (id,name,inductive,acic_term_of_cic_term' ty None,acons)
385 ) (List.rev idrefs) tys
387 C.AInductiveDefinition ("mettereaposto",atys,params,paramsno)
389 aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
390 ids_to_conjectures,ids_to_hypotheses