X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationLexer.ml;h=01ef6142c8de0c45603a341129804e98074ee78d;hb=ba2dfe6409e95bf9e558dc0d4be382b068671409;hp=3c262ceec1854c27a502b9c56f1d8853a04bd430;hpb=dbcc29c0e46454c7e31b485135900ceab38627e1;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml index 3c262ceec..01ef6142c 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.ml +++ b/helm/ocaml/cic_notation/cicNotationLexer.ml @@ -39,12 +39,59 @@ let regexp delim_begin = "\\[" let regexp delim_end = "\\]" let regexp keyword = '"' ident '"' +let regexp qkeyword = "'" ident "'" let regexp implicit = '?' let regexp meta = implicit number let regexp csymbol = '\'' ident +let regexp begin_group = "@{" | "${" +let regexp end_group = '}' +let regexp wildcard = "$_" +let regexp ast_ident = "@" ident +let regexp ast_csymbol = "@" csymbol +let regexp meta_ident = "$" ident +let regexp meta_anonymous = "$_" +let regexp qstring = '"' [^ '"']* '"' + +let level1_layouts = + [ "sub"; "sup"; + "below"; "above"; + "over"; "atop"; "frac"; + "sqrt"; "root" + ] + +let level1_keywords = + [ "hbox"; "hvbox"; "hovbox"; "vbox"; + "break"; + "list0"; "list1"; "sep"; + "opt"; + "term"; "ident"; "number" + ] @ level1_layouts + +let level2_meta_keywords = + [ "if"; "then"; "else"; + "fold"; "left"; "right"; "rec"; + "fail"; + "default"; + "anonymous"; "ident"; "number"; "term"; "fresh" + ] + + (* (string, unit) Hashtbl.t, to exploit multiple bindings *) +let level2_ast_keywords = Hashtbl.create 23 +let _ = + (* TODO ZACK: keyword list almost cut and paste from cicTextualLexer2.ml, to + * be reviewed *) + List.iter (fun k -> Hashtbl.add level2_ast_keywords k ()) + [ "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "match"; "with"; "in"; + "and"; "on" ] + +let add_level2_ast_keyword k = + prerr_endline ("Adding keyword " ^ k); + Hashtbl.add level2_ast_keywords k () +let remove_level2_ast_keyword k = Hashtbl.remove level2_ast_keywords k + let regexp uri = ("cic:/" | "theory:/") (* schema *) ident ('/' ident)* (* path *) @@ -58,8 +105,7 @@ let error_at_end lexbuf msg = let begin_cnum, end_cnum = Ulexing.loc lexbuf in raise (Error (begin_cnum, end_cnum, msg)) -let return lexbuf token = - let begin_cnum, end_cnum = Ulexing.loc lexbuf in +let return_with_loc token begin_cnum end_cnum = (* TODO handle line/column numbers *) let flocation_begin = { Lexing.pos_fname = ""; @@ -69,6 +115,10 @@ let return lexbuf token = let flocation_end = { flocation_begin with Lexing.pos_cnum = end_cnum } in (token, (flocation_begin, flocation_end)) +let return lexbuf token = + let begin_cnum, end_cnum = Ulexing.loc lexbuf in + return_with_loc token begin_cnum end_cnum + let return_lexeme lexbuf name = return lexbuf (name, Ulexing.utf8_lexeme lexbuf) let remove_quotes s = String.sub s 1 (String.length s - 2) @@ -104,22 +154,97 @@ let expand_macro lexbuf = let keyword lexbuf = "KEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf) -let rec token = lexer - | xml_blank+ -> token lexbuf +let remove_quotes s = String.sub s 1 (String.length s - 2) +let remove_left_quote s = String.sub s 1 (String.length s - 1) + +let rec level2_pattern_token_group counter buffer = lexer + | end_group -> + if (counter > 0) then + Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ; + snd (Ulexing.loc lexbuf) + | begin_group -> + Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ; + ignore (level2_pattern_token_group (counter + 1) buffer lexbuf) ; + level2_pattern_token_group counter buffer lexbuf + | _ -> + Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ; + level2_pattern_token_group counter buffer lexbuf + +let read_unparsed_group token_name lexbuf = + let buffer = Buffer.create 16 in + let begin_cnum, _ = Ulexing.loc lexbuf in + let end_cnum = level2_pattern_token_group 0 buffer lexbuf in + return_with_loc (token_name, Buffer.contents buffer) begin_cnum end_cnum + +let rec level2_meta_token = lexer + | xml_blank+ -> level2_meta_token lexbuf + | ident -> + let s = Ulexing.utf8_lexeme lexbuf in + begin + if List.mem s level2_meta_keywords then + return lexbuf ("", s) + else + return lexbuf ("IDENT", s) + end + | "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf + | ast_ident -> + return lexbuf ("UNPARSED_AST", + remove_left_quote (Ulexing.utf8_lexeme lexbuf)) + | ast_csymbol -> + return lexbuf ("UNPARSED_AST", + remove_left_quote (Ulexing.utf8_lexeme lexbuf)) + | eof -> return lexbuf ("EOI", "") + +let rec level2_ast_token = lexer + | xml_blank+ -> level2_ast_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) + | ident -> + let lexeme = Ulexing.utf8_lexeme lexbuf in + if Hashtbl.mem level2_ast_keywords lexeme then + return lexbuf ("", lexeme) + else + return lexbuf ("IDENT", lexeme) | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf) | keyword -> return lexbuf (keyword lexbuf) - | delim_begin -> return lexbuf ("DELIM", Ulexing.utf8_lexeme lexbuf) - | delim_end -> return lexbuf ("DELIM", Ulexing.utf8_lexeme lexbuf) | tex_token -> return lexbuf (expand_macro lexbuf) | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf) - | eof -> return lexbuf ("EOI", "") + | qstring -> + return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf)) | csymbol -> return lexbuf ("CSYMBOL", Ulexing.utf8_lexeme lexbuf) + | "${" -> read_unparsed_group "UNPARSED_META" lexbuf + | "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf + | '(' -> return lexbuf ("LPAREN", "") + | ')' -> return lexbuf ("RPAREN", "") + | meta_ident -> + return lexbuf ("UNPARSED_META", + remove_left_quote (Ulexing.utf8_lexeme lexbuf)) + | meta_anonymous -> return lexbuf ("UNPARSED_META", "anonymous") + | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf) + | eof -> return lexbuf ("EOI", "") + +let rec level1_pattern_token = lexer + | xml_blank+ -> level1_pattern_token lexbuf + | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf) + | ident -> + let s = Ulexing.utf8_lexeme lexbuf in + begin + if List.mem s level1_keywords then + return lexbuf ("", s) + else + return lexbuf ("IDENT", s) + end + | tex_token -> return lexbuf (expand_macro lexbuf) + | qkeyword -> + return lexbuf ("QKEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf)) + | '(' -> return lexbuf ("LPAREN", "") + | ')' -> return lexbuf ("RPAREN", "") + | eof -> return lexbuf ("EOI", "") | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf) (* API implementation *) -let notation_lexer = mk_lexer token +let level1_pattern_lexer = mk_lexer level1_pattern_token +let level2_ast_lexer = mk_lexer level2_ast_token +let level2_meta_lexer = mk_lexer level2_meta_token