From: Ferruccio Guidi Date: Tue, 9 Dec 2003 10:28:44 +0000 (+0000) Subject: standard library and while construction inserted X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=cf13d8dc120ae8745b26f8dbadea5af3f3b2193c standard library and while construction inserted --- diff --git a/helm/ocaml/mathql_interpreter/.depend b/helm/ocaml/mathql_interpreter/.depend index 3d89ece9a..4bad2ad26 100644 --- a/helm/ocaml/mathql_interpreter/.depend +++ b/helm/ocaml/mathql_interpreter/.depend @@ -27,3 +27,5 @@ mQueryInterpreter.cmo: mQIConn.cmi mQILib.cmi mQIProperty.cmi mQIUtil.cmi \ mQueryIO.cmi mQueryInterpreter.cmi mQueryInterpreter.cmx: mQIConn.cmx mQILib.cmx mQIProperty.cmx mQIUtil.cmx \ mQueryIO.cmx mQueryInterpreter.cmi +mQueryStandard.cmo: mQIConn.cmi mQILib.cmi mQIUtil.cmi mQueryStandard.cmi +mQueryStandard.cmx: mQIConn.cmx mQILib.cmx mQIUtil.cmx mQueryStandard.cmi diff --git a/helm/ocaml/mathql_interpreter/Makefile b/helm/ocaml/mathql_interpreter/Makefile index c82572648..48859300b 100644 --- a/helm/ocaml/mathql_interpreter/Makefile +++ b/helm/ocaml/mathql_interpreter/Makefile @@ -1,5 +1,5 @@ PACKAGE = mathql_interpreter -REQUIRES = helm-urimanager helm-mathql postgres +REQUIRES = postgres helm-mathql #natile-galax PREDICATES = @@ -7,7 +7,7 @@ PREDICATES = PRE_IFILES = mQIPostgres.mli mQIMap.mli mQIConn.mli \ mQIUtil.mli mQILib.mli mQIProperty.mli -POST_IFILES = mQueryIO.mli mQueryInterpreter.mli +POST_IFILES = mQueryIO.mli mQueryInterpreter.mli mQueryStandard.mli INTERFACE_FILES = $(PRE_IFILES) $(POST_IFILES) 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 diff --git a/helm/ocaml/mathql_interpreter/mQILib.mli b/helm/ocaml/mathql_interpreter/mQILib.mli index f5e187457..bfac2b4ff 100644 --- a/helm/ocaml/mathql_interpreter/mQILib.mli +++ b/helm/ocaml/mathql_interpreter/mQILib.mli @@ -60,4 +60,45 @@ 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 diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.ml b/helm/ocaml/mathql_interpreter/mQIUtil.ml index d0e127c64..8d5782dea 100644 --- a/helm/ocaml/mathql_interpreter/mQIUtil.ml +++ b/helm/ocaml/mathql_interpreter/mQIUtil.ml @@ -128,3 +128,13 @@ let xor v1 v2 = let b = v1 <> mql_false in if b && v2 <> mql_false then mql_false else if b then v1 else v2 + +(* numeric operations *******************************************************) + +exception NumberError of MathQL.result + +let int_of_set r = + try match r with + | [s, _] -> MQueryUtil.int_of_string s + | _ -> raise (Failure "int_of_string") + with Failure "int_of_string" -> raise (NumberError r) diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.mli b/helm/ocaml/mathql_interpreter/mQIUtil.mli index cd7adc760..f6063ad07 100644 --- a/helm/ocaml/mathql_interpreter/mQIUtil.mli +++ b/helm/ocaml/mathql_interpreter/mQIUtil.mli @@ -60,3 +60,6 @@ val mql_iter2 : ('c -> 'd -> ('a * 'b list) list) -> 'c list -> val xor : MathQL.result -> MathQL.result -> MathQL.result +exception NumberError of MathQL.result + +val int_of_set : MathQL.result -> int diff --git a/helm/ocaml/mathql_interpreter/mQueryIO.ml b/helm/ocaml/mathql_interpreter/mQueryIO.ml index a8fe2006e..5af9c7b10 100644 --- a/helm/ocaml/mathql_interpreter/mQueryIO.ml +++ b/helm/ocaml/mathql_interpreter/mQueryIO.ml @@ -116,29 +116,31 @@ let rec text_of_query out sep x = } in 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 - | M.Ex b x -> out "ex "; txt_set x -(* | M.Ex b x -> out "ex ["; P.flat_list out txt_avar "," b; - out "] "; txt_set x -*) | M.SVar sv -> txt_svar sv - | M.AVar av -> txt_avar av + | 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 + | M.Ex b x -> out "ex "; txt_set x +(* | M.Ex b x -> out "ex ["; P.flat_list out txt_avar "," b; + out "] "; txt_set x +*) | M.SVar sv -> txt_svar sv + | M.AVar av -> txt_avar av | M.Property q0 q1 q2 mc ct cfl xl b x -> out "property "; txt_qualif q0 q1 q2; main mc; txt_istrue ct; P.flat_list out txt_isfalse "" cfl; txt_exp_list xl; out " of "; pattern b; txt_set x - | M.Let sv x y -> out "let "; txt_svar sv; out " = "; - txt_set x; out " in "; txt_set y - | M.Select av x y -> out "select "; txt_avar av; out " from "; - txt_set x; out " where "; txt_set y - | M.For k av x y -> out "for "; txt_avar av; out " in "; - 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 "}" + | M.Let (Some sv) x y -> out "let "; txt_svar sv; out " = "; + txt_set x; out " in "; txt_set y + | M.Let None x y -> txt_set x; out " ;; "; txt_set y + | M.Select av x y -> out "select "; txt_avar av; out " from "; + txt_set x; out " where "; txt_set y + | M.For k av x y -> out "for "; txt_avar av; out " in "; + txt_set x; txt_gen k; txt_set y + | M.While k x y -> out "while "; 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 a852affde..b66228581 100644 --- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml +++ b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml @@ -60,15 +60,17 @@ let execute h x = in let proj v = List.map fst v in let rec eval_query c = function - | M.Const r -> r - | M.Dot i p -> begin - try U.mql_subj (List.assoc p (List.assoc i c.groups)) - with Not_found -> warn (M.Dot i p); [] end + | M.Const r -> c, r + | M.Dot i p -> + begin + try c, U.mql_subj (List.assoc p (List.assoc i c.groups)) + with Not_found -> warn (M.Dot i p); c, [] + end | M.Ex l y -> let rec ex_aux h = function | [] -> let d = {c with groups = h} in - if eval_query d y = U.mql_false then () else raise Found + if snd (eval_query d y) = U.mql_false then () else raise Found | i :: tail -> begin try @@ -81,38 +83,62 @@ let execute h x = with Not_found -> () end in - (try ex_aux [] l; U.mql_false with Found -> U.mql_true) - | M.SVar i -> begin - try List.assoc i c.svars - with Not_found -> warn (M.SVar i); [] end - | M.AVar i -> begin - try [List.assoc i c.avars] - with Not_found -> warn (M.AVar i); [] end - | M.Let i x1 x2 -> - let d = {c with svars = P.add_assoc (i, eval_query c x1) c.svars} in + begin try ex_aux [] l; c, U.mql_false with Found -> c, U.mql_true end + | M.SVar i -> + begin + try c, List.assoc i c.svars + with Not_found -> warn (M.SVar i); c, [] + end + | M.AVar i -> + begin + try c, [List.assoc i c.avars] + with Not_found -> warn (M.AVar i); c, [] + end + | M.Let (Some i) x1 x2 -> + let d, r = eval_query c x1 in + let d = {d with svars = P.add_assoc (i, r) d.svars} in eval_query d x2 + | M.Let None x1 x2 -> + let d, r = eval_query c x1 in eval_query d x2 | M.For k i x1 x2 -> let f = match k with | M.GenFJoin -> U.mql_union | M.GenFMeet -> U.mql_intersect in - let rec for_aux = function - | [] -> [] + let rec for_aux (d, r) = match r with + | [] -> d, [] | h :: t -> - let d = {c with avars = P.add_assoc (i, h) c.avars} in - f (eval_query d x2) (for_aux t) + let d = {d with avars = P.add_assoc (i, h) d.avars} in + let d, r = eval_query d x2 in + let d, s = for_aux (d, t) in + d, f r s in for_aux (eval_query c x1) + | M.While k x1 x2 -> + let f = match k with + | M.GenFJoin -> U.mql_union + | M.GenFMeet -> U.mql_intersect + in + let rec while_aux (d, r) = + let d, b = eval_query d x1 in + if b = U.mql_false then d, r else + let d, s = eval_query d x2 in + while_aux (d, f r s) + in + while_aux (c, U.mql_false) | M.Add b z x -> let f = if b then U.mql_prod else U.set_union in let g a s = (fst a, f (snd a) (eval_grp c z)) :: s in - List.fold_right g (eval_query c x) [] + let _, r = eval_query c x in + c, List.fold_right g r [] | M.Property q0 q1 q2 mc ct cfl el pat y -> + let _, r = eval_query c y in let subj, mct = - if q0 then [], (pat, q2 @ mc, eval_query c y) - else (q2 @ mc), (pat, [], eval_query c y) + if q0 then [], (pat, q2 @ mc, r) else (q2 @ mc), (pat, [], r) + in + let eval_cons (pat, p, y) = + let _, r = eval_query c y in (pat, q2 @ p, r) in - let eval_cons (pat, p, y) = (pat, q2 @ p, eval_query c y) in let cons_true = mct :: List.map eval_cons ct in let cons_false = List.map (List.map eval_cons) cfl in let eval_exp (p, po) = (q2 @ p, po) in @@ -122,26 +148,30 @@ let execute h x = let s = P.stop_time t in if C.set h C.Stat then C.log h (Printf.sprintf "Property: %s,%i\n" s (List.length r)); - r + c, r | M.Select i x y -> - let rec select_aux = function - | [] -> [] + let rec select_aux (d, r) = match r with + | [] -> d, [] | h :: t -> - let d = {c with avars = P.add_assoc (i, h) c.avars} in - if eval_query d y = U.mql_false - then select_aux t else h :: select_aux t + let d = {d with avars = P.add_assoc (i, h) d.avars} in + let d, r = eval_query d y in + let d, s = select_aux (d, t) in + if r = U.mql_false then d, s else d, (h :: s) in select_aux (eval_query c x) - | M.Fun p pl xl -> - let e = {L.eval = eval_query c; L.conn = h} in - L.fun_eval e (F.text_out_spec (C.log h) "\n") F.text_in_spec + | M.Fun p pl xl -> + let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in + c, 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 + let e = {L.eval = (fun x -> snd (eval_query c x)); 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 + let attr_aux g (p, y) = + let _, r = eval_query c y in + U.mql_union g [p, proj r] + in let attr_auxs s l = U.set_union s [List.fold_left attr_aux [] l] in List.fold_left attr_auxs [] gs | M.From i -> @@ -150,7 +180,7 @@ let execute h x = in let c = {svars = []; avars = []; groups = []} in let t = P.start_time () in - let r = eval_query c x in + let _, r = eval_query c x in let s = P.stop_time t in if C.set h C.Stat then C.log h (Printf.sprintf "MQIExecute: %s,%s\n" s diff --git a/helm/ocaml/mathql_interpreter/mQueryStandard.ml b/helm/ocaml/mathql_interpreter/mQueryStandard.ml new file mode 100644 index 000000000..4bd251b14 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQueryStandard.ml @@ -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 + *) + +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) diff --git a/helm/ocaml/mathql_interpreter/mQueryStandard.mli b/helm/ocaml/mathql_interpreter/mQueryStandard.mli new file mode 100644 index 000000000..7aa9fb00b --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQueryStandard.mli @@ -0,0 +1,29 @@ +(* 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 + *) + +val init : unit diff --git a/helm/ocaml/mathql_interpreter/mQueryTLexer.mll b/helm/ocaml/mathql_interpreter/mQueryTLexer.mll index d5f2fe10f..c4abce8e8 100644 --- a/helm/ocaml/mathql_interpreter/mQueryTLexer.mll +++ b/helm/ocaml/mathql_interpreter/mQueryTLexer.mll @@ -75,6 +75,7 @@ and query_token = parse out ("AVAR " ^ id); AVAR (strip id) } | "$" IDEN { let id = Lexing.lexeme lexbuf in out ("SVAR " ^ id); SVAR (strip id) } + | ";;" { out ";;" ; SEQ } | "add" { out "ADD" ; ADD } | "align" { out "ALIGN" ; ALIGN } | "allbut" { out "BUT" ; BUT } @@ -118,7 +119,6 @@ and query_token = parse | "read" { out "READ" ; READ } | "render" { out "RENDER"; RENDER } | "select" { out "SELECT"; SELECT } - | "seq" { out "SEQ" ; SEQ } | "source" { out "SOURCE"; SOURCE } | "stat" { out "STAT" ; STAT } | "sub" { out "SUB" ; SUB } @@ -128,6 +128,7 @@ and query_token = parse | "true" { out "TRUE" ; TRUE } | "union" { out "UNION" ; UNION } | "where" { out "WHERE" ; WHERE } + | "while" { out "WHILE" ; WHILE } | "xor" { out "XOR" ; XOR } | eof { out "EOF" ; EOF } | "=" { out "BE" ; BE } @@ -140,7 +141,6 @@ and query_token = parse | "||" { out "OR" ; OR } | "\\/" { out "UNION" ; UNION } | "/\\" { out "INTER" ; INTER } - | ";;" { out "SEQ" ; SEQ } | "begin" { out "LP" ; LP } | "end" { out "RP" ; RP } and result_token = parse diff --git a/helm/ocaml/mathql_interpreter/mQueryTParser.mly b/helm/ocaml/mathql_interpreter/mQueryTParser.mly index 3265a53a8..4945edfc0 100644 --- a/helm/ocaml/mathql_interpreter/mQueryTParser.mly +++ b/helm/ocaml/mathql_interpreter/mQueryTParser.mly @@ -59,6 +59,7 @@ | M.Let _ x y | M.Select _ x y | M.For _ _ x y -> iter an_set [x; y] + | M.While _ 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) @@ -82,7 +83,7 @@ %token ADD ALIGN AND AS ATTR BE BUT COUNT DIFF DISTR ELSE EMPTY EQ EX %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 + %token SEQ SOURCE STAT SUB SUP SUPER THEN TRUE UNION WHERE WHILE XOR %nonassoc SOURCE %right IN SEQ @@ -231,7 +232,6 @@ | 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] } @@ -253,8 +253,10 @@ | 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 } + | LET svar BE set_exp IN set_exp { M.Let (Some $2) $4 $6 } + | set_exp SEQ set_exp { M.Let None $1 $3 } | FOR avar IN set_exp gen_op { M.For (fst $5) $2 $4 (snd $5) } + | WHILE set_exp gen_op { M.While (fst $3) $2 (snd $3) } | 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 }