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