diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,19 @@ +* 0.1.3.0 (3 March 2022) + + - New features or syntax + - `∈` now works as a synonym for `elem` + - add `→` and `↔` as synonyms for `->`, `<->` + + - Additional documentation for `|~|`, `power` + + - UI + - `--help`, `--version`, and the welcome message now all report + the current version number + - Typechecking errors now report the name of the thing being + typechecked when the failure occurred + - The values of top-level expressions are now printed when + `:load`ing + * 0.1.2.0 (12 February 2022) - New features or syntax diff --git a/disco.cabal b/disco.cabal --- a/disco.cabal +++ b/disco.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: disco -version: 0.1.2.0 +version: 0.1.3.0 synopsis: Functional programming language for teaching discrete math. description: Disco is a simple functional programming language for use in teaching discrete math. Its syntax is designed to be close @@ -160,6 +160,8 @@ test/parse-280/capitalvars.disco test/parse-280/expected test/parse-280/input + test/parse-320/expected + test/parse-320/input test/parse-case-expr/expected test/parse-case-expr/input test/parse-nested-list/expected @@ -256,6 +258,8 @@ test/solver-issue112/diag-iso-bad.disco test/solver-issue112/expected test/solver-issue112/input + test/syntax-abs/expected + test/syntax-abs/input test/syntax-chain/expected test/syntax-chain/inRange.disco test/syntax-chain/input @@ -343,6 +347,9 @@ test/types-tydef-param/expected test/types-tydef-param/input test/types-tydef-param/types-tydef-param.disco + test/types-tydef-qual/expected + test/types-tydef-qual/input + test/types-tydef-qual/tydef-qual.disco test/types-tydefs/expected test/types-tydefs/input test/types-tydefs/types-tydefs.disco diff --git a/src/Disco/Doc.hs b/src/Disco/Doc.hs --- a/src/Disco/Doc.hs +++ b/src/Disco/Doc.hs @@ -51,7 +51,10 @@ , PrimBOp Geq ==> "Greater-than-or-equal test. x >= y is true if x is greater than or equal to y." , PrimBOp CartProd ==> "Cartesian product, i.e. the collection of all pairs. Also works on bags and sets." - + , PrimPower ==> "Power set, i.e. the set of all subsets. Also works on bags." + , PrimBOp Union ==> "Union of two sets (or bags)." + , PrimBOp Inter ==> "Intersection of two sets (or bags)." + , PrimBOp Diff ==> "Difference of two sets (or bags)." ] -- | A map from some primitives to their corresponding page in the @@ -77,6 +80,10 @@ , PrimBOp Impl ==> "logic-ops" , PrimBOp Iff ==> "logic-ops" , PrimBOp CartProd ==> "cp" + , PrimPower ==> "power" + , PrimBOp Union ==> "set-ops" + , PrimBOp Inter ==> "set-ops" + , PrimBOp Diff ==> "set-ops" ] otherDoc :: Map String String @@ -100,6 +107,7 @@ , "Boolean" ==> docB , "Prop" ==> "The type of propositions." , "Set" ==> "The type of finite sets." + , "|~|" ==> "Absolute value, or the size of a collection." ] where docN = "The type of natural numbers: 0, 1, 2, ..." @@ -129,4 +137,5 @@ , "Boolean" ==> "bool" , "Prop" ==> "prop" , "Set" ==> "set" + , "|~|" ==> "size" ] diff --git a/src/Disco/Error.hs b/src/Disco/Error.hs --- a/src/Disco/Error.hs +++ b/src/Disco/Error.hs @@ -33,7 +33,8 @@ import Disco.Parser (DiscoParseError) import Disco.Pretty import Disco.Typecheck.Solve -import Disco.Typecheck.Util (TCError (..)) +import Disco.Typecheck.Util (LocTCError (..), + TCError (..)) import Disco.Types import Disco.Types.Qualifiers @@ -47,7 +48,7 @@ CyclicImport :: [ModuleName] -> DiscoError -- | Error encountered during typechecking. - TypeCheckErr :: TCError -> DiscoError + TypeCheckErr :: LocTCError -> DiscoError -- | Error encountered during parsing. ParseErr :: ParseErrorBundle String DiscoParseError -> DiscoError @@ -94,13 +95,18 @@ instance Pretty DiscoError where pretty = \case - ModuleNotFound m -> "Error: couldn't find a module named '" <> text m <> "'." - CyclicImport ms -> cyclicImportError ms - TypeCheckErr te -> prettyTCError te - ParseErr pe -> text (errorBundlePretty pe) - EvalErr ee -> prettyEvalError ee - Panic s -> - hcat + ModuleNotFound m -> "Error: couldn't find a module named '" <> text m <> "'." + CyclicImport ms -> cyclicImportError ms + TypeCheckErr (LocTCError Nothing te) -> prettyTCError te + TypeCheckErr (LocTCError (Just n) te) -> + vcat + [ "While checking " <> pretty' n <> ":" + , nest 2 $ prettyTCError te + ] + ParseErr pe -> text (errorBundlePretty pe) + EvalErr ee -> prettyEvalError ee + Panic s -> + vcat [ "Bug! " <> text s , "Please report this as a bug at https://github.com/disco-lang/disco/issues/ ." ] diff --git a/src/Disco/Eval.hs b/src/Disco/Eval.hs --- a/src/Disco/Eval.hs +++ b/src/Disco/Eval.hs @@ -29,7 +29,7 @@ -- * Running things , runDisco - , runTCM, runTCMWith + , runTCM , inputTopEnv , parseDiscoModule , typecheckTop @@ -50,7 +50,7 @@ import Control.Arrow ((&&&)) import Control.Exception (SomeException, handle) import Control.Lens (makeLenses, toListOf, view, (%~), - (.~), (^.)) + (.~), (<>~), (^.)) import Control.Monad (unless, void, when) import Control.Monad.IO.Class (liftIO) import Data.Bifunctor @@ -235,26 +235,31 @@ -------------------------------------------------- -- Type checking --- | Run a typechecking computation, providing it with local --- (initially empty) contexts for variable types and type --- definitions. +-- | Run a typechecking computation, providing it with local contexts +-- (initialized to the provided arguments) for variable types and +-- type definitions. runTCM :: Member (Error DiscoError) r => - Sem (Reader TyCtx ': Reader TyDefCtx ': Fresh ': Error TCError ': r) a -> + TyCtx -> + TyDefCtx -> + Sem (Reader TyCtx ': Reader TyDefCtx ': Fresh ': Error LocTCError ': r) a -> Sem r a -runTCM = runTCMWith emptyCtx M.empty +runTCM tyCtx tyDefCtx = + mapError TypeCheckErr + . runFresh + . runReader @TyDefCtx tyDefCtx + . runReader @TyCtx tyCtx --- | Run a typechecking computation, providing it with local contexts --- (initialized to the provided arguments) for variable types and --- type definitions. -runTCMWith :: +-- | A variant of 'runTCM' that requires only a 'TCError' instead +-- of a 'LocTCError'. +runTCM' :: Member (Error DiscoError) r => TyCtx -> TyDefCtx -> Sem (Reader TyCtx ': Reader TyDefCtx ': Fresh ': Error TCError ': r) a -> Sem r a -runTCMWith tyCtx tyDefCtx = - mapError TypeCheckErr +runTCM' tyCtx tyDefCtx = + mapError (TypeCheckErr . noLoc) . runFresh . runReader @TyDefCtx tyDefCtx . runReader @TyCtx tyCtx @@ -270,7 +275,7 @@ imptyctx <- inputs (toListOf (replModInfo . miImports . traverse . miTys)) tydefs <- inputs (view (replModInfo . miTydefs)) imptydefs <- inputs (toListOf (replModInfo . miImports . traverse . miTydefs)) - runTCMWith (tyctx <> mconcat imptyctx) (tydefs <> mconcat imptydefs) tcm + runTCM' (tyctx <> mconcat imptyctx) (tydefs <> mconcat imptydefs) tcm -------------------------------------------------- -- Loading @@ -359,7 +364,7 @@ tydefns = case mode of { Standalone -> M.empty ; REPL -> topTyDefns } -- Typecheck (and resolve names in) the module. - m <- runTCMWith tyctx tydefns $ checkModule name importMap cm + m <- runTCM tyctx tydefns $ checkModule name importMap cm -- Evaluate all the module definitions and add them to the topEnv. mapError EvalErr $ loadDefsFrom m @@ -382,10 +387,7 @@ addToREPLModule :: Members '[Error DiscoError, State TopInfo, Random, State Mem, Output Message] r => ModuleInfo -> Sem r () -addToREPLModule mi = do - curMI <- use @TopInfo replModInfo - mi' <- mapError TypeCheckErr $ combineModuleInfo [curMI, mi] - modify @TopInfo $ replModInfo .~ mi' +addToREPLModule mi = modify @TopInfo (replModInfo <>~ mi) -- | Set the given 'ModuleInfo' record as the currently loaded -- module. This also includes updating the top-level state with new diff --git a/src/Disco/Interactive/CmdLine.hs b/src/Disco/Interactive/CmdLine.hs --- a/src/Disco/Interactive/CmdLine.hs +++ b/src/Disco/Interactive/CmdLine.hs @@ -24,8 +24,11 @@ ) where +import Data.Version (showVersion) +import Paths_disco (version) + import Control.Lens hiding (use) -import Control.Monad (unless) +import Control.Monad (unless, when) import qualified Control.Monad.Catch as CMC import Control.Monad.IO.Class (MonadIO (..)) import Data.Foldable (forM_) @@ -55,15 +58,24 @@ -- | Command-line options for disco. data DiscoOpts = DiscoOpts - { evaluate :: Maybe String -- ^ A single expression to evaluate - , cmdFile :: Maybe String -- ^ Execute the commands in a given file - , checkFile :: Maybe String -- ^ Check a file and then exit - , debugFlag :: Bool + { onlyVersion :: Bool -- ^ Should we just print the version? + , evaluate :: Maybe String -- ^ A single expression to evaluate + , cmdFile :: Maybe String -- ^ Execute the commands in a given file + , checkFile :: Maybe String -- ^ Check a file and then exit + , debugFlag :: Bool } discoOpts :: O.Parser DiscoOpts discoOpts = DiscoOpts - <$> O.optional ( + <$> O.switch ( + mconcat + [ O.long "version" + , O.short 'v' + , O.help "show current version" + ] + ) + + <*> O.optional ( O.strOption (mconcat [ O.long "evaluate" , O.short 'e' @@ -94,11 +106,14 @@ ] ) +discoVersion :: String +discoVersion = showVersion version + discoInfo :: O.ParserInfo DiscoOpts discoInfo = O.info (O.helper <*> discoOpts) $ mconcat [ O.fullDesc , O.progDesc "Command-line interface for Disco, a programming language for discrete mathematics." - , O.header "disco v0.1" + , O.header $ "disco " ++ discoVersion ] optsToCfg :: DiscoOpts -> DiscoConfig @@ -109,11 +124,15 @@ ------------------------------------------------------------ banner :: String -banner = "Welcome to Disco!\n\nA language for programming discrete mathematics.\n\n" +banner = "Welcome to Disco, version " ++ discoVersion ++ "!\n\nA language for programming discrete mathematics.\n\n" discoMain :: IO () discoMain = do opts <- O.execParser discoInfo + + when (onlyVersion opts) $ do + putStrLn discoVersion + exitSuccess let batch = any isJust [evaluate opts, cmdFile opts, checkFile opts] unless batch $ putStr banner diff --git a/src/Disco/Interactive/Commands.hs b/src/Disco/Interactive/Commands.hs --- a/src/Disco/Interactive/Commands.hs +++ b/src/Disco/Interactive/Commands.hs @@ -591,6 +591,9 @@ -- Now run any tests t <- inputToState $ runAllTests (m ^. miProps) + -- Evaluate and print any top-level terms + forM_ (m ^. miTerms) (mapError EvalErr . evalTerm True . fst) + -- Remember which was the most recently loaded file, so we can :reload modify @TopInfo (lastFile ?~ fp) info "Loaded." diff --git a/src/Disco/Module.hs b/src/Disco/Module.hs --- a/src/Disco/Module.hs +++ b/src/Disco/Module.hs @@ -23,7 +23,7 @@ import Control.Lens (Getting, foldOf, makeLenses, view) -import Control.Monad (filterM, foldM) +import Control.Monad (filterM) import Control.Monad.IO.Class (MonadIO (..)) import Data.Bifunctor (first) import Data.Map (Map) @@ -39,7 +39,6 @@ import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind) import Polysemy -import Polysemy.Error import Disco.AST.Surface import Disco.AST.Typed @@ -48,7 +47,7 @@ import Disco.Names import Disco.Pretty hiding ((<>)) import Disco.Typecheck.Erase (erase, erasePattern) -import Disco.Typecheck.Util (TCError (..), TyCtx) +import Disco.Typecheck.Util (TyCtx) import Disco.Types import Paths_disco @@ -110,6 +109,31 @@ makeLenses ''ModuleInfo +instance Semigroup ModuleInfo where + -- | Two ModuleInfos + -- are merged by joining their doc, type, type definition, and term + -- contexts. The property context of the new module is the one + -- obtained from the second module. The name of the new module is + -- taken from the first. Definitions from later modules override + -- earlier ones. Note that this function should really only be used + -- for the special top-level REPL module. + ModuleInfo n1 is1 d1 _ ty1 tyd1 tm1 tms1 es1 + <> ModuleInfo _ is2 d2 p2 ty2 tyd2 tm2 tms2 es2 + = ModuleInfo + n1 + (is1 <> is2) + (d2 <> d1) + p2 + (ty2 <> ty1) + (tyd2 <> tyd1) + (tm2 <> tm1) + (tms1 <> tms2) + (es1 <> es2) + +instance Monoid ModuleInfo where + mempty = emptyModuleInfo + mappend = (<>) + -- | Get something from a module and its direct imports. withImports :: Monoid a => Getting a ModuleInfo a -> ModuleInfo -> a withImports l = view l <> foldOf (miImports . traverse . l) @@ -125,32 +149,6 @@ -- | The empty module info record. emptyModuleInfo :: ModuleInfo emptyModuleInfo = ModuleInfo REPLModule M.empty emptyCtx emptyCtx emptyCtx M.empty emptyCtx [] S.empty - --- | Merges a list of ModuleInfos into one ModuleInfo. Two ModuleInfos --- are merged by joining their doc, type, type definition, and term --- contexts. The property context of the new module is the one --- obtained from the second module. The name of the new module is --- taken from the first. Definitions from later modules override --- earlier ones. Note that this function should really only be used --- for the special top-level REPL module. -combineModuleInfo :: Member (Error TCError) r => [ModuleInfo] -> Sem r ModuleInfo -combineModuleInfo = foldM combineMods emptyModuleInfo - where - combineMods :: Member (Error TCError) r => ModuleInfo -> ModuleInfo -> Sem r ModuleInfo - combineMods - (ModuleInfo n1 is1 d1 _ ty1 tyd1 tm1 tms1 es1) - (ModuleInfo _ is2 d2 p2 ty2 tyd2 tm2 tms2 es2) = - return $ - ModuleInfo - n1 - (is1 <> is2) - (d2 <> d1) - p2 - (ty2 <> ty1) - (tyd2 <> tyd1) - (tm2 <> tm1) - (tms1 <> tms2) - (es1 <> es2) ------------------------------------------------------------ -- Module resolution diff --git a/src/Disco/Parser.hs b/src/Disco/Parser.hs --- a/src/Disco/Parser.hs +++ b/src/Disco/Parser.hs @@ -75,9 +75,11 @@ import Disco.AST.Surface import Disco.Extensions import Disco.Module +import Disco.Pretty (prettyStr) import Disco.Syntax.Operators import Disco.Syntax.Prims import Disco.Types +import Polysemy (run) ------------------------------------------------------------ -- Lexer @@ -105,13 +107,27 @@ initParserState :: ParserState initParserState = ParserState NoIndent S.empty +-- OpaqueTerm is a wrapper around Term just to make ShowErrorComponent +-- happy, which requires Eq and Ord instances; but we can't make Term +-- an instance of either. +newtype OpaqueTerm = OT Term +instance Show OpaqueTerm where + show (OT t) = show t +instance Eq OpaqueTerm where + _ == _ = True +instance Ord OpaqueTerm where + compare _ _ = EQ + data DiscoParseError = ReservedVarName String + | InvalidPattern OpaqueTerm deriving (Show, Eq, Ord) instance ShowErrorComponent DiscoParseError where - showErrorComponent (ReservedVarName x) = "keyword \"" ++ x ++ "\" cannot be used as a variable name" + showErrorComponent (ReservedVarName x) = "keyword \"" ++ x ++ "\" cannot be used as a variable name" + showErrorComponent (InvalidPattern (OT t)) = "Invalid pattern: " ++ run (prettyStr t) errorComponentLen (ReservedVarName x) = length x + errorComponentLen (InvalidPattern _) = 1 -- | A parser is a megaparsec parser of strings, with an extra layer -- of state to keep track of the current indentation level and @@ -774,7 +790,7 @@ parseAtomicPattern = label "pattern" $ do t <- parseAtom case termToPattern t of - Nothing -> fail $ "Invalid pattern: " ++ show t + Nothing -> customFailure $ InvalidPattern (OT t) Just p -> return p -- | Parse a pattern, by parsing a term and then attempting to convert @@ -783,7 +799,7 @@ parsePattern = label "pattern" $ do t <- parseTerm case termToPattern t of - Nothing -> fail $ "Invalid pattern: " ++ show t + Nothing -> customFailure $ InvalidPattern (OT t) Just p -> return p -- | Attempt converting a term to a pattern. diff --git a/src/Disco/Syntax/Operators.hs b/src/Disco/Syntax/Operators.hs --- a/src/Disco/Syntax/Operators.hs +++ b/src/Disco/Syntax/Operators.hs @@ -172,8 +172,8 @@ ] , [ bopInfo InR Or ["\\/", "or", "∨", "||"] ] - , [ bopInfo InR Impl ["->", "==>", "implies"] - , bopInfo InR Iff ["<->", "<==>", "iff"] + , [ bopInfo InR Impl ["->", "==>", "→", "implies"] + , bopInfo InR Iff ["<->", "<==>", "↔", "iff"] ] ] where diff --git a/src/Disco/Typecheck.hs b/src/Disco/Typecheck.hs --- a/src/Disco/Typecheck.hs +++ b/src/Disco/Typecheck.hs @@ -106,7 +106,7 @@ -- imports should already be checked and passed in as the second -- argument. checkModule - :: Members '[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r + :: Members '[Output Message, Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh] r => ModuleName -> Map ModuleName ModuleInfo -> Module -> Sem r ModuleInfo checkModule name imports (Module es _ m docs terms) = do let (typeDecls, defns, tydefs) = partitionDecls m @@ -114,20 +114,20 @@ -- XXX this isn't right, if multiple modules define the same type synonyms. -- Need to use a normal Ctx for tydefs too. importTyDefnCtx = M.unions (imports ^.. traverse . miTydefs) - tyDefnCtx <- makeTyDefnCtx tydefs + tyDefnCtx <- mapError noLoc $ makeTyDefnCtx tydefs withTyDefns (tyDefnCtx `M.union` importTyDefnCtx) $ do - tyCtx <- makeTyCtx name typeDecls + tyCtx <- mapError noLoc $ makeTyCtx name typeDecls extends importTyCtx $ extends tyCtx $ do - mapM_ checkTyDefn tydefs + mapM_ (checkTyDefn name) tydefs adefns <- mapM (checkDefn name) defns let defnCtx = ctxForModule name (map (getDefnName &&& id) adefns) docCtx = ctxForModule name docs dups = filterDups . map getDefnName $ adefns case dups of - (x:_) -> throw $ DuplicateDefns (coerce x) + (x:_) -> throw $ noLoc $ DuplicateDefns (coerce x) [] -> do - aprops <- checkProperties docCtx - aterms <- mapM inferTop terms + aprops <- mapError noLoc $ checkProperties docCtx -- XXX location? + aterms <- mapError noLoc $ mapM inferTop terms -- XXX location? return $ ModuleInfo name imports docCtx aprops tyCtx tyDefnCtx defnCtx aterms es where getDefnName :: Defn -> Name ATerm getDefnName (Defn n _ _ _) = n @@ -153,8 +153,8 @@ [] -> return . M.fromList $ map convert tydefs -- | Check the validity of a type definition. -checkTyDefn :: Members '[Reader TyDefCtx, Error TCError] r => TypeDefn -> Sem r () -checkTyDefn defn@(TypeDefn x args body) = do +checkTyDefn :: Members '[Reader TyDefCtx, Error LocTCError] r => ModuleName -> TypeDefn -> Sem r () +checkTyDefn name defn@(TypeDefn x args body) = mapError (LocTCError (Just (name .- string2Name x))) $ do -- First, make sure the body is a valid type, i.e. everything inside -- it is well-kinded. @@ -255,9 +255,9 @@ -- | Type check a top-level definition in the given module. checkDefn - :: Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output Message] r + :: Members '[Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh, Output Message] r => ModuleName -> TermDefn -> Sem r Defn -checkDefn name (TermDefn x clauses) = do +checkDefn name (TermDefn x clauses) = mapError (LocTCError (Just (name .- x))) $ do -- Check that all clauses have the same number of patterns checkNumPats clauses diff --git a/src/Disco/Typecheck/Util.hs b/src/Disco/Typecheck/Util.hs --- a/src/Disco/Typecheck/Util.hs +++ b/src/Disco/Typecheck/Util.hs @@ -28,7 +28,7 @@ import Disco.AST.Surface import Disco.Context import Disco.Messages -import Disco.Names (ModuleName) +import Disco.Names (ModuleName, QName) import Disco.Typecheck.Constraints import Disco.Typecheck.Solve import Disco.Types @@ -43,6 +43,16 @@ ------------------------------------------------------------ -- Errors ------------------------------------------------------------ + +-- | A typechecking error, wrapped up together with the name of the +-- thing that was being checked when the error occurred. +data LocTCError = LocTCError (Maybe (QName Term)) TCError + deriving Show + +-- | Wrap a @TCError@ into a @LocTCError@ with no explicit provenance +-- information. +noLoc :: TCError -> LocTCError +noLoc = LocTCError Nothing -- | Potential typechecking errors. data TCError diff --git a/test/error-ambiguous/expected b/test/error-ambiguous/expected --- a/test/error-ambiguous/expected +++ b/test/error-ambiguous/expected @@ -1,8 +1,9 @@ Loading ambiguous.disco... Loading a.disco... Loading b.disco... -Error: the name x is ambiguous. It could refer to: - a.x - ambiguous.x - b.x -https://disco-lang.readthedocs.io/en/latest/reference/ambiguous.html +While checking ambiguous.y: + Error: the name x is ambiguous. It could refer to: + a.x + ambiguous.x + b.x + https://disco-lang.readthedocs.io/en/latest/reference/ambiguous.html diff --git a/test/error-cyclic/expected b/test/error-cyclic/expected --- a/test/error-cyclic/expected +++ b/test/error-cyclic/expected @@ -1,3 +1,4 @@ Loading cyclic.disco... -Error: cyclic type definition for A. -https://disco-lang.readthedocs.io/en/latest/reference/cyc-ty.html +While checking cyclic.A: + Error: cyclic type definition for A. + https://disco-lang.readthedocs.io/en/latest/reference/cyc-ty.html diff --git a/test/error-duplicatedefns/expected b/test/error-duplicatedefns/expected --- a/test/error-duplicatedefns/expected +++ b/test/error-duplicatedefns/expected @@ -1,3 +1,4 @@ Loading dupdefns.disco... -Error: duplicate definition for x. -https://disco-lang.readthedocs.io/en/latest/reference/dup-def.html +While checking dupdefns.x: + Error: duplicate definition for x. + https://disco-lang.readthedocs.io/en/latest/reference/dup-def.html diff --git a/test/error-notype/expected b/test/error-notype/expected --- a/test/error-notype/expected +++ b/test/error-notype/expected @@ -1,3 +1,4 @@ -Error: the definition of x must have an accompanying type signature. -Try writing something like 'x : Int' (or whatever the type of x should be) first. -https://disco-lang.readthedocs.io/en/latest/reference/missingtype.html +While checking REPL.x: + Error: the definition of x must have an accompanying type signature. + Try writing something like 'x : Int' (or whatever the type of x should be) first. + https://disco-lang.readthedocs.io/en/latest/reference/missingtype.html diff --git a/test/error-numpatterns/expected b/test/error-numpatterns/expected --- a/test/error-numpatterns/expected +++ b/test/error-numpatterns/expected @@ -1,3 +1,4 @@ Loading numpatterns.disco... -Error: number of arguments does not match. -https://disco-lang.readthedocs.io/en/latest/reference/num-args.html +While checking numpatterns.f: + Error: number of arguments does not match. + https://disco-lang.readthedocs.io/en/latest/reference/num-args.html diff --git a/test/error-pattype/expected b/test/error-pattype/expected --- a/test/error-pattype/expected +++ b/test/error-pattype/expected @@ -1,14 +1,17 @@ -Error: the pattern - left(x) -is supposed to have type - List(ℤ), -but instead it has a sum type. -https://disco-lang.readthedocs.io/en/latest/reference/pattern-type.html -Error: the pattern - (x1, y) -is supposed to have type - ℕ, -but instead it has a product type. -https://disco-lang.readthedocs.io/en/latest/reference/pattern-type.html -Error: the shape of two types does not match. -https://disco-lang.readthedocs.io/en/latest/reference/shape-mismatch.html +While checking REPL.f: + Error: the pattern + left(x) + is supposed to have type + List(ℤ), + but instead it has a sum type. + https://disco-lang.readthedocs.io/en/latest/reference/pattern-type.html +While checking REPL.g: + Error: the pattern + (x1, y) + is supposed to have type + ℕ, + but instead it has a product type. + https://disco-lang.readthedocs.io/en/latest/reference/pattern-type.html +While checking REPL.h: + Error: the shape of two types does not match. + https://disco-lang.readthedocs.io/en/latest/reference/shape-mismatch.html diff --git a/test/error-polyrec/expected b/test/error-polyrec/expected --- a/test/error-polyrec/expected +++ b/test/error-polyrec/expected @@ -1,4 +1,5 @@ Loading polyrec.disco... -Error: in the definition of Bush(a): recursive occurrences of Bush may only have type variables as arguments. - Bush(a × a) does not follow this rule. -https://disco-lang.readthedocs.io/en/latest/reference/no-poly-rec.html +While checking polyrec.Bush: + Error: in the definition of Bush(a): recursive occurrences of Bush may only have type variables as arguments. + Bush(a × a) does not follow this rule. + https://disco-lang.readthedocs.io/en/latest/reference/no-poly-rec.html diff --git a/test/error-qualskolem/expected b/test/error-qualskolem/expected --- a/test/error-qualskolem/expected +++ b/test/error-qualskolem/expected @@ -1,4 +1,5 @@ Loading qualskolem.disco... -Error: type variable a represents any type, so we cannot assume values of that type - can be subtracted. -https://disco-lang.readthedocs.io/en/latest/reference/qual-skolem.html +While checking qualskolem.f: + Error: type variable a represents any type, so we cannot assume values of that type + can be subtracted. + https://disco-lang.readthedocs.io/en/latest/reference/qual-skolem.html diff --git a/test/error-unboundtyvar/expected b/test/error-unboundtyvar/expected --- a/test/error-unboundtyvar/expected +++ b/test/error-unboundtyvar/expected @@ -1,3 +1,4 @@ Loading unboundtyvar.disco... -Error: Unknown type variable 'b'. -https://disco-lang.readthedocs.io/en/latest/reference/unbound-tyvar.html +While checking unboundtyvar.T: + Error: Unknown type variable 'b'. + https://disco-lang.readthedocs.io/en/latest/reference/unbound-tyvar.html diff --git a/test/error-unqual-base/expected b/test/error-unqual-base/expected --- a/test/error-unqual-base/expected +++ b/test/error-unqual-base/expected @@ -1,3 +1,4 @@ Loading unqualbase.disco... -Error: values of type ℕ cannot be subtracted. -https://disco-lang.readthedocs.io/en/latest/reference/not-qual.html +While checking unqualbase.f: + Error: values of type ℕ cannot be subtracted. + https://disco-lang.readthedocs.io/en/latest/reference/not-qual.html diff --git a/test/parse-320/expected b/test/parse-320/expected new file mode 100644 --- /dev/null +++ b/test/parse-320/expected @@ -0,0 +1,4 @@ +false +Error: there is nothing named nottrue. +https://disco-lang.readthedocs.io/en/latest/reference/unbound.html +5 diff --git a/test/parse-320/input b/test/parse-320/input new file mode 100644 --- /dev/null +++ b/test/parse-320/input @@ -0,0 +1,5 @@ +not true +nottrue +nottrue : Int +nottrue = 5 +nottrue diff --git a/test/parse-top-term/expected b/test/parse-top-term/expected --- a/test/parse-top-term/expected +++ b/test/parse-top-term/expected @@ -1,2 +1,4 @@ Loading parse-top-term.disco... +20 +36 Loaded. diff --git a/test/solver-issue112/expected b/test/solver-issue112/expected --- a/test/solver-issue112/expected +++ b/test/solver-issue112/expected @@ -1,5 +1,6 @@ Loading diag-iso-bad.disco... -Error: typechecking failed. -https://disco-lang.readthedocs.io/en/latest/reference/typecheck-fail.html +While checking diag-iso-bad.diagIso': + Error: typechecking failed. + https://disco-lang.readthedocs.io/en/latest/reference/typecheck-fail.html Error: typechecking failed. https://disco-lang.readthedocs.io/en/latest/reference/typecheck-fail.html diff --git a/test/syntax-abs/expected b/test/syntax-abs/expected new file mode 100644 --- /dev/null +++ b/test/syntax-abs/expected @@ -0,0 +1,16 @@ +5 +1/2 +5 +1/2 +4 +10 +[2, 1, 0, 1, 2] +21 +10 +0 +0 +3 +3 +15 +4 +4 diff --git a/test/syntax-abs/input b/test/syntax-abs/input new file mode 100644 --- /dev/null +++ b/test/syntax-abs/input @@ -0,0 +1,16 @@ +|5| +|1/2| +|-5| +|-1/2| +|1 + 3| +|1 + |2 - 5| + 6| +[ |x| | x <- [-2 .. 2] ] +3|5 + 2| +|-3| + |2| + |5| +|2 + {? 3 if true || false, 4 otherwise ?} - 5| +|{}| +|{1,2,3}| +| {1, 3, 1, 2} | +|{1,2,3}| * |-5| +|bag [1,3,1,2]| +|[1,3,1,2]| diff --git a/test/types-toomanypats/expected b/test/types-toomanypats/expected --- a/test/types-toomanypats/expected +++ b/test/types-toomanypats/expected @@ -1,3 +1,4 @@ Loading toomanypats.disco... -Error: number of arguments does not match. -https://disco-lang.readthedocs.io/en/latest/reference/num-args.html +While checking toomanypats.f: + Error: number of arguments does not match. + https://disco-lang.readthedocs.io/en/latest/reference/num-args.html diff --git a/test/types-tydef-bad/expected b/test/types-tydef-bad/expected --- a/test/types-tydef-bad/expected +++ b/test/types-tydef-bad/expected @@ -1,3 +1,4 @@ Loading types-tydef-bad.disco... -Error: there is no built-in or user-defined type named 'Flerb'. -https://disco-lang.readthedocs.io/en/latest/reference/no-tydef.html +While checking types-tydef-bad.X: + Error: there is no built-in or user-defined type named 'Flerb'. + https://disco-lang.readthedocs.io/en/latest/reference/no-tydef.html diff --git a/test/types-tydef-kind/expected b/test/types-tydef-kind/expected --- a/test/types-tydef-kind/expected +++ b/test/types-tydef-kind/expected @@ -1,3 +1,4 @@ Loading types-tydef-kind.disco... -Error: not enough arguments for the type 'Foo'. -https://disco-lang.readthedocs.io/en/latest/reference/num-args-type.html +While checking types-tydef-kind.Foo: + Error: not enough arguments for the type 'Foo'. + https://disco-lang.readthedocs.io/en/latest/reference/num-args-type.html diff --git a/test/types-tydef-qual/expected b/test/types-tydef-qual/expected new file mode 100644 --- /dev/null +++ b/test/types-tydef-qual/expected @@ -0,0 +1,5 @@ +Loading tydef-qual.disco... +Running tests... + mirror: OK + x: OK +Loaded. diff --git a/test/types-tydef-qual/input b/test/types-tydef-qual/input new file mode 100644 --- /dev/null +++ b/test/types-tydef-qual/input @@ -0,0 +1,1 @@ +:load test/types-tydef-qual/tydef-qual.disco diff --git a/test/types-tydef-qual/tydef-qual.disco b/test/types-tydef-qual/tydef-qual.disco new file mode 100644 --- /dev/null +++ b/test/types-tydef-qual/tydef-qual.disco @@ -0,0 +1,18 @@ +type S = List(Char) + +!!! x == "hi" +x : S +x = "hi" + +type T(a) = Unit + a * T(a) * T(a) + +leaf : T(a) +leaf = left(unit) + +testT : T(N) +testT = right(3, right(4, right(1, leaf, leaf), right(6, leaf, leaf)), right(9, leaf, leaf)) + +!!! mirror(mirror(testT)) == testT +mirror : T(a) -> T(a) +mirror(left(unit)) = left(unit) +mirror(right(a,l,r)) = right(a, mirror(r), mirror(l))