Disco.Module

The ModuleInfo record representing a disco module, and functions to resolve the location of a module on disk.

Documentation

data LoadingMode

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.

Constructors

REPL

Standalone

data Defn

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 ...]

Constructors

Defn (Name ATerm) [Type] Type [Clause]

Instances

Data Defn

Defined in Disco.Module

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Defn -> c Defn

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Defn

toConstr :: Defn -> Constr

dataTypeOf :: Defn -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Defn)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn)

gmapT :: (forall b. Data b => b -> b) -> Defn -> Defn

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r

gmapQ :: (forall d. Data d => d -> u) -> Defn -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Defn -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Defn -> m Defn

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Defn -> m Defn

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Defn -> m Defn

Show Defn

Defined in Disco.Module

Methods

showsPrec :: Int -> Defn -> ShowS

show :: Defn -> String

showList :: [Defn] -> ShowS

Generic Defn

Defined in Disco.Module

Associated Types

type Rep Defn :: Type -> Type

Methods

from :: Defn -> Rep Defn x

to :: Rep Defn x -> Defn

Alpha Defn

Defined in Disco.Module

Methods

aeq' :: AlphaCtx -> Defn -> Defn -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Defn -> f Defn

close :: AlphaCtx -> NamePatFind -> Defn -> Defn

open :: AlphaCtx -> NthPatFind -> Defn -> Defn

isPat :: Defn -> DisjointSet AnyName

isTerm :: Defn -> All

isEmbed :: Defn -> Bool

nthPatFind :: Defn -> NthPatFind

namePatFind :: Defn -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Defn -> Defn

lfreshen' :: LFresh m => AlphaCtx -> Defn -> (Defn -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Defn -> m (Defn, Perm AnyName)

acompare' :: AlphaCtx -> Defn -> Defn -> Ordering

Pretty Defn

Defined in Disco.Module

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Defn -> Sem r Doc

Subst Type Defn

Defined in Disco.Module

Methods

isvar :: Defn -> Maybe (SubstName Defn Type)

isCoerceVar :: Defn -> Maybe (SubstCoerce Defn Type)

subst :: Name Type -> Type -> Defn -> Defn

substs :: [(Name Type, Type)] -> Defn -> Defn

type Rep Defn

Defined in Disco.Module

type Rep Defn = D1 ('MetaData "Defn" "Disco.Module" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (C1 ('MetaCons "Defn" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Name ATerm)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause]))))

type Clause = Bind [APattern] ATerm

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

eraseClause :: Clause -> Bind [Pattern] Term

data ModuleInfo

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.

Constructors

ModuleInfo

Fields

• _miName :: ModuleName
• _miImports :: Map ModuleName ModuleInfo
• _miNames :: [QName Term]
• _miDocs :: Ctx Term Docs
• _miProps :: Ctx ATerm [AProperty]
• _miTys :: TyCtx
• _miTydefs :: TyDefCtx
• _miTermdefs :: Ctx ATerm Defn
• _miTerms :: [(ATerm, PolyType)]
• _miExts :: ExtSet

Instances

Show ModuleInfo

Defined in Disco.Module

Methods

showsPrec :: Int -> ModuleInfo -> ShowS

show :: ModuleInfo -> String

showList :: [ModuleInfo] -> ShowS

Semigroup ModuleInfo

Defined in Disco.Module

Methods

(<>) :: ModuleInfo -> ModuleInfo -> ModuleInfo

sconcat :: NonEmpty ModuleInfo -> ModuleInfo

stimes :: Integral b => b -> ModuleInfo -> ModuleInfo

Monoid ModuleInfo

Defined in Disco.Module

Methods

mempty :: ModuleInfo

mappend :: ModuleInfo -> ModuleInfo -> ModuleInfo

mconcat :: [ModuleInfo] -> ModuleInfo

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)

withImports :: Monoid a => Getting a ModuleInfo a -> ModuleInfo -> a

Get something from a module and its direct imports.

allTys :: ModuleInfo -> TyCtx

Get the types of all names bound in a module and its direct imports.

allTydefs :: ModuleInfo -> TyDefCtx

Get all type definitions from a module and its direct imports.

emptyModuleInfo :: ModuleInfo

The empty module info record.

data Resolver

A data type indicating where we should look for Disco modules to be loaded.

Constructors

FromStdlib

Load only from the stdlib (standard lib modules)

FromDir FilePath

Load only from a specific directory (:load)

FromCwdOrStdlib

Load from current working dir or stdlib (import at REPL)

FromDirOrStdlib FilePath

Load from specific dir or stdlib (import in file)

withStdlib :: Resolver -> 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).

resolveModule :: Member (Embed IO) r => Resolver -> String -> Sem r (Maybe (FilePath, ModuleProvenance))

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.