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
36 "discharge of current proofs is not implemented yet"
40 let out = prerr_string
42 (* helper functions *********************************************************)
46 let _ = TC.type_of_aux' [] [] t Un.default_ugraph in
47 out "Typecheck : OK\n"
50 let list_pos found l =
51 let rec aux n = function
52 | [] -> raise Not_found
53 | hd :: tl -> if found hd then n else aux (succ n) tl
57 let sh a b = if a == b then a else b
59 let rec list_map_sh map l = match l with
62 let hd', tl' = map hd, list_map_sh map tl in
63 if hd' == hd && tl' == tl then l else
64 sh hd hd' :: sh tl tl'
66 let flatten = function
67 | C.Appl vs :: tl -> vs @ tl
71 let obj, _ = E.get_obj Un.default_ugraph uri in
73 | C.Constant (_, _, _, vars, _)
74 | C.Variable (_, _, _, vars, _)
75 | C.InductiveDefinition (_, vars, _, _)
76 | C.CurrentProof (_, _, _, _, vars, _) -> vars
80 with Not_found -> C.Var (u, [])
82 (* main functions ***********************************************************)
85 dn: string -> string; (* name discharge map *)
86 du: UM.uri -> UM.uri; (* uri discharge map *)
87 c : C.context; (* var context of this object *)
88 ls: (UM.uri, UM.uri list) Hashtbl.t; (* var lists of subobjects *)
89 rl: UM.uri list; (* reverse var list of this object *)
90 h : int (* relocation index *)
93 let add st k = {st with h = st.h + k}
95 let discharge st u = st.h + list_pos (UM.eq u) st.rl
98 try Hashtbl.find st.ls u
100 let args = vars_of_uri u in
101 Hashtbl.add st.ls u args; args
103 let rec discharge_term st t = match t with
108 let args = get_args st u in
109 if args = [] then t else
110 let s = List.map (mk_arg s) args in
111 C.Appl (C.Const (st.du u, []) :: discharge_nsubst st s)
112 | C.MutInd (u, m, s) ->
113 let args = get_args st u in
114 if args = [] then t else
115 let s = List.map (mk_arg s) args in
116 C.Appl (C.MutInd (st.du u, m, []) :: discharge_nsubst st s)
117 | C.MutConstruct (u, m, n, s) ->
118 let args = get_args st u in
119 if args = [] then t else
120 let s = List.map (mk_arg s) args in
121 C.Appl (C.MutConstruct (st.du u, m, n, []) :: discharge_nsubst st s)
123 (* We do not discharge the nsubst because variables are not closed *)
124 (* thus only the identity nsubst should be allowed *)
125 if s <> [] then assert false else
126 C.Rel (discharge st u)
128 let s' = list_map_sh (discharge_usubst st) s in
129 if s' == s then t else C.Meta (i, s')
131 let vs' = list_map_sh (discharge_term st) vs in
132 if vs' == vs then t else C.Appl (flatten vs')
134 let v', w' = discharge_term st v, discharge_term st w in
135 if v' == v && w' == w then t else
136 C.Cast (sh v v', sh w w')
137 | C.MutCase (u, m, w, v, vs) ->
138 let args = get_args st u in
139 let u' = if args = [] then u else st.du u in
141 discharge_term st w, discharge_term st v,
142 list_map_sh (discharge_term st) vs
144 if UM.eq u u' && w' == w && v' == v && vs' == vs then t else
145 C.MutCase (u', m, sh w w', sh v v', sh vs vs')
146 | C.Prod (b, w, v) ->
147 let w', v' = discharge_term st w, discharge_term (add st 1) v in
148 if w' == w && v' == v then t else
149 C.Prod (b, sh w w', sh v v')
150 | C.Lambda (b, w, v) ->
151 let w', v' = discharge_term st w, discharge_term (add st 1) v in
152 if w' == w && v' == v then t else
153 C.Lambda (b, sh w w', sh v v')
154 | C.LetIn (b, y, w, v) ->
156 discharge_term st y, discharge_term st w, discharge_term (add st 1) v
158 if y' == y && w' == w && v' == v then t else
159 C.LetIn (b, sh y y', sh w w', sh v v')
161 let no = List.length s in
162 let s' = list_map_sh (discharge_cofun st no) s in
163 if s' == s then t else C.CoFix (i, s')
165 let no = List.length s in
166 let s' = list_map_sh (discharge_fun st no) s in
167 if s' == s then t else C.Fix (i, s')
169 and discharge_nsubst st s =
170 List.map (discharge_term st) s
172 and discharge_usubst st s = match s with
175 let t' = discharge_term st t in
176 if t' == t then s else Some t'
178 and discharge_cofun st no f =
180 let w', v' = discharge_term st w, discharge_term (add st no) v in
181 if w' == w && v' == v then f else
184 and discharge_fun st no f =
185 let b, i, w, v = f in
186 let w', v' = discharge_term st w, discharge_term (add st no) v in
187 if w' == w && v' == v then f else
188 b, i, sh w w', sh v v'
190 let close is_type st t =
192 | Some (b, C.Def (v, w)) -> C.LetIn (b, v, w, t)
193 | Some (b, C.Decl w) ->
194 if is_type then C.Prod (b, w, t) else C.Lambda (b, w, t)
195 | None -> assert false
197 List.fold_left map t st.c
199 let discharge_con st con =
201 let v' = discharge_term st v in
202 if v' == v && st.rl = [] then con else st.dn b, close true st (sh v v')
204 let discharge_type st ind_type =
205 let b, ind, w, cons = ind_type in
206 let w', cons' = discharge_term st w, list_map_sh (discharge_con st) cons in
207 if w' == w && cons' == cons && st.rl = [] then ind_type else
208 let w'' = close true st (sh w w') in
209 st.dn b, ind, w'', sh cons cons'
211 let rec discharge_object dn du obj =
212 let ls = Hashtbl.create hashtbl_size in match obj with
213 | C.Variable (b, None, w, vars, attrs) ->
214 let st = init_status dn du ls vars in
215 let w' = discharge_term st w in
216 if w' == w && vars = [] then obj else
218 let _ = typecheck w'' in
219 C.Variable (dn b, None, w'', [], attrs)
220 | C.Variable (b, Some v, w, vars, attrs) ->
221 let st = init_status dn du ls vars in
222 let w', v' = discharge_term st w, discharge_term st v in
223 if w' == w && v' == v && vars = [] then obj else
224 let w'', v'' = sh w w', sh v v' in
225 let _ = typecheck (C.Cast (v'', w'')) in
226 C.Variable (dn b, Some v'', w'', [], attrs)
227 | C.Constant (b, None, w, vars, attrs) ->
228 let st = init_status dn du ls vars in
229 let w' = discharge_term st w in
230 if w' == w && vars = [] then obj else
231 let w'' = close true st (sh w w') in
232 let _ = typecheck w'' in
233 C.Constant (dn b, None, w'', [], attrs)
234 | C.Constant (b, Some v, w, vars, attrs) ->
235 let st = init_status dn du ls vars in
236 let w', v' = discharge_term st w, discharge_term st v in
237 if w' == w && v' == v && vars = [] then obj else
238 let w'', v'' = close true st (sh w w'), close false st (sh v v') in
239 let _ = typecheck (C.Cast (v'', w'')) in
240 C.Constant (dn b, Some v'', w'', [], attrs)
241 | C.InductiveDefinition (types, vars, lpsno, attrs) ->
242 let st = init_status dn du ls vars in
243 let types' = list_map_sh (discharge_type st) types in
244 if types' == types && vars = [] then obj else
245 let lpsno' = lpsno + List.length vars in
246 C.InductiveDefinition (sh types types', [], lpsno', attrs)
247 | C.CurrentProof _ ->
248 HLog.warn not_implemented; obj
250 and discharge_uri dn du uri =
253 out msg; Ut.pp_obj out obj; out "\n"
256 let obj, _ = E.get_obj Un.default_ugraph uri in
257 prerr "Plain : " obj;
258 let obj' = discharge_object dn du obj in
259 prerr "Discharged: " obj';
262 and discharge_vars dn du vars =
263 (* We should check that the dependences are ordered telesopically *)
265 match discharge_uri dn du u with
266 | C.Variable (b, None, w, _, _), _ -> Some (C.Name b, C.Decl w)
267 | C.Variable (b, Some v, w, _, _), _ -> Some (C.Name b, C.Def (v, w))
270 List.rev_map map vars
272 and init_status dn du ls vars =
273 let c, rl = discharge_vars dn du vars, List.rev vars in
274 {dn = dn; du = du; c = c; ls = ls; rl = rl; h = 1}