+++ /dev/null
-(*
- ||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_______________________________________________________________ *)
-
-module O = Options
-
-type uri = NUri.uri
-type id = Aut.id
-type name = id * bool (* token, real? *)
-
-type names = name list
-
-type attr = Name of name (* name *)
- | Apix of int (* additional position index *)
- | Mark of int (* node marker *)
- | Meta of string (* metaliguistic annotation *)
- | Priv (* private global definition *)
-
-type attrs = attr list (* attributes *)
-
-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 status = {
- 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
- | [] -> err ()
-
-let names f map l a =
- let rec aux f i a = function
- | [] -> f a
- | Name (n, r) :: tl -> aux (map f i n r) false a tl
- | _ :: tl -> aux f i a tl
- in
- aux f true a l
-
-let rec get_name err f j = function
- | [] -> err ()
- | Name (n, r) :: _ when j = 0 -> f n r
- | Name _ :: tl -> get_name err f (pred j) tl
- | _ :: tl -> get_name err f j tl
-
-let rec get_names f = function
- | [] -> f [] []
- | Name _ as n :: tl ->
- let f a ns = f a (n :: ns) in get_names f tl
- | e :: tl ->
- let f a = f (e :: a) in get_names f tl
-
-let count_names a =
- let rec aux k = function
- | [] -> k
- | Name _ :: tl -> aux (succ k) tl
- | _ :: tl -> aux k tl
- in
- aux 0 a
-
-let rec apix err f = function
- | Apix i :: _ -> f i
- | _ :: tl -> apix err f tl
- | [] -> err ()
-
-let rec mark err f = function
- | Mark i :: _ -> f i
- | _ :: tl -> mark err f tl
- | [] -> err ()
-
-let rec priv err f = function
- | Priv :: _ -> f ()
- | _ :: tl -> priv err f tl
- | [] -> err ()
-
-let rec meta err f = function
- | Meta s :: _ -> f s
- | _ :: tl -> meta err f tl
- | [] -> err ()
-
-let resolve err f name a =
- let rec aux i = function
- | Name (n, true) :: _ when n = name -> f i
- | _ :: tl -> aux (succ i) tl
- | [] -> err i
- in
- aux 0 a
-
-let rec rev_append_names ns = function
- | [] -> ns
- | Name n :: tl -> rev_append_names (n :: ns) tl
- | _ :: tl -> rev_append_names ns tl
-
-let xlate f xlate_term = function
- | a, uri, Abst t ->
- 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 () = {
- delta = false; rt = false; si = !O.si; expand = !O.expand
-}
-
-let refresh_status st = {st with
- si = !O.si; expand = !O.expand
-}
-