examples_in_progress/parse_arith.coma

   1 use seq.Seq
   2 use int.Int
   3 use coma.Std
   4
   5 type char
   6 type word = seq char
   7
   8 constant space: char
   9 constant times: char
  10 constant plus: char
  11 constant lpar: char
  12 constant rpar: char
  13 constant c_0: char
  14 constant c_1: char
  15 constant c_2: char
  16 constant c_3: char
  17 constant c_4: char
  18 constant c_5: char
  19 constant c_6: char
  20 constant c_7: char
  21 constant c_8: char
  22 constant c_9: char
  23
  24 let caseNum (c: char)
  25   (case0 { c = c_0 })
  26   (case1 { c = c_1 })
  27   (case2 { c = c_2 })
  28   (case3 { c = c_3 })
  29   (case4 { c = c_4 })
  30   (case5 { c = c_5 })
  31   (case6 { c = c_6 })
  32   (case7 { c = c_7 })
  33   (case8 { c = c_8 })
  34   (case9 { c = c_9 })
  35   (no    { c <> c_0 /\ c <> c_1 /\ c <> c_2 /\
  36            c <> c_3 /\ c <> c_4 /\ c <> c_5 /\
  37            c <> c_6 /\ c <> c_7 /\ c <> c_8 /\
  38            c <> c_9 })
  39 = any
  40
  41 let atoi (c: char) (ok (i:int)) (err) =
  42   caseNum {c}
  43     (ok {0}) (ok {1}) (ok {2}) (ok {3}) (ok {4})
  44     (ok {5}) (ok {6}) (ok {7}) (ok {8}) (ok {9})
  45     (err)
  46
  47 let unSpace (c: char) (space) (else) = if {c = space} space else
  48
  49 let rec next (w: word) (i: int) {..} (k (c: char) {c <> space})
  50 = unSpace {w[i]}
  51     (-> {0 <= i < length w} (! next {w} {i+1} k))
  52     (-> k {w[i]})
  53
  54 let rec lit (w: word) (i v: int) (k (kv: int) (c: char) {c <> space})
  55 = atoi {w[i]}
  56        (fun (i: int) -> lit {w} {i} {10 * v + i} k)
  57        (-> unSpace {w[i]}
  58             (-> next {w} {i + 1} (k {v}))
  59             (-> k {v} {w[i]}))
  60
  61 let rec atom (w: word) (i: int) {..} (k (kv: int) (c: char))
  62 = next {w} {i} . fun (c: char) ->
  63     if {c = lpar}
  64        (-> sum {w} {i+1} .
  65              fun (kv: int) (c: char) -> if {c <> rpar}
  66                                            fail
  67                                            (-> next {w} {i+1} (k {kv})))
  68        (-> atoi {c} (fun (n:int) -> lit {w} {i+1} {n} k) fail)
  69
  70 with term (w: word) (i: int) (k (kv: int) (c: char)) =
  71   atom {w} {i} . fun (kv: int) (c: char) ->
  72     if { c = times }
  73        (-> term {w} {kv} (fun (v': int) (c: char) -> k {v*v'} c))
  74        (-> k {kv} {c})
  75
  76 with sum (w: word) (i: int) (k (kv: int) (c: char)) = any
  77
  78 let count (w: word) {} (ret (r: int) {}) = any