]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_proof_checking/cicDischarge.ml
better indentation
[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 module Ut = CicUtil
31 module TC = CicTypeChecker
32 module S  = CicSubstitution
33 module X  = HExtlib
34
35 let hashtbl_size = 11
36
37 let not_implemented =
38    "discharge of current proofs is not implemented yet"
39
40 let debug = ref false
41
42 let out = prerr_string
43
44 (* helper functions *********************************************************)
45
46 let rec count_prods n = function
47    | C.Prod (_, _, t) -> count_prods (succ n) t
48    | _                -> n
49
50 let get_ind_type_psnos uri tyno =
51    match E.get_obj Un.default_ugraph uri with
52       | C.InductiveDefinition (tys, _, lpsno, _), _ -> 
53          let _, _, ty, _ = List.nth tys tyno in
54          lpsno, count_prods 0 ty
55       | _                                           -> assert false
56
57 let typecheck b t =
58    if !debug then begin
59       out (Printf.sprintf "Pre Check ; %s\n" b);
60       Ut.pp_term out [] [] t; out "\n";      
61       let _ = TC.type_of_aux' [] [] t Un.default_ugraph in
62       out (Printf.sprintf "Typecheck : %s OK\n" b)
63    end
64
65 let list_pos found l =
66    let rec aux n = function
67       | []       -> raise Not_found
68       | hd :: tl -> if found hd then n else aux (succ n) tl
69    in 
70    aux 0 l
71
72 let sh a b = if a == b then a else b
73
74 let rec list_map_sh map l = match l with
75    | []       -> l
76    | hd :: tl ->
77       let hd', tl' = map hd, list_map_sh map tl in
78       if hd' == hd && tl' == tl then l else
79       sh hd hd' :: sh tl tl'
80
81 let flatten = function
82    | C.Appl vs :: tl -> vs @ tl
83    | ts              -> ts
84
85 let vars_of_uri uri =
86    let obj, _ = E.get_obj Un.default_ugraph uri in
87    match obj with
88       | C.Constant (_, _, _, vars, _)
89       | C.Variable (_, _, _, vars, _)
90       | C.InductiveDefinition (_, vars, _, _)
91       | C.CurrentProof (_, _, _, _, vars, _)  -> vars
92
93 let mk_arg s u =
94    try List.assq u s
95    with Not_found -> C.Var (u, [])
96
97 (* main functions ***********************************************************)
98
99 type status = {
100    dn: string -> string;                (* name discharge map              *)
101    du: UM.uri -> UM.uri;                (* uri discharge map               *)
102    ls: (UM.uri, UM.uri list) Hashtbl.t; (* var lists of subobjects         *)
103    rl: UM.uri list;                     (* reverse var list of this object *)
104    h : int;                             (* relocation index                *)
105    c : C.context                        (* local context of this object    *)
106 }
107
108 let add st k es = {st with h = st.h + k; c = List.rev_append es st.c}
109
110 let discharge st u = st.h + list_pos (UM.eq u) st.rl
111
112 let get_args st u =
113    try Hashtbl.find st.ls u
114    with Not_found -> 
115       let args = vars_of_uri u in
116       Hashtbl.add st.ls u args; args
117
118 let proj_fix (s, _, w, _) = s, w 
119
120 let proj_cofix (s, w, _) = s, w
121
122 let mk_context proj discharge_term s = 
123    let map e = 
124       let s, w = proj e in
125       let w' = discharge_term w in
126       Some (C.Name s, C.Decl w')      
127    in
128    List.length s, List.rev_map map s
129
130 let rec split_absts named no c = function
131    | C.Lambda (s, w, t) -> 
132       let e = Some (s, C.Decl w) in
133       let named = named && s <> C.Anonymous in
134       split_absts named (succ no) (e :: c) t
135    | t                  ->
136       named, no, c, t
137
138 let close is_type c t = 
139    let map t = function
140       | Some (b, C.Def (v, w)) -> C.LetIn (b, v, w, t)
141       | Some (b, C.Decl w)     ->
142          if is_type then C.Prod (b, w, t) else C.Lambda (b, w, t)
143       | None                   -> assert false
144    in
145    List.fold_left map t c
146
147 let relocate to_what from_what k m =
148    try 
149       let u = List.nth from_what (m - k) in
150       let map v m = if UM.eq u v then Some m else None in
151       match X.list_findopt map to_what with      
152          | Some m -> m + k
153          | None   -> raise (Failure "nth")
154    with
155       | Failure "nth" -> assert false
156
157 let rec discharge_term st t = match t with
158    | C.Implicit _
159    | C.Sort _
160    | C.Rel _                      -> t
161    | C.Const (u, s)               ->
162       let args = get_args st u in
163       if args = [] then t else
164       let s = List.map (mk_arg s) args in
165       C.Appl (C.Const (st.du u, []) :: discharge_nsubst st s)
166    | C.MutInd (u, m, s)           ->
167       let args = get_args st u in
168       if args = [] then t else
169       let s = List.map (mk_arg s) args in
170       C.Appl (C.MutInd (st.du u, m, []) :: discharge_nsubst st s)
171    | C.MutConstruct (u, m, n, s)  ->
172       let args = get_args st u in
173       if args = [] then t else
174       let s = List.map (mk_arg s) args in
175       C.Appl (C.MutConstruct (st.du u, m, n, []) :: discharge_nsubst st s)
176    | C.Var (u, s)                 ->
177 (* We do not discharge the nsubst because variables are not closed *)
178 (* thus only the identity nsubst should be allowed                 *)
179       if s <> [] then assert false else
180       C.Rel (discharge st u)
181    | C.Meta (i, s)                ->
182       let s' = list_map_sh (discharge_usubst st) s in
183       if s' == s then t else C.Meta (i, s')
184    | C.Appl vs                    ->
185       let vs' = list_map_sh (discharge_term st) vs in
186       if vs' == vs then t else C.Appl (flatten vs')
187    | C.Cast (v, w)                ->
188       let v', w' = discharge_term st v, discharge_term st w in
189       if v' == v && w' == w then t else
190       C.Cast (sh v v', sh w w')
191    | C.MutCase (u, m, w, v, vs)   ->
192       let args = get_args st u in
193       let u' = if args = [] then u else st.du u in
194       let w', v', vs' = 
195          discharge_term st w, discharge_term st v,
196          list_map_sh (discharge_term st) vs
197       in
198 (* BEGIN FIX OUT TYPE  *)
199       let lpsno, psno = get_ind_type_psnos u m in
200       let rpsno = psno - lpsno in
201       let named, frpsno, wc, wb = split_absts true 0 [] w' in
202       let w' =
203 (* No fixing needed *)      
204          if frpsno = succ rpsno then w' else
205 (* Fixing needed, no right parametes *)
206          if frpsno = rpsno && rpsno = 0 then
207             let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in
208             if !debug then begin
209                out "VTY: "; Ut.pp_term out [] st.c vty; out "\n"
210             end;
211             C.Lambda (C.Anonymous, vty, S.lift 1 wb)
212          else
213 (* Fixing needed, some right parametes *)
214          if frpsno = rpsno && named then
215             let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in
216             if !debug then begin
217                out "VTY: "; Ut.pp_term out [] st.c vty; out "\n"
218             end;
219             let vty, wb = S.lift rpsno vty, S.lift 1 wb in 
220             let vty = match vty with
221                | C.Appl (C.MutInd (fu, fm, _) as hd :: args) 
222                   when UM.eq fu u && fm = m && List.length args = psno ->
223                   let largs, _ = X.split_nth lpsno args in
224                   C.Appl (hd :: largs @ Ut.mk_rels rpsno 0)  
225                | _                                                     ->
226                   assert false
227             in
228             close false wc (C.Lambda (C.Anonymous, vty, wb))
229 (* This case should not happen *)
230          else assert false 
231       in
232 (* END FIX OUT TYPE  *)
233       if UM.eq u u' && w' == w && v' == v && vs' == vs then t else
234       C.MutCase (u', m, sh w w', sh v v', sh vs vs')
235    | C.Prod (b, w, v)             ->
236       let w' = discharge_term st w in 
237       let es = [Some (b, C.Decl w')] in
238       let v' = discharge_term (add st 1 es) v in
239       if w' == w && v' == v then t else
240       C.Prod (b, sh w w', sh v v')
241    | C.Lambda (b, w, v)           ->
242       let w' = discharge_term st w in 
243       let es = [Some (b, C.Decl w')] in
244       let v' = discharge_term (add st 1 es) v in
245       if w' == w && v' == v then t else
246       C.Lambda (b, sh w w', sh v v')
247    | C.LetIn (b, y, w, v)   ->
248       let y', w' = discharge_term st y, discharge_term st w in
249       let es = [Some (b, C.Def (y, w'))] in
250       let v' =  discharge_term (add st 1 es) v in
251       if y' == y && w' == w && v' == v then t else
252       C.LetIn (b, sh y y', sh w w', sh v v')
253    | C.CoFix (i, s)         ->
254       let no, es = mk_context proj_cofix (discharge_term st) s in
255       let s' = list_map_sh (discharge_cofun st no es) s in
256       if s' == s then t else C.CoFix (i, s')
257    | C.Fix (i, s)         ->
258       let no, es = mk_context proj_fix (discharge_term st) s in
259       let s' = list_map_sh (discharge_fun st no es) s in
260       if s' == s then t else C.Fix (i, s')
261
262 and discharge_nsubst st s =
263    List.map (discharge_term st) s
264
265 and discharge_usubst st s = match s with
266    | None   -> s
267    | Some t ->
268       let t' = discharge_term st t in
269       if t' == t then s else Some t'
270
271 and discharge_cofun st no es f =
272    let b, w, v = f in
273    let w', v' = discharge_term st w, discharge_term (add st no es) v in
274    if w' == w && v' == v then f else
275    b, sh w w', sh v v'
276
277 and discharge_fun st no es f =
278    let b, i, w, v = f in
279    let w', v' = discharge_term st w, discharge_term (add st no es) v in
280    if w' == w && v' == v then f else
281    b, i, sh w w', sh v v'
282
283 let close is_type st = close is_type st.c
284
285 let discharge_con st con =
286    let b, v = con in
287    let v' = discharge_term st v in
288    if v' == v && st.rl = [] then con else st.dn b, close true st (sh v v')
289
290 let discharge_type st ind_type =
291    let b, ind, w, cons = ind_type in
292    let w', cons' = discharge_term st w, list_map_sh (discharge_con st) cons in
293    if w' == w && cons' == cons && st.rl = [] then ind_type else
294    let w'' = close true st (sh w w') in
295    st.dn b, ind, w'', sh cons cons'
296
297 let rec discharge_object dn du obj = 
298    let ls = Hashtbl.create hashtbl_size in match obj with
299    | C.Variable (b, None, w, vars, attrs)              ->
300       let st = init_status dn du ls vars in
301       let w' = discharge_term st w in
302       if w' == w && vars = [] then obj else
303       let w'' = sh w w' in
304 (* We do not typecheck because variables are not closed *)
305       C.Variable (dn b, None, w'', vars, attrs)
306    | C.Variable (b, Some v, w, vars, attrs)            ->
307       let st = init_status dn du ls vars in
308       let w', v' = discharge_term st w, discharge_term st v in
309       if w' == w && v' == v && vars = [] then obj else
310       let w'', v'' = sh w w', sh v v' in
311 (* We do not typecheck because variables are not closed *)
312       C.Variable (dn b, Some v'', w'', vars, attrs)
313    | C.Constant (b, None, w, vars, attrs)              ->
314       let st = init_status dn du ls vars in
315       let w' = discharge_term st w in
316       if w' == w && vars = [] then obj else
317       let w'' = close true st (sh w w') in
318       let _ = typecheck (dn b) w'' in
319       C.Constant (dn b, None, w'', [], attrs)
320    | C.Constant (b, Some v, w, vars, attrs)            ->
321       let st = init_status dn du ls vars in
322       let w', v' = discharge_term st w, discharge_term st v in
323       if w' == w && v' == v && vars = [] then obj else
324       let w'', v'' = close true st (sh w w'), close false st (sh v v') in
325       let _ = typecheck (dn b) (C.Cast (v'', w'')) in
326       C.Constant (dn b, Some v'', w'', [], attrs)
327    | C.InductiveDefinition (types, vars, lpsno, attrs) ->
328       let st = init_status dn du ls vars in
329       let types' = list_map_sh (discharge_type st) types in
330       if types' == types && vars = [] then obj else
331       let lpsno' = lpsno + List.length vars in
332       C.InductiveDefinition (sh types types', [], lpsno', attrs)
333    | C.CurrentProof _                                  ->
334       HLog.warn not_implemented; obj
335
336 and discharge_uri dn du uri =
337    let prerr msg obj =
338       if !debug then begin
339          out msg; Ut.pp_obj out obj; out "\n"
340       end
341    in
342    let obj, _ = E.get_obj Un.default_ugraph uri in
343    prerr "Plain     : " obj;
344    let obj' = discharge_object dn du obj in
345    prerr "Discharged: " obj';
346    obj', obj' == obj
347
348 and discharge_vars dn du vars =
349    let rec aux us c = function
350       | []      -> c
351       | u :: tl ->
352          let e = match discharge_uri dn du u with
353             | C.Variable (b, None, w, vars, _), _   -> 
354                let map = relocate us (List.rev vars) in 
355                let w = S.lift_map 1 map w in
356                Some (C.Name b, C.Decl w)
357             | C.Variable (b, Some v, w, vars, _), _ -> 
358                let map = relocate us (List.rev vars) in
359                let v, w = S.lift_map 1 map v, S.lift_map 1 map w in
360                Some (C.Name b, C.Def (v, w))
361             | _                                     -> assert false
362          in
363          aux (u :: us) (e :: c) tl
364    in 
365    aux [] [] vars
366
367 and init_status dn du ls vars =
368    let c, rl = discharge_vars dn du vars, List.rev vars in
369    {dn = dn; du = du; ls = ls; rl = rl; h = 1; c = c}