1 (* Copyright (C) 2003-2005, 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/.
30 module TC = CicTypeChecker
31 module PEH = ProofEngineHelpers
32 module E = CicEnvironment
33 module UM = UriManager
35 module PER = ProofEngineReduction
37 module DTI = DoubleTypeInference
39 (* fresh name generator *****************************************************)
43 if i <= 0 then assert false else
44 let c = name.[pred i] in
45 if c >= '0' && c <= '9' then aux (pred i)
46 else Str.string_before name i, Str.string_after name i
48 let before, after = aux (String.length name) in
49 let i = if after = "" then -1 else int_of_string after in
53 C.Name (if i < 0 then s else s ^ string_of_int i)
55 let mk_fresh_name context (name, k) =
56 let rec aux i = function
58 | Some (C.Name s, _) :: entries ->
60 if m = name && j >= i then aux (succ j) entries else aux i entries
61 | _ :: entries -> aux i entries
65 let mk_fresh_name does_not_occur context = function
66 | C.Name s -> mk_fresh_name context (split s)
68 if does_not_occur then C.Anonymous
69 else mk_fresh_name context (split "LOCAL")
71 (* helper functions *********************************************************)
73 let rec list_fold_right_cps g map l a =
77 let h a = map g hd a in
78 list_fold_right_cps h map tl a
80 let rec list_fold_left_cps g map a = function
83 let h a = list_fold_left_cps g map a tl in
86 let rec list_map_cps g map = function
90 let g tl = g (hd :: tl) in
97 let compose f g x = f (g x)
99 let fst3 (x, _, _) = x
103 Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
104 Printf.eprintf "Ref: term : %s\n" (Pp.ppterm t);
107 try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t with
108 | Rf.RefineFailure s as e ->
109 Printf.eprintf "REFINE FAILURE: %s\n" (Lazy.force s);
112 Printf.eprintf "REFINE ERROR: %s\n" (Printexc.to_string e);
115 let get_type msg c t =
117 prerr_endline ("TC: " ^ s);
118 prerr_endline ("TC: context: " ^ Pp.ppcontext c);
119 prerr_string "TC: term : "; Ut.pp_term prerr_string [] c t;
120 prerr_newline (); prerr_endline ("TC: location: " ^ msg)
122 try let ty, _ = TC.type_of_aux' [] c t Un.default_ugraph in ty with
123 | TC.TypeCheckerFailure s as e ->
124 log ("failure: " ^ Lazy.force s); raise e
125 | TC.AssertFailure s as e ->
126 log ("assert : " ^ Lazy.force s); raise e
129 match PEH.split_with_whd (c, t) with
130 | (_, hd) :: _, _ -> hd
134 match get_tail c (get_type "is_prop" c t) with
135 | C.Sort C.Prop -> true
140 is_prop c (get_type "is_prop" c t)
142 let is_sort = function
146 let is_unsafe h (c, t) = true
148 let is_not_atomic = function
154 | C.MutConstruct _ -> false
157 let is_atomic t = not (is_not_atomic t)
159 let get_ind_type uri tyno =
160 match E.get_obj Un.default_ugraph uri with
161 | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
164 let get_ind_names uri tno =
166 let ts = match E.get_obj Un.default_ugraph uri with
167 | C.InductiveDefinition (ts, _, _, _), _ -> ts
170 match List.nth ts tno with
171 | (_, _, _, cs) -> List.map fst cs
172 with Invalid_argument _ -> failwith "get_ind_names"
174 let get_default_eliminator context uri tyno ty =
175 let _, (name, _, _, _) = get_ind_type uri tyno in
176 let ext = match get_tail context (get_type "get_def_elim" context ty) with
177 | C.Sort C.Prop -> "_ind"
178 | C.Sort C.Set -> "_rec"
179 | C.Sort (C.CProp _) -> "_rect"
180 | C.Sort (C.Type _) -> "_rect"
182 Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
185 let buri = UM.buri_of_uri uri in
186 let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
189 let get_ind_parameters c t =
190 let ty = get_type "get_ind_pars 1" c t in
191 let ps = match get_tail c ty with
193 | C.Appl (C.MutInd _ :: args) -> args
196 let disp = match get_tail c (get_type "get_ind_pars 2" c ty) with
203 let cic = D.deannotate_term
205 let occurs c ~what ~where =
206 let result = ref false in
207 let equality c t1 t2 =
208 let r = Ut.alpha_equivalence t1 t2 in
209 result := !result || r; r
211 let context, what, with_what = c, [what], [C.Rel 0] in
212 let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
215 let name_of_uri uri tyno cno =
216 let get_ind_type tys tyno =
217 let s, _, _, cs = List.nth tys tyno in s, cs
219 match (fst (E.get_obj Un.default_ugraph uri)), tyno, cno with
220 | C.Variable (s, _, _, _, _), _, _ -> s
221 | C.Constant (s, _, _, _, _), _, _ -> s
222 | C.InductiveDefinition (tys, _, _, _), Some i, None ->
223 let s, _ = get_ind_type tys i in s
224 | C.InductiveDefinition (tys, _, _, _), Some i, Some j ->
225 let _, cs = get_ind_type tys i in
226 let s, _ = List.nth cs (pred j) in s
229 (* Ensuring Barendregt convenction ******************************************)
231 let rec add_entries map c = function
234 let sname, w = map hd in
235 let entry = Some (Cic.Name sname, C.Decl w) in
236 add_entries map (entry :: c) tl
239 try match List.nth c (pred i) with
240 | Some (Cic.Name sname, _) -> sname
243 | Failure _ -> assert false
244 | Invalid_argument _ -> assert false
247 let get_fix_decl (sname, i, w, v) = sname, w in
248 let get_cofix_decl (sname, w, v) = sname, w in
249 let rec bc c = function
250 | C.LetIn (name, v, ty, t) ->
251 let dno = DTI.does_not_occur 1 t in
252 let name = mk_fresh_name dno c name in
253 let entry = Some (name, C.Def (v, ty)) in
254 let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
255 C.LetIn (name, v, ty, t)
256 | C.Lambda (name, w, t) ->
257 let dno = DTI.does_not_occur 1 t in
258 let name = mk_fresh_name dno c name in
259 let entry = Some (name, C.Decl w) in
260 let w, t = bc c w, bc (entry :: c) t in
261 C.Lambda (name, w, t)
262 | C.Prod (name, w, t) ->
263 let dno = DTI.does_not_occur 1 t in
264 let name = mk_fresh_name dno c name in
265 let entry = Some (name, C.Decl w) in
266 let w, t = bc c w, bc (entry :: c) t in
269 let vs = List.map (bc c) vs in
271 | C.MutCase (uri, tyno, u, v, ts) ->
272 let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
273 C.MutCase (uri, tyno, u, v, ts)
275 let t, u = bc c t, bc c u in
277 | C.Fix (i, fixes) ->
278 let d = add_entries get_fix_decl c fixes in
279 let bc_fix (sname, i, w, v) = (sname, i, bc c w, bc d v) in
280 let fixes = List.map bc_fix fixes in
282 | C.CoFix (i, cofixes) ->
283 let d = add_entries get_cofix_decl c cofixes in
284 let bc_cofix (sname, w, v) = (sname, bc c w, bc d v) in
285 let cofixes = List.map bc_cofix cofixes in
292 let get_fix_decl (id, sname, i, w, v) = sname, cic w in
293 let get_cofix_decl (id, sname, w, v) = sname, cic w in
294 let rec bc c = function
295 | C.ALetIn (id, name, v, ty, t) ->
296 let dno = DTI.does_not_occur 1 (cic t) in
297 let name = mk_fresh_name dno c name in
298 let entry = Some (name, C.Def (cic v, cic ty)) in
299 let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
300 C.ALetIn (id, name, v, ty, t)
301 | C.ALambda (id, name, w, t) ->
302 let dno = DTI.does_not_occur 1 (cic t) in
303 let name = mk_fresh_name dno c name in
304 let entry = Some (name, C.Decl (cic w)) in
305 let w, t = bc c w, bc (entry :: c) t in
306 C.ALambda (id, name, w, t)
307 | C.AProd (id, name, w, t) ->
308 let dno = DTI.does_not_occur 1 (cic t) in
309 let name = mk_fresh_name dno c name in
310 let entry = Some (name, C.Decl (cic w)) in
311 let w, t = bc c w, bc (entry :: c) t in
312 C.AProd (id, name, w, t)
313 | C.AAppl (id, vs) ->
314 let vs = List.map (bc c) vs in
316 | C.AMutCase (id, uri, tyno, u, v, ts) ->
317 let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
318 C.AMutCase (id, uri, tyno, u, v, ts)
319 | C.ACast (id, t, u) ->
320 let t, u = bc c t, bc c u in
322 | C.AFix (id, i, fixes) ->
323 let d = add_entries get_fix_decl c fixes in
324 let bc_fix (id, sname, i, w, v) = (id, sname, i, bc c w, bc d v) in
325 let fixes = List.map bc_fix fixes in
326 C.AFix (id, i, fixes)
327 | C.ACoFix (id, i, cofixes) ->
328 let d = add_entries get_cofix_decl c cofixes in
329 let bc_cofix (id, sname, w, v) = (id, sname, bc c w, bc d v) in
330 let cofixes = List.map bc_cofix cofixes in
331 C.ACoFix (id, i, cofixes)
332 | C.ARel (id1, id2, i, sname) ->
333 let sname = get_sname c i in
334 C.ARel (id1, id2, i, sname)