idris 0.9.13 → 0.9.13.1

raw patch · 52 files changed

+582/−329 lines, 52 filesdep ~optparse-applicative

Dependency ranges changed: optparse-applicative

Files

• idris.cabal +8/−2
• libs/base/Providers.idr +0/−9
• libs/effects/Effect/File.idr +5/−10
• libs/effects/Effect/StdIO.idr +5/−5
• libs/prelude/Builtins.idr +3/−11
• libs/prelude/Prelude.idr +1/−0
• libs/prelude/Prelude/Algebra.idr +1/−1
• libs/prelude/Prelude/Pairs.idr +42/−0
• libs/prelude/Prelude/Strings.idr +5/−1
• libs/prelude/Prelude/Vect.idr +4/−1
• libs/prelude/prelude.ipkg +1/−1
• main/Main.hs +4/−0
• src/Idris/AbsSyntax.hs +9/−8
• src/Idris/AbsSyntaxTree.hs +22/−17
• src/Idris/CaseSplit.hs +3/−1
• src/Idris/CmdOptions.hs +43/−2
• src/Idris/Colours.hs +15/−8
• src/Idris/Core/CaseTree.hs +3/−0
• src/Idris/Core/Elaborate.hs +2/−2
• src/Idris/Core/Evaluate.hs +10/−5
• src/Idris/Core/ProofState.hs +4/−0
• src/Idris/Core/TT.hs +2/−2
• src/Idris/DeepSeq.hs +5/−7
• src/Idris/Delaborate.hs +29/−4
• src/Idris/ElabDecls.hs +15/−13
• src/Idris/ElabTerm.hs +9/−9
• src/Idris/Erasure.hs +1/−1
• src/Idris/Help.hs +2/−1
• src/Idris/IdeSlave.hs +5/−4
• src/Idris/Interactive.hs +4/−4
• src/Idris/Output.hs +0/−32
• src/Idris/Parser.hs +14/−13
• src/Idris/Prover.hs +92/−82
• src/Idris/Providers.hs +1/−7
• src/Idris/REPL.hs +50/−15
• src/Idris/REPLParser.hs +6/−5
• src/Pkg/PParser.hs +7/−2
• src/Pkg/Package.hs +37/−1
• test/basic010/Main.idr +43/−0
• test/basic010/expected +3/−0
• test/basic010/run +35/−0
• test/ffi005/Postulate.idr +3/−3
• test/ffi005/Postulate2.idr +0/−13
• test/ffi005/Postulate3.idr +0/−13
• test/ffi005/expected +0/−2
• test/ffi005/run +0/−7
• test/reg030/reg030.idr +1/−1
• test/reg034/expected +2/−2
• test/reg045/expected +1/−0
• test/reg045/reg045.idr +19/−0
• test/reg045/run +4/−0
• test/tutorial006/expected +2/−2

@@ -1,5 +1,5 @@ Name:           idris-Version:        0.9.13+Version:        0.9.13.1 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -242,6 +242,9 @@                        test/reg044/run                        test/reg044/*.idr                        test/reg044/expected+                       test/reg045/run+                       test/reg045/*.idr+                       test/reg045/expected                         test/basic001/run                        test/basic001/*.idr@@ -271,6 +274,9 @@                        test/basic009/*.idr                        test/basic009/expected                        test/basic009/B/*.idr+                       test/basic010/run+                       test/basic010/*.idr+                       test/basic010/expected                         test/buffer001-disabled/*.idr                        test/buffer001-disabled/run@@ -636,7 +642,7 @@                 , xml                 , deepseq                 , zlib-                , optparse-applicative+                , optparse-applicative >= 0.8   Extensions:     MultiParamTypeClasses                 , FunctionalDependencies                 , FlexibleContexts

@@ -11,26 +11,17 @@   ||| @ msg the error message   Error : (msg : String) -> Provider a -  ||| Postulate the goal type-  Postulate : Provider a- -- instances instance Functor Provider where   map f (Provide a) = Provide (f a)   map f (Error err) = Error err-  map f Postulate   = Postulate  instance Applicative Provider where   (Provide f) <$> (Provide x) = Provide (f x)   (Provide f) <$> (Error err) = Error err-  (Provide f) <$> Postulate   = Postulate   (Error err) <$> _           = Error err-  Postulate   <$> (Error err) = Error err-  Postulate   <$> _           = Postulate   pure = Provide --- is this correct for Postulate? instance Monad Provider where   (Provide x) >>= f = f x   (Error err) >>= _ = Error err-  Postulate   >>= f = Postulate

@@ -101,8 +101,7 @@ |||  ||| @ fname The file name to be opened. ||| @ m The file mode.-open : Handler FileIO e =>-       (fname : String)+open : (fname : String)        -> (m : Mode)        -> { [FILE_IO ()] ==> [FILE_IO (if result                                           then OpenFile m@@ -111,23 +110,19 @@   ||| Close a file.-close : Handler FileIO e =>-        { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()+close : { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e () close = call $ Close  ||| Read a line from the file.-readLine : Handler FileIO e => -           { [FILE_IO (OpenFile Read)] } Eff e String +readLine : { [FILE_IO (OpenFile Read)] } Eff e String  readLine = call $ ReadLine  ||| Write a line to a file.-writeLine : Handler FileIO e => -            String -> { [FILE_IO (OpenFile Write)] } Eff e ()+writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff e () writeLine str = call $ WriteLine str  ||| End of file?-eof : Handler FileIO e => -      { [FILE_IO (OpenFile Read)] } Eff e Bool +eof : { [FILE_IO (OpenFile Read)] } Eff e Bool  eof = call $ EOF  -- --------------------------------------------------------------------- [ EOF ]

@@ -39,22 +39,22 @@ STDIO = MkEff () StdIO  ||| Write a string to standard output.-putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()+putStr : String -> { [STDIO] } Eff e () putStr s = call $ PutStr s  ||| Write a character to standard output.-putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()+putChar : Char -> { [STDIO] } Eff e () putChar c = call $ PutCh c  ||| Write a string to standard output, terminating with a newline.-putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()+putStrLn : String -> { [STDIO] } Eff e () putStrLn s = putStr (s ++ "\n")  ||| Read a string from standard input.-getStr : Handler StdIO e => { [STDIO] } Eff e String+getStr : { [STDIO] } Eff e String getStr = call $ GetStr  ||| Read a character from standard input.-getChar : Handler StdIO e => { [STDIO] } Eff e Char+getChar : { [STDIO] } Eff e Char getChar = call $ GetCh 

@@ -6,16 +6,8 @@ ||| Dependent pairs, in their internal representation ||| @ a the type of the witness ||| @ P the type of the proof-data Exists : (a : Type) -> (P : a -> Type) -> Type where-    Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Exists a P--||| The first projection from a dependent pair-getWitness : {P : a -> Type} -> Exists a P -> a-getWitness (a ** v) = a--||| The second projection from a dependent pair-getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)-getProof (a ** v) = v+data Sigma : (a : Type) -> (P : a -> Type) -> Type where+    Sg_intro : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P  ||| The eliminator for the empty type. FalseElim : _|_ -> a@@ -47,7 +39,7 @@ data Lazy' : LazyType -> Type -> Type where      ||| A delayed computation.      |||-     |||Delay is inserted automatically by the elaborator where necessary.+     ||| Delay is inserted automatically by the elaborator where necessary.      |||      ||| Note that compiled code gives `Delay` special semantics.      ||| @ t   whether this is laziness from codata or normal lazy evaluation

@@ -21,6 +21,7 @@ import Prelude.Bits import Prelude.Stream import Prelude.Uninhabited+import Prelude.Pairs  import Decidable.Equality 

@@ -106,7 +106,7 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where   total ringOpIsAssociative   : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r   total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)-  total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)+  total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (c <*> r)  ||| Sets equipped with two binary operations, one associative and commutative ||| supplied with a neutral element, and the other associative supplied with a

@@ -0,0 +1,42 @@+module Prelude.Pairs++import Builtins++%access public+%default total++using (a : Type, P : a -> Type)++  ||| Dependent pair where the first field is erased.+  data Exists : (P : a -> Type) -> Type where+    evidence : .(x : a) -> (pf : P x) -> Exists P++  ||| Dependent pair where the second field is erased. +  data Subset : (a : Type) -> (P : a -> Type) -> Type where+    element : (x : a) -> .(pf : P x) -> Subset a P++  -- Monomorphic projections++  namespace Exists+    getWitness : Exists {a} P -> a+    getWitness (evidence x pf) = x++    getProof : (x : Exists {a} P) -> P (getWitness x)+    getProof (evidence x pf) = pf++  namespace Subset+    getWitness : Subset a P -> a+    getWitness (element x pf) = x++    getProof : (x : Subset a P) -> P (getWitness x)+    getProof (element x pf) = pf++  namespace Sigma+    getWitness : Sigma a P -> a+    getWitness (x ** pf) = x++    getProof : (x : Sigma a P) -> P (getWitness x)+    getProof (x ** pf) = pf++  -- Polymorphic (class-based) projections have been removed+  -- because type-directed name disambiguation works better.

@@ -218,8 +218,12 @@  partial foldr1 : (a -> a -> a) -> List a -> a-foldr1 f [x] = x+foldr1 _ [x] = x foldr1 f (x::xs) = f x (foldr1 f xs)++partial+foldl1 : (a -> a -> a) -> List a -> a+foldl1 f (x::xs) = foldl f x xs  ||| Joins the character lists by spaces into a single character list. |||

@@ -260,10 +260,13 @@ concat []      = [] concat (v::vs) = v ++ concat vs -||| Fold without seeding the accumulator+||| Foldr without seeding the accumulator foldr1 : (t -> t -> t) -> Vect (S n) t -> t foldr1 f (x::xs) = foldr f x xs +||| Foldl without seeding the accumulator+foldl1 : (t -> t -> t) -> Vect (S n) t -> t+foldl1 f (x::xs) = foldl f x xs -------------------------------------------------------------------------------- -- Scans --------------------------------------------------------------------------------

@@ -8,7 +8,7 @@           Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,           Prelude.Vect, Prelude.Strings, Prelude.Chars, Prelude.Functor,           Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,-          Prelude.Uninhabited,+          Prelude.Uninhabited, Prelude.Pairs,            Decidable.Equality 

@@ -63,6 +63,10 @@            [] -> return ()            fs -> do runIO $ mapM_ documentPkg fs                     runIO $ exitWith ExitSuccess+       case opt getPkgTest opts of+           [] -> return ()+           fs -> do runIO $ mapM_ testPkg fs+                    runIO $ exitWith ExitSuccess        case opt getPkg opts of            [] -> case opt getPkgREPL opts of                       [] -> idrisMain opts

@@ -278,7 +278,7 @@         ty' <- case lookupCtxtName ty (idris_implicits i) of                        [(tyn, _)] -> return tyn                        [] -> throwError (NoSuchVariable ty)-                       tyns -> throwError (CantResolveAlts (map show (map fst tyns)))+                       tyns -> throwError (CantResolveAlts (map fst tyns))         let ns' = case lookupCtxt ty' (idris_namehints i) of                        [ns] -> ns ++ [n]                        _ -> [n]@@ -778,13 +778,14 @@ setColour ct c = do i <- getIState                     let newTheme = setColour' ct c (idris_colourTheme i)                     putIState $ i { idris_colourTheme = newTheme }-    where setColour' KeywordColour  c t = t { keywordColour = c }-          setColour' BoundVarColour c t = t { boundVarColour = c }-          setColour' ImplicitColour c t = t { implicitColour = c }-          setColour' FunctionColour c t = t { functionColour = c }-          setColour' TypeColour     c t = t { typeColour = c }-          setColour' DataColour     c t = t { dataColour = c }-          setColour' PromptColour   c t = t { promptColour = c }+    where setColour' KeywordColour   c t = t { keywordColour = c }+          setColour' BoundVarColour  c t = t { boundVarColour = c }+          setColour' ImplicitColour  c t = t { implicitColour = c }+          setColour' FunctionColour  c t = t { functionColour = c }+          setColour' TypeColour      c t = t { typeColour = c }+          setColour' DataColour      c t = t { dataColour = c }+          setColour' PromptColour    c t = t { promptColour = c }+          setColour' PostulateColour c t = t { postulateColour = c }  logLvl :: Int -> String -> Idris () logLvl l str = do i <- getIState

@@ -339,7 +339,7 @@              | WhoCalls Name              | CallsWho Name              | MakeDoc String                      -- IdrisDoc-+             | Warranty  data Opt = Filename String          | Quiet@@ -373,6 +373,7 @@          | PkgCheck String          | PkgREPL String          | PkgMkDoc String     -- IdrisDoc+         | PkgTest String          | WarnOnly          | Pkg String          | BCAsm String@@ -492,11 +493,12 @@ type DataOpts = [DataOpt]  -- | Type provider - what to provide-data ProvideWhat = ProvTerm      -- ^ only allow providing terms-                 | ProvPostulate -- ^ only allow postulates-                 | ProvAny       -- ^ either is ok-    deriving (Show, Eq)+data ProvideWhat' t = ProvTerm t t     -- ^ the first is the goal type, the second is the term+                    | ProvPostulate t  -- ^ goal type must be Type, so only term+    deriving (Show, Eq, Functor) +type ProvideWhat = ProvideWhat' PTerm+ -- | Top-level declarations such as compiler directives, definitions, -- datatypes and typeclasses. data PDecl' t@@ -529,7 +531,7 @@    | PSyntax  FC Syntax -- ^ Syntax definition    | PMutual  FC [PDecl' t] -- ^ Mutual block    | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.-   | PProvider SyntaxInfo FC ProvideWhat Name t t -- ^ Type provider. The first t is the type, the second is the term+   | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term    | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If                             -- bool is True, lhs and rhs must be convertible  deriving Functor@@ -1100,8 +1102,8 @@                       PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]  -- Defined in builtins.idr-sigmaTy   = sUN "Exists"-existsCon = sUN "Ex_intro"+sigmaTy   = sUN "Sigma"+existsCon = sUN "Sg_intro"  piBind :: [(Name, PTerm)] -> PTerm -> PTerm piBind = piBindp expl@@ -1148,18 +1150,22 @@ consoleDecorate ist (AnnName n _ _ _) = let ctxt  = tt_ctxt ist                                             theme = idris_colourTheme ist                                         in case () of-                                             _ | isDConName n ctxt -> colouriseData theme-                                             _ | isFnName n ctxt   -> colouriseFun theme-                                             _ | isTConName n ctxt -> colouriseType theme-                                             _ | otherwise         -> id -- don't colourise unknown names+                                             _ | isDConName n ctxt     -> colouriseData theme+                                             _ | isFnName n ctxt       -> colouriseFun theme+                                             _ | isTConName n ctxt     -> colouriseType theme+                                             _ | isPostulateName n ist -> colourisePostulate theme+                                             _ | otherwise             -> id -- don't colourise unknown names consoleDecorate ist (AnnFC _) = id consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)   where colour BoldText      = IdrisColour Nothing True False True False         colour UnderlineText = IdrisColour Nothing True True False False         colour ItalicText    = IdrisColour Nothing True False False True +isPostulateName :: Name -> IState -> Bool+isPostulateName n ist = S.member n (idris_postulates ist)+ -- | Pretty-print a high-level closed Idris term with no information about precedence/associativity-prettyImp :: PPOption -- ^^ pretty printing options +prettyImp :: PPOption -- ^^ pretty printing options           -> PTerm -- ^^ the term to pretty-print           -> Doc OutputAnnotation prettyImp impl = pprintPTerm impl [] [] []@@ -1169,7 +1175,7 @@ prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)  -- | Pretty-print a high-level Idris term in some bindings context with infix info-pprintPTerm :: PPOption -- ^^ pretty printing options +pprintPTerm :: PPOption -- ^^ pretty printing options             -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit             -> [Name] -- ^^ names to always show in pi, even if not used             -> [FixDecl] -- ^^ Fixity declarations@@ -1422,7 +1428,7 @@     getFixity = flip M.lookup fixities  prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation-prettyDocumentedIst ist (name, ty, docs) = +prettyDocumentedIst ist (name, ty, docs) =           prettyName True [] name <+> colon <+> align (prettyIst ist ty) <$>           fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs) @@ -1443,7 +1449,7 @@         strName (NS n ns) | showNS    = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n                           | otherwise = strName n         strName n | n == falseTy = "_|_"-        strName (MN i s) = T.unpack s +        strName (MN i s) = T.unpack s         strName other = show other  @@ -1702,4 +1708,3 @@      niTacImp env (TacImp _ _ scr) = ni env scr     niTacImp _ _                = []-

@@ -280,6 +280,8 @@     nshow t = show t      -- if there's any {n} replace with {n=n}+    -- but don't replace it in comments+    expandBraces ('{' : '-' : xs) = '{' : '-' : xs     expandBraces ('{' : xs)         = let (brace, (_:rest)) = span (/= '}') xs in               if (not ('=' `elem` brace))@@ -298,7 +300,7 @@               if (before == n && not (isAlphaNum next))                  then addBrackets tm ++ updatePat False n tm after                  else c : updatePat (not (isAlphaNum c)) n tm rest-    updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest+    updatePat start n tm (c:rest) = c : updatePat (not ((isAlphaNum c) || c == '_')) n tm rest      addBrackets tm | ' ' `elem` tm                    , not (isPrefixOf "(" tm)

@@ -10,11 +10,51 @@ import Options.Applicative.Arrows import Data.Maybe +import qualified Text.PrettyPrint.ANSI.Leijen as PP+ runArgParser :: IO [Opt]-runArgParser = do opts <- execParser $ info parser $-                    header ("Idris version " ++ ver ++ ", (C) The Idris Community 2014")+runArgParser = do opts <- execParser $ info parser+                          (fullDesc+                           <> headerDoc   (Just idrisHeader)+                           <> progDescDoc (Just idrisProgDesc)+                           <> footerDoc   (Just idrisFooter)+                          )                   return $ preProcOpts opts []+               where+                 idrisHeader = PP.hsep [PP.text "Idris version", PP.text ver, PP.text ", (C) The Idris Community 2014"]+                 idrisProgDesc = PP.vsep [PP.text "Idris is a general purpose pure functional programming language with dependent",+                                          PP.text "types. Dependent types allow types to be predicated on values, meaning that",+                                          PP.text "some aspects of a program’s behaviour can be specified precisely in the type.",+                                          PP.text "It is compiled, with eager evaluation. Its features are influenced by Haskell",+                                          PP.text "and ML.",+                                          PP.empty,+                                          PP.vsep $ map (\x -> PP.indent 4 (PP.text x)) [+                                            "+ Full dependent types with dependent pattern matching",+                                            "+ where clauses, with rule, simple case expressions",+                                            "+ pattern matching let and lambda bindings",+                                            "+ Type classes, monad comprehensions",+                                            "+ do notation, idiom brackets",+                                            "+ syntactic conveniences for lists, tuples, dependent pairs",+                                            "+ Totality checking",+                                            "+ Coinductive types",+                                            "+ Indentation significant syntax, extensible syntax",+                                            "+ Tactic based theorem proving (influenced by Coq)",+                                            "+ Cumulative universes",+                                            "+ Simple foreign function interface (to C)",+                                            "+ Hugs style interactive environment"+                                            ],+                                          PP.empty]+                 idrisFooter = PP.vsep [PP.text "It is important to note that Idris is first and foremost a research tool",+                                        PP.text "and project. Thus the tooling provided and resulting programs created",+                                        PP.text "should not necessarily be seen as production ready nor for industrial use.",+                                        PP.empty,+                                        PP.text "More details over Idris can be found online here:",+                                        PP.empty,+                                        PP.indent 4 (PP.text "http://www.idris-lang.org/")] +++ pureArgParser :: [String] -> [Opt] pureArgParser args = case execParserMaybe (info parser idm) args of   Just opts -> preProcOpts opts []@@ -61,6 +101,7 @@   <|> (PkgClean <$> strOption (long "clean" <> metavar "IPKG" <> help "Clean package"))   <|> (PkgMkDoc <$> strOption (long "mkdoc" <> metavar "IPKG" <> help "Generate IdrisDoc for package"))   <|> (PkgCheck <$> strOption (long "checkpkg" <> metavar "IPKG" <> help "Check package only"))+  <|> (PkgTest <$> strOption (long "testpkg" <> metavar "IPKG" <> help "Run tests for package"))   -- Misc options   <|> (BCAsm <$> strOption (long "bytecode"))   <|> flag' (OutputTy Raw) (short 'S' <> long "codegenonly" <> help "Do no further compilation of code generator output")

@@ -2,7 +2,7 @@   IdrisColour(..),   ColourTheme(..),   defaultTheme,-  colouriseKwd, colouriseBound, colouriseImplicit,+  colouriseKwd, colouriseBound, colouriseImplicit, colourisePostulate,   colouriseType, colouriseFun, colouriseData, colouriseKeyword,   colourisePrompt, colourise, ColourType(..)) where @@ -19,13 +19,14 @@ mkColour :: Color -> IdrisColour mkColour c = IdrisColour (Just c) True False False False -data ColourTheme = ColourTheme { keywordColour  :: IdrisColour-                               , boundVarColour :: IdrisColour-                               , implicitColour :: IdrisColour-                               , functionColour :: IdrisColour-                               , typeColour     :: IdrisColour-                               , dataColour     :: IdrisColour-                               , promptColour   :: IdrisColour+data ColourTheme = ColourTheme { keywordColour   :: IdrisColour+                               , boundVarColour  :: IdrisColour+                               , implicitColour  :: IdrisColour+                               , functionColour  :: IdrisColour+                               , typeColour      :: IdrisColour+                               , dataColour      :: IdrisColour+                               , promptColour    :: IdrisColour+                               , postulateColour :: IdrisColour                                }                    deriving (Eq, Show) @@ -38,6 +39,7 @@                            , typeColour = mkColour Blue                            , dataColour = mkColour Red                            , promptColour = IdrisColour Nothing True False True False+                           , postulateColour = IdrisColour (Just Green) True False True False                            }  -- | Set the colour of a string using POSIX escape codes@@ -74,6 +76,10 @@ colouriseKeyword :: ColourTheme -> String -> String colouriseKeyword t = colourise (keywordColour t) +colourisePostulate :: ColourTheme -> String -> String+colourisePostulate t = colourise (postulateColour t)++ data ColourType = KeywordColour                 | BoundVarColour                 | ImplicitColour@@ -81,4 +87,5 @@                 | TypeColour                 | DataColour                 | PromptColour+                | PostulateColour                   deriving (Eq, Show, Bounded, Enum)

@@ -336,6 +336,9 @@ toPat :: Bool -> Bool -> [Term] -> [Pat] toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []   where+    toPat' (P (DCon t a) nm@(UN n) _) [_,_,arg]+           | n == txt "Delay" = do arg' <- toPat' arg []+                                   return $ PCon nm t [PAny, PAny, arg']     toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args                                         return $ PCon n t args'     -- n + 1

@@ -709,7 +709,7 @@   -- Try a selection of tactics. Exactly one must work, all others must fail-tryAll :: [(Elab' aux a, String)] -> Elab' aux a+tryAll :: [(Elab' aux a, Name)] -> Elab' aux a tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs   where     cantResolve :: Elab' aux a@@ -718,7 +718,7 @@     tryAll' :: [Elab' aux a] -> -- successes                Int -> -- most problems                (Elab' aux a, Int) -> -- smallest failure-               [(Elab' aux a, String)] -> -- still to try+               [(Elab' aux a, Name)] -> -- still to try                Elab' aux a     tryAll' [res] pmax _   [] = res     tryAll' (_:_) pmax _   [] = cantResolve

@@ -8,7 +8,7 @@                 Context, initContext, ctxtAlist, uconstraints, next_tvar,                 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,                 addDatatype, addCasedef, simplifyCasedef, addOperator,-                lookupNames, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,+                lookupNames, lookupTyName, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,                 mapDefCtxt,                 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,                 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions) where@@ -868,14 +868,19 @@                 = let ns = lookupCtxtName n (definitions ctxt) in                       map fst ns -lookupTy :: Name -> Context -> [Type]-lookupTy n ctxt-                = do def <- lookupCtxt n (definitions ctxt)-                     case tfst def of+lookupTyName :: Name -> Context -> [(Name, Type)]+lookupTyName n ctxt = do +  (name, def) <- lookupCtxtName n (definitions ctxt)+  ty <- case tfst def of                        (Function ty _) -> return ty                        (TyDecl _ ty) -> return ty                        (Operator ty _ _) -> return ty                        (CaseOp _ ty _ _ _ _) -> return ty+  return (name, ty)+++lookupTy :: Name -> Context -> [Type]+lookupTy n ctxt = map snd (lookupTyName n ctxt)  isConName :: Name -> Context -> Bool isConName n ctxt = isTConName n ctxt || isDConName n ctxt

@@ -823,6 +823,10 @@ updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env  updateError [] err = err+updateError ns (At f e) = At f (updateError ns e)+updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)+updateError ns (ElaboratingArg f a env e) + = ElaboratingArg f a env (updateError ns e) updateError ns (CantUnify b l r e xs sc)  = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc updateError ns e = e

@@ -83,7 +83,7 @@                                      | otherwise            = show sl ++ ":" ++ show sc ++ "-" ++ show el ++ ":" ++ show ec  -- | Output annotation for pretty-printed name - decides colour-data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput  -- | Text formatting output data TextFormatting = BoldText | ItalicText | UnderlineText@@ -133,7 +133,7 @@           | NoTypeDecl Name           | NotInjective t t t           | CantResolve t-          | CantResolveAlts [String]+          | CantResolveAlts [Name]           | IncompleteTerm t           | UniverseError           | ProgramLineComment

@@ -156,16 +156,14 @@         rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()         rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()         rnf (PDirective x1) = ()-        rnf (PProvider x1 x2 x3 x4 x5 x6)-          = rnf x1 `seq`-              rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()+        rnf (PProvider x1 x2 x3 x4)+          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()         rnf (PTransform x1 x2 x3 x4)           = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` () -instance NFData ProvideWhat where-        rnf ProvAny       = ()-        rnf ProvTerm      = ()-        rnf ProvPostulate = ()+instance NFData t => NFData (ProvideWhat' t)  where+        rnf (ProvTerm ty tm)   = rnf ty `seq` rnf tm `seq` ()+        rnf (ProvPostulate tm) = rnf tm `seq` ()  instance NFData PunInfo where         rnf x = x `seq` ()

@@ -1,5 +1,5 @@ {-# LANGUAGE PatternGuards #-}-module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pprintErr) where+module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', fancifyAnnots, pprintErr) where  -- Convert core TT back into high level syntax, primarily for display -- purposes.@@ -9,6 +9,7 @@ import Idris.AbsSyntax import Idris.Core.TT import Idris.Core.Evaluate+import Idris.Docstrings (overview, renderDocstring) import Idris.ErrReverse  import Data.List (intersperse)@@ -92,13 +93,13 @@          | n == eqCon     = PRefl un (de env [] r)          | n == sUN "lazy" = de env [] r     deFn env (P _ n _) [ty, Bind x (Lam _) r]-         | n == sUN "Exists"+         | n == sUN "Sigma"                = PDPair un IsType (PRef un x) (de env [] ty)                            (de ((x,x):env) [] (instantiate (P Bound x ty) r))     deFn env (P _ n _) [_,_,l,r]          | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)          | n == eqTy    = PEq un (de env [] l) (de env [] r)-         | n == sUN "Ex_intro" = PDPair un IsTerm (de env [] l) Placeholder+         | n == sUN "Sg_intro" = PDPair un IsTerm (de env [] l) Placeholder                                            (de env [] r)     deFn env f@(P _ n _) args           | n `elem` map snd env @@ -195,7 +196,7 @@   pprintTerm i (delab i y) pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c) pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>-                                    align (cat (punctuate (comma <> space) (map text as)))+                                    align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as))) pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)@@ -257,6 +258,30 @@  annName' :: Name -> String -> Doc OutputAnnotation annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)++fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation+fancifyAnnots ist annot@(AnnName n _ _ _) =+  do let ctxt = tt_ctxt ist+         docs = docOverview ist n+         ty   = Just (getTy ist n)+     case () of+       _ | isDConName      n ctxt -> AnnName n (Just DataOutput) docs ty+       _ | isFnName        n ctxt -> AnnName n (Just FunOutput) docs ty+       _ | isTConName      n ctxt -> AnnName n (Just TypeOutput) docs ty+       _ | isMetavarName   n ist  -> AnnName n (Just MetavarOutput) docs ty+       _ | isPostulateName n ist  -> AnnName n (Just PostulateOutput) docs ty+       _ | otherwise            -> annot+  where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs+        docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)+                               let o   = overview (fst docs)+                                   -- TODO make width configurable+                                   out = displayS . renderPretty 1.0 50 $ renderDocstring o+                               return (out "")+        getTy :: IState -> Name -> String -- fails if name not already extant!+        getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $+                                  delabTy ist n+                      in (displayS . renderPretty 1.0 50 $ theTy) ""+fancifyAnnots _ annot = annot  showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation showSc i [] = empty

@@ -681,8 +681,8 @@   -- | Elaborate a type provider-elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> PTerm -> PTerm -> Idris ()-elabProvider info syn fc what n ty tm+elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()+elabProvider info syn fc what n     = do i <- getIState          -- Ensure that the experimental extension is enabled          unless (TypeProviders `elem` idris_language_extensions i) $@@ -692,12 +692,17 @@          ctxt <- getContext           -- First elaborate the expected type (and check that it's a type)-         (ty', typ) <- elabVal toplevel False ty+         -- The goal type for a postulate is always Type.+         (ty', typ) <- case what of+                         ProvTerm ty p   -> elabVal toplevel False ty+                         ProvPostulate _ -> elabVal toplevel False PType          unless (isTType typ) $            ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)           -- Elaborate the provider term to TT and check that the type matches-         (e, et) <- elabVal toplevel False tm+         (e, et) <- case what of+                      ProvTerm _ tm    -> elabVal toplevel False tm+                      ProvPostulate tm -> elabVal toplevel False tm          unless (isProviderOf (normalise ctxt [] ty') et) $            ifail $ "Expected provider type IO (Provider (" ++                    show ty' ++ "))" ++ ", got " ++ show et ++ " instead."@@ -715,17 +720,14 @@           case provided of            Provide tm-             | what `elem` [ProvTerm, ProvAny] ->+             | ProvTerm ty _ <- what ->                do -- Finally add a top-level definition of the provided term                   elabType info syn emptyDocstring [] fc [] n ty                   elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]                   logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm-             | otherwise ->-               ierror . Msg $ "Attempted to provide a term where a postulate was expected."-           Postulate-             | what `elem` [ProvPostulate, ProvAny] ->+             | ProvPostulate _ <- what ->                do -- Add the postulate-                  elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n ty+                  elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)                   logLvl 3 $ "Elaborated provided postulate " ++ show n              | otherwise ->                ierror . Msg $ "Attempted to provide a postulate where a term was expected."@@ -2042,7 +2044,7 @@                   [c] -> return c                   [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"                   cs -> tclift $ tfail $ At fc -                           (CantResolveAlts (map (show . fst) cs))+                           (CantResolveAlts (map fst cs))     let constraint = PApp fc (PRef fc n) (map pexp ps)     let iname = mkiname n ps expn     let emptyclass = null (class_methods ci)@@ -2408,10 +2410,10 @@          addIBC (IBCDSL n) elabDecl' what info (PDirective i)   | what /= EDefns = i-elabDecl' what info (PProvider syn fc provWhat n tp tm)+elabDecl' what info (PProvider syn fc provWhat n)   | what /= EDefns     = do iLOG $ "Elaborating type provider " ++ show n-         elabProvider info syn fc provWhat n tp tm+         elabProvider info syn fc provWhat n elabDecl' what info (PTransform fc safety old new)     = elabTransform info fc safety old new elabDecl' _ _ _ = return () -- skipped this time

@@ -70,7 +70,7 @@           when (not pattern) $             traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++-                        "Remaining problems:\n" ++ show probs) $ +                        "Remaining problems:\n" ++ qshow probs) $               do unify_all; matchProblems True; unifyProblems           probs <- get_probs@@ -271,10 +271,10 @@              let as' = pruneByType (map fst env) tc ctxt as --              trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $              tryAll (zip (map (elab' ina) as') (map showHd as'))-        where showHd (PApp _ (PRef _ n) _) = show n-              showHd (PRef _ n) = show n-              showHd (PApp _ h _) = show h-              showHd x = show x+        where showHd (PApp _ (PRef _ n) _) = n+              showHd (PRef _ n) = n+              showHd (PApp _ h _) = showHd h+              showHd x = NErased -- We probably should do something better than this here     elab' ina (PAlternative False as)         = trySeq as         where -- if none work, take the error from the first@@ -991,7 +991,7 @@                     ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)              let tacs = map (\ (fn', imps) ->                                  (match_apply (Var fn') (map (\x -> (x, 0)) imps),-                                     show fn')) fnimps+                                     fn')) fnimps              tryAll tacs              when autoSolve solveAll        where envArgs n = do e <- get_env@@ -1007,7 +1007,7 @@                     ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)              let tacs = map (\ (fn', imps) ->                                  (apply (Var fn') (map (\x -> (x, 0)) imps),-                                     show fn')) fnimps+                                     fn')) fnimps              tryAll tacs              when autoSolve solveAll        where isImp (PImp _ _ _ _ _) = True@@ -1609,8 +1609,8 @@             ] reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t] reflectErr (CantResolveAlts ss) =-  raw_apply (Var $ reflErrName "CantResolve")-            [rawList (Var $ (sUN "String")) (map (RConstant . Str) ss)]+  raw_apply (Var $ reflErrName "CantResolveAlts")+            [rawList (Var $ (sUN "String")) (map Var ss)] reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t] reflectErr UniverseError = Var $ reflErrName "UniverseError" reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

@@ -109,7 +109,7 @@     getMainName ist = case lookupCtxtName n (idris_implicits ist) of         [(n', _)] -> Right n'         []        -> Left (NoSuchVariable n)-        more      -> Left (CantResolveAlts (map (show . fst) more))+        more      -> Left (CantResolveAlts (map fst more))       where         n = sNS (sUN "main") ["Main"] 

@@ -58,7 +58,8 @@     ([":unset"], OptionArg, "Unset an option"),     ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),     ([":consolewidth"], ConsoleWidthArg, "Set the width of the console"),-    ([":q",":quit"], NoArg, "Exit the Idris system")+    ([":q",":quit"], NoArg, "Exit the Idris system"),+    ([":w", ":warranty"], NoArg, "Displays warranty information")   ]  -- | Use these for completion, but don't show them in :help

@@ -74,10 +74,11 @@    toSExp (l, m, n, o, p) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o, toSExp p]  instance SExpable NameOutput where-  toSExp TypeOutput    = SymbolAtom "type"-  toSExp FunOutput     = SymbolAtom "function"-  toSExp DataOutput    = SymbolAtom "data"-  toSExp MetavarOutput = SymbolAtom "metavar"+  toSExp TypeOutput      = SymbolAtom "type"+  toSExp FunOutput       = SymbolAtom "function"+  toSExp DataOutput      = SymbolAtom "data"+  toSExp MetavarOutput   = SymbolAtom "metavar"+  toSExp PostulateOutput = SymbolAtom "postulate"  maybeProps :: SExpable a => [(String, Maybe a)] -> [(SExp, SExp)] maybeProps [] = []

@@ -162,7 +162,7 @@          mn <- case lookupNames n ctxt of                     [x] -> return x                     [] -> return n-                    ns -> ierror (CantResolveAlts (map show ns))+                    ns -> ierror (CantResolveAlts ns)          i <- getIState          let (top, envlen, _) = case lookup mn (idris_metavars i) of                                   Just (t, e, False) -> (t, e, False)@@ -242,10 +242,10 @@         let isProv = checkProv tyline (show n)          ctxt <- getContext-        mty <- case lookupTy n ctxt of-                    [t] -> return t+        mty <- case lookupTyName n ctxt of+                    [(_,t)] -> return t                     [] -> ierror (NoSuchVariable n)-                    ns -> ierror (CantResolveAlts (map show ns))+                    ns -> ierror (CantResolveAlts (map fst ns))         i <- getIState          if (not isProv) then do

@@ -83,38 +83,6 @@                           RawOutput -> consoleDisplayAnnotated h d                           IdeSlave n -> ideSlaveReturnAnnotated n h d -makeAnnName :: IState -> Name -> Maybe OutputAnnotation-makeAnnName ist n-  | isDConName    n ctxt = annName DataOutput-  | isFnName      n ctxt = annName FunOutput-  | isTConName    n ctxt = annName TypeOutput-  | isMetavarName n ist  = annName MetavarOutput-  | otherwise            = Nothing-  where ctxt = tt_ctxt ist-        docs = docOverview ist n-        ty   = Just (getTy ist n)-        -        annName :: NameOutput -> Maybe OutputAnnotation-        annName nameType = Just (AnnName n (Just nameType) docs ty)-        docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs-        docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)-                               let o   = overview (fst docs)-                                   -- TODO make width configurable-                                   out = displayS . renderPretty 1.0 50 $ renderDocstring o-                               return (out "")-        getTy :: IState -> Name -> String -- fails if name not already extant!-        getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $-                                  delabTy ist n-                      in (displayS . renderPretty 1.0 50 $ theTy) ""---fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation-fancifyAnnots ist annot@(AnnName n _ _ _) = case makeAnnName ist n of-  Just fancyAnnot -> fancyAnnot-  Nothing         -> annot -fancifyAnnots _ annot = annot-- ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris () ideSlaveReturnWithStatus status n h out = do    ist <- getIState

@@ -1034,7 +1034,7 @@                             case lookupCtxtName n (idris_implicits i) of                               [(n', _)] -> return n'                               []        -> throwError (NoSuchVariable n)-                              more      -> throwError (CantResolveAlts (map (show . fst) more))+                              more      -> throwError (CantResolveAlts (map fst more))  pLangExt :: IdrisParser LanguageExt pLangExt = (reserved "TypeProviders" >> return TypeProviders)@@ -1061,19 +1061,20 @@  -} provider :: SyntaxInfo -> IdrisParser [PDecl] provider syn = do try (lchar '%' *> reserved "provide");-                  what <- provideWhat-                  lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'-                  fc <- getFC-                  reserved "with"-                  e <- expr syn-                  return  [PProvider syn fc what n t e]+                  provideTerm <|> providePostulate                <?> "type provider"-  where provideWhat :: IdrisParser ProvideWhat-        provideWhat = option ProvAny-                        (      ((reserved "proof" <|> reserved "term" <|> reserved "type") *>-                                pure ProvTerm)-                           <|> (reserved "postulate" *> pure ProvPostulate)-                   <?> "provider variety")+  where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'+                         fc <- getFC+                         reserved "with"+                         e <- expr syn <?> "provider expression"+                         return  [PProvider syn fc (ProvTerm t e) n]+        providePostulate = do reserved "postulate"+                              n <- fnName+                              fc <- getFC+                              reserved "with"+                              e <- expr syn <?> "provider expression"+                              return [PProvider syn fc (ProvPostulate e) n]+ {- | Parses a transform  @

@@ -63,9 +63,10 @@          ideslavePutSExp "start-proof-mode" n          (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing          iLOG $ "Adding " ++ show tm-         iputStrLn $ showProof lit n prf          i <- getIState-         ideslavePutSExp "end-proof-mode" n+         case idris_outputmode i of+           IdeSlave _ -> ideslavePutSExp "end-proof-mode" (n, showProof lit n prf)+           _          -> iputStrLn $ showProof lit n prf          let proofs = proof_list i          putIState (i { proof_list = (n, prf) : proofs })          let tree = simpleCase False True False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]@@ -85,6 +86,11 @@                                  [([], P Ref n ty, ptm)]                                  [([], P Ref n ty, ptm')] ty)          solveDeferred n+         case idris_outputmode i of+           IdeSlave n ->+             runIO . putStrLn $+               convSExp "return" (SymbolAtom "ok", "") n+           _ -> return ()  elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl]) elabStep st e = case runStateT eCheck st of@@ -171,7 +177,7 @@             ideslavePutSExp "return" good             receiveInput e        Just (Interpret cmd) -> return (Just cmd)-       Nothing -> return Nothing+       _ -> return Nothing  ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String]) ploop fn d prompt prf e h@@ -198,91 +204,95 @@          case cmd of             Success Abandon -> do iPrintError ""; ifail "Abandoned"             _ -> return ()-         (d, st, done, prf') <- idrisCatch+         (d, st, done, prf', res) <- idrisCatch            (case cmd of-              Failure err -> do iPrintError (show err)-                                return (False, e, False, prf)+              Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)               Success Undo -> do (_, st) <- elabStep e loadState-                                 iPrintResult ""-                                 return (True, st, False, init prf)-              Success ProofState -> do iPrintResult ""-                                       return (True, e, False, prf)+                                 return (True, st, False, init prf, Right "")+              Success ProofState -> return (True, e, False, prf, Right "")               Success ProofTerm -> do tm <- lifte e get_term-                                      iPrintResult $ "TT: " ++ show tm ++ "\n"-                                      return (False, e, False, prf)+                                      iputStrLn $ "TT: " ++ show tm ++ "\n"+                                      return (False, e, False, prf, Right "")               Success Qed -> do hs <- lifte e get_holes                                 when (not (null hs)) $ ifail "Incomplete proof"-                                iPrintResult "Proof completed!"-                                return (False, e, True, prf)-              Success (TCheck (PRef _ n)) ->-                do ctxt <- getContext-                   ist <- getIState-                   imp <- impShow-                   idrisCatch (do-                       let h      = idris_outh ist-                           OK env = envAtFocus (proof e)-                           ctxt'  = envCtxt env ctxt-                           bnd    = map (\x -> (fst x, False)) env-                           ist'   = ist { tt_ctxt = ctxt' }-                       putIState ist'-                       -- Unlike the REPL, metavars have no special treatment, to-                       -- make it easier to see how to prove with them.-                       case lookupNames n ctxt' of-                         [] -> ihPrintError h $ "No such variable " ++ show n-                         ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)-                       putIState ist-                       return (False, e, False, prf))-                     (\err -> do putIState ist ; ierror err)-              Success (TCheck t) ->-                do ist <- getIState-                   ctxt <- getContext-                   idrisCatch (do-                       let OK env = envAtFocus (proof e)-                           ctxt'  = envCtxt env ctxt-                       putIState ist { tt_ctxt = ctxt' }-                       (tm, ty) <- elabVal toplevel False t-                       let ppo = ppOptionIst ist-                           ty'     = normaliseC ctxt [] ty-                           h       = idris_outh ist-                           infixes = idris_infixes ist-                       case tm of-                          TType _ ->-                            ihPrintTermWithType h (prettyImp ppo PType) type1Doc-                          _ -> let bnd = map (\x -> (fst x, False)) env in-                               ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))-                                                     (pprintPTerm ppo bnd [] infixes (delab ist ty))-                       putIState ist-                       return (False, e, False, prf))-                     (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)-              Success (TEval t)  -> withErrorReflection $-                                    do ctxt <- getContext-                                       ist <- getIState-                                       idrisCatch (do-                                           let OK env = envAtFocus (proof e)-                                               ctxt'  = envCtxt env ctxt-                                               ist'   = ist { tt_ctxt = ctxt' }-                                               bnd    = map (\x -> (fst x, False)) env-                                           putIState ist'-                                           (tm, ty) <- elabVal toplevel False t-                                           let tm'     = force (normaliseAll ctxt' env tm)-                                               ty'     = force (normaliseAll ctxt' env ty)-                                               ppo     = ppOption (idris_options ist')-                                               infixes = idris_infixes ist-                                               tmDoc   = pprintPTerm ppo bnd [] infixes (delab ist' tm')-                                               tyDoc   = pprintPTerm ppo bnd [] infixes (delab ist' ty')-                                           ihPrintTermWithType (idris_outh ist') tmDoc tyDoc-                                           putIState ist-                                           return (False, e, False, prf))-                                         (\err -> do putIState ist ; ierror err)+                                iputStrLn "Proof completed!"+                                return (False, e, True, prf, Right "")+              Success (TCheck (PRef _ n)) -> checkNameType n+              Success (TCheck t) -> checkType t+              Success (TEval t)  -> evalTerm t e               Success tac -> do (_, e) <- elabStep e saveState                                 (_, st) <- elabStep e (runTac autoSolve i fn tac)---                               trace (show (problems (proof st))) $-                                iPrintResult ""-                                return (True, st, False, prf ++ [step]))-           (\err -> do iPrintError (pshow i err)-                       return (False, e, False, prf))+                                return (True, st, False, prf ++ [step], Right ""))+           (\err -> return (False, e, False, prf, Left err))          ideslavePutSExp "write-proof-state" (prf', length prf')-         if done then do (tm, _) <- elabStep st get_term-                         return (tm, prf')-                 else ploop fn d prompt prf' st h'+         case res of+           Left err -> do iPrintError (pshow i err)+                          ploop fn d prompt prf' st h'+           Right ok ->+             if done then do (tm, _) <- elabStep st get_term+                             return (tm, prf')+                     else do iPrintResult ok+                             ploop fn d prompt prf' st h'   where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env+        checkNameType n = do+          ctxt <- getContext+          ist <- getIState+          imp <- impShow+          idrisCatch (do+              let h      = idris_outh ist+                  OK env = envAtFocus (proof e)+                  ctxt'  = envCtxt env ctxt+                  bnd    = map (\x -> (fst x, False)) env+                  ist'   = ist { tt_ctxt = ctxt' }+              putIState ist'+              -- Unlike the REPL, metavars have no special treatment, to+              -- make it easier to see how to prove with them.+              case lookupNames n ctxt' of+                [] -> ihPrintError h $ "No such variable " ++ show n+                ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)+              putIState ist+              return (False, e, False, prf, Right ""))+            (\err -> do putIState ist ; ierror err)++        checkType t = do+          ist <- getIState+          ctxt <- getContext+          idrisCatch (do+              let OK env = envAtFocus (proof e)+                  ctxt'  = envCtxt env ctxt+              putIState ist { tt_ctxt = ctxt' }+              (tm, ty) <- elabVal toplevel False t+              let ppo = ppOptionIst ist+                  ty'     = normaliseC ctxt [] ty+                  h       = idris_outh ist+                  infixes = idris_infixes ist+              case tm of+                 TType _ ->+                   ihPrintTermWithType h (prettyImp ppo PType) type1Doc+                 _ -> let bnd = map (\x -> (fst x, False)) env in+                      ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))+                                            (pprintPTerm ppo bnd [] infixes (delab ist ty))+              putIState ist+              return (False, e, False, prf, Right ""))+            (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)++        evalTerm t e = withErrorReflection $+          do ctxt <- getContext+             ist <- getIState+             idrisCatch (do+               let OK env = envAtFocus (proof e)+                   ctxt'  = envCtxt env ctxt+                   ist'   = ist { tt_ctxt = ctxt' }+                   bnd    = map (\x -> (fst x, False)) env+               putIState ist'+               (tm, ty) <- elabVal toplevel False t+               let tm'     = force (normaliseAll ctxt' env tm)+                   ty'     = force (normaliseAll ctxt' env ty)+                   ppo     = ppOption (idris_options ist')+                   infixes = idris_infixes ist+                   tmDoc   = pprintPTerm ppo bnd [] infixes (delab ist' tm')+                   tyDoc   = pprintPTerm ppo bnd [] infixes (delab ist' ty')+               ihPrintTermWithType (idris_outh ist') tmDoc tyDoc+               putIState ist+               return (False, e, False, prf, Right ""))+              (\err -> do putIState ist ; ierror err)

@@ -11,16 +11,14 @@  -- | Wrap a type provider in the type of type providers providerTy :: FC -> PTerm -> PTerm-providerTy fc tm +providerTy fc tm   = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] (sMN 0 "pvarg") tm]  ioret = sUN "prim_io_return" ermod = sNS (sUN "Error") ["Providers"] prmod = sNS (sUN "Provide") ["Providers"]-posmod = sNS (sUN "Postulate") ["Providers"]  data Provided a = Provide a-                | Postulate   deriving (Show, Eq, Functor)  -- | Handle an error, if the type provider returned an error. Otherwise return the provided term.@@ -35,10 +33,6 @@                   , (P _ nm _, [_, res]) <- unApply result                   , pioret == ioret && nm == prmod                       = return . Provide $ res-                  | (P _ pioret _, [tp, result]) <- unApply tm-                  , (P _ nm _, [_]) <- unApply result-                  , pioret == ioret && nm == posmod-                      = return Postulate                   | otherwise = ifail $ "Internal type provider error: result was not " ++                                         "IO (Provider a), or perhaps missing normalisation." 

@@ -110,7 +110,7 @@                           return ()             Just input -> -- H.catch                 do ms <- H.catch (lift $ processInput input orig mods)-                                 (ctrlC (return (Just mods))) +                                 (ctrlC (return (Just mods)))                    case ms of                         Just mods -> repl orig mods                         Nothing -> return ()@@ -121,7 +121,7 @@                           act -- repl orig mods           showMVs c thm [] = ""-         showMVs c thm ms = "Metavariables: " ++ +         showMVs c thm ms = "Metavariables: " ++                                  show' 4 c thm (map fst ms) ++ "\n"           show' 0 c thm ms = let l = length ms in@@ -129,7 +129,7 @@                              ++ " other"                              ++ if l == 1 then ")" else "s)"          show' n c thm [m] = showM c thm m-         show' n c thm (m : ms) = showM c thm m ++ ", " ++ +         show' n c thm (m : ms) = showM c thm m ++ ", " ++                                   show' (n - 1) c thm ms           showM c thm n = if c then colouriseFun thm (show n)@@ -240,11 +240,25 @@      i <- getIState      case parseCmd i "(input)" cmd of        Failure err -> iPrintError $ show (fixColour c err)-       Success (Prove n') -> do iPrintResult ""-                                idrisCatch-                                  (process stdout fn (Prove n'))-                                  (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)-                                isetPrompt (mkPrompt mods)+       Success (Prove n') ->+         idrisCatch+           (do process stdout fn (Prove n')+               isetPrompt (mkPrompt mods)+               case idris_outputmode i of+                 IdeSlave n -> -- signal completion of proof to ide+                   runIO . hPutStrLn stdout $+                     IdeSlave.convSExp "return"+                       (IdeSlave.SymbolAtom "ok", "")+                       n+                 _ -> return ())+           (\e -> do ist <- getIState+                     isetPrompt (mkPrompt mods)+                     case idris_outputmode i of+                       IdeSlave n ->+                         runIO . hPutStrLn stdout $+                           IdeSlave.convSExp "abandon-proof" "Abandoned" n+                       _ -> return ()+                     ihRenderError stdout $ pprintErr ist e)        Success cmd -> idrisCatch                         (ideslaveProcess fn cmd)                         (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)@@ -388,6 +402,7 @@                 (n:ns) -> Right $ sNS (sUN n) ns  ideslaveProcess :: FilePath -> Command -> Idris ()+ideslaveProcess fn Warranty = process stdout fn Warranty ideslaveProcess fn Help = process stdout fn Help ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)                                             iPrintResult "changed directory to"@@ -511,7 +526,7 @@        n <- case lookupNames n' ctxt of                  [x] -> return x                  [] -> return n'-                 ns -> ierror (CantResolveAlts (map show ns))+                 ns -> ierror (CantResolveAlts ns)        return n  removeProof :: Name -> Idris ()@@ -564,6 +579,7 @@  process :: Handle -> FilePath -> Command -> Idris () process h fn Help = iPrintResult displayHelp+process h fn Warranty = iPrintResult warranty process h fn (ChangeDirectory f)                  = do runIO $ setCurrentDirectory f                       return ()@@ -709,7 +725,7 @@         when (not (null cg')) $ do iputStrLn "Call graph:\n"                                    iputStrLn (show cg') process h fn (Search t) = searchByType h t-process h fn (CaseSplitAt updatefile l n) +process h fn (CaseSplitAt updatefile l n)     = caseSplitAt h fn updatefile l n process h fn (AddClauseFrom updatefile l n)     = addClauseFrom h fn updatefile l n@@ -793,7 +809,7 @@               [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')               [(n, (_,_,False))] -> return n               [(_, (_,_,True))]  -> ierror (Msg $ "Declarations not solvable using prover")-              ns -> ierror (CantResolveAlts (map show ns))+              ns -> ierror (CantResolveAlts (map fst ns))           prover (lit fn) n           -- recheck totality           i <- getIState@@ -1022,10 +1038,10 @@                    let ifiles = getModuleFiles modTree                    iLOG ("MODULE TREE : " ++ show modTree)                    iLOG ("RELOAD: " ++ show ifiles)-                   when (not (all ibc ifiles) || loadCode) $ +                   when (not (all ibc ifiles) || loadCode) $                         tryLoad False (filter (not . ibc) ifiles)                    -- return the files that need rechecking-                   return ifiles) +                   return ifiles)                       ninputs            inew <- getIState            let tidata = idris_tyinfodata inew@@ -1350,6 +1366,11 @@ getPkgMkDoc (PkgMkDoc str) = Just str getPkgMkDoc _              = Nothing +getPkgTest :: Opt          -- ^ the option to extract+           -> Maybe String -- ^ the package file to test+getPkgTest (PkgTest f) = Just f+getPkgTest _ = Nothing+ getCodegen :: Opt -> Maybe Codegen getCodegen (UseCodegen x) = Just x getCodegen _ = Nothing@@ -1395,6 +1416,20 @@          "    /  _/___/ /____(_)____                                     \n" ++          "    / // __  / ___/ / ___/     Version " ++ ver ++ "\n" ++          "  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      \n" ++-         " /___/\\__,_/_/  /_/____/       Type :? for help                \n"-+         " /___/\\__,_/_/  /_/____/       Type :? for help               \n" +++         "\n" +++         "Idris is free software with ABSOLUTELY NO WARRANTY.            \n" +++         "For details type :warranty." +warranty = "\n"                                                                          +++           "\t THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY  \n" +++           "\t EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE     \n" +++           "\t IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR    \n" +++           "\t PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE   \n" +++           "\t LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR   \n" +++           "\t CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF  \n" +++           "\t SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR       \n" +++           "\t BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, \n" +++           "\t WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE  \n" +++           "\t OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN\n" +++           "\t IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n"

@@ -33,6 +33,7 @@ pCmd :: P.IdrisParser Command pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)               <|> try (do cmd ["h", "?", "help"]; eof; return Help)+              <|> try (do cmd ["w", "warranty"]; eof; return Warranty)               <|> try (do cmd ["r", "reload"]; eof; return Reload)               <|> try (do cmd ["module"]; f <- P.identifier; eof;                           return (ModImport (toPath f)))@@ -48,11 +49,11 @@               <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))               <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))               <|> try (do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))-              <|> try (do cmd ["lto", "loadto"]; +              <|> try (do cmd ["lto", "loadto"];                           toline <- P.natural-                          f <- many anyChar; +                          f <- many anyChar;                           return (Load f (Just (fromInteger toline))))-              <|> try (do cmd ["l", "load"]; f <- many anyChar; +              <|> try (do cmd ["l", "load"]; f <- many anyChar;                           return (Load f Nothing))               <|> try (do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f))               <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))@@ -71,7 +72,7 @@               <|> try (do cmd ["color", "colour"]; pSetColourCmd)               <|> try (do cmd ["set"]; o <- pOption; return (SetOpt o))               <|> try (do cmd ["unset"]; o <- pOption; return (UnsetOpt o))-              <|> try (do cmd ["s", "search"]; P.whiteSpace; +              <|> try (do cmd ["s", "search"]; P.whiteSpace;                           t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t))               <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;                           upd <- option False (do P.lchar '!'; return True)@@ -183,7 +184,7 @@           doNoItalic i    = i { italic = False }           doSetColour c i = i { colour = c } -+-- | Generate the colour type names using the default Show instance. colourTypes :: [(String, ColourType)] colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $               enumFromTo minBound maxBound

@@ -26,7 +26,8 @@                          sourcedir :: String,                          modules :: [Name],                          idris_main :: Name,-                         execout :: Maybe String+                         execout :: Maybe String,+                         idris_tests :: [Name]                        }     deriving Show @@ -34,7 +35,7 @@   someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()  -defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (sUN "") Nothing+defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (sUN "") Nothing []  parseDesc :: FilePath -> IO PkgDesc parseDesc fp = do p <- readFile fp@@ -85,4 +86,8 @@              mk <- iName []              st <- get              put (st { makefile = Just (show mk) })+      <|> do reserved "tests"; lchar '=';+             ts <- sepBy1 (iName []) (lchar ',')+             st <- get+             put st { idris_tests = idris_tests st ++ ts } 

@@ -5,7 +5,7 @@ import System.Directory import System.Exit import System.IO-import System.FilePath ((</>), addTrailingPathSeparator, takeFileName, takeDirectory)+import System.FilePath ((</>), addTrailingPathSeparator, takeFileName, takeDirectory, normalise) import System.Directory (createDirectoryIfMissing, copyFile)  import Util.System@@ -159,6 +159,42 @@                         Left msg -> do putStrLn msg                                        exitWith (ExitFailure 1) +-- | Build a package with a sythesized main function that runs the tests+testPkg :: FilePath -> IO ()+testPkg fp+     = do pkgdesc <- parseDesc fp+          ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)+          when (and ok) $+            do dir <- getCurrentDirectory+               setCurrentDirectory $ dir </> sourcedir pkgdesc+               make (makefile pkgdesc)+               -- Get a temporary file to save the tests' source in+               (tmpn, tmph) <- tempIdr+               hPutStrLn tmph $+                 "module Test_______\n" +++                 concat ["import " ++ show m ++ "\n"+                         | m <- modules pkgdesc] +++                 "namespace Main\n" +++                 "  main : IO ()\n" +++                 "  main = do " +++                 concat [show t ++ "\n            "+                         | t <- idris_tests pkgdesc]+               hClose tmph+               (tmpn', tmph') <- tempfile+               hClose tmph'+               m_ist <- idris (Filename tmpn : NoREPL : Verbose : Output tmpn' : idris_opts pkgdesc)+               system tmpn'+               setCurrentDirectory dir+               case m_ist of+                 Nothing -> exitWith (ExitFailure 1)+                 Just ist -> do+                    -- Quit with error code if problem building+                    case errSpan ist of+                      Just _ -> exitWith (ExitFailure 1)+                      _      -> return ()+  where tempIdr :: IO (FilePath, Handle)+        tempIdr = do dir <- getTemporaryDirectory+                     openTempFile (normalise dir) "idristests.idr"  -- | Install package installPkg :: PkgDesc -> IO ()

@@ -0,0 +1,43 @@+module Main++%default total++-- An expensive function.+qib : Nat -> Nat+qib       Z   = 1+qib    (S Z)  = 2+qib (S (S n)) = qib n * qib (S n)++-- An equality whose size reflects the size of numbers.+data equals : Nat -> Nat -> Type where+    eqZ : Z `equals` Z+    eqS : m `equals` n -> S m `equals` S n++eq_refl : {n : Nat} -> n `equals` n+eq_refl {n = Z}   = eqZ+eq_refl {n = S n} = eqS eq_refl++-- Here, the proof is very expensive to compute.+-- We add a recursive argument to prevent Idris from inlining the function.+f : (r, n : Nat) -> Subset Nat (\k => qib n `equals` qib k)+f  Z    n = element n eq_refl+f (S r) n = f r n++-- A (contrived) relation, just to have something to show.+data represents : Nat -> Nat -> Type where+  axiom : (n : Nat) -> qib n `represents` n++-- Here, the witness is very expensive to compute.+-- We add a recursive argument to prevent Idris from inlining the function.+g : (r, n : Nat) -> Exists (\k : Nat => k `represents` n)+g  Z    n = evidence (qib n) (axiom n)+g (S r) n = g r n++fmt : qib n `represents` n -> String+fmt (axiom n) = "axiom " ++ show n++main : IO ()+main = do+    n <- map (const 10000) (putStrLn "*oink*")+    putStrLn . show $ getWitness (f 4 n)+    putStrLn . fmt  $ getProof   (g 4 n)

@@ -0,0 +1,3 @@+*oink*+10000+axiom 10000

@@ -0,0 +1,35 @@+#!/usr/bin/env bash++# From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting+# Here copied from reg039.+#+# Executes command with a timeout+# Params:+#   $1 timeout in seconds+#   $2 command+# Returns 1 if timed out 0 otherwise+timeout() {++    time=$1++    # start the command in a subshell to avoid problem with pipes+    # (spawn accepts one command)+    command="/bin/sh -c \"$2\""++    expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"++    if [ $? = 1 ] ; then+        echo "Timeout after ${time} seconds"+    fi++}++declare -a extraargs+for arg in "$@"+do+    extraargs=("${extraargs[@]}" "'$arg'")+done++timeout 10 "idris ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010"+timeout 5  "./basic010"+rm -f *.ibc basic010

@@ -4,10 +4,10 @@  %language TypeProviders -bad : IO (Provider _|_)-bad = pure Postulate+bad : IO (Provider Type)+bad = return $ pure _|_ -%provide (oops : _|_) with bad+%provide postulate oops with bad  main : IO () main = putStrLn "oops"

@@ -1,13 +0,0 @@-module Main--import Providers--%language TypeProviders--bad : IO (Provider _|_)-bad = pure Postulate--%provide postulate (oops : _|_) with bad--main : IO ()-main = putStrLn "oops"

@@ -1,13 +0,0 @@-module Main--import Providers--%language TypeProviders--bad : IO (Provider _|_)-bad = pure Postulate--%provide term (oops : _|_) with bad--main : IO ()-main = putStrLn "oops"

@@ -1,3 +1,1 @@ oops-oops-Attempted to provide a postulate where a term was expected.

@@ -3,10 +3,3 @@ idris $@ Postulate.idr -o postulate ./postulate rm -f postulate *.ibc--idris $@ Postulate2.idr -o postulate-./postulate-rm -f postulate *.ibc--idris $@ Postulate3.idr -o postulate-rm -f postulate *.ibc

@@ -8,7 +8,7 @@  class Set univ => HasPower univ where   Powerset : (a : univ) -> -             Exists univ (\Pa => (c : univ) -> +             Sigma univ (\Pa => (c : univ) ->                                  (isSubsetOf c a) -> member c Pa)  powerset : HasPower univ => univ -> univ

@@ -1,7 +1,7 @@ reg034.idr:6:5:When elaborating left hand side of bar: When elaborating an application of main.bar:         Can't unify-                [95mx[0m [94m=[0m [95mx[0m+                [92mlength[0m [95mys[0m [94m=[0m [92mlength[0m [95mys[0m         with                 [92mlength[0m [95mxs[0m [94m=[0m [92mlength[0m [95mys[0m         @@ -13,7 +13,7 @@ reg034.idr:9:5:When elaborating left hand side of foo: When elaborating an application of main.foo:         Can't unify-                [95mx[0m [94m=[0m [95mx[0m+                [95mf[0m [95my[0m [94m=[0m [95mf[0m [95my[0m         with                 [95mf[0m [95mx[0m [94m=[0m [95mf[0m [95my[0m         

@@ -0,0 +1,1 @@+[1, 2, 3]

@@ -0,0 +1,19 @@+module Main++data ListZ : Type -> Type where+  (::) : a -> Lazy (ListZ a) -> ListZ a+  Nil  : ListZ a++instance Show a => Show (ListZ a) where+  show xs = "[" ++ show' "" xs ++ "]"+      where+        show' acc Nil        = acc+        show' acc (x :: Nil) = acc ++ show x+        show' acc (x :: xs)  = show' (acc ++ show x ++ ", ") xs++foo : ListZ Nat+foo = (1 :: 2 :: 3 :: Nil)++main : IO ()+main = print foo+

@@ -0,0 +1,4 @@+#!/usr/bin/env bash+idris $@ reg045.idr -o reg045+./reg045+rm -f reg045 *.ibc

@@ -1,13 +1,13 @@ tutorial006a.idr:3:23:When elaborating right hand side of vapp: When elaborating argument [95mxs[0m to constructor [91mPrelude.Vect.::[0m:         Can't unify-                [94mVect[0m ([95mn[0m [92m+[0m [95mm[0m) [95ma[0m+                [94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m         with                 [94mVect[0m ([92mplus[0m [95mn[0m [95mm[0m) [95ma[0m                  Specifically:                 Can't unify-                        [92mplus[0m [95mn[0m [95mm[0m+                        [92mplus[0m [95mn[0m [95mn[0m                 with                         [92mplus[0m [95mn[0m [95mm[0m tutorial006b.idr:10:10:When elaborating right hand side of Main.parity: