1structure parse_type :> parse_type = 2struct 3 4open type_tokens type_grammar HOLgrammars Feedback 5 6open qbuf 7 8type term = Term.term 9 10exception InternalFailure of locn.locn 11 12type ('a,'b) tyconstructors = 13 {vartype : string locn.located -> 'a, 14 tyop : (string locn.located * 'a list) -> 'a, 15 qtyop : {Thy:string, Tyop:string, Locn:locn.locn, Args: 'a list} -> 'a, 16 antiq : 'b -> 'a} 17 18(* antiquoting types into terms *) 19fun ty_antiq ty = Term.mk_var("ty_antiq",ty) 20 21fun dest_ty_antiq tm = 22 case Lib.with_exn Term.dest_var tm 23 (mk_HOL_ERR "Parse" "dest_ty_antiq" "not a type antiquotation") 24 of ("ty_antiq",Ty) => Ty 25 | _ => raise mk_HOL_ERR "Parse" "dest_ty_antiq" "not a type antiquotation"; 26 27val is_ty_antiq = Lib.can dest_ty_antiq 28 29val ERR = Feedback.mk_HOL_ERR "Parse" "parse_type" 30val ERRloc = Feedback.mk_HOL_ERRloc "Parse" "parse_type" 31 32fun totalify f x = SOME (f x) handle InternalFailure _ => NONE 33 34fun parse_type_fns tyfns allow_unknown_suffixes G = let 35 val G = rules G and abbrevs = parse_map G 36 and privabbs = privileged_abbrevs G 37 val {vartype = pVartype, tyop = pType, antiq = pAQ, qtyop} = tyfns 38 fun structure_to_value0 (s,locn) args st = 39 case st of 40 TYOP {Args, Thy, Tyop} => 41 qtyop {Args = map (structure_to_value0 (s,locn) args) Args, 42 Thy = Thy, Tyop = Tyop, Locn = locn} 43 | PARAM n => List.nth(args, n) 44 45 fun structure_to_value (s,locn) args st = 46 if num_params st <> length args then 47 raise ERRloc 48 locn 49 ("Incorrect number of arguments to abbreviated operator "^s^ 50 " (expects "^Int.toString (num_params st)^")") 51 else structure_to_value0 (s,locn) args st 52 53 (* extra fails on next two definitions will effectively make the stream 54 push back the unwanted token *) 55 (* can't use item for these, because this would require the token type 56 to be an equality type, which is icky *) 57 fun is_LParen t = case t of LParen => true | _ => false 58 fun is_RParen t = case t of RParen => true | _ => false 59 fun is_LBracket t = case t of LBracket => true | _ => false 60 fun is_RBracket t = case t of RBracket => true | _ => false 61 fun is_Comma t = case t of Comma => true | _ => false 62 fun itemP P fb = let 63 val (adv, (t,locn)) = typetok_of fb (* TODO:KSW: use locn *) 64 in 65 if P t then (locn,adv()) else raise InternalFailure locn 66 end 67 68 fun many f fb = let 69 fun recurse acc = 70 case totalify f fb of 71 NONE => List.rev acc 72 | SOME i => recurse (i::acc) 73 in 74 recurse [] 75 end 76 77 fun many1 f fb = let 78 val i1 = f fb 79 fun recurse acc = 80 case totalify f fb of 81 NONE => List.rev acc 82 | SOME i => recurse (i::acc) 83 in 84 recurse [i1] 85 end 86 87 fun is_numeric s = let 88 val lim = size s 89 fun recurse n = 90 n >= lim orelse (Char.isDigit (String.sub(s,n)) andalso 91 recurse (n + 1)) 92 in 93 recurse 0 94 end 95 96 fun generate_fcpbit ((s,locn), args) = let 97 val _ = null args orelse raise ERRloc locn "Number types take no arguments" 98 val n = Arbnum.fromString s 99 val _ = n <> Arbnum.zero orelse 100 raise ERRloc locn "Zero is not a valid number type" 101 fun recurse acc m = 102 if m = Arbnum.one then acc 103 else let 104 val (q,r) = Arbnum.divmod(m,Arbnum.two) 105 in 106 recurse ((r = Arbnum.one) :: acc) q 107 end 108 fun bit b arg = qtyop {Thy = "fcp", Tyop = if b then "bit1" else "bit0", 109 Locn = locn, Args = [arg]} 110 fun build acc bits = 111 case bits of 112 [] => acc 113 | b :: rest => build (bit b acc) rest 114 val one = qtyop {Thy = "one", Tyop = "one", Locn = locn, Args = []} 115 in 116 build one (recurse [] n) 117 end 118 119 fun apply_tyop (t,locn) args = 120 case t of 121 TypeIdent s => let 122 in 123 if is_numeric s then generate_fcpbit((s,locn), args) 124 else 125 case Binarymap.peek(privabbs, s) of 126 NONE => pType((s,locn), args) 127 | SOME thy => let 128 in 129 case Binarymap.peek(abbrevs, {Name = s, Thy = thy}) of 130 NONE => raise Fail 131 "parse_tyop.apply_tyop: probably shouldn't happen" 132 | SOME st => structure_to_value (s,locn) args st 133 end 134 end 135 | QTypeIdent(thy,ty) => 136 (case Binarymap.peek(abbrevs, {Name = ty, Thy = thy}) of 137 NONE => qtyop{Thy=thy,Tyop=ty,Locn=locn,Args=args} 138 | SOME st => structure_to_value (ty,locn) args st) 139 | _ => raise Fail "parse_type.apply_tyop: can't happen" 140 141 fun apply_asfx locn (base,index) = 142 qtyop{Thy = "fcp", Tyop = "cart",Locn=locn,Args = [base, index]} 143 144 fun parse_op slist fb = let 145 val (adv, (t,locn)) = typetok_of fb 146 in 147 case t of 148 TypeIdent s => if allow_unknown_suffixes orelse Lib.mem s slist then 149 (adv(); (t,locn)) 150 else raise InternalFailure locn 151 | QTypeIdent _ => (adv(); (t,locn)) 152 | _ => raise InternalFailure locn 153 end 154 155 fun parse_binop (stlist:{parse_string:string,opname:string}list) fb = let 156 val (adv, (t,locn)) = typetok_of fb 157 fun doit (t,locn) = 158 case List.find (fn r => (#parse_string r = token_string t)) stlist of 159 NONE => raise InternalFailure locn 160 | SOME r => (adv(); (TypeIdent (#opname r),locn)) 161 in 162 case t of 163 TypeIdent s => doit (t,locn) 164 | TypeSymbol s => doit (t,locn) 165 | _ => raise InternalFailure locn 166 end 167 168 fun parse_asfx prse fb = let 169 val (llocn, _) = itemP is_LBracket fb 170 val ty = prse fb 171 val (rlocn, _) = itemP is_RBracket fb 172 in 173 ty 174 end 175 176 fun parse_tuple prse fb = let 177 val (llocn,_) = itemP is_LParen fb 178 val ty1 = prse fb 179 fun recurse acc = let 180 val (adv,(t,locn)) = typetok_of fb 181 in 182 case t of 183 RParen => (adv(); (List.rev acc,locn.between llocn locn)) 184 | Comma => (adv(); recurse (prse fb :: acc)) 185 | _ => raise InternalFailure locn 186 end 187 in 188 recurse [ty1] 189 end 190 191 fun uniconvert c = let 192 val ((s,i), s') = valOf (UTF8.getChar c) 193 in 194 if s' = "" andalso 0x3B1 <= i andalso i <= 0x3C9 then 195 "'" ^ str (Char.chr (i - 0x3B1 + Char.ord #"a")) 196 else c 197 end 198 199 fun parse_atom fb = let 200 val (adv, (t,locn)) = typetok_of fb 201 in 202 case t of 203 TypeVar s => (adv(); pVartype (uniconvert s, locn)) 204 | AQ x => (adv(); pAQ x) 205 | TypeIdent s => (adv(); apply_tyop(t,locn) []) 206 (* should only be a number *) 207 | _ => raise InternalFailure locn 208 end 209 210 val {suffixes,infixes = rules} = G 211 212 datatype ('op,'array) OPARRAY = NormalSfx of 'op 213 | ArraySfx of 'array * locn.locn 214 fun parse_oparray p strm = let 215 val (adv, (t,locn)) = typetok_of strm 216 in 217 case t of 218 LBracket => ArraySfx (parse_asfx p strm, locn) 219 | _ => NormalSfx (parse_op suffixes strm) 220 end 221 fun apply_oparrays ops base = 222 case ops of 223 [] => base 224 | NormalSfx sfx :: rest => apply_oparrays rest (apply_tyop sfx [base]) 225 | ArraySfx (index,l) :: rest => 226 apply_oparrays rest (apply_asfx l (base, index)) 227 228 fun tuple_oparrays first rest tuple = 229 case first of 230 ArraySfx (i,l) => let 231 in 232 if length tuple <> 1 then 233 raise ERRloc l "array type can't take tuple as first argument" 234 else 235 apply_oparrays rest (apply_asfx l (hd tuple, i)) 236 end 237 | NormalSfx s => apply_oparrays rest (apply_tyop s tuple) 238 239 fun parse_atomsuffixes p strm = let 240 in 241 case totalify (parse_tuple p) strm of 242 NONE => let 243 val ty1 = let 244 val op1 = parse_op suffixes strm 245 in 246 apply_tyop op1 [] 247 end handle InternalFailure l => parse_atom strm 248 val ops = many (parse_oparray p) strm 249 in 250 apply_oparrays ops ty1 251 end 252 | SOME (tyl,locn) => let 253 in 254 case (many (parse_oparray p) strm) of 255 [] => if length tyl <> 1 then 256 raise ERRloc locn "tuple with no suffix" 257 else 258 hd tyl 259 | h::t => tuple_oparrays h t tyl 260 end 261 end 262 263 fun parse_term current strm = 264 case current of 265 [] => parse_atomsuffixes (parse_term rules) strm 266 | (x::xs) => parse_rule x xs strm 267 and parse_rule (rule as (_, r)) rs strm = let 268 val next_level = parse_term rs 269 val same_level = parse_rule rule rs 270 in 271 case r of 272 INFIX (stlist, NONASSOC) => let 273 val ty1 = next_level strm 274 in 275 case totalify (parse_binop stlist) strm of 276 NONE => ty1 277 | SOME opn => apply_tyop opn [ty1, next_level strm] 278 end 279 | INFIX (stlist, LEFT) => let 280 val ty1 = next_level strm 281 fun recurse acc = 282 case totalify (parse_binop stlist) strm of 283 NONE => acc 284 | SOME opn => recurse (apply_tyop opn [acc, next_level strm]) 285 in 286 recurse ty1 287 end 288 | INFIX (stlist, RIGHT) => let 289 val ty1 = next_level strm 290 in 291 case totalify (parse_binop stlist) strm of 292 NONE => ty1 293 | SOME opn => apply_tyop opn [ty1, same_level strm] 294 end 295 end 296in 297 ((fn qb => parse_term rules qb 298 handle InternalFailure locn => 299 raise ERRloc locn 300 ("Type parsing failure with remaining input: "^ 301 qbuf.toString qb)), 302 (fn qb => 303 case totalify (parse_op suffixes) qb of 304 NONE => (parse_atom qb 305 handle InternalFailure locn => 306 raise ERRloc locn 307 ("Type-atom parsing failure with remaining input: "^ 308 qbuf.toString qb) 309 ) 310 | SOME tloc => apply_tyop tloc [])) 311 312end 313 314fun parse_type tyfns allow_unknown_suffixes G qb = 315 #1 (parse_type_fns tyfns allow_unknown_suffixes G) qb 316 317fun parse_atom tyfns allow_unknown_suffixes G qb = 318 #2 (parse_type_fns tyfns allow_unknown_suffixes G) qb 319 320end; (* struct *) 321