From: Ferruccio Guidi Date: Tue, 23 Sep 2003 15:12:46 +0000 (+0000) Subject: Now mathql_generator compiles before mathql_interpreter. X-Git-Tag: V_0_4_3_4~18 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68e62a195d6228befb75b4e2edd59bc58b1cdb0c;p=helm.git Now mathql_generator compiles before mathql_interpreter. This feature, announced in my Ph.D. thesis, will allow the interpreter to interact with the generator. --- diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 8eae88814..c0ef52ff8 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -1,8 +1,8 @@ # Warning: the modules must be in compilation order MODULES = xml urimanager getter pxp cic cic_annotations cic_annotations_cache \ cic_cache cic_proof_checking cic_textual_parser \ - tex_cic_textual_parser cic_unification mathql mathql_interpreter \ - mathql_generator cic_omdoc tactics cic_transformations + tex_cic_textual_parser cic_unification mathql mathql_generator \ + mathql_interpreter cic_omdoc tactics cic_transformations OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ OCAMLFIND_META_DIR = @OCAMLFIND_META_DIR@ diff --git a/helm/ocaml/mathql/.cvsignore b/helm/ocaml/mathql/.cvsignore index cd9b591e3..6b3eba302 100644 --- a/helm/ocaml/mathql/.cvsignore +++ b/helm/ocaml/mathql/.cvsignore @@ -1 +1 @@ -*.cm[iaox] *.cmxa mQueryTLexer.ml mQueryTParser.ml mQueryTParser.mli +*.cm[iaox] *.cmxa diff --git a/helm/ocaml/mathql/.depend b/helm/ocaml/mathql/.depend index 769e30c89..30dbaa280 100644 --- a/helm/ocaml/mathql/.depend +++ b/helm/ocaml/mathql/.depend @@ -1,8 +1,2 @@ -mQueryTParser.cmi: mathQL.cmo -mQueryUtil.cmi: mathQL.cmo -mQueryTParser.cmo: mathQL.cmo mQueryTParser.cmi -mQueryTParser.cmx: mathQL.cmx mQueryTParser.cmi -mQueryTLexer.cmo: mQueryTParser.cmi -mQueryTLexer.cmx: mQueryTParser.cmx -mQueryUtil.cmo: mQueryTLexer.cmo mQueryTParser.cmi mathQL.cmo mQueryUtil.cmi -mQueryUtil.cmx: mQueryTLexer.cmx mQueryTParser.cmx mathQL.cmx mQueryUtil.cmi +mQueryMisc.cmo: mQueryMisc.cmi +mQueryMisc.cmx: mQueryMisc.cmi diff --git a/helm/ocaml/mathql/Makefile b/helm/ocaml/mathql/Makefile index 6d5481948..6554bf698 100644 --- a/helm/ocaml/mathql/Makefile +++ b/helm/ocaml/mathql/Makefile @@ -1,16 +1,13 @@ PACKAGE = mathql -REQUIRES = helm-urimanager +REQUIRES = helm-cic helm-cic_textual_parser PREDICATES = -INTERFACE_FILES = mQueryTParser.mli mQueryUtil.mli +INTERFACE_FILES = mQueryMisc.mli -IMPLEMENTATION_FILES = mathQL.ml mQueryTParser.ml mQueryTLexer.ml \ - mQueryUtil.ml +IMPLEMENTATION_FILES = mathQL.ml mQueryMisc.ml -EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi mQueryTLexer.cmi \ - mQueryTLexer.mll mQueryTParser.mly +EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi -EXTRA_OBJECTS_TO_CLEAN = mQueryTParser.ml mQueryTParser.mli \ - mQueryTLexer.ml +EXTRA_OBJECTS_TO_CLEAN = include ../Makefile.common diff --git a/helm/ocaml/mathql/mQueryMisc.ml b/helm/ocaml/mathql/mQueryMisc.ml new file mode 100644 index 000000000..0d8dcd5d9 --- /dev/null +++ b/helm/ocaml/mathql/mQueryMisc.ml @@ -0,0 +1,125 @@ +(* 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 *) +(* Ferruccio Guidi *) +(* 15/01/2003 *) +(* *) +(* *) +(****************************************************************************) + +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,[]) +;; + +(* conversion functions *****************************************************) + +type uriref = UriManager.uri * (int list) + +let string_of_uriref (uri, fi) = + let module UM = UriManager in + let str = UM.string_of_uri uri in + let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in + match fi with + | [] -> str + | [t] -> str ^ xp t ^ ")" + | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" diff --git a/helm/ocaml/mathql/mQueryMisc.mli b/helm/ocaml/mathql/mQueryMisc.mli new file mode 100644 index 000000000..6fb600dab --- /dev/null +++ b/helm/ocaml/mathql/mQueryMisc.mli @@ -0,0 +1,46 @@ +(* 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 *) +(* Ferruccio Guidi *) +(* 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 uriref = UriManager.uri * (int list) + +val string_of_uriref : uriref -> string diff --git a/helm/ocaml/mathql/mQueryTLexer.mll b/helm/ocaml/mathql/mQueryTLexer.mll deleted file mode 100644 index abccb4626..000000000 --- a/helm/ocaml/mathql/mQueryTLexer.mll +++ /dev/null @@ -1,132 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -{ - open MQueryTParser - - let debug = false - - let out s = if debug then prerr_endline s -} - -let SPC = [' ' '\t' '\n']+ -let ALPHA = ['A'-'Z' 'a'-'z' '_'] -let NUM = ['0'-'9'] -let IDEN = ALPHA (NUM | ALPHA)* -let QSTR = [^ '"' '\\']+ - -rule comm_token = parse - | "(*" { comm_token lexbuf; comm_token lexbuf } - | "*)" { () } - | ['*' '('] { 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 } -and query_token = parse - | "(*" { comm_token lexbuf; query_token lexbuf } - | SPC { query_token lexbuf } - | '"' { let str = qstr string_token lexbuf in - out ("STR " ^ str); STR str } - | '(' { out "LP"; LP } - | ')' { out "RP"; RP } - | '{' { out "LC"; LC } - | '}' { out "RC"; RC } - | '@' { out "AT"; AT } - | '%' { out "PC"; PC } - | '$' { out "DL"; DL } - | '.' { out "FS"; FS } - | ',' { out "CM"; CM } - | ';' { out "SC"; SC } - | '/' { out "SL"; SL } - | "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 } - | "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 } - | "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 } - | "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 } - | ',' { CM } - | ';' { SC } - | '=' { IS } - | "attr" { ATTR } - | eof { EOF } diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly deleted file mode 100644 index 313636c80..000000000 --- a/helm/ocaml/mathql/mQueryTParser.mly +++ /dev/null @@ -1,314 +0,0 @@ -/* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - */ - -/* AUTOR: Ferruccio Guidi - */ - -%{ - module M = MathQL - - let analyze x = - 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 :: 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.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.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_val x - - let f (x, y, z) = x - let s (x, y, z) = y - let t (x, y, z) = z -%} - %token ID STR - %token SL IS LC RC CM SC LP RP AT PC DL FS DQ EOF - %token ADD ALIGN AND AS ATTR BE BUT COUNT DIFF DISTR ELSE EMPTY EQ EX - %token FALSE FOR FROM IF IN INF INTER INV ISF IST KEEP LE LET LOG LT - %token MAIN MATCH MEET NOT OF OR PAT PROJ PROP SELECT SOURCE STAT SUB - %token SUBJ SUP SUPER THEN TRUE UNION WHERE XOR - %nonassoc IN SUP INF ELSE LOG STAT - %left DIFF - %left UNION - %left INTER - %nonassoc WHERE EX - %left XOR OR - %left AND - %nonassoc NOT - %nonassoc SUB MEET EQ LT LE - %nonassoc SUBJ OF PROJ COUNT ALIGN - - %start qstr query result - %type qstr - %type query - %type result -%% - qstr: - | DQ { "" } - | STR qstr { $1 ^ $2 } - ; - svar: - | PC ID { $2 } - ; - avar: - | AT ID { $2 } - ; - vvar: - | DL ID { $2 } - ; - strs: - | STR CM strs { $1 :: $3 } - | STR { [$1] } - ; - subpath: - | STR SL subpath { $1 :: $3 } - | STR { [$1] } - ; - path: - | subpath { $1 } - | SL subpath { $2 } - | SL { [] } - ; - paths: - | path CM paths { $1 :: $3 } - | path { [$1] } - inv: - | INV { true } - | { false } - ; - ref: - | 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 } - | { [] } - ; - isfalse: - | { [] } - | ISF conss isfalse { $2 :: $3 } - ; - 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: - | 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: - | 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 } - | set_exp error { $1 } - | EOF { raise End_of_file } - ; - attr: - | path IS strs { $1, $3 } - | path { $1, [] } - ; - attrs: - | attr SC attrs { $1 :: $3 } - | attr { [$1] } - ; - group: - LC attrs RC { $2 } - ; - groups: - | group CM groups { $1 :: $3 } - | group { [$1] } - ; - resource: - | STR ATTR groups { ($1, $3) } - | STR { ($1, []) } - ; - resources: - | resource SC resources { $1 :: $3 } - | resource { [$1] } - | { [] } - ; - result: - | resources { $1 } - | EOF { raise End_of_file } diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml deleted file mode 100644 index 349c2ac55..000000000 --- a/helm/ocaml/mathql/mQueryUtil.ml +++ /dev/null @@ -1,231 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* text linearization and parsing *******************************************) - -let rec txt_list out f s = function - | [] -> () - | [a] -> f a - | a :: tail -> f a; out s; txt_list out f s tail - -let txt_str out s = out ("\"" ^ s ^ "\"") - -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 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_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 " meet " - | 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.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 txt_attr = function - | (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; 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) - -(* operations on lists *****************************************************) - -type 'a comparison = Lt - | Gt - | Eq of 'a - -let list_join f l1 l2 = - let rec aux = function - | [], v - | v, [] -> v - | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin - match f h1 h2 with - | Lt -> h1 :: aux (t1, v2) - | Gt -> h2 :: aux (v1, t2) - | Eq h -> h :: aux (t1, t2) - end - in aux (l1, l2) - -let list_meet f l1 l2 = - let rec aux = function - | [], v - | v, [] -> [] - | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin - match f h1 h2 with - | Lt -> aux (t1, v2) - | Gt -> aux (v1, t2) - | Eq h -> h :: aux (t1, t2) - end - in aux (l1, l2) - -(* conversion functions *****************************************************) - -type uriref = UriManager.uri * (int list) - -let string_of_uriref (uri, fi) = - let module UM = UriManager in - let str = UM.string_of_uri uri in - let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in - match fi with - | [] -> str - | [t] -> str ^ xp t ^ ")" - | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" - diff --git a/helm/ocaml/mathql/mQueryUtil.mli b/helm/ocaml/mathql/mQueryUtil.mli deleted file mode 100644 index bb38dc91d..000000000 --- a/helm/ocaml/mathql/mQueryUtil.mli +++ /dev/null @@ -1,54 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -val text_of_query : (string -> unit) -> MathQL.query -> string -> unit - -val text_of_result : (string -> unit) -> MathQL.result -> string -> unit - -val query_of_text : Lexing.lexbuf -> MathQL.query - -val result_of_text : Lexing.lexbuf -> MathQL.result - -type time - -val start_time : unit -> time - -val stop_time : time -> string - -type 'a comparison = Lt - | Gt - | Eq of 'a - -val list_join : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list - -val list_meet : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list - - -type uriref = UriManager.uri * (int list) - -val string_of_uriref : uriref -> string diff --git a/helm/ocaml/mathql_generator/Makefile b/helm/ocaml/mathql_generator/Makefile index 3079a6643..a72f17ab2 100644 --- a/helm/ocaml/mathql_generator/Makefile +++ b/helm/ocaml/mathql_generator/Makefile @@ -1,7 +1,7 @@ PACKAGE = mathql_generator REQUIRES = helm-cic helm-cic_proof_checking helm-mathql - + PREDICATES = INTERFACE_FILES = mQGUtil.mli mQueryGenerator.mli \ diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.ml b/helm/ocaml/mathql_generator/cGLocateInductive.ml index 032060fd3..c5734f242 100644 --- a/helm/ocaml/mathql_generator/cGLocateInductive.ml +++ b/helm/ocaml/mathql_generator/cGLocateInductive.ml @@ -30,7 +30,7 @@ exception NotAnInductiveDefinition let get_constraints = function | Cic.MutInd (uri, t, _) -> - let uri = MQueryUtil.string_of_uriref (uri, [t]) in + let uri = MQueryMisc.string_of_uriref (uri, [t]) in let constr_obj = [(`InHypothesis, uri); (`MainHypothesis (Some 0), uri)] in diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml index 28639c8f7..bb87b461e 100644 --- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml +++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml @@ -43,7 +43,7 @@ let sort_entries entries = let levels_of_term metasenv context term = let module TC = CicTypeChecker in let module Red = CicReduction in - let module Util = MQueryUtil in + let module Misc = MQueryMisc in let degree t = let rec degree_aux = function | Cic.Sort _ -> 1 @@ -64,7 +64,7 @@ let levels_of_term metasenv context term = in let inspect_uri main l uri tc v term = let d = degree term in - entry_in (Util.string_of_uriref (uri, tc), main, 2 * v + d - 1) l + entry_in (Misc.string_of_uriref (uri, tc), main, 2 * v + d - 1) l in let rec inspect_term main l v term = match term with Cic.Rel _ -> l diff --git a/helm/ocaml/mathql_interpreter/.cvsignore b/helm/ocaml/mathql_interpreter/.cvsignore index 6b3eba302..cd9b591e3 100644 --- a/helm/ocaml/mathql_interpreter/.cvsignore +++ b/helm/ocaml/mathql_interpreter/.cvsignore @@ -1 +1 @@ -*.cm[iaox] *.cmxa +*.cm[iaox] *.cmxa mQueryTLexer.ml mQueryTParser.ml mQueryTParser.mli diff --git a/helm/ocaml/mathql_interpreter/.depend b/helm/ocaml/mathql_interpreter/.depend index 962eaf63a..7d9b3c625 100644 --- a/helm/ocaml/mathql_interpreter/.depend +++ b/helm/ocaml/mathql_interpreter/.depend @@ -1,21 +1,25 @@ mQIConn.cmi: mQIMap.cmi mQIProperty.cmi: mQIConn.cmi mQueryInterpreter.cmi: mQIConn.cmi -mQueryMisc.cmo: mQueryMisc.cmi -mQueryMisc.cmx: mQueryMisc.cmi +mQueryTParser.cmo: mQueryTParser.cmi +mQueryTParser.cmx: mQueryTParser.cmi +mQueryTLexer.cmo: mQueryTParser.cmi +mQueryTLexer.cmx: mQueryTParser.cmx +mQueryUtil.cmo: mQueryTLexer.cmo mQueryTParser.cmi mQueryUtil.cmi +mQueryUtil.cmx: mQueryTLexer.cmx mQueryTParser.cmx mQueryUtil.cmi mQIUtil.cmo: mQIUtil.cmi mQIUtil.cmx: mQIUtil.cmi mQIPostgres.cmo: mQIPostgres.cmi mQIPostgres.cmx: mQIPostgres.cmi -mQIMap.cmo: mQIMap.cmi -mQIMap.cmx: mQIMap.cmi +mQIMap.cmo: mQueryUtil.cmi mQIMap.cmi +mQIMap.cmx: mQueryUtil.cmx mQIMap.cmi mQIConn.cmo: mQIMap.cmi mQIPostgres.cmi mQIConn.cmi mQIConn.cmx: mQIMap.cmx mQIPostgres.cmx mQIConn.cmi mQIProperty.cmo: mQIConn.cmi mQIMap.cmi mQIPostgres.cmi mQIUtil.cmi \ mQIProperty.cmi mQIProperty.cmx: mQIConn.cmx mQIMap.cmx mQIPostgres.cmx mQIUtil.cmx \ mQIProperty.cmi -mQueryInterpreter.cmo: mQIConn.cmi mQIProperty.cmi mQIUtil.cmi \ +mQueryInterpreter.cmo: mQIConn.cmi mQIProperty.cmi mQIUtil.cmi mQueryUtil.cmi \ mQueryInterpreter.cmi -mQueryInterpreter.cmx: mQIConn.cmx mQIProperty.cmx mQIUtil.cmx \ +mQueryInterpreter.cmx: mQIConn.cmx mQIProperty.cmx mQIUtil.cmx mQueryUtil.cmx \ mQueryInterpreter.cmi diff --git a/helm/ocaml/mathql_interpreter/Makefile b/helm/ocaml/mathql_interpreter/Makefile index be32ff48c..88c66ac8e 100644 --- a/helm/ocaml/mathql_interpreter/Makefile +++ b/helm/ocaml/mathql_interpreter/Makefile @@ -1,17 +1,20 @@ PACKAGE = mathql_interpreter -REQUIRES = helm-cic helm-cic_textual_parser helm-mathql postgres +REQUIRES = helm-urimanager helm-mathql postgres #natile-galax PREDICATES = -INTERFACE_FILES = mQueryMisc.mli mQIUtil.mli \ +INTERFACE_FILES = mQueryUtil.mli mQIUtil.mli \ mQIPostgres.mli mQIMap.mli mQIConn.mli \ - mQIProperty.mli mQueryInterpreter.mli + mQIProperty.mli mQueryInterpreter.mli -IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +IMPLEMENTATION_FILES = mQueryTParser.ml mQueryTLexer.ml \ + $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_INSTALL = mQueryTLexer.cmi \ + mQueryTLexer.mll mQueryTParser.mly -EXTRA_OBJECTS_TO_CLEAN = +EXTRA_OBJECTS_TO_CLEAN = mQueryTParser.ml mQueryTParser.mli \ + mQueryTLexer.ml include ../Makefile.common diff --git a/helm/ocaml/mathql_interpreter/mQueryMisc.ml b/helm/ocaml/mathql_interpreter/mQueryMisc.ml deleted file mode 100644 index cb6f92a21..000000000 --- a/helm/ocaml/mathql_interpreter/mQueryMisc.ml +++ /dev/null @@ -1,111 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 15/01/2003 *) -(* *) -(* *) -(******************************************************************************) - -exception IllFormedUri of string;; - -let string_of_cic_textual_parser_uri uri = - let module C = Cic in - let module CTP = CicTextualParser0 in - let uri' = - match uri with - CTP.ConUri uri -> UriManager.string_of_uri uri - | CTP.VarUri uri -> UriManager.string_of_uri uri - | CTP.IndTyUri (uri,tyno) -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) - | CTP.IndConUri (uri,tyno,consno) -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^ - string_of_int consno - in - (* 4 = String.length "cic:" *) - String.sub uri' 4 (String.length uri' - 4) -;; - -let cic_textual_parser_uri_of_string uri' = - prerr_endline ("cic_textual_parser_uri_of_string INPUT = " ^ uri'); - try - (* Constant *) - if String.sub uri' (String.length uri' - 4) 4 = ".con" then - CicTextualParser0.ConUri (UriManager.uri_of_string uri') - else - if String.sub uri' (String.length uri' - 4) 4 = ".var" then - CicTextualParser0.VarUri (UriManager.uri_of_string uri') - else - (try - (* Inductive Type *) - let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in - CicTextualParser0.IndTyUri (uri'',typeno) - with - UriManager.IllFormedUri _ - | CicTextualParser0.LexerFailure _ - | Invalid_argument _ -> - (* Constructor of an Inductive Type *) - let uri'',typeno,consno = - CicTextualLexer.indconuri_of_uri uri' - in - CicTextualParser0.IndConUri (uri'',typeno,consno) - ) - with - UriManager.IllFormedUri _ - | CicTextualParser0.LexerFailure _ - | Invalid_argument _ -> - raise (IllFormedUri uri') -;; -let cic_textual_parser_uri_of_string uri' = - let res = cic_textual_parser_uri_of_string uri' in - prerr_endline ("RESULT: " ^ (string_of_cic_textual_parser_uri res)); - res - -(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *) -let wrong_xpointer_format_from_wrong_xpointer_format' uri = - try - let index_sharp = String.index uri '#' in - let index_rest = index_sharp + 10 in - let baseuri = String.sub uri 0 index_sharp in - let rest = - String.sub uri index_rest (String.length uri - index_rest - 1) - in - baseuri ^ "#" ^ rest - with Not_found -> uri -;; - -let term_of_cic_textual_parser_uri uri = - let module C = Cic in - let module CTP = CicTextualParser0 in - match uri with - CTP.ConUri uri -> C.Const (uri,[]) - | CTP.VarUri uri -> C.Var (uri,[]) - | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[]) - | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) -;; diff --git a/helm/ocaml/mathql_interpreter/mQueryMisc.mli b/helm/ocaml/mathql_interpreter/mQueryMisc.mli deleted file mode 100644 index 7c0aa7468..000000000 --- a/helm/ocaml/mathql_interpreter/mQueryMisc.mli +++ /dev/null @@ -1,41 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 15/01/2003 *) -(* *) -(* *) -(******************************************************************************) - -exception IllFormedUri of string - -val string_of_cic_textual_parser_uri : CicTextualParser0.uri -> string -val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri -val term_of_cic_textual_parser_uri: CicTextualParser0.uri -> Cic.term -val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string diff --git a/helm/ocaml/mathql_interpreter/mQueryTLexer.mll b/helm/ocaml/mathql_interpreter/mQueryTLexer.mll new file mode 100644 index 000000000..abccb4626 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQueryTLexer.mll @@ -0,0 +1,132 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +{ + open MQueryTParser + + let debug = false + + let out s = if debug then prerr_endline s +} + +let SPC = [' ' '\t' '\n']+ +let ALPHA = ['A'-'Z' 'a'-'z' '_'] +let NUM = ['0'-'9'] +let IDEN = ALPHA (NUM | ALPHA)* +let QSTR = [^ '"' '\\']+ + +rule comm_token = parse + | "(*" { comm_token lexbuf; comm_token lexbuf } + | "*)" { () } + | ['*' '('] { 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 } +and query_token = parse + | "(*" { comm_token lexbuf; query_token lexbuf } + | SPC { query_token lexbuf } + | '"' { let str = qstr string_token lexbuf in + out ("STR " ^ str); STR str } + | '(' { out "LP"; LP } + | ')' { out "RP"; RP } + | '{' { out "LC"; LC } + | '}' { out "RC"; RC } + | '@' { out "AT"; AT } + | '%' { out "PC"; PC } + | '$' { out "DL"; DL } + | '.' { out "FS"; FS } + | ',' { out "CM"; CM } + | ';' { out "SC"; SC } + | '/' { out "SL"; SL } + | "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 } + | "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 } + | "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 } + | "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 } + | ',' { CM } + | ';' { SC } + | '=' { IS } + | "attr" { ATTR } + | eof { EOF } diff --git a/helm/ocaml/mathql_interpreter/mQueryTParser.mly b/helm/ocaml/mathql_interpreter/mQueryTParser.mly new file mode 100644 index 000000000..313636c80 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQueryTParser.mly @@ -0,0 +1,314 @@ +/* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + */ + +/* AUTOR: Ferruccio Guidi + */ + +%{ + module M = MathQL + + let analyze x = + 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 :: 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.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.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_val x + + let f (x, y, z) = x + let s (x, y, z) = y + let t (x, y, z) = z +%} + %token ID STR + %token SL IS LC RC CM SC LP RP AT PC DL FS DQ EOF + %token ADD ALIGN AND AS ATTR BE BUT COUNT DIFF DISTR ELSE EMPTY EQ EX + %token FALSE FOR FROM IF IN INF INTER INV ISF IST KEEP LE LET LOG LT + %token MAIN MATCH MEET NOT OF OR PAT PROJ PROP SELECT SOURCE STAT SUB + %token SUBJ SUP SUPER THEN TRUE UNION WHERE XOR + %nonassoc IN SUP INF ELSE LOG STAT + %left DIFF + %left UNION + %left INTER + %nonassoc WHERE EX + %left XOR OR + %left AND + %nonassoc NOT + %nonassoc SUB MEET EQ LT LE + %nonassoc SUBJ OF PROJ COUNT ALIGN + + %start qstr query result + %type qstr + %type query + %type result +%% + qstr: + | DQ { "" } + | STR qstr { $1 ^ $2 } + ; + svar: + | PC ID { $2 } + ; + avar: + | AT ID { $2 } + ; + vvar: + | DL ID { $2 } + ; + strs: + | STR CM strs { $1 :: $3 } + | STR { [$1] } + ; + subpath: + | STR SL subpath { $1 :: $3 } + | STR { [$1] } + ; + path: + | subpath { $1 } + | SL subpath { $2 } + | SL { [] } + ; + paths: + | path CM paths { $1 :: $3 } + | path { [$1] } + inv: + | INV { true } + | { false } + ; + ref: + | 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 } + | { [] } + ; + isfalse: + | { [] } + | ISF conss isfalse { $2 :: $3 } + ; + 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: + | 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: + | 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 } + | set_exp error { $1 } + | EOF { raise End_of_file } + ; + attr: + | path IS strs { $1, $3 } + | path { $1, [] } + ; + attrs: + | attr SC attrs { $1 :: $3 } + | attr { [$1] } + ; + group: + LC attrs RC { $2 } + ; + groups: + | group CM groups { $1 :: $3 } + | group { [$1] } + ; + resource: + | STR ATTR groups { ($1, $3) } + | STR { ($1, []) } + ; + resources: + | resource SC resources { $1 :: $3 } + | resource { [$1] } + | { [] } + ; + result: + | resources { $1 } + | EOF { raise End_of_file } diff --git a/helm/ocaml/mathql_interpreter/mQueryUtil.ml b/helm/ocaml/mathql_interpreter/mQueryUtil.ml new file mode 100644 index 000000000..30e6688ee --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQueryUtil.ml @@ -0,0 +1,218 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +(* text linearization and parsing *******************************************) + +let rec txt_list out f s = function + | [] -> () + | [a] -> f a + | a :: tail -> f a; out s; txt_list out f s tail + +let txt_str out s = out ("\"" ^ s ^ "\"") + +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 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_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 " meet " + | 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.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 txt_attr = function + | (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; 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) + +(* operations on lists *****************************************************) + +type 'a comparison = Lt + | Gt + | Eq of 'a + +let list_join f l1 l2 = + let rec aux = function + | [], v + | v, [] -> v + | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin + match f h1 h2 with + | Lt -> h1 :: aux (t1, v2) + | Gt -> h2 :: aux (v1, t2) + | Eq h -> h :: aux (t1, t2) + end + in aux (l1, l2) + +let list_meet f l1 l2 = + let rec aux = function + | [], v + | v, [] -> [] + | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin + match f h1 h2 with + | Lt -> aux (t1, v2) + | Gt -> aux (v1, t2) + | Eq h -> h :: aux (t1, t2) + end + in aux (l1, l2) + diff --git a/helm/ocaml/mathql_interpreter/mQueryUtil.mli b/helm/ocaml/mathql_interpreter/mQueryUtil.mli new file mode 100644 index 000000000..2a3c80b83 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQueryUtil.mli @@ -0,0 +1,49 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +val text_of_query : (string -> unit) -> MathQL.query -> string -> unit + +val text_of_result : (string -> unit) -> MathQL.result -> string -> unit + +val query_of_text : Lexing.lexbuf -> MathQL.query + +val result_of_text : Lexing.lexbuf -> MathQL.result + +type time + +val start_time : unit -> time + +val stop_time : time -> string + +type 'a comparison = Lt + | Gt + | Eq of 'a + +val list_join : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list + +val list_meet : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list