mathQL.ml updated

[helm.git] / helm / gTopLevel / mquery.ml

diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml
index 0cf33c83cc155bff55f1abd37db3146422b35e07..f31fccd07c25a8d16f932c93fec775d9c7f3131d 100644 (file)
--- a/helm/gTopLevel/mquery.ml
+++ b/helm/gTopLevel/mquery.ml
@@ -72,8 +72,8 @@ let out_func = function
 
 let out_str = function
    | MQCons s      -> con s
-   | MQRVar s      -> out_rvar s
-   | MQSVar s      -> out_svar s
+   | MQSRVar s      -> out_rvar s
+   | MQSSVar s      -> out_svar s
    | MQFunc (f, r) -> out_func f ^ out_rvar r
    | MQMConclusion -> key "mainconclusion" 
    | MQConclusion  -> key "conclusion" 
@@ -98,7 +98,10 @@ and out_list = function
    | MQPattern p -> key "pattern" ^ out_pat p
    | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")"
    | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")"
-   | MQRVarOccur v -> key "rvaroccur" ^ v
+   | MQLRVar v -> key "rvaroccur" ^ v
+   | MQLetIn (v, l1, l2) ->
+      key "let " ^ out_rvar v ^ " = " ^ out_list l1 ^ key " in " ^ out_list l2
+   | MQLetRef v -> out_rvar v
 
 let out_query = function
    | MQList l -> out_list l
@@ -187,7 +190,6 @@ let rec inspect_term main l v = function
    | Meta (i, _)                  -> l
    | Sort s                       -> l 
    | Implicit                     -> l 
-   | Abst u                       -> l 
    | Var u                        -> inspect_uri main l u None None v
    | Const (u, i)                 -> inspect_uri main l u None None v
    | MutInd (u, i, t)             -> inspect_uri main l u (Some t) None v
@@ -245,7 +247,7 @@ let build_select (r, b, v) n =
    let mqs = if b then MQMConclusion else MQConclusion in
    MQSelect (rvar, 
              MQUse (MQPattern r, svar),
-             MQIs (MQSVar svar, mqs)
+             MQIs (MQSSVar svar, mqs)
             )
 
 let rec build_inter n = function
@@ -270,18 +272,21 @@ let restrict_universe query =
       in
        compose_universe !universe
      in
-      MQSelect (
-       "uri", query,
-        MQSubset (
-         MQSelect (
-          "uri2",
-          MQUsedBy (MQRVarOccur "uri", "pos"),
-          MQOr (
-           MQIs (MQSVar "pos", MQConclusion),
-           MQIs (MQSVar "pos", MQMConclusion)
+      MQLetIn (
+       "universe",universe,
+        MQSelect (
+         "uri", query,
+          MQSubset (
+           MQSelect (
+            "uri2",
+            MQUsedBy (MQLRVar "uri", "pos"),
+            MQOr (
+             MQIs (MQSSVar "pos", MQConclusion),
+             MQIs (MQSSVar "pos", MQMConclusion)
+            )
+           ),
+           MQLetRef "universe"
           )
-         ),
-         universe
         )
       )
 ;;