]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_interpreter/mQIUtil.ml
first version
[helm.git] / helm / ocaml / mathql_interpreter / mQIUtil.ml
index 00f5390b512a545b9fb29b5cd672cfbe7e5c4b7a..f80fefeec759b0a0c7ec0c50801c5da8f8da7cb3 100644 (file)
 
 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
@@ -123,31 +126,3 @@ let xor v1 v2 =
    let b = v1 <> mql_false in 
    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]
-
-(* context handling  ********************************************************)
-
-let rec set ap = function
-   | []                                  -> [ap]
-   | head :: tail when fst head = fst ap -> ap :: tail
-   | head :: tail                        -> head :: set ap tail