(*
    ||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 L = Log
module B = Brg
module E = BrgEnvironment

type environment = int * B.bind list

type stack = B.term list

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

exception LRefNotFound of (context, B.term) L.item list

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

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

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

let error i = raise (LRefNotFound (L.items1 (string_of_int i)))

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 error 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_bind f map b = match b with
   | B.Abbr v ->
      let f v' = f (S.sh1 v v' b B.abbr) in
      lref_map f map v      
   | B.Abst w ->
      let f w' = f (S.sh1 w w' b B.abst) in
      lref_map f map w
   | B.Void   -> f b

and 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, u) ->
      let f b' u' = f (S.sh2 b b' u u' t (B.bind id)) in
      let f b' = lref_map (f b') map u in 
      lref_map_bind f map b

(* 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
      | B.Abbr t -> let f t' = f (B.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) = f c (GRef_ (i, b)) in
      E.get_obj f uri
   | B.LRef i                ->
      let f = function
         | B.Void   -> f c (LRef_ (i, None))
	 | B.Abst t -> f c (LRef_ (i, Some t))
	 | B.Abbr t -> whd f c t
      in
      get_e f c i
   | B.Cast (_, t)           -> whd f c t
   | B.Appl (v, t)           -> whd f {c with s = v :: c.s} t   
   | 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) (B.Abbr v) c.l
      end
   | B.Bind (_, b, t) -> 
      let f l = whd f {c with l = l} t in
      push_e f b c.l

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) B.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_ (_, B.Abst u) -> ho_whd f c u
      | GRef_ (_, B.Abbr u) -> ho_whd f c u
      | LRef_ (_, None)     -> assert false
      | GRef_ (_, B.Void)   -> assert false
   in
   whd aux c t

let push f c b = 
   assert (c.l = empty_e && c.s = []);
   let f g = f {c with g = g} in
   push_e f b c.g

let get f c i =
   let gl, ge = c.g in
   if i >= gl then error i;
   f (List.nth ge (gl - (succ i)))

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

let iter f map c =
   let _, ge = c.g in   
   C.list_iter f map ge