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/.
26 module UM = UriManager
29 module E = CicEnvironment
31 module TC = CicTypeChecker
32 module S = CicSubstitution
38 "discharge of current proofs is not implemented yet"
42 let out = prerr_string
44 (* helper functions *********************************************************)
46 let rec count_prods n = function
47 | C.Prod (_, _, t) -> count_prods (succ n) t
50 let get_ind_type_psnos uri tyno =
51 match E.get_obj Un.default_ugraph uri with
52 | C.InductiveDefinition (tys, _, lpsno, _), _ ->
53 let _, _, ty, _ = List.nth tys tyno in
54 lpsno, count_prods 0 ty
59 out (Printf.sprintf "Pre Check ; %s\n" b);
60 Ut.pp_term out [] [] t; out "\n";
61 let _ = TC.type_of_aux' [] [] t Un.default_ugraph in
62 out (Printf.sprintf "Typecheck : %s OK\n" b)
65 let list_pos found l =
66 let rec aux n = function
67 | [] -> raise Not_found
68 | hd :: tl -> if found hd then n else aux (succ n) tl
72 let sh a b = if a == b then a else b
74 let rec list_map_sh map l = match l with
77 let hd', tl' = map hd, list_map_sh map tl in
78 if hd' == hd && tl' == tl then l else
79 sh hd hd' :: sh tl tl'
81 let flatten = function
82 | C.Appl vs :: tl -> vs @ tl
86 let obj, _ = E.get_obj Un.default_ugraph uri in
88 | C.Constant (_, _, _, vars, _)
89 | C.Variable (_, _, _, vars, _)
90 | C.InductiveDefinition (_, vars, _, _)
91 | C.CurrentProof (_, _, _, _, vars, _) -> vars
95 with Not_found -> C.Var (u, [])
97 (* main functions ***********************************************************)
100 dn: string -> string; (* name discharge map *)
101 du: UM.uri -> UM.uri; (* uri discharge map *)
102 ls: (UM.uri, UM.uri list) Hashtbl.t; (* var lists of subobjects *)
103 rl: UM.uri list; (* reverse var list of this object *)
104 h : int; (* relocation index *)
105 c : C.context (* local context of this object *)
108 let add st k es = {st with h = st.h + k; c = List.rev_append es st.c}
110 let discharge st u = st.h + list_pos (UM.eq u) st.rl
113 try Hashtbl.find st.ls u
115 let args = vars_of_uri u in
116 Hashtbl.add st.ls u args; args
118 let proj_fix (s, _, w, _) = s, w
120 let proj_cofix (s, w, _) = s, w
122 let mk_context proj discharge_term s =
125 let w' = discharge_term w in
126 Some (C.Name s, C.Decl w')
128 List.length s, List.rev_map map s
130 let rec split_absts named no c = function
131 | C.Lambda (s, w, t) ->
132 let e = Some (s, C.Decl w) in
133 let named = named && s <> C.Anonymous in
134 split_absts named (succ no) (e :: c) t
138 let close is_type c t =
140 | Some (b, C.Def (v, w)) -> C.LetIn (b, v, w, t)
141 | Some (b, C.Decl w) ->
142 if is_type then C.Prod (b, w, t) else C.Lambda (b, w, t)
143 | None -> assert false
145 List.fold_left map t c
147 let relocate to_what from_what k m =
149 let u = List.nth from_what (m - k) in
150 let map v m = if UM.eq u v then Some m else None in
151 match X.list_findopt map to_what with
153 | None -> raise (Failure "nth")
155 | Failure "nth" -> assert false
157 let rec discharge_term st t = match t with
162 let args = get_args st u in
163 if args = [] then t else
164 let s = List.map (mk_arg s) args in
165 C.Appl (C.Const (st.du u, []) :: discharge_nsubst st s)
166 | C.MutInd (u, m, s) ->
167 let args = get_args st u in
168 if args = [] then t else
169 let s = List.map (mk_arg s) args in
170 C.Appl (C.MutInd (st.du u, m, []) :: discharge_nsubst st s)
171 | C.MutConstruct (u, m, n, s) ->
172 let args = get_args st u in
173 if args = [] then t else
174 let s = List.map (mk_arg s) args in
175 C.Appl (C.MutConstruct (st.du u, m, n, []) :: discharge_nsubst st s)
177 (* We do not discharge the nsubst because variables are not closed *)
178 (* thus only the identity nsubst should be allowed *)
179 if s <> [] then assert false else
180 C.Rel (discharge st u)
182 let s' = list_map_sh (discharge_usubst st) s in
183 if s' == s then t else C.Meta (i, s')
185 let vs' = list_map_sh (discharge_term st) vs in
186 if vs' == vs then t else C.Appl (flatten vs')
188 let v', w' = discharge_term st v, discharge_term st w in
189 if v' == v && w' == w then t else
190 C.Cast (sh v v', sh w w')
191 | C.MutCase (u, m, w, v, vs) ->
192 let args = get_args st u in
193 let u' = if args = [] then u else st.du u in
195 discharge_term st w, discharge_term st v,
196 list_map_sh (discharge_term st) vs
198 (* BEGIN FIX OUT TYPE *)
199 let lpsno, psno = get_ind_type_psnos u m in
200 let rpsno = psno - lpsno in
201 let named, frpsno, wc, wb = split_absts true 0 [] w' in
203 (* No fixing needed *)
204 if frpsno = succ rpsno then w' else
205 (* Fixing needed, no right parametes *)
206 if frpsno = rpsno && rpsno = 0 then
207 let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in
209 out "VTY: "; Ut.pp_term out [] st.c vty; out "\n"
211 C.Lambda (C.Anonymous, vty, S.lift 1 wb)
213 (* Fixing needed, some right parametes *)
214 if frpsno = rpsno then
215 let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in
217 out "VTY: "; Ut.pp_term out [] st.c vty; out "\n"
219 let vty, wb = S.lift rpsno vty, S.lift (succ rpsno) wb in
220 close false wc (C.Lambda (C.Anonymous, vty, wb))
221 (* This case should not happen *)
224 (* END FIX OUT TYPE *)
225 if UM.eq u u' && w' == w && v' == v && vs' == vs then t else
226 C.MutCase (u', m, sh w w', sh v v', sh vs vs')
227 | C.Prod (b, w, v) ->
228 let w' = discharge_term st w in
229 let es = [Some (b, C.Decl w')] in
230 let v' = discharge_term (add st 1 es) v in
231 if w' == w && v' == v then t else
232 C.Prod (b, sh w w', sh v v')
233 | C.Lambda (b, w, v) ->
234 let w' = discharge_term st w in
235 let es = [Some (b, C.Decl w')] in
236 let v' = discharge_term (add st 1 es) v in
237 if w' == w && v' == v then t else
238 C.Lambda (b, sh w w', sh v v')
239 | C.LetIn (b, y, w, v) ->
240 let y', w' = discharge_term st y, discharge_term st w in
241 let es = [Some (b, C.Def (y, w'))] in
242 let v' = discharge_term (add st 1 es) v in
243 if y' == y && w' == w && v' == v then t else
244 C.LetIn (b, sh y y', sh w w', sh v v')
246 let no, es = mk_context proj_cofix (discharge_term st) s in
247 let s' = list_map_sh (discharge_cofun st no es) s in
248 if s' == s then t else C.CoFix (i, s')
250 let no, es = mk_context proj_fix (discharge_term st) s in
251 let s' = list_map_sh (discharge_fun st no es) s in
252 if s' == s then t else C.Fix (i, s')
254 and discharge_nsubst st s =
255 List.map (discharge_term st) s
257 and discharge_usubst st s = match s with
260 let t' = discharge_term st t in
261 if t' == t then s else Some t'
263 and discharge_cofun st no es f =
265 let w', v' = discharge_term st w, discharge_term (add st no es) v in
266 if w' == w && v' == v then f else
269 and discharge_fun st no es f =
270 let b, i, w, v = f in
271 let w', v' = discharge_term st w, discharge_term (add st no es) v in
272 if w' == w && v' == v then f else
273 b, i, sh w w', sh v v'
275 let close is_type st = close is_type st.c
277 let discharge_con st con =
279 let v' = discharge_term st v in
280 if v' == v && st.rl = [] then con else st.dn b, close true st (sh v v')
282 let discharge_type st ind_type =
283 let b, ind, w, cons = ind_type in
284 let w', cons' = discharge_term st w, list_map_sh (discharge_con st) cons in
285 if w' == w && cons' == cons && st.rl = [] then ind_type else
286 let w'' = close true st (sh w w') in
287 st.dn b, ind, w'', sh cons cons'
289 let rec discharge_object dn du obj =
290 let ls = Hashtbl.create hashtbl_size in match obj with
291 | C.Variable (b, None, w, vars, attrs) ->
292 let st = init_status dn du ls vars in
293 let w' = discharge_term st w in
294 if w' == w && vars = [] then obj else
296 (* We do not typecheck because variables are not closed *)
297 C.Variable (dn b, None, w'', [], attrs)
298 | C.Variable (b, Some v, w, vars, attrs) ->
299 let st = init_status dn du ls vars in
300 let w', v' = discharge_term st w, discharge_term st v in
301 if w' == w && v' == v && vars = [] then obj else
302 let w'', v'' = sh w w', sh v v' in
303 (* We do not typecheck because variables are not closed *)
304 C.Variable (dn b, Some v'', w'', [], attrs)
305 | C.Constant (b, None, w, vars, attrs) ->
306 let st = init_status dn du ls vars in
307 let w' = discharge_term st w in
308 if w' == w && vars = [] then obj else
309 let w'' = close true st (sh w w') in
310 let _ = typecheck (dn b) w'' in
311 C.Constant (dn b, None, w'', [], attrs)
312 | C.Constant (b, Some v, w, vars, attrs) ->
313 let st = init_status dn du ls vars in
314 let w', v' = discharge_term st w, discharge_term st v in
315 if w' == w && v' == v && vars = [] then obj else
316 let w'', v'' = close true st (sh w w'), close false st (sh v v') in
317 let _ = typecheck (dn b) (C.Cast (v'', w'')) in
318 C.Constant (dn b, Some v'', w'', [], attrs)
319 | C.InductiveDefinition (types, vars, lpsno, attrs) ->
320 let st = init_status dn du ls vars in
321 let types' = list_map_sh (discharge_type st) types in
322 if types' == types && vars = [] then obj else
323 let lpsno' = lpsno + List.length vars in
324 C.InductiveDefinition (sh types types', [], lpsno', attrs)
325 | C.CurrentProof _ ->
326 HLog.warn not_implemented; obj
328 and discharge_uri dn du uri =
331 out msg; Ut.pp_obj out obj; out "\n"
334 let obj, _ = E.get_obj Un.default_ugraph uri in
335 prerr "Plain : " obj;
336 let obj' = discharge_object dn du obj in
337 prerr "Discharged: " obj';
340 and discharge_vars dn du vars =
341 (* We should check that the dependences are ordered telesopically *)
343 match discharge_uri dn du u with
344 | C.Variable (b, None, w, _, _), _ -> Some (C.Name b, C.Decl w)
345 | C.Variable (b, Some v, w, _, _), _ -> Some (C.Name b, C.Def (v, w))
348 List.rev_map map vars
350 and init_status dn du ls vars =
351 let c, rl = discharge_vars dn du vars, List.rev vars in
352 {dn = dn; du = du; ls = ls; rl = rl; h = 1; c = c}