# 「SF-LC」13 ImpParser

## Logical Foundations - Lexing And Parsing In Coq

Posted by Hux on January 13, 2019

the parser relies on some “monadic” programming idioms

basically, parser combinator (But 非常麻烦 in Coq)

## Lex

 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.

## Syntax

 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 newtype Parser a = Parser (String -> [(a,String)]) instance Monad Parser where -- (>>=) :: Parser a -> (a -> Parser b) -> Parser b p >>= f = P (\inp -> case parse p inp of [] -> [] [(v,out)] -> parse (f v) out)