type 'term bind = Abst of 'term (* declaration: domain *)
| Abbr of 'term (* definition: body *)
+ | Void (* exclusion *)
type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *)
-type uri_generator = string -> string (* this could be in CPS *)
+type uri_generator = string -> string
+
+type status = {
+ delta: bool; (* global delta-expansion *)
+ rt: bool; (* reference typing *)
+ si: bool (* sort inclusion *)
+}
(* helpers ******************************************************************)
let f t = f (a, uri, Abst t) in xlate_term f t
| a, uri, Abbr t ->
let f t = f (a, uri, Abbr t) in xlate_term f t
+ | _, _, Void ->
+ assert false
+
+let initial_status si = {
+ delta = false; rt = false; si = si
+}