+(* Copyright (C) 2003-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module UM = UriManager
+module C = Cic
+module Un = CicUniv
+module E = CicEnvironment
+
+let hashtbl_size = 11
+
+let not_implemented =
+ "discharge of current proofs is not implemented yet"
+
+(* helper functions *********************************************************)
+
+let list_pos found l =
+ let rec aux n = function
+ | [] -> raise Not_found
+ | hd :: tl -> if found hd then n else aux (succ n) tl
+ in
+ aux 0 l
+
+let sh a b = if a == b then a else b
+
+let rec list_map_sh map l = match l with
+ | [] -> l
+ | hd :: tl ->
+ let hd', tl' = map hd, list_map_sh map tl in
+ if hd' == hd && tl' == tl then l else
+ sh hd hd' :: sh tl tl'
+
+let flatten = function
+ | C.Appl vs :: tl -> vs @ tl
+ | ts -> ts
+
+let vars_of_uri uri =
+ let obj, _ = E.get_obj Un.default_ugraph uri in
+ match obj with
+ | C.Constant (_, _, _, vars, _)
+ | C.Variable (_, _, _, vars, _)
+ | C.InductiveDefinition (_, vars, _, _)
+ | C.CurrentProof (_, _, _, _, vars, _) -> vars
+
+let mk_arg s u =
+ try List.assq u s
+ with Not_found -> C.Var (u, [])
+
+(* main functions ***********************************************************)
+
+type status = {
+ du: UM.uri -> UM.uri; (* uri discharge map *)
+ c : C.context; (* var context of this object *)
+ ls: (UM.uri, UM.uri list) Hashtbl.t; (* var lists of subobjects *)
+ rl: UM.uri list; (* reverse var list of this object *)
+ h : int (* relocation index *)
+}
+
+let add st k = {st with h = st.h + k}
+
+let discharge st u = st.h + list_pos (UM.eq u) st.rl
+
+let get_args st u =
+ try Hashtbl.find st.ls u
+ with Not_found ->
+ let args = vars_of_uri u in
+ Hashtbl.add st.ls u args; args
+
+let rec discharge_term st t = match t with
+ | C.Implicit _
+ | C.Sort _
+ | C.Rel _ -> t
+ | C.Const (u, s) ->
+ let args = get_args st u in
+ if args = [] then t else
+ let s = List.map (mk_arg s) args in
+ C.Appl (C.Const (st.du u, []) :: discharge_nsubst st s)
+ | C.MutInd (u, m, s) ->
+ let args = get_args st u in
+ if args = [] then t else
+ let s = List.map (mk_arg s) args in
+ C.Appl (C.MutInd (st.du u, m, []) :: discharge_nsubst st s)
+ | C.MutConstruct (u, m, n, s) ->
+ let args = get_args st u in
+ if args = [] then t else
+ let s = List.map (mk_arg s) args in
+ C.Appl (C.MutConstruct (st.du u, m, n, []) :: discharge_nsubst st s)
+ | C.Var (u, s) ->
+ let args = get_args st u in
+ if args = [] then C.Rel (discharge st u) else
+ let s = List.map (mk_arg s) args in
+ C.Appl (C.Rel (discharge st u) :: discharge_nsubst st s)
+ | C.Meta (i, s) ->
+ let s' = list_map_sh (discharge_usubst st) s in
+ if s' == s then t else C.Meta (i, s')
+ | C.Appl vs ->
+ let vs' = list_map_sh (discharge_term st) vs in
+ if vs' == vs then t else C.Appl (flatten vs')
+ | C.Cast (v, w) ->
+ let v', w' = discharge_term st v, discharge_term st w in
+ if v' = v && w' = w then t else
+ C.Cast (sh v v', sh w w')
+ | C.MutCase (u, m, w, v, vs) ->
+ let w', v', vs' =
+ discharge_term st w, discharge_term st v,
+ list_map_sh (discharge_term st) vs
+ in
+ if w' = w && v' = v && vs' == vs then t else
+ C.MutCase (st.du u, m, sh w w', sh v v', sh vs vs')
+ | C.Prod (b, w, v) ->
+ let w', v' = discharge_term st w, discharge_term (add st 1) v in
+ if w' = w && v' = v then t else
+ C.Prod (b, sh w w', sh v v')
+ | C.Lambda (b, w, v) ->
+ let w', v' = discharge_term st w, discharge_term (add st 1) v in
+ if w' = w && v' = v then t else
+ C.Lambda (b, sh w w', sh v v')
+ | C.LetIn (b, y, w, v) ->
+ let y', w', v' =
+ discharge_term st y, discharge_term st w, discharge_term (add st 1) v
+ in
+ if y' = y && w' = w && v' == v then t else
+ C.LetIn (b, sh y y', sh w w', sh v v')
+ | C.CoFix (i, s) ->
+ let no = List.length s in
+ let s' = list_map_sh (discharge_cofun st no) s in
+ if s' == s then t else C.CoFix (i, s')
+ | C.Fix (i, s) ->
+ let no = List.length s in
+ let s' = list_map_sh (discharge_fun st no) s in
+ if s' == s then t else C.Fix (i, s')
+
+and discharge_nsubst st s =
+ List.map (discharge_term st) s
+
+and discharge_usubst st s = match s with
+ | None -> s
+ | Some t ->
+ let t' = discharge_term st t in
+ if t' == t then s else Some t'
+
+and discharge_cofun st no f =
+ let b, w, v = f in
+ let w', v' = discharge_term st w, discharge_term (add st no) v in
+ if w' = w && v' = v then f else
+ b, sh w w', sh v v'
+
+and discharge_fun st no f =
+ let b, i, w, v = f in
+ let w', v' = discharge_term st w, discharge_term (add st no) v in
+ if w' = w && v' = v then f else
+ b, i, sh w w', sh v v'
+
+let close is_type st t =
+ let map t = function
+ | Some (b, C.Def (v, w)) -> C.LetIn (b, v, w, t)
+ | Some (b, C.Decl w) ->
+ if is_type then C.Prod (b, w, t) else C.Lambda (b, w, t)
+ | None -> assert false
+ in
+ List.fold_left map t st.c
+
+let discharge_con st con =
+ let b, v = con in
+ let v' = discharge_term st v in
+ if v' == v && st.rl = [] then con else b, close true st (sh v v')
+
+let discharge_type st ind_type =
+ let b, ind, w, cons = ind_type in
+ let w', cons' = discharge_term st w, list_map_sh (discharge_con st) cons in
+ if w' == w && cons' == cons && st.rl = [] then ind_type else
+ let w'' = close true st (sh w w') in
+ b, ind, w'', sh cons cons'
+
+let rec discharge_object du obj =
+ let ls = Hashtbl.create hashtbl_size in match obj with
+ | C.Variable (b, None, w, vars, attrs) ->
+ let st = init_status du ls vars in
+ let w' = discharge_term st w in
+ if w' = w && vars = [] then obj else
+ let w'' = close true st (sh w w') in
+ C.Variable (b, None, w'', [], attrs)
+ | C.Variable (b, Some v, w, vars, attrs) ->
+ let st = init_status du ls vars in
+ let w', v' = discharge_term st w, discharge_term st v in
+ if w' = w && v' = v && vars = [] then obj else
+ let w'', v'' = close true st (sh w w'), close false st (sh v v') in
+ C.Variable (b, Some v'', w'', [], attrs)
+ | C.Constant (b, None, w, vars, attrs) ->
+ let st = init_status du ls vars in
+ let w' = discharge_term st w in
+ if w' = w && vars = [] then obj else
+ let w'' = close true st (sh w w') in
+ C.Constant (b, None, w'', [], attrs)
+ | C.Constant (b, Some v, w, vars, attrs) ->
+ let st = init_status du ls vars in
+ let w', v' = discharge_term st w, discharge_term st v in
+ if w' = w && v' = v && vars = [] then obj else
+ let w'', v'' = close true st (sh w w'), close false st (sh v v') in
+ C.Constant (b, Some v'', w'', [], attrs)
+ | C.InductiveDefinition (types, vars, lpsno, attrs) ->
+ let st = init_status du ls vars in
+ let types' = list_map_sh (discharge_type st) types in
+ if types' == types && vars = [] then obj else
+ let lpsno' = lpsno + List.length vars in
+ C.InductiveDefinition (sh types types', [], lpsno', attrs)
+ | C.CurrentProof _ ->
+ HLog.warn not_implemented; obj
+
+and discharge_uri du uri =
+ let obj, _ = E.get_obj Un.default_ugraph uri in
+ let obj' = discharge_object du obj in
+ obj', obj' == obj
+
+and discharge_vars du vars =
+ let map u =
+ match discharge_uri du u with
+ | C.Variable (b, None, w, _, _), _ -> Some (C.Name b, C.Decl w)
+ | C.Variable (b, Some v, w, _, _), _ -> Some (C.Name b, C.Def (v, w))
+ | _ -> None
+ in
+ List.rev_map map vars
+
+and init_status du ls vars =
+ let c, rl = discharge_vars du vars, List.rev vars in
+ {du = du; c = c; ls = ls; rl = rl; h = 1}