--- /dev/null
+requires="helm-utf8_macros camlp4.gramlib"
+version="0.0.1"
+archive(byte)="cic_notation.cma"
+archive(native)="cic_notation.cmxa"
cic_omdoc \
metadata \
tactics \
+ cic_notation \
cic_transformations \
cic_textual_parser2 \
mathql \
--- /dev/null
+*.cm[aiox]
+*.cmxa
+*.[ao]
+test_lexer
+test_parser
--- /dev/null
+cicNotationLexer.cmo: cicNotationLexer.cmi
+cicNotationLexer.cmx: cicNotationLexer.cmi
+cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi
+cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi
--- /dev/null
+
+PACKAGE = cic_notation
+REQUIRES = \
+ helm-utf8_macros \
+ ulex
+NOTATIONS =
+NULL =
+INTERFACE_FILES = \
+ cicNotationLexer.mli \
+ cicNotationParser.mli \
+ $(NULL)
+IMPLEMENTATION_FILES = \
+ $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \
+ $(patsubst %,%_notation.ml,$(NOTATIONS)) \
+ $(NULL)
+
+all:
+
+cicNotationLexer.cmo: cicNotationLexer.ml
+ $(OCAMLC_P4) -c $<
+cicNotationLexer.cmx: cicNotationLexer.ml
+ $(OCAMLOPT_P4) -c $<
+cicNotationParser.cmo: cicNotationParser.ml
+ $(OCAMLC_P4) -c $<
+cicNotationParser.cmx: cicNotationParser.ml
+ $(OCAMLOPT_P4) -c $<
+
+%_notation.cmo: %_notation.ml
+ $(OCAMLC_P4) -c $<
+%_notation.cmx: %_notation.ml
+ $(OCAMLOPT_P4) -c $<
+
+LOCAL_LINKOPTS = -package helm-cic_notation -linkpkg
+test: test_lexer test_parser
+test_lexer: test_lexer.ml $(PACKAGE).cma
+ $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
+test_parser: test_parser.ml $(PACKAGE).cma
+ $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
+
+clean: extra_clean
+distclean: extra_clean
+ rm -f macro_table.dump
+extra_clean:
+ rm -f test_lexer test_parser
+
+include ../Makefile.common
+OCAMLARCHIVEOPTIONS += -linkall
+
+disambiguateTypes.cmi: disambiguateTypes.mli
+ $(OCAMLC) -c -rectypes $<
+disambiguateTypes.cmo: disambiguateTypes.ml disambiguateTypes.cmi
+ $(OCAMLC) -c -rectypes $<
+disambiguateTypes.cmx: disambiguateTypes.ml disambiguateTypes.cmi
+ $(OCAMLOPT) -c -rectypes $<
+
--- /dev/null
+(* Copyright (C) 2005, 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://helm.cs.unibo.it/
+ *)
+
+exception Error of int * int * string
+
+exception Not_an_extended_ident
+
+let regexp number = xml_digit+
+
+let regexp ident_decoration = '\'' | '!' | '?' | '`'
+let regexp ident_cont = xml_letter | xml_digit | '_'
+let regexp ident = xml_letter ident_cont* ident_decoration*
+
+let regexp tex_token = '\\' ident
+
+let regexp keyword = '"' ident '"'
+
+let regexp implicit = '?'
+let regexp meta = implicit number
+
+let error lexbuf msg =
+ raise (Error (Ulexing.lexeme_start lexbuf, Ulexing.lexeme_end lexbuf, msg))
+let error_at_end lexbuf msg =
+ raise (Error (Ulexing.lexeme_end lexbuf, Ulexing.lexeme_end lexbuf, msg))
+
+let return lexbuf token =
+ let flocation_begin =
+ { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
+ Lexing.pos_cnum = Ulexing.lexeme_start lexbuf }
+ in
+ let flocation_end =
+ { flocation_begin with Lexing.pos_cnum = Ulexing.lexeme_end lexbuf }
+ in
+ (token, (flocation_begin, flocation_end))
+
+let remove_quotes s = String.sub s 1 (String.length s - 2)
+
+let tok_func token stream =
+ let lexbuf = Ulexing.from_utf8_stream stream in
+ Token.make_stream_and_flocation
+ (fun () ->
+ try
+ token lexbuf
+ with
+ | Ulexing.Error -> error_at_end lexbuf "Unexpected character"
+ | Ulexing.InvalidCodepoint i -> error_at_end lexbuf "Invalid code point")
+
+let mk_lexer token = {
+ Token.tok_func = token;
+ Token.tok_using = (fun _ -> ());
+ Token.tok_removing = (fun _ -> ());
+ Token.tok_match = Token.default_match;
+ Token.tok_text = Token.lexer_text;
+ Token.tok_comm = None;
+}
+
+let expand_macro lexbuf =
+ let macro =
+ Ulexing.utf8_sub_lexeme lexbuf 1 (Ulexing.lexeme_length lexbuf - 1)
+ in
+ try
+ ("SYMBOL", Utf8Macro.expand macro)
+ with Utf8Macro.Macro_not_found _ -> "SYMBOL", Ulexing.utf8_lexeme lexbuf
+
+let keyword lexbuf = "KEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf)
+
+(** {2 Level 1 lexer} *)
+
+let rec level1_token = lexer
+ | xml_blank+ -> level1_token lexbuf
+ | ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
+ | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
+ | keyword -> return lexbuf (keyword lexbuf)
+ | tex_token -> return lexbuf (expand_macro lexbuf)
+ | eof -> return lexbuf ("EOI", "")
+ | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
+
+let level1_tok_func stream = tok_func level1_token stream
+let level1_lexer = mk_lexer level1_tok_func
+
+(** {2 Level 2 lexer} *)
+
+let rec level2_token = lexer
+ | xml_blank+ -> level1_token lexbuf
+ | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf)
+ | implicit -> return lexbuf ("IMPLICIT", Ulexing.utf8_lexeme lexbuf)
+ | ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
+ | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
+ | keyword -> return lexbuf (keyword lexbuf)
+ | tex_token -> return lexbuf (expand_macro lexbuf)
+ | eof -> return lexbuf ("EOI", "")
+ | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
+
+let level2_tok_func stream = tok_func level2_token stream
+let level2_lexer = mk_lexer level2_tok_func
+
--- /dev/null
+(* Copyright (C) 2005, 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://helm.cs.unibo.it/
+ *)
+
+exception Error of int * int * string
+
+ (** lexer for concrete syntax patterns (notation level 1) *)
+val level1_lexer: (string * string) Token.glexer
+
+ (** lexer for ast patterns (notation level 2) *)
+val level2_lexer: (string * string) Token.glexer
+
--- /dev/null
+(* Copyright (C) 2005, 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://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+exception Parse_error of Token.flocation * string
+
+let grammar = Grammar.gcreate CicNotationLexer.level1_lexer
+
+let level1 = Grammar.Entry.create grammar "level1"
+
+let return_term loc term = ()
+
+(*let fail floc msg =*)
+(* let (x, y) = CicAst.loc_of_floc floc in*)
+(* failwith (sprintf "Error at characters %d - %d: %s" x y msg)*)
+
+let int_of_string s =
+ try
+ Pervasives.int_of_string s
+ with Failure _ ->
+ failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
+
+EXTEND
+ GLOBAL: level1;
+
+ level1: [ [ p = pattern -> () ] ];
+
+ pattern: [ [ p = LIST1 simple_pattern -> () ] ];
+
+ literal: [
+ [ s = SYMBOL -> ()
+ | k = KEYWORD -> ()
+ ]
+ ];
+
+ sep: [ [ SYMBOL "\\SEP"; sep = literal -> () ] ];
+ row_sep: [ [ SYMBOL "\\ROWSEP"; sep = literal -> () ] ];
+ field_sep: [ [ SYMBOL "\\FIELDSEP"; sep = literal -> () ] ];
+
+ box_token: [
+ [ SYMBOL "\\HBOX"; p = simple_pattern -> ()
+ | SYMBOL "\\VBOX"; p = simple_pattern -> ()
+ | SYMBOL "\\BREAK" -> ()
+ ]
+ ];
+
+ layout_schemata: [
+ [ SYMBOL "\\ARRAY"; p = simple_pattern; fsep = OPT field_sep;
+ rsep = OPT row_sep ->
+ ()
+ | SYMBOL "\\FRAC"; p1 = simple_pattern; p2 = simple_pattern -> ()
+ | SYMBOL "\\SQRT"; p = simple_pattern -> ()
+ | SYMBOL "\\ROOT"; p1 = simple_pattern; SYMBOL "\\OF";
+ p2 = simple_pattern ->
+ ()
+ (* TODO XXX many issues here:
+ * - "^^" is lexed as two "^" symbols
+ * - "a_b" is lexed as IDENT "a_b" *)
+ | p1 = simple_pattern; SYMBOL "^"; p2 = simple_pattern -> ()
+ | p1 = simple_pattern; SYMBOL "^"; SYMBOL "^"; p2 = simple_pattern -> ()
+ | p1 = simple_pattern; SYMBOL "_"; p2 = simple_pattern -> ()
+ | p1 = simple_pattern; SYMBOL "_"; SYMBOL "_"; p2 = simple_pattern -> ()
+ ]
+ ];
+
+ simple_pattern: [
+ [ SYMBOL "\\LIST0"; p = simple_pattern; sep = OPT sep -> ()
+ | SYMBOL "\\LIST1"; p = simple_pattern; sep = OPT sep -> ()
+ | b = box_token -> ()
+ | id = IDENT -> ()
+ | SYMBOL "\\NUM"; id = IDENT -> ()
+ | SYMBOL "\\IDENT"; id = IDENT -> ()
+ | SYMBOL "\\OPT"; p = simple_pattern -> ()
+ | l = layout_schemata -> ()
+ | SYMBOL "["; p = pattern; SYMBOL "]" -> ()
+ ]
+ ];
+END
+
+let exc_located_wrapper f =
+ try
+ f ()
+ with
+ | Stdpp.Exc_located (floc, Stream.Error msg) ->
+ raise (Parse_error (floc, msg))
+ | Stdpp.Exc_located (floc, exn) ->
+ raise (Parse_error (floc, (Printexc.to_string exn)))
+
+let parse_level1_pattern stream =
+ exc_located_wrapper (fun () -> (Grammar.Entry.parse level1 stream))
+
+(* vim:set encoding=utf8: *)
--- /dev/null
+(* Copyright (C) 2005, 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://helm.cs.unibo.it/
+ *)
+
+exception Parse_error of Token.flocation * string
+
+(** {2 Parsing functions} *)
+
+val parse_level1_pattern: char Stream.t -> unit
+(*val parse_level2_pattern: char Stream.t -> unit*)
+
+(** {2 Grammar extensions} *)
+
+(*val term: CicAst.term Grammar.Entry.e |+* recursive rule +|*)
+(*val term0: CicAst.term Grammar.Entry.e |+* top level rule +|*)
+
+(*val return_term: CicAst.location -> CicAst.term -> CicAst.term*)
+
+ (** raise a parse error *)
+(*val fail: CicAst.location -> string -> 'a*)
+
--- /dev/null
+(* Copyright (C) 2005, 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://helm.cs.unibo.it/
+ *)
+
+let ic =
+ try
+ open_in Sys.argv.(1)
+ with Invalid_argument _ -> stdin
+in
+let token_stream =
+ fst (CicNotationLexer.level1_lexer.Token.tok_func (Stream.of_channel ic))
+in
+let rec dump () =
+ let (a,b) = Stream.next token_stream in
+ if a = "EOI" then raise Stream.Failure;
+ print_endline (Printf.sprintf "%s '%s'" a b);
+ dump ()
+in
+try
+ dump ()
+with Stream.Failure -> ()
--- /dev/null
+(* Copyright (C) 2005, 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://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+let _ =
+ let ic = stdin in
+ try
+ while true do
+ let line = input_line ic in
+ let istream = Stream.of_string line in
+ try
+ let _ = CicNotationParser.parse_level1_pattern istream in
+ print_endline "ok"
+ with
+ | CicNotationParser.Parse_error (floc, msg) ->
+ eprintf "parse error: %s\n" msg; flush stderr
+(* let (x, y) = CicAst.loc_of_floc floc in*)
+(* let before = String.sub line 0 x in*)
+(* let error = String.sub line x (y - x) in*)
+(* let after = String.sub line y (String.length line - y) in*)
+(* eprintf "%s\e[01;31m%s\e[00m%s\n" before error after;*)
+(* prerr_endline (sprintf "at character %d-%d: %s" x y msg)*)
+ done
+ with End_of_file ->
+ close_in ic
+
projects / helm.git / commitdiff