X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2FmQueryIO.ml;h=14199e513136d396f88380fe130346200d430395;hb=381006cf8b418cfdeaf145ab7df9e8f2b19ae2e6;hp=a7d30dd0910ade259a1a2f549c1a562384b63738;hpb=9cbce40d56958c466459b028cf250441ec29c9fe;p=helm.git diff --git a/helm/ocaml/mathql_interpreter/mQueryIO.ml b/helm/ocaml/mathql_interpreter/mQueryIO.ml index a7d30dd09..14199e513 100644 --- a/helm/ocaml/mathql_interpreter/mQueryIO.ml +++ b/helm/ocaml/mathql_interpreter/mQueryIO.ml @@ -27,31 +27,62 @@ *) module M = MathQL +module I = M.I module P = MQueryUtil module L = MQILib (* text linearization and parsing *******************************************) -let txt_str out s = out ("\"" ^ s ^ "\"") +let txt_quote s = + let rec aux r i l s = + let commit c = + let l = pred (l - i) in + aux (r ^ String.sub s 0 i ^ c) 0 l (String.sub s (succ i) l) + in + if i = l then r ^ s else + match s.[i] with + | '\\' -> commit "\\\\^" + | '^' -> commit "\\^^" + | '\"' -> commit "\\\"^" + | _ -> aux r (succ i) l s + in + aux "" 0 (String.length s) s + +let txt_str out s = out ("\"" ^ txt_quote s ^ "\"") let txt_path out p = out "/"; P.flat_list out (txt_str out) "/" p -let text_of_result out sep x = - let txt_attr = function - | (p, []) -> txt_path out p - | (p, l) -> txt_path out p; out " = "; - P.flat_list out (txt_str out) ", " l +let text_of_result out sep x = + let txt_attr _ p l b = + txt_path out p; + if l <> [] then begin + out " = "; P.flat_list out (txt_str out) ", " l + end; + if b then out ("; " ^ sep) + in + let txt_group l = out "{"; I.x_grp_iter txt_attr () l; out "}" in + let txt_res _ s l b = + txt_str out s; + if l <> [] then begin + out " = "; P.flat_list out txt_group ", " l + end; + if b then out "; " in + I.x_iter txt_res () x; out sep + +let rec xtext_of_groups out l = + let txt_attr (p, x) = txt_path out p; out " = "; text_of_query out "" x in let txt_group l = out "{"; P.flat_list out txt_attr "; " l; out "}" in + P.flat_list out txt_group ", " l + +and xtext_of_result out x = let txt_res = function | (s, []) -> txt_str out s - | (s, l) -> txt_str out s; out " attr "; - P.flat_list out txt_group ", " l + | (s, l) -> txt_str out s; out " attr "; xtext_of_groups out l in - let txt_set l = P.flat_list out txt_res ("; " ^ sep) l; out sep in - txt_set x + P.flat_list out txt_res "; " x -let text_of_query out sep x = +and text_of_query out sep x = let txt_svar sv = out ("$" ^ sv) in let txt_avar av = out ("@" ^ av) in let txt_inv i = if i then out "inverse " in @@ -88,47 +119,53 @@ let text_of_query out sep x = | l -> out s; P.flat_list out txt_con ", " l and txt_istrue lt = txt_con_list " istrue " lt and txt_isfalse lf = txt_con_list " isfalse " lf - and txt_ass (p, x) = txt_set x; out " as "; txt_path out p - and txt_ass_list l = P.flat_list out txt_ass ", " l - and txt_assg_list g = P.flat_list out txt_ass_list "; " g and txt_grp = function - | M.Attr g -> txt_assg_list g + | M.Attr g -> xtext_of_groups out g | M.From av -> txt_avar av and txt_set = function - | M.Fun p pl xl -> - let o = {L.out = out; L.path = txt_path out; L.query = txt_set; - L.result = text_of_result out sep} + | M.Fun (p, pl, xl) -> + let o = {L.out = out; L.path = txt_path; + L.query = text_of_query; L.result = text_of_result + } in - L.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.Property q0 q1 q2 mc ct cfl xl b x -> + L.fun_txt_out o p pl xl + | M.Const [s, []] -> txt_str out s + | M.Const r -> xtext_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.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 let text_out_spec out sep = - {L.out = out; L.path = txt_path out; L.query = text_of_query out sep; - L.result = text_of_result out sep} + {L.out = out; L.path = txt_path; + L.query = text_of_query; L.result = text_of_result + } let query_of_text lexbuf = MQueryTParser.query MQueryTLexer.query_token lexbuf let result_of_text lexbuf = MQueryTParser.result MQueryTLexer.result_token lexbuf + +let text_in_spec = {L.result_in = result_of_text}