| Safe Haskell | None |
|---|
DDC.Core.Fragment
Description
The ambient Disciple Core language is specialised to concrete languages
by adding primitive operations and optionally restricting the set of
available language features. This specialisation results in user-facing
language fragments such as Disciple Core Lite and Disciple Core Salt.
- data Fragment n err = Fragment {
- fragmentProfile :: Profile n
- fragmentExtension :: String
- fragmentReadName :: String -> Maybe n
- fragmentLexModule :: String -> Int -> String -> [Token (Tok n)]
- fragmentLexExp :: String -> Int -> String -> [Token (Tok n)]
- fragmentCheckModule :: forall a. Module a n -> Maybe (err a)
- fragmentCheckExp :: forall a. Exp a n -> Maybe (err a)
- data Profile n = Profile {
- profileName :: !String
- profileFeatures :: !Features
- profilePrimDataDefs :: !(DataDefs n)
- profilePrimKinds :: !(KindEnv n)
- profilePrimTypes :: !(TypeEnv n)
- profileTypeIsUnboxed :: !(Type n -> Bool)
- profileNameIsHole :: !(Maybe (n -> Bool))
- zeroProfile :: Profile n
- data Feature
- data Features = Features {
- featuresTrackedEffects :: Bool
- featuresTrackedClosures :: Bool
- featuresFunctionalEffects :: Bool
- featuresFunctionalClosures :: Bool
- featuresEffectCapabilities :: Bool
- featuresPartialPrims :: Bool
- featuresPartialApplication :: Bool
- featuresGeneralApplication :: Bool
- featuresNestedFunctions :: Bool
- featuresDebruijnBinders :: Bool
- featuresUnboundLevel0Vars :: Bool
- featuresUnboxedInstantiation :: Bool
- featuresNameShadowing :: Bool
- featuresUnusedBindings :: Bool
- featuresUnusedMatches :: Bool
- zeroFeatures :: Features
- complies :: (Ord n, Show n, Complies c) => Profile n -> c a n -> Maybe (Error a n)
- compliesWithEnvs :: (Ord n, Show n, Complies c) => Profile n -> KindEnv n -> TypeEnv n -> c a n -> Maybe (Error a n)
- class Complies c
- data Error a n
- = ErrorUnsupported !Feature
- | ErrorUndefinedPrim !n
- | ErrorUndefinedVar !n
- | ErrorShadowedBind !n
- | ErrorUnusedBind !n
- | ErrorNakedType !(Type n)
- | ErrorNakedWitness !(Witness a n)
Langauge fragments
Carries all the information we need to work on a particular fragment of the Disciple Core language.
Constructors
| Fragment | |
Fields
| |
Instances
| Show (Fragment n err) |
The fragment profile describes the language features and primitive operators available in the language.
Constructors
| Profile | |
Fields
| |
zeroProfile :: Profile nSource
A language profile with no features or primitive operators.
This provides a simple first-order language.
Fragment features
Language feature supported by a fragment.
Constructors
| TrackedEffects | Track effect type information. |
| TrackedClosures | Track closure type information. |
| FunctionalEffects | Attach latent effects to function types. |
| FunctionalClosures | Attach latent closures to function types. |
| EffectCapabilities | Treat effects as capabilities. |
| PartialPrims | Partially applied primitive operators. |
| PartialApplication | Partially applied functions |
| GeneralApplication | Function application where the thing being applied is not a variable. Most backend languages (like LLVM) don't support this. |
| NestedFunctions | Nested function bindings. The output of the lambda-lifter should not contain these. |
| DebruijnBinders | Debruijn binders. Most backends will want to use real names, instead of indexed binders. |
| UnboundLevel0Vars | Allow data and witness vars without binding occurrences if they are annotated directly with their types. This lets us work with open terms. |
| UnboxedInstantiation | Allow non-primitive functions to be instantiated at unboxed types. Our existing backends can't handle this, because boxed and unboxed objects have different representations. |
| NameShadowing | Allow name shadowing. |
| UnusedBindings | Allow unused named data and witness bindings. |
| UnusedMatches | Allow unused named matches. |
A flattened set of features, for easy lookup.
Constructors
| Features | |
Fields
| |
zeroFeatures :: FeaturesSource
An emtpy feature set, with all flags set to False.
Compliance
Arguments
| :: (Ord n, Show n, Complies c) | |
| => Profile n | Fragment profile giving the supported language features and primitive operators. |
| -> c a n | The thing to check. |
| -> Maybe (Error a n) |
Check whether a core thing complies with a language fragment profile.
Arguments
| :: (Ord n, Show n, Complies c) | |
| => Profile n | Fragment profile giving the supported language features and primitive operators. |
| -> KindEnv n | Starting kind environment. |
| -> TypeEnv n | Starting type environment. |
| -> c a n | The thing to check. |
| -> Maybe (Error a n) |
Like complies but with some starting environments.
Class of things we can check language fragment compliance for.
Language fragment compliance violations.
Constructors
| ErrorUnsupported !Feature | Found an unsupported language feature. |
| ErrorUndefinedPrim !n | Found an undefined primitive operator. |
| ErrorUndefinedVar !n | Found an unbound variable. |
| ErrorShadowedBind !n | Found a variable binder that shadows another one at a higher scope, but the profile doesn't permit this. |
| ErrorUnusedBind !n | Found a bound variable with no uses, but the profile doesn't permit this. |
| ErrorNakedType !(Type n) | Found a naked type that isn't used as a function argument. |
| ErrorNakedWitness !(Witness a n) | Found a naked witness that isn't used as a function argument. |