[ fix #63 ] interleaving let binders and local declarations (#691)

idris2api.ipkg

@@ -81,6 +81,7 @@ modules =
     Idris.ModTree,
     Idris.Package,
     Idris.Parser,
+    Idris.Parser.Let,
     Idris.Pretty,
     Idris.ProcessIdr,
     Idris.REPL,

libs/base/Data/List.idr

@@ -174,13 +174,20 @@ public export
 union : Eq a => List a -> List a -> List a
 union = unionBy (==)
 
+public export
+spanBy : (a -> Maybe b) -> List a -> (List b, List a)
+spanBy p [] = ([], [])
+spanBy p (x :: xs) = case p x of
+  Nothing => ([], x :: xs)
+  Just y => let (ys, zs) = spanBy p xs in (y :: ys, zs)
+
 public export
 span : (a -> Bool) -> List a -> (List a, List a)
 span p []      = ([], [])
 span p (x::xs) =
   if p x then
     let (ys, zs) = span p xs in
-      (x::ys, zs)
+        (x::ys, zs)
   else
     ([], x::xs)
 

libs/contrib/Data/String/Parser/Expression.idr

@@ -116,6 +116,6 @@ buildExpressionParser a operators simpleExpr =
           rassocP = mkRassocP amLeft amNon rassocOp termP
           lassocP = mkLassocP amRight amNon lassocOp termP
           nassocP = mkNassocP amRight amLeft amNon nassocOp termP
-          in
+      in
           do x <- termP
              rassocP x <|> lassocP x <|> nassocP x <|> pure x <?> "operator"

src/Core/FC.idr

@@ -1,9 +1,13 @@
 module Core.FC
 
+import Text.Bounded
 import Text.PrettyPrint.Prettyprinter
 
 %default total
 
+------------------------------------------------------------------------
+-- Types
+
 public export
 FilePos : Type
 FilePos = (Int, Int)
@@ -20,11 +24,8 @@ public export
 data FC = MkFC FileName FilePos FilePos
         | EmptyFC
 
-export
-Eq FC where
-  (==) (MkFC n s e) (MkFC n' s' e') = n == n' && s == s' && e == e'
-  (==) EmptyFC EmptyFC = True
-  (==) _ _ = False
+------------------------------------------------------------------------
+-- Projections
 
 export
 file : FC -> FileName
@@ -41,6 +42,16 @@ endPos : FC -> FilePos
 endPos (MkFC _ _ e) = e
 endPos EmptyFC = (0, 0)
 
+------------------------------------------------------------------------
+-- Smart constructor
+
+export
+boundToFC : FileName -> WithBounds t -> FC
+boundToFC fname b = MkFC fname (start b) (end b)
+
+------------------------------------------------------------------------
+-- Predicates
+
 -- Return whether a given file position is within the file context (assuming we're
 -- in the right file)
 export
@@ -57,6 +68,9 @@ onLine x (MkFC _ start end)
    = x >= fst start && x <= fst end
 onLine _ _ = False
 
+------------------------------------------------------------------------
+-- Constant values
+
 export
 emptyFC : FC
 emptyFC = EmptyFC
@@ -67,6 +81,15 @@ toplevelFC = MkFC "(toplevel)" (0, 0) (0, 0)
 
 %name FC fc
 
+------------------------------------------------------------------------
+-- Instances
+
+export
+Eq FC where
+  (==) (MkFC n s e) (MkFC n' s' e') = n == n' && s == s' && e == e'
+  (==) EmptyFC EmptyFC = True
+  (==) _ _ = False
+
 export
 Show FC where
   show loc = file loc ++ ":" ++

src/Idris/Parser.idr

@@ -7,11 +7,15 @@ import        Parser.Lexer.Source
 import        TTImp.TTImp
 
 import public Text.Parser
+import        Data.Either
 import        Data.List
 import        Data.List.Views
 import        Data.List1
 import        Data.Maybe
 import        Data.Strings
+import Utils.String
+
+import Idris.Parser.Let
 
 %default covering
 
@@ -48,9 +52,6 @@ plhs = MkParseOpts False False
 %hide Prelude.pure
 %hide Core.Core.pure
 
-boundToFC : String -> WithBounds t -> FC
-boundToFC fname b = MkFC fname (start b) (end b)
-
 atom : FileName -> Rule PTerm
 atom fname
     = do x <- bounds $ exactIdent "Type"
@@ -533,63 +534,31 @@ mutual
            = PLam (boundToFC fname pat) rig Explicit pat.val ty
                   (bindAll rest scope)
 
-  letBinder : FileName -> IndentInfo ->
-              Rule (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause)
-  letBinder fname indents
-      = do b <- bounds (do s <- bounds (MkPair <$> multiplicity <*> expr plhs fname indents)
-                           (rigc, pat) <- pure s.val
-                           ty <- option (PImplicit (boundToFC fname s))
-                                        (do symbol ":"
-                                            typeExpr (pnoeq pdef) fname indents)
-                           symbol "="
-                           val <- expr pnowith fname indents
-                           alts <- block (patAlt fname)
-                           rig <- getMult rigc
-                           pure (rig, pat, ty, val, alts))
-           (rig, pat, ty, val, alts) <- the (SourceEmptyRule (RigCount, PTerm, PTerm, PTerm, List PClause)) (pure b.val)
-           pure (start b, end b, rig, pat, ty, val, alts)
+  letBlock : FileName -> IndentInfo -> Rule (WithBounds (Either LetBinder LetDecl))
+  letBlock fname indents = bounds (letBinder <||> letDecl) where
 
-  buildLets : FileName ->
-              List (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause) ->
-              PTerm -> PTerm
-  buildLets fname [] sc = sc
-  buildLets fname ((start, end, rig, pat, ty, val, alts) :: rest) sc
-      = let fc = MkFC fname start end in
-            PLet fc rig pat ty val
-                 (buildLets fname rest sc) alts
+    letBinder : Rule LetBinder
+    letBinder = do s <- bounds (MkPair <$> multiplicity <*> expr plhs fname indents)
+                   (rigc, pat) <- pure s.val
+                   ty <- option (PImplicit (boundToFC fname s))
+                                (symbol ":" *> typeExpr (pnoeq pdef) fname indents)
+                   (symbol "=" <|> symbol ":=")
+                   val <- expr pnowith fname indents
+                   alts <- block (patAlt fname)
+                   rig <- getMult rigc
+                   pure (MkLetBinder rig pat ty val alts)
 
-  buildDoLets : FileName ->
-                List (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause) ->
-                List PDo
-  buildDoLets fname [] = []
-  buildDoLets fname ((start, end, rig, PRef fc' (UN n), ty, val, []) :: rest)
-      = let fc = MkFC fname start end in
-            if lowerFirst n
-               then DoLet fc (UN n) rig ty val :: buildDoLets fname rest
-               else DoLetPat fc (PRef fc' (UN n)) ty val []
-                         :: buildDoLets fname rest
-  buildDoLets fname ((start, end, rig, pat, ty, val, alts) :: rest)
-      = let fc = MkFC fname start end in
-            DoLetPat fc pat ty val alts :: buildDoLets fname rest
+    letDecl : Rule LetDecl
+    letDecl = collectDefs . concat <$> nonEmptyBlock (try . topDecl fname)
 
   let_ : FileName -> IndentInfo -> Rule PTerm
   let_ fname indents
-      = do b <- bounds (do keyword "let"
-                           res <- nonEmptyBlock (letBinder fname)
-                           commitKeyword indents "in"
-                           scope <- typeExpr pdef fname indents
-                           pure (res, scope))
-           (res, scope) <- pure b.val
-           pure (buildLets fname res scope)
-
-    <|> do b <- bounds (do keyword "let"
-                           commit
-                           ds <- nonEmptyBlock (topDecl fname)
-                           commitKeyword indents "in"
-                           scope <- typeExpr pdef fname indents
-                           pure (ds, scope))
-           (ds, scope) <- pure b.val
-           pure (PLocal (boundToFC fname b) (collectDefs (concat ds)) scope)
+      = do keyword "let"
+           commit
+           res <- nonEmptyBlock (letBlock fname)
+           commitKeyword indents "in"
+           scope <- typeExpr pdef fname indents
+           pure (mkLets fname res scope)
 
   case_ : FileName -> IndentInfo -> Rule PTerm
   case_ fname indents
@@ -695,10 +664,6 @@ mutual
                                      ns (concat actions.val))
                 _ => fail "Not a namespaced 'do'"
 
-  lowerFirst : String -> Bool
-  lowerFirst "" = False
-  lowerFirst str = assert_total (isLower (prim__strHead str))
-
   validPatternVar : Name -> SourceEmptyRule ()
   validPatternVar (UN n)
       = if lowerFirst n then pure ()
@@ -718,12 +683,10 @@ mutual
            (n, val) <- pure b.val
            pure [DoBind (boundToFC fname b) n val]
     <|> do keyword "let"
-           res <- block (letBinder fname)
+           commit
+           res <- nonEmptyBlock (letBlock fname)
            atEnd indents
-           pure (buildDoLets fname res)
-    <|> do b <- bounds (keyword "let" *> block (topDecl fname))
-           atEnd indents
-           pure [DoLetLocal (boundToFC fname b) (concat b.val)]
+           pure (mkDoLets fname res)
     <|> do b <- bounds (keyword "rewrite" *> expr pdef fname indents)
            atEnd indents
            pure [DoRewrite (boundToFC fname b) b.val]
@@ -831,7 +794,7 @@ mutual
                             symbol "("
                             wval <- bracketedExpr fname flags indents
                             ws <- nonEmptyBlock (clause (S withArgs) fname)
-                            pure (flags, wval, ws))
+                            pure (flags, wval, forget ws))
             (flags, wval, ws) <- pure b.val
             pure (MkWithClause (boundToFC fname (mergeBounds start b)) lhs wval flags.val ws)
      <|> do end <- bounds (keyword "impossible")
@@ -1177,10 +1140,6 @@ getVisibility (Just vis) (Left x :: xs)
    = fatalError "Multiple visibility modifiers"
 getVisibility v (_ :: xs) = getVisibility v xs
 
-getRight : Either a b -> Maybe b
-getRight (Left _) = Nothing
-getRight (Right v) = Just v
-
 constraints : FileName -> IndentInfo -> SourceEmptyRule (List (Maybe Name, PTerm))
 constraints fname indents
     = do tm <- appExpr pdef fname indents
@@ -1427,16 +1386,9 @@ topDecl fname indents
 -- collectDefs : List PDecl -> List PDecl
 collectDefs [] = []
 collectDefs (PDef annot cs :: ds)
-    = let (cs', rest) = spanMap isClause ds in
-          PDef annot (cs ++ cs') :: assert_total (collectDefs rest)
+    = let (cs', rest) = spanBy isClause ds in
+          PDef annot (cs ++ concat cs') :: assert_total (collectDefs rest)
   where
-    spanMap : (a -> Maybe (List b)) -> List a -> (List b, List a)
-    spanMap f [] = ([], [])
-    spanMap f (x :: xs) = case f x of
-                               Nothing => ([], x :: xs)
-                               Just y => case spanMap f xs of
-                                              (ys, zs) => (y ++ ys, zs)
-
     isClause : PDecl -> Maybe (List PClause)
     isClause (PDef annot cs)
         = Just cs

src/Idris/Parser/Let.idr

@@ -0,0 +1,90 @@
+module Idris.Parser.Let
+
+import Idris.Syntax
+import Text.Bounded
+
+import Data.Either
+import Data.List1
+
+import Utils.String
+
+%default total
+
+------------------------------------------------------------------------
+-- Types
+
+-- `let ... in ...` is used for two different notions:
+-- * pattern-matching let binders to locally take an expression apart
+-- * Local definitions that can be recursive
+
+public export
+record LetBinder where
+  constructor MkLetBinder
+  letUsage     : RigCount
+  letPattern   : PTerm
+  letBoundType : PTerm
+  letBoundTerm : PTerm
+  letUnhappy   : List PClause
+
+public export
+LetDecl : Type
+LetDecl = List PDecl
+
+------------------------------------------------------------------------
+-- Let-binding functions
+
+letFactory : (List (WithBounds LetBinder) -> a -> a) ->
+             (WithBounds LetDecl -> a -> a) ->
+             List1 (WithBounds (Either LetBinder LetDecl)) ->
+             a -> a
+letFactory letBind letDeclare blocks scope = foldr mkLet scope groups where
+
+  LetBlock : Type
+  LetBlock = Either (List1 (WithBounds LetBinder)) (List1 (WithBounds LetDecl))
+
+  groups : List LetBlock
+  groups = compress (forget $ map (\ b => bimap (<$ b) (<$ b) b.val) blocks)
+
+  mkLet : LetBlock -> a -> a
+  mkLet (Left  letBinds) = letBind (forget letBinds)
+  mkLet (Right letDecls) =
+    let bounds = mergeBounds (head letDecls) (last letDecls)
+    in letDeclare (concatMap val letDecls <$ bounds)
+
+export
+mkLets : FileName ->
+         List1 (WithBounds (Either LetBinder LetDecl)) ->
+         PTerm -> PTerm
+mkLets fname = letFactory buildLets
+  (\ decls, scope => PLocal (boundToFC fname decls) decls.val scope)
+
+  where
+
+    buildLets : List (WithBounds LetBinder) -> PTerm -> PTerm
+    buildLets [] sc = sc
+    buildLets (b :: rest) sc
+      = let (MkLetBinder rig pat ty val alts) = b.val
+            fc = boundToFC fname b
+        in PLet fc rig pat ty val (buildLets rest sc) alts
+
+export
+mkDoLets : FileName ->
+           List1 (WithBounds (Either LetBinder LetDecl)) ->
+           List PDo
+mkDoLets fname lets = letFactory
+    (\ binds, rest => buildDoLets binds ++ rest)
+    (\ decls, rest => DoLetLocal (boundToFC fname decls) decls.val :: rest)
+    lets
+    []
+
+  where
+
+    buildDoLets : List (WithBounds LetBinder) -> List PDo
+    buildDoLets [] = []
+    buildDoLets (b :: rest) = let fc = boundToFC fname b in case b.val of
+      (MkLetBinder rig (PRef fc' (UN n)) ty val []) =>
+         (if lowerFirst n
+            then DoLet fc (UN n) rig ty val
+            else DoLetPat fc (PRef fc' (UN n)) ty val []
+         ) :: buildDoLets rest
+      (MkLetBinder rig pat ty val alts) => DoLetPat fc pat ty val alts :: buildDoLets rest

src/Parser/Lexer/Source.idr

@@ -202,7 +202,7 @@ export
 reservedSymbols : List String
 reservedSymbols
     = symbols ++
-      ["%", "\\", ":", "=", "|", "|||", "<-", "->", "=>", "?", "!",
+      ["%", "\\", ":", "=", ":=", "|", "|||", "<-", "->", "=>", "?", "!",
        "&", "**", "..", "~"]
 
 fromBinLit : String -> Integer

src/Parser/Rule/Source.idr

@@ -5,6 +5,7 @@ import public Parser.Rule.Common
 import public Parser.Support
 
 import Core.TT
+import Data.List1
 import Data.Strings
 
 %default total
@@ -431,15 +432,15 @@ blockWithOptHeaderAfter {ty} mincol header item
                            pure (Nothing, ps)
 
 export
-nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty)
+nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List1 ty)
 nonEmptyBlock item
     = do symbol "{"
          commit
          res <- blockEntry AnyIndent item
          ps <- blockEntries (snd res) item
          symbol "}"
-         pure (fst res :: ps)
+         pure (fst res ::: ps)
   <|> do col <- column
          res <- blockEntry (AtPos col) item
          ps <- blockEntries (snd res) item
-         pure (fst res :: ps)
+         pure (fst res ::: ps)

src/TTImp/Parser.idr

@@ -504,7 +504,7 @@ mutual
            ws <- nonEmptyBlock (clause (S withArgs) fname)
            end <- location
            let fc = MkFC fname start end
-           pure (!(getFn lhs), WithClause fc lhs wval [] (map snd ws))
+           pure (!(getFn lhs), WithClause fc lhs wval [] (forget $ map snd ws))
 
     <|> do keyword "impossible"
            atEnd indents
@@ -683,7 +683,7 @@ topDecl fname indents
          ns <- namespaceDecl
          ds <- assert_total (nonEmptyBlock (topDecl fname))
          end <- location
-         pure (INamespace (MkFC fname start end) ns ds)
+         pure (INamespace (MkFC fname start end) ns (forget ds))
   <|> do start <- location
          visOpts <- many visOpt
          vis <- getVisibility Nothing visOpts
@@ -723,7 +723,7 @@ export
 prog : FileName -> Rule (List ImpDecl)
 prog fname
     = do ds <- nonEmptyBlock (topDecl fname)
-         pure (collectDefs ds)
+         pure (collectDefs $ forget ds)
 
 -- TTImp REPL commands
 export

src/TTImp/Utils.idr

@@ -7,11 +7,9 @@ import TTImp.TTImp
 import Data.List
 import Data.Strings
 
-%default covering
+import Utils.String
 
-lowerFirst : String -> Bool
-lowerFirst "" = False
-lowerFirst str = assert_total (isLower (prim__strHead str))
+%default covering
 
 export
 getUnique : List String -> String -> String

src/Text/Bounded.idr

@@ -34,6 +34,14 @@ export
 Functor WithBounds where
   map f (MkBounded val ir sl sc el ec) = MkBounded (f val) ir sl sc el ec
 
+export
+Foldable WithBounds where
+  foldr c n b = c b.val n
+
+export
+Traversable WithBounds where
+  traverse f (MkBounded v a b c d e) = (\ v => MkBounded v a b c d e) <$> f v
+
 export
 irrelevantBounds : ty -> WithBounds ty
 irrelevantBounds x = MkBounded x True (-1) (-1) (-1) (-1)

src/Text/Parser/Core.idr

@@ -23,6 +23,8 @@ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
      EOF : Grammar tok False ()
 
      Fail : Bool -> String -> Grammar tok c ty
+     Try : Grammar tok c ty -> Grammar tok c ty
+
      Commit : Grammar tok False ()
      MustWork : Grammar tok c a -> Grammar tok c a
 
@@ -67,21 +69,13 @@ join : {c1,c2 : Bool} ->
 join {c1 = False} p = SeqEmpty p id
 join {c1 = True} p = SeqEat p id
 
-||| Give two alternative grammars. If both consume, the combination is
-||| guaranteed to consume.
-export %inline
-(<|>) : {c1,c2 : Bool} -> 
-        Grammar tok c1 ty ->
-        Lazy (Grammar tok c2 ty) ->
-        Grammar tok (c1 && c2) ty
-(<|>) = Alt
-
 ||| Allows the result of a grammar to be mapped to a different value.
 export
 {c : _} ->
 Functor (Grammar tok c) where
   map f (Empty val)  = Empty (f val)
   map f (Fail fatal msg) = Fail fatal msg
+  map f (Try g) = Try (map f g)
   map f (MustWork g) = MustWork (map f g)
   map f (Terminal msg g) = Terminal msg (map f . g)
   map f (Alt x y)    = Alt (map f x) (map f y)
@@ -94,6 +88,25 @@ Functor (Grammar tok c) where
   -- so a sequence must be used.
   map {c = False} f p = SeqEmpty p (Empty . f)
 
+||| Give two alternative grammars. If both consume, the combination is
+||| guaranteed to consume.
+export %inline
+(<|>) : {c1,c2 : Bool} ->
+        Grammar tok c1 ty ->
+        Lazy (Grammar tok c2 ty) ->
+        Grammar tok (c1 && c2) ty
+(<|>) = Alt
+
+infixr 2 <||>
+||| Take the tagged disjunction of two grammars. If both consume, the
+||| combination is guaranteed to consume.
+export
+(<||>) : {c1,c2 : Bool} ->
+        Grammar tok c1 a ->
+        Lazy (Grammar tok c2 b) ->
+        Grammar tok (c1 && c2) (Either a b)
+(<||>) p q = (Left <$> p) <|> (Right <$> q)
+
 ||| Sequence a grammar with value type `a -> b` and a grammar
 ||| with value type `a`. If both succeed, apply the function
 ||| from the first grammar to the value from the second grammar.
@@ -132,6 +145,7 @@ mapToken f (Terminal msg g) = Terminal msg (g . map f)
 mapToken f (NextIs msg g) = SeqEmpty (NextIs msg (g . map f)) (Empty . f)
 mapToken f EOF = EOF
 mapToken f (Fail fatal msg) = Fail fatal msg
+mapToken f (Try g) = Try (mapToken f g)
 mapToken f (MustWork g) = MustWork (mapToken f g)
 mapToken f Commit = Commit
 mapToken f (SeqEat act next) = SeqEat (mapToken f act) (\x => mapToken f (next x))
@@ -169,6 +183,11 @@ export %inline
 fatalError : String -> Grammar tok c ty
 fatalError = Fail True
 
+||| Catch a fatal error
+export %inline
+try : Grammar tok c ty -> Grammar tok c ty
+try = Try
+
 ||| Succeed if the input is empty
 export %inline
 eof : Grammar tok False ()
@@ -202,6 +221,10 @@ mutual
             ParseResult tok ty
   doParse com (Empty val) xs = Res com (irrelevantBounds val) xs
   doParse com (Fail fatal str) xs = Failure com fatal str xs
+  doParse com (Try g) xs = case doParse com g xs of
+    -- recover from fatal match but still propagate the 'commit'
+    Failure com _ msg ts => Failure com False msg ts
+    res => res
   doParse com Commit xs = Res True (irrelevantBounds ()) xs
   doParse com (MustWork g) xs =
     case assert_total (doParse com g xs) of

src/Utils/String.idr

@@ -11,3 +11,8 @@ dotSep (x :: xs) = x ++ concat ["." ++ y | y <- xs]
 export
 stripQuotes : (str : String) -> String
 stripQuotes str = substr 1 (length str `minus` 2) str
+
+export
+lowerFirst : String -> Bool
+lowerFirst "" = False
+lowerFirst str = assert_total (isLower (prim__strHead str))

tests/Main.idr

@@ -42,7 +42,7 @@ idrisTests
        "basic031", "basic032", "basic033", "basic034", "basic035",
        "basic036", "basic037", "basic038", "basic039", "basic040",
        "basic041", "basic042", "basic043", "basic044", "basic045",
-       "basic046",
+       "basic046", "basic047",
        -- Coverage checking
        "coverage001", "coverage002", "coverage003", "coverage004",
        "coverage005", "coverage006", "coverage007", "coverage008",

tests/idris2/basic047/InterleavingLets.idr

@@ -0,0 +1,62 @@
+data Tag = MkTag
+
+data Elem :  a -> List a ->Type where
+  Z : Elem a (a :: as)
+  S : Elem a as -> Elem a (b :: as)
+
+toNat : Elem as a -> Nat
+toNat Z = 0
+toNat (S n) = 1 + toNat n
+
+Show (Elem as a) where
+  show = show . toNat
+
+data Subset : List a -> List a -> Type where
+  Nil  : Subset [] bs
+  (::) : Elem a bs -> Subset as bs -> Subset (a :: as) bs
+
+toList : Subset as bs -> List Nat
+toList [] = []
+toList (n :: ns) = toNat n :: toList ns
+
+Show (Subset as bs) where
+  show = show . toList
+
+search : {auto prf : a} -> a
+search = prf
+
+test : String
+test =
+  let x : Tag := MkTag
+      y : Tag := MkTag
+
+      as : List Tag
+      as = [y,x]
+
+      bs : List Tag
+      bs = [x,y,y]
+
+      prf : Subset as bs
+      prf = search
+
+      prf' : Subset as bs := search
+
+      eq : prf === [S (S Z), Z] := Refl
+
+--      eq' : prf' === [S (S Z), Z] := Refl
+-- ^ does not work because  prf' is opaque
+
+  in show prf
+
+
+reverse : List a -> List a
+reverse xs =
+  let revOnto : List a -> List a -> List a
+      revOnto acc [] = acc
+      revOnto acc (x :: xs) = revOnto (x :: acc) xs
+
+      rev := revOnto []
+
+      result := rev xs
+
+  in result

tests/idris2/basic047/expected

@@ -0,0 +1,3 @@
+1/1: Building InterleavingLets (InterleavingLets.idr)
+Main> "[2, 0]"
+Main> Bye for now!

tests/idris2/basic047/input

@@ -0,0 +1,2 @@
+test
+:q

tests/idris2/basic047/run

@@ -0,0 +1,3 @@
+$1 --no-banner --no-color --console-width 0 InterleavingLets.idr < input
+
+rm -rf build

tests/idris2/coverage006/foobar.idr

@@ -1,6 +1,6 @@
 foo : (pf : Nat -> Either (S Z = Z) (Z = S Z)) -> Z = S Z
 foo  pf =
- let baz : Z = S Z
+ let baz : Z === S Z
      baz  with (pf 0)
       baz | (Left Refl) impossible
       baz | (Right pf') = pf'

tests/idris2/perror003/PError2.idr

@@ -0,0 +1,8 @@
+foo : Int -> Int
+foo x = x
+
+bar : Int -> Int
+bar x = let y := (42 in y + x
+
+baz : Int -> Int
+baz x = x

tests/idris2/perror003/expected

@@ -1,3 +1,6 @@
 1/1: Building PError (PError.idr)
-Error: Parse error at line 5:17:
-Expected 'case', 'if', 'do', application or operator expression (next tokens: [symbol (, literal 42, in, identifier y, symbol +, identifier x, identifier baz, symbol :, identifier Int, symbol ->])
+Error: Parse error at line 5:9:
+Expected 'case', 'if', 'do', application or operator expression (next tokens: [let, identifier y, symbol =, symbol (, literal 42, in, identifier y, symbol +, identifier x, identifier baz])
+1/1: Building PError2 (PError2.idr)
+Error: Parse error at line 5:9:
+Expected 'case', 'if', 'do', application or operator expression (next tokens: [let, identifier y, symbol :=, symbol (, literal 42, in, identifier y, symbol +, identifier x, identifier baz])

tests/idris2/perror003/run

@@ -1,3 +1,4 @@
 $1 --no-color --console-width 0 --check PError.idr
+$1 --no-color --console-width 0 --check PError2.idr
 
 rm -rf build

tests/idris2/reflection001/expected

@@ -23,7 +23,7 @@ quote.idr:37:1--37:21
 
 Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IVar (MkFC "quote.idr" (3, 12) (3, 23)) (UN "+")) (IApp (MkFC "quote.idr" (6, 13) (6, 14)) (IVar (MkFC "quote.idr" (6, 13) (6, 14)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (6, 13) (6, 14)) (BI 3)))) (IApp (MkFC "quote.idr" (6, 18) (6, 19)) (IVar (MkFC "quote.idr" (6, 18) (6, 19)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (6, 18) (6, 19)) (BI 4)))
 Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IVar (MkFC "quote.idr" (3, 12) (3, 23)) (UN "+")) (IVar (MkFC "(interactive)" (0, 6) (0, 10)) (UN "True"))) (IVar (MkFC "(interactive)" (0, 14) (0, 19)) (UN "False"))
-Main> ILocal (MkFC "quote.idr" (10, 8) (12, 22)) [IClaim (MkFC "quote.idr" (10, 12) (11, 15)) MW Private [] (MkTy (MkFC "quote.idr" (10, 12) (10, 28)) (UN "xfn") (IPi (MkFC "quote.idr" (10, 18) (10, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (10, 18) (10, 21)) IntType) (IPrimVal (MkFC "quote.idr" (10, 25) (10, 28)) IntType))), IDef (MkFC "quote.idr" (11, 12) (11, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (11, 12) (11, 29)) (IApp (MkFC "quote.idr" (11, 12) (11, 19)) (IVar (MkFC "quote.idr" (11, 12) (11, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (11, 16) (11, 19)) "var")) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IVar (MkFC "quote.idr" (11, 22) (11, 29)) (UN "*")) (IVar (MkFC "quote.idr" (11, 22) (11, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (11, 28) (11, 29)) (IVar (MkFC "quote.idr" (11, 28) (11, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (12, 12) (12, 22)) (IVar (MkFC "quote.idr" (12, 12) (12, 15)) (UN "xfn")) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IVar (MkFC "(interactive)" (0, 9) (0, 12)) (UN "the")) (IPrimVal (MkFC "(interactive)" (0, 13) (0, 16)) IntType)) (IApp (MkFC "(interactive)" (0, 17) (0, 22)) (IVar (MkFC "(interactive)" (0, 17) (0, 22)) (UN "fromInteger")) (IPrimVal (MkFC "(interactive)" (0, 17) (0, 22)) (BI 99994)))))
-Main> ILocal (MkFC "quote.idr" (16, 8) (18, 43)) [IClaim (MkFC "quote.idr" (16, 12) (17, 15)) MW Private [] (MkTy (MkFC "quote.idr" (16, 12) (16, 28)) (UN "xfn") (IPi (MkFC "quote.idr" (16, 18) (16, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (16, 18) (16, 21)) IntType) (IPrimVal (MkFC "quote.idr" (16, 25) (16, 28)) IntType))), IDef (MkFC "quote.idr" (17, 12) (17, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (17, 12) (17, 29)) (IApp (MkFC "quote.idr" (17, 12) (17, 19)) (IVar (MkFC "quote.idr" (17, 12) (17, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (17, 16) (17, 19)) "var")) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IVar (MkFC "quote.idr" (17, 22) (17, 29)) (UN "*")) (IVar (MkFC "quote.idr" (17, 22) (17, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (17, 28) (17, 29)) (IVar (MkFC "quote.idr" (17, 28) (17, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (18, 12) (18, 43)) (IVar (MkFC "quote.idr" (18, 12) (18, 15)) (UN "xfn")) (IPrimVal EmptyFC (I 99994)))
+Main> ILocal (MkFC "quote.idr" (10, 12) (11, 32)) [IClaim (MkFC "quote.idr" (10, 12) (11, 15)) MW Private [] (MkTy (MkFC "quote.idr" (10, 12) (10, 28)) (UN "xfn") (IPi (MkFC "quote.idr" (10, 18) (10, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (10, 18) (10, 21)) IntType) (IPrimVal (MkFC "quote.idr" (10, 25) (10, 28)) IntType))), IDef (MkFC "quote.idr" (11, 12) (11, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (11, 12) (11, 29)) (IApp (MkFC "quote.idr" (11, 12) (11, 19)) (IVar (MkFC "quote.idr" (11, 12) (11, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (11, 16) (11, 19)) "var")) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IVar (MkFC "quote.idr" (11, 22) (11, 29)) (UN "*")) (IVar (MkFC "quote.idr" (11, 22) (11, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (11, 28) (11, 29)) (IVar (MkFC "quote.idr" (11, 28) (11, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (12, 12) (12, 22)) (IVar (MkFC "quote.idr" (12, 12) (12, 15)) (UN "xfn")) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IVar (MkFC "(interactive)" (0, 9) (0, 12)) (UN "the")) (IPrimVal (MkFC "(interactive)" (0, 13) (0, 16)) IntType)) (IApp (MkFC "(interactive)" (0, 17) (0, 22)) (IVar (MkFC "(interactive)" (0, 17) (0, 22)) (UN "fromInteger")) (IPrimVal (MkFC "(interactive)" (0, 17) (0, 22)) (BI 99994)))))
+Main> ILocal (MkFC "quote.idr" (16, 12) (17, 32)) [IClaim (MkFC "quote.idr" (16, 12) (17, 15)) MW Private [] (MkTy (MkFC "quote.idr" (16, 12) (16, 28)) (UN "xfn") (IPi (MkFC "quote.idr" (16, 18) (16, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (16, 18) (16, 21)) IntType) (IPrimVal (MkFC "quote.idr" (16, 25) (16, 28)) IntType))), IDef (MkFC "quote.idr" (17, 12) (17, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (17, 12) (17, 29)) (IApp (MkFC "quote.idr" (17, 12) (17, 19)) (IVar (MkFC "quote.idr" (17, 12) (17, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (17, 16) (17, 19)) "var")) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IVar (MkFC "quote.idr" (17, 22) (17, 29)) (UN "*")) (IVar (MkFC "quote.idr" (17, 22) (17, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (17, 28) (17, 29)) (IVar (MkFC "quote.idr" (17, 28) (17, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (18, 12) (18, 43)) (IVar (MkFC "quote.idr" (18, 12) (18, 15)) (UN "xfn")) (IPrimVal EmptyFC (I 99994)))
 Main> [UN "names", NS (MkNS ["Prelude"]) (UN "+")]
 Main> Bye for now!