equal
deleted
inserted
replaced
18 |
18 |
19 local |
19 local |
20 |
20 |
21 fun string_of_rat r = |
21 fun string_of_rat r = |
22 let |
22 let |
23 val (nom, den) = Rat.quotient_of_rat r |
23 val (nom, den) = Rat.dest r |
24 in |
24 in |
25 if den = 1 then string_of_int nom |
25 if den = 1 then string_of_int nom |
26 else string_of_int nom ^ "/" ^ string_of_int den |
26 else string_of_int nom ^ "/" ^ string_of_int den |
27 end |
27 end |
28 |
28 |
101 Scan.repeat1 (Scan.one Symbol.is_ascii_digit >> (fn s => ord s - ord "0")) |
101 Scan.repeat1 (Scan.one Symbol.is_ascii_digit >> (fn s => ord s - ord "0")) |
102 >> foldl1 (fn (n, d) => n * 10 + d) |
102 >> foldl1 (fn (n, d) => n * 10 + d) |
103 |
103 |
104 val nat = number |
104 val nat = number |
105 val int = Scan.optional (str "~" >> K ~1) 1 -- nat >> op * |
105 val int = Scan.optional (str "~" >> K ~1) 1 -- nat >> op * |
106 val rat = int --| str "/" -- int >> Rat.rat_of_quotient |
106 val rat = int --| str "/" -- int >> Rat.make |
107 val rat_int = rat || int >> Rat.rat_of_int |
107 val rat_int = rat || int >> Rat.of_int |
108 |
108 |
109 |
109 |
110 (* polynomial parsers *) |
110 (* polynomial parsers *) |
111 |
111 |
112 fun repeat_sep s f = f ::: Scan.repeat (str s |-- f) |
112 fun repeat_sep s f = f ::: Scan.repeat (str s |-- f) |