X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2FmQILib.ml;fp=helm%2Focaml%2Fmathql_interpreter%2FmQILib.ml;h=b2260244582f625ceb568cc342d43db8ffc55619;hb=cf13d8dc120ae8745b26f8dbadea5af3f3b2193c;hp=8cfa9deed961b501d721c4576036c91eeb7bc617;hpb=a32bcc14672dae13e8bb725e54c819958dfdb677;p=helm.git

diff --git a/helm/ocaml/mathql_interpreter/mQILib.ml b/helm/ocaml/mathql_interpreter/mQILib.ml
index 8cfa9deed..b22602445 100644
--- a/helm/ocaml/mathql_interpreter/mQILib.ml
+++ b/helm/ocaml/mathql_interpreter/mQILib.ml
@@ -86,36 +86,6 @@ let std o =
     s_query = o.query o.out ""; s_result = o.result o.out "\n"
    }
 
-type t = End
-       | Space
-       | Figure of int
-       | Error
-
-let my_int_of_string s =
-   let l = String.length s in
-   let get_t i =
-      if i = l then End else
-      match s.[i] with
-         | ' ' | '\t' | '\r' | 'n' -> Space
-	 | '0' .. '9'              -> Figure (Char.code s.[i] - Char.code '0')
-	 | _                       -> Error
-   in
-   let rec aux i xv = match get_t i, xv with
-      | Error, _ 
-      | End, None        -> raise (Failure "int_of_string") 
-      | End, Some v      -> v
-      | Space, xv        -> aux (succ i) xv
-      | Figure f, None   -> aux (succ i) (Some f)
-      | Figure f, Some v -> aux (succ i) (Some (10 * v + f))
-   in
-   aux 0 None
-
-let int_of_set r =
-   try match r with 
-      | [s, _] -> my_int_of_string s
-      | _      -> raise (Failure "int_of_string")
-   with Failure "int_of_string" -> raise (NumberError r)
-
 let out_txt2 o n x1 x2 =
    o.s_out "(" ; o.s_query x1; o.s_out (" " ^ n ^ " "); o.s_query x2; o.s_out ")"
 
@@ -127,14 +97,16 @@ let out_txt_full o p pl xl =
    o.s_path p; o.s_out " {"; P.flat_list o.s_out o.s_path ", " pl; o.s_out "} {";
    P.flat_list o.s_out o.s_query ", " xl; o.s_out "}"    
 
-let arity0 n r =
+let fun_arity0 p n r =
    let arity_p = Const 0 in
    let arity_s = Const 0 in
    let body _ _ _ _ _ = r in
-   let txt_out o _ _ = (std o).s_out n in
+   let txt_out o _ _ = 
+      if n = "" then out_txt_full (std o) p [] [] else (std o).s_out n
+   in
    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 
-let arity1 n f =
+let fun_arity1 p n f =
    let arity_p = Const 0 in
    let arity_s = Const 1 in
    let body e _ _ _ = function
@@ -142,12 +114,15 @@ let arity1 n f =
       | _   -> assert false
    in
    let txt_out o _ = function
-      | [x] -> let o = std o in o.s_out (n ^ " "); o.s_query x
+      | [x] ->
+         let o = std o in
+         if n = "" then out_txt_full o p [] [x] else
+	 begin o.s_out (n ^ " "); o.s_query x end
       | _   -> assert false
    in   
    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 
-let arity2 n f =
+let fun_arity2 p n f =
    let arity_p = Const 0 in
    let arity_s = Const 2 in
    let body e _ _ _ = function
@@ -155,329 +130,22 @@ let arity2 n f =
       | _        -> assert false
    in
    let txt_out o _ = function
-      | [x1; x2] -> let o = std o in out_txt2 o n x1 x2
-      | _        -> assert false
-   in   
-   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
-
-let false_fun b =
-   let s = if b then "false" else "empty" in 
-   arity0 s U.mql_false
-
-let true_fun = arity0 "true" U.mql_true
-
-let not_fun = 
-   let aux r = if r = U.mql_false then U.mql_true else U.mql_false in
-   arity1 "!" aux 
-
-let count_fun =
-   let aux r = [string_of_int (List.length r), []] in
-   arity1 "#" aux
-
-let peek_fun =
-   let aux = function [] -> [] | hd :: _ -> [hd] in
-   arity1 "peek" aux
-
-let diff_fun = arity2 "diff" U.mql_diff
-
-let xor_fun = arity2 "xor" U.xor
-
-let sub_fun = arity2 "sub" U.set_sub
-
-let meet_fun = arity2 "meet" U.set_meet
-
-let eq_fun = arity2 "==" U.set_eq
-
-let le_fun = 
-   let le v1 v2 =
-      if int_of_set v1 <= int_of_set v2 then U.mql_true else U.mql_false
-   in
-   arity2 "<=" le
-
-let lt_fun = 
-   let lt v1 v2 =
-      if int_of_set v1 < int_of_set v2 then U.mql_true else U.mql_false
-   in
-   arity2 "<" lt
-
-let stat_fun =
-   let arity_p = Const 0 in
-   let arity_s = Const 1 in
-   let body e o _ _ = function
-      | [x] -> 
-         let t = P.start_time () in
-	 let r = (e.eval x) in
-	 let s = P.stop_time t in
-         o.out (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
-	 r
-      | _   -> assert false
-   in
-   let txt_out o _ = function
-      | [x] -> let o = std o in o.s_out "stat "; o.s_query x
-      | _   -> assert false
-   in   
-   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
-
-let log_fun xml src =
-   let log_src e o x =
-      let t = P.start_time () in o.s_query x;
-      let s = P.stop_time t in
-      if C.set e.conn C.Stat then o.s_out (Printf.sprintf "Log source: %s\n" s);
-      e.eval x 
-   in
-   let log_res e o x =  
-      let s = e.eval x in
-      let t = P.start_time () in o.s_result s;
-      let r = P.stop_time t in
-      if C.set e.conn C.Stat then o.s_out (Printf.sprintf "Log: %s\n" r); s
-   in
-   let txt_log o = 
-      if xml then o.s_out "xml ";
-      if src then o.s_out "source "
-   in
-   let arity_p = Const 0 in
-   let arity_s = Const 1 in
-   let body e o _ _ = function
-      | [x] -> let o = std o in if src then log_src e o x else log_res e o x
-      | _   -> assert false
-   in        
-   let txt_out o _ = function
-      | [x] -> let o = std o in o.s_out "log "; txt_log o; o.s_query x
-      | _   -> assert false
-   in   
-   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
-
-let render_fun = 
-   let arity_p = Const 0 in
-   let arity_s = Const 1 in
-   let body e o _ _ = function
-      | [x] -> 
-         let rs = ref "" in
-	 let out s = rs := ! rs ^ s in 
-         o.result out " " (e.eval x);
-	 [! rs, []]
-      | _   -> assert false
-   in
-   let txt_out o _ = function
-      | [x] -> let o = std o in o.s_out "render "; o.s_query x
-      | _   -> assert false
-   in   
-   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
-
-let read_fun = 
-   let arity_p = Const 0 in
-   let arity_s = Const 1 in
-   let body e o i _ = function
-      | [x] -> 
-         let aux av = 
-	    let ich = open_in (fst av) in
-	    let r = i.result_in (Lexing.from_channel ich) in
-	    close_in ich; r
-	 in
-	 U.mql_iter aux (e.eval x)
-      | _   -> assert false
-   in
-   let txt_out o _ = function
-      | [x] -> let o = std o in o.s_out "read "; o.s_query x
-      | _   -> assert false
-   in   
-   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
-
-let align_fun =
-   let aux l (v, g) =
-      let c = String.length v in
-      if c < l then [(String.make (l - c) ' ' ^ v), g] else [v, g]
-   in   
-   let arity_p = Const 0 in
-   let arity_s = Const 2 in
-   let body e _ _ _ = function
-      | [y; x] ->
-         let l = int_of_set (e.eval y) in
-         U.mql_iter (aux l) (e.eval x)      
-      | _      -> assert false
-   in
-   let txt_out o _ = function
-      | [y; x] -> 
+      | [x1; x2] -> 
          let o = std o in
-	 o.s_out "align "; o.s_query y; o.s_out " in "; o.s_query x
-      | _      -> assert false
-   in
-   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
-   
-let if_fun =
-   let arity_p = Const 0 in
-   let arity_s = Const 3 in
-   let body e _ _ _ = function
-      | [y; x1; x2] ->
-         if (e.eval y) = U.mql_false then (e.eval x2) else (e.eval x1)
-      | _           -> assert false
-   in
-   let txt_out o _ = function
-      | [y; x1; x2] ->
-         let o = std o in
-         o.s_out "if "; o.s_query y; o.s_out " then "; o.s_query x1; 
-	 o.s_out " else "; o.s_query x2
-      | _           -> assert false
-   in
-   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
-
-let intersect_fun =
-   let rec iter f = function
-      | []           -> assert false
-      | [head]       -> f head
-      | head :: tail -> U.mql_intersect (f head) (iter f tail)  
-   in
-   let arity_p = Const 0 in
-   let arity_s = Positive in
-   let body e _ _ _ xl = iter e.eval xl in
-   let txt_out o _ = function
-      | []           -> assert false
-      | [x1; x2]     -> let o = std o in out_txt2 o "/\\" x1 x2
-      | xl           -> let o = std o in out_txt_ o ["intersect"] xl  
+	 if n = "" then out_txt_full o p [] [x1; x2] else out_txt2 o n x1 x2 
+      | _        -> assert false
    in   
    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 
-let union_fun = 
-   let arity_p = Const 0 in
-   let arity_s = Any in
-   let body e _ _ _ xl = U.mql_iter e.eval xl in
-   let txt_out o _ xl = let o = std o in out_txt_ o [] xl  
-   in      
-   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
-
-let or_fun = 
-   let rec iter f = function
-      | []           -> U.mql_false
-      | head :: tail -> 
-         let r1 = f head in
-	 if r1 = U.mql_false then (iter f tail) else r1
-   in
-   let arity_p = Const 0 in
-   let arity_s = Any in
-   let body e _ _ _ xl = iter e.eval xl in
-   let txt_out o _ = function
-      | [x1; x2]     -> let o = std o in out_txt2 o "||" x1 x2
-      | xl           -> let o = std o in out_txt_ o ["or"] xl  
-   in
-   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
-
-let and_fun = 
-   let rec iter f = function
-      | []           -> U.mql_true
-      | [head]       -> f head
-      | head :: tail -> 
-         if f head = U.mql_false then U.mql_false else iter f tail
-   in
-   let arity_p = Const 0 in
-   let arity_s = Any in
-   let body e _ _ _ xl = iter e.eval xl in
-   let txt_out o _ = function 
-      | [x1; x2]  -> let o = std o in out_txt2 o "&&" x1 x2
-      | xl        -> let o = std o in out_txt_ o ["and"] xl
-   in
-   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
-
-let seq_fun = 
-   let rec iter f = function
-      | []           -> U.mql_true
-      | [head]       -> f head
-      | head :: tail -> ignore (f head); iter f tail
-   in
-   let arity_p = Const 0 in
-   let arity_s = Any in
-   let body e _ _ _ xl = iter e.eval xl in
-   let txt_out o _ = function 
-      | [x1; x2]  -> 
-         let o = std o in o.s_query x1; o.s_out " ;; "; o.s_query x2
-      | xl        -> let o = std o in out_txt_ o ["seq"] xl
-   in
-   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
-
-let proj_fun =
-   let proj_group_aux p (q, v) = if q = p then U.mql_subj v else [] in 
-   let proj_group p a = U.mql_iter (proj_group_aux p) a in
-   let proj_set p (_, g) = U.mql_iter (proj_group p) g in
-   let arity_p = Const 1 in
-   let arity_s = Const 1 in
-   let body e _ _ pl xl =
-      match pl, xl with
-         | [p], [x] -> U.mql_iter (proj_set p) (e.eval x)
-	 | _        -> assert false
-   in
-   let txt_out o pl xl =
-      match pl, xl with
-         | [p], [x] -> 
-	    let o = std o in
-	    o.s_out "proj "; o.s_path p; o.s_out " of "; o.s_query x
-	 | _        -> assert false
-   in
-   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+(* external functions interface *********************************************)
 
-let keep_fun b =
-   let proj (r, _) = (r, []) in
-   let keep_path l (p, v) t = if List.mem p l = b then t else (p, v) :: t in
-   let keep_grp l a = List.fold_right (keep_path l) a [] in
-   let keep_set l a g = 
-      let kg = keep_grp l a in
-      if kg = [] then g else kg :: g
-   in
-   let keep_av l (s, g) = (s, List.fold_right (keep_set l) g []) in
-   let txt_allbut o = if b then o.s_out "allbut " in
-   let txt_path_list o l = P.flat_list o.s_out o.s_path ", " l in 
-   let arity_p = Any in
-   let arity_s = Const 1 in
-   let body e _ _ pl xl =
-      match b, pl, xl with
-         | true, [], [x]  -> e.eval x
-         | false, [], [x] -> List.map proj (e.eval x)
-         | _, l, [x]      -> List.map (keep_av l) (e.eval x)
-         | _              -> assert false
-  in
-  let txt_out o pl xl =
-      match pl, xl with
-         | [], [x] -> 
-	    let o = std o in 
-	    o.s_out "keep "; txt_allbut o; o.s_query x
-	 | l, [x]  -> 
-	    let o = std o in
-	    o.s_out "keep "; txt_allbut o; txt_path_list o l; 
-	    o.s_out " in "; o.s_query x
-	 | _      -> assert false
-   in
-   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+let funs = Hashtbl.create 11
 
-(* external functions interface *********************************************)
+let fun_register path spec = Hashtbl.add funs path spec 
 
-let fun_get_spec = function
-   | ["empty"]                 -> false_fun false
-   | ["false"]                 -> false_fun true
-   | ["true"]                  -> true_fun
-   | ["not"]                   -> not_fun
-   | ["count"]                 -> count_fun
-   | ["stat"]                  -> stat_fun
-   | ["log"; "text"; "result"] -> log_fun false false
-   | ["log"; "text"; "source"] -> log_fun false true
-   | ["render"]                -> render_fun
-   | ["read"]                  -> read_fun
-   | ["peek"]                  -> peek_fun
-   | ["diff"]                  -> diff_fun
-   | ["xor"]                   -> xor_fun
-   | ["sub"]                   -> sub_fun
-   | ["meet"]                  -> meet_fun
-   | ["eq"]                    -> eq_fun
-   | ["le"]                    -> le_fun
-   | ["lt"]                    -> lt_fun
-   | ["align"]                 -> align_fun
-   | ["if"]                    -> if_fun 
-   | ["intersect"]             -> intersect_fun
-   | ["union"]                 -> union_fun
-   | ["or"]                    -> or_fun
-   | ["and"]                   -> and_fun 
-   | ["seq"]                   -> seq_fun
-   | ["proj"]                  -> proj_fun
-   | ["keep"; "these"]         -> keep_fun false
-   | ["keep"; "allbut"]        -> keep_fun true
-   | p                         -> raise (NameError p) 
+let fun_get_spec path =
+   try Hashtbl.find funs path
+   with Not_found -> raise (NameError path) 
    
 let fun_arity p m n =
    check_arity p m (fun_get_spec p).arity_p; 
@@ -491,20 +159,15 @@ let fun_txt_out 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 gens = Hashtbl.create 11
+
+let gen_register path spec = Hashtbl.add gens path spec 
+
+let gen_get_spec path =
+   try Hashtbl.find gens path
+   with Not_found -> raise (NameError path) 
 
 let gen_arity p n = check_arity p n (gen_get_spec p).arity