New query implementation using LetIn.

Some benchmarks:

Query: 2*n <= 2*m

Results:

  No-LetIn     LetIn  Output
 1: 23s   >>>>  3s    9uri        uri/s: 3
 0: 276s  >>>> 14s   48uri        uri/s: 3.42

Open BUGs:
 the implementation of the LetIn scope is surely not correct. The whole
 semantics is wrong in case of repeated names.

diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml
index 093f0228cfc7b7696010b6610b4305808838f435..f31fccd07c25a8d16f932c93fec775d9c7f3131d 100644 (file)
--- a/helm/gTopLevel/mquery.ml
+++ b/helm/gTopLevel/mquery.ml
@@ -99,6 +99,9 @@ and out_list = function
    | 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 ")"
    | 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
@@ -269,18 +272,21 @@ let restrict_universe query =
       in
        compose_universe !universe
      in
-      MQSelect (
-       "uri", query,
-        MQSubset (
-         MQSelect (
-          "uri2",
-          MQUsedBy (MQLRVar "uri", "pos"),
-          MQOr (
-           MQIs (MQSSVar "pos", MQConclusion),
-           MQIs (MQSSVar "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
         )
       )
 ;;