From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 25 Sep 2002 13:54:42 +0000 (+0000)
Subject: binders list added to MathQL.Ex constructor
X-Git-Tag: new_mathql_before_first_merge~29
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d3211f255c561a026e3cba3999e85518ab926769;p=helm.git

binders list added to MathQL.Ex constructor
---

diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly
index 9af1be4f0..f32a41187 100644
--- a/helm/ocaml/mathql/mQueryTParser.mly
+++ b/helm/ocaml/mathql/mQueryTParser.mly
@@ -34,6 +34,46 @@
 /******************************************************************************/
 
 %{
+   let analyze x =
+      let module M = MathQL in
+      let rec join l1 l2 = match l1, l2 with
+         | [], _                           -> l2
+         | _, []                           -> l1
+         | s1 :: tl1, s2 :: _ when s1 < s2 -> s1 :: join tl1 l2                     
+         | s1 :: _, s2 :: tl2 when s2 < s1 -> s2 :: join l1 tl2 
+         | s1 :: tl1, s2 :: tl2            -> s1 :: join tl1 tl2 
+      in
+      let rec an_val = function
+         | M.Const _             -> []
+         | M.VVar _              -> []
+         | M.Record (rv, _)      -> [rv]
+         | M.Fun (_, x)          -> an_val x
+         | M.Attribute (_, _, x) -> an_val x
+         | M.RefOf x             -> an_set x
+      and an_boole = function
+         | M.False       -> []
+         | M.True        -> []
+         | M.Ex _ _      -> []
+         | M.Not x       -> an_boole x
+         | M.And (x, y)  -> join (an_boole x) (an_boole y)
+         | M.Or (x, y)   -> join (an_boole x) (an_boole y)
+         | M.Sub (x, y)  -> join (an_val x) (an_val y)
+         | M.Meet (x, y) -> join (an_val x) (an_val y)
+         | M.Eq (x, y)   -> join (an_val x) (an_val y)
+      and an_set = function
+         | M.SVar _                -> []
+         | M.RVar _                -> []
+         | M.Relation (_, _, x, _) -> an_set x
+         | M.Pattern x             -> an_val x
+         | M.Ref x                 -> an_val x
+         | M.Union (x, y)          -> join (an_set x) (an_set y)
+         | M.Intersect (x, y)      -> join (an_set x) (an_set y)
+         | M.Diff (x, y)           -> join (an_set x) (an_set y)
+         | M.LetSVar (_, x, y)     -> join (an_set x) (an_set y)
+         | M.LetVVar (_, x, y)     -> join (an_val x) (an_set y)
+         | M.Select (_, x, y)      -> join (an_set x) (an_boole y)
+      in
+      an_boole x
 %}
    %token    <string> ID STR
    %token    SL IS LC RC CM SC LP RP AT PC DL FS DQ EOF 
@@ -89,18 +129,19 @@
       | LC qstr_list RC                 { MathQL.Const $2               }
       | LC RC                           { MathQL.Const []               }
       | REFOF set_exp                   { MathQL.RefOf $2               }
+      | LP val_exp RP                   { $2                            }
    ;
    boole_exp:
-      | TRUE                    { MathQL.True          }
-      | FALSE                   { MathQL.False         }
-      | LP boole_exp RP         { $2                   }
-      | NOT boole_exp           { MathQL.Not $2        }
-      | EX boole_exp            { MathQL.Ex $2         }
-      | val_exp SUB val_exp     { MathQL.Sub ($1, $3)  }
-      | val_exp MEET val_exp    { MathQL.Meet ($1, $3) }
-      | val_exp EQ val_exp      { MathQL.Eq ($1, $3)   }
-      | boole_exp AND boole_exp { MathQL.And ($1, $3)  }
-      | boole_exp OR boole_exp  { MathQL.Or ($1, $3)   }
+      | TRUE                    { MathQL.True               }
+      | FALSE                   { MathQL.False              }
+      | LP boole_exp RP         { $2                        }
+      | NOT boole_exp           { MathQL.Not $2             }
+      | EX boole_exp            { MathQL.Ex (analyze $2) $2 }
+      | val_exp SUB val_exp     { MathQL.Sub ($1, $3)       }
+      | val_exp MEET val_exp    { MathQL.Meet ($1, $3)      }
+      | val_exp EQ val_exp      { MathQL.Eq ($1, $3)        }
+      | boole_exp AND boole_exp { MathQL.And ($1, $3)       }
+      | boole_exp OR boole_exp  { MathQL.Or ($1, $3)        }
    ;   
    set_exp:
       | REF val_exp                                 { MathQL.Ref $2                    }
diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml
index 450e40210..c5e111fae 100644
--- a/helm/ocaml/mathql/mQueryUtil.ml
+++ b/helm/ocaml/mathql/mQueryUtil.ml
@@ -67,7 +67,7 @@ let text_of_query x =
    and txt_boole = function
       | M.False       -> "false"
       | M.True        -> "true"
-      | M.Ex x        -> "ex " ^ txt_boole x
+      | M.Ex b x      -> "ex [" ^ txt_list txt_rvar "," b ^ "] " ^ txt_boole x
       | M.Not x       -> "not " ^ txt_boole x
       | M.And (x, y)  -> "(" ^ txt_boole x ^ " and " ^ txt_boole y ^ ")"
       | M.Or (x, y)   -> "(" ^ txt_boole x ^ " or " ^ txt_boole y ^ ")"
diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml
index 60b19297a..d375d92af 100644
--- a/helm/ocaml/mathql/mathQL.ml
+++ b/helm/ocaml/mathql/mathQL.ml
@@ -66,7 +66,7 @@ type set_exp = SVar of svar
 and boole_exp = False
               | True
 	      | Not of boole_exp
-	      | Ex of boole_exp
+	      | Ex of rvar list * boole_exp   
 	      | And of boole_exp * boole_exp
 	      | Or of boole_exp * boole_exp
 	      | Sub of val_exp * val_exp