components/acic_procedural/proceduralPreprocess.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 C    = Cic
  27 module Un   = CicUniv
  28 module S    = CicSubstitution
  29 module Rd   = CicReduction
  30 module TC   = CicTypeChecker
  31 module DTI  = DoubleTypeInference
  32 module HEL  = HExtlib
  33
  34 (* helper functions *********************************************************)
  35
  36 let identity x = x
  37
  38 let comp f g x = f (g x)
  39
  40 let get_type c t =
  41    let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
  42
  43 let is_proof c t =
  44    match Rd.whd ~delta:true c (get_type c (get_type c t)) with
  45       | C.Sort C.Prop -> true
  46       | C.Sort _      -> false
  47       | _             -> assert false
  48
  49 let is_not_atomic = function
  50    | C.Sort _
  51    | C.Rel _
  52    | C.Const _
  53    | C.Var _
  54    | C.MutInd _
  55    | C.MutConstruct _ -> false
  56    | _                -> true
  57
  58 let split c t =
  59    let add s v c = Some (s, C.Decl v) :: c in
  60    let rec aux whd a n c = function
  61       | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
  62       | v when whd        -> v :: a, n
  63       | v                 -> aux true a n c (Rd.whd ~delta:true c v)
  64     in
  65     aux false [] 0 c t
  66
  67 let add g htbl t proof decurry =
  68    if proof then C.CicHash.add htbl t decurry;
  69    g t proof decurry
  70
  71 let find g htbl t =
  72    try
  73       let decurry = C.CicHash.find htbl t in g t true decurry
  74    with Not_found -> g t false 0
  75
  76 (* term preprocessing *******************************************************)
  77
  78 let expanded_premise = "EXPANDED"
  79
  80 let defined_premise = "DEFINED"
  81
  82 let eta_expand g tys t =
  83    assert (tys <> []);
  84    let name i = Printf.sprintf "%s%u" expanded_premise i in
  85    let lambda i ty t = C.Lambda (C.Name (name i), ty, t) in
  86    let arg i = C.Rel (succ i) in
  87    let rec aux i f a = function
  88       | []       -> f, a
  89       | ty :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i :: a) tl
  90    in
  91    let n = List.length tys in
  92    let absts, args = aux 0 identity [] tys in
  93    let t = match S.lift n t with
  94       | C.Appl ts -> C.Appl (ts @ args)
  95       | t         -> C.Appl (t :: args)
  96    in
  97    g (absts t)
  98
  99 let get_tys c decurry =
 100    let rec aux n = function
 101 (*      | C.Appl (hd :: tl) -> aux (n + List.length tl) hd *)
 102       | t                 ->
 103          let tys, _ = split c (get_type c t) in
 104          let _, tys = HEL.split_nth n (List.rev tys) in
 105          let tys, _ = HEL.split_nth decurry tys in
 106          tys
 107    in
 108    aux 0
 109
 110 let eta_fix c t proof decurry =
 111    let rec aux g c = function
 112       | C.LetIn (name, v, t) ->
 113          let g t = g (C.LetIn (name, v, t)) in
 114          let entry = Some (name, C.Def (v, None)) in
 115          aux g (entry :: c) t
 116       | t                    -> eta_expand g (get_tys c decurry t) t
 117    in
 118    if proof && decurry > 0 then aux identity c t else t
 119
 120 let rec pp_cast g ht es c t v =
 121    if true then pp_proof g ht es c t else find g ht t
 122
 123 and pp_lambda g ht es c name v t =
 124    let name = if DTI.does_not_occur 1 t then C.Anonymous else name in
 125    let entry = Some (name, C.Decl v) in
 126    let g t _ decurry =
 127       let t = eta_fix (entry :: c) t true decurry in
 128       g (C.Lambda (name, v, t)) true 0 in
 129    if true then pp_proof g ht es (entry :: c) t else find g ht t
 130
 131 and pp_letin g ht es c name v t =
 132    let entry = Some (name, C.Def (v, None)) in
 133    let g t _ decurry =
 134       if DTI.does_not_occur 1 t then g (S.lift (-1) t) true decurry else
 135       let g v proof d = match v with
 136          | C.LetIn (mame, w, u) when proof ->
 137             let x = C.LetIn (mame, w, C.LetIn (name, u, S.lift_from 2 1 t)) in
 138             pp_proof g ht false c x
 139          | v                               ->
 140             let v = eta_fix c v proof d in
 141             g (C.LetIn (name, v, t)) true decurry
 142       in
 143       if true then pp_term g ht es c v else find g ht v
 144    in
 145    if true then pp_proof g ht es (entry :: c) t else find g ht t
 146
 147 and pp_appl_one g ht es c t v =
 148    let g t _ decurry =
 149       let g v proof d =
 150          match t, v with
 151             | t, C.LetIn (mame, w, u) when proof ->
 152                let x = C.LetIn (mame, w, C.Appl [S.lift 1 t; u]) in
 153                pp_proof g ht false c x
 154             | C.LetIn (mame, w, u), v            ->
 155                let x = C.LetIn (mame, w, C.Appl [u; S.lift 1 v]) in
 156                pp_proof g ht false c x
 157             | C.Appl ts, v when decurry > 0      ->
 158                let v = eta_fix c v proof d in
 159                g (C.Appl (List.append ts [v])) true (pred decurry)
 160             | t, v  when is_not_atomic t         ->
 161                let mame = C.Name defined_premise in
 162                let x = C.LetIn (mame, t, C.Appl [C.Rel 1; S.lift 1 v]) in
 163                pp_proof g ht false c x
 164             | t, v                               ->
 165                let v = eta_fix c v proof d in
 166                g (C.Appl [t; v]) true (pred decurry)
 167       in
 168       if true then pp_term g ht es c v else find g ht v
 169    in
 170    if true then pp_proof g ht es c t else find g ht t
 171
 172 and pp_appl g ht es c t = function
 173    | []             -> pp_proof g ht es c t
 174    | [v]            -> pp_appl_one g ht es c t v
 175    | v1 :: v2 :: vs ->
 176       let x = C.Appl (C.Appl [t; v1] :: v2 :: vs) in
 177       pp_proof g ht es c x
 178
 179 and pp_atomic g ht es c t =
 180    let _, premsno = split c (get_type c t) in
 181    g t true premsno
 182
 183 and pp_proof g ht es c t =
 184   Printf.eprintf "IN: |- %s\n" (*CicPp.ppcontext c*) (CicPp.ppterm t);
 185   let g t proof decurry =
 186      Printf.eprintf "OUT: %b %u |- %s\n" proof decurry (CicPp.ppterm t);
 187      g t proof decurry
 188   in
 189 (*   let g t proof decurry = add g ht t proof decurry in *)
 190    match t with
 191       | C.Cast (t, v)         -> pp_cast g ht es c t v
 192       | C.Lambda (name, v, t) -> pp_lambda g ht es c name v t
 193       | C.LetIn (name, v, t)  -> pp_letin g ht es c name v t
 194       | C.Appl (t :: vs)      -> pp_appl g ht es c t vs
 195       | t                     -> pp_atomic g ht es c t
 196
 197 and pp_term g ht es c t =
 198    if is_proof c t then pp_proof g ht es c t else g t false 0
 199
 200 (* object preprocessing *****************************************************)
 201
 202 let pp_obj = function
 203    | C.Constant (name, Some bo, ty, pars, attrs) ->
 204       let g bo proof decurry =
 205          let bo = eta_fix [] bo proof decurry in
 206          C.Constant (name, Some bo, ty, pars, attrs)
 207       in
 208       let ht = C.CicHash.create 1 in
 209       Printf.eprintf "BEGIN: %s\n" name;
 210       begin try pp_term g ht true [] bo
 211       with e -> failwith ("PPP: " ^ Printexc.to_string e) end
 212    | obj                                         -> obj