From: Ferruccio Guidi Date: Thu, 19 Jun 2003 14:37:12 +0000 (+0000) Subject: MathQL 1.3 ready for use X-Git-Tag: V7_3_new_exportation_merged~20 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=91db309a46f8b6f100a36abbc568deec10a8d1df;p=helm.git MathQL 1.3 ready for use --- diff --git a/helm/ocaml/META.helm-mathql.src b/helm/ocaml/META.helm-mathql.src index fa58fd1ce..df553d7d5 100644 --- a/helm/ocaml/META.helm-mathql.src +++ b/helm/ocaml/META.helm-mathql.src @@ -1,5 +1,5 @@ requires="helm-urimanager" -version="0.0.1" +version="1.3" archive(byte)="mathql.cma" archive(native)="mathql.cmxa" linkopts="" diff --git a/helm/ocaml/META.helm-mathql_generator.src b/helm/ocaml/META.helm-mathql_generator.src index 5a4537763..c4168201b 100644 --- a/helm/ocaml/META.helm-mathql_generator.src +++ b/helm/ocaml/META.helm-mathql_generator.src @@ -1,5 +1,5 @@ -requires="helm-urimanager helm-mathql helm-cic helm-cic_proof_checking" -version="1.2" +requires="helm-cic helm-cic_proof_checking helm-mathql" +version="1.3" archive(byte)="mathql_generator.cma" archive(native)="mathql_generator.cmxa" linkopts="" diff --git a/helm/ocaml/META.helm-mathql_interpreter.src b/helm/ocaml/META.helm-mathql_interpreter.src index 7247741fd..1806188c3 100644 --- a/helm/ocaml/META.helm-mathql_interpreter.src +++ b/helm/ocaml/META.helm-mathql_interpreter.src @@ -1,5 +1,5 @@ -requires="helm-urimanager postgres natile-galax" -version="0.0.1" +requires="helm-cic helm-cic_textual_parser postgres natile-galax helm-mathql" +version="1.3" archive(byte)="mathql_interpreter.cma" archive(native)="mathql_interpreter.cmxa" linkopts="" diff --git a/helm/ocaml/META.helm-mathql_test.src b/helm/ocaml/META.helm-mathql_test.src index 37f737a08..4d66fc34d 100644 --- a/helm/ocaml/META.helm-mathql_test.src +++ b/helm/ocaml/META.helm-mathql_test.src @@ -1 +1,3 @@ -version="1.2" +requires="unix helm-cic_textual_parser helm-mathql helm-mathql_interpreter helm-mathql_generator" +version="1.3" +linkopts="" diff --git a/helm/ocaml/mathql/Makefile b/helm/ocaml/mathql/Makefile index a700bb5ac..6d5481948 100644 --- a/helm/ocaml/mathql/Makefile +++ b/helm/ocaml/mathql/Makefile @@ -1,11 +1,11 @@ PACKAGE = mathql -REQUIRES = helm-urimanager helm-cic helm-cic_textual_parser +REQUIRES = helm-urimanager PREDICATES = -INTERFACE_FILES = mQueryTParser.mli mQueryUtil.mli mQueryMisc.mli +INTERFACE_FILES = mQueryTParser.mli mQueryUtil.mli IMPLEMENTATION_FILES = mathQL.ml mQueryTParser.ml mQueryTLexer.ml \ - mQueryUtil.ml mQueryMisc.ml + mQueryUtil.ml EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi mQueryTLexer.cmi \ mQueryTLexer.mll mQueryTParser.mly diff --git a/helm/ocaml/mathql/mQueryMisc.ml b/helm/ocaml/mathql/mQueryMisc.ml deleted file mode 100644 index 928050679..000000000 --- a/helm/ocaml/mathql/mQueryMisc.ml +++ /dev/null @@ -1,113 +0,0 @@ -(* Copyright (C) 2000-2002, 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/. - *) - -exception IllFormedUri of string;; - -let string_of_cic_textual_parser_uri uri = - let module C = Cic in - let module CTP = CicTextualParser0 in - let uri' = - match uri with - CTP.ConUri uri -> UriManager.string_of_uri uri - | CTP.VarUri uri -> UriManager.string_of_uri uri - | CTP.IndTyUri (uri,tyno) -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) - | CTP.IndConUri (uri,tyno,consno) -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^ - string_of_int consno - in - (* 4 = String.length "cic:" *) - String.sub uri' 4 (String.length uri' - 4) -;; - -let cic_textual_parser_uri_of_string uri' = - prerr_endline ("cic_textual_parser_uri_of_string INPUT = " ^ uri'); - try - (* Constant *) - if String.sub uri' (String.length uri' - 4) 4 = ".con" then - CicTextualParser0.ConUri (UriManager.uri_of_string uri') - else - if String.sub uri' (String.length uri' - 4) 4 = ".var" then - CicTextualParser0.VarUri (UriManager.uri_of_string uri') - else - (try - (* Inductive Type *) - let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in - CicTextualParser0.IndTyUri (uri'',typeno) - with - UriManager.IllFormedUri _ - | CicTextualParser0.LexerFailure _ - | Invalid_argument _ -> - (* Constructor of an Inductive Type *) - let uri'',typeno,consno = - CicTextualLexer.indconuri_of_uri uri' - in - CicTextualParser0.IndConUri (uri'',typeno,consno) - ) - with - UriManager.IllFormedUri _ - | CicTextualParser0.LexerFailure _ - | Invalid_argument _ -> - raise (IllFormedUri uri') -;; -let cic_textual_parser_uri_of_string uri' = - let res = cic_textual_parser_uri_of_string uri' in - prerr_endline ("RESULT: " ^ (string_of_cic_textual_parser_uri res)); - res - -(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *) -let wrong_xpointer_format_from_wrong_xpointer_format' uri = - try - let index_sharp = String.index uri '#' in - let index_rest = index_sharp + 10 in - let baseuri = String.sub uri 0 index_sharp in - let rest = - String.sub uri index_rest (String.length uri - index_rest - 1) - in - baseuri ^ "#" ^ rest - with Not_found -> uri -;; - -let term_of_cic_textual_parser_uri uri = - let module C = Cic in - let module CTP = CicTextualParser0 in - match uri with - CTP.ConUri uri -> C.Const (uri,[]) - | CTP.VarUri uri -> C.Var (uri,[]) - | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[]) - | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) -;; - -(* time handling ***********************************************************) - -type time = float * float - -let start_time () = - (Sys.time (), Unix.time ()) - -let stop_time (s0, u0) = - let s1 = Sys.time () in - let u1 = Unix.time () in - Printf.sprintf "%.2fs,%.2fs" (s1 -. s0) (u1 -. u0) diff --git a/helm/ocaml/mathql/mQueryMisc.mli b/helm/ocaml/mathql/mQueryMisc.mli deleted file mode 100644 index 2605fe286..000000000 --- a/helm/ocaml/mathql/mQueryMisc.mli +++ /dev/null @@ -1,45 +0,0 @@ -(* Copyright (C) 2000-2002, 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/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 15/01/2003 *) -(* *) -(* *) -(******************************************************************************) - -exception IllFormedUri of string - -val string_of_cic_textual_parser_uri : CicTextualParser0.uri -> string -val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri -val term_of_cic_textual_parser_uri: CicTextualParser0.uri -> Cic.term -val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string - -type time -val start_time : unit -> time -val stop_time : time -> string diff --git a/helm/ocaml/mathql/mQueryTLexer.mll b/helm/ocaml/mathql/mQueryTLexer.mll index f677ef688..b5366af89 100644 --- a/helm/ocaml/mathql/mQueryTLexer.mll +++ b/helm/ocaml/mathql/mQueryTLexer.mll @@ -23,15 +23,8 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 23/05/2002 *) -(* *) -(* *) -(******************************************************************************) +(* + *) { open MQueryTParser @@ -71,39 +64,64 @@ and query_token = parse | '$' { out "DL"; DL } | '.' { out "FS"; FS } | ',' { out "CM"; CM } + | ';' { out "SC"; SC } | '/' { out "SL"; SL } - | "<-" { out "GETS" ; GETS } + | "add" { out "ADD" ; ADD } + | "align" { out "ALIGN" ; ALIGN } + | "allbut" { out "BUT" ; BUT } | "and" { out "AND" ; AND } + | "as" { out "AS" ; AS } | "attr" { out "ATTR" ; ATTR } | "be" { out "BE" ; BE } + | "count" { out "COUNT" ; COUNT } | "diff" { out "DIFF" ; DIFF } + | "distr" { out "DISTR" ; DISTR } + | "else" { out "ELSE" ; ELSE } + | "empty" { out "EMPTY" ; EMPTY } | "eq" { out "EQ" ; EQ } | "ex" { out "EX" ; EX } | "false" { out "FALSE" ; FALSE } - | "fun" { out "FUN" ; FUN } + | "for" { out "FOR" ; FOR } + | "from" { out "FROM" ; FROM } + | "if" { out "IF" ; IF } | "in" { out "IN" ; IN } + | "inf" { out "INF" ; INF } | "intersect" { out "INTER" ; INTER } - | "inverse" { out "INV" ; INV } + | "inverse" { out "INV" ; INV } + | "istrue" { out "IST" ; IST } + | "isfalse" { out "ISF" ; ISF } + | "keep" { out "KEEP" ; KEEP } + | "le" { out "LE" ; LE } | "let" { out "LET" ; LET } + | "log" { out "LOG" ; LOG } + | "lt" { out "LT" ; LT } + | "main" { out "MAIN" ; MAIN } + | "match" { out "MATCH" ; MATCH } | "meet" { out "MEET" ; MEET } | "not" { out "NOT" ; NOT } + | "of" { out "OF" ; OF } | "or" { out "OR" ; OR } | "pattern" { out "PAT" ; PAT } + | "proj" { out "PROJ" ; PROJ } | "property" { out "PROP" ; PROP } - | "ref" { out "REF" ; REF } - | "refof" { out "REFOF" ; REFOF } - | "relation" { out "REL" ; REL } | "select" { out "SELECT"; SELECT } + | "source" { out "SOURCE"; SOURCE } + | "stat" { out "STAT" ; STAT } | "sub" { out "SUB" ; SUB } + | "subj" { out "SUBJ" ; SUBJ } + | "sup" { out "SUP" ; SUP } | "super" { out "SUPER" ; SUPER } + | "then" { out "THEN" ; THEN } | "true" { out "TRUE" ; TRUE } | "union" { out "UNION" ; UNION } | "where" { out "WHERE" ; WHERE } + | "xor" { out "XOR" ; XOR } | IDEN { let id = Lexing.lexeme lexbuf in out ("ID " ^ id); ID id } | eof { out "EOF" ; EOF } and result_token = parse | SPC { result_token lexbuf } + | "(*" { comm_token lexbuf; result_token lexbuf } | '"' { STR (qstr string_token lexbuf) } | '{' { LC } | '}' { RC } diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly index 390c214b4..707b7dd6c 100644 --- a/helm/ocaml/mathql/mQueryTParser.mly +++ b/helm/ocaml/mathql/mQueryTParser.mly @@ -23,70 +23,85 @@ * http://cs.unibo.it/helm/. */ -/******************************************************************************/ -/* */ -/* PROJECT HELM */ -/* */ -/* Ferruccio Guidi */ -/* 23/05/2002 */ -/* */ -/* */ -/******************************************************************************/ +/* + */ %{ + module M = MathQL + let analyze x = - let module M = MathQL in let rec join l1 l2 = match l1, l2 with | [], _ -> l2 | _, [] -> l1 - | s1 :: tl1, s2 :: _ when s1 < s2 -> s1 :: join tl1 l2 - | s1 :: _, s2 :: tl2 when s2 < s1 -> s2 :: join l1 tl2 + | s1 :: tl1, s2 :: _ when s1 < s2 -> s1 :: join tl1 l2 + | s1 :: _, s2 :: tl2 when s2 < s1 -> s2 :: join l1 tl2 | s1 :: tl1, s2 :: tl2 -> s1 :: join tl1 tl2 in + let rec iter f = function + | [] -> [] + | head :: tail -> join (f head) (iter f tail) + in let rec an_val = function - | M.Const _ -> [] - | M.VVar _ -> [] - | M.Record (rv, _) -> [rv] - | M.Fun (_, x) -> an_val x - | M.Property (_, _, _, x) -> an_val x - | M.RefOf x -> an_set x - and an_boole = function - | M.False -> [] - | M.True -> [] - | M.Ex _ -> [] - | M.Not x -> an_boole x - | M.And (x, y) -> join (an_boole x) (an_boole y) - | M.Or (x, y) -> join (an_boole x) (an_boole y) - | M.Sub (x, y) -> join (an_val x) (an_val y) - | M.Meet (x, y) -> join (an_val x) (an_val y) - | M.Eq (x, y) -> join (an_val x) (an_val y) + | M.True -> [] + | M.False -> [] + | M.Const _ -> [] + | M.VVar _ -> [] + | M.Ex _ -> [] + | M.Dot rv _ -> [rv] + | M.Not x -> an_val x + | M.StatVal x -> an_val x + | M.Count x -> an_val x + | M.Align _ x -> an_val x + | M.Proj _ x -> an_set x + | M.Test _ x y -> iter an_val [x; y] + | M.Set l -> iter an_val l and an_set = function - | M.SVar _ -> [] - | M.RVar _ -> [] - | M.Relation (_, _, _, x, _) -> an_set x - | M.Pattern x -> an_val x - | M.Ref x -> an_val x - | M.Union (x, y) -> join (an_set x) (an_set y) - | M.Intersect (x, y) -> join (an_set x) (an_set y) - | M.Diff (x, y) -> join (an_set x) (an_set y) - | M.LetSVar (_, x, y) -> join (an_set x) (an_set y) - | M.LetVVar (_, x, y) -> join (an_val x) (an_set y) - | M.Select (_, x, y) -> join (an_set x) (an_boole y) + | M.Empty -> [] + | M.SVar _ -> [] + | M.AVar _ -> [] + | M.Subj x -> an_val x + | M.Keep _ _ x -> an_set x + | M.Log _ _ x -> an_set x + | M.StatQuery x -> an_set x + | M.Bin _ x y -> iter an_set [x; y] + | M.LetSVar _ x y -> iter an_set [x; y] + | M.For _ _ x y -> iter an_set [x; y] + | M.Add _ g x -> join (an_grp g) (an_set x) + | M.LetVVar _ x y -> join (an_val x) (an_set y) + | M.Select _ x y -> join (an_set x) (an_val y) + | M.Property _ _ _ _ c d _ _ x -> + join (an_val x) (iter an_con [c; List.concat d]) + | M.If x y z -> join (an_val x) (iter an_set [y; z]) + and fc (_, _, v) = an_val v + and an_con c = iter fc c + and fg (_, v) = an_val v + and an_grp = function + | M.Attr g -> iter (iter fg) g + | M.From _ -> [] in - an_boole x + an_val x - let path_of_vvar v = (v, []) + let f (x, y, z) = x + let s (x, y, z) = y + let t (x, y, z) = z %} %token ID STR - %token SL IS LC RC CM SC LP RP AT PC DL FS DQ GETS EOF - %token AND ATTR BE DIFF EQ EX FALSE FUN IN INTER INV LET MEET NOT OR PAT - %token PROP REF REFOF REL SELECT SUB SUPER TRUE UNION WHERE - %left DIFF WHERE REFOF - %left OR UNION - %left AND INTER - %nonassoc REL - %nonassoc NOT EX IN ATTR - + %token SL IS LC RC CM SC LP RP AT PC DL FS DQ EOF + %token ADD ALIGN AND AS ATTR BE BUT COUNT DIFF DISTR ELSE EMPTY EQ EX + %token FALSE FOR FROM IF IN INF INTER INV ISF IST KEEP LE LET LOG LT + %token MAIN MATCH MEET NOT OF OR PAT PROJ PROP SELECT SOURCE STAT SUB + %token SUBJ SUP SUPER THEN TRUE UNION WHERE XOR + %nonassoc IN SUP INF ELSE LOG STAT + %left DIFF + %left UNION + %left INTER + %nonassoc WHERE EX + %left XOR OR + %left AND + %nonassoc NOT + %nonassoc SUB MEET EQ LT LE + %nonassoc SUBJ OF PROJ COUNT ALIGN + %start qstr query result %type qstr %type query @@ -99,7 +114,7 @@ svar: | PC ID { $2 } ; - rvar: + avar: | AT ID { $2 } ; vvar: @@ -114,62 +129,156 @@ | STR { [$1] } ; path: - | STR SL subpath { ($1, $3) } - | STR { ($1, []) } + | subpath { $1 } + | SL subpath { $2 } + | SL { [] } ; + paths: + | path CM paths { $1 :: $3 } + | path { [$1] } inv: | INV { true } | { false } ; ref: - | SUB { MathQL.RefineSub } - | SUPER { MathQL.RefineSuper } - | { MathQL.RefineExact } + | SUB { M.RefineSub } + | SUPER { M.RefineSuper } + | { M.RefineExact } + ; + qualif: + | inv ref path { $1, $2, $3 } + ; + cons: + | path IN val_exp { (false, $1, $3) } + | path MATCH val_exp { (true, $1, $3) } + ; + conss: + | cons CM conss { $1 :: $3 } + | cons { [$1] } + ; + istrue: + | IST conss { $2 } + | { [] } ; - assign: - | vvar GETS path { (path_of_vvar $1, $3) } + isfalse: + | { [] } + | ISF conss isfalse { $2 :: $3 } ; - assigns: - | assign CM assigns { $1 :: $3 } - | assign { [$1] } + mainc: + | MAIN path { $2 } + | { [] } + ; + exp: + | path AS path { $1, Some $3 } + | path { $1, None } + ; + exps: + | exp CM exps { $1 :: $3 } + | exp { [$1] } ; + attrc: + | ATTR exps { $2 } + | { [] } + ; + pattern: + | PAT { true } + | { false } + ; + opt_path: + | path { Some $1 } + | { None } + ; + ass: + | val_exp AS path { ($3, $1) } + ; + asss: + | ass CM asss { $1 :: $3 } + | ass { [$1] } + ; + assg: + | asss SC assg { $1 :: $3 } + | asss { [$1] } + ; + distr: + | DISTR { true } + | { false } + ; + allbut: + | BUT { true } + | { false } + ; + bin_op: + | set_exp DIFF set_exp { M.BinFDiff, $1, $3 } + | set_exp UNION set_exp { M.BinFJoin, $1, $3 } + | set_exp INTER set_exp { M.BinFMeet, $1, $3 } + ; + gen_op: + | SUP set_exp { M.GenFJoin, $2 } + | INF set_exp { M.GenFMeet, $2 } + ; + test_op: + | val_exp XOR val_exp { M.Xor, $1, $3 } + | val_exp OR val_exp { M.Or, $1, $3 } + | val_exp AND val_exp { M.And, $1, $3 } + | val_exp SUB val_exp { M.Sub, $1, $3 } + | val_exp MEET val_exp { M.Meet, $1, $3 } + | val_exp EQ val_exp { M.Eq, $1, $3 } + | val_exp LE val_exp { M.Le, $1, $3 } + | val_exp LT val_exp { M.Lt, $1, $3 } + ; + source: + | SOURCE { true } + | { false } + ; + xml: + | { false} + ; + grp_exp: + | assg { M.Attr $1 } + | avar { M.From $1 } + ; val_exp: - | STR { MathQL.Const [$1] } - | FUN STR val_exp { MathQL.Fun ($2, $3) } - | PROP inv ref path val_exp { MathQL.Property ($2, $3, $4, $5) } - | rvar FS vvar { MathQL.Record ($1, path_of_vvar $3) } - | vvar { MathQL.VVar $1 } - | LC strs RC { MathQL.Const $2 } - | LC RC { MathQL.Const [] } - | REFOF set_exp { MathQL.RefOf $2 } - | LP val_exp RP { $2 } - ; - boole_exp: - | TRUE { MathQL.True } - | FALSE { MathQL.False } - | LP boole_exp RP { $2 } - | NOT boole_exp { MathQL.Not $2 } - | EX boole_exp { MathQL.Ex (analyze $2) $2 } - | val_exp SUB val_exp { MathQL.Sub ($1, $3) } - | val_exp MEET val_exp { MathQL.Meet ($1, $3) } - | val_exp EQ val_exp { MathQL.Eq ($1, $3) } - | boole_exp AND boole_exp { MathQL.And ($1, $3) } - | boole_exp OR boole_exp { MathQL.Or ($1, $3) } + | TRUE { M.True } + | FALSE { M.False } + | STR { M.Const $1 } + | avar FS path { M.Dot $1 $3 } + | vvar { M.VVar $1 } + | LC vals RC { M.Set $2 } + | LC RC { M.Set [] } + | LP val_exp RP { $2 } + | STAT val_exp { M.StatVal $2 } + | EX val_exp { M.Ex (analyze $2) $2 } + | NOT val_exp { M.Not $2 } + | test_op { M.Test (f $1) (s $1) (t $1) } + | PROJ opt_path set_exp { M.Proj $2 $3 } + | COUNT val_exp { M.Count $2 } + | ALIGN STR IN val_exp { M.Align $2 $4 } ; + vals: + | val_exp CM vals { $1 :: $3 } + | val_exp { [$1] } + ; set_exp: - | REF val_exp { MathQL.Ref $2 } - | PAT val_exp { MathQL.Pattern $2 } - | LP set_exp RP { $2 } - | SELECT rvar IN set_exp WHERE boole_exp { MathQL.Select ($2, $4, $6) } - | REL inv ref path val_exp ATTR assigns { MathQL.Relation ($2, $3, $4, MathQL.Ref $5, $7) } - | REL inv ref path val_exp { MathQL.Relation ($2, $3, $4, MathQL.Ref $5, []) } - | svar { MathQL.SVar $1 } - | rvar { MathQL.RVar $1 } - | set_exp UNION set_exp { MathQL.Union ($1, $3) } - | set_exp INTER set_exp { MathQL.Intersect ($1, $3) } - | set_exp DIFF set_exp { MathQL.Diff ($1, $3) } - | LET svar BE set_exp IN set_exp { MathQL.LetSVar ($2, $4, $6) } - | LET vvar BE val_exp IN set_exp { MathQL.LetVVar ($2, $4, $6) } + | EMPTY { M.Empty } + | LP set_exp RP { $2 } + | svar { M.SVar $1 } + | avar { M.AVar $1 } + | LET svar BE set_exp IN set_exp { M.LetSVar $2 $4 $6 } + | LET vvar BE val_exp IN set_exp { M.LetVVar $2 $4 $6 } + | FOR avar IN set_exp gen_op + { M.For (fst $5) $2 $4 (snd $5) } + | ADD distr grp_exp IN set_exp { M.Add $2 $3 $5 } + | IF val_exp THEN set_exp ELSE set_exp { M.If $2 $4 $6 } + | PROP qualif mainc istrue isfalse attrc OF pattern val_exp + { M.Property (f $2) (s $2) (t $2) $3 $4 $5 $6 $8 $9 } + | LOG xml source set_exp { M.Log $2 $3 $4 } + | STAT set_exp { M.StatQuery $2 } + | KEEP allbut paths IN set_exp { M.Keep $2 $3 $5 } + | KEEP allbut IN set_exp { M.Keep $2 [] $4 } + | bin_op + { M.Bin (f $1) (s $1) (t $1) } + | SELECT avar FROM set_exp WHERE val_exp { M.Select $2 $4 $6 } + | SUBJ val_exp { M.Subj $2 } ; query: | set_exp { $1 } @@ -177,8 +286,8 @@ | EOF { raise End_of_file } ; attr: - | vvar IS strs { (path_of_vvar $1, $3) } - | vvar { (path_of_vvar $1, []) } + | path IS strs { $1, $3 } + | path { $1, [] } ; attrs: | attr SC attrs { $1 :: $3 } diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml index ba2382ef9..2de817932 100644 --- a/helm/ocaml/mathql/mQueryUtil.ml +++ b/helm/ocaml/mathql/mQueryUtil.ml @@ -23,16 +23,8 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 30/04/2002 *) -(* *) -(* *) -(******************************************************************************) - +(* + *) (* text linearization and parsing *******************************************) @@ -43,73 +35,139 @@ let rec txt_list out f s = function let txt_str out s = out ("\"" ^ s ^ "\"") -let txt_path out (p0, p1) = - txt_str out p0; if p1 <> [] then out "/"; txt_list out (txt_str out) "/" p1 - -let txt_svar out sv = out ("%" ^ sv) - -let txt_rvar out rv = out ("@" ^ rv) - -let txt_vvar out vv = out ("$" ^ vv) +let txt_path out p = out "/"; txt_list out (txt_str out) "/" p let text_of_query out x sep = - let module M = MathQL in + let module M = MathQL in + let txt_path_list l = txt_list out (txt_path out) ", " l in + let txt_svar sv = out ("%" ^ sv) in + let txt_avar av = out ("@" ^ av) in + let txt_vvar vv = out ("$" ^ vv) in let txt_inv i = if i then out "inverse " in let txt_ref = function | M.RefineExact -> () | M.RefineSub -> out "sub " | M.RefineSuper -> out "super " in - let txt_refpath i r p = txt_inv i; txt_ref r; txt_path out p; out " " in - let txt_assign (pl, pr) = txt_vvar out (fst pl); out " <- "; txt_path out pr in - let rec txt_val = function - | M.Const [s] -> txt_str out s - | M.Const l -> out "{"; txt_list out (txt_str out) ", " l; out "}" - | M.VVar vv -> txt_vvar out vv - | M.Record (rv, p) -> txt_rvar out rv; out "."; txt_vvar out (fst p) - | M.Fun (s, x) -> out "fun "; txt_str out s; out " "; txt_val x - | M.Property (i, r, p, x) -> out "property "; txt_refpath i r p; txt_val x - | M.RefOf x -> out "refof "; txt_set x - and txt_boole = function - | M.False -> out "false" - | M.True -> out "true" - | M.Ex b x -> out "ex "; txt_boole x -(* | M.Ex b x -> "ex [" ^ txt_list txt_rvar "," b ^ "] " ^ txt_boole x -*) | M.Not x -> out "not "; txt_boole x - | M.And (x, y) -> out "("; txt_boole x; out " and "; txt_boole y; out ")" - | M.Or (x, y) -> out "("; txt_boole x; out " or "; txt_boole y; out ")" - | M.Sub (x, y) -> out "("; txt_val x; out " sub "; txt_val y; out ")" - | M.Meet (x, y) -> out "("; txt_val x; out " meet "; txt_val y; out ")" - | M.Eq (x, y) -> out "("; txt_val x; out " eq "; txt_val y; out ")" + let txt_qualif i r p = txt_inv i; txt_ref r; txt_path out p in + let main = function + | [] -> () + | p -> out " main "; txt_path out p + in + let txt_exp = function + | (pl, None) -> txt_path out pl + | (pl, Some pr) -> txt_path out pl; out " as "; txt_path out pr + in + let txt_exp_list = function + | [] -> () + | l -> out " attr "; txt_list out txt_exp ", " l + in + let pattern b = if b then out "pattern " in + let txt_opt_path = function + | None -> () + | Some p -> txt_path out p; out " " + in + let txt_distr d = if d then out "distr " in + let txt_bin = function + | M.BinFJoin -> out " union " + | M.BinFMeet -> out " intersect " + | M.BinFDiff -> out " diff " + in + let txt_gen = function + | M.GenFJoin -> out " sup " + | M.GenFMeet -> out " inf " + in + let txt_test = function + | M.Xor -> out " xor " + | M.Or -> out " or " + | M.And -> out " and " + | M.Sub -> out " sub " + | M.Meet -> out " eq " + | M.Eq -> out " eq " + | M.Le -> out " le " + | M.Lt -> out " lt " + in + let txt_log a b = + if a then out "xml "; + if b then out "source " + in + let txt_allbut b = if b then out "allbut " in + let rec txt_con (pat, p, x) = + txt_path out p; + if pat then out " match " else out " in "; + txt_val x + and txt_con_list s = function + | [] -> () + | l -> out s; txt_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_val x; out " as "; txt_path out p + and txt_ass_list l = txt_list out txt_ass ", " l + and txt_assg_list g = txt_list out txt_ass_list "; " g + and txt_val_list = function + | [v] -> txt_val v + | l -> out "{"; txt_list out txt_val ", " l; out "}" + and txt_grp = function + | M.Attr g -> txt_assg_list g + | M.From av -> txt_avar av + and txt_val = function + | M.True -> out "true" + | M.False -> out "false" + | M.Const s -> txt_str out s + | M.Set l -> txt_val_list l + | M.VVar vv -> txt_vvar vv + | M.Dot av p -> txt_avar av; out "."; txt_path out p + | M.Proj op x -> out "proj "; txt_opt_path op; txt_set x + | M.Ex b x -> out "ex "; txt_val x +(* | M.Ex b x -> out "ex ["; txt_list out txt_avar "," b; out "] "; txt_val x +*) | M.Not x -> out "not "; txt_val x + | M.Test k x y -> out "("; txt_val x; txt_test k; txt_val y; out ")" + | M.StatVal x -> out "stat "; txt_val x + | M.Count x -> out "count "; txt_val x + | M.Align s x -> out "align "; txt_str out s; out " in "; txt_val x and txt_set = function - | M.SVar sv -> txt_svar out sv - | M.RVar rv -> txt_rvar out rv - | M.Relation (i, r, p, M.Ref x, []) -> out "relation "; txt_refpath i r p; txt_val x - | M.Relation (i, r, p, M.Ref x, l) -> out "relation "; txt_refpath i r p; txt_val x; out " attr "; txt_list out txt_assign ", " l - | M.Union (x, y) -> out "("; txt_set x; out " union "; txt_set y; out ")" - | M.Intersect (x, y) -> out "("; txt_set x; out " intersect "; txt_set y; out ")" - | M.Diff (x, y) -> out "("; txt_set x; out " diff "; txt_set y; out ")" - | M.LetSVar (sv, x, y) -> out "let "; txt_svar out sv; out " be "; txt_set x; out " in "; txt_set y - | M.LetVVar (vv, x, y) -> out "let "; txt_vvar out vv; out " be "; txt_val x; out " in "; txt_set y - | M.Select (rv, x, y) -> out "select "; txt_rvar out rv; out " in "; txt_set x; out " where "; txt_boole y - | M.Pattern x -> out "pattern "; txt_val x - | M.Ref x -> out "ref "; txt_val x - | _ -> assert false + | M.Empty -> out "empty" + | 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; txt_list out txt_isfalse "" cfl; txt_exp_list xl; + out " of "; pattern b; txt_val x + | M.Bin k x y -> out "("; txt_set x; txt_bin k; txt_set y; + out ")" + | M.LetSVar sv x y -> out "let "; txt_svar sv; out " be "; + txt_set x; out " in "; txt_set y + | M.LetVVar vv x y -> out "let "; txt_vvar vv; out " be "; + txt_val x; out " in "; txt_set y + | M.Select av x y -> out "select "; txt_avar av; out " from "; + txt_set x; out " where "; txt_val y + | M.Subj x -> out "subj "; txt_val x + | M.For k av x y -> out "for "; txt_avar av; out " in "; + txt_set x; txt_gen k; txt_set y + | M.If x y z -> out "if "; txt_val x; out " then "; + txt_set y; out " else "; txt_set z + | M.Add d g x -> out "add "; txt_distr d; txt_grp g; + out " in "; txt_set x + | M.Log a b x -> out "log "; txt_log a b; txt_set x + | M.StatQuery x -> out "stat "; txt_set x + | M.Keep b l x -> out "keep "; txt_allbut b; txt_path_list l; + txt_set x + in txt_set x; out sep -let text_of_result out x sep = +let text_of_result out x sep = let txt_attr = function - | (p, []) -> txt_vvar out (fst p) - | (p, l) -> txt_vvar out (fst p); out " = "; txt_list out (txt_str out) ", " l + | (p, []) -> txt_path out p + | (p, l) -> txt_path out p; out " = "; txt_list out (txt_str out) ", " l in let txt_group l = out "{"; txt_list out txt_attr "; " l; out "}" in let txt_res = function | (s, []) -> txt_str out s | (s, l) -> txt_str out s; out " attr "; txt_list out txt_group ", " l in - let txt_set l = txt_list out txt_res ("; " ^ sep) l in - txt_set x; out sep + let txt_set l = txt_list out txt_res ("; " ^ sep) l; out sep in + txt_set x let query_of_text lexbuf = MQueryTParser.query MQueryTLexer.query_token lexbuf @@ -117,6 +175,18 @@ let query_of_text lexbuf = let result_of_text lexbuf = MQueryTParser.result MQueryTLexer.result_token lexbuf +(* time handling ***********************************************************) + +type time = float * float + +let start_time () = + (Sys.time (), Unix.time ()) + +let stop_time (s0, u0) = + let s1 = Sys.time () in + let u1 = Unix.time () in + Printf.sprintf "%.2fs,%.2fs" (s1 -. s0) (u1 -. u0) + (* conversion functions *****************************************************) type uriref = UriManager.uri * (int list) @@ -129,3 +199,4 @@ let string_of_uriref (uri, fi) = | [] -> str | [t] -> str ^ xp t ^ ")" | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" + diff --git a/helm/ocaml/mathql/mQueryUtil.mli b/helm/ocaml/mathql/mQueryUtil.mli index 83337ddfb..53d612e82 100644 --- a/helm/ocaml/mathql/mQueryUtil.mli +++ b/helm/ocaml/mathql/mQueryUtil.mli @@ -42,8 +42,13 @@ val query_of_text : Lexing.lexbuf -> MathQL.query val result_of_text : Lexing.lexbuf -> MathQL.result +type time + +val start_time : unit -> time + +val stop_time : time -> string + type uriref = UriManager.uri * (int list) val string_of_uriref : uriref -> string - diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml index 61a7646aa..191090c4f 100644 --- a/helm/ocaml/mathql/mathQL.ml +++ b/helm/ocaml/mathql/mathQL.ml @@ -23,21 +23,12 @@ * http://www.cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* Irene Schena *) -(* 10/09/2002 *) -(* *) -(* *) -(******************************************************************************) - +(* + *) (* output data structures ***************************************************) -type path = string * (string list) (* the name of an attribute *) +type path = string list (* the name of an attribute *) type value = string list (* the value of an attribute *) @@ -58,7 +49,7 @@ type result = resource_set type svar = string (* the name of a variable for a resource set *) -type rvar = string (* the name of a variable for a resource *) +type avar = string (* the name of a variable for a resource *) type vvar = string (* the name of a variable for an attribute value *) @@ -68,35 +59,73 @@ type refine = RefineExact | RefineSub | RefineSuper -type assign = path * path - -type set_exp = SVar of svar - | RVar of rvar - | Ref of val_exp - | Pattern of val_exp - | Relation of inverse * refine * path * set_exp * assign list - | Select of rvar * set_exp * boole_exp - | Union of set_exp * set_exp - | Intersect of set_exp * set_exp - | Diff of set_exp * set_exp - | LetSVar of svar * set_exp * set_exp - | LetVVar of vvar * val_exp * set_exp - -and boole_exp = False - | True - | Not of boole_exp - | Ex of rvar list * boole_exp - | And of boole_exp * boole_exp - | Or of boole_exp * boole_exp - | Sub of val_exp * val_exp - | Meet of val_exp * val_exp - | Eq of val_exp * val_exp - -and val_exp = Const of string list - | RefOf of set_exp - | Record of rvar * path - | VVar of vvar - | Property of inverse * refine * path * val_exp - | Fun of string * val_exp - -type query = set_exp +type main = path + +type pattern = bool + +type exp = path * (path option) + +type exp_list = exp list + +type allbut = bool + +type xml = bool + +type source = bool + +type bin = BinFJoin (* full union - with attr handling *) + | BinFMeet (* full intersection - with attr handling *) + | BinFDiff (* full difference - with attr handling *) + +type gen = GenFJoin (* full union - with attr handling *) + | GenFMeet (* full intersection - with attr handling *) + +type test = Xor + | Or + | And + | Sub + | Meet + | Eq + | Le + | Lt + +type query = Empty + | SVar of svar + | AVar of avar + | Subj of msval + | Property of inverse * refine * path * + main * istrue * isfalse list * exp_list * + pattern * msval + | Select of avar * query * msval + | Bin of bin * query * query + | LetSVar of svar * query * query + | LetVVar of vvar * msval * query + | For of gen * avar * query * query + | Add of bool * groups * query + | If of msval * query * query + | Log of xml * source * query + | StatQuery of query + | Keep of allbut * path list * query + +and msval = False + | True + | Not of msval + | Ex of avar list * msval + | Test of test * msval * msval + | Const of string + | Set of msval list + | Proj of path option * query + | Dot of avar * path + | VVar of vvar + | StatVal of msval + | Count of msval + | Align of string * msval + +and groups = Attr of (path * msval) list list + | From of avar + +and con = pattern * path * msval + +and istrue = con list + +and isfalse = con list diff --git a/helm/ocaml/mathql_generator/Makefile b/helm/ocaml/mathql_generator/Makefile index 6675c58e8..a694e0376 100644 --- a/helm/ocaml/mathql_generator/Makefile +++ b/helm/ocaml/mathql_generator/Makefile @@ -1,10 +1,12 @@ PACKAGE = mathql_generator -REQUIRES = helm-urimanager helm-mathql helm-cic helm-cic_proof_checking + +REQUIRES = helm-cic helm-cic_proof_checking helm-mathql + PREDICATES = INTERFACE_FILES = mQueryLevels.mli mQueryLevels2.mli mQueryGenerator.mli -IMPLEMENTATION_FILES = mQueryLevels.ml mQueryLevels2.ml mQueryGenerator.ml +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml index ca0e36550..24720d0aa 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.ml +++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml @@ -23,24 +23,146 @@ * http://cs.unibo.it/helm/. *) -(* Query issuing functions **************************************************) - type uri = string type position = string -type depth = int option +type depth = string type sort = string + +type spec = MustObj of uri list * position list * depth list + | MustSort of sort list * position list * depth list + | MustRel of position list * depth list + | OnlyObj of uri list * position list * depth list + | OnlySort of sort list * position list * depth list + | OnlyRel of position list * depth list + | Universe of position list + +let text_of_builtin s = + let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in + if s = ns ^ "MainHypothesis" then "$MH" else + if s = ns ^ "InHypothesis" then "$IH" else + if s = ns ^ "MainConclusion" then "$MC" else + if s = ns ^ "InConclusion" then "$IC" else + if s = ns ^ "InBody" then "$IB" else + if s = ns ^ "Set" then "$SET" else + if s = ns ^ "Prop" then "$PROP" else + if s = ns ^ "Type" then "$TYPE" else s + +let text_of_spec out l = + let rec iter = function + | [] -> () + | [s] -> out "\""; out (text_of_builtin s); out "\"" + | s :: tail -> out "\""; out (text_of_builtin s); out "\", "; iter tail + in + let txt_list l = out "{"; iter l; out "} " in + let txt_spec = function + | MustObj (u, p, d) -> out "mustobj "; txt_list u; txt_list p; txt_list d; out "\n" + | MustSort (s, p, d) -> out "mustsort "; txt_list s; txt_list p; txt_list d; out "\n" + | MustRel ( p, d) -> out "mustrel "; txt_list p; txt_list d; out "\n" + | OnlyObj (u, p, d) -> out "onlyobj "; txt_list u; txt_list p; txt_list d; out "\n" + | OnlySort (s, p, d) -> out "onlysort "; txt_list s; txt_list p; txt_list d; out "\n" + | OnlyRel ( p, d) -> out "onlyrel "; txt_list p; txt_list d; out "\n" + | Universe ( p ) -> out "universe "; txt_list p; out "\n" + in + List.iter txt_spec l -type r_obj = (uri * position * depth) -type r_rel = (position* depth) -type r_sort = (position* depth * sort) +module M = MathQL -type must_restrictions = (r_obj list * r_rel list * r_sort list) -type only_restrictions = - (r_obj list option * r_rel list option * r_sort list option) -type universe = position list option +let locate s = + let query = + M.Property true M.RefineExact ["objectName"] [] [] [] [] + false (M.Const s) + in M.StatQuery query + +let compose cl = + let letin = ref [] in + let must = ref [] in + let onlyobj = ref [] in + let onlysort = ref [] in + let onlyrel = ref [] in + let only = ref true in + let univ = ref [] in + let set_val = function + | [s] -> M.Const s + | l -> + let msval = M.Set (List.map (fun s -> M.Const s) l) in + if ! only then begin + let vvar = "val" ^ string_of_int (List.length ! letin) in + letin := (vvar, msval) :: ! letin; + M.VVar vvar + end else msval + in + let cons o (r, s, p, d) = + let con p = function + | [] -> [] + | l -> [(false, [p], set_val l)] + in + only := o; + con "h:occurrence" r @ con "h:sort" s @ + con "h:position" p @ con "h:depth" d + in + let property_must n c = + M.Property true M.RefineExact [n] [] + (cons false c) [] [] false (M.Const "") + in + let property_only n cl = + let cll = List.map (cons true) cl in + M.Property false M.RefineExact [n] [] + ! univ cll [] false (M.Proj None (M.AVar "obj")) + in + let rec aux = function + | [] -> () + | Universe l :: tail -> + only := true; univ := [(false, ["h:position"], set_val l)]; aux tail + | MustObj r p d :: tail -> + must := property_must "refObj" (r, [], p, d) :: ! must; aux tail + | MustSort s p d :: tail -> + must := property_must "refSort" ([], s, p, d) :: ! must; aux tail + | MustRel p d :: tail -> + must := property_must "refRel" ([], [], p, d) :: ! must; aux tail + | OnlyObj r p d :: tail -> + onlyobj := (r, [], p, d) :: ! onlyobj; aux tail + | OnlySort s p d :: tail -> + onlysort := ([], s, p, d) :: ! onlysort; aux tail + | OnlyRel p d :: tail -> + onlyrel := ([], [], p, d) :: ! onlyrel; aux tail + in + let rec iter f g = function + | [] -> raise (Failure "MQueryGenerator.iter") + | [head] -> (f head) + | head :: tail -> let t = (iter f g tail) in g (f head) t + in + text_of_spec prerr_string cl; + aux cl; + let must_query = + if ! must = [] then + M.Property false M.RefineExact [] [] [] [] [] true (M.Const ".*") + else + iter (fun x -> x) (fun x y -> M.Bin M.BinFMeet x y) ! must + in + let onlyobj_val = M.Not (M.Proj None (property_only "refObj" ! onlyobj)) in + let onlysort_val = M.Not (M.Proj None (property_only "refSort" ! onlysort)) in + let onlyrel_val = M.Not (M.Proj None (property_only "refRel" ! onlyrel)) in + let select_query x = + match ! onlyobj, ! onlysort, ! onlyrel with + | [], [], [] -> x + | _, [], [] -> M.Select "obj" x onlyobj_val + | [], _, [] -> M.Select "obj" x onlysort_val + | [], [], _ -> M.Select "obj" x onlyrel_val + | _, _, [] -> M.Select "obj" x (M.Test M.And onlyobj_val onlysort_val) + | _, [], _ -> M.Select "obj" x (M.Test M.And onlyobj_val onlyrel_val) + | [], _, _ -> M.Select "obj" x (M.Test M.And onlysort_val onlyrel_val) + | _, _, _ -> M.Select "obj" x (M.Test M.And (M.Test M.And onlyobj_val onlysort_val) onlyrel_val) + in + let letin_query = + if ! letin = [] then fun x -> x + else + let f (vvar, msval) x = M.LetVVar vvar msval x in + iter f (fun x y z -> x (y z)) ! letin + in + M.StatQuery (letin_query (select_query must_query)) let builtin s = - let ns = "h:" in + let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in match s with | "MH" -> ns ^ "MainHypothesis" | "IH" -> ns ^ "InHypothesis" @@ -52,454 +174,52 @@ let builtin s = | "TYPE" -> ns ^ "Type" | _ -> raise (Failure "MQueryGenerator.builtin") -(* Query building functions ************************************************) - -module M = MathQL - -let locate s = - M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s])) - -let query_of_constraints univ must_use can_use = -(* FG : The (univ : universe) is not used in this implementation *) - let in_path s = (s, []) in - let assign v p = (in_path v, in_path p) in - -(* can restrictions *) - - let (cr_o,cr_r,cr_s) = can_use in - - let uri_of_entry (r, p, d) = r in - - let universe = - match cr_o with - None -> [] - | Some cr_o -> List.map uri_of_entry cr_o - in - - let tfst (a,b,c) = a in - let tsnd (a,b,c) = b in - let trd (a,b,c) = c in - - let to_int_list l d = - match d with - None -> l - | Some d -> l@[d] - in - - let opos = - match cr_o with - None -> [] - | Some cr_o -> (List.map tsnd cr_o) in - - let odep = - match cr_o with - None -> [] - | Some cr_o -> List.map trd cr_o - (* let odep_option_list = List.map trd cr_o in - let lo_dep_int = List.fold_left to_int_list [] odep_option_list in - List.map string_of_int lo_dep_int*) - in - print_string "#### LUNGHEZZA ODEP: "; print_int (List.length odep); flush stdout; - print_endline""; - let rpos = - match cr_r with - None -> [] - | Some cr_r -> (List.map fst cr_r) in - - let rdep = - match cr_r with - None -> [] - | Some cr_r -> List.map snd cr_r - (* let rdep_option_list = List.map snd cr_r in - let lr_dep_int = List.fold_left to_int_list [] rdep_option_list in - List.map string_of_int lr_dep_int *) - in - - - let spos = - match cr_s with - None -> [] - | Some cr_s -> (List.map tfst cr_s) in - - - let sdep = - match cr_s with - None -> [] - | Some cr_s -> List.map tsnd cr_s - (* let sdep_option_list = List.map tsnd cr_s in - let ls_dep_int = List.fold_left to_int_list [] sdep_option_list in - List.map string_of_int ls_dep_int*) - in - - - let sor = - match cr_s with - None -> [] - | Some cr_s -> List.map trd cr_s in - - (* let q_where_obj = function - Some l -> - if odep = [] then - M.Sub - (M.RefOf - (M.Select - ("uri", - M.Relation (false, M.RefineExact, in_path "refObj", M.Ref (M.RefOf (M.RVar "uri0")), [assign "pos" "position"]), - M.Ex ["uri"] - (M.Meet (M.VVar "obj_positions", M.Record ("uri", in_path "pos"))))), - M.VVar "universe") - else - M.Sub - (M.RefOf - (M.Select - ("uri", - M.Relation - (false, M.RefineExact, in_path "refObj", - M.Ref (M.RefOf (M.RVar "uri0")), - [assign "p" "position"; assign "d" "depth"] - ), - M.Ex ["uri"] - (M.And - ((M.Meet(M.VVar "obj_positions",M.Record("uri",in_path "p"))), - (M.Meet(M.VVar "obj_depths", M.Record("uri",in_path "d"))))) - ) - ), - M.VVar "universe" - ) - - | None -> M.True - in*) - - - - let q_where_obj n = function - Some l -> - let rec q_ex n = function - [] -> M.True - | [(u,p,None)] -> - M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p")) - - | [(u,p,d)] -> - print_string "@@@@@ IN-WHERE-OBJ"; flush stdout; - print_endline""; - M.And - (M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p")), - M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d"))) - | (u,p,None)::tl -> - M.Or - (M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p")), - q_ex (n+1) tl) - | (u,p,d)::tl -> - print_string "@@@@@ IN-WHERE-OBJ"; flush stdout; - print_endline""; - M.Or - ((M.And - ((M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p"))), - (M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d"))))), - q_ex (n+1) tl) - in - M.Sub - (M.RefOf - (M.Select - ("uri", - M.Relation - (false, M.RefineExact, in_path "refObj", - M.Ref (M.RefOf (M.RVar "uri0")), - [assign "p" "position"; assign "d" "depth"] - ), - M.Ex ["uri"] - (q_ex 1 l))), - M.VVar "universe") - | None -> M.True - in +(* conversion functions from the old constraints ***************************) +type old_depth = int option + +type r_obj = uri * position * old_depth +type r_rel = position * old_depth +type r_sort = position * old_depth * sort +type universe = position list option - - let rec q_where_rel n cr_r= (*function*) - (* Some l ->*) - let q0 = - M.Sub - (M.Property - (false, M.RefineExact, ("refRel", ["position"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("rel_position" ^ string_of_int n)) - in - match cr_r with - Some [] -> M.True - | Some [(p,None)] -> q0 - | Some [(p,d)] -> - M.And - (q0, - M.Sub - (M.Property - (false, M.RefineExact, ("refRel", ["depth"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("rel_depth" ^ string_of_int n))) - | Some ((p,None)::tl) -> - M.Or - (q0, - q_where_rel (n+1) (Some tl)) - | Some ((p,d)::tl) -> - M.Or - (M.And - (q0, - M.Sub - (M.Property - (false, M.RefineExact, ("refRel", ["depth"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("rel_depth" ^ string_of_int n))), - q_where_rel (n+1) (Some tl)) - | None -> M.True - in - - let rec q_where_sort n cr_s = (*function *) - (* Some l ->*) - let q0 = - M.And - (M.Sub - (M.Property - (false, M.RefineExact, ("refSort", ["position"]), - M.RefOf(M.RVar "uri0") - ), - M.VVar ("sort_position" ^ string_of_int n)), - M.Sub - (M.Property - (false, M.RefineExact, ("refSort", ["sort"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("sort" ^ string_of_int n))) - in - match cr_s with - Some [] -> M.True - | Some [(p,None,s)] -> q0 - - | Some [(p,d,s)] -> - M.And - (q0, - M.Sub - (M.Property - (false, M.RefineExact, ("refSort", ["depth"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("sort_depth" ^ string_of_int n))) - - | Some ((p,None,s)::tl) -> - M.Or - (q0, - q_where_sort (n+1) (Some tl)) - - | Some((p,d,s)::tl) -> - M.Or - (M.And - (q0, - M.Sub - (M.Property - (false, M.RefineExact, ("refSort", ["depth"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("sort_depth" ^ string_of_int n))), - q_where_sort (n+1) (Some tl)) - | None -> M.True - in - - - - - let q_where cr = - let (cr_o,cr_r,cr_s) = cr in - M.And(M.And(q_where_obj 1 cr_o, (q_where_rel 1 cr_r)), (q_where_sort 1 cr_s)) - - in - -(* must restrictions *) - - let build_select_obj (r, pos, dep) = - match dep with - None -> M.Select - ("uri", - M.Relation (false, M.RefineExact, ("backPointer", []), - M.Ref (M.Const [r]), [assign "p" "position"]), - M.Ex ["uri"] - ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))))) - | Some dep -> let string_dep = string_of_int dep in - M.Select - ("uri", - M.Relation (false, M.RefineExact, ("backPointer", []), - M.Ref (M.Const [r]), [assign "p" "position";assign "d" "depth"]), - M.Ex ["uri"] - (M.And - ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), - (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d")))))) - in - - let build_select_rel (pos, dep) = - match dep with - None -> M.Select - ("uri", - M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]), - M.Ex ["uri"] - (M.Sub (M.Const [pos], M.Record ("uri", in_path "p")))) - | Some dep -> let string_dep = string_of_int dep in - M.Select - ("uri", - M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]), - M.Ex ["uri"] - (M.And - ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), - (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d")))))) - in - - let build_select_sort (pos, dep, sor) = - match dep with - None -> M.Select - ("uri", - M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]), - M.Ex ["uri"] - (M.And - ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), - (M.Sub (M.Const [sor], M.Record ("uri", in_path "s")))))) - - | Some dep -> let string_dep = string_of_int dep in - M.Select - ("uri", - M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]), - M.Ex ["uri"] - (M.And - ((M.And - ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), - (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))), - (M.Sub (M.Const [sor], M.Record ("uri", in_path "s")))))) - in - - let rec build_intersect_obj = function - [] -> M.Pattern (M.Const ["[.]*"]) - | [hd] -> build_select_obj hd - | hd :: tl -> M.Intersect (build_select_obj hd, build_intersect_obj tl) - in - - let rec build_intersect_rel = function - [] -> M.Ref(M.Const []) - | [hd] -> build_select_rel hd - | hd :: tl -> M.Intersect (build_select_rel hd, build_intersect_rel tl) - in - - let rec build_intersect_sort = function - [] -> M.Ref(M.Const []) - | [hd] -> build_select_sort hd - | hd :: tl -> M.Intersect (build_select_sort hd, build_intersect_sort tl) - in - - let build_intersect = function -(* let tostring_sort (a,b,c) = - let b1 = string_of_int b in - (a,b1,c) - in - let tostring_rel (a,b) = - let b1 = string_of_int b in - (a,b1) - in*) - -(* let (l1,l2,l3) = must in - match (l1,l2,l3) with *) - l1,[],[] -> build_intersect_obj l1 - | [],l2,[] -> (*let lrel = List.map tostring_rel l2 in*) - build_intersect_rel l2 - | [],[],l3 ->(* let lsort = List.map tostring_sort l3 in*) - build_intersect_sort l3 - | l1,l2,[] -> (*let lrel = List.map tostring_rel l2 in*) - M.Intersect (build_intersect_obj l1, build_intersect_rel l2) - | l1,[],l3 ->(* let lsort = List.map tostring_sort l3 in *) - M.Intersect (build_intersect_obj l1, build_intersect_sort l3) - | [],l2,l3 ->(* let lrel = List.map tostring_rel l2 in - let lsort = List.map tostring_sort l3 in*) - M.Intersect (build_intersect_rel l2, build_intersect_sort l3) - | l1,l2,l3 ->(* let lrel = List.map tostring_rel l2 in - let lsort = List.map tostring_sort l3 in *) - M.Intersect (M.Intersect (build_intersect_obj l1, build_intersect_rel l2), build_intersect_sort l3) - in - - let q_in = build_intersect must_use in - let q_select = M.Select ("uri0", q_in, q_where can_use) in - -(* variables for can restrictions *) - - let q_let_u = M.LetVVar ("universe", M.Const universe, q_select) in - - let rec q_let_s sor n = - match sor with - [] -> q_let_u - | [s] -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_u) - | s::tl -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_s tl (n+1)) - in - -(* let q_let_s = M.LetVVar ("sorts", M.Const sor, q_let_u) in *) - - let rec q_let_ds sdep n = - match sdep with - [] - | [None] -> q_let_s sor 1 - | (None)::tl -> q_let_ds tl (n+1) - | [Some d] -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_s sor 1) - | (Some d)::tl -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds tl (n+1)) - in - -(* let q_let_ds = M.LetVVar ("sort_depths", M.Const sdep, q_let_s) in *) - - let rec q_let_dr rdep n = - match rdep with - [] - | [None] -> q_let_ds sdep 1 - | (None)::tl -> q_let_dr tl (n+1) - | [Some d] -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds sdep 1) - | (Some d)::tl -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr tl (n+1)) - in - - - (*let q_let_dr = M.LetVVar ("rel_depths", M.Const rdep, q_let_ds) in*) - - let rec q_let_do odep n = - match odep with - [] - | [None] -> q_let_dr rdep 1 - | (None)::tl -> q_let_do tl (n+1) - | [Some d] -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr rdep 1) - | (Some d)::tl -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_do tl (n+1)) - in - +type must_restrictions = r_obj list * r_rel list * r_sort list +type only_restrictions = + r_obj list option * r_rel list option * r_sort list option -(* let q_let_do = M.LetVVar ("obj_depths", M.Const odep, q_let_dr) in *) - - - let rec q_let_ps spos n = - match spos with - [] -> q_let_do odep 1 - | [p] -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_do odep 1) - | p::tl -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_ps tl (n+1)) +let query_of_constraints u (musts_obj, musts_rel, musts_sort) + (onlys_obj, onlys_rel, onlys_sort) = + let conv = function + | None -> [] + | Some i -> [string_of_int i] in - - -(* let q_let_ps = M.LetVVar ("sort_positions", M.Const spos, q_let_do) in *) - - - let rec q_let_pr rpos n = - match rpos with - [] -> q_let_ps spos 1 - | [p] -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_ps spos 1) - | p::tl -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_pr tl (n+1)) + let must_obj (r, p, d) = MustObj ([r], [p], conv d) in + let must_sort (p, d, s) = MustSort ([s], [p], conv d) in + let must_rel (p, d) = MustRel ([p], conv d) in + let only_obj (r, p, d) = OnlyObj ([r], [p], conv d) in + let only_sort (p, d, s) = OnlySort ([s], [p], conv d) in + let only_rel (p, d) = OnlyRel ([p], conv d) in + let must = List.map must_obj musts_obj @ + List.map must_rel musts_rel @ + List.map must_sort musts_sort in - - - -(* let q_let_pr = M.LetVVar ("rel_positions", M.Const rpos, q_let_ps) in *) - - let rec q_let_po opos n = - match opos with - [] -> q_let_pr rpos 1 - | [p] -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_pr rpos 1) - | p::tl -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_po tl (n+1)) + let only = + (match onlys_obj with + | None -> [] + | Some [] -> [OnlyObj ([], [], [])] + | Some l -> List.map only_obj l + ) @ + (match onlys_rel with + | None -> [] + | Some [] -> [OnlyRel ([], [])] + | Some l -> List.map only_rel l + ) @ + (match onlys_sort with + | None -> [] + | Some [] -> [OnlySort ([], [], [])] + | Some l -> List.map only_sort l + ) in - - (*let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in*) - - let query = (M.Ref (M.RefOf (q_let_po opos 1))) in - -print_endline "### "; MQueryUtil.text_of_query print_string query "\n"; flush stdout; - query + let univ = match u with None -> [] | Some l -> [Universe l] in + compose (must @ only @ univ) diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.mli b/helm/ocaml/mathql_generator/mQueryGenerator.mli index eace22532..c94dbcdb8 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.mli +++ b/helm/ocaml/mathql_generator/mQueryGenerator.mli @@ -25,20 +25,34 @@ type uri = string type position = string -type depth = int option +type depth = string type sort = string -type r_obj = (uri * position * depth) -type r_rel = (position * depth) -type r_sort = (position * depth * sort) +type spec = MustObj of uri list * position list * depth list + | MustSort of sort list * position list * depth list + | MustRel of position list * depth list + | OnlyObj of uri list * position list * depth list + | OnlySort of sort list * position list * depth list + | OnlyRel of position list * depth list + | Universe of position list + +val locate : string -> MathQL.query + +val compose : spec list -> MathQL.query + +val builtin : MathQL.vvar -> string + +(* interface for the old constraints ***************************************) + +type old_depth = int option + +type r_obj = uri * position * old_depth +type r_rel = position * old_depth +type r_sort = position * old_depth * sort type must_restrictions = (r_obj list * r_rel list * r_sort list) type only_restrictions = (r_obj list option * r_rel list option * r_sort list option) type universe = position list option -val locate : string -> MathQL.query - val query_of_constraints : universe -> must_restrictions -> only_restrictions -> MathQL.query - -val builtin : MathQL.vvar -> string diff --git a/helm/ocaml/mathql_interpreter/.depend b/helm/ocaml/mathql_interpreter/.depend index 313e8f055..927d5dcd0 100644 --- a/helm/ocaml/mathql_interpreter/.depend +++ b/helm/ocaml/mathql_interpreter/.depend @@ -1,36 +1,16 @@ -utility.cmi: mQIConn.cmi -relation.cmi: mQIConn.cmi -func.cmi: mQIConn.cmi -property.cmi: mQIConn.cmi -pattern.cmi: mQIConn.cmi +mQIProperty.cmi: mQIConn.cmi mQueryInterpreter.cmi: mQIConn.cmi -dbconn.cmo: dbconn.cmi -dbconn.cmx: dbconn.cmi -mQIConn.cmo: dbconn.cmi mQIConn.cmi -mQIConn.cmx: dbconn.cmx mQIConn.cmi -utility.cmo: dbconn.cmi mQIConn.cmi utility.cmi -utility.cmx: dbconn.cmx mQIConn.cmx utility.cmi -union.cmo: union.cmi -union.cmx: union.cmi -relation.cmo: dbconn.cmi mQIConn.cmi union.cmi utility.cmi relation.cmi -relation.cmx: dbconn.cmx mQIConn.cmx union.cmx utility.cmx relation.cmi -diff.cmo: diff.cmi -diff.cmx: diff.cmi -meet.cmo: meet.cmi -meet.cmx: meet.cmi -sub.cmo: sub.cmi -sub.cmx: sub.cmi -intersect.cmo: intersect.cmi -intersect.cmx: intersect.cmi -func.cmo: intersect.cmi mQIConn.cmi utility.cmi func.cmi -func.cmx: intersect.cmx mQIConn.cmx utility.cmx func.cmi -property.cmo: dbconn.cmi intersect.cmi mQIConn.cmi utility.cmi property.cmi -property.cmx: dbconn.cmx intersect.cmx mQIConn.cmx utility.cmx property.cmi -pattern.cmo: mQIConn.cmi utility.cmi pattern.cmi -pattern.cmx: mQIConn.cmx utility.cmx pattern.cmi -mQueryInterpreter.cmo: context.cmo dbconn.cmi diff.cmi func.cmi intersect.cmi \ - mQIConn.cmi meet.cmi pattern.cmi property.cmi relation.cmi sub.cmi \ - union.cmi mQueryInterpreter.cmi -mQueryInterpreter.cmx: context.cmx dbconn.cmx diff.cmx func.cmx intersect.cmx \ - mQIConn.cmx meet.cmx pattern.cmx property.cmx relation.cmx sub.cmx \ - union.cmx mQueryInterpreter.cmi +mQueryMisc.cmo: mQueryMisc.cmi +mQueryMisc.cmx: mQueryMisc.cmi +mQIPostgres.cmo: mQIPostgres.cmi +mQIPostgres.cmx: mQIPostgres.cmi +mQIConn.cmo: mQIPostgres.cmi mQIConn.cmi +mQIConn.cmx: mQIPostgres.cmx mQIConn.cmi +mQIUtil.cmo: mQIUtil.cmi +mQIUtil.cmx: mQIUtil.cmi +mQIProperty.cmo: mQIConn.cmi mQIPostgres.cmi mQIUtil.cmi mQIProperty.cmi +mQIProperty.cmx: mQIConn.cmx mQIPostgres.cmx mQIUtil.cmx mQIProperty.cmi +mQueryInterpreter.cmo: mQIConn.cmi mQIProperty.cmi mQIUtil.cmi \ + mQueryInterpreter.cmi +mQueryInterpreter.cmx: mQIConn.cmx mQIProperty.cmx mQIUtil.cmx \ + mQueryInterpreter.cmi diff --git a/helm/ocaml/mathql_interpreter/Makefile b/helm/ocaml/mathql_interpreter/Makefile index 7b6ffd28a..929f149e1 100644 --- a/helm/ocaml/mathql_interpreter/Makefile +++ b/helm/ocaml/mathql_interpreter/Makefile @@ -1,14 +1,16 @@ PACKAGE = mathql_interpreter -REQUIRES = helm-urimanager postgres natile-galax helm-mathql -PREDICATES = +REQUIRES = helm-cic helm-cic_textual_parser \ + postgres natile-galax helm-mathql -INTERFACE_FILES = dbconn.mli mQIConn.mli utility.mli union.mli relation.mli diff.mli meet.mli sub.mli intersect.mli func.mli property.mli pattern.mli mQueryInterpreter.mli +PREDICATES = -IMPLEMENTATION_FILES = dbconn.ml mQIConn.ml utility.ml union.ml relation.ml diff.ml meet.ml sub.ml intersect.ml context.ml func.ml property.ml pattern.ml mQueryInterpreter.ml +INTERFACE_FILES = mQueryMisc.mli mQIPostgres.mli mQIConn.mli \ + mQIUtil.mli mQIProperty.mli \ + mQueryInterpreter.mli -# $(INTERFACE_FILES:%.mli=%.ml) +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = context.ml +EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = diff --git a/helm/ocaml/mathql_interpreter/context.ml b/helm/ocaml/mathql_interpreter/context.ml deleted file mode 100644 index 377670d18..000000000 --- a/helm/ocaml/mathql_interpreter/context.ml +++ /dev/null @@ -1,24 +0,0 @@ -(* contexts *****************************************************************) - -type svar_context = (MathQL.svar * MathQL.resource_set) list - -type rvar_context = (MathQL.rvar * MathQL.resource) list - -type group_context = (MathQL.rvar * MathQL.attribute_group) list - -type vvar_context = (MathQL.vvar * MathQL.value) list - - -type context = {svars: svar_context; (* contesto delle svar *) - rvars: rvar_context; (* contesto delle rvar *) - groups: group_context; (* contesto dei gruppi *) - vvars: vvar_context (* contesto delle vvar introdotte con let-in *) - } - -let upd_svars c s = {c with svars = s} - -let upd_rvars c s = {c with rvars = s} - -let upd_groups c s = {c with groups = s} - -let upd_vvars c s = {c with vvars = s} diff --git a/helm/ocaml/mathql_interpreter/dbconn.ml b/helm/ocaml/mathql_interpreter/dbconn.ml deleted file mode 100644 index 95dc15cc3..000000000 --- a/helm/ocaml/mathql_interpreter/dbconn.ml +++ /dev/null @@ -1,33 +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://www.cs.unibo.it/helm/. - *) - -let init connection_param = - try Some (new Postgres.connection connection_param) - with _ -> None - -let close = function - | None -> () - | Some c -> c#close - diff --git a/helm/ocaml/mathql_interpreter/dbconn.mli b/helm/ocaml/mathql_interpreter/dbconn.mli deleted file mode 100644 index 5c9ef79cb..000000000 --- a/helm/ocaml/mathql_interpreter/dbconn.mli +++ /dev/null @@ -1,27 +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/. - *) - -val init : string -> Postgres.connection option -val close : Postgres.connection option -> unit diff --git a/helm/ocaml/mathql_interpreter/diff.ml b/helm/ocaml/mathql_interpreter/diff.ml deleted file mode 100644 index d52252691..000000000 --- a/helm/ocaml/mathql_interpreter/diff.ml +++ /dev/null @@ -1,98 +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/. - *) - -(* - * vecchia implementazione del comando DIFF - - -exception NotCompatible;; - -(* intersect_attributes is successful iff there is no attribute with *) -(* two different values in the two lists. The returned list is the *) -(* union of the two lists. *) -let rec intersect_attributes (attr1, attr2) = - match attr1, attr2 with - [],_ -> attr2 - | _,[] -> attr1 - | (key1,value1)::tl1, (key2,_)::_ when key1 < key2 -> - (key1,value1)::(intersect_attributes (tl1,attr2)) - | (key1,_)::_, (key2,value2)::tl2 when key2 < key1 -> - (key2,value2)::(intersect_attributes (attr1,tl2)) - | entry1::tl1, entry2::tl2 when entry1 = entry2 -> - entry1::(intersect_attributes (tl1,tl2)) - | _, _ -> raise NotCompatible (* same keys, different values *) -;; - - -let rec diff_ex l1 l2 = - let module S = Mathql_semantics in - match (l1, l2) with - [],_ -> [] - | l,[] -> l - | {S.uri = uri1}::_, {S.uri = uri2}::tl2 when uri2 < uri1 -> - (diff_ex l1 tl2) - | {S.uri = uri1 ; S.attributes = attributes1}::tl1, - {S.uri = uri2}::_ when uri1 < uri2 -> - {S.uri = uri1 ; S.attributes = attributes1 ; S.extra = ""}::(diff_ex tl1 l2) - | {S.uri = uri1 ; S.attributes = attributes1}::tl1, - {S.uri = uri2 ; S.attributes = attributes2}::tl2 -> - try - let attributes' = intersect_attributes (attributes1, attributes2) in - diff_ex tl1 tl2 - with - NotCompatible -> - {S.uri = uri1 ; S.attributes = attributes1 ; S.extra = ""}::(diff_ex tl1 tl2) -;; -*) - -(* - * implementazione del comando DIFF - *) -let rec diff_ex rs1 rs2 = - match (rs1, rs2) with - [],_ -> [] - | l,[] -> l - | (uri1,l)::tl1,(uri2,_)::_ when uri1 < uri2 -> (uri1,l)::(diff_ex tl1 rs2) - | (uri1,_)::_,(uri2,_)::tl2 when uri2 < uri1 -> (diff_ex rs1 tl2) - | (uri1,_)::tl1, (uri2,_)::tl2 -> (diff_ex tl1 tl2) -;; - - - -(* -let diff_ex l1 l2 = - let before = Sys.time () in - let res = diff_ex l1 l2 in - let after = Sys.time () in - let ll1 = string_of_int (List.length l1) in - let ll2 = string_of_int (List.length l2) in - let diff = string_of_float (after -. before) in - prerr_endline - ("DIFF(" ^ ll1 ^ ", " ^ ll2 ^ ") = " ^ string_of_int (List.length res) ^ - ": " ^ diff ^ "s") ; - flush stdout ; - res -;; -*) diff --git a/helm/ocaml/mathql_interpreter/diff.mli b/helm/ocaml/mathql_interpreter/diff.mli deleted file mode 100644 index 1cd9cf4de..000000000 --- a/helm/ocaml/mathql_interpreter/diff.mli +++ /dev/null @@ -1,27 +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/. - *) - -val diff_ex : - MathQL.resource_set -> MathQL.resource_set -> MathQL.resource_set diff --git a/helm/ocaml/mathql_interpreter/func.ml b/helm/ocaml/mathql_interpreter/func.ml deleted file mode 100644 index 7e1f22367..000000000 --- a/helm/ocaml/mathql_interpreter/func.ml +++ /dev/null @@ -1,45 +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/. - *) - -(* - * - *) - -open Utility;; -open Intersect;; - -(* - * implementazione delle funzioni dublin core - *) -let rec fun_ex handle tab = function - [] -> [] - | s::tl -> let res = - let c = MQIConn.pgc handle in - let q = ("select " ^ tab ^ ".uri from " ^ tab ^ " where " ^ tab ^ ".value = '" ^ s ^ "'") in - pgresult_to_string_list (c#exec q) - in - append (res,(fun_ex handle tab tl)) -;; - diff --git a/helm/ocaml/mathql_interpreter/func.mli b/helm/ocaml/mathql_interpreter/func.mli deleted file mode 100644 index cdf3f1f00..000000000 --- a/helm/ocaml/mathql_interpreter/func.mli +++ /dev/null @@ -1,26 +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/. - *) - -val fun_ex: MQIConn.handle -> string -> MathQL.value -> MathQL.value diff --git a/helm/ocaml/mathql_interpreter/intersect.ml b/helm/ocaml/mathql_interpreter/intersect.ml deleted file mode 100644 index 73bebaa50..000000000 --- a/helm/ocaml/mathql_interpreter/intersect.ml +++ /dev/null @@ -1,75 +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/. - *) - - -(* Catenates two lists preserving order and getting rid of duplicates *) -let rec append (l1,l2) = - match l1,l2 with - [],_ -> l2 - | _,[] -> l1 - | s1::tl1, s2::_ when s1 < s2 -> s1::append (tl1,l2) - | s1::_, s2::tl2 when s2 < s1 -> s2::append (l1,tl2) - | s1::tl1, s2::tl2 -> s1::append (tl1,tl2) - -;; - - -(* Sums two attribute groups preserving order *) -let rec sum_groups(gr1, gr2) = - match gr1, gr2 with - [],_ -> gr2 - | _,[] -> gr1 - | gr1, gr2 when gr1 = gr2 -> gr1 - | (key1,l1)::tl1, (key2,l2)::_ when key1 < key2 -> (key1,l1)::(sum_groups (tl1,gr2)) - | (key1,l1)::_, (key2,l2)::tl2 when key2 < key1 -> (key2,l2)::(sum_groups (gr1,tl2)) - | (key1,l1)::tl1, (key2,l2)::tl2 -> (key1,(append (l1,l2)))::(sum_groups (tl1,tl2)) - -;; - -(* Product between an attribute set and a group of attributes *) -let rec sub_prod (aset, gr) = (*prende un aset e un gr, fa la somma tra tutti i gruppi di aset e gr*) - match aset with - [] -> [] - | gr1::tl1 -> sum_groups (gr1, gr)::(sub_prod(tl1, gr)) -;; - - -(* Cartesian product between two attribute sets*) -let rec prod (as1, as2) = - match as1, as2 with - [],_ -> [] - | _,[] -> [] - | gr1::tl1, _ -> append((sub_prod (as2, gr1)), (prod (tl1, as2))) (* chiamo la sub_prod con un el. as1 e as2 *) -;; - -(* Intersection between two resource sets, preserves order and gets rid of duplicates *) -let rec intersect_ex rs1 rs2 = - match (rs1, rs2) with - [],_ - | _,[] -> [] - | (uri1,_)::tl1, (uri2,_)::_ when uri1 < uri2 -> intersect_ex tl1 rs2 - | (uri1,_)::_, (uri2,_)::tl2 when uri2 < uri1 -> intersect_ex rs1 tl2 - | (uri1,as1)::tl1, (uri2,as2)::tl2 -> (uri1, prod(as1,as2))::intersect_ex tl1 tl2 -;; diff --git a/helm/ocaml/mathql_interpreter/intersect.mli b/helm/ocaml/mathql_interpreter/intersect.mli deleted file mode 100644 index 5045162b6..000000000 --- a/helm/ocaml/mathql_interpreter/intersect.mli +++ /dev/null @@ -1,30 +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/. - *) - -val intersect_ex : - MathQL.result -> MathQL.result -> MathQL.result - -val append: - (string list * string list) -> string list diff --git a/helm/ocaml/mathql_interpreter/mQIConn.ml b/helm/ocaml/mathql_interpreter/mQIConn.ml index f38964f06..1de6663e4 100644 --- a/helm/ocaml/mathql_interpreter/mQIConn.ml +++ b/helm/ocaml/mathql_interpreter/mQIConn.ml @@ -23,9 +23,7 @@ * http://cs.unibo.it/helm/. *) -exception InvalidConnection - -type flag = Postgres | Galax | Stat | Quiet | Warn +type flag = Postgres | Galax | Stat | Quiet | Warn | Log type handle = {log : string -> unit; (* logging function *) set : flag list; (* options *) @@ -36,10 +34,9 @@ let log handle = handle.log let set handle flag = List.mem flag handle.set -let pgc handle = - match handle.pgc with - | None -> raise InvalidConnection - | Some c -> c +let pgc handle = handle.pgc + +let flags handle = handle.set let string_of_flag = function | Postgres -> "P" @@ -47,6 +44,7 @@ let string_of_flag = function | Stat -> "S" | Quiet -> "Q" | Warn -> "W" + | Log -> "L" let flag_of_char = function | 'P' -> [Postgres] @@ -54,6 +52,7 @@ let flag_of_char = function | 'S' -> [Stat] | 'Q' -> [Quiet] | 'W' -> [Warn] + | 'L' -> [Log] | _ -> [] let string_fold_left f a s = @@ -68,24 +67,16 @@ let flags_of_string s = string_fold_left (fun l c -> l @ flag_of_char c) [] s let init myflags mylog = - let default_connection_string = - "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" - in - let connection_string = - try Sys.getenv "POSTGRESQL_CONNECTION_STRING" - with Not_found -> default_connection_string - in {log = mylog; set = myflags; pgc = if List.mem Galax myflags - then None else Dbconn.init connection_string + then None else MQIPostgres.init () } let close handle = - if set handle Galax then () else Dbconn.close handle.pgc + if set handle Galax then () else MQIPostgres.close handle.pgc let connected handle = - if set handle Galax then false else - try ignore (pgc handle); true with InvalidConnection -> false + if set handle Galax then false else (pgc handle) <> None let init_if_connected myflags mylog = let handle = init myflags mylog in diff --git a/helm/ocaml/mathql_interpreter/mQIConn.mli b/helm/ocaml/mathql_interpreter/mQIConn.mli index 26cb291f9..7eff1b4b4 100644 --- a/helm/ocaml/mathql_interpreter/mQIConn.mli +++ b/helm/ocaml/mathql_interpreter/mQIConn.mli @@ -23,13 +23,11 @@ * http://cs.unibo.it/helm/. *) -type flag = Postgres | Galax | Stat | Quiet | Warn +type flag = Postgres | Galax | Stat | Quiet | Warn | Log val string_of_flags : flag list -> string val flags_of_string : string -> flag list -exception InvalidConnection - type handle val init : flag list -> (string -> unit) -> handle @@ -42,6 +40,7 @@ val init_if_connected : flag list -> (string -> unit) -> handle * For exclusive use of the interpreter. *) -val log : handle -> string -> unit -val set : handle -> flag -> bool -val pgc : handle -> Postgres.connection +val log : handle -> string -> unit +val set : handle -> flag -> bool +val pgc : handle -> Postgres.connection option +val flags : handle -> flag list diff --git a/helm/ocaml/mathql_interpreter/mQIExecute.ml b/helm/ocaml/mathql_interpreter/mQIExecute.ml deleted file mode 100644 index efb8feb1c..000000000 --- a/helm/ocaml/mathql_interpreter/mQIExecute.ml +++ /dev/null @@ -1,249 +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/. - *) - -(* modifiers ***************************************************************) - -let galax_char = 'G' - -let stat_char = 'S' - -let warn_char = 'W' - -(* 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 U = MQIUtil - -let execute out m x = - let warn q = - if String.contains m warn_char then - begin - out "MQIExecute: waring: reference to undefined variables: "; - P.text_of_query out 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 = U.start_time () in - let r = (eval_val c y) in - let s = U.stop_time t in - out (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 = U.start_time () in - P.text_of_query out x "\n"; - let s = U.stop_time t in - if String.contains m stat_char then - out (Printf.sprintf "Log source: %s\n" s); - eval_query c x - end else begin - let s = (eval_query c x) in - let t = U.start_time () in - P.text_of_result out s "\n"; - let r = U.stop_time t in - if String.contains m stat_char then - out (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 f = if String.contains m galax_char - then MQIProperty.galax else MQIProperty.postgres - 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 = U.start_time () in - let r = f q1 subj cons_true cons_false exp in - let s = U.stop_time t in - if String.contains m stat_char then - out (Printf.sprintf "Property: %s,%i\n" s (List.length r)); - r - | M.StatQuery x -> - let t = U.start_time () in - let r = (eval_query c x) in - let s = U.stop_time t in - out (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 = U.start_time () in - let r = eval_query c x in - let s = U.stop_time t in - if String.contains m stat_char then - out (Printf.sprintf "MQIExecute: %s,%s\n" s m); - r diff --git a/helm/ocaml/mathql_interpreter/mQIExecute.mli b/helm/ocaml/mathql_interpreter/mQIExecute.mli deleted file mode 100644 index 536e489c1..000000000 --- a/helm/ocaml/mathql_interpreter/mQIExecute.mli +++ /dev/null @@ -1,36 +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/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 06/01/2003 *) -(* *) -(* *) -(******************************************************************************) - -val execute : (string -> unit) -> string -> MathQL.query -> MathQL.result diff --git a/helm/ocaml/mathql_interpreter/mQIPostgres.ml b/helm/ocaml/mathql_interpreter/mQIPostgres.ml index fe4e3f6f9..b19a51c83 100644 --- a/helm/ocaml/mathql_interpreter/mQIPostgres.ml +++ b/helm/ocaml/mathql_interpreter/mQIPostgres.ml @@ -24,25 +24,21 @@ *) let default_connection_string = - "dbname=mowgli_test user=helm" - -let connection = ref None + "dbname=mowgli user=helm" let connection_string = try Sys.getenv "POSTGRESQL_CONNECTION_STRING" with Not_found -> default_connection_string let init () = - try connection := Some (new Postgres.connection connection_string); + try Some (new Postgres.connection connection_string) with _ -> raise (Failure ("MQIPostgres.init: " ^ connection_string)) -let close () = match ! connection with +let close = function | None -> () | Some c -> c#close -let check () = ! connection <> None - -let exec q = match ! connection with +let exec c q = match c with | None -> [] | Some c -> (c#exec q)#get_list diff --git a/helm/ocaml/mathql_interpreter/mQIPostgres.mli b/helm/ocaml/mathql_interpreter/mQIPostgres.mli index 8906a4985..d6b9d3f33 100644 --- a/helm/ocaml/mathql_interpreter/mQIPostgres.mli +++ b/helm/ocaml/mathql_interpreter/mQIPostgres.mli @@ -23,23 +23,10 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 06/01/2003 *) -(* *) -(* *) -(******************************************************************************) +val init : unit -> Postgres.connection option +val close : Postgres.connection option -> unit -val init : unit -> unit - -val close : unit -> unit - -val check : unit -> bool - -val exec : string -> string list list +val exec : Postgres.connection option -> string -> string list list val quote : string -> string diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.ml b/helm/ocaml/mathql_interpreter/mQIProperty.ml index 56a9d6421..b07fdd551 100644 --- a/helm/ocaml/mathql_interpreter/mQIProperty.ml +++ b/helm/ocaml/mathql_interpreter/mQIProperty.ml @@ -26,6 +26,7 @@ module M = MathQL module P = MQIPostgres +module C = MQIConn module U = MQIUtil let not_supported s = @@ -51,7 +52,11 @@ let cl_print l = (* PostgreSQL backend ******************************************************) -let pg_query table cols ct cfl = +let pg_query h table cols ct cfl = + let exec q = + if C.set h C.Log then C.log h (q ^ "\n"); + P.exec (C.pgc h) q + in let rec iter f sep = function | [] -> "" | [head] -> f head @@ -77,12 +82,21 @@ let pg_query table cols ct cfl = | [], llf -> " where " ^ pg_cons_not_l llf | lt, llf -> " where " ^ pg_cons lt ^ " and " ^ pg_cons_not_l llf in - if cols = [] then [] else begin - let q = "select " ^ pg_cols ^ " from " ^ table ^ pg_where ^ - " order by " ^ List.hd cols ^ " asc" in - prerr_endline q; - P.exec q end - + if cols = [] then + let r = exec ("select count (source) from " ^ table ^ pg_where) in + match r with + | [[s]] when int_of_string s > 0 -> [[]] + | _ -> [] + else + exec ("select " ^ pg_cols ^ " from " ^ table ^ pg_where ^ + " order by " ^ List.hd cols ^ " asc") + +(* Galax backend ***********************************************************) + +let gx_query h table cols ct cfl = not_supported "Galax" + +(* Common functions ********************************************************) + let pg_result distinct subj el res = let compose = if distinct then List.map else fun f -> U.mql_iter (fun x -> [f x]) in let get_name = function (p, None) -> p | (_, Some p) -> p in @@ -131,38 +145,35 @@ let conv = function | [_; t] -> decolon t | _ -> not_supported "conv" -let postgres_single mc ct cfl el t = +let exec_single h mc ct cfl el t = let table = match t with Some t -> decolon t | None -> "objectName" in let first = conv mc in let mk_con l = List.map (fun (pat, p, v) -> (pat, conv p, v)) l in let cons_true = mk_con ct in let cons_false = List.map mk_con cfl in let other_cols = List.map (fun (p, _) -> conv p) el in - let cols = if first = "" then other_cols else first :: other_cols in - pg_result false first el (pg_query table cols cons_true cons_false) + let cols = if first = "" then other_cols else first :: other_cols in + let low_level = if C.set h C.Galax then gx_query else pg_query in + pg_result false first el (low_level h table cols cons_true cons_false) let deadline = 100 -let postgres refine mc ct cfl el = - if refine <> M.RefineExact then not_supported "postgres"; +let exec h refine mc ct cfl el = + if refine <> M.RefineExact then not_supported "exec"; let table = get_table mc ct cfl el in - let rec postgres_aux ct = match ct with + let rec exec_aux ct = match ct with | (pat, p, v) :: tail when List.length v > deadline -> - let single s = postgres_aux ((pat, p, [s]) :: tail) in + let single s = exec_aux ((pat, p, [s]) :: tail) in U.mql_iter single v | _ -> - postgres_single mc ct cfl el table - in postgres_aux ct - -(* Galax backend ***********************************************************) - -let galax refine mc ct cfl el = not_supported "Galax" + exec_single h mc ct cfl el table + in exec_aux ct (* funzioni vecchie ********************************************************) -let pg_name s = +let pg_name h s = let q = "select id from registry where uri = " ^ P.quote s in - match P.exec q with + match P.exec h q with | [[id]] -> "t" ^ id | _ -> "" diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.mli b/helm/ocaml/mathql_interpreter/mQIProperty.mli index d47fc34c4..7c2bc95f8 100644 --- a/helm/ocaml/mathql_interpreter/mQIProperty.mli +++ b/helm/ocaml/mathql_interpreter/mQIProperty.mli @@ -24,11 +24,8 @@ *) open MathQL +open MQIConn -val postgres: refine -> path -> - (bool * path * value) list -> (bool * path * value) list list -> - exp_list -> result - -val galax: refine -> path -> - (bool * path * value) list -> (bool * path * value) list list -> - exp_list -> result +val exec: handle -> refine -> path -> + (bool * path * value) list -> (bool * path * value) list list -> + exp_list -> result diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.ml b/helm/ocaml/mathql_interpreter/mQIUtil.ml index 537e32d77..4d74ef120 100644 --- a/helm/ocaml/mathql_interpreter/mQIUtil.ml +++ b/helm/ocaml/mathql_interpreter/mQIUtil.ml @@ -151,15 +151,3 @@ let rec set ap = function | [] -> [ap] | head :: tail when fst head = fst ap -> ap :: tail | head :: tail -> head :: set ap tail - -(* time handling ***********************************************************) - -type time = float * float - -let start_time () = - (Sys.time (), Unix.time ()) - -let stop_time (s0, u0) = - let s1 = Sys.time () in - let u1 = Unix.time () in - Printf.sprintf "%.2fs,%.2fs" (s1 -. s0) (u1 -. u0) diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.mli b/helm/ocaml/mathql_interpreter/mQIUtil.mli index 38ca8f380..217ba8c01 100644 --- a/helm/ocaml/mathql_interpreter/mQIUtil.mli +++ b/helm/ocaml/mathql_interpreter/mQIUtil.mli @@ -73,9 +73,3 @@ val lt : MathQL.value -> MathQL.value -> MathQL.value val align : string -> string -> MathQL.value val set : string * 'a -> (string * 'a) list -> (string * 'a) list - -type time - -val start_time : unit -> time - -val stop_time : time -> string diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml index c1422b8ae..5816a99bc 100644 --- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml +++ b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml @@ -23,205 +23,218 @@ * http://cs.unibo.it/helm/. *) -open Dbconn;; -open Union;; -open Intersect;; -open Meet;; -open Property;; -open Sub;; -open Context;; -open Diff;; -open Relation;; -open Func;; -open Pattern;; +(* contexts *****************************************************************) -exception SVarUnbound of string;; -exception RVarUnbound of string;; -exception VVarUnbound of string;; -exception PathUnbound of (string * string list);; +type svar_context = (MathQL.svar * MathQL.resource_set) list -exception BooleExpTrue - -(* valuta una MathQL.set_exp e ritorna un MathQL.resource_set *) +type avar_context = (MathQL.avar * MathQL.resource) list -let galax_char = 'G' -let stat_char = 'S' +type group_context = (MathQL.avar * MathQL.attribute_group) list -let execute_aux handle x = - let module M = MathQL in - let module X = MQueryMisc in -let rec exec_set_exp c = function - M.SVar svar -> - (try - List.assoc svar c.svars - with Not_found -> - raise (SVarUnbound svar)) - | M.RVar rvar -> - (try - [List.assoc rvar c.rvars] - with Not_found -> - raise (RVarUnbound rvar)) - | M.Ref vexp -> List.map (fun s -> (s,[])) (exec_val_exp c vexp) - | M.Pattern vexp -> pattern_ex handle (exec_val_exp c vexp) - | M.Intersect (sexp1, sexp2) -> - let before = X.start_time() in - let rs1 = exec_set_exp c sexp1 in - let rs2 = exec_set_exp c sexp2 in - let res = intersect_ex rs1 rs2 in - let diff = X.stop_time before in - let ll1 = string_of_int (List.length rs1) in - let ll2 = string_of_int (List.length rs2) in - if MQIConn.set handle MQIConn.Stat then - MQIConn.log handle ("INTERSECT(" ^ ll1 ^ "," ^ ll2 ^ ") = " ^ string_of_int (List.length res) ^ - ": " ^ diff ^ "\n"); - res - | M.Union (sexp1, sexp2) -> - let before = X.start_time () in - let res = union_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2) in - let diff = X.stop_time before in - if MQIConn.set handle MQIConn.Stat then MQIConn.log handle ("UNION: " ^ diff ^ "\n"); - res - | M.LetSVar (svar, sexp1, sexp2) -> - let before = X.start_time() in - let c1 = upd_svars c ((svar, exec_set_exp c sexp1) :: c.svars) in - let res = exec_set_exp c1 sexp2 in - if MQIConn.set handle MQIConn.Stat then begin - MQIConn.log handle ("LETIN " ^ svar ^ " = " ^ string_of_int (List.length res) ^ ": "); - MQIConn.log handle (X.stop_time before ^ "\n"); - end; - res - | M.LetVVar (vvar, vexp, sexp) -> - let before = X.start_time() in - let c1 = upd_vvars c ((vvar, exec_val_exp c vexp) :: c.vvars) in - let res = exec_set_exp c1 sexp in - if MQIConn.set handle MQIConn.Stat then begin - MQIConn.log handle ("LETIN " ^ vvar ^ " = " ^ string_of_int (List.length res) ^ ": "); - MQIConn.log handle (X.stop_time before ^ "\n"); - end; - res - | M.Relation (inv, rop, path, sexp, assl) -> - let before = X.start_time() in - if MQIConn.set handle MQIConn.Galax then begin - let res = relation_galax_ex handle inv rop path (exec_set_exp c sexp) assl in - if MQIConn.set handle MQIConn.Stat then begin - MQIConn.log handle ("RELATION-GALAX " ^ (fst path) ^ " = " ^ string_of_int(List.length res) ^ ": "); - MQIConn.log handle (X.stop_time before ^ "\n") - end; - res - end else begin - let res = relation_ex handle inv rop path (exec_set_exp c sexp) assl in - if MQIConn.set handle MQIConn.Stat then begin - MQIConn.log handle ("RELATION " ^ (fst path) ^ " = " ^ string_of_int(List.length res) ^ ": "); - MQIConn.log handle (X.stop_time before ^ "\n") - end; - res - end - | M.Select (rvar, sexp, bexp) -> - let before = X.start_time() in - let rset = (exec_set_exp c sexp) in - let rec select_ex = - function - [] -> [] - | r::tl -> - let c1 = upd_rvars c ((rvar,r)::c.rvars) in - if (exec_boole_exp c1 bexp) then - r::(select_ex tl) - else - select_ex tl - in - let res = select_ex rset in - if MQIConn.set handle MQIConn.Stat then begin - MQIConn.log handle ("SELECT " ^ rvar ^ " = " ^ string_of_int (List.length res) ^ ": "); - MQIConn.log handle (X.stop_time before ^ "\n"); - end; - res - | M.Diff (sexp1, sexp2) -> diff_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2) - -(* valuta una MathQL.boole_exp e ritorna un boole *) +type vvar_context = (MathQL.vvar * MathQL.value) list -and exec_boole_exp c = - function - M.False -> false - | M.True -> true - | M.Not x -> not (exec_boole_exp c x) - | M.And (x, y) -> (exec_boole_exp c x) && (exec_boole_exp c y) - | M.Or (x, y) -> (exec_boole_exp c x) || (exec_boole_exp c y) - | M.Sub (vexp1, vexp2) -> - sub_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2) - | M.Meet (vexp1, vexp2) -> - meet_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2) - | M.Eq (vexp1, vexp2) -> (exec_val_exp c vexp1) = (exec_val_exp c vexp2) - | M.Ex l bexp -> - if l = [] then - (exec_boole_exp c bexp) - else - let latt = - List.map - (fun uri -> - let (r,attl) = - (try - List.assoc uri c.rvars - with Not_found -> assert false) - in - (uri,attl) - ) l (*latt = l + attributi*) - in - try - let rec prod c = - function - [] -> if (exec_boole_exp c bexp) then raise BooleExpTrue - | (uri,attl)::tail1 -> - (*per ogni el. di attl devo andare in ric. su tail1*) - let rec sub_prod attl = - match attl with - [] -> () - | att::tail2 -> - let c1 = upd_groups c ((uri,att)::c.groups) in - prod c1 tail1; sub_prod tail2 - in - sub_prod attl - in - prod c latt; - false - with BooleExpTrue -> true - -(* valuta una MathQL.val_exp e ritorna un MathQL.value *) - -and exec_val_exp c = function - M.Const x -> let - ol = List.sort compare x in - let rec edup = function - - [] -> [] - | s::tl -> if tl <> [] then - if s = (List.hd tl) then edup tl - else s::(edup tl) - else s::[] - in - edup ol - | M.Record (rvar, path) -> - (try - List.assoc path - (try - List.assoc rvar c.groups - with Not_found -> - raise (RVarUnbound rvar)) - with Not_found -> - raise (PathUnbound path)) - | M.VVar s -> - (try - List.assoc s c.vvars - with Not_found -> - raise (VVarUnbound s)) - | M.RefOf sexp -> List.map (fun (s,_) -> s) (exec_set_exp c sexp) - | M.Fun (s, vexp) -> fun_ex handle s (exec_val_exp c vexp) - | M.Property (inv, rop, path, vexp) -> property_ex handle rop path inv (exec_val_exp c vexp) +type context = {svars: svar_context; + avars: avar_context; + groups: group_context; (* auxiliary context *) + vvars: vvar_context + } -(* valuta una MathQL.set_exp nel contesto vuoto e ritorna un MathQL.resource_set *) -in - exec_set_exp {svars = []; rvars = []; groups = []; vvars = []} x +(* execute *****************************************************************) -(* new interface ***********************************************************) +exception Found -let execute handle x = execute_aux handle x +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 diff --git a/helm/ocaml/mathql_interpreter/mQueryMisc.ml b/helm/ocaml/mathql_interpreter/mQueryMisc.ml new file mode 100644 index 000000000..aa842b4b3 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQueryMisc.ml @@ -0,0 +1,101 @@ +(* Copyright (C) 2000-2002, 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/. + *) + +exception IllFormedUri of string;; + +let string_of_cic_textual_parser_uri uri = + let module C = Cic in + let module CTP = CicTextualParser0 in + let uri' = + match uri with + CTP.ConUri uri -> UriManager.string_of_uri uri + | CTP.VarUri uri -> UriManager.string_of_uri uri + | CTP.IndTyUri (uri,tyno) -> + UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) + | CTP.IndConUri (uri,tyno,consno) -> + UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^ + string_of_int consno + in + (* 4 = String.length "cic:" *) + String.sub uri' 4 (String.length uri' - 4) +;; + +let cic_textual_parser_uri_of_string uri' = + prerr_endline ("cic_textual_parser_uri_of_string INPUT = " ^ uri'); + try + (* Constant *) + if String.sub uri' (String.length uri' - 4) 4 = ".con" then + CicTextualParser0.ConUri (UriManager.uri_of_string uri') + else + if String.sub uri' (String.length uri' - 4) 4 = ".var" then + CicTextualParser0.VarUri (UriManager.uri_of_string uri') + else + (try + (* Inductive Type *) + let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in + CicTextualParser0.IndTyUri (uri'',typeno) + with + UriManager.IllFormedUri _ + | CicTextualParser0.LexerFailure _ + | Invalid_argument _ -> + (* Constructor of an Inductive Type *) + let uri'',typeno,consno = + CicTextualLexer.indconuri_of_uri uri' + in + CicTextualParser0.IndConUri (uri'',typeno,consno) + ) + with + UriManager.IllFormedUri _ + | CicTextualParser0.LexerFailure _ + | Invalid_argument _ -> + raise (IllFormedUri uri') +;; +let cic_textual_parser_uri_of_string uri' = + let res = cic_textual_parser_uri_of_string uri' in + prerr_endline ("RESULT: " ^ (string_of_cic_textual_parser_uri res)); + res + +(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *) +let wrong_xpointer_format_from_wrong_xpointer_format' uri = + try + let index_sharp = String.index uri '#' in + let index_rest = index_sharp + 10 in + let baseuri = String.sub uri 0 index_sharp in + let rest = + String.sub uri index_rest (String.length uri - index_rest - 1) + in + baseuri ^ "#" ^ rest + with Not_found -> uri +;; + +let term_of_cic_textual_parser_uri uri = + let module C = Cic in + let module CTP = CicTextualParser0 in + match uri with + CTP.ConUri uri -> C.Const (uri,[]) + | CTP.VarUri uri -> C.Var (uri,[]) + | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[]) + | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) +;; diff --git a/helm/ocaml/mathql_interpreter/mQueryMisc.mli b/helm/ocaml/mathql_interpreter/mQueryMisc.mli new file mode 100644 index 000000000..7c0aa7468 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQueryMisc.mli @@ -0,0 +1,41 @@ +(* Copyright (C) 2000-2002, 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/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 15/01/2003 *) +(* *) +(* *) +(******************************************************************************) + +exception IllFormedUri of string + +val string_of_cic_textual_parser_uri : CicTextualParser0.uri -> string +val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri +val term_of_cic_textual_parser_uri: CicTextualParser0.uri -> Cic.term +val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string diff --git a/helm/ocaml/mathql_interpreter/meet.ml b/helm/ocaml/mathql_interpreter/meet.ml deleted file mode 100644 index bf0b5d780..000000000 --- a/helm/ocaml/mathql_interpreter/meet.ml +++ /dev/null @@ -1,34 +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/. - *) - - -let rec meet_ex v1 v2 = - match v1,v2 with - [],_ - | _,[] -> false - | s1::tl1, s2::_ when s1 < s2 -> meet_ex tl1 v2 - | s1::_, s2::tl2 when s2 < s1 -> meet_ex v1 tl2 - | _, _ -> true -;; diff --git a/helm/ocaml/mathql_interpreter/meet.mli b/helm/ocaml/mathql_interpreter/meet.mli deleted file mode 100644 index 366abd7fd..000000000 --- a/helm/ocaml/mathql_interpreter/meet.mli +++ /dev/null @@ -1,27 +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/. - *) - - -val meet_ex: MathQL.value -> MathQL.value -> bool diff --git a/helm/ocaml/mathql_interpreter/pattern.ml b/helm/ocaml/mathql_interpreter/pattern.ml deleted file mode 100644 index 5dcb8a585..000000000 --- a/helm/ocaml/mathql_interpreter/pattern.ml +++ /dev/null @@ -1,53 +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://www.cs.unibo.it/helm/. - *) - -open Utility;; - -let cat l1 l2 = - if l1 > l2 then - l2 @ l1 - else - l1 @ l2 -;; - -let rec pattern_ex handle l = - match l with - [] -> [] - | s::tl -> let result = - let c = MQIConn.pgc handle in - let quoted_s = - Str.global_substitute (Str.regexp "'") - (function _ -> "\\'") s in - let qq = "select uri from registry where uri ~ '" ^ quoted_s ^ "' order by registry.uri asc" in - let res = c#exec (qq) in - List.map (function uri -> (List.hd uri,[])) res#get_list - (*for i = 0 to res#ntuples do - List.map (function uri -> (uri,[])) (res#get_tuple_list i) - done*) - - in - cat result (pattern_ex handle tl) -;; - diff --git a/helm/ocaml/mathql_interpreter/pattern.mli b/helm/ocaml/mathql_interpreter/pattern.mli deleted file mode 100644 index c5bf0bb82..000000000 --- a/helm/ocaml/mathql_interpreter/pattern.mli +++ /dev/null @@ -1,27 +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/. - *) - -val pattern_ex : - MQIConn.handle -> MathQL.value -> MathQL.resource_set diff --git a/helm/ocaml/mathql_interpreter/property.ml b/helm/ocaml/mathql_interpreter/property.ml deleted file mode 100644 index 34a75aa9a..000000000 --- a/helm/ocaml/mathql_interpreter/property.ml +++ /dev/null @@ -1,118 +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/. - *) - -(* - * - *) - -open Dbconn;; -open Utility;; -open Intersect;; - - -let getpid p = - if (p = "refObj") then "F" - else "B" -;; - -(* - * implementazione delle funzioni dublin core - *) -let rec property_ex handle rop path inv = function - [] -> [] - | s::tl -> let mprop = fst path in - prerr_endline mprop; - let l_sub_p = snd path in - - let prop = (if (l_sub_p <> []) then List.hd l_sub_p - else "") - in - match mprop with - - "refObj" (* in base al valore di prop restituisco i valori del relativo campo della tabella relativa all'uri rappresentata da s *) - | "backPointer" -> - prerr_endline mprop; - let mpid = getpid mprop in - let res = - let c = MQIConn.pgc handle in - let quoted_s = - Str.global_substitute (Str.regexp "'") - (function _ -> "\\'") s in - let tv = pgresult_to_string (c#exec ("select distinct id from registry where uri='" ^ quoted_s ^ "' order by id")) in - let q = "select distinct t" ^ tv ^ "." ^ prop ^ " from t" ^ tv ^ " where prop_id= '" ^ mpid ^ "' order by t" ^ tv ^ "." ^ prop in - prerr_endline q; - pgresult_to_string_list (c#exec q) - in - append (res,(property_ex handle rop path inv tl)) - - (*Rimane da capire cosa restituire nelle inverse!!!!*) - - - | "refRel" - | "refSort" -> - if inv then (* restituisco gli uri che il valore della prop richiesta uguale a s *) - let res = - let c = MQIConn.pgc handle in - let q = ("select distinct h" ^ mprop ^ ".uri from h" ^ mprop ^ " where h" ^ mprop ^ "." ^ prop ^ "= '" ^ s ^ "' order by h" ^ mprop ^ ".uri") in - prerr_endline q; - pgresult_to_string_list (c#exec q) - in - append (res,(property_ex handle rop path inv tl)) - - else - let res = (* restituisco il valore della prop relativo all'uri rappresentato da s*) - let c = MQIConn.pgc handle in - let quoted_s = - Str.global_substitute (Str.regexp "'") - (function _ -> "\\'") s in - let q = ("select distinct h" ^ mprop ^ "." ^ prop ^" from h" ^ mprop ^ " where h" ^ mprop ^ ".uri = '" ^ quoted_s ^ "' order by h" ^ mprop ^ "." ^ prop) in - pgresult_to_string_list (c#exec q) - in - append (res,(property_ex handle rop path inv tl)) - - - | _ -> (* metadati DC !!!! Controllare se i nomi delle tabelle cominciano con h !!!!*) - prerr_endline "DC"; - if inv then - let res = - let c = MQIConn.pgc handle in - let q = ("select " ^ mprop ^ ".uri from " ^ mprop ^ " where " ^ mprop ^ ".value = '" ^ s ^ "'") in - prerr_endline q; - pgresult_to_string_list (c#exec q) - in - append (res,(property_ex handle rop path inv tl)) - else - let res = - let c = MQIConn.pgc handle in - let quoted_s = - Str.global_substitute (Str.regexp "'") - (function _ -> "\\'") s in - let q = ("select " ^ mprop ^ ".value from " ^ mprop ^ " where " ^ mprop ^ ".uri = '" ^ quoted_s ^ "'") in - pgresult_to_string_list (c#exec q) - in - append (res,(property_ex handle rop path inv tl)) - -;; - diff --git a/helm/ocaml/mathql_interpreter/property.mli b/helm/ocaml/mathql_interpreter/property.mli deleted file mode 100644 index 832fc5eca..000000000 --- a/helm/ocaml/mathql_interpreter/property.mli +++ /dev/null @@ -1,27 +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/. - *) - -val property_ex: MQIConn.handle -> MathQL.refine -> MathQL.path -> bool -> MathQL.value -> MathQL.value - diff --git a/helm/ocaml/mathql_interpreter/relation.ml b/helm/ocaml/mathql_interpreter/relation.ml deleted file mode 100644 index 044bb82d3..000000000 --- a/helm/ocaml/mathql_interpreter/relation.ml +++ /dev/null @@ -1,506 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * - if 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://www.cs.unibo.it/helm/. - *) - - -(* - * implementazione del comando Relation - *) - - -open Union;; -open Dbconn;; -open Utility;; - -let quoted s = Str.global_substitute (Str.regexp "'") (function _ -> "\\'") s - -(* Cerca in una lista di assegnamenti (lista di coppie (path,path) dove path e' -di tipo (string * string list) quello relativo alla proprietà p e ne -restituisce la variabile a cui tale proprietà deve essere associata *) -let rec search p = function - [] -> "" - | (path1,path2)::tl -> if (fst(path2) = p) then fst(path1) - else search p tl -;; - - -let get_prop_id prop = - if prop="refObj" then "F" - else if prop="backPointer" then "B" - else assert false -;; - - -let relation_ex handle inv rop path rset assl = - let relk = fst path in - match relk with - - (* Nota: mancano le inverse di refObj e backPointer!!!! *) - -(* Notabis: ora per refObj si restituiscono tutti gli uri della tabella, nella diretta c'e` l'uri vuota *) -(* Notater: quando non richiedo tutte le proprieta` della tabella quelle che non voglio mi vengono restituite lo stesso ma con nome vuoto *) - - "refObj" - | "backPointer" -> (* proprieta` refObj e backPointer *) -(* print_endline "IN BACKPOINTER"; *) - let prop = get_prop_id relk in - if assl = [] then (* se non ci sono assegnamenti *) - let c = MQIConn.pgc handle in - let rset_list = (* lista di singoletti:resource_set di un elemento *) - (List.fold_left (fun acc (uri,l) -> - let tv = pgresult_to_string (c#exec ("select id from registry where uri='" ^ quoted uri ^ "'")) in - let qq = "select uri from t" ^ tv ^ " where prop_id='" ^ prop ^ "' order by uri asc" in -(* print_endline qq; *) - let res = c#exec qq in - - let l = (pgresult_to_string_list res) in -(* List.iter print_endline l; *) - (List.map - (function - [uri] -> [(uri,[])] - | _ -> assert false ) - res#get_list) @ acc - ) - [] rset - ) - in - let rec edup = function - [] -> [] - | rs1::tl -> union_ex rs1 (edup tl) - in - edup rset_list - - - else (* con assegnamenti *) - let c = MQIConn.pgc handle in - let rset_list = (* lista di singoletti:resource_set di un elemento *) - (List.fold_left (fun acc (uri,l) -> - let tv = pgresult_to_string (c#exec ("select id from registry where uri='" ^ quoted uri ^ "'")) in - let qq = "select uri, position, depth from t" ^ tv ^ " where prop_id='" ^ prop ^ "' order by uri asc" in - print_endline qq; - let res = c#exec qq in - let pos = search "position" assl in - let dep = search "depth" assl in - if ((pos != "") && (dep != "")) then (*caso in cui voglio sia position che depth*) - (List.map - (function - [uri;position;depth] -> [(uri,[[((pos, []),[position]);((dep, []),[depth])]])] - | _ -> assert false ) - res#get_list) @ acc - else - if (dep = "") then (* voglio solo position *) - (List.map - (function - [uri;position;depth] -> [(uri,[[((pos, []),[position])]])] - | _ -> assert false ) - res#get_list) @ acc - else (* voglio solo depth *) - (List.map - (function - [uri;position;depth] -> [(uri,[[((dep, []),[depth])]])] - | _ -> assert false ) - res#get_list) @ acc - - ) - [] rset - ) - in - let rec edup = function - [] -> [] - | rs1::tl -> union_ex rs1 (edup tl) - in - edup rset_list - -(* Fine proprieta` refObj e backPointer *) - - | "refRel" -> (* proprietà refRel *) - if assl = [] then [] (* se non ci sono assegnamenti *) -(* let c = MQIConn.pgc handle in - let rset_list = (* lista di singoletti:resource_set di un elemento *) - (List.fold_left (fun acc (uri,l) -> - let qq = "select uri from hrefRel order by uri asc" in - let res = c#exec qq in - (List.map - (function - [uri] -> [(uri,[])] - | _ -> assert false ) - res#get_list) @ acc - ) - [] rset - ) - in - let rec edup = function - [] -> [] - | rs1::tl -> union_ex rs1 (edup tl) - in - edup rset_list -*) - - else (* con assegnamenti *) - if inv then (* INVERSA *) - let c = MQIConn.pgc handle in - let rset_list = (* lista di singoletti:resource_set di un elemento *) - (List.fold_left (fun acc (uri,l) -> - let qq = "select uri, position, depth from hrefRel order by uri asc" in - let res = c#exec qq in - let pos = search "position" assl in - let dep = search "depth" assl in - if ((pos != "") && (dep != "")) then (*caso in cui voglio sia position che depth*) - (List.map - (function - [uri;position;depth] -> [(uri,[[((pos, []),[position]);((dep, []),[depth])]])] - | _ -> assert false ) - res#get_list) @ acc - else - if (dep = "") then (* voglio solo position *) - (List.map - (function - [uri;position;depth] -> [(uri,[[((pos, []),[position])]])] - | _ -> assert false ) - res#get_list) @ acc - else (* voglio solo depth *) - (List.map - (function - [uri;position;depth] -> [(uri,[[((dep, []),[depth])]])] - | _ -> assert false ) - res#get_list) @ acc - - ) - [] rset - ) - in - let rec edup = function - [] -> [] - | rs1::tl -> union_ex rs1 (edup tl) - in - edup rset_list - else (* DIRETTA, con risorsa nulla *) - let c = MQIConn.pgc handle in - let rset_list = (* lista di singoletti:resource_set di un elemento *) - (List.fold_left (fun acc (uri,l) -> - let qq = "select position, depth from hrefRel order by uri asc" in - let res = c#exec qq in - let pos = search "position" assl in - let dep = search "depth" assl in - if ((pos != "") && (dep != "")) then (*caso in cui voglio sia position che depth*) - (List.map - (function - [position;depth] -> [("",[[((pos, []),[position]);((dep, []),[depth])]])] - | _ -> assert false ) - res#get_list) @ acc - else - if (dep = "") then (* voglio solo position *) - (List.map - (function - [position;depth] -> [("",[[((pos, []),[position])]])] - | _ -> assert false ) - res#get_list) @ acc - else (* voglio solo depth *) - (List.map - (function - [position;depth] -> [("",[[((dep, []),[depth])]])] - | _ -> assert false ) - res#get_list) @ acc - - ) - [] rset - ) - in - let rec edup = function - [] -> [] - | rs1::tl -> union_ex rs1 (edup tl) - in - edup rset_list - - - - - -(* Fine proprieta` refRel *) - - - - - | "refSort" -> (* proprietà refSort *) - if assl = [] then [] (* se non ci sono assegnamenti *) -(* let c = MQIConn.pgc handle in - let rset_list = (* lista di singoletti:resource_set di un elemento *) - (List.fold_left (fun acc (uri,l) -> - let qq = "select uri from hrefSort order by uri asc" in - let res = c#exec qq in - (List.map - (function - [uri] -> [(uri,[])] - | _ -> assert false ) - res#get_list) @ acc - - ) - [] rset - ) - in - let rec edup = function - [] -> [] - | rs1::tl -> union_ex rs1 (edup tl) - in - edup rset_list -*) - - - else (* con assegnamenti *) - if inv then (*INVERSA ----> SISTEMARE: vedi refRel!!!!*) - let c = MQIConn.pgc handle in - let rset_list = (* lista di singoletti:resource_set di un elemento *) - (List.fold_left (fun acc (uri,l) -> - let qq = "select uri, position, depth, sort from hrefSort order by uri asc" in - let res = c#exec qq in - let pos = search "position" assl in - let dep = search "depth" assl in - let sor = search "sort" assl in - if ((pos != "") && (dep != "") && (sor != "")) then (*caso in cui - voglio position, depth e sort*) - (List.map - (function - [uri;position;depth;sort] -> [(uri,[[((pos, []),[position]);((dep, []),[depth]);((sor, []),[sort])]])] - | _ -> assert false ) - res#get_list) @ acc - else - if ((dep = "") && (sor = "")) then (* voglio solo position *) - (List.map - (function - [uri;position;depth;sort] -> [(uri,[[((pos, []),[position])]])] - | _ -> assert false ) - res#get_list) @ acc - - else - if ((pos = "") && (sor = "")) then (* voglio solo depth *) - (List.map - (function - [uri;position;depth;sort] -> [(uri,[[((dep, []),[depth])]])] - | _ -> assert false ) - res#get_list) @ acc - - else - if ((pos = "") && (dep = "")) then (* voglio solo sort *) - (List.map - (function - [uri;position;depth;sort] -> [(uri,[[((sor, []),[sort])]])] - | _ -> assert false ) - res#get_list) @ acc - - else - if ((pos = "") && (dep != "") && (sor != "")) then (*voglio depth e sort*) - (List.map - (function - [uri;position;depth;sort] -> [(uri,[[((dep, []),[depth]);((sor, []),[sort])]])] - | _ -> assert false ) - res#get_list) @ acc - - else - if((pos != "") && (dep = "") && (sor != "")) then (*voglio - position e sort*) - (List.map - (function - [uri;position;depth;sort] -> [(uri,[[((pos, []),[position]);((sor, []),[sort])]])] - | _ -> assert false ) - res#get_list) @ acc - - else - (* if ((pos != "") && (dep != "") && (sor = "")) then*) (*voglio - position e depth*) - (List.map - (function - [uri;position;depth;sort] -> [(uri,[[((pos, []),[position]);((dep, []),[depth])]])] - | _ -> assert false ) - res#get_list) @ acc - - ) - [] rset - ) - in - let rec edup = function - [] -> [] - | rs1::tl -> union_ex rs1 (edup tl) - in - edup rset_list - - else (* DIRETTA con risorsa vuota ----> SISTEMARE: vedi refRel!!!!*) - let c = MQIConn.pgc handle in - let rset_list = (* lista di singoletti:resource_set di un elemento *) - (List.fold_left (fun acc (uri,l) -> - let qq = "select position, depth, sort from hrefSort order by uri asc" in - let res = c#exec qq in - let pos = search "position" assl in - let dep = search "depth" assl in - let sor = search "sort" assl in - if ((pos != "") && (dep != "") && (sor != "")) then (*caso in cui - voglio position, depth e sort*) - (List.map - (function - [position;depth;sort] -> [("",[[((pos, []),[position]);((dep, []),[depth]);((sor, []),[sort])]])] - | _ -> assert false ) - res#get_list) @ acc - else - if ((dep = "") && (sor = "")) then (* voglio solo position *) - (List.map - (function - [position;depth;sort] -> [("",[[((pos, []),[position])]])] - | _ -> assert false ) - res#get_list) @ acc - - else - if ((pos = "") && (sor = "")) then (* voglio solo depth *) - (List.map - (function - [position;depth;sort] -> [("",[[((dep, []),[depth])]])] - | _ -> assert false ) - res#get_list) @ acc - - else - if ((pos = "") && (dep = "")) then (* voglio solo sort *) - (List.map - (function - [position;depth;sort] -> [("",[[((sor, []),[sort])]])] - | _ -> assert false ) - res#get_list) @ acc - - else - if ((pos = "") && (dep != "") && (sor != "")) then (*voglio depth e sort*) - (List.map - (function - [position;depth;sort] -> [("",[[((dep, []),[depth]);((sor, []),[sort])]])] - | _ -> assert false ) - res#get_list) @ acc - - else - if((pos != "") && (dep = "") && (sor != "")) then (*voglio - position e sort*) - (List.map - (function - [position;depth;sort] -> [("",[[((pos, []),[position]);((sor, []),[sort])]])] - | _ -> assert false ) - res#get_list) @ acc - - else - (* if ((pos != "") && (dep != "") && (sor = "")) then*) (*voglio - position e depth*) - (List.map - (function - [position;depth;sort] -> [("",[[((pos, []),[position]);((dep, []),[depth])]])] - | _ -> assert false ) - res#get_list) @ acc - - ) - [] rset - ) - in - let rec edup = function - [] -> [] - | rs1::tl -> union_ex rs1 (edup tl) - in - edup rset_list - - - -(* Fine proprieta` refSort *) - - - - | _ -> [] - -;; - - - -(**** IMPLEMENTAZIONE DELLA RELATION PER GALAX ****) - - -(* trasforma un uri in un filename *) -let tofname uri = - if String.contains uri ':' then - (let len = String.length uri in - let scuri = String.sub uri 4 (len-4) in (*tolgo cic:*) - if String.contains scuri '#' then - (let pos = String.index scuri '#' in - let s1 = Str.string_before scuri pos in - let xp = Str.string_after scuri pos in - let xp = Str.global_replace (Str.regexp "#xpointer(1") "" xp in - let xp = Str.global_replace (Str.regexp "\/") "," xp in - let xp = Str.global_replace (Str.regexp ")") "" xp in - let fname = (s1 ^ xp) in - fname) - else - scuri) - else uri - - -(* prende una lista di uri (contenente alternativamente uri e pos) e costruisce una lista di resource *) -let rec rsetl uril vvar = - match uril with - | uri::tl -> let scuri = (*tofname*) uri in - [(scuri, [[((vvar, []), [(List.hd tl)])]])]::(rsetl (List.tl tl) vvar) - | [] -> [] - - -(* prende una resource e una vvar e restituisce la lista delle resource in relazione (refObj o backPointer in base al parametro "path") con tale resource e associa alla proprieta' il nome della vvar contenuto in "assl" *) -let muse path assl r = - let vvar = if assl = [] then "position" - else List.hd assl - in - let uri = fst r in - let furi = tofname uri in - let dtag = fst path in - let dir = - match dtag with - "refObj" -> "/projects/helm/metadata/create4/forward" - | _ -> "/projects/helm/metadata/create4/backward" - in - let xq ="namespace h=\"http://www.cs.unibo.it/helm/schemas/mattone.rdf#\" - namespace rdf=\"http://www.w3.org/1999/02/22-rdf-syntax-ns#\" - for $i in document(" ^ "\"" ^ dir ^ furi ^ ".xml" ^ "\"" ^ - ")/rdf:RDF/h:Object/h:" ^ dtag ^ "/h:Occurrence - return ($i/h:occurrence, $i/h:position)" - - in - let uril = Toputils.eval_query_string xq in (* e' una lista di liste di stringhe*) - let hd_uril = List.hd uril in(*prendo la testa che contiene altern. lista di uri e pos. *) - let rset_list = rsetl hd_uril vvar in (* da hd_uril costruisco una lista di resource_set(singoletti)*) - let rec edup = function - [] -> [] - | rs1::tl -> union_ex rs1 (edup tl) - in - edup rset_list - - - - -(* prende un resource_set, una vvar (primo el. di assl) a cui associare la posizione, e la relazione (refObj o backPointer) e per ogni resource chiama la muse -NOTA: "rop" per ora non viene usato perche' vale sempre "ExactOp" *) -let relation_galax_ex handle inv rop path rset assl = [] - -(* - - List.stable_sort (fun (uri1,l1) (uri2,l2) -> compare uri1 uri2) (List.concat (List.map (muse path assl) rset)) - -*) diff --git a/helm/ocaml/mathql_interpreter/relation.mli b/helm/ocaml/mathql_interpreter/relation.mli deleted file mode 100644 index b32f36f3b..000000000 --- a/helm/ocaml/mathql_interpreter/relation.mli +++ /dev/null @@ -1,32 +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/. - *) - -val relation_ex : MQIConn.handle -> - bool -> MathQL.refine -> MathQL.path -> MathQL.resource_set -> MathQL.assign list-> MathQL.resource_set - - -val relation_galax_ex : MQIConn.handle -> -bool -> MathQL.refine -> MathQL.path -> MathQL.resource_set -> MathQL.assign list -> MathQL.resource_set - diff --git a/helm/ocaml/mathql_interpreter/sub.ml b/helm/ocaml/mathql_interpreter/sub.ml deleted file mode 100644 index a8ca9e629..000000000 --- a/helm/ocaml/mathql_interpreter/sub.ml +++ /dev/null @@ -1,43 +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/. - *) - - -let rec sub_ex v1 v2 = - match v1,v2 with - [],_ -> true - | _,[] -> false - | s1::_, s2::_ when s1 < s2 -> false - | s1::_, s2::tl2 when s2 < s1 -> sub_ex v1 tl2 - | s1::tl1, s2::tl2 -> sub_ex tl1 tl2 -;; - -(* DEBUGGING ONLY -let sub_ex v1 v2 = - let b = sub_ex v1 v2 in - prerr_endline - ("SUB({" ^ String.concat "," v1 ^ "},{" ^ String.concat "," v2 ^"}) = " ^ - if b then "tt" else "ff") ; - b -;; *) diff --git a/helm/ocaml/mathql_interpreter/sub.mli b/helm/ocaml/mathql_interpreter/sub.mli deleted file mode 100644 index b81f542c4..000000000 --- a/helm/ocaml/mathql_interpreter/sub.mli +++ /dev/null @@ -1,27 +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/. - *) - - -val sub_ex: MathQL.value -> MathQL.value -> bool diff --git a/helm/ocaml/mathql_interpreter/union.ml b/helm/ocaml/mathql_interpreter/union.ml deleted file mode 100644 index e2d9fcb01..000000000 --- a/helm/ocaml/mathql_interpreter/union.ml +++ /dev/null @@ -1,52 +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/. - *) - -(* - * implementazione del comando UNION - *) - - -(* Merges two attribute group lists preserves order and gets rid of duplicates*) -let rec merge l1 l2 = - match (l1,l2) with - [],l - | l,[] -> l - | g1::tl1,g2::_ when g1 < g2 -> g1::(merge tl1 l2) - | g1::_,g2::tl2 when g2 < g1 -> g2::(merge l1 tl2) - | g1::tl1,g2::tl2 -> g1::(merge tl1 tl2) -;; - -(* preserves order and gets rid of duplicates *) -let rec union_ex rs1 rs2 = - match (rs1, rs2) with - [],l - | l,[] -> l - | (uri1,l1)::tl1,(uri2,_)::_ when uri1 < uri2 -> (uri1,l1)::(union_ex tl1 rs2) - | (uri1,_)::_,(uri2,l2)::tl2 when uri2 < uri1 -> (uri2,l2)::(union_ex rs1 tl2) - | (uri1,l1)::tl1,(uri2,l2)::tl2 -> if l1 = l2 then (uri1,l1)::(union_ex tl1 tl2) - else (uri1,merge l1 l2)::(union_ex tl1 tl2) -;; - - diff --git a/helm/ocaml/mathql_interpreter/union.mli b/helm/ocaml/mathql_interpreter/union.mli deleted file mode 100644 index 6890bdb0c..000000000 --- a/helm/ocaml/mathql_interpreter/union.mli +++ /dev/null @@ -1,27 +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/. - *) - -val union_ex : -MathQL.result -> MathQL.result -> MathQL.result diff --git a/helm/ocaml/mathql_interpreter/utility.ml b/helm/ocaml/mathql_interpreter/utility.ml deleted file mode 100644 index af99d72fe..000000000 --- a/helm/ocaml/mathql_interpreter/utility.ml +++ /dev/null @@ -1,119 +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://www.cs.unibo.it/helm/. - *) - -(* - * funzioni di utilita' generale - *) - -open Dbconn;; - -(* - * converte il risultato di una query in una lista di stringhe - * - * parametri: - * l: Postgres.result; risultato della query - * - * output: string list; lista di stringhe (una per tupla) - * - * assumo che il risultato della query sia - * costituito da un solo valore per tupla - * - * TODO - * verificare che l sia effettivamente costruita come richiesto - *) -let pgresult_to_string_list l = List.map (List.hd) l#get_list;; - -(* - * converte il risultato di una query in una stringa - * - * paramteri: - * l: Postgres.result; risultato della query - * - * output: string; valore dell'unica tupla del risultato - * - * mi aspetto che il risultato contenga una sola tupla - * formata da un solo valore - * - * TODO - * verificare che l sia costruita come richiesto - *) -let pgresult_to_string l = - match l#get_list with - [] -> "" - | t -> List.hd (List.hd t) -;; - -(* - * parametri: - * x: 'a; chiave di cui settare il valore - * v: 'b; valore da assegnare alla chiave - * l: ('a * 'b) list; lista di coppie in cui effettuare - * l'assegnamento - * - * output: ('a * 'b) list; lista di coppie contenente (x, v) - * - * TODO - * gestire i casi in cui in l compaiono piu' coppie (x, _) - * si sostituiscono tutte? se ne sostituisce una e si eliminano - * le altre? - *) -let set_assoc x v l = - let rec spila testa key value lista = - match lista with - [] -> testa @ [(key, value)] - | (j, _)::tl when j = key -> testa @ [(key, value)] @ tl - | hd::tl -> spila (testa @ [hd]) key value tl - in - spila [] x v l -;; - -(* - * parametri: - * p: string; nome della proprieta' - * - * output: string; id interno associato alla proprieta' - *) -let helm_property_id handle p = - let c = MQIConn.pgc handle in - let q1 = "select att0 from namespace where att1='http://www.cs.unibo.it/helm/schemas/mattone.rdf#'" in - let ns = pgresult_to_string (c#exec q1) in - let q2 = ("select att0 from property where att2='" ^ p ^ "' and att1=" ^ ns) in - let retval = pgresult_to_string (c#exec q2) in - (*let _ = prerr_endline ("utility:q2: " ^ q2 ^ " : " ^ retval) in*) - retval -;; - -(* - * parametri: - * c: string; nome della classe - * - * output: string; id interno associato alla classe - *) -let helm_class_id handle cl = - let c = MQIConn.pgc handle in - let ns = pgresult_to_string (c#exec ("select att0 from namespace where att1='http://www.cs.unibo.it/helm/schemas/mattone.rdf#'")) in - pgresult_to_string (c#exec ("select att0 from class where att2='" ^ cl ^ "' and att1=" ^ ns)) -;; - diff --git a/helm/ocaml/mathql_interpreter/utility.mli b/helm/ocaml/mathql_interpreter/utility.mli deleted file mode 100644 index 2ee3db007..000000000 --- a/helm/ocaml/mathql_interpreter/utility.mli +++ /dev/null @@ -1,30 +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://www.cs.unibo.it/helm/. - *) - -val pgresult_to_string_list : < get_list : string list list; .. > -> string list -val pgresult_to_string : < get_list : string list list; .. > -> string -val set_assoc : 'a -> 'b -> ('a * 'b) list -> ('a * 'b) list -val helm_property_id: MQIConn.handle -> string -> string -val helm_class_id: MQIConn.handle -> string -> string diff --git a/helm/ocaml/mathql_test/.depend b/helm/ocaml/mathql_test/.depend index 3a19b9d0a..b8d9e578a 100644 --- a/helm/ocaml/mathql_test/.depend +++ b/helm/ocaml/mathql_test/.depend @@ -1,5 +1,5 @@ -mqgtop.cmo: mQGTopParser.cmi -mqgtop.cmx: mQGTopParser.cmx +mqgtop.cmo: mQGTopLexer.cmo mQGTopParser.cmi +mqgtop.cmx: mQGTopLexer.cmx mQGTopParser.cmx mQGTopParser.cmo: mQGTopParser.cmi mQGTopParser.cmx: mQGTopParser.cmi mQGTopLexer.cmo: mQGTopParser.cmi diff --git a/helm/ocaml/mathql_test/Makefile b/helm/ocaml/mathql_test/Makefile index 6b2c6662f..04fea5185 100644 --- a/helm/ocaml/mathql_test/Makefile +++ b/helm/ocaml/mathql_test/Makefile @@ -1,6 +1,6 @@ BIN_DIR = /usr/local/bin -REQUIRES = unix helm-cic helm-cic_textual_parser helm-mathql \ - helm-mathql_interpreter helm-mathql_generator +REQUIRES = unix helm-cic_textual_parser \ + helm-mathql helm-mathql_interpreter helm-mathql_generator PREDICATES = OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) diff --git a/helm/ocaml/mathql_test/mQGTopLexer.mll b/helm/ocaml/mathql_test/mQGTopLexer.mll index 476460646..da6971028 100644 --- a/helm/ocaml/mathql_test/mQGTopLexer.mll +++ b/helm/ocaml/mathql_test/mQGTopLexer.mll @@ -23,8 +23,15 @@ * http://cs.unibo.it/helm/. *) -(* AUTOR: Ferruccio Guidi - *) +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Ferruccio Guidi *) +(* 23/05/2002 *) +(* *) +(* *) +(******************************************************************************) { open MQGTopParser @@ -46,28 +53,26 @@ rule comm_token = parse | ['*' '('] { comm_token lexbuf } | [^ '*' '(']* { comm_token lexbuf } and string_token = parse - | '"' { DQ } - | '\\' _ { STR (String.sub (Lexing.lexeme lexbuf) 1 1) } - | QSTR { STR (Lexing.lexeme lexbuf) } - | eof { EOF } + | '"' { DQ } + | '\\' _ { STR (String.sub (Lexing.lexeme lexbuf) 1 1) } + | QSTR { STR (Lexing.lexeme lexbuf) } + | eof { EOF } and spec_token = parse - | "(*" { comm_token lexbuf; spec_token lexbuf } - | SPC { spec_token lexbuf } - | '"' { let str = qstr string_token lexbuf in - out ("STR " ^ str); STR str } - | '{' { out "LC"; LC } - | '}' { out "RC"; RC } - | ',' { out "CM"; CM } - | '$' { out "DL"; DL } - | "not" { out "NOT" ; NOT } - | "mustobj" { out "MOBJ" ; MOBJ } - | "mustsort" { out "MSORT" ; MSORT } - | "mustrel" { out "MREL" ; MREL } - | "sonlyobj" { out "SOBJ" ; SOBJ } - | "sonlysort" { out "SSORT" ; SSORT } - | "onlyrel" { out "OREL" ; OREL } - | "wonlyobj" { out "WOBJ" ; WOBJ } - | "wonlysort" { out "WSORT" ; WSORT } - | IDEN { let id = Lexing.lexeme lexbuf in - out ("ID " ^ id); ID id } - | eof { EOF } + | "(*" { comm_token lexbuf; spec_token lexbuf } + | SPC { spec_token lexbuf } + | '"' { let str = qstr string_token lexbuf in + out ("STR " ^ str); STR str } + | '{' { out "LC"; LC } + | '}' { out "RC"; RC } + | ',' { out "CM"; CM } + | '$' { out "DL"; DL } + | "mustobj" { out "MOBJ" ; MOBJ } + | "mustsort" { out "MSORT" ; MSORT } + | "mustrel" { out "MREL" ; MREL } + | "onlyobj" { out "OOBJ" ; OOBJ } + | "onlysort" { out "OSORT" ; OSORT } + | "onlyrel" { out "OREL" ; OREL } + | "universe" { out "UNIV" ; UNIV } + | IDEN { let id = Lexing.lexeme lexbuf in + out ("ID " ^ id); ID id } + | eof { EOF } diff --git a/helm/ocaml/mathql_test/mQGTopParser.mly b/helm/ocaml/mathql_test/mQGTopParser.mly index 8aa01b6c4..e36dd5435 100644 --- a/helm/ocaml/mathql_test/mQGTopParser.mly +++ b/helm/ocaml/mathql_test/mQGTopParser.mly @@ -26,7 +26,6 @@ /* AUTOR: Ferruccio Guidi */ - %{ let f (x, y, z) = x let s (x, y, z) = y @@ -45,11 +44,12 @@ %type CicTextualParser0.interpretation_codomain_item option> interp %token STR - %token DL DQ LC RC CM NOT - %token MOBJ MSORT MREL SOBJ SSORT OREL WOBJ WSORT + %token DL DQ LC RC CM + %token MOBJ MSORT MREL OOBJ OSORT OREL UNIV - %start qstr - %type qstr + %start qstr specs + %type qstr + %type specs %% uri: | CONURI { CicTextualParser0.ConUri $1 } @@ -74,7 +74,7 @@ | DQ { "" } | STR qstr { $1 ^ $2 } ; -/* str: + str: | STR { $1 } | DL ID { try G.builtin $2 with _ -> "" } ; @@ -86,22 +86,16 @@ list: | LC strs RC { $2 } ; - not: - | NOT { true } - | { false } - ; spec: - | MOBJ not list list list { G.MustObj ($2, $3, $4, $5) } - | MSORT not list list list { G.MustSort ($2, $3, $4, $5) } - | MREL not list list { G.MustRel ($2, $3, $4) } - | SOBJ not list list list { G.SOnlyObj ($2, $3, $4, $5) } - | SSORT not list list list { G.SOnlySort ($2, $3, $4, $5) } - | OREL not list list { G.OnlyRel ($2, $3, $4) } - | WOBJ not list list list { G.WOnlyObj ($2, $3, $4, $5) } - | WSORT not list list list { G.WOnlySort ($2, $3, $4, $5) } + | MOBJ list list list { G.MustObj ($2, $3, $4) } + | MSORT list list list { G.MustSort ($2, $3, $4) } + | MREL list list { G.MustRel ($2, $3) } + | OOBJ list list list { G.OnlyObj ($2, $3, $4) } + | OSORT list list list { G.OnlySort ($2, $3, $4) } + | OREL list list { G.OnlyRel ($2, $3) } + | UNIV list { G.Universe $2 } ; specs: | spec specs { $1 :: $2 } | EOF { [] } ; -*/ diff --git a/helm/ocaml/mathql_test/mqgtop.ml b/helm/ocaml/mathql_test/mqgtop.ml index be35ac6c8..9e1dcde0d 100644 --- a/helm/ocaml/mathql_test/mqgtop.ml +++ b/helm/ocaml/mathql_test/mqgtop.ml @@ -38,17 +38,22 @@ let int_options = ref "" let nl = "

\n" -module MQX = MQueryMisc -module MQI = MQueryInterpreter -module MQIC = MQIConn -module MQG = MQueryGenerator +module U = MQueryUtil +module I = MQueryInterpreter +module C = MQIConn +module G = MQueryGenerator +module L = MQGTopLexer +module P = MQGTopParser +module TL = CicTextualLexer +module TP = CicTextualParser +module C2 = MQueryLevels2 +module C1 = MQueryLevels let get_handle () = - MQIC.init (MQIC.flags_of_string ! int_options) - (fun s -> print_string s; flush stdout) + C.init (C.flags_of_string ! int_options) + (fun s -> print_string s; flush stdout) let issue handle q = - let module U = MQueryUtil in let mode = [Open_wronly; Open_append; Open_creat; Open_text] in let perm = 64 * 6 + 8 * 6 + 4 in let time () = @@ -72,29 +77,26 @@ let issue handle q = close_out och in if ! show_queries then U.text_of_query (output_string stdout) q nl; - let r = MQI.execute handle q in + let r = I.execute handle q in U.text_of_result (output_string stdout) r nl; if ! log_file <> "" then log q r; incr query_num; flush stdout let get_interp () = - let module L = CicTextualLexer in - let module T = CicTextualParser in - let module P = MQGTopParser in let lexer = function - | T.ID s -> P.ID s - | T.CONURI u -> P.CONURI u - | T.VARURI u -> P.VARURI u - | T.INDTYURI (u, p) -> P.INDTYURI (u, p) - | T.INDCONURI (u, p, s) -> P.INDCONURI (u, p, s) - | T.LETIN -> P.ALIAS - | T.EOF -> P.EOF + | TP.ID s -> P.ID s + | TP.CONURI u -> P.CONURI u + | TP.VARURI u -> P.VARURI u + | TP.INDTYURI (u, p) -> P.INDTYURI (u, p) + | TP.INDCONURI (u, p, s) -> P.INDCONURI (u, p, s) + | TP.LETIN -> P.ALIAS + | TP.EOF -> P.EOF | _ -> assert false in let ich = open_in ! interp_file in let lexbuf = Lexing.from_channel ich in - let f = P.interp (fun x -> lexer (L.token x)) lexbuf in + let f = P.interp (fun x -> lexer (TL.token x)) lexbuf in close_in ich; f let get_terms interp = @@ -131,7 +133,6 @@ let rec display = function flush stdout let execute ich = - let module U = MQueryUtil in let lexbuf = Lexing.from_channel ich in let handle = get_handle () in let rec execute_aux () = @@ -141,43 +142,43 @@ let execute ich = with End_of_file -> () in execute_aux (); - MQIC.close handle -(* + C.close handle + let compose () = - let module P = MQGTopParser in - let module L = MQGTopLexer in - let module G = MQueryGeneratorNew in + let handle = get_handle () in let cl = P.specs L.spec_token (Lexing.from_channel stdin) in - issue (G.compose cl) -*) + issue handle (G.compose cl); + C.close handle + let locate name = let handle = get_handle () in - issue handle (MQG.locate name); - MQIC.close handle + issue handle (G.locate name); + C.close handle let mpattern n m l = - let module C = MQueryLevels2 in let queries = ref [] in + let univ = Some [G.builtin "MH"; G.builtin "IH"; + G.builtin "MC"; G.builtin "IC"] in let handle = get_handle () in let rec pattern level = function | [] -> () | term :: tail -> pattern level tail; print_string ("? " ^ CicPp.ppterm term ^ nl); - let t = MQX.start_time () in - let om,rm,sm = C.get_constraints term in + let t = U.start_time () in + let om,rm,sm = C2.get_constraints term in let oml,rml,sml = List.length om, List.length rm, List.length sm in let oo, ool = if level land 1 = 0 then None, 0 else Some om, oml in let ro, rol = if level land 2 = 0 then None, 0 else Some rm, rml in let so, sol = if level land 4 = 0 then None, 0 else Some sm, sml in - let q = MQG.query_of_constraints None (om,rm,sm) (oo,ro,so) in + let q = G.query_of_constraints univ (om,rm,sm) (oo,ro,so) in if not (List.mem q ! queries) then begin issue handle q; Printf.eprintf "[%i] " (pred ! query_num); flush stderr; Printf.printf "%i GEN = %i: %s" (pred ! query_num) (oml + rml + sml + ool + rol + sol) - (MQX.stop_time t ^ nl); + (U.stop_time t ^ nl); flush stdout; queries := q :: ! queries end in @@ -188,38 +189,35 @@ let mpattern n m l = Printf.eprintf "\nmqgtop: pattern: %i queries issued\n" (List.length ! queries); flush stderr; - MQIC.close handle -(* + C.close handle + let mbackward n m l = - let module C = MQueryLevels in - let module G = MQueryGenerator in let queries = ref [] in let torigth_restriction (u, b) = - let p = if b - then "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" - else "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" - in + let p = if b then G.builtin "MC" else G.builtin "IC" in (u, p, None) in + let univ = Some [G.builtin "MC"; G.builtin "IC"] in + let handle = get_handle () in let rec backward level = function | [] -> () | term :: tail -> backward level tail; print_string ("? " ^ CicPp.ppterm term ^ nl); - let t0 = Sys.time () in - let list_of_must, only = C.out_restr [] [] term in + let t = U.start_time () in + let list_of_must, only = C1.out_restr [] [] term in let max_level = pred (List.length list_of_must) in let must = List.nth list_of_must (min level max_level) in let rigth_must = List.map torigth_restriction must in let rigth_only = Some (List.map torigth_restriction only) in - let q = G.searchPattern (rigth_must, [], []) (rigth_only , None, None) in + let q = G.query_of_constraints univ (rigth_must, [], []) (rigth_only , None, None) in if not (List.mem q ! queries) then begin - issue q; - let t1 = Sys.time () -. t0 in + issue handle q; Printf.eprintf "[%i] " (pred ! query_num); flush stderr; - Printf.printf "%i GEN = %i: %.2fs%s" - (pred ! query_num) (List.length must) t1 nl; + Printf.printf "%i GEN = %i: %s" + (pred ! query_num) (List.length must) + (U.stop_time t ^ nl); flush stdout; queries := q :: ! queries end in @@ -229,15 +227,15 @@ let mbackward n m l = done; Printf.eprintf "\nmqgtop: backward: %i queries issued\n" (List.length ! queries); - flush stderr -*) - + flush stderr; + C.close handle + let check () = let handle = get_handle () in Printf.eprintf "mqgtop: current options: %s, connection: %s\n" - ! int_options (if MQIC.connected handle then "on" else "off"); - MQIC.close handle + ! int_options (if C.connected handle then "on" else "off"); + C.close handle let prerr_help () = prerr_endline "\nUSAGE: mqgtop.opt OPTIONS < INPUTFILE\n"; @@ -255,13 +253,13 @@ let prerr_help () = prerr_endline "-i -interp FILE sets the CIC short names interpretation file"; prerr_endline "-d -disply outputs the CIC terms given in the input file"; prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias"; -(* prerr_endline "-C -compose issues the \"Compose\" query reading its specifications"; + prerr_endline "-C -compose issues the \"Compose\" query reading its specifications"; prerr_endline " from the input file"; prerr_endline "-B -backward LEVEL issues the \"Backward\" query for the given level on all"; prerr_endline " CIC terms in the input file"; prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0"; prerr_endline " on all CIC terms in the input file"; -*) prerr_endline "-P -pattern LEVEL issues the \"Pattern\" query for the given level on all"; + prerr_endline "-P -pattern LEVEL issues the \"Pattern\" query for the given level on all"; prerr_endline " CIC terms in the input file"; prerr_endline "-MP -multi-pattern issues the \"Pattern\" query for each level from 7 to 0"; prerr_endline " on all CIC terms in the input file\n"; @@ -282,21 +280,21 @@ let rec parse = function | ("-c"|"-check") :: rem -> check (); parse rem | ("-l"|"-log-file") :: arg :: rem -> log_file := arg; parse rem | ("-L"|"-Locate") :: arg :: rem -> locate arg; parse rem -(* | ("-C"|"-compose") :: rem -> compose (); parse rem + | ("-C"|"-compose") :: rem -> compose (); parse rem | ("-M"|"-backward") :: arg :: rem -> let m = (int_of_string arg) in mbackward m m (get_terms ()); parse rem | ("-MB"|"-multi-backward") :: arg :: rem -> let m = (int_of_string arg) in mbackward m 0 (get_terms ()); parse rem -*) | ("-P"|"-pattern") :: arg :: rem -> + | ("-P"|"-pattern") :: arg :: rem -> let m = (int_of_string arg) in mpattern m m (get_terms ()); parse rem | ("-MP"|"-multi-pattern") :: rem -> mpattern 7 0 (get_terms ()); parse rem | _ :: rem -> parse rem let _ = - let t = MQX.start_time () in + let t = U.start_time () in Logger.log_callback := (Logger.log_to_html ~print_and_flush:(fun s -> print_string s; flush stdout)) ; parse (List.tl (Array.to_list Sys.argv)); - prerr_endline ("mqgtop: done in " ^ (MQX.stop_time t)); + prerr_endline ("mqgtop: done in " ^ (U.stop_time t)); exit 0 diff --git a/helm/ocaml/mathql_test/mqitop.ml b/helm/ocaml/mathql_test/mqitop.ml index 8a8053718..7dd43888c 100644 --- a/helm/ocaml/mathql_test/mqitop.ml +++ b/helm/ocaml/mathql_test/mqitop.ml @@ -27,12 +27,11 @@ *) module U = MQueryUtil -module X = MQueryMisc module I = MQueryInterpreter module C = MQIConn let _ = - let t = X.start_time () in + let t = U.start_time () in let ich = Lexing.from_channel stdin in let flags = if Array.length Sys.argv >= 2 then Sys.argv.(1) else "" in let log s = print_string s; flush stdout in @@ -41,13 +40,13 @@ let _ = print_endline "mqitop: no connection"; flush stdout end; let rec aux () = - let t = X.start_time () in + let t = U.start_time () in let r = I.execute handle (U.query_of_text ich) in - U.text_of_result print_string r "\n"; - Printf.printf "mqitop: query: %s,%i\n" (X.stop_time t) (List.length r); +(* U.text_of_result log r "\n"; +*) Printf.printf "mqitop: query: %s,%i\n" (U.stop_time t) (List.length r); flush stdout; aux() in begin try aux() with End_of_file -> () end; C.close handle; - Printf.printf "mqitop: done: %s\n" (X.stop_time t) + Printf.printf "mqitop: done: %s\n" (U.stop_time t) diff --git a/helm/ocaml/mathql_test/mqtop.ml b/helm/ocaml/mathql_test/mqtop.ml index 4b8da7f49..48ffb1e74 100644 --- a/helm/ocaml/mathql_test/mqtop.ml +++ b/helm/ocaml/mathql_test/mqtop.ml @@ -28,14 +28,13 @@ let _ = let module U = MQueryUtil in - let module X = MQueryMisc in - let t = X.start_time () in + let t = U.start_time () in let ich = Lexing.from_channel stdin in let rec aux () = - let t = X.start_time () in + let t = U.start_time () in U.text_of_query print_string (U.query_of_text ich) "\n"; - Printf.printf "mqtop: query: %s\n" (X.stop_time t); + Printf.printf "mqtop: query: %s\n" (U.stop_time t); flush stdout; aux() in begin try aux() with End_of_file -> () end; - Printf.printf "mqtop: done: %s\n" (X.stop_time t) + Printf.printf "mqtop: done: %s\n" (U.stop_time t)