(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.              
     \ /   This software is distributed as is, NO WARRANTY.              
      V_______________________________________________________________ *)

module KH = Hashtbl

module L = Log
module P = Marks
module G = Options

type value = Inf                 (* infinite layer *)
           | Fin of int          (* finite layer *)
           | Ref of P.mark * int (* referred layer, step *)
           | Unk                 (* no layer set *)

type layer = {
  mutable v: value; (* value *)  
          s: bool;  (* static layer? *)
  mutable b: bool;  (* beta allowed? *)
}

type status = (P.mark, layer) KH.t (* environment for layer variables *)

(* Internal functions *******************************************************)

let level = 7

let env_size = 1300

let warn s = L.warn (pred level) s

let zero = Fin 0

let string_of_value k = function
   | Inf        -> ""
   | Fin i      -> string_of_int i
   | Ref (k, i) -> "-" ^ P.string_of_mark k ^ "-" ^ string_of_int i
   | Unk        -> "-" ^ P.string_of_mark k

(* Note: remove assigned variables *)
let pp_table st =
   let map k n = 
      warn (Printf.sprintf "%s: v %s (s:%b b:%b)" 
         (P.string_of_mark k) (string_of_value k n.v) n.s n.b
      )
   in
   KH.iter map st 

let cell s v = {
   v = v; s = s; b = false
}

let empty () = cell true Unk

let dynamic k i = cell false (Ref (k, i))

let find_with_default st default k =
   try KH.find st k with Not_found -> KH.add st k default; default 

let find st k =
   try KH.find st k with Not_found -> assert false 

let rec resolve_key_with_default st default k = match find_with_default st default k with
   | {v = Ref (k, i)} when i = 0 -> resolve_key_with_default st default k
   | cell                        -> k, cell

let rec resolve_key st k = match find st k with
   | {v = Ref (k, i)} when i = 0 -> resolve_key st k
   | cell                        -> k, cell

let resolve_layer st = function
   | {v = Ref (k, i)} when i = 0 -> resolve_key st k
   | cell                        -> P.null_mark, cell

let rec generated st h i =
   let default = dynamic h i in
   let k = P.new_mark () in
   let k, n = resolve_key_with_default st default k in 
   if n.s then generated st h i else begin
      if n <> default then KH.replace st k default;
      if !G.trace >= level then pp_table st; default
   end

let assert_finite st n j =
   if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
   let rec aux (k, n) j = match n.v with    
      | Fin i when i = j -> true
      | Fin i            ->
         Printf.printf "binder %s is %u but must be %u\n" (P.string_of_mark k) i j; true (**)
      | Inf              ->
         Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; true (**)
      | Unk              -> n.v <- Fin j; if !G.trace >= level then pp_table st; true
      | Ref (k, i)       -> n.v <- Fin j; aux (resolve_key st k) (i+j) 
   in
   let k, n = resolve_layer st n in
(*   if j = 0 && n.b then begin
      Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false (**)
   end else *)
      aux (k, n) j

let assert_infinite st n =
   if !G.trace >= level then warn "ASSERT INFINITE";
   let rec aux (k, n) = match n.v with
      | Inf        -> true
      | Fin i      -> 
         Printf.printf "binder %s is %u but must be infinite\n" (P.string_of_mark k) i; true (**)
      | Unk        -> n.v <- Inf; if !G.trace >= level then pp_table st; true
      | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k) 
   in
   aux (resolve_layer st n)

(* Interface functions ******************************************************)

let initial_status () =
   KH.create env_size

let refresh_status st = st 

let infinite = cell true Inf

let finite i = cell true (Fin i)

let one = finite 1

let two = finite 2

let rec unknown st =
   if !G.trace >= level then warn "UNKNOWN";
   let default = empty () in
   let k = P.new_mark () in
   let k, n = resolve_key_with_default st default k in
   if n.s then match n.v with
      | Inf
      | Fin _ -> n
      | Unk   -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
      | Ref _ -> assert false
   else unknown st
 
let minus st n j =
   if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j);
   let rec aux k n j = match n.v with
      | Inf              -> cell false n.v
      | Fin i when i > j -> cell false (Fin (i - j))
      | Fin _            -> cell false zero
      | Unk              ->
         if k = P.null_mark then assert false else generated st k j
      | Ref (k, i)       -> 
         let k, n = resolve_key st k in
         aux k n (i+j)      
   in
   let k, n = resolve_layer st n in
   aux k n j

let to_string st n =
   let k, n = resolve_layer st n in
   string_of_value k n.v

let assert_not_zero st n =
   if !G.trace >= level then warn "ASSERT NOT ZERO";
   let k, n = resolve_layer st n in
   match n.b, n.v with
      | true, _                -> n.b
(*      | _   , Fin i when i = 0 ->   
         Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false *) (**)
(*      if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (P.string_of_mark k); *)      
      | _                      -> n.b <- true; if !G.trace >= level then pp_table st; n.b

let assert_zero st n = assert_finite st n 0

let assert_equal st n1 n2 =
   let k1, n1 = resolve_layer st n1 in
   let k2, n2 = resolve_layer st n2 in
   if n1 = n2 then true else
   let b =
      if not n1.b || assert_not_zero st n2 then match n1.v with
         | Inf   -> assert_infinite st n2
         | Fin i -> assert_finite st n2 i
         | Unk   -> true
         | Ref _ -> assert false
      else false
   in begin
   if !G.trace >= level then warn "ASSERT EQUAL";
   if b && k1 <> P.null_mark && k2 <> P.null_mark then begin
      n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st
   end; b end

let is_not_zero st n  =
   let _, n = resolve_layer st n in n.v <> zero