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 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 (succ rpsno) wb in
 220             close false wc (C.Lambda (C.Anonymous, vty, wb))
 221 (* This case should not happen *)
 222          else assert false
 223       in
 224 (* END FIX OUT TYPE  *)
 225       if UM.eq u u' && w' == w && v' == v && vs' == vs then t else
 226       C.MutCase (u', m, sh w w', sh v v', sh vs vs')
 227    | C.Prod (b, w, v)             ->
 228       let w' = discharge_term st w in
 229       let es = [Some (b, C.Decl w')] in
 230       let v' = discharge_term (add st 1 es) v in
 231       if w' == w && v' == v then t else
 232       C.Prod (b, sh w w', sh v v')
 233    | C.Lambda (b, w, v)           ->
 234       let w' = discharge_term st w in
 235       let es = [Some (b, C.Decl w')] in
 236       let v' = discharge_term (add st 1 es) v in
 237       if w' == w && v' == v then t else
 238       C.Lambda (b, sh w w', sh v v')
 239    | C.LetIn (b, y, w, v)   ->
 240       let y', w' = discharge_term st y, discharge_term st w in
 241       let es = [Some (b, C.Def (y, w'))] in
 242       let v' =  discharge_term (add st 1 es) v in
 243       if y' == y && w' == w && v' == v then t else
 244       C.LetIn (b, sh y y', sh w w', sh v v')
 245    | C.CoFix (i, s)         ->
 246       let no, es = mk_context proj_cofix (discharge_term st) s in
 247       let s' = list_map_sh (discharge_cofun st no es) s in
 248       if s' == s then t else C.CoFix (i, s')
 249    | C.Fix (i, s)         ->
 250       let no, es = mk_context proj_fix (discharge_term st) s in
 251       let s' = list_map_sh (discharge_fun st no es) s in
 252       if s' == s then t else C.Fix (i, s')
 253
 254 and discharge_nsubst st s =
 255    List.map (discharge_term st) s
 256
 257 and discharge_usubst st s = match s with
 258    | None   -> s
 259    | Some t ->
 260       let t' = discharge_term st t in
 261       if t' == t then s else Some t'
 262
 263 and discharge_cofun st no es f =
 264    let b, w, v = f in
 265    let w', v' = discharge_term st w, discharge_term (add st no es) v in
 266    if w' == w && v' == v then f else
 267    b, sh w w', sh v v'
 268
 269 and discharge_fun st no es f =
 270    let b, i, w, v = f in
 271    let w', v' = discharge_term st w, discharge_term (add st no es) v in
 272    if w' == w && v' == v then f else
 273    b, i, sh w w', sh v v'
 274
 275 let close is_type st = close is_type st.c
 276
 277 let discharge_con st con =
 278    let b, v = con in
 279    let v' = discharge_term st v in
 280    if v' == v && st.rl = [] then con else st.dn b, close true st (sh v v')
 281
 282 let discharge_type st ind_type =
 283    let b, ind, w, cons = ind_type in
 284    let w', cons' = discharge_term st w, list_map_sh (discharge_con st) cons in
 285    if w' == w && cons' == cons && st.rl = [] then ind_type else
 286    let w'' = close true st (sh w w') in
 287    st.dn b, ind, w'', sh cons cons'
 288
 289 let rec discharge_object dn du obj =
 290    let ls = Hashtbl.create hashtbl_size in match obj with
 291    | C.Variable (b, None, w, vars, attrs)              ->
 292       let st = init_status dn du ls vars in
 293       let w' = discharge_term st w in
 294       if w' == w && vars = [] then obj else
 295       let w'' = sh w w' in
 296 (* We do not typecheck because variables are not closed *)
 297       C.Variable (dn b, None, w'', [], attrs)
 298    | C.Variable (b, Some v, w, vars, attrs)            ->
 299       let st = init_status dn du ls vars in
 300       let w', v' = discharge_term st w, discharge_term st v in
 301       if w' == w && v' == v && vars = [] then obj else
 302       let w'', v'' = sh w w', sh v v' in
 303 (* We do not typecheck because variables are not closed *)
 304       C.Variable (dn b, Some v'', w'', [], attrs)
 305    | C.Constant (b, None, w, vars, attrs)              ->
 306       let st = init_status dn du ls vars in
 307       let w' = discharge_term st w in
 308       if w' == w && vars = [] then obj else
 309       let w'' = close true st (sh w w') in
 310       let _ = typecheck (dn b) w'' in
 311       C.Constant (dn b, None, w'', [], attrs)
 312    | C.Constant (b, Some v, w, vars, attrs)            ->
 313       let st = init_status dn du ls vars in
 314       let w', v' = discharge_term st w, discharge_term st v in
 315       if w' == w && v' == v && vars = [] then obj else
 316       let w'', v'' = close true st (sh w w'), close false st (sh v v') in
 317       let _ = typecheck (dn b) (C.Cast (v'', w'')) in
 318       C.Constant (dn b, Some v'', w'', [], attrs)
 319    | C.InductiveDefinition (types, vars, lpsno, attrs) ->
 320       let st = init_status dn du ls vars in
 321       let types' = list_map_sh (discharge_type st) types in
 322       if types' == types && vars = [] then obj else
 323       let lpsno' = lpsno + List.length vars in
 324       C.InductiveDefinition (sh types types', [], lpsno', attrs)
 325    | C.CurrentProof _                                  ->
 326       HLog.warn not_implemented; obj
 327
 328 and discharge_uri dn du uri =
 329    let prerr msg obj =
 330       if !debug then begin
 331          out msg; Ut.pp_obj out obj; out "\n"
 332       end
 333    in
 334    let obj, _ = E.get_obj Un.default_ugraph uri in
 335    prerr "Plain     : " obj;
 336    let obj' = discharge_object dn du obj in
 337    prerr "Discharged: " obj';
 338    obj', obj' == obj
 339
 340 and discharge_vars dn du vars =
 341 (* We should check that the dependences are ordered telesopically *)
 342    let map u =
 343       match discharge_uri dn du u with
 344          | C.Variable (b, None, w, _, _), _   -> Some (C.Name b, C.Decl w)
 345          | C.Variable (b, Some v, w, _, _), _ -> Some (C.Name b, C.Def (v, w))
 346          | _                                  -> None
 347    in
 348    List.rev_map map vars
 349
 350 and init_status dn du ls vars =
 351    let c, rl = discharge_vars dn du vars, List.rev vars in
 352    {dn = dn; du = du; ls = ls; rl = rl; h = 1; c = c}