1structure type_tokens :> type_tokens =
2struct
3
4val greek_tyvars = ref true
5
6val _ = Feedback.register_btrace ("Greek tyvars", greek_tyvars)
7
8datatype type_token = datatype type_tokens_dtype.type_token
9
10fun toksize tt =
11    case tt of
12      TypeIdent s => size s
13    | QTypeIdent (s1,s2) => size s1 + size s2 + 1
14    | TypeSymbol s => size s
15    | TypeVar s => size s
16    | Comma => 1
17    | LParen => 1
18    | RParen => 1
19    | LBracket => 1
20    | _ => 0 (* a lie, but unimportant given calling context *)
21
22
23val ERR = Feedback.mk_HOL_ERR "type_tokens"
24
25open qbuf base_tokens
26
27fun munge slist = String.concat (List.rev slist)
28
29
30fun special_symb c = c = #"(" orelse c = #")" orelse c = #","
31
32fun typeidentp (part1, part2) s = let
33  open UnicodeChars
34  (* record whether or not we're onto part2 by checking if part2 is non-null *)
35in
36  if isAlphaNum s orelse s = "_" then
37    if not (null part2) then
38      SOME (part1, s :: part2)
39    else SOME (s :: part1, part2)
40  else if s = "$" then SOME (part1, s :: part2)
41  else NONE
42end
43fun MkTypeIdent (part1, part2) =
44    if null part2 then TypeIdent (munge part1)
45    else if length part2 = 1 then
46      raise ERR "MkTypeIdent" "Malformed qualified identifier (no part after $)"
47    else QTypeIdent(munge part1, String.extract (munge part2, 1, NONE))
48
49fun typevarp0 s = UnicodeChars.isAlphaNum s orelse s = "'" orelse s = "_"
50fun typevarp acc s = if typevarp0 s then SOME (s::acc) else NONE
51
52fun typesymp0 s =
53    case s of
54      "(" => false
55    | ")" => false
56    | "," => false
57    | "[" => false
58    | "]" => false
59    | "'" => false
60    | "\"" => false
61    | _ => UnicodeChars.isSymbolic s
62fun typesymp acc s = if typesymp0 s then SOME (s::acc) else NONE
63
64fun numeraltypep (pfx,sfx) s = let
65  val c = String.sub(s,0)
66in
67  if isSome sfx then NONE
68  else if Char.isDigit c then SOME (s::pfx, sfx)
69  else if Char.isAlpha c then SOME (pfx, SOME c)
70  else NONE
71end
72
73fun MkNumType (pfx, sfx) =
74    case sfx of
75      NONE => TypeIdent (munge pfx)
76    | SOME _ => Error (BT_Numeral (Arbnum.fromString (munge pfx), sfx))
77
78fun isGreekLower i = (* but not lambda *)
79    0x3B1 <= i andalso i <= 0x3C9 andalso i <> 0x3BB
80
81fun split_and_check fb s locn = let
82  val ((s0,i), srest) = valOf (UTF8.getChar s)
83  fun nadvance n tt =
84      if size s = n then ((fn () => advance fb),(tt,locn))
85      else let
86          val (locn',locn'') = locn.split_at n locn
87        in
88          ((fn () => replace_current (BT_Ident (String.extract(s, n, NONE)),
89                                      locn'') fb),
90           (tt,locn'))
91        end
92  fun consume_type p con acc s =
93      case UTF8.getChar s of
94        NONE => ((fn () => advance fb), (con acc,locn))
95      | SOME ((c,_), rest) => let
96        in
97          case p acc c of
98            NONE => let
99              val res = con acc
100            in
101              nadvance (toksize res) res
102            end
103          | SOME acc' => consume_type p con acc' rest
104        end
105  open UnicodeChars
106in
107  if s0 = "'" orelse (isGreekLower i andalso !greek_tyvars) then
108    consume_type typevarp (TypeVar o munge) [s0] srest
109  else if isAlpha s0 then consume_type typeidentp MkTypeIdent ([s0],[]) srest
110  else if Char.isDigit (String.sub(s0,0)) then
111    consume_type numeraltypep MkNumType ([s0], NONE) srest
112  else if s0 = "(" then nadvance 1 LParen
113  else if s0 = ")" then nadvance 1 RParen
114  else if s0 = "," then nadvance 1 Comma
115  else if s0 = "[" then nadvance 1 LBracket
116  else if s0 = "]" then nadvance 1 RBracket
117  else if s0 = "\"" then ((fn () => advance fb), (Error (BT_Ident s),locn))
118  else consume_type typesymp (TypeSymbol o munge) [s0] srest
119end
120
121fun handle_num numinfo =
122    case numinfo of
123      (num, NONE) => TypeIdent (Arbnum.toString num)
124    | (num, SOME _) => Error (BT_Numeral numinfo)
125
126fun typetok_of fb = let
127  val (bt,locn) = current fb
128in
129  case bt of
130    BT_Numeral numinfo => ((fn () => advance fb), (handle_num numinfo, locn))
131  | BT_AQ x => ((fn () => advance fb), (AQ x,locn))
132  | BT_EOI => ((fn () => ()), (Error bt,locn))
133  | BT_Ident s => split_and_check fb s locn
134  | BT_DecimalFraction r => ((fn () => ()), (Error bt, locn))
135  | BT_StrLit _ => ((fn () => ()), (Error bt, locn))
136end
137
138fun lextest s =
139    let
140      val qb = qbuf.new_buffer [QUOTE s]
141      fun recurse acc =
142          let
143            val (adv, (ttok, _ (* locn *))) = typetok_of qb
144          in
145            case ttok of
146                Error BT_EOI => List.rev acc
147              | _ => (adv(); recurse (ttok::acc))
148          end
149    in
150      recurse []
151    end
152
153fun token_string _ (TypeIdent s) = "ID(" ^ s ^ ")"
154  | token_string _ (TypeVar s) = "VAR(" ^ s ^ ")"
155  | token_string _ (TypeSymbol s) = "SYM(" ^ s ^ ")"
156  | token_string _ (QTypeIdent(thy,tyop)) = "QID(" ^ thy ^ "," ^ tyop ^ ")"
157  | token_string _ Comma = "Comma"
158  | token_string _ LParen = "LParen"
159  | token_string _ RParen = "RParen"
160  | token_string _ LBracket = "LBracket"
161  | token_string _ RBracket = "RBracket"
162  | token_string pf (AQ a) = "AQ(" ^ pf a ^ ")"
163  | token_string _ (Error bt) = "Error(" ^ base_tokens.toString bt ^ ")"
164
165fun dest_aq (AQ x) = x
166  | dest_aq _ = raise Fail "dest_aq of non antiquote token"
167
168fun is_ident (TypeIdent _) = true
169  | is_ident _ = false
170fun is_tvar (TypeVar _) = true
171  | is_tvar _ = false
172fun is_typesymbol (TypeSymbol _) = true
173  | is_typesymbol _ = false
174fun is_aq (AQ _) = true
175  | is_aq _ = false
176
177end
178