disco 0.1.5 → 0.1.6

raw patch · 114 files changed

+10317/−9016 lines, 114 filesdep +prettyprinterdep −oeisdep −prettydep ~algebraic-graphsdep ~arithmoidep ~basePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: prettyprinter

Dependencies removed: oeis, pretty

Dependency ranges changed: algebraic-graphs, arithmoi, base, bytestring, fgl, lens, megaparsec, mtl, optparse-applicative, polysemy, pretty-show, tasty, unbound-generics

API changes (from Hackage documentation)

Files

• CHANGELOG.md +13/−0
• README.md +86/−70
• disco.cabal +41/−31
• example/catalan.disco +0/−19
• example/gcd.disco +2/−0
• example/grid.disco +1/−6
• example/prime.disco +1/−4
• example/tree.disco +1/−1
• lib/oeis.disco +0/−13
• repl/REPL.hs +2/−3
• src/Disco/AST/Core.hs +140/−124
• src/Disco/AST/Desugared.hs +130/−122
• src/Disco/AST/Generic.hs +231/−282
• src/Disco/AST/Surface.hs +366/−288
• src/Disco/AST/Typed.hs +272/−246
• src/Disco/Compile.hs +127/−115
• src/Disco/Context.hs +72/−68
• src/Disco/Data.hs +9/−10
• src/Disco/Desugar.hs +434/−411
• src/Disco/Doc.hs +135/−119
• src/Disco/Effects/Counter.hs +11/−12
• src/Disco/Effects/Fresh.hs +36/−33
• src/Disco/Effects/Input.hs +12/−13
• src/Disco/Effects/LFresh.hs +67/−58
• src/Disco/Effects/Random.hs +12/−12
• src/Disco/Effects/State.hs +15/−13
• src/Disco/Effects/Store.hs +24/−25
• src/Disco/Enumerate.hs +80/−80
• src/Disco/Error.hs +221/−226
• src/Disco/Eval.hs +179/−157
• src/Disco/Extensions.hs +9/−9
• src/Disco/Interactive/CmdLine.hs +152/−132
• src/Disco/Interactive/Commands.hs +413/−367
• src/Disco/Interpret/CESK.hs +324/−293
• src/Disco/Messages.hs +25/−25
• src/Disco/Module.hs +69/−57
• src/Disco/Names.hs +51/−37
• src/Disco/Parser.hs +1258/−1088
• src/Disco/Pretty.hs +56/−64
• src/Disco/Pretty/DSL.hs +55/−54
• src/Disco/Pretty/Prec.hs +4/−4
• src/Disco/Property.hs +142/−18
• src/Disco/Report.hs +15/−17
• src/Disco/Subst.hs +33/−30
• src/Disco/Syntax/Operators.hs +202/−130
• src/Disco/Syntax/Prims.hs +187/−132
• src/Disco/Typecheck.hs +1703/−1680
• src/Disco/Typecheck/Constraints.hs +45/−46
• src/Disco/Typecheck/Erase.hs +74/−69
• src/Disco/Typecheck/Graph.hs +59/−54
• src/Disco/Typecheck/Solve.hs +1182/−1083
• src/Disco/Typecheck/Unify.hs +80/−83
• src/Disco/Typecheck/Util.hs +76/−55
• src/Disco/Types.hs +237/−268
• src/Disco/Types/Qualifiers.hs +47/−36
• src/Disco/Types/Rules.hs +144/−129
• src/Disco/Util.hs +5/−5
• src/Disco/Value.hs +232/−260
• stack.yaml +7/−10
• test/compile-misc/expected +3/−3
• test/containers-filter/expected +0/−1
• test/containers-reduce/containers-reduce.disco +1/−1
• test/error-nonlinear/expected +5/−0
• test/error-nonlinear/input +3/−0
• test/error-parse-RHS/expected +5/−5
• test/error-parse-RHS/input +1/−1
• test/error-pattype/expected +1/−1
• test/lib-oeis/expected +0/−8
• test/lib-oeis/input +0/−22
• test/list-comp/expected +0/−1
• test/list-poly/expected +0/−1
• test/logic-cmp/expected +4/−0
• test/logic-cmp/input +4/−0
• test/map-basic/expected +0/−1
• test/parse-patguard/expected +7/−0
• test/parse-patguard/input +1/−0
• test/parse-quantifiers/expected +78/−19
• test/parse-quantifiers/input +7/−8
• test/poly-bad/input +2/−2
• test/poly-infer-sort/expected +4/−4
• test/poly-infer-sort/input +5/−5
• test/poly-instantiate/expected +9/−9
• test/poly-instantiate/input +9/−9
• test/pretty-issue258/expected +0/−12
• test/pretty-issue258/input +0/−4
• test/prop-basic/expected +5/−5
• test/prop-binary/expected +401/−0
• test/prop-binary/input +49/−0
• test/prop-fail/expected +12/−13
• test/prop-higher-order/expected +5/−14
• test/prop-higher-order/higher-order.disco +2/−24
• test/prop-higher-order/input +1/−1
• test/prop-tests/prop-tests.disco +1/−1
• test/prop-type/expected +3/−6
• test/repl-ann/expected +1/−1
• test/repl-ann/input +1/−1
• test/repl-doc/expected +4/−0
• test/repl-doc/input +1/−0
• test/repl-proptest/expected +7/−7
• test/syntax-clause/input +1/−1
• test/syntax-ellipsis/expected +10/−0
• test/syntax-ellipsis/input +10/−0
• test/syntax-lambda-pat/expected +1/−1
• test/syntax-lambda-pat/input +3/−3
• test/syntax-lambda/expected +10/−2
• test/syntax-lambda/input +5/−4
• test/types-192/expected +1/−1
• test/types-192/input +1/−1
• test/types-306/expected +9/−9
• test/types-357/expected +6/−0
• test/types-357/input +5/−0
• test/types-char-string/expected +1/−1
• test/types-ops/expected +0/−1
• test/types-tydef-param/types-tydef-param.disco +6/−6

@@ -1,3 +1,16 @@+* 0.1.6 (16 December 2023)++  - A bunch more documentation+  - Allow `!=` as a synonym for `/=`+  - Allow `=<` and `=>` as aliases for `<=` and `>=`, respectively+  - Better reporting of test results+  - Load standard library modules immediately on startup+  - `:doc` now works for case expressions, wildcard patterns, `unit`+    and `Unit`+  - Allow optional commas on either side of an ellipsis (#361)+  - Propositions can be combined with binary operators (thanks to+    @cally-cmd)+ * 0.1.5 (12 March 2022)    - Syntax errors in function definitions now result in much more

@@ -5,13 +5,96 @@ 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+-----------------++* Includes those features, and *only* those features, useful in the+  context of a discrete math course. This is *not* intended to be a+  general-purpose language.+* Syntax is as close to standard *mathematical* practice as possible,+  to make it easier for mathematicians to pick up, and to reduce as+  much as possible the incongruity between the language and the+  mathematics being explored and modeled.+* Tooling, error messages, etc. are very important---the language+  needs to be accessible to undergrads with no prior programming+  experience. (However, this principle is, as of yet, only+  that---there is no tooling or nice error messages to speak of.)++Feel free to look around, ask questions, etc.  You can also+[contribute](CONTRIBUTING.md)---collaborators are most welcome.++Community+---------++Check out the disco IRC channel, `#disco-lang` on Libera.Chat.  If+you're not familiar with IRC, you can connect via [this web client](https://kiwiirc.com/nextclient/irc.libera.chat/?nick=Guest?#disco-lang).++Documentation+-------------++Documentation is [hosted on+readthedocs.io](http://disco-lang.readthedocs.io/en/latest/).++Contributing+------------++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 you just want to *use* disco (*i.e.* if you are a student), follow-these instructions.  If you want to *contribute* to disco development,-you should skip to the instructions below about building with stack.+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.+ - 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@@ -110,70 +193,3 @@ workarounds I learn. So even if you encounter a difficulty but figure out the solution youself, let me know --- that way I can include the problem and solution here so others can benefit!--Design principles--------------------* Includes those features, and *only* those features, useful in the-  context of a discrete math course. This is *not* intended to be a-  general-purpose language.-* Syntax is as close to standard *mathematical* practice as possible,-  to make it easier for mathematicians to pick up, and to reduce as-  much as possible the incongruity between the language and the-  mathematics being explored and modeled.-* Tooling, error messages, etc. are very important---the language-  needs to be accessible to undergrads with no prior programming-  experience. (However, this principle is, as of yet, only-  that---there is no tooling or nice error messages to speak of.)--Feel free to look around, ask questions, etc.  You can also-[contribute](CONTRIBUTING.md)---collaborators are most welcome.--Community------------Check out the disco IRC channel, `#disco-lang` on Libera.Chat.  If-you're not familiar with IRC, you can connect via [this web client](https://kiwiirc.com/nextclient/irc.libera.chat/?nick=Guest?#disco-lang).--Documentation----------------Documentation is [hosted on-readthedocs.io](http://disco-lang.readthedocs.io/en/latest/).--Contributing---------------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.

@@ -1,6 +1,6 @@ cabal-version:       2.4 name:                disco-version:             0.1.5+version:             0.1.6 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,14 +12,14 @@ copyright:           Disco team 2016-2022 (see LICENSE) category:            Language -tested-with:         GHC == 8.10.4+tested-with:         GHC ==8.10.7 || ==9.2.5 || ==9.4.3  data-dir:            lib  data-files:          *.disco -extra-source-files:  README.md, CHANGELOG.md, stack.yaml, example/*.disco, repl/*.hs-                     docs/tutorial/example/*.disco+extra-doc-files:     README.md, CHANGELOG.md, example/*.disco, docs/tutorial/example/*.disco+extra-source-files:  stack.yaml, repl/*.hs                      --- TEST FILES BEGIN (updated automatically by add-test-files.hs) ---                      test/README.md                      test/Tests.hs@@ -91,6 +91,8 @@                      test/error-emptycase/input                      test/error-names/expected                      test/error-names/input+                     test/error-nonlinear/expected+                     test/error-nonlinear/input                      test/error-notcon/expected                      test/error-notcon/input                      test/error-notype/expected@@ -132,8 +134,6 @@                      test/interp-strictmatch/bomb.disco                      test/interp-strictmatch/expected                      test/interp-strictmatch/input-                     test/lib-oeis/expected-                     test/lib-oeis/input                      test/list-comp/expected                      test/list-comp/input                      test/list-poly/expected@@ -170,6 +170,8 @@                      test/parse-case-expr/input                      test/parse-nested-list/expected                      test/parse-nested-list/input+                     test/parse-patguard/expected+                     test/parse-patguard/input                      test/parse-quantifiers/expected                      test/parse-quantifiers/input                      test/parse-top-term/expected@@ -189,8 +191,6 @@                      test/pretty-defn/input                      test/pretty-functions/expected                      test/pretty-functions/input-                     test/pretty-issue258/expected-                     test/pretty-issue258/input                      test/pretty-lit/expected                      test/pretty-lit/input                      test/pretty-ops/expected@@ -212,6 +212,8 @@                      test/prop-basic/expected                      test/prop-basic/input                      test/prop-basic/prop-basic.disco+                     test/prop-binary/expected+                     test/prop-binary/input                      test/prop-cmp/expected                      test/prop-cmp/input                      test/prop-fail/bad-tests.disco@@ -280,6 +282,8 @@                      test/syntax-doc/expected                      test/syntax-doc/input                      test/syntax-doc/syntax-doc.disco+                     test/syntax-ellipsis/expected+                     test/syntax-ellipsis/input                      test/syntax-exts/expected                      test/syntax-exts/input                      test/syntax-exts/syntax-exts.disco@@ -315,6 +319,8 @@                      test/types-192/input                      test/types-306/expected                      test/types-306/input+                     test/types-357/expected+                     test/types-357/input                      test/types-bind/expected                      test/types-bind/input                      test/types-char-string/expected@@ -448,34 +454,37 @@   other-modules:       Paths_disco   autogen-modules:     Paths_disco -  build-depends:       base >=4.8 && <4.17,+  build-depends:       base >=4.8 && <4.18,                        filepath,                        directory,-                       mtl >=2.2 && <2.3,-                       megaparsec >= 6.1.1 && < 9.3,+                       mtl >=2.2 && <2.4,+                       megaparsec >= 6.1.1 && < 9.6,                        parser-combinators >= 1.0.0 && < 1.4,-                       pretty >=1.1 && <1.2,+                       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.5,-                       polysemy >= 1.6.0.0 && < 1.8,+                       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+                       polysemy >= 1.6.0.0 && < 1.10,                        polysemy-plugin >= 0.4 && < 0.5,                        polysemy-zoo >= 0.7 && < 0.9,-                       lens >= 4.14 && < 5.2,+                       lens >= 4.14 && < 5.3,                        exact-combinatorics >= 0.2 && < 0.3,-                       arithmoi >= 0.10 && < 0.13,+                       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,                        splitmix >= 0.1 && < 0.2,-                       fgl >= 5.5 && < 5.8,-                       optparse-applicative >= 0.12 && < 0.18,-                       oeis >= 0.3.10,-                       algebraic-graphs >= 0.5,-                       pretty-show >= 1.10+                       fgl >= 5.5 && < 5.9,+                       optparse-applicative >= 0.12 && < 0.19,+                       -- oeis2 < 1.1,+                       algebraic-graphs >= 0.5 && < 0.8,+                       pretty-show >= 1.10 && < 1.11    hs-source-dirs:      src   default-language:    Haskell2010@@ -484,19 +493,20 @@   import:              common   hs-source-dirs:      repl   main-is:             REPL.hs+  ghc-options:         +RTS --io-manager=native -RTS   build-depends:       base,                        disco,                        directory,                        filepath,                        haskeline >=0.8 && <0.9,-                       mtl >=2.2 && <2.3,+                       mtl >=2.2 && <2.4,                        transformers >= 0.4 && < 0.7,-                       megaparsec >= 6.1.1 && < 9.3,+                       megaparsec >= 6.1.1 && < 9.6,                        containers >= 0.5 && < 0.7,-                       unbound-generics >= 0.3 && < 0.5,-                       lens >= 4.14 && < 5.2,-                       optparse-applicative >= 0.12 && < 0.18,-                       oeis >= 0.3.10+                       unbound-generics >= 0.3 && < 0.4.3,+                       lens >= 4.14 && < 5.3,+                       optparse-applicative >= 0.12 && < 0.19+                       -- oeis2 < 1.1    default-language:    Haskell2010 @@ -506,13 +516,13 @@   main-is: Tests.hs   hs-source-dirs: test   ghc-options: -threaded-  build-depends:    base >= 4.7 && < 4.17,-                    tasty >= 0.10 && < 1.5,+  build-depends:    base >= 4.7 && < 4.18,+                    tasty >= 0.10 && < 1.6,                     tasty-golden >= 2.3 && < 2.4,                     directory >= 1.2 && < 1.4,                     filepath >= 1.4 && < 1.5,                     process >= 1.4 && < 1.7,-                    bytestring >= 0.9 && < 0.12,+                    bytestring >= 0.9 && < 0.13,                     disco   default-language: Haskell2010 @@ -522,7 +532,7 @@   main-is: TestExamples.hs   hs-source-dirs: example   ghc-options: -threaded-  build-depends:    base >= 4.7 && < 4.17,+  build-depends:    base >= 4.7 && < 4.18,                     directory >= 1.2 && < 1.4,                     filepath >= 1.4 && < 1.5,                     process >= 1.4 && < 1.7

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

@@ -16,6 +16,8 @@ !!! gcd(7,6)   == 1 !!! gcd(12,18) == 6 !!! gcd(0,0)   == 0+!!! forall a:N, b:N. gcd(a,b) divides a /\ gcd(a,b) divides b+!!! forall a:N, b:N, g:N. (g divides a /\ g divides b) ==> g divides gcd(a,b)  gcd : N * N -> N gcd(a,0) = a

@@ -59,12 +59,7 @@ -- in infinite recursion!  One way that would work is to write the -- test as follows: -!!! forall n:Nat. powerIsoPos (powerIsoPos' (n+1)) == (n+1)---- Alternatively, since 'implies' is lazy (i.e. "short-circuiting"),--- we can write--!!! ∀ n : Nat. (n > 0) ==> powerIsoPos (powerIsoPos' n) == n+-- !!! forall n:Nat. powerIsoPos (powerIsoPos' (n+1)) == (n+1)  powerIsoPos : ℕ×ℕ → ℕ powerIsoPos (x,y) = 2^x * (2y + 1)

@@ -47,7 +47,4 @@ !!! isPrime 113  isPrime : N -> Bool-isPrime n =-  {? false      if n <= 1,-     ld n == n  otherwise-  ?}+isPrime n = (n >= 2) and (ld n == n)

@@ -4,7 +4,7 @@ leaf = left(■)  node : N * Tree * Tree -> Tree-node(x, l, r) = right(x, l, r)+node = right  tree1 : Tree tree1 = node(3, node(5, node(1, leaf, leaf), leaf), node(6, node(2, leaf, leaf), node(8, leaf, leaf)))

@@ -1,13 +0,0 @@-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

@@ -1,5 +1,5 @@ -------------------------------------------------------------------------------- |+-- \| -- Module      :  REPL -- Copyright   :  disco team and contributors -- Maintainer  :  byorgey@gmail.com@@ -7,10 +7,9 @@ -- SPDX-License-Identifier: BSD-3-Clause -- -- A text-based REPL for disco.--- ----------------------------------------------------------------------------- -import           Disco.Interactive.CmdLine+import Disco.Interactive.CmdLine  main :: IO () main = discoMain

@@ -1,10 +1,9 @@-{-# LANGUAGE DeriveAnyClass           #-}-{-# LANGUAGE DeriveDataTypeable       #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE NondecreasingIndentation #-}-{-# LANGUAGE OverloadedStrings        #-}-{-# LANGUAGE UndecidableInstances     #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE UndecidableInstances #-} ------------------------------------------------------------------------------ -- | -- Module      :  Disco.AST.Core -- Copyright   :  disco team and contributors@@ -14,34 +13,35 @@ -- -- Abstract syntax trees representing the desugared, untyped core -- language for Disco.--------------------------------------------------------------------------------module Disco.AST.Core-       ( -- * Core AST-         RationalDisplay(..)-       , Core(..)-       , Op(..), opArity, substQC, substsQC-       )-       where+module Disco.AST.Core (+  -- * Core AST+  RationalDisplay (..),+  Core (..),+  Op (..),+  opArity,+  substQC,+  substsQC,+)+where -import           Control.Lens.Plated-import           Data.Data                        (Data)-import           Data.Data.Lens                   (uniplate)-import qualified Data.Set                         as S-import           GHC.Generics-import           Prelude                          hiding ((<>))-import qualified Prelude                          as P-import           Unbound.Generics.LocallyNameless hiding (LFresh, lunbind)+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 Disco.Effects.LFresh+import Polysemy (Members, Sem)+import Polysemy.Reader -import           Data.Ratio-import           Disco.AST.Generic                (Side, selectSide)-import           Disco.Names                      (QName)-import           Disco.Pretty-import           Disco.Types+import Data.Ratio+import Disco.AST.Generic (Side, selectSide)+import Disco.Names (QName)+import Disco.Pretty+import Disco.Types  -- | A type of flags specifying whether to display a rational number --   as a fraction or a decimal.@@ -51,7 +51,7 @@ instance Semigroup RationalDisplay where   Decimal <> _ = Decimal   _ <> Decimal = Decimal-  _ <> _       = Fraction+  _ <> _ = Fraction  -- | The 'Monoid' instance for 'RationalDisplay' corresponds to the --   idea that the result should be displayed as a decimal if any@@ -231,8 +231,8 @@   | -- | Equality assertion, @=!=@     OShouldEq Type   | -- Other primitives--    -- | Error for non-exhaustive pattern match+    OShouldLt Type+  | -- | Error for non-exhaustive pattern match     OMatchErr   | -- | Crash with a user-supplied message     OCrash@@ -242,6 +242,15 @@     OLookupSeq   | -- | Extend a List via OEIS     OExtendSeq+  | -- | Not the Boolean `And`, but instead a propositional BOp+    -- | Should only be seen and used with Props.+    OAnd+  | -- | Not the Boolean `Or`, but instead a propositional BOp+    -- | Should only be seen and used with Props.+    OOr+  | -- | Not the Boolean `Impl`, but instead a propositional BOp+    -- | Should only be seen and used with Props.+    OImpl   deriving (Show, Generic, Data, Alpha, Eq, Ord)  -- | Get the arity (desired number of arguments) of a function@@ -249,8 +258,8 @@ --   uncurried and hence has arity 1. opArity :: Op -> Int opArity OEmptyGraph = 0-opArity OMatchErr   = 0-opArity _           = 1+opArity OMatchErr = 0+opArity _ = 1  substQC :: QName Core -> Core -> Core -> Core substQC x s = transform $ \case@@ -263,63 +272,66 @@ substsQC xs = transform $ \case   CVar y -> case P.lookup y xs of     Just c -> c-    _      -> CVar y+    _ -> CVar y   t -> t  instance Pretty Core where   pretty = \case-    CVar qn         -> pretty qn+    CVar qn -> pretty qn     CNum _ r       | denominator r == 1 -> text (show (numerator r))-      | otherwise          -> text (show (numerator r)) <> "/" <> text (show (denominator r))+      | otherwise -> text (show (numerator r)) <> "/" <> text (show (denominator r))     CApp (CConst op) (CPair c1 c2)       | isInfix op -> parens (pretty c1 <+> text (opToStr op) <+> pretty c2)     CApp (CConst op) c       | isPrefix op -> text (opToStr op) <> pretty c       | isPostfix op -> pretty c <> text (opToStr op)-    CConst op       -> pretty op-    CInj s c        -> withPA funPA $ selectSide s "left" "right" <+> rt (pretty c)-    CCase c l r     -> do+    CConst op -> pretty op+    CInj s c -> withPA funPA $ selectSide s "left" "right" <+> rt (pretty c)+    CCase c l r -> do       lunbind l $ \(x, lc) -> do-      lunbind r $ \(y, rc) -> do-        "case" <+> pretty c <+> "of {"-          $+$ nest 2 (-            vcat-            [ withPA funPA $ "left" <+> rt (pretty x) <+> "->" <+> pretty lc-            , withPA funPA $ "right" <+> rt (pretty y) <+> "->" <+> pretty rc-            ])-          $+$ "}"-    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+        lunbind r $ \(y, rc) -> do+          nest 2 $+            "case"+              <+> pretty c+              <+> "of {"+              $+$ vcat+                [ withPA funPA $ "left" <+> rt (pretty x) <+> "->" <+> pretty lc+                , withPA funPA $ "right" <+> rt (pretty y) <+> "->" <+> pretty rc+                ]+              $+$ "}"+    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       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-    CType ty        -> pretty ty-    CDelay d        -> withPA initPA $ do+    CApp c1 c2 -> withPA funPA $ lt (pretty c1) <+> rt (pretty c2)+    CTest xs c -> "test" <+> prettyTestVars xs <+> pretty c+    CType ty -> pretty ty+    CDelay d -> withPA initPA $ do       lunbind d $ \(xs, bodies) ->         "delay" <+> intercalate "," (map pretty xs) <> "." <+> pretty (toTuple bodies)-    CForce c        -> withPA funPA $ "force" <+> rt (pretty c)+    CForce c -> withPA funPA $ "force" <+> rt (pretty c)  toTuple :: [Core] -> Core toTuple = foldr CPair CUnit -prettyTestVars :: Members '[Reader PA, LFresh] r => [(String, Type, Name Core)] -> Sem r Doc+prettyTestVars :: Members '[Reader PA, LFresh] r => [(String, Type, Name Core)] -> Sem r (Doc ann) prettyTestVars = brackets . intercalate "," . map prettyTestVar-  where-    prettyTestVar (s, ty, n) = parens (intercalate "," [text s, pretty ty, pretty n])+ where+  prettyTestVar (s, ty, n) = parens (intercalate "," [text s, pretty ty, pretty n])  isInfix, isPrefix, isPostfix :: Op -> Bool-isInfix OShouldEq{} = True-isInfix op = op `S.member` S.fromList-  [ OAdd, OMul, ODiv, OExp, OMod, ODivides, OMultinom, OEq, OLt]-+isInfix OShouldEq {} = True+isInfix OShouldLt {} = True+isInfix op =+  op+    `S.member` S.fromList+      [OAdd, OMul, ODiv, OExp, OMod, ODivides, OMultinom, OEq, OLt, OAnd, OOr, OImpl] isPrefix ONeg = True-isPrefix _    = False-+isPrefix _ = False isPostfix OFact = True-isPostfix _     = False+isPostfix _ = False  instance Pretty Op where   pretty (OForall tys) = "∀" <> intercalate "," (map pretty tys) <> "."@@ -328,63 +340,67 @@     | isInfix op = "~" <> text (opToStr op) <> "~"     | isPrefix op = text (opToStr op) <> "~"     | isPostfix op = "~" <> text (opToStr op)-    | otherwise  = text (opToStr op)+    | otherwise = text (opToStr op)  opToStr :: Op -> String opToStr = \case-  OAdd               -> "+"-  ONeg               -> "-"-  OSqrt              -> "sqrt"-  OFloor             -> "floor"-  OCeil              -> "ceil"-  OAbs               -> "abs"-  OMul               -> "*"-  ODiv               -> "/"-  OExp               -> "^"-  OMod               -> "mod"-  ODivides           -> "divides"-  OMultinom          -> "choose"-  OFact              -> "!"-  OEq                -> "=="-  OLt                -> "<"-  OEnum              -> "enumerate"-  OCount             -> "count"-  OPower             -> "power"-  OBagElem           -> "elem_bag"-  OListElem          -> "elem_list"-  OEachBag           -> "each_bag"-  OEachSet           -> "each_set"-  OFilterBag         -> "filter_bag"-  OMerge             -> "merge"-  OBagUnions         -> "unions_bag"-  OSummary           -> "summary"-  OEmptyGraph        -> "emptyGraph"-  OVertex            -> "vertex"-  OOverlay           -> "overlay"-  OConnect           -> "connect"-  OInsert            -> "insert"-  OLookup            -> "lookup"-  OUntil             -> "until"-  OSetToList         -> "set2list"-  OBagToSet          -> "bag2set"-  OBagToList         -> "bag2list"-  OListToSet         -> "list2set"-  OListToBag         -> "list2bag"-  OBagToCounts       -> "bag2counts"-  OCountsToBag       -> "counts2bag"+  OAdd -> "+"+  ONeg -> "-"+  OSqrt -> "sqrt"+  OFloor -> "floor"+  OCeil -> "ceil"+  OAbs -> "abs"+  OMul -> "*"+  ODiv -> "/"+  OExp -> "^"+  OMod -> "mod"+  ODivides -> "divides"+  OMultinom -> "choose"+  OFact -> "!"+  OEq -> "=="+  OLt -> "<"+  OEnum -> "enumerate"+  OCount -> "count"+  OPower -> "power"+  OBagElem -> "elem_bag"+  OListElem -> "elem_list"+  OEachBag -> "each_bag"+  OEachSet -> "each_set"+  OFilterBag -> "filter_bag"+  OMerge -> "merge"+  OBagUnions -> "unions_bag"+  OSummary -> "summary"+  OEmptyGraph -> "emptyGraph"+  OVertex -> "vertex"+  OOverlay -> "overlay"+  OConnect -> "connect"+  OInsert -> "insert"+  OLookup -> "lookup"+  OUntil -> "until"+  OSetToList -> "set2list"+  OBagToSet -> "bag2set"+  OBagToList -> "bag2list"+  OListToSet -> "list2set"+  OListToBag -> "list2bag"+  OBagToCounts -> "bag2counts"+  OCountsToBag -> "counts2bag"   OUnsafeCountsToBag -> "ucounts2bag"-  OMapToSet          -> "map2set"-  OSetToMap          -> "set2map"-  OIsPrime           -> "isPrime"-  OFactor            -> "factor"-  OFrac              -> "frac"-  OHolds             -> "holds"-  ONotProp           -> "not"-  OShouldEq _        -> "=!="-  OMatchErr          -> "matchErr"-  OCrash             -> "crash"-  OId                -> "id"-  OLookupSeq         -> "lookupSeq"-  OExtendSeq         -> "extendSeq"-  OForall{}          -> "∀"-  OExists{}          -> "∃"+  OMapToSet -> "map2set"+  OSetToMap -> "set2map"+  OIsPrime -> "isPrime"+  OFactor -> "factor"+  OFrac -> "frac"+  OHolds -> "holds"+  ONotProp -> "not"+  OShouldEq _ -> "=!="+  OShouldLt _ -> "!<"+  OMatchErr -> "matchErr"+  OCrash -> "crash"+  OId -> "id"+  OLookupSeq -> "lookupSeq"+  OExtendSeq -> "extendSeq"+  OForall {} -> "∀"+  OExists {} -> "∃"+  OAnd -> "and"+  OOr -> "or"+  OImpl -> "implies"

@@ -1,6 +1,5 @@ {-# LANGUAGE PatternSynonyms #-} ------------------------------------------------------------------------------ -- | -- Module      :  Disco.AST.Desugared -- Copyright   :  disco team and contributors@@ -10,57 +9,51 @@ -- -- Typed abstract syntax trees representing the typechecked, desugared -- Disco language.-----------------------------------------------------------------------------------module Disco.AST.Desugared-       ( -- * Desugared, type-annotated terms-       DTerm-       , pattern DTVar-       , pattern DTPrim-       , pattern DTUnit-       , pattern DTBool-       , pattern DTChar-       , pattern DTNat-       , pattern DTRat-       , pattern DTAbs-       , pattern DTApp-       , pattern DTPair-       , pattern DTCase-       , pattern DTTyOp-       , pattern DTNil-       , pattern DTTest--       , Container(..)-       , DBinding-       , pattern DBinding-         -- * Branches and guards-       , DBranch--       , DGuard-       , pattern DGPat--       , DPattern-       , pattern DPVar-       , pattern DPWild-       , pattern DPUnit-       , pattern DPPair-       , pattern DPInj+module Disco.AST.Desugared (+  -- * Desugared, type-annotated terms+  DTerm,+  pattern DTVar,+  pattern DTPrim,+  pattern DTUnit,+  pattern DTBool,+  pattern DTChar,+  pattern DTNat,+  pattern DTRat,+  pattern DTAbs,+  pattern DTApp,+  pattern DTPair,+  pattern DTCase,+  pattern DTTyOp,+  pattern DTNil,+  pattern DTTest,+  Container (..),+  DBinding,+  pattern DBinding, -       , DProperty-       )-       where+  -- * Branches and guards+  DBranch,+  DGuard,+  pattern DGPat,+  DPattern,+  pattern DPVar,+  pattern DPWild,+  pattern DPUnit,+  pattern DPPair,+  pattern DPInj,+  DProperty,+)+where -import           GHC.Generics+import GHC.Generics -import           Data.Void-import           Unbound.Generics.LocallyNameless+import Data.Void+import Unbound.Generics.LocallyNameless -import           Disco.AST.Generic-import           Disco.Names                      (QName (..))-import           Disco.Syntax.Operators-import           Disco.Syntax.Prims-import           Disco.Types+import Disco.AST.Generic+import Disco.Names (QName (..))+import Disco.Syntax.Operators+import Disco.Syntax.Prims+import Disco.Types  data DS @@ -69,36 +62,37 @@ -- | A @DTerm@ is a term which has been typechecked and desugared, so --   it has fewer constructors and complex features than 'ATerm', but --   still retains typing information.- type DTerm = Term_ DS -type instance X_Binder DS         = Name DTerm+type instance X_Binder DS = Name DTerm -type instance X_TVar DS           = Void -- names are qualified-type instance X_TPrim DS          = Type-type instance X_TLet DS           = Void -- Let gets translated to lambda-type instance X_TUnit DS          = ()-type instance X_TBool DS          = Type-type instance X_TChar DS          = ()-type instance X_TString DS        = Void-type instance X_TNat DS           = Type-type instance X_TRat DS           = ()-type instance X_TAbs DS           = Type -- For lambas this is the function type but-                                         -- for forall/exists it's the argument type-type instance X_TApp DS           = Type-type instance X_TCase DS          = Type-type instance X_TChain DS         = Void -- Chains are translated into conjunctions of-                                         -- binary comparisons-type instance X_TTyOp DS          = Type-type instance X_TContainer DS     = Void -- Literal containers are desugared into-                                         -- conversion functions applied to list literals+type instance X_TVar DS = Void -- names are qualified+type instance X_TPrim DS = Type+type instance X_TLet DS = Void -- Let gets translated to lambda+type instance X_TUnit DS = ()+type instance X_TBool DS = Type+type instance X_TChar DS = ()+type instance X_TString DS = Void+type instance X_TNat DS = Type+type instance X_TRat DS = ()+type instance X_TAbs DS = Type -- For lambas this is the function type but+-- for forall/exists it's the argument type +type instance X_TApp DS = Type+type instance X_TCase DS = Type+type instance X_TChain DS = Void -- Chains are translated into conjunctions of+-- binary comparisons++type instance X_TTyOp DS = Type+type instance X_TContainer DS = Void -- Literal containers are desugared into+-- conversion functions applied to list literals+ type instance X_TContainerComp DS = Void -- Container comprehensions are translated-                                         -- into monadic chains+-- into monadic chains -type instance X_TAscr DS          = Void -- No type ascriptions-type instance X_TTup DS           = Void -- No tuples, only pairs-type instance X_TParens DS        = Void -- No explicit parens+type instance X_TAscr DS = Void -- No type ascriptions+type instance X_TTup DS = Void -- No tuples, only pairs+type instance X_TParens DS = Void -- No explicit parens  -- Extra constructors type instance X_Term DS = X_DTerm@@ -125,7 +119,7 @@ pattern DTBool :: Type -> Bool -> DTerm pattern DTBool ty bool = TBool_ ty bool -pattern DTNat  :: Type -> Integer -> DTerm+pattern DTNat :: Type -> Integer -> DTerm pattern DTNat ty int = TNat_ ty int  pattern DTRat :: Rational -> DTerm@@ -137,7 +131,7 @@ pattern DTAbs :: Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm pattern DTAbs q ty lam = TAbs_ q ty lam -pattern DTApp  :: Type -> DTerm -> DTerm -> DTerm+pattern DTApp :: Type -> DTerm -> DTerm -> DTerm pattern DTApp ty term1 term2 = TApp_ ty term1 term2  pattern DTPair :: Type -> DTerm -> DTerm -> DTerm@@ -158,9 +152,22 @@ pattern DTTest :: [(String, Type, Name DTerm)] -> DTerm -> DTerm pattern DTTest ns t = XTerm_ (DTTest_ ns t) -{-# COMPLETE DTVar, DTPrim, DTUnit, DTBool, DTChar, DTNat, DTRat,-             DTAbs, DTApp, DTPair, DTCase, DTTyOp,-             DTNil, DTTest #-}+{-# COMPLETE+  DTVar+  , DTPrim+  , DTUnit+  , DTBool+  , DTChar+  , DTNat+  , DTRat+  , DTAbs+  , DTApp+  , DTPair+  , DTCase+  , DTTyOp+  , DTNil+  , DTTest+  #-}  type instance X_TLink DS = Void @@ -175,9 +182,9 @@  type DGuard = Guard_ DS -type instance X_GBool DS = Void   -- Boolean guards get desugared to pattern-matching-type instance X_GPat  DS = ()-type instance X_GLet  DS = Void   -- Let gets desugared to 'when' with a variable+type instance X_GBool DS = Void -- Boolean guards get desugared to pattern-matching+type instance X_GPat DS = ()+type instance X_GLet DS = Void -- Let gets desugared to 'when' with a variable  pattern DGPat :: Embed DTerm -> DPattern -> DGuard pattern DGPat embedt pat = GPat_ () embedt pat@@ -186,23 +193,23 @@  type DPattern = Pattern_ DS -type instance X_PVar     DS = Embed Type-type instance X_PWild    DS = Embed Type-type instance X_PAscr    DS = Void-type instance X_PUnit    DS = ()-type instance X_PBool    DS = Void-type instance X_PChar    DS = Void-type instance X_PString  DS = Void-type instance X_PTup     DS = Void-type instance X_PInj     DS = Void-type instance X_PNat     DS = Void-type instance X_PCons    DS = Void-type instance X_PList    DS = Void-type instance X_PAdd     DS = Void-type instance X_PMul     DS = Void-type instance X_PSub     DS = Void-type instance X_PNeg     DS = Void-type instance X_PFrac    DS = Void+type instance X_PVar DS = Embed Type+type instance X_PWild DS = Embed Type+type instance X_PAscr DS = Void+type instance X_PUnit DS = ()+type instance X_PBool DS = Void+type instance X_PChar DS = Void+type instance X_PString DS = Void+type instance X_PTup DS = Void+type instance X_PInj DS = Void+type instance X_PNat DS = Void+type instance X_PCons DS = Void+type instance X_PList DS = Void+type instance X_PAdd DS = Void+type instance X_PMul DS = Void+type instance X_PSub DS = Void+type instance X_PNeg DS = Void+type instance X_PFrac DS = Void  -- In the desugared language, constructor patterns (DPPair, DPInj) can -- only contain variables, not nested patterns.  This means that the@@ -210,10 +217,11 @@ -- exploding nested patterns into sequential guards, which makes the -- interpreter simpler. -type instance X_Pattern  DS =-  Either-    (Embed Type, Name DTerm, Name DTerm)     -- DPPair-    (Embed Type, Side, Name DTerm)           -- DPInj+type instance+  X_Pattern DS =+    Either+      (Embed Type, Name DTerm, Name DTerm) -- DPPair+      (Embed Type, Side, Name DTerm) -- DPInj  pattern DPVar :: Type -> Name DTerm -> DPattern pattern DPVar ty name <- PVar_ (unembed -> ty) name@@ -228,19 +236,19 @@ pattern DPUnit :: DPattern pattern DPUnit = PUnit_ () -pattern DPPair  :: Type -> Name DTerm -> Name DTerm -> DPattern+pattern DPPair :: Type -> Name DTerm -> Name DTerm -> DPattern pattern DPPair ty x1 x2 <- XPattern_ (Left (unembed -> ty, x1, x2))   where     DPPair ty x1 x2 = XPattern_ (Left (embed ty, x1, x2)) -pattern DPInj  :: Type -> Side -> Name DTerm -> DPattern+pattern DPInj :: Type -> Side -> Name DTerm -> DPattern pattern DPInj ty s x <- XPattern_ (Right (unembed -> ty, s, x))   where     DPInj ty s x = XPattern_ (Right (embed ty, s, x))  {-# COMPLETE DPVar, DPWild, DPUnit, DPPair, DPInj #-} -type instance X_QBind  DS = Void+type instance X_QBind DS = Void type instance X_QGuard DS = Void  ------------------------------------------------------------@@ -248,25 +256,25 @@ ------------------------------------------------------------  instance HasType DTerm where-  getType (DTVar ty _)     = ty-  getType (DTPrim ty _)    = ty-  getType DTUnit           = TyUnit-  getType (DTBool ty _)    = ty-  getType (DTChar _)       = TyC-  getType (DTNat ty _)     = ty-  getType (DTRat _)        = TyF+  getType (DTVar ty _) = ty+  getType (DTPrim ty _) = ty+  getType DTUnit = TyUnit+  getType (DTBool ty _) = ty+  getType (DTChar _) = TyC+  getType (DTNat ty _) = ty+  getType (DTRat _) = TyF   getType (DTAbs Lam ty _) = ty-  getType DTAbs{}          = TyProp-  getType (DTApp ty _ _)   = ty-  getType (DTPair ty _ _)  = ty-  getType (DTCase ty _)    = ty-  getType (DTTyOp ty _ _)  = ty-  getType (DTNil ty)       = ty-  getType (DTTest _ _)     = TyProp+  getType DTAbs {} = TyProp+  getType (DTApp ty _ _) = ty+  getType (DTPair ty _ _) = ty+  getType (DTCase ty _) = ty+  getType (DTTyOp ty _ _) = ty+  getType (DTNil ty) = ty+  getType (DTTest _ _) = TyProp  instance HasType DPattern where-  getType (DPVar ty _)    = ty-  getType (DPWild ty)     = ty-  getType DPUnit          = TyUnit+  getType (DPVar ty _) = ty+  getType (DPWild ty) = ty+  getType DPUnit = TyUnit   getType (DPPair ty _ _) = ty-  getType (DPInj ty _ _)  = ty+  getType (DPInj ty _ _) = ty

@@ -1,15 +1,19 @@-{-# LANGUAGE ConstraintKinds      #-}-{-# LANGUAGE DeriveAnyClass       #-}-{-# LANGUAGE DeriveDataTypeable   #-}-{-# LANGUAGE DeriveTraversable    #-}-{-# LANGUAGE OverloadedStrings    #-}-{-# LANGUAGE StandaloneDeriving   #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE UndecidableInstances #-}- -- Orphan Alpha Void instance {-# OPTIONS_GHC -fno-warn-orphans #-}  -----------------------------------------------------------------------------++-----------------------------------------------------------------------------++-- SPDX-License-Identifier: BSD-3-Clause+ -- | -- Module      :  Disco.AST.Generic -- Copyright   :  disco team and contributors@@ -36,128 +40,117 @@ -- underlying type.  Particular instantiations of the generic -- framework here can be found in "Disco.AST.Surface", -- "Disco.AST.Typed", and "Disco.AST.Desugared".---------------------------------------------------------------------------------- SPDX-License-Identifier: BSD-3-Clause--module Disco.AST.Generic-       ( -- * Telescopes--         Telescope (..), telCons-       , foldTelescope, mapTelescope-       , traverseTelescope-       , toTelescope, fromTelescope--         -- * Utility types--       , Side (..), selectSide, fromSide-       , Container (..)-       , Ellipsis (..)--         -- * Term--       , Term_ (..)--       , X_TVar-       , X_TPrim-       , X_TLet-       , X_TParens-       , X_TUnit-       , X_TBool-       , X_TNat-       , X_TRat-       , X_TChar-       , X_TString-       , X_TAbs-       , X_TApp-       , X_TTup-       , X_TCase-       , X_TChain-       , X_TTyOp-       , X_TContainer-       , X_TContainerComp-       , X_TAscr-       , X_Term--       , ForallTerm--       -- * Link--       , Link_ (..)-       , X_TLink-       , ForallLink--       -- * Qual--       , Qual_ (..)-       , X_QBind-       , X_QGuard-       , ForallQual--       -- * Binding+module Disco.AST.Generic (+  -- * Telescopes+  Telescope (..),+  telCons,+  foldTelescope,+  mapTelescope,+  traverseTelescope,+  toTelescope,+  fromTelescope, -       , Binding_ (..)+  -- * Utility types+  Side (..),+  selectSide,+  fromSide,+  Container (..),+  Ellipsis (..), -       -- * Branch-       , Branch_+  -- * Term+  Term_ (..),+  X_TVar,+  X_TPrim,+  X_TLet,+  X_TParens,+  X_TUnit,+  X_TBool,+  X_TNat,+  X_TRat,+  X_TChar,+  X_TString,+  X_TAbs,+  X_TApp,+  X_TTup,+  X_TCase,+  X_TChain,+  X_TTyOp,+  X_TContainer,+  X_TContainerComp,+  X_TAscr,+  X_Term,+  ForallTerm, -       -- * Guard+  -- * Link+  Link_ (..),+  X_TLink,+  ForallLink, -       , Guard_ (..)-       , X_GBool-       , X_GPat-       , X_GLet-       , ForallGuard+  -- * Qual+  Qual_ (..),+  X_QBind,+  X_QGuard,+  ForallQual, -       -- * Pattern+  -- * Binding+  Binding_ (..), -       , Pattern_ (..)-       , X_PVar-       , X_PWild-       , X_PAscr-       , X_PUnit-       , X_PBool-       , X_PTup-       , X_PInj-       , X_PNat-       , X_PChar-       , X_PString-       , X_PCons-       , X_PList-       , X_PAdd-       , X_PMul-       , X_PSub-       , X_PNeg-       , X_PFrac-       , X_Pattern-       , ForallPattern+  -- * Branch+  Branch_, -       -- * Quantifiers+  -- * Guard+  Guard_ (..),+  X_GBool,+  X_GPat,+  X_GLet,+  ForallGuard, -       , Quantifier(..)-       , Binder_-       , X_Binder+  -- * Pattern+  Pattern_ (..),+  X_PVar,+  X_PWild,+  X_PAscr,+  X_PUnit,+  X_PBool,+  X_PTup,+  X_PInj,+  X_PNat,+  X_PChar,+  X_PString,+  X_PCons,+  X_PList,+  X_PAdd,+  X_PMul,+  X_PSub,+  X_PNeg,+  X_PFrac,+  X_Pattern,+  ForallPattern, -       -- * Property+  -- * Quantifiers+  Quantifier (..),+  Binder_,+  X_Binder, -       , Property_-       )-       where+  -- * Property+  Property_,+)+where -import           Control.Lens.Plated-import           Data.Data                        (Data)-import           Data.Data.Lens                   (uniplate)-import           Data.Typeable-import           GHC.Exts                         (Constraint)-import           GHC.Generics                     (Generic)+import Control.Lens.Plated+import Data.Data (Data)+import Data.Data.Lens (uniplate)+import Data.Typeable+import GHC.Exts (Constraint)+import GHC.Generics (Generic) -import           Data.Void-import           Unbound.Generics.LocallyNameless+import Data.Void+import Unbound.Generics.LocallyNameless -import           Disco.Pretty-import           Disco.Syntax.Operators-import           Disco.Syntax.Prims-import           Disco.Types+import Disco.Pretty+import Disco.Syntax.Operators+import Disco.Syntax.Prims+import Disco.Types  ------------------------------------------------------------ -- Telescopes@@ -166,13 +159,11 @@ -- | A telescope is essentially a list, except that each item can bind --   names in the rest of the list. data Telescope b where-   -- | The empty telescope.   TelEmpty :: Telescope b-   -- | A binder of type @b@ followed by zero or more @b@'s.  This @b@   --   can bind variables in the subsequent @b@'s.-  TelCons  :: Rebind b (Telescope b) -> Telescope b+  TelCons :: Rebind b (Telescope b) -> Telescope b   deriving (Show, Generic, Alpha, Subst t, Data)  -- | Add a new item to the beginning of a 'Telescope'.@@ -182,17 +173,19 @@ -- | Fold a telescope given a combining function and a value to use --   for the empty telescope.  Analogous to 'foldr' for lists. foldTelescope :: Alpha b => (b -> r -> r) -> r -> Telescope b -> r-foldTelescope _ z TelEmpty                       = z-foldTelescope f z (TelCons (unrebind -> (b,bs))) = f b (foldTelescope f z bs)+foldTelescope _ z TelEmpty = z+foldTelescope f z (TelCons (unrebind -> (b, bs))) = f b (foldTelescope f z bs)  -- | Apply a function to every item in a telescope. mapTelescope :: (Alpha a, Alpha b) => (a -> b) -> Telescope a -> Telescope b mapTelescope f = toTelescope . map f . fromTelescope  -- | Traverse over a telescope.-traverseTelescope-  :: (Applicative f, Alpha a, Alpha b)-  => (a -> f b) -> Telescope a -> f (Telescope b)+traverseTelescope ::+  (Applicative f, Alpha a, Alpha b) =>+  (a -> f b) ->+  Telescope a ->+  f (Telescope b) traverseTelescope f = foldTelescope (\a ftb -> telCons <$> f a <*> ftb) (pure TelEmpty)  -- | Convert a list to a telescope.@@ -230,8 +223,8 @@ --   lists, bags, and sets. data Container where   ListContainer :: Container-  BagContainer  :: Container-  SetContainer  :: Container+  BagContainer :: Container+  SetContainer :: Container   deriving (Show, Eq, Enum, Generic, Data, Alpha, Subst t)  -- | An ellipsis is an "omitted" part of a literal container (such as@@ -240,7 +233,7 @@ --   containers must be finite. data Ellipsis t where   -- | 'Until' represents an ellipsis with a given endpoint, as in @[3 .. 20]@.-  Until   :: t -> Ellipsis t   -- @.. t@+  Until :: t -> Ellipsis t -- @.. t@   deriving (Show, Generic, Functor, Foldable, Traversable, Alpha, Subst a, Data)  ------------------------------------------------------------@@ -276,43 +269,32 @@ --   example, in the typed phase many constructors store an extra --   type, giving the type of the term. data Term_ e where-   -- | A term variable.-  TVar_   :: X_TVar e -> Name (Term_ e) -> Term_ e-+  TVar_ :: X_TVar e -> Name (Term_ e) -> Term_ e   -- | A primitive, /i.e./ a constant  which is interpreted specially   --   at runtime.  See "Disco.Syntax.Prims".-  TPrim_  :: X_TPrim e -> Prim -> Term_ e-+  TPrim_ :: X_TPrim e -> Prim -> Term_ e   -- | A (non-recursive) let expression, @let x1 = t1, x2 = t2, ... in t@.-  TLet_   :: X_TLet e -> Bind (Telescope (Binding_ e)) (Term_ e) -> Term_ e-+  TLet_ :: X_TLet e -> Bind (Telescope (Binding_ e)) (Term_ e) -> Term_ e   -- | Explicit parentheses.  We need to keep track of these in the   --   surface syntax in order to syntactically distinguish   --   multiplication and function application.  However, note that   --   these disappear after the surface syntax phase.   TParens_ :: X_TParens e -> Term_ e -> Term_ e-   -- | The unit value, (), of type Unit.-  TUnit_  :: X_TUnit e -> Term_ e-+  TUnit_ :: X_TUnit e -> Term_ e   -- | A boolean value.-  TBool_  :: X_TBool e -> Bool -> Term_ e-+  TBool_ :: X_TBool e -> Bool -> Term_ e   -- | A natural number.-  TNat_   :: X_TNat e -> Integer -> Term_ e-+  TNat_ :: X_TNat e -> Integer -> Term_ e   -- | A nonnegative rational number, parsed as a decimal.  (Note   --   syntax like @3/5@ does not parse as a rational, but rather as   --   the application of a division operator to two natural numbers.)-  TRat_   :: X_TRat e -> Rational -> Term_ e-+  TRat_ :: X_TRat e -> Rational -> Term_ e   -- | A literal unicode character, /e.g./ @'d'@.-  TChar_  :: X_TChar e -> Char -> Term_ e-+  TChar_ :: X_TChar e -> Char -> Term_ e   -- | A string literal, /e.g./ @"disco"@.   TString_ :: X_TString e -> [Char] -> Term_ e-   -- | A binding abstraction, of the form @Q vars. expr@ where @Q@ is   --   a quantifier and @vars@ is a list of bound variables and   --   optional type annotations.  In particular, this could be a@@ -320,77 +302,68 @@   --   (y:N). 2x + y@), a universal quantifier (@forall x, (y:N). x^2 +   --   y > 0@), or an existential quantifier (@exists x, (y:N). x^2 + y   --   == 0@).-  TAbs_   :: Quantifier -> X_TAbs e -> Binder_ e (Term_ e) -> Term_ e-+  TAbs_ :: Quantifier -> X_TAbs e -> Binder_ e (Term_ e) -> Term_ e   -- | Function application, @t1 t2@.-  TApp_   :: X_TApp e -> Term_ e -> Term_ e -> Term_ e-+  TApp_ :: X_TApp e -> Term_ e -> Term_ e -> Term_ e   -- | An n-tuple, @(t1, ..., tn)@.-  TTup_   :: X_TTup e -> [Term_ e] -> Term_ e-+  TTup_ :: X_TTup e -> [Term_ e] -> Term_ e   -- | A case expression.-  TCase_  :: X_TCase e -> [Branch_ e] -> Term_ e-+  TCase_ :: X_TCase e -> [Branch_ e] -> Term_ e   -- | A chained comparison, consisting of a term followed by one or   --   more "links", where each link is a comparison operator and   --   another term.   TChain_ :: X_TChain e -> Term_ e -> [Link_ e] -> Term_ e-   -- | An application of a type operator.-  TTyOp_  :: X_TTyOp e -> TyOp -> Type -> Term_ e-+  TTyOp_ :: X_TTyOp e -> TyOp -> Type -> Term_ e   -- | A containter literal (set, bag, or list).   TContainer_ :: X_TContainer e -> Container -> [(Term_ e, Maybe (Term_ e))] -> Maybe (Ellipsis (Term_ e)) -> Term_ e-   -- | A container comprehension.   TContainerComp_ :: X_TContainerComp e -> Container -> Bind (Telescope (Qual_ e)) (Term_ e) -> Term_ e-   -- | Type ascription, @(Term_ e : type)@.-  TAscr_  :: X_TAscr e -> Term_ e -> PolyType -> Term_ e-+  TAscr_ :: X_TAscr e -> Term_ e -> PolyType -> Term_ e   -- | A data constructor with an extension descriptor that a "concrete"   --   implementation of a generic AST may use to carry extra information.-  XTerm_   :: X_Term e -> Term_ e+  XTerm_ :: X_Term e -> Term_ e   deriving (Generic)  -- A type that abstracts over constraints for generic data constructors. -- This makes it easier to derive typeclass instances for generic types.-type ForallTerm (a :: * -> Constraint) e-  = ( a (X_TVar e)-    , a (X_TPrim e)-    , a (X_TLet e)-    , a (X_TParens e)-    , a (X_TUnit e)-    , a (X_TBool e)-    , a (X_TNat e)-    , a (X_TRat e)-    , a (X_TChar e)-    , a (X_TString e)-    , a (X_TAbs e)-    , a (X_TApp e)-    , a (X_TCase e)-    , a (X_TTup e)-    , a (X_TChain e)-    , a (X_TTyOp e)-    , a (X_TContainer e)-    , a (X_TContainerComp e)-    , a (X_TAscr e)-    , a (X_Term e)-    , a (Qual_ e)-    , a (Guard_ e)-    , a (Link_ e)-    , a (Binding_ e)-    , a (Pattern_ e)-    , a (Binder_ e (Term_ e))-    )+type ForallTerm (a :: * -> Constraint) e =+  ( a (X_TVar e)+  , a (X_TPrim e)+  , a (X_TLet e)+  , a (X_TParens e)+  , a (X_TUnit e)+  , a (X_TBool e)+  , a (X_TNat e)+  , a (X_TRat e)+  , a (X_TChar e)+  , a (X_TString e)+  , a (X_TAbs e)+  , a (X_TApp e)+  , a (X_TCase e)+  , a (X_TTup e)+  , a (X_TChain e)+  , a (X_TTyOp e)+  , a (X_TContainer e)+  , a (X_TContainerComp e)+  , a (X_TAscr e)+  , a (X_Term e)+  , a (Qual_ e)+  , a (Guard_ e)+  , a (Link_ e)+  , a (Binding_ e)+  , a (Pattern_ e)+  , a (Binder_ e (Term_ e))+  )  deriving instance ForallTerm Show e => Show (Term_ e) instance   ( Typeable e   , ForallTerm (Subst Type) e   , ForallTerm Alpha e-  )-  => Subst Type (Term_ e)+  ) =>+  Subst Type (Term_ e) instance (Typeable e, ForallTerm Alpha e) => Alpha (Term_ e) deriving instance (Data e, Typeable e, ForallTerm Data e) => Data (Term_ e) @@ -407,19 +380,18 @@ --   followed by a sequence of links makes up a comparison chain, such --   as @2 < x < y < 10@. data Link_ e where-   -- | Note that although the type of 'TLink_' says it can hold any   --   'BOp', it should really only hold comparison operators.   TLink_ :: X_TLink e -> BOp -> Term_ e -> Link_ e-  deriving Generic+  deriving (Generic) -type ForallLink (a :: * -> Constraint) e-  = ( a (X_TLink e)-    , a (Term_ e)-    )+type ForallLink (a :: * -> Constraint) e =+  ( a (X_TLink e)+  , a (Term_ e)+  ) -deriving instance ForallLink Show e         => Show       (Link_ e)-instance          ForallLink (Subst Type) e => Subst Type (Link_ e)+deriving instance ForallLink Show e => Show (Link_ e)+instance ForallLink (Subst Type) e => Subst Type (Link_ e) instance (Typeable e, Show (Link_ e), ForallLink Alpha e) => Alpha (Link_ e) deriving instance (Typeable e, Data e, ForallLink Data e) => Data (Link_ e) @@ -434,23 +406,20 @@ --   of qualifiers. Each qualifier either binds a variable to some --   collection or consists of a boolean guard. data Qual_ e where-   -- | A binding qualifier (i.e. @x in t@).-  QBind_   :: X_QBind e -> Name (Term_ e) -> Embed (Term_ e) -> Qual_ e-+  QBind_ :: X_QBind e -> Name (Term_ e) -> Embed (Term_ e) -> Qual_ e   -- | A boolean guard qualfier (i.e. @x + y > 4@).-  QGuard_  :: X_QGuard e -> Embed (Term_ e) -> Qual_ e--  deriving Generic+  QGuard_ :: X_QGuard e -> Embed (Term_ e) -> Qual_ e+  deriving (Generic) -type ForallQual (a :: * -> Constraint) e-  = ( a (X_QBind e)-    , a (X_QGuard e)-    , a (Term_ e)-    )+type ForallQual (a :: * -> Constraint) e =+  ( a (X_QBind e)+  , a (X_QGuard e)+  , a (Term_ e)+  ) -deriving instance ForallQual Show         e => Show       (Qual_ e)-instance          ForallQual (Subst Type) e => Subst Type (Qual_ e)+deriving instance ForallQual Show e => Show (Qual_ e)+instance ForallQual (Subst Type) e => Subst Type (Qual_ e) instance (Typeable e, ForallQual Alpha e) => Alpha (Qual_ e) deriving instance (Typeable e, Data e, ForallQual Data e) => Data (Qual_ e) @@ -463,7 +432,7 @@ data Binding_ e = Binding_ (Maybe (Embed PolyType)) (Name (Term_ e)) (Embed (Term_ e))   deriving (Generic) -deriving instance ForallTerm Show  e => Show (Binding_ e)+deriving instance ForallTerm Show e => Show (Binding_ e) instance Subst Type (Term_ e) => Subst Type (Binding_ e) instance (Typeable e, Show (Binding_ e), Alpha (Term_ e)) => Alpha (Binding_ e) deriving instance (Typeable e, Data e, ForallTerm Data e) => Data (Binding_ e)@@ -475,7 +444,6 @@ -- | A branch of a case is a list of guards with an accompanying term. --   The guards scope over the term.  Additionally, each guard scopes --   over subsequent guards.- type Branch_ e = Bind (Telescope (Guard_ e)) (Term_ e)  ------------------------------------------------------------@@ -488,29 +456,25 @@  -- | Guards in case expressions. data Guard_ e where-   -- | Boolean guard (@if <test>@)   GBool_ :: X_GBool e -> Embed (Term_ e) -> Guard_ e-   -- | Pattern guard (@when term = pat@)-  GPat_  :: X_GPat e -> Embed (Term_ e) -> Pattern_ e -> Guard_ e-+  GPat_ :: X_GPat e -> Embed (Term_ e) -> Pattern_ e -> Guard_ e   -- | Let (@let x = term@)-  GLet_  :: X_GLet e -> Binding_ e -> Guard_ e--  deriving Generic+  GLet_ :: X_GLet e -> Binding_ e -> Guard_ e+  deriving (Generic) -type ForallGuard (a :: * -> Constraint) e-  = ( a (X_GBool e)-    , a (X_GPat  e)-    , a (X_GLet  e)-    , a (Term_ e)-    , a (Pattern_ e)-    , a (Binding_ e)-    )+type ForallGuard (a :: * -> Constraint) e =+  ( a (X_GBool e)+  , a (X_GPat e)+  , a (X_GLet e)+  , a (Term_ e)+  , a (Pattern_ e)+  , a (Binding_ e)+  ) -deriving instance ForallGuard Show         e => Show       (Guard_ e)-instance          ForallGuard (Subst Type) e => Subst Type (Guard_ e)+deriving instance ForallGuard Show e => Show (Guard_ e)+instance ForallGuard (Subst Type) e => Subst Type (Guard_ e) instance (Typeable e, Show (Guard_ e), ForallGuard Alpha e) => Alpha (Guard_ e) deriving instance (Typeable e, Data e, ForallGuard Data e) => Data (Guard_ e) @@ -539,87 +503,72 @@  -- | Patterns. data Pattern_ e where-   -- | Variable pattern: matches anything and binds the variable.-  PVar_  :: X_PVar e -> Name (Term_ e) -> Pattern_ e-+  PVar_ :: X_PVar e -> Name (Term_ e) -> Pattern_ e   -- | Wildcard pattern @_@: matches anything.   PWild_ :: X_PWild e -> Pattern_ e-   -- | Type ascription pattern @pat : ty@.   PAscr_ :: X_PAscr e -> Pattern_ e -> Type -> Pattern_ e-   -- | Unit pattern @()@: matches @()@.   PUnit_ :: X_PUnit e -> Pattern_ e-   -- | Literal boolean pattern.   PBool_ :: X_PBool e -> Bool -> Pattern_ e-   -- | Tuple pattern @(pat1, .. , patn)@.-  PTup_  :: X_PTup e -> [Pattern_ e] -> Pattern_ e-+  PTup_ :: X_PTup e -> [Pattern_ e] -> Pattern_ e   -- | Injection pattern (@inl pat@ or @inr pat@).-  PInj_  :: X_PInj e -> Side -> Pattern_ e -> Pattern_ e-+  PInj_ :: X_PInj e -> Side -> Pattern_ e -> Pattern_ e   -- | Literal natural number pattern.-  PNat_  :: X_PNat e -> Integer -> Pattern_ e-+  PNat_ :: X_PNat e -> Integer -> Pattern_ e   -- | Unicode character pattern   PChar_ :: X_PChar e -> Char -> Pattern_ e-   -- | String pattern.   PString_ :: X_PString e -> String -> Pattern_ e-   -- | Cons pattern @p1 :: p2@.   PCons_ :: X_PCons e -> Pattern_ e -> Pattern_ e -> Pattern_ e-   -- | List pattern @[p1, .., pn]@.   PList_ :: X_PList e -> [Pattern_ e] -> Pattern_ e-   -- | Addition pattern, @p + t@ or @t + p@-  PAdd_  :: X_PAdd e -> Side -> Pattern_ e -> Term_ e -> Pattern_ e-+  PAdd_ :: X_PAdd e -> Side -> Pattern_ e -> Term_ e -> Pattern_ e   -- | Multiplication pattern, @p * t@ or @t * p@-  PMul_  :: X_PMul e -> Side -> Pattern_ e -> Term_ e -> Pattern_ e-+  PMul_ :: X_PMul e -> Side -> Pattern_ e -> Term_ e -> Pattern_ e   -- | Subtraction pattern, @p - t@-  PSub_  :: X_PSub e -> Pattern_ e -> Term_ e -> Pattern_ e-+  PSub_ :: X_PSub e -> Pattern_ e -> Term_ e -> Pattern_ e   -- | Negation pattern, @-p@-  PNeg_  :: X_PNeg e -> Pattern_ e -> Pattern_ e-+  PNeg_ :: X_PNeg e -> Pattern_ e -> Pattern_ e   -- | Fraction pattern, @p1/p2@   PFrac_ :: X_PFrac e -> Pattern_ e -> Pattern_ e -> Pattern_ e-+  -- | A special placeholder node for a nonlinear occurrence of a+  --   variable; we can only detect this at parse time but need to+  --   generate an error later.+  PNonlinear_ :: Embed (Pattern_ e) -> Name (Term_ e) -> Pattern_ e   -- | Expansion slot.   XPattern_ :: X_Pattern e -> Pattern_ e-   deriving (Generic) -type ForallPattern (a :: * -> Constraint) e-      = ( a (X_PVar e)-        , a (X_PWild e)-        , a (X_PAscr e)-        , a (X_PUnit e)-        , a (X_PBool e)-        , a (X_PNat e)-        , a (X_PChar e)-        , a (X_PString e)-        , a (X_PTup e)-        , a (X_PInj e)-        , a (X_PCons e)-        , a (X_PList e)-        , a (X_PAdd e)-        , a (X_PMul e)-        , a (X_PSub e)-        , a (X_PNeg e)-        , a (X_PFrac e)-        , a (X_Pattern e)-        , a (Term_ e)-        )+type ForallPattern (a :: * -> Constraint) e =+  ( a (X_PVar e)+  , a (X_PWild e)+  , a (X_PAscr e)+  , a (X_PUnit e)+  , a (X_PBool e)+  , a (X_PNat e)+  , a (X_PChar e)+  , a (X_PString e)+  , a (X_PTup e)+  , a (X_PInj e)+  , a (X_PCons e)+  , a (X_PList e)+  , a (X_PAdd e)+  , a (X_PMul e)+  , a (X_PSub e)+  , a (X_PNeg e)+  , a (X_PFrac e)+  , a (X_Pattern e)+  , a (Term_ e)+  ) -deriving instance ForallPattern Show         e => Show       (Pattern_ e)-instance          ForallPattern (Subst Type) e => Subst Type (Pattern_ e)+deriving instance ForallPattern Show e => Show (Pattern_ e)+instance ForallPattern (Subst Type) e => Subst Type (Pattern_ e) instance (Typeable e, Show (Pattern_ e), ForallPattern Alpha e) => Alpha (Pattern_ e) deriving instance (Typeable e, Data e, ForallPattern Data e) => Data (Pattern_ e) 

@@ -1,8 +1,7 @@-{-# LANGUAGE PatternSynonyms      #-}-{-# LANGUAGE StandaloneDeriving   #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE UndecidableInstances #-} ------------------------------------------------------------------------------ -- | -- Module      :  Disco.AST.Surface -- Copyright   :  disco team and contributors@@ -12,147 +11,173 @@ -- -- Abstract syntax trees representing the surface syntax of the Disco -- language.-----------------------------------------------------------------------------------module Disco.AST.Surface-       ( -- * Modules-         Module(..), TopLevel(..)-         -- ** Documentation-       , Docs, DocThing(..), Property-         -- ** Declarations-       , TypeDecl(..), TermDefn(..), TypeDefn(..)-       , Decl(..), partitionDecls, prettyTyDecl--         -- * Terms-       , UD-       , Term-       , pattern TVar-       , pattern TPrim-       , pattern TUn-       , pattern TBin-       , pattern TLet-       , pattern TParens-       , pattern TUnit-       , pattern TBool-       , pattern TChar-       , pattern TString-       , pattern TNat-       , pattern TRat-       , pattern TAbs-       , pattern TApp-       , pattern TTup-       , pattern TCase-       , pattern TChain-       , pattern TTyOp-       , pattern TContainerComp-       , pattern TContainer-       , pattern TAscr-       , pattern TWild-       , pattern TList-       , pattern TListComp--       , Quantifier(..)--         -- ** Telescopes-       , Telescope(..), foldTelescope, mapTelescope, toTelescope, fromTelescope-         -- ** Expressions-       , Side(..)--       , Link-       , pattern TLink--       , Binding+module Disco.AST.Surface (+  -- * Modules+  Module (..),+  emptyModule,+  TopLevel (..), -         -- ** Lists-       , Qual-       , pattern QBind-       , pattern QGuard+  -- ** Documentation+  Docs,+  DocThing (..),+  Property, -       , Container(..)+  -- ** Declarations+  TypeDecl (..),+  TermDefn (..),+  TypeDefn (..),+  Decl (..),+  partitionDecls,+  prettyTyDecl, -       , Ellipsis(..)+  -- * Terms+  UD,+  Term,+  pattern TVar,+  pattern TPrim,+  pattern TUn,+  pattern TBin,+  pattern TLet,+  pattern TParens,+  pattern TUnit,+  pattern TBool,+  pattern TChar,+  pattern TString,+  pattern TNat,+  pattern TRat,+  pattern TAbs,+  pattern TApp,+  pattern TTup,+  pattern TCase,+  pattern TChain,+  pattern TTyOp,+  pattern TContainerComp,+  pattern TContainer,+  pattern TAscr,+  pattern TWild,+  pattern TList,+  pattern TListComp,+  Quantifier (..), -         -- ** Case expressions and patterns-       , Branch+  -- ** Telescopes+  Telescope (..),+  foldTelescope,+  mapTelescope,+  toTelescope,+  fromTelescope, -       , Guard-       , pattern GBool-       , pattern GPat-       , pattern GLet+  -- ** Expressions+  Side (..),+  Link,+  pattern TLink,+  Binding, -       , Pattern-       , pattern PVar-       , pattern PWild-       , pattern PAscr-       , pattern PUnit-       , pattern PBool-       , pattern PChar-       , pattern PString-       , pattern PTup-       , pattern PInj-       , pattern PNat-       , pattern PCons-       , pattern PList-       , pattern PAdd-       , pattern PMul-       , pattern PSub-       , pattern PNeg-       , pattern PFrac+  -- ** Lists+  Qual,+  pattern QBind,+  pattern QGuard,+  Container (..),+  Ellipsis (..), -       , pattern Binding-       )-       where+  -- ** Case expressions and patterns+  Branch,+  Guard,+  pattern GBool,+  pattern GPat,+  pattern GLet,+  Pattern,+  pattern PVar,+  pattern PWild,+  pattern PAscr,+  pattern PUnit,+  pattern PBool,+  pattern PChar,+  pattern PString,+  pattern PTup,+  pattern PInj,+  pattern PNat,+  pattern PCons,+  pattern PList,+  pattern PAdd,+  pattern PMul,+  pattern PSub,+  pattern PNeg,+  pattern PFrac,+  pattern PNonlinear,+  pattern Binding,+)+where -import           Prelude                          hiding ((<>))+import Prelude hiding ((<>)) -import           Control.Lens                     (_1, _2, _3, (%~))-import           Data.Char                        (toLower)-import qualified Data.Map                         as M-import           Data.Set                         (Set)-import           Data.Void+import Control.Lens ((%~), _1, _2, _3)+import Data.Char (toLower)+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)-import           Polysemy.Reader+import Disco.Effects.LFresh+import Polysemy hiding (Embed, embed)+import Polysemy.Reader -import           Disco.AST.Generic-import           Disco.Extensions-import           Disco.Pretty-import           Disco.Syntax.Operators-import           Disco.Syntax.Prims-import           Disco.Types-import           Unbound.Generics.LocallyNameless hiding (LFresh (..), lunbind)+import Disco.AST.Generic+import Disco.Extensions+import Disco.Pretty+import Disco.Syntax.Operators+import Disco.Syntax.Prims+import Disco.Types+import Unbound.Generics.LocallyNameless hiding (LFresh (..), lunbind)  -- | The extension descriptor for Surface specific AST types. data UD  -- | A module contains all the information from one disco source file. data Module = Module-  { modExts    :: Set Ext             -- ^ Enabled extensions-  , modImports :: [String]            -- ^ Module imports-  , modDecls   :: [Decl]              -- ^ Declarations-  , modDocs    :: [(Name Term, Docs)] -- ^ Documentation-  , modTerms   :: [Term]              -- ^ Top-level (bare) terms+  { modExts :: Set Ext+  -- ^ Enabled extensions+  , modImports :: [String]+  -- ^ Module imports+  , modDecls :: [Decl]+  -- ^ Declarations+  , modDocs :: [(Name Term, Docs)]+  -- ^ Documentation+  , modTerms :: [Term]+  -- ^ Top-level (bare) terms   }-deriving instance ForallTerm Show  UD => Show Module +deriving instance ForallTerm Show UD => Show Module++emptyModule :: Module+emptyModule =+  Module+    { modExts = S.empty+    , modImports = []+    , modDecls = []+    , modDocs = []+    , modTerms = []+    }+ -- | A @TopLevel@ is either documentation (a 'DocThing') or a --   declaration ('Decl'). data TopLevel = TLDoc DocThing | TLDecl Decl | TLExpr Term-deriving instance ForallTerm Show  UD => Show TopLevel +deriving instance ForallTerm Show UD => Show TopLevel+ -- | Convenient synonym for a list of 'DocThing's. type Docs = [DocThing]  -- | An item of documentation. data DocThing-  = DocString   [String]    -- ^ A documentation string, i.e. a block-                            --   of @||| text@ items-  | DocProperty Property    -- ^ An example/doctest/property of the-                            --   form @!!! forall (x1:ty1) ... . property@-deriving instance ForallTerm Show  UD => Show DocThing+  = -- | A documentation string, i.e. a block+    --   of @||| text@ items+    DocString [String]+  | -- | An example/doctest/property of the+    --   form @!!! forall (x1:ty1) ... . property@+    DocProperty Property +deriving instance ForallTerm Show UD => Show DocThing+ -- | A property is a universally quantified term of the form --   @forall v1 : T1, v2 : T2. term@. type Property = Property_ UD@@ -169,24 +194,24 @@ -- --   @type T arg1 arg2 ... = body data TypeDefn = TypeDefn String [String] Type-  deriving Show+  deriving (Show)  -- | A declaration is either a type declaration, a term definition, or --   a type definition. data Decl where-  DType  :: TypeDecl -> Decl-  DDefn  :: TermDefn -> Decl+  DType :: TypeDecl -> Decl+  DDefn :: TermDefn -> Decl   DTyDef :: TypeDefn -> Decl -deriving instance ForallTerm Show  UD => Show TypeDecl-deriving instance ForallTerm Show  UD => Show TermDefn-deriving instance ForallTerm Show  UD => Show Decl+deriving instance ForallTerm Show UD => Show TypeDecl+deriving instance ForallTerm Show UD => Show TermDefn+deriving instance ForallTerm Show UD => Show Decl  partitionDecls :: [Decl] -> ([TypeDecl], [TermDefn], [TypeDefn])-partitionDecls (DType  tyDecl : ds) = (_1 %~ (tyDecl:)) (partitionDecls ds)-partitionDecls (DDefn  def    : ds) = (_2 %~ (def:))    (partitionDecls ds)-partitionDecls (DTyDef def    : ds) = (_3 %~ (def:))    (partitionDecls ds)-partitionDecls []                   = ([], [], [])+partitionDecls (DType tyDecl : ds) = (_1 %~ (tyDecl :)) (partitionDecls ds)+partitionDecls (DDefn def : ds) = (_2 %~ (def :)) (partitionDecls ds)+partitionDecls (DTyDef def : ds) = (_3 %~ (def :)) (partitionDecls ds)+partitionDecls [] = ([], [], [])  ------------------------------------------------------------ -- Pretty-printing top-level declarations@@ -196,10 +221,10 @@  instance Pretty Decl where   pretty = \case-    DType  (TypeDecl x ty) -> pretty x <+> text ":" <+> pretty ty+    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,)) bs  -- | Pretty-print a single clause in a definition. instance Pretty (Name a, Bind [Pattern] Term) where@@ -207,7 +232,7 @@     pretty x <> hcat (map prettyPatternP ps) <+> text "=" <+> setPA initPA (pretty t)  -- | Pretty-print a type declaration.-prettyTyDecl :: Members '[Reader PA, LFresh] r => Name t -> Type -> Sem r Doc+prettyTyDecl :: Members '[Reader PA, LFresh] r => Name t -> Type -> Sem r (Doc ann) prettyTyDecl x ty = hsep [pretty x, text ":", pretty ty]  ------------------------------------------------------------@@ -219,28 +244,28 @@ -- (nonempty) list of patterns. Each pattern might contain any -- number of variables, and might have type annotations on some -- of its components.-type instance X_Binder          UD = [Pattern]+type instance X_Binder UD = [Pattern] -type instance X_TVar            UD = ()-type instance X_TPrim           UD = ()-type instance X_TLet            UD = ()-type instance X_TParens         UD = ()-type instance X_TUnit           UD = ()-type instance X_TBool           UD = ()-type instance X_TNat            UD = ()-type instance X_TRat            UD = ()-type instance X_TChar           UD = ()-type instance X_TString         UD = ()-type instance X_TAbs            UD = ()-type instance X_TApp            UD = ()-type instance X_TTup            UD = ()-type instance X_TCase           UD = ()-type instance X_TChain          UD = ()-type instance X_TTyOp           UD = ()-type instance X_TContainer      UD = ()-type instance X_TContainerComp  UD = ()-type instance X_TAscr           UD = ()-type instance X_Term            UD = ()  -- TWild+type instance X_TVar UD = ()+type instance X_TPrim UD = ()+type instance X_TLet UD = ()+type instance X_TParens UD = ()+type instance X_TUnit UD = ()+type instance X_TBool UD = ()+type instance X_TNat UD = ()+type instance X_TRat UD = ()+type instance X_TChar UD = ()+type instance X_TString UD = ()+type instance X_TAbs UD = ()+type instance X_TApp UD = ()+type instance X_TTup UD = ()+type instance X_TCase UD = ()+type instance X_TChain UD = ()+type instance X_TTyOp UD = ()+type instance X_TContainer UD = ()+type instance X_TContainerComp UD = ()+type instance X_TAscr UD = ()+type instance X_Term UD = () -- TWild  pattern TVar :: Name Term -> Term pattern TVar name = TVar_ () name@@ -258,7 +283,7 @@ pattern TLet bind = TLet_ () bind  pattern TParens :: Term -> Term-pattern TParens term  = TParens_ () term+pattern TParens term = TParens_ () term  pattern TUnit :: Term pattern TUnit = TUnit_ ()@@ -266,7 +291,7 @@ pattern TBool :: Bool -> Term pattern TBool bool = TBool_ () bool -pattern TNat  :: Integer -> Term+pattern TNat :: Integer -> Term pattern TNat int = TNat_ () int  pattern TRat :: Rational -> Term@@ -281,7 +306,7 @@ pattern TAbs :: Quantifier -> Bind [Pattern] Term -> Term pattern TAbs q bind = TAbs_ q () bind -pattern TApp  :: Term -> Term -> Term+pattern TApp :: Term -> Term -> Term pattern TApp term1 term2 = TApp_ () term1 term2  pattern TTup :: [Term] -> Term@@ -311,9 +336,28 @@ pattern TWild :: Term pattern TWild = XTerm_ () -{-# COMPLETE TVar, TPrim, TLet, TParens, TUnit, TBool, TNat, TRat, TChar,-             TString, TAbs, TApp, TTup, TCase, TChain, TTyOp,-             TContainer, TContainerComp, TAscr, TWild #-}+{-# COMPLETE+  TVar+  , TPrim+  , TLet+  , TParens+  , TUnit+  , TBool+  , TNat+  , TRat+  , TChar+  , TString+  , TAbs+  , TApp+  , TTup+  , TCase+  , TChain+  , TTyOp+  , TContainer+  , TContainerComp+  , TAscr+  , TWild+  #-}  pattern TList :: [Term] -> Maybe (Ellipsis Term) -> Term pattern TList ts e <- TContainer_ () ListContainer (map fst -> ts) e@@ -357,8 +401,8 @@ type Guard = Guard_ UD  type instance X_GBool UD = ()-type instance X_GPat  UD = ()-type instance X_GLet  UD = ()+type instance X_GPat UD = ()+type instance X_GLet UD = ()  pattern GBool :: Embed Term -> Guard pattern GBool embedt = GBool_ () embedt@@ -373,23 +417,23 @@  type Pattern = Pattern_ UD -type instance X_PVar UD    = ()-type instance X_PWild UD   = ()-type instance X_PAscr UD   = ()-type instance X_PUnit UD   = ()-type instance X_PBool UD   = ()-type instance X_PTup UD    = ()-type instance X_PInj UD    = ()-type instance X_PNat UD    = ()-type instance X_PChar UD   = ()+type instance X_PVar UD = ()+type instance X_PWild UD = ()+type instance X_PAscr UD = ()+type instance X_PUnit UD = ()+type instance X_PBool UD = ()+type instance X_PTup UD = ()+type instance X_PInj UD = ()+type instance X_PNat UD = ()+type instance X_PChar UD = () type instance X_PString UD = ()-type instance X_PCons UD   = ()-type instance X_PList UD   = ()-type instance X_PAdd UD    = ()-type instance X_PMul UD    = ()-type instance X_PSub UD    = ()-type instance X_PNeg UD    = ()-type instance X_PFrac UD   = ()+type instance X_PCons UD = ()+type instance X_PList UD = ()+type instance X_PAdd UD = ()+type instance X_PMul UD = ()+type instance X_PSub UD = ()+type instance X_PNeg UD = ()+type instance X_PFrac UD = () type instance X_Pattern UD = Void  pattern PVar :: Name Term -> Pattern@@ -398,8 +442,8 @@ pattern PWild :: Pattern pattern PWild = PWild_ () - -- (?) TAscr uses a PolyType, but without higher rank types- -- I think we can't possibly need that here.+-- (?) TAscr uses a PolyType, but without higher rank types+-- I think we can't possibly need that here. pattern PAscr :: Pattern -> Type -> Pattern pattern PAscr p ty = PAscr_ () p ty @@ -407,7 +451,7 @@ pattern PUnit = PUnit_ ()  pattern PBool :: Bool -> Pattern-pattern PBool  b = PBool_ () b+pattern PBool b = PBool_ () b  pattern PChar :: Char -> Pattern pattern PChar c = PChar_ () c@@ -415,17 +459,17 @@ pattern PString :: String -> Pattern pattern PString s = PString_ () s -pattern PTup  :: [Pattern] -> Pattern+pattern PTup :: [Pattern] -> Pattern pattern PTup lp = PTup_ () lp -pattern PInj  :: Side -> Pattern -> Pattern+pattern PInj :: Side -> Pattern -> Pattern pattern PInj s p = PInj_ () s p -pattern PNat  :: Integer -> Pattern+pattern PNat :: Integer -> Pattern pattern PNat n = PNat_ () n  pattern PCons :: Pattern -> Pattern -> Pattern-pattern PCons  p1 p2 = PCons_ () p1 p2+pattern PCons p1 p2 = PCons_ () p1 p2  pattern PList :: [Pattern] -> Pattern pattern PList lp = PList_ () lp@@ -445,9 +489,31 @@ pattern PFrac :: Pattern -> Pattern -> Pattern pattern PFrac p1 p2 = PFrac_ () p1 p2 -{-# COMPLETE PVar, PWild, PAscr, PUnit, PBool, PTup, PInj, PNat,-             PChar, PString, PCons, PList, PAdd, PMul, PSub, PNeg, PFrac #-}+pattern PNonlinear :: Pattern -> Name Term -> Pattern+pattern PNonlinear p x <- PNonlinear_ (unembed -> p) x+  where+    PNonlinear p x = PNonlinear_ (embed p) x +{-# COMPLETE+  PVar+  , PWild+  , PAscr+  , PUnit+  , PBool+  , PTup+  , PInj+  , PNat+  , PChar+  , PString+  , PCons+  , PList+  , PAdd+  , PMul+  , PSub+  , PNeg+  , PFrac+  #-}+ ------------------------------------------------------------ -- Pretty-printing for surface-syntax terms --@@ -456,86 +522,88 @@ -- term (e.g. via the :doc REPL command).  -- | Pretty-print a term with guaranteed parentheses.-prettyTermP :: Members '[LFresh, Reader PA] r => Term -> Sem r Doc-prettyTermP t@TTup{} = setPA initPA $ pretty t+prettyTermP :: Members '[LFresh, Reader PA] r => Term -> Sem r (Doc ann)+prettyTermP t@TTup {} = setPA initPA $ pretty t -- prettyTermP t@TContainer{} = setPA initPA $ "" <+> prettyTerm t-prettyTermP t        = withPA initPA $ pretty t+prettyTermP t = withPA initPA $ pretty t  instance Pretty Term where   pretty = \case-    TVar x      -> pretty x+    TVar x -> pretty x     TPrim (PrimUOp uop) ->       case M.lookup uop uopMap of-        Just (OpInfo (UOpF Pre _) (syn:_) _)  -> text syn <> text "~"-        Just (OpInfo (UOpF Post _) (syn:_) _) -> text "~" <> text syn+        Just (OpInfo (UOpF Pre _) (syn : _) _) -> text syn <> text "~"+        Just (OpInfo (UOpF Post _) (syn : _) _) -> text "~" <> text syn         _ -> error $ "pretty @Term: " ++ show uop ++ " is not in the uopMap!"     TPrim (PrimBOp bop) -> text "~" <> pretty bop <> text "~"     TPrim p ->       case M.lookup p primMap of-        Just (PrimInfo _ nm True)  -> text nm+        Just (PrimInfo _ nm True) -> text nm         Just (PrimInfo _ nm False) -> text "$" <> text nm         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)-    TChar c     -> text (show c)-    TString cs  -> doubleQuotes $ text cs-    TAbs q bnd  -> withPA initPA $+    TParens t -> pretty t+    TUnit -> text "■"+    (TBool b) -> text (map toLower $ show b)+    TChar c -> text (show c)+    TString cs -> doubleQuotes $ text cs+    TAbs q bnd -> withPA initPA $       lunbind bnd $ \(args, body) ->-      prettyQ q-        <> (hsep =<< punctuate (text ",") (map pretty args))-        <> text "."-        <+> lt (pretty body)-      where-        prettyQ Lam = text "λ"-        prettyQ All = text "∀"-        prettyQ Ex  = text "∃"+        prettyQ q+          <> (hsep =<< punctuate (text ",") (map pretty args))+          <> text "."+          <+> lt (pretty body)+     where+      prettyQ Lam = text "λ"+      prettyQ All = text "∀"+      prettyQ Ex = text "∃"      -- special case for fully applied unary operators     TApp (TPrim (PrimUOp uop)) t ->       case M.lookup uop uopMap of-        Just (OpInfo (UOpF Post _) _ _) -> withPA (ugetPA uop) $-          lt (pretty t) <> pretty uop-        Just (OpInfo (UOpF Pre  _) _ _) -> withPA (ugetPA uop) $-          pretty uop <> rt (pretty t)+        Just (OpInfo (UOpF Post _) _ _) ->+          withPA (ugetPA uop) $+            lt (pretty t) <> pretty uop+        Just (OpInfo (UOpF Pre _) _ _) ->+          withPA (ugetPA uop) $+            pretty uop <> rt (pretty t)         _ -> error $ "pretty @Term: uopMap doesn't contain " ++ show uop-     -- special case for fully applied binary operators-    TApp (TPrim (PrimBOp bop)) (TTup [t1, t2]) -> withPA (getPA bop) $-      hsep-      [ lt (pretty t1)-      , pretty bop-      , rt (pretty t2)-      ]-+    TApp (TPrim (PrimBOp bop)) (TTup [t1, t2]) ->+      withPA (getPA bop) $+        hsep+          [ lt (pretty t1)+          , pretty bop+          , rt (pretty t2)+          ]     -- Always pretty-print function applications with parentheses-    TApp t1 t2  -> withPA funPA $-      lt (pretty t1) <> prettyTermP t2--    TTup ts     -> setPA initPA $ do+    TApp t1 t2 ->+      withPA funPA $+        lt (pretty t1) <> prettyTermP t2+    TTup ts -> setPA initPA $ do       ds <- punctuate (text ",") (map pretty ts)       parens (hsep ds)-    TContainer c ts e  -> setPA initPA $ do+    TContainer c ts e -> setPA initPA $ do       ds <- punctuate (text ",") (map prettyCount ts)       let pe = case e of-                 Nothing        -> []-                 Just (Until t) -> [text "..", pretty t]+            Nothing -> []+            Just (Until t) -> [text "..", pretty t]       containerDelims c (hsep (ds ++ pe))-      where-        prettyCount (t, Nothing) = pretty t-        prettyCount (t, Just n)  = lt (pretty t) <+> text "#" <+> rt (pretty n)+     where+      prettyCount (t, Nothing) = pretty t+      prettyCount (t, Just n) = lt (pretty t) <+> text "#" <+> rt (pretty n)     TContainerComp c bqst ->-      lunbind bqst $ \(qs,t) ->-      setPA initPA $ containerDelims c (hsep [pretty t, text "|", pretty qs])-    TNat n       -> integer n-    TChain t lks -> withPA (getPA Eq) . hsep $+      lunbind bqst $ \(qs, t) ->+        setPA initPA $ containerDelims c (hsep [pretty t, text "|", pretty qs])+    TNat n -> integer n+    TChain t lks ->+      withPA (getPA Eq) . hsep $         lt (pretty t)-        : concatMap prettyLink lks-      where-        prettyLink (TLink op t2) =-          [ pretty op-          , setPA (getPA op) . rt $ pretty t2-          ]+          : concatMap prettyLink lks+     where+      prettyLink (TLink op t2) =+        [ pretty op+        , setPA (getPA op) . rt $ pretty t2+        ]     TLet bnd -> withPA initPA $       lunbind bnd $ \(bs, t2) -> do         ds <- punctuate (text ",") (map pretty (fromTelescope bs))@@ -545,46 +613,47 @@           , text "in"           , pretty t2           ]--    TCase b    -> withPA initPA $-      (text "{?" <+> prettyBranches b) $+$ text "?}"-    TAscr t ty -> withPA ascrPA $-      lt (pretty t) <+> text ":" <+> rt (pretty ty)-    TRat  r    -> text (prettyDecimal r)-    TTyOp op ty  -> withPA funPA $-      pretty op <+> pretty ty+    TCase b ->+      withPA initPA $+        (text "{?" <+> prettyBranches b) $+$ text "?}"+    TAscr t ty ->+      withPA ascrPA $+        lt (pretty t) <+> text ":" <+> rt (pretty ty)+    TRat r -> text (prettyDecimal r)+    TTyOp op ty ->+      withPA funPA $+        pretty op <+> pretty ty     TWild -> text "_"  -- | Print appropriate delimiters for a container literal.-containerDelims :: Member (Reader PA) r => Container -> (Sem r Doc -> Sem r Doc)+containerDelims :: Member (Reader PA) r => Container -> (Sem r (Doc ann) -> Sem r (Doc ann)) containerDelims ListContainer = brackets-containerDelims BagContainer  = bag-containerDelims SetContainer  = braces+containerDelims BagContainer = bag+containerDelims SetContainer = braces -prettyBranches :: Members '[Reader PA, LFresh] r => [Branch] -> Sem r Doc+prettyBranches :: Members '[Reader PA, LFresh] r => [Branch] -> Sem r (Doc ann) prettyBranches = \case   [] -> error "Empty branches are disallowed."-  b:bs ->+  b : bs ->     pretty b-    $+$-    foldr (($+$) . (text "," <+>) . pretty) empty bs+      $+$ foldr (($+$) . (text "," <+>) . pretty) empty bs  -- | Pretty-print a single branch in a case expression. instance Pretty Branch where-  pretty br = lunbind br $ \(gs,t) ->+  pretty br = lunbind br $ \(gs, t) ->     pretty t <+> pretty gs  -- | Pretty-print the guards in a single branch of a case expression. instance Pretty (Telescope Guard) where   pretty = \case     TelEmpty -> text "otherwise"-    gs       -> foldr (\g r -> pretty g <+> r) (text "") (fromTelescope gs)+    gs -> foldr (\g r -> pretty g <+> r) (text "") (fromTelescope gs)  instance Pretty Guard where   pretty = \case-    GBool et  -> text "if" <+> pretty (unembed et)+    GBool et -> text "if" <+> pretty (unembed et)     GPat et p -> text "when" <+> pretty (unembed et) <+> text "is" <+> pretty p-    GLet b    -> text "let" <+> pretty b+    GLet b -> text "let" <+> pretty b  -- | Pretty-print a binding, i.e. a pairing of a name (with optional --   type annotation) and term.@@ -605,12 +674,12 @@ instance Pretty Qual where   pretty = \case     QBind x (unembed -> t) -> hsep [pretty x, text "in", pretty t]-    QGuard (unembed -> t)  -> pretty t+    QGuard (unembed -> t) -> pretty t  -- | Pretty-print a pattern with guaranteed parentheses.-prettyPatternP :: Members '[LFresh, Reader PA] r => Pattern -> Sem r Doc-prettyPatternP p@PTup{} = setPA initPA $ pretty p-prettyPatternP p        = withPA initPA $ pretty p+prettyPatternP :: Members '[LFresh, Reader PA] r => Pattern -> Sem r (Doc ann)+prettyPatternP p@PTup {} = setPA initPA $ pretty p+prettyPatternP p = withPA initPA $ pretty p  -- We could probably alternatively write a function to turn a pattern -- back into a term, and pretty-print that instead of the below.@@ -618,37 +687,46 @@  instance Pretty Pattern where   pretty = \case-    PVar x      -> pretty x-    PWild       -> text "_"-    PAscr p ty  -> withPA ascrPA $-      lt (pretty p) <+> text ":" <+> rt (pretty ty)-    PUnit       -> text "■"-    PBool b     -> text $ map toLower $ show b-    PChar c     -> text (show c)-    PString s   -> text (show s)-    PTup ts     -> setPA initPA $ do+    PVar x -> pretty x+    PWild -> text "_"+    PAscr p ty ->+      withPA ascrPA $+        lt (pretty p) <+> text ":" <+> rt (pretty ty)+    PUnit -> text "■"+    PBool b -> text $ map toLower $ show b+    PChar c -> text (show c)+    PString s -> text (show s)+    PTup ts -> setPA initPA $ do       ds <- punctuate (text ",") (map pretty ts)       parens (hsep ds)-    PInj s p    -> withPA funPA $-      pretty s <> prettyPatternP p-    PNat n      -> integer n-    PCons p1 p2 -> withPA (getPA Cons) $-      lt (pretty p1) <+> text "::" <+> rt (pretty p2)-    PList ps    -> setPA initPA $ do+    PInj s p ->+      withPA funPA $+        pretty s <> prettyPatternP p+    PNat n -> integer n+    PCons p1 p2 ->+      withPA (getPA Cons) $+        lt (pretty p1) <+> text "::" <+> rt (pretty p2)+    PList ps -> setPA initPA $ do       ds <- punctuate (text ",") (map pretty ps)       brackets (hsep ds)-    PAdd L p t  -> withPA (getPA Add) $-      lt (pretty p) <+> text "+" <+> rt (pretty t)-    PAdd R p t  -> withPA (getPA Add) $-      lt (pretty t) <+> text "+" <+> rt (pretty p)-    PMul L p t  -> withPA (getPA Mul) $-      lt (pretty p) <+> text "*" <+> rt (pretty t)-    PMul R p t  -> withPA (getPA Mul) $-      lt (pretty t) <+> text "*" <+> rt (pretty p)-    PSub p t    -> withPA (getPA Sub) $-      lt (pretty p) <+> text "-" <+> rt (pretty t)-    PNeg p      -> withPA (ugetPA Neg) $-      text "-" <> rt (pretty p)-    PFrac p1 p2 -> withPA (getPA Div) $-      lt (pretty p1) <+> text "/" <+> rt (pretty p2)-+    PAdd L p t ->+      withPA (getPA Add) $+        lt (pretty p) <+> text "+" <+> rt (pretty t)+    PAdd R p t ->+      withPA (getPA Add) $+        lt (pretty t) <+> text "+" <+> rt (pretty p)+    PMul L p t ->+      withPA (getPA Mul) $+        lt (pretty p) <+> text "*" <+> rt (pretty t)+    PMul R p t ->+      withPA (getPA Mul) $+        lt (pretty t) <+> text "*" <+> rt (pretty p)+    PSub p t ->+      withPA (getPA Sub) $+        lt (pretty p) <+> text "-" <+> rt (pretty t)+    PNeg p ->+      withPA (ugetPA Neg) $+        text "-" <> rt (pretty p)+    PFrac p1 p2 ->+      withPA (getPA Div) $+        lt (pretty p1) <+> text "/" <+> rt (pretty p2)

@@ -1,7 +1,10 @@ {-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE PatternSynonyms    #-}+{-# LANGUAGE PatternSynonyms #-}  -----------------------------------------------------------------------------++-----------------------------------------------------------------------------+ -- | -- Module      :  Disco.AST.Typed -- Copyright   :  disco team and contributors@@ -12,100 +15,91 @@ -- Typed abstract syntax trees representing the typechecked surface -- syntax of the Disco language.  Each tree node is annotated with the -- type of its subtree.-----------------------------------------------------------------------------------module Disco.AST.Typed-       ( -- * Type-annotated terms-         ATerm-       , pattern ATVar-       , pattern ATPrim-       , pattern ATLet-       , pattern ATUnit-       , pattern ATBool-       , pattern ATNat-       , pattern ATRat-       , pattern ATChar-       , pattern ATString-       , pattern ATAbs-       , pattern ATApp-       , pattern ATTup-       , pattern ATCase-       , pattern ATChain-       , pattern ATTyOp-       , pattern ATContainer-       , pattern ATContainerComp-       , pattern ATList-       , pattern ATListComp-       , pattern ATTest--       , ALink-       , pattern ATLink--       , Container(..)-       , ABinding-         -- * Branches and guards-       , ABranch--       , AGuard-       , pattern AGBool-       , pattern AGPat-       , pattern AGLet--       , AQual-       , pattern AQBind-       , pattern AQGuard--       , APattern-       , pattern APVar-       , pattern APWild-       , pattern APUnit-       , pattern APBool-       , pattern APTup-       , pattern APInj-       , pattern APNat-       , pattern APChar-       , pattern APString-       , pattern APCons-       , pattern APList-       , pattern APAdd-       , pattern APMul-       , pattern APSub-       , pattern APNeg-       , pattern APFrac+module Disco.AST.Typed (+  -- * Type-annotated terms+  ATerm,+  pattern ATVar,+  pattern ATPrim,+  pattern ATLet,+  pattern ATUnit,+  pattern ATBool,+  pattern ATNat,+  pattern ATRat,+  pattern ATChar,+  pattern ATString,+  pattern ATAbs,+  pattern ATApp,+  pattern ATTup,+  pattern ATCase,+  pattern ATChain,+  pattern ATTyOp,+  pattern ATContainer,+  pattern ATContainerComp,+  pattern ATList,+  pattern ATListComp,+  pattern ATTest,+  ALink,+  pattern ATLink,+  Container (..),+  ABinding, -       , pattern ABinding-         -- * Utilities-       , varsBound-       , getType-       , setType-       , substQT+  -- * Branches and guards+  ABranch,+  AGuard,+  pattern AGBool,+  pattern AGPat,+  pattern AGLet,+  AQual,+  pattern AQBind,+  pattern AQGuard,+  APattern,+  pattern APVar,+  pattern APWild,+  pattern APUnit,+  pattern APBool,+  pattern APTup,+  pattern APInj,+  pattern APNat,+  pattern APChar,+  pattern APString,+  pattern APCons,+  pattern APList,+  pattern APAdd,+  pattern APMul,+  pattern APSub,+  pattern APNeg,+  pattern APFrac,+  pattern ABinding, -       , AProperty-       )-       where+  -- * Utilities+  varsBound,+  getType,+  setType,+  substQT,+  AProperty,+)+where -import           Unbound.Generics.LocallyNameless-import           Unbound.Generics.LocallyNameless.Unsafe+import Unbound.Generics.LocallyNameless+import Unbound.Generics.LocallyNameless.Unsafe -import           Control.Arrow                           ((***))-import           Data.Coerce                             (coerce)-import           Data.Data                               (Data)-import           Data.Void+import Control.Arrow ((***))+import Data.Coerce (coerce)+import Data.Data (Data)+import Data.Void -import           Control.Lens.Plated                     (transform)-import           Disco.AST.Generic-import           Disco.AST.Surface-import           Disco.Names-import           Disco.Pretty-import           Disco.Syntax.Operators-import           Disco.Syntax.Prims-import           Disco.Types+import Control.Lens.Plated (transform)+import Disco.AST.Generic+import Disco.AST.Surface+import Disco.Names+import Disco.Pretty+import Disco.Syntax.Operators+import Disco.Syntax.Prims+import Disco.Types  -- | The extension descriptor for Typed specific AST types.- data TY-  deriving Data+  deriving (Data)  type AProperty = Property_ TY @@ -116,34 +110,33 @@  -- | An @ATerm@ is a typechecked term where every node in the tree has --   been annotated with the type of the subterm rooted at that node.- type ATerm = Term_ TY -type instance X_Binder          TY = [APattern]+type instance X_Binder TY = [APattern] -type instance X_TVar            TY = Void -- Names are now qualified-type instance X_TPrim           TY = Type-type instance X_TLet            TY = Type-type instance X_TUnit           TY = ()-type instance X_TBool           TY = Type-type instance X_TNat            TY = Type-type instance X_TRat            TY = ()-type instance X_TChar           TY = ()-type instance X_TString         TY = ()-type instance X_TAbs            TY = Type-type instance X_TApp            TY = Type-type instance X_TCase           TY = Type-type instance X_TChain          TY = Type-type instance X_TTyOp           TY = Type-type instance X_TContainer      TY = Type-type instance X_TContainerComp  TY = Type-type instance X_TAscr           TY = Void -- No more type ascriptions in typechecked terms-type instance X_TTup            TY = Type-type instance X_TParens         TY = Void -- No more explicit parens+type instance X_TVar TY = Void -- Names are now qualified+type instance X_TPrim TY = Type+type instance X_TLet TY = Type+type instance X_TUnit TY = ()+type instance X_TBool TY = Type+type instance X_TNat TY = Type+type instance X_TRat TY = ()+type instance X_TChar TY = ()+type instance X_TString TY = ()+type instance X_TAbs TY = Type+type instance X_TApp TY = Type+type instance X_TCase TY = Type+type instance X_TChain TY = Type+type instance X_TTyOp TY = Type+type instance X_TContainer TY = Type+type instance X_TContainerComp TY = Type+type instance X_TAscr TY = Void -- No more type ascriptions in typechecked terms+type instance X_TTup TY = Type+type instance X_TParens TY = Void -- No more explicit parens - -- A test frame for reporting counterexamples in a test. These don't appear- -- in source programs, but because the deugarer manipulates partly-desugared- -- terms it helps to be able to represent these in 'ATerm'.+-- A test frame for reporting counterexamples in a test. These don't appear+-- in source programs, but because the deugarer manipulates partly-desugared+-- terms it helps to be able to represent these in 'ATerm'. type instance X_Term TY = Either ([(String, Type, Name ATerm)], ATerm) (Type, QName ATerm)  pattern ATVar :: Type -> QName ATerm -> ATerm@@ -161,7 +154,7 @@ pattern ATBool :: Type -> Bool -> ATerm pattern ATBool ty bool = TBool_ ty bool -pattern ATNat  :: Type -> Integer -> ATerm+pattern ATNat :: Type -> Integer -> ATerm pattern ATNat ty int = TNat_ ty int  pattern ATRat :: Rational -> ATerm@@ -176,7 +169,7 @@ pattern ATAbs :: Quantifier -> Type -> Bind [APattern] ATerm -> ATerm pattern ATAbs q ty bind = TAbs_ q ty bind -pattern ATApp  :: Type -> ATerm -> ATerm -> ATerm+pattern ATApp :: Type -> ATerm -> ATerm -> ATerm pattern ATApp ty term1 term2 = TApp_ ty term1 term2  pattern ATTup :: Type -> [ATerm] -> ATerm@@ -200,9 +193,26 @@ pattern ATTest :: [(String, Type, Name ATerm)] -> ATerm -> ATerm pattern ATTest ns t = XTerm_ (Left (ns, t)) -{-# COMPLETE ATVar, ATPrim, ATLet, ATUnit, ATBool, ATNat, ATRat, ATChar,-             ATString, ATAbs, ATApp, ATTup, ATCase, ATChain, ATTyOp,-             ATContainer, ATContainerComp, ATTest #-}+{-# COMPLETE+  ATVar+  , ATPrim+  , ATLet+  , ATUnit+  , ATBool+  , ATNat+  , ATRat+  , ATChar+  , ATString+  , ATAbs+  , ATApp+  , ATTup+  , ATCase+  , ATChain+  , ATTyOp+  , ATContainer+  , ATContainerComp+  , ATTest+  #-}  pattern ATList :: Type -> [ATerm] -> Maybe (Ellipsis ATerm) -> ATerm pattern ATList t xs e <- ATContainer t ListContainer (map fst -> xs) e@@ -221,13 +231,11 @@  {-# COMPLETE ATLink #-} - type AQual = Qual_ TY  type instance X_QBind TY = () type instance X_QGuard TY = () - pattern AQBind :: Name ATerm -> Embed ATerm -> AQual pattern AQBind namet embedt = QBind_ () namet embedt @@ -248,8 +256,8 @@ type AGuard = Guard_ TY  type instance X_GBool TY = ()-type instance X_GPat  TY = ()-type instance X_GLet  TY = ()   -- ??? Type?+type instance X_GPat TY = ()+type instance X_GLet TY = () -- ??? Type?  pattern AGBool :: Embed ATerm -> AGuard pattern AGBool embedt = GBool_ () embedt@@ -267,25 +275,25 @@ -- We have to use Embed Type because we don't want any type variables -- inside the types being treated as binders! -type instance X_PVar     TY = Embed Type-type instance X_PWild    TY = Embed Type-type instance X_PAscr    TY = Void -- No more ascriptions in typechecked patterns.-type instance X_PUnit    TY = ()-type instance X_PBool    TY = ()-type instance X_PChar    TY = ()-type instance X_PString  TY = ()-type instance X_PTup     TY = Embed Type-type instance X_PInj     TY = Embed Type-type instance X_PNat     TY = Embed Type-type instance X_PCons    TY = Embed Type-type instance X_PList    TY = Embed Type-type instance X_PAdd     TY = Embed Type-type instance X_PMul     TY = Embed Type-type instance X_PSub     TY = Embed Type-type instance X_PNeg     TY = Embed Type-type instance X_PFrac    TY = Embed Type+type instance X_PVar TY = Embed Type+type instance X_PWild TY = Embed Type+type instance X_PAscr TY = Void -- No more ascriptions in typechecked patterns.+type instance X_PUnit TY = ()+type instance X_PBool TY = ()+type instance X_PChar TY = ()+type instance X_PString TY = ()+type instance X_PTup TY = Embed Type+type instance X_PInj TY = Embed Type+type instance X_PNat TY = Embed Type+type instance X_PCons TY = Embed Type+type instance X_PList TY = Embed Type+type instance X_PAdd TY = Embed Type+type instance X_PMul TY = Embed Type+type instance X_PSub TY = Embed Type+type instance X_PNeg TY = Embed Type+type instance X_PFrac TY = Embed Type -type instance X_Pattern  TY = ()+type instance X_Pattern TY = ()  pattern APVar :: Type -> Name ATerm -> APattern pattern APVar ty name <- PVar_ (unembed -> ty) name@@ -301,25 +309,25 @@ pattern APUnit = PUnit_ ()  pattern APBool :: Bool -> APattern-pattern APBool  b = PBool_ () b+pattern APBool b = PBool_ () b  pattern APChar :: Char -> APattern-pattern APChar  c = PChar_ () c+pattern APChar c = PChar_ () c  pattern APString :: String -> APattern pattern APString s = PString_ () s -pattern APTup  :: Type -> [APattern] -> APattern+pattern APTup :: Type -> [APattern] -> APattern pattern APTup ty lp <- PTup_ (unembed -> ty) lp   where     APTup ty lp = PTup_ (embed ty) lp -pattern APInj  :: Type -> Side -> APattern -> APattern+pattern APInj :: Type -> Side -> APattern -> APattern pattern APInj ty s p <- PInj_ (unembed -> ty) s p   where     APInj ty s p = PInj_ (embed ty) s p -pattern APNat  :: Type -> Integer -> APattern+pattern APNat :: Type -> Integer -> APattern pattern APNat ty n <- PNat_ (unembed -> ty) n   where     APNat ty n = PNat_ (embed ty) n@@ -359,87 +367,103 @@   where     APFrac ty p1 p2 = PFrac_ (embed ty) p1 p2 -{-# COMPLETE APVar, APWild, APUnit, APBool, APChar, APString,-    APTup, APInj, APNat, APCons, APList, APAdd, APMul, APSub, APNeg, APFrac #-}+{-# COMPLETE+  APVar+  , APWild+  , APUnit+  , APBool+  , APChar+  , APString+  , APTup+  , APInj+  , APNat+  , APCons+  , APList+  , APAdd+  , APMul+  , APSub+  , APNeg+  , APFrac+  #-}  varsBound :: APattern -> [(Name ATerm, Type)]-varsBound (APVar ty n)    = [(n, ty)]-varsBound (APWild _)      = []-varsBound APUnit          = []-varsBound (APBool _)      = []-varsBound (APChar _)      = []-varsBound (APString _)    = []-varsBound (APTup _ ps)    = varsBound =<< ps-varsBound (APInj _ _ p)   = varsBound p-varsBound (APNat _ _)     = []-varsBound (APCons _ p q)  = varsBound p ++ varsBound q-varsBound (APList _ ps)   = varsBound =<< ps+varsBound (APVar ty n) = [(n, ty)]+varsBound (APWild _) = []+varsBound APUnit = []+varsBound (APBool _) = []+varsBound (APChar _) = []+varsBound (APString _) = []+varsBound (APTup _ ps) = varsBound =<< ps+varsBound (APInj _ _ p) = varsBound p+varsBound (APNat _ _) = []+varsBound (APCons _ p q) = varsBound p ++ varsBound q+varsBound (APList _ ps) = varsBound =<< ps varsBound (APAdd _ _ p _) = varsBound p varsBound (APMul _ _ p _) = varsBound p-varsBound (APSub _ p _)   = varsBound p-varsBound (APNeg _ p)     = varsBound p-varsBound (APFrac _ p q)  = varsBound p ++ varsBound q+varsBound (APSub _ p _) = varsBound p+varsBound (APNeg _ p) = varsBound p+varsBound (APFrac _ p q) = varsBound p ++ varsBound q  ------------------------------------------------------------ -- getType ------------------------------------------------------------  instance HasType ATerm where-  getType (ATVar ty _)             = ty-  getType (ATPrim ty _)            = ty-  getType ATUnit                   = TyUnit-  getType (ATBool ty _)            = ty-  getType (ATNat ty _)             = ty-  getType (ATRat _)                = TyF-  getType (ATChar _)               = TyC-  getType (ATString _)             = TyList TyC-  getType (ATAbs _ ty _)           = ty-  getType (ATApp ty _ _)           = ty-  getType (ATTup ty _)             = ty-  getType (ATTyOp ty _ _)          = ty-  getType (ATChain ty _ _)         = ty-  getType (ATContainer ty _ _ _)   = ty+  getType (ATVar ty _) = ty+  getType (ATPrim ty _) = ty+  getType ATUnit = TyUnit+  getType (ATBool ty _) = ty+  getType (ATNat ty _) = ty+  getType (ATRat _) = TyF+  getType (ATChar _) = TyC+  getType (ATString _) = TyList TyC+  getType (ATAbs _ ty _) = ty+  getType (ATApp ty _ _) = ty+  getType (ATTup ty _) = ty+  getType (ATTyOp ty _ _) = ty+  getType (ATChain ty _ _) = ty+  getType (ATContainer ty _ _ _) = ty   getType (ATContainerComp ty _ _) = ty-  getType (ATLet ty _)             = ty-  getType (ATCase ty _)            = ty-  getType (ATTest _ _ )            = TyProp+  getType (ATLet ty _) = ty+  getType (ATCase ty _) = ty+  getType (ATTest _ _) = TyProp -  setType ty (ATVar _ x      )       = ATVar ty x-  setType ty (ATPrim _ x     )       = ATPrim ty x-  setType _  ATUnit                  = ATUnit-  setType ty (ATBool _ b)            = ATBool ty b-  setType ty (ATNat _ x      )       = ATNat ty x-  setType _  (ATRat r)               = ATRat r-  setType _ (ATChar c)               = ATChar c-  setType _ (ATString cs)            = ATString cs-  setType ty (ATAbs q _ x    )       = ATAbs q ty x-  setType ty (ATApp _ x y    )       = ATApp ty x y-  setType ty (ATTup _ x      )       = ATTup ty x-  setType ty (ATTyOp _ x y   )       = ATTyOp ty x y-  setType ty (ATChain _ x y  )       = ATChain ty x y-  setType ty (ATContainer _ x y z)   = ATContainer ty x y z+  setType ty (ATVar _ x) = ATVar ty x+  setType ty (ATPrim _ x) = ATPrim ty x+  setType _ ATUnit = ATUnit+  setType ty (ATBool _ b) = ATBool ty b+  setType ty (ATNat _ x) = ATNat ty x+  setType _ (ATRat r) = ATRat r+  setType _ (ATChar c) = ATChar c+  setType _ (ATString cs) = ATString cs+  setType ty (ATAbs q _ x) = ATAbs q ty x+  setType ty (ATApp _ x y) = ATApp ty x y+  setType ty (ATTup _ x) = ATTup ty x+  setType ty (ATTyOp _ x y) = ATTyOp ty x y+  setType ty (ATChain _ x y) = ATChain ty x y+  setType ty (ATContainer _ x y z) = ATContainer ty x y z   setType ty (ATContainerComp _ x y) = ATContainerComp ty x y-  setType ty (ATLet _ x      )       = ATLet ty x-  setType ty (ATCase _ x     )       = ATCase ty x-  setType _ (ATTest vs x)            = ATTest vs x+  setType ty (ATLet _ x) = ATLet ty x+  setType ty (ATCase _ x) = ATCase ty x+  setType _ (ATTest vs x) = ATTest vs x  instance HasType APattern where-  getType (APVar ty _)     = ty-  getType (APWild ty)      = ty-  getType APUnit           = TyUnit-  getType (APBool _)       = TyBool-  getType (APChar _)       = TyC-  getType (APString _)     = TyList TyC-  getType (APTup ty _)     = ty-  getType (APInj ty _ _)   = ty-  getType (APNat ty _)     = ty-  getType (APCons ty _ _)  = ty-  getType (APList ty _)    = ty+  getType (APVar ty _) = ty+  getType (APWild ty) = ty+  getType APUnit = TyUnit+  getType (APBool _) = TyBool+  getType (APChar _) = TyC+  getType (APString _) = TyList TyC+  getType (APTup ty _) = ty+  getType (APInj ty _ _) = ty+  getType (APNat ty _) = ty+  getType (APCons ty _ _) = ty+  getType (APList ty _) = ty   getType (APAdd ty _ _ _) = ty   getType (APMul ty _ _ _) = ty-  getType (APSub ty _ _)   = ty-  getType (APNeg ty _)     = ty-  getType (APFrac ty _ _)  = ty+  getType (APSub ty _ _) = ty+  getType (APNeg ty _) = ty+  getType (APFrac ty _ _) = ty  instance HasType ABranch where   getType = getType . snd . unsafeUnbind@@ -451,7 +475,7 @@ substQT :: QName ATerm -> ATerm -> ATerm -> ATerm substQT x s = transform $ \case   t@(ATVar _ y)-    | x == y    -> s+    | x == y -> s     | otherwise -> t   t -> t @@ -464,32 +488,34 @@  explode :: ATerm -> Term explode = \case-  ATVar ty x             -> TAscr (TVar (coerce (qname x))) (toPolyType ty)-  ATPrim ty x            -> TAscr (TPrim x) (toPolyType ty)-  ATLet ty tel           -> TAscr (TLet (explodeTelescope explodeBinding tel)) (toPolyType ty)-  ATUnit                 -> TUnit-  ATBool _ty b           -> TBool b-  ATNat ty x             -> TAscr (TNat x) (toPolyType ty)-  ATRat r                -> TRat r-  ATChar c               -> TChar c-  ATString cs            -> TString cs-  ATAbs q ty a           -> TAscr (TAbs q (explodeAbs a)) (toPolyType ty)-  ATApp ty x y           -> TAscr (TApp (explode x) (explode y)) (toPolyType ty)-  ATTup ty xs            -> TAscr (TTup (map explode xs)) (toPolyType ty)-  ATCase ty bs           -> TAscr (TCase (map explodeBranch bs)) (toPolyType ty)-  ATChain ty t ls        -> TAscr (TChain (explode t) (map explodeLink ls)) (toPolyType ty)-  ATTyOp ty x y          -> TAscr (TTyOp x y) (toPolyType ty)+  ATVar ty x -> TAscr (TVar (coerce (qname x))) (toPolyType ty)+  ATPrim ty x -> TAscr (TPrim x) (toPolyType ty)+  ATLet ty tel -> TAscr (TLet (explodeTelescope explodeBinding tel)) (toPolyType ty)+  ATUnit -> TUnit+  ATBool _ty b -> TBool b+  ATNat ty x -> TAscr (TNat x) (toPolyType ty)+  ATRat r -> TRat r+  ATChar c -> TChar c+  ATString cs -> TString cs+  ATAbs q ty a -> TAscr (TAbs q (explodeAbs a)) (toPolyType ty)+  ATApp ty x y -> TAscr (TApp (explode x) (explode y)) (toPolyType ty)+  ATTup ty xs -> TAscr (TTup (map explode xs)) (toPolyType ty)+  ATCase ty bs -> TAscr (TCase (map explodeBranch bs)) (toPolyType ty)+  ATChain ty t ls -> TAscr (TChain (explode t) (map explodeLink ls)) (toPolyType ty)+  ATTyOp ty x y -> TAscr (TTyOp x y) (toPolyType ty)   ATContainer ty c ts el ->     TAscr       (TContainer c (map (explode *** fmap explode) ts) (fmap (fmap explode) el))       (toPolyType ty)   ATContainerComp ty c b -> TAscr (TContainerComp c (explodeTelescope explodeQual b)) (toPolyType ty)-  ATTest _vs x           -> TAscr (explode x) (toPolyType TyProp)+  ATTest _vs x -> TAscr (explode x) (toPolyType TyProp) -explodeTelescope-  :: (Alpha a, Alpha b)-  => (a -> b) -> Bind (Telescope a) ATerm -> Bind (Telescope b) Term-explodeTelescope explodeBinder (unsafeUnbind -> (xs,at)) = bind (mapTelescope explodeBinder xs) (explode at)+explodeTelescope ::+  (Alpha a, Alpha b) =>+  (a -> b) ->+  Bind (Telescope a) ATerm ->+  Bind (Telescope b) Term+explodeTelescope explodeBinder (unsafeUnbind -> (xs, at)) = bind (mapTelescope explodeBinder xs) (explode at)  explodeBinding :: ABinding -> Binding explodeBinding (ABinding m b (unembed -> n)) = Binding m (coerce b) (embed (explode n))@@ -499,34 +525,34 @@  explodePattern :: APattern -> Pattern explodePattern = \case-  APVar ty x      -> PAscr (PVar (coerce x)) ty-  APWild ty       -> PAscr PWild ty-  APUnit          -> PUnit-  APBool b        -> PBool b-  APChar c        -> PChar c-  APString s      -> PString s-  APTup ty ps     -> PAscr (PTup (map explodePattern ps)) ty-  APInj ty s p    -> PAscr (PInj s (explodePattern p)) ty-  APNat ty n      -> PAscr (PNat n) ty+  APVar ty x -> PAscr (PVar (coerce x)) ty+  APWild ty -> PAscr PWild ty+  APUnit -> PUnit+  APBool b -> PBool b+  APChar c -> PChar c+  APString s -> PString s+  APTup ty ps -> PAscr (PTup (map explodePattern ps)) ty+  APInj ty s p -> PAscr (PInj s (explodePattern p)) ty+  APNat ty n -> PAscr (PNat n) ty   APCons ty p1 p2 -> PAscr (PCons (explodePattern p1) (explodePattern p2)) ty-  APList ty ps    -> PAscr (PList (map explodePattern ps)) ty-  APAdd ty s p t  -> PAscr (PAdd s (explodePattern p) (explode t)) ty-  APMul ty s p t  -> PAscr (PMul s (explodePattern p) (explode t)) ty-  APSub ty p t    -> PAscr (PSub (explodePattern p) (explode t)) ty-  APNeg ty p      -> PAscr (PNeg (explodePattern p)) ty-  APFrac ty p q   -> PAscr (PFrac (explodePattern p) (explodePattern q)) ty+  APList ty ps -> PAscr (PList (map explodePattern ps)) ty+  APAdd ty s p t -> PAscr (PAdd s (explodePattern p) (explode t)) ty+  APMul ty s p t -> PAscr (PMul s (explodePattern p) (explode t)) ty+  APSub ty p t -> PAscr (PSub (explodePattern p) (explode t)) ty+  APNeg ty p -> PAscr (PNeg (explodePattern p)) ty+  APFrac ty p q -> PAscr (PFrac (explodePattern p) (explodePattern q)) ty  explodeBranch :: ABranch -> Branch explodeBranch = explodeTelescope explodeGuard  explodeGuard :: AGuard -> Guard-explodeGuard (AGBool (unembed -> at))   = GBool (embed (explode at))+explodeGuard (AGBool (unembed -> at)) = GBool (embed (explode at)) explodeGuard (AGPat (unembed -> at) ap) = GPat (embed (explode at)) (explodePattern ap)-explodeGuard (AGLet ab)                 = GLet (explodeBinding ab)+explodeGuard (AGLet ab) = GLet (explodeBinding ab)  explodeLink :: ALink -> Link explodeLink (ATLink bop at) = TLink bop (explode at)  explodeQual :: AQual -> Qual explodeQual (AQBind x (unembed -> at)) = QBind (coerce x) (embed (explode at))-explodeQual (AQGuard (unembed -> at))  = QGuard (embed (explode at))+explodeQual (AQGuard (unembed -> at)) = QGuard (embed (explode at))

@@ -1,4 +1,7 @@ -----------------------------------------------------------------------------++-----------------------------------------------------------------------------+ -- | -- Module      :  Disco.Compile -- Copyright   :  disco team and contributors@@ -8,37 +11,39 @@ -- -- Compiling the typechecked, desugared AST to the untyped core -- language.------------------------------------------------------------------------------- module Disco.Compile where -import           Control.Monad                    ((<=<))-import           Data.Bool                        (bool)-import           Data.Coerce-import qualified Data.Map                         as M-import           Data.Ratio-import           Data.Set                         (Set)-import qualified Data.Set                         as S-import           Data.Set.Lens                    (setOf)+import Control.Monad ((<=<))+import Data.Bool (bool)+import Data.Coerce+import qualified Data.Map as M+import Data.Ratio+import Data.Set (Set)+import qualified Data.Set as S+import Data.Set.Lens (setOf) -import           Disco.Effects.Fresh-import           Polysemy                         (Member, Sem, run)-import           Unbound.Generics.LocallyNameless (Name, bind, string2Name,-                                                   unembed)+import Disco.Effects.Fresh+import Polysemy (Member, Sem, run)+import Unbound.Generics.LocallyNameless (+  Name,+  bind,+  string2Name,+  unembed,+ ) -import           Disco.AST.Core-import           Disco.AST.Desugared-import           Disco.AST.Generic-import           Disco.AST.Typed-import           Disco.Context                    as Ctx-import           Disco.Desugar-import           Disco.Module-import           Disco.Names-import           Disco.Syntax.Operators-import           Disco.Syntax.Prims-import qualified Disco.Typecheck.Graph            as G-import           Disco.Types-import           Disco.Util+import Disco.AST.Core+import Disco.AST.Desugared+import Disco.AST.Generic+import Disco.AST.Typed+import Disco.Context as Ctx+import Disco.Desugar+import Disco.Module+import Disco.Names+import Disco.Syntax.Operators+import Disco.Syntax.Prims+import qualified Disco.Typecheck.Graph as G+import Disco.Types+import Disco.Util  ------------------------------------------------------------ -- Convenience operations@@ -106,19 +111,18 @@   -- have   --   --   fT = force (delay fL. [force fL / fT] body)-  | f `S.member` setOf fvQ defn = return . (:[]) $-    (fT, CForce (CProj L (CDelay (bind [qname fL] [substQC fT (CForce (CVar fL)) cdefn]))))-+  | f `S.member` setOf fvQ defn =+      return . (: []) $+        (fT, CForce (CProj L (CDelay (bind [qname fL] [substQC fT (CForce (CVar fL)) cdefn]))))   -- A non-recursive definition just compiles simply.   | otherwise =-    return [(fT, cdefn)]--  where-    fT, fL :: QName Core-    fT = coerce f-    fL = localName (coerce (qname f))+      return [(fT, cdefn)]+ where+  fT, fL :: QName Core+  fT = coerce f+  fL = localName (coerce (qname f)) -    cdefn = compileThing desugarDefn defn+  cdefn = compileThing desugarDefn defn  -- A group of mutually recursive definitions  {f = fbody, g = gbody, ...} -- compiles to@@ -140,12 +144,12 @@       bodies' :: [Core]       bodies' = map (substsQC forceVars . compileThing desugarDefn) bodies   return $-    (grp, CDelay (bind (map qname varsL) bodies')) :-    zip varsT (for [0 ..] $ CForce . flip proj (CVar grp))-  where-    proj :: Int -> Core -> Core-    proj 0 = CProj L-    proj n = proj (n -1) . CProj R+    (grp, CDelay (bind (map qname varsL) bodies'))+      : zip varsT (for [0 ..] $ CForce . flip proj (CVar grp))+ where+  proj :: Int -> Core -> Core+  proj 0 = CProj L+  proj n = proj (n - 1) . CProj R  ------------------------------------------------------------ -- Compiling terms@@ -166,22 +170,22 @@   cbody <- compileDTerm body   case q of     Lam -> return $ abstract xs cbody-    Ex  -> return $ quantify (OExists tys) (abstract xs cbody)+    Ex -> return $ quantify (OExists tys) (abstract xs cbody)     All -> return $ quantify (OForall tys) (abstract xs cbody)-  where-    -- Gather nested abstractions with the same quantifier.-    unbindDeep :: Member Fresh r => DTerm -> Sem r ([Name DTerm], [Type], DTerm)-    unbindDeep (DTAbs q' ty l) | q == q' = do-      (name, inner) <- unbind l-      (ns, tys, body) <- unbindDeep inner-      return (name : ns, ty : tys, body)-    unbindDeep t = return ([], [], t)+ where+  -- Gather nested abstractions with the same quantifier.+  unbindDeep :: Member Fresh r => DTerm -> Sem r ([Name DTerm], [Type], DTerm)+  unbindDeep (DTAbs q' ty l) | q == q' = do+    (name, inner) <- unbind l+    (ns, tys, body) <- unbindDeep inner+    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 :: [Name DTerm] -> Core -> Core+  abstract xs body = CAbs (bind (map coerce xs) body) -    quantify :: Op -> Core -> Core-    quantify op = CApp (CConst op)+  quantify :: Op -> Core -> Core+  quantify op = CApp (CConst op)  -- Special case for Cons, which compiles to a constructor application -- rather than a function application.@@ -197,12 +201,12 @@   CPair <$> compileDTerm t1 <*> compileDTerm t2 compileDTerm (DTCase _ bs) = CApp <$> compileCase bs <*> pure CUnit compileDTerm (DTTyOp _ op ty) = return $ CApp (CConst (tyOps ! op)) (CType ty)-  where-    tyOps =-      M.fromList-        [ Enumerate ==> OEnum,-          Count ==> OCount-        ]+ where+  tyOps =+    M.fromList+      [ Enumerate ==> OEnum+      , Count ==> OCount+      ] compileDTerm (DTNil _) = return $ CInj L CUnit compileDTerm (DTTest info t) = CTest (coerce info) <$> compileDTerm t @@ -231,27 +235,27 @@   hd <- fresh (string2Name "hd")   tl <- fresh (string2Name "tl")   return $ CAbs $ 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))- compilePrim _ PrimRight = do   a <- fresh (string2Name "a")   return $ CAbs $ 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 compilePrim _ PrimFloor = return $ CConst OFloor compilePrim _ PrimCeil = return $ CConst OCeil-compilePrim (TySet _ :->: _) PrimAbs = return $-  CVar (Named Stdlib "container" .- string2Name "setSize")-compilePrim (TyBag _ :->: _) PrimAbs = return $-  CVar (Named Stdlib "container" .- string2Name "bagSize")-compilePrim (TyList _ :->: _) PrimAbs = return $-  CVar (Named Stdlib "list" .- string2Name "length")-compilePrim _                PrimAbs = return $ CConst OAbs+compilePrim (TySet _ :->: _) PrimAbs =+  return $+    CVar (Named Stdlib "container" .- string2Name "setSize")+compilePrim (TyBag _ :->: _) PrimAbs =+  return $+    CVar (Named Stdlib "container" .- string2Name "bagSize")+compilePrim (TyList _ :->: _) PrimAbs =+  return $+    CVar (Named Stdlib "list" .- string2Name "length")+compilePrim _ PrimAbs = return $ CConst OAbs compilePrim (TySet _ :->: _) PrimPower = return $ CConst OPower compilePrim (TyBag _ :->: _) PrimPower = return $ CConst OPower compilePrim ty PrimPower = compilePrimErr PrimPower ty@@ -284,34 +288,38 @@ compilePrim ty PrimConnect = compilePrimErr PrimConnect ty compilePrim _ PrimInsert = return $ CConst OInsert compilePrim _ PrimLookup = return $ CConst OLookup-compilePrim (_ :*: TyList _ :->: _) PrimEach = return $-  CVar (Named Stdlib "list" .- string2Name "eachlist")+compilePrim (_ :*: TyList _ :->: _) PrimEach =+  return $+    CVar (Named Stdlib "list" .- string2Name "eachlist") compilePrim (_ :*: TyBag _ :->: TyBag _) PrimEach = return $ CConst OEachBag compilePrim (_ :*: TySet _ :->: TySet _) PrimEach = return $ CConst OEachSet compilePrim ty PrimEach = compilePrimErr PrimEach ty compilePrim (_ :*: _ :*: TyList _ :->: _) PrimReduce =   return $ CVar (Named Stdlib "list" .- string2Name "foldr")-compilePrim (_ :*: _ :*: TyBag _ :->: _) PrimReduce = return $-  CVar (Named Stdlib "container" .- string2Name "reducebag")-compilePrim (_ :*: _ :*: TySet _ :->: _) PrimReduce = return $-  CVar (Named Stdlib "container" .- string2Name "reduceset")+compilePrim (_ :*: _ :*: TyBag _ :->: _) PrimReduce =+  return $+    CVar (Named Stdlib "container" .- string2Name "reducebag")+compilePrim (_ :*: _ :*: TySet _ :->: _) PrimReduce =+  return $+    CVar (Named Stdlib "container" .- string2Name "reduceset") compilePrim ty PrimReduce = compilePrimErr PrimReduce ty-compilePrim (_ :*: TyList _ :->: _) PrimFilter = return $-  CVar (Named Stdlib "list" .- string2Name "filterlist")+compilePrim (_ :*: TyList _ :->: _) PrimFilter =+  return $+    CVar (Named Stdlib "list" .- string2Name "filterlist") compilePrim (_ :*: TyBag _ :->: _) PrimFilter = return $ CConst OFilterBag compilePrim (_ :*: TySet _ :->: _) PrimFilter = return $ CConst OFilterBag compilePrim ty PrimFilter = compilePrimErr PrimFilter ty-compilePrim (_ :->: TyList _) PrimJoin = return $-  CVar (Named Stdlib "list" .- string2Name "concat")+compilePrim (_ :->: TyList _) PrimJoin =+  return $+    CVar (Named Stdlib "list" .- string2Name "concat") compilePrim (_ :->: TyBag _) PrimJoin = return $ CConst OBagUnions-compilePrim (_ :->: TySet _) PrimJoin = return $-  CVar (Named Stdlib "container" .- string2Name "unions")+compilePrim (_ :->: TySet _) PrimJoin =+  return $+    CVar (Named Stdlib "container" .- string2Name "unions") compilePrim ty PrimJoin = compilePrimErr PrimJoin ty- compilePrim (_ :*: TyBag _ :*: _ :->: _) PrimMerge = return $ CConst OMerge compilePrim (_ :*: TySet _ :*: _ :->: _) PrimMerge = return $ CConst OMerge-compilePrim ty                           PrimMerge = compilePrimErr PrimMerge ty-+compilePrim ty PrimMerge = compilePrimErr PrimMerge ty compilePrim _ PrimIsPrime = return $ CConst OIsPrime compilePrim _ PrimFactor = return $ CConst OFactor compilePrim _ PrimFrac = return $ CConst OFrac@@ -418,13 +426,14 @@   UOp ->   Core compileUOp _ op = CConst (coreUOps ! op)-  where-    -- Just look up the corresponding core operator.-    coreUOps =-      M.fromList-        [ Neg ==> ONeg,-          Fact ==> OFact-        ]+ where+  -- Just look up the corresponding core operator.+  coreUOps =+    M.fromList+      [ Neg ==> ONeg+      , Fact ==> OFact+      , Not ==> ONotProp+      ]  -- | Compile a binary operator.  This function needs to know the types --   of the arguments and result since some operators are overloaded@@ -462,13 +471,13 @@ -- addition and multiplication. compileBOp (TyGraph _) (TyGraph _) (TyGraph _) op   | op `elem` [Add, Mul] =-    CConst (regularOps ! op)-  where-    regularOps =-      M.fromList-        [ Add ==> OOverlay,-          Mul ==> OConnect-        ]+      CConst (regularOps ! op)+ where+  regularOps =+    M.fromList+      [ Add ==> OOverlay+      , Mul ==> OConnect+      ]  -- The Cartesian product operator just compiles to library function calls. compileBOp (TySet _) _ _ CartProd =@@ -477,28 +486,31 @@   CVar (Named Stdlib "container" .- string2Name "bagCP") compileBOp (TyList _) _ _ CartProd =   CVar (Named Stdlib "list" .- string2Name "listCP")- -- Some regular arithmetic operations that just translate straightforwardly. compileBOp _ _ _ op   | op `M.member` regularOps = CConst (regularOps ! op)-  where-    regularOps =-      M.fromList-        [ Add ==> OAdd,-          Mul ==> OMul,-          Div ==> ODiv,-          Exp ==> OExp,-          Mod ==> OMod,-          Divides ==> ODivides,-          Choose ==> OMultinom,-          Eq ==> OEq,-          Lt ==> OLt-        ]+ where+  regularOps =+    M.fromList+      [ Add ==> OAdd+      , Mul ==> OMul+      , Div ==> ODiv+      , Exp ==> OExp+      , Mod ==> OMod+      , Divides ==> ODivides+      , Choose ==> OMultinom+      , Eq ==> OEq+      , Lt ==> OLt+      , And ==> OAnd+      , Or ==> OOr+      , Impl ==> OImpl+      ]  -- ShouldEq 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 (TyList _) _ Elem = CConst OListElem compileBOp _ty _ _ Elem = CConst OBagElem compileBOp ty1 ty2 resTy op =

@@ -1,6 +1,11 @@ {-# LANGUAGE DeriveTraversable #-}  -----------------------------------------------------------------------------++-----------------------------------------------------------------------------++-- SPDX-License-Identifier: BSD-3-Clause+ -- | -- Module      :  Disco.Context -- Copyright   :  disco team and contributors@@ -9,81 +14,80 @@ -- A *context* is a mapping from names to other things (such as types -- or values).  This module defines a generic type of contexts which -- is used in many different places throughout the disco codebase.------------------------------------------------------------------------------------- SPDX-License-Identifier: BSD-3-Clause--module Disco.Context-       ( -- * Context type-         Ctx--         -- * Construction-       , emptyCtx-       , singleCtx-       , fromList-       , ctxForModule-       , localCtx+module Disco.Context (+  -- * Context type+  Ctx, -       -- * Insertion-       , insert-       , extend-       , extends+  -- * Construction+  emptyCtx,+  singleCtx,+  fromList,+  ctxForModule,+  localCtx, -       -- * Query-       , null-       , lookup, lookup'-       , lookupNonLocal, lookupNonLocal'-       , lookupAll, lookupAll'+  -- * Insertion+  insert,+  extend,+  extends, -       -- * Conversion-       , names-       , elems-       , assocs-       , keysSet+  -- * Query+  null,+  lookup,+  lookup',+  lookupNonLocal,+  lookupNonLocal',+  lookupAll,+  lookupAll', -       -- * Traversal-       , coerceKeys-       , restrictKeys+  -- * Conversion+  names,+  elems,+  assocs,+  keysSet, -       -- * Combination-       , joinCtx-       , joinCtxs+  -- * Traversal+  coerceKeys,+  restrictKeys, -       -- * Filter-       , filter+  -- * Combination+  joinCtx,+  joinCtxs, -       ) where+  -- * Filter+  filter,+) where -import           Control.Monad                    ((<=<))-import           Data.Bifunctor                   (first, second)-import           Data.Coerce-import           Data.Map                         (Map)-import qualified Data.Map                         as M-import           Data.Map.Merge.Lazy              as MM-import           Data.Set                         (Set)-import qualified Data.Set                         as S-import           Prelude                          hiding (filter, lookup, null)+import Control.Monad ((<=<))+import Data.Bifunctor (first, second)+import Data.Coerce+import Data.Map (Map)+import qualified Data.Map as M+import Data.Map.Merge.Lazy as MM+import Data.Set (Set)+import qualified Data.Set as S+import Prelude hiding (filter, lookup, null) -import           Unbound.Generics.LocallyNameless (Name)+import Unbound.Generics.LocallyNameless (Name) -import           Polysemy-import           Polysemy.Reader+import Polysemy+import Polysemy.Reader -import           Disco.Names                      (ModuleName,-                                                   NameProvenance (..),-                                                   QName (..))+import Disco.Names (+  ModuleName,+  NameProvenance (..),+  QName (..),+ )  -- | A context maps qualified names to things.  In particular a @Ctx a --   b@ maps qualified names for @a@s to values of type @b@.-newtype Ctx a b = Ctx { getCtx :: M.Map NameProvenance (M.Map (Name a) b) }+newtype Ctx a b = Ctx {getCtx :: M.Map NameProvenance (M.Map (Name a) b)}   deriving (Eq, Show, Functor, Foldable, Traversable) -  -- Note that we implement a context as a nested map from-  -- NameProvenance to Name to b, rather than as a Map QName b.  They-  -- are isomorphic, but this way it is easier to do name resolution,-  -- because given an (unqualified) Name, we can look it up in each-  -- inner map corresponding to modules that are in scope.+-- Note that we implement a context as a nested map from+-- NameProvenance to Name to b, rather than as a Map QName b.  They+-- are isomorphic, but this way it is easier to do name resolution,+-- because given an (unqualified) Name, we can look it up in each+-- inner map corresponding to modules that are in scope.  instance Semigroup (Ctx a b) where   (<>) = joinCtx@@ -159,8 +163,8 @@ -- | Look up all the non-local bindings of a name in a context. lookupNonLocal' :: Name a -> Ctx a b -> [(ModuleName, b)] lookupNonLocal' n = nonLocal . lookupAll' n-  where-    nonLocal bs = [(m,b) | (QName (QualifiedName m) _, b) <- bs]+ where+  nonLocal bs = [(m, b) | (QName (QualifiedName m) _, b) <- bs]  -- | Look up all the bindings of an (unqualified) name in an ambient context. lookupAll :: Member (Reader (Ctx a b)) r => Name a -> Sem r [(QName a, b)]@@ -186,9 +190,9 @@ --   context. assocs :: Ctx a b -> [(QName a, b)] assocs = concatMap (uncurry modAssocs) . M.assocs . getCtx-  where-    modAssocs :: NameProvenance -> Map (Name a) b -> [(QName a, b)]-    modAssocs p = map (first (QName p)) . M.assocs+ where+  modAssocs :: NameProvenance -> Map (Name a) b -> [(QName a, b)]+  modAssocs p = map (first (QName p)) . M.assocs  -- | Return a set of all qualified names in the context. keysSet :: Ctx a b -> Set (QName a)@@ -205,9 +209,9 @@ -- | Restrict a context to only the keys in the given set. restrictKeys :: Ctx a b -> Set (QName a) -> Ctx a b restrictKeys ctx xs = Ctx . restrict m . getCtx $ ctx-  where-    restrict = MM.merge MM.dropMissing MM.dropMissing (MM.zipWithMatched (\_ ns m' -> M.restrictKeys m' ns))-    m = M.fromListWith S.union . map (\(QName p n) -> (p, S.singleton n)) . S.toList $ xs+ where+  restrict = MM.merge MM.dropMissing MM.dropMissing (MM.zipWithMatched (\_ ns m' -> M.restrictKeys m' ns))+  m = M.fromListWith S.union . map (\(QName p n) -> (p, S.singleton n)) . S.toList $ xs  ------------------------------------------------------------ -- Combination@@ -217,7 +221,7 @@ --   exists in both contexts, the result will use the value from the --   first context, and throw away the value from the second.). joinCtx :: Ctx a b -> Ctx a b -> Ctx a b-joinCtx a b = joinCtxs [a,b]+joinCtx a b = joinCtxs [a, b]  -- | Join a list of contexts (left-biased). joinCtxs :: [Ctx a b] -> Ctx a b

@@ -1,25 +1,25 @@-{-# OPTIONS_GHC -Wno-orphans #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE StandaloneDeriving #-}+{-# OPTIONS_GHC -Wno-orphans #-}  -----------------------------------------------------------------------------++-----------------------------------------------------------------------------+ -- | -- Module      :  Disco.Data -- Copyright   :  disco team and contributors -- Maintainer  :  byorgey@gmail.com -- -- Some orphan 'Data' instances.---------------------------------------------------------------------------------- module Disco.Data where -import           Unbound.Generics.LocallyNameless.Bind-import           Unbound.Generics.LocallyNameless.Embed-import           Unbound.Generics.LocallyNameless.Name+import Unbound.Generics.LocallyNameless.Bind+import Unbound.Generics.LocallyNameless.Embed+import Unbound.Generics.LocallyNameless.Name -import           Data.Data                               (Data)-import           Unbound.Generics.LocallyNameless.Rebind+import Data.Data (Data)+import Unbound.Generics.LocallyNameless.Rebind  ------------------------------------------------------------ -- Some orphan instances@@ -29,4 +29,3 @@ deriving instance Data t => Data (Embed t) deriving instance (Data a, Data b) => Data (Rebind a b) deriving instance Data a => Data (Name a)-

@@ -1,4 +1,7 @@ -----------------------------------------------------------------------------++-----------------------------------------------------------------------------+ -- | -- Module      :  Disco.Desugar -- Copyright   :  disco team and contributors@@ -8,43 +11,49 @@ -- -- Desugaring the typechecked surface language to a (still typed) -- simpler language.-----------------------------------------------------------------------------------module Disco.Desugar-       ( -- * Running desugaring computations-         runDesugar+module Disco.Desugar (+  -- * Running desugaring computations+  runDesugar, -         -- * Programs, terms, and properties-       , desugarDefn, desugarTerm, desugarProperty+  -- * Programs, terms, and properties+  desugarDefn,+  desugarTerm,+  desugarProperty, -         -- * Case expressions and patterns-       , desugarBranch, desugarGuards-       )-       where+  -- * Case expressions and patterns+  desugarBranch,+  desugarGuards,+)+where -import           Control.Monad.Cont-import           Data.Bool                               (bool)-import           Data.Coerce-import           Data.Maybe                              (fromMaybe, isJust)+import Control.Monad.Cont+import Data.Bool (bool)+import Data.Coerce+import Data.Maybe (fromMaybe, isJust) -import           Disco.AST.Desugared-import           Disco.AST.Surface-import           Disco.AST.Typed-import           Disco.Module-import           Disco.Names-import           Disco.Syntax.Operators-import           Disco.Syntax.Prims-import           Disco.Typecheck                         (containerTy)-import           Disco.Types+import Disco.AST.Desugared+import Disco.AST.Surface+import Disco.AST.Typed+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, Name, bind,-                                                          embed, name2String,-                                                          string2Name, unembed,-                                                          unrebind)-import           Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)+import Disco.Effects.Fresh+import Polysemy (Member, Sem, run)+import Unbound.Generics.LocallyNameless (+  Bind,+  Name,+  bind,+  embed,+  name2String,+  string2Name,+  unembed,+  unrebind,+ )+import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)  ------------------------------------------------------------ -- Running desugaring computations@@ -53,11 +62,12 @@ -- | Run a desugaring computation. runDesugar :: Sem '[Fresh] a -> a runDesugar = run . runFresh1-  -- Using runFresh1 is a bit of a hack; that way we won't-  -- ever pick a name with #0 (which is what is generated by default-  -- by string2Name), hence won't conflict with any existing free-  -- variables which came from the parser. +-- Using runFresh1 is a bit of a hack; that way we won't+-- ever pick a name with #0 (which is what is generated by default+-- by string2Name), hence won't conflict with any existing free+-- variables which came from the parser.+ ------------------------------------------------------------ -- ATerm DSL ------------------------------------------------------------@@ -71,20 +81,20 @@  tapp :: ATerm -> ATerm -> ATerm tapp t1 t2 = ATApp resTy t1 t2-  where-    resTy = case getType t1 of-      (_ :->: r) -> r-      ty         -> error $ "Impossible! Got non-function type " ++ show ty ++ " in tapp"+ where+  resTy = case getType t1 of+    (_ :->: r) -> r+    ty -> error $ "Impossible! Got non-function type " ++ show ty ++ " in tapp"  mkBin :: Type -> BOp -> ATerm -> ATerm -> ATerm-mkBin resTy bop t1 t2-  = tapp (ATPrim (getType t1 :*: getType t2 :->: resTy) (PrimBOp bop)) (mkPair t1 t2)+mkBin resTy bop t1 t2 =+  tapp (ATPrim (getType t1 :*: getType t2 :->: resTy) (PrimBOp bop)) (mkPair t1 t2)  mkUn :: Type -> UOp -> ATerm -> ATerm mkUn resTy uop t = tapp (ATPrim (getType t :->: resTy) (PrimUOp uop)) t  mkPair :: ATerm -> ATerm -> ATerm-mkPair t1 t2 = mkTup [t1,t2]+mkPair t1 t2 = mkTup [t1, t2]  mkTup :: [ATerm] -> ATerm mkTup ts = ATTup (foldr1 (:*:) (map getType ts)) ts@@ -151,14 +161,14 @@  dtapp :: DTerm -> DTerm -> DTerm dtapp t1 t2 = DTApp resTy t1 t2-  where-    resTy = case getType t1 of-      (_ :->: r) -> r-      ty         -> error $ "Impossible! Got non-function type " ++ show ty ++ " in dtapp"+ where+  resTy = case getType t1 of+    (_ :->: r) -> r+    ty -> error $ "Impossible! Got non-function type " ++ show ty ++ " in dtapp"  dtbin :: Type -> Prim -> DTerm -> DTerm -> DTerm-dtbin resTy p dt1 dt2-  = dtapp (DTPrim (getType dt1 :*: getType dt2 :->: resTy) p) (mkDTPair dt1 dt2)+dtbin resTy p dt1 dt2 =+  dtapp (DTPrim (getType dt1 :*: getType dt2 :->: resTy) p) (mkDTPair dt1 dt2)  mkDTPair :: DTerm -> DTerm -> DTerm mkDTPair dt1 dt2 = DTPair (getType dt1 :*: getType dt2) dt1 dt2@@ -181,15 +191,14 @@ --   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 -- Special case for compiling a single lambda with no pattern matching directly to a lambda 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+ where+  getVar (APVar _ x) = coerce x -- General case desugarAbs quant overallTy body = do   clausePairs <- unbindClauses body@@ -205,36 +214,37 @@   let branches = zipWith (mkBranch (zip args patTys)) bodies pats   dcase <- desugarTerm $ ATCase bodyTy branches   return $ mkAbs quant overallTy patTys (coerce args) dcase--  where-    mkBranch :: [(Name ATerm, Type)] -> ATerm -> [APattern] -> ABranch-    mkBranch xs b ps = bind (mkGuards xs ps) b+ where+  mkBranch :: [(Name ATerm, Type)] -> ATerm -> [APattern] -> ABranch+  mkBranch xs b ps = bind (mkGuards xs ps) b -    mkGuards :: [(Name ATerm, Type)] -> [APattern] -> Telescope AGuard-    mkGuards xs ps = toTelescope $ zipWith AGPat (map (\(x,ty) -> embed (atVar ty x)) xs) ps+  mkGuards :: [(Name ATerm, Type)] -> [APattern] -> Telescope AGuard+  mkGuards xs ps = toTelescope $ zipWith AGPat (map (\(x, ty) -> embed (atVar ty x)) xs) ps -    -- To make searches fairer, we lift up directly nested abstractions-    -- 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-      (ps, t) <- liftClause c-      return [(ps, addDbgInfo ps t)]-    unbindClauses cs  = mapM unbind cs+  -- To make searches fairer, we lift up directly nested abstractions+  -- 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+    (ps, t) <- liftClause c+    return [(ps, addDbgInfo ps t)]+  unbindClauses cs = mapM unbind cs -    liftClause :: Member Fresh r => Bind [APattern] ATerm -> Sem r ([APattern], ATerm)-    liftClause c = unbind c >>= \case+  liftClause :: Member Fresh r => Bind [APattern] ATerm -> Sem r ([APattern], ATerm)+  liftClause c =+    unbind c >>= \case       (ps, ATAbs q _ c') | q == quant -> do         (ps', b) <- liftClause c'         return (ps ++ ps', b)       (ps, b) -> return (ps, b) -    -- 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-      where withName (n, ty) = (name2String n, ty, n)+  -- 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+   where+    withName (n, ty) = (name2String n, ty, n)  ------------------------------------------------------------ -- Term desugaring@@ -245,11 +255,14 @@ desugarCList2B :: Member Fresh r => Prim -> Type -> Type -> Type -> Sem r DTerm desugarCList2B p ty cts b = do   c <- fresh (string2Name "c")-  body <- desugarTerm $-    tapp (ATPrim (TyBag cts :->: TyBag b) p)-      (tapp (ATPrim (TyList cts :->: TyBag cts) PrimBag)-        (atVar (TyList cts) c)-      )+  body <-+    desugarTerm $+      tapp+        (ATPrim (TyBag cts :->: TyBag b) p)+        ( tapp+            (ATPrim (TyList cts :->: TyBag cts) PrimBag)+            (atVar (TyList cts) c)+        )   return $ mkLambda ty [c] body  -- | Desugar a typechecked term.@@ -261,43 +274,33 @@   | 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 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)        =+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 [lam] -- Special cases for fully applied operators desugarTerm (ATApp resTy (ATPrim _ (PrimUOp uop)) t)   | uopDesugars (getType t) resTy uop = desugarUnApp resTy uop t-desugarTerm (ATApp resTy (ATPrim _ (PrimBOp bop)) (ATTup _ [t1,t2]))+desugarTerm (ATApp resTy (ATPrim _ (PrimBOp bop)) (ATTup _ [t1, t2]))   | bopDesugars (getType t1) (getType t2) resTy bop = desugarBinApp resTy bop t1 t2--desugarTerm (ATApp ty t1 t2)     =+desugarTerm (ATApp ty t1 t2) =   DTApp ty <$> desugarTerm t1 <*> desugarTerm t2-desugarTerm (ATTup ty ts)        = desugarTuples ty ts-desugarTerm (ATNat ty n)         = return $ DTNat ty n-desugarTerm (ATRat r)            = return $ DTRat r--desugarTerm (ATTyOp ty op t)      = return $ DTTyOp ty op t--desugarTerm (ATChain _ t1 links)  = desugarTerm $ expandChain t1 links-+desugarTerm (ATTup ty ts) = desugarTuples ty ts+desugarTerm (ATNat ty n) = return $ DTNat ty n+desugarTerm (ATRat r) = return $ DTRat r+desugarTerm (ATTyOp ty op t) = return $ DTTyOp ty op t+desugarTerm (ATChain _ t1 links) = desugarTerm $ expandChain t1 links desugarTerm (ATContainer ty c es mell) = desugarContainer ty c es mell- desugarTerm (ATContainerComp _ ctr bqt) = do   (qs, t) <- unbind bqt   desugarComp ctr t qs- desugarTerm (ATLet _ t) = do   (bs, t2) <- unbind t   desugarLet (fromTelescope bs) t2- desugarTerm (ATCase ty bs) = DTCase ty <$> mapM desugarBranch bs- desugarTerm (ATTest info t) = DTTest (coerce info) <$> desugarTerm t  -- | Desugar a property by wrapping its corresponding term in a test@@ -313,7 +316,8 @@ --   desugared, given the type of the argument and result. uopDesugars :: Type -> Type -> UOp -> Bool -- uopDesugars _ (TyFin _) Neg = True-uopDesugars _ _         uop = uop == Not+uopDesugars TyProp TyProp Not = False+uopDesugars _ _ uop = uop == Not  desugarPrimUOp :: Member Fresh r => Type -> Type -> UOp -> Sem r DTerm desugarPrimUOp argTy resTy op = do@@ -324,16 +328,34 @@ -- | Test whether a given binary operator is one that needs to be --   desugared, given the two types of the arguments and the type of the result. bopDesugars :: Type -> Type -> Type -> BOp -> Bool-bopDesugars _   TyN _ Choose = True+bopDesugars _ TyN _ Choose = True -- bopDesugars _   _   (TyFin _) bop | bop `elem` [Add, Mul] = True-bopDesugars _   _   _ bop = bop `elem`-  [ And, Or, Impl, Iff-  , Neq, Gt, Leq, Geq, Min, Max-  , IDiv-  , Sub, SSub-  , Inter, Diff, Union, Subset-  ] +-- 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+bopDesugars _ _ _ bop =+  bop+    `elem` [ And+           , Or+           , Impl+           , Iff+           , Neq+           , Gt+           , Leq+           , Geq+           , Min+           , Max+           , IDiv+           , Sub+           , SSub+           , Inter+           , Diff+           , Union+           , Subset+           ]+ -- | Desugar a primitive binary operator at the given type. desugarPrimBOp :: Member Fresh r => Type -> Type -> Type -> BOp -> Sem r DTerm desugarPrimBOp ty1 ty2 resTy op = do@@ -342,17 +364,18 @@   y <- fresh (string2Name "arg2")   let argsTy = ty1 :*: ty2   body <- desugarBinApp resTy op (atVar ty1 x) (atVar ty2 y)-  return $ mkLambda (argsTy :->: resTy) [p] $-    DTCase resTy-    [ bind-        (toTelescope [DGPat (embed (dtVar argsTy (coerce p))) (DPPair argsTy (coerce x) (coerce y))])-        body-    ]+  return $+    mkLambda (argsTy :->: resTy) [p] $+      DTCase+        resTy+        [ bind+            (toTelescope [DGPat (embed (dtVar argsTy (coerce p))) (DPPair argsTy (coerce x) (coerce y))])+            body+        ]  -- | Desugar a saturated application of a unary operator. --   The first argument is the type of the result. desugarUnApp :: Member Fresh r => Type -> UOp -> ATerm -> Sem r DTerm- -- Desugar negation on TyFin to a negation on TyZ followed by a mod. -- See the comments below re: Add and Mul on TyFin. -- desugarUnApp (TyFin n) Neg t =@@ -360,83 +383,84 @@  -- XXX This should be turned into a standard library definition. -- not t ==> {? false if t, true otherwise ?}-desugarUnApp _ Not t = desugarTerm $-  ATCase TyBool-    [ fls <==. [AGBool (embed t)]-    , tru <==. []-    ]-+desugarUnApp _ Not t =+  desugarTerm $+    ATCase+      TyBool+      [ fls <==. [AGBool (embed t)]+      , tru <==. []+      ] desugarUnApp ty uop t = error $ "Impossible! desugarUnApp " ++ show ty ++ " " ++ show uop ++ " " ++ show t  -- | Desugar a saturated application of a binary operator. --   The first argument is the type of the result. desugarBinApp :: Member Fresh r => Type -> BOp -> ATerm -> ATerm -> Sem r DTerm- -- Implies, and, or should all be turned into a standard library -- definition.  This will require first (1) adding support for -- modules/a standard library, including (2) the ability to define -- infix operators.  -- t1 and t2 ==> {? t2 if t1, false otherwise ?}-desugarBinApp _ And t1 t2 = desugarTerm $-  ATCase TyBool-    [ t2  <==. [tif t1]-    , fls <==. []-    ]-+desugarBinApp _ And t1 t2 =+  desugarTerm $+    ATCase+      TyBool+      [ t2 <==. [tif t1]+      , fls <==. []+      ] -- (t1 implies t2) ==> (not t1 or t2) desugarBinApp _ Impl t1 t2 = desugarTerm $ tnot t1 ||. t2- -- (t1 iff t2) ==> (t1 == t2) desugarBinApp _ Iff t1 t2 = desugarTerm $ t1 ==. t2- -- t1 or t2 ==> {? true if t1, t2 otherwise ?})-desugarBinApp _ Or t1 t2 = desugarTerm $-  ATCase TyBool-    [ tru <==. [tif t1]-    , t2  <==. []-    ]-+desugarBinApp _ Or t1 t2 =+  desugarTerm $+    ATCase+      TyBool+      [ tru <==. [tif t1]+      , t2 <==. []+      ] desugarBinApp _ Neq t1 t2 = desugarTerm $ tnot (t1 ==. t2)-desugarBinApp _ Gt  t1 t2 = desugarTerm $ t2 <. t1+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 <==. []-    ]-+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 $-  ATApp resTy (ATPrim (getType t1 :->: resTy) PrimFloor) (mkBin (getType t1) Div t1 t2)-+desugarBinApp resTy IDiv t1 t2 =+  desugarTerm $+    ATApp resTy (ATPrim (getType t1 :->: resTy) PrimFloor) (mkBin (getType t1) Div t1 t2) -- Desugar normal binomial coefficient (n choose k) to a multinomial -- coefficient with a singleton list, (n choose [k]). -- Note this will only be called when (getType t2 == TyN); see bopDesugars.-desugarBinApp _ Choose t1 t2-  = desugarTerm $ mkBin TyN Choose t1 (ctrSingleton ListContainer t2)--desugarBinApp ty Sub  t1 t2 = desugarTerm $ mkBin ty Add t1 (mkUn ty Neg t2)-desugarBinApp ty SSub t1 t2 = desugarTerm $-  -- t1 -. t2 ==> {? 0 if t1 < t2, t1 - t2 otherwise ?}-  ATCase ty-    [ ATNat ty 0         <==. [tif (t1 <. t2)]-    , mkBin ty Sub t1 t2 <==. []+desugarBinApp _ Choose t1 t2 =+  desugarTerm $ mkBin TyN Choose t1 (ctrSingleton ListContainer t2)+desugarBinApp ty Sub t1 t2 = desugarTerm $ mkBin ty Add t1 (mkUn ty Neg t2)+desugarBinApp ty SSub t1 t2 =+  desugarTerm $+    -- t1 -. t2 ==> {? 0 if t1 < t2, t1 - t2 otherwise ?}+    ATCase+      ty+      [ ATNat ty 0 <==. [tif (t1 <. t2)]+      , mkBin ty Sub t1 t2 <==. []       -- NOTE, the above is slightly bogus since the whole point of SSub is       -- because we can't subtract naturals.  However, this will       -- immediately desugar to a DTerm.  When we write a linting       -- typechecker for DTerms we should allow subtraction on TyN!-    ]-+      ] -- Addition and multiplication on TyFin just desugar to the operation -- followed by a call to mod. -- desugarBinApp (TyFin n) op t1 t2@@ -444,57 +468,60 @@ --       mkBin (TyFin n) Mod --         (mkBin TyN op t1 t2) --         (ATNat TyN n)-    -- Note the typing of this is a bit funny: t1 and t2 presumably-    -- have type (TyFin n), and now we are saying that applying 'op'-    -- to them results in TyN, then applying 'mod' results in a TyFin-    -- n again.  Using TyN as the intermediate result is necessary so-    -- we don't fall into an infinite desugaring loop, and intuitively-    -- makes sense because the idea is that we first do the operation-    -- as a normal operation in "natural land" and then do a mod.-    ---    -- We will have to think carefully about how the linting-    -- typechecker for DTerms should treat TyN and TyFin.  Probably-    -- something like this will work: TyFin is a subtype of TyN, and-    -- TyN can be turned into TyFin with mod.  (We don't want such-    -- typing rules in the surface disco language itself because-    -- implicit coercions from TyFin -> N don't commute with-    -- operations like addition and multiplication, e.g. 3+3 yields 1-    -- if we add them in Z5 and then coerce to Nat, but 6 if we first-    -- coerce both and then add.+-- Note the typing of this is a bit funny: t1 and t2 presumably+-- have type (TyFin n), and now we are saying that applying 'op'+-- to them results in TyN, then applying 'mod' results in a TyFin+-- n again.  Using TyN as the intermediate result is necessary so+-- we don't fall into an infinite desugaring loop, and intuitively+-- makes sense because the idea is that we first do the operation+-- as a normal operation in "natural land" and then do a mod.+--+-- We will have to think carefully about how the linting+-- typechecker for DTerms should treat TyN and TyFin.  Probably+-- something like this will work: TyFin is a subtype of TyN, and+-- TyN can be turned into TyFin with mod.  (We don't want such+-- typing rules in the surface disco language itself because+-- implicit coercions from TyFin -> N don't commute with+-- operations like addition and multiplication, e.g. 3+3 yields 1+-- if we add them in Z5 and then coerce to Nat, but 6 if we first+-- coerce both and then add.  -- Intersection, difference, and union all desugar to an application -- of 'merge' with an appropriate combining operation. desugarBinApp ty op t1 t2   | op `elem` [Inter, Diff, Union] =-    desugarTerm $-    tapps (ATPrim ((TyN :*: TyN :->: TyN) :*: ty :*: ty :->: ty) PrimMerge)-      [ ATPrim (TyN :*: TyN :->: TyN) (mergeOp ty op)-      , t1-      , t2-      ]-  where-    mergeOp _         Inter = PrimBOp Min-    mergeOp _         Diff  = PrimBOp SSub-    mergeOp (TySet _) Union = PrimBOp Max-    mergeOp (TyBag _) Union = PrimBOp Add-    mergeOp _         _     = error $ "Impossible! mergeOp " ++ show ty ++ " " ++ show op+      desugarTerm $+        tapps+          (ATPrim ((TyN :*: TyN :->: TyN) :*: ty :*: ty :->: ty) PrimMerge)+          [ ATPrim (TyN :*: TyN :->: TyN) (mergeOp ty op)+          , t1+          , t2+          ]+ where+  mergeOp _ Inter = PrimBOp Min+  mergeOp _ Diff = PrimBOp SSub+  mergeOp (TySet _) Union = PrimBOp Max+  mergeOp (TyBag _) Union = PrimBOp Add+  mergeOp _ _ = error $ "Impossible! mergeOp " ++ show ty ++ " " ++ show op  -- A ⊆ B  <==>  (A ⊔ B = B) --   where ⊔ denotes 'merge max'. --   Note it is NOT union, since this doesn't work for bags. --   e.g.  bag [1] union bag [1,2] =  bag [1,1,2] /= bag [1,2].-desugarBinApp _ Subset t1 t2 = desugarTerm $-  tapps (ATPrim (ty :*: ty :->: TyBool) (PrimBOp Eq))-  [ tapps (ATPrim ((TyN :*: TyN :->: TyN) :*: ty :*: ty :->: ty) PrimMerge)-    [ ATPrim (TyN :*: TyN :->: TyN) (PrimBOp Max)-    , t1-    , t2-    ]-  , t2   -- XXX sharing-  ]-  where-    ty = getType t1-+desugarBinApp _ Subset t1 t2 =+  desugarTerm $+    tapps+      (ATPrim (ty :*: ty :->: TyBool) (PrimBOp Eq))+      [ tapps+          (ATPrim ((TyN :*: TyN :->: TyN) :*: ty :*: ty :->: ty) PrimMerge)+          [ ATPrim (TyN :*: TyN :->: TyN) (PrimBOp Max)+          , t1+          , t2+          ]+      , t2 -- XXX sharing+      ]+ where+  ty = getType t1 desugarBinApp ty bop t1 t2 = error $ "Impossible! desugarBinApp " ++ show ty ++ " " ++ show bop ++ " " ++ show t1 ++ " " ++ show t2  ------------------------------------------------------------@@ -508,36 +535,37 @@  -- | Expand a container comprehension into an equivalent ATerm. expandComp :: Member Fresh r => Container -> ATerm -> Telescope AQual -> Sem r ATerm- -- [ t | ] = [ t ] expandComp ctr t TelEmpty = return $ ctrSingleton ctr t- -- [ t | q, qs ] = ...-expandComp ctr t (TelCons (unrebind -> (q,qs)))-  = case q of-      -- [ t | x in l, qs ] = join (map (\x -> [t | qs]) l)-      AQBind x (unembed -> lst) -> do-        tqs <- expandComp ctr t qs-        let c      = containerTy ctr-            tTy    = getType t-            xTy    = case getType lst of-                       TyContainer _ e -> e-                       _ -> error "Impossible! Not a container in expandComp"-            joinTy = c (c tTy) :->: c tTy-            mapTy  = (xTy :->: c tTy) :*: c xTy :->: c (c tTy)-        return $ tapp (ATPrim joinTy PrimJoin) $+expandComp ctr t (TelCons (unrebind -> (q, qs))) =+  case q of+    -- [ t | x in l, qs ] = join (map (\x -> [t | qs]) l)+    AQBind x (unembed -> lst) -> do+      tqs <- expandComp ctr t qs+      let c = containerTy ctr+          tTy = getType t+          xTy = case getType lst of+            TyContainer _ e -> e+            _ -> error "Impossible! Not a container in expandComp"+          joinTy = c (c tTy) :->: c tTy+          mapTy = (xTy :->: c tTy) :*: c xTy :->: c (c tTy)+      return $+        tapp (ATPrim joinTy PrimJoin) $           tapp             (ATPrim mapTy PrimEach)-            (mkPair-              (ATAbs Lam (xTy :->: c tTy) (bind [APVar xTy x] tqs))-              lst+            ( mkPair+                (ATAbs Lam (xTy :->: c tTy) (bind [APVar xTy x] tqs))+                lst             ) -      -- [ t | g, qs ] = if g then [ t | qs ] else []-      AQGuard (unembed -> g)    -> do-        tqs <- expandComp ctr t qs-        return $ ATCase (containerTy ctr (getType t))-          [ tqs                    <==. [tif g]+    -- [ t | g, qs ] = if g then [ t | qs ] else []+    AQGuard (unembed -> g) -> do+      tqs <- expandComp ctr t qs+      return $+        ATCase+          (containerTy ctr (getType t))+          [ tqs <==. [tif g]           , ctrNil ctr (getType t) <==. []           ] @@ -553,8 +581,8 @@ desugarLet [] t = desugarTerm t desugarLet ((ABinding _ x (unembed -> t1)) : ls) t =   dtapp-    <$> (DTAbs Lam (getType t1 :->: getType t)-          <$> (bind (coerce x) <$> desugarLet ls t)+    <$> ( DTAbs Lam (getType t1 :->: getType t)+            <$> (bind (coerce x) <$> desugarLet ls t)         )     <*> desugarTerm t1 @@ -569,26 +597,26 @@ --     @\x. \y. \z. q@ mkLambda :: Type -> [Name ATerm] -> DTerm -> DTerm mkLambda funty args c = go funty args-  where-    go _ []                    = c-    go ty@(_ :->: ty2) (x:xs) = DTAbs Lam ty (bind (coerce x) (go ty2 xs))-    go ty as = error $ "Impossible! mkLambda.go " ++ show ty ++ " " ++ show as+ where+  go _ [] = c+  go ty@(_ :->: ty2) (x : xs) = DTAbs Lam ty (bind (coerce x) (go ty2 xs))+  go ty as = error $ "Impossible! mkLambda.go " ++ show ty ++ " " ++ show as  mkQuant :: Quantifier -> [Type] -> [Name ATerm] -> DTerm -> DTerm mkQuant q argtys args c = foldr quantify c (zip args argtys)  where-   quantify (x, ty) body = DTAbs q ty (bind (coerce x) body)+  quantify (x, ty) body = DTAbs q ty (bind (coerce x) body)  mkAbs :: Quantifier -> Type -> [Type] -> [Name ATerm] -> DTerm -> DTerm mkAbs Lam funty _ args c = mkLambda funty args c-mkAbs q _ argtys args c  = mkQuant q argtys args c+mkAbs q _ argtys args c = mkQuant q argtys args c  -- | Desugar a tuple to nested pairs, /e.g./ @(a,b,c,d) ==> (a,(b,(c,d)))@.a desugarTuples :: Member Fresh r => Type -> [ATerm] -> Sem r DTerm-desugarTuples _ [t]                    = desugarTerm t-desugarTuples ty@(_ :*: ty2) (t:ts) = DTPair ty <$> desugarTerm t <*> desugarTuples ty2 ts-desugarTuples ty ats-  = error $ "Impossible! desugarTuples " ++ show ty ++ " " ++ show ats+desugarTuples _ [t] = desugarTerm t+desugarTuples ty@(_ :*: ty2) (t : ts) = DTPair ty <$> desugarTerm t <*> desugarTuples ty2 ts+desugarTuples ty ats =+  error $ "Impossible! desugarTuples " ++ show ty ++ " " ++ show ats  -- | Expand a chain of comparisons into a sequence of binary --   comparisons combined with @and@.  Note we only expand it into@@ -600,7 +628,9 @@ expandChain _ [] = error "Can't happen! expandChain _ []" expandChain t1 [ATLink op t2] = mkBin TyBool op t1 t2 expandChain t1 (ATLink op t2 : links) =-  mkBin TyBool And+  mkBin+    TyBool+    And     (mkBin TyBool op t1 t2)     (expandChain t2 links) @@ -609,7 +639,7 @@ desugarBranch b = do   (ags, at) <- unbind b   dgs <- desugarGuards ags-  d   <- desugarTerm at+  d <- desugarTerm at   return $ bind dgs d  -- | Desugar the list of guards in one branch of a case expression.@@ -617,215 +647,208 @@ --   turned into pattern guards which match against @true@. desugarGuards :: Member Fresh r => Telescope AGuard -> Sem r (Telescope DGuard) desugarGuards = fmap (toTelescope . concat) . mapM desugarGuard . fromTelescope-  where-    desugarGuard :: Member Fresh r => AGuard -> Sem r [DGuard]--    -- A Boolean guard is desugared to a pattern-match on @true = right(unit)@.-    desugarGuard (AGBool (unembed -> at)) = do-      dt <- desugarTerm at-      desugarMatch dt (APInj TyBool R APUnit)--    -- 'let x = t' is desugared to 'when t is x'.-    desugarGuard (AGLet (ABinding _ x (unembed -> at))) = do-      dt <- desugarTerm at-      varMatch dt (coerce x)--    -- Desugaring 'when t is p' is the most complex case; we have to-    -- break down the pattern and match it incrementally.-    desugarGuard (AGPat (unembed -> at) p) = do-      dt <- desugarTerm at-      desugarMatch dt p+ where+  desugarGuard :: Member Fresh r => AGuard -> Sem r [DGuard] -    -- Desugar a guard of the form 'when dt is p'.  An entire match is-    -- the right unit to desugar --- as opposed to, say, writing a-    -- function to desugar a pattern --- since a match may desugar to-    -- multiple matches, and on recursive calls we need to know what-    -- term/variable should be bound to the pattern.-    ---    -- A match may desugar to multiple matches for two reasons:-    ---    --   1. Nested patterns 'explode' into a 'telescope' matching one-    --   constructor at a time, for example, 'when t is (x,y,3)'-    --   becomes 'when t is (x,x0) when x0 is (y,x1) when x1 is 3'.-    --   This makes the order of matching explicit and enables lazy-    --   matching without requiring special support from the-    --   interpreter other than WHNF reduction.-    ---    --   2. Matches against arithmetic patterns desugar to a-    --   combination of matching, computation, and boolean checks.-    --   For example, 'when t is (y+1)' becomes 'when t is x0 if x0 >=-    --   1 let y = x0-1'.-    desugarMatch :: Member Fresh r => DTerm -> APattern -> Sem r [DGuard]-    desugarMatch dt (APVar ty x)      = mkMatch dt (DPVar ty (coerce x))-    desugarMatch _  (APWild _)        = return []-    desugarMatch dt APUnit            = mkMatch dt DPUnit-    desugarMatch dt (APBool b)        = desugarMatch dt (APInj TyBool (bool L R b) APUnit)-    desugarMatch dt (APNat ty n)      = desugarMatch (dtbin TyBool (PrimBOp Eq) dt (DTNat ty n)) (APBool True)-    desugarMatch dt (APChar c)        = desugarMatch (dtbin TyBool (PrimBOp Eq) dt (DTChar c)) (APBool True)-    desugarMatch dt (APString s)      = desugarMatch dt (APList (TyList TyC) (map APChar s))-    desugarMatch dt (APTup tupTy pat) = desugarTuplePats tupTy dt pat-      where-        desugarTuplePats :: Member Fresh r => Type -> DTerm -> [APattern] -> Sem r [DGuard]-        desugarTuplePats _ _  [] = error "Impossible! desugarTuplePats []"-        desugarTuplePats _ t [p] = desugarMatch t p-        desugarTuplePats ty@(_ :*: ty2) t (p:ps) = do-          (x1,gs1) <- varForPat p-          (x2,gs2) <- case ps of-            [APVar _ px2] -> return (coerce px2, [])-            _             -> do-              x <- fresh (string2Name "x")-              (x,) <$> desugarTuplePats ty2 (dtVar ty2 x) ps-          fmap concat . sequence $-            [ mkMatch t $ DPPair ty x1 x2-            , return gs1-            , return gs2-            ]-        desugarTuplePats ty _ _-          = error $ "Impossible! desugarTuplePats with non-pair type " ++ show ty+  -- A Boolean guard is desugared to a pattern-match on @true = right(unit)@.+  desugarGuard (AGBool (unembed -> at)) = do+    dt <- desugarTerm at+    desugarMatch dt (APInj TyBool R APUnit) -    desugarMatch dt (APInj ty s p) = do-      (x,gs) <- varForPat p-      fmap concat . sequence $-        [ mkMatch dt $ DPInj ty s x-        , return gs-        ]+  -- 'let x = t' is desugared to 'when t is x'.+  desugarGuard (AGLet (ABinding _ x (unembed -> at))) = do+    dt <- desugarTerm at+    varMatch dt (coerce x) -    desugarMatch dt (APCons ty p1 p2) = do-      y <- fresh (string2Name "y")-      (x1, gs1) <- varForPat p1-      (x2, gs2) <- varForPat p2+  -- Desugaring 'when t is p' is the most complex case; we have to+  -- break down the pattern and match it incrementally.+  desugarGuard (AGPat (unembed -> at) p) = do+    dt <- desugarTerm at+    desugarMatch dt p -      let eltTy = getType p1-          unrolledTy = eltTy :*: ty+  -- Desugar a guard of the form 'when dt is p'.  An entire match is+  -- the right unit to desugar --- as opposed to, say, writing a+  -- function to desugar a pattern --- since a match may desugar to+  -- multiple matches, and on recursive calls we need to know what+  -- term/variable should be bound to the pattern.+  --+  -- A match may desugar to multiple matches for two reasons:+  --+  --   1. Nested patterns 'explode' into a 'telescope' matching one+  --   constructor at a time, for example, 'when t is (x,y,3)'+  --   becomes 'when t is (x,x0) when x0 is (y,x1) when x1 is 3'.+  --   This makes the order of matching explicit and enables lazy+  --   matching without requiring special support from the+  --   interpreter other than WHNF reduction.+  --+  --   2. Matches against arithmetic patterns desugar to a+  --   combination of matching, computation, and boolean checks.+  --   For example, 'when t is (y+1)' becomes 'when t is x0 if x0 >=+  --   1 let y = x0-1'.+  desugarMatch :: Member Fresh r => DTerm -> APattern -> Sem r [DGuard]+  desugarMatch dt (APVar ty x) = mkMatch dt (DPVar ty (coerce x))+  desugarMatch _ (APWild _) = return []+  desugarMatch dt APUnit = mkMatch dt DPUnit+  desugarMatch dt (APBool b) = desugarMatch dt (APInj TyBool (bool L R b) APUnit)+  desugarMatch dt (APNat ty n) = desugarMatch (dtbin TyBool (PrimBOp Eq) dt (DTNat ty n)) (APBool True)+  desugarMatch dt (APChar c) = desugarMatch (dtbin TyBool (PrimBOp Eq) dt (DTChar c)) (APBool True)+  desugarMatch dt (APString s) = desugarMatch dt (APList (TyList TyC) (map APChar s))+  desugarMatch dt (APTup tupTy pat) = desugarTuplePats tupTy dt pat+   where+    desugarTuplePats :: Member Fresh r => Type -> DTerm -> [APattern] -> Sem r [DGuard]+    desugarTuplePats _ _ [] = error "Impossible! desugarTuplePats []"+    desugarTuplePats _ t [p] = desugarMatch t p+    desugarTuplePats ty@(_ :*: ty2) t (p : ps) = do+      (x1, gs1) <- varForPat p+      (x2, gs2) <- case ps of+        [APVar _ px2] -> return (coerce px2, [])+        _ -> do+          x <- fresh (string2Name "x")+          (x,) <$> desugarTuplePats ty2 (dtVar ty2 x) ps       fmap concat . sequence $-        [ mkMatch dt (DPInj ty R y)-        , mkMatch (dtVar unrolledTy y) (DPPair unrolledTy x1 x2)+        [ mkMatch t $ DPPair ty x1 x2         , return gs1         , return gs2         ]--    desugarMatch dt (APList ty []) = desugarMatch dt (APInj ty L APUnit)-    desugarMatch dt (APList ty ps) =-      desugarMatch dt $ foldr (APCons ty) (APList ty []) ps--    -- when dt is (p + t) ==> when dt is x0; let v = t; [if x0 >= v]; when x0-v is p-    desugarMatch dt (APAdd ty _ p t) = arithBinMatch posRestrict (-.) dt ty p t-      where-        posRestrict plusty-          | plusty `elem` [TyN, TyF] = Just (>=.)-          | otherwise                = Nothing--    -- when dt is (p * t) ==> when dt is x0; let v = t; [if v divides x0]; when x0 / v is p-    desugarMatch dt (APMul ty _ p t) = arithBinMatch intRestrict (/.) dt ty p t-      where-        intRestrict plusty-          | plusty `elem` [TyN, TyZ] = Just (flip (|.))-          | otherwise                = Nothing--    -- when dt is (p - t) ==> when dt is x0; let v = t; when x0 + v is p-    desugarMatch dt (APSub ty p t)  = arithBinMatch (const Nothing) (+.) dt ty p t--    -- when dt is (p/q) ==> when $frac(dt) is (p, q)-    desugarMatch dt (APFrac _ p q)-      = desugarMatch-          (dtapp (DTPrim (TyQ :->: TyZ :*: TyN) PrimFrac) dt)-          (APTup (TyZ :*: TyN) [p, q])+    desugarTuplePats ty _ _ =+      error $ "Impossible! desugarTuplePats with non-pair type " ++ show ty+  desugarMatch dt (APInj ty s p) = do+    (x, gs) <- varForPat p+    fmap concat . sequence $+      [ mkMatch dt $ DPInj ty s x+      , return gs+      ]+  desugarMatch dt (APCons ty p1 p2) = do+    y <- fresh (string2Name "y")+    (x1, gs1) <- varForPat p1+    (x2, gs2) <- varForPat p2 -    -- when dt is (-p) ==> when dt is x0; if x0 < 0; when -x0 is p-    desugarMatch dt (APNeg ty p) = do+    let eltTy = getType p1+        unrolledTy = eltTy :*: ty+    fmap concat . sequence $+      [ mkMatch dt (DPInj ty R y)+      , mkMatch (dtVar unrolledTy y) (DPPair unrolledTy x1 x2)+      , return gs1+      , return gs2+      ]+  desugarMatch dt (APList ty []) = desugarMatch dt (APInj ty L APUnit)+  desugarMatch dt (APList ty ps) =+    desugarMatch dt $ foldr (APCons ty) (APList ty []) ps+  -- when dt is (p + t) ==> when dt is x0; let v = t; [if x0 >= v]; when x0-v is p+  desugarMatch dt (APAdd ty _ p t) = arithBinMatch posRestrict (-.) dt ty p t+   where+    posRestrict plusty+      | plusty `elem` [TyN, TyF] = Just (>=.)+      | otherwise = Nothing -      -- when dt is x0-      (x0, g1) <- varFor dt+  -- when dt is (p * t) ==> when dt is x0; let v = t; [if v divides x0]; when x0 / v is p+  desugarMatch dt (APMul ty _ p t) = arithBinMatch intRestrict (/.) dt ty p t+   where+    intRestrict plusty+      | plusty `elem` [TyN, TyZ] = Just (flip (|.))+      | otherwise = Nothing -      -- if x0 < 0-      g2  <- desugarGuard $ AGBool (embed (atVar ty (coerce x0) <. ATNat ty 0))+  -- when dt is (p - t) ==> when dt is x0; let v = t; when x0 + v is p+  desugarMatch dt (APSub ty p t) = arithBinMatch (const Nothing) (+.) dt ty p t+  -- when dt is (p/q) ==> when $frac(dt) is (p, q)+  desugarMatch dt (APFrac _ p q) =+    desugarMatch+      (dtapp (DTPrim (TyQ :->: TyZ :*: TyN) PrimFrac) dt)+      (APTup (TyZ :*: TyN) [p, q])+  -- when dt is (-p) ==> when dt is x0; if x0 < 0; when -x0 is p+  desugarMatch dt (APNeg ty p) = do+    -- when dt is x0+    (x0, g1) <- varFor dt -      -- when -x0 is p-      neg <- desugarTerm $ mkUn ty Neg (atVar ty (coerce x0))-      g3  <- desugarMatch neg p+    -- if x0 < 0+    g2 <- desugarGuard $ AGBool (embed (atVar ty (coerce x0) <. ATNat ty 0)) -      return (g1 ++ g2 ++ g3)+    -- when -x0 is p+    neg <- desugarTerm $ mkUn ty Neg (atVar ty (coerce x0))+    g3 <- desugarMatch neg p -    mkMatch :: Member Fresh r => DTerm -> DPattern -> Sem r [DGuard]-    mkMatch dt dp = return [DGPat (embed dt) dp]+    return (g1 ++ g2 ++ g3) -    varMatch :: Member Fresh r => DTerm -> Name DTerm -> Sem r [DGuard]-    varMatch dt x = mkMatch dt (DPVar (getType dt) x)+  mkMatch :: Member Fresh r => DTerm -> DPattern -> Sem r [DGuard]+  mkMatch dt dp = return [DGPat (embed dt) dp] -    varFor :: Member Fresh r => DTerm -> Sem r (Name DTerm, [DGuard])-    varFor (DTVar _ (QName _ x)) = return (x, [])  -- XXX return a name + provenance??-    varFor dt          = do-      x <- fresh (string2Name "x")-      g <- varMatch dt x-      return (x, g)+  varMatch :: Member Fresh r => DTerm -> Name DTerm -> Sem r [DGuard]+  varMatch dt x = mkMatch dt (DPVar (getType dt) x) -    varForPat :: Member Fresh r => APattern -> Sem r (Name DTerm, [DGuard])-    varForPat (APVar _ x) = return (coerce x, [])-    varForPat p           = do-      x <- fresh (string2Name "px")     -- changing this from x fixed a bug and I don't know why =(-      (x,) <$> desugarMatch (dtVar (getType p) x) p+  varFor :: Member Fresh r => DTerm -> Sem r (Name DTerm, [DGuard])+  varFor (DTVar _ (QName _ x)) = return (x, []) -- XXX return a name + provenance??+  varFor dt = do+    x <- fresh (string2Name "x")+    g <- varMatch dt x+    return (x, g) -    arithBinMatch-      :: Member Fresh r-      => (Type -> Maybe (ATerm -> ATerm -> ATerm))-      -> (ATerm -> ATerm -> ATerm)-      -> DTerm -> Type -> APattern -> ATerm -> Sem r [DGuard]-    arithBinMatch restrict inverse dt ty p t = do-      (x0, g1) <- varFor dt+  varForPat :: Member Fresh r => APattern -> Sem r (Name DTerm, [DGuard])+  varForPat (APVar _ x) = return (coerce x, [])+  varForPat p = do+    x <- fresh (string2Name "px") -- changing this from x fixed a bug and I don't know why =(+    (x,) <$> desugarMatch (dtVar (getType p) x) p -      -- let v = t-      t' <- desugarTerm t-      (v, g2) <- varFor t'+  arithBinMatch ::+    Member Fresh r =>+    (Type -> Maybe (ATerm -> ATerm -> ATerm)) ->+    (ATerm -> ATerm -> ATerm) ->+    DTerm ->+    Type ->+    APattern ->+    ATerm ->+    Sem r [DGuard]+  arithBinMatch restrict inverse dt ty p t = do+    (x0, g1) <- varFor dt -      g3 <- case restrict ty of-        Nothing -> return []+    -- let v = t+    t' <- desugarTerm t+    (v, g2) <- varFor t' -        -- if x0 `cmp` v-        Just cmp ->-          desugarGuard $-            AGBool (embed (atVar ty (coerce x0) `cmp` atVar (getType t) (coerce v)))+    g3 <- case restrict ty of+      Nothing -> return []+      -- if x0 `cmp` v+      Just cmp ->+        desugarGuard $+          AGBool (embed (atVar ty (coerce x0) `cmp` atVar (getType t) (coerce v))) -      -- when x0 `inverse` v is p-      inv <- desugarTerm (atVar ty (coerce x0) `inverse` atVar (getType t) (coerce v))-      g4  <- desugarMatch inv p+    -- when x0 `inverse` v is p+    inv <- desugarTerm (atVar ty (coerce x0) `inverse` atVar (getType t) (coerce v))+    g4 <- desugarMatch inv p -      return (g1 ++ g2 ++ g3 ++ g4)+    return (g1 ++ g2 ++ g3 ++ g4)  -- | Desugar a container literal such as @[1,2,3]@ or @{1,2,3}@. desugarContainer :: Member Fresh r => Type -> Container -> [(ATerm, Maybe ATerm)] -> Maybe (Ellipsis ATerm) -> Sem r DTerm- -- Literal list containers desugar to nested applications of cons. desugarContainer ty ListContainer es Nothing =   foldr (dtbin ty (PrimBOp Cons)) (DTNil ty) <$> mapM (desugarTerm . fst) es- -- A list container with an ellipsis @[x, y, z .. e]@ desugars to an -- application of the primitive 'until' function. desugarContainer ty@(TyList _) ListContainer es (Just (Until t)) =   dtbin ty PrimUntil     <$> desugarTerm t     <*> desugarContainer ty ListContainer es Nothing- -- If desugaring a bag and there are any counts specified, desugar to -- an application of bagFromCounts to a bag of pairs (with a literal -- value of 1 filled in for missing counts as needed). desugarContainer (TyBag eltTy) BagContainer es mell   | any (isJust . snd) es =-    dtapp (DTPrim (TySet (eltTy :*: TyN) :->: TyBag eltTy) PrimC2B)-      <$> desugarContainer (TyBag (eltTy :*: TyN)) BagContainer counts mell--    where-      -- turn e.g.  x # 3, y   into   (x, 3), (y, 1)-      counts = [ (ATTup (eltTy :*: TyN) [t, fromMaybe (ATNat TyN 1) n], Nothing)-               | (t, n) <- es-               ]+      dtapp (DTPrim (TySet (eltTy :*: TyN) :->: TyBag eltTy) PrimC2B)+        <$> desugarContainer (TyBag (eltTy :*: TyN)) BagContainer counts mell+ where+  -- turn e.g.  x # 3, y   into   (x, 3), (y, 1)+  counts =+    [ (ATTup (eltTy :*: TyN) [t, fromMaybe (ATNat TyN 1) n], Nothing)+    | (t, n) <- es+    ]  -- Other containers desugar to an application of the appropriate -- container conversion function to the corresponding desugared list. desugarContainer ty _ es mell =   dtapp (DTPrim (TyList eltTy :->: ty) conv)     <$> desugarContainer (TyList eltTy) ListContainer es mell-  where-    (conv, eltTy) = case ty of-      TyBag e -> (PrimBag, e)-      TySet e -> (PrimSet, e)-      _       -> error $ "Impossible! Non-container type " ++ show ty ++ " in desugarContainer"+ where+  (conv, eltTy) = case ty of+    TyBag e -> (PrimBag, e)+    TySet e -> (PrimSet, e)+    _ -> error $ "Impossible! Non-container type " ++ show ty ++ " in desugarContainer"

@@ -1,141 +1,157 @@ -----------------------------------------------------------------------------++-----------------------------------------------------------------------------++-- SPDX-License-Identifier: BSD-3-Clause+ -- | -- Module      :  Disco.Doc -- Copyright   :  disco team and contributors -- Maintainer  :  byorgey@gmail.com -- -- Built-in documentation.------------------------------------------------------------------------------------- SPDX-License-Identifier: BSD-3-Clause--module Disco.Doc-       ( primDoc, primReference, otherDoc, otherReference-       ) where+module Disco.Doc (+  primDoc,+  primReference,+  otherDoc,+  otherReference,+) where -import           Data.Map               (Map)-import qualified Data.Map               as M+import Data.Map (Map)+import qualified Data.Map as M -import           Disco.Syntax.Operators-import           Disco.Syntax.Prims-import           Disco.Util             ((==>))+import Disco.Syntax.Operators+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)."-  ]+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)."+    ]  -- | 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"-  ]+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"+    ]  otherDoc :: Map String String-otherDoc = 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-  , "Prop"       ==> "The type of propositions."-  , "Set"        ==> "The type of finite sets."-  , "|~|"        ==> "Absolute value, or the size of a collection."-  ]-  where-    docN = "The type of natural numbers: 0, 1, 2, ..."-    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)."+otherDoc =+  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."+    ]+ 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)."  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"-  , "Prop"       ==> "prop"-  , "Set"        ==> "set"-  , "|~|"        ==> "size"-  ]+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"+    ]

@@ -1,7 +1,10 @@-{-# LANGUAGE BlockArguments  #-}+{-# LANGUAGE BlockArguments #-} {-# LANGUAGE TemplateHaskell #-}  -----------------------------------------------------------------------------++-----------------------------------------------------------------------------+ -- | -- Module      :  Disco.Effects.Counter -- Copyright   :  disco team and contributors@@ -10,30 +13,26 @@ -- SPDX-License-Identifier: BSD-3-Clause -- -- Polysemy effect for integer counter.---------------------------------------------------------------------------------- module Disco.Effects.Counter where -import           Polysemy-import           Polysemy.State+import Polysemy+import Polysemy.State  data Counter m a where-   -- | Return the next integer in sequence.-  Next  :: Counter m Integer+  Next :: Counter m Integer  makeSem ''Counter  -- | Dispatch a counter effect, starting the counter from the given --   Integer. runCounter' :: Integer -> Sem (Counter ': r) a -> Sem r a-runCounter' i-  = evalState i-  . reinterpret \case+runCounter' i =+  evalState i+    . reinterpret \case       Next -> do         n <- get-        put (n+1)+        put (n + 1)         return n  -- | Dispatch a counter effect, starting the counter from zero.

@@ -1,8 +1,11 @@-{-# LANGUAGE BlockArguments             #-}+{-# LANGUAGE BlockArguments #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE TemplateHaskell            #-}+{-# LANGUAGE TemplateHaskell #-}  -----------------------------------------------------------------------------++-----------------------------------------------------------------------------+ -- | -- Module      :  Disco.Effects.Fresh -- Copyright   :  disco team and contributors@@ -12,50 +15,47 @@ -- -- Polysemy effect for fresh name generation, compatible with the -- unbound-generics library.---------------------------------------------------------------------------------- module Disco.Effects.Fresh where -import           Disco.Effects.Counter-import           Disco.Names                           (QName, localName)-import           Polysemy-import           Polysemy.ConstraintAbsorber-import qualified Unbound.Generics.LocallyNameless      as U-import           Unbound.Generics.LocallyNameless.Name+import Disco.Effects.Counter+import Disco.Names (QName, localName)+import Polysemy+import Polysemy.ConstraintAbsorber+import qualified Unbound.Generics.LocallyNameless as U+import Unbound.Generics.LocallyNameless.Name  -- | Fresh name generation effect, supporting raw generation of fresh --   names, and opening binders with automatic freshening.  Simply --   increments a global counter every time 'fresh' is called and --   makes a variable with that numeric suffix. data Fresh m a where-  Fresh  :: Name x -> Fresh m (Name x)+  Fresh :: Name x -> Fresh m (Name x)  makeSem ''Fresh  -- | Dispatch the fresh name generation effect, starting at a given --   integer. runFresh' :: Integer -> Sem (Fresh ': r) a -> Sem r a-runFresh' i-  = runCounter' i-  . reinterpret \case+runFresh' i =+  runCounter' i+    . reinterpret \case       Fresh x -> case x of-        Fn s _  -> Fn s <$> next-        nm@Bn{} -> return nm+        Fn s _ -> Fn s <$> next+        nm@Bn {} -> return nm -    -- Above code copied from-    -- https://hackage.haskell.org/package/unbound-generics-0.4.1/docs/src/Unbound.Generics.LocallyNameless.Fresh.html ;-    -- see instance Monad m => Fresh (FreshMT m) .+-- Above code copied from+-- https://hackage.haskell.org/package/unbound-generics-0.4.1/docs/src/Unbound.Generics.LocallyNameless.Fresh.html ;+-- see instance Monad m => Fresh (FreshMT m) . -    -- It turns out to make things much simpler to reimplement the-    -- Fresh effect ourselves in terms of a state effect, since then-    -- we can immediately dispatch it.  The alternative would be to-    -- implement it in terms of (Embed U.FreshM), but then we are-    -- stuck with that constraint.  Given the constraint-absorbing-    -- machinery below, just impementing the 'fresh' effect itself-    -- means we can then reuse other things from unbound-generics that-    -- depend on a Fresh constraint, such as the 'unbind' function-    -- below.+-- It turns out to make things much simpler to reimplement the+-- Fresh effect ourselves in terms of a state effect, since then+-- we can immediately dispatch it.  The alternative would be to+-- implement it in terms of (Embed U.FreshM), but then we are+-- stuck with that constraint.  Given the constraint-absorbing+-- machinery below, just impementing the 'fresh' effect itself+-- means we can then reuse other things from unbound-generics that+-- depend on a Fresh constraint, such as the 'unbind' function+-- below.  -- | Run a computation requiring fresh name generation, beginning with --   0 for the initial freshly generated name.@@ -92,7 +92,7 @@ absorbFresh = absorbWithSem @U.Fresh @Action (FreshDict fresh) (Sub Dict) {-# INLINEABLE absorbFresh #-} -newtype FreshDict m = FreshDict { fresh_ :: forall x. Name x -> m (Name x) }+newtype FreshDict m = FreshDict {fresh_ :: forall x. Name x -> m (Name x)}  -- | Wrapper for a monadic action with phantom type parameter for reflection. --   Locally defined so that the instance we are going to build with reflection@@ -100,8 +100,11 @@ newtype Action m s' a = Action (m a)   deriving (Functor, Applicative, Monad) -instance ( Monad m-         , Reifies s' (FreshDict m)-         ) => U.Fresh (Action m s') where+instance+  ( Monad m+  , Reifies s' (FreshDict m)+  ) =>+  U.Fresh (Action m s')+  where   fresh x = Action $ fresh_ (reflect $ Proxy @s') x   {-# INLINEABLE fresh #-}

@@ -1,4 +1,7 @@ -----------------------------------------------------------------------------++-----------------------------------------------------------------------------+ -- | -- Module      :  Disco.Effects.Input -- Copyright   :  disco team and contributors@@ -7,20 +10,16 @@ -- SPDX-License-Identifier: BSD-3-Clause -- -- Utility functions for input effect.-----------------------------------------------------------------------------------module Disco.Effects.Input-  ( module Polysemy.Input-  , inputToState-  )-  where+module Disco.Effects.Input (+  module Polysemy.Input,+  inputToState,+)+where -import           Polysemy-import           Polysemy.Input-import           Polysemy.State+import Polysemy+import Polysemy.Input+import Polysemy.State  -- | 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 })-+inputToState = interpret (\case Input -> get @s)

@@ -1,8 +1,11 @@-{-# LANGUAGE BlockArguments             #-}+{-# LANGUAGE BlockArguments #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE TemplateHaskell            #-}+{-# LANGUAGE TemplateHaskell #-}  -----------------------------------------------------------------------------++-----------------------------------------------------------------------------+ -- | -- Module      :  Disco.Effects.LFresh -- Copyright   :  disco team and contributors@@ -12,24 +15,21 @@ -- -- Polysemy effect for local fresh name generation, compatible with -- the unbound-generics library.---------------------------------------------------------------------------------- module Disco.Effects.LFresh where -import           Data.Set                              (Set)-import qualified Data.Set                              as S-import           Data.Typeable                         (Typeable)-import           Polysemy-import           Polysemy.ConstraintAbsorber-import           Polysemy.Reader-import qualified Unbound.Generics.LocallyNameless      as U-import           Unbound.Generics.LocallyNameless.Name+import Data.Set (Set)+import qualified Data.Set as S+import Data.Typeable (Typeable)+import Polysemy+import Polysemy.ConstraintAbsorber+import Polysemy.Reader+import qualified Unbound.Generics.LocallyNameless as U+import Unbound.Generics.LocallyNameless.Name  -- | Local fresh name generation effect. data LFresh m a where-  Lfresh    :: Typeable a => Name a -> LFresh m (Name a)-  Avoid     :: [AnyName] -> m a -> LFresh m a+  Lfresh :: Typeable a => Name a -> LFresh m (Name a)+  Avoid :: [AnyName] -> m a -> LFresh m a   GetAvoids :: LFresh m (Set AnyName)  makeSem ''LFresh@@ -40,44 +40,48 @@ runLFresh = runReader S.empty . runLFresh'  runLFresh' :: Sem (LFresh ': r) a -> Sem (Reader (Set AnyName) ': r) a-runLFresh'-  = reinterpretH @_ @(Reader (Set AnyName)) \case-      Lfresh nm -> do-        let s = name2String nm-        used <- ask-        pureT $ head (filter (\x -> not (S.member (AnyName x) used))-                       (map (makeName s) [0..]))-      Avoid names m -> do-        m' <- runT m-        raise (subsume (runLFresh' (local (S.union (S.fromList names)) m')))-      GetAvoids  -> ask >>= pureT+runLFresh' =+  reinterpretH @_ @(Reader (Set AnyName)) \case+    Lfresh nm -> do+      let s = name2String nm+      used <- ask+      pureT $+        head+          ( filter+              (\x -> not (S.member (AnyName x) used))+              (map (makeName s) [0 ..])+          )+    Avoid names m -> do+      m' <- runT m+      raise (subsume (runLFresh' (local (S.union (S.fromList names)) m')))+    GetAvoids -> ask >>= pureT -  -- Much of the above code copied from-  -- https://hackage.haskell.org/package/unbound-generics-0.4.1/docs/src/Unbound.Generics.LocallyNameless.LFresh.html-  -- (see instance Monad m => LFresh (LFreshMT m))+-- Much of the above code copied from+-- https://hackage.haskell.org/package/unbound-generics-0.4.1/docs/src/Unbound.Generics.LocallyNameless.LFresh.html+-- (see instance Monad m => LFresh (LFreshMT m)) -  -- It turns out to make things much simpler to reimplement the-  -- LFresh effect ourselves in terms of a reader effect, since then-  -- we can immediately dispatch it as above.  The alternative would-  -- be to implement it in terms of (Final U.LFreshM) (see the-  -- commented code at the bottom of this file), but then we are stuck-  -- with that constraint.  Given the constraint-absorbing machinery-  -- below, just impementing the 'LFresh' effect itself means we can-  -- then reuse other things from unbound-generics that depend on a-  -- Fresh constraint, such as the 'lunbind' function below.+-- It turns out to make things much simpler to reimplement the+-- LFresh effect ourselves in terms of a reader effect, since then+-- we can immediately dispatch it as above.  The alternative would+-- be to implement it in terms of (Final U.LFreshM) (see the+-- commented code at the bottom of this file), but then we are stuck+-- with that constraint.  Given the constraint-absorbing machinery+-- below, just impementing the 'LFresh' effect itself means we can+-- then reuse other things from unbound-generics that depend on a+-- Fresh constraint, such as the 'lunbind' function below. -  -- NOTE: originally, there was a single function runLFresh which-  -- called reinterpretH and then immediately dispatched the Reader-  -- (Set AnyName) effect.  However, since runLFresh is recursive,-  -- this means that the recursive calls were running with a-  -- completely *separate* Reader effect that started over from the-  -- empty set! This meant that LFresh basically never changed any-  -- names, leading to all sorts of name clashes and crashes.-  ---  -- Instead, we need to organize things as above: runLFresh' is-  -- recursive, and keeps the Reader effect (using 'subsume' to squash-  -- the duplicated Reader effects together).  Then a top-level-  -- runLFresh function finally runs the Reader effect.+-- NOTE: originally, there was a single function runLFresh which+-- called reinterpretH and then immediately dispatched the Reader+-- (Set AnyName) effect.  However, since runLFresh is recursive,+-- this means that the recursive calls were running with a+-- completely *separate* Reader effect that started over from the+-- empty set! This meant that LFresh basically never changed any+-- names, leading to all sorts of name clashes and crashes.+--+-- Instead, we need to organize things as above: runLFresh' is+-- recursive, and keeps the Reader effect (using 'subsume' to squash+-- the duplicated Reader effects together).  Then a top-level+-- runLFresh function finally runs the Reader effect.  -------------------------------------------------- -- Other functions@@ -86,9 +90,11 @@ --   variables, and providing the opened pattern and term to the --   provided continuation.  The bound variables are also added to the --   set of in-scope variables within in the continuation.-lunbind-  :: (Member LFresh r, U.Alpha p, U.Alpha t)-  => U.Bind p t -> ((p,t) -> Sem r c) -> Sem r c+lunbind ::+  (Member LFresh r, U.Alpha p, U.Alpha t) =>+  U.Bind p t ->+  ((p, t) -> Sem r c) ->+  Sem r c lunbind b k = absorbLFresh (U.lunbind b k)  ------------------------------------------------------------@@ -101,8 +107,8 @@ {-# INLINEABLE absorbLFresh #-}  data LFreshDict m = LFreshDict-  { lfresh_    :: forall a. Typeable a => Name a -> m (Name a)-  , avoid_     :: forall a. [AnyName] -> m a -> m a+  { lfresh_ :: forall a. Typeable a => Name a -> m (Name a)+  , avoid_ :: forall a. [AnyName] -> m a -> m a   , getAvoids_ :: m (Set AnyName)   } @@ -112,9 +118,12 @@ newtype Action m s' a = Action (m a)   deriving (Functor, Applicative, Monad) -instance ( Monad m-         , Reifies s' (LFreshDict m)-         ) => U.LFresh (Action m s') where+instance+  ( Monad m+  , Reifies s' (LFreshDict m)+  ) =>+  U.LFresh (Action m s')+  where   lfresh x = Action $ lfresh_ (reflect $ Proxy @s') x   {-# INLINEABLE lfresh #-}   avoid xs (Action m) = Action $ avoid_ (reflect $ Proxy @s') xs m

@@ -1,4 +1,7 @@ -----------------------------------------------------------------------------++-----------------------------------------------------------------------------+ -- | -- Module      :  Disco.Effects.Random -- Copyright   :  disco team and contributors@@ -7,22 +10,19 @@ -- SPDX-License-Identifier: BSD-3-Clause -- -- Utility functions for random effect.-----------------------------------------------------------------------------------module Disco.Effects.Random-  ( module Polysemy.Random-  , runGen-  )-  where+module Disco.Effects.Random (+  module Polysemy.Random,+  runGen,+)+where -import           Polysemy-import           Polysemy.Random+import Polysemy+import Polysemy.Random import qualified System.Random.SplitMix as SM-import qualified Test.QuickCheck.Gen    as QC+import qualified Test.QuickCheck.Gen as QC import qualified Test.QuickCheck.Random as QCR -import           Data.Word              (Word64)+import Data.Word (Word64)  -- | Run a QuickCheck generator using a 'Random' effect. runGen :: Member Random r => QC.Gen a -> Sem r a

@@ -1,6 +1,9 @@ {-# LANGUAGE BlockArguments #-}  -----------------------------------------------------------------------------++-----------------------------------------------------------------------------+ -- | -- Module      :  Disco.Effects.State -- Copyright   :  disco team and contributors@@ -9,25 +12,24 @@ -- SPDX-License-Identifier: BSD-3-Clause -- -- Utility functions for state effect.-----------------------------------------------------------------------------------module Disco.Effects.State-  ( module Polysemy.State-  , zoom-  , use-  ,(%=),(.=))-  where+module Disco.Effects.State (+  module Polysemy.State,+  zoom,+  use,+  (%=),+  (.=),+)+where -import           Control.Lens   (Getter, Lens', view, (%~), (.~))+import Control.Lens (Getter, Lens', view, (%~), (.~)) -import           Polysemy-import           Polysemy.State+import Polysemy+import Polysemy.State  -- | Use a lens to zoom into a component of a state. zoom :: forall s a r c. Member (State s) r => Lens' s a -> Sem (State a ': r) c -> Sem r c zoom l = interpret \case-  Get   -> view l <$> get+  Get -> view l <$> get   Put a -> modify (l .~ a)  use :: Member (State s) r => Getter s a -> Sem r a

@@ -1,7 +1,10 @@-{-# LANGUAGE BlockArguments  #-}+{-# LANGUAGE BlockArguments #-} {-# LANGUAGE TemplateHaskell #-}  -----------------------------------------------------------------------------++-----------------------------------------------------------------------------+ -- | -- Module      :  Disco.Effects.Store -- Copyright   :  disco team and contributors@@ -10,44 +13,40 @@ -- SPDX-License-Identifier: BSD-3-Clause -- -- Polysemy effect for a memory store with integer keys.---------------------------------------------------------------------------------- module Disco.Effects.Store where -import qualified Data.IntMap.Lazy      as IntMap-import           Data.IntSet           (IntSet)-import qualified Data.IntSet           as IntSet+import qualified Data.IntMap.Lazy as IntMap+import Data.IntSet (IntSet)+import qualified Data.IntSet as IntSet -import           Disco.Effects.Counter-import           Polysemy-import           Polysemy.State+import Disco.Effects.Counter+import Polysemy+import Polysemy.State  data Store v m a where--  ClearStore  :: Store v m ()-  New         :: v -> Store v m Int+  ClearStore :: Store v m ()+  New :: v -> Store v m Int   LookupStore :: Int -> Store v m (Maybe v)   InsertStore :: Int -> v -> Store v m ()-  MapStore    :: (v -> v) -> Store v m ()+  MapStore :: (v -> v) -> Store v m ()   AssocsStore :: Store v m [(Int, v)]-  KeepKeys    :: IntSet -> Store v m ()+  KeepKeys :: IntSet -> Store v m ()  makeSem ''Store  -- | Dispatch a store effect. runStore :: forall v r a. Sem (Store v ': r) a -> Sem r a-runStore-  = runCounter-  . evalState @(IntMap.IntMap v) IntMap.empty-  . reinterpret2 \case-      ClearStore      -> put IntMap.empty-      New v           -> do+runStore =+  runCounter+    . evalState @(IntMap.IntMap v) IntMap.empty+    . reinterpret2 \case+      ClearStore -> put IntMap.empty+      New v -> do         loc <- fromIntegral <$> next         modify $ IntMap.insert loc v         return loc-      LookupStore k   -> gets (IntMap.lookup k)+      LookupStore k -> gets (IntMap.lookup k)       InsertStore k v -> modify (IntMap.insert k v)-      MapStore f      -> modify (IntMap.map f)-      AssocsStore     -> gets IntMap.assocs-      KeepKeys ks     -> modify (\m -> IntMap.withoutKeys m (IntMap.keysSet m `IntSet.difference` ks))+      MapStore f -> modify (IntMap.map f)+      AssocsStore -> gets IntMap.assocs+      KeepKeys ks -> modify (\m -> IntMap.withoutKeys m (IntMap.keysSet m `IntSet.difference` ks))

@@ -1,6 +1,9 @@ {-# LANGUAGE NondecreasingIndentation #-}  -----------------------------------------------------------------------------++-----------------------------------------------------------------------------+ -- | -- Module      :  Disco.Enumerate -- Copyright   :  disco team and contributors@@ -9,41 +12,38 @@ -- SPDX-License-Identifier: BSD-3-Clause -- -- Enumerate values inhabiting Disco types.---------------------------------------------------------------------------------+module Disco.Enumerate (+  ValueEnumeration, -module Disco.Enumerate-       (-         ValueEnumeration-         -- * Base types-         , enumVoid-         , enumUnit-         , enumBool-         , enumN-         , enumZ-         , enumF-         , enumQ-         , enumC+  -- * Base types+  enumVoid,+  enumUnit,+  enumBool,+  enumN,+  enumZ,+  enumF,+  enumQ,+  enumC, -         -- * Containers-         , enumSet-        --  , enumBag-         , enumList+  -- * Containers+  enumSet,+  --  , enumBag+  enumList, -         -- * Any type-         , enumType-         , enumTypes+  -- * Any type+  enumType,+  enumTypes, -         -- * Lifted functions that return lists-         , enumerateType-         , enumerateTypes-       )-       where+  -- * Lifted functions that return lists+  enumerateType,+  enumerateTypes,+)+where  import qualified Data.Enumeration.Invertible as E-import           Disco.AST.Generic           (Side (..))-import           Disco.Types-import           Disco.Value+import Disco.AST.Generic (Side (..))+import Disco.Types+import Disco.Value  type ValueEnumeration = E.IEnumeration Value @@ -58,16 +58,16 @@ -- | Enumerate the values of type @Bool@ as @[false, true]@. enumBool :: ValueEnumeration enumBool = E.mapE toV fromV $ E.finiteList [L, R]-  where-    toV i = VInj i VUnit-    fromV (VInj i VUnit) = i-    fromV _              = error "enumBool.fromV: value isn't a bool"+ where+  toV i = VInj i VUnit+  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"+valToRat _ = error "valToRat: value isn't a number"  ratToVal :: Rational -> Value ratToVal = VNum mempty@@ -93,9 +93,9 @@ -- | Enumerate all Unicode characters. enumC :: ValueEnumeration enumC = E.mapE toV fromV (E.boundedEnum @Char)-  where-    toV   = ratToVal . fromIntegral . fromEnum-    fromV = toEnum . floor . valToRat+ where+  toV = ratToVal . fromIntegral . fromEnum+  fromV = toEnum . floor . valToRat  -- | Enumerate all *finite* sets over a certain element type, given an --   enumeration of the elements.  If we think of each finite set as a@@ -103,21 +103,21 @@ --   members, the sets are enumerated in order of the binary strings. enumSet :: ValueEnumeration -> ValueEnumeration enumSet e = E.mapE toV fromV (E.finiteSubsetOf e)-  where-    toV = VBag . map (,1)-    fromV (VBag vs) = map fst vs-    fromV _         = error "enumSet.fromV: value isn't a set"+ where+  toV = VBag . map (,1)+  fromV (VBag vs) = map fst vs+  fromV _ = error "enumSet.fromV: value isn't a set"  -- | Enumerate all *finite* lists over a certain element type, given --   an enumeration of the elements.  It is very difficult to describe --   the order in which the lists are generated. enumList :: ValueEnumeration -> ValueEnumeration enumList e = E.mapE toV fromV (E.listOf e)-  where-    toV = foldr VCons VNil-    fromV (VCons h t) = h : fromV t-    fromV VNil        = []-    fromV _           = error "enumList.fromV: value isn't a list"+ where+  toV = foldr VCons VNil+  fromV (VCons h t) = h : fromV t+  fromV VNil = []+  fromV _ = error "enumList.fromV: value isn't a list"  -- | Enumerate all functions from a finite domain, given enumerations --   for the domain and codomain.@@ -127,60 +127,60 @@     (E.Finite 0, _) -> E.singleton (VFun $ \_ -> error "enumFunction: void function called")     (_, E.Finite 0) -> E.void     (_, E.Finite 1) -> E.singleton (VFun $ \_ -> E.select ys 0)-    _               -> E.mapE toV fromV (E.functionOf xs ys)+    _ -> E.mapE toV fromV (E.functionOf xs ys)+ where+  -- XXX TODO: better error message on functions with an infinite domain -    -- XXX TODO: better error message on functions with an infinite domain-  where-    toV = VFun-    fromV (VFun f) = f-    fromV _        = error "enumFunction.fromV: value isn't a VFun"+  toV = VFun+  fromV (VFun f) = f+  fromV _ = error "enumFunction.fromV: value isn't a VFun"  -- | Enumerate all values of a product type, given enumerations of the --   two component types.  Uses a fair interleaving for infinite --   component types. enumProd :: ValueEnumeration -> ValueEnumeration -> ValueEnumeration enumProd xs ys = E.mapE toV fromV $ (E.><) xs ys-  where-    toV (x, y)        = VPair x y-    fromV (VPair x y) = (x, y)-    fromV _           = error "enumProd.fromV: value isn't a pair"+ where+  toV (x, y) = VPair x y+  fromV (VPair x y) = (x, y)+  fromV _ = error "enumProd.fromV: value isn't a pair"  -- | Enumerate all values of a sum type, given enumerations of the two --   component types. enumSum :: ValueEnumeration -> ValueEnumeration -> ValueEnumeration enumSum xs ys = E.mapE toV fromV $ (E.<+>) xs ys-  where-    toV (Left x)  = VInj L x-    toV (Right y) = VInj R y-    fromV (VInj L x) = Left x-    fromV (VInj R y) = Right y-    fromV _          = error "enumSum.fromV: value isn't a sum"+ where+  toV (Left x) = VInj L x+  toV (Right y) = VInj R y+  fromV (VInj L x) = Left x+  fromV (VInj R y) = Right y+  fromV _ = error "enumSum.fromV: value isn't a sum"  -- | Enumerate the values of a given type. enumType :: Type -> ValueEnumeration-enumType TyVoid     = enumVoid-enumType TyUnit     = enumUnit-enumType TyBool     = enumBool-enumType TyN        = enumN-enumType TyZ        = enumZ-enumType TyF        = enumF-enumType TyQ        = enumQ-enumType TyC        = enumC-enumType (TySet  t) = enumSet (enumType t)+enumType TyVoid = enumVoid+enumType TyUnit = enumUnit+enumType TyBool = enumBool+enumType TyN = enumN+enumType TyZ = enumZ+enumType TyF = enumF+enumType TyQ = enumQ+enumType TyC = enumC+enumType (TySet t) = enumSet (enumType t) enumType (TyList t) = enumList (enumType t)-enumType (a :*: b)  = enumProd (enumType a) (enumType b)-enumType (a :+: b)  = enumSum (enumType a) (enumType b)+enumType (a :*: b) = enumProd (enumType a) (enumType b)+enumType (a :+: b) = enumSum (enumType a) (enumType b) enumType (a :->: b) = enumFunction (enumType a) (enumType b)-enumType ty         = error $ "enumType: can't enumerate " ++ show ty+enumType ty = error $ "enumType: can't enumerate " ++ show ty  -- | Enumerate a finite product of types. enumTypes :: [Type] -> E.IEnumeration [Value]-enumTypes []     = E.singleton []-enumTypes (t:ts) = E.mapE toL fromL $ (E.><) (enumType t) (enumTypes ts)-  where-    toL (x, xs)  = x:xs-    fromL (x:xs) = (x, xs)-    fromL []     = error "enumTypes.fromL: empty list not in enumeration range"+enumTypes [] = E.singleton []+enumTypes (t : ts) = E.mapE toL fromL $ (E.><) (enumType t) (enumTypes ts)+ where+  toL (x, xs) = x : xs+  fromL (x : xs) = (x, xs)+  fromL [] = error "enumTypes.fromL: empty list not in enumeration range"  -- | Produce an actual list of the values of a type. enumerateType :: Type -> [Value]

@@ -1,7 +1,10 @@-{-# LANGUAGE OverloadedStrings  #-}+{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE StandaloneDeriving #-}  -----------------------------------------------------------------------------++-----------------------------------------------------------------------------+ -- | -- Module      :  Disco.Error -- Copyright   :  disco team and contributors@@ -11,323 +14,315 @@ -- -- Type for collecting all potential Disco errors at the top level, -- and a type for runtime errors.-----------------------------------------------------------------------------------module Disco.Error (DiscoError(..), EvalError(..), panic, outputDiscoErrors) where+module Disco.Error (DiscoError (..), EvalError (..), panic, outputDiscoErrors) where -import           Prelude                          hiding ((<>))+import Prelude hiding ((<>)) -import           Text.Megaparsec                  (ParseErrorBundle,-                                                   errorBundlePretty)-import           Unbound.Generics.LocallyNameless (Name)+import Text.Megaparsec (+  ParseErrorBundle,+  errorBundlePretty,+ )+import Unbound.Generics.LocallyNameless (Name) -import           Disco.Effects.LFresh-import           Polysemy-import           Polysemy.Error-import           Polysemy.Output-import           Polysemy.Reader+import Disco.Effects.LFresh+import Polysemy+import Polysemy.Error+import Polysemy.Output+import Polysemy.Reader -import           Disco.Messages-import           Disco.Names                      (ModuleName, QName)-import           Disco.Parser                     (DiscoParseError)-import           Disco.Pretty-import           Disco.Typecheck.Solve-import           Disco.Typecheck.Util             (LocTCError (..),-                                                   TCError (..))-import           Disco.Types-import           Disco.Types.Qualifiers+import Disco.Messages+import Disco.Names (ModuleName, QName)+import Disco.Parser (DiscoParseError)+import Disco.Pretty+import Disco.Typecheck.Solve+import Disco.Typecheck.Util (+  LocTCError (..),+  TCError (..),+ )+import Disco.Types+import Disco.Types.Qualifiers  -- | Top-level error type for Disco. data DiscoError where-   -- | Module not found.   ModuleNotFound :: String -> DiscoError-   -- | Cyclic import encountered.   CyclicImport :: [ModuleName] -> DiscoError-   -- | Error encountered during typechecking.   TypeCheckErr :: LocTCError -> DiscoError-   -- | Error encountered during parsing.   ParseErr :: ParseErrorBundle String DiscoParseError -> DiscoError-   -- | Error encountered at runtime.   EvalErr :: EvalError -> DiscoError-   -- | Something that shouldn't happen; indicates the presence of a   --   bug.-  Panic         :: String    -> DiscoError--  deriving Show+  Panic :: String -> DiscoError+  deriving (Show)  -- | Errors that can be generated at runtime. data EvalError where-   -- | An unbound name was encountered.-  UnboundError  :: QName core  -> EvalError-+  UnboundError :: QName core -> EvalError   -- | An unbound name that really shouldn't happen, coming from some   --   kind of internal name generation scheme.-  UnboundPanic  :: Name core   -> EvalError-+  UnboundPanic :: Name core -> EvalError   -- | Division by zero.-  DivByZero     ::              EvalError-+  DivByZero :: EvalError   -- | Overflow, e.g. (2^66)!-  Overflow      ::              EvalError-+  Overflow :: EvalError   -- | Non-exhaustive case analysis.-  NonExhaustive ::              EvalError-+  NonExhaustive :: EvalError   -- | Infinite loop detected via black hole.-  InfiniteLoop  ::              EvalError-+  InfiniteLoop :: EvalError   -- | User-generated crash.-  Crash         :: String    -> EvalError+  Crash :: String -> EvalError  deriving instance Show EvalError  panic :: Member (Error DiscoError) r => String -> Sem r a panic = throw . Panic -outputDiscoErrors :: Member (Output Message) r => Sem (Error DiscoError ': r) () -> Sem r ()+outputDiscoErrors :: Member (Output (Message ann)) r => Sem (Error DiscoError ': r) () -> Sem r () outputDiscoErrors m = do   e <- runError m   either (err . pretty') return e  instance Pretty DiscoError where   pretty = \case-    ModuleNotFound m  -> "Error: couldn't find a module named '" <> text m <> "'."-    CyclicImport ms   -> cyclicImportError ms+    ModuleNotFound m -> "Error: couldn't find a module named '" <> text m <> "'."+    CyclicImport ms -> cyclicImportError ms     TypeCheckErr (LocTCError Nothing te) -> prettyTCError te     TypeCheckErr (LocTCError (Just n) te) ->-      vcat+      nest 2 $ vcat         [ "While checking " <> pretty' n <> ":"-        , nest 2 $ prettyTCError te+        , prettyTCError te         ]-    ParseErr pe       -> text (errorBundlePretty pe)-    EvalErr ee        -> prettyEvalError ee-    Panic s           ->+    ParseErr pe -> text (errorBundlePretty pe)+    EvalErr ee -> prettyEvalError ee+    Panic s ->       vcat         [ "Bug! " <> text s         , "Please report this as a bug at https://github.com/disco-lang/disco/issues/ ."         ] -rtd :: String -> Sem r Doc+rtd :: String -> Sem r (Doc ann) rtd page = "https://disco-lang.readthedocs.io/en/latest/reference/" <> text page <> ".html" -issue :: Int -> Sem r Doc+issue :: Int -> Sem r (Doc ann) issue n = "See https://github.com/disco-lang/disco/issues/" <> text (show n) -cyclicImportError-  :: Members '[Reader PA, LFresh] r-  => [ModuleName] -> Sem r Doc+cyclicImportError ::+  Members '[Reader PA, LFresh] r =>+  [ModuleName] ->+  Sem r (Doc ann) cyclicImportError ms =-  vcat+  nest 2 $ vcat     [ "Error: module imports form a cycle:"-    , nest 2 $ intercalate " ->" (map pretty ms)+    , intercalate " ->" (map pretty ms)     ] -prettyEvalError :: Members '[Reader PA, LFresh] r => EvalError -> Sem r Doc+prettyEvalError :: Members '[Reader PA, LFresh] r => EvalError -> Sem r (Doc ann) prettyEvalError = \case-   UnboundPanic x ->-     ("Bug! No variable found named" <+> pretty' x <> ".")-     $+$-     "Please report this as a bug at https://github.com/disco-lang/disco/issues/ ."-   UnboundError x -> "Error: encountered undefined name" <+> pretty' x <> ". Maybe you haven't defined it yet?"-   DivByZero      -> "Error: division by zero."-   Overflow       -> "Error: that number would not even fit in the universe!"-   NonExhaustive  -> "Error: value did not match any of the branches in a case expression."-   InfiniteLoop   -> "Error: infinite loop detected!"-   Crash s        -> "User crash:" <+> text s+  UnboundPanic x ->+    ("Bug! No variable found named" <+> pretty' x <> ".")+      $+$ "Please report this as a bug at https://github.com/disco-lang/disco/issues/ ."+  UnboundError x -> "Error: encountered undefined name" <+> pretty' x <> ". Maybe you haven't defined it yet?"+  DivByZero -> "Error: division by zero."+  Overflow -> "Error: that number would not even fit in the universe!"+  NonExhaustive -> "Error: value did not match any of the branches in a case expression."+  InfiniteLoop -> "Error: infinite loop detected!"+  Crash s -> "User crash:" <+> text s  -- [X] Step 1: nice error messages, make sure all are tested -- [ ] Step 2: link to wiki/website with more info on errors! -- [ ] Step 3: improve error messages according to notes below -- [ ] Step 4: get it to return multiple error messages -- [ ] Step 5: save parse locations, display with errors-prettyTCError :: Members '[Reader PA, LFresh] r => TCError -> Sem r Doc+prettyTCError :: Members '[Reader PA, LFresh] r => TCError -> Sem r (Doc ann) 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"-    ]--  Ambiguous x ms -> vcat-    [ "Error: the name" <+> pretty' x <+> "is ambiguous. It could refer to:"-    , nest 2 (vcat . map (\m -> pretty' m <> "." <> pretty' x) $ ms)-    , rtd "ambiguous"-    ]--  NoType x -> vcat-    [ "Error: the definition of" <+> pretty' x <+> "must have an accompanying type signature."-    , "Try writing something like '" <> pretty' x <+> ": Int' (or whatever the type of"-      <+> pretty' x <+> "should be) first."-    , rtd "missingtype"-    ]--  NotCon c t ty -> vcat-    [ "Error: the expression"-    , nest 2 $ pretty' t-    , "must have both a" <+> conWord c <+> "type and also the incompatible type"-    , nest 2 $ pretty' ty <> "."-    , rtd "notcon"-    ]--  EmptyCase -> vcat-    [ "Error: empty case expressions {? ?} are not allowed."-    , rtd "empty-case"-    ]--  PatternType c pat ty -> vcat-    [ "Error: the pattern"-    , nest 2 $ pretty' pat-    , "is supposed to have type"-    , nest 2 $ pretty' ty <> ","-    , "but instead it has a" <+> conWord c <+> "type."-    , rtd "pattern-type"-    ]--  DuplicateDecls x -> vcat-    [ "Error: duplicate type signature for" <+> pretty' x <> "."-    , rtd "dup-sig"-    ]--  DuplicateDefns x -> vcat-    [ "Error: duplicate definition for" <+> pretty' x <> "."-    , rtd "dup-def"-    ]--  DuplicateTyDefns s -> vcat-    [ "Error: duplicate definition for type" <+> text s <> "."-    , rtd "dup-tydef"-    ]-+  Unbound x ->+    vcat+      [ "Error: there is nothing named" <+> pretty' x <> "."+      , rtd "unbound"+      ]+  Ambiguous x ms ->+    vcat+      [ "Error: the name" <+> pretty' x <+> "is ambiguous. It could refer to:"+      , indent 2 . vcat . map (\m -> pretty' m <> "." <> pretty' x) $ ms+      , rtd "ambiguous"+      ]+  NoType x ->+    vcat+      [ "Error: the definition of" <+> pretty' x <+> "must have an accompanying type signature."+      , "Try writing something like '"+          <> pretty' x+          <+> ": Int' (or whatever the type of"+          <+> pretty' x+          <+> "should be) first."+      , rtd "missingtype"+      ]+  NotCon c t ty ->+    vcat+      [ "Error: the expression"+      , indent 2 $ pretty' t+      , "must have both a" <+> conWord c <+> "type and also the incompatible type"+      , indent 2 $ pretty' ty <> "."+      , rtd "notcon"+      ]+  EmptyCase ->+    vcat+      [ "Error: empty case expressions {? ?} are not allowed."+      , rtd "empty-case"+      ]+  PatternType c pat ty ->+    vcat+      [ "Error: the pattern"+      , indent 2 $ pretty' pat+      , "is supposed to have type"+      , indent 2 $ pretty' ty <> ","+      , "but instead it has a" <+> conWord c <+> "type."+      , rtd "pattern-type"+      ]+  DuplicateDecls x ->+    vcat+      [ "Error: duplicate type signature for" <+> pretty' x <> "."+      , rtd "dup-sig"+      ]+  DuplicateDefns x ->+    vcat+      [ "Error: duplicate definition for" <+> pretty' x <> "."+      , rtd "dup-def"+      ]+  DuplicateTyDefns s ->+    vcat+      [ "Error: duplicate definition for type" <+> text s <> "."+      , rtd "dup-tydef"+      ]   -- XXX include all types involved in the cycle.-  CyclicTyDef s -> vcat-    [ "Error: cyclic type definition for" <+> text s <> "."-    , rtd "cyc-ty"-    ]-+  CyclicTyDef s ->+    vcat+      [ "Error: cyclic type definition for" <+> text s <> "."+      , rtd "cyc-ty"+      ]   -- XXX lots more info!  & Split into several different errors.-  NumPatterns -> vcat-    [ "Error: number of arguments does not match."-    , rtd "num-args"-    ]-+  NumPatterns ->+    vcat+      [ "Error: number of arguments does not match."+      , rtd "num-args"+      ]+  NonlinearPattern p x ->+    vcat+      [ "Error: pattern" <+> pretty' p <+> "contains duplicate variable" <+> pretty' x <> "."+      , rtd "nonlinear"+      ]   NoSearch ty ->     vcat-    [ "Error: the type"-    , nest 2 $ pretty' ty-    , "is not searchable (i.e. it cannot be used in a forall)."-    , rtd "no-search"-    ]-+      [ "Error: the type"+      , indent 2 $ pretty' ty+      , "is not searchable (i.e. it cannot be used in a forall)."+      , rtd "no-search"+      ]   Unsolvable solveErr -> prettySolveError solveErr-   -- XXX maybe include close edit-distance alternatives?-  NotTyDef s -> vcat-    [ "Error: there is no built-in or user-defined type named '" <> text s <> "'."-    , rtd "no-tydef"-    ]--  NoTWild -> vcat-    [ "Error: wildcards (_) are not allowed in expressions."-    , rtd "wildcard-expr"-    ]-+  NotTyDef s ->+    vcat+      [ "Error: there is no built-in or user-defined type named '" <> text s <> "'."+      , rtd "no-tydef"+      ]+  NoTWild ->+    vcat+      [ "Error: wildcards (_) are not allowed in expressions."+      , rtd "wildcard-expr"+      ]   -- XXX say how many are expected, how many there were, what the actual arguments were?   -- XXX distinguish between built-in and user-supplied type constructors in the error   --     message?-  NotEnoughArgs con -> vcat-    [ "Error: not enough arguments for the type '" <> pretty' con <> "'."-    , rtd "num-args-type"-    ]--  TooManyArgs con -> vcat-    [ "Error: too many arguments for the type '" <> pretty' con <> "'."-    , rtd "num-args-type"-    ]-+  NotEnoughArgs con ->+    vcat+      [ "Error: not enough arguments for the type '" <> pretty' con <> "'."+      , rtd "num-args-type"+      ]+  TooManyArgs con ->+    vcat+      [ "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"-    ]--  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."-    , nest 2 (-        text s <> parens (intercalate "," (map pretty' tys)) <+> "does not follow this rule."-      )-    , rtd "no-poly-rec"-    ]-+  UnboundTyVar v ->+    vcat+      [ "Error: Unknown type variable '" <> pretty' v <> "'."+      , 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."+      , indent+          2+          ( text s <> parens (intercalate "," (map pretty' tys)) <+> "does not follow this rule."+          )+      , rtd "no-poly-rec"+      ]   NoError -> empty -conWord :: Con -> Sem r Doc+conWord :: Con -> Sem r (Doc ann) conWord = \case-  CArr         -> "function"-  CProd        -> "product"-  CSum         -> "sum"-  CSet         -> "set"-  CBag         -> "bag"-  CList        -> "list"+  CArr -> "function"+  CProd -> "pair"+  CSum -> "sum"+  CSet -> "set"+  CBag -> "bag"+  CList -> "list"   CContainer _ -> "container"-  CMap         -> "map"-  CGraph       -> "graph"-  CUser s      -> text s+  CMap -> "map"+  CGraph -> "graph"+  CUser s -> text s -prettySolveError :: Members '[Reader PA, LFresh] r => SolveError -> Sem r Doc+prettySolveError :: Members '[Reader PA, LFresh] r => SolveError -> Sem r (Doc ann) prettySolveError = \case-   -- XXX say which types!-  NoWeakUnifier -> vcat-    [ "Error: the shape of two types does not match."-    , rtd "shape-mismatch"-    ]-+  NoWeakUnifier ->+    vcat+      [ "Error: the shape of two types does not match."+      , rtd "shape-mismatch"+      ]   -- XXX say more!  XXX HIGHEST PRIORITY!-  NoUnify       -> vcat-    [ "Error: typechecking failed."-    , rtd "typecheck-fail"-    ]--  UnqualBase q b -> vcat-    [ "Error: values of type" <+> pretty' b <+> qualPhrase False q <> "."-    , rtd "not-qual"-    ]--  Unqual q ty -> vcat-    [ "Error: values of type" <+> pretty' ty <+> qualPhrase False q <> "."-    , rtd "not-qual"-    ]--  QualSkolem q a -> vcat-    [ "Error: type variable" <+> pretty' a <+> "represents any type, so we cannot assume values of that type"-    , nest 2 (qualPhrase True q) <> "."-    , rtd "qual-skolem"-    ]+  NoUnify ->+    vcat+      [ "Error: typechecking failed."+      , rtd "typecheck-fail"+      ]+  UnqualBase q b ->+    vcat+      [ "Error: values of type" <+> pretty' b <+> qualPhrase False q <> "."+      , rtd "not-qual"+      ]+  Unqual q ty ->+    vcat+      [ "Error: values of type" <+> pretty' ty <+> qualPhrase False q <> "."+      , rtd "not-qual"+      ]+  QualSkolem q a ->+    vcat+      [ "Error: type variable" <+> pretty' a <+> "represents any type, so we cannot assume values of that type"+      , indent 2 (qualPhrase True q) <> "."+      , rtd "qual-skolem"+      ] -qualPhrase :: Bool -> Qualifier -> Sem r Doc+qualPhrase :: Bool -> Qualifier -> Sem r (Doc ann) qualPhrase b q   | q `elem` [QBool, QBasic, QSimple] = "are" <+> (if b then empty else "not") <+> qualAction q   | otherwise = "can" <> (if b then empty else "not") <+> "be" <+> qualAction q -qualAction :: Qualifier -> Sem r Doc+qualAction :: Qualifier -> Sem r (Doc ann) qualAction = \case-  QNum    -> "added and multiplied"-  QSub    -> "subtracted"-  QDiv    -> "divided"-  QCmp    -> "compared"-  QEnum   -> "enumerated"-  QBool   -> "boolean"-  QBasic  -> "basic"+  QNum -> "added and multiplied"+  QSub -> "subtracted"+  QDiv -> "divided"+  QCmp -> "compared"+  QEnum -> "enumerated"+  QBool -> "boolean"+  QBasic -> "basic"   QSimple -> "simple"-

@@ -1,8 +1,7 @@-{-# LANGUAGE OverloadedStrings    #-}-{-# LANGUAGE TemplateHaskell      #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeSynonymInstances #-} ------------------------------------------------------------------------------ -- | -- Module      :  Disco.Eval -- Copyright   :  disco team and contributors@@ -11,86 +10,91 @@ -- SPDX-License-Identifier: BSD-3-Clause -- -- Top-level evaluation utilities.--------------------------------------------------------------------------------module Disco.Eval-       (-         -- * Effects--         EvalEffects-       , DiscoEffects--         -- * Top-level info record and associated lenses--       , DiscoConfig, initDiscoConfig, debugMode-       , TopInfo-       , replModInfo, topEnv, topModMap, lastFile, discoConfig--         -- * Running things--       , runDisco-       , runTCM-       , inputTopEnv-       , parseDiscoModule-       , typecheckTop+module Disco.Eval (+  -- * Effects+  EvalEffects,+  DiscoEffects, -         -- * Loading modules+  -- * Top-level info record and associated lenses+  DiscoConfig,+  initDiscoConfig,+  debugMode,+  TopInfo,+  replModInfo,+  topEnv,+  topModMap,+  lastFile,+  discoConfig, -       , loadDiscoModule-       , loadParsedDiscoModule-       , loadFile-       , addToREPLModule-       , setREPLModule-       , loadDefsFrom-       , loadDef+  -- * Running things+  runDisco,+  runTCM,+  inputTopEnv,+  parseDiscoModule,+  typecheckTop, -       )-       where+  -- * Loading modules+  loadDiscoModule,+  loadParsedDiscoModule,+  loadFile,+  addToREPLModule,+  setREPLModule,+  loadDefsFrom,+  loadDef,+)+where -import           Control.Arrow            ((&&&))-import           Control.Exception        (SomeException, handle)-import           Control.Lens             (makeLenses, toListOf, view, (%~),-                                           (.~), (<>~), (^.))-import           Control.Monad            (unless, void, when)-import           Control.Monad.IO.Class   (liftIO)-import           Data.Bifunctor-import           Data.Map                 (Map)-import qualified Data.Map                 as M-import qualified Data.Set                 as S-import           Prelude-import           System.FilePath          ((-<.>))+import Control.Arrow ((&&&))+import Control.Exception (SomeException, handle)+import Control.Lens (+  makeLenses,+  toListOf,+  view,+  (%~),+  (.~),+  (<>~),+  (^.),+ )+import Control.Monad (unless, void, when)+import Control.Monad.IO.Class (liftIO)+import Data.Bifunctor+import Data.Map (Map)+import qualified Data.Map as M+import qualified Data.Set as S+import System.FilePath ((-<.>))+import Prelude  import qualified System.Console.Haskeline as H -import           Disco.Effects.Fresh-import           Disco.Effects.Input-import           Disco.Effects.LFresh-import           Disco.Effects.State-import           Polysemy-import           Polysemy.Embed-import           Polysemy.Error-import           Polysemy.Fail-import           Polysemy.Output-import           Polysemy.Random-import           Polysemy.Reader+import Disco.Effects.Fresh+import Disco.Effects.Input+import Disco.Effects.LFresh+import Disco.Effects.State+import Polysemy+import Polysemy.Embed+import Polysemy.Error+import Polysemy.Fail+import Polysemy.Output+import Polysemy.Random+import Polysemy.Reader -import           Disco.AST.Core-import           Disco.AST.Surface-import           Disco.Compile            (compileDefns)-import           Disco.Context            as Ctx-import           Disco.Error-import           Disco.Extensions-import           Disco.Interpret.CESK-import           Disco.Messages-import           Disco.Module-import           Disco.Names-import           Disco.Parser-import           Disco.Pretty             hiding ((<>))-import qualified Disco.Pretty             as Pretty-import           Disco.Typecheck          (checkModule)-import           Disco.Typecheck.Util-import           Disco.Types-import           Disco.Value+import Disco.AST.Core+import Disco.AST.Surface+import Disco.Compile (compileDefns)+import Disco.Context as Ctx+import Disco.Error+import Disco.Extensions+import Disco.Interpret.CESK+import Disco.Messages+import Disco.Module+import Disco.Names+import Disco.Parser+import Disco.Pretty hiding ((<>))+import qualified Disco.Pretty as Pretty+import Disco.Typecheck (checkModule)+import Disco.Typecheck.Util+import Disco.Types+import Disco.Value  ------------------------------------------------------------ -- Configuation options@@ -103,9 +107,10 @@ makeLenses ''DiscoConfig  initDiscoConfig :: DiscoConfig-initDiscoConfig = DiscoConfig-  { _debugMode = False-  }+initDiscoConfig =+  DiscoConfig+    { _debugMode = False+    }  ------------------------------------------------------------ -- Top level info record@@ -114,32 +119,29 @@ -- | A record of information about the current top-level environment. data TopInfo = TopInfo   { _replModInfo :: ModuleInfo-    -- ^ Info about the top-level module collecting stuff entered at-    --   the REPL.--  , _topEnv      :: Env-    -- ^ Top-level environment mapping names to values.  Set by-    --   'loadDefs'.--  , _topModMap   :: Map ModuleName ModuleInfo-    -- ^ Mapping from loaded module names to their 'ModuleInfo'-    --   records.--  , _lastFile    :: Maybe FilePath-    -- ^ The most recent file which was :loaded by the user.-+  -- ^ Info about the top-level module collecting stuff entered at+  --   the REPL.+  , _topEnv :: Env+  -- ^ Top-level environment mapping names to values.  Set by+  --   'loadDefs'.+  , _topModMap :: Map ModuleName ModuleInfo+  -- ^ Mapping from loaded module names to their 'ModuleInfo'+  --   records.+  , _lastFile :: Maybe FilePath+  -- ^ The most recent file which was :loaded by the user.   , _discoConfig :: DiscoConfig   }  -- | The initial (empty) record of top-level info. initTopInfo :: DiscoConfig -> TopInfo-initTopInfo cfg = TopInfo-  { _replModInfo = emptyModuleInfo-  , _topEnv      = emptyCtx-  , _topModMap   = M.empty-  , _lastFile    = Nothing-  , _discoConfig = cfg-  }+initTopInfo cfg =+  TopInfo+    { _replModInfo = emptyModuleInfo+    , _topEnv = emptyCtx+    , _topModMap = M.empty+    , _lastFile = Nothing+    , _discoConfig = cfg+    }  makeLenses ''TopInfo @@ -158,13 +160,14 @@ -- However, just manually implementing it here seems easier.  -- | Effects needed at the top level.-type TopEffects = '[Error DiscoError, State TopInfo, Output Message, Embed IO, Final (H.InputT IO)]+type TopEffects = '[Error DiscoError, State TopInfo, Output (Message ()), Embed IO, Final (H.InputT IO)]  -- | Effects needed for evaluation.-type EvalEffects = [Error EvalError, Random, LFresh, Output Message, State Mem]-  -- XXX write about order.-  -- memory, counter etc. should not be reset by errors.+type EvalEffects = [Error EvalError, Random, LFresh, Output (Message ()), State Mem] +-- XXX write about order.+-- memory, counter etc. should not be reset by errors.+ -- | All effects needed for the top level + evaluation. type DiscoEffects = AppendEffects EvalEffects TopEffects @@ -188,21 +191,21 @@     . runFinal @(H.InputT IO)     . embedToFinal     . runEmbedded @_ @(H.InputT IO) liftIO-    . runOutputSem (handleMsg msgFilter)    -- Handle Output Message via printing to console-    . stateToIO (initTopInfo cfg)           -- Run State TopInfo via an IORef-    . inputToState                          -- Dispatch Input TopInfo effect via State effect-    . runState emptyMem                     -- Start with empty memory-    . outputDiscoErrors                     -- Output any top-level errors-    . runLFresh                             -- Generate locally fresh names-    . runRandomIO                           -- Generate randomness via IO-    . 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+    . runOutputSem (handleMsg msgFilter) -- Handle Output Message via printing to console+    . stateToIO (initTopInfo cfg) -- Run State TopInfo via an IORef+    . inputToState -- Dispatch Input TopInfo effect via State effect+    . runState emptyMem -- Start with empty memory+    . outputDiscoErrors -- Output any top-level errors+    . runLFresh -- Generate locally fresh names+    . runRandomIO -- Generate randomness via IO+    . 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-      | otherwise        = (/= Debug) . view messageType+ where+  msgFilter+    | cfg ^. debugMode = const True+    | otherwise = (/= Debug) . view messageType  ------------------------------------------------------------ -- Environment utilities@@ -252,7 +255,7 @@  -- | A variant of 'runTCM' that requires only a 'TCError' instead --   of a 'LocTCError'.-runTCM'  ::+runTCM' ::   Member (Error DiscoError) r =>   TyCtx ->   TyDefCtx ->@@ -266,12 +269,12 @@  -- | Run a typechecking computation in the context of the top-level --   REPL module, re-throwing a wrapped error if it fails.-typecheckTop-  :: Members '[Input TopInfo, Error DiscoError] r-  => Sem (Reader TyCtx ': Reader TyDefCtx ': Fresh ': Error TCError ': r) a-  -> Sem r a+typecheckTop ::+  Members '[Input TopInfo, Error DiscoError] r =>+  Sem (Reader TyCtx ': Reader TyDefCtx ': Fresh ': Error TCError ': r) a ->+  Sem r a typecheckTop tcm = do-  tyctx  <- inputs (view (replModInfo . miTys))+  tyctx <- inputs (view (replModInfo . miTys))   imptyctx <- inputs (toListOf (replModInfo . miImports . traverse . miTys))   tydefs <- inputs (view (replModInfo . miTydefs))   imptydefs <- inputs (toListOf (replModInfo . miImports . traverse . miTydefs))@@ -288,9 +291,12 @@ -- --   The 'Resolver' argument specifies where to look for imported --   modules.-loadDiscoModule-  :: Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r-  => Bool -> Resolver -> FilePath -> Sem r ModuleInfo+loadDiscoModule ::+  Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r =>+  Bool ->+  Resolver ->+  FilePath ->+  Sem r ModuleInfo loadDiscoModule quiet resolver =   loadDiscoModule' quiet resolver [] @@ -299,9 +305,13 @@ --   a context that includes the current top-level context (unlike a --   module loaded from disk).  Used for e.g. blocks/modules entered --   at the REPL prompt.-loadParsedDiscoModule-  :: Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r-  => Bool -> Resolver -> ModuleName -> Module -> Sem r ModuleInfo+loadParsedDiscoModule ::+  Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r =>+  Bool ->+  Resolver ->+  ModuleName ->+  Module ->+  Sem r ModuleInfo loadParsedDiscoModule quiet resolver =   loadParsedDiscoModule' quiet REPL resolver [] @@ -309,15 +319,19 @@ --   Map from module names to 'ModuleInfo' records, to avoid loading --   any imported module more than once. Resolve the module, load and --   parse it, then call 'loadParsedDiscoModule''.-loadDiscoModule'-  :: Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r-  => Bool -> Resolver -> [ModuleName] -> FilePath-  -> Sem r ModuleInfo-loadDiscoModule' quiet resolver inProcess modPath  = do-  (resolvedPath, prov) <- resolveModule resolver modPath-                  >>= maybe (throw $ ModuleNotFound modPath) return+loadDiscoModule' ::+  Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r =>+  Bool ->+  Resolver ->+  [ModuleName] ->+  FilePath ->+  Sem r ModuleInfo+loadDiscoModule' quiet resolver inProcess modPath = do+  (resolvedPath, prov) <-+    resolveModule resolver modPath+      >>= maybe (throw $ ModuleNotFound modPath) return   let name = Named prov modPath-  when (name `elem` inProcess) (throw $ CyclicImport (name:inProcess))+  when (name `elem` inProcess) (throw $ CyclicImport (name : inProcess))   modMap <- use @TopInfo topModMap   case M.lookup name modMap of     Just mi -> return mi@@ -337,34 +351,39 @@ --   it in the context of the top-level type context iff the --   'LoadingMode' parameter is 'REPL'.  Recursively load all its --   imports, then typecheck it.-loadParsedDiscoModule'-  :: Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r-  => Bool -> LoadingMode -> Resolver -> [ModuleName] -> ModuleName -> Module -> Sem r ModuleInfo+loadParsedDiscoModule' ::+  Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r =>+  Bool ->+  LoadingMode ->+  Resolver ->+  [ModuleName] ->+  ModuleName ->+  Module ->+  Sem r ModuleInfo loadParsedDiscoModule' quiet mode resolver inProcess name cm@(Module _ mns _ _ _) = do-   -- Recursively load any modules imported by this one, plus standard   -- library modules (unless NoStdLib is enabled), and build a map with the results.   mis <- mapM (loadDiscoModule' quiet (withStdlib resolver) inProcess) mns   stdmis <- case NoStdLib `S.member` modExts cm of-    True  -> return []+    True -> return []     False -> mapM (loadDiscoModule' True FromStdlib inProcess) stdLib   let modImps = M.fromList (map (view miName &&& id) (mis ++ stdmis))    -- Get context and type definitions from the REPL, in case we are in REPL mode.   topImports <- use (replModInfo . miImports)-  topTyCtx   <- use (replModInfo . miTys)+  topTyCtx <- use (replModInfo . miTys)   topTyDefns <- use (replModInfo . miTydefs)    -- Choose the contexts to use based on mode: if we are loading a   -- standalone module, we should start it in an empty context.  If we   -- are loading something entered at the REPL, we need to include any   -- existing top-level REPL context.-  let importMap = case mode of { Standalone -> modImps; REPL -> topImports <> modImps }-      tyctx   = case mode of { Standalone -> emptyCtx ; REPL -> topTyCtx }-      tydefns = case mode of { Standalone -> M.empty ; REPL -> topTyDefns }+  let importMap = case mode of Standalone -> modImps; REPL -> topImports <> modImps+      tyctx = case mode of Standalone -> emptyCtx; REPL -> topTyCtx+      tydefns = case mode of Standalone -> M.empty; REPL -> topTyDefns    -- Typecheck (and resolve names in) the module.-  m  <- runTCM tyctx tydefns $ checkModule name importMap cm+  m <- runTCM tyctx tydefns $ checkModule name importMap cm    -- Evaluate all the module definitions and add them to the topEnv.   mapError EvalErr $ loadDefsFrom m@@ -375,27 +394,29 @@  -- | Try loading the contents of a file from the filesystem, emitting --   an error if it's not found.-loadFile :: Members '[Output Message, Embed IO] r => FilePath -> Sem r (Maybe String)+loadFile :: Members '[Output (Message ann), Embed IO] r => FilePath -> Sem r (Maybe String) loadFile file = do   res <- liftIO $ handle @SomeException (return . Left) (Right <$> readFile file)   case res of-    Left _  -> info ("File not found:" <+> text file) >> return Nothing+    Left _ -> info ("File not found:" <+> text file) >> return Nothing     Right s -> return (Just s)  -- | Add things from the given module to the set of currently loaded --   things.-addToREPLModule-  :: Members '[Error DiscoError, State TopInfo, Random, State Mem, Output Message] r-  => ModuleInfo -> Sem r ()+addToREPLModule ::+  Members '[Error DiscoError, State TopInfo, Random, State Mem, Output (Message ann)] r =>+  ModuleInfo ->+  Sem r () addToREPLModule mi = modify @TopInfo (replModInfo <>~ mi)  -- | Set the given 'ModuleInfo' record as the currently loaded --   module. This also includes updating the top-level state with new --   term definitions, documentation, types, and type definitions. --   Replaces any previously loaded module.-setREPLModule-  :: Members '[State TopInfo, Random, Error EvalError, State Mem, Output Message] r-  => ModuleInfo -> Sem r ()+setREPLModule ::+  Members '[State TopInfo, Random, Error EvalError, State Mem, Output (Message ann)] r =>+  ModuleInfo ->+  Sem r () setREPLModule mi = do   modify @TopInfo $ replModInfo .~ mi @@ -408,7 +429,6 @@   ModuleInfo ->   Sem r () loadDefsFrom mi = do-   -- Note that the compiled definitions we get back from compileDefns   -- are topologically sorted by mutually recursive group. Each   -- definition needs to be evaluated in an environment containing the@@ -418,7 +438,9 @@  loadDef ::   Members '[State TopInfo, Random, Error EvalError, State Mem] r =>-  QName Core -> Core -> Sem r ()+  QName Core ->+  Core ->+  Sem r () loadDef x body = do   v <- inputToState @TopInfo . inputTopEnv $ eval body   modify @TopInfo $ topEnv %~ Ctx.insert x v