This feature, announced in my Ph.D. thesis, will allow the interpreter to interact with the generator.
# 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@
-*.cm[iaox] *.cmxa mQueryTLexer.ml mQueryTParser.ml mQueryTParser.mli
+*.cm[iaox] *.cmxa
-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
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
--- /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> *)
+(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
+(* 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 ^ ")"
--- /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> *)
+(* Ferruccio Guidi <fguidi@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 uriref = UriManager.uri * (int list)
+
+val string_of_uriref : uriref -> 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/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-{
- 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 }
+++ /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/.
- */
-
-/* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- */
-
-%{
- 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 <string> 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 <string> qstr
- %type <MathQL.query> query
- %type <MathQL.result> 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 }
+++ /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/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-(* 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 ^ ")"
-
+++ /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/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-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
PACKAGE = mathql_generator
REQUIRES = helm-cic helm-cic_proof_checking helm-mathql
-
+
PREDICATES =
INTERFACE_FILES = mQGUtil.mli mQueryGenerator.mli \
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
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
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
-*.cm[iaox] *.cmxa
+*.cm[iaox] *.cmxa mQueryTLexer.ml mQueryTParser.ml mQueryTParser.mli
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
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
+++ /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;;
-
-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/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+{
+ 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 }
--- /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/.
+ */
+
+/* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ */
+
+%{
+ 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 <string> 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 <string> qstr
+ %type <MathQL.query> query
+ %type <MathQL.result> 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 }
--- /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/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* 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)
+
--- /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/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+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
projects / helm.git / commitdiff