Safe Haskell | Safe |
---|---|
Language | Haskell98 |
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)
- data Cons n
- isConsType :: Cons n -> Bool
- isConsValue :: Cons n -> Bool
- isConsBox :: Cons n -> Bool
- takeCallConsFromExp :: Exp a n -> [Cons n]
- takeCallConsFromType :: Type n -> [Cons n]
- splitStdCallCons :: [Cons n] -> Maybe ([Cons n], [Cons n], [Cons n])
- takeStdCallConsFromTypeArity :: Type n -> Int -> Int -> Int -> Maybe [Cons n]
- data Elim a n
- isElimType :: Elim a n -> Bool
- isElimValue :: Elim a n -> Bool
- isElimRun :: Elim a n -> Bool
- takeCallElim :: Exp a n -> (Exp a n, [Elim a n])
- applyElim :: Exp a n -> Elim a n -> Exp a n
- splitStdCallElims :: [Elim a n] -> Maybe ([Elim a n], [Elim a n], [Elim a n])
- elimForCons :: Elim a n -> Cons n -> Bool
- dischargeConsWithElims :: Ord n => [Cons n] -> [Elim a n] -> ([Cons n], [Elim a n])
- dischargeTypeWithElims :: Ord n => Type n -> [Elim a n] -> Maybe (Type n)
Call constructors
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.
isConsType :: Cons n -> Bool Source
Check if this is an ConsType
.
isConsValue :: 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.
Example:
takeStdCallConsFromType [| 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
One component of a super call.
isElimType :: Elim a n -> Bool Source
Check if this is an ElimType
.
isElimValue :: 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.
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)
Matching
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.