diff --git a/idris.cabal b/idris.cabal --- a/idris.cabal +++ b/idris.cabal @@ -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 diff --git a/libs/base/Providers.idr b/libs/base/Providers.idr --- a/libs/base/Providers.idr +++ b/libs/base/Providers.idr @@ -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 diff --git a/libs/effects/Effect/File.idr b/libs/effects/Effect/File.idr --- a/libs/effects/Effect/File.idr +++ b/libs/effects/Effect/File.idr @@ -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 ] diff --git a/libs/effects/Effect/StdIO.idr b/libs/effects/Effect/StdIO.idr --- a/libs/effects/Effect/StdIO.idr +++ b/libs/effects/Effect/StdIO.idr @@ -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 diff --git a/libs/prelude/Builtins.idr b/libs/prelude/Builtins.idr --- a/libs/prelude/Builtins.idr +++ b/libs/prelude/Builtins.idr @@ -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 diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr --- a/libs/prelude/Prelude.idr +++ b/libs/prelude/Prelude.idr @@ -21,6 +21,7 @@ import Prelude.Bits import Prelude.Stream import Prelude.Uninhabited +import Prelude.Pairs import Decidable.Equality diff --git a/libs/prelude/Prelude/Algebra.idr b/libs/prelude/Prelude/Algebra.idr --- a/libs/prelude/Prelude/Algebra.idr +++ b/libs/prelude/Prelude/Algebra.idr @@ -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 diff --git a/libs/prelude/Prelude/Pairs.idr b/libs/prelude/Prelude/Pairs.idr new file mode 100644 --- /dev/null +++ b/libs/prelude/Prelude/Pairs.idr @@ -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. diff --git a/libs/prelude/Prelude/Strings.idr b/libs/prelude/Prelude/Strings.idr --- a/libs/prelude/Prelude/Strings.idr +++ b/libs/prelude/Prelude/Strings.idr @@ -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. ||| diff --git a/libs/prelude/Prelude/Vect.idr b/libs/prelude/Prelude/Vect.idr --- a/libs/prelude/Prelude/Vect.idr +++ b/libs/prelude/Prelude/Vect.idr @@ -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 -------------------------------------------------------------------------------- diff --git a/libs/prelude/prelude.ipkg b/libs/prelude/prelude.ipkg --- a/libs/prelude/prelude.ipkg +++ b/libs/prelude/prelude.ipkg @@ -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 diff --git a/main/Main.hs b/main/Main.hs --- a/main/Main.hs +++ b/main/Main.hs @@ -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 diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -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 diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs --- a/src/Idris/AbsSyntaxTree.hs +++ b/src/Idris/AbsSyntaxTree.hs @@ -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 _ _ = [] - diff --git a/src/Idris/CaseSplit.hs b/src/Idris/CaseSplit.hs --- a/src/Idris/CaseSplit.hs +++ b/src/Idris/CaseSplit.hs @@ -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) diff --git a/src/Idris/CmdOptions.hs b/src/Idris/CmdOptions.hs --- a/src/Idris/CmdOptions.hs +++ b/src/Idris/CmdOptions.hs @@ -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") diff --git a/src/Idris/Colours.hs b/src/Idris/Colours.hs --- a/src/Idris/Colours.hs +++ b/src/Idris/Colours.hs @@ -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) diff --git a/src/Idris/Core/CaseTree.hs b/src/Idris/Core/CaseTree.hs --- a/src/Idris/Core/CaseTree.hs +++ b/src/Idris/Core/CaseTree.hs @@ -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 diff --git a/src/Idris/Core/Elaborate.hs b/src/Idris/Core/Elaborate.hs --- a/src/Idris/Core/Elaborate.hs +++ b/src/Idris/Core/Elaborate.hs @@ -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 diff --git a/src/Idris/Core/Evaluate.hs b/src/Idris/Core/Evaluate.hs --- a/src/Idris/Core/Evaluate.hs +++ b/src/Idris/Core/Evaluate.hs @@ -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 diff --git a/src/Idris/Core/ProofState.hs b/src/Idris/Core/ProofState.hs --- a/src/Idris/Core/ProofState.hs +++ b/src/Idris/Core/ProofState.hs @@ -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 diff --git a/src/Idris/Core/TT.hs b/src/Idris/Core/TT.hs --- a/src/Idris/Core/TT.hs +++ b/src/Idris/Core/TT.hs @@ -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 diff --git a/src/Idris/DeepSeq.hs b/src/Idris/DeepSeq.hs --- a/src/Idris/DeepSeq.hs +++ b/src/Idris/DeepSeq.hs @@ -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` () diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs --- a/src/Idris/Delaborate.hs +++ b/src/Idris/Delaborate.hs @@ -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 diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs --- a/src/Idris/ElabDecls.hs +++ b/src/Idris/ElabDecls.hs @@ -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 diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs --- a/src/Idris/ElabTerm.hs +++ b/src/Idris/ElabTerm.hs @@ -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" diff --git a/src/Idris/Erasure.hs b/src/Idris/Erasure.hs --- a/src/Idris/Erasure.hs +++ b/src/Idris/Erasure.hs @@ -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"] diff --git a/src/Idris/Help.hs b/src/Idris/Help.hs --- a/src/Idris/Help.hs +++ b/src/Idris/Help.hs @@ -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 diff --git a/src/Idris/IdeSlave.hs b/src/Idris/IdeSlave.hs --- a/src/Idris/IdeSlave.hs +++ b/src/Idris/IdeSlave.hs @@ -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 [] = [] diff --git a/src/Idris/Interactive.hs b/src/Idris/Interactive.hs --- a/src/Idris/Interactive.hs +++ b/src/Idris/Interactive.hs @@ -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 diff --git a/src/Idris/Output.hs b/src/Idris/Output.hs --- a/src/Idris/Output.hs +++ b/src/Idris/Output.hs @@ -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 diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs --- a/src/Idris/Parser.hs +++ b/src/Idris/Parser.hs @@ -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 @ diff --git a/src/Idris/Prover.hs b/src/Idris/Prover.hs --- a/src/Idris/Prover.hs +++ b/src/Idris/Prover.hs @@ -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) diff --git a/src/Idris/Providers.hs b/src/Idris/Providers.hs --- a/src/Idris/Providers.hs +++ b/src/Idris/Providers.hs @@ -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." diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs --- a/src/Idris/REPL.hs +++ b/src/Idris/REPL.hs @@ -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" diff --git a/src/Idris/REPLParser.hs b/src/Idris/REPLParser.hs --- a/src/Idris/REPLParser.hs +++ b/src/Idris/REPLParser.hs @@ -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 diff --git a/src/Pkg/PParser.hs b/src/Pkg/PParser.hs --- a/src/Pkg/PParser.hs +++ b/src/Pkg/PParser.hs @@ -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 } diff --git a/src/Pkg/Package.hs b/src/Pkg/Package.hs --- a/src/Pkg/Package.hs +++ b/src/Pkg/Package.hs @@ -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 () diff --git a/test/basic010/Main.idr b/test/basic010/Main.idr new file mode 100644 --- /dev/null +++ b/test/basic010/Main.idr @@ -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) diff --git a/test/basic010/expected b/test/basic010/expected new file mode 100644 --- /dev/null +++ b/test/basic010/expected @@ -0,0 +1,3 @@ +*oink* +10000 +axiom 10000 diff --git a/test/basic010/run b/test/basic010/run new file mode 100644 --- /dev/null +++ b/test/basic010/run @@ -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 diff --git a/test/ffi005/Postulate.idr b/test/ffi005/Postulate.idr --- a/test/ffi005/Postulate.idr +++ b/test/ffi005/Postulate.idr @@ -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" diff --git a/test/ffi005/Postulate2.idr b/test/ffi005/Postulate2.idr deleted file mode 100644 --- a/test/ffi005/Postulate2.idr +++ /dev/null @@ -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" diff --git a/test/ffi005/Postulate3.idr b/test/ffi005/Postulate3.idr deleted file mode 100644 --- a/test/ffi005/Postulate3.idr +++ /dev/null @@ -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" diff --git a/test/ffi005/expected b/test/ffi005/expected --- a/test/ffi005/expected +++ b/test/ffi005/expected @@ -1,3 +1,1 @@ oops -oops -Attempted to provide a postulate where a term was expected. diff --git a/test/ffi005/run b/test/ffi005/run --- a/test/ffi005/run +++ b/test/ffi005/run @@ -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 diff --git a/test/reg030/reg030.idr b/test/reg030/reg030.idr --- a/test/reg030/reg030.idr +++ b/test/reg030/reg030.idr @@ -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 diff --git a/test/reg034/expected b/test/reg034/expected --- a/test/reg034/expected +++ b/test/reg034/expected @@ -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 - x = x + length ys = length ys with length xs = length ys @@ -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 - x = x + f y = f y with f x = f y diff --git a/test/reg045/expected b/test/reg045/expected new file mode 100644 --- /dev/null +++ b/test/reg045/expected @@ -0,0 +1,1 @@ +[1, 2, 3] diff --git a/test/reg045/reg045.idr b/test/reg045/reg045.idr new file mode 100644 --- /dev/null +++ b/test/reg045/reg045.idr @@ -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 + diff --git a/test/reg045/run b/test/reg045/run new file mode 100644 --- /dev/null +++ b/test/reg045/run @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +idris $@ reg045.idr -o reg045 +./reg045 +rm -f reg045 *.ibc diff --git a/test/tutorial006/expected b/test/tutorial006/expected --- a/test/tutorial006/expected +++ b/test/tutorial006/expected @@ -1,13 +1,13 @@ tutorial006a.idr:3:23:When elaborating right hand side of vapp: When elaborating argument xs to constructor Prelude.Vect.::: Can't unify - Vect (n + m) a + Vect (n + n) a with Vect (plus n m) a Specifically: Can't unify - plus n m + plus n n with plus n m tutorial006b.idr:10:10:When elaborating right hand side of Main.parity: