Literate programming

- Add support for .lidr files.
- Add new Parse Error for Literate fails.
- Add support for Case Split.
- Add support for Add Clause.
- Add support for Add Lemma.
- Add tests.

idris2.ipkg

@@ -73,6 +73,7 @@ modules =
 
     Parser.Lexer,
     Parser.Support,
+    Parser.Unlit,
 
     Text.Lexer,
     Text.Lexer.Core,

src/Idris/IDEMode/CaseSplit.idr

@@ -6,6 +6,8 @@ import Core.Metadata
 import Core.TT
 import Core.Value
 
+import Parser.Unlit
+
 import TTImp.Interactive.CaseSplit
 import TTImp.TTImp
 import TTImp.Utils
@@ -164,6 +166,7 @@ fnName lhs n = show n
 export
 getClause : {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
+            {auto o : Ref ROpts REPLOpts} ->
             Int -> Name -> Core (Maybe String)
 getClause l n
     = do defs <- get Ctxt
@@ -171,8 +174,12 @@ getClause l n
              | Nothing => pure Nothing
          n <- getFullName nidx
          argns <- getEnvArgNames defs envlen !(nf defs [] ty)
-         pure (Just (indent loc ++ fnName True n ++ concat (map (" " ++) argns) ++
+         Just srcLine <- getSourceLine l
+           | Nothing => pure Nothing
+         let (lit, src) = isLit srcLine
+         pure (Just (indent lit loc ++ fnName True n ++ concat (map (" " ++) argns) ++
                   " = ?" ++ fnName False n ++ "_rhs"))
   where
-    indent : FC -> String
-    indent fc = pack (replicate (cast (snd (startPos fc))) ' ')
+    indent : Bool -> FC -> String
+    indent True fc = ">" ++ pack (replicate (cast (max 0 (snd (startPos fc) - 1))) ' ')
+    indent False fc = pack (replicate (cast (snd (startPos fc))) ' ')

src/Idris/IDEMode/MakeClause.idr

@@ -2,16 +2,10 @@ module Idris.IDEMode.MakeClause
 
 import Core.Name
 import Parser.Lexer
+import Parser.Unlit
 
 -- Implement make-with and make-case from the IDE mode
 
-isLit : String -> (Bool, String)
-isLit str
-    = assert_total $
-         if length str > 0 && strHead str == '>'
-            then (True, strTail str)
-            else (False, str)
-
 showRHSName : Name -> String
 showRHSName n
     = let fn = show (dropNS n) in

src/Idris/IDEMode/REPL.idr

@@ -258,7 +258,7 @@ displayIDEResult outf i  (VersionIs x) = printIDEResult outf i versionSExp
 
 displayIDEResult outf i  (Edited (DisplayEdit xs)) = printIDEResult outf i $ StringAtom $ showSep "\n" xs
 displayIDEResult outf i  (Edited (EditError x)) = printIDEError outf i x
-displayIDEResult outf i  (Edited (MadeLemma name pty pappstr)) = printIDEResult outf i $ StringAtom $ show name ++ " : " ++ show pty ++ "\n" ++ pappstr
+displayIDEResult outf i  (Edited (MadeLemma lit name pty pappstr)) = printIDEResult outf i $ StringAtom $ (if lit then "> " else "") ++ show name ++ " : " ++ show pty ++ "\n" ++ pappstr
 displayIDEResult outf i  _ = pure ()
 
 

src/Idris/ProcessIdr.idr

@@ -9,6 +9,8 @@ import Core.Metadata
 import Core.Options
 import Core.Unify
 
+import Parser.Unlit
+
 import TTImp.Elab.Check
 import TTImp.TTImp
 
@@ -192,6 +194,7 @@ export
 getParseErrorLoc : String -> ParseError -> FC
 getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos
 getParseErrorLoc fname (LexFail (l, c, _)) = MkFC fname (l, c) (l, c)
+getParseErrorLoc fname (LitFail (l :: _)) = MkFC fname (l, 0) (l, 0)
 getParseErrorLoc fname _ = replFC
 
 export
@@ -200,7 +203,7 @@ readHeader : {auto c : Ref Ctxt Defs} ->
 readHeader path
     = do Right res <- coreLift (readFile path)
             | Left err => throw (FileErr path err)
-         case runParserTo isColon res (progHdr path) of
+         case runParserTo (isLitFile path) False isColon res (progHdr path) of
               Left err => throw (ParseFail (getParseErrorLoc path err) err)
               Right mod => pure mod
   where
@@ -258,7 +261,7 @@ processMod srcf ttcf msg sourcecode
            else -- needs rebuilding
              do iputStrLn msg
                 Right mod <- logTime ("Parsing " ++ srcf) $
-                            pure (runParser sourcecode (do p <- prog srcf; eoi; pure p))
+                            pure (runParser (isLitFile srcf) True sourcecode (do p <- prog srcf; eoi; pure p))
                       | Left err => pure (Just [ParseFail (getParseErrorLoc srcf err) err])
                 initHash
                 resetNextVar

src/Idris/REPL.idr

@@ -19,6 +19,8 @@ import Core.Termination
 import Core.TT
 import Core.Unify
 
+import Parser.Unlit
+
 import Idris.Desugar
 import Idris.Error
 import Idris.IDEMode.CaseSplit
@@ -242,21 +244,22 @@ anyAt p loc y = p loc
 
 printClause : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->
-              Nat -> ImpClause ->
+              Bool -> Nat -> ImpClause ->
               Core String
-printClause i (PatClause _ lhsraw rhsraw)
+printClause l i (PatClause _ lhsraw rhsraw)
     = do lhs <- pterm lhsraw
          rhs <- pterm rhsraw
-         pure (pack (replicate i ' ') ++ show lhs ++ " = " ++ show rhs)
-printClause i (WithClause _ lhsraw wvraw csraw)
+         pure ((if l then ">" else "") ++ (pack (replicate i ' ') ++ show lhs ++ " = " ++ show rhs))
+printClause l i (WithClause _ lhsraw wvraw csraw)
     = do lhs <- pterm lhsraw
          wval <- pterm wvraw
-         cs <- traverse (printClause (i + 2)) csraw
-         pure (pack (replicate i ' ') ++ show lhs ++ " with (" ++ show wval ++ ")\n" ++
-                 showSep "\n" cs)
-printClause i (ImpossibleClause _ lhsraw)
+         cs <- traverse (printClause l (i + 2)) csraw
+         pure ((if l then ">" else "") ++ (pack (replicate i ' ') ++ show lhs ++ " with (" ++ show wval ++ ")\n" ++
+                 showSep "\n" cs))
+printClause l i (ImpossibleClause _ lhsraw)
     = do lhs <- pterm lhsraw
-         pure (pack (replicate i ' ') ++ show lhs ++ " impossible")
+         pure ((if l then ">" else "") ++ (pack (replicate i ' ') ++ show lhs ++ " impossible"))
+
 
 lookupDefTyName : Name -> Context ->
                   Core (List (Name, Int, (Def, ClosedTerm)))
@@ -266,7 +269,7 @@ public export
 data EditResult : Type where
   DisplayEdit : List String -> EditResult
   EditError : String -> EditResult
-  MadeLemma : Name -> PTerm -> String -> EditResult
+  MadeLemma : Bool -> Name -> PTerm -> String -> EditResult
 
 updateFile : {auto r : Ref ROpts REPLOpts} ->
              (List String -> List String) -> Core EditResult
@@ -306,22 +309,22 @@ proofSearch n res Z (x :: xs) = replaceStr ("?" ++ show n) res x :: xs
 proofSearch n res (S k) (x :: xs) = x :: proofSearch n res k xs
 proofSearch n res _ [] = []
 
-addMadeLemma : Name -> String -> String -> Nat -> List String -> List String
-addMadeLemma n ty app line content
-    = addApp line [] (proofSearch n app line content)
+addMadeLemma : Bool -> Name -> String -> String -> Nat -> List String -> List String
+addMadeLemma lit n ty app line content
+    = addApp lit line [] (proofSearch n app line content)
   where
     -- Put n : ty in the first blank line
-    insertInBlank : List String -> List String
-    insertInBlank [] = [show n ++ " : " ++ ty ++ "\n"]
-    insertInBlank (x :: xs)
+    insertInBlank : Bool -> List String -> List String
+    insertInBlank lit [] = [(if lit then "> " else "") ++ show n ++ " : " ++ ty ++ "\n"]
+    insertInBlank lit (x :: xs)
         = if trim x == ""
-             then ("\n" ++ show n ++ " : " ++ ty ++ "\n") :: xs
-             else x :: insertInBlank xs
+             then ("\n" ++ (if lit then "> " else "") ++ show n ++ " : " ++ ty ++ "\n") :: xs
+             else x :: insertInBlank lit xs
 
-    addApp : Nat -> List String -> List String -> List String
-    addApp Z acc rest = reverse (insertInBlank acc) ++ rest
-    addApp (S k) acc (x :: xs) = addApp k (x :: acc) xs
-    addApp (S k) acc [] = reverse acc
+    addApp : Bool -> Nat -> List String -> List String -> List String
+    addApp lit Z acc rest = reverse (insertInBlank lit acc) ++ rest
+    addApp lit (S k) acc (x :: xs) = addApp lit k (x :: acc) xs
+    addApp _ (S k) acc [] = reverse acc
 
 processEdit : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
@@ -413,11 +416,15 @@ processEdit (GenerateDef upd line name)
                   catch
                     (do Just (fc, cs) <- makeDef (\p, n => onLine line p) n'
                            | Nothing => processEdit (AddClause upd line name)
-                        ls <- traverse (printClause (cast (snd (startPos fc)))) cs
+                        Just srcLine <- getSourceLine line
+                           | Nothing => pure (EditError "Source line not found")
+                        let (lit, _) = isLit srcLine
+                        let l : Nat = if lit then cast (max 0 (snd (startPos fc) - 1)) else cast (snd (startPos fc))
+                        ls <- traverse (printClause lit l) cs
                         if upd
                            then updateFile (addClause (unlines ls) (cast line))
                            else pure $ DisplayEdit ls)
-                    (\err => pure $ EditError $ "Can't find a definition for " ++ show n')
+                    (\err => pure $ EditError $ "Can't find a definition for " ++ show n' ++ ": " ++ show err)
               Just _ => pure $ EditError "Already defined"
               Nothing => pure $ EditError $ "Can't find declaration for " ++ show name
 processEdit (MakeLemma upd line name)
@@ -433,10 +440,13 @@ processEdit (MakeLemma upd line name)
                      let pappstr = show (if brack
                                             then addBracket replFC papp
                                             else papp)
+                     Just srcLine <- getSourceLine line
+                       | Nothing => pure (EditError "Source line not found")
+                     let (lit, _) = isLit srcLine
                      if upd
-                        then updateFile (addMadeLemma name (show pty) pappstr
+                        then updateFile (addMadeLemma lit name (show pty) pappstr
                                                       (cast (line - 1)))
-                        else pure $ MadeLemma name pty pappstr
+                        else pure $ MadeLemma lit name pty pappstr
               _ => pure $ EditError "Can't make lifted definition"
 processEdit (MakeCase upd line name)
     = pure $ EditError "Not implemented yet"
@@ -720,7 +730,7 @@ export
 parseRepl : String -> Either ParseError (Maybe REPLCmd)
 parseRepl inp
     = case fnameCmd [(":load ", Load), (":l ", Load), (":cd ", CD)] inp of
-           Nothing => runParser inp (parseEmptyCmd <|> parseCmd)
+           Nothing => runParser False False inp (parseEmptyCmd <|> parseCmd)
            Just cmd => Right $ Just cmd
   where
     -- a right load of hackery - we can't tokenise the filename using the
@@ -836,7 +846,7 @@ mutual
   displayResult  (Edited (DisplayEdit [])) = pure ()
   displayResult  (Edited (DisplayEdit xs)) = printResult $ showSep "\n" xs
   displayResult  (Edited (EditError x)) = printError x
-  displayResult  (Edited (MadeLemma name pty pappstr)) = printResult (show name ++ " : " ++ show pty ++ "\n" ++ pappstr)
+  displayResult  (Edited (MadeLemma lit name pty pappstr)) = printResult ((if lit then "> " else "") ++ show name ++ " : " ++ show pty ++ "\n" ++ pappstr)
   displayResult  (OptionsSet opts) = printResult $ showSep "\n" $ map show opts
   displayResult  _ = pure ()
 

src/Parser/Support.idr

@@ -2,6 +2,7 @@ module Parser.Support
 
 import public Text.Lexer
 import public Parser.Lexer
+import public Parser.Unlit
 import public Text.Parser
 
 import Core.TT
@@ -21,6 +22,7 @@ public export
 data ParseError = ParseFail String (Maybe (Int, Int)) (List Token)
                 | LexFail (Int, Int, String)
                 | FileFail FileError
+                | LitFail (List Int)
 
 export
 Show ParseError where
@@ -31,6 +33,8 @@ Show ParseError where
       = "Lex error at " ++ show (c, l) ++ " input: " ++ str
   show (FileFail err)
       = "File error: " ++ show err
+  show (LitFail l)
+      = "Lit error(s) at " ++ show l
 
 export
 eoi : EmptyRule ()
@@ -43,30 +47,33 @@ eoi
     isEOI _ = False
 
 export
-runParserTo : (TokenData Token -> Bool) ->
+runParserTo : Bool -> Bool -> (TokenData Token -> Bool) ->
               String -> Grammar (TokenData Token) e ty -> Either ParseError ty
-runParserTo pred str p
-    = case lexTo pred str of
-           Left err => Left $ LexFail err
-           Right toks =>
-              case parse p toks of
-                   Left (Error err []) =>
-                          Left $ ParseFail err Nothing []
-                   Left (Error err (t :: ts)) =>
-                          Left $ ParseFail err (Just (line t, col t))
-                                               (map tok (t :: ts))
-                   Right (val, _) => Right val
+runParserTo lit enforce pred str p
+    = case unlit lit enforce str of
+           Left l => Left $ LitFail l
+           Right str =>
+             case lexTo pred str of
+               Left err => Left $ LexFail err
+               Right toks =>
+                  case parse p toks of
+                       Left (Error err []) =>
+                              Left $ ParseFail err Nothing []
+                       Left (Error err (t :: ts)) =>
+                              Left $ ParseFail err (Just (line t, col t))
+                                                   (map tok (t :: ts))
+                       Right (val, _) => Right val
 
 export
-runParser : String -> Grammar (TokenData Token) e ty -> Either ParseError ty
-runParser = runParserTo (const False)
+runParser : Bool -> Bool -> String -> Grammar (TokenData Token) e ty -> Either ParseError ty
+runParser lit enforce = runParserTo lit enforce (const False)
 
 export
 parseFile : (fn : String) -> Rule ty -> IO (Either ParseError ty)
 parseFile fn p
     = do Right str <- readFile fn
              | Left err => pure (Left (FileFail err))
-         pure (runParser str p)
+         pure (runParser (isLitFile fn) True str p)
 
 
 -- Some basic parsers used by all the intermediate forms

src/Parser/Unlit.idr

@@ -0,0 +1,44 @@
+module Parser.Unlit
+
+%default total
+
+export
+isLitFile : String -> Bool
+isLitFile file = isSuffixOf ".lidr" file
+
+data LineType = Blank | Code | Text
+
+lineType : String -> (LineType, String)
+lineType str = if length str > 0
+  then
+    if assert_total (strHead str) == '>'
+       then (Code, assert_total (strTail str))
+       else
+         if all isSpace (unpack str)
+            then (Blank, str)
+            else (Text, str)
+  else (Blank, str)
+
+export
+isLit : String -> (Bool, String)
+isLit str = case lineType str of
+               (Code, tail) => (True, tail)
+               _ => (False, str)
+
+export
+unlit : Bool -> Bool -> String -> Either (List Int) String
+unlit lit enforce str = if lit
+  then let (_, lns, errors) = foldr unlit' (Blank, [], []) (lines str) in
+           if enforce
+              then case errors of
+                        [] => Right (unlines lns)
+                        _ => let l : Int = cast (length lns) in Left (map (l -) errors)
+              else Right (unlines lns)
+  else Right str where
+    unlit' : String -> (LineType, List String, List Int) -> (LineType, List String, List Int)
+    unlit' str (type, ls, errs) with (lineType str)
+      unlit' str (Code, ls, errs) | (Text, _) = (Text, "" :: ls, cast (length ls) :: errs)
+      unlit' str (Text, ls, errs) | (Code, s) = (Code, (strCons ' ' s) :: ls, cast (length ls) :: errs)
+      unlit' str (type, ls, errs) | (Code, s) = (Code, (strCons ' ' s) :: ls, errs)
+      unlit' str (type, ls, errs) | (new, s) = (new, "" :: ls, errs)
+

src/Yaffle/REPL.idr

@@ -151,7 +151,7 @@ repl : {auto c : Ref Ctxt Defs} ->
 repl
     = do coreLift (putStr "Yaffle> ")
          inp <- coreLift getLine
-         case runParser inp command of
+         case runParser False False inp command of
               Left err => do coreLift (printLn err)
                              repl
               Right cmd =>

tests/Main.idr

@@ -44,6 +44,10 @@ idrisTests
        "interactive001", "interactive002", "interactive003", "interactive004",
        "interactive005", "interactive006", "interactive007", "interactive008",
        "interactive009", "interactive010", "interactive011", "interactive012",
+       -- Literate
+       "literate001", "literate002", "literate003", "literate004",
+       "literate005", "literate006", "literate007", "literate008",
+       "literate009",
        -- Interfaces
        "interface001", "interface002", "interface003", "interface004",
        "interface005", "interface006", "interface007", "interface008",

tests/idris2/literate001/IEdit.lidr

@@ -0,0 +1,19 @@
+> data Vect : Nat -> Type -> Type where
+>      Nil : Vect Z a
+>      (::) : a -> Vect k a -> Vect (S k) a
+
+> %name Vect xs, ys, zs
+
+> append : Vect n a -> Vect m a -> Vect (n + m) a
+> append {n} xs ys = ?foo
+
+> vadd : Num a => Vect n a -> Vect n a -> Vect n a
+> vadd [] ys = ?bar
+> vadd (x :: xs) ys = ?baz
+
+> suc : (x : Nat) -> (y : Nat) -> x = y -> S x = S y
+> suc x y prf = ?quux
+
+> suc' : x = y -> S x = S y
+> suc' {x} {y} prf = ?quuz
+

tests/idris2/literate001/expected

@@ -0,0 +1,8 @@
+1/1: Building IEdit (IEdit.lidr)
+Main> > append {n = Z} [] ys = ?foo_1
+> append {n = (S k)} (x :: xs) ys = ?foo_2
+Main> > vadd [] [] = ?bar_1
+Main> > vadd (x :: xs) (y :: ys) = ?baz_1
+Main> > suc x x Refl = ?quux_1
+Main> > suc' {x = y} {y = y} Refl = ?quuz_1
+Main> Bye for now!

tests/idris2/literate001/input

@@ -0,0 +1,6 @@
+:cs 8 14 xs
+:cs 11 11 ys
+:cs 12 18 ys
+:cs 15 12 prf
+:cs 18 16 prf
+:q

tests/idris2/literate001/run

@@ -0,0 +1,3 @@
+$1 --no-banner IEdit.lidr < input
+
+rm -rf build

tests/idris2/literate002/IEdit.lidr

@@ -0,0 +1,15 @@
+> data Vect : Nat -> Type -> Type where
+>      Nil : Vect Z a
+>      (::) : a -> Vect k a -> Vect (S k) a
+
+> %name Vect xs, ys, zs
+
+> append : Vect n a -> Vect m a -> Vect (n + m) a
+> append xs ys
+>     = case xs of
+>            foo => ?bar
+
+> data Foo a = MkFoo a | MkBar (a -> a)
+
+> Functor Foo where
+>   map f thing = ?baz

tests/idris2/literate002/IEdit2.lidr

@@ -0,0 +1,12 @@
+> data Vect : Nat -> Type -> Type where
+>      Nil : Vect Z a
+>      (::) : a -> Vect k a -> Vect (S k) a
+
+> %name Vect xs, ys, zs
+
+> append : Vect n a -> Vect m a -> Vect (n + m) a
+> append xs ys
+>     = case xs of
+>            [] => ?bar_3
+>            (x :: zs) => ?bar_4
+

tests/idris2/literate002/expected

@@ -0,0 +1,10 @@
+1/1: Building IEdit (IEdit.lidr)
+Main> >            [] => ?bar_1
+>            (x :: zs) => ?bar_2
+Main> >   map f (MkFoo x) = ?baz_1
+>   map f (MkBar g) = ?baz_2
+Main> Bye for now!
+1/1: Building IEdit2 (IEdit2.lidr)
+Main> >            (x :: []) => ?bar_5
+>            (x :: (y :: zs)) => ?bar_6
+Main> Bye for now!

tests/idris2/literate002/input

@@ -0,0 +1,3 @@
+:cs 10 16 foo
+:cs 15 15 thing
+:q

tests/idris2/literate002/input2

@@ -0,0 +1,2 @@
+:cs 11 20 zs
+:q

tests/idris2/literate002/run

@@ -0,0 +1,4 @@
+$1 --no-banner IEdit.lidr < input
+$1 --no-banner IEdit2.lidr < input2
+
+rm -rf build

tests/idris2/literate003/IEdit.lidr

@@ -0,0 +1,29 @@
+> data Vect : Nat -> Type -> Type where
+>      Nil : Vect Z a
+>      (::) : a -> Vect k a -> Vect (S k) a
+
+> %name Vect xs, ys, zs
+
+> my_cong : forall f . (x : a) -> (y : a) -> x = y -> f x = f y
+
+> my_curry : ((a, b) -> c) -> a -> b -> c
+
+> my_uncurry : (a -> b -> c) -> (a, b) -> c
+
+> append : Vect n a -> Vect m a -> Vect (n + m) a
+
+> lappend : (1 xs : List a) -> (1 ys : List a) -> List a
+
+> zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
+
+> data Env : Vect n Type -> Type where
+>      ENil : Env []
+>      ECons : a -> Env xs -> Env (a :: xs)
+
+> %name Env es
+
+> data Elem : a -> Vect n a -> Type where
+>      Here : Elem x (x :: xs)
+>      There : (p : Elem x xs) -> Elem x (y :: xs)
+
+> lookup : Elem ty vs -> Env vs -> ty

tests/idris2/literate003/expected

@@ -0,0 +1,14 @@
+1/1: Building IEdit (IEdit.lidr)
+Main> > my_cong x x Refl = Refl
+Main> > my_curry f x y = f (x, y)
+Main> > my_uncurry f x = f (fst x) (snd x)
+Main> > append [] ys = ys
+> append (x :: xs) ys = x :: append xs ys
+Main> > lappend [] ys = ys
+> lappend (x :: xs) ys = x :: lappend xs ys
+Main> > zipWith f [] ys = []
+> zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
+Main> > lookup Here (ECons x es) = x
+> lookup (There p) (ECons x es) = lookup p es
+Main> Main.my_uncurry : (a -> b -> c) -> (a, b) -> c
+Main> Bye for now!

tests/idris2/literate003/input

@@ -0,0 +1,9 @@
+:gd 7 my_cong
+:gd 9 my_curry
+:gd 11 my_uncurry
+:gd 13 append
+:gd 15 lappend
+:gd 17 zipWith
+:gd 29 lookup
+:t my_uncurry
+:q

tests/idris2/literate003/run

@@ -0,0 +1,3 @@
+$1 --no-banner IEdit.lidr < input
+
+rm -rf build

tests/idris2/literate004/IEdit.lidr

@@ -0,0 +1,10 @@
+> data Vect : Nat -> Type -> Type where
+>      Nil : Vect Z a
+>      (::) : a -> Vect k a -> Vect (S k) a
+
+> %name Vect xs, ys, zs
+
+> transpose : {m : Nat} -> Vect n (Vect m a) -> Vect m (Vect n a)
+> transpose [] = ?empties
+> transpose (x :: xs) = let xs_trans = transpose xs in
+>                           ?transposeHelper

tests/idris2/literate004/expected

@@ -0,0 +1,6 @@
+1/1: Building IEdit (IEdit.lidr)
+Main> > empties : (m : Nat) -> Vect m (Vect Z a)
+empties m
+Main> > transposeHelper : Vect m a -> Vect k (Vect m a) -> Vect m (Vect k a) -> Vect m (Vect (S k) a)
+transposeHelper x xs xs_trans
+Main> Bye for now!

tests/idris2/literate004/input

@@ -0,0 +1,3 @@
+:ml 8 empties
+:ml 10 transposeHelper
+:q

tests/idris2/literate004/run

@@ -0,0 +1,3 @@
+$1 --no-banner IEdit.lidr < input
+
+rm -rf build

tests/idris2/literate005/IEdit.lidr

@@ -0,0 +1,7 @@
+> data Vect : Nat -> Type -> Type where
+>      Nil : Vect Z a
+>      (::) : a -> Vect k a -> Vect (S k) a
+
+> %name Vect xs, ys, zs
+
+> transposeHelper : Vect m a -> (1 xs_trans : Vect m (Vect k a)) -> Vect m (Vect (S k) a)

tests/idris2/literate005/expected

@@ -0,0 +1,4 @@
+1/1: Building IEdit (IEdit.lidr)
+Main> > transposeHelper [] [] = []
+> transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys
+Main> Bye for now!

tests/idris2/literate005/input

@@ -0,0 +1,2 @@
+:gd 7 transposeHelper
+:q

tests/idris2/literate005/run

@@ -0,0 +1,3 @@
+$1 --no-banner IEdit.lidr < input
+
+rm -rf build

tests/idris2/literate006/Door.lidr

@@ -0,0 +1,69 @@
+> data Usage = Once | Many
+
+> data Use : Usage -> (Type -> Type) -> Type -> Type where
+>      Pure : (1 x : a) -> Use t m a
+>      BindOnce : (1 act : Use Once m a) -> (1 k : (1 x : a) -> Use t m b) -> Use t m b
+>      BindMany : (1 act : Use Many m a) -> (1 k : (x : a) -> Use t m b) -> Use t m b
+
+> contType : (Type -> Type) -> Usage -> Usage -> Type -> Type -> Type
+> contType m Once q a b = ((1 x : a) -> Use q m b)
+> contType m Many q a b = ((x : a) -> Use q m b)
+
+> (>>=) : {p : _} -> (1 f : Use p m a) -> (1 k : contType m p q a b) -> Use q m b
+> (>>=) {p = Once} = BindOnce
+> (>>=) {p = Many} = BindMany
+
+> pure : (1 x : a) -> Use t m a
+> pure = Pure
+
+> One : (Type -> Type) -> Type -> Type
+> One = Use Once
+
+> Any : (Type -> Type) -> Type -> Type
+> Any = Use Many
+
+> infix 2 @@
+
+> data Res : (a : Type) -> (a -> Type) -> Type where
+>      (@@) : (x : a) -> (1 res : r x) -> Res a r
+
+> data DoorState = Closed | Open
+
+> data Door : DoorState -> Type where
+>      MkDoor : (isOpen : Bool) -> Door (if isOpen then Open else Closed)
+
+> newDoor : One m (Door Closed)
+> newDoor = pure (MkDoor False)
+
+> knock : (1 d : Door Closed) -> One m (Door Closed)
+> openDoor : (1 d : Door Closed) ->
+>            One m (Res Bool (\r => Door (if r then Open else Closed)))
+
+> closeDoor : (1 d : Door Open) -> One m (Door Closed)
+
+> deleteDoor : (1 d : Door Closed) -> Any m ()
+
+> doorProg : Any m ()
+> doorProg
+>     = do d <- newDoor
+>          r <- openDoor d
+>          let x = 42
+>          case r of
+>               what => ?now
+
+> doorProg2 : Any m ()
+> doorProg2
+>     = do d <- newDoor
+>          r <- openDoor d
+>          let x = 42
+>          case r of
+>               (res @@ d) => ?now_1
+
+> doorProg3 : Any m ()
+> doorProg3
+>     = do d <- newDoor
+>          r <- openDoor d
+>          let x = 42
+>          case r of
+>               (True @@ d) => ?now_2
+>               (False @@ d) => ?now_3

tests/idris2/literate006/expected

@@ -0,0 +1,17 @@
+1/1: Building Door (Door.lidr)
+Main> >               (y @@ res) => ?now_4
+Main> >               (True @@ d) => ?now_4
+>               (False @@ d) => ?now_5
+Main>  0 m : Type -> Type
+ 1 d : Door Open
+   x : Integer
+ 0 r : Res Bool (\r => (Door (if r then Open else Closed)))
+-------------------------------------
+now_2 : Use Many m ()
+Main>  0 m : Type -> Type
+ 1 d : Door Closed
+   x : Integer
+ 0 r : Res Bool (\r => (Door (if r then Open else Closed)))
+-------------------------------------
+now_3 : Use Many m ()
+Main> Bye for now!

tests/idris2/literate006/input

@@ -0,0 +1,5 @@
+:cs 52 17 what
+:cs 60 18 res
+:t now_2
+:t now_3
+:q

tests/idris2/literate006/run

@@ -0,0 +1,3 @@
+$1 --no-banner Door.lidr < input
+
+rm -rf build

tests/idris2/literate007/IEdit.lidr

@@ -0,0 +1,11 @@
+> data Vect : Nat -> Type -> Type where
+>      Nil : Vect Z a
+>      (::) : a -> Vect k a -> Vect (S k) a
+
+> %name Vect xs, ys, zs
+
+> dupAll : Vect n a -> Vect n (a, a)
+> dupAll xs = zipHere xs xs
+>   where
+>     zipHere : forall n . Vect n a -> Vect n b -> Vect n (a, b)
+

tests/idris2/literate007/expected

@@ -0,0 +1,4 @@
+1/1: Building IEdit (IEdit.lidr)
+Main> >     zipHere [] ys = []
+>     zipHere (x :: xs) (y :: ys) = (x, y) :: zipHere xs ys
+Main> Bye for now!

tests/idris2/literate007/input

@@ -0,0 +1,2 @@
+:gd 10 zipHere
+:q

tests/idris2/literate007/run

@@ -0,0 +1,3 @@
+$1 --no-banner IEdit.lidr < input
+
+rm -rf build

tests/idris2/literate008/IEdit.lidr

@@ -0,0 +1,12 @@
+> natElim : (p : Nat -> Type) -> p Z -> ((k : Nat) -> p k -> p (S k)) ->
+>           (x : Nat) -> p x
+
+> natElim2 : (p : Nat -> Type) -> p Z -> ((k : Nat) -> p k -> p (S k)) ->
+>            (x : Nat) -> p x
+> natElim2 p x f Z = x
+> natElim2 p x f (S k) = ?foo
+
+> listElim : (p : List a -> Type) ->
+>            (mnil : p []) ->
+>            (mcons : (x : _) -> (xs : List a) -> p xs -> p (x :: xs)) ->
+>            (xs : List a) -> p xs

tests/idris2/literate008/expected

@@ -0,0 +1,7 @@
+1/1: Building IEdit (IEdit.lidr)
+Main> > natElim p x f Z = x
+> natElim p x f (S k) = f k (natElim p x f k)
+Main> f k (natElim2 p x f k)
+Main> > listElim p mnil mcons [] = mnil
+> listElim p mnil mcons (x :: xs) = mcons x xs (listElim p mnil mcons xs)
+Main> Bye for now!

tests/idris2/literate008/input

@@ -0,0 +1,4 @@
+:gd 1 natElim
+:ps 7 foo
+:gd 9 listElim
+:q

tests/idris2/literate008/run

@@ -0,0 +1,3 @@
+$1 --no-banner IEdit.lidr < input
+
+rm -rf build

tests/idris2/literate009/WithLift.lidr

@@ -0,0 +1,27 @@
+> data Elem : a -> List a -> Type where
+>      Here : Elem x (x :: xs)
+>      There : Elem x xs -> Elem x (y :: xs)
+
+> interface DecEq a where
+>   decEq : (x : a) -> (y : a) -> Dec (x = y)
+
+> zeroNotSucc : Z = (S k) -> Void
+> zeroNotSucc Refl impossible
+
+> recNotEq : (k = j -> Void) -> (S k) = (S j) -> Void
+
+> DecEq Nat where
+>   decEq Z Z = Yes Refl
+>   decEq Z (S k) = No zeroNotSucc
+>   decEq (S k) Z = No ?succNotZero
+>   decEq (S k) (S j) with (decEq k j)
+>     decEq (S j) (S j) | (Yes Refl) = Yes Refl
+>     decEq (S k) (S j) | (No contra) = No ?recNotEqLift
+
+> isElem : DecEq a => (x : a) -> (xs : List a) -> Maybe (Elem x xs)
+> isElem x [] = Nothing
+> isElem x (y :: xs) with (decEq x y)
+>   isElem y (y :: xs) | (Yes Refl) = Just Here
+>   isElem x (y :: xs) | (No contra) with (isElem x xs)
+>     isElem x (y :: xs) | (No contra) | Nothing = Nothing
+>     isElem x (y :: xs) | (No contra) | (Just z) = Just (There z)

tests/idris2/literate009/expected

@@ -0,0 +1,7 @@
+1/1: Building WithLift (WithLift.lidr)
+Main> > succNotZero : S k = Z -> Void
+succNotZero
+Main> > recNotEqLift : (k = j -> Void) -> S k = S j -> Void
+(recNotEqLift contra)
+Main> > recNotEq f Refl = f Refl
+Main> Bye for now!

tests/idris2/literate009/input

@@ -0,0 +1,4 @@
+:ml 16 succNotZero
+:ml 19 recNotEqLift
+:gd 11 recNotEq
+:q

tests/idris2/literate009/run

@@ -0,0 +1,3 @@
+$1 --no-banner WithLift.lidr < input
+
+rm -rf build