commands parser, formatting

Author: Alex Gryzlov

src/ImpParser.lidr

@@ -7,7 +7,7 @@ The development of the Imp language in `Imp.lidr` completely ignores issues of
 concrete syntax -- how an ascii string that a programmer might write gets
 translated into abstract syntax trees defined by the datatypes `aexp`, `bexp`,
 and `com`.  In this chapter, we illustrate how the rest of the story can be
-filled in by building a simple lexical analyzer and parser using Coq's
+filled in by building a simple lexical analyzer and parser using Idris's
 functional programming facilities.
 
 It is not important to understand all the details here (and accordingly, the
@@ -18,15 +18,6 @@ code -- most of it is not very complicated, though the parser relies on some
 most readers will probably want to just skim down to the Examples section at the
 very end to get the punchline.
 
-
-Set Warnings "-notation-overridden,-parsing,-deprecated-implicit-arguments".
-Require Import Coq.Strings.String.
-Require Import Coq.Strings.Ascii.
-Require Import Coq.Arith.Arith.
-Require Import Coq.Arith.EqNat.
-Require Import Coq.Lists.List.
-Import ListNotations.
-
 > import Maps
 > import Imp
 >
@@ -37,9 +28,9 @@ Import ListNotations.
 
 > isLowerAlpha : (c : Char) -> Bool
 > isLowerAlpha c = isLower c || isDigit c
-
+>
 > data Chartype = White | Alpha | Digit | Other
-
+>
 > classifyChar : (c : Char) -> Chartype
 > classifyChar c =
 >   if isSpace c then
@@ -50,10 +41,10 @@ Import ListNotations.
 >     Digit
 >   else
 >     Other
-
+>
 > Token : Type
 > Token = String
-
+>
 > tokenizeHelper : (cls : Chartype) -> (acc, xs : List Char) -> List (List Char)
 > tokenizeHelper cls acc xs =
 >   case xs of
@@ -79,12 +70,13 @@ Import ListNotations.
 >   tk = case acc of
 >          []     => []
 >          (_::_) => [reverse acc]
-
+>
 > tokenize : (s : String) -> List String
 > tokenize s = map pack (tokenizeHelper White [] (unpack s))
-
+>
 > tokenizeEx1 : tokenize "abc12==3  223*(3+(a+c))" = ["abc","12","==","3","223","*","(","3","+","(","a","+","c",")",")"]
 > tokenizeEx1 = Refl
+>
 
 === Parsing
 
@@ -95,6 +87,7 @@ An `option` type with error messages:
 > data OptionE : (x : Type) -> Type where
 >   SomeE : x -> OptionE x
 >   NoneE : String -> OptionE x
+>
 
 Some interface instances to make writing nested match-expressions on `OptionE`
 more convenient.
@@ -104,69 +97,75 @@ more convenient.
 > Functor OptionE where
 >   map f (SomeE x)   = SomeE (f x)
 >   map _ (NoneE err) = NoneE err
-
+>
 > Applicative OptionE where
 >   pure = SomeE
 >   (SomeE f)  <*> (SomeE x)  = SomeE (f x)
 >   (SomeE _)  <*> (NoneE e2) = NoneE e2
 >   (NoneE e1) <*> (SomeE _)  = NoneE e1
 >   (NoneE e1) <*> (NoneE e2) = NoneE (e1 ++ ";" ++ e2)
-
+>
 > Alternative OptionE where
->     empty = NoneE ""
->     (SomeE x) <|> _ = SomeE x
->     (NoneE _) <|> v = v
-
+>   empty = NoneE ""
+>   (SomeE x) <|> _ = SomeE x
+>   (NoneE _) <|> v = v
+>
 > Monad OptionE where
->     (NoneE e) >>= _ = NoneE e
->     (SomeE x) >>= k = k x
+>   (NoneE e) >>= _ = NoneE e
+>   (SomeE x) >>= k = k x
+>
 
 ==== Generic Combinators for Building Parsers
 
 > Parser : (t : Type) -> Type
 > Parser t = List Token -> OptionE (t, List Token)
-
+>
 > manyHelper : (p : Parser t) -> (acc : List t) -> (steps : Nat) -> Parser (List t)
 > manyHelper p acc Z _ = NoneE "Too many recursive calls"
 > manyHelper p acc (S steps') xs with (p xs)
 >  | NoneE _        = SomeE (reverse acc, xs)
 >  | SomeE (t', xs') = manyHelper p (t'::acc) steps' xs'
+>
 
 A (step-indexed) parser that expects zero or more `p`s:
 
 > many : (p : Parser t) -> (steps : Nat) -> Parser (List t)
 > many p steps = manyHelper p [] steps
+>
 
 A parser that expects a given token, followed by `p`:
 
 > firstExpect : (a : Token) -> (p : Parser t) -> Parser t
-> firstExpect a p (x::xs) = if x == a then p xs else NoneE ("expected '" ++ a ++ "'.")
-> firstExpect a _ [] = NoneE ("expected '" ++ a ++ "'.")
+> firstExpect a p (x::xs) = if x == a then p xs else NoneE ("Expected '" ++ a ++ "'")
+> firstExpect a _ [] = NoneE ("Expected '" ++ a ++ "'")
+>
 
 A parser that expects a particular token:
 
 > expect : (t : Token) -> Parser ()
 > expect t = firstExpect t (\xs => SomeE ((), xs))
-
+>
 ==== A Recursive-Descent Parser for Imp
 
 Identifiers:
 
 > parseIdentifier : Parser Id
 > parseIdentifier [] = NoneE "Expected identifier"
-> parseIdentifier (x::xs') =
+> parseIdentifier (x::xs) =
 >   if all isLowerAlpha (unpack x)
->     then SomeE (MkId x, xs')
+>     then SomeE (MkId x, xs)
 >     else NoneE ("Illegal identifier:'" ++ x ++ "'")
+>
 
 Numbers:
 
 > parseNumber : Parser Nat
 > parseNumber [] = NoneE "Expected number"
-> parseNumber (x::xs') =
+> parseNumber (x::xs) =
 >   if all isDigit (unpack x)
->     then SomeE (foldl (\n, d => 10 * n + (cast (ord d - ord '0'))) 0 (unpack x), xs')
+>     then SomeE (foldl (\n, d => 10 * n + (cast (ord d - ord '0'))) 0 (unpack x), xs)
 >     else NoneE "Expected number"
+>
 
 Parse arithmetic expressions
 
@@ -213,24 +212,25 @@ Parse arithmetic expressions
 >
 > parseAExp : (steps : Nat) -> Parser AExp
 > parseAExp = parseSumExp
+>
 
 Parsing boolean expressions:
 
 > mutual
 >   parseAtomicExp : (steps : Nat) -> Parser BExp
 >   parseAtomicExp Z _ = NoneE "Too many recursive calls"
 >   parseAtomicExp (S steps') xs =
->     (do (u, rest) <- expect "true" xs
+>     (do (_, rest) <- expect "true" xs
 >         pure (BTrue, rest))
 >     <|>
->     (do (u, rest) <- expect "false" xs
+>     (do (_, rest) <- expect "false" xs
 >         pure (BFalse, rest))
 >     <|>
 >     (do (e, rest) <- firstExpect "not" (parseAtomicExp steps') xs
 >         pure (BNot e, rest))
 >     <|>
 >     (do (e, rest) <- firstExpect "(" (parseConjunctionExp steps') xs
->         (u, rest') <- expect ")" rest
+>         (_, rest') <- expect ")" rest
 >         pure (e, rest'))
 >     <|>
 >     (do (e, rest) <- parseProductExp steps' xs
@@ -251,85 +251,58 @@ Parsing boolean expressions:
 >
 > parseBExp : (steps : Nat) -> Parser BExp
 > parseBExp = parseConjunctionExp
+>
+> testParsing : (p : Nat -> Parser t) -> (s : String) -> OptionE (t, List Token)
+> testParsing p s = p 100 (tokenize s)
+>
 
-``coq
-Check parseConjunctionExp.
-
-Definition testParsing {X : Type}
-           (p : nat ->
-                list token ->
-                optionE (X * list token))
-           (s : string) :=
-  let t := tokenize s in
-  p 100 t.
+\todo[inline]{The second one seems designed to fail}
 
-(*
-Eval compute in
-  testParsing parseProductExp "x*y*(x*x)*x".
+```idris
+λΠ> testParsing parseProductExp "x*y*(x*x)*x"
 
-Eval compute in
-  testParsing parseConjunctionExp "not((x==x||x*x<=(x*x)*x)&&x==x".
-*)
+λΠ> testParsing parseConjunctionExp "not((x==x||x*x<=(x*x)*x)&&x==x"
 ```
 
 Parsing commands:
 
-```coq
-Fixpoint parseSimpleCommand (steps:nat)
-                            (xs : list token) :=
-  match steps with
-  | 0 => NoneE "Too many recursive calls"
-  | S steps' =>
-    DO (u, rest) <-- expect "SKIP" xs;
-      SomeE (SKIP, rest)
-    OR DO (e,rest) <--
-         firstExpect "IF" (parseBExp steps') xs;
-       DO (c,rest')  <==
-         firstExpect "THEN"
-           (parseSequencedCommand steps') rest;
-       DO (c',rest'') <==
-         firstExpect "ELSE"
-           (parseSequencedCommand steps') rest';
-       DO (u,rest''') <==
-         expect "END" rest'';
-       SomeE(IFB e THEN c ELSE c' FI, rest''')
-    OR DO (e,rest) <--
-         firstExpect "WHILE"
-           (parseBExp steps') xs;
-       DO (c,rest') <==
-         firstExpect "DO"
-           (parseSequencedCommand steps') rest;
-       DO (u,rest'') <==
-         expect "END" rest';
-       SomeE(WHILE e DO c END, rest'')
-    OR DO (i, rest) <==
-         parseIdentifier xs;
-       DO (e, rest') <==
-         firstExpect ":=" (parseAExp steps') rest;
-       SomeE(i ::= e, rest')
-  end
-
-with parseSequencedCommand (steps:nat)
-                           (xs : list token) :=
-  match steps with
-  | 0 => NoneE "Too many recursive calls"
-  | S steps' =>
-      DO (c, rest) <==
-        parseSimpleCommand steps' xs;
-      DO (c', rest') <--
-        firstExpect ";;"
-          (parseSequencedCommand steps') rest;
-        SomeE(c ;; c', rest')
-      OR
-        SomeE(c, rest)
-  end.
-
-Definition bignumber := 1000.
-
-Definition parse (str : string) : optionE (com * list token) :=
-  let tokens := tokenize str in
-  parseSequencedCommand bignumber tokens.
-```
+> mutual
+>   parseSimpleCommand : (steps : Nat) -> Parser Com
+>   parseSimpleCommand Z _ = NoneE "Too many recursive calls"
+>   parseSimpleCommand (S steps') xs =
+>     (do (_, rest) <- expect "SKIP" xs
+>         pure (SKIP, rest))
+>     <|>
+>     (do (e, rest) <- firstExpect "IF" (parseBExp steps') xs
+>         (c, rest') <- firstExpect "THEN" (parseSequencedCommand steps') rest
+>         (c', rest'') <- firstExpect "ELSE" (parseSequencedCommand steps') rest'
+>         (_, rest''') <- expect "END" rest''
+>         pure (IFB e THEN c ELSE c' FI, rest'''))
+>     <|>
+>     (do (e, rest) <- firstExpect "WHILE" (parseBExp steps') xs
+>         (c, rest') <- firstExpect "DO" (parseSequencedCommand steps') rest
+>         (_, rest'') <- expect "END" rest'
+>         pure (WHILE e DO c END, rest''))
+>     <|>
+>     (do (i, rest) <- parseIdentifier xs;
+>         (e, rest') <- firstExpect ":=" (parseAExp steps') rest
+>         pure (i ::= e, rest'))
+>
+>   parseSequencedCommand : (steps : Nat) -> Parser Com
+>   parseSequencedCommand Z _ = NoneE "Too many recursive calls"
+>   parseSequencedCommand (S steps') xs =
+>     do (c, rest) <- parseSimpleCommand steps' xs
+>        ((do (c', rest') <- firstExpect ";;" (parseSequencedCommand steps') rest
+>             pure (c ;; c', rest'))
+>         <|>
+>         (pure (c, rest)))
+>
+> bignumber : Nat
+> bignumber = 1000
+>
+> parse : (str : String) -> OptionE (Com, List Token)
+> parse str = parseSequencedCommand bignumber (tokenize str)
+>
 
 == Examples