1(* ========================================================================= *) 2(* FILE : TheoryLexer.sml *) 3(* DESCRIPTION : Tokenize theory data *) 4(* AUTHOR : (c) Thibault Gauthier, University of Innsbruck *) 5(* DATE : 2017 *) 6(* ========================================================================== *) 7 8structure TheoryLexer :> TheoryLexer = 9struct 10 11open Feedback Lib Type Term Thm 12 13val ERR = mk_HOL_ERR "TheoryLexer" 14 15(*---------------------------------------------------------------------------- 16 Token types 17 -----------------------------------------------------------------------------*) 18 19fun is_blank c = c = #" " orelse c = #"\n" orelse c = #"\t" 20 21fun is_sep c = c = #"," orelse c = #"[" orelse c = #"]" 22 23fun is_alphanum #"_" = true 24 | is_alphanum ch = Char.isAlphaNum ch 25 26(*---------------------------------------------------------------------------- 27 Lexer 28 -----------------------------------------------------------------------------*) 29 30fun wait_char f_char buf charl = case charl of 31 [] => (implode (rev buf), []) 32 | a :: m => 33 ( 34 if f_char a 35 then (implode (rev buf), charl) 36 else wait_char f_char (a :: buf) m 37 ) 38 39fun wait_endquote buf charl = case charl of 40 #"\\" :: #"\\" :: m => wait_endquote (#"\\" :: #"\\" :: buf) m 41 | #"\\" :: #"\"" :: m => wait_endquote (#"\"" :: #"\\" :: buf) m 42 | #"\"" :: m => (implode (rev (#"\"" :: buf)), m) 43 | a :: m => wait_endquote (a :: buf) m 44 | _ => raise ERR "wait_endquote" "" 45 46fun lex_helper acc charl = case charl of 47 [] => rev acc 48 | #"\"" :: m => 49 let val (token, cont) = wait_endquote [#"\""] m in 50 lex_helper (token :: acc) cont 51 end 52 | a :: m => 53 ( 54 if is_blank a 55 then lex_helper acc m 56 else if is_sep a 57 then lex_helper (Char.toString a :: acc) m 58 else if is_alphanum a 59 then 60 let val (token, cont) = wait_char (not o is_alphanum) [] charl in 61 lex_helper (token :: acc) cont 62 end 63 else raise ERR "lex_helper" (Char.toString a) 64 ) 65 66fun lex_thydata s = lex_helper [] (explode s) 67 handle HOL_ERR _ => raise ERR "lex_thydata" s 68 69end (* struct *) 70