From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 18 Jun 2002 13:00:43 +0000 (+0000)
Subject: New query implementation using LetIn.
X-Git-Tag: V_0_3_0_debian_8~37
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cae32e92127664318d52b0cc8884a69a2892f6ba;p=helm.git

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 093f0228c..f31fccd07 100644
--- 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
         )
       )
 ;;