* http://cs.unibo.it/helm/.
*)
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
type uri = string
type position = string
type depth = string
| 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 ^ "MainConclusion" then "$MC" else
if s = ns ^ "InConclusion" then "$IC" else
if s = ns ^ "InBody" then "$IB" else
- if s = ns ^ "Set" then "$SET" else
- if s = ns ^ "Prop" then "$PROP" else
- if s = ns ^ "Type" then "$TYPE" else s
+ 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
let builtin s =
let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
match s with
- | "MH" -> ns ^ "MainHypothesis"
- | "IH" -> ns ^ "InHypothesis"
- | "MC" -> ns ^ "MainConclusion"
- | "IC" -> ns ^ "InConclusion"
- | "IB" -> ns ^ "InBody"
- | "SET" -> ns ^ "Set"
- | "PROP" -> ns ^ "Prop"
- | "TYPE" -> ns ^ "Type"
- | _ -> raise (Failure "MQueryGenerator.builtin")
+ | MainHypothesis -> ns ^ "MainHypothesis"
+ | InHypothesis -> ns ^ "InHypothesis"
+ | MainConclusion -> ns ^ "MainConclusion"
+ | InConclusion -> ns ^ "InConclusion"
+ | InBody -> ns ^ "InBody"
+ | Set -> "Set"
+ | Prop -> "Prop"
+ | Type -> "Type"
(* conversion functions from the old constraints ***************************)