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 IFDEF TRACE THEN
  48
  49 (* Note: remove assigned variables *)
  50 let pp_table st =
  51    let map k n =
  52       warn (Printf.sprintf "%s: v %s (s:%b b:%b)"
  53          (P.string_of_mark k) (string_of_value k n.v) n.s n.b
  54       )
  55    in
  56    KH.iter map st
  57
  58 END
  59
  60 let cell s v = {
  61    v = v; s = s; b = false
  62 }
  63
  64 let empty () = cell true Unk
  65
  66 let dynamic k i = cell false (Ref (k, i))
  67
  68 let find_with_default st default k =
  69    try KH.find st k with Not_found -> KH.add st k default; default
  70
  71 let find st k =
  72    try KH.find st k with Not_found -> assert false
  73
  74 let rec resolve_key_with_default st default k = match find_with_default st default k with
  75    | {v = Ref (k, i)} when i = 0 -> resolve_key_with_default st default k
  76    | cell                        -> k, cell
  77
  78 let rec resolve_key st k = match find st k with
  79    | {v = Ref (k, i)} when i = 0 -> resolve_key st k
  80    | cell                        -> k, cell
  81
  82 let resolve_layer st = function
  83    | {v = Ref (k, i)} when i = 0 -> resolve_key st k
  84    | cell                        -> P.null_mark, cell
  85
  86 let rec generated st h i =
  87    let default = dynamic h i in
  88    let k = P.new_mark () in
  89    let k, n = resolve_key_with_default st default k in
  90    if n.s then generated st h i else begin
  91       if n <> default then KH.replace st k default;
  92 IFDEF TRACE THEN
  93       if !G.ct >= level then pp_table st
  94 ELSE () END;
  95       default
  96    end
  97
  98 let assert_finite st n j =
  99 IFDEF TRACE THEN
 100    if !G.ct >= level then warn (Printf.sprintf "ASSERT FINITE %u" j)
 101 ELSE () END;
 102    let rec aux (k, n) j = match n.v with
 103       | Fin i when i = j -> true
 104       | Fin i            ->
 105          Printf.printf "binder %s is %u but must be %u\n" (P.string_of_mark k) i j; true (**)
 106       | Inf              ->
 107          Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; true (**)
 108       | Unk              ->
 109          n.v <- Fin j;
 110 IFDEF TRACE THEN
 111          if !G.ct >= level then pp_table st
 112 ELSE () END;
 113          true
 114       | Ref (k, i)       -> n.v <- Fin j; aux (resolve_key st k) (i+j)
 115    in
 116    let k, n = resolve_layer st n in
 117 (*   if j = 0 && n.b then begin
 118       Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false (**)
 119    end else *)
 120       aux (k, n) j
 121
 122 let assert_infinite st n =
 123 IFDEF TRACE THEN
 124    if !G.ct >= level then warn "ASSERT INFINITE"
 125 ELSE () END;
 126    let rec aux (k, n) = match n.v with
 127       | Inf        -> true
 128       | Fin i      ->
 129          Printf.printf "binder %s is %u but must be infinite\n" (P.string_of_mark k) i; true (**)
 130       | Unk        ->
 131          n.v <- Inf;
 132 IFDEF TRACE THEN
 133          if !G.ct >= level then pp_table st
 134 ELSE () END;
 135          true
 136       | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k)
 137    in
 138    aux (resolve_layer st n)
 139
 140 (* Interface functions ******************************************************)
 141
 142 let initial_status () =
 143    KH.create env_size
 144
 145 let refresh_status st = st
 146
 147 let infinity = cell true Inf
 148
 149 let finite i = cell true (Fin i)
 150
 151 let one = finite 1
 152
 153 let two = finite 2
 154
 155 let rec unknown st =
 156 IFDEF TRACE THEN
 157    if !G.ct >= level then warn "UNKNOWN"
 158 ELSE () END;
 159    let default = empty () in
 160    let k = P.new_mark () in
 161    let k, n = resolve_key_with_default st default k in
 162    if n.s then match n.v with
 163       | Inf
 164       | Fin _ -> n
 165       | Unk   ->
 166 IFDEF TRACE THEN
 167          if !G.ct >= level then pp_table st
 168 ELSE () END;
 169          cell true (Ref (k, 0))
 170       | Ref _ -> assert false
 171    else unknown st
 172
 173 let minus st n j =
 174 IFDEF TRACE THEN
 175    if !G.ct >= level then warn (Printf.sprintf "MINUS %u" j)
 176 ELSE () END;
 177    let rec aux k n j = match n.v with
 178       | Inf              -> cell false n.v
 179       | Fin i when i > j -> cell false (Fin (i - j))
 180       | Fin _            -> cell false zero
 181       | Unk              ->
 182          if k = P.null_mark then assert false else generated st k j
 183       | Ref (k, i)       ->
 184          let k, n = resolve_key st k in
 185          aux k n (i+j)
 186    in
 187    let k, n = resolve_layer st n in
 188    aux k n j
 189
 190 let to_string st n =
 191    let k, n = resolve_layer st n in
 192    string_of_value k n.v
 193
 194 let assert_not_zero st n =
 195 IFDEF TRACE THEN
 196    if !G.ct >= level then warn "ASSERT NOT ZERO"
 197 ELSE () END;
 198    let k, n = resolve_layer st n in
 199    match n.b, n.v with
 200       | true, _ -> n.b
 201 (*      | _   , Fin i when i = 0 ->
 202          Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false *) (**)
 203 (*      if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (P.string_of_mark k); *)
 204       | _       ->
 205          n.b <- true;
 206 IFDEF TRACE THEN
 207          if !G.ct >= level then pp_table st
 208 ELSE () END;
 209          n.b
 210
 211 let assert_zero st n = assert_finite st n 0
 212
 213 let assert_equal st n1 n2 =
 214    let k1, n1 = resolve_layer st n1 in
 215    let k2, n2 = resolve_layer st n2 in
 216    if n1 = n2 then true else
 217    let b =
 218       if not n1.b || assert_not_zero st n2 then match n1.v with
 219          | Inf   -> assert_infinite st n2
 220          | Fin i -> assert_finite st n2 i
 221          | Unk   -> true
 222          | Ref _ -> assert false
 223       else false
 224    in
 225 IFDEF TRACE THEN
 226    if !G.ct >= level then warn "ASSERT EQUAL"
 227 ELSE () END;
 228    if b && k1 <> P.null_mark && k2 <> P.null_mark then begin
 229       n1.v <- Ref (k2, 0);
 230 IFDEF TRACE THEN
 231       if !G.ct >= level then pp_table st
 232 ELSE () END
 233    end; b
 234
 235 let is_not_zero st n  =
 236 (*   let _, n = resolve_layer st n in *) n.v <> zero
 237
 238 let are_equal st n1 n2 =
 239 (*
 240    let _, n1 = resolve_layer st n1 in
 241    let _, n2 = resolve_layer st n2 in
 242 *)
 243    n1.v = n2.v