(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
-type uri = string
-type position = string
-type depth = string
-type sort = string
+(* interface for the low-level constraints *********************************)
-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
+val locate : string -> MathQL.query
-type builtin_t = MainHypothesis
- | InHypothesis
- | MainConclusion
- | InConclusion
- | InBody
- | Set
- | Prop
- | Type
+val unreferred : string -> string -> MathQL.query
-val locate : string -> MathQL.query
+val compose : MQGTypes.spec list -> MathQL.query
-val compose : spec list -> MathQL.query
+(* interface for the high-level constraints ********************************)
-val builtin : builtin_t -> string
-
-(* interface for the old constraints ***************************************)
-
-type old_depth = int option
-
-type r_obj = uri * position * old_depth
-type r_rel = position * old_depth
-type r_sort = position * old_depth * sort
-
-type must_restrictions = (r_obj list * r_rel list * r_sort list)
-type only_restrictions =
- (r_obj list option * r_rel list option * r_sort list option)
-type universe = position list option
-
-val query_of_constraints : universe -> must_restrictions -> only_restrictions -> MathQL.query
+val query_of_constraints : MQGTypes.universe option ->
+ MQGTypes.must_restrictions ->
+ MQGTypes.only_restrictions ->
+ MathQL.query