]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_generator/mQueryGenerator.mli
MathQL 1.3 ready for use
[helm.git] / helm / ocaml / mathql_generator / mQueryGenerator.mli
index eace22532b96f5a9f6fb1b9d5e82f3c3b663687b..c94dbcdb87809d376738b63caaf08bdb5c8f02a9 100644 (file)
 
 type uri = string
 type position = string
-type depth = int option
+type depth = string
 type sort = string 
 
-type r_obj = (uri * position * depth) 
-type r_rel = (position * depth)
-type r_sort = (position * depth * sort) 
+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
+
+val compose : spec list -> MathQL.query
+
+val builtin : MathQL.vvar -> 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 locate               : string -> MathQL.query
-
 val query_of_constraints : universe -> must_restrictions -> only_restrictions -> MathQL.query
-
-val builtin              : MathQL.vvar -> string