]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_interpreter/mQILib.mli
optimized and patched
[helm.git] / helm / ocaml / mathql_interpreter / mQILib.mli
index 69bd3c04e500bacf80abd91f13798af377e68649..a8de33743e98934a48776060b128f985a85bcee4 100644 (file)
@@ -30,27 +30,76 @@ type arity_t = Const of int
              | Positive
             | Any
 
-type eval_spec = {eval   : MathQL.query -> MathQL.result;
-                  handle : MQIConn.handle
+type eval_spec = {eval : MathQL.query -> MathQL.result;
+                  conn : MQIConn.handle
                 }
 
-type txt_out_spec = {out    : string -> unit;
-                     path   : MathQL.path -> unit;
-                    query  : MathQL.query -> unit;
-                    result : MathQL.result -> unit
-                   }
+type text_out_spec = {out    : string -> unit;
+                      sep    : string;
+                      path   : (string -> unit) -> MathQL.path -> unit;
+                     query  : (string -> unit) -> string -> MathQL.query -> unit;
+                     result : (string -> unit) -> string -> MathQL.result -> unit
+                    }
 
-val check_arity : MathQL.path -> int -> int -> unit
+type text_in_spec = {result_in : Lexing.lexbuf -> MathQL.result}
 
-val eval        : eval_spec -> txt_out_spec -> 
+val fun_arity   : MathQL.path -> int -> int -> unit
+
+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     : txt_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
 
-exception NumberError of MathQL.result
+type std_text_out_spec = {s_out    : string -> unit;
+                          s_path   : MathQL.path -> unit;
+                         s_query  : MathQL.query -> unit;
+                         s_result : MathQL.result -> unit
+}
+
+val std : text_out_spec -> std_text_out_spec
+
+(* function registration ****************************************************)
+
+type fun_spec = {arity_p : arity_t;
+                 arity_s : arity_t;
+                 body    : eval_spec -> text_out_spec -> text_in_spec ->
+                          MathQL.path list -> MathQL.query list -> MathQL.result;
+                txt_out : text_out_spec ->  
+                          MathQL.path list -> MathQL.query list -> unit
+               }
+
+val fun_register : MathQL.path -> fun_spec -> unit
+
+val fun_arity0   : MathQL.path -> string -> MathQL.result -> fun_spec
+
+val fun_arity1   : MathQL.path -> string -> (MathQL.result -> MathQL.result) -> fun_spec
+
+val fun_arity2   : MathQL.path -> string -> (MathQL.result ->  MathQL.result -> MathQL.result) -> fun_spec
+
+val out_txt2     : std_text_out_spec -> 
+                   string -> MathQL.query -> MathQL.query -> unit 
+
+val out_txt_     : std_text_out_spec -> 
+                   MathQL.path -> MathQL.query list -> unit 
+
+val out_txt_full : std_text_out_spec -> 
+                   MathQL.path -> MathQL.path list -> MathQL.query list -> unit 
+
+(* generator registration ***************************************************)
+
+type gen_spec = {arity : arity_t;
+                 code  : eval_spec ->  MathQL.query list ->  MathQL.query
+                }
+
+val gen_register : MathQL.path -> gen_spec -> unit