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
38 (* fresh name generator *****************************************************)
42 if i <= 0 then assert false else
43 let c = name.[pred i] in
44 if c >= '0' && c <= '9' then aux (pred i)
45 else Str.string_before name i, Str.string_after name i
47 let before, after = aux (String.length name) in
48 let i = if after = "" then -1 else int_of_string after in
52 C.Name (if i < 0 then s else s ^ string_of_int i)
54 let mk_fresh_name context (name, k) =
55 let rec aux i = function
57 | Some (C.Name s, _) :: entries ->
59 if m = name && j >= i then aux (succ j) entries else aux i entries
60 | _ :: entries -> aux i entries
64 let mk_fresh_name context = function
65 | C.Anonymous -> C.Anonymous
66 | C.Name s -> mk_fresh_name context (split s)
68 (* helper functions *********************************************************)
70 let rec list_fold_right_cps g map l a =
74 let h a = map g hd a in
75 list_fold_right_cps h map tl a
77 let rec list_fold_left_cps g map a = function
80 let h a = list_fold_left_cps g map a tl in
83 let rec list_map_cps g map = function
87 let g tl = g (hd :: tl) in
94 let compose f g x = f (g x)
96 let fst3 (x, _, _) = x
100 Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
101 Printf.eprintf "Ref: term : %s\n" (Pp.ppterm t);
104 try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t with
105 | Rf.RefineFailure s as e ->
106 Printf.eprintf "REFINE FAILURE: %s\n" (Lazy.force s);
109 Printf.eprintf "REFINE ERROR: %s\n" (Printexc.to_string e);
112 let get_type msg c t =
114 prerr_endline ("TC: " ^ s);
115 prerr_endline ("TC: context: " ^ Pp.ppcontext c);
116 prerr_string "TC: term : "; Ut.pp_term prerr_string [] c t;
117 prerr_newline (); prerr_endline ("TC: location: " ^ msg)
119 try let ty, _ = TC.type_of_aux' [] c t Un.default_ugraph in ty with
120 | TC.TypeCheckerFailure s as e ->
121 log ("failure: " ^ Lazy.force s); raise e
122 | TC.AssertFailure s as e ->
123 log ("assert : " ^ Lazy.force s); raise e
126 match PEH.split_with_whd (c, t) with
127 | (_, hd) :: _, _ -> hd
131 match get_tail c (get_type "is_proof 1" c (get_type "is_proof 2" c t)) with
132 | C.Sort C.Prop -> true
136 let is_sort = function
140 let is_unsafe h (c, t) = true
142 let is_not_atomic = function
148 | C.MutConstruct _ -> false
151 let is_atomic t = not (is_not_atomic t)
153 let get_ind_type uri tyno =
154 match E.get_obj Un.default_ugraph uri with
155 | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
158 let get_ind_names uri tno =
160 let ts = match E.get_obj Un.default_ugraph uri with
161 | C.InductiveDefinition (ts, _, _, _), _ -> ts
164 match List.nth ts tno with
165 | (_, _, _, cs) -> List.map fst cs
166 with Invalid_argument _ -> failwith "get_ind_names"
168 let get_default_eliminator context uri tyno ty =
169 let _, (name, _, _, _) = get_ind_type uri tyno in
170 let ext = match get_tail context (get_type "get_def_elim" context ty) with
171 | C.Sort C.Prop -> "_ind"
172 | C.Sort C.Set -> "_rec"
173 | C.Sort (C.CProp _) -> "_rect"
174 | C.Sort (C.Type _) -> "_rect"
176 Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
179 let buri = UM.buri_of_uri uri in
180 let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
183 let get_ind_parameters c t =
184 let ty = get_type "get_ind_pars 1" c t in
185 let ps = match get_tail c ty with
187 | C.Appl (C.MutInd _ :: args) -> args
190 let disp = match get_tail c (get_type "get_ind_pars 2" c ty) with
197 let cic = D.deannotate_term
199 let occurs c ~what ~where =
200 let result = ref false in
201 let equality c t1 t2 =
202 let r = Ut.alpha_equivalence t1 t2 in
203 result := !result || r; r
205 let context, what, with_what = c, [what], [C.Rel 0] in
206 let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
209 let name_of_uri uri tyno cno =
210 let get_ind_type tys tyno =
211 let s, _, _, cs = List.nth tys tyno in s, cs
213 match (fst (E.get_obj Un.default_ugraph uri)), tyno, cno with
214 | C.Variable (s, _, _, _, _), _, _ -> s
215 | C.Constant (s, _, _, _, _), _, _ -> s
216 | C.InductiveDefinition (tys, _, _, _), Some i, None ->
217 let s, _ = get_ind_type tys i in s
218 | C.InductiveDefinition (tys, _, _, _), Some i, Some j ->
219 let _, cs = get_ind_type tys i in
220 let s, _ = List.nth cs (pred j) in s
223 (* Ensuring Barendregt convenction ******************************************)
225 let rec add_entries map c = function
228 let sname, w = map hd in
229 let entry = Some (Cic.Name sname, C.Decl w) in
230 add_entries map (entry :: c) tl
233 try match List.nth c (pred i) with
234 | Some (Cic.Name sname, _) -> sname
237 | Failure _ -> assert false
238 | Invalid_argument _ -> assert false
241 let get_fix_decl (sname, i, w, v) = sname, w in
242 let get_cofix_decl (sname, w, v) = sname, w in
243 let rec bc c = function
244 | C.LetIn (name, v, ty, t) ->
245 let name = mk_fresh_name c name in
246 let entry = Some (name, C.Def (v, ty)) in
247 let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
248 C.LetIn (name, v, ty, t)
249 | C.Lambda (name, w, t) ->
250 let name = mk_fresh_name c name in
251 let entry = Some (name, C.Decl w) in
252 let w, t = bc c w, bc (entry :: c) t in
253 C.Lambda (name, w, t)
254 | C.Prod (name, w, t) ->
255 let name = mk_fresh_name c name in
256 let entry = Some (name, C.Decl w) in
257 let w, t = bc c w, bc (entry :: c) t in
260 let vs = List.map (bc c) vs in
262 | C.MutCase (uri, tyno, u, v, ts) ->
263 let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
264 C.MutCase (uri, tyno, u, v, ts)
266 let t, u = bc c t, bc c u in
268 | C.Fix (i, fixes) ->
269 let d = add_entries get_fix_decl c fixes in
270 let bc_fix (sname, i, w, v) = (sname, i, bc c w, bc d v) in
271 let fixes = List.map bc_fix fixes in
273 | C.CoFix (i, cofixes) ->
274 let d = add_entries get_cofix_decl c cofixes in
275 let bc_cofix (sname, w, v) = (sname, bc c w, bc d v) in
276 let cofixes = List.map bc_cofix cofixes in
283 let get_fix_decl (id, sname, i, w, v) = sname, cic w in
284 let get_cofix_decl (id, sname, w, v) = sname, cic w in
285 let rec bc c = function
286 | C.ALetIn (id, name, v, ty, t) ->
287 let name = mk_fresh_name c name in
288 let entry = Some (name, C.Def (cic v, cic ty)) in
289 let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
290 C.ALetIn (id, name, v, ty, t)
291 | C.ALambda (id, name, w, t) ->
292 let name = mk_fresh_name c name in
293 let entry = Some (name, C.Decl (cic w)) in
294 let w, t = bc c w, bc (entry :: c) t in
295 C.ALambda (id, name, w, t)
296 | C.AProd (id, name, w, t) ->
297 let name = mk_fresh_name c name in
298 let entry = Some (name, C.Decl (cic w)) in
299 let w, t = bc c w, bc (entry :: c) t in
300 C.AProd (id, name, w, t)
301 | C.AAppl (id, vs) ->
302 let vs = List.map (bc c) vs in
304 | C.AMutCase (id, uri, tyno, u, v, ts) ->
305 let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
306 C.AMutCase (id, uri, tyno, u, v, ts)
307 | C.ACast (id, t, u) ->
308 let t, u = bc c t, bc c u in
310 | C.AFix (id, i, fixes) ->
311 let d = add_entries get_fix_decl c fixes in
312 let bc_fix (id, sname, i, w, v) = (id, sname, i, bc c w, bc d v) in
313 let fixes = List.map bc_fix fixes in
314 C.AFix (id, i, fixes)
315 | C.ACoFix (id, i, cofixes) ->
316 let d = add_entries get_cofix_decl c cofixes in
317 let bc_cofix (id, sname, w, v) = (id, sname, bc c w, bc d v) in
318 let cofixes = List.map bc_cofix cofixes in
319 C.ACoFix (id, i, cofixes)
320 | C.ARel (id1, id2, i, sname) ->
321 let sname = get_sname c i in
322 C.ARel (id1, id2, i, sname)