From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 18 Jun 2002 17:42:23 +0000 (+0000)
Subject: updated for the new version of mathQL.ml
X-Git-Tag: V_0_3_0_debian_8~32
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=b855d2cee134386df462125b5a395f0063c7a93e

updated for the new version of mathQL.ml
---

diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml
index f31fccd07..3e5548c68 100644
--- 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
-   | MQSRVar s      -> out_rvar s
-   | MQSSVar s      -> out_svar s
+   | MQStringRVar s      -> out_rvar s
+   | MQStringSVar s      -> out_svar s
    | MQFunc (f, r) -> out_func f ^ out_rvar r
    | MQMConclusion -> key "mainconclusion" 
    | MQConclusion  -> key "conclusion" 
@@ -98,10 +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 ")"
-   | MQLRVar v -> key "rvaroccur" ^ v
+   | MQListRVar 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
+   | MQListLVar v -> out_rvar v
 
 let out_query = function
    | MQList l -> out_list l
@@ -247,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 (MQSSVar svar, mqs)
+             MQIs (MQStringSVar svar, mqs)
             )
 
 let rec build_inter n = function
@@ -279,13 +279,13 @@ let restrict_universe query =
           MQSubset (
            MQSelect (
             "uri2",
-            MQUsedBy (MQLRVar "uri", "pos"),
+            MQUsedBy (MQListRVar "uri", "pos"),
             MQOr (
-             MQIs (MQSSVar "pos", MQConclusion),
-             MQIs (MQSSVar "pos", MQMConclusion)
+             MQIs (MQStringSVar "pos", MQConclusion),
+             MQIs (MQStringSVar "pos", MQMConclusion)
             )
            ),
-           MQLetRef "universe"
+           MQListLVar "universe"
           )
         )
       )