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 du: UM.uri -> UM.uri; (* uri discharge map *)
74 c : C.context; (* var context of this object *)
75 ls: (UM.uri, UM.uri list) Hashtbl.t; (* var lists of subobjects *)
76 rl: UM.uri list; (* reverse var list of this object *)
77 h : int (* relocation index *)
80 let add st k = {st with h = st.h + k}
82 let discharge st u = st.h + list_pos (UM.eq u) st.rl
85 try Hashtbl.find st.ls u
87 let args = vars_of_uri u in
88 Hashtbl.add st.ls u args; args
90 let rec discharge_term st t = match t with
95 let args = get_args st u in
96 if args = [] then t else
97 let s = List.map (mk_arg s) args in
98 C.Appl (C.Const (st.du u, []) :: discharge_nsubst st s)
99 | C.MutInd (u, m, s) ->
100 let args = get_args st u in
101 if args = [] then t else
102 let s = List.map (mk_arg s) args in
103 C.Appl (C.MutInd (st.du u, m, []) :: discharge_nsubst st s)
104 | C.MutConstruct (u, m, n, s) ->
105 let args = get_args st u in
106 if args = [] then t else
107 let s = List.map (mk_arg s) args in
108 C.Appl (C.MutConstruct (st.du u, m, n, []) :: discharge_nsubst st s)
110 let args = get_args st u in
111 if args = [] then C.Rel (discharge st u) else
112 let s = List.map (mk_arg s) args in
113 C.Appl (C.Rel (discharge st u) :: discharge_nsubst st s)
115 let s' = list_map_sh (discharge_usubst st) s in
116 if s' == s then t else C.Meta (i, s')
118 let vs' = list_map_sh (discharge_term st) vs in
119 if vs' == vs then t else C.Appl (flatten vs')
121 let v', w' = discharge_term st v, discharge_term st w in
122 if v' = v && w' = w then t else
123 C.Cast (sh v v', sh w w')
124 | C.MutCase (u, m, w, v, vs) ->
126 discharge_term st w, discharge_term st v,
127 list_map_sh (discharge_term st) vs
129 if w' = w && v' = v && vs' == vs then t else
130 C.MutCase (st.du u, m, sh w w', sh v v', sh vs vs')
131 | C.Prod (b, w, v) ->
132 let w', v' = discharge_term st w, discharge_term (add st 1) v in
133 if w' = w && v' = v then t else
134 C.Prod (b, sh w w', sh v v')
135 | C.Lambda (b, w, v) ->
136 let w', v' = discharge_term st w, discharge_term (add st 1) v in
137 if w' = w && v' = v then t else
138 C.Lambda (b, sh w w', sh v v')
139 | C.LetIn (b, y, w, v) ->
141 discharge_term st y, discharge_term st w, discharge_term (add st 1) v
143 if y' = y && w' = w && v' == v then t else
144 C.LetIn (b, sh y y', sh w w', sh v v')
146 let no = List.length s in
147 let s' = list_map_sh (discharge_cofun st no) s in
148 if s' == s then t else C.CoFix (i, s')
150 let no = List.length s in
151 let s' = list_map_sh (discharge_fun st no) s in
152 if s' == s then t else C.Fix (i, s')
154 and discharge_nsubst st s =
155 List.map (discharge_term st) s
157 and discharge_usubst st s = match s with
160 let t' = discharge_term st t in
161 if t' == t then s else Some t'
163 and discharge_cofun st no f =
165 let w', v' = discharge_term st w, discharge_term (add st no) v in
166 if w' = w && v' = v then f else
169 and discharge_fun st no f =
170 let b, i, w, v = f in
171 let w', v' = discharge_term st w, discharge_term (add st no) v in
172 if w' = w && v' = v then f else
173 b, i, sh w w', sh v v'
175 let close is_type st t =
177 | Some (b, C.Def (v, w)) -> C.LetIn (b, v, w, t)
178 | Some (b, C.Decl w) ->
179 if is_type then C.Prod (b, w, t) else C.Lambda (b, w, t)
180 | None -> assert false
182 List.fold_left map t st.c
184 let discharge_con st con =
186 let v' = discharge_term st v in
187 if v' == v && st.rl = [] then con else b, close true st (sh v v')
189 let discharge_type st ind_type =
190 let b, ind, w, cons = ind_type in
191 let w', cons' = discharge_term st w, list_map_sh (discharge_con st) cons in
192 if w' == w && cons' == cons && st.rl = [] then ind_type else
193 let w'' = close true st (sh w w') in
194 b, ind, w'', sh cons cons'
196 let rec discharge_object du obj =
197 let ls = Hashtbl.create hashtbl_size in match obj with
198 | C.Variable (b, None, w, vars, attrs) ->
199 let st = init_status du ls vars in
200 let w' = discharge_term st w in
201 if w' = w && vars = [] then obj else
202 let w'' = close true st (sh w w') in
203 C.Variable (b, None, w'', [], attrs)
204 | C.Variable (b, Some v, w, vars, attrs) ->
205 let st = init_status du ls vars in
206 let w', v' = discharge_term st w, discharge_term st v in
207 if w' = w && v' = v && vars = [] then obj else
208 let w'', v'' = close true st (sh w w'), close false st (sh v v') in
209 C.Variable (b, Some v'', w'', [], attrs)
210 | C.Constant (b, None, w, vars, attrs) ->
211 let st = init_status du ls vars in
212 let w' = discharge_term st w in
213 if w' = w && vars = [] then obj else
214 let w'' = close true st (sh w w') in
215 C.Constant (b, None, w'', [], attrs)
216 | C.Constant (b, Some v, w, vars, attrs) ->
217 let st = init_status du ls vars in
218 let w', v' = discharge_term st w, discharge_term st v in
219 if w' = w && v' = v && vars = [] then obj else
220 let w'', v'' = close true st (sh w w'), close false st (sh v v') in
221 C.Constant (b, Some v'', w'', [], attrs)
222 | C.InductiveDefinition (types, vars, lpsno, attrs) ->
223 let st = init_status du ls vars in
224 let types' = list_map_sh (discharge_type st) types in
225 if types' == types && vars = [] then obj else
226 let lpsno' = lpsno + List.length vars in
227 C.InductiveDefinition (sh types types', [], lpsno', attrs)
228 | C.CurrentProof _ ->
229 HLog.warn not_implemented; obj
231 and discharge_uri du uri =
232 let obj, _ = E.get_obj Un.default_ugraph uri in
233 let obj' = discharge_object du obj in
236 and discharge_vars du vars =
238 match discharge_uri du u with
239 | C.Variable (b, None, w, _, _), _ -> Some (C.Name b, C.Decl w)
240 | C.Variable (b, Some v, w, _, _), _ -> Some (C.Name b, C.Def (v, w))
243 List.rev_map map vars
245 and init_status du ls vars =
246 let c, rl = discharge_vars du vars, List.rev vars in
247 {du = du; c = c; ls = ls; rl = rl; h = 1}