]> matita.cs.unibo.it Git - helm.git/blob - components/acic_procedural/proceduralPreprocess.ml
some improvements
[helm.git] / 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 true 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 true 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 (*          let t = eta_fix (entry :: c) t true decurry in *)
123             g (C.LetIn (name, v, t)) true decurry
124       in
125       if true then pp_term g ht es c v else find g ht v
126    in
127    if true then pp_proof g ht es (entry :: c) t else find g ht t
128
129 and pp_appl_one g ht es c t v =
130    let g t _ decurry =
131       let g v proof d =
132          match t, v with
133             | t, C.LetIn (mame, w, u) when proof ->
134                let x = C.LetIn (mame, w, C.Appl [S.lift 1 t; u]) in
135                pp_proof g ht false c x 
136             | C.LetIn (mame, w, u), v            ->
137                let x = C.LetIn (mame, w, C.Appl [u; S.lift 1 v]) in
138                pp_proof g ht false c x
139             | C.Appl ts, v when decurry > 0      ->
140                let v = eta_fix c v proof d in
141                g (C.Appl (List.append ts [v])) true (pred decurry)
142             | t, v  when is_not_atomic t         ->
143                let mame = C.Name defined_premise in
144                let x = C.LetIn (mame, t, C.Appl [C.Rel 1; S.lift 1 v]) in
145                pp_proof g ht false c x
146             | t, v                               ->
147                let _, premsno = split c (get_type c t) in
148                let v = eta_fix c v proof d in
149                g (C.Appl [t; v]) true (pred premsno)
150       in
151       if true then pp_term g ht es c v else find g ht v
152    in
153    if true then pp_proof g ht es c t else find g ht t
154
155 and pp_appl g ht es c t = function
156    | []             -> pp_proof g ht es c t
157    | [v]            -> pp_appl_one g ht es c t v
158    | v1 :: v2 :: vs ->
159       let x = C.Appl (C.Appl [t; v1] :: v2 :: vs) in 
160       pp_proof g ht es c x
161
162 and pp_proof g ht es c t = 
163 (*   let g t proof decurry = add g ht t proof decurry in *)
164    match t with
165       | C.Cast (t, v)         -> pp_cast g ht es c t v
166       | C.Lambda (name, v, t) -> pp_lambda g ht es c name v t
167       | C.LetIn (name, v, t)  -> pp_letin g ht es c name v t
168       | C.Appl (t :: vs)      -> pp_appl g ht es c t vs
169       | t                     -> g t true 0
170
171 and pp_term g ht es c t =
172    if is_proof c t then pp_proof g ht es c t else g t false 0
173
174 (* object preprocessing *****************************************************)
175
176 let pp_obj = function
177    | C.Constant (name, Some bo, ty, pars, attrs) ->
178       let g bo proof decurry = 
179          let bo = eta_fix [] bo proof decurry in
180          C.Constant (name, Some bo, ty, pars, attrs)
181       in
182       let ht = C.CicHash.create 1 in
183       begin try pp_term g ht true [] bo
184       with e -> failwith ("PPP: " ^ Printexc.to_string e) end
185    | obj                                         -> obj