「SF-LC」13 ImpParser

1
2
3
4
5
6
7
8
9
10
Inductive chartype := white | alpha | digit | other.

Definition classifyChar (c : ascii) : chartype :=
  if      isWhite c then white
  else if isAlpha c then alpha
  else if isDigit c then digit
  else                   other.
  

Definition token := string.

1
2
3
4
5
6
Inductive optionE (X:Type) : Type :=
  | SomeE (x : X)
  | NoneE (s : string).       (** w/ error msg **)

Arguments SomeE {X}.
Arguments NoneE {X}.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Notation "' p <- e1 ;; e2"
   := (match e1 with
       | SomeE p ⇒ e2
       | NoneE err ⇒ NoneE err
       end)
   (right associativity, p pattern, at level 60, e1 at next level).

Notation "'TRY' ' p <- e1 ;; e2 'OR' e3"
   := (match e1 with
       | SomeE p ⇒ e2
       | NoneE _ ⇒ e3
       end)
   (right associativity, p pattern,
    at level 60, e1 at next level, e2 at next level).

1
2
Definition parser (T : Type) :=
  list token → optionE (T * list token).

1
2
3
4
5
6
7
8
9
10
11
12
Fixpoint many_helper {T} (p : parser T) acc steps xs :=
  match steps, p xs with
  | 0, _ ⇒
      NoneE "Too many recursive calls"
  | _, NoneE _ ⇒
      SomeE ((rev acc), xs)
  | S steps', SomeE (t, xs') ⇒
      many_helper p (t :: acc) steps' xs'
  end.

Fixpoint many {T} (p : parser T) (steps : nat) : parser (list T) :=
  many_helper p [] steps.

1
2
3
4
5
6
7
Definition parseIdentifier (xs : list token) : optionE (string * list token) :=
  match xs with
  | [] ⇒ NoneE "Expected identifier"
  | x::xs' ⇒ if forallb isLowerAlpha (list_of_string x)
             then SomeE (x, xs')
             else NoneE ("Illegal identifier:'" ++ x ++ "'")
  end.