2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
12 (* kernel version: basic, relative, global *)
13 (* note : ufficial basic lambda-delta *)
17 type attrs = Entity.attrs
19 type bind = Void of attrs (* attrs *)
20 | Abst of attrs * term (* attrs, type *)
21 | Abbr of attrs * term (* attrs, body *)
23 and term = Sort of attrs * int (* attrs, hierarchy index *)
24 | LRef of attrs * int (* attrs, position index *)
25 | GRef of attrs * uri (* attrs, reference *)
26 | Cast of attrs * term * term (* attrs, type, term *)
27 | Appl of attrs * term * term (* attrs, argument, function *)
28 | Bind of bind * term (* binder, scope *)
30 type entity = term Entity.entity (* attrs, uri, binder *)
33 (* Cons: tail, relative local environment, binder *)
34 | Cons of lenv * lenv option * bind
36 (* helpers ******************************************************************)
39 String.concat "/" ["ld:"; "brg"; root; s ^ ".ld"]
41 (* Currified constructors ***************************************************)
43 let abst a w = Abst (a, w)
45 let abbr a v = Abbr (a, v)
47 let lref a i = LRef (a, i)
49 let cast a u t = Cast (a, u, t)
51 let appl a u t = Appl (a, u, t)
53 let bind b t = Bind (b, t)
55 let bind_abst a u t = Bind (Abst (a, u), t)
57 let bind_abbr a v t = Bind (Abbr (a, v), t)
59 (* local environment handling functions *************************************)
64 let es = Cons (es, c, b) in f es
67 let rec aux j = function
69 | Cons (tl, None, b) when j = 0 -> f tl b
70 | Cons (_, Some c, b) when j = 0 -> f c b
71 | Cons (tl, _, _) -> aux (pred j) tl
75 let rec rev_iter f map = function
77 | Cons (tl, None, b) ->
78 let f _ = map f tl b in rev_iter f map tl
79 | Cons (tl, Some c, b) ->
80 let f _ = map f c b in rev_iter f map tl
82 let rec fold_left f map x = function
85 let f x = fold_left f map x tl in