diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,16 @@ +* 0.1.4 (10 March 2022) + + - New features or syntax + - `if` and `when` are now synonyms + + - Bug fixes + - Only allow constructing sets and bags with element types + that can be compared ([#306](https://github.com/disco-lang/disco/issues/306)) + + - UI + - Test results are now printed in the same order in which + they were declared + * 0.1.3.1 (5 March 2022) - Fix [#340](https://github.com/disco-lang/disco/issues/340): disco 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.3.1 +version: 0.1.4 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 @@ -455,7 +455,7 @@ unbound-generics >= 0.3 && < 0.5, polysemy >= 1.6.0.0 && < 1.8, polysemy-plugin >= 0.4 && < 0.5, - polysemy-zoo >= 0.7 && < 0.8, + polysemy-zoo >= 0.7 && < 0.9, lens >= 4.14 && < 5.2, exact-combinatorics >= 0.2 && < 0.3, arithmoi >= 0.10 && < 0.13, diff --git a/docs/tutorial/example/case-pattern.disco b/docs/tutorial/example/case-pattern.disco --- a/docs/tutorial/example/case-pattern.disco +++ b/docs/tutorial/example/case-pattern.disco @@ -1,5 +1,5 @@ g : Z*Z -> Z g(p) = {? 0 when p is (3,_), - x + y when p is (x,y) if x > 5 or y > 20, + x + y when p is (x,y) when x > 5 or y > 20, -100 otherwise ?} diff --git a/example/grid.disco b/example/grid.disco --- a/example/grid.disco +++ b/example/grid.disco @@ -37,6 +37,7 @@ ||| where the first column contains the triangular numbers. !!! ∀ n : Nat. diagIso (diagIso' n) == n +!!! ∀ p : Nat * Nat. diagIso' (diagIso p) == p diagIso : ℕ×ℕ → ℕ diagIso (x,y) = (x+y)*(x+y+1)//2 + x @@ -54,22 +55,58 @@ ||| and ℕ×ℕ, but at the moment the disco type system doesn't let us ||| say that (and it likely never will). --- We have to be careful not to call powerIso' 0 because it gets stuck +-- We have to be careful not to call powerIsoPos' 0 because it gets stuck -- in infinite recursion! One way that would work is to write the -- test as follows: -!!! forall n:Nat. powerIso (powerIso' (n+1)) == (n+1) +!!! forall n:Nat. powerIsoPos (powerIsoPos' (n+1)) == (n+1) -- Alternatively, since 'implies' is lazy (i.e. "short-circuiting"), -- we can write -!!! ∀ n : Nat. (n > 0) ==> powerIso (powerIso' n) == n +!!! ∀ n : Nat. (n > 0) ==> powerIsoPos (powerIsoPos' n) == n -powerIso : ℕ×ℕ → ℕ -powerIso (x,y) = 2^x * (2y + 1) +powerIsoPos : ℕ×ℕ → ℕ +powerIsoPos (x,y) = 2^x * (2y + 1) -powerIso' : ℕ → ℕ×ℕ -powerIso' n = +powerIsoPos' : ℕ → ℕ×ℕ +powerIsoPos' n = {? (0, n//2) if not (2 divides n), - (x+1,y) when powerIso' (n//2) is (x,y) + (x+1,y) when powerIsoPos' (n//2) is (x,y) ?} + +||| We can turn powerIsoPos into an isomorphism between all natural +||| numbers and ℕ×ℕ simply by adding and subtracting one. + +!!! forall n:Nat. powerIso (powerIso' n) == n +!!! ∀ p : ℕ×ℕ. powerIso' (powerIso p) == p + +powerIso : ℕ×ℕ → ℕ +powerIso(p) = powerIsoPos(p) .- 1 + +powerIso' : ℕ → ℕ×ℕ +powerIso'(n) = powerIsoPos'(n+1) + + +||| And finally, there is a very cool isomorphism called "Morton +||| Z-order" which takes a pair of natural numbers, expresses them in +||| binary, and interleaves their binary representations to form a +||| single natural number. It ends up looking like this: +||| +||| 0 2 8 10 +||| 1 3 9 11 +||| 4 6 12 14 +||| 5 7 13 15 + +!!! forall n:N. zOrder(zOrder'(n)) == n +!!! forall p:N*N. zOrder'(zOrder(p)) == p + +zOrder : ℕ×ℕ → ℕ +zOrder(0,0) = 0 +zOrder(2m,n) = 2 * zOrder(n,m) +zOrder(2m+1,n) = 2 * zOrder(n,m) + 1 + +zOrder' : ℕ → ℕ×ℕ +zOrder'(0) = (0,0) +zOrder'(2n) = {? (2y,x) when zOrder'(n) is (x,y) ?} +zOrder'(2n+1) = {? (2y+1,x) when zOrder'(n) is (x,y) ?} 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 @@ -48,7 +48,7 @@ import Polysemy.Output import Polysemy.Reader -import Data.Maybe (maybeToList) +import Data.Maybe (mapMaybe, maybeToList) import Disco.AST.Surface import Disco.AST.Typed import Disco.Compile @@ -589,7 +589,7 @@ setREPLModule m -- Now run any tests - t <- inputToState $ runAllTests (m ^. miProps) + t <- inputToState $ runAllTests (m ^. miNames) (m ^. miProps) -- Evaluate and print any top-level terms forM_ (m ^. miTerms) (mapError EvalErr . evalTerm True . fst) @@ -602,18 +602,19 @@ -- XXX Return a structured summary of the results, not a Bool; -- separate out results generation and pretty-printing, & move this -- somewhere else. -runAllTests :: Members (Output Message ': Input TopInfo ': EvalEffects) r => Ctx ATerm [AProperty] -> Sem r Bool -- (Ctx ATerm [TestResult]) -runAllTests aprops +runAllTests :: Members (Output Message ': Input TopInfo ': EvalEffects) r => [QName Term] -> Ctx ATerm [AProperty] -> Sem r Bool -- (Ctx ATerm [TestResult]) +runAllTests declNames aprops | Ctx.null aprops = return True | otherwise = do info "Running tests..." - and <$> mapM (uncurry runTests) (Ctx.assocs aprops) + -- Use the order the names were defined in the module + and <$> mapM (uncurry runTests) (mapMaybe (\n -> (n,) <$> Ctx.lookup' (coerce n) aprops) declNames) where numSamples :: Int numSamples = 50 -- XXX make this configurable somehow - runTests :: Members (Output Message ': Input TopInfo ': EvalEffects) r => QName ATerm -> [AProperty] -> Sem r Bool + runTests :: Members (Output Message ': Input TopInfo ': EvalEffects) r => QName Term -> [AProperty] -> Sem r Bool runTests (QName _ n) props = do results <- inputTopEnv $ traverse (sequenceA . (id &&& runTest numSamples)) props let failures = P.filter (not . testIsOk . snd) results diff --git a/src/Disco/Interpret/CESK.hs b/src/Disco/Interpret/CESK.hs --- a/src/Disco/Interpret/CESK.hs +++ b/src/Disco/Interpret/CESK.hs @@ -21,8 +21,6 @@ ) where -import Text.Show.Pretty (ppShow) - import Unbound.Generics.LocallyNameless (Bind, Name) import Algebra.Graph @@ -547,7 +545,7 @@ valCmp (VBag cs1) (VBag cs2) = compareBags cs1 cs2 valCmp (VMap m1) (VMap m2) = compareMaps (M.assocs m1) (M.assocs m2) valCmp (VGraph g1) (VGraph g2) = valCmp (graphSummary g1) (graphSummary g2) -valCmp v1 v2 = error $ "valCmp " ++ show v1 ++ " " ++ show v2 +valCmp v1 v2 = error $ "valCmp\n " ++ take 100 (show v1) ++ "...\n " ++ take 100 (show v2) ++ "..." compareBags :: [(Value, Integer)] -> [(Value, Integer)] -> Ordering compareBags [] [] = EQ diff --git a/src/Disco/Module.hs b/src/Disco/Module.hs --- a/src/Disco/Module.hs +++ b/src/Disco/Module.hs @@ -97,6 +97,9 @@ data ModuleInfo = ModuleInfo { _miName :: ModuleName , _miImports :: Map ModuleName ModuleInfo + + -- List of names declared by the module, in the order they occur + , _miNames :: [QName Term] , _miDocs :: Ctx Term Docs , _miProps :: Ctx ATerm [AProperty] , _miTys :: TyCtx @@ -117,11 +120,12 @@ -- 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 ns1 d1 _ ty1 tyd1 tm1 tms1 es1 + <> ModuleInfo _ is2 ns2 d2 p2 ty2 tyd2 tm2 tms2 es2 = ModuleInfo n1 (is1 <> is2) + (ns1 <> ns2) (d2 <> d1) p2 (ty2 <> ty1) @@ -148,7 +152,7 @@ -- | The empty module info record. emptyModuleInfo :: ModuleInfo -emptyModuleInfo = ModuleInfo REPLModule M.empty emptyCtx emptyCtx emptyCtx M.empty emptyCtx [] S.empty +emptyModuleInfo = ModuleInfo REPLModule M.empty [] emptyCtx emptyCtx emptyCtx M.empty emptyCtx [] S.empty ------------------------------------------------------------ -- Module resolution diff --git a/src/Disco/Parser.hs b/src/Disco/Parser.hs --- a/src/Disco/Parser.hs +++ b/src/Disco/Parser.hs @@ -775,12 +775,13 @@ parseGuards :: Parser (Telescope Guard) parseGuards = (TelEmpty <$ reserved "otherwise") <|> (toTelescope <$> many parseGuard) --- | Parse a single guard (either @if@ or @when@) +-- | Parse a single guard (@if@, @if ... is@, or @let@) parseGuard :: Parser Guard -parseGuard = parseGBool <|> parseGPat <|> parseGLet +parseGuard = try parseGPat <|> parseGBool <|> parseGLet where - parseGBool = GBool <$> (embed <$> (reserved "if" *> parseTerm)) - parseGPat = GPat <$> (embed <$> (reserved "when" *> parseTerm)) + guardWord = reserved "if" <|> reserved "when" + parseGBool = GBool <$> (embed <$> (guardWord *> parseTerm)) + parseGPat = GPat <$> (embed <$> (guardWord *> parseTerm)) <*> (reserved "is" *> parsePattern) parseGLet = GLet <$> (reserved "let" *> parseBinding) diff --git a/src/Disco/Typecheck.hs b/src/Disco/Typecheck.hs --- a/src/Disco/Typecheck.hs +++ b/src/Disco/Typecheck.hs @@ -128,10 +128,13 @@ [] -> do 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 + return $ ModuleInfo name imports (map ((name .-) . getDeclName) typeDecls) docCtx aprops tyCtx tyDefnCtx defnCtx aterms es where getDefnName :: Defn -> Name ATerm getDefnName (Defn n _ _ _) = n + getDeclName :: TypeDecl -> Name Term + getDeclName (TypeDecl n _) = n + -------------------------------------------------- -- Type definitions @@ -1134,9 +1137,11 @@ constraints $ map (`CSub` tyv) tys return $ containerTy c tyv Check ty -> return ty - when (isJust ell) $ do - eltTy <- getEltTy c resTy - constraint $ CQual QEnum eltTy + eltTy <- getEltTy c resTy + + -- See Note [Container literal constraints] + when (c /= ListContainer && not (P.null xs)) $ constraint $ CQual QCmp eltTy + when (isJust ell) $ constraint $ CQual QEnum eltTy return $ ATContainer resTy c axns aell where @@ -1145,6 +1150,43 @@ => Mode -> Maybe (Ellipsis Term) -> Sem r (Maybe (Ellipsis ATerm)) typecheckEllipsis _ Nothing = return Nothing typecheckEllipsis m (Just (Until tm)) = Just . Until <$> typecheck m tm + +-- ~~~~ Note [Container literal constraints] +-- +-- It should only be possible to construct something of type Set(a) or +-- Bag(a) when a is comparable, so we can normalize the set or bag +-- value. For example, Set(N) is OK, but Set(N -> N) is not. On the +-- other hand, List(a) is fine for any type a. We want to maintain +-- the invariant that we can only actually obtain a value of type +-- Set(a) or Bag(a) if a is comparable. This means we will be able to +-- write polymorphic functions that take bags or sets as input without +-- having to specify any constraints --- the only way to call such +-- functions is with element types that actually support comparison. +-- For example, 'unions' can simply have the type Set(Set(a)) -> +-- Set(a). +-- +-- Hence, container literals (along with the 'set' and 'bag' +-- conversion functions) serve as "gatekeepers" to make sure we can +-- only construct containers with appropriate element types. So when +-- we see a container literal, if it is a bag or set literal, we have +-- to introduce an additional QCmp constraint for the element type. +-- +-- But not so fast --- with that rule, 'unions' does not type check! +-- To see why, look at the definition: +-- +-- unions(ss) = foldr(~∪~, {}, list(ss)) +-- +-- The empty set literal in the definition means we end up generating +-- a QCmp constraint on the element type anyway. But there is a +-- solution: we refine our invariant to say that we can only +-- actually obtain a *non-empty* value of type Set(a) or Bag(a) if a +-- is comparable. Empty bags and sets are allowed to have any element +-- type. This is safe because there is no way to generate a non-empty +-- set from an empty one, without also making use of something like a +-- non-empty set literal or conversion function. So we add a special +-- case to the rule that says we only add a QCmp constraint in the +-- case of a *non-empty* set or bag literal. Now the definition of +-- 'unions' type checks perfectly well. -- Container comprehensions typecheck mode tcc@(TContainerComp c bqt) = do diff --git a/src/Disco/Typecheck/Solve.hs b/src/Disco/Typecheck/Solve.hs --- a/src/Disco/Typecheck/Solve.hs +++ b/src/Disco/Typecheck/Solve.hs @@ -421,6 +421,11 @@ let ty' = body tys go (S.insert (t, tys, q) seen) ty' q + -- If we have a container type where the container is still a variable, + -- just replace it with List for the purposes of generating constraints--- + -- all containers (lists, bags, sets) have the same qualifier rules. + go seen (TyCon (CContainer (AVar _)) tys) q = go seen (TyCon CList tys) q + -- Otherwise, decompose a type constructor according to the qualRules. go seen ty@(TyCon c tys) q = case qualRules c q of Nothing -> throw $ Unqual q ty diff --git a/test/case-basic/case-basic.disco b/test/case-basic/case-basic.disco --- a/test/case-basic/case-basic.disco +++ b/test/case-basic/case-basic.disco @@ -1,7 +1,7 @@ foo : List(N) + Bool -> N foo x = {? n when x is left (n :: _), - 0 when x is left [], + 0 if x is left [], 1 when x is right True, 2 when x is right False ?} diff --git a/test/types-tydef-qual/expected b/test/types-tydef-qual/expected --- a/test/types-tydef-qual/expected +++ b/test/types-tydef-qual/expected @@ -1,5 +1,5 @@ Loading tydef-qual.disco... Running tests... - mirror: OK x: OK + mirror: OK Loaded.