(*
    ||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, absolute, global *)
(* note          : experimental *) 

type uri = Entity.uri
type id = Entity.id

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

and term = Sort of int                    (* hierarchy index *)
         | LRef of int                    (* location *)
         | GRef of uri                    (* reference *)
         | Cast of term * term            (* domain, element *)
         | Appl of term * term            (* argument, function *)
         | Bind of int * id * bind * term (* location, name, binder, scope *)

type entity = term Entity.entity (* attrs, uri, binder *)

type lenv = (int * id * bind) list (* location, name, binder *) 

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

(* helpers ******************************************************************)

let mk_uri root s =
   String.concat "/" ["ld:"; "bag"; root; s ^ ".ld"]

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

let abst w = Abst w

let abbr v = Abbr v

let lref i = LRef i

let cast u t = Cast (u, t)

let appl u t = Appl (u, t)

let bind l id b t = Bind (l, id, b, t)

let bind_abst l id u t = Bind (l, id, Abst u, t)

let bind_abbr l id v t = Bind (l, id, Abbr v, t)

(* location handling functions **********************************************)

let location = ref 0

let new_location () = let loc = !location in incr location; loc

let locations () = !location

(* local environment handling functions *************************************)

let empty_lenv = []

let push msg f es l id b =
   let rec does_not_occur loc = function
      | []                          -> true
      | (l, _, _) :: _ when l = loc -> false
      | _ :: es                     -> does_not_occur l es
   in
   if not (does_not_occur l es) then failwith msg else
   let c = (l, id, b) :: es in f c

let append f es1 es2 = 
   f (List.append es2 es1)

let map f map es =
   Cps.list_map f map es

let contents f es = f es

let get f es i =
   let rec aux = function
      | []               -> f None
      | (l, id, b) :: tl -> if l = i then f (Some (id, b)) else aux tl
   in
   aux es