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 R    = 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 (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 (R.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 n t =
  82    let ty = C.Implicit None in
  83    let name i = Printf.sprintf "%s%u" expanded_premise i in
  84    let lambda i 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 =
  87       if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a)
  88    in
  89    let absts, args = aux 0 identity [] in
  90    absts (C.Appl (S.lift n t :: args))
  91
  92 let eta_fix t proof decurry =
  93    if proof && decurry > 0 then eta_expand decurry t else t
  94
  95 let rec pp_cast g ht es c t v =
  96    if es then pp_proof g ht es c t else find g ht t
  97
  98 and pp_lambda g ht es c name v t =
  99    let name = if DTI.does_not_occur 1 t then C.Anonymous else name in
 100    let entry = Some (name, C.Decl v) in
 101    let g t _ decurry =
 102       let t = eta_fix t true decurry in
 103       g (C.Lambda (name, v, t)) true 0 in
 104    if es then pp_proof g ht es (entry :: c) t else find g ht t
 105
 106 and pp_letin g ht es c name v t =
 107    let entry = Some (name, C.Def (v, None)) in
 108    let g t _ decurry =
 109       if DTI.does_not_occur 1 t then g (S.lift (-1) t) true decurry else
 110       let g v proof d = match v with
 111          | C.LetIn (mame, w, u) when proof ->
 112             let x = C.LetIn (mame, w, C.LetIn (name, u, S.lift_from 2 1 t)) in
 113             pp_proof g ht false c x
 114          | v                               ->
 115             let v = eta_fix v proof d in
 116             g (C.LetIn (name, v, t)) true decurry
 117       in
 118       if es then pp_term g ht es c v else find g ht v
 119    in
 120    if es then pp_proof g ht es (entry :: c) t else find g ht t
 121
 122 and pp_appl_one g ht es c t v =
 123    let g t _ decurry =
 124       let g v proof d =
 125          match t, v with
 126             | t, C.LetIn (mame, w, u) when proof ->
 127                let x = C.LetIn (mame, w, C.Appl [S.lift 1 t; u]) in
 128                pp_proof g ht false c x
 129             | C.LetIn (mame, w, u), v            ->
 130                let x = C.LetIn (mame, w, C.Appl [u; S.lift 1 v]) in
 131                pp_proof g ht false c x
 132             | C.Appl ts, v when decurry > 0      ->
 133                let v = eta_fix v proof d in
 134                g (C.Appl (List.append ts [v])) true (pred decurry)
 135             | t, v  when is_not_atomic t         ->
 136                let mame = C.Name defined_premise in
 137                let x = C.LetIn (mame, t, C.Appl [C.Rel 1; S.lift 1 v]) in
 138                pp_proof g ht false c x
 139             | t, v                               ->
 140                let _, premsno = split c (get_type c t) in
 141                let v = eta_fix v proof d in
 142                g (C.Appl [t; v]) true (pred premsno)
 143       in
 144       if es then pp_term g ht es c v else find g ht v
 145    in
 146    if es then pp_proof g ht es c t else find g ht t
 147
 148 and pp_appl g ht es c t = function
 149    | []             -> pp_proof g ht es c t
 150    | [v]            -> pp_appl_one g ht es c t v
 151    | v1 :: v2 :: vs ->
 152       let x = C.Appl (C.Appl [t; v1] :: v2 :: vs) in
 153       pp_proof g ht es c x
 154
 155 and pp_proof g ht es c t =
 156    let g t proof decurry = add g ht t proof decurry in
 157    match t with
 158       | C.Cast (t, v)         -> pp_cast g ht es c t v
 159       | C.Lambda (name, v, t) -> pp_lambda g ht es c name v t
 160       | C.LetIn (name, v, t)  -> pp_letin g ht es c name v t
 161       | C.Appl (t :: vs)      -> pp_appl g ht es c t vs
 162       | t                     -> g t true 0
 163
 164 and pp_term g ht es c t =
 165    if is_proof c t then pp_proof g ht es c t else g t false 0
 166
 167 (* object preprocessing *****************************************************)
 168
 169 let pp_obj = function
 170    | C.Constant (name, Some bo, ty, pars, attrs) ->
 171       let g bo proof decurry =
 172          let bo = eta_fix bo proof decurry in
 173          C.Constant (name, Some bo, ty, pars, attrs)
 174       in
 175       let ht = C.CicHash.create 1 in
 176       pp_term g ht true [] bo
 177    | obj                                         -> obj