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.trace >= level then pp_table st; default
  89    end
  90
  91 let assert_finite st n j =
  92    if !G.trace >= 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.trace >= 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.trace >= 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.trace >= 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.trace >= 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.trace >= 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.trace >= 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.trace >= 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.trace >= 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.trace >= 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.trace >= 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