From: Stefano Zacchiroli Date: Tue, 17 May 2005 15:34:42 +0000 (+0000) Subject: first check-in of cic_notation X-Git-Tag: single_binding~46 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=879797d6505bc39489009d9ae1e2506022bde9e2;p=helm.git first check-in of cic_notation --- diff --git a/helm/ocaml/METAS/meta.helm-cic_notation.src b/helm/ocaml/METAS/meta.helm-cic_notation.src new file mode 100644 index 000000000..255652e61 --- /dev/null +++ b/helm/ocaml/METAS/meta.helm-cic_notation.src @@ -0,0 +1,4 @@ +requires="helm-utf8_macros camlp4.gramlib" +version="0.0.1" +archive(byte)="cic_notation.cma" +archive(native)="cic_notation.cmxa" diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index e1cba430e..af199d3b5 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -16,6 +16,7 @@ MODULES = \ cic_omdoc \ metadata \ tactics \ + cic_notation \ cic_transformations \ cic_textual_parser2 \ mathql \ diff --git a/helm/ocaml/cic_notation/.cvsignore b/helm/ocaml/cic_notation/.cvsignore new file mode 100644 index 000000000..6aa2e0cb9 --- /dev/null +++ b/helm/ocaml/cic_notation/.cvsignore @@ -0,0 +1,5 @@ +*.cm[aiox] +*.cmxa +*.[ao] +test_lexer +test_parser diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend new file mode 100644 index 000000000..e0012b1af --- /dev/null +++ b/helm/ocaml/cic_notation/.depend @@ -0,0 +1,4 @@ +cicNotationLexer.cmo: cicNotationLexer.cmi +cicNotationLexer.cmx: cicNotationLexer.cmi +cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi +cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile new file mode 100644 index 000000000..6b4d13c26 --- /dev/null +++ b/helm/ocaml/cic_notation/Makefile @@ -0,0 +1,55 @@ + +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 $< + diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml new file mode 100644 index 000000000..6ff589384 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationLexer.ml @@ -0,0 +1,118 @@ +(* 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 + diff --git a/helm/ocaml/cic_notation/cicNotationLexer.mli b/helm/ocaml/cic_notation/cicNotationLexer.mli new file mode 100644 index 000000000..61632667e --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationLexer.mli @@ -0,0 +1,33 @@ +(* 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 + diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml new file mode 100644 index 000000000..2b5598c42 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -0,0 +1,115 @@ +(* 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: *) diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli new file mode 100644 index 000000000..84ce24b14 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -0,0 +1,42 @@ +(* 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*) + diff --git a/helm/ocaml/cic_notation/test_lexer.ml b/helm/ocaml/cic_notation/test_lexer.ml new file mode 100644 index 000000000..7672d3070 --- /dev/null +++ b/helm/ocaml/cic_notation/test_lexer.ml @@ -0,0 +1,42 @@ +(* 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 -> () diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml new file mode 100644 index 000000000..21315c77f --- /dev/null +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -0,0 +1,49 @@ +(* 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%s%s\n" before error after;*) +(* prerr_endline (sprintf "at character %d-%d: %s" x y msg)*) + done + with End_of_file -> + close_in ic +