X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2FmQueryInterpreter.ml;fp=helm%2Focaml%2Fmathql_interpreter%2FmQueryInterpreter.ml;h=0000000000000000000000000000000000000000;hp=58fb7b87e734545491f893046333a50a85265bf0;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml deleted file mode 100644 index 58fb7b87e..000000000 --- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml +++ /dev/null @@ -1,243 +0,0 @@ -(* 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 - *) - -(* contexts *****************************************************************) - -type svar_context = (MathQL.svar * MathQL.resource_set) list - -type avar_context = (MathQL.avar * MathQL.resource) list - -type group_context = (MathQL.avar * MathQL.attribute_group) list - -type vvar_context = (MathQL.vvar * MathQL.value) list - -type context = {svars: svar_context; - avars: avar_context; - groups: group_context; (* auxiliary context *) - vvars: vvar_context - } - -(* execute *****************************************************************) - -exception Found - -module M = MathQL -module P = MQueryUtil -module C = MQIConn -module U = MQIUtil - -let execute h x = - let warn q = - if C.set h C.Warn then - begin - C.log h "MQIExecute: waring: reference to undefined variables: "; - P.text_of_query (C.log h) q "\n" - end - in - let rec eval_val c = function - | M.False -> U.mql_false - | M.True -> U.mql_true - | M.Const s -> [s] - | M.Set l -> U.iter (eval_val c) l - | M.Test k y1 y2 -> - let cand y1 y2 = - if eval_val c y1 = U.mql_false then U.mql_false else eval_val c y2 - in - let cor y1 y2 = - let v1 = eval_val c y1 in - if v1 = U.mql_false then eval_val c y2 else v1 - in - let h f y1 y2 = f (eval_val c y1) (eval_val c y2) in - let f = match k with - | M.And -> cand - | M.Or -> cor - | M.Xor -> h U.xor - | M.Sub -> h U.set_sub - | M.Meet -> h U.set_meet - | M.Eq -> h U.set_eq - | M.Le -> h U.le - | M.Lt -> h U.lt - in - f y1 y2 - | M.Not y -> - if eval_val c y = U.mql_false then U.mql_true else U.mql_false - | M.VVar i -> begin - try List.assoc i c.vvars - with Not_found -> warn (M.Subj (M.VVar i)); [] end - | M.Dot i p -> begin - try List.assoc p (List.assoc i c.groups) - with Not_found -> warn (M.Subj (M.Dot i p)); [] end - | M.Proj None x -> List.map (fun (r, _) -> r) (eval_query c x) - | M.Proj (Some p) x -> - let proj_group_aux (q, v) = if q = p then v else [] in - let proj_group a = U.iter proj_group_aux a in - let proj_set (_, g) = U.iter proj_group g in - U.iter proj_set (eval_query c x) - | M.Ex l y -> - let rec ex_aux h = function - | [] -> - let d = {c with groups = h} in - if eval_val d y = U.mql_false then () else raise Found - | i :: tail -> - begin - try - let (_, a) = List.assoc i c.avars in - let rec add_group = function - | [] -> () - | g :: t -> ex_aux ((i, g) :: h) tail; add_group t - in - add_group a - with Not_found -> () - end - in - (try ex_aux [] l; U.mql_false with Found -> U.mql_true) - | M.StatVal y -> - let t = P.start_time () in - let r = (eval_val c y) in - let s = P.stop_time t in - C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r)); - r - | M.Count y -> [string_of_int (List.length (eval_val c y))] - | M.Align s y -> U.iter (U.align s) (eval_val c y) - and eval_query c = function - | M.Empty -> [] - | M.Subj x -> - List.map (fun s -> (s, [])) (eval_val c x) - | M.Log _ b x -> - if b then begin - let t = P.start_time () in - P.text_of_query (C.log h) x "\n"; - let s = P.stop_time t in - if C.set h C.Stat then - C.log h (Printf.sprintf "Log source: %s\n" s); - eval_query c x - end else begin - let s = (eval_query c x) in - let t = P.start_time () in - P.text_of_result (C.log h) s "\n"; - let r = P.stop_time t in - if C.set h C.Stat then - C.log h (Printf.sprintf "Log: %s\n" r); - s - end - | M.If y x1 x2 -> - if (eval_val c y) = U.mql_false - then (eval_query c x2) else (eval_query c x1) - | M.Bin k x1 x2 -> - let f = match k with - | M.BinFJoin -> U.mql_union - | M.BinFMeet -> U.mql_intersect - | M.BinFDiff -> U.mql_diff - in - f (eval_query c x1) (eval_query c x2) - | 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.LetSVar i x1 x2 -> - let d = {c with svars = U.set (i, eval_query c x1) c.svars} in - eval_query d x2 - | M.LetVVar i y x -> - let d = {c with vvars = U.set (i, eval_val c y) c.vvars} in - eval_query d x - | 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 - | [] -> [] - | h :: t -> - let d = {c with avars = U.set (i, h) c.avars} in - f (eval_query d x2) (for_aux t) - in - for_aux (eval_query c x1) - | 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) [] - | M.Property q0 q1 q2 mc ct cfl el pat y -> - let subj, mct = - if q0 then [], (pat, q2 @ mc, eval_val c y) - else (q2 @ mc), (pat, [], eval_val c y) - in - let eval_cons (pat, p, y) = (pat, q2 @ p, eval_val 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 - let exp = List.map eval_exp el in - let t = P.start_time () in - let r = MQIProperty.exec h q1 subj cons_true cons_false exp in - 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 - | M.StatQuery x -> - let t = P.start_time () in - let r = (eval_query c x) in - let s = P.stop_time t in - C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r)); - r - | M.Select i x y -> - let rec select_aux = function - | [] -> [] - | h :: t -> - let d = {c with avars = U.set (i, h) c.avars} in - if eval_val d y = U.mql_false - then select_aux t else h :: select_aux t - in - select_aux (eval_query c x) - | M.Keep b l x -> - let keep_path (p, v) t = - if List.mem p l = b then t else (p, v) :: t in - let keep_grp a = List.fold_right keep_path a [] in - let keep_set a g = - let kg = keep_grp a in - if kg = [] then g else kg :: g - in - let keep_av (s, g) = (s, List.fold_right keep_set g []) in - List.map keep_av (eval_query c x) - and eval_grp c = function - | M.Attr gs -> - let attr_aux g (p, y) = U.mql_union g [(p, eval_val c y)] 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 -> - try snd (List.assoc i c.avars) - with Not_found -> warn (M.AVar i); [] - in - let c = {svars = []; avars = []; groups = []; vvars = []} in - let t = P.start_time () 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 - (C.string_of_flags (C.flags h))); - r