47 (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode) |
47 (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode) |
48 --| junk)) |
48 --| junk)) |
49 -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::); |
49 -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::); |
50 in explode #> scan_valids #> space_implode "_" end; |
50 in explode #> scan_valids #> space_implode "_" end; |
51 |
51 |
52 fun purify_op s = |
52 fun purify_op "op -->" = "implies" |
53 let |
53 | purify_op "{}" = "empty" |
54 fun rep_op "+" = SOME "plus" |
54 | purify_op s = |
55 | rep_op "*" = SOME "times" |
55 let |
56 | rep_op "&" = SOME "and" |
56 fun rep_op "+" = SOME "plus" |
57 | rep_op "|" = SOME "or" |
57 | rep_op "*" = SOME "times" |
58 | rep_op "=" = SOME "eq" |
58 | rep_op "&" = SOME "and" |
59 | rep_op "{" = SOME "empty" |
59 | rep_op "|" = SOME "or" |
60 | rep_op s = NONE; |
60 | rep_op "=" = SOME "eq" |
61 val scan_valids = Symbol.scanner "Malformed input" |
61 | rep_op s = NONE; |
62 (Scan.repeat (Scan.some rep_op || Scan.one Symbol.not_eof)); |
62 val scan_valids = Symbol.scanner "Malformed input" |
63 in (explode #> scan_valids #> implode) s end; |
63 (Scan.repeat (Scan.some rep_op || Scan.one Symbol.not_eof)); |
|
64 in (explode #> scan_valids #> implode) s end; |
64 |
65 |
65 val purify_lower = |
66 val purify_lower = |
66 explode |
67 explode |
67 #> (fn cs => (if forall Symbol.is_ascii_upper cs |
68 #> (fn cs => (if forall Symbol.is_ascii_upper cs |
68 then map else nth_map 0) Symbol.to_ascii_lower cs) |
69 then map else nth_map 0) Symbol.to_ascii_lower cs) |