From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 3 Jul 2003 10:55:47 +0000 (+0000)
Subject: new "light" implementation of intersection (compatible with the generator)
X-Git-Tag: camera_ready~21
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6cf989363e4b92e47a5385ae4f01e77c5bbe4553;p=helm.git

new "light" implementation of intersection (compatible with the generator)
---

diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.ml b/helm/ocaml/mathql_interpreter/mQIUtil.ml
index fef3252ac..00f5390b5 100644
--- a/helm/ocaml/mathql_interpreter/mQIUtil.ml
+++ b/helm/ocaml/mathql_interpreter/mQIUtil.ml
@@ -56,11 +56,19 @@ let set_eq v1 v2 =
 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)  
@@ -85,7 +93,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
@@ -98,7 +106,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
diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.mli b/helm/ocaml/mathql_interpreter/mQIUtil.mli
index c294832c8..76735a863 100644
--- a/helm/ocaml/mathql_interpreter/mQIUtil.mli
+++ b/helm/ocaml/mathql_interpreter/mQIUtil.mli
@@ -38,6 +38,8 @@ val set_eq        : MathQL.value -> MathQL.value -> MathQL.value
 
 val set_union     : 'a list -> 'a list -> 'a list
 
+val set_intersect : 'a list -> 'a list -> 'a list
+
 val mql_union     : ('a * 'b list) list -> ('a * 'b list) list -> 
                     ('a * 'b list) list