-type uri = string
-type position = string
-type depth = string
-type sort = string
-
-type spec = MustObj of uri list * position list * depth list
- | MustSort of sort list * position list * depth list
- | MustRel of position list * depth list
- | OnlyObj of uri list * position list * depth list
- | OnlySort of sort list * position list * depth list
- | OnlyRel of position list * depth list
- | Universe of position list
-
-type builtin_t = MainHypothesis
- | InHypothesis
- | MainConclusion
- | InConclusion
- | InBody
- | Set
- | Prop
- | Type
-
-let text_of_builtin s =
- let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
- if s = ns ^ "MainHypothesis" then "$MH" else
- if s = ns ^ "InHypothesis" then "$IH" else
- if s = ns ^ "MainConclusion" then "$MC" else
- if s = ns ^ "InConclusion" then "$IC" else
- if s = ns ^ "InBody" then "$IB" else
- if s = "Set" then "$SET" else
- if s = "Prop" then "$PROP" else
- if s = "Type" then "$TYPE" else s
-
-let text_of_spec out l =
- let rec iter = function
- | [] -> ()
- | [s] -> out "\""; out (text_of_builtin s); out "\""
- | s :: tail -> out "\""; out (text_of_builtin s); out "\", "; iter tail
- in
- let txt_list l = out "{"; iter l; out "} " in
- let txt_spec = function
- | MustObj (u, p, d) -> out "mustobj "; txt_list u; txt_list p; txt_list d; out "\n"
- | MustSort (s, p, d) -> out "mustsort "; txt_list s; txt_list p; txt_list d; out "\n"
- | MustRel ( p, d) -> out "mustrel "; txt_list p; txt_list d; out "\n"
- | OnlyObj (u, p, d) -> out "onlyobj "; txt_list u; txt_list p; txt_list d; out "\n"
- | OnlySort (s, p, d) -> out "onlysort "; txt_list s; txt_list p; txt_list d; out "\n"
- | OnlyRel ( p, d) -> out "onlyrel "; txt_list p; txt_list d; out "\n"
- | Universe ( p ) -> out "universe "; txt_list p; out "\n"
- in
- List.iter txt_spec l
-