From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 7 Nov 2003 11:49:14 +0000 (+0000)
Subject: patched and new Gen constructor added
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=88271fa4a71a3642880d85e9efe32ce2306f0661

patched and new Gen constructor added
---

diff --git a/helm/ocaml/mathql_interpreter/mQILib.ml b/helm/ocaml/mathql_interpreter/mQILib.ml
index 7a1e4e53b..8cfa9deed 100644
--- a/helm/ocaml/mathql_interpreter/mQILib.ml
+++ b/helm/ocaml/mathql_interpreter/mQILib.ml
@@ -57,6 +57,10 @@ type fun_spec = {arity_p : arity_t;
 		           M.path list -> M.query list -> unit
 		}
 
+type gen_spec = {arity : arity_t;
+                 code  : eval_spec -> M.query list -> M.query
+                }
+
 exception ArityError of M.path * arity_t * int
 
 exception NameError of M.path
@@ -69,6 +73,12 @@ type std_text_out_spec = {s_out    : string -> unit;
 		          s_result : M.result -> unit
 }
 
+let check_arity p i = function 
+   | Const k when i = k  -> ()
+   | Positive when i > 0 -> ()
+   | Any                 -> ()
+   | a                   -> raise (ArityError (p, a, i))
+
 (* external functions implementation ****************************************)
 
 let std o = 
@@ -438,7 +448,7 @@ let keep_fun b =
 
 (* external functions interface *********************************************)
 
-let get_spec = function
+let fun_get_spec = function
    | ["empty"]                 -> false_fun false
    | ["false"]                 -> false_fun true
    | ["true"]                  -> true_fun
@@ -469,17 +479,33 @@ let get_spec = function
    | ["keep"; "allbut"]        -> keep_fun true
    | p                         -> raise (NameError p) 
    
-let check_arity p m n =
-   let aux i = function 
-      | Const k when i = k  -> ()
-      | Positive when i > 0 -> ()
-      | Any                 -> ()
-      | a                   -> raise (ArityError (p, a, i))
-   in   
-   aux m (get_spec p).arity_p; aux n (get_spec p).arity_s 
+let fun_arity p m n =
+   check_arity p m (fun_get_spec p).arity_p; 
+   check_arity p n (fun_get_spec p).arity_s 
 
-let eval e o i p pl xl = (get_spec p).body e o i pl xl
+let fun_eval e o i p pl xl = (fun_get_spec p).body e o i pl xl
 
-let txt_out o p pl xl =
-   try (get_spec p).txt_out o pl xl 
+let fun_txt_out o p pl xl =
+   try (fun_get_spec p).txt_out o pl xl 
    with NameError q when q = p -> out_txt_full (std o) p pl xl
+
+(* generator functions implementation ***************************************)
+
+let helm_vars_gen =
+   let mk_let v s x = M.Let (v, M.Const [(s, [])], x) in 
+   let arity = Const 1 in
+   let code _ = function
+      | [x] -> mk_let "SET" "Set" x
+      | _   -> assert false
+   in
+   {arity = arity; code = code}
+
+(* generator functions interface ********************************************)
+
+let gen_get_spec = function
+   | ["helm"; "vars"] -> helm_vars_gen
+   | p                -> raise (NameError p) 
+
+let gen_arity p n = check_arity p n (gen_get_spec p).arity 
+
+let gen_eval e p xl = (gen_get_spec p).code e xl
diff --git a/helm/ocaml/mathql_interpreter/mQILib.mli b/helm/ocaml/mathql_interpreter/mQILib.mli
index acc465b7a..f5e187457 100644
--- a/helm/ocaml/mathql_interpreter/mQILib.mli
+++ b/helm/ocaml/mathql_interpreter/mQILib.mli
@@ -42,15 +42,20 @@ type text_out_spec = {out    : string -> unit;
 
 type text_in_spec = {result_in : Lexing.lexbuf -> MathQL.result}
 
-val check_arity : MathQL.path -> int -> int -> unit
+val fun_arity   : MathQL.path -> int -> int -> unit
 
-val eval        : eval_spec -> text_out_spec -> text_in_spec -> 
+val fun_eval    : eval_spec -> text_out_spec -> text_in_spec -> 
                   MathQL.path -> MathQL.path list -> MathQL.query list -> 
-		  MathQL.result
+	          MathQL.result
 
-val txt_out     : text_out_spec ->
+val fun_txt_out : text_out_spec ->
 		  MathQL.path -> MathQL.path list -> MathQL.query list -> unit
 
+val gen_arity   : MathQL.path -> int -> unit
+
+val gen_eval    : eval_spec ->
+                  MathQL.path -> MathQL.query list -> MathQL.query
+
 exception ArityError of MathQL.path * arity_t * int
 
 exception NameError of MathQL.path
diff --git a/helm/ocaml/mathql_interpreter/mQueryIO.ml b/helm/ocaml/mathql_interpreter/mQueryIO.ml
index f220a270d..a8fe2006e 100644
--- a/helm/ocaml/mathql_interpreter/mQueryIO.ml
+++ b/helm/ocaml/mathql_interpreter/mQueryIO.ml
@@ -115,7 +115,7 @@ let rec text_of_query out sep x =
 	          L.query = text_of_query; L.result = text_of_result
 		 } 
 	 in
-	 L.txt_out o p pl xl 
+	 L.fun_txt_out o p pl xl 
       | M.Const [s, []] -> txt_str out s
       | M.Const r       -> text_of_result out " " r
       | M.Dot av p      -> txt_avar av; out "."; txt_path out p
@@ -136,6 +136,9 @@ let rec text_of_query out sep x =
                            txt_set x; txt_gen k; txt_set y
       | M.Add d g x     -> out "add "; txt_distr d; txt_grp g; 
                            out " in "; txt_set x
+      | M.Gen p [x]     -> out "gen "; txt_path out p; out " in "; txt_set x
+      | M.Gen p l       -> out "gen "; txt_path out p; out " {";
+                           P.flat_list out txt_set ", " l; out "}"
    in 
    txt_set x; out sep
 
diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
index a459fe829..a852affde 100644
--- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
+++ b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
@@ -134,8 +134,11 @@ let execute h x =
 	 select_aux (eval_query c x)
       | M.Fun p pl xl -> 
          let e = {L.eval = eval_query c; L.conn = h} in
-         L.eval e (F.text_out_spec (C.log h) "\n") F.text_in_spec 
+         L.fun_eval e (F.text_out_spec (C.log h) "\n") F.text_in_spec 
             p pl xl
+      | M.Gen p xl -> 
+         let e = {L.eval = eval_query c; L.conn = h} in
+	 eval_query c (L.gen_eval e p xl)
    and eval_grp c = function
       | M.Attr gs ->
          let attr_aux g (p, y) = U.mql_union g [p, proj (eval_query c y)] in
diff --git a/helm/ocaml/mathql_interpreter/mQueryTLexer.mll b/helm/ocaml/mathql_interpreter/mQueryTLexer.mll
index 00fc9dc68..d5f2fe10f 100644
--- a/helm/ocaml/mathql_interpreter/mQueryTLexer.mll
+++ b/helm/ocaml/mathql_interpreter/mQueryTLexer.mll
@@ -92,6 +92,7 @@ and query_token = parse
    | "false"     { out "FALSE" ; FALSE  }
    | "for"       { out "FOR"   ; FOR    }
    | "from"      { out "FROM"  ; FROM   }
+   | "gen"       { out "GEN"   ; GEN    }
    | "if"        { out "IF"    ; IF     }
    | "in"        { out "IN"    ; IN     }
    | "inf"       { out "INF"   ; INF    }   
diff --git a/helm/ocaml/mathql_interpreter/mQueryTParser.mly b/helm/ocaml/mathql_interpreter/mQueryTParser.mly
index a529326b1..3265a53a8 100644
--- a/helm/ocaml/mathql_interpreter/mQueryTParser.mly
+++ b/helm/ocaml/mathql_interpreter/mQueryTParser.mly
@@ -31,9 +31,13 @@
    module L = MQILib
 
    let make_fun p pl xl = 
-      L.check_arity p (List.length pl) (List.length xl); 
+      L.fun_arity p (List.length pl) (List.length xl); 
       M.Fun p pl xl
 
+   let make_gen p xl = 
+      L.gen_arity p (List.length xl); 
+      M.Gen p xl
+
    let analyze x =
       let rec join l1 l2 = match l1, l2 with
          | [], _                           -> l2
@@ -56,6 +60,7 @@
 	 | M.Select _ x y
          | M.For _ _ x y                -> iter an_set [x; y]
 	 | M.Fun _ _ l                  -> iter an_set l
+	 | M.Gen _ l                    -> iter an_set l
 	 | M.Add _ g x                  -> join (an_grp g) (an_set x)
          | M.Property _ _ _ _ c d _ _ x -> 
 	    join (an_set x) (iter an_con [c; List.concat d])
@@ -75,7 +80,7 @@
    %token    <string> SVAR AVAR STR
    %token    LB RB SL LC RC CM SC LP RP FS DQ EOF 
    %token    ADD ALIGN AND AS ATTR BE BUT COUNT DIFF DISTR ELSE EMPTY EQ EX  
-   %token    FALSE FOR FROM IF IN INF INTER INV ISF IST KEEP LE LET LOG LT   
+   %token    FALSE FOR FROM GEN IF IN INF INTER INV ISF IST KEEP LE LET LOG LT
    %token    MAIN MATCH MEET NOT OF OR PAT PEEK PROJ PROP READ RENDER SELECT 
    %token    SEQ SOURCE STAT SUB SUP SUPER THEN TRUE UNION WHERE XOR
 
@@ -117,7 +122,8 @@
    ;
    path:
       | SL subpath { $2 }
-      | SL         { [] }
+/*    | subpath    { $1 }
+*/    | SL         { [] }
    ;   
    ppaths:
       | path CM ppaths { $1 :: $3 }
@@ -210,88 +216,51 @@
       | avar { M.From $1 }
    ;
    set_exp:
-      | FALSE
-         { make_fun ["false"] [] [] }
-      | TRUE
-         { make_fun ["true"] [] [] }
-      | STR 
-         { M.Const [$1, []] }
-      | LB resources RB 
-         { M.Const $2 }
-      | avar FS path
-         { M.Dot $1 $3 }
-      | LC sets RC
-         { make_fun ["union"] [] $2 }
-      | LP set_exp RP
-         { $2 }
-      | STAT set_exp
-         { make_fun ["stat"] [] [$2] }
-      | RENDER set_exp
-         { make_fun ["render"] [] [$2] }
-      | READ set_exp
-         { make_fun ["read"] [] [$2] }
-      | EX set_exp
-         { M.Ex (analyze $2) $2 }
-      | NOT set_exp
-         { make_fun ["not"] [] [$2] }
-      | PROJ path OF set_exp
-         { make_fun ["proj"] [$2] [$4] }
-      | COUNT set_exp
-         { make_fun ["count"] [] [$2] }
-      | ALIGN set_exp IN set_exp    
-         { make_fun ["align"] [] [$2; $4] }
-      | EMPTY
-         { make_fun ["empty"] [] [] }
-      | svar
-         { M.SVar $1 }
-      | avar
-         { M.AVar $1 }
-      | LET svar BE set_exp IN set_exp
-         { M.Let $2 $4 $6 }
-      | FOR avar IN set_exp gen_op             
-         { M.For (fst $5) $2 $4 (snd $5) }
-      | ADD distr grp_exp IN set_exp
-         { M.Add $2 $3 $5 }
-      | IF set_exp THEN set_exp ELSE set_exp
+      | STAT set_exp                  { make_fun ["stat"] [] [$2] }
+      | RENDER set_exp                { make_fun ["render"] [] [$2] }
+      | READ set_exp                  { make_fun ["read"] [] [$2] }
+      | FALSE                         { make_fun ["false"] [] [] }
+      | TRUE                          { make_fun ["true"] [] [] }
+      | LC sets RC                    { make_fun ["union"] [] $2 }
+      | NOT set_exp                   { make_fun ["not"] [] [$2] }
+      | PROJ path OF set_exp          { make_fun ["proj"] [$2] [$4] }
+      | COUNT set_exp                 { make_fun ["count"] [] [$2] }
+      | ALIGN set_exp IN set_exp      { make_fun ["align"] [] [$2; $4] }
+      | EMPTY                         { make_fun ["empty"] [] [] }
+      | LOG xml source set_exp        { make_fun ["log"; $2; $3] [] [$4] }
+      | KEEP allbut ppaths IN set_exp { make_fun ["keep"; $2] $3 [$5] } 
+      | KEEP allbut set_exp           { make_fun ["keep"; $2] [] [$3] } 
+      | path LC paths RC LC sets RC   { make_fun $1 $3 $6 }
+      | set_exp SEQ set_exp           { make_fun ["seq"] [] [$1; $3] }
+      | set_exp DIFF set_exp          { make_fun ["diff"] [] [$1; $3] }
+      | set_exp UNION set_exp         { make_fun ["union"] [] [$1; $3] }
+      | set_exp INTER set_exp         { make_fun ["intersect"] [] [$1; $3] }
+      | set_exp XOR set_exp           { make_fun ["xor"] [] [$1; $3] }
+      | set_exp OR set_exp            { make_fun ["or"] [] [$1; $3] }
+      | set_exp AND set_exp           { make_fun ["and"] [] [$1; $3] }
+      | set_exp SUB set_exp           { make_fun ["sub"] [] [$1; $3] }
+      | set_exp MEET set_exp          { make_fun ["meet"] [] [$1; $3] }
+      | set_exp EQ set_exp            { make_fun ["eq"] [] [$1; $3] }
+      | set_exp LE set_exp            { make_fun ["le"] [] [$1; $3] }
+      | set_exp LT set_exp            { make_fun ["lt"] [] [$1; $3] }
+      | PEEK set_exp                  { make_fun ["peek"] [] [$2] }
+      | IF set_exp THEN set_exp ELSE set_exp 
          { make_fun ["if"] [] [$2; $4; $6] }
+      | STR                            { M.Const [$1, []] }
+      | LB resources RB                { M.Const $2 }
+      | avar FS path                   { M.Dot $1 $3 }
+      | LP set_exp RP                  { $2 }
+      | EX set_exp                     { M.Ex (analyze $2) $2 }
+      | svar                           { M.SVar $1 }
+      | avar                           { M.AVar $1 }
+      | LET svar BE set_exp IN set_exp { M.Let $2 $4 $6 }
+      | FOR avar IN set_exp gen_op     { M.For (fst $5) $2 $4 (snd $5) }
+      | ADD distr grp_exp IN set_exp   { M.Add $2 $3 $5 }
       | PROP qualif mainc istrue isfalse attrc OF pattern set_exp     
          { M.Property (f $2) (s $2) (t $2) $3 $4 $5 $6 $8 $9 }
-      | LOG xml source set_exp
-         { make_fun ["log"; $2; $3] [] [$4] }
-      | KEEP allbut ppaths IN set_exp
-         { make_fun ["keep"; $2] $3 [$5] } 
-      | KEEP allbut set_exp
-         { make_fun ["keep"; $2] [] [$3] } 
-      | SELECT avar FROM set_exp WHERE set_exp
-         { M.Select $2 $4 $6 }
-      | path LC paths RC LC sets RC
-         { make_fun $1 $3 $6 }
-      | set_exp SEQ set_exp
-         { make_fun ["seq"] [] [$1; $3] }
-      | set_exp DIFF set_exp
-         { make_fun ["diff"] [] [$1; $3] }
-      | set_exp UNION set_exp
-         { make_fun ["union"] [] [$1; $3] }
-      | set_exp INTER set_exp
-         { make_fun ["intersect"] [] [$1; $3] }
-      | set_exp XOR set_exp
-         { make_fun ["xor"] [] [$1; $3] }
-      | set_exp OR set_exp
-         { make_fun ["or"] [] [$1; $3] }
-      | set_exp AND set_exp
-         { make_fun ["and"] [] [$1; $3] }
-      | set_exp SUB set_exp
-         { make_fun ["sub"] [] [$1; $3] }
-      | set_exp MEET set_exp
-         { make_fun ["meet"] [] [$1; $3] }
-      | set_exp EQ set_exp
-         { make_fun ["eq"] [] [$1; $3] }
-      | set_exp LE set_exp
-         { make_fun ["le"] [] [$1; $3] }
-      | set_exp LT set_exp
-         { make_fun ["lt"] [] [$1; $3] }
-      | PEEK set_exp
-         { make_fun ["peek"] [] [$2] }
+      | SELECT avar FROM set_exp WHERE set_exp { M.Select $2 $4 $6 }
+      | GEN path LC sets RC { make_gen $2 $4 }
+      | GEN path IN set_exp { make_gen $2 [$4] }
    ;   
    psets:
       | set_exp CM psets { $1 :: $3 }