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
  33 let hashtbl_size = 11
  34
  35 let not_implemented =
  36    "discharge of current proofs is not implemented yet"
  37
  38 let debug = ref false
  39
  40 let out = prerr_string
  41
  42 (* helper functions *********************************************************)
  43
  44 let typecheck t =
  45    if !debug then begin
  46       let _ = TC.type_of_aux' [] [] t Un.default_ugraph in
  47       out "Typecheck : OK\n"
  48    end
  49
  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
  54    in
  55    aux 0 l
  56
  57 let sh a b = if a == b then a else b
  58
  59 let rec list_map_sh map l = match l with
  60    | []       -> l
  61    | hd :: tl ->
  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'
  65
  66 let flatten = function
  67    | C.Appl vs :: tl -> vs @ tl
  68    | ts              -> ts
  69
  70 let vars_of_uri uri =
  71    let obj, _ = E.get_obj Un.default_ugraph uri in
  72    match obj with
  73       | C.Constant (_, _, _, vars, _)
  74       | C.Variable (_, _, _, vars, _)
  75       | C.InductiveDefinition (_, vars, _, _)
  76       | C.CurrentProof (_, _, _, _, vars, _)  -> vars
  77
  78 let mk_arg s u =
  79    try List.assq u s
  80    with Not_found -> C.Var (u, [])
  81
  82 (* main functions ***********************************************************)
  83
  84 type status = {
  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                *)
  91 }
  92
  93 let add st k = {st with h = st.h + k}
  94
  95 let discharge st u = st.h + list_pos (UM.eq u) st.rl
  96
  97 let get_args st u =
  98    try Hashtbl.find st.ls u
  99    with Not_found ->
 100       let args = vars_of_uri u in
 101       Hashtbl.add st.ls u args; args
 102
 103 let rec discharge_term st t = match t with
 104    | C.Implicit _
 105    | C.Sort _
 106    | C.Rel _                      -> t
 107    | C.Const (u, 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.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)
 122    | C.Var (u, 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)
 127    | C.Meta (i, s)                ->
 128       let s' = list_map_sh (discharge_usubst st) s in
 129       if s' == s then t else C.Meta (i, s')
 130    | C.Appl vs                    ->
 131       let vs' = list_map_sh (discharge_term st) vs in
 132       if vs' == vs then t else C.Appl (flatten vs')
 133    | C.Cast (v, w)                ->
 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
 140       let w', v', vs' =
 141          discharge_term st w, discharge_term st v,
 142          list_map_sh (discharge_term st) vs
 143       in
 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)   ->
 155       let y', w', v' =
 156          discharge_term st y, discharge_term st w, discharge_term (add st 1) v
 157       in
 158       if y' == y && w' == w && v' == v then t else
 159       C.LetIn (b, sh y y', sh w w', sh v v')
 160    | C.CoFix (i, s)         ->
 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')
 164    | C.Fix (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')
 168
 169 and discharge_nsubst st s =
 170    List.map (discharge_term st) s
 171
 172 and discharge_usubst st s = match s with
 173    | None   -> s
 174    | Some t ->
 175       let t' = discharge_term st t in
 176       if t' == t then s else Some t'
 177
 178 and discharge_cofun st no f =
 179    let b, w, v = f in
 180    let w', v' = discharge_term st w, discharge_term (add st no) v in
 181    if w' == w && v' == v then f else
 182    b, sh w w', sh v v'
 183
 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'
 189
 190 let close is_type st t =
 191    let map t = function
 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
 196    in
 197    List.fold_left map t st.c
 198
 199 let discharge_con st con =
 200    let b, v = con in
 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')
 203
 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'
 210
 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
 217       let w'' = sh w w' in
 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
 249
 250 and discharge_uri dn du uri =
 251    let prerr msg obj =
 252       if !debug then begin
 253          out msg; Ut.pp_obj out obj; out "\n"
 254       end
 255    in
 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';
 260    obj', obj' == obj
 261
 262 and discharge_vars dn du vars =
 263 (* We should check that the dependences are ordered telesopically *)
 264    let map u =
 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))
 268          | _                                  -> None
 269    in
 270    List.rev_map map vars
 271
 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}