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