ddc-core-0.4.1.3: Disciplined Disciple Compiler core language and type checker.

Safe HaskellNone

DDC.Core.Fragment

Contents

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.

Synopsis

Langauge fragments

data Fragment n err Source

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 -> [Token (Tok n)]

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

fragmentLexExp :: String -> Int -> String -> [Token (Tok 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) 

data Profile n Source

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.

zeroProfile :: Profile nSource

A language profile with no features or primitive operators.

This provides a simple first-order language.

Fragment features

data Feature Source

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.

Instances

Eq Feature 
Ord Feature 
Show Feature 

zeroFeatures :: FeaturesSource

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

Compliance

compliesSource

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.

compliesWithEnvsSource

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 Source

Class of things we can check language fragment compliance for.

data Error a n Source

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) 
(Pretty n, Eq n) => Pretty (Error a n)