(*
    ||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_______________________________________________________________ *)

(* kernel version: basic, relative, global *)
(* note          : ufficial basic lambda-delta *) 

type uri = Item.uri
type id = Item.id

type attr = Name of bool * id  (* real?, name *)
          | Apix of int        (* additional position index *)

type attrs = attr list

type bind = Void         (* exclusion *)
          | Abst of term (* abstraction *)
          | Abbr of term (* abbreviation *)

and term = Sort of attrs * int         (* attrs, hierarchy index *)
         | LRef of attrs * int         (* attrs, position index *)
         | GRef of attrs * uri         (* attrs, reference *)
         | Cast of attrs * term * term (* attrs, type, term *)
         | Appl of attrs * term * term (* attrs, argument, function *)
         | Bind of attrs * bind * term (* attrs, binder, scope *)

type obj = bind Item.obj (* age, uri, binder *)

type item = bind Item.item

type context = Null
(* Cons: tail, relative context, attrs, binder *) 
             | Cons of context * context option * attrs * bind 

type message = (context, term) Log.item list

(* Currified constructors ***************************************************)

let abst w = Abst w

let abbr v = Abbr v

let lref a i = LRef (a, i)

let cast a u t = Cast (a, u, t)

let appl a u t = Appl (a, u, t)

let bind a b t = Bind (a, b, t)

let bind_abst a u t = Bind (a, Abst u, t)

let bind_abbr a v t = Bind (a, Abbr v, t)

(* context handling functions ***********************************************)

let empty_context = Null

let push f es ?c a b =
   let es = Cons (es, c, a, b) in f es

let get err f es i =
   let rec aux j = function
      | Null                               -> err i
      | Cons (tl, None, a, b)   when j = 0 -> f tl a b
      | Cons (_, Some c, a, b) when j = 0  -> f c a b
      | Cons (tl, _, _, _)                 -> aux (pred j) tl
   in
   aux i es

let rec rev_iter f map = function   
   | Null                    -> f ()
   | Cons (tl, None, a, b)   -> 
      let f () = map f tl a b in rev_iter f map tl
   | Cons (tl, Some c, a, b) -> 
      let f () = map f c a b in rev_iter f map tl

let rec fold_left f map x = function
   | Null               -> f x
   | Cons (tl, _, a, b) ->
      let f x = fold_left f map x tl in
      map f x a b

let rec name err f = function
   | []               -> err ()
   | Name (r, n) :: _ -> f n r
   | _ :: tl          -> name err f tl

let rec apix err f = function
   | []          -> err ()
   | Apix i :: _ -> f i
   | _ :: tl     -> apix err f tl