Skip to content

Commit aa95f11

Browse files
author
Alex Gryzlov
committed
Id/Nat/AExp parsers
1 parent 4c39a10 commit aa95f11

File tree

1 file changed

+80
-106
lines changed

1 file changed

+80
-106
lines changed

‎src/ImpParser.lidr

Lines changed: 80 additions & 106 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,7 @@ Require Import Coq.Lists.List.
2828
Import ListNotations.
2929

3030
> import Maps
31+
> import Imp
3132
>
3233

3334
== Internals
@@ -82,7 +83,7 @@ Import ListNotations.
8283
> tokenize : (s : String) -> List String
8384
> tokenize s = map pack (tokenizeHelper White [] (unpack s))
8485

85-
> tokenizeEx1 : tokenize "abc12==3 223*(3+(a+c))" = ["abc", "12", "==", "3", "223", "*", "(", "3", "+", "(", "a", "+", "c", ")", ")"]
86+
> tokenizeEx1 : tokenize "abc12==3 223*(3+(a+c))" = ["abc","12","==","3","223","*","(","3","+","(","a","+","c",")",")"]
8687
> tokenizeEx1 = Refl
8788

8889
=== Parsing
@@ -95,24 +96,30 @@ An `option` type with error messages:
9596
> SomeE : x -> OptionE x
9697
> NoneE : String -> OptionE x
9798

98-
Some syntactic sugar to make writing nested match-expressions on `OptionE` more
99-
convenient.
99+
Some interface instances to make writing nested match-expressions on `OptionE`
100+
more convenient.
100101

101-
```coq
102-
Notation "'DO' ( x , y ) <== e1 ; e2"
103-
:= (match e1 with
104-
| SomeE (x,y) => e2
105-
| NoneE err => NoneE err
106-
end)
107-
(right associativity, at level 60).
108-
109-
Notation "'DO' ( x , y ) <-- e1 ; e2 'OR' e3"
110-
:= (match e1 with
111-
| SomeE (x,y) => e2
112-
| NoneE err => e3
113-
end)
114-
(right associativity, at level 60, e2 at next level).
115-
```
102+
\todo[inline]{Explain these/link to Haskell etc?}
103+
104+
> Functor OptionE where
105+
> map f (SomeE x) = SomeE (f x)
106+
> map _ (NoneE err) = NoneE err
107+
108+
> Applicative OptionE where
109+
> pure = SomeE
110+
> (SomeE f) <*> (SomeE x) = SomeE (f x)
111+
> (SomeE _) <*> (NoneE e2) = NoneE e2
112+
> (NoneE e1) <*> (SomeE _) = NoneE e1
113+
> (NoneE e1) <*> (NoneE e2) = NoneE (e1 ++ ";" ++ e2)
114+
115+
> Alternative OptionE where
116+
> empty = NoneE ""
117+
> (SomeE x) <|> _ = SomeE x
118+
> (NoneE _) <|> v = v
119+
120+
> Monad OptionE where
121+
> (NoneE e) >>= _ = NoneE e
122+
> (SomeE x) >>= k = k x
116123

117124
==== Generic Combinators for Building Parsers
118125

@@ -145,100 +152,67 @@ A parser that expects a particular token:
145152

146153
Identifiers:
147154

148-
```coq
149-
Definition parseIdentifier (xs : list token)
150-
: optionE (id * list token) :=
151-
match xs with
152-
| [] => NoneE "Expected identifier"
153-
| x::xs' =>
154-
if forallb isLowerAlpha (list_of_string x) then
155-
SomeE (Id x, xs')
156-
else
157-
NoneE ("Illegal identifier:'" ++ x ++ "'")
158-
end.
159-
```
155+
> parseIdentifier : (xs : List Token) -> OptionE (Id, List Token)
156+
> parseIdentifier [] = NoneE "Expected identifier"
157+
> parseIdentifier (x::xs') =
158+
> if all isLowerAlpha (unpack x)
159+
> then SomeE (MkId x, xs')
160+
> else NoneE ("Illegal identifier:'" ++ x ++ "'")
160161

161162
Numbers:
162163

163-
```coq
164-
Definition parseNumber (xs : list token)
165-
: optionE (nat * list token) :=
166-
match xs with
167-
| [] => NoneE "Expected number"
168-
| x::xs' =>
169-
if forallb isDigit (list_of_string x) then
170-
SomeE (fold_left
171-
(fun n d =>
172-
10 * n + (nat_of_ascii d -
173-
nat_of_ascii "0"%char))
174-
(list_of_string x)
175-
0,
176-
xs')
177-
else
178-
NoneE "Expected number"
179-
end.
180-
```
164+
> parseNumber : (xs : List Token) -> OptionE (Nat, List Token)
165+
> parseNumber [] = NoneE "Expected number"
166+
> parseNumber (x::xs') =
167+
> if all isDigit (unpack x)
168+
> then SomeE (foldl (\n, d => 10 * n + (cast (ord d - ord '0'))) 0 (unpack x), xs')
169+
> else NoneE "Expected number"
181170

182171
Parse arithmetic expressions
183172

184-
```coq
185-
Fixpoint parsePrimaryExp (steps:nat)
186-
(xs : list token)
187-
: optionE (aexp * list token) :=
188-
match steps with
189-
| 0 => NoneE "Too many recursive calls"
190-
| S steps' =>
191-
DO (i, rest) <-- parseIdentifier xs ;
192-
SomeE (AId i, rest)
193-
OR DO (n, rest) <-- parseNumber xs ;
194-
SomeE (ANum n, rest)
195-
OR (DO (e, rest) <== firstExpect "("
196-
(parseSumExp steps') xs;
197-
DO (u, rest') <== expect ")" rest ;
198-
SomeE(e,rest'))
199-
end
200-
201-
with parseProductExp (steps:nat)
202-
(xs : list token) :=
203-
match steps with
204-
| 0 => NoneE "Too many recursive calls"
205-
| S steps' =>
206-
DO (e, rest) <==
207-
parsePrimaryExp steps' xs ;
208-
DO (es, rest') <==
209-
many (firstExpect "*" (parsePrimaryExp steps'))
210-
steps' rest;
211-
SomeE (fold_left AMult es e, rest')
212-
end
213-
214-
with parseSumExp (steps:nat) (xs : list token) :=
215-
match steps with
216-
| 0 => NoneE "Too many recursive calls"
217-
| S steps' =>
218-
DO (e, rest) <==
219-
parseProductExp steps' xs ;
220-
DO (es, rest') <==
221-
many (fun xs =>
222-
DO (e,rest') <--
223-
firstExpect "+"
224-
(parseProductExp steps') xs;
225-
SomeE ( (true, e), rest')
226-
OR DO (e,rest') <==
227-
firstExpect "-"
228-
(parseProductExp steps') xs;
229-
SomeE ( (false, e), rest'))
230-
steps' rest;
231-
SomeE (fold_left (fun e0 term =>
232-
match term with
233-
(true, e) => APlus e0 e
234-
| (false, e) => AMinus e0 e
235-
end)
236-
es e,
237-
rest')
238-
end.
239-
240-
Definition parseAExp := parseSumExp.
241-
```
173+
> mutual
174+
> parsePrimaryExp : (steps : Nat) -> (xs : List Token) -> OptionE (AExp, List Token)
175+
> parsePrimaryExp Z _ = NoneE "Too many recursive calls"
176+
> parsePrimaryExp (S steps') xs =
177+
> (do (i, rest) <- parseIdentifier xs
178+
> pure (AId i, rest))
179+
> <|>
180+
> (do (n, rest) <- parseNumber xs
181+
> pure (ANum n, rest))
182+
> <|>
183+
> (do (e, rest) <- firstExpect "(" (parseSumExp steps') xs
184+
> (u, rest') <- expect ")" rest
185+
> pure (e, rest'))
186+
>
187+
> parseProductExp : (steps : Nat) -> (xs : List Token) -> OptionE (AExp, List Token)
188+
> parseProductExp Z _ = NoneE "Too many recursive calls"
189+
> parseProductExp (S steps') xs =
190+
> do (e, rest) <- parsePrimaryExp steps' xs
191+
> (es, rest') <- many (firstExpect "*" (parsePrimaryExp steps')) steps' rest
192+
> pure (foldl AMult e es, rest')
193+
>
194+
> parseSumExp : (steps : Nat) -> (xs : List Token) -> OptionE (AExp, List Token)
195+
> parseSumExp Z _ = NoneE "Too many recursive calls"
196+
> parseSumExp (S steps') xs =
197+
> do (e, rest) <- parseProductExp steps' xs
198+
> (es, rest') <- many psum steps' rest
199+
> pure (foldl (\e0, term =>
200+
> case term of
201+
> (True, e) => APlus e0 e
202+
> (False, e) => AMinus e0 e
203+
> ) e es, rest')
204+
> where
205+
> psum : Parser (Bool, AExp)
206+
> psum xs =
207+
> let p = parseProductExp steps' in
208+
> (do (e, r) <- firstExpect "+" p xs
209+
> pure ((True, e), r))
210+
> <|>
211+
> (do (e, r) <- firstExpect "-" p xs
212+
> pure ((False, e), r))
213+
>
214+
> parseAExp : (steps : Nat) -> (xs : List Token) -> OptionE (AExp, List Token)
215+
> parseAExp = parseSumExp
242216

243217
Parsing boolean expressions:
244218

0 commit comments

Comments
 (0)