]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_proof_checking/cicDischarge.ml
52b841952a2158e47784108e62ea5f740ece3ca0
[helm.git] / helm / software / components / cic_proof_checking / cicDischarge.ml
1 (* Copyright (C) 2003-2005, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 module UM = UriManager
27 module C  = Cic
28 module Un = CicUniv
29 module E  = CicEnvironment
30
31 let hashtbl_size = 11
32
33 let not_implemented =
34    "discharge of current proofs is not implemented yet"
35
36 let debug = ref false
37
38 (* helper functions *********************************************************)
39
40 let list_pos found l =
41    let rec aux n = function
42       | []       -> raise Not_found
43       | hd :: tl -> if found hd then n else aux (succ n) tl
44    in 
45    aux 0 l
46
47 let sh a b = if a == b then a else b
48
49 let rec list_map_sh map l = match l with
50    | []       -> l
51    | hd :: tl ->
52       let hd', tl' = map hd, list_map_sh map tl in
53       if hd' == hd && tl' == tl then l else
54       sh hd hd' :: sh tl tl'
55
56 let flatten = function
57    | C.Appl vs :: tl -> vs @ tl
58    | ts              -> ts
59
60 let vars_of_uri uri =
61    let obj, _ = E.get_obj Un.default_ugraph uri in
62    match obj with
63       | C.Constant (_, _, _, vars, _)
64       | C.Variable (_, _, _, vars, _)
65       | C.InductiveDefinition (_, vars, _, _)
66       | C.CurrentProof (_, _, _, _, vars, _)  -> vars
67
68 let mk_arg s u =
69    try List.assq u s
70    with Not_found -> C.Var (u, [])
71
72 (* main functions ***********************************************************)
73
74 type status = {
75    dn: string -> string;                (* name discharge map              *)
76    du: UM.uri -> UM.uri;                (* uri discharge map               *)
77    c : C.context;                       (* var context of this object      *)
78    ls: (UM.uri, UM.uri list) Hashtbl.t; (* var lists of subobjects         *)
79    rl: UM.uri list;                     (* reverse var list of this object *)
80    h : int                              (* relocation index                *)
81 }
82
83 let add st k = {st with h = st.h + k}
84
85 let discharge st u = st.h + list_pos (UM.eq u) st.rl
86
87 let get_args st u =
88    try Hashtbl.find st.ls u
89    with Not_found -> 
90       let args = vars_of_uri u in
91       Hashtbl.add st.ls u args; args
92
93 let rec discharge_term st t = match t with
94    | C.Implicit _
95    | C.Sort _
96    | C.Rel _                      -> t
97    | C.Const (u, s)               ->
98       let args = get_args st u in
99       if args = [] then t else
100       let s = List.map (mk_arg s) args in
101       C.Appl (C.Const (st.du u, []) :: discharge_nsubst st s)
102    | C.MutInd (u, m, s)           ->
103       let args = get_args st u in
104       if args = [] then t else
105       let s = List.map (mk_arg s) args in
106       C.Appl (C.MutInd (st.du u, m, []) :: discharge_nsubst st s)
107    | C.MutConstruct (u, m, n, s)  ->
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.MutConstruct (st.du u, m, n, []) :: discharge_nsubst st s)
112    | C.Var (u, s)                 ->
113 (* We do not discharge the nsubst because variables are not closed *)
114 (* thus only the identity nsubst should be allowed                 *)
115       if s <> [] then assert false else
116       C.Rel (discharge st u)
117    | C.Meta (i, s)                ->
118       let s' = list_map_sh (discharge_usubst st) s in
119       if s' == s then t else C.Meta (i, s')
120    | C.Appl vs                    ->
121       let vs' = list_map_sh (discharge_term st) vs in
122       if vs' == vs then t else C.Appl (flatten vs')
123    | C.Cast (v, w)                ->
124       let v', w' = discharge_term st v, discharge_term st w in
125       if v' = v && w' = w then t else
126       C.Cast (sh v v', sh w w')
127    | C.MutCase (u, m, w, v, vs)   ->
128       let w', v', vs' = 
129          discharge_term st w, discharge_term st v,
130          list_map_sh (discharge_term st) vs
131       in
132       if w' = w && v' = v && vs' == vs then t else
133       C.MutCase (st.du u, m, sh w w', sh v v', sh vs vs')
134    | C.Prod (b, w, v)             ->
135       let w', v' = discharge_term st w, discharge_term (add st 1) v in
136       if w' = w && v' = v then t else
137       C.Prod (b, sh w w', sh v v')
138    | C.Lambda (b, w, v)           ->
139       let w', v' = discharge_term st w, discharge_term (add st 1) v in
140       if w' = w && v' = v then t else
141       C.Lambda (b, sh w w', sh v v')
142    | C.LetIn (b, y, w, v)   ->
143       let y', w', v' = 
144          discharge_term st y, discharge_term st w, discharge_term (add st 1) v
145       in
146       if y' = y && w' = w && v' == v then t else
147       C.LetIn (b, sh y y', sh w w', sh v v')
148    | C.CoFix (i, s)         ->
149       let no = List.length s in
150       let s' = list_map_sh (discharge_cofun st no) s in
151       if s' == s then t else C.CoFix (i, s')
152    | C.Fix (i, s)         ->
153       let no = List.length s in
154       let s' = list_map_sh (discharge_fun st no) s in
155       if s' == s then t else C.Fix (i, s')
156
157 and discharge_nsubst st s =
158    List.map (discharge_term st) s
159
160 and discharge_usubst st s = match s with
161    | None   -> s
162    | Some t ->
163       let t' = discharge_term st t in
164       if t' == t then s else Some t'
165
166 and discharge_cofun st no f =
167    let b, w, v = f in
168    let w', v' = discharge_term st w, discharge_term (add st no) v in
169    if w' = w && v' = v then f else
170    b, sh w w', sh v v'
171
172 and discharge_fun st no f =
173    let b, i, w, v = f in
174    let w', v' = discharge_term st w, discharge_term (add st no) v in
175    if w' = w && v' = v then f else
176    b, i, sh w w', sh v v'
177
178 let close is_type st t = 
179    let map t = function
180       | Some (b, C.Def (v, w)) -> C.LetIn (b, v, w, t)
181       | Some (b, C.Decl w)     ->
182          if is_type then C.Prod (b, w, t) else C.Lambda (b, w, t)
183       | None                   -> assert false
184    in   
185    List.fold_left map t st.c
186
187 let discharge_con st con =
188    let b, v = con in
189    let v' = discharge_term st v in
190    if v' == v && st.rl = [] then con else st.dn b, close true st (sh v v')
191
192 let discharge_type st ind_type =
193    let b, ind, w, cons = ind_type in
194    let w', cons' = discharge_term st w, list_map_sh (discharge_con st) cons in
195    if w' == w && cons' == cons && st.rl = [] then ind_type else
196    let w'' = close true st (sh w w') in
197    st.dn b, ind, w'', sh cons cons'
198
199 let rec discharge_object dn du obj = 
200    let ls = Hashtbl.create hashtbl_size in match obj with
201    | C.Variable (b, None, w, vars, attrs)              ->
202       let st = init_status dn du ls vars in
203       let w' = discharge_term st w in
204       if w' = w && vars = [] then obj else
205       let w'' = sh w w' in
206       C.Variable (dn b, None, w'', [], attrs)
207    | C.Variable (b, Some v, w, vars, attrs)            ->
208       let st = init_status dn du ls vars in
209       let w', v' = discharge_term st w, discharge_term st v in
210       if w' = w && v' = v && vars = [] then obj else
211       let w'', v'' = sh w w', sh v v' in
212       C.Variable (dn b, Some v'', w'', [], attrs)
213    | C.Constant (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
217       let w'' = close true st (sh w w') in
218       C.Constant (dn b, None, w'', [], attrs)
219    | C.Constant (b, Some v, w, vars, attrs)            ->
220       let st = init_status dn du ls vars in
221       let w', v' = discharge_term st w, discharge_term st v in
222       if w' = w && v' = v && vars = [] then obj else
223       let w'', v'' = close true st (sh w w'), close false st (sh v v') in
224       C.Constant (dn b, Some v'', w'', [], attrs)
225    | C.InductiveDefinition (types, vars, lpsno, attrs) ->
226       let st = init_status dn du ls vars in
227       let types' = list_map_sh (discharge_type st) types in
228       if types' == types && vars = [] then obj else
229       let lpsno' = lpsno + List.length vars in
230       C.InductiveDefinition (sh types types', [], lpsno', attrs)
231    | C.CurrentProof _                                  ->
232       HLog.warn not_implemented; obj
233
234 and discharge_uri dn du uri =
235    let obj, _ = E.get_obj Un.default_ugraph uri in
236    if !debug then prerr_endline ("Plain     : " ^ CicPp.ppobj obj); 
237    let obj' = discharge_object dn du obj in
238    if !debug then prerr_endline ("Discharged: " ^ CicPp.ppobj obj'); 
239    obj', obj' == obj
240
241 and discharge_vars dn du vars =
242 (* We should check that the dependences are ordered telesopically *)   
243    let map u =
244       match discharge_uri dn du u with
245          | C.Variable (b, None, w, _, _), _   -> Some (C.Name b, C.Decl w)
246          | C.Variable (b, Some v, w, _, _), _ -> Some (C.Name b, C.Def (v, w))
247          | _                                  -> None
248    in
249    List.rev_map map vars
250
251 and init_status dn du ls vars =
252    let c, rl = discharge_vars dn du vars, List.rev vars in
253    {dn = dn; du = du; c = c; ls = ls; rl = rl; h = 1}