(*
    ||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 U = NUri
module C = Cps
module S = Share
module B = Brg
module E = BrgEnvironment

exception LRefNotFound of string Lazy.t

type bind = Void_
          | Abst_ of B.term
          | Abbr_ of B.term

type environment = int * bind list

type stack = B.term list

type context = {
   g: environment;
   l: environment;
   s: stack
}

type whd_result =
   | Sort_ of int
   | LRef_ of int * B.term option
   | GRef_ of int * B.bind * B.term
   | Bind_ of B.term * B.term

type ho_whd_result =
   | Sort of int
   | Abst of B.term

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

let empty_e = 0, []

let push_e f b (l, e) =
   f (succ l, b :: e)

let get_e f c i =
   let (gl, ge), (ll, le) = c.g, c.l in
   if i >= gl + ll then raise (LRefNotFound (lazy (string_of_int i)));
   let b =
      if i < gl then List.nth ge (gl - (succ i)) 
      else List.nth le (gl + ll - (succ i))
   in
   f b

let rec lref_map f map t = match t with
   | B.LRef i             -> f (B.LRef (map i))
   | B.GRef _             -> f t
   | B.Sort _             -> f t
   | B.Cast (w, u)        ->
      let f w' u' = f (S.sh2 w w' u u' t B.cast) in
      let f w' = lref_map (f w') map u in 
      lref_map f map w
   | B.Appl (w, u)        ->
      let f w' u' = f (S.sh2 w w' u u' t B.appl) in
      let f w' = lref_map (f w') map u in 
      lref_map f map w
   | B.Bind (id, b, w, u) ->
      let f w' u' = f (S.sh2 w w' u u' t (B.bind id b)) in
      let f w' = lref_map (f w') map u in 
      lref_map f map w

(* to share *)
let lift f c = 
   let (gl, _), (ll, le) = c.g, c.l in
   let map i = if i >= gl then succ i else i in
   let map f = function
      | Abbr_ t -> let f t' = f (Abbr_ t') in lref_map f map t
      | _       -> assert false
   in
   let f le' = f {c with l = (ll, le')} in
   C.list_map f map le

let xchg f c t =
   let (gl, _), (ll, _) = c.g, c.l in
   let map i =
      if i < gl || i > gl + ll then i else
      if i >= gl && i < gl + ll then succ i else gl
   in
   lref_map (f c) map t

(* to share *)
let rec whd f c t = match t with
   | B.Sort h                 -> f c (Sort_ h)
   | B.GRef uri               ->
      let f (i, _, b, t) = f c (GRef_ (i, b, t)) in
      E.get_obj f uri
   | B.LRef i                 ->
      let f = function
         | Void_   -> f c (LRef_ (i, None))
	 | Abst_ t -> f c (LRef_ (i, Some t))
	 | Abbr_ t -> whd f c t
      in
      get_e f c i
   | B.Appl (v, t)            -> whd f {c with s = v :: c.s} t   
   | B.Bind (_, B.Abbr, v, t) -> 
      let f l = whd f {c with l = l} t in
      push_e f (Abbr_ v) c.l
   | B.Bind (_, B.Abst, w, t) -> 
      begin match c.s with
         | []      -> f c (Bind_ (w, t))
	 | v :: tl -> 
	    let f tl l = whd f {c with l = l; s = tl} t in
	    push_e (f tl) (Abbr_ v) c.l
      end
   | B.Cast (_, t)            -> whd f c t

let push f c t = 
   assert (c.s = []);
   let f c g = xchg f {c with g = g} t in
   let f c = push_e (f c) Void_ c.g in
   lift f c 

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

let rec are_convertible f c1 t1 c2 t2 =
   let rec aux c1' r1 c2' r2 = match r1, r2 with
      | Sort_ h1, Sort_ h2                             -> f (h1 = h2)
      | LRef_ (i1, _), LRef_ (i2, _)                   ->
         if i1 = i2 then are_convertible_stacks f c1' c2' else f false
      | GRef_ (a1, B.Abst, _), GRef_ (a2, B.Abst, _)   ->
         if a1 = a2 then are_convertible_stacks f c1' c2' else f false
      | GRef_ (a1, B.Abbr, v1), GRef_ (a2, B.Abbr, v2) ->
         if a1 = a2 then are_convertible_stacks f c1' c2' else
	 if a1 < a2 then whd (aux c1' r1) c2' v2 else
	 whd (aux_rev c2' r2) c1' v1
      | _, GRef_ (_, B.Abbr, v2)                       ->
         whd (aux c1' r1) c2' v2
      | GRef_ (_, B.Abbr, v1), _                       ->
	 whd (aux_rev c2' r2) c1' v1
      | Bind_ (w1, t1), Bind_ (w2, t2)                 ->
         let f b = 
	    if b then 
	       let f c1'' t1' = push (are_convertible f c1'' t1') c2' t2 in
               push f c1' t1
	    else f false
	 in
	 are_convertible f c1' w1 c2' w2
      | _                                              -> f false
   and aux_rev c2 r2 c1 r1 = aux c1 r1 c2 r2 in
   let f c1' r1 = whd (aux c1' r1) c2 t2 in 
   whd f c1 t1

and are_convertible_stacks f c1 c2 =
   let map f v1 v2 = are_convertible f c1 v1 c2 v2 in
   if List.length c1.s <> List.length c2.s then f false else
   C.forall2 f map c1.s c2.s

let are_convertible f c t1 t2 = are_convertible f c t1 c t2

let rec ho_whd f c t =
   let aux c' = function
      | Sort_ h           -> f c' (Sort h)
      | Bind_ (w, t)      -> f c' (Abst w)
      | LRef_ (_, Some w) -> ho_whd f c w
      | GRef_ (_, _, u)   -> ho_whd f c u
      | LRef_ (_, None)   -> assert false
   in
   whd aux c t

let push f c b t = 
   assert (c.l = empty_e && c.s = []);
   let f g = f {c with g = g} in
   let b = match b with
      | B.Abbr -> Abbr_ t
      | B.Abst -> Abst_ t
   in
   push_e f b c.g

let get f c i =
   let gl, ge = c.g in
   if i >= gl then raise (LRefNotFound (lazy (string_of_int i)));
   match List.nth ge (gl - (succ i)) with
      | Abbr_ v -> f (B.Abbr, v)
      | Abst_ w -> f (B.Abst, w)
      | Void_   -> assert false

let empty_context = {
   g = empty_e; l = empty_e; s = []
}