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 = {
+ g: Hierarchy.graph; (* sort hierarchy parameter *)
+ delta: bool; (* global delta-expansion *)
+ rt: bool; (* reference typing *)
+ si: bool; (* sort inclusion *)
+ expand: bool (* always expand global definitions *)
+}
(* helpers ******************************************************************)
+let common f (a, u, _) = f a u
+
let rec name err f = function
| Name (n, r) :: _ -> f n r
| _ :: tl -> name err f tl
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 g expand si = {
+ g = g; delta = false; rt = false; si = si; expand = expand
+}