X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationLexer.ml;h=3d9d6be252a3d28118d1d1f5e7af47630928d4e1;hb=c784fcbfe47beaa2c399cb71b3d2b84dedc4fb76;hp=26dc5aacae4b9e8f83ec1f9863d1b700e13fdd6f;hpb=c27b932e5adcf89dc9de0e28f65e3370fe3e6b05;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml index 26dc5aaca..3d9d6be25 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.ml +++ b/helm/ocaml/cic_notation/cicNotationLexer.ml @@ -29,19 +29,37 @@ exception Error of int * int * string 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* + (* ZACK: breaks unicode's binder followed by an ascii letter without blank *) +(* let regexp ident_letter = xml_letter *) + +let regexp ident_letter = [ 'a' - 'z' 'A' - 'Z' ] + + (* must be in sync with "is_ligature_char" below *) +let regexp ligature_char = [ "'`~!?@*()[]<>-+=|:;.,/\"" ] +let regexp ligature = ligature_char ligature_char+ + +let is_ligature_char = + (* must be in sync with "regexp ligature_char" above *) + let chars = "'`~!?@*()[]<>-+=|:;.,/\"" in + (fun char -> + (try + ignore (String.index chars char); + true + with Not_found -> false)) + +let regexp ident_decoration = '\'' | '?' | '`' +let regexp ident_cont = ident_letter | xml_digit | '_' +let regexp ident = ident_letter ident_cont* ident_decoration* let regexp tex_token = '\\' ident let regexp delim_begin = "\\[" let regexp delim_end = "\\]" -let regexp keyword = '"' ident '"' let regexp qkeyword = "'" ident "'" let regexp implicit = '?' +let regexp placeholder = '%' let regexp meta = implicit number let regexp csymbol = '\'' ident @@ -55,6 +73,12 @@ let regexp meta_ident = "$" ident let regexp meta_anonymous = "$_" let regexp qstring = '"' [^ '"']* '"' +let regexp begincomment = "(**" xml_blank +let regexp beginnote = "(*" +let regexp endcomment = "*)" +(* let regexp comment_char = [^'*'] | '*'[^')'] +let regexp note = "|+" ([^'*'] | "**") comment_char* "+|" *) + let level1_layouts = [ "sub"; "sup"; "below"; "above"; @@ -62,6 +86,14 @@ let level1_layouts = "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"; @@ -70,13 +102,26 @@ let level2_meta_keywords = "anonymous"; "ident"; "number"; "term"; "fresh" ] -let level1_keywords = - [ "hbox"; "hvbox"; "hovbox"; "vbox"; - "break"; - "list0"; "list1"; "sep"; - "opt"; - "term"; "ident"; "number" - ] + (* (string, unit) Hashtbl.t, to exploit multiple bindings *) +let level2_ast_keywords = Hashtbl.create 23 +let _ = + List.iter (fun k -> Hashtbl.add level2_ast_keywords k ()) + [ "CProp"; "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "match"; + "with"; "in"; "and"; "to"; "as"; "on"; "return" ] + +let add_level2_ast_keyword k = Hashtbl.add level2_ast_keywords k () +let remove_level2_ast_keyword k = Hashtbl.remove level2_ast_keywords k + + (* (string, int) Hashtbl.t, with multiple bindings. + * int is the unicode codepoint *) +let ligatures = Hashtbl.create 23 +let _ = + List.iter + (fun (ligature, symbol) -> Hashtbl.add ligatures ligature symbol) + [ ("->", <:unicode>); ("=>", <:unicode>); + ("<=", <:unicode>); (">=", <:unicode>); + ("<>", <:unicode>); (":=", <:unicode>); + ] let regexp uri = ("cic:/" | "theory:/") (* schema *) @@ -107,11 +152,26 @@ let return lexbuf token = let return_lexeme lexbuf name = return lexbuf (name, Ulexing.utf8_lexeme lexbuf) +let return_symbol lexbuf s = return lexbuf ("SYMBOL", s) +let return_eoi lexbuf = return lexbuf ("EOI", "") + let remove_quotes s = String.sub s 1 (String.length s - 2) let mk_lexer token = let tok_func stream = - let lexbuf = Ulexing.from_utf8_stream stream in +(* let lexbuf = Ulexing.from_utf8_stream stream in *) +(** XXX Obj.magic rationale. + * The problem. + * camlp4 constraints the tok_func field of Token.glexer to have type: + * Stream.t char -> (Stream.t 'te * flocation_function) + * In order to use ulex we have (in theory) to instantiate a new lexbuf each + * time a char Stream.t is passed, destroying the previous lexbuf which may + * have consumed a character from the old stream which is lost forever :-( + * The "solution". + * Instead of passing to camlp4 a char Stream.t we pass a lexbuf, casting it to + * char Stream.t with Obj.magic where needed. + *) + let lexbuf = Obj.magic stream in Token.make_stream_and_flocation (fun () -> try @@ -138,12 +198,11 @@ let expand_macro lexbuf = ("SYMBOL", Utf8Macro.expand macro) with Utf8Macro.Macro_not_found _ -> "SYMBOL", Ulexing.utf8_lexeme lexbuf -let keyword lexbuf = "KEYWORD", remove_quotes (Ulexing.utf8_lexeme 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 +let rec level2_pattern_token_group counter buffer = + lexer | end_group -> if (counter > 0) then Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ; @@ -162,7 +221,8 @@ let read_unparsed_group token_name lexbuf = 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 +let rec level2_meta_token = + lexer | xml_blank+ -> level2_meta_token lexbuf | ident -> let s = Ulexing.utf8_lexeme lexbuf in @@ -173,32 +233,86 @@ let rec level2_meta_token = lexer 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", "") + | 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_eoi lexbuf + +let rec comment_token acc depth = + lexer + | beginnote -> + let acc = acc ^ Ulexing.utf8_lexeme lexbuf in + comment_token acc (depth + 1) lexbuf + | endcomment -> + let acc = acc ^ Ulexing.utf8_lexeme lexbuf in + if depth = 0 + then acc + else comment_token acc (depth - 1) lexbuf + | _ -> + let acc = acc ^ Ulexing.utf8_lexeme lexbuf in + comment_token acc depth lexbuf -let rec level2_ast_token = lexer - | xml_blank+ -> level2_ast_token lexbuf + (** @param k continuation to be invoked when no ligature has been found *) +let rec ligatures_token k = + lexer + | ligature -> + let lexeme = Ulexing.utf8_lexeme lexbuf in + (match List.rev (Hashtbl.find_all ligatures lexeme) with + | [] -> (* ligature not found, rollback and try default lexer *) + Ulexing.rollback lexbuf; + k lexbuf + | default_lig :: _ -> (* ligatures found, use the default one *) + return_symbol lexbuf default_lig) + | eof -> return_eoi lexbuf + | _ -> (* not a ligature, rollback and try default lexer *) + Ulexing.rollback lexbuf; + k lexbuf + +and level2_ast_token = + lexer + | xml_blank+ -> ligatures_token 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) + | implicit -> return lexbuf ("IMPLICIT", "") + | placeholder -> return lexbuf ("PLACEHOLDER", "") + | 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) | tex_token -> return lexbuf (expand_macro lexbuf) | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf) - | qstring -> return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf)) - | csymbol -> return lexbuf ("CSYMBOL", Ulexing.utf8_lexeme lexbuf) + | qstring -> + return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf)) + | csymbol -> + return lexbuf ("CSYMBOL", remove_left_quote (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_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", "") + | beginnote -> + let comment = comment_token (Ulexing.utf8_lexeme lexbuf) 0 lexbuf in +(* let comment = + Ulexing.utf8_sub_lexeme lexbuf 2 (Ulexing.lexeme_length lexbuf - 4) + in + return lexbuf ("NOTE", comment) *) + ligatures_token level2_ast_token lexbuf + | begincomment -> return lexbuf ("BEGINCOMMENT","") + | endcomment -> return lexbuf ("ENDCOMMENT","") + | eof -> return_eoi lexbuf + | _ -> return_symbol lexbuf (Ulexing.utf8_lexeme lexbuf) -let rec level1_pattern_token = lexer - | xml_blank+ -> level1_pattern_token lexbuf +and level1_pattern_token = + lexer + | xml_blank+ -> ligatures_token level1_pattern_token lexbuf | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf) | ident -> let s = Ulexing.utf8_lexeme lexbuf in @@ -209,11 +323,15 @@ let rec level1_pattern_token = lexer return lexbuf ("IDENT", s) end | tex_token -> return lexbuf (expand_macro lexbuf) - | qkeyword -> return lexbuf ("QKEYWORD", remove_quotes (Ulexing.utf8_lexeme 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) + | eof -> return_eoi lexbuf + | _ -> return_symbol lexbuf (Ulexing.utf8_lexeme lexbuf) + +let level1_pattern_token = ligatures_token level1_pattern_token +let level2_ast_token = ligatures_token level2_ast_token (* API implementation *) @@ -221,3 +339,10 @@ 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 +let lookup_ligatures lexeme = + try + if lexeme.[0] = '\\' + then [ Utf8Macro.expand (String.sub lexeme 1 (String.length lexeme - 1)) ] + else List.rev (Hashtbl.find_all ligatures lexeme) + with Invalid_argument _ | Utf8Macro.Macro_not_found _ as exn -> [] +