]> matita.cs.unibo.it Git - helm.git/blob - helm/software/helena/src/common/layer.ml
1ad6cf28cae6b5522bbb37cc33ba6c720d6e1c3c
[helm.git] / helm / software / helena / src / common / layer.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.              
9      \ /   This software is distributed as is, NO WARRANTY.              
10       V_______________________________________________________________ *)
11
12 module KH = Hashtbl
13
14 module L  = Log
15 module P  = Marks
16 module G  = Options
17
18 type value = Inf                 (* infinite layer *)
19            | Fin of int          (* finite layer *)
20            | Ref of P.mark * int (* referred layer, step *)
21            | Unk                 (* no layer set *)
22
23 type layer = {
24   mutable v: value; (* value *)  
25           s: bool;  (* static layer? *)
26   mutable b: bool;  (* beta allowed? *)
27 }
28
29 type status = (P.mark, layer) KH.t (* environment for layer variables *)
30
31 (* Internal functions *******************************************************)
32
33 let level = 7
34
35 let env_size = 1300
36
37 let warn s = L.warn (pred level) s
38
39 let zero = Fin 0
40
41 let string_of_value k = function
42    | Inf        -> ""
43    | Fin i      -> string_of_int i
44    | Ref (k, i) -> "-" ^ P.string_of_mark k ^ "-" ^ string_of_int i
45    | Unk        -> "-" ^ P.string_of_mark k
46
47 (* Note: remove assigned variables *)
48 let pp_table st =
49    let map k n = 
50       warn (Printf.sprintf "%s: v %s (s:%b b:%b)" 
51          (P.string_of_mark k) (string_of_value k n.v) n.s n.b
52       )
53    in
54    KH.iter map st 
55
56 let cell s v = {
57    v = v; s = s; b = false
58 }
59
60 let empty () = cell true Unk
61
62 let dynamic k i = cell false (Ref (k, i))
63
64 let find_with_default st default k =
65    try KH.find st k with Not_found -> KH.add st k default; default 
66
67 let find st k =
68    try KH.find st k with Not_found -> assert false 
69
70 let rec resolve_key_with_default st default k = match find_with_default st default k with
71    | {v = Ref (k, i)} when i = 0 -> resolve_key_with_default st default k
72    | cell                        -> k, cell
73
74 let rec resolve_key st k = match find st k with
75    | {v = Ref (k, i)} when i = 0 -> resolve_key st k
76    | cell                        -> k, cell
77
78 let resolve_layer st = function
79    | {v = Ref (k, i)} when i = 0 -> resolve_key st k
80    | cell                        -> P.null_mark, cell
81
82 let rec generated st h i =
83    let default = dynamic h i in
84    let k = P.new_mark () in
85    let k, n = resolve_key_with_default st default k in 
86    if n.s then generated st h i else begin
87       if n <> default then KH.replace st k default;
88       if !G.ct >= level then pp_table st; default
89    end
90
91 let assert_finite st n j =
92    if !G.ct >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
93    let rec aux (k, n) j = match n.v with    
94       | Fin i when i = j -> true
95       | Fin i            ->
96          Printf.printf "binder %s is %u but must be %u\n" (P.string_of_mark k) i j; true (**)
97       | Inf              ->
98          Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; true (**)
99       | Unk              -> n.v <- Fin j; if !G.ct >= level then pp_table st; true
100       | Ref (k, i)       -> n.v <- Fin j; aux (resolve_key st k) (i+j) 
101    in
102    let k, n = resolve_layer st n in
103 (*   if j = 0 && n.b then begin
104       Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false (**)
105    end else *)
106       aux (k, n) j
107
108 let assert_infinite st n =
109    if !G.ct >= level then warn "ASSERT INFINITE";
110    let rec aux (k, n) = match n.v with
111       | Inf        -> true
112       | Fin i      -> 
113          Printf.printf "binder %s is %u but must be infinite\n" (P.string_of_mark k) i; true (**)
114       | Unk        -> n.v <- Inf; if !G.ct >= level then pp_table st; true
115       | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k) 
116    in
117    aux (resolve_layer st n)
118
119 (* Interface functions ******************************************************)
120
121 let initial_status () =
122    KH.create env_size
123
124 let refresh_status st = st 
125
126 let infinite = cell true Inf
127
128 let finite i = cell true (Fin i)
129
130 let one = finite 1
131
132 let two = finite 2
133
134 let rec unknown st =
135    if !G.ct >= level then warn "UNKNOWN";
136    let default = empty () in
137    let k = P.new_mark () in
138    let k, n = resolve_key_with_default st default k in
139    if n.s then match n.v with
140       | Inf
141       | Fin _ -> n
142       | Unk   -> if !G.ct >= level then pp_table st; cell true (Ref (k, 0))
143       | Ref _ -> assert false
144    else unknown st
145  
146 let minus st n j =
147    if !G.ct >= level then warn (Printf.sprintf "MINUS %u" j);
148    let rec aux k n j = match n.v with
149       | Inf              -> cell false n.v
150       | Fin i when i > j -> cell false (Fin (i - j))
151       | Fin _            -> cell false zero
152       | Unk              ->
153          if k = P.null_mark then assert false else generated st k j
154       | Ref (k, i)       -> 
155          let k, n = resolve_key st k in
156          aux k n (i+j)      
157    in
158    let k, n = resolve_layer st n in
159    aux k n j
160
161 let to_string st n =
162    let k, n = resolve_layer st n in
163    string_of_value k n.v
164
165 let assert_not_zero st n =
166    if !G.ct >= level then warn "ASSERT NOT ZERO";
167    let k, n = resolve_layer st n in
168    match n.b, n.v with
169       | true, _                -> n.b
170 (*      | _   , Fin i when i = 0 ->   
171          Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false *) (**)
172 (*      if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (P.string_of_mark k); *)      
173       | _                      -> n.b <- true; if !G.ct >= level then pp_table st; n.b
174
175 let assert_zero st n = assert_finite st n 0
176
177 let assert_equal st n1 n2 =
178    let k1, n1 = resolve_layer st n1 in
179    let k2, n2 = resolve_layer st n2 in
180    if n1 = n2 then true else
181    let b =
182       if not n1.b || assert_not_zero st n2 then match n1.v with
183          | Inf   -> assert_infinite st n2
184          | Fin i -> assert_finite st n2 i
185          | Unk   -> true
186          | Ref _ -> assert false
187       else false
188    in begin
189    if !G.ct >= level then warn "ASSERT EQUAL";
190    if b && k1 <> P.null_mark && k2 <> P.null_mark then begin
191       n1.v <- Ref (k2, 0); if !G.ct >= level then pp_table st
192    end; b end
193
194 let is_not_zero st n  =
195 (*   let _, n = resolve_layer st n in *) n.v <> zero
196
197 let are_equal st n1 n2 =
198 (*
199    let _, n1 = resolve_layer st n1 in
200    let _, n2 = resolve_layer st n2 in
201 *)
202    n1.v = n2.v