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
34 "discharge of current proofs is not implemented yet"
36 (* helper functions *********************************************************)
38 let list_pos found l =
39 let rec aux n = function
40 | [] -> raise Not_found
41 | hd :: tl -> if found hd then n else aux (succ n) tl
45 let sh a b = if a == b then a else b
47 let rec list_map_sh map l = match l with
50 let hd', tl' = map hd, list_map_sh map tl in
51 if hd' == hd && tl' == tl then l else
52 sh hd hd' :: sh tl tl'
54 let flatten = function
55 | C.Appl vs :: tl -> vs @ tl
59 let obj, _ = E.get_obj Un.default_ugraph uri in
61 | C.Constant (_, _, _, vars, _)
62 | C.Variable (_, _, _, vars, _)
63 | C.InductiveDefinition (_, vars, _, _)
64 | C.CurrentProof (_, _, _, _, vars, _) -> vars
68 with Not_found -> C.Var (u, [])
70 (* main functions ***********************************************************)
73 dn: string -> string; (* name discharge map *)
74 du: UM.uri -> UM.uri; (* uri discharge map *)
75 c : C.context; (* var context of this object *)
76 ls: (UM.uri, UM.uri list) Hashtbl.t; (* var lists of subobjects *)
77 rl: UM.uri list; (* reverse var list of this object *)
78 h : int (* relocation index *)
81 let add st k = {st with h = st.h + k}
83 let discharge st u = st.h + list_pos (UM.eq u) st.rl
86 try Hashtbl.find st.ls u
88 let args = vars_of_uri u in
89 Hashtbl.add st.ls u args; args
91 let rec discharge_term st t = match t with
96 let args = get_args st u in
97 if args = [] then t else
98 let s = List.map (mk_arg s) args in
99 C.Appl (C.Const (st.du u, []) :: discharge_nsubst st s)
100 | C.MutInd (u, m, s) ->
101 let args = get_args st u in
102 if args = [] then t else
103 let s = List.map (mk_arg s) args in
104 C.Appl (C.MutInd (st.du u, m, []) :: discharge_nsubst st s)
105 | C.MutConstruct (u, m, n, s) ->
106 let args = get_args st u in
107 if args = [] then t else
108 let s = List.map (mk_arg s) args in
109 C.Appl (C.MutConstruct (st.du u, m, n, []) :: discharge_nsubst st s)
111 (* FG: We do not discharge the nsubst here ?? *)
112 let args = get_args st u in
113 if args = [] then C.Rel (discharge st u) else
114 let s = List.map (mk_arg s) args in
115 (* C.Appl ( *) C.Rel (discharge st u) (* :: discharge_nsubst st s) *)
117 let s' = list_map_sh (discharge_usubst st) s in
118 if s' == s then t else C.Meta (i, s')
120 let vs' = list_map_sh (discharge_term st) vs in
121 if vs' == vs then t else C.Appl (flatten vs')
123 let v', w' = discharge_term st v, discharge_term st w in
124 if v' = v && w' = w then t else
125 C.Cast (sh v v', sh w w')
126 | C.MutCase (u, m, w, v, vs) ->
128 discharge_term st w, discharge_term st v,
129 list_map_sh (discharge_term st) vs
131 if w' = w && v' = v && vs' == vs then t else
132 C.MutCase (st.du u, m, sh w w', sh v v', sh vs vs')
133 | C.Prod (b, w, v) ->
134 let w', v' = discharge_term st w, discharge_term (add st 1) v in
135 if w' = w && v' = v then t else
136 C.Prod (b, sh w w', sh v v')
137 | C.Lambda (b, w, v) ->
138 let w', v' = discharge_term st w, discharge_term (add st 1) v in
139 if w' = w && v' = v then t else
140 C.Lambda (b, sh w w', sh v v')
141 | C.LetIn (b, y, w, v) ->
143 discharge_term st y, discharge_term st w, discharge_term (add st 1) v
145 if y' = y && w' = w && v' == v then t else
146 C.LetIn (b, sh y y', sh w w', sh v v')
148 let no = List.length s in
149 let s' = list_map_sh (discharge_cofun st no) s in
150 if s' == s then t else C.CoFix (i, s')
152 let no = List.length s in
153 let s' = list_map_sh (discharge_fun st no) s in
154 if s' == s then t else C.Fix (i, s')
156 and discharge_nsubst st s =
157 List.map (discharge_term st) s
159 and discharge_usubst st s = match s with
162 let t' = discharge_term st t in
163 if t' == t then s else Some t'
165 and discharge_cofun st no f =
167 let w', v' = discharge_term st w, discharge_term (add st no) v in
168 if w' = w && v' = v then f else
171 and discharge_fun st no f =
172 let b, i, w, v = f in
173 let w', v' = discharge_term st w, discharge_term (add st no) v in
174 if w' = w && v' = v then f else
175 b, i, sh w w', sh v v'
177 let close is_type st t =
179 | Some (b, C.Def (v, w)) -> C.LetIn (b, v, w, t)
180 | Some (b, C.Decl w) ->
181 if is_type then C.Prod (b, w, t) else C.Lambda (b, w, t)
182 | None -> assert false
184 List.fold_left map t st.c
186 let discharge_con st con =
188 let v' = discharge_term st v in
189 if v' == v && st.rl = [] then con else st.dn b, close true st (sh v v')
191 let discharge_type st ind_type =
192 let b, ind, w, cons = ind_type in
193 let w', cons' = discharge_term st w, list_map_sh (discharge_con st) cons in
194 if w' == w && cons' == cons && st.rl = [] then ind_type else
195 let w'' = close true st (sh w w') in
196 st.dn b, ind, w'', sh cons cons'
198 let rec discharge_object dn du obj =
199 let ls = Hashtbl.create hashtbl_size in match obj with
200 | C.Variable (b, None, w, vars, attrs) ->
201 let st = init_status dn du ls vars in
202 let w' = discharge_term st w in
203 if w' = w && vars = [] then obj else
205 C.Variable (dn b, None, w'', [], attrs)
206 | C.Variable (b, Some v, w, vars, attrs) ->
207 let st = init_status dn du ls vars in
208 let w', v' = discharge_term st w, discharge_term st v in
209 if w' = w && v' = v && vars = [] then obj else
210 let w'', v'' = sh w w', sh v v' in
211 C.Variable (dn b, Some v'', w'', [], attrs)
212 | C.Constant (b, None, w, vars, attrs) ->
213 let st = init_status dn du ls vars in
214 let w' = discharge_term st w in
215 if w' = w && vars = [] then obj else
216 let w'' = close true st (sh w w') in
217 C.Constant (dn b, None, w'', [], attrs)
218 | C.Constant (b, Some v, w, vars, attrs) ->
219 let st = init_status dn du ls vars in
220 let w', v' = discharge_term st w, discharge_term st v in
221 if w' = w && v' = v && vars = [] then obj else
222 let w'', v'' = close true st (sh w w'), close false st (sh v v') in
223 C.Constant (dn b, Some v'', w'', [], attrs)
224 | C.InductiveDefinition (types, vars, lpsno, attrs) ->
225 let st = init_status dn du ls vars in
226 let types' = list_map_sh (discharge_type st) types in
227 if types' == types && vars = [] then obj else
228 let lpsno' = lpsno + List.length vars in
229 C.InductiveDefinition (sh types types', [], lpsno', attrs)
230 | C.CurrentProof _ ->
231 HLog.warn not_implemented; obj
233 and discharge_uri dn du uri =
234 let obj, _ = E.get_obj Un.default_ugraph uri in
235 prerr_endline ("Plain : " ^ CicPp.ppobj obj);
236 let obj' = discharge_object dn du obj in
237 prerr_endline ("Discharged: " ^ CicPp.ppobj obj');
240 and discharge_vars dn du vars =
241 (* We should check that the dependences are ordered telesopically *)
243 match discharge_uri dn du u with
244 | C.Variable (b, None, w, _, _), _ -> Some (C.Name b, C.Decl w)
245 | C.Variable (b, Some v, w, _, _), _ -> Some (C.Name b, C.Def (v, w))
248 List.rev_map map vars
250 and init_status dn du ls vars =
251 let c, rl = discharge_vars dn du vars, List.rev vars in
252 {dn = dn; du = du; c = c; ls = ls; rl = rl; h = 1}