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 (* raw cic prettyprinter ****************************************************)
40 let xiter out so ss sc map l =
41 let rec aux = function
42 | hd :: tl when tl <> [] -> map hd; out ss; aux tl
43 | hd :: tl -> map hd; aux tl
48 let abst s w = Some (s, C.Decl w)
50 let abbr s v w = Some (s, C.Def (v, w))
52 let pp_sort out = function
53 | C.Type _ -> out "\Type"
54 | C.Prop -> out "\Prop"
55 | C.CProp _ -> out "\CProp"
58 let pp_name out = function
60 | C.Anonymous -> out "_"
63 try match List.nth c (pred i) with
64 | None -> out (Printf.sprintf "%u[?]" i)
65 | Some (s, _) -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
66 with Failure "nth" -> out (Printf.sprintf "%u[%u]" i (List.length c - i))
68 let pp_implict out = function
70 | Some `Closed -> out "?[Closed]"
71 | Some `Type -> out "?[Type]"
72 | Some `Hole -> out "?[Hole]"
75 out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a))
77 let rec pp_term out e c = function
78 | C.Sort h -> pp_sort out h
79 | C.Rel i -> pp_rel out c i
80 | C.Implicit x -> pp_implict out x
82 let map = function None -> out "_" | Some v -> pp_term out e c v in
83 out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss
85 pp_uri out a; pp_xss out e c xss
87 pp_uri out a; pp_xss out e c xss
88 | C.MutInd (a, m, xss) ->
89 pp_uri out a; out (Printf.sprintf "/%u" m);
91 | C.MutConstruct (a, m, n, xss) ->
92 pp_uri out a; out (Printf.sprintf "/%u/%u" m n);
95 out "type "; pp_term out e c w; out " contains "; pp_term out e c v
97 xiter out "(" " @ " ")" (pp_term out e c) vs
98 | C.MutCase (a, m, w, v, vs) ->
99 out "match "; pp_term out e c v;
100 out " of "; pp_uri out a; out (Printf.sprintf "/%u" m);
101 out " to "; pp_term out e c w;
102 xiter out " cases " " | " "" (pp_term out e c) vs
103 | C.Prod (s, w, t) ->
104 out "forall "; pp_name out s; out " of "; pp_term out e c w;
105 out " in "; pp_term out e (abst s w :: c) t
106 | C.Lambda (s, w, t) ->
107 out "fun "; pp_name out s; out " of "; pp_term out e c w;
108 out " in "; pp_term out e (abst s w :: c) t
109 | C.LetIn (s, v, w, t) ->
110 out "let "; pp_name out s;
111 out " def "; pp_term out e c v; out " of "; pp_term out e c w;
112 out " in "; pp_term out e (abbr s v w :: c) t
114 let map c (s, _, w, v) = abbr (C.Name s) v w :: c in
115 let c' = List.fold_left map c fs in
116 let map (s, i, w, v) =
117 out (Printf.sprintf "%s[%u] def " s i); pp_term out e c' v;
118 out " of "; pp_term out e c w;
120 xiter out "let rec " " and " " in " map fs; pp_rel out c' (succ i)
122 let map c (s, w, v) = abbr (C.Name s) v w :: c in
123 let c' = List.fold_left map c fs in
125 out s; pp_term out e c' v;
126 out " of "; pp_term out e c w;
128 xiter out "let corec " " and " " in " map fs; pp_rel out c' (succ i)
130 and pp_xss out e c xss =
131 let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
132 xiter out "[" "; " "]" map xss
134 (* fresh name generator *****************************************************)
138 if i <= 0 then assert false else
139 let c = name.[pred i] in
140 if c >= '0' && c <= '9' then aux (pred i)
141 else Str.string_before name i, Str.string_after name i
143 let before, after = aux (String.length name) in
144 let i = if after = "" then -1 else int_of_string after in
148 C.Name (if i < 0 then s else s ^ string_of_int i)
150 let mk_fresh_name context (name, k) =
151 let rec aux i = function
153 | Some (C.Name s, _) :: entries ->
154 let m, j = split s in
155 if m = name && j >= i then aux (succ j) entries else aux i entries
156 | _ :: entries -> aux i entries
160 let mk_fresh_name context = function
161 | C.Anonymous -> C.Anonymous
162 | C.Name s -> mk_fresh_name context (split s)
164 (* helper functions *********************************************************)
166 let rec list_map_cps g map = function
170 let g tl = g (hd :: tl) in
171 list_map_cps g map tl
177 let compose f g x = f (g x)
179 let fst3 (x, _, _) = x
182 try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t
184 Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
185 Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
186 Printf.eprintf "Ref: term : %s\n" (Pp.ppterm t);
189 let get_type msg c t =
191 prerr_endline ("TC: " ^ s);
192 prerr_endline ("TC: context: " ^ Pp.ppcontext c);
193 prerr_string "TC: term : "; pp_term prerr_string [] c t;
194 prerr_newline (); prerr_endline ("TC: location: " ^ msg)
196 try let ty, _ = TC.type_of_aux' [] c t Un.default_ugraph in ty with
197 | TC.TypeCheckerFailure s as e ->
198 log ("failure: " ^ Lazy.force s); raise e
199 | TC.AssertFailure s as e ->
200 log ("assert : " ^ Lazy.force s); raise e
203 match PEH.split_with_whd (c, t) with
204 | (_, hd) :: _, _ -> hd
208 match get_tail c (get_type "is_proof 1" c (get_type "is_proof 2" c t)) with
209 | C.Sort C.Prop -> true
213 let is_sort = function
217 let is_unsafe h (c, t) = true
219 let is_not_atomic = function
225 | C.MutConstruct _ -> false
228 let is_atomic t = not (is_not_atomic t)
230 let get_ind_type uri tyno =
231 match E.get_obj Un.default_ugraph uri with
232 | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
235 let get_ind_names uri tno =
237 let ts = match E.get_obj Un.default_ugraph uri with
238 | C.InductiveDefinition (ts, _, _, _), _ -> ts
241 match List.nth ts tno with
242 | (_, _, _, cs) -> List.map fst cs
243 with Invalid_argument _ -> failwith "get_ind_names"
245 let get_default_eliminator context uri tyno ty =
246 let _, (name, _, _, _) = get_ind_type uri tyno in
247 let ext = match get_tail context (get_type "get_def_elim" context ty) with
248 | C.Sort C.Prop -> "_ind"
249 | C.Sort C.Set -> "_rec"
250 | C.Sort (C.CProp _) -> "_rect"
251 | C.Sort (C.Type _) -> "_rect"
253 Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
256 let buri = UM.buri_of_uri uri in
257 let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
260 let get_ind_parameters c t =
261 let ty = get_type "get_ind_pars 1" c t in
262 let ps = match get_tail c ty with
264 | C.Appl (C.MutInd _ :: args) -> args
267 let disp = match get_tail c (get_type "get_ind_pars 2" c ty) with
274 let cic = D.deannotate_term
276 let occurs c ~what ~where =
277 let result = ref false in
278 let equality c t1 t2 =
279 let r = Ut.alpha_equivalence t1 t2 in
280 result := !result || r; r
282 let context, what, with_what = c, [what], [C.Rel 0] in
283 let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
286 let name_of_uri uri tyno cno =
287 let get_ind_type tys tyno =
288 let s, _, _, cs = List.nth tys tyno in s, cs
290 match (fst (E.get_obj Un.default_ugraph uri)), tyno, cno with
291 | C.Variable (s, _, _, _, _), _, _ -> s
292 | C.Constant (s, _, _, _, _), _, _ -> s
293 | C.InductiveDefinition (tys, _, _, _), Some i, None ->
294 let s, _ = get_ind_type tys i in s
295 | C.InductiveDefinition (tys, _, _, _), Some i, Some j ->
296 let _, cs = get_ind_type tys i in
297 let s, _ = List.nth cs (pred j) in s
300 (* Ensuring Barendregt convenction ******************************************)
302 let rec add_entries map c = function
305 let sname, w = map hd in
306 let entry = Some (Cic.Name sname, C.Decl w) in
307 add_entries map (entry :: c) tl
310 try match List.nth c (pred i) with
311 | Some (Cic.Name sname, _) -> sname
314 | Failure _ -> assert false
315 | Invalid_argument _ -> assert false
318 let get_fix_decl (sname, i, w, v) = sname, w in
319 let get_cofix_decl (sname, w, v) = sname, w in
320 let rec bc c = function
321 | C.LetIn (name, v, ty, t) ->
322 let name = mk_fresh_name c name in
323 let entry = Some (name, C.Def (v, ty)) in
324 let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
325 C.LetIn (name, v, ty, t)
326 | C.Lambda (name, w, t) ->
327 let name = mk_fresh_name c name in
328 let entry = Some (name, C.Decl w) in
329 let w, t = bc c w, bc (entry :: c) t in
330 C.Lambda (name, w, t)
331 | C.Prod (name, w, t) ->
332 let name = mk_fresh_name c name in
333 let entry = Some (name, C.Decl w) in
334 let w, t = bc c w, bc (entry :: c) t in
337 let vs = List.map (bc c) vs in
339 | C.MutCase (uri, tyno, u, v, ts) ->
340 let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
341 C.MutCase (uri, tyno, u, v, ts)
343 let t, u = bc c t, bc c u in
345 | C.Fix (i, fixes) ->
346 let d = add_entries get_fix_decl c fixes in
347 let bc_fix (sname, i, w, v) = (sname, i, bc c w, bc d v) in
348 let fixes = List.map bc_fix fixes in
350 | C.CoFix (i, cofixes) ->
351 let d = add_entries get_cofix_decl c cofixes in
352 let bc_cofix (sname, w, v) = (sname, bc c w, bc d v) in
353 let cofixes = List.map bc_cofix cofixes in
360 let get_fix_decl (id, sname, i, w, v) = sname, cic w in
361 let get_cofix_decl (id, sname, w, v) = sname, cic w in
362 let rec bc c = function
363 | C.ALetIn (id, name, v, ty, t) ->
364 let name = mk_fresh_name c name in
365 let entry = Some (name, C.Def (cic v, cic ty)) in
366 let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
367 C.ALetIn (id, name, v, ty, t)
368 | C.ALambda (id, name, w, t) ->
369 let name = mk_fresh_name c name in
370 let entry = Some (name, C.Decl (cic w)) in
371 let w, t = bc c w, bc (entry :: c) t in
372 C.ALambda (id, name, w, t)
373 | C.AProd (id, name, w, t) ->
374 let name = mk_fresh_name c name in
375 let entry = Some (name, C.Decl (cic w)) in
376 let w, t = bc c w, bc (entry :: c) t in
377 C.AProd (id, name, w, t)
378 | C.AAppl (id, vs) ->
379 let vs = List.map (bc c) vs in
381 | C.AMutCase (id, uri, tyno, u, v, ts) ->
382 let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
383 C.AMutCase (id, uri, tyno, u, v, ts)
384 | C.ACast (id, t, u) ->
385 let t, u = bc c t, bc c u in
387 | C.AFix (id, i, fixes) ->
388 let d = add_entries get_fix_decl c fixes in
389 let bc_fix (id, sname, i, w, v) = (id, sname, i, bc c w, bc d v) in
390 let fixes = List.map bc_fix fixes in
391 C.AFix (id, i, fixes)
392 | C.ACoFix (id, i, cofixes) ->
393 let d = add_entries get_cofix_decl c cofixes in
394 let bc_cofix (id, sname, w, v) = (id, sname, bc c w, bc d v) in
395 let cofixes = List.map bc_cofix cofixes in
396 C.ACoFix (id, i, cofixes)
397 | C.ARel (id1, id2, i, sname) ->
398 let sname = get_sname c i in
399 C.ARel (id1, id2, i, sname)