requires="helm-urimanager"
-version="0.0.1"
+version="1.3"
archive(byte)="mathql.cma"
archive(native)="mathql.cmxa"
linkopts=""
-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=""
-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=""
-version="1.2"
+requires="unix helm-cic_textual_parser helm-mathql helm-mathql_interpreter helm-mathql_generator"
+version="1.3"
+linkopts=""
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
+++ /dev/null
-(* 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)
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 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
* http://cs.unibo.it/helm/.
*)
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
-(* 23/05/2002 *)
-(* *)
-(* *)
-(******************************************************************************)
+(*
+ *)
{
open MQueryTParser
| '$' { 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 }
* http://cs.unibo.it/helm/.
*/
-/******************************************************************************/
-/* */
-/* PROJECT HELM */
-/* */
-/* Ferruccio Guidi <fguidi@cs.unibo.it> */
-/* 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 <string> 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 <string> qstr
%type <MathQL.query> query
svar:
| PC ID { $2 }
;
- rvar:
+ avar:
| AT ID { $2 }
;
vvar:
| 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 }
| 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 }
* http://cs.unibo.it/helm/.
*)
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
-(* 30/04/2002 *)
-(* *)
-(* *)
-(******************************************************************************)
-
+(*
+ *)
(* text linearization and parsing *******************************************)
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
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)
| [] -> str
| [t] -> str ^ xp t ^ ")"
| t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")"
+
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
-
* http://www.cs.unibo.it/helm/.
*)
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
-(* Irene Schena <schena@cs.unibo.it> *)
-(* 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 *)
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 *)
| 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
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 =
* 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"
| "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)
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
-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
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 =
+++ /dev/null
-(* 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}
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
-;;
-*)
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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))
-;;
-
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
-;;
+++ /dev/null
-(* 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
* 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 *)
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"
| Stat -> "S"
| Quiet -> "Q"
| Warn -> "W"
+ | Log -> "L"
let flag_of_char = function
| 'P' -> [Postgres]
| 'S' -> [Stat]
| 'Q' -> [Quiet]
| 'W' -> [Warn]
+ | 'L' -> [Log]
| _ -> []
let string_fold_left f a 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
* 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
* 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
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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 <fguidi@cs.unibo.it> *)
-(* 06/01/2003 *)
-(* *)
-(* *)
-(******************************************************************************)
-
-val execute : (string -> unit) -> string -> MathQL.query -> MathQL.result
*)
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
* http://cs.unibo.it/helm/.
*)
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
-(* 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
module M = MathQL
module P = MQIPostgres
+module C = MQIConn
module U = MQIUtil
let not_supported s =
(* 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
| [], 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
| [_; 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
| _ -> ""
*)
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
| [] -> [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)
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
* 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
--- /dev/null
+(* 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,[])
+;;
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
+++ /dev/null
-(* 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
-;;
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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)
-;;
-
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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))
-
-;;
-
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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))
-
-*)
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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
-;; *)
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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)
-;;
-
-
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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))
-;;
-
+++ /dev/null
-(* 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
-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
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)
* http://cs.unibo.it/helm/.
*)
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
+(* 23/05/2002 *)
+(* *)
+(* *)
+(******************************************************************************)
{
open MQGTopParser
| ['*' '('] { 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 }
/* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*/
-
%{
let f (x, y, z) = x
let s (x, y, z) = y
%type <CicTextualParser0.interpretation_domain_item -> CicTextualParser0.interpretation_codomain_item option> interp
%token <string> 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 <string> qstr
+ %start qstr specs
+ %type <string> qstr
+ %type <MQueryGenerator.spec list> specs
%%
uri:
| CONURI { CicTextualParser0.ConUri $1 }
| DQ { "" }
| STR qstr { $1 ^ $2 }
;
-/* str:
+ str:
| STR { $1 }
| DL ID { try G.builtin $2 with _ -> "" }
;
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 { [] }
;
-*/
let nl = " <p>\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 () =
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 =
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 () =
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
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
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";
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";
| ("-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
*)
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
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)
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)
projects / helm.git / commitdiff