disco 0.1.6 → 0.2

raw patch · 129 files changed

+3795/−1712 lines, 129 filesdep +boxesdep +constraintsdep +edit-distancedep −polysemy-zoodep ~QuickCheckdep ~basedep ~containersPVP ok

version bump matches the API change (PVP)

Dependencies added: boxes, constraints, edit-distance, infinite-list, oeis2, random, reflection, text

Dependencies removed: polysemy-zoo

Dependency ranges changed: QuickCheck, base, containers, filepath, lens, megaparsec, unbound-generics

API changes (from Hackage documentation)

Files

• CHANGELOG.md +19/−0
• LICENSE +36/−0
• README.md +9/−68
• disco.cabal +51/−25
• example/catalan.disco +19/−0
• example/demo.disco +1/−1
• example/fib.disco +47/−0
• example/lists.disco +0/−12
• example/rsa.disco +36/−5
• example/tree.disco +1/−1
• lib/oeis.disco +13/−0
• src/Disco/AST/Core.hs +30/−41
• src/Disco/AST/Generic.hs +0/−4
• src/Disco/AST/Surface.hs +15/−11
• src/Disco/Compile.hs +63/−25
• src/Disco/Context.hs +0/−4
• src/Disco/Desugar.hs +63/−48
• src/Disco/Doc.hs +185/−133
• src/Disco/Effects/Input.hs +6/−4
• src/Disco/Effects/LFresh.hs +3/−10
• src/Disco/Effects/Random.hs +0/−32
• src/Disco/Enumerate.hs +6/−19
• src/Disco/Error.hs +26/−26
• src/Disco/Eval.hs +13/−3
• src/Disco/Exhaustiveness.hs +417/−0
• src/Disco/Exhaustiveness/Constraint.hs +151/−0
• src/Disco/Exhaustiveness/Possibilities.hs +59/−0
• src/Disco/Exhaustiveness/TypeInfo.hs +183/−0
• src/Disco/Interactive/Commands.hs +253/−93
• src/Disco/Interpret/CESK.hs +106/−75
• src/Disco/Messages.hs +1/−5
• src/Disco/Module.hs +6/−9
• src/Disco/Parser.hs +38/−31
• src/Disco/Pretty.hs +24/−9
• src/Disco/Pretty/Prec.hs +19/−3
• src/Disco/Property.hs +22/−38
• src/Disco/Subst.hs +1/−5
• src/Disco/Syntax/Operators.hs +12/−19
• src/Disco/Syntax/Prims.hs +87/−114
• src/Disco/Typecheck.hs +198/−86
• src/Disco/Typecheck/Constraints.hs +15/−18
• src/Disco/Typecheck/Solve.hs +159/−129
• src/Disco/Typecheck/Unify.hs +3/−6
• src/Disco/Typecheck/Util.hs +26/−24
• src/Disco/Types.hs +9/−4
• src/Disco/Types/Rules.hs +4/−8
• src/Disco/Util.hs +53/−4
• src/Disco/Value.hs +75/−48
• src/Polysemy/ConstraintAbsorber.hs +53/−0
• src/Polysemy/ConstraintAbsorber/MonadCatch.hs +128/−0
• src/Polysemy/Random.hs +63/−0
• stack.yaml +4/−6
• test/Tests.hs +56/−45
• test/arith-basic-un/expected +2/−0
• test/arith-count/expected +3/−3
• test/arith-numthry/expected +10/−10
• test/compile-misc/expected +1/−1
• test/containers-cmp/expected +2/−2
• test/containers-each/expected +18/−0
• test/containers-merge/input +4/−4
• test/containers-ops/expected +22/−22
• test/containers-reduce/expected +5/−2
• test/error-expdivbyzero/expected +5/−0
• test/error-expdivbyzero/input +5/−0
• test/error-tyargs/error-tyargs.disco +1/−1
• test/error-tyargs/expected +3/−3
• test/error-tyargs/input +4/−4
• test/error-unbound/expected +14/−0
• test/error-unbound/input +7/−0
• test/error-unboundtyvar/expected +2/−1
• test/error-unboundtyvar/unboundtyvar.disco +1/−1
• test/graphs-basic/expected +3/−0
• test/graphs-equality/expected +4/−4
• test/list-poly/expected +2/−2
• test/logic-bools/expected +34/−32
• test/logic-bools/input +2/−0
• test/logic-cmp/expected +43/−43
• test/logic-cmp/input +6/−6
• test/map-basic/expected +21/−3
• test/map-compare/expected +4/−4
• test/parse-320/expected +1/−1
• test/parse-case-expr/expected +1/−1
• test/parse-try/expected +7/−0
• test/parse-try/input +1/−0
• test/poly-infer-sort/expected +17/−1
• test/poly-instantiate/expected +15/−3
• test/pretty-ops/expected +1/−1
• test/pretty-type/expected +1/−1
• test/prop-basic/expected +2/−2
• test/prop-basic/input +2/−2
• test/prop-binary/expected +202/−204
• test/prop-fail/bad-tests.disco +4/−4
• test/prop-fail/expected +11/−4
• test/prop-fairness/expected +4/−4
• test/prop-higher-order/expected +4/−3
• test/prop-higher-order/input +2/−2
• test/prop-holds/expected +7/−7
• test/prop-impredicative/prop-impredicative.disco +1/−1
• test/prop-type/expected +3/−3
• test/repl-ann/expected +1/−1
• test/repl-defn/expected +1/−1
• test/repl-doc/expected +21/−4
• test/repl-help/expected +1/−0
• test/repl-import/expected +1/−1
• test/repl-proptest/expected +12/−8
• test/repl-proptest/input +3/−3
• test/syntax-chain/expected +14/−14
• test/syntax-decimals/expected +33/−19
• test/syntax-decimals/input +14/−0
• test/syntax-lambda/expected +1/−1
• test/syntax-types/expected +1/−1
• test/table-error/expected +2/−0
• test/table-error/input +2/−0
• test/table-function/expected +160/−0
• test/table-function/input +11/−0
• test/table-list/expected +55/−0
• test/table-list/input +13/−0
• test/types-192/expected +3/−0
• test/types-char-string/expected +2/−2
• test/types-compare/expected +1/−1
• test/types-container/expected +21/−0
• test/types-naked-ops/expected +13/−1
• test/types-ops/expected +3/−3
• test/types-standalone-ops/expected +5/−3
• test/types-syntax/expected +7/−0
• test/types-syntax/input +7/−0
• test/types-tydef-param/expected +1/−1
• test/types-tydef-param/types-tydef-param.disco +1/−1
• test/types-tydef-qual/tydef-qual.disco +4/−4

@@ -1,3 +1,22 @@+* 0.2 (22 January 2025)++  - Allow `><` as syntax for product types+  - Use syntax `T` and `F` for booleans+  - New `:table` command+  - Suggest alternate variable names based on edit distance+  - Fix crash when computing `0^(-1)`+  - `min` and `max` are now prefix instead of infix+  - Display multiple example types for things with nontrivial polymorphism (#388)+  - Randomness primitives (Justin Grubbs, #390)+  - Automatic memoization (Justin Grubbs, #394)+  - Remove decimal output+  - Function pattern coverage checking (Colin Phillips, #434)+  - A lot more documentation, including the start of a "gentle+    introduction"+  - Add support for GHC 9.10 and drop 9.4+  - Better parser for `:load` (#430)+  - Better test result reporting (#428)+ * 0.1.6 (16 December 2023)    - A bunch more documentation

@@ -29,3 +29,39 @@ THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.++++Licensing for polysemy-zoo code:+Portions of the code as noted are covered under the following license:++Copyright Sandy Maguire (c) 2019++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Sandy Maguire nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -5,17 +5,6 @@ programming principles in the context of a discrete mathematics course. -Using Disco on replit.com------------------------------If you just want to *use* disco (*i.e.* if you are a student, or just-checking out the language), the recommended way is to use it via-`replit.com`.  Simply [visit this-REPL](https://replit.com/@BrentYorgey/Disco#README.md) and follow the-instructions there to fork your own copy, where you will be able to-evaluate Disco expressions, and edit and run your own `.disco` files,-all via your web browser, without installing anything on your computer.- Design principles ----------------- @@ -52,64 +41,16 @@ If you'd like to contribute to disco development, check out [CONTRIBUTING.md](CONTRIBUTING.md). -Building with stack----------------------First, make sure you have-[the `stack` tool](https://docs.haskellstack.org/en/stable/README/)-(the easiest way to install it is via [ghcup](https://www.haskell.org/ghcup/)).-Then open a command prompt, navigate to the root directory of this-repository, and execute--```-stack build-```--After this completes, you should be able to--```-stack exec disco-```--to run the Disco command-line REPL.--While developing, you may want to use a command like--```-stack test --fast --file-watch --ghc-options='-Wall'-```--which will turn on warnings, turn off optimizations for a faster-edit-compile-test cycle, and automatically recompile and run the test-suite every time a source file changes.--Installation---------------If for some reasons you want to actually install `disco` on your-computer, follow the below instructions.  (If you want to *contribute*-to disco development, you should skip to the instructions about-building with stack.)--**Note**, if you are a student, you should **not** need to do this!-The above instructions about using `disco` on `replit.com` should be-all you need.  The below instructions are kept here for completeness.+Building disco+-------------- -- Follow the instructions to [install-  ghcup](https://www.haskell.org/ghcup/) by opening a terminal or-  command prompt and copy-pasting the given installation command.  You-  can just accept all the defaults.  If you don't have [Windows-  Subsystem for Linux](https://docs.microsoft.com/en-us/windows/wsl/)-  (if you don't know what that is, then you don't have it), see the-  [instructions here](https://www.haskell.org/ghcup/install/) for a-  PowerShell command to run.-    - If you use PowerShell, note that after running the magic-      PowerShell command to set up `ghcup`, you need to close and-      reopen PowerShell in order for it to recognize the `cabal`-      command.+- The first step is to install the Haskell programming language (the+  language in which Disco is implemented).  If you don't already have+  Haskell installed, you can [follow the directions+  here](http://ozark.hendrix.edu/~yorgey/install-haskell.html). -- Run `cabal update`, which will download the latest information about-  Haskell packages.+- Now, at a command prompt, run `cabal update`, which will download+  the latest information about Haskell packages.  - Now run `cabal install disco` at a command prompt. @@ -155,7 +96,7 @@ - If installation seems like it succeeded but the `disco` command is   not recognized, it may be an issue with your path environment   variable settings.  Try running `disco` using an explicit path:-    - `~/.cabal/bin/disco` on Linux or OSX+    - `~/.cabal/bin/disco` on Linux, OSX, or WSL2     - `C:\cabal\bin\disco` on Windows     - If those don't work, poke around and see if you can figure       out where the `cabal/bin` folder is on your computer, and

@@ -1,6 +1,6 @@ cabal-version:       2.4 name:                disco-version:             0.1.6+version:             0.2 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@@ -12,7 +12,7 @@ copyright:           Disco team 2016-2022 (see LICENSE) category:            Language -tested-with:         GHC ==8.10.7 || ==9.2.5 || ==9.4.3+tested-with:         GHC ==9.6.6 || ==9.8.4 || ==9.10.1  data-dir:            lib @@ -89,6 +89,8 @@                      test/error-duplicatetydefns/input                      test/error-emptycase/expected                      test/error-emptycase/input+                     test/error-expdivbyzero/expected+                     test/error-expdivbyzero/input                      test/error-names/expected                      test/error-names/input                      test/error-nonlinear/expected@@ -177,6 +179,8 @@                      test/parse-top-term/expected                      test/parse-top-term/input                      test/parse-top-term/parse-top-term.disco+                     test/parse-try/expected+                     test/parse-try/input                      test/poly-bad/expected                      test/poly-bad/input                      test/poly-infer-sort/expected@@ -315,6 +319,12 @@                      test/syntax-tuples/input                      test/syntax-types/expected                      test/syntax-types/input+                     test/table-error/expected+                     test/table-error/input+                     test/table-function/expected+                     test/table-function/input+                     test/table-list/expected+                     test/table-list/input                      test/types-192/expected                      test/types-192/input                      test/types-306/expected@@ -347,6 +357,8 @@                      test/types-squash/input                      test/types-standalone-ops/expected                      test/types-standalone-ops/input+                     test/types-syntax/expected+                     test/types-syntax/input                      test/types-toomanypats/expected                      test/types-toomanypats/input                      test/types-toomanypats/toomanypats.disco@@ -409,7 +421,6 @@                        Disco.Effects.Fresh                        Disco.Effects.Input                        Disco.Effects.LFresh-                       Disco.Effects.Random                        Disco.Effects.State                        Disco.Effects.Store                        Disco.AST.Core@@ -434,6 +445,10 @@                        Disco.Value                        Disco.Error                        Disco.Eval+                       Disco.Exhaustiveness+                       Disco.Exhaustiveness.Constraint+                       Disco.Exhaustiveness.Possibilities+                       Disco.Exhaustiveness.TypeInfo                        Disco.Interpret.CESK                        Disco.Subst                        Disco.Typecheck@@ -452,39 +467,48 @@                        Disco.Doc    other-modules:       Paths_disco+                       Polysemy.ConstraintAbsorber+                       Polysemy.ConstraintAbsorber.MonadCatch+                       Polysemy.Random+   autogen-modules:     Paths_disco -  build-depends:       base >=4.8 && <4.18,+  build-depends:       base >=4.8 && <4.21,                        filepath,                        directory,                        mtl >=2.2 && <2.4,-                       megaparsec >= 6.1.1 && < 9.6,+                       megaparsec >= 6.1.1 && < 9.7,                        parser-combinators >= 1.0.0 && < 1.4,                        prettyprinter >=1.7 && < 1.8,                        split >= 0.2 && < 0.3,                        transformers >= 0.4 && < 0.7,-                       containers >=0.5 && <0.7,-                       unbound-generics >= 0.3 && < 0.4.3,-                       -- unbound-generics 0.4.3 added substBvs to-                       -- Subst class which adds a new Generic-                       -- constraint, hence a breaking change+                       containers >=0.5 && <0.8,+                       unbound-generics >= 0.4.4 && < 0.5,+                       -- Need the Alpha and Subst instances for+                       -- NonEmpty from unbound-generics 0.4.4                        polysemy >= 1.6.0.0 && < 1.10,                        polysemy-plugin >= 0.4 && < 0.5,-                       polysemy-zoo >= 0.7 && < 0.9,-                       lens >= 4.14 && < 5.3,+                       reflection >= 2.1.7 && < 2.2,+                       random >= 1.2.1.1 && < 1.3,+                       constraints >= 0.13.4 && < 0.15,+                       text >= 2.0.2 && < 2.2,+                       lens >= 4.14 && < 5.4,                        exact-combinatorics >= 0.2 && < 0.3,                        arithmoi >= 0.10 && < 0.14,                        integer-logarithms >= 1.0 && < 1.1,                        simple-enumeration >= 0.2 && < 0.3,                        haskeline >=0.8 && <0.9,                        exceptions >= 0.10 && < 0.11,-                       QuickCheck >= 2.9 && < 2.15,+                       QuickCheck >= 2.9 && < 2.16,                        splitmix >= 0.1 && < 0.2,                        fgl >= 5.5 && < 5.9,                        optparse-applicative >= 0.12 && < 0.19,-                       -- oeis2 < 1.1,+                       oeis2 >= 1.0.9 && < 1.1,                        algebraic-graphs >= 0.5 && < 0.8,-                       pretty-show >= 1.10 && < 1.11+                       pretty-show >= 1.10 && < 1.11,+                       boxes >= 0.1.5 && < 0.2,+                       edit-distance >= 0.2 && < 0.3,+                       infinite-list >= 0.1 && < 0.2,    hs-source-dirs:      src   default-language:    Haskell2010@@ -501,12 +525,12 @@                        haskeline >=0.8 && <0.9,                        mtl >=2.2 && <2.4,                        transformers >= 0.4 && < 0.7,-                       megaparsec >= 6.1.1 && < 9.6,-                       containers >= 0.5 && < 0.7,-                       unbound-generics >= 0.3 && < 0.4.3,-                       lens >= 4.14 && < 5.3,-                       optparse-applicative >= 0.12 && < 0.19-                       -- oeis2 < 1.1+                       megaparsec >= 6.1.1 && < 9.7,+                       containers >= 0.5 && < 0.8,+                       unbound-generics >= 0.3 && < 0.5,+                       lens >= 4.14 && < 5.4,+                       optparse-applicative >= 0.12 && < 0.19,+                       oeis2 >= 1.0.9 && < 1.1    default-language:    Haskell2010 @@ -516,11 +540,12 @@   main-is: Tests.hs   hs-source-dirs: test   ghc-options: -threaded-  build-depends:    base >= 4.7 && < 4.18,+  build-tool-depends: disco:disco+  build-depends:    base >= 4.7 && < 4.21,                     tasty >= 0.10 && < 1.6,                     tasty-golden >= 2.3 && < 2.4,                     directory >= 1.2 && < 1.4,-                    filepath >= 1.4 && < 1.5,+                    filepath >= 1.4 && < 1.6,                     process >= 1.4 && < 1.7,                     bytestring >= 0.9 && < 0.13,                     disco@@ -532,8 +557,9 @@   main-is: TestExamples.hs   hs-source-dirs: example   ghc-options: -threaded-  build-depends:    base >= 4.7 && < 4.18,+  build-tool-depends: disco:disco+  build-depends:    base >= 4.7 && < 4.21,                     directory >= 1.2 && < 1.4,-                    filepath >= 1.4 && < 1.5,+                    filepath >= 1.4 && < 1.6,                     process >= 1.4 && < 1.7   default-language: Haskell2010

@@ -0,0 +1,19 @@+import list+import oeis++-- The type of binary tree shapes: empty tree, or a pair of subtrees.+type BT = Unit + BT*BT++-- Generate the list of all binary tree shapes of a given size.+treesOfSize : N -> List(BT)+treesOfSize(0)   = [left(■)]+treesOfSize(k+1) =+  [ right (l,r) | x <- [0 .. k], l <- treesOfSize(x), r <- treesOfSize(k .- x) ]++-- Compute first few Catalan numbers by brute force.+catalan1 : List(N)+catalan1 = each(\k. length(treesOfSize(k)), [0..4])++-- Extend the sequence via the OEIS.+catalan : List(N)+catalan = extendSequence(catalan1)

@@ -26,4 +26,4 @@  height : P(a) -> N height (left(_)) = 0-height (right(l, r)) = 1 + (height l) max (height r)+height (right(l, r)) = 1 + max(height l, height r)

@@ -0,0 +1,47 @@+-- | Normal: should be memoized.+!!! fib 100 == 354224848179261915075+fib : N -> N+fib 0 = 0+fib 1 = 1+fib x = fib (x .- 1) + fib (x .- 2)++-- | Multiple arrows: should be memoized.+!!! fibA 100 0 == 354224848179261915075+fibA : N -> N -> N+fibA 0 _ = 0+fibA 1 _ = 1+fibA x n = fibA (x .- 1) n + fibA (x .- 2) n++-- | Container types: can be memoized but may cause+--   performance issues depending on size of container.+!!! fibList 100 [1..100] == 354224848179261915075+fibList : N -> List(N) -> N+fibList 0 _ = 0+fibList 1 _ = 1+fibList x l = fibList (x .- 1) l + fibList (x .- 2) l++!!! fibSet 100 {1..100} == 354224848179261915075+fibSet : N -> Set(N) -> N+fibSet 0 _ = 0+fibSet 1 _ = 1+fibSet x s = fibSet (x .- 1) s + fibSet (x .- 2) s++!!! fibBag 100 ⟅1..100⟆ == 354224848179261915075+fibBag : N -> Bag(N) -> N+fibBag 0 _ = 0+fibBag 1 _ = 1+fibBag x b = fibBag (x .- 1) b + fibBag (x .- 2) b++-- | Higher-order: should not be memoized.+fibH : N -> (N -> N) -> N+fibH 0 _ = 0+fibH 1 _ = 1+fibH x f = fibH (x .- 1) f + fibH (x .- 2) f++fibHH : N -> (N -> (N -> N) -> N) -> N+fibHH 0 _ = 0+fibHH 1 _ = 1+fibHH x f = fibHH (x .- 1) f + fibHH (x .- 2) f++id : a -> a+id x = x

@@ -1,12 +0,0 @@-iterateP : (a → a) → a → List(a)-iterateP f p = p :: iterateP f (f p)--fib2_helper : ℕ×ℕ → ℕ×ℕ-fib2_helper (a,b) = (b,a+b)--indexP : ℕ -> List(a) -> a-indexP 0 (p::_) = p-indexP (n+1) (_::l') = indexP n l'--fib2 : ℕ → ℕ-fib2 n = {? x when (indexP n (iterateP fib2_helper (0,1))) is (x,_) ?}

@@ -4,20 +4,51 @@ -- Implementation of RSA encryption algorithm. -- Reference: https://simple.wikipedia.org/wiki/RSA_(algorithm) --- To use, first call `getKeys` with two prime numbers, which returns--- two pairs. The first pair is the public key, the second is the--- private key. These keys, along with the `encrypt` and `decrypt`--- functions can be used to encrypt and decrypt lists of natural--- numbers. +-- To use with randomly generated prime numbers, call `randKeys`+-- with a number, representing how many digits the generated primes +-- will have, and a pseudorandom number generator, created +-- by calling `seed` with a natural number. ++-- To manually input prime numbers, call `getKeys` +-- with two prime numbers. ++-- Output: Both of the above functions output two pairs of two +-- natural numbers. The first pair is the public key, the +-- second is the private key. These keys, along with the `encrypt` +-- and `decrypt` functions can be used to encrypt and decrypt +-- lists of natural numbers.+ encrypt : N * N -> List(N) -> List(N) encrypt key xs = each (encrypt1 key, xs)  decrypt : N * N -> List(N) -> List(N) decrypt = encrypt ++randKeys : N -> Gen -> (N * N) * (N * N)+randKeys 0 g = randKeys 1 g+randKeys d g = +   let   p1 = genPrime (10^(d.-1),10^d) g,+         p2 = genPrime (10^(d.-1),10^d) (snd p1)+   in getKeys (fst p1) (fst p2) ++genPrime : (N * N) -> Gen -> (N * Gen)+genPrime r g = let p = random(r,g) in +   {? p                          if isPrime (fst p)+   ,  genPrime r (snd p)         otherwise+   ?}++fst : (a * b) -> a +fst (a,_) = a ++snd : (a * b) -> b +snd (_,b) = b ++ -- takes two primes, returns a pair of pairs containing the RSA public/private keys -- prime -> prime -> (public key, private key)+ getKeys : N -> N -> (N * N) * (N * N) getKeys p1 p2 =   let m = p1 * p2,

@@ -20,4 +20,4 @@ treeSize(t) = treeFold(0, \(x,l,r). 1 + l + r, t)  treeHeight : Tree -> N-treeHeight(t) = treeFold(0, \(x,l,r). 1 + l max r, t)+treeHeight(t) = treeFold(0, \(x,l,r). 1 + max(l,r), t)

@@ -0,0 +1,13 @@+using Primitives++||| Look up a sequence of integers using https://oeis.org+!!!  lookupSequence [] == left(unit)+!!!  lookupSequence [1,1,2,3] == right "https://oeis.org/A000045"+lookupSequence : List(N) -> Unit + List(Char)+lookupSequence = $lookupSequence++||| Extend a known sequence of integers with data from https://oeis.org+!!!  extendSequence [] == []+!!!  extendSequence [1,1,2,3,5] == [1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181, 6765, 10946, 17711, 28657, 46368, 75025, 121393, 196418, 317811, 514229, 832040, 1346269, 2178309, 3524578, 5702887, 9227465, 14930352, 24157817, 39088169, 63245986, 102334155]+extendSequence : List(N) -> List(N)+extendSequence = $extendSequence

@@ -15,7 +15,7 @@ -- language for Disco. module Disco.AST.Core (   -- * Core AST-  RationalDisplay (..),+  ShouldMemo (..),   Core (..),   Op (..),   opArity,@@ -27,47 +27,29 @@ import Control.Lens.Plated import Data.Data (Data) import Data.Data.Lens (uniplate)-import qualified Data.Set as S-import GHC.Generics-import Unbound.Generics.LocallyNameless hiding (LFresh, lunbind)-import Prelude hiding ((<>))-import qualified Prelude as P--import Disco.Effects.LFresh-import Polysemy (Members, Sem)-import Polysemy.Reader- import Data.Ratio+import qualified Data.Set as S import Disco.AST.Generic (Side, selectSide)+import Disco.Effects.LFresh import Disco.Names (QName) import Disco.Pretty+import Disco.Syntax.Operators (BOp (..)) import Disco.Types---- | A type of flags specifying whether to display a rational number---   as a fraction or a decimal.-data RationalDisplay = Fraction | Decimal-  deriving (Eq, Show, Generic, Data, Ord, Alpha)--instance Semigroup RationalDisplay where-  Decimal <> _ = Decimal-  _ <> Decimal = Decimal-  _ <> _ = Fraction+import GHC.Generics+import Polysemy (Members, Sem)+import Polysemy.Reader+import Unbound.Generics.LocallyNameless hiding (LFresh, lunbind)+import Prelude hiding ((<>))+import qualified Prelude as P --- | The 'Monoid' instance for 'RationalDisplay' corresponds to the---   idea that the result should be displayed as a decimal if any---   decimal literals are used in the input; otherwise, the default is---   to display as a fraction.  So the identity element is 'Fraction',---   and 'Decimal' always wins when combining.-instance Monoid RationalDisplay where-  mempty = Fraction-  mappend = (P.<>)+data ShouldMemo = Memo | NoMemo deriving (Show, Generic, Data, Alpha)  -- | AST for the desugared, untyped core language. data Core where   -- | A variable.   CVar :: QName Core -> Core   -- | A rational number.-  CNum :: RationalDisplay -> Rational -> Core+  CNum :: Rational -> Core   -- | A built-in constant.   CConst :: Op -> Core   -- | An injection into a sum type, i.e. a value together with a tag@@ -87,7 +69,7 @@   -- | A projection from a product type, i.e. @fst@ or @snd@.   CProj :: Side -> Core -> Core   -- | An anonymous function.-  CAbs :: Bind [Name Core] Core -> Core+  CAbs :: ShouldMemo -> Bind [Name Core] Core -> Core   -- | Function application.   CApp :: Core -> Core -> Core   -- | A "test frame" under which a test case is run. Records the@@ -228,10 +210,8 @@     OHolds   | -- | Flip success and failure for a prop.     ONotProp-  | -- | Equality assertion, @=!=@-    OShouldEq Type-  | -- Other primitives-    OShouldLt Type+  | -- | Comparison assertion+    OShould BOp Type   | -- | Error for non-exhaustive pattern match     OMatchErr   | -- | Crash with a user-supplied message@@ -251,6 +231,8 @@   | -- | Not the Boolean `Impl`, but instead a propositional BOp     -- | Should only be seen and used with Props.     OImpl+  | OSeed+  | ORandom   deriving (Show, Generic, Data, Alpha, Eq, Ord)  -- | Get the arity (desired number of arguments) of a function@@ -278,7 +260,7 @@ instance Pretty Core where   pretty = \case     CVar qn -> pretty qn-    CNum _ r+    CNum r       | denominator r == 1 -> text (show (numerator r))       | otherwise -> text (show (numerator r)) <> "/" <> text (show (denominator r))     CApp (CConst op) (CPair c1 c2)@@ -303,7 +285,7 @@     CUnit -> "unit"     CPair c1 c2 -> setPA initPA $ parens (pretty c1 <> ", " <> pretty c2)     CProj s c -> withPA funPA $ selectSide s "fst" "snd" <+> rt (pretty c)-    CAbs lam -> withPA initPA $ do+    CAbs _ lam -> withPA initPA $ do       lunbind lam $ \(xs, body) -> "λ" <> intercalate "," (map pretty xs) <> "." <+> lt (pretty body)     CApp c1 c2 -> withPA funPA $ lt (pretty c1) <+> rt (pretty c2)     CTest xs c -> "test" <+> prettyTestVars xs <+> pretty c@@ -322,8 +304,7 @@   prettyTestVar (s, ty, n) = parens (intercalate "," [text s, pretty ty, pretty n])  isInfix, isPrefix, isPostfix :: Op -> Bool-isInfix OShouldEq {} = True-isInfix OShouldLt {} = True+isInfix OShould {} = True isInfix op =   op     `S.member` S.fromList@@ -392,8 +373,14 @@   OFrac -> "frac"   OHolds -> "holds"   ONotProp -> "not"-  OShouldEq _ -> "=!="-  OShouldLt _ -> "!<"+  OShould Eq _ -> "=!="+  OShould Neq _ -> "=!!="+  OShould Lt _ -> "!<"+  OShould Gt _ -> "!>"+  OShould Leq _ -> "!<="+  OShould Geq _ -> "!>="+  OShould Divides _ -> "!|"+  OShould _ _ -> "<!>"   OMatchErr -> "matchErr"   OCrash -> "crash"   OId -> "id"@@ -404,3 +391,5 @@   OAnd -> "and"   OOr -> "or"   OImpl -> "implies"+  ORandom -> "random"+  OSeed -> "seed"

@@ -8,10 +8,6 @@ -- Orphan Alpha Void instance {-# OPTIONS_GHC -fno-warn-orphans #-} -------------------------------------------------------------------------------------------------------------------------------------------------------------- -- SPDX-License-Identifier: BSD-3-Clause  -- |

@@ -105,29 +105,31 @@   pattern PFrac,   pattern PNonlinear,   pattern Binding,++  -- ** Pretty printing+  prettyPatternP, ) where -import Prelude hiding ((<>))- import Control.Lens ((%~), _1, _2, _3) import Data.Char (toLower)+import Data.List.NonEmpty (NonEmpty)+import qualified Data.List.NonEmpty as NE import qualified Data.Map as M import Data.Set (Set) import qualified Data.Set as S import Data.Void--import Disco.Effects.LFresh-import Polysemy hiding (Embed, embed)-import Polysemy.Reader- import Disco.AST.Generic+import Disco.Effects.LFresh import Disco.Extensions import Disco.Pretty import Disco.Syntax.Operators import Disco.Syntax.Prims import Disco.Types+import Polysemy hiding (Embed, embed)+import Polysemy.Reader import Unbound.Generics.LocallyNameless hiding (LFresh (..), lunbind)+import Prelude hiding ((<>))  -- | The extension descriptor for Surface specific AST types. data UD@@ -188,7 +190,7 @@ -- | A group of definition clauses of the form @name pat1 .. patn = term@. The --   patterns bind variables in the term. For example, @f n (x,y) = --   n*x + y@.-data TermDefn = TermDefn (Name Term) [Bind [Pattern] Term]+data TermDefn = TermDefn (Name Term) (NonEmpty (Bind [Pattern] Term))  -- | A user-defined type (potentially recursive). --@@ -224,7 +226,7 @@     DType (TypeDecl x ty) -> pretty x <+> text ":" <+> pretty ty     DTyDef (TypeDefn x args body) ->       text "type" <+> text x <+> hsep (map text args) <+> text "=" <+> pretty body-    DDefn (TermDefn x bs) -> vcat $ map (pretty . (x,)) bs+    DDefn (TermDefn x bs) -> vcat $ map (pretty . (x,)) (NE.toList bs)  -- | Pretty-print a single clause in a definition. instance Pretty (Name a, Bind [Pattern] Term) where@@ -512,6 +514,7 @@   , PSub   , PNeg   , PFrac+  , PNonlinear   #-}  ------------------------------------------------------------@@ -543,7 +546,7 @@         Nothing -> error $ "pretty @Term: Prim " ++ show p ++ " is not in the primMap!"     TParens t -> pretty t     TUnit -> text "■"-    (TBool b) -> text (map toLower $ show b)+    (TBool b) -> text (take 1 $ show b)     TChar c -> text (show c)     TString cs -> doubleQuotes $ text cs     TAbs q bnd -> withPA initPA $@@ -633,7 +636,7 @@  prettyBranches :: Members '[Reader PA, LFresh] r => [Branch] -> Sem r (Doc ann) prettyBranches = \case-  [] -> error "Empty branches are disallowed."+  [] -> text ""   b : bs ->     pretty b       $+$ foldr (($+$) . (text "," <+>) . pretty) empty bs@@ -730,3 +733,4 @@     PFrac p1 p2 ->       withPA (getPA Div) $         lt (pretty p1) <+> text "/" <+> rt (pretty p2)+    PNonlinear p _ -> pretty p

@@ -1,7 +1,3 @@-------------------------------------------------------------------------------------------------------------------------------------------------------------- -- | -- Module      :  Disco.Compile -- Copyright   :  disco team and contributors@@ -162,16 +158,16 @@ compileDTerm (DTPrim ty x) = compilePrim ty x compileDTerm DTUnit = return CUnit compileDTerm (DTBool _ b) = return $ CInj (bool L R b) CUnit-compileDTerm (DTChar c) = return $ CNum Fraction (toInteger (fromEnum c) % 1)-compileDTerm (DTNat _ n) = return $ CNum Fraction (n % 1) -- compileNat ty n-compileDTerm (DTRat r) = return $ CNum Decimal r+compileDTerm (DTChar c) = return $ CNum (toInteger (fromEnum c) % 1)+compileDTerm (DTNat _ n) = return $ CNum (n % 1) -- compileNat ty n+compileDTerm (DTRat r) = return $ CNum r compileDTerm term@(DTAbs q _ _) = do   (xs, tys, body) <- unbindDeep term   cbody <- compileDTerm body   case q of-    Lam -> return $ abstract xs cbody-    Ex -> return $ quantify (OExists tys) (abstract xs cbody)-    All -> return $ quantify (OForall tys) (abstract xs cbody)+    Lam -> return $ abstract (canMemo tys) xs cbody+    Ex -> return $ quantify (OExists tys) (abstract NoMemo xs cbody)+    All -> return $ quantify (OForall tys) (abstract NoMemo xs cbody)  where   -- Gather nested abstractions with the same quantifier.   unbindDeep :: Member Fresh r => DTerm -> Sem r ([Name DTerm], [Type], DTerm)@@ -181,12 +177,47 @@     return (name : ns, ty : tys, body)   unbindDeep t = return ([], [], t) -  abstract :: [Name DTerm] -> Core -> Core-  abstract xs body = CAbs (bind (map coerce xs) body)+  abstract :: ShouldMemo -> [Name DTerm] -> Core -> Core+  abstract m xs body = CAbs m (bind (map coerce xs) body)    quantify :: Op -> Core -> Core   quantify op = CApp (CConst op) +  -- Given a function's arguments, determine if it is memoizable.+  -- A function is memoizable if its arguments can be converted into+  -- a simple value (Haskell Ord instance can be derived).+  canMemo :: [Type] -> ShouldMemo+  canMemo tys+    | all canMemoTy tys = Memo+    | otherwise = NoMemo++  canMemoTy :: Type -> Bool+  canMemoTy (TyAtom a) = canMemoAtom a+  -- Anti-higher order while allowing for curried functions.+  canMemoTy (TyCon CArr tys@(t : _)) = case t of+    TyCon CArr _ -> False+    _ -> all canMemoTy tys+  canMemoTy (TyCon c tys) = canMemoCon c && all canMemoTy tys++  canMemoCon :: Con -> Bool+  canMemoCon = \case+    CArr -> False+    CUser _ -> False+    CGraph -> False+    CMap -> False+    CContainer a -> canMemoAtom a+    _ -> True++  canMemoAtom :: Atom -> Bool+  canMemoAtom (AVar _) = False+  canMemoAtom (ABase b) = canMemoBase b++  canMemoBase :: BaseTy -> Bool+  canMemoBase = \case+    Gen -> False+    P -> False+    _ -> True+ -- Special case for Cons, which compiles to a constructor application -- rather than a function application. compileDTerm (DTApp _ (DTPrim _ (PrimBOp Cons)) (DTPair _ t1 t2)) =@@ -234,13 +265,13 @@ compilePrim _ (PrimBOp Cons) = do   hd <- fresh (string2Name "hd")   tl <- fresh (string2Name "tl")-  return $ CAbs $ bind [hd, tl] $ CInj R (CPair (CVar (localName hd)) (CVar (localName tl)))+  return $ CAbs NoMemo $ bind [hd, tl] $ CInj R (CPair (CVar (localName hd)) (CVar (localName tl))) compilePrim _ PrimLeft = do   a <- fresh (string2Name "a")-  return $ CAbs $ bind [a] $ CInj L (CVar (localName a))+  return $ CAbs NoMemo $ bind [a] $ CInj L (CVar (localName a)) compilePrim _ PrimRight = do   a <- fresh (string2Name "a")-  return $ CAbs $ bind [a] $ CInj R (CVar (localName a))+  return $ CAbs NoMemo $ bind [a] $ CInj R (CVar (localName a)) compilePrim (ty1 :*: ty2 :->: resTy) (PrimBOp bop) = return $ compileBOp ty1 ty2 resTy bop compilePrim ty p@(PrimBOp _) = compilePrimErr p ty compilePrim _ PrimSqrt = return $ CConst OSqrt@@ -288,6 +319,8 @@ compilePrim ty PrimConnect = compilePrimErr PrimConnect ty compilePrim _ PrimInsert = return $ CConst OInsert compilePrim _ PrimLookup = return $ CConst OLookup+compilePrim _ PrimRandom = return $ CConst ORandom+compilePrim _ PrimSeed = return $ CConst OSeed compilePrim (_ :*: TyList _ :->: _) PrimEach =   return $     CVar (Named Stdlib "list" .- string2Name "eachlist")@@ -328,10 +361,15 @@ compilePrim _ PrimHolds = return $ CConst OHolds compilePrim _ PrimLookupSeq = return $ CConst OLookupSeq compilePrim _ PrimExtendSeq = return $ CConst OExtendSeq+compilePrim ty PrimMin = desugaredPrimErr PrimMin ty+compilePrim ty PrimMax = desugaredPrimErr PrimMax ty  compilePrimErr :: Prim -> Type -> a compilePrimErr p ty = error $ "Impossible! compilePrim " ++ show p ++ " on bad type " ++ show ty +desugaredPrimErr :: Prim -> Type -> a+desugaredPrimErr p ty = error $ "Impossible! compilePrim " ++ show p ++ " at type " ++ show ty ++ ", should have been desugared away"+ ------------------------------------------------------------ -- Case expressions ------------------------------------------------------------@@ -340,13 +378,13 @@ --   of type (Unit → τ), in order to delay evaluation until explicitly --   applying it to the unit value. compileCase :: Member Fresh r => [DBranch] -> Sem r Core-compileCase [] = return $ CAbs (bind [string2Name "_"] (CConst OMatchErr))+compileCase [] = return $ CAbs NoMemo (bind [string2Name "_"] (CConst OMatchErr)) -- empty case ==>  λ _ . error  compileCase (b : bs) = do   c1 <- compileBranch b   c2 <- compileCase bs-  return $ CAbs (bind [string2Name "_"] (CApp c1 c2))+  return $ CAbs NoMemo (bind [string2Name "_"] (CApp c1 c2))  -- | Compile a branch of a case expression of type τ to a core --   language expression of type (Unit → τ) → τ.  The idea is that it@@ -360,7 +398,7 @@   c <- compileDTerm e   k <- fresh (string2Name "k") -- Fresh name for the failure continuation   bc <- compileGuards (fromTelescope gs) k c-  return $ CAbs (bind [k] bc)+  return $ CAbs NoMemo (bind [k] bc)  -- | 'compileGuards' takes a list of guards, the name of the failure --   continuation of type (Unit → τ), and a Core term of type τ to@@ -382,13 +420,13 @@ --   calls the failure continuation in the case of failure, or the --   rest of the guards in the case of success. compileMatch :: Member Fresh r => DPattern -> Core -> Name Core -> Core -> Sem r Core-compileMatch (DPVar _ x) s _ e = return $ CApp (CAbs (bind [coerce x] e)) s+compileMatch (DPVar _ x) s _ e = return $ CApp (CAbs NoMemo (bind [coerce x] e)) s -- Note in the below two cases that we can't just discard s since -- that would result in a lazy semantics.  With an eager/strict -- semantics, we have to make sure s gets evaluated even if its -- value is then discarded.-compileMatch (DPWild _) s _ e = return $ CApp (CAbs (bind [string2Name "_"] e)) s-compileMatch DPUnit s _ e = return $ CApp (CAbs (bind [string2Name "_"] e)) s+compileMatch (DPWild _) s _ e = return $ CApp (CAbs NoMemo (bind [string2Name "_"] e)) s+compileMatch DPUnit s _ e = return $ CApp (CAbs NoMemo (bind [string2Name "_"] e)) s compileMatch (DPPair _ x1 x2) s _ e = do   y <- fresh (string2Name "y") @@ -396,11 +434,12 @@   return $     CApp       ( CAbs+          NoMemo           ( bind               [y]               ( CApp                   ( CApp-                      (CAbs (bind [coerce x1, coerce x2] e))+                      (CAbs NoMemo (bind [coerce x1, coerce x2] e))                       (CProj L (CVar (localName y)))                   )                   (CProj R (CVar (localName y)))@@ -506,11 +545,10 @@       , Impl ==> OImpl       ] --- ShouldEq needs to know the type at which the comparison is+-- Should needs to know the type at which the comparison is -- occurring, so values can be correctly pretty-printed if the test -- fails.-compileBOp ty _ _ ShouldEq = CConst (OShouldEq ty)-compileBOp ty _ _ ShouldLt = CConst (OShouldLt ty)+compileBOp ty _ _ (Should op) = CConst (OShould op ty) compileBOp _ty (TyList _) _ Elem = CConst OListElem compileBOp _ty _ _ Elem = CConst OBagElem compileBOp ty1 ty2 resTy op =

@@ -1,9 +1,5 @@ {-# LANGUAGE DeriveTraversable #-} -------------------------------------------------------------------------------------------------------------------------------------------------------------- -- SPDX-License-Identifier: BSD-3-Clause  -- |

@@ -1,6 +1,7 @@------------------------------------------------------------------------------+{-# OPTIONS_GHC -fno-warn-unrecognised-pragmas #-}+{-# OPTIONS_GHC -fno-warn-x-data-list-nonempty-unzip #-} ------------------------------------------------------------------------------+{-# HLINT ignore "Functor law" #-}  -- | -- Module      :  Disco.Desugar@@ -26,22 +27,22 @@ ) where -import Control.Monad.Cont+import Control.Monad (zipWithM) import Data.Bool (bool) import Data.Coerce+import Data.List.NonEmpty (NonEmpty (..))+import qualified Data.List.NonEmpty as NE import Data.Maybe (fromMaybe, isJust)- import Disco.AST.Desugared import Disco.AST.Surface import Disco.AST.Typed+import Disco.Effects.Fresh import Disco.Module import Disco.Names import Disco.Syntax.Operators import Disco.Syntax.Prims import Disco.Typecheck (containerTy) import Disco.Types--import Disco.Effects.Fresh import Polysemy (Member, Sem, run) import Unbound.Generics.LocallyNameless (   Bind,@@ -191,28 +192,29 @@ --   with their corresponding patterns. Definitions are abstractions --   (which happen to be named), and source-level lambdas are also --   abstractions (which happen to have only one clause).-desugarAbs :: Member Fresh r => Quantifier -> Type -> [Clause] -> Sem r DTerm+desugarAbs :: Member Fresh r => Quantifier -> Type -> NonEmpty Clause -> Sem r DTerm -- Special case for compiling a single lambda with no pattern matching directly to a lambda-desugarAbs Lam ty [cl@(unsafeUnbind -> ([APVar _ _], _))] = do+desugarAbs Lam ty (cl@(unsafeUnbind -> ([APVar _ _], _)) :| []) = do   (ps, at) <- unbind cl-  d <- desugarTerm at-  return $ DTAbs Lam ty (bind (getVar (head ps)) d)- where-  getVar (APVar _ x) = coerce x+  case ps of+    [APVar _ x] -> do+      d <- desugarTerm at+      return $ DTAbs Lam ty (bind (coerce x) d)+    _ -> error "desugarAbs: impossible: ps must be a singleton APVar" -- General case desugarAbs quant overallTy body = do   clausePairs <- unbindClauses body-  let (pats, bodies) = unzip clausePairs-  let patTys = map getType (head pats)-  let bodyTy = getType (head bodies)+  let (pats, bodies) = NE.unzip clausePairs+  let patTys = map getType (NE.head pats)+  let bodyTy = getType (NE.head bodies)    -- generate dummy variables for lambdas-  args <- zipWithM (\_ i -> fresh (string2Name ("arg" ++ show i))) (head pats) [0 :: Int ..]+  args <- zipWithM (\_ i -> fresh (string2Name ("arg" ++ show i))) (NE.head pats) [0 :: Int ..]    -- Create lambdas and one big case.  Recursively desugar the case to   -- deal with arithmetic patterns.-  let branches = zipWith (mkBranch (zip args patTys)) bodies pats-  dcase <- desugarTerm $ ATCase bodyTy branches+  let branches = NE.zipWith (mkBranch (zip args patTys)) bodies pats+  dcase <- desugarTerm $ ATCase bodyTy (NE.toList branches)   return $ mkAbs quant overallTy patTys (coerce args) dcase  where   mkBranch :: [(Name ATerm, Type)] -> ATerm -> [APattern] -> ABranch@@ -225,10 +227,10 @@   -- with the same quantifier when there's only a single clause. That   -- way, we generate a chain of abstractions followed by a case, instead   -- of a bunch of alternating abstractions and cases.-  unbindClauses :: Member Fresh r => [Clause] -> Sem r [([APattern], ATerm)]-  unbindClauses [c] | quant `elem` [All, Ex] = do+  unbindClauses :: Member Fresh r => NonEmpty Clause -> Sem r (NonEmpty ([APattern], ATerm))+  unbindClauses (c :| []) | quant `elem` [All, Ex] = do     (ps, t) <- liftClause c-    return [(ps, addDbgInfo ps t)]+    return ((ps, addDbgInfo ps t) :| [])   unbindClauses cs = mapM unbind cs    liftClause :: Member Fresh r => Bind [APattern] ATerm -> Sem r ([APattern], ATerm)@@ -242,7 +244,7 @@   -- Wrap a term in a test frame to report the values of all variables   -- bound in the patterns.   addDbgInfo :: [APattern] -> ATerm -> ATerm-  addDbgInfo ps t = ATTest (map withName $ concatMap varsBound ps) t+  addDbgInfo ps = ATTest (map withName $ concatMap varsBound ps)    where     withName (n, ty) = (name2String n, ty, n) @@ -265,6 +267,26 @@         )   return $ mkLambda ty [c] body +-- | Desugar the @min@ and @max@ functions into conditional expressions.+desugarMinMax :: Member Fresh r => Prim -> Type -> Sem r DTerm+desugarMinMax m ty = do+  p <- fresh (string2Name "p")+  a <- fresh (string2Name "a")+  b <- fresh (string2Name "b")+  body <-+    desugarTerm $+      ATCase+        ty+        [ bind+            (toTelescope [AGPat (embed (atVar ty p)) (APTup (ty :*: ty) [APVar ty a, APVar ty b])])+            $ ATCase+              ty+              [ atVar ty (if m == PrimMin then a else b) <==. [tif (atVar ty a <. atVar ty b)]+              , atVar ty (if m == PrimMin then b else a) <==. []+              ]+        ]+  return $ mkLambda ((ty :*: ty) :->: ty) [p] body+ -- | Desugar a typechecked term. desugarTerm :: Member Fresh r => ATerm -> Sem r DTerm desugarTerm (ATVar ty x) = return $ DTVar ty (coerce x)@@ -274,13 +296,15 @@   | bopDesugars ty1 ty2 resTy bop = desugarPrimBOp ty1 ty2 resTy bop desugarTerm (ATPrim ty@(TyList cts :->: TyBag b) PrimC2B) = desugarCList2B PrimC2B ty cts b desugarTerm (ATPrim ty@(TyList cts :->: TyBag b) PrimUC2B) = desugarCList2B PrimUC2B ty cts b+desugarTerm (ATPrim (_ :->: ty) PrimMin) = desugarMinMax PrimMin ty+desugarTerm (ATPrim (_ :->: ty) PrimMax) = desugarMinMax PrimMax ty desugarTerm (ATPrim ty x) = return $ DTPrim ty x desugarTerm ATUnit = return DTUnit desugarTerm (ATBool ty b) = return $ DTBool ty b desugarTerm (ATChar c) = return $ DTChar c desugarTerm (ATString cs) =   desugarContainer (TyList TyC) ListContainer (map (\c -> (ATChar c, Nothing)) cs) Nothing-desugarTerm (ATAbs q ty lam) = desugarAbs q ty [lam]+desugarTerm (ATAbs q ty lam) = desugarAbs q ty (NE.singleton lam) -- Special cases for fully applied operators desugarTerm (ATApp resTy (ATPrim _ (PrimUOp uop)) t)   | uopDesugars (getType t) resTy uop = desugarUnApp resTy uop t@@ -306,7 +330,7 @@ -- | Desugar a property by wrapping its corresponding term in a test --   frame to catch its exceptions & convert booleans to props. desugarProperty :: Member Fresh r => AProperty -> Sem r DTerm-desugarProperty p = DTTest [] <$> desugarTerm p+desugarProperty p = DTTest [] <$> desugarTerm (setType TyProp p)  ------------------------------------------------------------ -- Desugaring operators@@ -331,10 +355,8 @@ bopDesugars _ TyN _ Choose = True -- bopDesugars _   _   (TyFin _) bop | bop `elem` [Add, Mul] = True --- And, Or, Impl for Props don't desugar because they are primitive--- Prop constructors.  On the other hand, logical operations on Bool--- can desugar in terms of more primitive conditional expressions.-bopDesugars _ _ TyProp bop | bop `elem` [And, Or, Impl] = False+-- Eq and Lt at type Prop desugar into ShouldEq, ShouldLt .+bopDesugars _ _ TyProp bop | bop `elem` [Eq, Neq, Lt, Gt, Leq, Geq, Divides] = True bopDesugars _ _ _ bop =   bop     `elem` [ And@@ -345,8 +367,6 @@            , Gt            , Leq            , Geq-           , Min-           , Max            , IDiv            , Sub            , SSub@@ -400,6 +420,14 @@ -- modules/a standard library, including (2) the ability to define -- infix operators. +-- And, Or, Impl at type Prop are primitive Prop constructors so don't+-- desugar; but we push the Prop type down so we properly desugar+-- their arguments.+desugarBinApp TyProp b t1 t2 | b `elem` [And, Or, Impl] = do+  d1 <- desugarTerm $ setType TyProp t1+  d2 <- desugarTerm $ setType TyProp t2+  pure $ dtbin TyProp (PrimBOp b) d1 d2+ -- t1 and t2 ==> {? t2 if t1, false otherwise ?} desugarBinApp _ And t1 t2 =   desugarTerm $@@ -420,25 +448,12 @@       [ tru <==. [tif t1]       , t2 <==. []       ]+desugarBinApp TyProp op t1 t2+  | op `elem` [Eq, Neq, Lt, Gt, Leq, Geq, Divides] = desugarTerm $ mkBin TyProp (Should op) t1 t2 desugarBinApp _ Neq t1 t2 = desugarTerm $ tnot (t1 ==. t2) desugarBinApp _ Gt t1 t2 = desugarTerm $ t2 <. t1 desugarBinApp _ Leq t1 t2 = desugarTerm $ tnot (t2 <. t1) desugarBinApp _ Geq t1 t2 = desugarTerm $ tnot (t1 <. t2)--- XXX sharing!-desugarBinApp ty Min t1 t2 =-  desugarTerm $-    ATCase-      ty-      [ t1 <==. [tif (t1 <. t2)]-      , t2 <==. []-      ]-desugarBinApp ty Max t1 t2 =-  desugarTerm $-    ATCase-      ty-      [ t1 <==. [tif (t2 <. t1)]-      , t2 <==. []-      ] -- t1 // t2 ==> floor (t1 / t2) desugarBinApp resTy IDiv t1 t2 =   desugarTerm $@@ -498,9 +513,9 @@           , t2           ]  where-  mergeOp _ Inter = PrimBOp Min+  mergeOp _ Inter = PrimMin   mergeOp _ Diff = PrimBOp SSub-  mergeOp (TySet _) Union = PrimBOp Max+  mergeOp (TySet _) Union = PrimMax   mergeOp (TyBag _) Union = PrimBOp Add   mergeOp _ _ = error $ "Impossible! mergeOp " ++ show ty ++ " " ++ show op @@ -514,7 +529,7 @@       (ATPrim (ty :*: ty :->: TyBool) (PrimBOp Eq))       [ tapps           (ATPrim ((TyN :*: TyN :->: TyN) :*: ty :*: ty :->: ty) PrimMerge)-          [ ATPrim (TyN :*: TyN :->: TyN) (PrimBOp Max)+          [ ATPrim (TyN :*: TyN :->: TyN) PrimMax           , t1           , t2           ]

@@ -1,7 +1,3 @@-------------------------------------------------------------------------------------------------------------------------------------------------------------- -- SPDX-License-Identifier: BSD-3-Clause  -- |@@ -11,10 +7,12 @@ -- -- Built-in documentation. module Disco.Doc (-  primDoc,-  primReference,-  otherDoc,-  otherReference,+  DocKey (..),+  RefType (..),+  Reference (..),+  mkRef,+  mkIntro,+  docMap, ) where  import Data.Map (Map)@@ -24,134 +22,188 @@ import Disco.Syntax.Prims import Disco.Util ((==>)) --- | A map from some primitives to a short descriptive string,---   to be shown by the :doc command.-primDoc :: Map Prim String-primDoc =-  M.fromList-    [ PrimUOp Neg ==> "Arithmetic negation."-    , PrimBOp Add ==> "The sum of two numbers, types, or graphs."-    , PrimBOp Sub ==> "The difference of two numbers."-    , PrimBOp SSub ==> "The difference of two numbers, with a lower bound of 0."-    , PrimBOp Mul ==> "The product of two numbers, types, or graphs."-    , PrimBOp Div ==> "Divide two numbers."-    , PrimBOp IDiv ==> "The integer quotient of two numbers, rounded down."-    , PrimBOp Mod ==> "a mod b is the remainder when a is divided by b."-    , PrimBOp Exp ==> "Exponentiation.  a ^ b is a raised to the b power."-    , PrimUOp Fact ==> "n! computes the factorial of n, that is, 1 * 2 * ... * n."-    , PrimFloor ==> "floor(x) is the largest integer which is <= x."-    , PrimCeil ==> "ceiling(x) is the smallest integer which is >= x."-    , PrimAbs ==> "abs(x) is the absolute value of x.  Also written |x|."-    , PrimUOp Not ==> "Logical negation: not(true) = false and not(false) = true."-    , PrimBOp And ==> "Logical conjunction (and): true /\\ true = true; otherwise x /\\ y = false."-    , PrimBOp Or ==> "Logical disjunction (or): false \\/ false = false; otherwise x \\/ y = true."-    , PrimBOp Impl ==> "Logical implication (implies): true -> false = false; otherwise x -> y = true."-    , PrimBOp Iff ==> "Biconditional (if and only if)."-    , PrimBOp Eq ==> "Equality test.  x == y is true if x and y are equal."-    , PrimBOp Neq ==> "Inequality test.  x /= y is true if x and y are unequal."-    , PrimBOp Lt ==> "Less-than test. x < y is true if x is less than (but not equal to) y."-    , PrimBOp Gt ==> "Greater-than test. x > y is true if x is greater than (but not equal to) y."-    , PrimBOp Leq ==> "Less-than-or-equal test. x <= y is true if x is less than or equal to y."-    , 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)."-    ]+-- | Lookup keys for documentation.+data DocKey where+  PrimKey :: Prim -> DocKey+  OtherKey :: String -> DocKey+  deriving (Eq, Ord, Show) --- | A map from some primitives to their corresponding page in the---   Disco language reference---   (https://disco-lang.readthedocs.io/en/latest/reference/index.html).-primReference :: Map Prim String-primReference =-  M.fromList-    [ PrimBOp Add ==> "addition"-    , PrimBOp Sub ==> "subtraction"-    , PrimBOp SSub ==> "subtraction"-    , PrimBOp Mul ==> "multiplication"-    , PrimBOp Div ==> "division"-    , PrimBOp IDiv ==> "integerdiv"-    , PrimBOp Mod ==> "mod"-    , PrimBOp Exp ==> "exponentiation"-    , PrimUOp Fact ==> "factorial"-    , PrimFloor ==> "round"-    , PrimCeil ==> "round"-    , PrimAbs ==> "abs"-    , PrimUOp Not ==> "logic-ops"-    , PrimBOp And ==> "logic-ops"-    , PrimBOp Or ==> "logic-ops"-    , 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"-    , PrimBOp Eq ==> "compare"-    , PrimBOp Neq ==> "compare"-    , PrimBOp Lt ==> "compare"-    , PrimBOp Gt ==> "compare"-    , PrimBOp Leq ==> "compare"-    , PrimBOp Geq ==> "compare"-    ]+-- | An enumeration of different types of documentation references.+data RefType where+  -- | A reference to the Gentle Introduction (https://disco-lang.readthedocs.io/en/latest/introduction/index.html)+  Intro :: RefType+  -- | A reference to the Language Reference (https://disco-lang.readthedocs.io/en/latest/reference/index.html)+  Ref :: RefType+  -- | An arbitrary free-form URL+  URL :: RefType+  deriving (Eq, Ord, Show, Read, Bounded, Enum) -otherDoc :: Map String String-otherDoc =+-- | A reference for further reading.+data Reference = Reference {refType :: RefType, ref :: String}+  deriving (Eq, Ord, Show)++mkRef :: String -> Reference+mkRef = Reference Ref++mkIntro :: String -> Reference+mkIntro = Reference Intro++-- | A map storing documentation for various things that can be looked+--   up with :doc.  Each key is mapped to a short descriptive string,+--   plus references for further reading.+docMap :: Map DocKey (String, [Reference])+docMap =   M.fromList-    [ "N" ==> docN-    , "ℕ" ==> docN-    , "Nat" ==> docN-    , "Natural" ==> docN-    , "Z" ==> docZ-    , "ℤ" ==> docZ-    , "Int" ==> docZ-    , "Integer" ==> docZ-    , "F" ==> docF-    , "𝔽" ==> docF-    , "Frac" ==> docF-    , "Fractional" ==> docF-    , "Q" ==> docQ-    , "ℚ" ==> docQ-    , "Rational" ==> docQ-    , "Bool" ==> docB-    , "Boolean" ==> docB-    , "Unit" ==> "The unit type, i.e. a type with only a single value."-    , "Prop" ==> "The type of propositions."-    , "Set" ==> "The type of finite sets."-    , "|~|" ==> "Absolute value, or the size of a collection."-    , "{?" ==> "{? ... ?} is a case expression, for choosing a result based on conditions."+    [ PrimKey (PrimUOp Neg)+        ==> "Arithmetic negation."+        ==> []+    , PrimKey (PrimBOp Add)+        ==> "The sum of two numbers, types, or graphs."+        ==> [mkIntro "arithmetic", mkRef "addition"]+    , PrimKey (PrimBOp Sub)+        ==> "The difference of two numbers."+        ==> [mkIntro "arithmetic", mkRef "subtraction"]+    , PrimKey (PrimBOp SSub)+        ==> "The difference of two numbers, with a lower bound of 0."+        ==> [mkIntro "arithmetic", mkRef "subtraction", mkRef "symbols"]+    , PrimKey (PrimBOp Mul)+        ==> "The product of two numbers, types, or graphs."+        ==> [mkIntro "arithmetic", mkRef "multiplication"]+    , PrimKey (PrimBOp Div)+        ==> "Divide two numbers."+        ==> [mkIntro "arithmetic", mkRef "division"]+    , PrimKey (PrimBOp IDiv)+        ==> "The integer quotient of two numbers, rounded down."+        ==> [mkIntro "arithmetic", mkRef "integerdiv"]+    , PrimKey (PrimBOp Mod)+        ==> "a mod b is the remainder when a is divided by b."+        ==> [mkRef "mod"]+    , PrimKey (PrimBOp Exp)+        ==> "Exponentiation.  a ^ b is a raised to the b power."+        ==> [mkIntro "arithmetic", mkRef "exponentiation"]+    , PrimKey (PrimUOp Fact)+        ==> "n! computes the factorial of n, that is, 1 * 2 * ... * n."+        ==> [mkRef "factorial"]+    , PrimKey PrimFloor+        ==> "floor(x) is the largest integer which is <= x."+        ==> [mkIntro "arithmetic", mkRef "round", mkRef "symbols"]+    , PrimKey PrimCeil+        ==> "ceiling(x) is the smallest integer which is >= x."+        ==> [mkIntro "arithmetic", mkRef "round", mkRef "symbols"]+    , PrimKey PrimAbs+        ==> "abs(x) is the absolute value of x."+        ==> [mkIntro "arithmetic", mkRef "abs"]+    , PrimKey PrimMin+        ==> "min(x,y) is the minimum of x and y, i.e. whichever is smaller."+        ==> [mkRef "compare"]+    , PrimKey PrimMax+        ==> "max(x,y) is the maximum of x and y, i.e. whichever is larger."+        ==> [mkRef "compare"]+    , PrimKey (PrimUOp Not)+        ==> "Logical negation: not(T) = F and not(F) = T."+        ==> [mkRef "logic-ops", mkRef "symbols"]+    , PrimKey (PrimBOp And)+        ==> "Logical conjunction (and): T /\\ T = T; otherwise x /\\ y = F."+        ==> [mkRef "logic-ops", mkRef "symbols"]+    , PrimKey (PrimBOp Or)+        ==> "Logical disjunction (or): F \\/ F = F; otherwise x \\/ y = T."+        ==> [mkRef "logic-ops", mkRef "symbols"]+    , PrimKey (PrimBOp Impl)+        ==> "Logical implication (implies): T -> F = F; otherwise x -> y = T."+        ==> [mkRef "logic-ops", mkRef "symbols"]+    , PrimKey (PrimBOp Iff)+        ==> "Biconditional (if and only if)."+        ==> [mkRef "logic-ops", mkRef "symbols"]+    , PrimKey (PrimBOp Eq)+        ==> "Equality test.  x == y is T if x and y are equal."+        ==> [mkRef "compare"]+    , PrimKey (PrimBOp Neq)+        ==> "Inequality test.  x /= y is T if x and y are unequal."+        ==> [mkRef "compare", mkRef "symbols"]+    , PrimKey (PrimBOp Lt)+        ==> "Less-than test. x < y is T if x is less than (but not equal to) y."+        ==> [mkRef "compare"]+    , PrimKey (PrimBOp Gt)+        ==> "Greater-than test. x > y is T if x is greater than (but not equal to) y."+        ==> [mkRef "compare"]+    , PrimKey (PrimBOp Leq)+        ==> "Less-than-or-equal test. x <= y is T if x is less than or equal to y."+        ==> [mkRef "compare", mkRef "symbols"]+    , PrimKey (PrimBOp Geq)+        ==> "Greater-than-or-equal test. x >= y is T if x is greater than or equal to y."+        ==> [mkRef "compare", mkRef "symbols"]+    , PrimKey (PrimBOp CartProd)+        ==> "Cartesian product, i.e. the collection of all pairs.  Also works on bags and sets."+        ==> [mkRef "cp", mkRef "symbols"]+    , PrimKey PrimPower+        ==> "Power set, i.e. the set of all subsets.  Also works on bags."+        ==> [mkRef "power"]+    , PrimKey (PrimBOp Union)+        ==> "Union of two sets (or bags)."+        ==> [mkRef "set-ops", mkRef "symbols"]+    , PrimKey (PrimBOp Inter)+        ==> "Intersection of two sets (or bags)."+        ==> [mkRef "set-ops", mkRef "symbols"]+    , PrimKey (PrimBOp Diff)+        ==> "Difference of two sets (or bags)."+        ==> [mkRef "set-ops"]+    , OtherKey "N" ==> docN+    , OtherKey "ℕ" ==> docN+    , OtherKey "Nat" ==> docN+    , OtherKey "Natural" ==> docN+    , OtherKey "Z" ==> docZ+    , OtherKey "ℤ" ==> docZ+    , OtherKey "Int" ==> docZ+    , OtherKey "Integer" ==> docZ+    , OtherKey "F" ==> docF+    , OtherKey "𝔽" ==> docF+    , OtherKey "Frac" ==> docF+    , OtherKey "Fractional" ==> docF+    , OtherKey "Q" ==> docQ+    , OtherKey "ℚ" ==> docQ+    , OtherKey "Rational" ==> docQ+    , OtherKey "Bool" ==> docB+    , OtherKey "Boolean" ==> docB+    , OtherKey "Unit"+        ==> "The unit type, i.e. a type with only a single value."+        ==> [mkRef "unit", mkRef "symbols"]+    , OtherKey "Prop"+        ==> "The type of propositions."+        ==> [mkRef "prop"]+    , OtherKey "List"+        ==> "List(T) is the type of lists whose elements have type T."+        ==> [mkRef "list", mkRef "list-lib"]+    , OtherKey "Bag"+        ==> "Bag(T) is the type of bags (i.e. sets with multiplicity) whose elements have type T."+        ==> [mkRef "bag", mkRef "symbols"]+    , OtherKey "Set"+        ==> "Set(T) is the type of finite sets whose elements have type T."+        ==> [mkRef "set", mkRef "symbols"]+    , OtherKey "|~|"+        ==> "Absolute value, or the size of a collection."+        ==> [mkIntro "arithmetic", mkRef "size"]+    , OtherKey "{?"+        ==> "{? ... ?} is a case expression, for choosing a result based on conditions."+        ==> [mkRef "case"]+    , OtherKey "λ"+        ==> "λ (aka lambda, alternatively `\\`) introduces an anonymous function."+        ==> [mkRef "anonymous-func", mkRef "symbols"]+    , OtherKey "#"+        ==> "The # character is used to denote the cardinality of an element in a bag."+        ==> [mkRef "bag"]     ]  where-  docN = "The type of natural numbers: 0, 1, 2, ..."-  docZ = "The type of integers: ..., -2, -1, 0, 1, 2, ..."-  docF = "The type of fractional numbers p/q >= 0."-  docQ = "The type of rational numbers p/q."-  docB = "The type of Booleans (true or false)."+  docN = ("The type of natural numbers: 0, 1, 2, ...", refsN)+  refsN = [mkIntro "types", mkRef "natural", mkRef "symbols"] -otherReference :: Map String String-otherReference =-  M.fromList-    [ "N" ==> "natural"-    , "ℕ" ==> "natural"-    , "Nat" ==> "natural"-    , "Natural" ==> "natural"-    , "Z" ==> "integer"-    , "ℤ" ==> "integer"-    , "Int" ==> "integer"-    , "Integer" ==> "integer"-    , "F" ==> "fraction"-    , "𝔽" ==> "fraction"-    , "Frac" ==> "fraction"-    , "Fractional" ==> "fraction"-    , "Q" ==> "rational"-    , "ℚ" ==> "rational"-    , "Rational" ==> "rational"-    , "Bool" ==> "bool"-    , "Boolean" ==> "bool"-    , "Unit" ==> "unit"-    , "Prop" ==> "prop"-    , "Set" ==> "set"-    , "|~|" ==> "size"-    , "{?" ==> "case"-    ]+  docZ = ("The type of integers: ..., -2, -1, 0, 1, 2, ...", refsZ)+  refsZ = [mkIntro "types", mkRef "integer", mkRef "symbols"]++  docF = ("The type of fractional numbers p/q >= 0.", refsF)+  refsF = [mkIntro "types", mkRef "fraction", mkRef "symbols"]++  docQ = ("The type of rational numbers p/q.", refsQ)+  refsQ = [mkIntro "types", mkRef "rational", mkRef "symbols"]++  docB = ("The type of Booleans (T or F).", refsB)+  refsB = [mkRef "bool"]

@@ -1,7 +1,3 @@-------------------------------------------------------------------------------------------------------------------------------------------------------------- -- | -- Module      :  Disco.Effects.Input -- Copyright   :  disco team and contributors@@ -13,6 +9,7 @@ module Disco.Effects.Input (   module Polysemy.Input,   inputToState,+  mapInput, ) where @@ -23,3 +20,8 @@ -- | Run an input effect in terms of an ambient state effect. inputToState :: forall s r a. Member (State s) r => Sem (Input s ': r) a -> Sem r a inputToState = interpret (\case Input -> get @s)++-- | Use a function to (contravariantly) transform the input value in+--   an input effect.+mapInput :: forall s t r a. Member (Input s) r => (s -> t) -> Sem (Input t ': r) a -> Sem r a+mapInput f = interpret (\case Input -> inputs @s f)

@@ -2,10 +2,6 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE TemplateHaskell #-} -------------------------------------------------------------------------------------------------------------------------------------------------------------- -- | -- Module      :  Disco.Effects.LFresh -- Copyright   :  disco team and contributors@@ -20,6 +16,7 @@ import Data.Set (Set) import qualified Data.Set as S import Data.Typeable (Typeable)+import Disco.Util (gate, iterUntil) import Polysemy import Polysemy.ConstraintAbsorber import Polysemy.Reader@@ -45,12 +42,8 @@     Lfresh nm -> do       let s = name2String nm       used <- ask-      pureT $-        head-          ( filter-              (\x -> not (S.member (AnyName x) used))-              (map (makeName s) [0 ..])-          )+      let ok n = S.notMember (AnyName n) used+      pureT $ iterUntil (+ 1) (gate ok . makeName s) 0     Avoid names m -> do       m' <- runT m       raise (subsume (runLFresh' (local (S.union (S.fromList names)) m')))

@@ -1,32 +0,0 @@----------------------------------------------------------------------------------------------------------------------------------------------------------------- |--- Module      :  Disco.Effects.Random--- Copyright   :  disco team and contributors--- Maintainer  :  byorgey@gmail.com------ SPDX-License-Identifier: BSD-3-Clause------ Utility functions for random effect.-module Disco.Effects.Random (-  module Polysemy.Random,-  runGen,-)-where--import Polysemy-import Polysemy.Random-import qualified System.Random.SplitMix as SM-import qualified Test.QuickCheck.Gen as QC-import qualified Test.QuickCheck.Random as QCR--import Data.Word (Word64)---- | Run a QuickCheck generator using a 'Random' effect.-runGen :: Member Random r => QC.Gen a -> Sem r a-runGen g = do-  n <- random @_ @Int-  w <- random @_ @Word64-  return $ QC.unGen g (QCR.QCGen (SM.mkSMGen w)) n

@@ -1,9 +1,5 @@ {-# LANGUAGE NondecreasingIndentation #-} -------------------------------------------------------------------------------------------------------------------------------------------------------------- -- | -- Module      :  Disco.Enumerate -- Copyright   :  disco team and contributors@@ -63,39 +59,30 @@   fromV (VInj i VUnit) = i   fromV _ = error "enumBool.fromV: value isn't a bool" --- | Unsafely extract the numeric value of a @Value@---   (assumed to be a VNum).-valToRat :: Value -> Rational-valToRat (VNum _ r) = r-valToRat _ = error "valToRat: value isn't a number"--ratToVal :: Rational -> Value-ratToVal = VNum mempty- -- | Enumerate all values of type @Nat@ (0, 1, 2, ...). enumN :: ValueEnumeration-enumN = E.mapE (ratToVal . fromInteger) (floor . valToRat) E.nat+enumN = E.mapE (ratv . fromInteger) (floor . vrat) E.nat  -- | Enumerate all values of type @Integer@ (0, 1, -1, 2, -2, ...). enumZ :: ValueEnumeration-enumZ = E.mapE (ratToVal . fromInteger) (floor . valToRat) E.int+enumZ = E.mapE (ratv . fromInteger) (floor . vrat) E.int  -- | Enumerate all values of type @Fractional@ in the Calkin-Wilf --   order (1, 1/2, 2, 1/3, 3/2, 2/3, 3, ...). enumF :: ValueEnumeration-enumF = E.mapE ratToVal valToRat E.cw+enumF = E.mapE ratv vrat E.cw  -- | Enumerate all values of type @Rational@ in the Calkin-Wilf order, --   with negatives interleaved (0, 1, -1, 1/2, -1/2, 2, -2, ...). enumQ :: ValueEnumeration-enumQ = E.mapE ratToVal valToRat E.rat+enumQ = E.mapE ratv vrat E.rat  -- | Enumerate all Unicode characters. enumC :: ValueEnumeration enumC = E.mapE toV fromV (E.boundedEnum @Char)  where-  toV = ratToVal . fromIntegral . fromEnum-  fromV = toEnum . floor . valToRat+  toV = ratv . fromIntegral . fromEnum+  fromV = toEnum . floor . vrat  -- | Enumerate all *finite* sets over a certain element type, given an --   enumeration of the elements.  If we think of each finite set as a

@@ -1,10 +1,6 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE StandaloneDeriving #-} -------------------------------------------------------------------------------------------------------------------------------------------------------------- -- | -- Module      :  Disco.Error -- Copyright   :  disco team and contributors@@ -93,10 +89,11 @@     CyclicImport ms -> cyclicImportError ms     TypeCheckErr (LocTCError Nothing te) -> prettyTCError te     TypeCheckErr (LocTCError (Just n) te) ->-      nest 2 $ vcat-        [ "While checking " <> pretty' n <> ":"-        , prettyTCError te-        ]+      nest 2 $+        vcat+          [ "While checking " <> pretty' n <> ":"+          , prettyTCError te+          ]     ParseErr pe -> text (errorBundlePretty pe)     EvalErr ee -> prettyEvalError ee     Panic s ->@@ -108,18 +105,22 @@ rtd :: String -> Sem r (Doc ann) rtd page = "https://disco-lang.readthedocs.io/en/latest/reference/" <> text page <> ".html" -issue :: Int -> Sem r (Doc ann)-issue n = "See https://github.com/disco-lang/disco/issues/" <> text (show n)+-- issue :: Int -> Sem r (Doc ann)+-- issue n = "See https://github.com/disco-lang/disco/issues/" <> text (show n) +squote :: String -> String+squote x = "'" ++ x ++ "'"+ cyclicImportError ::   Members '[Reader PA, LFresh] r =>   [ModuleName] ->   Sem r (Doc ann) cyclicImportError ms =-  nest 2 $ vcat-    [ "Error: module imports form a cycle:"-    , intercalate " ->" (map pretty ms)-    ]+  nest 2 $+    vcat+      [ "Error: module imports form a cycle:"+      , intercalate " ->" (map pretty ms)+      ]  prettyEvalError :: Members '[Reader PA, LFresh] r => EvalError -> Sem r (Doc ann) prettyEvalError = \case@@ -142,11 +143,11 @@ prettyTCError = \case   -- XXX include some potential misspellings along with Unbound   --   see https://github.com/disco-lang/disco/issues/180-  Unbound x ->-    vcat-      [ "Error: there is nothing named" <+> pretty' x <> "."-      , rtd "unbound"-      ]+  Unbound x suggestions ->+    vcat $+      ["Error: there is nothing named" <+> pretty' x <> "."]+        ++ ["Perhaps you meant" <+> intercalate " or" (map (text . squote) suggestions) <> "?" | not (null suggestions)]+        ++ [rtd "unbound"]   Ambiguous x ms ->     vcat       [ "Error: the name" <+> pretty' x <+> "is ambiguous. It could refer to:"@@ -249,13 +250,12 @@       [ "Error: too many arguments for the type '" <> pretty' con <> "'."       , rtd "num-args-type"       ]-  -- XXX Mention the definition in which it was found, suggest adding the variable-  --     as a parameter-  UnboundTyVar v ->-    vcat-      [ "Error: Unknown type variable '" <> pretty' v <> "'."-      , rtd "unbound-tyvar"-      ]+  -- XXX Mention the definition in which it was found+  UnboundTyVar v suggestions ->+    vcat $+      ["Error: Unknown type variable '" <> pretty' v <> "'."]+        ++ ["Perhaps you meant" <+> intercalate " or" (map (text . squote) suggestions) <> "?" | not (null suggestions)]+        ++ [rtd "unbound-tyvar"]   NoPolyRec s ss tys ->     vcat       [ "Error: in the definition of " <> text s <> parens (intercalate "," (map text ss)) <> ": recursive occurrences of" <+> text s <+> "may only have type variables as arguments."

@@ -78,11 +78,13 @@ import Polysemy.Random import Polysemy.Reader +import qualified Data.List.NonEmpty as NonEmpty import Disco.AST.Core import Disco.AST.Surface import Disco.Compile (compileDefns) import Disco.Context as Ctx import Disco.Error+import Disco.Exhaustiveness (checkClauses) import Disco.Extensions import Disco.Interpret.CESK import Disco.Messages@@ -100,7 +102,7 @@ -- Configuation options ------------------------------------------------------------ -data DiscoConfig = DiscoConfig+newtype DiscoConfig = DiscoConfig   { _debugMode :: Bool   } @@ -185,7 +187,7 @@  -- | Run a top-level computation. runDisco :: DiscoConfig -> (forall r. Members DiscoEffects r => Sem r ()) -> IO ()-runDisco cfg m =+runDisco cfg =   void     . H.runInputT inputSettings     . runFinal @(H.InputT IO)@@ -201,7 +203,6 @@     . mapError EvalErr -- Embed runtime errors into top-level error type     . failToError Panic -- Turn pattern-match failures into a Panic error     . runReader emptyCtx -- Keep track of current Env-    $ m  where   msgFilter     | cfg ^. debugMode = const True@@ -385,6 +386,10 @@   -- Typecheck (and resolve names in) the module.   m <- runTCM tyctx tydefns $ checkModule name importMap cm +  -- Check for partial functions+  let allTyDefs = M.unionWith const tydefns (m ^. miTydefs)+  runFresh $ mapM_ (checkExhaustive allTyDefs) (Ctx.elems $ m ^. miTermdefs)+   -- Evaluate all the module definitions and add them to the topEnv.   mapError EvalErr $ loadDefsFrom m @@ -444,3 +449,8 @@ loadDef x body = do   v <- inputToState @TopInfo . inputTopEnv $ eval body   modify @TopInfo $ topEnv %~ Ctx.insert x v++checkExhaustive :: Members '[Fresh, Output (Message ann), Embed IO] r => TyDefCtx -> Defn -> Sem r ()+checkExhaustive tyDefCtx (Defn name argsType _ boundClauses) = do+  clauses <- NonEmpty.map fst <$> mapM unbind boundClauses+  runReader @TyDefCtx tyDefCtx $ checkClauses name argsType clauses

@@ -0,0 +1,417 @@+{-# LANGUAGE PatternSynonyms #-}++-- |+-- Module      :  Disco.Exhaustiveness+-- Copyright   :  disco team and contributors+-- Maintainer  :  byorgey@gmail.com+--+-- SPDX-License-Identifier: BSD-3-Clause+--+-- Entry point into the exhaustiveness checker.+-- Converts information into a format the checker understands,+-- then pretty prints the results of running it.+module Disco.Exhaustiveness where++import Control.Monad (forM, unless, zipWithM)+import Control.Monad.Trans.Maybe (MaybeT, runMaybeT)+import Data.List (nub)+import Data.List.NonEmpty (NonEmpty)+import qualified Data.List.NonEmpty as NonEmpty+import Data.Maybe (catMaybes)+import Disco.AST.Generic (Side (..))+import Disco.AST.Surface (+  Pattern,+  prettyPatternP,+  pattern PBool,+  pattern PChar,+  pattern PInj,+  pattern PList,+  pattern PNat,+  pattern PNeg,+  pattern PString,+  pattern PTup,+  pattern PUnit,+  pattern PWild,+ )+import Disco.AST.Typed (+  APattern,+  ATerm,+  pattern APBool,+  pattern APChar,+  pattern APCons,+  pattern APInj,+  pattern APList,+  pattern APNat,+  pattern APNeg,+  pattern APString,+  pattern APTup,+  pattern APUnit,+  pattern APVar,+  pattern APWild,+ )+import Disco.Effects.Fresh (Fresh)+import Disco.Effects.LFresh (LFresh, runLFresh)+import qualified Disco.Exhaustiveness.Constraint as C+import qualified Disco.Exhaustiveness.Possibilities as Poss+import qualified Disco.Exhaustiveness.TypeInfo as TI+import Disco.Messages+import Disco.Pretty (Doc, initPA, withPA)+import qualified Disco.Pretty.DSL as DSL+import Disco.Pretty.Prec (PA, funPA)+import qualified Disco.Types as Ty+import Polysemy+import Polysemy.Output+import Polysemy.Reader+import Unbound.Generics.LocallyNameless (Name)++-- | This exhaustiveness checking algorithm is based on the paper+--   "Lower Your Guards: A Compositional Pattern-Match Coverage Checker":+--   https://www.microsoft.com/en-us/research/uploads/prod/2020/03/lyg.pdf+--+--   Some simplifications were made to adapt the algorithm to suit Disco.+--   The most notable change is that here we always generate (at most) 3+--   concrete examples of uncovered patterns, instead of finding the most+--   general complete description of every uncovered input.+checkClauses :: (Members '[Fresh, Reader Ty.TyDefCtx, Output (Message ann), Embed IO] r) => Name ATerm -> [Ty.Type] -> NonEmpty [APattern] -> Sem r ()+checkClauses name types pats = do+  args <- TI.newVars types+  cl <- zipWithM (desugarClause args) [1 ..] (NonEmpty.toList pats)+  let gdt = foldr1 Branch cl++  let argsNref = []+  (normalizedNrefs, _) <- ua [argsNref] gdt++  examples <- findPosExamples normalizedNrefs args++  unless (null examples) $ do+    let prettyExampleArgs exArgs =+          DSL.hcat $ map prettyPrintExample exArgs++    let prettyExampleLine prettyArgs =+          DSL.text (show name) DSL.<> prettyArgs DSL.<+> DSL.text "= ..."++    let prettyExamples =+          DSL.vcat $ map (prettyExampleLine . prettyExampleArgs) examples++    warn $+      DSL.text "Warning: the function"+        DSL.<+> DSL.text (show name)+        DSL.<+> DSL.text "is undefined for some inputs. For example:"+        DSL.$+$ prettyExamples++prettyPrintExample :: ExamplePat -> Sem r (Doc ann)+prettyPrintExample = runLFresh . runReader initPA . prettyPrintPattern . exampleToDiscoPattern++prettyPrintPattern :: (Members '[Reader PA, LFresh] r) => Pattern -> Sem r (Doc ann)+prettyPrintPattern = withPA funPA . prettyPatternP++exampleToDiscoPattern :: ExamplePat -> Pattern+exampleToDiscoPattern e@(ExamplePat TI.DataCon {TI.dcIdent = ident, TI.dcTypes = types} args) = case (ident, args) of+  (TI.KUnknown, _) -> PWild+  (TI.KUnit, _) -> PUnit+  (TI.KBool b, _) -> PBool b+  (TI.KNat n, _) -> PNat n+  (TI.KInt z, _) ->+    if z >= 0+      then PNat z+      else PNeg (PNat (abs z))+  (TI.KPair, _) -> PTup $ map exampleToDiscoPattern $ resugarPair e+  (TI.KCons, _) ->+    if take 1 types == [Ty.TyC]+      then PString $ resugarString e+      else PList $ map exampleToDiscoPattern $ resugarList e+  (TI.KNil, _) -> PList []+  (TI.KChar c, _) -> PChar c+  (TI.KLeft, [l]) -> PInj L $ exampleToDiscoPattern l+  (TI.KRight, [r]) -> PInj R $ exampleToDiscoPattern r+  (TI.KLeft, _) -> error "Found KLeft data constructor with 0 or multiple arguments"+  (TI.KRight, _) -> error "Found KRight data constructor with 0 or multiple arguments"++resugarPair :: ExamplePat -> [ExamplePat]+resugarPair e@(ExamplePat TI.DataCon {TI.dcIdent = ident} args) = case (ident, args) of+  (TI.KPair, [efst, esnd]) -> efst : resugarPair esnd+  (_, _) -> [e]++resugarList :: ExamplePat -> [ExamplePat]+resugarList (ExamplePat TI.DataCon {TI.dcIdent = ident} args) = case (ident, args) of+  (TI.KCons, [ehead, etail]) -> ehead : resugarList etail+  (_, _) -> []++resugarString :: ExamplePat -> String+resugarString (ExamplePat TI.DataCon {TI.dcIdent = ident} args) = case (ident, args) of+  (TI.KCons, [ehead, etail]) -> assumeExampleChar ehead : resugarString etail+  (_, _) -> []++assumeExampleChar :: ExamplePat -> Char+assumeExampleChar (ExamplePat TI.DataCon {TI.dcIdent = TI.KChar c} _) = c+assumeExampleChar _ = error "Wrongly assumed that an ExamplePat was a Char"++desugarClause :: (Members '[Fresh, Embed IO] r) => [TI.TypedVar] -> Int -> [APattern] -> Sem r Gdt+desugarClause args clauseIdx argsPats = do+  guards <- zipWithM desugarMatch args argsPats+  return $ foldr Guarded (Grhs clauseIdx) $ concat guards++-- To work with the LYG algorithm, we need to desugar n-tuples to nested pairs+-- Just having a Tuple type with a variable number of arguments breaks.+-- Imagine we have+-- foo (1,2,3) = ...+-- foo (1,(2,n)) = ...+-- if we keep things in our nice "sugared" form, the solver will get confused,+-- and not realize that the last element of the tuple is fully covered by n,+-- because there will be two notions of last element: the last in the triple and+-- the last in the nested pair+desugarTuplePats :: [APattern] -> APattern+desugarTuplePats [] = error "Found empty tuple, what happened?"+desugarTuplePats [p] = p+desugarTuplePats (pfst : rest) = APTup (Ty.getType pfst Ty.:*: Ty.getType psnd) [pfst, psnd]+ where+  psnd = desugarTuplePats rest++-- | Convert a Disco APattern into a list of Guards which cover that pattern+--+--   These patterns are currently not handled:+--     , APNeg     --still need to handle rational case+--     , APFrac    --required for rationals?+--     algebraic (probably will be eventually replaced anyway):+--     , APAdd+--     , APMul+--     , APSub+--   These (or some updated version of them) may be handled eventually,+--   once updated arithmetic patterns are merged.+--+--   We treat unhandled patterns as if they are exhaustively matched against+--   (aka, they are seen as wildcards by the checker).+--   This necessarily results in some false negatives, but no false positives.+desugarMatch :: (Members '[Fresh, Embed IO] r) => TI.TypedVar -> APattern -> Sem r [Guard]+desugarMatch var pat = case pat of+  (APTup (ta Ty.:*: tb) [pfst, psnd]) -> do+    varFst <- TI.newVar ta+    varSnd <- TI.newVar tb+    guardsFst <- desugarMatch varFst pfst+    guardsSnd <- desugarMatch varSnd psnd+    let guardPair = (var, GMatch (TI.pair ta tb) [varFst, varSnd])+    return $ [guardPair] ++ guardsFst ++ guardsSnd+  (APTup _ sugary) -> desugarMatch var (desugarTuplePats sugary)+  (APCons _ subHead subTail) -> do+    let typeHead = Ty.getType subHead+    let typeTail = Ty.getType subTail+    varHead <- TI.newVar typeHead+    varTail <- TI.newVar typeTail+    guardsHead <- desugarMatch varHead subHead+    guardsTail <- desugarMatch varTail subTail+    let guardCons = (var, GMatch (TI.cons typeHead typeTail) [varHead, varTail])+    return $ [guardCons] ++ guardsHead ++ guardsTail+  -- We have to desugar Lists into Cons and Nils+  (APList _ []) -> return [(var, GMatch TI.nil [])]+  (APList ty (phead : ptail)) -> do+    -- APCons have the type of the list they are part of+    desugarMatch var (APCons ty phead (APList ty ptail))+  -- we have to desugar to a list, becuse we can match strings with cons+  (APString str) -> do+    let strType = Ty.TyList Ty.TyC+    desugarMatch var (APList strType (map APChar str))+  -- A bit of strangeness is required here because of how patterns work+  (APNat Ty.TyN nat) -> return [(var, GMatch (TI.natural nat) [])]+  (APNat Ty.TyZ z) -> return [(var, GMatch (TI.integer z) [])]+  (APNeg Ty.TyZ (APNat Ty.TyN z)) -> return [(var, GMatch (TI.integer (-z)) [])]+  -- These are more straightforward:+  (APWild _) -> return []+  (APVar ty name) -> do+    let newAlias = TI.TypedVar (name, ty)+    return [(newAlias, GWasOriginally var)]+  APUnit -> return [(var, GMatch TI.unit [])]+  (APBool b) -> return [(var, GMatch (TI.bool b) [])]+  (APChar c) -> return [(var, GMatch (TI.char c) [])]+  (APInj (tl Ty.:+: tr) side subPat) -> do+    let dc = case side of+          L -> TI.left tl+          R -> TI.right tr+    newVar <- case side of+      L -> TI.newVar tl+      R -> TI.newVar tr+    guards <- desugarMatch newVar subPat+    return $ (var, GMatch dc [newVar]) : guards+  _ -> return []++data Gdt where+  Grhs :: Int -> Gdt+  Branch :: Gdt -> Gdt -> Gdt+  Guarded :: Guard -> Gdt -> Gdt+  deriving (Show, Eq)++type Guard = (TI.TypedVar, GuardConstraint)++data GuardConstraint where+  GMatch :: TI.DataCon -> [TI.TypedVar] -> GuardConstraint+  GWasOriginally :: TI.TypedVar -> GuardConstraint+  deriving (Show, Eq)++newtype Literal = Literal (TI.TypedVar, LitCond)++data LitCond where+  LitMatch :: TI.DataCon -> [TI.TypedVar] -> LitCond+  LitNot :: TI.DataCon -> LitCond+  LitWasOriginally :: TI.TypedVar -> LitCond+  deriving (Show, Eq, Ord)++data Ant where+  AGrhs :: [C.NormRefType] -> Int -> Ant+  ABranch :: Ant -> Ant -> Ant+  deriving (Show)++ua :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => [C.NormRefType] -> Gdt -> Sem r ([C.NormRefType], Ant)+ua nrefs gdt = case gdt of+  Grhs k -> return ([], AGrhs nrefs k)+  Branch t1 t2 -> do+    (n1, u1) <- ua nrefs t1+    (n2, u2) <- ua n1 t2+    return (n2, ABranch u1 u2)+  Guarded (y, GWasOriginally x) t -> do+    n <- addLitMulti nrefs $ Literal (y, LitWasOriginally x)+    ua n t+  Guarded (x, GMatch dc args) t -> do+    n <- addLitMulti nrefs $ Literal (x, LitMatch dc args)+    (n', u) <- ua n t+    n'' <- addLitMulti nrefs $ Literal (x, LitNot dc)+    return (n'' ++ n', u)++addLitMulti :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => [C.NormRefType] -> Literal -> Sem r [C.NormRefType]+addLitMulti [] _ = return []+addLitMulti (n : ns) lit = do+  r <- runMaybeT $ addLiteral n lit+  case r of+    Nothing -> addLitMulti ns lit+    Just cfs -> do+      ns' <- addLitMulti ns lit+      return $ cfs : ns'++addLiteral :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => C.NormRefType -> Literal -> MaybeT (Sem r) C.NormRefType+addLiteral constraints (Literal (x, c)) = case c of+  LitWasOriginally z ->+    constraints `C.addConstraint` (x, C.CWasOriginally z)+  LitMatch dc args ->+    constraints `C.addConstraint` (x, C.CMatch dc args)+  LitNot dc ->+    constraints `C.addConstraint` (x, C.CNot dc)++data InhabPat where+  IPIs :: TI.DataCon -> [InhabPat] -> InhabPat+  IPNot :: [TI.DataCon] -> InhabPat+  deriving (Show, Eq, Ord)++-- Sanity check: are we giving the dataconstructor the+-- correct number of arguments?+mkIPMatch :: TI.DataCon -> [InhabPat] -> InhabPat+mkIPMatch k pats =+  if length (TI.dcTypes k) /= length pats+    then error $ "Wrong number of DataCon args" ++ show (k, pats)+    else IPIs k pats++findInhabitants :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => [C.NormRefType] -> [TI.TypedVar] -> Sem r (Poss.Possibilities [InhabPat])+findInhabitants nrefs args = do+  a <- forM nrefs (`findAllForNref` args)+  return $ Poss.anyOf a++findAllForNref :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => C.NormRefType -> [TI.TypedVar] -> Sem r (Poss.Possibilities [InhabPat])+findAllForNref nref args = do+  argPats <- forM args (`findVarInhabitants` nref)+  return $ Poss.allCombinations argPats++findVarInhabitants :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => TI.TypedVar -> C.NormRefType -> Sem r (Poss.Possibilities InhabPat)+findVarInhabitants var cns =+  case posMatch of+    Just (k, args) -> do+      argPossibilities <- findAllForNref cns args+      return (mkIPMatch k <$> argPossibilities)+    Nothing -> case nub negMatches of+      [] -> Poss.retSingle $ IPNot []+      neg -> do+        tyCtx <- ask @Ty.TyDefCtx+        case TI.tyDataCons (TI.getType var) tyCtx of+          TI.Infinite _ -> Poss.retSingle $ IPNot neg+          TI.Finite dcs ->+            do+              let tryAddDc dc = do+                    vars <- TI.newVars (TI.dcTypes dc)+                    runMaybeT (cns `C.addConstraint` (var, C.CMatch dc vars))++              -- Try to add a positive constraint for each data constructor+              -- to the current nref+              -- If any of these additions succeed, save that nref,+              -- it now has positive information+              posNrefs <- catMaybes <$> forM dcs tryAddDc++              if null posNrefs+                then Poss.retSingle $ IPNot []+                else Poss.anyOf <$> forM posNrefs (findVarInhabitants var)+ where+  constraintsOnX = C.onVar var cns+  posMatch = C.posMatch constraintsOnX+  negMatches = C.negMatches constraintsOnX++findRedundant :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => Ant -> [TI.TypedVar] -> Sem r [Int]+findRedundant ant args = case ant of+  AGrhs ref i -> do+    uninhabited <- Poss.none <$> findInhabitants ref args+    return [i | uninhabited]+  ABranch a1 a2 -> mappend <$> findRedundant a1 args <*> findRedundant a2 args++data ExamplePat where+  ExamplePat :: TI.DataCon -> [ExamplePat] -> ExamplePat+  deriving (Show)++-- | Less general version of the above inhabitant finding function+--   returns a maximum of 3 possible args lists that haven't been matched against,+--   as to not overwhelm new users of the language.+--   This is essentially a DFS, and it has a bad habit of+--   trying to build infinite lists whenever it can, so we give it a max depth of 32+--   If we reach 32 levels of nested dataconstructors in this language,+--   it is pretty safe to assume we were chasing after an infinite structure+findPosExamples :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => [C.NormRefType] -> [TI.TypedVar] -> Sem r [[ExamplePat]]+findPosExamples nrefs args = do+  a <- forM nrefs (\nref -> findAllPosForNref 32 nref args)+  return $ take 3 $ Poss.getPossibilities $ Poss.anyOf a++findAllPosForNref :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => Int -> C.NormRefType -> [TI.TypedVar] -> Sem r (Poss.Possibilities [ExamplePat])+findAllPosForNref fuel nref args = do+  argPats <- forM args (\arg -> findVarPosExamples (fuel - 1) arg nref)+  return $ Poss.allCombinations argPats++findVarPosExamples :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => Int -> TI.TypedVar -> C.NormRefType -> Sem r (Poss.Possibilities ExamplePat)+findVarPosExamples fuel var cns =+  if fuel < 0+    then return mempty+    else case posMatch of+      Just (k, args) -> do+        argPossibilities <- findAllPosForNref (fuel - 1) cns args+        return (mkExampleMatch k <$> argPossibilities)+      Nothing -> do+        tyCtx <- ask @Ty.TyDefCtx+        let dcs = getPosFrom (TI.getType var) tyCtx negMatches+        let tryAddDc dc = do+              vars <- TI.newVars (TI.dcTypes dc)+              runMaybeT (cns `C.addConstraint` (var, C.CMatch dc vars))+        -- Try to add a positive constraint for each data constructor+        -- to the current nref+        -- If any of these additions succeed, save that nref,+        -- it now has positive information+        posNrefs <- catMaybes <$> forM dcs tryAddDc++        Poss.anyOf <$> forM posNrefs (findVarPosExamples (fuel - 1) var)+ where+  constraintsOnX = C.onVar var cns+  posMatch = C.posMatch constraintsOnX+  negMatches = C.negMatches constraintsOnX++getPosFrom :: Ty.Type -> Ty.TyDefCtx -> [TI.DataCon] -> [TI.DataCon]+getPosFrom ty ctx neg = take 3 $ filter (`notElem` neg) dcs+ where+  dcs = case TI.tyDataCons ty ctx of+    TI.Finite dcs' -> dcs'+    TI.Infinite dcs' -> dcs'++mkExampleMatch :: TI.DataCon -> [ExamplePat] -> ExamplePat+mkExampleMatch k pats =+  if length (TI.dcTypes k) /= length pats+    then error $ "Wrong number of DataCon args" ++ show (k, pats)+    else ExamplePat k pats

@@ -0,0 +1,151 @@+-- |+-- Module      :  Disco.Exhaustiveness.Constraint+-- Copyright   :  disco team and contributors+-- Maintainer  :  byorgey@gmail.com+--+-- SPDX-License-Identifier: BSD-3-Clause+--+-- The heart of the Lower Your Guards algorithm.+-- Functions for converting constraints detailing+-- pattern matches into a normalized description+-- of everything that is left uncovered.+module Disco.Exhaustiveness.Constraint where++import Control.Applicative (Alternative)+import Control.Monad (foldM, guard)+import Control.Monad.Trans (lift)+import Control.Monad.Trans.Maybe (MaybeT, runMaybeT)+import Data.Bifunctor (first)+import Data.List (partition)+import Data.Maybe (isJust, listToMaybe, mapMaybe)+import Disco.Effects.Fresh (Fresh)+import qualified Disco.Exhaustiveness.TypeInfo as TI+import qualified Disco.Types as Ty+import Polysemy+import Polysemy.Reader++data Constraint where+  CMatch :: TI.DataCon -> [TI.TypedVar] -> Constraint+  CNot :: TI.DataCon -> Constraint+  CWasOriginally :: TI.TypedVar -> Constraint+  deriving (Show, Eq, Ord)++posMatch :: [Constraint] -> Maybe (TI.DataCon, [TI.TypedVar])+posMatch constraints = listToMaybe $ mapMaybe (\case (CMatch k ys) -> Just (k, ys); _ -> Nothing) constraints++negMatches :: [Constraint] -> [TI.DataCon]+negMatches = mapMaybe (\case (CNot k) -> Just k; _ -> Nothing)++type ConstraintFor = (TI.TypedVar, Constraint)++-- Resolves term equalities, finding the leftmost id for a variable+-- I believe I3 of section 3.4 allows us to+-- do a linear scan from right to left+lookupVar :: TI.TypedVar -> [ConstraintFor] -> TI.TypedVar+lookupVar x = foldr getNextId x+ where+  getNextId (x', CWasOriginally y) | x' == x = const y+  getNextId _ = id++alistLookup :: (Eq a) => a -> [(a, b)] -> [b]+alistLookup a = map snd . filter ((== a) . fst)++onVar :: TI.TypedVar -> [ConstraintFor] -> [Constraint]+onVar x cs = alistLookup (lookupVar x cs) cs++type NormRefType = [ConstraintFor]++addConstraints :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> [ConstraintFor] -> MaybeT (Sem r) NormRefType+addConstraints = foldM addConstraint++addConstraint :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> ConstraintFor -> MaybeT (Sem r) NormRefType+addConstraint cns (x, c) = do+  breakIf $ any (conflictsWith c) (onVar x cns)+  addConstraintHelper cns (lookupVar x cns, c)++addConstraintHelper :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> ConstraintFor -> MaybeT (Sem r) NormRefType+addConstraintHelper cns cf@(origX, c) = case c of+  --- Equation (10)+  CMatch k args -> do+    case getConstructorArgs k (onVar origX cns) of+      -- 10c+      Just args' ->+        addConstraints+          cns+          (zipWith (\a b -> (a, CWasOriginally b)) args args')+      Nothing -> return added+  --- Equation (11)+  CNot _ -> do+    inh <- lift (inhabited added origX)+    guard inh -- ensure that origX is still inhabited, as per I2+    return added+  -- Equation (14)+  CWasOriginally y -> do+    let origY = lookupVar y cns+    if origX == origY+      then return cns+      else do+        let (noX', withX') = partition ((/= origX) . fst) cns+        addConstraints (noX' ++ [cf]) (substituteVarIDs origY origX withX')+ where+  added = cns ++ [cf]++-----+----- Helper functions for adding constraints:+-----++breakIf :: (Alternative f) => Bool -> f ()+breakIf = guard . not++-- | Returns a predicate that returns true if another+--   constraint conflicts with the one given.+--   This alone is not sufficient to test+--   if a constraint can be added, but it+--   filters out the easy negatives early on+conflictsWith :: Constraint -> (Constraint -> Bool)+conflictsWith c = case c of+  CMatch k _ -> \case+    (CMatch k' _) | k /= k' -> True -- 10a+    (CNot k') | k == k' -> True -- 10b+    _ -> False+  CNot k -> \case+    (CMatch k' _) | k == k' -> True -- 11a+    _ -> False+  CWasOriginally _ -> const False++-- | Search for a MatchDataCon that is matching on k specifically+--   (there should be at most one, see I4 in section 3.4)+--   and if it exists, return the variable ids of its arguments+getConstructorArgs :: TI.DataCon -> [Constraint] -> Maybe [TI.TypedVar]+getConstructorArgs k cfs =+  listToMaybe $+    mapMaybe (\case (CMatch k' vs) | k' == k -> Just vs; _ -> Nothing) cfs++-- | substituting y *for* x+--   ie replace the second with the first, replace x with y+substituteVarIDs :: TI.TypedVar -> TI.TypedVar -> [ConstraintFor] -> [ConstraintFor]+substituteVarIDs y x = map (first subst)+ where+  subst var = if var == x then y else x++-- | Deals with I2 from section 3.4+--   if a variable in the context has a resolvable type, there must be at least one constructor+--   which can be instantiated without contradiction of the refinement type+--   This function tests if this is true+inhabited :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> TI.TypedVar -> Sem r Bool+inhabited n var = do+  tyCtx <- ask @Ty.TyDefCtx+  case TI.tyDataCons (TI.getType var) tyCtx of+    TI.Infinite _ -> return True -- assume opaque types are inhabited+    TI.Finite constructors -> do+      or <$> mapM (instantiate n var) constructors++-- | Attempts to "instantiate" a match of the dataconstructor k on x+--   If we can add the MatchDataCon constraint to the normalized refinement+--   type without contradiction (a Nothing value),+--   then x is inhabited by k and we return true+instantiate :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> TI.TypedVar -> TI.DataCon -> Sem r Bool+instantiate cns var k = do+  args <- TI.newVars $ TI.dcTypes k+  let attempt = cns `addConstraint` (var, CMatch k args)+  isJust <$> runMaybeT attempt

@@ -0,0 +1,59 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++-- |+-- Module      :  Disco.Exhaustiveness.Possibilities+-- Copyright   :  disco team and contributors+-- Maintainer  :  byorgey@gmail.com+--+-- SPDX-License-Identifier: BSD-3-Clause+--+-- Meaningful types and functions for describing+-- combinations of different possible options.+module Disco.Exhaustiveness.Possibilities (Possibilities, retSingle, allCombinations, anyOf, none, getPossibilities) where++import Data.Foldable (fold)++newtype Possibilities a = Possibilities {getPossibilities :: [a]}+  deriving (Show, Eq, Ord, Functor, Semigroup, Monoid, Applicative)++anyOf :: [Possibilities a] -> Possibilities a+anyOf = fold++none :: Possibilities a -> Bool+none = null . getPossibilities++retSingle :: (Monad m) => a -> m (Possibilities a)+retSingle i = return $ Possibilities [i]++-- | List all possible paths through the list of Possibilites+--+--   Ex.+--   > allCombinations+--       [ Possibilities [1]+--       , Possibilities [2,3]+--       , Possibilities [4]+--       , Possibilities [5,6,7]+--       ]+--   ===+--   Possibilities {getPossibilities =+--     [[1,2,4,5]+--     ,[1,2,4,6]+--     ,[1,2,4,7]+--     ,[1,3,4,5]+--     ,[1,3,4,6]+--     ,[1,3,4,7]+--     ]}+--+--         2       5+--       /   \   /+--     1       4 --6+--       \   /   \+--         3       7+--+--   If any any of the Possibilities is empty,+--   an empty Possibility is returned+--+--   In other words, this lists all elements of the+--   cartesian product of multiple sets+allCombinations :: [Possibilities a] -> Possibilities [a]+allCombinations = sequenceA

@@ -0,0 +1,183 @@+-- |+-- Module      :  Disco.Exhaustiveness.TypeInfo+-- Copyright   :  disco team and contributors+-- Maintainer  :  byorgey@gmail.com+--+-- SPDX-License-Identifier: BSD-3-Clause+--+-- Utilities for converting Disco types into 'Constructors'+-- that the exhaustiveness checker understands, and utilities+-- for working with 'TypedVar's and their names.+module Disco.Exhaustiveness.TypeInfo where++import Control.Monad (replicateM)+import Data.Function (on)+import Data.List ((\\))+import qualified Data.Map as M+import Disco.AST.Typed (ATerm)+import Disco.Effects.Fresh (Fresh, fresh)+import qualified Disco.Types as Ty+import Polysemy+import Unbound.Generics.LocallyNameless (Name, s2n)++newtype TypedVar = TypedVar (Name ATerm, Ty.Type)+  deriving (Show, Ord)++instance Eq TypedVar where+  TypedVar (n1, _) == TypedVar (n2, _) = n1 == n2++getType :: TypedVar -> Ty.Type+getType (TypedVar (_, t)) = t++data DataCon = DataCon+  { dcIdent :: Ident+  , dcTypes :: [Ty.Type]+  }+  deriving (Ord, Show)++-- This is very important, as we have (sometimes recursive) type aliases+-- Equality of dcTypes doesn't measure equality of dataconstructors,+-- because we could have two different aliases for the same type+-- (And we can't just resolve all aliases up front, because they can be recursive)+instance Eq DataCon where+  (==) = (==) `on` dcIdent++-- The Show instance of 'Ident' should never be used+-- for displaying results to the user.+-- Instead, convert to a proper pattern and use the+-- pretty printer, like in Exhaustiveness.hs+data Ident where+  KUnit :: Ident+  KBool :: Bool -> Ident+  KNat :: Integer -> Ident+  KInt :: Integer -> Ident+  KPair :: Ident+  KCons :: Ident+  KNil :: Ident+  KChar :: Char -> Ident+  KLeft :: Ident+  KRight :: Ident+  KUnknown :: Ident+  deriving (Show, Eq, Ord)++-- | 'Finite' constructors are used in the LYG checker+--   'Infinite' constructors are used when reporting+--   examples of uncovered patterns, we only pick out a few of them+data Constructors where+  Finite :: [DataCon] -> Constructors+  Infinite :: [DataCon] -> Constructors++unknown :: DataCon+unknown = DataCon {dcIdent = KUnknown, dcTypes = []}++unit :: DataCon+unit = DataCon {dcIdent = KUnit, dcTypes = []}++bool :: Bool -> DataCon+bool b = DataCon {dcIdent = KBool b, dcTypes = []}++natural :: Integer -> DataCon+natural n = DataCon {dcIdent = KNat n, dcTypes = []}++integer :: Integer -> DataCon+integer z = DataCon {dcIdent = KInt z, dcTypes = []}++char :: Char -> DataCon+char c = DataCon {dcIdent = KChar c, dcTypes = []}++cons :: Ty.Type -> Ty.Type -> DataCon+cons tHead tTail = DataCon {dcIdent = KCons, dcTypes = [tHead, tTail]}++nil :: DataCon+nil = DataCon {dcIdent = KNil, dcTypes = []}++pair :: Ty.Type -> Ty.Type -> DataCon+pair a b = DataCon {dcIdent = KPair, dcTypes = [a, b]}++left :: Ty.Type -> DataCon+left tl = DataCon {dcIdent = KLeft, dcTypes = [tl]}++right :: Ty.Type -> DataCon+right tr = DataCon {dcIdent = KRight, dcTypes = [tr]}++tyDataCons :: Ty.Type -> Ty.TyDefCtx -> Constructors+tyDataCons ty ctx = tyDataConsHelper $ resolveAlias ty ctx++-- Type aliases that would cause infinite recursion here are+-- not possible to construct, so we don't have to worry about that.+-- (aka cyclic type definitions are not allowed in Disco)+resolveAlias :: Ty.Type -> Ty.TyDefCtx -> Ty.Type+resolveAlias (Ty.TyUser name args) ctx = case M.lookup name ctx of+  Nothing -> error $ show ctx ++ "\nType definition not found for: " ++ show name+  Just (Ty.TyDefBody _argNames typeCon) -> resolveAlias (typeCon args) ctx+resolveAlias t _ = t++-- | Assuming type aliases have been resolved, this+--   function converts Disco types into lists of DataCons+--   that are compatible with the LYG checker.+--+--   A list of constructors is 'Infinite' if the only way to fully+--   match against the type is with a wildcard or variable pattern.+--   Otherwise, it is 'Finite'.+--+--   The LYG checker only reads the list of constructors if+--   a type is 'Finite'. From the point of view of the checker,+--   'Infinite' is a synonym for opaque, and the constructors are discarded.+--   The dataconstructors in an `Infinite` list are only+--   used when generating the 3 positive examples of what+--   you haven't matched against.+--   This will probably need to change a bit when bringing+--   exhaustiveness checking to the new arithmetic patterns.+--+--   Notice the last case of this function, which a wildcard handling the types:+--   (_ Ty.:->: _) (Ty.TySet _) (Ty.TyBag _) (Ty.TyVar _)+--   (Ty.TySkolem _) (Ty.TyProp) (Ty.TyMap _ _) (Ty.TyGraph _)+--+--   I believe all of these are impossible to pattern match against+--   with anything other than a wildcard (or variable pattern) in Disco, so they should always+--   be fully covered. But if they are in a pair, for example, Set(Int)*Int,+--   we still need to generate 3 examples of the pair if that Int part isn't covered.+--   So how do we fill the concrete part of Set(Int), (or a generic type "a", or a function, etc.)?+--   I'm calling that 'unknown', and printing an underscore.+--   (Also, I'm using 'Infinite' for reasons metioned above).+tyDataConsHelper :: Ty.Type -> Constructors+tyDataConsHelper (a Ty.:*: b) = Finite [pair a b]+tyDataConsHelper (l Ty.:+: r) = Finite [left l, right r]+tyDataConsHelper t@(Ty.TyList a) = Finite [nil, cons a t]+tyDataConsHelper Ty.TyVoid = Finite []+tyDataConsHelper Ty.TyUnit = Finite [unit]+tyDataConsHelper Ty.TyBool = Finite [bool True, bool False]+tyDataConsHelper Ty.TyN = Infinite $ map natural [0, 1 ..]+-- Many thanks to this answer and its comment for a convenient way to list the integers+-- https://stackoverflow.com/a/9749957+tyDataConsHelper Ty.TyZ = Infinite $ map integer $ 0 : [y | x <- [1 ..], y <- [x, -x]]+tyDataConsHelper Ty.TyF = Infinite []+tyDataConsHelper Ty.TyQ = Infinite []+-- The Char constructors are all unicode characters, but+-- given in a very particular order that I think will+-- make the most sense for students.+-- Many thanks to Dr. Yorgey for mentioning [minBound .. maxBound] and \\+tyDataConsHelper Ty.TyC =+  Infinite $+    map char $+      alphanum ++ (allUnicodeNicelyOrdered \\ alphanum)+ where+  allUnicodeNicelyOrdered = [(toEnum 32) .. (toEnum 126)] ++ [(toEnum 161) .. maxBound] ++ [minBound .. (toEnum 31)] ++ [(toEnum 127) .. (toEnum 160)]+  alphanum = ['a' .. 'z'] ++ ['A' .. 'Z'] ++ ['0' .. '9']+tyDataConsHelper _ = Infinite [unknown]++newName :: (Member Fresh r) => Sem r (Name ATerm)+newName = fresh $ s2n ""++newVar :: (Member Fresh r) => Ty.Type -> Sem r TypedVar+newVar types = do+  names <- newName+  return $ TypedVar (names, types)++newNames :: (Member Fresh r) => Int -> Sem r [Name ATerm]+newNames i = replicateM i newName++newVars :: (Member Fresh r) => [Ty.Type] -> Sem r [TypedVar]+newVars types = do+  names <- newNames (length types)+  return $ zipWith (curry TypedVar) names types

@@ -1,5 +1,5 @@+{-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE StandaloneDeriving #-}  -- |@@ -28,39 +28,28 @@   (?~),   (^.),  )-import Control.Monad.Except+import Control.Monad (forM_, void, when)+import Control.Monad.Except ()+import Data.Bifunctor (second) import Data.Char (isSpace) import Data.Coerce-import Data.List (find, isPrefixOf, sortBy)+import Data.List (find, isPrefixOf, sortBy, transpose)+import Data.List.NonEmpty qualified as NE import Data.Map ((!))-import qualified Data.Map as M-import Data.Typeable-import System.FilePath (splitFileName)-import Prelude as P--import Text.Megaparsec hiding (State, runParser)-import qualified Text.Megaparsec.Char as C-import Unbound.Generics.LocallyNameless (-  Name,-  name2String,-  string2Name,- )--import Disco.Effects.Input-import Disco.Effects.LFresh-import Disco.Effects.State-import Polysemy-import Polysemy.Error hiding (try)-import Polysemy.Output-import Polysemy.Reader-+import Data.Map qualified as M import Data.Maybe (mapMaybe, maybeToList)+import Data.Typeable import Disco.AST.Surface import Disco.AST.Typed import Disco.Compile import Disco.Context as Ctx import Disco.Desugar import Disco.Doc+import Disco.Effects.Fresh (runFresh)+import Disco.Effects.Input+import Disco.Effects.LFresh+import Disco.Effects.State+import Disco.Enumerate (enumerateType) import Disco.Error import Disco.Eval import Disco.Extensions@@ -80,17 +69,33 @@   withExts,  ) import Disco.Pretty hiding (empty, (<>))-import qualified Disco.Pretty as PP+import Disco.Pretty qualified as PP import Disco.Property (prettyTestResult) import Disco.Syntax.Operators import Disco.Syntax.Prims (-  Prim (PrimBOp, PrimUOp),+  Prim (PrimAbs, PrimBOp, PrimCeil, PrimFloor, PrimUOp),   toPrim,  ) import Disco.Typecheck import Disco.Typecheck.Erase-import Disco.Types (toPolyType, pattern TyString)+import Disco.Types+import Disco.Util (maximum0) import Disco.Value+import Polysemy+import Polysemy.Error hiding (try)+import Polysemy.Output+import Polysemy.Reader+import System.FilePath (splitFileName)+import Text.Megaparsec hiding (State, runParser)+import Text.Megaparsec.Char qualified as C+import Text.Megaparsec.Char.Lexer qualified as L+import Text.PrettyPrint.Boxes qualified as B+import Unbound.Generics.LocallyNameless (+  Name,+  name2String,+  string2Name,+ )+import Prelude as P  ------------------------------------------------------------ -- REPL expression type@@ -106,6 +111,7 @@   Parse :: Term -> REPLExpr 'CParse -- Show the parsed AST   Pretty :: Term -> REPLExpr 'CPretty -- Pretty-print a term   Print :: Term -> REPLExpr 'CPrint -- Print a string+  Table :: Term -> REPLExpr 'CTable -- Print a table   Ann :: Term -> REPLExpr 'CAnn -- Show type-annotated term   Desugar :: Term -> REPLExpr 'CDesugar -- Show a desugared term   Compile :: Term -> REPLExpr 'CCompile -- Show a compiled term@@ -150,6 +156,7 @@   | CParse   | CPretty   | CPrint+  | CTable   | CAnn   | CDesugar   | CCompile@@ -229,6 +236,7 @@   , SomeCmd parseCmd   , SomeCmd prettyCmd   , SomeCmd printCmd+  , SomeCmd tableCmd   , SomeCmd reloadCmd   , SomeCmd showDefnCmd   , SomeCmd typeCheckCmd@@ -262,7 +270,9 @@  -- | Parse a file name. fileParser :: Parser FilePath-fileParser = many C.spaceChar *> many (satisfy (not . isSpace))+fileParser = many C.spaceChar *> some (escapedSpace <|> L.charLiteral <|> anySingle)+ where+  escapedSpace = try (C.char '\\' *> C.char ' ')  -- | A parser for something entered at the REPL prompt. lineParser :: REPLCommands -> Parser SomeREPLExpr@@ -303,7 +313,7 @@   REPLExpr 'CAnn ->   Sem r () handleAnn (Ann t) = do-  (at, _) <- typecheckTop $ inferTop t+  (at, _) <- typecheckTop $ inferTop1 t   infoPretty at  ------------------------------------------------------------@@ -326,7 +336,7 @@   REPLExpr 'CCompile ->   Sem r () handleCompile (Compile t) = do-  (at, _) <- typecheckTop $ inferTop t+  (at, _) <- typecheckTop $ inferTop1 t   infoPretty . compileTerm $ at  ------------------------------------------------------------@@ -349,7 +359,7 @@   REPLExpr 'CDesugar ->   Sem r () handleDesugar (Desugar t) = do-  (at, _) <- typecheckTop $ inferTop t+  (at, _) <- typecheckTop $ inferTop1 t   info $ pretty' . eraseDTerm . runDesugar . desugarTerm $ at  ------------------------------------------------------------@@ -390,25 +400,25 @@ handleDoc (Doc (DocTerm _)) =   err "Can't display documentation for an expression.  Try asking about a function, operator, or type name." handleDoc (Doc (DocPrim p)) = handleDocPrim p-handleDoc (Doc (DocOther s)) = handleDocOther s+handleDoc (Doc (DocOther s)) = handleDocMap (OtherKey s)  handleDocBool :: Members '[Output (Message ())] r => Sem r () handleDocBool =   info $-    "true and false (also written True and False) are the two possible values of type Boolean."-      $+$ mkReference "bool"+    "T and F (also written true and false, or True and False) are the two possible values of type Boolean."+      $+$ formatReference (mkRef "bool")  handleDocUnit :: Members '[Output (Message ())] r => Sem r () handleDocUnit =   info $     "The unit value, i.e. the single value of type Unit."-      $+$ mkReference "unit"+      $+$ formatReference (mkRef "unit")  handleDocWild :: Members '[Output (Message ())] r => Sem r () handleDocWild =   info $     "A wildcard pattern."-      $+$ mkReference "wild-pattern"+      $+$ formatReference (mkRef "wild-pattern")  handleDocVar ::   Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>@@ -438,16 +448,16 @@     (binds, def) ->       mapM_ (showDoc docs) (map Left binds ++ map Right (maybeToList def))  where-  showDoc docMap (Left (qn, ty)) =+  showDoc docs (Left (qn, ty)) =     info $       hsep [pretty' x, ":", pretty' ty]-        $+$ case Ctx.lookup' qn docMap of+        $+$ case Ctx.lookup' qn docs of           Just (DocString ss : _) -> vcat (text "" : map text ss ++ [text ""])           _ -> PP.empty-  showDoc docMap (Right tdBody) =+  showDoc docs (Right tdBody) =     info $       pretty' (name2String x, tdBody)-        $+$ case Ctx.lookupAll' x docMap of+        $+$ case Ctx.lookupAll' x docs of           ((_, DocString ss : _) : _) -> vcat (text "" : map text ss ++ [text ""])           _ -> PP.empty @@ -457,31 +467,27 @@   Sem r () handleDocPrim prim = do   handleTypeCheck (TypeCheck (TPrim prim))-  info-    . vcat-    $ ( case prim of-          PrimUOp u -> describeAlts (f == Post) (f == Pre) syns-           where-            OpInfo (UOpF f _) syns _ = uopMap ! u-          PrimBOp b -> describeAlts True True (opSyns $ bopMap ! b)-          _ -> []-      )-      ++ ( case prim of-            PrimUOp u -> [describePrec (uPrec u)]-            PrimBOp b -> [describePrec (bPrec b) <> describeFixity (assoc b)]+  let attrs =+        ( case prim of+            PrimUOp u -> case uopMap ! u of+              OpInfo (UOpF f _) syns _ -> describeAlts (f == Post) (f == Pre) syns+              _ -> error $ "handleDocPrim: No OpInfo for unary op " ++ show u+            PrimBOp b -> describeAlts True True (opSyns $ bopMap ! b)+            PrimFloor -> describeAlts False False ["floor(x)", "⌊x⌋"]+            PrimCeil -> describeAlts False False ["ceiling(x)", "⌈x⌉"]+            PrimAbs -> describeAlts False False ["abs(x)", "|x|"]             _ -> []-         )-  case (M.lookup prim primDoc, M.lookup prim primReference) of-    (Nothing, Nothing) -> return ()-    (Nothing, Just p) -> info $ mkReference p-    (Just d, mp) ->-      info $-        vcat-          [ PP.empty-          , text d-          , PP.empty-          , maybe PP.empty (\p -> vcat [mkReference p, PP.empty]) mp-          ]+        )+          ++ ( case prim of+                PrimUOp u -> [describePrec (uPrec u)]+                PrimBOp b -> [describePrec (bPrec b) <> describeFixity (assoc b)]+                _ -> []+             )+  case attrs of+    [] -> pure ()+    _ -> info . vcat $ attrs+  info PP.empty+  handleDocMap (PrimKey prim)  where   describePrec p = "precedence level" <+> text (show p)   describeFixity In = PP.empty@@ -498,25 +504,28 @@         , if post then "~" else PP.empty         ] -mkReference :: String -> Sem r (Doc ann)-mkReference p =-  "https://disco-lang.readthedocs.io/en/latest/reference/" <> text p <> ".html"+formatReference :: Reference -> Sem r (Doc ann)+formatReference (Reference rty p) = case rty of+  Ref -> "https://disco-lang.readthedocs.io/en/latest/reference/" <> text p <> ".html"+  Intro -> "https://disco-lang.readthedocs.io/en/latest/introduction/" <> text p <> ".html"+  URL -> text p -handleDocOther ::+handleDocMap ::   Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>-  String ->+  DocKey ->   Sem r ()-handleDocOther s =-  case (M.lookup s otherDoc, M.lookup s otherReference) of-    (Nothing, Nothing) -> info $ "No documentation found for '" <> text s <> "'."-    (Nothing, Just p) -> info $ mkReference p-    (Just d, mp) ->-      info $-        vcat-          [ text d-          , PP.empty-          , maybe PP.empty (\p -> vcat [mkReference p, PP.empty]) mp-          ]+handleDocMap k = case M.lookup k docMap of+  Nothing -> case k of+    PrimKey _ -> pure ()+    OtherKey s -> info $ "No documentation found for '" <> text s <> "'."+  Just (d, refs) ->+    info . vcat $+      [ text d+      , PP.empty+      ]+        ++ case refs of+          [] -> []+          _ -> map formatReference refs ++ [PP.empty]  ------------------------------------------------------------ -- eval@@ -538,7 +547,7 @@   REPLExpr 'CEval ->   Sem r () handleEval (Eval m) = do-  mi <- inputToState @TopInfo $ loadParsedDiscoModule False FromCwdOrStdlib REPLModule m+  mi <- loadParsedDiscoModule False FromCwdOrStdlib REPLModule m   addToREPLModule mi   forM_ (mi ^. miTerms) (mapError EvalErr . evalTerm True . fst) @@ -589,7 +598,7 @@   sortedList cmds =     sortBy (\(SomeCmd x) (SomeCmd y) -> compare (name x) (name y)) $ filteredCommands cmds   showCmd c = text (padRight (helpcmd c) maxlen ++ "  " ++ shortHelp c)-  longestCmd cmds = maximum $ map (\(SomeCmd c) -> length $ helpcmd c) cmds+  longestCmd cmds = maximum0 $ map (\(SomeCmd c) -> length $ helpcmd c) cmds   padRight s maxsize = take maxsize (s ++ repeat ' ')   --  don't show dev-only commands by default   filteredCommands = P.filter (\(SomeCmd c) -> category c == User)@@ -782,6 +791,148 @@   info $ text (vlist vchar v)  ------------------------------------------------------------+-- :table++tableCmd :: REPLCommand 'CTable+tableCmd =+  REPLCommand+    { name = "table"+    , helpcmd = ":table <expr>"+    , shortHelp = "Print a formatted table for a list or function"+    , category = User+    , cmdtype = ColonCmd+    , action = handleTable+    , parser = Table <$> parseTermOrOp+    }++handleTable :: Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': EvalEffects) r => REPLExpr 'CTable -> Sem r ()+handleTable (Table t) = do+  (at, ty) <- inputToState . typecheckTop $ inferTop1 t+  v <- mapError EvalErr . evalTerm False $ at++  tydefs <- use @TopInfo (replModInfo . to allTydefs)+  info $ runInputConst tydefs $ formatTableFor ty v >>= text++-- | The max number of rows to show in the output of :table.+maxFunTableRows :: Int+maxFunTableRows = 25++-- | Uncurry a type, turning a type of the form A -> B -> ... -> Y ->+--   Z into the pair of types (A * B * ... * Y * Unit, Z).  Note we do+--   not optimize away the Unit at the end of the chain, since this+--   needs to be an isomorphism.  Otherwise we would not be able to+--   distinguish between e.g.  Z and Unit -> Z.+uncurryTy :: Type -> (Type, Type)+uncurryTy (tyA :->: tyB) = (tyA :*: tyAs, tyRes)+ where+  (tyAs, tyRes) = uncurryTy tyB+uncurryTy ty = (TyUnit, ty)++-- | Evaluate the application of a curried function to an uncurried+--   input.+evalCurried :: Members EvalEffects r => Type -> Value -> Type -> Value -> Sem r Value+evalCurried (_ :->: tyB) f (_ :*: tyY) v = do+  let (v1, v2) = vpair id id v+  f' <- evalApp f [v1]+  evalCurried tyB f' tyY v2+evalCurried _ v _ _ = return v++formatTableFor ::+  Members (LFresh ': Input TyDefCtx ': EvalEffects) r =>+  PolyType ->+  Value ->+  Sem r String+formatTableFor (Forall bnd) v = lunbind bnd $ \(vars, ty) ->+  case vars of+    [] -> case ty of+      TyList ety -> do+        byRows <- mapM (formatCols TopLevel ety) . vlist id $ v+        return $ renderTable byRows+      (_ :->: _) -> do+        let (tyInputs, tyRes) = uncurryTy ty+            vs = take (maxFunTableRows + 1) $ enumerateType tyInputs+            (tyInputs', stripV) = stripFinalUnit tyInputs+        results <- mapM (evalCurried ty v tyInputs) vs+        byRows <-+          mapM+            (formatCols TopLevel (tyInputs' :*: tyRes))+            (zipWith (curry (pairv id id)) (take maxFunTableRows (map stripV vs)) results)+        return $ renderTable (byRows ++ [[(B.left, "...")] | length vs == maxFunTableRows + 1])+      _otherTy -> do+        tyStr <- prettyStr ty+        return $ "Don't know how to make a table for type " ++ tyStr+    _vars -> return "Can't make a table for a polymorphic type"++-- | Strip the unit type from the end of a chain like (tA :*: (tB :*: (tC :*: Unit))),+--   which is an output of 'uncurryTy', and return a function to make the corresponding+--   change to a value of that type.+stripFinalUnit :: Type -> (Type, Value -> Value)+stripFinalUnit (tA :*: TyUnit) = (tA, fst . vpair id id)+stripFinalUnit (tA :*: tB) = (tA :*: tB', pairv id id . second v' . vpair id id)+ where+  (tB', v') = stripFinalUnit tB+stripFinalUnit ty = (ty, id)++data Level = TopLevel | NestedPair | InnerLevel+  deriving (Eq, Ord, Show)++-- | Turn a value into a list of formatted columns in a type-directed+--   way.  Lists and tuples are only split out into columns if they+--   occur at the top level; lists or tuples nested inside of other+--   data structures are simply pretty-printed.  However, note we have+--   to make a special case for nested tuples: if a pair type occurs+--   at the top level we keep recursively splitting out its children+--   into columns as long as they are also pair types.+--+--   Any value of a type other than a list or tuple is simply+--   pretty-printed.+formatCols ::+  (Member LFresh r, Member (Input TyDefCtx) r) =>+  Level ->+  Type ->+  Value ->+  Sem r [(B.Alignment, String)]+formatCols l (t1 :*: t2) (vpair id id -> (v1, v2))+  | l `elem` [TopLevel, NestedPair] =+      (++) <$> formatCols NestedPair t1 v1 <*> formatCols NestedPair t2 v2+-- Special case for String (= List Char), just print as string value+formatCols TopLevel TyString v = formatColDefault TyString v+-- For any other lists @ top level, print each element in a separate column+formatCols TopLevel (TyList ety) (vlist id -> vs) =+  concat <$> mapM (formatCols InnerLevel ety) vs+formatCols _ ty v = formatColDefault ty v++-- | Default formatting of a typed column value by simply+--   pretty-printing it, and using the alignment appropriate for its+--   type.+formatColDefault ::+  (Member (Input TyDefCtx) r, Member LFresh r) =>+  Type ->+  Value ->+  Sem r [(B.Alignment, String)]+formatColDefault ty v = (: []) . (alignmentForType ty,) <$> renderDoc (prettyValue ty v)++alignmentForType :: Type -> B.Alignment+alignmentForType ty | ty `elem` [TyN, TyZ, TyF, TyQ] = B.right+alignmentForType _ = B.left++-- | Render a table, given as a list of rows, formatting it so that+-- each column is aligned.+renderTable :: [[(B.Alignment, String)]] -> String+renderTable = stripTrailingWS . B.render . B.hsep 2 B.top . map renderCol . transpose . pad+ where+  pad :: [[(B.Alignment, String)]] -> [[(B.Alignment, String)]]+  pad rows = map (padTo (maximum0 . map length $ rows)) rows+  padTo n = take n . (++ repeat (B.left, ""))++  renderCol :: [(B.Alignment, String)] -> B.Box+  renderCol [] = B.nullBox+  renderCol ((align, x) : xs) = B.vcat align . map B.text $ x : map snd xs++  stripTrailingWS = unlines . map stripEnd . lines+  stripEnd = reverse . dropWhile isSpace . reverse++------------------------------------------------------------ -- :reload  reloadCmd :: REPLCommand 'CReload@@ -837,7 +988,7 @@     let ds = map (pretty' . snd) xdefs ++ maybe [] (pure . pretty' . (name2s,)) mtydef     case ds of       [] -> text "No definition for" <+> pretty' x-      _ -> vcat ds+      _nonEmptyList -> vcat ds  ------------------------------------------------------------ -- :test@@ -877,28 +1028,37 @@     , category = Dev     , cmdtype = ColonCmd     , action = inputToState @TopInfo . handleTypeCheck-    , parser = parseTypeCheck+    , parser = TypeCheck <$> parseTermOrOp     } +maxInferredTypes :: Int+maxInferredTypes = 16+ handleTypeCheck ::   Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>   REPLExpr 'CTypeCheck ->   Sem r () handleTypeCheck (TypeCheck t) = do-  (_, sig) <- typecheckTop $ inferTop t-  info $ pretty' t <+> text ":" <+> pretty' sig+  asigs <- typecheckTop $ inferTop maxInferredTypes t+  sigs <- runFresh . mapInput (view (replModInfo . miTydefs)) $ thin $ NE.map snd asigs+  let (toShow, extra) = NE.splitAt 8 sigs+  when (length sigs > 1) $ info "This expression has multiple possible types.  Some examples:"+  info $+    vcat $+      map (\sig -> pretty' t <+> text ":" <+> pretty' sig) toShow+        ++ ["..." | not (P.null extra)] -parseTypeCheck :: Parser (REPLExpr 'CTypeCheck)-parseTypeCheck =-  TypeCheck-    <$> ( (try term <?> "expression")-            <|> (parseNakedOp <?> "operator")-        )+------------------------------------------------------------ --- In a :type or :doc command, allow naked operators, as in :type + ,+-- In :type, :doc, or :table commands, allow naked operators, as in :type + , -- even though + by itself is not a syntactically valid term. -- However, this seems like it may be a common thing for a student to -- ask and there is no reason we can't have this as a special case.+parseTermOrOp :: Parser Term+parseTermOrOp =+  (try term <?> "expression")+    <|> (parseNakedOp <?> "operator")+ parseNakedOp :: Parser Term parseNakedOp = TPrim <$> parseNakedOpPrim 

@@ -1,10 +1,6 @@ {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -fmax-pmcheck-models=200 #-} -------------------------------------------------------------------------------------------------------------------------------------------------------------- -- | -- Module      :  Disco.Interpret.CESK -- Copyright   :  disco team and contributors@@ -18,6 +14,7 @@   runCESK,   step,   eval,+  evalApp,   runTest, ) where@@ -29,10 +26,13 @@ import Control.Arrow ((***), (>>>)) import Control.Monad ((>=>)) import Data.Bifunctor (first, second)+import Data.Functor (($>)) import Data.List (find)+import qualified Data.List.Infinite as InfList import qualified Data.Map as M import Data.Maybe (isJust) import Data.Ratio+import qualified Data.Text as T import Disco.AST.Core import Disco.AST.Generic (   Ellipsis (..),@@ -42,29 +42,30 @@ import Disco.AST.Typed (AProperty) import Disco.Compile import Disco.Context as Ctx+import Disco.Effects.Fresh+import Disco.Effects.Input import Disco.Enumerate import Disco.Error import Disco.Names import Disco.Property+import Disco.Syntax.Operators (BOp (..)) import Disco.Types hiding (V) import Disco.Value import Math.Combinatorics.Exact.Binomial (choose) import Math.Combinatorics.Exact.Factorial (factorial) import Math.NumberTheory.Primes (factorise, unPrime) import Math.NumberTheory.Primes.Testing (isPrime)---- import Math.OEIS (---   catalogNums,---   extendSequence,---   lookupSequence,---  )--import Disco.Effects.Fresh-import Disco.Effects.Input-import Disco.Effects.Random+import Math.OEIS (+  SearchStatus (SubSeq),+  extendSeq,+  lookupSeq,+  number,+ ) import Polysemy import Polysemy.Error+import Polysemy.Random import Polysemy.State+import qualified System.Random as R  ------------------------------------------------------------ -- Utilities@@ -114,6 +115,9 @@     FUpdate Int   | -- | Record the results of a test.     FTest TestVars Env+  | -- | Given the index of a memory cell and a function's arguments,+    --   memoize the results of a function.+    FMemo Int SimpleValue   deriving (Show)  ------------------------------------------------------------@@ -164,7 +168,7 @@   (In (CVar x) e k) -> case Ctx.lookup' x e of     Nothing -> return $ Up (UnboundError x) k     Just v -> return $ Out v k-  (In (CNum d r) _ k) -> return $ Out (VNum d r) k+  (In (CNum r) _ k) -> return $ Out (VNum r) k   (In (CConst OMatchErr) _ k) -> return $ Up NonExhaustive k   (In (CConst OEmptyGraph) _ k) -> return $ Out (VGraph empty) k   (In (CConst op) _ k) -> return $ Out (VConst op) k@@ -173,9 +177,13 @@   (In CUnit _ k) -> return $ Out VUnit k   (In (CPair c1 c2) e k) -> return $ In c1 e (FPairR e c2 : k)   (In (CProj s c) e k) -> return $ In c e (FProj s : k)-  (In (CAbs b) e k) -> do+  (In (CAbs mem b) e k) -> do     (xs, body) <- unbind b-    return $ Out (VClo e xs body) k+    case mem of+      Memo -> do+        cell <- allocateValue (VMap M.empty)+        return $ Out (VClo (Just (cell, [])) e xs body) k+      NoMemo -> return $ Out (VClo Nothing e xs body) k   (In (CApp c1 c2) e k) -> return $ In c1 e (FArg e c2 : k)   (In (CType ty) _ k) -> return $ Out (VType ty) k   (In (CDelay b) e k) -> do@@ -195,15 +203,23 @@   (Out v2 (FPairL v1 : k)) -> return $ Out (VPair v1 v2) k   (Out (VPair v1 v2) (FProj s : k)) -> return $ Out (selectSide s v1 v2) k   (Out v (FArg e c2 : k)) -> return $ In c2 e (FApp v : k)-  (Out v2 (FApp (VClo e [x] b) : k)) -> return $ In b (Ctx.insert (localName x) v2 e) k-  (Out v2 (FApp (VClo e (x : xs) b) : k)) -> return $ Out (VClo (Ctx.insert (localName x) v2 e) xs b) k+  (Out v (FMemo n sv : k)) -> memoSet n sv v $> Out v k+  (Out v (FApp (VClo mi e [x] b) : k)) -> case mi of+    Nothing -> return $ In b (Ctx.insert (localName x) v e) k+    Just (n, mem) -> do+      let sv = toSimpleValue $ foldr VPair VUnit (v : mem)+      mv <- memoLookup n sv+      case mv of+        Nothing -> return $ In b (Ctx.insert (localName x) v e) (FMemo n sv : k)+        Just v' -> return $ Out v' k+  (Out v (FApp (VClo mi e (x : xs) b) : k)) -> return $ Out (VClo (second (v :) <$> mi) (Ctx.insert (localName x) v e) xs b) k   (Out v2 (FApp (VConst op) : k)) -> appConst k op v2   (Out v2 (FApp (VFun f) : k)) -> return $ Out (f v2) k   -- Annoying to repeat this code, not sure of a better way.   -- The usual evaluation order (function then argument) doesn't work when   -- we're applying a test function to randomly generated values.-  (Out (VClo e [x] b) (FArgV v : k)) -> return $ In b (Ctx.insert (localName x) v e) k-  (Out (VClo e (x : xs) b) (FArgV v : k)) -> return $ Out (VClo (Ctx.insert (localName x) v e) xs b) k+  (Out (VClo _ e [x] b) (FArgV v : k)) -> return $ In b (Ctx.insert (localName x) v e) k+  (Out (VClo mi e (x : xs) b) (FArgV v : k)) -> return $ Out (VClo mi (Ctx.insert (localName x) v e) xs b) k   (Out (VConst op) (FArgV v : k)) -> appConst k op v   (Out (VFun f) (FArgV v : k)) -> return $ Out (f v) k   (Out (VRef n) (FForce : k)) -> do@@ -268,23 +284,23 @@     divOp :: Member (Error EvalError) r => Rational -> Rational -> Sem r Value     divOp _ 0 = throw DivByZero     divOp m n = return $ ratv (m / n)-  OExp -> numOp2 (\m n -> m ^^ numerator n) >=> out+  OExp -> numOp2' expOp >>> outWithErr+   where+    expOp :: Member (Error EvalError) r => Rational -> Rational -> Sem r Value+    expOp m n+      | m == 0 && n < 0 = throw DivByZero+      | otherwise = return $ ratv (m ^^ numerator n)   OMod -> numOp2' modOp >>> outWithErr    where     modOp :: Member (Error EvalError) r => Rational -> Rational -> Sem r Value     modOp m n       | n == 0 = throw DivByZero       | otherwise = return $ intv (numerator m `mod` numerator n)-  ODivides -> numOp2' (\m n -> return (enumv $ divides m n)) >=> out-   where-    divides 0 0 = True-    divides 0 _ = False-    divides x y = denominator (y / x) == 1-+  ODivides -> numOp2' (\m n -> return (boolv $ divides m n)) >=> out   --------------------------------------------------   -- Number theory -  OIsPrime -> intOp1 (enumv . isPrime) >=> out+  OIsPrime -> intOp1 (boolv . isPrime) >=> out   OFactor -> intOp1' primFactor >>> outWithErr    where     -- Semantics of the @$factor@ prim: turn a natural number into its@@ -336,13 +352,13 @@   -- Sequences    OUntil -> arity2 $ \v1 -> out . ellipsis (Until v1)-  -- OLookupSeq -> out . oeisLookup-  -- OExtendSeq -> out . oeisExtend+  OLookupSeq -> out . oeisLookup+  OExtendSeq -> out . oeisExtend   --------------------------------------------------   -- Comparison -  OEq -> arity2 $ \v1 v2 -> out $ enumv (valEq v1 v2)-  OLt -> arity2 $ \v1 v2 -> out $ enumv (valLt v1 v2)+  OEq -> arity2 $ \v1 v2 -> out $ boolv (valEq v1 v2)+  OLt -> arity2 $ \v1 v2 -> out $ boolv (valLt v1 v2)   --------------------------------------------------   -- Container operations @@ -356,8 +372,8 @@     cons n (x, k') (zs, m) = ((x, k') : zs, choose n k' * m)   OBagElem -> arity2 $ \x ->     withBag OBagElem $-      out . enumv . isJust . find (valEq x) . map fst-  OListElem -> arity2 $ \x -> out . enumv . isJust . find (valEq x) . vlist id+      out . boolv . isJust . find (valEq x) . map fst+  OListElem -> arity2 $ \x -> out . boolv . isJust . find (valEq x) . vlist id   OEachSet -> arity2 $ \f ->     withBag OEachSet $       outWithErr . fmap (VBag . countValues) . mapM (evalApp f . (: []) . fst)@@ -425,7 +441,13 @@       out . toMaybe . M.lookup (toSimpleValue k')    where     toMaybe = maybe (VInj L VUnit) (VInj R)+  --------------------------------------------------+  -- Randomness +  ORandom -> arity2 . flip $ \g -> arity2 $ \v1 v2 ->+    let (a, g') = R.randomR (vint v1, vint v2) (vgen g)+     in out $ VPair (intv a) (genv g')+  OSeed -> out . VGen . (R.mkStdGen . fromIntegral . vint)   --------------------------------------------------   -- Graph operations @@ -442,10 +464,8 @@   OExists tys -> out . (\v -> VProp (VPSearch SMExists tys v emptyTestEnv))   OHolds -> testProperty Exhaustive >=> resultToBool >>> outWithErr   ONotProp -> out . VProp . notProp . ensureProp-  OShouldEq ty -> arity2 $ \v1 v2 ->-    out $ VProp (VPDone (TestResult (valEq v1 v2) (TestEqual ty v1 v2) emptyTestEnv))-  OShouldLt ty -> arity2 $ \v1 v2 ->-    out $ VProp (VPDone (TestResult (valLt v1 v2) (TestLt ty v1 v2) emptyTestEnv))+  OShould op ty -> arity2 $ \v1 v2 ->+    out $ VProp (VPDone (TestResult (valOp op v1 v2) (TestCmp op ty v1 v2) emptyTestEnv))   OAnd -> arity2 $ \p1 p2 ->     out $ VProp (VPBin LAnd (ensureProp p1) (ensureProp p2))   OOr -> arity2 $ \p1 p2 ->@@ -493,7 +513,7 @@ numOp1 f = numOp1' $ return . ratv . f  numOp1' :: (Rational -> Sem r Value) -> Value -> Sem r Value-numOp1' f (VNum _ m) = f m+numOp1' f (VNum m) = f m numOp1' _ v = error $ "Impossible! numOp1' on non-VNum " ++ show v  numOp2 :: (Rational -> Rational -> Rational) -> Value -> Sem r Value@@ -502,11 +522,7 @@ numOp2' :: (Rational -> Rational -> Sem r Value) -> Value -> Sem r Value numOp2' (#) =   arity2 $ \v1 v2 -> case (v1, v2) of-    (VNum d1 n1, VNum d2 n2) -> do-      res <- n1 # n2-      case res of-        VNum _ r -> return $ VNum (d1 <> d2) r-        _ -> return res+    (VNum n1, VNum n2) -> n1 # n2     (VNum {}, _) -> error $ "Impossible! numOp2' on non-VNum " ++ show v2     _ -> error $ "Impossible! numOp2' on non-VNum " ++ show v1 @@ -525,9 +541,9 @@       (lowerRoot, lowerN) =         last $ takeWhile ((n >=) . snd) $ zip (1 : twopows) twopows       newtonStep x = div (x + div n x) 2-      iters = iterate newtonStep (integerSqrt' (div n lowerN) * lowerRoot)+      iters = InfList.iterate' newtonStep (integerSqrt' (div n lowerN) * lowerRoot)       isRoot r = r ^! 2 <= n && n < (r + 1) ^! 2-   in head $ dropWhile (not . isRoot) iters+   in InfList.head $ InfList.dropWhile (not . isRoot) iters  -- this operator is used for `integerSqrt'` (^!) :: Num a => a -> Int -> a@@ -537,14 +553,32 @@ -- Comparison ------------------------------------------------------------ -valEq :: Value -> Value -> Bool-valEq v1 v2 = valCmp v1 v2 == EQ+valEq, valLt :: Value -> Value -> Bool+valEq = valOp Eq+valLt = valOp Lt -valLt :: Value -> Value -> Bool-valLt v1 v2 = valCmp v1 v2 == LT+valOp :: BOp -> Value -> Value -> Bool+valOp op v1 v2 = case op of+  Eq -> valCmp v1 v2 == EQ+  Neq -> valCmp v1 v2 /= EQ+  Lt -> valCmp v1 v2 == LT+  Gt -> valCmp v1 v2 == GT+  Leq -> valCmp v1 v2 /= GT+  Geq -> valCmp v1 v2 /= LT+  Divides -> valDivides v1 v2+  _ -> False +valDivides :: Value -> Value -> Bool+valDivides (VNum r1) (VNum r2) = divides r1 r2+valDivides _ _ = False++divides :: Rational -> Rational -> Bool+divides 0 0 = True+divides 0 _ = False+divides x y = denominator (y / x) == 1+ valCmp :: Value -> Value -> Ordering-valCmp (VNum _ r1) (VNum _ r2) = compare r1 r2+valCmp (VNum r1) (VNum r2) = compare r1 r2 valCmp (VInj L _) (VInj R _) = LT valCmp (VInj R _) (VInj L _) = GT valCmp (VInj L v1) (VInj L v2) = valCmp v1 v2@@ -602,7 +636,7 @@ -- | Compute the forward difference of the given sequence, that is, --   differences of consecutive pairs of elements. diff :: Num a => [a] -> [a]-diff xs = zipWith (-) (tail xs) xs+diff xs = zipWith (-) (drop 1 xs) xs  -- | Take forward differences until the result is constant, and return --   the constant.  The sign of the constant difference tells us the@@ -617,23 +651,19 @@ -- OEIS ------------------------------------------------------------ --- -- | Looks up a sequence of integers in OEIS.--- --   Returns 'left()' if the sequence is unknown in OEIS,--- --   otherwise 'right "https://oeis.org/<oeis_sequence_id>"'--- oeisLookup :: Value -> Value--- oeisLookup (vlist vint -> ns) = maybe VNil parseResult (lookupSequence ns)---  where---   parseResult r = VInj R (listv charv ("https://oeis.org/" ++ seqNum r))---   seqNum = getCatalogNum . catalogNums----   getCatalogNum [] = error "No catalog info"---   getCatalogNum (n : _) = n+-- | Looks up a sequence of integers in OEIS.+--   Returns 'left()' if the sequence is unknown in OEIS,+--   otherwise 'right "https://oeis.org/<oeis_sequence_id>"'+oeisLookup :: Value -> Value+oeisLookup (vlist vint -> ns) = maybe VNil parseResult (lookupSeq (SubSeq ns))+ where+  parseResult r = VInj R (listv charv ("https://oeis.org/" ++ T.unpack (number r))) --- -- | Extends a Disco integer list with data from a known OEIS--- --   sequence.  Returns a list of integers upon success, otherwise the--- --   original list (unmodified).--- oeisExtend :: Value -> Value--- oeisExtend = listv intv . extendSequence . vlist vint+-- | Extends a Disco integer list with data from a known OEIS+--   sequence.  Returns a list of integers upon success, otherwise the+--   original list (unmodified).+oeisExtend :: Value -> Value+oeisExtend = listv intv . extendSeq . vlist vint  ------------------------------------------------------------ -- Normalizing bags/sets@@ -702,8 +732,8 @@   mergeCons a m1 m2 zs = do     nm <- evalApp g [VPair (intv m1) (intv m2)]     return $ case nm of-      VNum _ 0 -> zs-      VNum _ n -> (a, numerator n) : zs+      VNum 0 -> zs+      VNum n -> (a, numerator n) : zs       v -> error $ "Impossible! merge function in mergeM returned non-VNum " ++ show v  ------------------------------------------------------------@@ -727,7 +757,7 @@  resultToBool :: Member (Error EvalError) r => TestResult -> Sem r Value resultToBool (TestResult _ (TestRuntimeError e) _) = throw e-resultToBool (TestResult b _ _) = return $ enumv b+resultToBool (TestResult b _ _) = return $ boolv b  notProp :: ValProp -> ValProp notProp (VPDone r) = VPDone (invertPropResult r)@@ -743,8 +773,9 @@ ensureProp (VInj R _) = VPDone (TestResult True TestBool emptyTestEnv) ensureProp _ = error "ensureProp: non-prop value" -combineTestResultBool :: LOp -> TestResult -> TestResult -> Bool-combineTestResultBool op (TestResult b1 _ _) (TestResult b2 _ _) = interpLOp op b1 b2+combineTestResults :: LOp -> TestResult -> TestResult -> TestResult+combineTestResults op tr1@(TestResult b1 _ e1) tr2@(TestResult b2 _ e2) =+  TestResult (interpLOp op b1 b2) (TestBin op tr1 tr2) (mergeTestEnv e1 e2)  testProperty ::   Members '[Random, State Mem] r =>@@ -761,7 +792,7 @@   checkProp (VPBin op vp1 vp2) = do     tr1 <- checkProp vp1     tr2 <- checkProp vp2-    return $ TestResult (combineTestResultBool op tr1 tr2) (TestBin op tr1 tr2) emptyTestEnv+    return $ combineTestResults op tr1 tr2   checkProp (VPSearch sm tys f e) =     extendResultEnv e <$> (generateSamples initialSt vals >>= go)    where

@@ -1,10 +1,6 @@ {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE TemplateHaskell #-} -------------------------------------------------------------------------------------------------------------------------------------------------------------- -- | -- Module      :  Disco.Messages -- Copyright   :  disco team and contributors@@ -30,7 +26,7 @@   | Debug   deriving (Show, Read, Eq, Ord, Enum, Bounded) -data Message ann = Message {_messageType :: MessageType, _message :: (Doc ann)}+data Message ann = Message {_messageType :: MessageType, _message :: Doc ann}   deriving (Show)  makeLenses ''Message

@@ -4,10 +4,6 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE UndecidableInstances #-} -------------------------------------------------------------------------------------------------------------------------------------------------------------- -- | -- Module      :  Disco.Module -- Copyright   :  (c) 2019 disco team (see LICENSE)@@ -19,9 +15,6 @@ -- to resolve the location of a module on disk. module Disco.Module where -import Data.Data (Data)-import GHC.Generics (Generic)- import Control.Lens (   Getting,   foldOf,@@ -31,10 +24,14 @@ import Control.Monad (filterM) import Control.Monad.IO.Class (MonadIO (..)) import Data.Bifunctor (first)+import Data.Data (Data)+import Data.List.NonEmpty (NonEmpty)+import qualified Data.List.NonEmpty as NE import Data.Map (Map) import qualified Data.Map as M import Data.Maybe (listToMaybe) import qualified Data.Set as S+import GHC.Generics (Generic) import System.Directory (doesFileExist) import System.FilePath (   replaceExtension,@@ -84,14 +81,14 @@ --   @ -- --   might look like @Defn f [Z, Z*Z] B [clause 1 ..., clause 2 ...]@-data Defn = Defn (Name ATerm) [Type] Type [Clause]+data Defn = Defn (Name ATerm) [Type] Type (NonEmpty Clause)   deriving (Show, Generic, Alpha, Data, Subst Type)  instance Pretty Defn where   pretty (Defn x patTys ty clauses) =     vcat $       prettyTyDecl x (foldr (:->:) ty patTys)-        : map (pretty . (x,) . eraseClause) clauses+        : map (pretty . (x,) . eraseClause) (NE.toList clauses)  -- | A clause in a definition consists of a list of patterns (the LHS --   of the =) and a term (the RHS).  For example, given the concrete

@@ -1,5 +1,8 @@ {-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -fno-warn-unrecognised-pragmas #-} +{-# HLINT ignore "Functor law" #-}+ -- | -- Module      :  Disco.Parser -- Copyright   :  disco team and contributors@@ -81,25 +84,6 @@ ) where -import Unbound.Generics.LocallyNameless (-  Name,-  bind,-  embed,-  fvAny,-  name2String,-  string2Name,- )-import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)--import Control.Monad.Combinators.Expr-import Text.Megaparsec hiding (-  State,-  runParser,- )-import qualified Text.Megaparsec as MP-import Text.Megaparsec.Char-import qualified Text.Megaparsec.Char.Lexer as L- import Control.Lens (   makeLenses,   toListOf,@@ -109,16 +93,18 @@   (&),   (.=),  )-import Control.Monad.State+import Control.Monad (guard, void)+import Control.Monad.Combinators.Expr+import Control.Monad.State (State, StateT, evalState, evalStateT, gets, modify) import Data.Char (isAlpha, isDigit) import Data.Foldable (asum) import Data.List (find, intercalate)+import qualified Data.List.NonEmpty as NE import qualified Data.Map as M import Data.Maybe (fromMaybe, isNothing) import Data.Ratio import Data.Set (Set) import qualified Data.Set as S- import Disco.AST.Surface import Disco.Extensions import Disco.Module@@ -127,6 +113,22 @@ import Disco.Syntax.Prims import Disco.Types import Polysemy (run)+import Text.Megaparsec hiding (+  State,+  runParser,+ )+import qualified Text.Megaparsec as MP+import Text.Megaparsec.Char+import qualified Text.Megaparsec.Char.Lexer as L+import Unbound.Generics.LocallyNameless (+  Name,+  bind,+  embed,+  fvAny,+  name2String,+  string2Name,+ )+import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)  ------------------------------------------------------------ -- Lexer@@ -304,8 +306,8 @@ lambda :: Parser String lambda = symbol "\\" <|> symbol "λ" -forall :: Parser ()-forall = void (symbol "∀") <|> reserved "forall"+forAll :: Parser ()+forAll = void (symbol "∀") <|> reserved "forall"  exists :: Parser () exists = void (symbol "∃") <|> reserved "exists"@@ -345,7 +347,7 @@     -- either some digits optionally followed by bracketed digits...     (,) <$> some digit <*> optional (brackets (some digit))       -- ...or just bracketed digits.-      <|> ([],) <$> (Just <$> brackets (some digit))+      <|> (([],) . Just <$> brackets (some digit))    readDecimal a (b, mrep) =     read a % 1 -- integer part@@ -399,6 +401,8 @@   , "false"   , "True"   , "False"+  , "T"+  , "F"   , "let"   , "in"   , "is"@@ -411,8 +415,6 @@   , "choose"   , "implies"   , "iff"-  , "min"-  , "max"   , "union"   , "∪"   , "intersect"@@ -444,6 +446,7 @@   , "Set"   , "Graph"   , "Map"+  , "Gen"   , "N"   , "Z"   , "F"@@ -540,7 +543,9 @@   defnGroups [] = []   defnGroups (d@DType {} : ds) = d : defnGroups ds   defnGroups (d@DTyDef {} : ds) = d : defnGroups ds-  defnGroups (DDefn (TermDefn x bs) : ds) = DDefn (TermDefn x (bs ++ concatMap (\(TermDefn _ cs) -> cs) grp)) : defnGroups rest+  defnGroups (DDefn (TermDefn x bs) : ds) =+    DDefn (TermDefn x (bs `NE.appendList` concatMap (\(TermDefn _ cs) -> NE.toList cs) grp))+      : defnGroups rest    where     (grp, rest) = matchDefn ds     matchDefn :: [Decl] -> ([TermDefn], [Decl])@@ -648,7 +653,7 @@ parseDefn :: Parser TermDefn parseDefn =   label "definition" $-    (\(x, ps) body -> TermDefn x [bind ps body])+    (\(x, ps) body -> TermDefn x (NE.singleton (bind ps body)))       -- Only backtrack if we don't get a complete 'LHS ='.  Once we see       -- an = sign, commit to parsing a definition, because it can't be a       -- valid standalone expression anymore.  If the RHS fails, we don't@@ -695,8 +700,8 @@ parseAtom =   label "expression" $     parseUnit-      <|> TBool True <$ (reserved "true" <|> reserved "True")-      <|> TBool False <$ (reserved "false" <|> reserved "False")+      <|> TBool True <$ (reserved "true" <|> reserved "True" <|> reserved "T")+      <|> TBool False <$ (reserved "false" <|> reserved "False" <|> reserved "F")       <|> TChar <$> lexeme (between (char '\'') (char '\'') L.charLiteral)       <|> TString <$> lexeme (char '"' >> manyTill L.charLiteral (char '"'))       <|> TWild <$ try parseWild@@ -888,7 +893,7 @@ parseQuantifier :: Parser Quantifier parseQuantifier =   Lam <$ lambda-    <|> All <$ forall+    <|> All <$ forAll     <|> Ex <$ exists  -- | Parse a let expression (@let x1 = t1, x2 = t2, ... in t@).@@ -1204,6 +1209,7 @@       <|> TyZ <$ (reserved "Integer" <|> reserved "Int" <|> reserved "Z" <|> reserved "ℤ")       <|> TyF <$ (reserved "Fractional" <|> reserved "Frac" <|> reserved "F" <|> reserved "𝔽")       <|> TyQ <$ (reserved "Rational" <|> reserved "Q" <|> reserved "ℚ")+      <|> TyGen <$ reserved "Gen"       <|> TyCon <$> parseCon <*> (fromMaybe [] <$> optional (parens (parseType `sepBy1` comma)))       <|> TyVar <$> parseTyVar       <|> parens parseType@@ -1241,6 +1247,7 @@     [       [ infixR "*" (:*:)       , infixR "×" (:*:)+      , infixR "><" (:*:)       ]     ,       [ infixR "+" (:+:)

@@ -24,6 +24,8 @@  import Data.Bifunctor import Data.Char (isAlpha)+import Data.List.NonEmpty (NonEmpty)+import qualified Data.List.NonEmpty as NE import Data.Map (Map) import qualified Data.Map as M import Data.Ratio@@ -73,7 +75,7 @@ mparens :: Member (Reader PA) r => PA -> Sem r (Doc ann) -> Sem r (Doc ann) mparens pa doc = do   parentPA <- ask-  (if pa < parentPA then parens else id) doc+  (if pa `lowerPrec` parentPA then parens else id) doc  ------------------------------------------------------------ -- Pretty type class@@ -93,6 +95,9 @@ instance Pretty a => Pretty [a] where   pretty = brackets . intercalate "," . map pretty +instance Pretty a => Pretty (NonEmpty a) where+  pretty = pretty . NE.toList+ instance (Pretty k, Pretty v) => Pretty (Map k v) where   pretty m = do     let es = map (\(k, v) -> pretty k <+> "->" <+> pretty v) (M.assocs m)@@ -124,28 +129,38 @@ -- | Pretty-print a binary operator, by looking up its concrete syntax --   in the 'bopMap'. instance Pretty BOp where+  pretty (Should op) = pretty op <> "!"   pretty op = case M.lookup op bopMap of     Just (OpInfo _ (syn : _) _) -> text syn     _ -> error $ "BOp " ++ show op ++ " not in bopMap!"  ----------------------------------------------------- Pretty-printing decimals+-- Pretty-printing rationals + decimals +-- | Pretty-print a rational number as a fraction.+prettyRational :: Rational -> String+prettyRational r+  | denominator r == 1 = show (numerator r)+  | otherwise = show (numerator r) ++ "/" ++ show (denominator r)+ -- | Pretty-print a rational number using its decimal expansion, in --   the format @nnn.prefix[rep]...@, with any repeating digits enclosed --   in square brackets. prettyDecimal :: Rational -> String-prettyDecimal r = printedDecimal+prettyDecimal r = wholePart ++ "." ++ decimalPart  where-  (n, d) = properFraction r :: (Integer, Rational)+  (n', d') = properFraction r :: (Integer, Rational)+  d = abs d'+  n = abs n'   (expan, len) = digitalExpansion 10 (numerator d) (denominator d)-  printedDecimal+  wholePart = (if d' < 0 then "-" else "") ++ show n+  decimalPart     | length first102 > 101 || length first102 == 101 && last first102 /= 0 =-        show n ++ "." ++ concatMap show (take 100 expan) ++ "..."+        concatMap show (take 100 expan) ++ "..."     | rep == [0] =-        show n ++ "." ++ (if null pre then "0" else concatMap show pre)+        if null pre then "0" else concatMap show pre     | otherwise =-        show n ++ "." ++ concatMap show pre ++ "[" ++ concatMap show rep ++ "]"+        concatMap show pre ++ "[" ++ concatMap show rep ++ "]"    where     (pre, rep) = splitAt len expan     first102 = take 102 expan@@ -179,5 +194,5 @@ digitalExpansion b n d = digits  where   longDivStep (_, r) = (b * r) `divMod` d-  res = tail $ iterate longDivStep (0, n)+  res = drop 1 $ iterate longDivStep (0, n)   digits = first (map fst) (findRep res)

@@ -19,10 +19,26 @@ type Prec = Int  data PA = PA Prec BFixity-  deriving (Show, Eq)+  deriving (Show, Eq) -- Do NOT derive Ord, see note below. -instance Ord PA where-  compare (PA p1 a1) (PA p2 a2) = compare p1 p2 `mappend` (if a1 == a2 then EQ else LT)+lowerPrec :: PA -> PA -> Bool+lowerPrec (PA p1 a1) (PA p2 a2) = p1 < p2 || (p1 == p2 && a1 /= a2)++-- Note re: lowerPrec: we used to have an unlawful Ord instance defined by+--+--   compare (PA p1 a1) (PA p2 a2) = compare p1 p2 `mappend` (if a1 == a2 then EQ else LT)+--+-- with the idea that we could test whether one precedence was lower+-- than another simply using (<).+--+-- However, this was unlawful since e.g. it does not satisfy x < y ==+-- y > x: If x and y have the same Prec value but different BFixity+-- values, we would have both x < y and y < x.+--+-- In base-4.18 apparently something in the default implementations of+-- Ord methods changed so that e.g. not (PA 2 InR < PA 2 InL).  Hence+-- the 'mparens' method in such cases of nested same-precedence+-- operators was not emitting parentheses in cases where it should.  -- Standard precedence levels 

@@ -1,5 +1,3 @@------------------------------------------------------------------------------------------------------------------------------------------------------------ {-# LANGUAGE OverloadedStrings #-}  -- |@@ -28,7 +26,6 @@ import Data.Char (toLower) import qualified Data.Enumeration.Invertible as E -import Disco.Effects.Random import Polysemy  import Disco.AST.Typed@@ -40,6 +37,7 @@ import Disco.Typecheck.Erase (eraseProperty) import Disco.Types (TyDefCtx) import Disco.Value+import Polysemy.Random import Polysemy.Reader  -- | Toggles which outcome (finding or not finding the thing being@@ -52,7 +50,7 @@ --   the explanation unchanged. invertPropResult :: TestResult -> TestResult invertPropResult res@(TestResult b r env)-  | TestRuntimeError _ <- r = res+  | TestRuntimeError {} <- r = res   | otherwise = TestResult (not b) r env  randomLarge :: Member Random r => [Integer] -> Sem r [Integer]@@ -88,44 +86,38 @@   Bool ->   AProperty ->   TestReason ->+  TestEnv ->   Sem r (Doc ann)-prettyTestReason _ _ TestBool = empty-prettyTestReason b _ (TestFound (TestResult _ _ env))-  | b = prettyTestEnv "Found example:" env-  | not b = prettyTestEnv "Found counterexample:" env-prettyTestReason b _ (TestNotFound Exhaustive)+prettyTestReason _ _ TestBool _ = empty+prettyTestReason b (ATAbs _ _ body) (TestFound (TestResult b' r' env')) env = do+  lunbind body $ \(_, p) ->+    prettyTestEnv ("Found " ++ if b then "example:" else "counterexample:") env+      $+$ prettyTestReason b' p r' env'+prettyTestReason b _ (TestNotFound Exhaustive) _   | b = "No counterexamples exist; all possible values were checked."-  | not b = "No example exists; all possible values were checked."-prettyTestReason b _ (TestNotFound (Randomized n m))+  | otherwise = "No example exists; all possible values were checked."+prettyTestReason b _ (TestNotFound (Randomized n m)) _   | b = "Checked" <+> text (show (n + m)) <+> "possibilities without finding a counterexample."-  | not b = "No example was found; checked" <+> text (show (n + m)) <+> "possibilities."-prettyTestReason _ _ (TestEqual t a1 a2) =-  bulletList-    "-"-    [ "Left side:  " <> prettyValue t a1-    , "Right side: " <> prettyValue t a2-    ]-prettyTestReason _ _ (TestLt t a1 a2) =+  | otherwise = "No example was found; checked" <+> text (show (n + m)) <+> "possibilities."+prettyTestReason _ _ (TestCmp _ t a1 a2) _ =   bulletList     "-"     [ "Left side:  " <> prettyValue t a1     , "Right side: " <> prettyValue t a2     ]-prettyTestReason _ _ (TestRuntimeError ee) =+prettyTestReason _ _ (TestRuntimeError ee) env =   nest 2 $     "Test failed with an error:"       $+$ pretty (EvalErr ee)--- \$+$--- prettyTestEnv "Example inputs that caused the error:" env--- See #364-prettyTestReason b (ATApp _ (ATPrim _ (PrimBOp _)) (ATTup _ [p1, p2])) (TestBin _ tr1 tr2) =+      $+$ prettyTestEnv "Example inputs that caused the error:" env+prettyTestReason _ (ATApp _ (ATPrim _ (PrimBOp _)) (ATTup _ [p1, p2])) (TestBin _ tr1 tr2) _ =   bulletList     "-"-    [ nest 2 $ "Left side:" $+$ prettyTestResult' b p1 tr1-    , nest 2 $ "Right side:" $+$ prettyTestResult' b p2 tr2+    [ nest 2 $ prettyTestResult p1 tr1+    , nest 2 $ prettyTestResult p2 tr2     ] -- See Note [prettyTestReason fallback]-prettyTestReason _ _ _ = empty+prettyTestReason _ _ _ _ = empty  -- ~~~~ Note [prettyTestReason fallback] --@@ -147,22 +139,14 @@ -- of the test result.  So we just give up and decline to print a -- reason. -prettyTestResult' ::-  Members '[Input TyDefCtx, LFresh, Reader PA] r =>-  Bool ->-  AProperty ->-  TestResult ->-  Sem r (Doc ann)-prettyTestResult' _ prop (TestResult bool tr _) =-  prettyResultCertainty tr prop (map toLower (show bool))-    $+$ prettyTestReason bool prop tr- prettyTestResult ::   Members '[Input TyDefCtx, LFresh, Reader PA] r =>   AProperty ->   TestResult ->   Sem r (Doc ann)-prettyTestResult prop (TestResult b r env) = prettyTestResult' b prop (TestResult b r env)+prettyTestResult prop (TestResult bool tr env) =+  prettyResultCertainty tr prop (map toLower (show bool))+    $+$ prettyTestReason bool prop tr env  prettyTestEnv ::   Members '[Input TyDefCtx, LFresh, Reader PA] r =>

@@ -1,9 +1,5 @@ {-# LANGUAGE OverloadedStrings #-} -------------------------------------------------------------------------------------------------------------------------------------------------------------- -- SPDX-License-Identifier: BSD-3-Clause  -- |@@ -98,7 +94,7 @@ --   As one would expect, composition is associative and has 'idS' as --   its identity. (@@) :: Subst a a => Substitution a -> Substitution a -> Substitution a-(Substitution s1) @@ (Substitution s2) = Substitution ((M.map (applySubst (Substitution s1))) s2 `M.union` s1)+(Substitution s1) @@ (Substitution s2) = Substitution $ M.map (applySubst (Substitution s1)) s2 `M.union` s1  -- | Compose a whole container of substitutions.  For example, --   @compose [s1, s2, s3] = s1 \@\@ s2 \@\@ s3@.

@@ -1,10 +1,6 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} -------------------------------------------------------------------------------------------------------------------------------------------------------------- -- SPDX-License-Identifier: BSD-3-Clause  -- |@@ -30,6 +26,7 @@   opTable,   uopMap,   bopMap,+  opNames,   uPrec,   bPrec,   assoc,@@ -40,6 +37,7 @@ import GHC.Generics (Generic) import Unbound.Generics.LocallyNameless +import Data.Char (isAlpha) import Data.Map (Map, (!)) import qualified Data.Map as M @@ -85,10 +83,6 @@     Leq   | -- | Greater than or equal (@>=@)     Geq-  | -- | Minimum (@min@)-    Min-  | -- | Maximum (@max@)-    Max   | -- | Logical and (@&&@ / @and@)     And   | -- | Logical or (@||@ / @or@)@@ -117,10 +111,8 @@     Elem   | -- | Subset test (@⊆@)     Subset-  | -- | Equality assertion (@=!=@)-    ShouldEq-  | -- | Less than assertion (@!<@)-    ShouldLt+  | -- | Make a binary boolean operator into a testable proposition+    Should BOp   deriving (Show, Read, Eq, Ord, Generic, Data, Alpha, Subst t)  -- | Type operators.@@ -205,10 +197,6 @@       , bopInfo InL Diff ["\\"]       ]     ,-      [ bopInfo InL Min ["min"]-      , bopInfo InL Max ["max"]-      ]-    ,       [ bopInfo InL Mul ["*"]       , bopInfo InL Div ["/"]       , bopInfo InL Mod ["mod", "%"]@@ -224,8 +212,6 @@       ]     ,       [ bopInfo InR Eq ["=="]-      , bopInfo InR ShouldEq ["=!="]-      , bopInfo InR ShouldLt ["!<"]       , bopInfo InR Neq ["/=", "≠", "!="]       , bopInfo InR Lt ["<"]       , bopInfo InR Gt [">"]@@ -268,16 +254,23 @@   M.fromList $     [(op, info) | opLevel <- opTable, info@(OpInfo (BOpF _ op) _ _) <- opLevel] +opNames :: [String]+opNames = [syn | OpInfo _ syns _ <- concat opTable, syn <- filter (all isAlpha) syns]+ -- | A convenient function for looking up the precedence of a unary operator. uPrec :: UOp -> Int uPrec = opPrec . (uopMap !)  -- | A convenient function for looking up the precedence of a binary operator. bPrec :: BOp -> Int-bPrec = opPrec . (bopMap !)+bPrec (Should op) = bPrec op+bPrec op = case M.lookup op bopMap of+  Just (OpInfo _ _ p) -> p+  _ -> error $ "BOp " ++ show op ++ " not in bopMap!"  -- | Look up the \"fixity\" (/i.e./ associativity) of a binary operator. assoc :: BOp -> BFixity+assoc (Should op) = assoc op assoc op =   case M.lookup op bopMap of     Just (OpInfo (BOpF fx _) _ _) -> fx

@@ -37,120 +37,89 @@  -- | Primitives, /i.e./ built-in constants. data Prim where-  PrimUOp ::-    UOp ->-    -- | Unary operator-    Prim-  PrimBOp ::-    BOp ->-    -- | Binary operator-    Prim-  PrimLeft ::-    -- | Left injection into a sum type.-    Prim-  PrimRight ::-    -- | Right injection into a sum type.-    Prim-  PrimSqrt ::-    -- | Integer square root (@sqrt@)-    Prim-  PrimFloor ::-    -- | Floor of fractional type (@floor@)-    Prim-  PrimCeil ::-    -- | Ceiling of fractional type (@ceiling@)-    Prim-  PrimAbs ::-    -- | Absolute value (@abs@)-    Prim-  PrimPower ::-    -- | Power set (XXX or bag?)-    Prim-  PrimList ::-    -- | Container -> list conversion-    Prim-  PrimBag ::-    -- | Container -> bag conversion-    Prim-  PrimSet ::-    -- | Container -> set conversion-    Prim-  PrimB2C ::-    -- | bag -> set of counts conversion-    Prim-  PrimC2B ::-    -- | set of counts -> bag conversion-    Prim-  PrimUC2B ::-    -- | unsafe set of counts -> bag conversion-    --   that assumes all distinct-    Prim-  PrimMapToSet ::-    -- | Map k v -> Set (k × v)-    Prim-  PrimSetToMap ::-    -- | Set (k × v) -> Map k v-    Prim-  PrimSummary ::-    -- | Get Adjacency list of Graph-    Prim-  PrimVertex ::-    -- | Construct a graph Vertex-    Prim-  PrimEmptyGraph ::-    -- | Empty graph-    Prim-  PrimOverlay ::-    -- | Overlay two Graphs-    Prim-  PrimConnect ::-    -- | Connect Graph to another with directed edges-    Prim-  PrimInsert ::-    -- | Insert into map-    Prim-  PrimLookup ::-    -- | Get value associated with key in map-    Prim-  PrimEach ::-    -- | Each operation for containers-    Prim-  PrimReduce ::-    -- | Reduce operation for containers-    Prim-  PrimFilter ::-    -- | Filter operation for containers-    Prim-  PrimJoin ::-    -- | Monadic join for containers-    Prim-  PrimMerge ::-    -- | Generic merge operation for bags/sets-    Prim-  PrimIsPrime ::-    -- | Efficient primality test-    Prim-  PrimFactor ::-    -- | Factorization-    Prim-  PrimFrac ::-    -- | Turn a rational into a pair (num, denom)-    Prim-  PrimCrash ::-    -- | Crash-    Prim-  PrimUntil ::-    -- | @[x, y, z .. e]@-    Prim-  PrimHolds ::-    -- | Test whether a proposition holds-    Prim-  PrimLookupSeq ::-    -- | Lookup OEIS sequence-    Prim-  PrimExtendSeq ::-    -- | Extend OEIS sequence-    Prim+  -- | Unary operator+  PrimUOp :: UOp -> Prim+  -- | Binary operator+  PrimBOp :: BOp -> Prim+  -- | Left injection into a sum type.+  PrimLeft :: Prim+  -- | Right injection into a sum type.+  PrimRight :: Prim+  -- | Integer square root (@sqrt@)+  PrimSqrt :: Prim+  -- | Floor of fractional type (@floor@)+  PrimFloor :: Prim+  -- | Ceiling of fractional type (@ceiling@)+  PrimCeil :: Prim+  -- | Absolute value (@abs@)+  PrimAbs :: Prim+  -- | Min+  PrimMin :: Prim+  -- | Max+  PrimMax :: Prim+  -- | Power set (XXX or bag?)+  PrimPower :: Prim+  -- | Container -> list conversion+  PrimList :: Prim+  -- | Container -> bag conversion+  PrimBag :: Prim+  -- | Container -> set conversion+  PrimSet :: Prim+  -- | bag -> set of counts conversion+  PrimB2C :: Prim+  -- | set of counts -> bag conversion+  PrimC2B :: Prim+  -- | unsafe set of counts -> bag conversion+  --   that assumes all distinct+  PrimUC2B :: Prim+  -- | Map k v -> Set (k × v)+  PrimMapToSet :: Prim+  -- | Set (k × v) -> Map k v+  PrimSetToMap :: Prim+  -- | Get Adjacency list of Graph+  PrimSummary :: Prim+  -- | Construct a graph Vertex+  PrimVertex :: Prim+  -- | Empty graph+  PrimEmptyGraph :: Prim+  -- | Overlay two Graphs+  PrimOverlay :: Prim+  -- | Connect Graph to another with directed edges+  PrimConnect :: Prim+  -- | Insert into map+  PrimInsert :: Prim+  -- | Get value associated with key in map+  PrimLookup :: Prim+  -- | Each operation for containers+  PrimEach :: Prim+  -- | Reduce operation for containers+  PrimReduce :: Prim+  -- | Filter operation for containers+  PrimFilter :: Prim+  -- | Monadic join for containers+  PrimJoin :: Prim+  -- | Generic merge operation for bags/sets+  PrimMerge :: Prim+  -- | Efficient primality test+  PrimIsPrime :: Prim+  -- | Factorization+  PrimFactor :: Prim+  -- | Turn a rational into a pair (num, denom)+  PrimFrac :: Prim+  -- | Crash+  PrimCrash :: Prim+  -- | @[x, y, z .. e]@+  PrimUntil :: Prim+  -- | Test whether a proposition holds+  PrimHolds :: Prim+  -- | Lookup OEIS sequence+  PrimLookupSeq :: Prim+  -- | Extend OEIS sequence+  PrimExtendSeq :: Prim+  -- | Generates a pseudorandom number generator+  PrimSeed :: Prim+  -- | Given a range and a generator, generates random number+  PrimRandom :: Prim   deriving (Show, Read, Eq, Ord, Generic, Alpha, Subst t, Data)  ------------------------------------------------------------@@ -192,6 +161,8 @@   , PrimInfo PrimFloor "floor" True   , PrimInfo PrimCeil "ceiling" True   , PrimInfo PrimAbs "abs" True+  , PrimInfo PrimMin "min" True+  , PrimInfo PrimMax "max" True   , PrimInfo PrimPower "power" True   , PrimInfo PrimList "list" True   , PrimInfo PrimBag "bag" True@@ -221,6 +192,8 @@   , PrimInfo PrimHolds "holds" True   , PrimInfo PrimLookupSeq "lookupSequence" False   , PrimInfo PrimExtendSeq "extendSequence" False+  , PrimInfo PrimSeed "seed" True+  , PrimInfo PrimRandom "random" True   ]  -- | Find any exposed prims with the given name.

@@ -2,10 +2,6 @@ {-# LANGUAGE NondecreasingIndentation #-} {-# LANGUAGE OverloadedStrings #-} -------------------------------------------------------------------------------------------------------------------------------------------------------------- -- | -- Module      :  Disco.Typecheck -- Copyright   :  disco team and contributors@@ -19,43 +15,24 @@  import Control.Arrow ((&&&)) import Control.Lens ((^..))-import Control.Monad.Except+import Control.Monad (filterM, forM_, replicateM, unless, when, zipWithM) import Control.Monad.Trans.Maybe import Data.Bifunctor (first) import Data.Coerce import qualified Data.Foldable as F-import Data.List (group, sort)+import Data.List (sort)+import Data.List.NonEmpty (NonEmpty (..))+import qualified Data.List.NonEmpty as NE import Data.Map (Map) import qualified Data.Map as M import Data.Maybe (isJust) import Data.Set (Set) import qualified Data.Set as S-import Prelude as P hiding (lookup)--import Unbound.Generics.LocallyNameless (-  Alpha,-  Bind,-  Name,-  bind,-  embed,-  name2String,-  string2Name,-  substs,-  unembed,- )-import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)--import Disco.Effects.Fresh-import Polysemy hiding (embed)-import Polysemy.Error-import Polysemy.Output-import Polysemy.Reader-import Polysemy.Writer- import Disco.AST.Surface import Disco.AST.Typed import Disco.Context hiding (filter) import qualified Disco.Context as Ctx+import Disco.Effects.Fresh import Disco.Messages import Disco.Module import Disco.Names@@ -64,9 +41,31 @@ import Disco.Syntax.Operators import Disco.Syntax.Prims import Disco.Typecheck.Constraints+import Disco.Typecheck.Solve (SolutionLimit (..), solveConstraint) import Disco.Typecheck.Util import Disco.Types import Disco.Types.Rules+import Polysemy hiding (embed)+import Polysemy.Error+import Polysemy.Input+import Polysemy.Output+import Polysemy.Reader+import Polysemy.State (evalState)+import Polysemy.Writer+import Text.EditDistance (defaultEditCosts, restrictedDamerauLevenshteinDistance)+import Unbound.Generics.LocallyNameless (+  Alpha,+  Bind,+  Name,+  bind,+  embed,+  name2String,+  string2Name,+  substs,+  unembed,+ )+import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)+import Prelude as P hiding (lookup)  ------------------------------------------------------------ -- Container utilities@@ -105,6 +104,13 @@       return (tyb : tybs, ctx <> ctx')  ------------------------------------------------------------+-- Variable name utilities+------------------------------------------------------------++suggestionsFrom :: String -> [String] -> [String]+suggestionsFrom x = filter ((<= 1) . restrictedDamerauLevenshteinDistance defaultEditCosts x)++------------------------------------------------------------ -- Modules ------------------------------------------------------------ @@ -138,7 +144,7 @@         (x : _) -> throw $ noLoc $ DuplicateDefns (coerce x)         [] -> do           aprops <- mapError noLoc $ checkProperties docCtx -- XXX location?-          aterms <- mapError noLoc $ mapM inferTop terms -- XXX location?+          aterms <- mapError noLoc $ mapM inferTop1 terms -- XXX location?           return $ ModuleInfo name imports (map ((name .-) . getDeclName) typeDecls) docCtx aprops tyCtx tyDefnCtx defnCtx aterms es  where   getDefnName :: Defn -> Name ATerm@@ -214,8 +220,11 @@ checkUnboundVars (TypeDefn _ args body) = go body  where   go (TyAtom (AVar (U x)))-    | name2String x `elem` args = return ()-    | otherwise = throw $ UnboundTyVar x+    | xn `elem` args = return ()+    | otherwise = throw $ UnboundTyVar x suggestions+   where+    xn = name2String x+    suggestions = suggestionsFrom xn args   go (TyAtom _) = return ()   go (TyUser name tys) = lookupTyDefn name tys >> mapM_ go tys   go (TyCon _ tys) = mapM_ go tys@@ -239,7 +248,7 @@ --   >>> filterDups [1,3,2,1,1,4,2] --   [1,2] filterDups :: Ord a => [a] -> [a]-filterDups = map head . filter ((> 1) . length) . group . sort+filterDups = map NE.head . filter ((> 1) . NE.length) . NE.group . sort  -------------------------------------------------- -- Type declarations@@ -273,6 +282,8 @@   TermDefn ->   Sem r Defn checkDefn name (TermDefn x clauses) = mapError (LocTCError (Just (name .- x))) $ do+  debug "======================================================================"+  debug "Checking definition:"   -- Check that all clauses have the same number of patterns   checkNumPats clauses @@ -285,26 +296,25 @@   -- Try to decompose the type into a chain of arrows like pty1 ->   -- pty2 -> pty3 -> ... -> bodyTy, according to the number of   -- patterns, and lazily unrolling type definitions along the way.-  (patTys, bodyTy) <- decomposeDefnTy (numPats (head clauses)) ty+  (patTys, bodyTy) <- decomposeDefnTy (numPats (NE.head clauses)) ty -  ((acs, _), theta) <- solve $ do+  ((acs, _), thetas) <- solve 1 $ do     aclauses <- forAll nms $ mapM (checkClause patTys bodyTy) clauses     return (aclauses, ty) -  return $ applySubst theta (Defn (coerce x) patTys bodyTy acs)+  return $ applySubst (NE.head thetas) (Defn (coerce x) patTys bodyTy acs)  where   numPats = length . fst . unsafeUnbind -  checkNumPats [] = return () -- This can't happen, but meh-  checkNumPats [_] = return ()-  checkNumPats (c : cs)+  checkNumPats (_ :| []) = return ()+  checkNumPats (c :| cs)     | all ((== 0) . numPats) (c : cs) = throw (DuplicateDefns x)     | not (all ((== numPats c) . numPats) cs) = throw NumPatterns     -- XXX more info, this error actually means # of     -- patterns don't match across different clauses     | otherwise = return () -  -- \| Check a clause of a definition against a list of pattern types and a body type.+  -- Check a clause of a definition against a list of pattern types and a body type.   checkClause ::     Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>     [Type] ->@@ -352,9 +362,12 @@   Property ->   Sem r AProperty checkProperty prop = do-  (at, theta) <- solve $ check prop TyProp+  debug "======================================================================"+  debug "Checking property:"+  debugPretty prop+  (at, thetas) <- solve 1 $ check prop TyProp   -- XXX do we need to default container variables here?-  return $ applySubst theta at+  return $ applySubst (NE.head thetas) at  ------------------------------------------------------------ -- Type checking/inference@@ -441,34 +454,87 @@   Sem r ATerm infer = typecheck Infer --- | Top-level type inference algorithm: infer a (polymorphic) type---   for a term by running type inference, solving the resulting---   constraints, and quantifying over any remaining type variables.-inferTop ::+-- | Top-level type inference algorithm, returning only the first+--   possible result.+inferTop1 ::   Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r =>   Term ->   Sem r (ATerm, PolyType)-inferTop t = do+inferTop1 t = NE.head <$> inferTop 1 t++-- | Top-level type inference algorithm: infer up to the requested max+--   number of possible (polymorphic) types for a term by running type+--   inference, solving the resulting constraints, and quantifying+--   over any remaining type variables.+inferTop ::+  Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r =>+  Int ->+  Term ->+  Sem r (NonEmpty (ATerm, PolyType))+inferTop lim t = do   -- Run inference on the term and try to solve the resulting   -- constraints.-  (at, theta) <- solve $ infer t+  debug "======================================================================"+  debug "Inferring the type of:"+  debugPretty t+  (at, thetas) <- solve lim $ infer t    debug "Final annotated term (before substitution and container monomorphizing):"   debugPretty at -  -- Apply the resulting substitution.-  let at' = applySubst theta at+  -- Currently the following code generates *every possible*+  -- combination of substitutions for container variables, which can+  -- lead to exponential blowup in some cases.  For example, inferring+  -- the type of+  --+  --   \x. \y. \z. (set(x), set(y), set(z))+  --+  -- takes a Very Long Time.  Potential solutions include:+  --+  --   1. Do something similar as in the 'solve' function, using a State SolutionLimit+  --      effect to stop early once we've generated enough variety.+  --+  --   2. Use a proper backtracking search monad like LogicT to scope+  --      over both the generation of solution substitutions *and*+  --      choosing container variable monomorphizations, then just+  --      take a limited number of solutions.  Unfortunately,+  --      polysemy's NonDet effect seems to be somewhat broken+  --      (https://stackoverflow.com/questions/62627695/running-the-nondet-effect-once-in-polysemy+  --      ; https://github.com/polysemy-research/polysemy/issues/246 )+  --      and using LogicT on top of Sem is going to be tedious since+  --      it would require calling 'lift' on almost everything.+  --+  --   3. Also, it is probably (?) the case that no matter which of+  --      the generated substitutions is used, the exact same+  --      container variables are still unconstrained in all of them.+  --      So we should be able to pick container variable+  --      monomorphizations independently of the substitutions from+  --      the solver.  Doing this would help though it would not+  --      address the fundamental issue. -      -- Find any remaining container variables.-      cvs = containerVars (getType at')+  -- Quantify over any remaining type variables and return+  -- the term along with the resulting polymorphic type.+  return $ do+    -- Monad NonEmpty -      -- Replace them all with List.-      at'' = applySubst (Subst.fromList $ zip (S.toList cvs) (repeat (TyAtom (ABase CtrList)))) at'+    -- Iterate over all possible solutions...+    theta <- thetas -  -- Finally, quantify over any remaining type variables and return-  -- the term along with the resulting polymorphic type.-  return (at'', closeType (getType at''))+    let -- Apply each one...+        at' = applySubst theta at +        -- Find any remaining container variables...+        cvs = containerVars (getType at')++    -- Build all possible substitutions for those container variables...+    ctrs <- replicateM (S.size cvs) (NE.map (TyAtom . ABase) (CtrList :| [CtrBag, CtrSet]))++    -- Substitute for the container variables...+    let at'' = applySubst (Subst.fromList $ zip (S.toList cvs) ctrs) at'++    -- Return the term along with its type, with all substitutions applied.+    return (at'', closeType (getType at''))+ -- | Top-level type checking algorithm: check that a term has a given --   polymorphic type by running type checking and solving the --   resulting constraints.@@ -478,8 +544,12 @@   PolyType ->   Sem r ATerm checkTop t ty = do-  (at, theta) <- solve $ checkPolyTy t ty-  return $ applySubst theta at+  debug "======================================================================"+  debug "Checking the type of:"+  debugPretty t+  debugPretty ty+  (at, theta) <- solve 1 $ checkPolyTy t ty+  return $ applySubst (NE.head theta) at  -------------------------------------------------- -- The typecheck function@@ -539,7 +609,10 @@   -- Pick the first method that succeeds; if none do, throw an unbound   -- variable error.   mt <- runMaybeT . F.asum . map MaybeT $ [tryLocal, tryModule, tryPrim]-  maybe (throw (Unbound x)) return mt+  ctx <- ask @TyCtx+  let inScope = map name2String (Ctx.names ctx) ++ opNames ++ [syn | PrimInfo _ syn _ <- M.elems primMap]+      suggestions = suggestionsFrom (name2String x) inScope+  maybe (throw $ Unbound x suggestions) return mt  where   -- 1. See if the variable name is bound locally.   tryLocal = do@@ -559,13 +632,13 @@         (_, ty) <- unbind sig         return . Just $ ATVar ty (m .- coerce x)       [] -> return Nothing-      _ -> throw $ Ambiguous x (map fst bs)+      _nonEmpty -> throw $ Ambiguous x (map fst bs)    -- 3. See if we should convert it to a primitive.   tryPrim =     case toPrim (name2String x) of       (prim : _) -> Just <$> typecheck Infer (TPrim prim)-      _ -> return Nothing+      [] -> return Nothing  -------------------------------------------------- -- Primitives@@ -722,7 +795,7 @@     c <- freshAtom     a <- freshTy     constraint $-      COr+      cOr         [ CEq (TyAtom (ABase CtrBag)) (TyAtom c)         , CEq (TyAtom (ABase CtrSet)) (TyAtom c)         ]@@ -737,7 +810,7 @@     a <- freshTy     c <- freshAtom     constraint $-      COr+      cOr         [ CEq (TyAtom (ABase CtrBag)) (TyAtom c)         , CEq (TyAtom (ABase CtrSet)) (TyAtom c)         ]@@ -761,6 +834,11 @@     return $ a :*: TyContainer c a :->: TyBool    ----------------------------------------+  -- Randomness++  inferPrim PrimRandom = return $ (TyN :*: TyN) :*: TyGen :->: (TyN :*: TyGen)+  inferPrim PrimSeed = return $ TyN :->: TyGen+  ----------------------------------------   -- Arithmetic    inferPrim (PrimBOp IDiv) = do@@ -816,7 +894,7 @@      -- b can be either Nat (a binomial coefficient)     -- or a list of Nat (a multinomial coefficient).-    constraint $ COr [CEq b TyN, CEq b (TyList TyN)]+    constraint $ cOr [CEq b TyN, CEq b (TyList TyN)]     return $ TyN :*: b :->: TyN    ----------------------------------------@@ -842,13 +920,9 @@    -- 'holds' converts a Prop into a Bool (but might not terminate).   inferPrim PrimHolds = return $ TyProp :->: TyBool-  -- An equality assertion =!= is just like a comparison ==, except+  -- An binary assertion is just like a comparison, except   -- the result is a Prop.-  inferPrim (PrimBOp ShouldEq) = do-    ty <- freshTy-    constraint $ CQual QCmp ty-    return $ ty :*: ty :->: TyProp-  inferPrim (PrimBOp ShouldLt) = do+  inferPrim (PrimBOp (Should _)) = do     ty <- freshTy     constraint $ CQual QCmp ty     return $ ty :*: ty :->: TyProp@@ -877,16 +951,6 @@   inferPrim (PrimBOp Geq) = error "inferPrim Geq should be unreachable"   ------------------------------------------------------------ -  inferPrim (PrimBOp op) | op `elem` [Min, Max] = do-    ty <- freshTy-    constraint $ CQual QCmp ty-    return $ ty :*: ty :->: ty--  -- See Note [Pattern coverage] ------------------------------  inferPrim (PrimBOp Min) = error "inferPrim Min should be unreachable"-  inferPrim (PrimBOp Max) = error "inferPrim Max should be unreachable"-  -------------------------------------------------------------   ----------------------------------------   -- Special arithmetic functions: fact, sqrt, floor, ceil, abs @@ -905,10 +969,22 @@   inferPrim PrimAbs = do     argTy <- freshTy     resTy <- freshTy-    cAbs argTy resTy `cOr` cSize argTy resTy+    cAbs argTy resTy `orElse` cSize argTy resTy     return $ argTy :->: resTy    ----------------------------------------+  -- min/max++  inferPrim PrimMin = do+    a <- freshTy+    constraint $ CQual QCmp a+    return $ (a :*: a) :->: a+  inferPrim PrimMax = do+    a <- freshTy+    constraint $ CQual QCmp a+    return $ (a :*: a) :->: a++  ----------------------------------------   -- power set/bag    inferPrim PrimPower = do@@ -917,7 +993,7 @@      constraint $ CQual QCmp a     constraint $-      COr+      cOr         [ CEq (TyAtom (ABase CtrSet)) (TyAtom c)         , CEq (TyAtom (ABase CtrBag)) (TyAtom c)         ]@@ -973,7 +1049,7 @@   -- Then check the type of the body under a context extended with   -- types for all the arguments.   extends ctx $-    ATAbs Lam checkTy <$> (bind (coerce typedArgs) <$> check t resTy)+    ATAbs Lam checkTy . bind (coerce typedArgs) <$> check t resTy  where   -- Given the patterns and their optional type annotations in the   -- head of a lambda (e.g.  @x (y:Z) (f : N -> N) -> ...@), and the@@ -1468,7 +1544,7 @@       -- Valid types for absolute value are Z -> N, Q -> F, or T -> T       -- (e.g. Z5 -> Z5).       constraint $-        COr+        cOr           [ cAnd [CSub ty TyZ, CSub TyN res]           , cAnd [CSub ty TyQ, CSub TyF res]           , CEq ty res@@ -1497,7 +1573,7 @@       -- Valid types for absolute value are F -> N, Q -> Z, or T -> T       -- (e.g. Z5 -> Z5).       constraint $-        COr+        cOr           [ cAnd [CSub ty TyF, CSub TyN res]           , cAnd [CSub ty TyQ, CSub TyZ res]           , CEq ty res@@ -1529,7 +1605,7 @@   -- to support multiplication, or else the exponent is Z, in which   -- case the result type also has to support division.   constraint $-    COr+    cOr       [ cAnd [CQual QNum resTy, CEq ty2 TyN]       , cAnd [CQual QDiv resTy, CEq ty2 TyZ]       ]@@ -1701,3 +1777,39 @@ ensureEq ty1 ty2   | ty1 == ty2 = return ()   | otherwise = constraint $ CEq ty1 ty2++------------------------------------------------------------+-- Subtyping+------------------------------------------------------------++isSubPolyType ::+  Members '[Input TyDefCtx, Output (Message ann), Fresh] r =>+  PolyType ->+  PolyType ->+  Sem r Bool+isSubPolyType (Forall b1) (Forall b2) = do+  (as1, ty1) <- unbind b1+  (as2, ty2) <- unbind b2+  let c = CAll (bind as1 (CSub ty1 (substs (zip as2 (map TyVar as1)) ty2)))+  debug "======================================================================"+  debug "Checking subtyping..."+  debugPretty (Forall b1)+  debugPretty (Forall b2)+  ss <- runError (evalState (SolutionLimit 1) (solveConstraint c))+  return (either (const False) (not . P.null) ss)++thin :: Members '[Input TyDefCtx, Output (Message ann), Fresh] r => NonEmpty PolyType -> Sem r (NonEmpty PolyType)+thin = fmap NE.fromList . thin' . NE.toList++-- Intuitively, this will always return a nonempty list given a nonempty list as input;+-- we could probably rewrite it in terms of NonEmpty combinators but it's more effort than+-- I cared to spend at the moment.+thin' :: Members '[Input TyDefCtx, Output (Message ann), Fresh] r => [PolyType] -> Sem r [PolyType]+thin' [] = return []+thin' (ty : tys) = do+  ss <- or <$> mapM (`isSubPolyType` ty) tys+  if ss+    then thin' tys+    else do+      tys' <- filterM (fmap not . (ty `isSubPolyType`)) tys+      (ty :) <$> thin' tys'

@@ -1,10 +1,6 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE OverloadedStrings #-} -------------------------------------------------------------------------------------------------------------------------------------------------------------- -- | -- Module      :  Disco.Typecheck.Constraints -- Copyright   :  disco team and contributors@@ -16,20 +12,20 @@ module Disco.Typecheck.Constraints (   Constraint (..),   cAnd,+  cOr, ) where +import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE import Data.Semigroup-import GHC.Generics (Generic)-import Unbound.Generics.LocallyNameless hiding (lunbind)- import Disco.Effects.LFresh- import Disco.Pretty hiding ((<>)) import Disco.Syntax.Operators (BFixity (In, InL, InR)) import Disco.Types import Disco.Types.Rules+import GHC.Generics (Generic)+import Unbound.Generics.LocallyNameless hiding (lunbind)  -- | Constraints are generated as a result of type inference and checking. --   These constraints are accumulated during the inference and checking phase@@ -38,9 +34,9 @@   CSub :: Type -> Type -> Constraint   CEq :: Type -> Type -> Constraint   CQual :: Qualifier -> Type -> Constraint-  CAnd :: [Constraint] -> Constraint+  CAnd :: NonEmpty Constraint -> Constraint   CTrue :: Constraint-  COr :: [Constraint] -> Constraint+  COr :: NonEmpty Constraint -> Constraint   CAll :: Bind [Name Type] Constraint -> Constraint   deriving (Show, Generic, Alpha, Subst Type) @@ -49,14 +45,10 @@     CSub ty1 ty2 -> withPA (PA 4 In) $ lt (pretty ty1) <+> "<:" <+> rt (pretty ty2)     CEq ty1 ty2 -> withPA (PA 4 In) $ lt (pretty ty1) <+> "=" <+> rt (pretty ty2)     CQual q ty -> withPA (PA 10 InL) $ lt (pretty q) <+> rt (pretty ty)-    CAnd [c] -> pretty c-    -- Use rt for both, since we don't need to print parens for /\ at all-    CAnd (c : cs) -> withPA (PA 3 InR) $ rt (pretty c) <+> "/\\" <+> rt (pretty (CAnd cs))-    CAnd [] -> "True"+    -- Use rt for everything, since we don't need to print parens for /\ at all+    CAnd cs -> withPA (PA 3 InR) $ foldr1 (\a b -> a <+> "/\\" <+> b) (NE.map (rt . pretty) cs)     CTrue -> "True"-    COr [c] -> pretty c-    COr (c : cs) -> withPA (PA 2 InR) $ lt (pretty c) <+> "\\/" <+> rt (pretty (COr cs))-    COr [] -> "False"+    COr cs -> withPA (PA 2 InR) $ foldr1 (\a b -> lt a <+> "\\/" <+> rt b) (NE.map pretty cs)     CAll b -> lunbind b $ \(xs, c) ->       "∀" <+> intercalate "," (map pretty xs) <> "." <+> pretty c @@ -65,10 +57,15 @@ cAnd cs = case filter nontrivial cs of   [] -> CTrue   [c] -> c-  cs' -> CAnd cs'+  (c : cs') -> CAnd (c :| cs')  where   nontrivial CTrue = False   nontrivial _ = True++cOr :: [Constraint] -> Constraint+cOr [] = error "Empty list of constraints in cOr"+cOr [c] = c+cOr (c : cs) = COr (c :| cs)  instance Semigroup Constraint where   c1 <> c2 = cAnd [c1, c2]

@@ -1,11 +1,8 @@ {-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TemplateHaskell #-} -------------------------------------------------------------------------------------------------------------------------------------------------------------- -- | -- Module      :  Disco.Typecheck.Solve -- Copyright   :  disco team and contributors@@ -17,60 +14,61 @@ -- checking/inference. module Disco.Typecheck.Solve where -import Unbound.Generics.LocallyNameless (-  Alpha,-  Name,-  Subst,-  fv,-  name2Integer,-  string2Name,-  substs,- )--import Data.Coerce-import GHC.Generics (Generic)- import Control.Arrow ((&&&), (***)) import Control.Lens hiding (use, (%=), (.=))-import Control.Monad (unless, zipWithM)+import Control.Monad (forM, join, unless, zipWithM) import Data.Bifunctor (first, second)+import Data.Coerce import Data.Either (partitionEithers)+import Data.Foldable (Foldable (..)) import Data.List (   find,-  foldl',   intersect,   partition,  )+import Data.List.NonEmpty (NonEmpty (..))+import Data.List.NonEmpty qualified as NE import Data.Map (Map, (!))-import qualified Data.Map as M+import Data.Map qualified as M import Data.Maybe (   fromJust,   fromMaybe,   mapMaybe,  ) import Data.Monoid (First (..))+import Data.Semigroup (sconcat) import Data.Set (Set)-import qualified Data.Set as S+import Data.Set qualified as S import Data.Tuple- import Disco.Effects.Fresh import Disco.Effects.State-import Polysemy-import Polysemy.Error-import Polysemy.Input-import Polysemy.Output- import Disco.Messages import Disco.Pretty hiding ((<>)) import Disco.Subst-import qualified Disco.Subst as Subst+import Disco.Subst qualified as Subst import Disco.Typecheck.Constraints import Disco.Typecheck.Graph (Graph)-import qualified Disco.Typecheck.Graph as G+import Disco.Typecheck.Graph qualified as G import Disco.Typecheck.Unify import Disco.Types import Disco.Types.Qualifiers import Disco.Types.Rules+import Disco.Util (partitionEithersNE)+import GHC.Generics (Generic)+import Polysemy+import Polysemy.Error+import Polysemy.Input+import Polysemy.Output+import Unbound.Generics.LocallyNameless (+  Alpha,+  Name,+  Subst,+  fv,+  name2Integer,+  string2Name,+  substs,+ )+import Prelude hiding (Foldable (..))  -------------------------------------------------- -- Solver errors@@ -91,27 +89,45 @@ -------------------------------------------------- -- Error utilities -runSolve :: Sem (Fresh ': Error SolveError ': r) a -> Sem r (Either SolveError a)-runSolve = runError . runFresh+runSolve :: SolutionLimit -> Sem (State SolutionLimit ': Fresh ': Error SolveError ': r) a -> Sem r (Either SolveError a)+runSolve lim = runError . runFresh . evalState lim  -- | Run a list of actions, and return the results from those which do --   not throw an error.  If all of them throw an error, rethrow the --   first one.-filterErrors :: Member (Error e) r => [Sem r a] -> Sem r [a]+filterErrors :: Member (Error e) r => NonEmpty (Sem r a) -> Sem r (NonEmpty a) filterErrors ms = do   es <- mapM try ms-  case partitionEithers es of-    (e : _, []) -> throw e-    (_, as) -> return as+  case partitionEithersNE es of+    Left (e :| _) -> throw e+    Right (_, as) -> return as --- | A variant of 'asum' which picks the first action that succeeds,---   or re-throws the error of the last one if none of them---   do. Precondition: the list must not be empty.-asum' :: Member (Error e) r => [Sem r a] -> Sem r a-asum' [] = error "Impossible: asum' []"-asum' [m] = m-asum' (m : ms) = m `catch` (\_ -> asum' ms)+--------------------------------------------------+-- Solution limits +-- | Max number of solutions to generate.+newtype SolutionLimit = SolutionLimit {getSolutionLimit :: Int}++-- | Register the fact that we found one solution, by decrementing the+--   solution limit.+countSolution :: Member (State SolutionLimit) r => Sem r ()+countSolution = modify (SolutionLimit . subtract 1 . getSolutionLimit)++-- | Run a subcomputation conditional on the solution limit still+--   being positive.  If the solution limit has reached zero, stop+--   early.+withSolutionLimit ::+  (Member (State SolutionLimit) r, Member (Output (Message ann)) r, Monoid a) =>+  Sem r a ->+  Sem r a+withSolutionLimit m = do+  SolutionLimit lim <- get+  case lim of+    0 -> do+      debug "Reached solution limit, stopping early..."+      return mempty+    _ -> m+ -------------------------------------------------- -- Simple constraints @@ -249,15 +265,16 @@ -- Top-level solver algorithm  solveConstraint ::-  Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx] r =>+  Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx, State SolutionLimit] r =>   Constraint ->-  Sem r S+  Sem r (NonEmpty S) solveConstraint c = do   -- Step 1. Open foralls (instantiating with skolem variables) and   -- collect wanted qualifiers; also expand disjunctions.  Result in a   -- list of possible constraint sets; each one consists of equational   -- and subtyping constraints in addition to qualifiers. +  debug "============================================================"   debug "Solving:"   debugPretty c @@ -266,16 +283,17 @@    qcList <- decomposeConstraint c -  -- Now try continuing with each set and pick the first one that has-  -- a solution.-  asum' (map (uncurry solveConstraintChoice) qcList)+  -- Now try continuing with each set.+  sconcat <$> filterErrors (NE.map (uncurry solveConstraintChoice) qcList)  solveConstraintChoice ::-  Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx] r =>+  Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx, State SolutionLimit] r =>   TyVarInfoMap ->   [SimpleConstraint] ->-  Sem r S+  Sem r (NonEmpty S) solveConstraintChoice quals cs = do+  debug "solveConstraintChoice"+   debugPretty quals   debug $ vcat (map pretty' cs) @@ -387,16 +405,19 @@   debug "------------------------------"   debug "Solving for type variables..." -  theta_sol <- solveGraph vm' g'''-  debugPretty theta_sol+  theta_sols <- solveGraph vm' g'''+  case NE.nonEmpty theta_sols of+    Nothing -> throw NoUnify+    Just theta_sols_NE -> do+      debugPretty theta_sols -  debug "------------------------------"-  debug "Composing final substitution..."+      debug "------------------------------"+      debug "Composing final substitution..." -  let theta_final = theta_sol @@ theta_cyc @@ theta_skolem @@ theta_simp-  debugPretty theta_final+      let theta_finals = NE.map (@@ (theta_cyc @@ theta_skolem @@ theta_simp)) theta_sols_NE+      debugPretty theta_finals -  return theta_final+      return theta_finals  -------------------------------------------------- -- Step 1. Constraint decomposition.@@ -404,20 +425,20 @@ decomposeConstraint ::   Members '[Fresh, Error SolveError, Input TyDefCtx] r =>   Constraint ->-  Sem r [(TyVarInfoMap, [SimpleConstraint])]-decomposeConstraint (CSub t1 t2) = return [(mempty, [t1 :<: t2])]-decomposeConstraint (CEq t1 t2) = return [(mempty, [t1 :=: t2])]-decomposeConstraint (CQual q ty) = (: []) . (,[]) <$> decomposeQual ty q-decomposeConstraint (CAnd cs) = map mconcat . sequence <$> mapM decomposeConstraint cs-decomposeConstraint CTrue = return [mempty]+  Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))+decomposeConstraint (CSub t1 t2) = return $ NE.singleton (mempty, [t1 :<: t2])+decomposeConstraint (CEq t1 t2) = return $ NE.singleton (mempty, [t1 :=: t2])+decomposeConstraint (CQual q ty) = NE.singleton . (,[]) <$> decomposeQual ty q+decomposeConstraint (CAnd cs) = fmap sconcat . sequence <$> mapM decomposeConstraint cs+decomposeConstraint CTrue = return $ NE.singleton mempty decomposeConstraint (CAll ty) = do   (vars, c) <- unbind ty   let c' = substs (mkSkolems vars) c-  (map . first . addSkolems) vars <$> decomposeConstraint c'+  (NE.map . first . addSkolems) vars <$> decomposeConstraint c'  where   mkSkolems :: [Name Type] -> [(Name Type, Type)]   mkSkolems = map (id &&& TySkolem)-decomposeConstraint (COr cs) = concat <$> filterErrors (map decomposeConstraint cs)+decomposeConstraint (COr cs) = sconcat <$> filterErrors (NE.map decomposeConstraint cs)  decomposeQual ::   Members '[Fresh, Error SolveError, Input TyDefCtx] r =>@@ -878,6 +899,7 @@ -- | A RelMap associates each variable to its sets of base type and --   variable predecessors and successors in the constraint graph. newtype RelMap = RelMap {unRelMap :: Map (Name Type, Dir) Rels}+  deriving (Show)  instance Pretty RelMap where   pretty (RelMap rm) = vcat (map prettyVar byVar)@@ -950,6 +972,18 @@ lubBySort vm rm = limBySort vm rm SuperTy glbBySort vm rm = limBySort vm rm SubTy +allBySort :: TyVarInfoMap -> RelMap -> Dir -> [BaseTy] -> Sort -> Set (Name Type) -> Set BaseTy+allBySort vm rm dir ts s x =+  isects+    . map (\t -> S.fromList (dirtypesBySort vm rm dir t s x))+    $ ts+ where+  isects = foldr1 S.intersection++ubsBySort, lbsBySort :: TyVarInfoMap -> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Set BaseTy+ubsBySort vm rm = allBySort vm rm SuperTy+lbsBySort vm rm = allBySort vm rm SubTy+ -- | From the constraint graph, build the sets of sub- and super- base --   types of each type variable, as well as the sets of sub- and --   supertype variables.  For each type variable x in turn, try to@@ -964,11 +998,14 @@ --   predecessors in this case, since it seems nice to default to --   "simpler" types lower down in the subtyping chain. solveGraph ::-  Members '[Fresh, Error SolveError, Output (Message ann)] r =>+  Members '[Fresh, Error SolveError, Output (Message ann), State SolutionLimit] r =>   TyVarInfoMap ->   Graph UAtom ->-  Sem r S-solveGraph vm g = atomToTypeSubst . unifyWCC <$> go topRelMap+  Sem r [S]+solveGraph vm g = do+  debug "Solving graph..."+  debugPretty g+  map (atomToTypeSubst . unifyWCC) <$> go topRelMap  where   unifyWCC :: Substitution BaseTy -> Substitution Atom   unifyWCC s = compose (map mkEquateSubst wccVarGroups) @@ fmap ABase s@@ -1030,35 +1067,37 @@     fromVar _ = error "Impossible! UB but uisVar."    go ::-    Members '[Fresh, Error SolveError, Output (Message ann)] r =>+    Members '[Fresh, Output (Message ann), State SolutionLimit] r =>     RelMap ->-    Sem r (Substitution BaseTy)-  go relMap@(RelMap rm) =-    debugPretty relMap >> case as of+    Sem r [Substitution BaseTy]+  go relMap@(RelMap rm) = withSolutionLimit $ do+    debugPretty relMap+    case as of       -- No variables left that have base type constraints.-      [] -> return idS+      [] -> do+        -- Found a solution, decrement the counter.+        countSolution+        return [idS]       -- Solve one variable at a time.  See below.       (a : _) -> do         debug $ "Solving for" <+> pretty' a-        case solveVar a of-          Nothing -> do-            debug $ "Couldn't solve for" <+> pretty' a-            throw NoUnify+        let ss = solveVar a+        debugPretty ss -          -- If we solved for a, delete it from the maps, apply the-          -- resulting substitution to the remainder (updating the-          -- relMap appropriately), and recurse.  The substitution we-          -- want will be the composition of the substitution for a-          -- with the substitution generated by the recursive call.-          ---          -- Note we don't need to delete a from the TyVarInfoMap; we-          -- never use the set of keys from the TyVarInfoMap for-          -- anything (indeed, some variables might not be keys if-          -- they have an empty sort), so it doesn't matter if old-          -- variables hang around in it.-          Just s -> do-            debugPretty s-            (@@ s) <$> go (substRel a (fromJust $ Subst.lookup (coerce a) s) relMap)+        -- If we solved for a, delete it from the maps, apply the+        -- resulting substitution to the remainder (updating the+        -- relMap appropriately), and recurse.  The substitution we+        -- want will be the composition of the substitution for a+        -- with the substitution generated by the recursive call.+        --+        -- Note we don't need to delete a from the TyVarInfoMap; we+        -- never use the set of keys from the TyVarInfoMap for+        -- anything (indeed, some variables might not be keys if+        -- they have an empty sort), so it doesn't matter if old+        -- variables hang around in it.+        ss' <- forM ss $ \s ->+          map (@@ s) <$> go (substRel a (fromJust $ Subst.lookup (coerce a) s) relMap)+        return (join ss')    where     -- NOTE we can't solve a bunch in parallel!  Might end up     -- assigning them conflicting solutions if some depend on@@ -1099,9 +1138,14 @@       [] -> filter ((/= topSort) . getSort vm) . map fst $ M.keys rm       _ -> asBase -    -- Solve for a variable, failing if it has no solution, otherwise returning-    -- a substitution for it.-    solveVar :: Name Type -> Maybe (Substitution BaseTy)+    -- XXX the right way to do this is to keep track of the+    -- polarity of each variable.  For variables that have only+    -- one polarity we can pick the greatest or least solution as+    -- appropriate.  For other variables, we have to return all of+    -- them.++    -- Solve for a variable, returning all possible substitutions.+    solveVar :: Name Type -> [Substitution BaseTy]     solveVar v =       case ((v, SuperTy), (v, SubTy)) & over both (S.toList . baseRels . lkup "solveGraph.solveVar" rm) of         -- No sub- or supertypes; the only way this can happen is@@ -1122,24 +1166,22 @@         -- nontrivial sorts means that we are dealing with numeric         -- types; so we can just call N a base subtype and go from         -- there.+        --+        -- Hmm, no, this is wrong!  E.g. we could have a QCmp+        -- constraint, in which case something like Char or Bool+        -- could be OK...  In any case, this is really just to be+        -- able to show users some sample types, it's not an issue+        -- of soundness.  We don't (can't?) guarantee to return ALL possible types.          ([], []) ->-          if getSort vm v == S.fromList [QBool]-            then Just (coerce v |-> B)-            else -- Debug.trace (show v ++ " has no sub- or supertypes.  Assuming N as a subtype.")--              (coerce v |->)-                <$> lubBySort-                  vm-                  relMap-                  [N]-                  (getSort vm v)-                  (varRels (lkup "solveVar none, rels" rm (v, SubTy)))+          -- Debug.trace (show v ++ " has no sub- or supertypes.")+          -- Pick some base type with an appropriate sort.+          map (coerce v |->) $ filter (`hasSort` getSort vm v) [N, Z, F, Q, B, C]         -- Only supertypes.  Just assign a to their inf, if one exists.         (bsupers, []) ->           -- Debug.trace (show v ++ " has only supertypes (" ++ show bsupers ++ ")") $-          (coerce v |->)-            <$> glbBySort+          map (coerce v |->) . S.toList $+            lbsBySort               vm               relMap               bsupers@@ -1148,35 +1190,23 @@         -- Only subtypes.  Just assign a to their sup.         ([], bsubs) ->           -- Debug.trace (show v ++ " has only subtypes (" ++ show bsubs ++ ")") $-          -- Debug.trace ("sortmap: " ++ show vm) $+          -- Debug.trace ("varmap: " ++ show vm) $           -- Debug.trace ("relmap: " ++ show relMap) $           -- Debug.trace ("sort for " ++ show v ++ ": " ++ show (getSort vm v)) $           -- Debug.trace ("relvars: " ++ show (varRels (relMap ! (v,SubTy)))) $-          (coerce v |->)-            <$> lubBySort+          map (coerce v |->) . S.toList $+            ubsBySort               vm               relMap               bsubs               (getSort vm v)               (varRels (lkup "solveVar bsubs, rels" rm (v, SubTy)))         -- Both successors and predecessors.  Both must have a-        -- valid bound, and the bounds must not overlap.  Assign a-        -- to the sup of its predecessors.-        (bsupers, bsubs) -> do-          ub <--            glbBySort-              vm-              relMap-              bsupers-              (getSort vm v)-              (varRels (rm ! (v, SuperTy)))-          lb <--            lubBySort-              vm-              relMap-              bsubs-              (getSort vm v)-              (varRels (rm ! (v, SubTy)))-          case isSubB lb ub of-            True -> Just (coerce v |-> lb)-            False -> Nothing+        -- valid bound, and the bounds must not overlap.+        (bsupers, bsubs) ->+          let mub = glbBySort vm relMap bsupers (getSort vm v) (varRels (rm ! (v, SuperTy)))+              mlb = lubBySort vm relMap bsubs (getSort vm v) (varRels (rm ! (v, SubTy)))+           in case (mlb, mub) of+                (Just lb, Just ub) ->+                  map (coerce v |->) (filter (`isSubB` ub) (supertypes lb))+                _ -> []

@@ -1,7 +1,3 @@-------------------------------------------------------------------------------------------------------------------------------------------------------------- -- | -- Module      :  Disco.Typecheck.Unify -- Copyright   :  disco team and contributors@@ -15,7 +11,8 @@ import Unbound.Generics.LocallyNameless (Name, fv)  import Control.Lens (anyOf)-import Control.Monad.State+import Control.Monad (mzero)+import Control.Monad.State (StateT, evalStateT, get, modify) import qualified Data.Map as M import Data.Set (Set) import qualified Data.Set as S@@ -120,7 +117,7 @@ equate :: TyDefCtx -> [Type] -> Maybe S equate tyDefns tys = unify tyDefns eqns  where-  eqns = zip tys (tail tys)+  eqns = zip tys (drop 1 tys)  occurs :: Name Type -> Type -> Bool occurs x = anyOf fv (== x)

@@ -1,4 +1,3 @@- -- | -- Module      :  Disco.Typecheck.Util -- Copyright   :  (c) 2016 disco team (see LICENSE)@@ -9,25 +8,24 @@ -- used during type checking. module Disco.Typecheck.Util where -import Disco.Effects.Fresh-import Polysemy-import Polysemy.Error-import Polysemy.Output-import Polysemy.Reader-import Polysemy.Writer-import Unbound.Generics.LocallyNameless (Name, bind, string2Name)-+import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.Map as M import Data.Tuple (swap)-import Prelude hiding (lookup)- import Disco.AST.Surface import Disco.Context+import Disco.Effects.Fresh import Disco.Messages import Disco.Names (ModuleName, QName) import Disco.Typecheck.Constraints import Disco.Typecheck.Solve import Disco.Types+import Polysemy+import Polysemy.Error+import Polysemy.Output+import Polysemy.Reader+import Polysemy.Writer+import Unbound.Generics.LocallyNameless (Name, bind, string2Name)+import Prelude hiding (lookup)  ------------------------------------------------------------ -- Contexts@@ -52,8 +50,10 @@  -- | Potential typechecking errors. data TCError-  = -- | Encountered an unbound variable-    Unbound (Name Term)+  = -- | Encountered an unbound variable.  The offending variable+    --   together with some suggested in-scope names with small edit+    --   distance.+    Unbound (Name Term) [String]   | -- | Encountered an ambiguous name.     Ambiguous (Name Term) [ModuleName]   | -- | No type is specified for a definition@@ -91,8 +91,8 @@     NotEnoughArgs Con   | -- | Too many arguments provided to type constructor.     TooManyArgs Con-  | -- | Unbound type variable-    UnboundTyVar (Name Type)+  | -- | Unbound type variable, together with suggested edits+    UnboundTyVar (Name Type) [String]   | -- | Polymorphic recursion is not allowed     NoPolyRec String [String] [Type]   | -- | Not an error.  The identity of the@@ -126,11 +126,11 @@  -- | Run two constraint-generating actions and combine the constraints --   via disjunction.-cOr :: Members '[Writer Constraint] r => Sem r () -> Sem r () -> Sem r ()-cOr m1 m2 = do+orElse :: Members '[Writer Constraint] r => Sem r () -> Sem r () -> Sem r ()+orElse m1 m2 = do   (c1, _) <- censor (const CTrue) (listen m1)   (c2, _) <- censor (const CTrue) (listen m2)-  constraint $ COr [c1, c2]+  constraint $ COr (c1 :| [c2])  -- | Run a computation that generates constraints, returning the --   generated 'Constraint' along with the output. Note that this@@ -142,18 +142,20 @@ withConstraint = fmap swap . runWriter  -- | Run a computation and solve its generated constraint, returning---   the resulting substitution (or failing with an error).  Note that---   this locally dispatches the constraint writer effect.+--   up to the requested number of possible resulting substitutions+--   (or failing with an error).  Note that this locally dispatches+--   the constraint writer and solution limit effects. solve ::   Members '[Reader TyDefCtx, Error TCError, Output (Message ann)] r =>+  Int ->   Sem (Writer Constraint ': r) a ->-  Sem r (a, S)-solve m = do+  Sem r (a, NonEmpty S)+solve lim m = do   (a, c) <- withConstraint m-  res <- runSolve . inputToReader . solveConstraint $ c+  res <- runSolve (SolutionLimit lim) . inputToReader . solveConstraint $ c   case res of     Left e -> throw (Unsolvable e)-    Right s -> return (a, s)+    Right ss -> return (a, ss)  ------------------------------------------------------------ -- Contexts

@@ -5,10 +5,6 @@ {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -------------------------------------------------------------------------------------------------------------------------------------------------------------- -- SPDX-License-Identifier: BSD-3-Clause  -- |@@ -56,6 +52,7 @@   pattern TyF,   pattern TyQ,   pattern TyC,+  pattern TyGen,   -- , pattern TyFin   pattern (:->:),   pattern (:*:),@@ -156,6 +153,7 @@   -- the exact number of inhabitants.   -- Fin  :: Integer -> BaseTy +  Gen :: BaseTy   -- | Set container type.  It's a bit odd putting these here since   --   they have kind * -> * and all the other base types have kind *;   --   but there's nothing fundamentally wrong with it and in@@ -182,6 +180,7 @@     CtrList -> text "List"     CtrBag -> text "Bag"     CtrSet -> text "Set"+    Gen -> text "Gen"  -- | Test whether a 'BaseTy' is a container (set, bag, or list). isCtr :: BaseTy -> Bool@@ -415,6 +414,7 @@ instance Subst Type Rational where   subst _ _ = id   substs _ = id+  substBvs _ _ = id instance Subst Type Void where   subst _ _ = id   substs _ = id@@ -462,6 +462,9 @@ pattern TyC :: Type pattern TyC = TyAtom (ABase C) +pattern TyGen :: Type+pattern TyGen = TyAtom (ABase Gen)+ -- pattern TyFin :: Integer -> Type -- pattern TyFin n = TyAtom (ABase (Fin n)) @@ -537,9 +540,11 @@ instance (Ord a, Subst t a) => Subst t (Set a) where   subst x t = S.map (subst x t)   substs s = S.map (substs s)+  substBvs c bs = S.map (substBvs c bs) instance (Ord k, Subst t a) => Subst t (Map k a) where   subst x t = M.map (subst x t)   substs s = M.map (substs s)+  substBvs c bs = M.map (substBvs c bs)  -- | The definition of a user-defined type contains: --

@@ -1,14 +1,10 @@----------------------------------------------------------------------------------------------------------------------------------------------------------------- SPDX-License-Identifier: BSD-3-Clause- -- | -- Module      :  Disco.Types.Rules -- Copyright   :  disco team and contributors -- Maintainer  :  byorgey@gmail.com --+-- SPDX-License-Identifier: BSD-3-Clause+-- -- "Disco.Types.Rules" defines some generic rules about arity, -- subtyping, and sorts for disco base types. module Disco.Types.Rules (@@ -44,13 +40,13 @@ where  import Control.Monad ((>=>))-import Data.List (foldl')+import Data.Foldable (Foldable (..)) import Data.Map (Map) import qualified Data.Map as M import qualified Data.Set as S- import Disco.Types import Disco.Types.Qualifiers+import Prelude hiding (Foldable (..))  ------------------------------------------------------------ -- Arity

@@ -1,6 +1,4 @@-------------------------------------------------------------------------------------------------------------------------------------------------------------+{-# LANGUAGE ImportQualifiedPost #-}  -- | -- Module      :  Disco.Util@@ -12,7 +10,12 @@ -- Miscellaneous utilities. module Disco.Util where -import qualified Data.Map as M+import Control.Applicative (Alternative)+import Control.Monad (guard)+import Data.Bifunctor (bimap)+import Data.List.NonEmpty (NonEmpty)+import Data.List.NonEmpty qualified as NE+import Data.Map qualified as M  infixr 1 ==> @@ -21,10 +24,56 @@ (==>) :: a -> b -> (a, b) (==>) = (,) +-- | Flipped variant of 'map'. for :: [a] -> (a -> b) -> [b] for = flip map +-- | A variant of 'Map' indexing that throws a custom error message+--   in case the key is not found, to help with debugging. (!) :: (Show k, Ord k) => M.Map k v -> k -> v m ! k = case M.lookup k m of   Nothing -> error $ "key " ++ show k ++ " is not an element in the map"   Just v -> v++-- | Find the maximum of a list of positive numbers, yielding 0 in the+--   case of an empty list.+maximum0 :: (Num a, Ord a) => [a] -> a+maximum0 [] = 0+maximum0 xs = maximum xs++-- | A variant of 'filter' that returns a @Maybe (NonEmpty a)@ instead+--   of a regular list.+filterNE :: (a -> Bool) -> NonEmpty a -> Maybe (NonEmpty a)+filterNE p = NE.nonEmpty . NE.filter p++-- | A variant of 'partition' that returns @Maybe (NonEmpty a)@s instead+--   of regular lists.+partitionNE :: (a -> Bool) -> NonEmpty a -> (Maybe (NonEmpty a), Maybe (NonEmpty a))+partitionNE p as = (filterNE p as, filterNE (not . p) as)++-- | A variant of 'partitionEithers' for nonempty lists.  If the+--   result is Left, it means all the inputs were Left.  If the result+--   is Right, we definitely have some Rights, and possibly some Lefts+--   as well.  This properly encodes the fact that at least one result+--   list must be nonempty.+partitionEithersNE :: NonEmpty (Either a b) -> Either (NonEmpty a) ([a], NonEmpty b)+partitionEithersNE = foldr1 combine . NE.map (bimap NE.singleton (([],) . NE.singleton))+ where+  combine :: Either (NonEmpty a) ([a], NonEmpty b) -> Either (NonEmpty a) ([a], NonEmpty b) -> Either (NonEmpty a) ([a], NonEmpty b)+  combine (Left as1) (Left as2) = Left (NE.append as1 as2)+  combine (Left as1) (Right (as2, bs)) = Right (NE.toList as1 ++ as2, bs)+  combine (Right (as1, bs)) (Left as2) = Right (as1 ++ NE.toList as2, bs)+  combine (Right (as1, bs1)) (Right (as2, bs2)) = Right (as1 ++ as2, NE.append bs1 bs2)++-- | Iterate a function until finding the first value that satisfies+--   the given predicate.  @iterUntil f p@ is equivalent to @head+--   . filter p . iterate f@ but does not trigger a partiality+--   warning.+iterUntil :: (a -> a) -> (a -> Maybe b) -> a -> b+iterUntil f p a = case p a of+  Just b -> b+  _ -> iterUntil f p (f a)++-- | Allow a value through only if it satisfies the given predicate.+gate :: Alternative f => (a -> Bool) -> a -> f a+gate p a = a <$ guard (p a)

@@ -4,10 +4,6 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-} -------------------------------------------------------------------------------------------------------------------------------------------------------------- -- | -- Module      :  Disco.Value -- Copyright   :  disco team and contributors@@ -30,11 +26,14 @@   vint,   charv,   vchar,-  enumv,+  boolv,+  vbool,   pairv,   vpair,   listv,   vlist,+  genv,+  vgen,    -- * Props & testing   ValProp (..),@@ -46,6 +45,7 @@   TestVars (..),   TestEnv (..),   emptyTestEnv,+  mergeTestEnv,   getTestEnv,   extendPropEnv,   extendResultEnv,@@ -65,45 +65,47 @@   Mem,   emptyMem,   allocate,+  allocateValue,   allocateRec,   lkup,+  memoLookup,   set,+  memoSet,    -- * Pretty-printing   prettyValue',   prettyValue, ) where -import Prelude hiding ((<>))-import qualified Prelude as P-+import Algebra.Graph (Graph, foldg) import Control.Monad (forM) import Data.Bifunctor (first)-import Data.Char (chr, ord, toLower)+import Data.Char (chr, ord)+import Data.Foldable (Foldable (..))+import Data.Function (on) import Data.IntMap (IntMap) import qualified Data.IntMap as IM-import Data.List (foldl')+import Data.List (nubBy) import Data.Map (Map) import qualified Data.Map as M import Data.Ratio--import Algebra.Graph (Graph, foldg)- import Disco.AST.Core import Disco.AST.Generic (Side (..)) import Disco.Context as Ctx+import Disco.Effects.LFresh import Disco.Error import Disco.Names import Disco.Pretty import Disco.Syntax.Operators (BOp (Add, Mul)) import Disco.Types--import Disco.Effects.LFresh import Polysemy import Polysemy.Input import Polysemy.Reader import Polysemy.State+import System.Random (StdGen) import Unbound.Generics.LocallyNameless (Name)+import Prelude hiding (Foldable (..), (<>))+import qualified Prelude as P  ------------------------------------------------------------ -- Value type@@ -112,9 +114,8 @@ -- | Different types of values which can result from the evaluation --   process. data Value where-  -- | A numeric value, which also carries a flag saying how-  --   fractional values should be diplayed.-  VNum :: RationalDisplay -> Rational -> Value+  -- | A numeric value.+  VNum :: Rational -> Value   -- | A built-in function constant.   VConst :: Op -> Value   -- | An injection into a sum type.@@ -125,7 +126,7 @@   VPair :: Value -> Value -> Value   -- | A closure, i.e. a function body together with its   --   environment.-  VClo :: Env -> [Name Core] -> Core -> Value+  VClo :: Maybe (Int, [Value]) -> Env -> [Name Core] -> Core -> Value   -- | A disco type can be a value.  For now, there are only a very   --   limited number of places this could ever show up (in   --   particular, as an argument to @enumerate@ or @count@).@@ -158,6 +159,7 @@   --   actually construct the set of entries, while functions only have this   --   property when the key type is finite.   VMap :: Map SimpleValue Value -> Value+  VGen :: StdGen -> Value   deriving (Show)  -- | Convenient pattern for the empty list.@@ -178,7 +180,7 @@ --   only reason for actually doing this would be constructing graphs --   of graphs or maps of maps, or the like. data SimpleValue where-  SNum :: RationalDisplay -> Rational -> SimpleValue+  SNum :: Rational -> SimpleValue   SUnit :: SimpleValue   SInj :: Side -> SimpleValue -> SimpleValue   SPair :: SimpleValue -> SimpleValue -> SimpleValue@@ -188,7 +190,7 @@  toSimpleValue :: Value -> SimpleValue toSimpleValue = \case-  VNum d n -> SNum d n+  VNum n -> SNum n   VUnit -> SUnit   VInj s v1 -> SInj s (toSimpleValue v1)   VPair v1 v2 -> SPair (toSimpleValue v1) (toSimpleValue v2)@@ -197,7 +199,7 @@   t -> error $ "A non-simple value was passed as simple: " ++ show t  fromSimpleValue :: SimpleValue -> Value-fromSimpleValue (SNum d n) = VNum d n+fromSimpleValue (SNum n) = VNum n fromSimpleValue SUnit = VUnit fromSimpleValue (SInj s v) = VInj s (fromSimpleValue v) fromSimpleValue (SPair v1 v2) = VPair (fromSimpleValue v1) (fromSimpleValue v2)@@ -221,13 +223,11 @@  -- XXX write some comments about partiality --- | A convenience function for creating a default @VNum@ value with a---   default (@Fractional@) flag. ratv :: Rational -> Value-ratv = VNum mempty+ratv = VNum  vrat :: Value -> Rational-vrat (VNum _ r) = r+vrat (VNum r) = r vrat v = error $ "vrat " ++ show v  -- | A convenience function for creating a default @VNum@ value with a@@ -236,7 +236,7 @@ intv = ratv . (% 1)  vint :: Value -> Integer-vint (VNum _ n) = numerator n+vint (VNum n) = numerator n vint v = error $ "vint " ++ show v  vchar :: Value -> Char@@ -245,11 +245,13 @@ charv :: Char -> Value charv = intv . fromIntegral . ord --- | Turn any instance of @Enum@ into a @Value@, by creating a---   constructor with an index corresponding to the enum value.-enumv :: Enum e => e -> Value-enumv e = VInj (toEnum $ fromEnum e) VUnit+boolv :: Bool -> Value+boolv e = VInj (toEnum $ fromEnum e) VUnit +vbool :: Value -> Bool+vbool (VInj s VUnit) = toEnum $ fromEnum s+vbool v = error $ "vbool " ++ show v+ pairv :: (a -> Value) -> (b -> Value) -> (a, b) -> Value pairv av bv (a, b) = VPair (av a) (bv b) @@ -266,6 +268,13 @@ vlist velt (VCons v vs) = velt v : vlist velt vs vlist _ v = error $ "vlist " ++ show v +vgen :: Value -> StdGen+vgen (VGen v) = v+vgen v = error $ "vgen " ++ show v++genv :: StdGen -> Value+genv = VGen+ ------------------------------------------------------------ -- Propositions ------------------------------------------------------------@@ -305,6 +314,11 @@ emptyTestEnv :: TestEnv emptyTestEnv = TestEnv [] +mergeTestEnv :: TestEnv -> TestEnv -> TestEnv+mergeTestEnv (TestEnv e1) (TestEnv e2) = TestEnv (nubBy ((==) `on` fst3) (e1 P.<> e2))+ where+  fst3 (a, _, _) = a+ getTestEnv :: TestVars -> Env -> Either EvalError TestEnv getTestEnv (TestVars tvs) e = fmap TestEnv . forM tvs $ \(s, ty, name) -> do   let value = Ctx.lookup' (localName name) e@@ -329,12 +343,10 @@ data TestReason_ a   = -- | The prop evaluated to a boolean.     TestBool-  | -- | The test was an equality test. Records the values being-    --   compared and also their type (which is needed for printing).-    TestEqual Type a a-  | -- | The test was a less than test. Records the values being-    --   compared and also their type (which is needed for printing).-    TestLt Type a a+  | -- | The test was a comparison. Records the comparison operator,+    --   the values being compared, and also their type (which is+    --   needed for printing).+    TestCmp BOp Type a a   | -- | The search didn't find any examples/counterexamples.     TestNotFound SearchType   | -- | The search found an example/counterexample.@@ -354,7 +366,7 @@  -- | Whether the property test resulted in a runtime error. testIsError :: TestResult -> Bool-testIsError (TestResult _ (TestRuntimeError _) _) = True+testIsError (TestResult _ (TestRuntimeError {}) _) = True testIsError _ = False  -- | Whether the property test resulted in success.@@ -373,12 +385,11 @@  resultIsCertain :: TestReason -> Bool resultIsCertain TestBool = True-resultIsCertain TestEqual {} = True-resultIsCertain TestLt {} = True+resultIsCertain TestCmp {} = True resultIsCertain (TestNotFound Exhaustive) = True resultIsCertain (TestNotFound (Randomized _ _)) = False resultIsCertain (TestFound r) = testIsCertain r-resultIsCertain (TestRuntimeError _) = True+resultIsCertain (TestRuntimeError {}) = True resultIsCertain (TestBin op tr1 tr2)   | c1 && c2 = True   | c1 && ((op == LOr) == ok1) = True@@ -401,7 +412,7 @@   deriving (Show)  extendPropEnv :: TestEnv -> ValProp -> ValProp-extendPropEnv g (VPDone (TestResult b r e)) = VPDone (TestResult b r (g P.<> e))+extendPropEnv g (VPDone res) = VPDone (extendResultEnv g res) extendPropEnv g (VPSearch sm tys v e) = VPSearch sm tys v (g P.<> e) extendPropEnv g (VPBin op vp1 vp2) = VPBin op (extendPropEnv g vp1) (extendPropEnv g vp2) @@ -436,6 +447,12 @@   put $ Mem (n + 1) (IM.insert n (E e t) m)   return n +allocateValue :: Members '[State Mem] r => Value -> Sem r Int+allocateValue v = do+  Mem n m <- get+  put $ Mem (n + 1) (IM.insert n (Disco.Value.V v) m)+  return n+ -- | Allocate new memory cells for a group of mutually recursive --   bindings, and return the indices of the allocate cells. allocateRec :: Members '[State Mem] r => Env -> [(QName Core, Core)] -> Sem r [Int]@@ -456,6 +473,19 @@ set :: Members '[State Mem] r => Int -> Cell -> Sem r () set n c = modify $ \(Mem nxt m) -> Mem nxt (IM.insert n c m) +memoLookup :: Members '[State Mem] r => Int -> SimpleValue -> Sem r (Maybe Value)+memoLookup n sv = gets (mLookup . IM.lookup n . mu)+ where+  mLookup (Just (Disco.Value.V (VMap vmap))) = M.lookup sv vmap+  mLookup _ = Nothing++memoSet :: Members '[State Mem] r => Int -> SimpleValue -> Value -> Sem r ()+memoSet n sv v = do+  mc <- lkup n+  case mc of+    Just (Disco.Value.V (VMap vmap)) -> set n (Disco.Value.V (VMap (M.insert sv v vmap)))+    _ -> return ()+ ------------------------------------------------------------ -- Pretty-printing values ------------------------------------------------------------@@ -471,7 +501,7 @@   prettyValue (body args) v prettyValue _ VUnit = "■" prettyValue TyProp _ = prettyPlaceholder TyProp-prettyValue TyBool (VInj s _) = text $ map toLower (show (s == R))+prettyValue TyBool (VInj s _) = text $ take 1 (show (s == R)) prettyValue TyBool v =   error $ "Non-VInj passed with Bool type to prettyValue: " ++ show v prettyValue TyC (vchar -> c) = text (show c)@@ -486,11 +516,8 @@ prettyValue (_ :+: ty2) (VInj R v) = "right" <> prettyVP ty2 v prettyValue (_ :+: _) v =   error $ "Non-VInj passed with sum type to prettyValue: " ++ show v-prettyValue _ (VNum d r)-  | denominator r == 1 = text $ show (numerator r)-  | otherwise = text $ case d of-      Fraction -> show (numerator r) ++ "/" ++ show (denominator r)-      Decimal -> prettyDecimal r+prettyValue _ (VNum r) = text $ prettyRational r+prettyValue _ (VGen _) = prettyPlaceholder TyGen prettyValue ty@(_ :->: _) _ = prettyPlaceholder ty prettyValue (TySet ty) (VBag xs) = braces $ prettySequence ty "," (map fst xs) prettyValue (TySet _) v =

@@ -0,0 +1,53 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}++-- This module was copied from polysemy-zoo:+-- https://hackage.haskell.org/package/polysemy-zoo-0.8.2.0/docs/src/Polysemy.ConstraintAbsorber.html++module Polysemy.ConstraintAbsorber (+  -- * Absorb builder+  absorbWithSem,++  -- * Re-exports+  Reifies,+  (:-) (Sub),+  Dict (Dict),+  reflect,+  Proxy (Proxy),+) where++import Data.Constraint (Dict (Dict), (:-) (Sub), (\\))+import qualified Data.Constraint as C+import qualified Data.Constraint.Unsafe as C+import Data.Kind (Constraint, Type)+import Data.Proxy (Proxy (..))+import Data.Reflection (Reifies, reflect)+import qualified Data.Reflection as R+import Polysemy++------------------------------------------------------------------------------++-- | This function can be used to locally introduce typeclass instances for+-- 'Sem'. See 'Polysemy.ConstraintAbsorber.MonadState' for an example of how to+-- use it.+absorbWithSem ::+  forall+    -- Constraint to be absorbed+    (p :: (Type -> Type) -> Constraint)+    -- Wrapper to avoid orphan instances+    (x :: (Type -> Type) -> Type -> Type -> Type)+    d+    r+    a.+  -- | Reified dictionary+  d ->+  -- | This parameter should always be @'Sub' 'Dict'@+  (forall s. R.Reifies s d :- p (x (Sem r) s)) ->+  (p (Sem r) => Sem r a) ->+  Sem r a+absorbWithSem d i m = R.reify d $ \(_ :: Proxy (s :: Type)) ->+  m+    \\ C.trans+      (C.unsafeCoerceConstraint :: (p (x m s) :- p m))+      i+{-# INLINEABLE absorbWithSem #-}

@@ -0,0 +1,128 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE UndecidableInstances #-}++-- This module was copied from polysemy-zoo:+-- https://hackage.haskell.org/package/polysemy-zoo-0.8.2.0/docs/src/Polysemy.ConstraintAbsorber.MonadCatch.html++module Polysemy.ConstraintAbsorber.MonadCatch (+  -- * Constraint Absorbers+  absorbMonadThrow,+  absorbMonadCatch,++  -- * run helper+  runMonadCatch,+  runMonadCatchAsText,++  -- * Re-exports+  Exception (..),+  SomeException,+)+where++import Control.Monad.Catch (+  Exception (..),+  SomeException,+  toException,+ )+import qualified Control.Monad.Catch as C++import qualified Data.Text as T+import Polysemy+import Polysemy.ConstraintAbsorber+import qualified Polysemy.Error as E++------------------------------------------------------------------------------++-- | Like 'E.runError' but applies a given function from 'SomeException'+-- to some other type, typically something less opaque.+-- e.g.:+--  @runMonadCatch C.displayException@+runMonadCatch ::+  Exception e =>+  (Maybe e -> e') ->+  Sem (E.Error C.SomeException : E.Error e' : r) a ->+  Sem r (Either e' a)+runMonadCatch f = E.runError . E.mapError (f . C.fromException)++runMonadCatchAsText ::+  Sem (E.Error C.SomeException : E.Error T.Text : r) a ->+  Sem r (Either T.Text a)+runMonadCatchAsText = E.runError . E.mapError (T.pack . C.displayException)++-- | Introduce a local 'S.MonadCatch' constraint on 'Sem' --- allowing it to+-- interop nicely with exceptions+absorbMonadCatch ::+  Member (E.Error C.SomeException) r =>+  -- | A computation that requires an instance of 'C.MonadCatch'+  -- or 'C.MonadThrow' for+  -- 'Sem'. This might be something with type @'C.MonadCatch' e m => m a@.+  (C.MonadCatch (Sem r) => Sem r a) ->+  Sem r a+absorbMonadCatch =+  absorbWithSem @C.MonadCatch @Action (CatchDict E.throw E.catch) (Sub Dict)+{-# INLINEABLE absorbMonadCatch #-}++-- | Introduce a local 'S.MonadThrow' constraint on 'Sem' --- allowing it to+-- interop nicely with exceptions+absorbMonadThrow ::+  Member (E.Error C.SomeException) r =>+  -- | A computation that requires an instance of 'C.MonadCatch'+  -- or 'C.MonadThrow' for+  -- 'Sem'. This might be something with type @'C.MonadCatch' e m => m a@.+  (C.MonadThrow (Sem r) => Sem r a) ->+  Sem r a+absorbMonadThrow = absorbMonadCatch+{-# INLINEABLE absorbMonadThrow #-}++------------------------------------------------------------------------------++-- | A dictionary of the functions we need to supply+-- to make an instance of Error+data CatchDict m = CatchDict+  { throwM_ :: forall a. C.SomeException -> m a+  , catch_ :: forall a. m a -> (C.SomeException -> m a) -> m a+  }++------------------------------------------------------------------------------++-- | Wrapper for a monadic action with phantom+-- type parameter for reflection.+-- Locally defined so that the instance we are going+-- to build with reflection must be coherent, that is+-- there cannot be orphans.+newtype Action m s' a = Action {action :: m a}+  deriving (Functor, Applicative, Monad)++------------------------------------------------------------------------------++-- | Given a reifiable mtl Error dictionary,+-- we can make an instance of @MonadError@ for the action+-- wrapped in @Action@.+instance+  ( Monad m+  , Reifies s' (CatchDict m)+  ) =>+  C.MonadThrow (Action m s')+  where+  throwM e = Action $ throwM_ (reflect $ Proxy @s') (C.toException e)+  {-# INLINEABLE throwM #-}++instance+  ( Monad m+  , Reifies s' (CatchDict m)+  ) =>+  C.MonadCatch (Action m s')+  where+  catch x f =+    let catchF = catch_ (reflect $ Proxy @s')+     in Action $+          action x `catchF` \e -> case C.fromException e of+            Just e' -> action $ f e'+            _ -> throwM_ (reflect $ Proxy @s') (C.toException e)+  {-# INLINEABLE catch #-}

@@ -0,0 +1,63 @@+{-# LANGUAGE TemplateHaskell #-}++-- This module was copied from polysemy-zoo:+-- https://hackage.haskell.org/package/polysemy-zoo-0.8.2.0/docs/src/Polysemy.Random.html++module Polysemy.Random (+  -- * Effect+  Random (..),++  -- * Actions+  random,+  randomR,++  -- * Interpretations+  runRandom,+  runRandomIO,+) where++import Polysemy+import Polysemy.State+import qualified System.Random as R++------------------------------------------------------------------------------++-- | An effect capable of providing 'R.Random' values.+data Random m a where+  Random :: R.Random x => Random m x+  RandomR :: R.Random x => (x, x) -> Random m x++makeSem ''Random++------------------------------------------------------------------------------++-- | Run a 'Random' effect with an explicit 'R.RandomGen'.+runRandom ::+  forall q r a.+  R.RandomGen q =>+  q ->+  Sem (Random ': r) a ->+  Sem r (q, a)+runRandom q =+  runState q+    . reinterpret+      ( \case+          Random -> do+            ~(a, q') <- gets @q R.random+            put q'+            pure a+          RandomR r -> do+            ~(a, q') <- gets @q $ R.randomR r+            put q'+            pure a+      )+{-# INLINE runRandom #-}++------------------------------------------------------------------------------++-- | Run a 'Random' effect by using the 'IO' random generator.+runRandomIO :: Member (Embed IO) r => Sem (Random ': r) a -> Sem r a+runRandomIO m = do+  q <- embed @IO R.newStdGen+  snd <$> runRandom q m+{-# INLINE runRandomIO #-}

@@ -2,7 +2,7 @@ # For more information, see: http://docs.haskellstack.org/en/stable/yaml_configuration/  # Specifies the GHC version and set of packages available (e.g., lts-3.5, nightly-2015-09-21, ghc-7.10.2)-resolver: lts-21.13+resolver: lts-22.13  # Local packages, usually specified by relative directory name packages:@@ -10,12 +10,10 @@  # Packages to be pulled from upstream that are not in the resolver (e.g., acme-missiles-0.3) extra-deps:-  - unbound-generics-0.4.2-    # unbound-generics-0.4.3 contains breaking changes (adding methods to Subst class)+  - unbound-generics-0.4.4+  - ansi-wl-pprint-0.6.9   - simple-enumeration-0.2.1@sha256:8625b269c1650d3dd0e3887351c153049f4369853e0d525219e07480ea004b9f,1178-  - polysemy-zoo-0.8.2.0-    # - HTTP-4000.3.16@sha256:6042643c15a0b43e522a6693f1e322f05000d519543a84149cb80aeffee34f71,5947-    # HTTP-4000.3 needed for oeis-0.3.10+  - oeis2-1.0.9  # Override default flag values for local packages and extra-deps flags: {}

@@ -1,43 +1,47 @@ module Main where -import           Control.Monad              (filterM)-import qualified Data.ByteString            as BS-import           Data.Function              (on)-import           Data.List                  (groupBy, sort)-import           System.Directory           (doesFileExist,-                                             getDirectoryContents)-import           System.FilePath            (isPathSeparator, (</>))-import           System.IO                  (hGetContents)-import           System.Process             (StdStream (CreatePipe),-                                             createProcess, shell, std_out,-                                             system)-import           Text.Printf--import           Test.Tasty-import           Test.Tasty.Golden.Advanced+import Control.Monad (filterM, void)+import qualified Data.ByteString as BS+import Data.Function (on)+import Data.List (sort)+import qualified Data.List.NonEmpty as NE+import System.Directory (+  doesFileExist,+  getDirectoryContents,+ )+import System.FilePath (isPathSeparator, (</>))+import System.IO (hGetContents)+import System.Process (+  StdStream (CreatePipe),+  createProcess,+  shell,+  std_out,+  system,+ )+import Test.Tasty+import Test.Tasty.Golden.Advanced+import Text.Printf  main :: IO () main = do-  testDirs <- getDirectoryContents "test"-    >>= filterM (doesFileExist . (\d -> ("test" </> d </> "input")))-  let testDirs'-        = groupBy ((==) `on` extractGroup)-        . sort-        . filter (\f -> f /= "." && f /= "..")-        $ testDirs+  testDirs <-+    getDirectoryContents "test"+      >>= filterM (doesFileExist . (\d -> "test" </> d </> "input"))+  let testDirs' =+        NE.groupBy ((==) `on` extractGroup)+          . sort+          . filter (\f -> f /= "." && f /= "..")+          $ testDirs   let testTree = testGroup "disco" $ map mkGroup testDirs'   defaultMain testTree-  where-    mkGroup ds = testGroup (extractGroup (head ds)) $ map mkGolden ds-      -- (head ds) is safe since mkGroup is called on testDirs', which-      -- is the output of groupBy, so each element of testDirs' will-      -- be a non-empty list.+ where+  mkGroup ds = testGroup (extractGroup (NE.head ds)) $ map mkGolden (NE.toList ds)  extractGroup :: FilePath -> String-extractGroup = takeWhile (/='-')+extractGroup = takeWhile (/= '-')  extractName :: FilePath -> String-extractName = takeWhile (not . isPathSeparator) . drop 1 . dropWhile (/='-')+extractName = takeWhile (not . isPathSeparator) . drop 1 . dropWhile (/= '-')  mkGolden :: FilePath -> TestTree mkGolden relDir =@@ -45,19 +49,24 @@     (extractName relDir)     (dir </> "expected")     (dir </> "output")-    (system ("disco -f " ++ (dir </> "input") ++ " > " ++ (dir </> "output")) >> return ())-  where-    dir = "test" </> relDir+    (void $ system ("disco -f " ++ (dir </> "input") ++ " > " ++ (dir </> "output")))+ where+  dir = "test" </> relDir  -- | A variant of goldenVsFile that prints the result of @diff@ if --   the files are different, so we don't have to manually call @diff@ --   every time there is a test failure.-goldenVsFileWithDiff-  :: TestName -- ^ test name-  -> FilePath -- ^ path to the «golden» file (the file that contains correct output)-  -> FilePath -- ^ path to the output file-  -> IO ()    -- ^ action that creates the output file-  -> TestTree -- ^ the test verifies that the output file contents is the same as the golden file contents+goldenVsFileWithDiff ::+  -- | test name+  TestName ->+  -- | path to the «golden» file (the file that contains correct output)+  FilePath ->+  -- | path to the output file+  FilePath ->+  -- | action that creates the output file+  IO () ->+  -- | the test verifies that the output file contents is the same as the golden file contents+  TestTree goldenVsFileWithDiff name ref new act =   goldenTest     name@@ -65,7 +74,7 @@     (act >> BS.readFile new)     cmp     upd-  where+ where   cmp = cmpWithDiff ref new   upd = BS.writeFile ref @@ -74,10 +83,12 @@   if x == y     then return Nothing     else do-      (_, Just hout, _, _)-        <- createProcess (shell $ printf "diff %s %s" f1 f2) { std_out = CreatePipe }+      (_, Just hout, _, _) <-+        createProcess (shell $ printf "diff %s %s" f1 f2) {std_out = CreatePipe}       diffStr <- hGetContents hout-      return $ Just $ unlines-        [ printf "Files '%s' and '%s' differ:" f1 f2-        , diffStr-        ]+      return $+        Just $+          unlines+            [ printf "Files '%s' and '%s' differ:" f1 f2+            , diffStr+            ]

@@ -17,7 +17,9 @@ -6 Error: that number would not even fit in the universe! -9+This expression has multiple possible types.  Some examples: -~ : ℤ → ℤ+-~ : ℚ → ℚ -3 : ℤ -(3 : ℕ) : ℤ -(3 : 𝔽) : ℚ

@@ -17,10 +17,10 @@ 1 10 45-true-true+T+T 12600-true+T 2520 0 3628800

@@ -1,12 +1,12 @@ 3 3-true-true-true-true-true-false-false-false-true-true+T+T+T+T+T+F+F+F+T+T

@@ -1,4 +1,4 @@-holds (∀ℕ. (λarg0. (λ_. (λk. (λx. test [(x, ℕ, x)] (3 < x)) arg0) (λ_1. matchErr)) unit))+holds (∀ℕ. (λarg0. (λ_. (λk. (λx. test [(x, ℕ, x)] (x !> 3)) arg0) (λ_1. matchErr)) unit)) λx, y. x (λ_. (λk. (λy. (λp, q. p) (fst y) (snd y)) (frac (2 / 3))) (λ_1. matchErr)) unit (λ_. (λk. case (3 < 2) of {

@@ -1,4 +1,4 @@ {{1, 2}, {1, 3}, {2, 3}}-true+T {⟅1 # 3⟆, ⟅2 # 5⟆}-true+T

@@ -1,5 +1,23 @@+This expression has multiple possible types.  Some examples: λxs. each(λx. x + 1, xs) : List(ℕ) → List(ℕ)+λxs. each(λx. x + 1, xs) : Bag(ℕ) → Bag(ℕ)+λxs. each(λx. x + 1, xs) : Set(ℕ) → Set(ℕ)+λxs. each(λx. x + 1, xs) : List(ℤ) → List(ℤ)+λxs. each(λx. x + 1, xs) : Bag(ℤ) → Bag(ℤ)+λxs. each(λx. x + 1, xs) : Set(ℤ) → Set(ℤ)+λxs. each(λx. x + 1, xs) : List(𝔽) → List(𝔽)+λxs. each(λx. x + 1, xs) : Bag(𝔽) → Bag(𝔽)+...+This expression has multiple possible types.  Some examples: λxs. each(list, xs) : List(List(a)) → List(List(a))+λxs. each(list, xs) : List(Bag(a)) → List(List(a))+λxs. each(list, xs) : List(Set(a)) → List(List(a))+λxs. each(list, xs) : Bag(List(a)) → Bag(List(a))+λxs. each(list, xs) : Bag(Bag(a)) → Bag(List(a))+λxs. each(list, xs) : Bag(Set(a)) → Bag(List(a))+λxs. each(list, xs) : Set(List(a)) → Set(List(a))+λxs. each(list, xs) : Set(Bag(a)) → Set(List(a))+... each(λx. x + 1, [1, 2, 3]) : List(ℕ) each(λx. x + 1, ⟅1, 2, 3⟆) : Bag(ℕ) each(λx. x + 1, {1, 2, 3}) : Set(ℕ)

@@ -1,9 +1,9 @@ using primitives $merge(~+~, bag [1,1,2,2,2], bag [2,2,3,3]) $merge(~.-~, bag [1,1,2,2,2], bag [2,2,3,3])-$merge(~min~, bag [1,1,2,2,2], bag [2,2,3,3])-$merge(~max~, bag [1,1,2,2,2], bag [2,2,3,3])-$merge(~min~, {1,2,3}, {2,4})-$merge(~max~, {1,2,3}, {2,4})+$merge(min, bag [1,1,2,2,2], bag [2,2,3,3])+$merge(max, bag [1,1,2,2,2], bag [2,2,3,3])+$merge(min, {1,2,3}, {2,4})+$merge(max, {1,2,3}, {2,4}) $merge(~.-~, {1,2,3}, {2,4}) $merge(\p. {? (x + y) mod 2 when p is (x,y) ?}, {1,2,3}, {2,4})

@@ -8,9 +8,9 @@ {(1, 10), (1, 20), (1, 30), (2, 10), (2, 20), (2, 30)} {(1, 10), (1, 20), (1, 30), (2, 10), (2, 20), (2, 30)} {1}-true-true-true+T+T+T {{}, {1}, {1, 2}, {1, 2, 3}, {1, 3}, {2}, {2, 3}, {3}} {{}} {{}, {1}}@@ -29,31 +29,31 @@ ⟅⟆ ⟅2 # 2, 3, 5⟆ ⟅1⟆-true-true-true+T+T+T ⟅⟅⟆⟆ ⟅⟅⟆, ⟅1⟆⟆ ⟅⟅⟆, ⟅1⟆, ⟅1, 2⟆, ⟅2⟆⟆ ⟅⟅⟆, ⟅'a'⟆, ⟅'a', 'b'⟆ # 2, ⟅'a', 'b' # 2⟆, ⟅'b'⟆ # 2, ⟅'b' # 2⟆⟆ ⟅⟅⟆, ⟅'a'⟆ # 2, ⟅'a', 'b'⟆ # 6, ⟅'a', 'b' # 2⟆ # 6, ⟅'a', 'b' # 3⟆ # 2, ⟅'a' # 2⟆, ⟅'a' # 2, 'b'⟆ # 3, ⟅'a' # 2, 'b' # 2⟆ # 3, ⟅'a' # 2, 'b' # 3⟆, ⟅'b'⟆ # 3, ⟅'b' # 2⟆ # 3, ⟅'b' # 3⟆⟆ [(2, 3), (2, 4), (2, 4), (1, 3), (1, 4), (1, 4)]-true-true-false-false-true-false-false-true-true-true-false-false-true-false-true-true+T+T+F+F+T+F+F+T+T+T+F+F+T+F+T+T ⟅'x' # 3, 'y' # 2⟆ ⟅'x' # 3, 'y'⟆ ⟅'x', 'y'⟆

@@ -4,12 +4,15 @@   dummy: OK   setSize2: OK Loaded.+This expression has multiple possible types.  Some examples: reduce : (a × a → a) × a × List(a) → a+reduce : (a × a → a) × a × Bag(a) → a+reduce : (a × a → a) × a × Set(a) → a reduce(~+~, 0, [1 .. 10]) : ℕ 55 60-true+T 2351 6 7-true+T

@@ -0,0 +1,5 @@+Error: division by zero.+Error: division by zero.+1+0+1/25

@@ -0,0 +1,5 @@+0^(-2)+0^(-1)+0^0+0^1+5^(-2)

@@ -1,1 +1,1 @@-type T(a,b) = Unit + a*b+type X(a,b) = Unit + a*b

@@ -1,10 +1,10 @@ Loading error-tyargs.disco... Loaded.-Error: not enough arguments for the type 'T'.+Error: not enough arguments for the type 'X'. https://disco-lang.readthedocs.io/en/latest/reference/num-args-type.html-Error: not enough arguments for the type 'T'.+Error: not enough arguments for the type 'X'. https://disco-lang.readthedocs.io/en/latest/reference/num-args-type.html-Error: too many arguments for the type 'T'.+Error: too many arguments for the type 'X'. https://disco-lang.readthedocs.io/en/latest/reference/num-args-type.html Error: not enough arguments for the type 'List'. https://disco-lang.readthedocs.io/en/latest/reference/num-args-type.html

@@ -1,7 +1,7 @@ :load test/error-tyargs/error-tyargs.disco-x : T-y : T(Int)-z : T(Int,Char)-w : T(Int,Char,Bool)+x : X+y : X(Int)+z : X(Int,Char)+w : X(Int,Char,Bool) q : List p : List(Int,Char)

@@ -1,1 +1,15 @@ Error: encountered undefined name REPL.even. Maybe you haven't defined it yet?+Error: there is nothing named fo.+Perhaps you meant 'foo'?+https://disco-lang.readthedocs.io/en/latest/reference/unbound.html+Error: there is nothing named ofo.+Perhaps you meant 'foo'?+https://disco-lang.readthedocs.io/en/latest/reference/unbound.html+Error: there is nothing named for.+Perhaps you meant 'foo' or 'or'?+https://disco-lang.readthedocs.io/en/latest/reference/unbound.html+Error: there is nothing named oof.+https://disco-lang.readthedocs.io/en/latest/reference/unbound.html+Error: there is nothing named Foo.+Perhaps you meant 'foo'?+https://disco-lang.readthedocs.io/en/latest/reference/unbound.html

@@ -1,2 +1,9 @@ even : Z -> Bool even(2)+foo : N+foo = 3+fo + 1+ofo + 1+for + 1+oof + 1+Foo + 1

@@ -1,4 +1,5 @@ Loading unboundtyvar.disco...-While checking unboundtyvar.T:+While checking unboundtyvar.Ty:   Error: Unknown type variable 'b'.+  Perhaps you meant 'a'?   https://disco-lang.readthedocs.io/en/latest/reference/unbound-tyvar.html

@@ -1,1 +1,1 @@-type T(a) = a + b+type Ty(a) = a + b

@@ -1,4 +1,7 @@+This expression has multiple possible types.  Some examples: emptyGraph : Graph(ℕ)+emptyGraph : Graph(Bool)+emptyGraph : Graph(Char) emptyGraph vertex(1) : Graph(ℕ) vertex(1)

@@ -1,4 +1,4 @@-true-true-true-true+T+T+T+T

@@ -12,7 +12,7 @@ [10, 9, 8, 7, 6] [1, 3, 6, 10, 15, 21] [1, 4, 9, 16, 25, 36]-true+T [] [1, 3, 4, 4, 3, 1, -2, -6, -11, -17] [1, 3/2, 2, 5/2, 3]@@ -26,6 +26,6 @@ [2, 3 .. -6] : List(ℤ) [2, 3 .. 8 / 3] : List(𝔽) [-2, 3 .. 8 / 3] : List(ℚ)-[1.5]+[3/2] [1, 2, 3, 4, 5] [1, 2, 3, 4, 5]

@@ -1,32 +1,34 @@-true-false-true-false-true-false-false-false-false-false-true-true-true-false-true-true-false-true-true-false-true-true-true-false-true-true-true-false-false-true-false-false+T+F+T+F+T+F+T+F+F+F+F+F+T+T+T+F+T+T+F+T+T+F+T+T+T+F+T+T+T+F+F+T+F+F

@@ -2,6 +2,8 @@ false True False+T+F true and true true and false false and true

@@ -1,46 +1,46 @@-true-false-false-true-true-true-false-false-true-false-false-true-true-false-false-false-true-true-false-true-false-true-true-false-true-false-true-false-false-true-true-true-false-true-false-true-true-false-true-true-false-false-true+T+F+F+T+T+T+F+F+T+F+F+T+T+F+F+F+T+T+F+T+F+T+T+F+T+F+T+F+F+T+T+T+F+T+F+T+T+F+T+T+F+F+T 3 5 1