]> matita.cs.unibo.it Git - helm.git/commitdiff
binders list added to MathQL.Ex constructor
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 25 Sep 2002 13:54:42 +0000 (13:54 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 25 Sep 2002 13:54:42 +0000 (13:54 +0000)
helm/ocaml/mathql/mQueryTParser.mly
helm/ocaml/mathql/mQueryUtil.ml
helm/ocaml/mathql/mathQL.ml

index 9af1be4f0d59dc3e3040e63d01671efdd768901c..f32a4118756044213a3a89d2cf4c719caf6398ff 100644 (file)
 /******************************************************************************/
 
 %{
+   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 
       | 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                    }
index 450e40210560b8d40c063f213212a223f3c0fdfd..c5e111fae62ab3db227746cb10f7366e9a4067b9 100644 (file)
@@ -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 ^ ")"
index 60b19297aa2e8581e0171e10f013cc5aa9b6a2d7..d375d92afeac7ecf3971081247b8ad2dd5316e71 100644 (file)
@@ -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