disco 0.1.3.1 → 0.1.4

raw patch · 12 files changed

+134/−33 lines, 12 filesdep ~polysemy-zooPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: polysemy-zoo

API changes (from Hackage documentation)

Files

• CHANGELOG.md +13/−0
• disco.cabal +2/−2
• docs/tutorial/example/case-pattern.disco +1/−1
• example/grid.disco +45/−8
• src/Disco/Interactive/Commands.hs +7/−6
• src/Disco/Interpret/CESK.hs +1/−3
• src/Disco/Module.hs +7/−3
• src/Disco/Parser.hs +5/−4
• src/Disco/Typecheck.hs +46/−4
• src/Disco/Typecheck/Solve.hs +5/−0
• test/case-basic/case-basic.disco +1/−1
• test/types-tydef-qual/expected +1/−1

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

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

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

@@ -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) ?}

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

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

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

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

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

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

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

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