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       | _             -> false
  47
  48 let is_not_atomic = function
  49    | C.Sort _
  50    | C.Rel _
  51    | C.Const _
  52    | C.Var _
  53    | C.MutInd _
  54    | C.MutConstruct _ -> false
  55    | _                -> true
  56
  57 let split c t =
  58    let add s v c = Some (s, C.Decl v) :: c in
  59    let rec aux whd a n c = function
  60       | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
  61       | v when whd        -> v :: a, n
  62       | v                 -> aux true a n c (Rd.whd ~delta:true c v)
  63     in
  64     aux false [] 0 c t
  65
  66 let add g htbl t proof decurry =
  67    if proof then C.CicHash.add htbl t decurry;
  68    g t proof decurry
  69
  70 let find g htbl t =
  71    try
  72       let decurry = C.CicHash.find htbl t in g t true decurry
  73    with Not_found -> g t false 0
  74
  75 (* term preprocessing *******************************************************)
  76
  77 let expanded_premise = "EXPANDED"
  78
  79 let defined_premise = "DEFINED"
  80
  81 let eta_expand tys t =
  82    let n = List.length tys in
  83    let name i = Printf.sprintf "%s%u" expanded_premise i in
  84    let lambda i ty t = C.Lambda (C.Name (name i), ty, t) in
  85    let arg i n = C.Rel (n - i) in
  86    let rec aux i f a = function
  87       | []       -> f, a
  88       | ty :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i n :: a) tl
  89    in
  90    let absts, args = aux 0 identity [] tys in
  91    absts (C.Appl (S.lift n t :: args))
  92
  93 let get_tys c decurry t =
  94    let tys, _ = split c (get_type c t) in
  95    let tys, _ = HEL.split_nth decurry (List.tl tys) in
  96    List.rev tys
  97
  98 let eta_fix c t proof decurry =
  99    if proof && decurry > 0 then eta_expand (get_tys c decurry t) t else t
 100
 101 let rec pp_cast g ht es c t v =
 102    if es then pp_proof g ht es c t else find g ht t
 103
 104 and pp_lambda g ht es c name v t =
 105    let name = if DTI.does_not_occur 1 t then C.Anonymous else name in
 106    let entry = Some (name, C.Decl v) in
 107    let g t _ decurry =
 108       let t = eta_fix (entry :: c) t true decurry in
 109       g (C.Lambda (name, v, t)) true 0 in
 110    if es then pp_proof g ht es (entry :: c) t else find g ht t
 111
 112 and pp_letin g ht es c name v t =
 113    let entry = Some (name, C.Def (v, None)) in
 114    let g t _ decurry =
 115       if DTI.does_not_occur 1 t then g (S.lift (-1) t) true decurry else
 116       let g v proof d = match v with
 117          | C.LetIn (mame, w, u) when proof ->
 118             let x = C.LetIn (mame, w, C.LetIn (name, u, S.lift_from 2 1 t)) in
 119             pp_proof g ht false c x
 120          | v                               ->
 121             let v = eta_fix c v proof d in
 122             g (C.LetIn (name, v, t)) true decurry
 123       in
 124       if es then pp_term g ht es c v else find g ht v
 125    in
 126    if es then pp_proof g ht es (entry :: c) t else find g ht t
 127
 128 and pp_appl_one g ht es c t v =
 129    let g t _ decurry =
 130       let g v proof d =
 131          match t, v with
 132             | t, C.LetIn (mame, w, u) when proof ->
 133                let x = C.LetIn (mame, w, C.Appl [S.lift 1 t; u]) in
 134                pp_proof g ht false c x
 135             | C.LetIn (mame, w, u), v            ->
 136                let x = C.LetIn (mame, w, C.Appl [u; S.lift 1 v]) in
 137                pp_proof g ht false c x
 138             | C.Appl ts, v when decurry > 0      ->
 139                let v = eta_fix c v proof d in
 140                g (C.Appl (List.append ts [v])) true (pred decurry)
 141             | t, v  when is_not_atomic t         ->
 142                let mame = C.Name defined_premise in
 143                let x = C.LetIn (mame, t, C.Appl [C.Rel 1; S.lift 1 v]) in
 144                pp_proof g ht false c x
 145             | t, v                               ->
 146                let _, premsno = split c (get_type c t) in
 147                let v = eta_fix c v proof d in
 148                g (C.Appl [t; v]) true (pred premsno)
 149       in
 150       if es then pp_term g ht es c v else find g ht v
 151    in
 152    if es then pp_proof g ht es c t else find g ht t
 153
 154 and pp_appl g ht es c t = function
 155    | []             -> pp_proof g ht es c t
 156    | [v]            -> pp_appl_one g ht es c t v
 157    | v1 :: v2 :: vs ->
 158       let x = C.Appl (C.Appl [t; v1] :: v2 :: vs) in
 159       pp_proof g ht es c x
 160
 161 and pp_proof g ht es c t =
 162    let g t proof decurry = add g ht t proof decurry in
 163    match t with
 164       | C.Cast (t, v)         -> pp_cast g ht es c t v
 165       | C.Lambda (name, v, t) -> pp_lambda g ht es c name v t
 166       | C.LetIn (name, v, t)  -> pp_letin g ht es c name v t
 167       | C.Appl (t :: vs)      -> pp_appl g ht es c t vs
 168       | t                     -> g t true 0
 169
 170 and pp_term g ht es c t =
 171    if is_proof c t then pp_proof g ht es c t else g t false 0
 172
 173 (* object preprocessing *****************************************************)
 174
 175 let pp_obj = function
 176    | C.Constant (name, Some bo, ty, pars, attrs) ->
 177       let g bo proof decurry =
 178          let bo = eta_fix [] bo proof decurry in
 179          C.Constant (name, Some bo, ty, pars, attrs)
 180       in
 181       let ht = C.CicHash.create 1 in
 182       begin try pp_term g ht true [] bo
 183       with e -> failwith ("PPP: " ^ Printexc.to_string e) end
 184    | obj                                         -> obj