DDC.Core.Fragment

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 Tetra and Disciple Core Salt.

Langauge fragments

data Fragment n err

Carries all the information we need to work on a particular fragment of the Disciple Core language.

Constructors

Fragment

Fields

• fragmentProfile :: Profile n

  Language profile for this fragment.

• fragmentExtension :: String

  File extension to use when dumping modules in this fragment.

• fragmentReadName :: String -> Maybe n

  Read a name.

• fragmentLexModule :: String -> Int -> String -> [Located (Token n)]

  Lex module source into tokens, given the source name and starting line number.

• fragmentLexExp :: String -> Int -> String -> [Located (Token n)]

  Lex expression source into tokens, given the source name and starting line number.

• fragmentCheckModule :: forall a. Module a n -> Maybe (err a)

  Perform language fragment specific checks on a module.

• fragmentCheckExp :: forall a. Exp a n -> Maybe (err a)

  Perform language fragment specific checks on an expression.

Instances

Show (Fragment n err)

Methods

showsPrec :: Int -> Fragment n err -> ShowS

show :: Fragment n err -> String

showList :: [Fragment n err] -> ShowS

mapProfileOfFragment :: (Profile n -> Profile n) -> Fragment n err -> Fragment n err

Apply a function to the profile in a fragment.

data Profile n

The fragment profile describes the language features and primitive operators available in the language.

Constructors

Profile

Fields

• profileName :: !String

  The name of this profile.

• profileFeatures :: !Features

  Permitted language features.

• profilePrimDataDefs :: !(DataDefs n)

  Primitive data type declarations.

• profilePrimKinds :: !(KindEnv n)

  Kinds of primitive types.

• profilePrimTypes :: !(TypeEnv n)

  Types of primitive operators.

• profileTypeIsUnboxed :: !(Type n -> Bool)

  Check whether a type is an unboxed type. Some fragments limit how these can be used.

• profileNameIsHole :: !(Maybe (n -> Bool))

  Check whether some name represents a hole that needs to be filled in by the type checker.

• profileMakeLiteralName :: Maybe (SourcePos -> Literal -> Bool -> Maybe n)

  Convert a literal to a name, given the source position, literal value and whether the literal should be taken as a language primitive (with a trailing #).

mapFeaturesOfProfile :: (Features -> Features) -> Profile n -> Profile n

Apply a function to the Features of a Profile.

zeroProfile :: Profile n

A language profile with no features or primitive operators.

This provides a simple first-order language.

Fragment features

data Feature

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.

ImplicitRun

Insert implicit run casts for effectful applications.

ImplicitBox

Insert implicit box casts for bodies of abstractions.

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.

GeneralLetRec

Recursive let-expressions where the right hand sides are not lambda abstractions.

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.

Instances

Eq Feature

Methods

(==) :: Feature -> Feature -> Bool

(/=) :: Feature -> Feature -> Bool

Ord Feature

Methods

compare :: Feature -> Feature -> Ordering

(<) :: Feature -> Feature -> Bool

(<=) :: Feature -> Feature -> Bool

(>) :: Feature -> Feature -> Bool

(>=) :: Feature -> Feature -> Bool

max :: Feature -> Feature -> Feature

min :: Feature -> Feature -> Feature

Show Feature

Methods

showsPrec :: Int -> Feature -> ShowS

show :: Feature -> String

showList :: [Feature] -> ShowS

data Features

A flattened set of features, for easy lookup.

Constructors

Features

Fields

• featuresTrackedEffects :: Bool
• featuresTrackedClosures :: Bool
• featuresFunctionalEffects :: Bool
• featuresFunctionalClosures :: Bool
• featuresEffectCapabilities :: Bool
• featuresImplicitRun :: Bool
• featuresImplicitBox :: Bool
• featuresPartialPrims :: Bool
• featuresPartialApplication :: Bool
• featuresGeneralApplication :: Bool
• featuresNestedFunctions :: Bool
• featuresGeneralLetRec :: Bool
• featuresDebruijnBinders :: Bool
• featuresUnboundLevel0Vars :: Bool
• featuresUnboxedInstantiation :: Bool
• featuresNameShadowing :: Bool
• featuresUnusedBindings :: Bool
• featuresUnusedMatches :: Bool

zeroFeatures :: Features

An emtpy feature set, with all flags set to False.

setFeature :: Feature -> Bool -> Features -> Features

Set a language Flag in the Profile.

Compliance

complies

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.

compliesWithEnvs

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 Complies c

Class of things we can check language fragment compliance for.

Minimal complete definition

compliesX

Instances

Complies Alt

Methods

compliesX :: (Ord n, Show n) => Profile n -> Env n -> Env n -> Context -> Alt a n -> CheckM a n (Set n, Set n)

Complies Exp

Methods

compliesX :: (Ord n, Show n) => Profile n -> Env n -> Env n -> Context -> Exp a n -> CheckM a n (Set n, Set n)

Complies Module

Methods

compliesX :: (Ord n, Show n) => Profile n -> Env n -> Env n -> Context -> Module a n -> CheckM a n (Set n, Set n)

data Error a n

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.

Instances

(Show a, Show n) => Show (Error a n)

Methods

showsPrec :: Int -> Error a n -> ShowS

show :: Error a n -> String

showList :: [Error a n] -> ShowS

(Pretty n, Eq n) => Pretty (Error a n)

Associated Types

data PrettyMode (Error a n) :: *

Methods

pprDefaultMode :: PrettyMode (Error a n)

ppr :: Error a n -> Doc

pprPrec :: Int -> Error a n -> Doc

pprModePrec :: PrettyMode (Error a n) -> Int -> Error a n -> Doc