-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Functional programming language for teaching discrete math. -- -- Disco is a simple functional programming language for use in teaching -- discrete math. Its syntax is designed to be close to standard -- mathematical practice. @package disco @version 0.2 -- | Some orphan Data instances. module Disco.Data instance (Data.Data.Data a, Data.Data.Data b) => Data.Data.Data (Unbound.Generics.LocallyNameless.Bind.Bind a b) instance Data.Data.Data t => Data.Data.Data (Unbound.Generics.LocallyNameless.Embed.Embed t) instance (Data.Data.Data a, Data.Data.Data b) => Data.Data.Data (Unbound.Generics.LocallyNameless.Rebind.Rebind a b) instance Data.Data.Data a => Data.Data.Data (Unbound.Generics.LocallyNameless.Name.Name a) -- | Polysemy effect for integer counter. module Disco.Effects.Counter data Counter m a -- | Return the next integer in sequence. [Next] :: Counter m Integer -- | Return the next integer in sequence. next :: forall r_arCG. Member Counter r_arCG => Sem r_arCG Integer -- | Dispatch a counter effect, starting the counter from the given -- Integer. runCounter' :: Integer -> Sem (Counter ': r) a -> Sem r a -- | Dispatch a counter effect, starting the counter from zero. runCounter :: Sem (Counter ': r) a -> Sem r a -- | Utility functions for input effect. module Disco.Effects.Input -- | 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 -- | Use a function to (contravariantly) transform the input value in an -- input effect. mapInput :: forall s t r a. Member (Input s) r => (s -> t) -> Sem (Input t ': r) a -> Sem r a -- | Utility functions for state effect. module Disco.Effects.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 use :: Member (State s) r => Getter s a -> Sem r a (%=) :: Member (State s) r => Lens' s a -> (a -> a) -> Sem r () infix 4 %= (.=) :: Member (State s) r => Lens' s a -> a -> Sem r () infix 4 .= -- | Polysemy effect for a memory store with integer keys. module Disco.Effects.Store data Store v m a [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 () [AssocsStore] :: Store v m [(Int, v)] [KeepKeys] :: IntSet -> Store v m () keepKeys :: forall v_auzq r_auFO. Member (Store v_auzq) r_auFO => IntSet -> Sem r_auFO () assocsStore :: forall v_auzo r_auFN. Member (Store v_auzo) r_auFN => Sem r_auFN [(Int, v_auzo)] mapStore :: forall v_auzm r_auFL. Member (Store v_auzm) r_auFL => (v_auzm -> v_auzm) -> Sem r_auFL () insertStore :: forall v_auzk r_auFI. Member (Store v_auzk) r_auFI => Int -> v_auzk -> Sem r_auFI () lookupStore :: forall v_auzi r_auFG. Member (Store v_auzi) r_auFG => Int -> Sem r_auFG (Maybe v_auzi) new :: forall v_auzg r_auFE. Member (Store v_auzg) r_auFE => v_auzg -> Sem r_auFE Int clearStore :: forall v_auze r_auFD. Member (Store v_auze) r_auFD => Sem r_auFD () -- | Dispatch a store effect. runStore :: forall v r a. Sem (Store v ': r) a -> Sem r a -- | Meaningful types and functions for describing combinations of -- different possible options. module Disco.Exhaustiveness.Possibilities data Possibilities a retSingle :: Monad m => a -> m (Possibilities a) -- | List all possible paths through the list of Possibilites -- -- Ex. > allCombinations [ Possibilities [1] , Possibilities [2,3] , -- Possibilities [4] , Possibilities [5,6,7] ] === Possibilities -- {getPossibilities = [[1,2,4,5] ,[1,2,4,6] ,[1,2,4,7] ,[1,3,4,5] -- ,[1,3,4,6] ,[1,3,4,7] ]} -- -- 2 5 1 4 --6 / 3 7 -- -- If any any of the Possibilities is empty, an empty Possibility is -- returned -- -- In other words, this lists all elements of the cartesian product of -- multiple sets allCombinations :: [Possibilities a] -> Possibilities [a] anyOf :: [Possibilities a] -> Possibilities a none :: Possibilities a -> Bool getPossibilities :: Possibilities a -> [a] instance GHC.Base.Applicative Disco.Exhaustiveness.Possibilities.Possibilities instance GHC.Base.Monoid (Disco.Exhaustiveness.Possibilities.Possibilities a) instance GHC.Base.Semigroup (Disco.Exhaustiveness.Possibilities.Possibilities a) instance GHC.Base.Functor Disco.Exhaustiveness.Possibilities.Possibilities instance GHC.Classes.Ord a => GHC.Classes.Ord (Disco.Exhaustiveness.Possibilities.Possibilities a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Disco.Exhaustiveness.Possibilities.Possibilities a) instance GHC.Show.Show a => GHC.Show.Show (Disco.Exhaustiveness.Possibilities.Possibilities a) -- | Optional extensions to the disco language. module Disco.Extensions -- | Enumeration of optional language extensions. data Ext -- | Allow primitives, i.e. $prim Primitives :: Ext -- | Don't automatically import standard library modules NoStdLib :: Ext -- | Allow randomness. This is not implemented yet. Randomness :: Ext type ExtSet = Set Ext -- | The default set of language extensions (currently, the empty set). defaultExts :: ExtSet -- | A set of all possible language extensions, provided for convenience. allExts :: ExtSet -- | All possible language extensions in the form of a list. allExtsList :: [Ext] -- | Add an extension to an extension set. addExtension :: Ext -> ExtSet -> ExtSet instance GHC.Enum.Bounded Disco.Extensions.Ext instance GHC.Enum.Enum Disco.Extensions.Ext instance GHC.Read.Read Disco.Extensions.Ext instance GHC.Show.Show Disco.Extensions.Ext instance GHC.Classes.Ord Disco.Extensions.Ext instance GHC.Classes.Eq Disco.Extensions.Ext -- | XXX module Disco.Report data Report RTxt :: String -> Report RSeq :: [Report] -> Report RVSeq :: [Report] -> Report RList :: [Report] -> Report RNest :: Report -> Report text :: String -> Report hcat :: [Report] -> Report hsep :: [Report] -> Report vcat :: [Report] -> Report vsep :: [Report] -> Report list :: [Report] -> Report nest :: Report -> Report instance GHC.Show.Show Disco.Report.Report -- | Unary and binary operators along with information like precedence, -- fixity, and concrete syntax. module Disco.Syntax.Operators -- | Unary operators. data UOp -- | Arithmetic negation (-) Neg :: UOp -- | Logical negation (not) Not :: UOp -- | Factorial (!) Fact :: UOp -- | Binary operators. data BOp -- | Addition (+) Add :: BOp -- | Subtraction (-) Sub :: BOp -- | Saturating Subtraction (.- / ∸) SSub :: BOp -- | Multiplication (*) Mul :: BOp -- | Division (/) Div :: BOp -- | Exponentiation (^) Exp :: BOp -- | Integer division (//) IDiv :: BOp -- | Equality test (==) Eq :: BOp -- | Not-equal (/=) Neq :: BOp -- | Less than (<) Lt :: BOp -- | Greater than (>) Gt :: BOp -- | Less than or equal (<=) Leq :: BOp -- | Greater than or equal (>=) Geq :: BOp -- | Logical and (&& / and) And :: BOp -- | Logical or (|| / or) Or :: BOp -- | Logical implies (-> / implies) Impl :: BOp -- | Logical biconditional (- / iff) Iff :: BOp -- | Modulo (mod) Mod :: BOp -- | Divisibility test (|) Divides :: BOp -- | Binomial and multinomial coefficients (choose) Choose :: BOp -- | List cons (::) Cons :: BOp -- | Cartesian product of sets (** / ⨯) CartProd :: BOp -- | Union of two sets (union / ∪) Union :: BOp -- | Intersection of two sets (intersect / ∩) Inter :: BOp -- | Difference between two sets (@@) Diff :: BOp -- | Element test (∈) Elem :: BOp -- | Subset test (⊆) Subset :: BOp -- | Make a binary boolean operator into a testable proposition Should :: BOp -> BOp -- | Type operators. data TyOp -- | List all values of a type Enumerate :: TyOp -- | Count how many values there are of a type Count :: TyOp -- | Fixities of unary operators (either pre- or postfix). data UFixity -- | Unary prefix. Pre :: UFixity -- | Unary postfix. Post :: UFixity -- | Fixity/associativity of infix binary operators (either left, right, or -- non-associative). data BFixity -- | Left-associative infix. InL :: BFixity -- | Right-associative infix. InR :: BFixity -- | Infix. In :: BFixity -- | Operators together with their fixity. data OpFixity UOpF :: UFixity -> UOp -> OpFixity BOpF :: BFixity -> BOp -> OpFixity -- | An OpInfo record contains information about an operator, such -- as the operator itself, its fixity, a list of concrete syntax -- representations, and a numeric precedence level. data OpInfo OpInfo :: OpFixity -> [String] -> Int -> OpInfo [opFixity] :: OpInfo -> OpFixity [opSyns] :: OpInfo -> [String] [opPrec] :: OpInfo -> Int -- | The opTable lists all the operators in the language, in order -- of precedence (highest precedence first). Operators in the same list -- have the same precedence. This table is used by both the parser and -- the pretty-printer. opTable :: [[OpInfo]] -- | A map from all unary operators to their associated OpInfo -- records. uopMap :: Map UOp OpInfo -- | A map from all binary operators to their associatied OpInfo -- records. bopMap :: Map BOp OpInfo opNames :: [String] -- | A convenient function for looking up the precedence of a unary -- operator. uPrec :: UOp -> Int -- | A convenient function for looking up the precedence of a binary -- operator. bPrec :: BOp -> Int -- | Look up the "fixity" (i.e. associativity) of a binary operator. assoc :: BOp -> BFixity -- | The precedence level of function application (higher than any other -- precedence level). funPrec :: Int instance Unbound.Generics.LocallyNameless.Subst.Subst t Disco.Syntax.Operators.UOp instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Syntax.Operators.UOp instance Data.Data.Data Disco.Syntax.Operators.UOp instance GHC.Generics.Generic Disco.Syntax.Operators.UOp instance GHC.Classes.Ord Disco.Syntax.Operators.UOp instance GHC.Classes.Eq Disco.Syntax.Operators.UOp instance GHC.Read.Read Disco.Syntax.Operators.UOp instance GHC.Show.Show Disco.Syntax.Operators.UOp instance Unbound.Generics.LocallyNameless.Subst.Subst t Disco.Syntax.Operators.BOp instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Syntax.Operators.BOp instance Data.Data.Data Disco.Syntax.Operators.BOp instance GHC.Generics.Generic Disco.Syntax.Operators.BOp instance GHC.Classes.Ord Disco.Syntax.Operators.BOp instance GHC.Classes.Eq Disco.Syntax.Operators.BOp instance GHC.Read.Read Disco.Syntax.Operators.BOp instance GHC.Show.Show Disco.Syntax.Operators.BOp instance Unbound.Generics.LocallyNameless.Subst.Subst t Disco.Syntax.Operators.TyOp instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Syntax.Operators.TyOp instance Data.Data.Data Disco.Syntax.Operators.TyOp instance GHC.Generics.Generic Disco.Syntax.Operators.TyOp instance GHC.Classes.Ord Disco.Syntax.Operators.TyOp instance GHC.Classes.Eq Disco.Syntax.Operators.TyOp instance GHC.Show.Show Disco.Syntax.Operators.TyOp instance GHC.Generics.Generic Disco.Syntax.Operators.UFixity instance GHC.Show.Show Disco.Syntax.Operators.UFixity instance GHC.Enum.Bounded Disco.Syntax.Operators.UFixity instance GHC.Enum.Enum Disco.Syntax.Operators.UFixity instance GHC.Classes.Ord Disco.Syntax.Operators.UFixity instance GHC.Classes.Eq Disco.Syntax.Operators.UFixity instance GHC.Generics.Generic Disco.Syntax.Operators.BFixity instance GHC.Show.Show Disco.Syntax.Operators.BFixity instance GHC.Enum.Bounded Disco.Syntax.Operators.BFixity instance GHC.Enum.Enum Disco.Syntax.Operators.BFixity instance GHC.Classes.Ord Disco.Syntax.Operators.BFixity instance GHC.Classes.Eq Disco.Syntax.Operators.BFixity instance GHC.Generics.Generic Disco.Syntax.Operators.OpFixity instance GHC.Show.Show Disco.Syntax.Operators.OpFixity instance GHC.Classes.Eq Disco.Syntax.Operators.OpFixity instance GHC.Show.Show Disco.Syntax.Operators.OpInfo -- | Precedence and associativity for pretty-printing. module Disco.Pretty.Prec type Prec = Int data PA PA :: Prec -> BFixity -> PA lowerPrec :: PA -> PA -> Bool initPA :: PA ascrPA :: PA funPA :: PA rPA :: Int -> PA tarrPA :: PA taddPA :: PA tmulPA :: PA tfunPA :: PA ugetPA :: UOp -> PA getPA :: BOp -> PA instance GHC.Classes.Eq Disco.Pretty.Prec.PA instance GHC.Show.Show Disco.Pretty.Prec.PA -- | Adapter DSL on top of Text.PrettyPrint for Applicative -- pretty-printing. module Disco.Pretty.DSL vcat :: Applicative f => [f (Doc ann)] -> f (Doc ann) hcat :: Applicative f => [f (Doc ann)] -> f (Doc ann) hsep :: Applicative f => [f (Doc ann)] -> f (Doc ann) parens :: Functor f => f (Doc ann) -> f (Doc ann) brackets :: Functor f => f (Doc ann) -> f (Doc ann) braces :: Functor f => f (Doc ann) -> f (Doc ann) bag :: Applicative f => f (Doc ann) -> f (Doc ann) quotes :: Functor f => f (Doc ann) -> f (Doc ann) doubleQuotes :: Functor f => f (Doc ann) -> f (Doc ann) text :: Applicative m => String -> m (Doc ann) integer :: Applicative m => Integer -> m (Doc ann) nest :: Functor f => Int -> f (Doc ann) -> f (Doc ann) indent :: Functor f => Int -> f (Doc ann) -> f (Doc ann) hang :: Applicative f => f (Doc ann) -> Int -> f (Doc ann) -> f (Doc ann) empty :: Applicative m => m (Doc ann) (<+>) :: Applicative f => f (Doc ann) -> f (Doc ann) -> f (Doc ann) (<>) :: Applicative f => f (Doc ann) -> f (Doc ann) -> f (Doc ann) ($+$) :: Applicative f => f (Doc ann) -> f (Doc ann) -> f (Doc ann) punctuate :: Applicative f => f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)] intercalate :: Monad f => f (Doc ann) -> [f (Doc ann)] -> f (Doc ann) bulletList :: Applicative f => f (Doc ann) -> [f (Doc ann)] -> f (Doc ann) renderDoc :: Sem (Reader PA ': r) (Doc ann) -> Sem r String renderDoc' :: Doc ann -> String instance Data.String.IsString (Polysemy.Internal.Sem r (Prettyprinter.Internal.Doc ann)) -- | Concrete syntax for the prims (i.e. built-in constants) supported by -- the language. module Disco.Syntax.Prims -- | Primitives, i.e. built-in constants. data Prim -- | Unary operator [PrimUOp] :: UOp -> Prim -- | Binary operator [PrimBOp] :: BOp -> Prim -- | Left injection into a sum type. [PrimLeft] :: Prim -- | Right injection into a sum type. [PrimRight] :: Prim -- | Integer square root (sqrt) [PrimSqrt] :: Prim -- | Floor of fractional type (floor) [PrimFloor] :: Prim -- | Ceiling of fractional type (ceiling) [PrimCeil] :: Prim -- | Absolute value (abs) [PrimAbs] :: Prim -- | Min [PrimMin] :: Prim -- | Max [PrimMax] :: Prim -- | Power set (XXX or bag?) [PrimPower] :: Prim -- | Container -> list conversion [PrimList] :: Prim -- | Container -> bag conversion [PrimBag] :: Prim -- | Container -> set conversion [PrimSet] :: Prim -- | bag -> set of counts conversion [PrimB2C] :: Prim -- | set of counts -> bag conversion [PrimC2B] :: Prim -- | unsafe set of counts -> bag conversion that assumes all distinct [PrimUC2B] :: Prim -- | Map k v -> Set (k × v) [PrimMapToSet] :: Prim -- | Set (k × v) -> Map k v [PrimSetToMap] :: Prim -- | Get Adjacency list of Graph [PrimSummary] :: Prim -- | Construct a graph Vertex [PrimVertex] :: Prim -- | Empty graph [PrimEmptyGraph] :: Prim -- | Overlay two Graphs [PrimOverlay] :: Prim -- | Connect Graph to another with directed edges [PrimConnect] :: Prim -- | Insert into map [PrimInsert] :: Prim -- | Get value associated with key in map [PrimLookup] :: Prim -- | Each operation for containers [PrimEach] :: Prim -- | Reduce operation for containers [PrimReduce] :: Prim -- | Filter operation for containers [PrimFilter] :: Prim -- | Monadic join for containers [PrimJoin] :: Prim -- | Generic merge operation for bags/sets [PrimMerge] :: Prim -- | Efficient primality test [PrimIsPrime] :: Prim -- | Factorization [PrimFactor] :: Prim -- | Turn a rational into a pair (num, denom) [PrimFrac] :: Prim -- | Crash [PrimCrash] :: Prim -- | 
--   [x, y, z .. e]
--
[PrimUntil] :: Prim -- | Test whether a proposition holds [PrimHolds] :: Prim -- | Lookup OEIS sequence [PrimLookupSeq] :: Prim -- | Extend OEIS sequence [PrimExtendSeq] :: Prim -- | Generates a pseudorandom number generator [PrimSeed] :: Prim -- | Given a range and a generator, generates random number [PrimRandom] :: Prim -- | An info record for a single primitive name, containing the primitive -- itself, its concrete syntax, and whether it is "exposed", i.e. -- available to be used in the surface syntax of the basic language. -- Unexposed prims can only be referenced by enabling the Primitives -- language extension and prefixing their name by $. data PrimInfo PrimInfo :: Prim -> String -> Bool -> PrimInfo [thePrim] :: PrimInfo -> Prim [primSyntax] :: PrimInfo -> String [primExposed] :: PrimInfo -> Bool -- | A table containing a PrimInfo record for every non-operator -- Prim recognized by the language. primTable :: [PrimInfo] -- | Find any exposed prims with the given name. toPrim :: String -> [Prim] -- | A convenient map from each Prim to its info record. primMap :: Map Prim PrimInfo instance Data.Data.Data Disco.Syntax.Prims.Prim instance Unbound.Generics.LocallyNameless.Subst.Subst t Disco.Syntax.Prims.Prim instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Syntax.Prims.Prim instance GHC.Generics.Generic Disco.Syntax.Prims.Prim instance GHC.Classes.Ord Disco.Syntax.Prims.Prim instance GHC.Classes.Eq Disco.Syntax.Prims.Prim instance GHC.Read.Read Disco.Syntax.Prims.Prim instance GHC.Show.Show Disco.Syntax.Prims.Prim -- | Miscellaneous utilities. module Disco.Util -- | A synonym for pairing which makes convenient syntax for constructing -- literal maps via M.fromList. (==>) :: a -> b -> (a, b) infixr 1 ==> -- | Flipped variant of map. for :: [a] -> (a -> b) -> [b] -- | A variant of Map indexing that throws a custom error message -- in case the key is not found, to help with debugging. (!) :: (Show k, Ord k) => Map k v -> k -> v -- | Find the maximum of a list of positive numbers, yielding 0 in the case -- of an empty list. maximum0 :: (Num a, Ord a) => [a] -> a -- | A variant of filter that returns a Maybe (NonEmpty a) -- instead of a regular list. filterNE :: (a -> Bool) -> NonEmpty a -> Maybe (NonEmpty a) -- | A variant of partition that returns Maybe (NonEmpty -- a)s instead of regular lists. partitionNE :: (a -> Bool) -> NonEmpty a -> (Maybe (NonEmpty a), Maybe (NonEmpty a)) -- | A variant of partitionEithers for nonempty lists. If the -- result is Left, it means all the inputs were Left. If the result is -- Right, we definitely have some Rights, and possibly some Lefts as -- well. This properly encodes the fact that at least one result list -- must be nonempty. partitionEithersNE :: NonEmpty (Either a b) -> Either (NonEmpty a) ([a], NonEmpty b) -- | Iterate a function until finding the first value that satisfies the -- given predicate. iterUntil f p is equivalent to head . -- filter p . iterate f but does not trigger a partiality warning. iterUntil :: (a -> a) -> (a -> Maybe b) -> a -> b -- | Allow a value through only if it satisfies the given predicate. gate :: Alternative f => (a -> Bool) -> a -> f a -- | Built-in documentation. module Disco.Doc -- | Lookup keys for documentation. data DocKey [PrimKey] :: Prim -> DocKey [OtherKey] :: String -> DocKey -- | An enumeration of different types of documentation references. data RefType -- | A reference to the Gentle Introduction -- (https:/disco-lang.readthedocs.ioenlatestintroduction/index.html) [Intro] :: RefType -- | A reference to the Language Reference -- (https:/disco-lang.readthedocs.ioenlatestreference/index.html) [Ref] :: RefType -- | An arbitrary free-form URL [URL] :: RefType -- | A reference for further reading. data Reference Reference :: RefType -> String -> Reference [refType] :: Reference -> RefType [ref] :: Reference -> String mkRef :: String -> Reference mkIntro :: String -> Reference -- | A map storing documentation for various things that can be looked up -- with :doc. Each key is mapped to a short descriptive string, plus -- references for further reading. docMap :: Map DocKey (String, [Reference]) instance GHC.Show.Show Disco.Doc.DocKey instance GHC.Classes.Ord Disco.Doc.DocKey instance GHC.Classes.Eq Disco.Doc.DocKey instance GHC.Enum.Enum Disco.Doc.RefType instance GHC.Enum.Bounded Disco.Doc.RefType instance GHC.Read.Read Disco.Doc.RefType instance GHC.Show.Show Disco.Doc.RefType instance GHC.Classes.Ord Disco.Doc.RefType instance GHC.Classes.Eq Disco.Doc.RefType instance GHC.Show.Show Disco.Doc.Reference instance GHC.Classes.Ord Disco.Doc.Reference instance GHC.Classes.Eq Disco.Doc.Reference -- | Polysemy effect for local fresh name generation, compatible with the -- unbound-generics library. module Disco.Effects.LFresh -- | Local fresh name generation effect. data LFresh m a [Lfresh] :: Typeable a => Name a -> LFresh m (Name a) [Avoid] :: [AnyName] -> m a -> LFresh m a [GetAvoids] :: LFresh m (Set AnyName) getAvoids :: forall r_a1ewG. Member LFresh r_a1ewG => Sem r_a1ewG (Set AnyName) avoid :: forall r_a1ewD a_a1euQ. Member LFresh r_a1ewD => [AnyName] -> Sem r_a1ewD a_a1euQ -> Sem r_a1ewD a_a1euQ lfresh :: forall r_a1ewB a_X0. (Member LFresh r_a1ewB, Typeable a_X0) => Name a_X0 -> Sem r_a1ewB (Name a_X0) -- | Dispatch an LFresh effect via a Reader effect to keep -- track of a set of in-scope names. runLFresh :: Sem (LFresh ': r) a -> Sem r a runLFresh' :: Sem (LFresh ': r) a -> Sem (Reader (Set AnyName) ': r) a -- | Open a binder, automatically freshening the names of the bound -- 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, Alpha p, Alpha t) => Bind p t -> ((p, t) -> Sem r c) -> Sem r c absorbLFresh :: Member LFresh r => (LFresh (Sem r) => Sem r a) -> Sem r a data LFreshDict m LFreshDict :: (forall a. Typeable a => Name a -> m (Name a)) -> (forall a. [AnyName] -> m a -> m a) -> m (Set AnyName) -> LFreshDict m [lfresh_] :: LFreshDict m -> forall a. Typeable a => Name a -> m (Name a) [avoid_] :: LFreshDict m -> forall a. [AnyName] -> m a -> m a [getAvoids_] :: LFreshDict m -> m (Set AnyName) -- | Wrapper for a monadic action with phantom type parameter for -- reflection. Locally defined so that the instance we are going to build -- with reflection must be coherent, that is there cannot be orphans. newtype Action m s' a Action :: m a -> Action m s' a instance forall (m :: * -> *) k (s' :: k). GHC.Base.Monad m => GHC.Base.Monad (Disco.Effects.LFresh.Action m s') instance forall (m :: * -> *) k (s' :: k). GHC.Base.Applicative m => GHC.Base.Applicative (Disco.Effects.LFresh.Action m s') instance forall (m :: * -> *) k (s' :: k). GHC.Base.Functor m => GHC.Base.Functor (Disco.Effects.LFresh.Action m s') instance forall k (m :: * -> *) (s' :: k). (GHC.Base.Monad m, Data.Reflection.Reifies s' (Disco.Effects.LFresh.LFreshDict m)) => Unbound.Generics.LocallyNameless.LFresh.LFresh (Disco.Effects.LFresh.Action m s') -- | Various pretty-printing facilities for disco. module Disco.Pretty class Pretty t pretty :: (Pretty t, Members '[Reader PA, LFresh] r) => t -> Sem r (Doc ann) pretty' :: Pretty t => t -> Sem r (Doc ann) prettyStr :: Pretty t => t -> Sem r String -- | Convenience function combining setPA and mparens, since -- we often want to simultaneously indicate what the precedence and -- associativity of a term is, and optionally surround it with -- parentheses depending on the precedence and associativity of its -- parent. withPA :: Member (Reader PA) r => PA -> Sem r (Doc ann) -> Sem r (Doc ann) -- | Mark a subcomputation as pretty-printing a term on the left of an -- operator (so parentheses can be inserted appropriately, depending on -- the associativity). lt :: Member (Reader PA) r => Sem r (Doc ann) -> Sem r (Doc ann) -- | Optionally surround a pretty-printed term with parentheses, depending -- on its precedence and associativity (given as the PA argument) -- and that of its context (given by the ambient 'Reader PA' effect). mparens :: Member (Reader PA) r => PA -> Sem r (Doc ann) -> Sem r (Doc ann) -- | Locally set the precedence and associativity within a subcomputation. setPA :: Member (Reader PA) r => PA -> Sem r a -> Sem r a -- | Mark a subcomputation as pretty-printing a term on the right of an -- operator (so parentheses can be inserted appropriately, depending on -- the associativity). rt :: Member (Reader PA) r => Sem r (Doc ann) -> Sem r (Doc ann) -- | Pretty-print a rational number as a fraction. prettyRational :: Rational -> String -- | Pretty-print a rational number using its decimal expansion, in the -- format nnn.prefix[rep]..., with any repeating digits enclosed -- in square brackets. prettyDecimal :: Rational -> String -- | digitalExpansion b n d takes the numerator and denominator of -- a fraction n/d between 0 and 1, and returns a pair of (1) a list of -- digits ds, and (2) a nonnegative integer k such that -- splitAt k ds = (prefix, rep), where the infinite base-b -- expansion of n/d is 0.(prefix ++ cycle rep). For example, -- -- 
--   digitalExpansion 10 1 4  = ([2,5,0], 2)
--   digitalExpansion 10 1 7  = ([1,4,2,8,5,7], 0)
--   digitalExpansion 10 3 28 = ([1,0,7,1,4,2,8,5], 2)
--   digitalExpansion 2  1 5  = ([0,0,1,1], 0)
--
-- -- It works by performing the standard long division algorithm, and -- looking for the first time that the remainder repeats. digitalExpansion :: Integer -> Integer -> Integer -> ([Integer], Int) findRep :: Ord a => [a] -> ([a], Int) findRep' :: Ord a => Map a Int -> Int -> [a] -> ([a], Int) -- | The abstract data type Doc ann represents pretty -- documents that have been annotated with data of type ann. -- -- More specifically, a value of type Doc represents a -- non-empty set of possible layouts of a document. The layout functions -- select one of these possibilities, taking into account things like the -- width of the output document. -- -- The annotation is an arbitrary piece of data associated with (part of) -- a document. Annotations may be used by the rendering backends in order -- to display output differently, such as -- -- -- -- The simplest way to display a Doc is via the Show class. -- -- 
--   >>> putStrLn (show (vsep ["hello", "world"]))
--   hello
--   world
--
data () => Doc ann instance Disco.Pretty.Pretty a => Disco.Pretty.Pretty [a] instance Disco.Pretty.Pretty a => Disco.Pretty.Pretty (GHC.Base.NonEmpty a) instance (Disco.Pretty.Pretty k, Disco.Pretty.Pretty v) => Disco.Pretty.Pretty (Data.Map.Internal.Map k v) instance Disco.Pretty.Pretty a => Disco.Pretty.Pretty (Data.Set.Internal.Set a) instance Disco.Pretty.Pretty (Unbound.Generics.LocallyNameless.Name.Name a) instance Disco.Pretty.Pretty Disco.Syntax.Operators.TyOp instance Disco.Pretty.Pretty Disco.Syntax.Operators.UOp instance Disco.Pretty.Pretty Disco.Syntax.Operators.BOp -- | Type qualifiers and sorts. module Disco.Types.Qualifiers -- | A "qualifier" is kind of like a type class in Haskell; but unlike -- Haskell, disco users cannot define their own. Rather, there is a -- finite fixed list of qualifiers supported by disco. For example, -- QSub denotes types which support a subtraction operation. -- Each qualifier corresponds to a set of types which satisfy it (see -- hasQual and qualRules). -- -- These qualifiers generally arise from uses of various operations. For -- example, the expression \x y. x - y would be inferred to have -- a type a -> a -> a [subtractive a], that is, a function -- of type a -> a -> a where a is any type that -- supports subtraction. -- -- These qualifiers can appear in a CQual constraint; see -- Disco.Typecheck.Constraint. data Qualifier -- | Numeric, i.e. a semiring supporting + and * QNum :: Qualifier -- | Subtractive, i.e. supports - QSub :: Qualifier -- | Divisive, i.e. supports / QDiv :: Qualifier -- | Comparable, i.e. supports decidable ordering/comparison (see Note -- [QCmp]) QCmp :: Qualifier -- | Enumerable, i.e. supports ellipsis notation [x .. y] QEnum :: Qualifier -- | Boolean, i.e. supports and, or, not (Bool or Prop) QBool :: Qualifier -- | Things that do not involve Prop. QBasic :: Qualifier -- | Things for which we can derive a *Haskell* Ord instance QSimple :: Qualifier -- | A helper function that returns the appropriate qualifier for a binary -- arithmetic operation. bopQual :: BOp -> Qualifier -- | A Sort represents a set of qualifiers, and also represents a -- set of types (in general, the intersection of the sets corresponding -- to the qualifiers). type Sort = Set Qualifier -- | The special sort <math> which includes all types. topSort :: Sort instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Types.Qualifiers.Qualifier instance GHC.Generics.Generic Disco.Types.Qualifiers.Qualifier instance GHC.Classes.Ord Disco.Types.Qualifiers.Qualifier instance GHC.Classes.Eq Disco.Types.Qualifiers.Qualifier instance GHC.Show.Show Disco.Types.Qualifiers.Qualifier instance Disco.Pretty.Pretty Disco.Types.Qualifiers.Qualifier -- | A thin layer on top of graphs from the fgl package, which -- allows dealing with vertices by label instead of by integer -- Node values. module Disco.Typecheck.Graph -- | Directed graphs, with vertices labelled by a and unlabelled -- edges. data Graph a G :: Gr a () -> Map a Node -> Map Node a -> Graph a -- | Create a graph with the given set of vertices and directed edges. If -- any edges refer to vertices that are not in the given vertex set, they -- will simply be dropped. mkGraph :: (Show a, Ord a) => Set a -> Set (a, a) -> Graph a -- | Return the set of vertices (nodes) of a graph. nodes :: Graph a -> Set a -- | Return the set of directed edges of a graph. edges :: Ord a => Graph a -> Set (a, a) -- | Map a function over all the vertices of a graph. Graph is not -- a Functor instance because of the Ord constraint on -- b. map :: Ord b => (a -> b) -> Graph a -> Graph b -- | Delete a vertex. delete :: (Show a, Ord a) => a -> Graph a -> Graph a -- | The condensation of a graph is the graph of its strongly -- connected components, i.e. each strongly connected component is -- compressed to a single node, labelled by the set of vertices in the -- component. There is an edge from component A to component B in the -- condensed graph iff there is an edge from any vertex in component A to -- any vertex in component B in the original graph. condensation :: Ord a => Graph a -> Graph (Set a) -- | Get a list of the weakly connected components of a graph, providing -- the set of vertices in each. Equivalently, return the strongly -- connected components of the graph when considered as an undirected -- graph. wcc :: Ord a => Graph a -> [Set a] wccIDs :: Ord a => Graph a -> [Set (Node, a)] -- | Do a topological sort on a DAG. topsort :: Graph a -> [a] -- | A miscellaneous utility function to turn a Graph Maybe into a -- Maybe Graph: the result is Just iff all the vertices -- in the input graph are. sequenceGraph :: Ord a => Graph (Maybe a) -> Maybe (Graph a) -- | Get a list of all the successors of a given node in the graph, -- i.e. all the nodes reachable from the given node by a directed -- path. Does not include the given node itself. suc :: (Show a, Ord a) => Graph a -> a -> [a] -- | Get a list of all the predecessors of a given node in the -- graph, i.e. all the nodes from which from the given node is -- reachable by a directed path. Does not include the given node itself. pre :: (Show a, Ord a) => Graph a -> a -> [a] -- | Given a graph, return two mappings: the first maps each vertex to its -- set of successors; the second maps each vertex to its set of -- predecessors. Equivalent to -- -- 
--   (M.fromList *** M.fromList) . unzip . map (\a -> ((a, suc g a), (a, pre g a))) . nodes $ g
--
-- -- but much more efficient. cessors :: (Show a, Ord a) => Graph a -> (Map a (Set a), Map a (Set a)) instance GHC.Show.Show a => GHC.Show.Show (Disco.Typecheck.Graph.Graph a) instance Disco.Pretty.Pretty a => Disco.Pretty.Pretty (Disco.Typecheck.Graph.Graph a) -- | The Disco.Subst module defines a generic type of substitutions -- that map variable names to values. module Disco.Subst -- | A value of type Substitution a is a substitution which maps -- some set of names (the domain, see dom) to values of -- type a. Substitutions can be applied to certain terms -- (see applySubst), replacing any free occurrences of names in -- the domain with their corresponding values. Thus, substitutions can be -- thought of as functions of type Term -> Term (for suitable -- Terms that contain names and values of the right type). -- -- Concretely, substitutions are stored using a Map. -- -- See also Disco.Types, which defines S as an alias for -- substitutions on types (the most common kind in the disco codebase). newtype Substitution a Substitution :: Map (Name a) a -> Substitution a [getSubst] :: Substitution a -> Map (Name a) a -- | The domain of a substitution is the set of names for which the -- substitution is defined. dom :: Substitution a -> Set (Name a) -- | The identity substitution, i.e. the unique substitution with an -- empty domain, which acts as the identity function on terms. idS :: Substitution a -- | Construct a singleton substitution, which maps the given name to the -- given value. (|->) :: Name a -> a -> Substitution a -- | Create a substitution from an association list of names and values. fromList :: [(Name a, a)] -> Substitution a -- | Convert a substitution into an association list. toList :: Substitution a -> [(Name a, a)] -- | Compose two substitutions. Applying s1 @@ s2 is the same as -- applying first s2, then s1; that is, semantically, -- composition of substitutions corresponds exactly to function -- composition when they are considered as functions on terms. -- -- As one would expect, composition is associative and has idS as -- its identity. (@@) :: Subst a a => Substitution a -> Substitution a -> Substitution a -- | Compose a whole container of substitutions. For example, compose -- [s1, s2, s3] = s1 @@ s2 @@ s3. compose :: (Subst a a, Foldable t) => t (Substitution a) -> Substitution a -- | Apply a substitution to a term, resulting in a new term in which any -- free variables in the domain of the substitution have been replaced by -- their corresponding values. Note this requires a Subst b a -- constraint, which intuitively means that values of type a -- contain variables of type b we can substitute for. applySubst :: Subst b a => Substitution b -> a -> a -- | Look up the value a particular name maps to under the given -- substitution; or return Nothing if the name being looked up -- is not in the domain. lookup :: Name a -> Substitution a -> Maybe a instance GHC.Show.Show a => GHC.Show.Show (Disco.Subst.Substitution a) instance GHC.Classes.Ord a => GHC.Classes.Ord (Disco.Subst.Substitution a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Disco.Subst.Substitution a) instance GHC.Base.Functor Disco.Subst.Substitution instance Disco.Pretty.Pretty a => Disco.Pretty.Pretty (Disco.Subst.Substitution a) -- | The Disco.Types module defines the set of types used in the -- disco language type system, along with various utility functions. module Disco.Types -- | Base types are the built-in types which form the basis of the disco -- type system, out of which more complex types can be built. data BaseTy -- | The void type, with no inhabitants. [Void] :: BaseTy -- | The unit type, with one inhabitant. [Unit] :: BaseTy -- | Booleans. [B] :: BaseTy -- | Propositions. [P] :: BaseTy -- | Natural numbers. [N] :: BaseTy -- | Integers. [Z] :: BaseTy -- | Fractionals (i.e. nonnegative rationals). [F] :: BaseTy -- | Rationals. [Q] :: BaseTy -- | Unicode characters. [C] :: BaseTy [Gen] :: BaseTy -- | Set container type. It's a bit odd putting these here since they have -- kind * -> * and all the other base types have kind *; but there's -- nothing fundamentally wrong with it and in particular this allows us -- to reuse all the existing constraint solving machinery for container -- subtyping. [CtrSet] :: BaseTy -- | Bag container type. [CtrBag] :: BaseTy -- | List container type. [CtrList] :: BaseTy -- | Test whether a BaseTy is a container (set, bag, or list). isCtr :: BaseTy -> Bool -- | Var represents type variables, that is, variables which -- stand for some type. data Var [V] :: Ilk -> Name Type -> Var -- | Var represents type variables, that is, variables which -- stand for some type. There are two kinds of type variables: -- -- data Ilk Skolem :: Ilk Unification :: Ilk pattern U :: Name Type -> Var pattern S :: Name Type -> Var -- | An atomic type is either a base type or a type variable. The -- alternative is a compound type which is built out of type -- constructors. The reason we split out the concept of atomic types into -- its own data type Atom is because constraints involving -- compound types can always be simplified/translated into constraints -- involving only atomic types. After that simplification step, we want -- to be able to work with collections of constraints that are guaranteed -- to contain only atomic types. data Atom [AVar] :: Var -> Atom [ABase] :: BaseTy -> Atom -- | Is this atomic type a variable? isVar :: Atom -> Bool -- | Is this atomic type a base type? isBase :: Atom -> Bool -- | Is this atomic type a skolem variable? isSkolem :: Atom -> Bool -- | Unifiable atomic types are the same as atomic types but without -- skolem variables. Hence, a unifiable atomic type is either a base type -- or a unification variable. -- -- Again, the reason this has its own type is that at some stage of the -- typechecking/constraint solving process, these should be the only -- things around; we can get rid of skolem variables because either they -- impose no constraints, or result in an error if they are related to -- something other than themselves. After checking these things, we can -- just focus on base types and unification variables. data UAtom [UB] :: BaseTy -> UAtom [UV] :: Name Type -> UAtom -- | Is this unifiable atomic type a (unification) variable? uisVar :: UAtom -> Bool -- | Convert a unifiable atomic type into a regular atomic type. uatomToAtom :: UAtom -> Atom -- | Convert a unifiable atomic type to an explicit Either type. uatomToEither :: UAtom -> Either BaseTy (Name Type) -- | Compound types, such as functions, product types, and sum -- types, are an application of a type constructor to one or more -- argument types. data Con -- | Function type constructor, T1 -> T2. [CArr] :: Con -- | Product type constructor, T1 * T2. [CProd] :: Con -- | Sum type constructor, T1 + T2. [CSum] :: Con -- | Container type (list, bag, or set) constructor. Note this looks like -- it could contain any Atom, but it will only ever contain either -- a type variable or a CtrList, CtrBag, or CtrSet. -- -- See also CList, CBag, and CSet. [CContainer] :: Atom -> Con -- | Key value maps, Map k v [CMap] :: Con -- | Graph constructor, Graph a [CGraph] :: Con -- | The name of a user defined algebraic datatype. [CUser] :: String -> Con -- | CList is provided for convenience; it represents a list type -- constructor (i.e. List a). pattern CList :: Con -- | CBag is provided for convenience; it represents a bag type -- constructor (i.e. Bag a). pattern CBag :: Con -- | CSet is provided for convenience; it represents a set type -- constructor (i.e. Set a). pattern CSet :: Con -- | The main data type for representing types in the disco language. A -- type can be either an atomic type, or the application of a type -- constructor to one or more type arguments. -- -- Types are broken down into two cases (TyAtom and -- TyCon) for ease of implementation: there are many situations -- where all atoms can be handled generically in one way and all type -- constructors can be handled generically in another. However, using -- this representation to write down specific types is tedious; for -- example, to represent the type N -> a one must write -- something like TyCon CArr [TyAtom (ABase N), TyAtom (AVar (U -- a))]. For this reason, pattern synonyms such as :->:, -- TyN, and TyVar are provided so that one can use them to -- construct and pattern-match on types when convenient. For example, -- using these synonyms the foregoing example can be written TyN -- :->: TyVar a. data Type -- | Atomic types (variables and base types), e.g. N, -- Bool, etc. [TyAtom] :: Atom -> Type -- | Application of a type constructor to type arguments, e.g. N -- -> Bool is the application of the arrow type constructor to -- the arguments N and Bool. [TyCon] :: Con -> [Type] -> Type pattern TyVar :: Name Type -> Type pattern TySkolem :: Name Type -> Type pattern TyVoid :: Type pattern TyUnit :: Type pattern TyBool :: Type pattern TyProp :: Type pattern TyN :: Type pattern TyZ :: Type pattern TyF :: Type pattern TyQ :: Type pattern TyC :: Type pattern TyGen :: Type pattern (:->:) :: Type -> Type -> Type infixr 5 :->: pattern (:*:) :: Type -> Type -> Type infixr 7 :*: pattern (:+:) :: Type -> Type -> Type infixr 6 :+: pattern TyList :: Type -> Type pattern TyBag :: Type -> Type pattern TySet :: Type -> Type pattern TyGraph :: Type -> Type pattern TyMap :: Type -> Type -> Type pattern TyContainer :: Atom -> Type -> Type -- | An application of a user-defined type. pattern TyUser :: String -> [Type] -> Type pattern TyString :: Type -- | PolyType represents a polymorphic type of the form forall -- a1 a2 ... an. ty (note, however, that n may be 0, that is, we can -- have a "trivial" polytype which quantifies zero variables). newtype PolyType Forall :: Bind [Name Type] Type -> PolyType -- | Convert a monotype into a trivial polytype that does not quantify over -- any type variables. If the type can contain free type variables, use -- closeType instead. toPolyType :: Type -> PolyType -- | Convert a monotype into a polytype by quantifying over all its free -- type variables. closeType :: Type -> PolyType -- | Check whether a type is a numeric type (N, Z, -- F, Q, or Zn). isNumTy :: Type -> Bool -- | Decide whether a type is empty, i.e. uninhabited. isEmptyTy :: Type -> Bool -- | Decide whether a type is finite. isFiniteTy :: Type -> Bool -- | Decide whether a type is searchable, i.e. effectively enumerable. isSearchable :: Type -> Bool -- | A value of type Substitution a is a substitution which maps -- some set of names (the domain, see dom) to values of -- type a. Substitutions can be applied to certain terms -- (see applySubst), replacing any free occurrences of names in -- the domain with their corresponding values. Thus, substitutions can be -- thought of as functions of type Term -> Term (for suitable -- Terms that contain names and values of the right type). -- -- Concretely, substitutions are stored using a Map. -- -- See also Disco.Types, which defines S as an alias for -- substitutions on types (the most common kind in the disco codebase). data Substitution a -- | Convert a substitution on atoms into a substitution on types. atomToTypeSubst :: Substitution Atom -> Substitution Type -- | Convert a substitution on unifiable atoms into a substitution on -- types. uatomToTypeSubst :: Substitution UAtom -> Substitution Type -- | Strictness represents the strictness (either strict or lazy) -- of a function application or let-expression. data Strictness Strict :: Strictness Lazy :: Strictness -- | Numeric types are strict; others are lazy. strictness :: Type -> Strictness -- | Is this a type variable? isTyVar :: Type -> Bool -- | Return a set of all the free container variables in a type. containerVars :: Type -> Set (Name Type) -- | Compute the number of inhabitants of a type. Nothing means -- the type is countably infinite. countType :: Type -> Maybe Integer -- | Decompose a nested product T1 * (T2 * ( ... )) into a list of -- types. unpair :: Type -> [Type] -- | Define S as a substitution on types (the most common kind) -- for convenience. type S = Substitution Type -- | The definition of a user-defined type contains: -- -- -- -- We represent type definitions this way (using a function, as opposed -- to a chunk of abstract syntax) because it makes some things simpler, -- and we don't particularly need to do anything more complicated. data TyDefBody TyDefBody :: [String] -> ([Type] -> Type) -> TyDefBody -- | A TyDefCtx is a mapping from type names to their corresponding -- definitions. type TyDefCtx = Map String TyDefBody -- | A type class for things whose type can be extracted or set. class HasType t -- | Get the type of a thing. getType :: HasType t => t -> Type -- | Set the type of a thing, when that is possible; the default -- implementation is for setType to do nothing. setType :: HasType t => Type -> t -> t instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.BaseTy Disco.Types.UAtom instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Types.UAtom instance GHC.Generics.Generic Disco.Types.UAtom instance GHC.Classes.Ord Disco.Types.UAtom instance GHC.Classes.Eq Disco.Types.UAtom instance GHC.Show.Show Disco.Types.UAtom instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.Types.BaseTy instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.UAtom Disco.Types.BaseTy instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Atom Disco.Types.BaseTy instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.BaseTy Disco.Types.BaseTy instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Types.BaseTy instance Data.Data.Data Disco.Types.BaseTy instance GHC.Generics.Generic Disco.Types.BaseTy instance GHC.Classes.Ord Disco.Types.BaseTy instance GHC.Classes.Eq Disco.Types.BaseTy instance GHC.Show.Show Disco.Types.BaseTy instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.Types.Ilk instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Atom Disco.Types.Ilk instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Types.Ilk instance Data.Data.Data Disco.Types.Ilk instance GHC.Generics.Generic Disco.Types.Ilk instance GHC.Show.Show Disco.Types.Ilk instance GHC.Read.Read Disco.Types.Ilk instance GHC.Classes.Ord Disco.Types.Ilk instance GHC.Classes.Eq Disco.Types.Ilk instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.Types.Var instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Atom Disco.Types.Var instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Types.Var instance Data.Data.Data Disco.Types.Var instance GHC.Generics.Generic Disco.Types.Var instance GHC.Classes.Ord Disco.Types.Var instance GHC.Classes.Eq Disco.Types.Var instance GHC.Show.Show Disco.Types.Var instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.Types.Atom instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Types.Atom instance Data.Data.Data Disco.Types.Atom instance GHC.Generics.Generic Disco.Types.Atom instance GHC.Classes.Ord Disco.Types.Atom instance GHC.Classes.Eq Disco.Types.Atom instance GHC.Show.Show Disco.Types.Atom instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Types.Con instance Data.Data.Data Disco.Types.Con instance GHC.Generics.Generic Disco.Types.Con instance GHC.Classes.Ord Disco.Types.Con instance GHC.Classes.Eq Disco.Types.Con instance GHC.Show.Show Disco.Types.Con instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Types.Type instance Data.Data.Data Disco.Types.Type instance GHC.Generics.Generic Disco.Types.Type instance GHC.Classes.Ord Disco.Types.Type instance GHC.Classes.Eq Disco.Types.Type instance GHC.Show.Show Disco.Types.Type instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.Types.PolyType instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Types.PolyType instance Data.Data.Data Disco.Types.PolyType instance GHC.Generics.Generic Disco.Types.PolyType instance GHC.Show.Show Disco.Types.PolyType instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Types.Strictness instance GHC.Generics.Generic Disco.Types.Strictness instance GHC.Show.Show Disco.Types.Strictness instance GHC.Classes.Eq Disco.Types.Strictness instance Disco.Pretty.Pretty Disco.Types.PolyType instance GHC.Show.Show Disco.Types.TyDefBody instance Disco.Pretty.Pretty (GHC.Base.String, Disco.Types.TyDefBody) instance Disco.Pretty.Pretty Disco.Types.BaseTy instance Disco.Pretty.Pretty Disco.Types.Ilk instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Atom Disco.Types.Atom instance Disco.Pretty.Pretty Disco.Types.Atom instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.UAtom Disco.Types.UAtom instance Disco.Pretty.Pretty Disco.Types.UAtom instance Disco.Pretty.Pretty Disco.Types.Con instance Disco.Pretty.Pretty Disco.Types.Type instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.Types.Qualifiers.Qualifier instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type GHC.Real.Rational instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type GHC.Base.Void instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.Types.Con instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.Types.Type instance (GHC.Classes.Ord a, Unbound.Generics.LocallyNameless.Subst.Subst t a) => Unbound.Generics.LocallyNameless.Subst.Subst t (Data.Set.Internal.Set a) instance (GHC.Classes.Ord k, Unbound.Generics.LocallyNameless.Subst.Subst t a) => Unbound.Generics.LocallyNameless.Subst.Subst t (Data.Map.Internal.Map k a) -- | Disco.Types.Rules defines some generic rules about arity, -- subtyping, and sorts for disco base types. module Disco.Types.Rules -- | A particular type argument can be either co- or contravariant with -- respect to subtyping. data Variance Co :: Variance Contra :: Variance -- | The arity of a type constructor is a list of variances, expressing -- both how many type arguments the constructor takes, and the variance -- of each argument. This is used to decompose subtyping constraints. -- -- For example, arity CArr = [Contra, Co] since function arrow -- is contravariant in its first argument and covariant in its second. -- That is, S1 -> T1 S2 - T2 (<: means "is -- a subtype of") if and only if S2 <: S1 and T1 <: -- T2. arity :: Con -> [Variance] -- | A "qualifier" is kind of like a type class in Haskell; but unlike -- Haskell, disco users cannot define their own. Rather, there is a -- finite fixed list of qualifiers supported by disco. For example, -- QSub denotes types which support a subtraction operation. -- Each qualifier corresponds to a set of types which satisfy it (see -- hasQual and qualRules). -- -- These qualifiers generally arise from uses of various operations. For -- example, the expression \x y. x - y would be inferred to have -- a type a -> a -> a [subtractive a], that is, a function -- of type a -> a -> a where a is any type that -- supports subtraction. -- -- These qualifiers can appear in a CQual constraint; see -- Disco.Typecheck.Constraint. data Qualifier -- | Numeric, i.e. a semiring supporting + and * QNum :: Qualifier -- | Subtractive, i.e. supports - QSub :: Qualifier -- | Divisive, i.e. supports / QDiv :: Qualifier -- | Comparable, i.e. supports decidable ordering/comparison (see Note -- [QCmp]) QCmp :: Qualifier -- | Enumerable, i.e. supports ellipsis notation [x .. y] QEnum :: Qualifier -- | Boolean, i.e. supports and, or, not (Bool or Prop) QBool :: Qualifier -- | Things that do not involve Prop. QBasic :: Qualifier -- | Things for which we can derive a *Haskell* Ord instance QSimple :: Qualifier -- | A helper function that returns the appropriate qualifier for a binary -- arithmetic operation. bopQual :: BOp -> Qualifier -- | A Sort represents a set of qualifiers, and also represents a -- set of types (in general, the intersection of the sets corresponding -- to the qualifiers). type Sort = Set Qualifier -- | The special sort <math> which includes all types. topSort :: Sort -- | A "direction" for the subtyping relation (either subtype or -- supertype). data Dir SubTy :: Dir SuperTy :: Dir -- | Swap directions. other :: Dir -> Dir -- | Check whether one atomic type is a subtype of the other. Returns -- True if either they are equal, or if they are base types and -- isSubB returns true. isSubA :: Atom -> Atom -> Bool -- | Check whether one base type is a subtype of another. isSubB :: BaseTy -> BaseTy -> Bool -- | Check whether one base type is a sub- or supertype of another. isDirB :: Dir -> BaseTy -> BaseTy -> Bool -- | List all the supertypes of a given base type. supertypes :: BaseTy -> [BaseTy] -- | List all the subtypes of a given base type. subtypes :: BaseTy -> [BaseTy] -- | List all the sub- or supertypes of a given base type. dirtypes :: Dir -> BaseTy -> [BaseTy] -- | Check whether a given base type satisfies a qualifier. hasQual :: BaseTy -> Qualifier -> Bool -- | Check whether a base type has a certain sort, which simply amounts to -- whether it satisfies every qualifier in the sort. hasSort :: BaseTy -> Sort -> Bool -- | Given a constructor T and a qualifier we want to hold of a type T t1 -- t2 ..., return a list of qualifiers that need to hold of t1, t2, ... qualRules :: Con -> Qualifier -> Maybe [Maybe Qualifier] -- | sortRules T s = [s1, ..., sn] means that sort s -- holds of type (T t1 ... tn) if and only if s1 t1 ... -- sn tn. For now this is just derived directly from -- qualRules. -- -- This is the arity function described in section 4.1 of -- Traytel et al. sortRules :: Con -> Sort -> Maybe [Sort] -- | Pick a base type (generally the "simplest") that satisfies a given -- sort. pickSortBaseTy :: Sort -> BaseTy instance GHC.Classes.Ord Disco.Types.Rules.Variance instance GHC.Classes.Eq Disco.Types.Rules.Variance instance GHC.Read.Read Disco.Types.Rules.Variance instance GHC.Show.Show Disco.Types.Rules.Variance instance GHC.Show.Show Disco.Types.Rules.Dir instance GHC.Read.Read Disco.Types.Rules.Dir instance GHC.Classes.Ord Disco.Types.Rules.Dir instance GHC.Classes.Eq Disco.Types.Rules.Dir -- | Constraints generated by type inference & checking. module Disco.Typecheck.Constraints -- | Constraints are generated as a result of type inference and checking. -- These constraints are accumulated during the inference and checking -- phase and are subsequently solved by the constraint solver. data Constraint [CSub] :: Type -> Type -> Constraint [CEq] :: Type -> Type -> Constraint [CQual] :: Qualifier -> Type -> Constraint [CAnd] :: NonEmpty Constraint -> Constraint [CTrue] :: Constraint [COr] :: NonEmpty Constraint -> Constraint [CAll] :: Bind [Name Type] Constraint -> Constraint cAnd :: [Constraint] -> Constraint cOr :: [Constraint] -> Constraint instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.Typecheck.Constraints.Constraint instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Typecheck.Constraints.Constraint instance GHC.Generics.Generic Disco.Typecheck.Constraints.Constraint instance GHC.Show.Show Disco.Typecheck.Constraints.Constraint instance Disco.Pretty.Pretty Disco.Typecheck.Constraints.Constraint instance GHC.Base.Semigroup Disco.Typecheck.Constraints.Constraint instance GHC.Base.Monoid Disco.Typecheck.Constraints.Constraint -- | Unification. module Disco.Typecheck.Unify -- | Given a list of equations between types, return a substitution which -- makes all the equations satisfied (or fail if it is not possible). -- -- This is not the most efficient way to implement unification but it is -- simple. unify :: TyDefCtx -> [(Type, Type)] -> Maybe S -- | Given a list of equations between types, return a substitution which -- makes all the equations equal *up to* identifying all base types. So, -- for example, Int = Nat weakly unifies but Int = (Int -> Int) does -- not. This is used to check whether subtyping constraints are -- structurally sound before doing constraint simplification/solving, to -- ensure termination. weakUnify :: TyDefCtx -> [(Type, Type)] -> Maybe S -- | Given a list of equations between types, return a substitution which -- makes all the equations satisfied (or fail if it is not possible), up -- to the given comparison on base types. unify' :: (BaseTy -> BaseTy -> Bool) -> TyDefCtx -> [(Type, Type)] -> Maybe S equate :: TyDefCtx -> [Type] -> Maybe S occurs :: Name Type -> Type -> Bool unifyAtoms :: TyDefCtx -> [Atom] -> Maybe (Substitution Atom) unifyUAtoms :: TyDefCtx -> [UAtom] -> Maybe (Substitution UAtom) -- | Names for modules and identifiers. module Disco.Names -- | Where did a module come from? data ModuleProvenance -- | From a particular directory (relative to cwd) Dir :: FilePath -> ModuleProvenance -- | From the standard library Stdlib :: ModuleProvenance -- | The name of a module. data ModuleName -- | The special top-level "module" consisting of what has been entered at -- the REPL. REPLModule :: ModuleName -- | A named module, with its name and provenance. Named :: ModuleProvenance -> String -> ModuleName -- | Where did a name come from? data NameProvenance -- | The name is locally bound LocalName :: NameProvenance -- | The name is exported by the given module QualifiedName :: ModuleName -> NameProvenance -- | A QName, or qualified name, is a Name paired with its -- NameProvenance. data QName a QName :: NameProvenance -> Name a -> QName a [qnameProvenance] :: QName a -> NameProvenance [qname] :: QName a -> Name a -- | Does this name correspond to a free variable? isFree :: QName a -> Bool -- | Create a locally bound qualified name. localName :: Name a -> QName a -- | Create a module-bound qualified name. (.-) :: ModuleName -> Name a -> QName a -- | The unbound-generics library gives us free variables for -- free. But when dealing with typed and desugared ASTs, we want all the -- free QNames instead of just Names. fvQ :: (Data t, Typeable e) => Traversal' t (QName e) substQ :: Subst b a => QName b -> b -> a -> a substsQ :: Subst b a => [(QName b, b)] -> a -> a instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.Names.ModuleProvenance instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Names.ModuleProvenance instance Data.Data.Data Disco.Names.ModuleProvenance instance GHC.Generics.Generic Disco.Names.ModuleProvenance instance GHC.Show.Show Disco.Names.ModuleProvenance instance GHC.Classes.Ord Disco.Names.ModuleProvenance instance GHC.Classes.Eq Disco.Names.ModuleProvenance instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.Names.ModuleName instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Names.ModuleName instance Data.Data.Data Disco.Names.ModuleName instance GHC.Generics.Generic Disco.Names.ModuleName instance GHC.Show.Show Disco.Names.ModuleName instance GHC.Classes.Ord Disco.Names.ModuleName instance GHC.Classes.Eq Disco.Names.ModuleName instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.Names.NameProvenance instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Names.NameProvenance instance Data.Data.Data Disco.Names.NameProvenance instance GHC.Generics.Generic Disco.Names.NameProvenance instance GHC.Show.Show Disco.Names.NameProvenance instance GHC.Classes.Ord Disco.Names.NameProvenance instance GHC.Classes.Eq Disco.Names.NameProvenance instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type (Disco.Names.QName a) instance Data.Typeable.Internal.Typeable a => Unbound.Generics.LocallyNameless.Alpha.Alpha (Disco.Names.QName a) instance Data.Data.Data a => Data.Data.Data (Disco.Names.QName a) instance GHC.Generics.Generic (Disco.Names.QName a) instance GHC.Show.Show (Disco.Names.QName a) instance GHC.Classes.Ord (Disco.Names.QName a) instance GHC.Classes.Eq (Disco.Names.QName a) instance Disco.Pretty.Pretty (Disco.Names.QName a) instance Disco.Pretty.Pretty Disco.Names.ModuleName -- | 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. module Disco.Context -- | A context maps qualified names to things. In particular a Ctx a -- b maps qualified names for as to values of type -- b. data Ctx a b -- | The empty context. emptyCtx :: Ctx a b -- | A singleton context, mapping a qualified name to a thing. singleCtx :: QName a -> b -> Ctx a b -- | Create a context from a list of (qualified name, value) pairs. fromList :: [(QName a, b)] -> Ctx a b -- | Create a context for bindings from a single module. ctxForModule :: ModuleName -> [(Name a, b)] -> Ctx a b -- | Create a context with local bindings. localCtx :: [(Name a, b)] -> Ctx a b -- | Insert a new binding into a context. The new binding shadows any old -- binding for the same qualified name. insert :: QName a -> b -> Ctx a b -> Ctx a b -- | Run a computation under a context extended with a new binding. The new -- binding shadows any old binding for the same name. extend :: Member (Reader (Ctx a b)) r => QName a -> b -> Sem r c -> Sem r c -- | Run a computation in a context extended with an additional context. -- Bindings in the additional context shadow any bindings with the same -- names in the existing context. extends :: Member (Reader (Ctx a b)) r => Ctx a b -> Sem r c -> Sem r c -- | Check if a context is empty. null :: Ctx a b -> Bool -- | Look up a qualified name in an ambient context. lookup :: Member (Reader (Ctx a b)) r => QName a -> Sem r (Maybe b) -- | Look up a qualified name in a context. lookup' :: QName a -> Ctx a b -> Maybe b -- | Look up all the non-local bindings of a name in an ambient context. lookupNonLocal :: Member (Reader (Ctx a b)) r => Name a -> Sem r [(ModuleName, b)] -- | Look up all the non-local bindings of a name in a context. lookupNonLocal' :: Name a -> Ctx a b -> [(ModuleName, b)] -- | 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)] -- | Look up all the bindings of an (unqualified) name in a context. lookupAll' :: Name a -> Ctx a b -> [(QName a, b)] -- | Return a list of the names defined by the context. names :: Ctx a b -> [Name a] -- | Return a list of all the values bound by the context. elems :: Ctx a b -> [b] -- | Return a list of the qualified name-value associations in the context. assocs :: Ctx a b -> [(QName a, b)] -- | Return a set of all qualified names in the context. keysSet :: Ctx a b -> Set (QName a) -- | Coerce the type of the qualified name keys in a context. coerceKeys :: Ctx a1 b -> Ctx a2 b -- | Restrict a context to only the keys in the given set. restrictKeys :: Ctx a b -> Set (QName a) -> Ctx a b -- | Join two contexts (left-biased, i.e. if the same qualified name -- 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 -- | Join a list of contexts (left-biased). joinCtxs :: [Ctx a b] -> Ctx a b -- | Filter a context using a predicate. filter :: (b -> Bool) -> Ctx a b -> Ctx a b instance Data.Traversable.Traversable (Disco.Context.Ctx a) instance Data.Foldable.Foldable (Disco.Context.Ctx a) instance GHC.Base.Functor (Disco.Context.Ctx a) instance GHC.Show.Show b => GHC.Show.Show (Disco.Context.Ctx a b) instance GHC.Classes.Eq b => GHC.Classes.Eq (Disco.Context.Ctx a b) instance GHC.Base.Semigroup (Disco.Context.Ctx a b) instance GHC.Base.Monoid (Disco.Context.Ctx a b) -- | Message logging framework (e.g. for errors, warnings, etc.) for disco. module Disco.Messages data MessageType Info :: MessageType Warning :: MessageType ErrMsg :: MessageType Debug :: MessageType data Message ann Message :: MessageType -> Doc ann -> Message ann [_messageType] :: Message ann -> MessageType [_message] :: Message ann -> Doc ann messageType :: forall ann_a2r44. Lens' (Message ann_a2r44) MessageType message :: forall ann_a2r44 ann_a2rcP. Lens (Message ann_a2r44) (Message ann_a2rcP) (Doc ann_a2r44) (Doc ann_a2rcP) handleMsg :: Member (Embed IO) r => (Message ann -> Bool) -> Message ann -> Sem r () printMsg :: Member (Embed IO) r => Message ann -> Sem r () msg :: Member (Output (Message ann)) r => MessageType -> Sem r (Doc ann) -> Sem r () info :: Member (Output (Message ann)) r => Sem r (Doc ann) -> Sem r () infoPretty :: (Member (Output (Message ann)) r, Pretty t) => t -> Sem r () warn :: Member (Output (Message ann)) r => Sem r (Doc ann) -> Sem r () debug :: Member (Output (Message ann)) r => Sem r (Doc ann) -> Sem r () debugPretty :: (Member (Output (Message ann)) r, Pretty t) => t -> Sem r () err :: Member (Output (Message ann)) r => Sem r (Doc ann) -> Sem r () instance GHC.Enum.Bounded Disco.Messages.MessageType instance GHC.Enum.Enum Disco.Messages.MessageType instance GHC.Classes.Ord Disco.Messages.MessageType instance GHC.Classes.Eq Disco.Messages.MessageType instance GHC.Read.Read Disco.Messages.MessageType instance GHC.Show.Show Disco.Messages.MessageType instance GHC.Show.Show (Disco.Messages.Message ann) -- | Abstract syntax trees representing the generic syntax of the Disco -- language. Concrete AST instances may use this module as a template. -- -- For more detail on the approach used here, see -- -- Najd and Peyton Jones, "Trees that Grow". Journal of Universal -- Computer Science, vol. 23 no. 1 (2017), 42-62. -- https://arxiv.org/abs/1610.04799 -- -- Essentially, we define a basic generic Term_ type, with a type -- index to indicate what kind of term it is, i.e. what phase the term -- belongs to. Each constructor has a type family used to define any -- extra data that should go in the constructor for a particular phase; -- there is also one additional constructor which can be used to store -- arbitrary additional information, again governed by a type family. -- Together with the use of pattern synonyms, the result is that it looks -- like we have a different type for each phase, each with its own set of -- constructors, but in fact all use the same underlying type. Particular -- instantiations of the generic framework here can be found in -- Disco.AST.Surface, Disco.AST.Typed, and -- Disco.AST.Desugared. module Disco.AST.Generic -- | A telescope is essentially a list, except that each item can bind -- names in the rest of the list. data Telescope b -- | 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 -- | Add a new item to the beginning of a Telescope. telCons :: Alpha b => b -> Telescope b -> Telescope b -- | 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 -- | Apply a function to every item in a telescope. mapTelescope :: (Alpha a, Alpha b) => (a -> b) -> Telescope a -> Telescope b -- | Traverse over a telescope. traverseTelescope :: (Applicative f, Alpha a, Alpha b) => (a -> f b) -> Telescope a -> f (Telescope b) -- | Convert a list to a telescope. toTelescope :: Alpha b => [b] -> Telescope b -- | Convert a telescope to a list. fromTelescope :: Alpha b => Telescope b -> [b] -- | Injections into a sum type (inl or inr) have a -- "side" (L or R). data Side L :: Side R :: Side -- | Use a Side to select one of two arguments (the first argument -- for L, and the second for R). selectSide :: Side -> a -> a -> a -- | Convert a Side to a boolean. fromSide :: Side -> Bool -- | An enumeration of the different kinds of containers in disco: lists, -- bags, and sets. data Container [ListContainer] :: Container [BagContainer] :: Container [SetContainer] :: Container -- | An ellipsis is an "omitted" part of a literal container (such as a -- list or set), of the form .. t. We don't have open-ended -- ellipses since everything is evaluated eagerly and hence containers -- must be finite. data Ellipsis t -- | Until represents an ellipsis with a given endpoint, as in -- [3 .. 20]. [Until] :: t -> Ellipsis t -- | The base generic AST representing terms in the disco language. -- e is a type index indicating the kind of term, i.e. the phase -- (for example, surface, typed, or desugared). Type families like -- X_TVar and so on use the phase index to determine what extra -- information (if any) should be stored in each constructor. For -- example, in the typed phase many constructors store an extra type, -- giving the type of the term. data Term_ e -- | A term variable. [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 -- | A (non-recursive) let expression, let x1 = t1, x2 = t2, ... in -- t. [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 -- | A boolean value. [TBool_] :: X_TBool e -> Bool -> Term_ e -- | A natural number. [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 -- | A literal unicode character, e.g. d. [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 lambda abstraction, i.e. an anonymous function (e.g. -- x, (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 -- | Function application, t1 t2. [TApp_] :: X_TApp e -> Term_ e -> Term_ e -> Term_ e -- | An n-tuple, (t1, ..., tn). [TTup_] :: X_TTup e -> [Term_ e] -> Term_ e -- | A case expression. [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 -- | 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 -- | 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 type family X_TVar e type family X_TPrim e type family X_TLet e type family X_TParens e type family X_TUnit e type family X_TBool e type family X_TNat e type family X_TRat e type family X_TChar e type family X_TString e type family X_TAbs e type family X_TApp e type family X_TTup e type family X_TCase e type family X_TChain e type family X_TTyOp e type family X_TContainer e type family X_TContainerComp e type family X_TAscr e type family X_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))) -- | A "link" is a comparison operator and a term; a single term followed -- by a sequence of links makes up a comparison chain, such as 2 < -- x < y < 10. data Link_ e -- | 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 type family X_TLink e type ForallLink (a :: * -> Constraint) e = (a (X_TLink e), a (Term_ e)) -- | A container comprehension consists of a head term and then a list of -- qualifiers. Each qualifier either binds a variable to some collection -- or consists of a boolean guard. data Qual_ e -- | A binding qualifier (i.e. x in t). [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 type family X_QBind e type family X_QGuard e type ForallQual (a :: * -> Constraint) e = (a (X_QBind e), a (X_QGuard e), a (Term_ e)) -- | A binding is a name along with its definition, and optionally its -- type. data Binding_ e Binding_ :: Maybe (Embed PolyType) -> Name (Term_ e) -> Embed (Term_ e) -> Binding_ e -- | 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) -- | Guards in case expressions. data Guard_ e -- | 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 -- | Let (let x = term) [GLet_] :: X_GLet e -> Binding_ e -> Guard_ e type family X_GBool e type family X_GPat e type family X_GLet 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)) -- | Patterns. data Pattern_ e -- | Variable pattern: matches anything and binds the variable. [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 -- | Injection pattern (inl pat or inr pat). [PInj_] :: X_PInj e -> Side -> Pattern_ e -> Pattern_ e -- | Literal natural number pattern. [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 -- | Multiplication pattern, p * t or t * p [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 -- | Negation pattern, -p [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 type family X_PVar e type family X_PWild e type family X_PAscr e type family X_PUnit e type family X_PBool e type family X_PTup e type family X_PInj e type family X_PNat e type family X_PChar e type family X_PString e type family X_PCons e type family X_PList e type family X_PAdd e type family X_PMul e type family X_PSub e type family X_PNeg e type family X_PFrac e type family X_Pattern 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)) -- | A quantifier: λ, ∀, or ∃ data Quantifier Lam :: Quantifier Ex :: Quantifier All :: Quantifier -- | A binder represents the stuff between the quantifier and the body of a -- lambda, ∀, or ∃ abstraction, as in x : N, r : F. type Binder_ e a = Bind (X_Binder e) a -- | A type family specifying what the binder in an abstraction can be. -- Should have at least variables in it, but how many variables and what -- other information is carried along may vary. type family X_Binder e -- | A property is just a term (of type Prop). type Property_ e = Term_ e instance Data.Data.Data b => Data.Data.Data (Disco.AST.Generic.Telescope b) instance Unbound.Generics.LocallyNameless.Subst.Subst t b => Unbound.Generics.LocallyNameless.Subst.Subst t (Disco.AST.Generic.Telescope b) instance Unbound.Generics.LocallyNameless.Alpha.Alpha b => Unbound.Generics.LocallyNameless.Alpha.Alpha (Disco.AST.Generic.Telescope b) instance GHC.Generics.Generic (Disco.AST.Generic.Telescope b) instance GHC.Show.Show b => GHC.Show.Show (Disco.AST.Generic.Telescope b) instance Unbound.Generics.LocallyNameless.Subst.Subst t Disco.AST.Generic.Side instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.AST.Generic.Side instance Data.Data.Data Disco.AST.Generic.Side instance GHC.Generics.Generic Disco.AST.Generic.Side instance GHC.Enum.Bounded Disco.AST.Generic.Side instance GHC.Enum.Enum Disco.AST.Generic.Side instance GHC.Classes.Ord Disco.AST.Generic.Side instance GHC.Classes.Eq Disco.AST.Generic.Side instance GHC.Show.Show Disco.AST.Generic.Side instance Unbound.Generics.LocallyNameless.Subst.Subst t Disco.AST.Generic.Container instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.AST.Generic.Container instance Data.Data.Data Disco.AST.Generic.Container instance GHC.Generics.Generic Disco.AST.Generic.Container instance GHC.Enum.Enum Disco.AST.Generic.Container instance GHC.Classes.Eq Disco.AST.Generic.Container instance GHC.Show.Show Disco.AST.Generic.Container instance Data.Data.Data t => Data.Data.Data (Disco.AST.Generic.Ellipsis t) instance Unbound.Generics.LocallyNameless.Subst.Subst a t => Unbound.Generics.LocallyNameless.Subst.Subst a (Disco.AST.Generic.Ellipsis t) instance Unbound.Generics.LocallyNameless.Alpha.Alpha t => Unbound.Generics.LocallyNameless.Alpha.Alpha (Disco.AST.Generic.Ellipsis t) instance Data.Traversable.Traversable Disco.AST.Generic.Ellipsis instance Data.Foldable.Foldable Disco.AST.Generic.Ellipsis instance GHC.Base.Functor Disco.AST.Generic.Ellipsis instance GHC.Generics.Generic (Disco.AST.Generic.Ellipsis t) instance GHC.Show.Show t => GHC.Show.Show (Disco.AST.Generic.Ellipsis t) instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.AST.Generic.Quantifier instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.AST.Generic.Quantifier instance GHC.Show.Show Disco.AST.Generic.Quantifier instance GHC.Classes.Ord Disco.AST.Generic.Quantifier instance GHC.Classes.Eq Disco.AST.Generic.Quantifier instance Data.Data.Data Disco.AST.Generic.Quantifier instance GHC.Generics.Generic Disco.AST.Generic.Quantifier instance GHC.Generics.Generic (Disco.AST.Generic.Link_ e) instance GHC.Generics.Generic (Disco.AST.Generic.Qual_ e) instance GHC.Generics.Generic (Disco.AST.Generic.Binding_ e) instance GHC.Generics.Generic (Disco.AST.Generic.Pattern_ e) instance GHC.Generics.Generic (Disco.AST.Generic.Guard_ e) instance GHC.Generics.Generic (Disco.AST.Generic.Term_ e) instance Disco.AST.Generic.ForallTerm GHC.Show.Show e => GHC.Show.Show (Disco.AST.Generic.Term_ e) instance (Data.Data.Data e, Data.Typeable.Internal.Typeable e, Disco.AST.Generic.ForallTerm Data.Data.Data e) => Data.Data.Data (Disco.AST.Generic.Term_ e) instance Disco.AST.Generic.ForallLink GHC.Show.Show e => GHC.Show.Show (Disco.AST.Generic.Link_ e) instance (Data.Typeable.Internal.Typeable e, Data.Data.Data e, Disco.AST.Generic.ForallLink Data.Data.Data e) => Data.Data.Data (Disco.AST.Generic.Link_ e) instance Disco.AST.Generic.ForallQual GHC.Show.Show e => GHC.Show.Show (Disco.AST.Generic.Qual_ e) instance (Data.Typeable.Internal.Typeable e, Data.Data.Data e, Disco.AST.Generic.ForallQual Data.Data.Data e) => Data.Data.Data (Disco.AST.Generic.Qual_ e) instance Disco.AST.Generic.ForallTerm GHC.Show.Show e => GHC.Show.Show (Disco.AST.Generic.Binding_ e) instance (Data.Typeable.Internal.Typeable e, Data.Data.Data e, Disco.AST.Generic.ForallTerm Data.Data.Data e) => Data.Data.Data (Disco.AST.Generic.Binding_ e) instance Disco.AST.Generic.ForallGuard GHC.Show.Show e => GHC.Show.Show (Disco.AST.Generic.Guard_ e) instance (Data.Typeable.Internal.Typeable e, Data.Data.Data e, Disco.AST.Generic.ForallGuard Data.Data.Data e) => Data.Data.Data (Disco.AST.Generic.Guard_ e) instance Disco.AST.Generic.ForallPattern GHC.Show.Show e => GHC.Show.Show (Disco.AST.Generic.Pattern_ e) instance (Data.Typeable.Internal.Typeable e, Data.Data.Data e, Disco.AST.Generic.ForallPattern Data.Data.Data e) => Data.Data.Data (Disco.AST.Generic.Pattern_ e) instance (Data.Typeable.Internal.Typeable e, Disco.AST.Generic.ForallTerm (Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type) e, Disco.AST.Generic.ForallTerm Unbound.Generics.LocallyNameless.Alpha.Alpha e) => Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type (Disco.AST.Generic.Term_ e) instance (Data.Typeable.Internal.Typeable e, Disco.AST.Generic.ForallTerm Unbound.Generics.LocallyNameless.Alpha.Alpha e) => Unbound.Generics.LocallyNameless.Alpha.Alpha (Disco.AST.Generic.Term_ e) instance (Data.Data.Data e, Disco.AST.Generic.ForallTerm Data.Data.Data e) => Control.Lens.Plated.Plated (Disco.AST.Generic.Term_ e) instance Disco.AST.Generic.ForallLink (Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type) e => Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type (Disco.AST.Generic.Link_ e) instance (Data.Typeable.Internal.Typeable e, GHC.Show.Show (Disco.AST.Generic.Link_ e), Disco.AST.Generic.ForallLink Unbound.Generics.LocallyNameless.Alpha.Alpha e) => Unbound.Generics.LocallyNameless.Alpha.Alpha (Disco.AST.Generic.Link_ e) instance Disco.AST.Generic.ForallQual (Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type) e => Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type (Disco.AST.Generic.Qual_ e) instance (Data.Typeable.Internal.Typeable e, Disco.AST.Generic.ForallQual Unbound.Generics.LocallyNameless.Alpha.Alpha e) => Unbound.Generics.LocallyNameless.Alpha.Alpha (Disco.AST.Generic.Qual_ e) instance Disco.AST.Generic.ForallGuard (Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type) e => Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type (Disco.AST.Generic.Guard_ e) instance (Data.Typeable.Internal.Typeable e, GHC.Show.Show (Disco.AST.Generic.Guard_ e), Disco.AST.Generic.ForallGuard Unbound.Generics.LocallyNameless.Alpha.Alpha e) => Unbound.Generics.LocallyNameless.Alpha.Alpha (Disco.AST.Generic.Guard_ e) instance Disco.AST.Generic.ForallPattern (Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type) e => Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type (Disco.AST.Generic.Pattern_ e) instance (Data.Typeable.Internal.Typeable e, GHC.Show.Show (Disco.AST.Generic.Pattern_ e), Disco.AST.Generic.ForallPattern Unbound.Generics.LocallyNameless.Alpha.Alpha e) => Unbound.Generics.LocallyNameless.Alpha.Alpha (Disco.AST.Generic.Pattern_ e) instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type (Disco.AST.Generic.Term_ e) => Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type (Disco.AST.Generic.Binding_ e) instance (Data.Typeable.Internal.Typeable e, GHC.Show.Show (Disco.AST.Generic.Binding_ e), Unbound.Generics.LocallyNameless.Alpha.Alpha (Disco.AST.Generic.Term_ e)) => Unbound.Generics.LocallyNameless.Alpha.Alpha (Disco.AST.Generic.Binding_ e) instance Disco.Pretty.Pretty Disco.AST.Generic.Side instance Unbound.Generics.LocallyNameless.Alpha.Alpha GHC.Base.Void -- | Typed abstract syntax trees representing the typechecked, desugared -- Disco language. module Disco.AST.Desugared -- | 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 pattern DTVar :: Type -> QName DTerm -> DTerm pattern DTPrim :: Type -> Prim -> DTerm pattern DTUnit :: DTerm pattern DTBool :: Type -> Bool -> DTerm pattern DTChar :: Char -> DTerm pattern DTNat :: Type -> Integer -> DTerm pattern DTRat :: Rational -> DTerm pattern DTAbs :: Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm pattern DTApp :: Type -> DTerm -> DTerm -> DTerm pattern DTPair :: Type -> DTerm -> DTerm -> DTerm pattern DTCase :: Type -> [DBranch] -> DTerm pattern DTTyOp :: Type -> TyOp -> Type -> DTerm pattern DTNil :: Type -> DTerm -- | A test frame, recording a collection of variables with their types and -- their original user-facing names. Used for legible reporting of test -- failures inside the enclosed term. pattern DTTest :: [(String, Type, Name DTerm)] -> DTerm -> DTerm -- | An enumeration of the different kinds of containers in disco: lists, -- bags, and sets. data Container [ListContainer] :: Container [BagContainer] :: Container [SetContainer] :: Container type DBinding = Binding_ DS pattern DBinding :: Maybe (Embed PolyType) -> Name DTerm -> Embed DTerm -> DBinding type DBranch = Bind (Telescope DGuard) DTerm type DGuard = Guard_ DS pattern DGPat :: Embed DTerm -> DPattern -> DGuard type DPattern = Pattern_ DS pattern DPVar :: Type -> Name DTerm -> DPattern pattern DPWild :: Type -> DPattern pattern DPUnit :: DPattern pattern DPPair :: Type -> Name DTerm -> Name DTerm -> DPattern pattern DPInj :: Type -> Side -> Name DTerm -> DPattern type DProperty = Property_ DS instance GHC.Generics.Generic Disco.AST.Desugared.X_DTerm instance GHC.Show.Show Disco.AST.Desugared.X_DTerm instance Disco.Types.HasType Disco.AST.Desugared.DPattern instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.AST.Desugared.X_DTerm instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.AST.Desugared.X_DTerm instance Disco.Types.HasType Disco.AST.Desugared.DTerm -- | Abstract syntax trees representing the surface syntax of the Disco -- language. module Disco.AST.Surface -- | A module contains all the information from one disco source file. data Module Module :: Set Ext -> [String] -> [Decl] -> [(Name Term, Docs)] -> [Term] -> Module -- | Enabled extensions [modExts] :: Module -> Set Ext -- | Module imports [modImports] :: Module -> [String] -- | Declarations [modDecls] :: Module -> [Decl] -- | Documentation [modDocs] :: Module -> [(Name Term, Docs)] -- | Top-level (bare) terms [modTerms] :: Module -> [Term] emptyModule :: Module -- | A TopLevel is either documentation (a DocThing) or a -- declaration (Decl). data TopLevel TLDoc :: DocThing -> TopLevel TLDecl :: Decl -> TopLevel TLExpr :: Term -> TopLevel -- | Convenient synonym for a list of DocThings. type Docs = [DocThing] -- | An item of documentation. data DocThing -- | A documentation string, i.e. a block of ||| text items DocString :: [String] -> DocThing -- | An exampledoctestproperty of the form !!! forall (x1:ty1) -- ... . property DocProperty :: Property -> DocThing -- | A property is a universally quantified term of the form forall v1 -- : T1, v2 : T2. term. type Property = Property_ UD -- | A type declaration, name : type. data TypeDecl TypeDecl :: Name Term -> PolyType -> TypeDecl -- | A group of definition clauses of the form name pat1 .. patn = -- term. The patterns bind variables in the term. For example, f -- n (x,y) = n*x + y. data TermDefn TermDefn :: Name Term -> NonEmpty (Bind [Pattern] Term) -> TermDefn -- | A user-defined type (potentially recursive). -- -- @type T arg1 arg2 ... = body data TypeDefn TypeDefn :: String -> [String] -> Type -> TypeDefn -- | A declaration is either a type declaration, a term definition, or a -- type definition. data Decl [DType] :: TypeDecl -> Decl [DDefn] :: TermDefn -> Decl [DTyDef] :: TypeDefn -> Decl partitionDecls :: [Decl] -> ([TypeDecl], [TermDefn], [TypeDefn]) -- | Pretty-print a type declaration. prettyTyDecl :: Members '[Reader PA, LFresh] r => Name t -> Type -> Sem r (Doc ann) -- | The extension descriptor for Surface specific AST types. data UD type Term = Term_ UD pattern TVar :: Name Term -> Term pattern TPrim :: Prim -> Term pattern TUn :: UOp -> Term -> Term pattern TBin :: BOp -> Term -> Term -> Term pattern TLet :: Bind (Telescope Binding) Term -> Term pattern TParens :: Term -> Term pattern TUnit :: Term pattern TBool :: Bool -> Term pattern TChar :: Char -> Term pattern TString :: String -> Term pattern TNat :: Integer -> Term pattern TRat :: Rational -> Term pattern TAbs :: Quantifier -> Bind [Pattern] Term -> Term pattern TApp :: Term -> Term -> Term pattern TTup :: [Term] -> Term pattern TCase :: [Branch] -> Term pattern TChain :: Term -> [Link] -> Term pattern TTyOp :: TyOp -> Type -> Term pattern TContainerComp :: Container -> Bind (Telescope Qual) Term -> Term pattern TContainer :: Container -> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> Term pattern TAscr :: Term -> PolyType -> Term pattern TWild :: Term pattern TList :: [Term] -> Maybe (Ellipsis Term) -> Term pattern TListComp :: Bind (Telescope Qual) Term -> Term -- | A quantifier: λ, ∀, or ∃ data Quantifier Lam :: Quantifier Ex :: Quantifier All :: Quantifier -- | A telescope is essentially a list, except that each item can bind -- names in the rest of the list. data Telescope b -- | 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 -- | 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 -- | Apply a function to every item in a telescope. mapTelescope :: (Alpha a, Alpha b) => (a -> b) -> Telescope a -> Telescope b -- | Convert a list to a telescope. toTelescope :: Alpha b => [b] -> Telescope b -- | Convert a telescope to a list. fromTelescope :: Alpha b => Telescope b -> [b] -- | Injections into a sum type (inl or inr) have a -- "side" (L or R). data Side L :: Side R :: Side type Link = Link_ UD pattern TLink :: BOp -> Term -> Link type Binding = Binding_ UD type Qual = Qual_ UD pattern QBind :: Name Term -> Embed Term -> Qual pattern QGuard :: Embed Term -> Qual -- | An enumeration of the different kinds of containers in disco: lists, -- bags, and sets. data Container [ListContainer] :: Container [BagContainer] :: Container [SetContainer] :: Container -- | An ellipsis is an "omitted" part of a literal container (such as a -- list or set), of the form .. t. We don't have open-ended -- ellipses since everything is evaluated eagerly and hence containers -- must be finite. data Ellipsis t -- | Until represents an ellipsis with a given endpoint, as in -- [3 .. 20]. [Until] :: t -> Ellipsis t type Branch = Branch_ UD type Guard = Guard_ UD pattern GBool :: Embed Term -> Guard pattern GPat :: Embed Term -> Pattern -> Guard pattern GLet :: Binding -> Guard type Pattern = Pattern_ UD pattern PVar :: Name Term -> Pattern pattern PWild :: Pattern pattern PAscr :: Pattern -> Type -> Pattern pattern PUnit :: Pattern pattern PBool :: Bool -> Pattern pattern PChar :: Char -> Pattern pattern PString :: String -> Pattern pattern PTup :: [Pattern] -> Pattern pattern PInj :: Side -> Pattern -> Pattern pattern PNat :: Integer -> Pattern pattern PCons :: Pattern -> Pattern -> Pattern pattern PList :: [Pattern] -> Pattern pattern PAdd :: Side -> Pattern -> Term -> Pattern pattern PMul :: Side -> Pattern -> Term -> Pattern pattern PSub :: Pattern -> Term -> Pattern pattern PNeg :: Pattern -> Pattern pattern PFrac :: Pattern -> Pattern -> Pattern pattern PNonlinear :: Pattern -> Name Term -> Pattern pattern Binding :: Maybe (Embed PolyType) -> Name Term -> Embed Term -> Binding -- | Pretty-print a pattern with guaranteed parentheses. prettyPatternP :: Members '[LFresh, Reader PA] r => Pattern -> Sem r (Doc ann) instance GHC.Show.Show Disco.AST.Surface.TypeDefn instance Disco.AST.Generic.ForallTerm GHC.Show.Show Disco.AST.Surface.UD => GHC.Show.Show Disco.AST.Surface.Module instance Disco.AST.Generic.ForallTerm GHC.Show.Show Disco.AST.Surface.UD => GHC.Show.Show Disco.AST.Surface.TopLevel instance Disco.AST.Generic.ForallTerm GHC.Show.Show Disco.AST.Surface.UD => GHC.Show.Show Disco.AST.Surface.DocThing instance Disco.AST.Generic.ForallTerm GHC.Show.Show Disco.AST.Surface.UD => GHC.Show.Show Disco.AST.Surface.TypeDecl instance Disco.AST.Generic.ForallTerm GHC.Show.Show Disco.AST.Surface.UD => GHC.Show.Show Disco.AST.Surface.TermDefn instance Disco.AST.Generic.ForallTerm GHC.Show.Show Disco.AST.Surface.UD => GHC.Show.Show Disco.AST.Surface.Decl instance Disco.Pretty.Pretty Disco.AST.Surface.Decl instance Disco.Pretty.Pretty (Unbound.Generics.LocallyNameless.Name.Name a, Unbound.Generics.LocallyNameless.Bind.Bind [Disco.AST.Surface.Pattern] Disco.AST.Surface.Term) instance Disco.Pretty.Pretty Disco.AST.Surface.Pattern instance Disco.Pretty.Pretty (Disco.AST.Generic.Telescope Disco.AST.Surface.Guard) instance Disco.Pretty.Pretty Disco.AST.Surface.Guard instance Disco.Pretty.Pretty Disco.AST.Surface.Branch instance Disco.Pretty.Pretty Disco.AST.Surface.Binding instance Disco.Pretty.Pretty (Disco.AST.Generic.Telescope Disco.AST.Surface.Qual) instance Disco.Pretty.Pretty Disco.AST.Surface.Qual instance Disco.Pretty.Pretty Disco.AST.Surface.Term -- | 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 -- | 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 pattern ATVar :: Type -> QName ATerm -> ATerm pattern ATPrim :: Type -> Prim -> ATerm pattern ATLet :: Type -> Bind (Telescope ABinding) ATerm -> ATerm pattern ATUnit :: ATerm pattern ATBool :: Type -> Bool -> ATerm pattern ATNat :: Type -> Integer -> ATerm pattern ATRat :: Rational -> ATerm pattern ATChar :: Char -> ATerm pattern ATString :: String -> ATerm pattern ATAbs :: Quantifier -> Type -> Bind [APattern] ATerm -> ATerm pattern ATApp :: Type -> ATerm -> ATerm -> ATerm pattern ATTup :: Type -> [ATerm] -> ATerm pattern ATCase :: Type -> [ABranch] -> ATerm pattern ATChain :: Type -> ATerm -> [ALink] -> ATerm pattern ATTyOp :: Type -> TyOp -> Type -> ATerm pattern ATContainer :: Type -> Container -> [(ATerm, Maybe ATerm)] -> Maybe (Ellipsis ATerm) -> ATerm pattern ATContainerComp :: Type -> Container -> Bind (Telescope AQual) ATerm -> ATerm pattern ATList :: Type -> [ATerm] -> Maybe (Ellipsis ATerm) -> ATerm pattern ATListComp :: Type -> Bind (Telescope AQual) ATerm -> ATerm pattern ATTest :: [(String, Type, Name ATerm)] -> ATerm -> ATerm type ALink = Link_ TY pattern ATLink :: BOp -> ATerm -> ALink -- | An enumeration of the different kinds of containers in disco: lists, -- bags, and sets. data Container [ListContainer] :: Container [BagContainer] :: Container [SetContainer] :: Container type ABinding = Binding_ TY type ABranch = Bind (Telescope AGuard) ATerm type AGuard = Guard_ TY pattern AGBool :: Embed ATerm -> AGuard pattern AGPat :: Embed ATerm -> APattern -> AGuard pattern AGLet :: ABinding -> AGuard type AQual = Qual_ TY pattern AQBind :: Name ATerm -> Embed ATerm -> AQual pattern AQGuard :: Embed ATerm -> AQual type APattern = Pattern_ TY pattern APVar :: Type -> Name ATerm -> APattern pattern APWild :: Type -> APattern pattern APUnit :: APattern pattern APBool :: Bool -> APattern pattern APTup :: Type -> [APattern] -> APattern pattern APInj :: Type -> Side -> APattern -> APattern pattern APNat :: Type -> Integer -> APattern pattern APChar :: Char -> APattern pattern APString :: String -> APattern pattern APCons :: Type -> APattern -> APattern -> APattern pattern APList :: Type -> [APattern] -> APattern pattern APAdd :: Type -> Side -> APattern -> ATerm -> APattern pattern APMul :: Type -> Side -> APattern -> ATerm -> APattern pattern APSub :: Type -> APattern -> ATerm -> APattern pattern APNeg :: Type -> APattern -> APattern pattern APFrac :: Type -> APattern -> APattern -> APattern pattern ABinding :: Maybe (Embed PolyType) -> Name ATerm -> Embed ATerm -> ABinding varsBound :: APattern -> [(Name ATerm, Type)] -- | Get the type of a thing. getType :: HasType t => t -> Type -- | Set the type of a thing, when that is possible; the default -- implementation is for setType to do nothing. setType :: HasType t => Type -> t -> t substQT :: QName ATerm -> ATerm -> ATerm -> ATerm type AProperty = Property_ TY instance Data.Data.Data Disco.AST.Typed.TY instance Disco.Types.HasType Disco.AST.Typed.APattern instance Disco.Types.HasType Disco.AST.Typed.ABranch instance Disco.Types.HasType Disco.AST.Typed.ATerm instance Disco.Pretty.Pretty Disco.AST.Typed.ATerm -- | Typecheck the Disco surface language and transform it into a -- type-annotated AST. module Disco.Typecheck.Erase -- | Erase all the type annotations from a term. erase :: ATerm -> Term eraseBinding :: ABinding -> Binding erasePattern :: APattern -> Pattern eraseBranch :: ABranch -> Branch eraseGuard :: AGuard -> Guard eraseLink :: ALink -> Link eraseQual :: AQual -> Qual eraseProperty :: AProperty -> Property eraseDTerm :: DTerm -> Term eraseDBranch :: DBranch -> Branch eraseDGuard :: DGuard -> Guard eraseDPattern :: DPattern -> Pattern -- | Abstract syntax trees representing the desugared, untyped core -- language for Disco. module Disco.AST.Core data ShouldMemo Memo :: ShouldMemo NoMemo :: ShouldMemo -- | AST for the desugared, untyped core language. data Core -- | A variable. [CVar] :: QName Core -> Core -- | A rational number. [CNum] :: Rational -> Core -- | A built-in constant. [CConst] :: Op -> Core -- | An injection into a sum type, i.e. a value together with a tag -- indicating which element of a sum type we are in. For example, false -- is represented by CSum L CUnit; right(v) is -- represented by CSum R v. Note we do not need to remember -- which type the constructor came from; if the program typechecked then -- we will never end up comparing constructors from different types. [CInj] :: Side -> Core -> Core -- | A primitive case expression on a value of a sum type. [CCase] :: Core -> Bind (Name Core) Core -> Bind (Name Core) Core -> Core -- | The unit value. [CUnit] :: Core -- | A pair of values. [CPair] :: Core -> Core -> Core -- | A projection from a product type, i.e. fst or snd. [CProj] :: Side -> Core -> Core -- | An anonymous function. [CAbs] :: ShouldMemo -> Bind [Name Core] Core -> Core -- | Function application. [CApp] :: Core -> Core -> Core -- | A "test frame" under which a test case is run. Records the types and -- legible names of the variables that should be reported to the user if -- the test fails. [CTest] :: [(String, Type, Name Core)] -> Core -> Core -- | A type. [CType] :: Type -> Core -- | Introduction form for a lazily evaluated value of type Lazy T for some -- type T. We can have multiple bindings to multiple terms to create a -- simple target for compiling mutual recursion. [CDelay] :: Bind [Name Core] [Core] -> Core -- | Force evaluation of a lazy value. [CForce] :: Core -> Core -- | Operators that can show up in the core language. Note that not all -- surface language operators show up here, since some are desugared into -- combinators of the operators here. data Op -- | Addition (+) OAdd :: Op -- | Arithmetic negation (-) ONeg :: Op -- | Integer square root (sqrt) OSqrt :: Op -- | Floor of fractional type (floor) OFloor :: Op -- | Ceiling of fractional type (ceiling) OCeil :: Op -- | Absolute value (abs) OAbs :: Op -- | Multiplication (*) OMul :: Op -- | Division (/) ODiv :: Op -- | Exponentiation (^) OExp :: Op -- | Modulo (mod) OMod :: Op -- | Divisibility test (|) ODivides :: Op -- | Multinomial coefficient (choose) OMultinom :: Op -- | Factorial (!) OFact :: Op -- | Equality test (==) OEq :: Op -- | Less than (<) OLt :: Op -- | Enumerate the values of a type. OEnum :: Op -- | Count the values of a type. OCount :: Op -- | Power setbag of a given setbag (power). OPower :: Op -- | Set/bag element test. OBagElem :: Op -- | List element test. OListElem :: Op -- | Map a function over a bag. Carries the output type of the function. OEachBag :: Op -- | Map a function over a set. Carries the output type of the function. OEachSet :: Op -- | Filter a bag. OFilterBag :: Op -- | Merge two bags/sets. OMerge :: Op -- | Bag join, i.e. union a bag of bags. OBagUnions :: Op -- | Adjacency List of given graph OSummary :: Op -- | Empty graph OEmptyGraph :: Op -- | Construct a vertex with given value OVertex :: Op -- | Graph overlay OOverlay :: Op -- | Graph connect OConnect :: Op -- | Map insert OInsert :: Op -- | Map lookup OLookup :: Op -- | Continue until end, [x, y, z .. e] OUntil :: Op -- | set -> list conversion (sorted order). OSetToList :: Op -- | bag -> set conversion (forget duplicates). OBagToSet :: Op -- | bag -> list conversion (sorted order). OBagToList :: Op -- | list -> set conversion (forget order, duplicates). OListToSet :: Op -- | list -> bag conversion (forget order). OListToBag :: Op -- | bag -> set of counts OBagToCounts :: Op -- | set of counts -> bag OCountsToBag :: Op -- | unsafe set of counts -> bag, assumes all are distinct OUnsafeCountsToBag :: Op -- | Map k v -> Set (k × v) OMapToSet :: Op -- | Set (k × v) -> Map k v OSetToMap :: Op -- | Primality test OIsPrime :: Op -- | Factorization OFactor :: Op -- | Turn a rational into a (num, denom) pair OFrac :: Op -- | Universal quantification. Applied to a closure t1, ..., tn -> -- Prop it yields a Prop. OForall :: [Type] -> Op -- | Existential quantification. Applied to a closure t1, ..., tn -> -- Prop it yields a Prop. OExists :: [Type] -> Op -- | Convert Prop -> Bool via exhaustive search. OHolds :: Op -- | Flip success and failure for a prop. ONotProp :: Op -- | Comparison assertion OShould :: BOp -> Type -> Op -- | Error for non-exhaustive pattern match OMatchErr :: Op -- | Crash with a user-supplied message OCrash :: Op -- | No-op/identity function OId :: Op -- | Lookup OEIS sequence OLookupSeq :: Op -- | Extend a List via OEIS OExtendSeq :: Op -- | Not the Boolean And, but instead a propositional BOp | Should -- only be seen and used with Props. OAnd :: Op -- | Not the Boolean Or, but instead a propositional BOp | Should -- only be seen and used with Props. OOr :: Op -- | Not the Boolean Impl, but instead a propositional BOp | Should -- only be seen and used with Props. OImpl :: Op OSeed :: Op ORandom :: Op -- | Get the arity (desired number of arguments) of a function constant. A -- few constants have arity 0; everything else is uncurried and hence has -- arity 1. opArity :: Op -> Int substQC :: QName Core -> Core -> Core -> Core substsQC :: [(QName Core, Core)] -> Core -> Core instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.AST.Core.ShouldMemo instance Data.Data.Data Disco.AST.Core.ShouldMemo instance GHC.Generics.Generic Disco.AST.Core.ShouldMemo instance GHC.Show.Show Disco.AST.Core.ShouldMemo instance GHC.Classes.Ord Disco.AST.Core.Op instance GHC.Classes.Eq Disco.AST.Core.Op instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.AST.Core.Op instance Data.Data.Data Disco.AST.Core.Op instance GHC.Generics.Generic Disco.AST.Core.Op instance GHC.Show.Show Disco.AST.Core.Op instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.AST.Core.Core instance Data.Data.Data Disco.AST.Core.Core instance GHC.Generics.Generic Disco.AST.Core.Core instance GHC.Show.Show Disco.AST.Core.Core instance Control.Lens.Plated.Plated Disco.AST.Core.Core instance Disco.Pretty.Pretty Disco.AST.Core.Core instance Disco.Pretty.Pretty Disco.AST.Core.Op -- | Polysemy effect for fresh name generation, compatible with the -- unbound-generics library. module Disco.Effects.Fresh -- | 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 [Fresh] :: Name x -> Fresh m (Name x) fresh :: forall r_a4KCF x_X0. Member Fresh r_a4KCF => Name x_X0 -> Sem r_a4KCF (Name x_X0) -- | Dispatch the fresh name generation effect, starting at a given -- integer. runFresh' :: Integer -> Sem (Fresh ': r) a -> Sem r a -- | Run a computation requiring fresh name generation, beginning with 0 -- for the initial freshly generated name. runFresh :: Sem (Fresh ': r) a -> Sem r a -- | Run a computation requiring fresh name generation, beginning with 1 -- instead of 0 for the initial freshly generated name. runFresh1 :: Sem (Fresh ': r) a -> Sem r a -- | Open a binder, automatically creating fresh names for the bound -- variables. unbind :: (Member Fresh r, Alpha p, Alpha t) => Bind p t -> Sem r (p, t) -- | Generate a fresh (local, free) qualified name based on a given string. freshQ :: Member Fresh r => String -> Sem r (QName a) -- | Run a Sem computation requiring a Fresh constraint (from -- the unbound-generics library) in terms of an available -- Fresh effect. absorbFresh :: Member Fresh r => (Fresh (Sem r) => Sem r a) -> Sem r a newtype FreshDict m FreshDict :: (forall x. Name x -> m (Name x)) -> FreshDict m [fresh_] :: FreshDict m -> 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 must be coherent, that is there cannot be orphans. newtype Action m s' a Action :: m a -> Action m s' a instance forall (m :: * -> *) k (s' :: k). GHC.Base.Monad m => GHC.Base.Monad (Disco.Effects.Fresh.Action m s') instance forall (m :: * -> *) k (s' :: k). GHC.Base.Applicative m => GHC.Base.Applicative (Disco.Effects.Fresh.Action m s') instance forall (m :: * -> *) k (s' :: k). GHC.Base.Functor m => GHC.Base.Functor (Disco.Effects.Fresh.Action m s') instance forall k (m :: * -> *) (s' :: k). (GHC.Base.Monad m, Data.Reflection.Reifies s' (Disco.Effects.Fresh.FreshDict m)) => Unbound.Generics.LocallyNameless.Fresh.Fresh (Disco.Effects.Fresh.Action m s') -- | Constraint solver for the constraints generated during type -- checking/inference. module Disco.Typecheck.Solve -- | Type of errors which can be generated by the constraint solving -- process. data SolveError [NoWeakUnifier] :: SolveError [NoUnify] :: SolveError [UnqualBase] :: Qualifier -> BaseTy -> SolveError [Unqual] :: Qualifier -> Type -> SolveError [QualSkolem] :: Qualifier -> Name Type -> SolveError runSolve :: SolutionLimit -> Sem (State SolutionLimit ': (Fresh ': (Error SolveError ': r))) a -> Sem r (Either SolveError a) -- | Run a list of actions, and return the results from those which do not -- throw an error. If all of them throw an error, rethrow the first one. filterErrors :: Member (Error e) r => NonEmpty (Sem r a) -> Sem r (NonEmpty a) -- | Max number of solutions to generate. newtype SolutionLimit SolutionLimit :: Int -> SolutionLimit [getSolutionLimit] :: SolutionLimit -> Int -- | Register the fact that we found one solution, by decrementing the -- solution limit. countSolution :: Member (State SolutionLimit) r => Sem r () -- | Run a subcomputation conditional on the solution limit still being -- positive. If the solution limit has reached zero, stop early. withSolutionLimit :: (Member (State SolutionLimit) r, Member (Output (Message ann)) r, Monoid a) => Sem r a -> Sem r a data SimpleConstraint [:<:] :: Type -> Type -> SimpleConstraint [:=:] :: Type -> Type -> SimpleConstraint -- | Information about a particular type variable. More information may be -- added in the future (e.g. polarity). data TyVarInfo TVI :: First Ilk -> Sort -> TyVarInfo -- | The ilk (unification or skolem) of the variable, if known [_tyVarIlk] :: TyVarInfo -> First Ilk -- | The sort (set of qualifiers) of the type variable. [_tyVarSort] :: TyVarInfo -> Sort tyVarSort :: Lens' TyVarInfo Sort tyVarIlk :: Lens' TyVarInfo (First Ilk) -- | Create a TyVarInfo given an Ilk and a Sort. mkTVI :: Ilk -> Sort -> TyVarInfo -- | A TyVarInfoMap records what we know about each type variable; -- it is a mapping from type variable names to TyVarInfo records. newtype TyVarInfoMap VM :: Map (Name Type) TyVarInfo -> TyVarInfoMap [unVM] :: TyVarInfoMap -> Map (Name Type) TyVarInfo -- | Utility function for acting on a TyVarInfoMap by acting on the -- underlying Map. onVM :: (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo) -> TyVarInfoMap -> TyVarInfoMap -- | Look up a given variable name in a TyVarInfoMap. lookupVM :: Name Type -> TyVarInfoMap -> Maybe TyVarInfo -- | Remove the mapping for a particular variable name (if it exists) from -- a TyVarInfoMap. deleteVM :: Name Type -> TyVarInfoMap -> TyVarInfoMap -- | Given a list of type variable names, add them all to the -- TyVarInfoMap as Skolem variables (with a trivial sort). addSkolems :: [Name Type] -> TyVarInfoMap -> TyVarInfoMap -- | Get the sort of a particular variable recorded in a -- TyVarInfoMap. Returns the trivial (empty) sort for a variable -- not in the map. getSort :: TyVarInfoMap -> Name Type -> Sort -- | Get the Ilk of a variable recorded in a TyVarInfoMap. -- Returns Nothing if the variable is not in the map, or if its -- ilk is not known. getIlk :: TyVarInfoMap -> Name Type -> Maybe Ilk -- | Extend the sort of a type variable by combining its existing sort with -- the given one. Has no effect if the variable is not already in the -- map. extendSort :: Name Type -> Sort -> TyVarInfoMap -> TyVarInfoMap data SimplifyState SS :: TyVarInfoMap -> [SimpleConstraint] -> S -> Set SimpleConstraint -> SimplifyState [_ssVarMap] :: SimplifyState -> TyVarInfoMap [_ssConstraints] :: SimplifyState -> [SimpleConstraint] [_ssSubst] :: SimplifyState -> S [_ssSeen] :: SimplifyState -> Set SimpleConstraint ssVarMap :: Lens' SimplifyState TyVarInfoMap ssSubst :: Lens' SimplifyState S ssSeen :: Lens' SimplifyState (Set SimpleConstraint) ssConstraints :: Lens' SimplifyState [SimpleConstraint] lkup :: (Ord k, Show k, Show (Map k a)) => String -> Map k a -> k -> a solveConstraint :: Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx, State SolutionLimit] r => Constraint -> Sem r (NonEmpty S) solveConstraintChoice :: Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx, State SolutionLimit] r => TyVarInfoMap -> [SimpleConstraint] -> Sem r (NonEmpty S) decomposeConstraint :: Members '[Fresh, Error SolveError, Input TyDefCtx] r => Constraint -> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint])) decomposeQual :: Members '[Fresh, Error SolveError, Input TyDefCtx] r => Type -> Qualifier -> Sem r TyVarInfoMap checkQual :: Members '[Fresh, Error SolveError] r => Qualifier -> Atom -> Sem r TyVarInfoMap -- | This step does unification of equality constraints, as well as -- structural decomposition of subtyping constraints. For example, if we -- have a constraint (x -> y) (z - Int), then we can decompose -- it into two constraints, (z <: x) and (y <: Int); if we have a -- constraint v <: (a,b), then we substitute v ↦ (x,y) (where x and y -- are fresh type variables) and continue; and so on. -- -- After this step, the remaining constraints will all be atomic -- constraints, that is, only of the form (v1 <: v2), (v <: b), or -- (b <: v), where v is a type variable and b is a base type. simplify :: Members '[Error SolveError, Output (Message ann), Input TyDefCtx] r => TyVarInfoMap -> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S) -- | Given a list of atoms and atomic subtype constraints (each pair -- (a1,a2) corresponds to the constraint a1 <: a2) -- build the corresponding constraint graph. mkConstraintGraph :: (Show a, Ord a) => Set a -> [(a, a)] -> Graph a -- | Check for any weakly connected components containing more than one -- skolem, or a skolem and a base type, or a skolem and any variables -- with nontrivial sorts; such components are not allowed. If there are -- any WCCs with a single skolem, no base types, and only unsorted -- variables, just unify them all with the skolem and remove those -- components. checkSkolems :: Members '[Error SolveError, Output (Message ann), Input TyDefCtx] r => TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S) -- | Eliminate cycles in the constraint set by collapsing each strongly -- connected component to a single node, (unifying all the types in the -- SCC). A strongly connected component is a maximal set of nodes where -- every node is reachable from every other by a directed path; since we -- are using directed edges to indicate a subtyping constraint, this -- means every node must be a subtype of every other, and the only way -- this can happen is if all are in fact equal. -- -- Of course, this step can fail if the types in a SCC are not unifiable. -- If it succeeds, it returns the collapsed graph (which is now -- guaranteed to be acyclic, i.e. a DAG) and a substitution. elimCycles :: Members '[Error SolveError] r => TyDefCtx -> Graph UAtom -> Sem r (Graph UAtom, S) elimCyclesGen :: forall a b r. (Subst a a, Ord a, Members '[Error SolveError] r) => (Substitution a -> Substitution b) -> ([a] -> Maybe (Substitution a)) -> Graph a -> Sem r (Graph a, Substitution b) isBaseEdge :: (UAtom, UAtom) -> Either (BaseTy, BaseTy) (UAtom, UAtom) checkBaseEdge :: Members '[Error SolveError] r => (BaseTy, BaseTy) -> Sem r () checkBaseEdges :: Members '[Error SolveError] r => Graph UAtom -> Sem r (Graph UAtom) -- | Rels stores the set of base types and variables related to a given -- variable in the constraint graph (either predecessors or successors, -- but not both). data Rels Rels :: Set BaseTy -> Set (Name Type) -> Rels [baseRels] :: Rels -> Set BaseTy [varRels] :: Rels -> Set (Name Type) -- | A RelMap associates each variable to its sets of base type and -- variable predecessors and successors in the constraint graph. newtype RelMap RelMap :: Map (Name Type, Dir) Rels -> RelMap [unRelMap] :: RelMap -> Map (Name Type, Dir) Rels -- | Modify a RelMap to record the fact that we have solved for a -- type variable. In particular, delete the variable from the -- RelMap as a key, and also update the relative sets of every -- other variable to remove this variable and add the base type we chose -- for it. substRel :: Name Type -> BaseTy -> RelMap -> RelMap -- | Essentially dirtypesBySort vm rm dir t s x finds all the dir-types -- (sub- or super-) of t which have sort s, relative to the variables in -- x. This is overbar{T}_S^X (resp. underbar...) from Traytel et al. dirtypesBySort :: TyVarInfoMap -> RelMap -> Dir -> BaseTy -> Sort -> Set (Name Type) -> [BaseTy] -- | Sort-aware infimum or supremum. limBySort :: TyVarInfoMap -> RelMap -> Dir -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy lubBySort :: TyVarInfoMap -> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy glbBySort :: TyVarInfoMap -> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy allBySort :: TyVarInfoMap -> RelMap -> Dir -> [BaseTy] -> Sort -> Set (Name Type) -> Set BaseTy ubsBySort :: TyVarInfoMap -> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Set BaseTy lbsBySort :: TyVarInfoMap -> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Set BaseTy -- | From the constraint graph, build the sets of sub- and super- base -- types of each type variable, as well as the sets of sub- and supertype -- variables. For each type variable x in turn, try to find a common -- supertype of its base subtypes which is consistent with the sort of x -- and with the sorts of all its sub-variables, as well as symmetrically -- a common subtype of its supertypes, etc. Assign x one of the two: if -- it has only successors, assign it their inf; otherwise, assign it the -- sup of its predecessors. If it has both, we have a choice of whether -- to assign it the sup of predecessors or inf of successors; both lead -- to a sound & complete algorithm. We choose to assign it the sup of -- its predecessors in this case, since it seems nice to default to -- "simpler" types lower down in the subtyping chain. solveGraph :: Members '[Fresh, Error SolveError, Output (Message ann), State SolutionLimit] r => TyVarInfoMap -> Graph UAtom -> Sem r [S] instance GHC.Classes.Eq Disco.Typecheck.Solve.Rels instance GHC.Show.Show Disco.Typecheck.Solve.Rels instance GHC.Show.Show Disco.Typecheck.Solve.RelMap instance Disco.Pretty.Pretty Disco.Typecheck.Solve.RelMap instance GHC.Show.Show Disco.Typecheck.Solve.TyVarInfoMap instance Disco.Pretty.Pretty Disco.Typecheck.Solve.TyVarInfoMap instance GHC.Base.Semigroup Disco.Typecheck.Solve.TyVarInfoMap instance GHC.Base.Monoid Disco.Typecheck.Solve.TyVarInfoMap instance Disco.Pretty.Pretty Disco.Typecheck.Solve.TyVarInfo instance GHC.Base.Semigroup Disco.Typecheck.Solve.TyVarInfo instance GHC.Show.Show Disco.Typecheck.Solve.SolveError instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.Typecheck.Solve.SimpleConstraint instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Typecheck.Solve.SimpleConstraint instance GHC.Generics.Generic Disco.Typecheck.Solve.SimpleConstraint instance GHC.Classes.Ord Disco.Typecheck.Solve.SimpleConstraint instance GHC.Classes.Eq Disco.Typecheck.Solve.SimpleConstraint instance GHC.Show.Show Disco.Typecheck.Solve.SimpleConstraint instance GHC.Show.Show Disco.Typecheck.Solve.TyVarInfo instance Disco.Pretty.Pretty Disco.Typecheck.Solve.SimpleConstraint instance GHC.Base.Semigroup Disco.Typecheck.Solve.SolveError -- | Definition of type contexts, type errors, and various utilities used -- during type checking. module Disco.Typecheck.Util -- | A typing context is a mapping from term names to types. type TyCtx = Ctx Term PolyType -- | A typechecking error, wrapped up together with the name of the thing -- that was being checked when the error occurred. data LocTCError LocTCError :: Maybe (QName Term) -> TCError -> LocTCError -- | Wrap a TCError into a LocTCError with no explicit -- provenance information. noLoc :: TCError -> LocTCError -- | Potential typechecking errors. data TCError -- | Encountered an unbound variable. The offending variable together with -- some suggested in-scope names with small edit distance. Unbound :: Name Term -> [String] -> TCError -- | Encountered an ambiguous name. Ambiguous :: Name Term -> [ModuleName] -> TCError -- | No type is specified for a definition NoType :: Name Term -> TCError -- | The type of the term should have an outermost constructor matching -- Con, but it has type Type instead NotCon :: Con -> Term -> Type -> TCError -- | Case analyses cannot be empty. EmptyCase :: TCError -- | The given pattern should have the type, but it doesn't. instead it has -- a kind of type given by the Con. PatternType :: Con -> Pattern -> Type -> TCError -- | Duplicate declarations. DuplicateDecls :: Name Term -> TCError -- | Duplicate definitions. DuplicateDefns :: Name Term -> TCError -- | Duplicate type definitions. DuplicateTyDefns :: String -> TCError -- | Cyclic type definition. CyclicTyDef :: String -> TCError -- | # of patterns does not match type in definition NumPatterns :: TCError -- | Duplicate variable in a pattern NonlinearPattern :: Pattern -> Name Term -> TCError -- | Type can't be quantified over. NoSearch :: Type -> TCError -- | The constraint solver couldn't find a solution. Unsolvable :: SolveError -> TCError -- | An undefined type name was used. NotTyDef :: String -> TCError -- | Wildcards are not allowed in terms. NoTWild :: TCError -- | Not enough arguments provided to type constructor. NotEnoughArgs :: Con -> TCError -- | Too many arguments provided to type constructor. TooManyArgs :: Con -> TCError -- | Unbound type variable, together with suggested edits UnboundTyVar :: Name Type -> [String] -> TCError -- | Polymorphic recursion is not allowed NoPolyRec :: String -> [String] -> [Type] -> TCError -- | Not an error. The identity of the Monoid TCError instance. NoError :: TCError -- | Emit a constraint. constraint :: Member (Writer Constraint) r => Constraint -> Sem r () -- | Emit a list of constraints. constraints :: Member (Writer Constraint) r => [Constraint] -> Sem r () -- | Close over the current constraint with a forall. forAll :: Member (Writer Constraint) r => [Name Type] -> Sem r a -> Sem r a -- | Run two constraint-generating actions and combine the constraints via -- disjunction. orElse :: Members '[Writer Constraint] r => Sem r () -> Sem r () -> Sem r () -- | Run a computation that generates constraints, returning the generated -- Constraint along with the output. Note that this locally -- dispatches the constraint writer effect. -- -- This function is somewhat low-level; typically you should use -- solve instead, which also solves the generated constraints. withConstraint :: Sem (Writer Constraint ': r) a -> Sem r (a, Constraint) -- | Run a computation and solve its generated constraint, returning up to -- the requested number of possible resulting substitutions (or failing -- with an error). Note that this locally dispatches the constraint -- writer and solution limit effects. solve :: Members '[Reader TyDefCtx, Error TCError, Output (Message ann)] r => Int -> Sem (Writer Constraint ': r) a -> Sem r (a, NonEmpty S) -- | Look up the definition of a named type. Throw a NotTyDef error -- if it is not found. lookupTyDefn :: Members '[Reader TyDefCtx, Error TCError] r => String -> [Type] -> Sem r Type -- | Run a subcomputation with an extended type definition context. withTyDefns :: Member (Reader TyDefCtx) r => TyDefCtx -> Sem r a -> Sem r a -- | Generate a type variable with a fresh name. freshTy :: Member Fresh r => Sem r Type -- | Generate a fresh variable as an atom. freshAtom :: Member Fresh r => Sem r Atom instance GHC.Show.Show Disco.Typecheck.Util.TCError instance GHC.Show.Show Disco.Typecheck.Util.LocTCError instance GHC.Base.Semigroup Disco.Typecheck.Util.TCError instance GHC.Base.Monoid Disco.Typecheck.Util.TCError -- | The ModuleInfo record representing a disco module, and -- functions to resolve the location of a module on disk. module Disco.Module -- | When loading a module, we could be loading it from code entered at the -- REPL, or from a standalone file. The two modes have slightly different -- behavior. data LoadingMode REPL :: LoadingMode Standalone :: LoadingMode -- | A definition consists of a name being defined, the types of any -- pattern arguments (each clause must have the same number of patterns), -- the type of the body of each clause, and a list of clauses. For -- example, -- -- 
--   f x (0,z) = 3*x + z > 5
--   f x (y,z) = z == 9
--   
--
-- -- might look like Defn f [Z, Z*Z] B [clause 1 ..., clause 2 -- ...] data Defn Defn :: Name ATerm -> [Type] -> Type -> NonEmpty Clause -> Defn -- | A clause in a definition consists of a list of patterns (the LHS of -- the =) and a term (the RHS). For example, given the concrete syntax -- f n (x,y) = n*x + y, the corresponding Clause would be -- something like [n, (x,y)] (n*x + y). type Clause = Bind [APattern] ATerm eraseClause :: Clause -> Bind [Pattern] Term -- | Type checking a module yields a value of type ModuleInfo which -- contains mapping from terms to their relavent documenation, a mapping -- from terms to properties, and a mapping from terms to their types. data ModuleInfo ModuleInfo :: ModuleName -> Map ModuleName ModuleInfo -> [QName Term] -> Ctx Term Docs -> Ctx ATerm [AProperty] -> TyCtx -> TyDefCtx -> Ctx ATerm Defn -> [(ATerm, PolyType)] -> ExtSet -> ModuleInfo [_miName] :: ModuleInfo -> ModuleName [_miImports] :: ModuleInfo -> Map ModuleName ModuleInfo [_miNames] :: ModuleInfo -> [QName Term] [_miDocs] :: ModuleInfo -> Ctx Term Docs [_miProps] :: ModuleInfo -> Ctx ATerm [AProperty] [_miTys] :: ModuleInfo -> TyCtx [_miTydefs] :: ModuleInfo -> TyDefCtx [_miTermdefs] :: ModuleInfo -> Ctx ATerm Defn [_miTerms] :: ModuleInfo -> [(ATerm, PolyType)] [_miExts] :: ModuleInfo -> ExtSet miTys :: Lens' ModuleInfo TyCtx miTydefs :: Lens' ModuleInfo TyDefCtx miTerms :: Lens' ModuleInfo [(ATerm, PolyType)] miTermdefs :: Lens' ModuleInfo (Ctx ATerm Defn) miProps :: Lens' ModuleInfo (Ctx ATerm [AProperty]) miNames :: Lens' ModuleInfo [QName Term] miName :: Lens' ModuleInfo ModuleName miImports :: Lens' ModuleInfo (Map ModuleName ModuleInfo) miExts :: Lens' ModuleInfo ExtSet miDocs :: Lens' ModuleInfo (Ctx Term Docs) -- | Get something from a module and its direct imports. withImports :: Monoid a => Getting a ModuleInfo a -> ModuleInfo -> a -- | Get the types of all names bound in a module and its direct imports. allTys :: ModuleInfo -> TyCtx -- | Get all type definitions from a module and its direct imports. allTydefs :: ModuleInfo -> TyDefCtx -- | The empty module info record. emptyModuleInfo :: ModuleInfo -- | A data type indicating where we should look for Disco modules to be -- loaded. data Resolver -- | Load only from the stdlib (standard lib modules) FromStdlib :: Resolver -- | Load only from a specific directory (:load) FromDir :: FilePath -> Resolver -- | Load from current working dir or stdlib (import at REPL) FromCwdOrStdlib :: Resolver -- | Load from specific dir or stdlib (import in file) FromDirOrStdlib :: FilePath -> Resolver -- | Add the possibility of loading imports from the stdlib. For example, -- this is what we want to do after a user loads a specific file using -- `:load` (for which we will NOT look in the stdlib), but then we need -- to recursively load modules which it imports (which may either be in -- the stdlib, or the same directory as the `:load`ed module). withStdlib :: Resolver -> Resolver -- | Given a module resolution mode and a raw module name, relavent -- directories are searched for the file containing the provided module -- name. Returns Nothing if no module with the given name could be found. resolveModule :: Member (Embed IO) r => Resolver -> String -> Sem r (Maybe (FilePath, ModuleProvenance)) instance GHC.Base.Semigroup Disco.Module.ModuleInfo instance GHC.Base.Monoid Disco.Module.ModuleInfo instance Unbound.Generics.LocallyNameless.Subst.Subst Disco.Types.Type Disco.Module.Defn instance Data.Data.Data Disco.Module.Defn instance Unbound.Generics.LocallyNameless.Alpha.Alpha Disco.Module.Defn instance GHC.Generics.Generic Disco.Module.Defn instance GHC.Show.Show Disco.Module.Defn instance GHC.Show.Show Disco.Module.ModuleInfo instance Disco.Pretty.Pretty Disco.Module.Defn -- | Parser to convert concrete Disco syntax into an (untyped, surface -- language) AST. module Disco.Parser data DiscoParseError ReservedVarName :: String -> DiscoParseError InvalidPattern :: OpaqueTerm -> DiscoParseError MissingAscr :: DiscoParseError MultiArgLambda :: DiscoParseError -- | A parser is a megaparsec parser of strings, with an extra layer of -- state to keep track of the current indentation level and language -- extensions, and some custom error messages. type Parser = StateT ParserState (Parsec DiscoParseError String) -- | Run a parser from the initial state. runParser :: Parser a -> FilePath -> String -> Either (ParseErrorBundle String DiscoParseError) a -- | Locally set the enabled extensions within a subparser. withExts :: Set Ext -> Parser a -> Parser a -- | indented p is just like p, except that every token -- must not start in the first column. indented :: Parser a -> Parser a -- | indented p is just like p, except that every token -- after the first must not start in the first column. thenIndented :: Parser a -> Parser a -- | Generically consume whitespace, including comments. sc :: Parser () -- | Parse a lexeme, that is, a parser followed by consuming whitespace. lexeme :: Parser a -> Parser a -- | Parse a given string as a lexeme. symbol :: String -> Parser String -- | Parse a reserved operator. reservedOp :: String -> Parser () -- | Parse a natural number. natural :: Parser Integer -- | Parse a reserved word. reserved :: String -> Parser () -- | The list of all reserved words. reservedWords :: [String] -- | Parse an identifier and turn it into a Name. ident :: Parser (Name Term) parens :: Parser a -> Parser a braces :: Parser a -> Parser a angles :: Parser a -> Parser a brackets :: Parser a -> Parser a semi :: Parser String comma :: Parser String colon :: Parser String dot :: Parser String pipe :: Parser String -- | The symbol that starts an anonymous function (either a backslash or a -- Greek λ). lambda :: Parser String -- | Parse the entire input as a module (with leading whitespace and no -- leftovers). wholeModule :: LoadingMode -> Parser Module -- | Parse an entire module (a list of declarations ended by semicolons). -- The LoadingMode parameter tells us whether to include or -- replace any language extensions enabled at the top level. We include -- them when parsing a module entered at the REPL, and replace them when -- parsing a standalone module. parseModule :: LoadingMode -> Parser Module -- | Parse the name of a language extension (case-insensitive). parseExtName :: Parser Ext -- | Parse a top level item (either documentation or a declaration), which -- must start at the left margin. parseTopLevel :: Parser TopLevel -- | Parse a single top-level declaration (either a type declaration or -- single definition clause). parseDecl :: Parser Decl -- | Parse an import, of the form import modulename. parseImport :: Parser String -- | Parse the name of a module. parseModuleName :: Parser String -- | Parse the entire input as a term (with leading whitespace and no -- leftovers). term :: Parser Term -- | Parse a term, consisting of a parseTerm' optionally followed -- by an ascription. parseTerm :: Parser Term -- | Parse a non-atomic, non-ascribed term. parseTerm' :: Parser Term -- | Parse an expression built out of unary and binary operators. parseExpr :: Parser Term -- | Parse an atomic term. parseAtom :: Parser Term -- | Parse a container, like a literal list, set, bag, or a comprehension -- (not including the square or curly brackets). -- -- 
--   container-contents
--     ::= nonempty-container | empty
--   
--   nonempty-container ::= term container-end
--   
--   container-end
--     ::= '|' comprehension
--          | (',' term)* [ ellipsis ]
--   
--   comprehension ::= qual [ ',' qual ]*
--   
--   qual
--     ::= ident 'in' term
--       | term
--   
--   ellipsis ::= [ ',' ] '..' [ ',' ] term
--
parseContainer :: Container -> Parser Term -- | Parse an ellipsis at the end of a literal list, of the form .. -- t. Any number > 1 of dots may be used, just for fun. parseEllipsis :: Parser (Ellipsis Term) -- | Parse the part of a list comprehension after the | (without square -- brackets), i.e. a list of qualifiers. -- -- 
--   q [,q]*
--
parseContainerComp :: Container -> Term -> Parser Term -- | Parse a qualifier in a comprehension: either a binder x in t -- or a guard t. parseQual :: Parser Qual -- | Parse a let expression (let x1 = t1, x2 = t2, ... in t). parseLet :: Parser Term parseTypeOp :: Parser Term -- | Parse a case expression. parseCase :: Parser Term -- | Parse one branch of a case expression. parseBranch :: Parser Branch -- | Parse the list of guards in a branch. otherwise can be used -- interchangeably with an empty list of guards. parseGuards :: Parser (Telescope Guard) -- | Parse a single guard (if, if ... is ..., or -- let) parseGuard :: Parser Guard -- | Parse a pattern, by parsing a term and then attempting to convert it -- to a pattern. The Bool parameter says whether to require a type -- ascription. parsePattern :: Bool -> Parser Pattern -- | Parse an atomic pattern, by parsing a term and then attempting to -- convert it to a pattern. parseAtomicPattern :: Parser Pattern -- | Parse a type expression built out of binary operators. parseType :: Parser Type -- | Parse an atomic type. parseAtomicType :: Parser Type parsePolyTy :: Parser PolyType instance GHC.Classes.Ord Disco.Parser.DiscoParseError instance GHC.Classes.Eq Disco.Parser.DiscoParseError instance GHC.Show.Show Disco.Parser.DiscoParseError instance Text.Megaparsec.Error.ShowErrorComponent Disco.Parser.DiscoParseError instance GHC.Show.Show Disco.Parser.OpaqueTerm instance GHC.Classes.Eq Disco.Parser.OpaqueTerm instance GHC.Classes.Ord Disco.Parser.OpaqueTerm -- | Type for collecting all potential Disco errors at the top level, and a -- type for runtime errors. module Disco.Error -- | Top-level error type for Disco. data DiscoError -- | 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 -- | Errors that can be generated at runtime. data EvalError -- | An unbound name was encountered. [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 -- | Division by zero. [DivByZero] :: EvalError -- | Overflow, e.g. (2^66)! [Overflow] :: EvalError -- | Non-exhaustive case analysis. [NonExhaustive] :: EvalError -- | Infinite loop detected via black hole. [InfiniteLoop] :: EvalError -- | User-generated crash. [Crash] :: String -> EvalError panic :: Member (Error DiscoError) r => String -> Sem r a outputDiscoErrors :: Member (Output (Message ann)) r => Sem (Error DiscoError ': r) () -> Sem r () instance GHC.Show.Show Disco.Error.DiscoError instance GHC.Show.Show Disco.Error.EvalError instance Disco.Pretty.Pretty Disco.Error.DiscoError -- | Disco runtime values and environments. module Disco.Value -- | Different types of values which can result from the evaluation -- process. data Value -- | A numeric value. [VNum] :: Rational -> Value -- | A built-in function constant. [VConst] :: Op -> Value -- | An injection into a sum type. [VInj] :: Side -> Value -> Value -- | The unit value. [VUnit] :: Value -- | A pair of values. [VPair] :: Value -> Value -> Value -- | A closure, i.e. a function body together with its environment. [VClo] :: Maybe (Int, [Value]) -> Env -> [Name Core] -> Core -> Value -- | A disco type can be a value. For now, there are only a very limited -- number of places this could ever show up (in particular, as an -- argument to enumerate or count). [VType] :: Type -> Value -- | A reference, i.e. a pointer to a memory cell. This is used to -- implement (optional, user-requested) laziness as well as recursion. [VRef] :: Int -> Value -- | A literal function value. VFun is only used when enumerating -- function values in order to decide comparisons at higher-order -- function types. For example, in order to compare two values of type -- (Bool -> Bool) -> Bool for equality, we have to -- enumerate all functions of type Bool -> Bool as -- VFun values. -- -- We assume that all VFun values are strict, that is, -- their arguments should be fully evaluated to RNF before being passed -- to the function. [VFun_] :: ValFun -> Value -- | A proposition. [VProp] :: ValProp -> Value -- | A literal bag, containing a finite list of (perhaps only partially -- evaluated) values, each paired with a count. This is also used to -- represent sets (with the invariant that all counts are equal to 1). [VBag] :: [(Value, Integer)] -> Value -- | A graph, stored using an algebraic repesentation. [VGraph] :: Graph SimpleValue -> Value -- | A map from keys to values. Differs from functions because we can -- actually construct the set of entries, while functions only have this -- property when the key type is finite. [VMap] :: Map SimpleValue Value -> Value [VGen] :: StdGen -> Value -- | Convenient pattern for the empty list. pattern VNil :: Value -- | Convenient pattern for list cons. pattern VCons :: Value -> Value -> Value pattern VFun :: (Value -> Value) -> Value -- | Values which can be used as keys in a map, i.e. those for which a -- Haskell Ord instance can be easily created. These should always be of -- a type for which the QSimple qualifier can be constructed. At the -- moment these are always fully evaluated (containing no indirections) -- and thus don't need memory management. At some point in the future -- constructors for simple graphs and simple maps could be created, if -- the value type is also QSimple. The only reason for actually doing -- this would be constructing graphs of graphs or maps of maps, or the -- like. data SimpleValue [SNum] :: Rational -> SimpleValue [SUnit] :: SimpleValue [SInj] :: Side -> SimpleValue -> SimpleValue [SPair] :: SimpleValue -> SimpleValue -> SimpleValue [SBag] :: [(SimpleValue, Integer)] -> SimpleValue [SType] :: Type -> SimpleValue toSimpleValue :: Value -> SimpleValue fromSimpleValue :: SimpleValue -> Value ratv :: Rational -> Value vrat :: Value -> Rational -- | A convenience function for creating a default VNum value with -- a default (Fractional) flag. intv :: Integer -> Value vint :: Value -> Integer charv :: Char -> Value vchar :: Value -> Char boolv :: Bool -> Value vbool :: Value -> Bool pairv :: (a -> Value) -> (b -> Value) -> (a, b) -> Value vpair :: (Value -> a) -> (Value -> b) -> Value -> (a, b) listv :: (a -> Value) -> [a] -> Value vlist :: (Value -> a) -> Value -> [a] genv :: StdGen -> Value vgen :: Value -> StdGen -- | A ValProp is the normal form of a Disco value of type -- Prop. data ValProp -- | A prop that has already either succeeded or failed. VPDone :: TestResult -> ValProp -- | A pending search. VPSearch :: SearchMotive -> [Type] -> Value -> TestEnv -> ValProp -- | A binary logical operator combining two prop values. VPBin :: LOp -> ValProp -> ValProp -> ValProp -- | The possible outcomes of a proposition. data TestResult TestResult :: Bool -> TestReason -> TestEnv -> TestResult -- | The possible outcomes of a property test, parametrized over the type -- of values. A TestReason explains why a proposition succeeded -- or failed. data TestReason_ a -- | The prop evaluated to a boolean. TestBool :: TestReason_ a -- | The test was a comparison. Records the comparison operator, the values -- being compared, and also their type (which is needed for printing). TestCmp :: BOp -> Type -> a -> a -> TestReason_ a -- | The search didn't find any examples/counterexamples. TestNotFound :: SearchType -> TestReason_ a -- | The search found an example/counterexample. TestFound :: TestResult -> TestReason_ a -- | A binary logical operator was used to combine the given two results. TestBin :: LOp -> TestResult -> TestResult -> TestReason_ a -- | The prop failed at runtime. This is always a failure, no matter which -- quantifiers or negations it's under. TestRuntimeError :: EvalError -> TestReason_ a type TestReason = TestReason_ Value data SearchType -- | All possibilities were checked. Exhaustive :: SearchType -- | A number of small cases were checked exhaustively and then a number of -- additional cases were checked at random. Randomized :: Integer -> Integer -> SearchType -- | The answer (success or failure) we're searching for, and the result -- (success or failure) we return when we find it. The motive (False, -- False) corresponds to a "forall" quantifier (look for a -- counterexample, fail if you find it) and the motive (True, -- True) corresponds to "exists". The other values arise from -- negations. newtype SearchMotive SearchMotive :: (Bool, Bool) -> SearchMotive pattern SMExists :: SearchMotive pattern SMForall :: SearchMotive -- | A collection of variables that might need to be reported for a test, -- along with their types and user-legible names. newtype TestVars TestVars :: [(String, Type, Name Core)] -> TestVars -- | A variable assignment found during a test. newtype TestEnv TestEnv :: [(String, Type, Value)] -> TestEnv emptyTestEnv :: TestEnv mergeTestEnv :: TestEnv -> TestEnv -> TestEnv getTestEnv :: TestVars -> Env -> Either EvalError TestEnv extendPropEnv :: TestEnv -> ValProp -> ValProp extendResultEnv :: TestEnv -> TestResult -> TestResult -- | Whether the property test resulted in success. testIsOk :: TestResult -> Bool -- | Whether the property test resulted in a runtime error. testIsError :: TestResult -> Bool -- | The reason the property test had this result. testReason :: TestResult -> TestReason testEnv :: TestResult -> TestEnv resultIsCertain :: TestReason -> Bool -- | Binary logical operators. data LOp LAnd :: LOp LOr :: LOp LImpl :: LOp interpLOp :: LOp -> Bool -> Bool -> Bool -- | An environment is a mapping from names to values. type Env = Ctx Core Value data Cell Blackhole :: Cell E :: Env -> Core -> Cell V :: Value -> Cell -- | Mem represents a memory, containing Cells data Mem emptyMem :: Mem -- | Allocate a new memory cell containing an unevaluated expression with -- the current environment. Return the index of the allocated cell. allocate :: Members '[State Mem] r => Env -> Core -> Sem r Int allocateValue :: Members '[State Mem] r => Value -> Sem r Int -- | Allocate new memory cells for a group of mutually recursive bindings, -- and return the indices of the allocate cells. allocateRec :: Members '[State Mem] r => Env -> [(QName Core, Core)] -> Sem r [Int] -- | Look up the cell at a given index. lkup :: Members '[State Mem] r => Int -> Sem r (Maybe Cell) memoLookup :: Members '[State Mem] r => Int -> SimpleValue -> Sem r (Maybe Value) -- | Set the cell at a given index. set :: Members '[State Mem] r => Int -> Cell -> Sem r () memoSet :: Members '[State Mem] r => Int -> SimpleValue -> Value -> Sem r () prettyValue' :: Member (Input TyDefCtx) r => Type -> Value -> Sem r (Doc ann) prettyValue :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r (Doc ann) instance GHC.Classes.Ord Disco.Value.SimpleValue instance GHC.Classes.Eq Disco.Value.SimpleValue instance GHC.Show.Show Disco.Value.SimpleValue instance GHC.Show.Show Disco.Value.SearchType instance GHC.Show.Show Disco.Value.SearchMotive instance GHC.Base.Monoid Disco.Value.TestVars instance GHC.Base.Semigroup Disco.Value.TestVars instance GHC.Show.Show Disco.Value.TestVars instance GHC.Enum.Bounded Disco.Value.LOp instance GHC.Enum.Enum Disco.Value.LOp instance GHC.Show.Show Disco.Value.LOp instance GHC.Classes.Ord Disco.Value.LOp instance GHC.Classes.Eq Disco.Value.LOp instance GHC.Base.Monoid Disco.Value.TestEnv instance GHC.Base.Semigroup Disco.Value.TestEnv instance GHC.Show.Show Disco.Value.TestEnv instance Data.Traversable.Traversable Disco.Value.TestReason_ instance Data.Foldable.Foldable Disco.Value.TestReason_ instance GHC.Base.Functor Disco.Value.TestReason_ instance GHC.Show.Show a => GHC.Show.Show (Disco.Value.TestReason_ a) instance GHC.Show.Show Disco.Value.TestResult instance GHC.Show.Show Disco.Value.ValProp instance GHC.Show.Show Disco.Value.Value instance GHC.Show.Show Disco.Value.Cell instance GHC.Show.Show Disco.Value.Mem instance GHC.Show.Show Disco.Value.ValFun -- | Enumerate values inhabiting Disco types. module Disco.Enumerate type ValueEnumeration = IEnumeration Value -- | Enumerate all values of type Void (none). enumVoid :: ValueEnumeration -- | Enumerate all values of type Unit (the single value -- unit). enumUnit :: ValueEnumeration -- | Enumerate the values of type Bool as [false, true]. enumBool :: ValueEnumeration -- | Enumerate all values of type Nat (0, 1, 2, ...). enumN :: ValueEnumeration -- | Enumerate all values of type Integer (0, 1, -1, 2, -2, ...). enumZ :: ValueEnumeration -- | Enumerate all values of type Fractional in the Calkin-Wilf -- order (1, 12, 2, 13, 32, 23, 3, ...). enumF :: ValueEnumeration -- | Enumerate all values of type Rational in the Calkin-Wilf -- order, with negatives interleaved (0, 1, -1, 12, -12, 2, -2, -- ...). enumQ :: ValueEnumeration -- | Enumerate all Unicode characters. enumC :: ValueEnumeration -- | Enumerate all *finite* sets over a certain element type, given an -- enumeration of the elements. If we think of each finite set as a -- binary string indicating which elements in the enumeration are -- members, the sets are enumerated in order of the binary strings. enumSet :: ValueEnumeration -> ValueEnumeration -- | 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 -- | Enumerate the values of a given type. enumType :: Type -> ValueEnumeration -- | Enumerate a finite product of types. enumTypes :: [Type] -> IEnumeration [Value] -- | Produce an actual list of the values of a type. enumerateType :: Type -> [Value] -- | Produce an actual list of values enumerated from a finite product of -- types. enumerateTypes :: [Type] -> [[Value]] -- | Typecheck the Disco surface language and transform it into a -- type-annotated AST. module Disco.Typecheck containerTy :: Container -> Type -> Type containerToCon :: Container -> Con -- | Infer the type of a telescope, given a way to infer the type of each -- item along with a context of variables it binds; each such context is -- then added to the overall context when inferring subsequent items in -- the telescope. inferTelescope :: (Alpha b, Alpha tyb, Member (Reader TyCtx) r) => (b -> Sem r (tyb, TyCtx)) -> Telescope b -> Sem r (Telescope tyb, TyCtx) suggestionsFrom :: String -> [String] -> [String] -- | Check all the types and extract all relevant info (docs, properties, -- types) from a module, returning a ModuleInfo record on success. -- This function does not handle imports at all; any imports should -- already be checked and passed in as the second argument. checkModule :: Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh] r => ModuleName -> Map ModuleName ModuleInfo -> Module -> Sem r ModuleInfo -- | Turn a list of type definitions into a TyDefCtx, checking for -- duplicate names among the definitions and also any type definitions -- already in the context. makeTyDefnCtx :: Members '[Reader TyDefCtx, Error TCError] r => [TypeDefn] -> Sem r TyDefCtx -- | Check the validity of a type definition. checkTyDefn :: Members '[Reader TyDefCtx, Error LocTCError] r => ModuleName -> TypeDefn -> Sem r () -- | Check if a given type is cyclic. A type ty is cyclic if: -- --
    --
  1. ty is the name of a user-defined type.
    2. --
  2. Repeated expansions of the type yield nothing but other -- user-defined types.
    3. --
  3. An expansion of one of those types yields another type that has -- been previously encountered.
    4. --
-- -- In other words, repeatedly expanding the definition can get us back to -- exactly where we started. -- -- The function returns the set of TyDefs encountered during expansion if -- the TyDef is not cyclic. checkCyclicTy :: Members '[Reader TyDefCtx, Error TCError] r => Type -> Set String -> Sem r (Set String) -- | Ensure that a type definition does not use any unbound type variables -- or undefined types. checkUnboundVars :: Members '[Reader TyDefCtx, Error TCError] r => TypeDefn -> Sem r () -- | Check for polymorphic recursion: starting from a user-defined type, -- keep expanding its definition recursively, ensuring that any recursive -- references to the defined type have only type variables as arguments. checkPolyRec :: Member (Error TCError) r => TypeDefn -> Sem r () -- | Keep only the duplicate elements from a list. -- -- 
--   >>> filterDups [1,3,2,1,1,4,2]
--   [1,2]
--
filterDups :: Ord a => [a] -> [a] -- | Given a list of type declarations from a module, first check that -- there are no duplicate type declarations, and that the types are -- well-formed; then create a type context containing the given -- declarations. makeTyCtx :: Members '[Reader TyDefCtx, Error TCError] r => ModuleName -> [TypeDecl] -> Sem r TyCtx -- | Check that all the types in a context are valid. checkCtx :: Members '[Reader TyDefCtx, Error TCError] r => TyCtx -> Sem r () -- | Type check a top-level definition in the given module. checkDefn :: Members '[Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh, Output (Message ann)] r => ModuleName -> TermDefn -> Sem r Defn -- | Given a context mapping names to documentation, extract the properties -- attached to each name and typecheck them. checkProperties :: Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output (Message ann)] r => Ctx Term Docs -> Sem r (Ctx ATerm [AProperty]) -- | Check the types of the terms embedded in a property. checkProperty :: Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output (Message ann)] r => Property -> Sem r AProperty -- | Check that a sigma type is a valid type. See checkTypeValid. checkPolyTyValid :: Members '[Reader TyDefCtx, Error TCError] r => PolyType -> Sem r () -- | Disco doesn't need kinds per se, since all types must be fully -- applied. But we do need to check that every type is applied to the -- correct number of arguments. checkTypeValid :: Members '[Reader TyDefCtx, Error TCError] r => Type -> Sem r () conArity :: Members '[Reader TyDefCtx, Error TCError] r => Con -> Sem r Int -- | Typechecking can be in one of two modes: inference mode means we are -- trying to synthesize a valid type for a term; checking mode means we -- are trying to show that a term has a given type. data Mode Infer :: Mode Check :: Type -> Mode -- | Check that a term has the given type. Either throws an error, or -- returns the term annotated with types for all subterms. -- -- This function is provided for convenience; it simply calls -- typecheck with an appropriate Mode. check :: Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Term -> Type -> Sem r ATerm -- | Check that a term has the given polymorphic type. checkPolyTy :: Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Term -> PolyType -> Sem r ATerm -- | Infer the type of a term. If it succeeds, it returns the term with all -- subterms annotated. -- -- This function is provided for convenience; it simply calls -- typecheck with an appropriate Mode. infer :: Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Term -> Sem r ATerm -- | Top-level type inference algorithm, returning only the first possible -- result. inferTop1 :: Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r => Term -> Sem r (ATerm, PolyType) -- | Top-level type inference algorithm: infer up to the requested max -- number of possible (polymorphic) types for a term by running type -- inference, solving the resulting constraints, and quantifying over any -- remaining type variables. inferTop :: Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r => Int -> Term -> Sem r (NonEmpty (ATerm, PolyType)) -- | Top-level type checking algorithm: check that a term has a given -- polymorphic type by running type checking and solving the resulting -- constraints. checkTop :: Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r => Term -> PolyType -> Sem r ATerm -- | The main workhorse of the typechecker. Instead of having two -- functions, one for inference and one for checking, typecheck -- takes a Mode. This cuts down on code duplication in many cases, -- and allows all the checking and inference code related to a given AST -- node to be placed together. typecheck :: Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Mode -> Term -> Sem r ATerm -- | Check that a pattern has the given type, and return a context of -- pattern variables bound in the pattern along with their types. checkPattern :: Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Pattern -> Type -> Sem r (TyCtx, APattern) -- | Constraints needed on a function type for it to be the type of the -- absolute value function. cAbs :: Members '[Writer Constraint, Fresh] r => Type -> Type -> Sem r () -- | Constraints needed on a function type for it to be the type of the -- container size operation. cSize :: Members '[Writer Constraint, Fresh] r => Type -> Type -> Sem r () -- | Given an input type ty, return a type which represents the -- output type of the absolute value function, and generate appropriate -- constraints. cPos :: Members '[Writer Constraint, Fresh] r => Type -> Sem r Type -- | Given an input type ty, return a type which represents the -- output type of the floor or ceiling functions, and generate -- appropriate constraints. cInt :: Members '[Writer Constraint, Fresh] r => Type -> Sem r Type -- | Given input types to the exponentiation operator, return a type which -- represents the output type, and generate appropriate constraints. cExp :: Members '[Writer Constraint, Fresh] r => Type -> Type -> Sem r Type -- | Get the argument (element) type of a (known) container type. Returns a -- fresh variable with a suitable constraint if the given type is not -- literally a container type. getEltTy :: Members '[Writer Constraint, Fresh] r => Container -> Type -> Sem r Type -- | Ensure that a type's outermost constructor matches the provided -- constructor, returning the types within the matched constructor or -- throwing a type error. If the type provided is a type variable, -- appropriate constraints are generated to guarantee the type variable's -- outermost constructor matches the provided constructor, and a list of -- fresh type variables is returned whose count matches the arity of the -- provided constructor. ensureConstr :: forall r. Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Con -> Type -> Either Term Pattern -> Sem r [Type] -- | A variant of ensureConstr that expects to get exactly one argument -- type out, and throws an error if we get any other number. ensureConstr1 :: Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Con -> Type -> Either Term Pattern -> Sem r Type -- | A variant of ensureConstr that expects to get exactly two argument -- types out, and throws an error if we get any other number. ensureConstr2 :: Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Con -> Type -> Either Term Pattern -> Sem r (Type, Type) -- | A variant of ensureConstr that works on Modes instead of -- Types. Behaves similarly to ensureConstr if the -- Mode is Check; otherwise it generates an appropriate -- number of copies of Infer. ensureConstrMode :: Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Con -> Mode -> Either Term Pattern -> Sem r [Mode] -- | A variant of ensureConstrMode that expects to get a single -- Mode and throws an error if it encounters any other number. ensureConstrMode1 :: Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Con -> Mode -> Either Term Pattern -> Sem r Mode -- | A variant of ensureConstrMode that expects to get two -- Modes and throws an error if it encounters any other number. ensureConstrMode2 :: Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Con -> Mode -> Either Term Pattern -> Sem r (Mode, Mode) -- | Ensure that two types are equal: 1. Do nothing if they are literally -- equal 2. Generate an equality constraint otherwise ensureEq :: Member (Writer Constraint) r => Type -> Type -> Sem r () isSubPolyType :: Members '[Input TyDefCtx, Output (Message ann), Fresh] r => PolyType -> PolyType -> Sem r Bool thin :: Members '[Input TyDefCtx, Output (Message ann), Fresh] r => NonEmpty PolyType -> Sem r (NonEmpty PolyType) thin' :: Members '[Input TyDefCtx, Output (Message ann), Fresh] r => [PolyType] -> Sem r [PolyType] instance GHC.Show.Show Disco.Typecheck.Mode -- | Utilities for converting Disco types into Constructors that the -- exhaustiveness checker understands, and utilities for working with -- TypedVars and their names. module Disco.Exhaustiveness.TypeInfo newtype TypedVar TypedVar :: (Name ATerm, Type) -> TypedVar getType :: TypedVar -> Type data DataCon DataCon :: Ident -> [Type] -> DataCon [dcIdent] :: DataCon -> Ident [dcTypes] :: DataCon -> [Type] data Ident [KUnit] :: Ident [KBool] :: Bool -> Ident [KNat] :: Integer -> Ident [KInt] :: Integer -> Ident [KPair] :: Ident [KCons] :: Ident [KNil] :: Ident [KChar] :: Char -> Ident [KLeft] :: Ident [KRight] :: Ident [KUnknown] :: Ident -- | Finite constructors are used in the LYG checker Infinite -- constructors are used when reporting examples of uncovered patterns, -- we only pick out a few of them data Constructors [Finite] :: [DataCon] -> Constructors [Infinite] :: [DataCon] -> Constructors unknown :: DataCon unit :: DataCon bool :: Bool -> DataCon natural :: Integer -> DataCon integer :: Integer -> DataCon char :: Char -> DataCon cons :: Type -> Type -> DataCon nil :: DataCon pair :: Type -> Type -> DataCon left :: Type -> DataCon right :: Type -> DataCon tyDataCons :: Type -> TyDefCtx -> Constructors resolveAlias :: Type -> TyDefCtx -> Type -- | Assuming type aliases have been resolved, this function converts Disco -- types into lists of DataCons that are compatible with the LYG checker. -- -- A list of constructors is Infinite if the only way to fully -- match against the type is with a wildcard or variable pattern. -- Otherwise, it is Finite. -- -- The LYG checker only reads the list of constructors if a type is -- Finite. From the point of view of the checker, Infinite -- is a synonym for opaque, and the constructors are discarded. The -- dataconstructors in an Infinite list are only used when -- generating the 3 positive examples of what you haven't matched -- against. This will probably need to change a bit when bringing -- exhaustiveness checking to the new arithmetic patterns. -- -- Notice the last case of this function, which a wildcard handling the -- types: (_ Ty.:->: _) (Ty.TySet _) (Ty.TyBag _) (Ty.TyVar _) -- (Ty.TySkolem _) (Ty.TyProp) (Ty.TyMap _ _) (Ty.TyGraph _) -- -- I believe all of these are impossible to pattern match against with -- anything other than a wildcard (or variable pattern) in Disco, so they -- should always be fully covered. But if they are in a pair, for -- example, Set(Int)*Int, we still need to generate 3 examples of the -- pair if that Int part isn't covered. So how do we fill the concrete -- part of Set(Int), (or a generic type "a", or a function, etc.)? I'm -- calling that unknown, and printing an underscore. (Also, I'm -- using Infinite for reasons metioned above). tyDataConsHelper :: Type -> Constructors newName :: Member Fresh r => Sem r (Name ATerm) newVar :: Member Fresh r => Type -> Sem r TypedVar newNames :: Member Fresh r => Int -> Sem r [Name ATerm] newVars :: Member Fresh r => [Type] -> Sem r [TypedVar] instance GHC.Classes.Ord Disco.Exhaustiveness.TypeInfo.TypedVar instance GHC.Show.Show Disco.Exhaustiveness.TypeInfo.TypedVar instance GHC.Classes.Ord Disco.Exhaustiveness.TypeInfo.Ident instance GHC.Classes.Eq Disco.Exhaustiveness.TypeInfo.Ident instance GHC.Show.Show Disco.Exhaustiveness.TypeInfo.Ident instance GHC.Show.Show Disco.Exhaustiveness.TypeInfo.DataCon instance GHC.Classes.Ord Disco.Exhaustiveness.TypeInfo.DataCon instance GHC.Classes.Eq Disco.Exhaustiveness.TypeInfo.DataCon instance GHC.Classes.Eq Disco.Exhaustiveness.TypeInfo.TypedVar -- | The heart of the Lower Your Guards algorithm. Functions for converting -- constraints detailing pattern matches into a normalized description of -- everything that is left uncovered. module Disco.Exhaustiveness.Constraint data Constraint [CMatch] :: DataCon -> [TypedVar] -> Constraint [CNot] :: DataCon -> Constraint [CWasOriginally] :: TypedVar -> Constraint posMatch :: [Constraint] -> Maybe (DataCon, [TypedVar]) negMatches :: [Constraint] -> [DataCon] type ConstraintFor = (TypedVar, Constraint) lookupVar :: TypedVar -> [ConstraintFor] -> TypedVar alistLookup :: Eq a => a -> [(a, b)] -> [b] onVar :: TypedVar -> [ConstraintFor] -> [Constraint] type NormRefType = [ConstraintFor] addConstraints :: Members '[Fresh, Reader TyDefCtx] r => NormRefType -> [ConstraintFor] -> MaybeT (Sem r) NormRefType addConstraint :: Members '[Fresh, Reader TyDefCtx] r => NormRefType -> ConstraintFor -> MaybeT (Sem r) NormRefType addConstraintHelper :: Members '[Fresh, Reader TyDefCtx] r => NormRefType -> ConstraintFor -> MaybeT (Sem r) NormRefType breakIf :: Alternative f => Bool -> f () -- | Returns a predicate that returns true if another constraint conflicts -- with the one given. This alone is not sufficient to test if a -- constraint can be added, but it filters out the easy negatives early -- on conflictsWith :: Constraint -> Constraint -> Bool -- | Search for a MatchDataCon that is matching on k specifically (there -- should be at most one, see I4 in section 3.4) and if it exists, return -- the variable ids of its arguments getConstructorArgs :: DataCon -> [Constraint] -> Maybe [TypedVar] -- | substituting y *for* x ie replace the second with the first, replace x -- with y substituteVarIDs :: TypedVar -> TypedVar -> [ConstraintFor] -> [ConstraintFor] -- | Deals with I2 from section 3.4 if a variable in the context has a -- resolvable type, there must be at least one constructor which can be -- instantiated without contradiction of the refinement type This -- function tests if this is true inhabited :: Members '[Fresh, Reader TyDefCtx] r => NormRefType -> TypedVar -> Sem r Bool -- | Attempts to "instantiate" a match of the dataconstructor k on x If we -- can add the MatchDataCon constraint to the normalized refinement type -- without contradiction (a Nothing value), then x is inhabited by k and -- we return true instantiate :: Members '[Fresh, Reader TyDefCtx] r => NormRefType -> TypedVar -> DataCon -> Sem r Bool instance GHC.Classes.Ord Disco.Exhaustiveness.Constraint.Constraint instance GHC.Classes.Eq Disco.Exhaustiveness.Constraint.Constraint instance GHC.Show.Show Disco.Exhaustiveness.Constraint.Constraint -- | Entry point into the exhaustiveness checker. Converts information into -- a format the checker understands, then pretty prints the results of -- running it. module Disco.Exhaustiveness -- | This exhaustiveness checking algorithm is based on the paper "Lower -- Your Guards: A Compositional Pattern-Match Coverage Checker": -- https://www.microsoft.com/en-us/research/uploads/prod/2020/03/lyg.pdf -- -- Some simplifications were made to adapt the algorithm to suit Disco. -- The most notable change is that here we always generate (at most) 3 -- concrete examples of uncovered patterns, instead of finding the most -- general complete description of every uncovered input. checkClauses :: Members '[Fresh, Reader TyDefCtx, Output (Message ann), Embed IO] r => Name ATerm -> [Type] -> NonEmpty [APattern] -> Sem r () prettyPrintExample :: ExamplePat -> Sem r (Doc ann) prettyPrintPattern :: Members '[Reader PA, LFresh] r => Pattern -> Sem r (Doc ann) exampleToDiscoPattern :: ExamplePat -> Pattern resugarPair :: ExamplePat -> [ExamplePat] resugarList :: ExamplePat -> [ExamplePat] resugarString :: ExamplePat -> String assumeExampleChar :: ExamplePat -> Char desugarClause :: Members '[Fresh, Embed IO] r => [TypedVar] -> Int -> [APattern] -> Sem r Gdt desugarTuplePats :: [APattern] -> APattern -- | Convert a Disco APattern into a list of Guards which cover that -- pattern -- -- These patterns are currently not handled: , APNeg --still need to -- handle rational case , APFrac --required for rationals? algebraic -- (probably will be eventually replaced anyway): , APAdd , APMul , APSub -- These (or some updated version of them) may be handled eventually, -- once updated arithmetic patterns are merged. -- -- We treat unhandled patterns as if they are exhaustively matched -- against (aka, they are seen as wildcards by the checker). This -- necessarily results in some false negatives, but no false positives. desugarMatch :: Members '[Fresh, Embed IO] r => TypedVar -> APattern -> Sem r [Guard] data Gdt [Grhs] :: Int -> Gdt [Branch] :: Gdt -> Gdt -> Gdt [Guarded] :: Guard -> Gdt -> Gdt type Guard = (TypedVar, GuardConstraint) data GuardConstraint [GMatch] :: DataCon -> [TypedVar] -> GuardConstraint [GWasOriginally] :: TypedVar -> GuardConstraint newtype Literal Literal :: (TypedVar, LitCond) -> Literal data LitCond [LitMatch] :: DataCon -> [TypedVar] -> LitCond [LitNot] :: DataCon -> LitCond [LitWasOriginally] :: TypedVar -> LitCond data Ant [AGrhs] :: [NormRefType] -> Int -> Ant [ABranch] :: Ant -> Ant -> Ant ua :: Members '[Fresh, Reader TyDefCtx] r => [NormRefType] -> Gdt -> Sem r ([NormRefType], Ant) addLitMulti :: Members '[Fresh, Reader TyDefCtx] r => [NormRefType] -> Literal -> Sem r [NormRefType] addLiteral :: Members '[Fresh, Reader TyDefCtx] r => NormRefType -> Literal -> MaybeT (Sem r) NormRefType data InhabPat [IPIs] :: DataCon -> [InhabPat] -> InhabPat [IPNot] :: [DataCon] -> InhabPat mkIPMatch :: DataCon -> [InhabPat] -> InhabPat findInhabitants :: Members '[Fresh, Reader TyDefCtx] r => [NormRefType] -> [TypedVar] -> Sem r (Possibilities [InhabPat]) findAllForNref :: Members '[Fresh, Reader TyDefCtx] r => NormRefType -> [TypedVar] -> Sem r (Possibilities [InhabPat]) findVarInhabitants :: Members '[Fresh, Reader TyDefCtx] r => TypedVar -> NormRefType -> Sem r (Possibilities InhabPat) findRedundant :: Members '[Fresh, Reader TyDefCtx] r => Ant -> [TypedVar] -> Sem r [Int] data ExamplePat [ExamplePat] :: DataCon -> [ExamplePat] -> ExamplePat -- | Less general version of the above inhabitant finding function returns -- a maximum of 3 possible args lists that haven't been matched against, -- as to not overwhelm new users of the language. This is essentially a -- DFS, and it has a bad habit of trying to build infinite lists whenever -- it can, so we give it a max depth of 32 If we reach 32 levels of -- nested dataconstructors in this language, it is pretty safe to assume -- we were chasing after an infinite structure findPosExamples :: Members '[Fresh, Reader TyDefCtx] r => [NormRefType] -> [TypedVar] -> Sem r [[ExamplePat]] findAllPosForNref :: Members '[Fresh, Reader TyDefCtx] r => Int -> NormRefType -> [TypedVar] -> Sem r (Possibilities [ExamplePat]) findVarPosExamples :: Members '[Fresh, Reader TyDefCtx] r => Int -> TypedVar -> NormRefType -> Sem r (Possibilities ExamplePat) getPosFrom :: Type -> TyDefCtx -> [DataCon] -> [DataCon] mkExampleMatch :: DataCon -> [ExamplePat] -> ExamplePat instance GHC.Classes.Eq Disco.Exhaustiveness.GuardConstraint instance GHC.Show.Show Disco.Exhaustiveness.GuardConstraint instance GHC.Classes.Eq Disco.Exhaustiveness.Gdt instance GHC.Show.Show Disco.Exhaustiveness.Gdt instance GHC.Classes.Ord Disco.Exhaustiveness.LitCond instance GHC.Classes.Eq Disco.Exhaustiveness.LitCond instance GHC.Show.Show Disco.Exhaustiveness.LitCond instance GHC.Show.Show Disco.Exhaustiveness.Ant instance GHC.Classes.Ord Disco.Exhaustiveness.InhabPat instance GHC.Classes.Eq Disco.Exhaustiveness.InhabPat instance GHC.Show.Show Disco.Exhaustiveness.InhabPat instance GHC.Show.Show Disco.Exhaustiveness.ExamplePat -- | Desugaring the typechecked surface language to a (still typed) simpler -- language. module Disco.Desugar -- | Run a desugaring computation. runDesugar :: Sem '[Fresh] a -> a -- | Desugar a definition (consisting of a collection of pattern clauses -- with bodies) into a core language term. desugarDefn :: Member Fresh r => Defn -> Sem r DTerm -- | Desugar a typechecked term. desugarTerm :: Member Fresh r => ATerm -> Sem r DTerm -- | Desugar a property by wrapping its corresponding term in a test frame -- to catch its exceptions & convert booleans to props. desugarProperty :: Member Fresh r => AProperty -> Sem r DTerm -- | Desugar a branch of a case expression. desugarBranch :: Member Fresh r => ABranch -> Sem r DBranch -- | Desugar the list of guards in one branch of a case expression. Pattern -- guards essentially remain as they are; boolean guards get turned into -- pattern guards which match against true. desugarGuards :: Member Fresh r => Telescope AGuard -> Sem r (Telescope DGuard) -- | Compiling the typechecked, desugared AST to the untyped core language. module Disco.Compile -- | Utility function to desugar and compile a thing, given a desugaring -- function for it. compileThing :: (a -> Sem '[Fresh] DTerm) -> a -> Core -- | Compile a typechecked term (ATerm) directly to a Core -- term, by desugaring and then compiling. compileTerm :: ATerm -> Core -- | Compile a typechecked property (AProperty) directly to a -- Core term, by desugaring and then compilling. compileProperty :: AProperty -> Core -- | Compile a context of typechecked definitions (Defn) to a -- sequence of compiled Core bindings, such that the body of each -- binding depends only on previous ones in the list. First topologically -- sorts the definitions into mutually recursive groups, then compiles -- recursive definitions specially in terms of delay and -- force. compileDefns :: Ctx ATerm Defn -> [(QName Core, Core)] -- | Compile a group of mutually recursive definitions, using -- delay to compile recursion via references to memory cells. compileDefnGroup :: Member Fresh r => [(QName ATerm, Defn)] -> Sem r [(QName Core, Core)] -- | Compile a typechecked, desugared DTerm to an untyped -- Core term. compileDTerm :: Member Fresh r => DTerm -> Sem r Core -- | Compile a natural number. A separate function is needed in case the -- number is of a finite type, in which case we must mod it by its type. -- compileNat :: Member Fresh r => Type -> Integer -> Sem r Core -- compileNat (TyFin n) x = return $ CNum Fraction ((x mod n) % 1) -- compileNat _ x = return $ CNum Fraction (x % 1) -- -- Compile a primitive. Typically primitives turn into a corresponding -- function constant in the core language, but sometimes the particular -- constant it turns into may depend on the type. compilePrim :: Member Fresh r => Type -> Prim -> Sem r Core compilePrimErr :: Prim -> Type -> a desugaredPrimErr :: Prim -> Type -> a -- | Compile a case expression of type τ to a core language expression of -- type (Unit → τ), in order to delay evaluation until explicitly -- applying it to the unit value. compileCase :: Member Fresh r => [DBranch] -> Sem r Core -- | Compile a branch of a case expression of type τ to a core language -- expression of type (Unit → τ) → τ. The idea is that it takes a failure -- continuation representing the subsequent branches in the case -- expression. If the branch succeeds, it just returns the associated -- expression of type τ; if it fails, it calls the continuation to -- proceed with the case analysis. compileBranch :: Member Fresh r => DBranch -> Sem r Core -- | compileGuards takes a list of guards, the name of the failure -- continuation of type (Unit → τ), and a Core term of type τ to return -- in the case of success, and compiles to an expression of type τ which -- evaluates the guards in sequence, ultimately returning the given -- expression if all guards succeed, or calling the failure continuation -- at any point if a guard fails. compileGuards :: Member Fresh r => [DGuard] -> Name Core -> Core -> Sem r Core -- | compileMatch takes a pattern, the compiled scrutinee, the name -- of the failure continuation, and a Core term representing the -- compilation of any guards which come after this one, and returns a -- Core expression of type τ that performs the match and either calls the -- failure continuation in the case of failure, or the rest of the guards -- in the case of success. compileMatch :: Member Fresh r => DPattern -> Core -> Name Core -> Core -> Sem r Core -- | Compile a unary operator. compileUOp :: Type -> UOp -> Core -- | Compile a binary operator. This function needs to know the types of -- the arguments and result since some operators are overloaded and -- compile to different code depending on their type. -- -- 
--   arg1 ty -> arg2 ty -> result ty -> op -> result
--
compileBOp :: Type -> Type -> Type -> BOp -> Core -- | Properties of disco functions. module Disco.Property -- | Select samples from an enumeration according to a search type. Also -- returns a SearchType describing the results, which may be -- Exhaustive if the enumeration is no larger than the number of -- samples requested. generateSamples :: Member Random r => SearchType -> IEnumeration a -> Sem r ([a], SearchType) -- | Toggles which outcome (finding or not finding the thing being searched -- for) qualifies as success, without changing the thing being searched -- for. invertMotive :: SearchMotive -> SearchMotive -- | Flips the success or failure status of a PropResult, leaving -- the explanation unchanged. invertPropResult :: TestResult -> TestResult prettyTestResult :: Members '[Input TyDefCtx, LFresh, Reader PA] r => AProperty -> TestResult -> Sem r (Doc ann) -- | CESK machine interpreter for Disco. module Disco.Interpret.CESK -- | The CESK machine has two basic kinds of states. data CESK -- | Run a CESK machine to completion. runCESK :: Members '[Fresh, Random, State Mem] r => CESK -> Sem r (Either EvalError Value) -- | Advance the CESK machine by one step. step :: Members '[Fresh, Random, State Mem] r => CESK -> Sem r CESK eval :: Members '[Random, Error EvalError, Input Env, State Mem] r => Core -> Sem r Value evalApp :: Members '[Random, Error EvalError, State Mem] r => Value -> [Value] -> Sem r Value runTest :: Members '[Random, Error EvalError, Input Env, State Mem] r => Int -> AProperty -> Sem r TestResult instance GHC.Show.Show Disco.Interpret.CESK.Frame instance GHC.Show.Show Disco.Interpret.CESK.CESK -- | Top-level evaluation utilities. module Disco.Eval -- | Effects needed for evaluation. type EvalEffects = [Error EvalError, Random, LFresh, Output (Message ()), State Mem] -- | All effects needed for the top level + evaluation. type DiscoEffects = AppendEffects EvalEffects TopEffects data DiscoConfig initDiscoConfig :: DiscoConfig debugMode :: Iso' DiscoConfig Bool -- | A record of information about the current top-level environment. data TopInfo replModInfo :: Lens' TopInfo ModuleInfo topEnv :: Lens' TopInfo Env topModMap :: Lens' TopInfo (Map ModuleName ModuleInfo) lastFile :: Lens' TopInfo (Maybe FilePath) discoConfig :: Lens' TopInfo DiscoConfig -- | Run a top-level computation. runDisco :: DiscoConfig -> (forall r. Members DiscoEffects r => Sem r ()) -> IO () -- | Run a typechecking computation, providing it with local contexts -- (initialized to the provided arguments) for variable types and type -- definitions. runTCM :: Member (Error DiscoError) r => TyCtx -> TyDefCtx -> Sem (Reader TyCtx ': (Reader TyDefCtx ': (Fresh ': (Error LocTCError ': r)))) a -> Sem r a -- | Run a computation that needs an input environment, grabbing the -- current top-level environment from the TopInfo records. inputTopEnv :: Member (Input TopInfo) r => Sem (Input Env ': r) a -> Sem r a -- | Parse a module from a file, re-throwing a parse error if it fails. parseDiscoModule :: Members '[Error DiscoError, Embed IO] r => FilePath -> Sem r Module -- | 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 -- | Recursively loads a given module by first recursively loading and -- typechecking its imported modules, adding the obtained -- ModuleInfo records to a map from module names to info records, -- and then typechecking the parent module in an environment with access -- to this map. This is really just a depth-first search. -- -- The Resolver argument specifies where to look for imported -- modules. loadDiscoModule :: Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r => Bool -> Resolver -> FilePath -> Sem r ModuleInfo -- | Like loadDiscoModule, but start with an already parsed -- Module instead of loading a module from disk by name. Also, -- check it in 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 ann), Random, State Mem, Error DiscoError, Embed IO] r => Bool -> Resolver -> ModuleName -> Module -> Sem r ModuleInfo -- | Try loading the contents of a file from the filesystem, emitting an -- error if it's not found. loadFile :: Members '[Output (Message ann), Embed IO] r => FilePath -> Sem r (Maybe String) -- | Add things from the given module to the set of currently loaded -- things. addToREPLModule :: Members '[Error DiscoError, State TopInfo, Random, State Mem, Output (Message ann)] r => ModuleInfo -> Sem r () -- | 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 ann)] r => ModuleInfo -> Sem r () -- | Populate various pieces of the top-level info record (docs, type -- context, type and term definitions) from the ModuleInfo record -- corresponding to the currently loaded module, and load all the -- definitions into the current top-level environment. loadDefsFrom :: Members '[State TopInfo, Random, Error EvalError, State Mem] r => ModuleInfo -> Sem r () loadDef :: Members '[State TopInfo, Random, Error EvalError, State Mem] r => QName Core -> Core -> Sem r () -- | Defining and dispatching all commands/functionality available at the -- REPL prompt. module Disco.Interactive.Commands -- | Given a list of REPL commands and something typed at the REPL, pick -- the first command with a matching type-level tag and run its -- associated action. dispatch :: Members DiscoEffects r => REPLCommands -> SomeREPLExpr -> Sem r () -- | The list of all commands that can be used at the REPL. Resolution of -- REPL commands searches this list in order, which means -- ambiguous command prefixes (e.g. :t for :type) are resolved to the -- first matching command. discoCommands :: REPLCommands handleLoad :: Members (Error DiscoError ': (State TopInfo ': (Output (Message ()) ': (Embed IO ': EvalEffects)))) r => FilePath -> Sem r Bool -- | Try loading the contents of a file from the filesystem, emitting an -- error if it's not found. loadFile :: Members '[Output (Message ann), Embed IO] r => FilePath -> Sem r (Maybe String) -- | Given a list of available REPL commands and the currently enabled -- extensions, parse a string entered at the REPL prompt, returning -- either a parse error message or a parsed REPL expression. parseLine :: REPLCommands -> ExtSet -> String -> Either String SomeREPLExpr instance GHC.Show.Show Disco.Interactive.Commands.REPLCommandCategory instance GHC.Classes.Eq Disco.Interactive.Commands.REPLCommandCategory instance GHC.Show.Show Disco.Interactive.Commands.REPLCommandType instance GHC.Classes.Eq Disco.Interactive.Commands.REPLCommandType instance GHC.Classes.Eq Disco.Interactive.Commands.CmdTag instance GHC.Show.Show Disco.Interactive.Commands.CmdTag instance GHC.Show.Show Disco.Interactive.Commands.DocInput instance GHC.Show.Show Disco.Interactive.Commands.Level instance GHC.Classes.Ord Disco.Interactive.Commands.Level instance GHC.Classes.Eq Disco.Interactive.Commands.Level instance GHC.Show.Show (Disco.Interactive.Commands.REPLExpr c) -- | Definition of the command-line REPL interface for Disco. module Disco.Interactive.CmdLine -- | Command-line options for disco. data DiscoOpts DiscoOpts :: Bool -> Maybe String -> Maybe String -> Maybe String -> Bool -> DiscoOpts -- | Should we just print the version? [onlyVersion] :: DiscoOpts -> Bool -- | A single expression to evaluate [evaluate] :: DiscoOpts -> Maybe String -- | Execute the commands in a given file [cmdFile] :: DiscoOpts -> Maybe String -- | Check a file and then exit [checkFile] :: DiscoOpts -> Maybe String [debugFlag] :: DiscoOpts -> Bool discoOpts :: Parser DiscoOpts discoInfo :: ParserInfo DiscoOpts discoMain :: IO ()