X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2FmQIUtil.ml;h=8d5782deaf4c66160f627c938c32f574328f334f;hb=efdc3184ccd0738fe48aa0056fc444fba23329e8;hp=00f5390b512a545b9fb29b5cd672cfbe7e5c4b7a;hpb=6cf989363e4b92e47a5385ae4f01e77c5bbe4553;p=helm.git

diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.ml b/helm/ocaml/mathql_interpreter/mQIUtil.ml
index 00f5390b5..8d5782dea 100644
--- a/helm/ocaml/mathql_interpreter/mQIUtil.ml
+++ b/helm/ocaml/mathql_interpreter/mQIUtil.ml
@@ -30,28 +30,31 @@
 
 let mql_false = []
 
-let mql_true = [""]
+let mql_true = ["", []]
 
 (* set theoretic operations *************************************************)
 
 let rec set_sub v1 v2 =
-   match v1, v2 with
-      | [], _                          -> mql_true 
-      | _, []                          -> mql_false
-      | h1 :: _, h2 :: _ when h1 < h2  -> mql_false
-      | h1 :: _, h2 :: t2 when h1 > h2 -> set_sub v1 t2
-      | _ :: t1, _ :: t2               -> set_sub t1 t2
+   match (v1, v2) with 
+      | [], _                                    -> mql_true 
+      | _, []                                    -> mql_false
+      | (h1, _) :: _, (h2, _) :: _ when h1 < h2  -> mql_false
+      | (h1, _) :: _, (h2, _) :: t2 when h1 > h2 -> set_sub v1 t2
+      | _ :: t1, _ :: t2                         -> set_sub t1 t2
 
 let rec set_meet v1 v2 =
    match v1, v2 with
-      | [], _                          -> mql_false 
-      | _, []                          -> mql_false
-      | h1 :: t1, h2 :: _ when h1 < h2 -> set_meet t1 v2
-      | h1 :: _, h2 :: t2 when h1 > h2 -> set_meet v1 t2
-      | _, _                           -> mql_true
+      | [], _                                    
+      | _, []                                    -> mql_false
+      | (h1, _) :: t1, (h2, _) :: _ when h1 < h2 -> set_meet t1 v2
+      | (h1, _) :: _, (h2, _) :: t2 when h1 > h2 -> set_meet v1 t2
+      | _, _                                     -> mql_true
 
-let set_eq v1 v2 =
-   if v1 = v2 then mql_true else mql_false
+let rec set_eq v1 v2 =
+   match v1, v2 with
+      | [], []                                    -> mql_true 
+      | (h1, _) :: t1, (h2, _) :: t2 when h1 = h2 -> set_eq t1 t2
+      | _, _                                      -> mql_false
 
 let rec set_union v1 v2 =
    match v1, v2 with
@@ -75,6 +78,8 @@ let rec iter f = function
 
 (* MathQL specific set operations  ******************************************)
 
+let mql_subj v = List.map (fun s -> (s, [])) v
+
 let rec mql_union s1 s2 =
    match s1, s2 with
       | [], s                                     -> s
@@ -124,30 +129,12 @@ let xor v1 v2 =
    if b && v2 <> mql_false then mql_false else
    if b then v1 else v2
 
-(* numeric operations  ******************************************************)
-
-let int_of_list = function
-   | [s] -> int_of_string s
-   | _   -> raise (Failure "int_of_list")
-
-let le v1 v2 =
-   try if int_of_list v1 <= int_of_list v2 then mql_true else mql_false
-   with _ -> mql_false
-
-let lt v1 v2 =
-   try if int_of_list v1 < int_of_list v2 then mql_true else mql_false
-   with _ -> mql_false
-
-let align n v =
-   let c = String.length v in
-   try
-      let l = int_of_list [n] in
-      if c < l then [(String.make (l - c) ' ') ^ v] else [v] 
-   with _ -> [v]
+(* numeric operations *******************************************************)
 
-(* context handling  ********************************************************)
+exception NumberError of MathQL.result
 
-let rec set ap = function
-   | []                                  -> [ap]
-   | head :: tail when fst head = fst ap -> ap :: tail
-   | head :: tail                        -> head :: set ap tail
+let int_of_set r =
+   try match r with 
+      | [s, _] -> MQueryUtil.int_of_string s
+      | _      -> raise (Failure "int_of_string")
+   with Failure "int_of_string" -> raise (NumberError r)