]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_interpreter/mQueryStandard.ml
standard library and while construction inserted
[helm.git] / helm / ocaml / mathql_interpreter / mQueryStandard.ml
diff --git a/helm/ocaml/mathql_interpreter/mQueryStandard.ml b/helm/ocaml/mathql_interpreter/mQueryStandard.ml
new file mode 100644 (file)
index 0000000..4bd251b
--- /dev/null
@@ -0,0 +1,406 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+module P = MQueryUtil 
+module C = MQIConn 
+module U = MQIUtil
+module L = MQILib
+
+let init = ()
+
+(* FALSE / EMPTY ************************************************************)
+
+let false_fun b =
+   let s = if b then "false" else "empty" in 
+   L.fun_arity0 [] s U.mql_false
+
+let _ = L.fun_register ["empty"] (false_fun false)
+
+let _ = L.fun_register ["false"] (false_fun true)
+
+(* TRUE *********************************************************************)
+
+let true_fun = L.fun_arity0 [] "true" U.mql_true
+
+let _ = L.fun_register ["true"] true_fun
+
+(* NOT **********************************************************************)
+
+let not_fun = 
+   let aux r = if r = U.mql_false then U.mql_true else U.mql_false in
+   L.fun_arity1 [] "!" aux 
+
+let _ = L.fun_register ["not"] not_fun
+
+(* COUNT ********************************************************************)
+
+let count_fun =
+   let aux r = [string_of_int (List.length r), []] in
+   L.fun_arity1 [] "#" aux
+
+let _ = L.fun_register ["count"] count_fun
+
+(* PEEK *********************************************************************)
+
+let peek_fun =
+   let aux = function [] -> [] | hd :: _ -> [hd] in
+   L.fun_arity1 [] "peek" aux
+
+let _ = L.fun_register ["peek"] peek_fun
+
+(* DIFF *********************************************************************)
+
+let diff_fun = L.fun_arity2 [] "diff" U.mql_diff
+
+let _ = L.fun_register ["diff"] diff_fun
+
+(* XOR **********************************************************************)
+
+let xor_fun = L.fun_arity2 [] "xor" U.xor
+
+let _ = L.fun_register ["xor"] xor_fun
+
+(* SUB **********************************************************************)
+
+let sub_fun = L.fun_arity2 [] "sub" U.set_sub
+
+let _ = L.fun_register ["sub"] sub_fun
+
+(* MEET *********************************************************************)
+
+let meet_fun = L.fun_arity2 [] "meet" U.set_meet
+
+let _ = L.fun_register ["meet"] meet_fun
+
+(* EQ ***********************************************************************)
+
+let eq_fun = L.fun_arity2 [] "==" U.set_eq
+
+let _ = L.fun_register ["eq"] eq_fun
+
+(* LE ***********************************************************************)
+
+let le_fun = 
+   let le v1 v2 =
+      if U.int_of_set v1 <= U.int_of_set v2 then U.mql_true else U.mql_false
+   in
+   L.fun_arity2 [] "<=" le
+
+let _ = L.fun_register ["le"] le_fun
+
+(* LT ***********************************************************************)
+
+let lt_fun = 
+   let lt v1 v2 =
+      if U.int_of_set v1 < U.int_of_set v2 then U.mql_true else U.mql_false
+   in
+   L.fun_arity2 [] "<" lt
+
+let _ = L.fun_register ["lt"] lt_fun
+
+(* STAT *********************************************************************)
+
+let stat_fun =
+   let arity_p = L.Const 0 in
+   let arity_s = L.Const 1 in
+   let body e o _ _ = function
+      | [x] -> 
+         let t = P.start_time () in
+        let r = (e.L.eval x) in
+        let s = P.stop_time t in
+         o.L.out (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
+        r
+      | _   -> assert false
+   in
+   let txt_out o _ = function
+      | [x] -> let o = L.std o in o.L.s_out "stat "; o.L.s_query x
+      | _   -> assert false
+   in   
+   {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
+
+let _ = L.fun_register ["stat"] stat_fun
+
+(* LOG **********************************************************************)
+
+let log_fun xml src =
+   let log_src e o x =
+      let t = P.start_time () in o.L.s_query x;
+      let s = P.stop_time t in
+      if C.set e.L.conn C.Stat then o.L.s_out (Printf.sprintf "Log source: %s\n" s);
+      e.L.eval x 
+   in
+   let log_res e o x =  
+      let s = e.L.eval x in
+      let t = P.start_time () in o.L.s_result s;
+      let r = P.stop_time t in
+      if C.set e.L.conn C.Stat then o.L.s_out (Printf.sprintf "Log: %s\n" r); s
+   in
+   let txt_log o = 
+      if xml then o.L.s_out "xml ";
+      if src then o.L.s_out "source "
+   in
+   let arity_p = L.Const 0 in
+   let arity_s = L.Const 1 in
+   let body e o _ _ = function
+      | [x] -> let o = L.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 = L.std o in o.L.s_out "log "; txt_log o; o.L.s_query x
+      | _   -> assert false
+   in   
+   {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
+
+let _ = L.fun_register ["log"; "text"; "result"] (log_fun false false)
+
+let _ = L.fun_register ["log"; "text"; "source"] (log_fun false true)
+
+(* RENDER *******************************************************************)
+
+let render_fun = 
+   let arity_p = L.Const 0 in
+   let arity_s = L.Const 1 in
+   let body e o _ _ = function
+      | [x] -> 
+         let rs = ref "" in
+        let out s = rs := ! rs ^ s in 
+         o.L.result out " " (e.L.eval x);
+        [! rs, []]
+      | _   -> assert false
+   in
+   let txt_out o _ = function
+      | [x] -> let o = L.std o in o.L.s_out "render "; o.L.s_query x
+      | _   -> assert false
+   in   
+   {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
+
+let _ = L.fun_register ["render"] render_fun
+
+(* READ *********************************************************************)
+
+let read_fun = 
+   let arity_p = L.Const 0 in
+   let arity_s = L.Const 1 in
+   let body e o i _ = function
+      | [x] -> 
+         let aux av = 
+           let ich = open_in (fst av) in
+           let r = i.L.result_in (Lexing.from_channel ich) in
+           close_in ich; r
+        in
+        U.mql_iter aux (e.L.eval x)
+      | _   -> assert false
+   in
+   let txt_out o _ = function
+      | [x] -> let o = L.std o in o.L.s_out "read "; o.L.s_query x
+      | _   -> assert false
+   in   
+   {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
+
+let _ = L.fun_register ["read"] read_fun
+
+(* ALIGN ********************************************************************)
+
+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 = L.Const 0 in
+   let arity_s = L.Const 2 in
+   let body e _ _ _ = function
+      | [y; x] ->
+         let l = U.int_of_set (e.L.eval y) in
+         U.mql_iter (aux l) (e.L.eval x)      
+      | _      -> assert false
+   in
+   let txt_out o _ = function
+      | [y; x] -> 
+         let o = L.std o in
+        o.L.s_out "align "; o.L.s_query y; o.L.s_out " in "; o.L.s_query x
+      | _      -> assert false
+   in
+   {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
+
+let _ = L.fun_register ["align"] align_fun
+
+(* IF ***********************************************************************)
+
+let if_fun =
+   let arity_p = L.Const 0 in
+   let arity_s = L.Const 3 in
+   let body e _ _ _ = function
+      | [y; x1; x2] ->
+         if (e.L.eval y) = U.mql_false then (e.L.eval x2) else (e.L.eval x1)
+      | _           -> assert false
+   in
+   let txt_out o _ = function
+      | [y; x1; x2] ->
+         let o = L.std o in
+         o.L.s_out "if "; o.L.s_query y; o.L.s_out " then "; o.L.s_query x1; 
+        o.L.s_out " else "; o.L.s_query x2
+      | _           -> assert false
+   in
+   {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
+
+let _ = L.fun_register["if"] if_fun 
+
+(* INTERSECT ****************************************************************)
+
+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 = L.Const 0 in
+   let arity_s = L.Positive in
+   let body e _ _ _ xl = iter e.L.eval xl in
+   let txt_out o _ = function
+      | []           -> assert false
+      | [x1; x2]     -> let o = L.std o in L.out_txt2 o "/\\" x1 x2
+      | xl           -> let o = L.std o in L.out_txt_ o ["intersect"] xl  
+   in   
+   {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
+
+let _ = L.fun_register ["intersect"] intersect_fun
+
+(* UNION ********************************************************************)
+
+let union_fun = 
+   let arity_p = L.Const 0 in
+   let arity_s = L.Any in
+   let body e _ _ _ xl = U.mql_iter e.L.eval xl in
+   let txt_out o _ xl = let o = L.std o in L.out_txt_ o [] xl  
+   in      
+   {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
+
+let _ = L.fun_register ["union"] union_fun
+
+(* OR ***********************************************************************)
+
+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 = L.Const 0 in
+   let arity_s = L.Any in
+   let body e _ _ _ xl = iter e.L.eval xl in
+   let txt_out o _ = function
+      | [x1; x2]     -> let o = L.std o in L.out_txt2 o "||" x1 x2
+      | xl           -> let o = L.std o in L.out_txt_ o ["or"] xl  
+   in
+   {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
+
+let _ = L.fun_register ["or"] or_fun
+
+(* AND **********************************************************************)
+
+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 = L.Const 0 in
+   let arity_s = L.Any in
+   let body e _ _ _ xl = iter e.L.eval xl in
+   let txt_out o _ = function 
+      | [x1; x2]  -> let o = L.std o in L.out_txt2 o "&&" x1 x2
+      | xl        -> let o = L.std o in L.out_txt_ o ["and"] xl
+   in
+   {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
+
+let _ = L.fun_register ["and"] and_fun 
+
+(* PROJ *********************************************************************)
+
+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) (List.rev g) in
+   let arity_p = L.Const 1 in
+   let arity_s = L.Const 1 in
+   let body e _ _ pl xl =
+      match pl, xl with
+         | [p], [x] -> U.mql_iter (proj_set p) (e.L.eval x)
+        | _        -> assert false
+   in
+   let txt_out o pl xl =
+      match pl, xl with
+         | [p], [x] -> 
+           let o = L.std o in
+           o.L.s_out "proj "; o.L.s_path p; o.L.s_out " of "; o.L.s_query x
+        | _        -> assert false
+   in
+   {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
+
+let _ = L.fun_register ["proj"] proj_fun
+
+(* KEEP *********************************************************************)
+
+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.L.s_out "allbut " in
+   let txt_path_list o l = P.flat_list o.L.s_out o.L.s_path ", " l in 
+   let arity_p = L.Any in
+   let arity_s = L.Const 1 in
+   let body e _ _ pl xl =
+      match b, pl, xl with
+         | true, [], [x]  -> e.L.eval x
+         | false, [], [x] -> List.map proj (e.L.eval x)
+         | _, l, [x]      -> List.map (keep_av l) (e.L.eval x)
+         | _              -> assert false
+  in
+  let txt_out o pl xl =
+      match pl, xl with
+         | [], [x] -> 
+           let o = L.std o in 
+           o.L.s_out "keep "; txt_allbut o; o.L.s_query x
+        | l, [x]  -> 
+           let o = L.std o in
+           o.L.s_out "keep "; txt_allbut o; txt_path_list o l; 
+           o.L.s_out " in "; o.L.s_query x
+        | _      -> assert false
+   in
+   {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
+
+let _ = L.fun_register ["keep"; "these"] (keep_fun false)
+
+let _ = L.fun_register ["keep"; "allbut"] (keep_fun true)