disco 0.1.2.0 → 0.1.3.0

raw patch · 34 files changed

+299/−130 lines, 34 filesdep ~optparse-applicativePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: optparse-applicative

API changes (from Hackage documentation)

Files

• CHANGELOG.md +16/−0
• disco.cabal +8/−1
• src/Disco/Doc.hs +10/−1
• src/Disco/Error.hs +15/−9
• src/Disco/Eval.hs +21/−19
• src/Disco/Interactive/CmdLine.hs +27/−8
• src/Disco/Interactive/Commands.hs +3/−0
• src/Disco/Module.hs +27/−29
• src/Disco/Parser.hs +19/−3
• src/Disco/Syntax/Operators.hs +2/−2
• src/Disco/Typecheck.hs +11/−11
• src/Disco/Typecheck/Util.hs +11/−1
• test/error-ambiguous/expected +6/−5
• test/error-cyclic/expected +3/−2
• test/error-duplicatedefns/expected +3/−2
• test/error-notype/expected +4/−3
• test/error-numpatterns/expected +3/−2
• test/error-pattype/expected +17/−14
• test/error-polyrec/expected +4/−3
• test/error-qualskolem/expected +4/−3
• test/error-unboundtyvar/expected +3/−2
• test/error-unqual-base/expected +3/−2
• test/parse-320/expected +4/−0
• test/parse-320/input +5/−0
• test/parse-top-term/expected +2/−0
• test/solver-issue112/expected +3/−2
• test/syntax-abs/expected +16/−0
• test/syntax-abs/input +16/−0
• test/types-toomanypats/expected +3/−2
• test/types-tydef-bad/expected +3/−2
• test/types-tydef-kind/expected +3/−2
• test/types-tydef-qual/expected +5/−0
• test/types-tydef-qual/input +1/−0
• test/types-tydef-qual/tydef-qual.disco +18/−0

@@ -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

@@ -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

@@ -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"   ]

@@ -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/ ."         ]

@@ -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

@@ -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

@@ -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."

@@ -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

@@ -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.

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -0,0 +1,4 @@+false+Error: there is nothing named nottrue.+https://disco-lang.readthedocs.io/en/latest/reference/unbound.html+5

@@ -0,0 +1,5 @@+not true+nottrue+nottrue : Int+nottrue = 5+nottrue

@@ -1,2 +1,4 @@ Loading parse-top-term.disco...+20+36 Loaded.

@@ -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

@@ -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

@@ -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]|

@@ -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

@@ -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

@@ -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

@@ -0,0 +1,5 @@+Loading tydef-qual.disco...+Running tests...+  mirror: OK+  x: OK+Loaded.

@@ -0,0 +1,1 @@+:load 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))