* 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 = "Set" then "$SET" else
- if s = "Prop" then "$PROP" else
- if s = "Type" then "$TYPE" else s
+ if s = ns ^ "Set" then "$SET" else
+ if s = ns ^ "Prop" then "$PROP" else
+ if s = ns ^ "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
- | MainHypothesis -> ns ^ "MainHypothesis"
- | InHypothesis -> ns ^ "InHypothesis"
- | MainConclusion -> ns ^ "MainConclusion"
- | InConclusion -> ns ^ "InConclusion"
- | InBody -> ns ^ "InBody"
- | Set -> "Set"
- | Prop -> "Prop"
- | Type -> "Type"
+ | "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")
(* conversion functions from the old constraints ***************************)