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 *)
18 type attr = Name of bool * id (* real?, name *)
19 | Apix of int (* additional position index *)
21 type attrs = attr list
23 type bind = Void (* exclusion *)
24 | Abst of term (* abstraction *)
25 | Abbr of term (* abbreviation *)
27 and term = Sort of attrs * int (* attrs, hierarchy index *)
28 | LRef of attrs * int (* attrs, position index *)
29 | GRef of attrs * uri (* attrs, reference *)
30 | Cast of attrs * term * term (* attrs, type, term *)
31 | Appl of attrs * term * term (* attrs, argument, function *)
32 | Bind of attrs * bind * term (* attrs, binder, scope *)
34 type obj = bind Item.obj (* age, uri, binder *)
36 type item = bind Item.item
39 (* Cons: tail, relative context, attrs, binder *)
40 | Cons of context * context option * attrs * bind
42 type message = (context, term) Log.item list
44 (* Currified constructors ***************************************************)
50 let lref a i = LRef (a, i)
52 let cast a u t = Cast (a, u, t)
54 let appl a u t = Appl (a, u, t)
56 let bind a b t = Bind (a, b, t)
58 let bind_abst a u t = Bind (a, Abst u, t)
60 let bind_abbr a v t = Bind (a, Abbr v, t)
62 (* context handling functions ***********************************************)
64 let empty_context = Null
66 let push f es ?c a b =
67 let es = Cons (es, c, a, b) in f es
70 let rec aux j = function
72 | Cons (tl, None, a, b) when j = 0 -> f tl a b
73 | Cons (_, Some c, a, b) when j = 0 -> f c a b
74 | Cons (tl, _, _, _) -> aux (pred j) tl
78 let rec rev_iter f map = function
80 | Cons (tl, None, a, b) ->
81 let f () = map f tl a b in rev_iter f map tl
82 | Cons (tl, Some c, a, b) ->
83 let f () = map f c a b in rev_iter f map tl
85 let rec fold_left f map x = function
87 | Cons (tl, _, a, b) ->
88 let f x = fold_left f map x tl in
91 let rec name err f = function
93 | Name (r, n) :: _ -> f n r
94 | _ :: tl -> name err f tl
96 let rec apix err f = function
99 | _ :: tl -> apix err f tl