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

Safe HaskellSafe




Call patterns.

A call pattern describes the sequence of objects that are eliminated by some object when we apply it, and before it starts constructing new values.

Constructor (+ve)             Eliminator (-ve)
 /x.  (type   abstraction)    @'    (type   application)
  x.  (object abstraction)    @     (object application) 
 box   (suspend evaluation)   run   (commence evaluation)


Call constructors

data Cons n Source #

One component of the call pattern of a super. This is the "outer wrapper" of the computation,

With /(a : k). (x : t). box (x + 1) the call pattern consists of the two lambdas and the box. These three things need to be eliminated before we can construct any new values.


ConsType (Bind n)

A type lambda that needs a type of this kind.

ConsValue (Type n)

A value lambda that needs a value of this type.


A suspended expression that needs to be run.


Show n => Show (Cons n) Source # 


showsPrec :: Int -> Cons n -> ShowS #

show :: Cons n -> String #

showList :: [Cons n] -> ShowS #

isConsType :: Cons n -> Bool Source #

Check if this is an ConsType.

isConsValue :: Cons n -> Bool Source #

Check if this is an ElimType.

isConsBox :: Cons n -> Bool Source #

Check if this is an ElimType.

takeCallConsFromExp :: Exp a n -> [Cons n] Source #

Get the call pattern of an expression.

takeCallConsFromType :: Type n -> [Cons n] Source #

Infer the call pattern of an expression from its type. If the type has a function constructor then we assume there is a corresponding lambda abstraction in the expression, and so on.

splitStdCallCons :: [Cons n] -> Maybe ([Cons n], [Cons n], [Cons n]) Source #

Like splitStdCallElim, but for the constructor side.

takeStdCallConsFromTypeArity Source #


:: Type n

Type of super

-> Int

Number of type parameters.

-> Int

Number of value parameters.

-> Int

Number of boxings.

-> Maybe [Cons n] 

Given the type of a super, and the number of type parameters, value parameters and boxings, produce the corresponding list of call constructors.


      [| forall (a : k1) (b : k2). a -> b -> S e b |] 
      2 2 1
   => [ ConsType  [|k1|], ConsType  [|k2|]
      , ConsValue [|a],  ConsValue [|b|]
      , ConsBox ]

When we're considering the parts of the type, if the given arity does not match what is in the type then Nothing.

Call eliminators

data Elim a n Source #

One component of a super call.


ElimType a a (Type n)

Give a type to a type lambda.

ElimValue a (Exp a n)

Give a value to a value lambda.

ElimRun a

Run a suspended computation.


(Show a, Show n) => Show (Elim a n) Source # 


showsPrec :: Int -> Elim a n -> ShowS #

show :: Elim a n -> String #

showList :: [Elim a n] -> ShowS #

isElimType :: Elim a n -> Bool Source #

Check if this is an ElimType.

isElimValue :: Elim a n -> Bool Source #

Check if this is an ElimType.

isElimRun :: Elim a n -> Bool Source #

Check if this is an ElimType.

takeCallElim :: Exp a n -> (Exp a n, [Elim a n]) Source #

Split the application of some object into the object being applied and its eliminators.

applyElim :: Exp a n -> Elim a n -> Exp a n Source #

Apply an eliminator to an expression.

splitStdCallElims :: [Elim a n] -> Maybe ([Elim a n], [Elim a n], [Elim a n]) Source #

Group eliminators into sets for a standard call.

The standard call sequence is a list of type arguments, followed by some objects, and optionally running the result suspension.

run f [T1] [T2] x1 x2

If f is a super, and this is a saturating call then the super header will look like the following:

f = (t1. t2. v1. v2. box. body)


elimForCons :: Elim a n -> Cons n -> Bool Source #

Check if this an eliminator for the given constructor. This only checks the general form of the eliminator and constructor, not the exact types or kinds.

dischargeConsWithElims :: Ord n => [Cons n] -> [Elim a n] -> ([Cons n], [Elim a n]) Source #

Given lists of constructors and eliminators, check if the eliminators satisfy the constructors, and return any remaining unmatching constructors and eliminators.

We assume that the application is well typed and that applying the given eliminators will not cause variable capture.

dischargeTypeWithElims :: Ord n => Type n -> [Elim a n] -> Maybe (Type n) Source #

Given a type of a function and eliminators, discharge foralls, abstractions and boxes to get the result type of performing the application.

We assume that the application is well typed.