X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2FmQIUtil.ml;h=f80fefeec759b0a0c7ec0c50801c5da8f8da7cb3;hb=5bef9ac5a9bfe07b11ce0e44fab51ea4b6eb4057;hp=537e32d77e9cddd02be0c91bcff8dbffb2a554d1;hpb=48b9bb5e9504aba97cff28a9d7e2797feb42972e;p=helm.git

diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.ml b/helm/ocaml/mathql_interpreter/mQIUtil.ml
index 537e32d77..f80fefeec 100644
--- a/helm/ocaml/mathql_interpreter/mQIUtil.ml
+++ b/helm/ocaml/mathql_interpreter/mQIUtil.ml
@@ -23,52 +23,55 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
-(*                                 06/01/2003                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
+(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
 
 (* boolean constants  *******************************************************)
 
 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
       | [], v                           -> v
-      | v, []                           -> v (* (zz h1 ">" h2); *)
+      | v, []                           -> v 
       | h1 :: t1, h2 :: t2 when h1 < h2 -> h1 :: set_union t1 v2
       | h1 :: t1, h2 :: t2 when h1 > h2 -> h2 :: set_union v1 t2
       | h1 :: t1, _ :: t2               -> h1 :: set_union t1 t2
 
+let rec set_intersect v1 v2 =
+   match v1, v2 with
+      | [], v                          -> []
+      | v, []                          -> []
+      | h1 :: t1, h2 :: _ when h1 < h2 -> set_intersect t1 v2
+      | h1 :: _, h2 :: t2 when h1 > h2 -> set_intersect v1 t2
+      | h1 :: t1, _ :: t2              -> h1 :: set_intersect t1 t2
+
 let rec iter f = function
    | []           -> []
    | head :: tail -> set_union (f head) (iter f tail)  
@@ -93,7 +96,7 @@ let rec mql_iter f = function
 let rec mql_iter2 f l1 l2 = match l1, l2 with
    | [], []             -> []
    | h1 :: t1, h2 :: t2 -> mql_union (f h1 h2) (mql_iter2 f t1 t2)
-   | _                  -> raise (Invalid_argument "mql_itwr2")
+   | _                  -> raise (Invalid_argument "mql_iter2")
 
 let rec mql_prod g1 g2 =
    let mql_prod_aux a = iter (fun h -> [mql_union a h]) g2 in
@@ -106,7 +109,7 @@ let rec mql_intersect s1 s2 =
       | (r1, _) :: t1, (r2, _) :: _ when r1 < r2 -> mql_intersect t1 s2
       | (r1, _) :: _, (r2, _) :: t2 when r1 > r2 -> mql_intersect s1 t2
       | (r1, g1) :: t1, (_, g2) :: t2            ->
-         (r1, mql_prod g1 g2) :: mql_intersect t1 t2
+         (r1, set_intersect g1 g2) :: mql_intersect t1 t2
 
 let rec mql_diff s1 s2 =
    match s1, s2 with
@@ -123,43 +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
-
-(* time handling  ***********************************************************)
-
-type time = float * float 
-
-let start_time () =
-   (Sys.time (), Unix.time ())
-   
-let stop_time (s0, u0) =
-   let s1 = Sys.time () in
-   let u1 = Unix.time () in
-   Printf.sprintf "%.2fs,%.2fs" (s1 -. s0) (u1 -. u0)