]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_interpreter/mQILib.ml
patched and new Gen constructor added
[helm.git] / helm / ocaml / mathql_interpreter / mQILib.ml
index 7a1e4e53b114489e568e3561da1a81add3ba7c9f..8cfa9deed961b501d721c4576036c91eeb7bc617 100644 (file)
@@ -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