]> matita.cs.unibo.it Git - helm.git/commitdiff
updated for the new version of mathQL.ml
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 18 Jun 2002 17:42:23 +0000 (17:42 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 18 Jun 2002 17:42:23 +0000 (17:42 +0000)
helm/gTopLevel/mquery.ml

index f31fccd07c25a8d16f932c93fec775d9c7f3131d..3e5548c68247e568f0598fcf59bfc6cc41fcf1b6 100644 (file)
@@ -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"
           )
         )
       )