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 (* time stamping ************************************************************)
43 let times = Unix.times () in
44 let stamp = times.Unix.tms_utime +. times.Unix.tms_utime in
45 let lap = stamp -. !old in
46 Printf.eprintf "TIME STAMP: %s: %f\n" msg lap; flush stdout;
49 (* raw cic prettyprinter ****************************************************)
51 let xiter out so ss sc map l =
52 let rec aux = function
53 | hd :: tl when tl <> [] -> map hd; out ss; aux tl
54 | hd :: tl -> map hd; aux tl
59 let abst s w = Some (s, C.Decl w)
61 let abbr s v w = Some (s, C.Def (v, w))
63 let pp_sort out = function
64 | C.Type _ -> out "\Type"
65 | C.Prop -> out "\Prop"
66 | C.CProp _ -> out "\CProp"
69 let pp_name out = function
71 | C.Anonymous -> out "_"
74 try match List.nth c (pred i) with
75 | None -> out (Printf.sprintf "%u[?]" i)
76 | Some (s, _) -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
77 with Failure "nth" -> out (Printf.sprintf "%u[%u]" i (List.length c - i))
79 let pp_implict out = function
81 | Some `Closed -> out "?[Closed]"
82 | Some `Type -> out "?[Type]"
83 | Some `Hole -> out "?[Hole]"
86 out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a))
88 let rec pp_term out e c = function
89 | C.Sort h -> pp_sort out h
90 | C.Rel i -> pp_rel out c i
91 | C.Implicit x -> pp_implict out x
93 let map = function None -> out "_" | Some v -> pp_term out e c v in
94 out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss
96 pp_uri out a; pp_xss out e c xss
98 pp_uri out a; pp_xss out e c xss
99 | C.MutInd (a, m, xss) ->
100 pp_uri out a; out (Printf.sprintf "/%u" m);
102 | C.MutConstruct (a, m, n, xss) ->
103 pp_uri out a; out (Printf.sprintf "/%u/%u" m n);
106 out "type "; pp_term out e c w; out " contains "; pp_term out e c v
108 xiter out "(" " @ " ")" (pp_term out e c) vs
109 | C.MutCase (a, m, w, v, vs) ->
110 out "match "; pp_term out e c v;
111 out " of "; pp_uri out a; out (Printf.sprintf "/%u" m);
112 out " to "; pp_term out e c w;
113 xiter out " cases " " | " "" (pp_term out e c) vs
114 | C.Prod (s, w, t) ->
115 out "forall "; pp_name out s; out " of "; pp_term out e c w;
116 out " in "; pp_term out e (abst s w :: c) t
117 | C.Lambda (s, w, t) ->
118 out "fun "; pp_name out s; out " of "; pp_term out e c w;
119 out " in "; pp_term out e (abst s w :: c) t
120 | C.LetIn (s, v, w, t) ->
121 out "let "; pp_name out s;
122 out " def "; pp_term out e c v; out " of "; pp_term out e c w;
123 out " in "; pp_term out e (abbr s v w :: c) t
125 let map c (s, _, w, v) = abbr (C.Name s) v w :: c in
126 let c' = List.fold_left map c fs in
127 let map (s, i, w, v) =
128 out (Printf.sprintf "%s[%u] def " s i); pp_term out e c' v;
129 out " of "; pp_term out e c w;
131 xiter out "let rec " " and " " in " map fs; pp_rel out c' (succ i)
133 let map c (s, w, v) = abbr (C.Name s) v w :: c in
134 let c' = List.fold_left map c fs in
136 out s; pp_term out e c' v;
137 out " of "; pp_term out e c w;
139 xiter out "let corec " " and " " in " map fs; pp_rel out c' (succ i)
141 and pp_xss out e c xss =
142 let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
143 xiter out "[" "; " "]" map xss
145 (* fresh name generator *****************************************************)
149 if i <= 0 then assert false else
150 let c = name.[pred i] in
151 if c >= '0' && c <= '9' then aux (pred i)
152 else Str.string_before name i, Str.string_after name i
154 let before, after = aux (String.length name) in
155 let i = if after = "" then -1 else int_of_string after in
159 C.Name (if i < 0 then s else s ^ string_of_int i)
161 let mk_fresh_name context (name, k) =
162 let rec aux i = function
164 | Some (C.Name s, _) :: entries ->
165 let m, j = split s in
166 if m = name && j >= i then aux (succ j) entries else aux i entries
167 | _ :: entries -> aux i entries
171 let mk_fresh_name context = function
172 | C.Anonymous -> C.Anonymous
173 | C.Name s -> mk_fresh_name context (split s)
175 (* helper functions *********************************************************)
177 let rec list_map_cps g map = function
181 let g tl = g (hd :: tl) in
182 list_map_cps g map tl
188 let compose f g x = f (g x)
190 let fst3 (x, _, _) = x
193 try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t
195 Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
196 Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
197 Printf.eprintf "Ref: term : %s\n" (Pp.ppterm t);
200 let get_type msg c t =
202 prerr_endline ("TC: " ^ s);
203 prerr_endline ("TC: context: " ^ Pp.ppcontext c);
204 prerr_string "TC: term : "; pp_term prerr_string [] c t;
205 prerr_newline (); prerr_endline ("TC: location: " ^ msg)
207 try let ty, _ = TC.type_of_aux' [] c t Un.default_ugraph in ty with
208 | TC.TypeCheckerFailure s as e ->
209 log ("failure: " ^ Lazy.force s); raise e
210 | TC.AssertFailure s as e ->
211 log ("assert : " ^ Lazy.force s); raise e
214 match PEH.split_with_whd (c, t) with
215 | (_, hd) :: _, _ -> hd
219 match get_tail c (get_type "is_proof 1" c (get_type "is_proof 2" c t)) with
220 | C.Sort C.Prop -> true
224 let is_sort = function
228 let is_unsafe h (c, t) = true
230 let is_not_atomic = function
236 | C.MutConstruct _ -> false
239 let is_atomic t = not (is_not_atomic t)
241 let get_ind_type uri tyno =
242 match E.get_obj Un.default_ugraph uri with
243 | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
246 let get_ind_names uri tno =
248 let ts = match E.get_obj Un.default_ugraph uri with
249 | C.InductiveDefinition (ts, _, _, _), _ -> ts
252 match List.nth ts tno with
253 | (_, _, _, cs) -> List.map fst cs
254 with Invalid_argument _ -> failwith "get_ind_names"
256 let get_default_eliminator context uri tyno ty =
257 let _, (name, _, _, _) = get_ind_type uri tyno in
258 let ext = match get_tail context (get_type "get_def_elim" context ty) with
259 | C.Sort C.Prop -> "_ind"
260 | C.Sort C.Set -> "_rec"
261 | C.Sort (C.CProp _) -> "_rect"
262 | C.Sort (C.Type _) -> "_rect"
264 Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
267 let buri = UM.buri_of_uri uri in
268 let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
271 let get_ind_parameters c t =
272 let ty = get_type "get_ind_pars 1" c t in
273 let ps = match get_tail c ty with
275 | C.Appl (C.MutInd _ :: args) -> args
278 let disp = match get_tail c (get_type "get_ind_pars 2" c ty) with
285 let cic = D.deannotate_term
287 let occurs c ~what ~where =
288 let result = ref false in
289 let equality c t1 t2 =
290 let r = Ut.alpha_equivalence t1 t2 in
291 result := !result || r; r
293 let context, what, with_what = c, [what], [C.Rel 0] in
294 let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
297 let name_of_uri uri tyno cno =
298 let get_ind_type tys tyno =
299 let s, _, _, cs = List.nth tys tyno in s, cs
301 match (fst (E.get_obj Un.default_ugraph uri)), tyno, cno with
302 | C.Variable (s, _, _, _, _), _, _ -> s
303 | C.Constant (s, _, _, _, _), _, _ -> s
304 | C.InductiveDefinition (tys, _, _, _), Some i, None ->
305 let s, _ = get_ind_type tys i in s
306 | C.InductiveDefinition (tys, _, _, _), Some i, Some j ->
307 let _, cs = get_ind_type tys i in
308 let s, _ = List.nth cs (pred j) in s
311 (* Ensuring Barendregt convenction ******************************************)
313 let rec add_entries map c = function
316 let sname, w = map hd in
317 let entry = Some (Cic.Name sname, C.Decl w) in
318 add_entries map (entry :: c) tl
321 try match List.nth c (pred i) with
322 | Some (Cic.Name sname, _) -> sname
325 | Failure _ -> assert false
326 | Invalid_argument _ -> assert false
329 let get_fix_decl (sname, i, w, v) = sname, w in
330 let get_cofix_decl (sname, w, v) = sname, w in
331 let rec bc c = function
332 | C.LetIn (name, v, ty, t) ->
333 let name = mk_fresh_name c name in
334 let entry = Some (name, C.Def (v, ty)) in
335 let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
336 C.LetIn (name, v, ty, t)
337 | C.Lambda (name, w, t) ->
338 let name = mk_fresh_name c name in
339 let entry = Some (name, C.Decl w) in
340 let w, t = bc c w, bc (entry :: c) t in
341 C.Lambda (name, w, t)
342 | C.Prod (name, w, t) ->
343 let name = mk_fresh_name c name in
344 let entry = Some (name, C.Decl w) in
345 let w, t = bc c w, bc (entry :: c) t in
348 let vs = List.map (bc c) vs in
350 | C.MutCase (uri, tyno, u, v, ts) ->
351 let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
352 C.MutCase (uri, tyno, u, v, ts)
354 let t, u = bc c t, bc c u in
356 | C.Fix (i, fixes) ->
357 let d = add_entries get_fix_decl c fixes in
358 let bc_fix (sname, i, w, v) = (sname, i, bc c w, bc d v) in
359 let fixes = List.map bc_fix fixes in
361 | C.CoFix (i, cofixes) ->
362 let d = add_entries get_cofix_decl c cofixes in
363 let bc_cofix (sname, w, v) = (sname, bc c w, bc d v) in
364 let cofixes = List.map bc_cofix cofixes in
371 let get_fix_decl (id, sname, i, w, v) = sname, cic w in
372 let get_cofix_decl (id, sname, w, v) = sname, cic w in
373 let rec bc c = function
374 | C.ALetIn (id, name, v, ty, t) ->
375 let name = mk_fresh_name c name in
376 let entry = Some (name, C.Def (cic v, cic ty)) in
377 let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
378 C.ALetIn (id, name, v, ty, t)
379 | C.ALambda (id, name, w, t) ->
380 let name = mk_fresh_name c name in
381 let entry = Some (name, C.Decl (cic w)) in
382 let w, t = bc c w, bc (entry :: c) t in
383 C.ALambda (id, name, w, t)
384 | C.AProd (id, name, w, t) ->
385 let name = mk_fresh_name c name in
386 let entry = Some (name, C.Decl (cic w)) in
387 let w, t = bc c w, bc (entry :: c) t in
388 C.AProd (id, name, w, t)
389 | C.AAppl (id, vs) ->
390 let vs = List.map (bc c) vs in
392 | C.AMutCase (id, uri, tyno, u, v, ts) ->
393 let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
394 C.AMutCase (id, uri, tyno, u, v, ts)
395 | C.ACast (id, t, u) ->
396 let t, u = bc c t, bc c u in
398 | C.AFix (id, i, fixes) ->
399 let d = add_entries get_fix_decl c fixes in
400 let bc_fix (id, sname, i, w, v) = (id, sname, i, bc c w, bc d v) in
401 let fixes = List.map bc_fix fixes in
402 C.AFix (id, i, fixes)
403 | C.ACoFix (id, i, cofixes) ->
404 let d = add_entries get_cofix_decl c cofixes in
405 let bc_cofix (id, sname, w, v) = (id, sname, bc c w, bc d v) in
406 let cofixes = List.map bc_cofix cofixes in
407 C.ACoFix (id, i, cofixes)
408 | C.ARel (id1, id2, i, sname) ->
409 let sname = get_sname c i in
410 C.ARel (id1, id2, i, sname)