(*
    ||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: dual, relative, global *)
(* note          : fragment of dual lambda-delta serving as abstract layer *) 

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

type attr = Name of id * bool  (* name, real? *)
	  | Priv               (* private global definition *)

type attrs = attr list (* attributes *)

type bind = Abst of attrs * term (* attrs, domain *)
          | Abbr of attrs * term (* attrs, body   *)
          | Void of attrs        (* attrs         *)

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, domain, element *)
         | Proj of attrs * lenv * term      (* attrs, closure, scope *)
         | Appl of attrs * term list * term (* attrs, arguments, function *)
	 | Bind of bind * term              (* binder, scope *)

and lenv = bind list (* local environment *)

type entry = bind Entity.entry (* age, uri, binder *)

type entity = bind Entity.entity

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

let mk_uri root f s =
   let str = String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"] in
   f str

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

let name_of_binder err f = function
   | Abst (a, _) -> name_of err f a
   | Abbr (a, _) -> name_of err f a
   | Void a      -> name_of err f a

let resolve_lref err f id lenv =
   let rec aux f i = function
     | []      -> err ()
     | b :: tl ->
        let err () = aux f (succ i) tl in
	let f name _ = if name = id then f i else err () in
	name_of_binder err f b
   in
   aux f 0 lenv