(*
    ||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 S  = Share
module L  = Log
module G  = Options
module H  = Hierarchy
module N  = Layer
module E  = Entity
module O  = Output
module B  = Brg
module BO = BrgOutput
module BE = BrgEnvironment

type rtm = {
   e: B.lenv;                 (* environment              *)
   s: (B.lenv * B.term) list; (* stack                    *)
   l: int;                    (* level                    *)
   d: int;                    (* inferred type iterations *)
   n: int option;             (* expected type iterations *)
}

type message = (rtm, B.term) L.message

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

let level = 5

let sublevel = succ level

let log1 st s c t =
   let s1, s2 = s ^ " in the environment", "the term" in
   L.log st BO.specs (pred level) (L.et_items1 s1 c s2 t)

let log2 st s cu u ct t =
   let s1, s2, s3 = s ^ " in the environment (expected)", "the term", "and in the environment (inferred)" in
   L.log st BO.specs (pred level) (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)

let rec list_and map = function
   | hd1 :: tl1, hd2 :: tl2 ->
      if map hd1 hd2 then list_and map (tl1, tl2) else false
   | l1, l2                 -> l1 = l2

let zero = Some 0

(* check closure *)
let are_alpha_convertible err f t1 t2 =
   let rec aux f = function
      | B.Sort (_, p1), B.Sort (_, p2)
      | B.LRef (_, p1), B.LRef (_, p2)         ->
         if p1 = p2 then f () else err ()
      | B.GRef (_, u1), B.GRef (_, u2)         ->
         if U.eq u1 u2 then f () else err ()
      | B.Cast (_, v1, t1), B.Cast (_, v2, t2)         
      | B.Appl (_, v1, t1), B.Appl (_, v2, t2) ->
         let f _ = aux f (t1, t2) in
	 aux f (v1, v2)
      | B.Bind (_, b1, t1), B.Bind (_, b2, t2) ->
         let f _ = aux f (t1, t2) in
	 aux_bind f (b1, b2)
      | _                                      -> err ()
   and aux_bind f = function
      | B.Abbr v1, B.Abbr v2                          -> aux f (v1, v2)
      | B.Abst (n1, v1), B.Abst (n2, v2) when n1 = n2 -> aux f (v1, v2)
      | B.Void, B.Void                                -> f ()
      | _                                             -> err ()
   in
   if S.eq t1 t2 then f () else aux f (t1, t2)

let assert_tstep m vo = match m.n with
   | Some n -> n > m.d
   | None   -> vo

let tstep m = {m with d = succ m.d}

let tsteps m = match m.n with
   | Some n when n > m.d -> n - m.d
   | _                   -> 0

let get m i =
   let _, c, a, b = B.get m.e i in c, a, b

(* to share *)
let rec step st m x = 
   if !G.trace >= sublevel then 
   log1 st (Printf.sprintf "entering R.step: l:%u d:%i n:%s" m.l m.d (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e x;
   match x with
   | B.Sort (a, h)                ->
      if assert_tstep m false then
         step st (tstep m) (B.Sort (a, H.apply h))      
      else m, x, None
   | B.GRef (_, uri)              ->
      begin match BE.get_entity uri with
         | _, _, _, E.Abbr v ->
            if m.n = None || !G.expand then begin
	       if !G.summary then O.add ~gdelta:1 ();
               step st m v
            end else
	       m, x, Some v
         | _, _, _, E.Abst w ->
            if assert_tstep m true then begin
               if !G.summary then O.add ~grt:1 (); 
               step st (tstep m) w
            end else
	     m, x, None   
	 | _, _, _, E.Void   ->
            assert false
      end
   | B.LRef (_, i)                ->
      begin match get m i with
	 | c, _, B.Abbr v      ->
	    if !G.summary then O.add ~ldelta:1 ();
	    step st {m with e = c} v
	 | c, a, B.Abst (_, w) ->
            if assert_tstep m true then begin
               if !G.summary then O.add ~lrt:1 ();
               step st {(tstep m) with e = c} w
            end else
	       m, B.LRef (a, i), None
	 | _, _, B.Void        ->
	    assert false
      end
   | B.Cast (_, u, t)             ->
      if assert_tstep m false then begin
         if !G.summary then O.add ~e:1 ();
         step st (tstep m) u
      end else begin
         if !G.summary then O.add ~epsilon:1 ();
         step st m t
      end
   | B.Appl (_, v, t)             ->
      step st {m with s = (m.e, v) :: m.s} t   
   | B.Bind (a, B.Abst (n, w), t) ->
      let i = tsteps m in
      let n = if i = 0 then n else N.minus st n i in
      if !G.si || N.is_not_zero st n then begin match m.s with
         | []          ->
            if i = 0 then m, x, None else
            m, B.Bind (a, B.Abst (n, w), t), None
	 | (c, v) :: s ->
            if !G.cc && not (N.assert_not_zero st n) then assert false;
	    if !G.summary then O.add ~beta:1 ~theta:(List.length s) ();
	    let v = if assert_tstep m false then B.Cast (E.empty_node, w, v) else v in
            let e = B.push m.e c a (B.abbr v) in
	    step st {m with e = e; s = s} t
      end else begin
         if !G.summary then O.add ~upsilon:1 ();
         let e = B.push m.e m.e a B.Void in 
         step st {m with e = e} t
      end
   | B.Bind (a, b, t)        ->
      if !G.summary then O.add ~theta:(List.length m.s) ();
      let e = B.push m.e m.e a b in 
      step st {m with e = e} t

let reset m ?(e=m.e) n =
   {m with e = e; n = n; s = []; d = 0} 

let assert_iterations m1 m2 = match m1.n, m2.n with
      | Some n1, Some n2 -> n1 - m1.d = n2 - m2.d
      | _                -> false 

let push m a b = 
   let a, l = match b with
      | B.Abst _ -> {a with E.n_apix = m.l}, succ m.l
      | _        -> a, m.l
   in
   let e = B.push m.e m.e a b in
   {m with e = e; l = l}

let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
   if !G.trace >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2;
   match t1, r1, t2, r2 with
      | B.Sort (_, h1), _, B.Sort (_, h2), _         ->
         h1 = h2
      | B.LRef ({E.n_apix = e1}, _), _, 
        B.LRef ({E.n_apix = e2}, _), _               ->
	 if e1 = e2 then ac_stacks st m1 m2 else false
      | B.GRef (_, u1), None, B.GRef (_, u2), None   ->
	 if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false
      | B.GRef ({E.n_apix = e1}, u1), Some v1, 
        B.GRef ({E.n_apix = e2}, u2), Some v2        ->
         if e1 < e2 then begin 
            if !G.summary then O.add ~gdelta:1 ();
	    ac_nfs st (m1, t1, r1) (step st m2 v2)
	 end else if e2 < e1 then begin
	    if !G.summary then O.add ~gdelta:1 ();
	    ac_nfs st (step st m1 v1) (m2, t2, r2) 
         end else if U.eq u1 u2 && assert_iterations m1 m2 && ac_stacks st m1 m2 then true
         else begin
	    if !G.summary then O.add ~gdelta:2 ();
	    ac st m1 v1 m2 v2
         end 
      | _, _, B.GRef _, Some v2                      ->
         if !G.summary then O.add ~gdelta:1 ();
	 ac_nfs st (m1, t1, r1) (step st m2 v2)
      | B.GRef _, Some v1, _, _                      ->
	 if !G.summary then O.add ~gdelta:1 ();
	 ac_nfs st (step st m1 v1) (m2, t2, r2)
      | B.Bind (a1, (B.Abst (n1, w1) as b1), t1), _, 
        B.Bind (a2, (B.Abst (n2, w2) as b2), t2), _  ->
	 if !G.cc && not (N.assert_equal st n1 n2) then false else
         if ac st (reset m1 zero) w1 (reset m2 zero) w2 then
	    ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
	 else false
      | B.Sort _, _, B.Bind (a, B.Abst (n, _), t), _ ->
         if !G.si then
            if !G.cc && not (N.assert_zero st n) then false else begin
	    if !G.summary then O.add ~upsilon:1 ();
	    ac st (push m1 a B.Void) t1 (push m2 a B.Void) t end
         else false
      | _                                            -> false

and ac st m1 t1 m2 t2 =
(*   L.warn "entering R.are_convertible"; *)
   ac_nfs st (step st m1 t1) (step st m2 t2)

and ac_stacks st m1 m2 =
(*   L.warn "entering R.are_convertible_stacks"; *)
   if List.length m1.s <> List.length m2.s then false else
   let map (c1, v1) (c2, v2) =
      let m1, m2 = reset m1 ~e:c1 zero, reset m2 ~e:c2 zero in
      ac st m1 v1 m2 v2
   in
   list_and map (m1.s, m2.s)

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

let empty_rtm = { 
   e = B.empty; s = []; l = 0; d = 0; n = None
}

let get m i =
   assert (m.s = []);
   let _, _, _, b = B.get m.e i in b

let xwhd st m n t =
   if !G.trace >= level then log1 st "Now scanning" m.e t;   
   let m, t, _ = step st (reset m n) t in
   m, t

let are_convertible st m1 n1 t1 m2 n2 t2 = 
   if !G.trace >= level then log2 st "Now converting" m1.e t1 m2.e t2;
   let r = ac st (reset m1 n1) t1 (reset m2 n2) t2 in
   r
(*    let err _ = in 
      if S.eq mu mw then are_alpha_convertible err f u w else err () *)

(* error reporting **********************************************************)

let pp_term st m och t = BO.specs.L.pp_term st m.e och t

let pp_lenv st och m = BO.specs.L.pp_lenv st och m.e

let specs = {
   L.pp_term = pp_term; L.pp_lenv = pp_lenv
}