Safe Haskell	Safe-Inferred
Language	Haskell2010

Synthesizer.Monad

Contents

Synth
Rules
Gamma
Delta
Omega
Restrictions
Constraints (WIP)
Names
Utilities
Other Types
Orphan instances

Synopsis

newtype Synth a = Synth {
- unSynth :: LogicT (RWST (Depth, [RestrictTag], Gamma, Omega) () (Int, Delta, [Ct]) TcM) a
}
runSynth :: Int -> Type -> Synth a -> TcM [a]
type Rule = String
rule :: Rule -> Type -> Synth a -> Synth a
(=>>) :: Type -> Type -> Type
newtype Gamma = Gamma {
- gamma :: [Prop]
}
inGamma :: Prop -> Synth a -> Synth a
getGamma :: Synth [Prop]
newtype Delta = Delta {
- delta :: [Prop]
}
pushDelta :: Prop -> Synth ()
delDelta :: Prop -> Synth ()
getDelta :: Synth [Prop]
setDelta :: [Prop] -> Synth ()
guardUsed :: SName -> Synth ()
newtype Omega = Omega {
- omega :: [Prop]
}
takeOmegaOr :: Synth a -> (Prop -> Synth a) -> Synth a
inOmega :: Prop -> Synth a -> Synth a
extendOmega :: [Prop] -> Synth a -> Synth a
data RestrictTag
- = ConstructTy Type
- | DeconstructTy Type
- | DecideLeftBangR Type Type
addRestriction :: RestrictTag -> Synth a -> Synth a
guardRestricted :: RestrictTag -> Synth ()
guardNotRestricted :: RestrictTag -> Synth ()
getConstraints :: Synth [Ct]
setConstraints :: [Ct] -> Synth ()
newWantedWithLoc :: CtLoc -> PredType -> TcM CtEvidence
solveConstraintsWithEq :: Type -> Type -> Synth ()
fresh :: Synth SName
guardWith :: String -> Bool -> Synth ()
forMFairConj :: MonadLogic m => [t] -> (t -> m a) -> m [a]
liftTcM :: TcM a -> Synth a
t4 :: (a, b, c, d) -> d
type Depth = Int
type SName = OccNameStr
type Prop = (SName, Type)

Synth

newtype Synth a #

Synthesis monad

Handles threading of state, propagation of reading state, backtracking, constraint solving, and friends

Constructors

Synth
Fields unSynth :: LogicT (RWST (Depth, [RestrictTag], Gamma, Omega) () (Int, Delta, [Ct]) TcM) a

Instances

Instances details

MonadFail Synth #
Instance details Defined in Synthesizer.Monad Methods fail :: String -> Synth a #
MonadIO Synth #
Instance details Defined in Synthesizer.Monad Methods liftIO :: IO a -> Synth a #
Alternative Synth #
Instance details Defined in Synthesizer.Monad Methods empty :: Synth a # (<\|>) :: Synth a -> Synth a -> Synth a # some :: Synth a -> Synth [a] # many :: Synth a -> Synth [a] #
Applicative Synth #
Instance details Defined in Synthesizer.Monad Methods pure :: a -> Synth a # (<>) :: Synth (a -> b) -> Synth a -> Synth b # liftA2 :: (a -> b -> c) -> Synth a -> Synth b -> Synth c # (>) :: Synth a -> Synth b -> Synth b # (<*) :: Synth a -> Synth b -> Synth a #
Functor Synth #
Instance details Defined in Synthesizer.Monad Methods fmap :: (a -> b) -> Synth a -> Synth b # (<$) :: a -> Synth b -> Synth a #
Monad Synth #
Instance details Defined in Synthesizer.Monad Methods (>>=) :: Synth a -> (a -> Synth b) -> Synth b # (>>) :: Synth a -> Synth b -> Synth b # return :: a -> Synth a #
MonadLogic Synth #
Instance details Defined in Synthesizer.Monad Methods msplit :: Synth a -> Synth (Maybe (a, Synth a)) interleave :: Synth a -> Synth a -> Synth a (>>-) :: Synth a -> (a -> Synth b) -> Synth b once :: Synth a -> Synth a lnot :: Synth a -> Synth () ifte :: Synth a -> (a -> Synth b) -> Synth b -> Synth b
MonadState (Int, Delta, [Ct]) Synth #
Instance details Defined in Synthesizer.Monad Methods get :: Synth (Int, Delta, [Ct]) # put :: (Int, Delta, [Ct]) -> Synth () # state :: ((Int, Delta, [Ct]) -> (a, (Int, Delta, [Ct]))) -> Synth a #
MonadReader (Depth, [RestrictTag], Gamma, Omega) Synth #
Instance details Defined in Synthesizer.Monad Methods ask :: Synth (Depth, [RestrictTag], Gamma, Omega) # local :: ((Depth, [RestrictTag], Gamma, Omega) -> (Depth, [RestrictTag], Gamma, Omega)) -> Synth a -> Synth a # reader :: ((Depth, [RestrictTag], Gamma, Omega) -> a) -> Synth a #

runSynth :: Int -> Type -> Synth a -> TcM [a] #

Run a synthesis computation.

Receives the amount of results to observe, the type of the recursive call (small hack while I don't have the module info), and the synthesis computation

Rules

type Rule = String #

A Rule is a string e.g. "-oR", but could also eventually be a custom datatype

rule :: Rule -> Type -> Synth a -> Synth a #

Run computation where the current rule is being applied to the given type

This is used to track the depth of the proof, and for logging

(=>>) :: Type -> Type -> Type #

From two types (a,b) create a new type (a => b) for usage with rule

Used for representing e.g. left focus => synth goal

Gamma

newtype Gamma #

Unrestricted hypothesis (Γ)

Constructors

Gamma
Fields gamma :: [Prop]

Instances

Instances details

Show Gamma #
Instance details Defined in Synthesizer.Monad Methods showsPrec :: Int -> Gamma -> ShowS # show :: Gamma -> String # showList :: [Gamma] -> ShowS #
Eq Gamma #
Instance details Defined in Synthesizer.Monad Methods (==) :: Gamma -> Gamma -> Bool # (/=) :: Gamma -> Gamma -> Bool #
Show ([RestrictTag], Gamma, Omega) #
Instance details Defined in Synthesizer.Monad Methods showsPrec :: Int -> ([RestrictTag], Gamma, Omega) -> ShowS # show :: ([RestrictTag], Gamma, Omega) -> String # showList :: [([RestrictTag], Gamma, Omega)] -> ShowS #
MonadReader (Depth, [RestrictTag], Gamma, Omega) Synth #
Instance details Defined in Synthesizer.Monad Methods ask :: Synth (Depth, [RestrictTag], Gamma, Omega) # local :: ((Depth, [RestrictTag], Gamma, Omega) -> (Depth, [RestrictTag], Gamma, Omega)) -> Synth a -> Synth a # reader :: ((Depth, [RestrictTag], Gamma, Omega) -> a) -> Synth a #

inGamma :: Prop -> Synth a -> Synth a #

Run a computation with additional proposition in gamma

getGamma :: Synth [Prop] #

Get the unrestricted context

Delta

newtype Delta #

Linear hypothesis (not left asynchronous) (Δ)

Constructors

Delta
Fields delta :: [Prop]

Instances

Instances details

Show Delta #
Instance details Defined in Synthesizer.Monad Methods showsPrec :: Int -> Delta -> ShowS # show :: Delta -> String # showList :: [Delta] -> ShowS #
Eq Delta #
Instance details Defined in Synthesizer.Monad Methods (==) :: Delta -> Delta -> Bool # (/=) :: Delta -> Delta -> Bool #
MonadState (Int, Delta, [Ct]) Synth #
Instance details Defined in Synthesizer.Monad Methods get :: Synth (Int, Delta, [Ct]) # put :: (Int, Delta, [Ct]) -> Synth () # state :: ((Int, Delta, [Ct]) -> (a, (Int, Delta, [Ct]))) -> Synth a #

pushDelta :: Prop -> Synth () #

Add a proposition to the linear context

delDelta :: Prop -> Synth () #

Remove a proposition from the linear context

getDelta :: Synth [Prop] #

Get the linear context

setDelta :: [Prop] -> Synth () #

Set the linear context

guardUsed :: SName -> Synth () #

This computation succeeds when

Omega

newtype Omega #

Ordered (linear?) hypothesis (Ω)

Constructors

Omega
Fields omega :: [Prop]

Instances

Instances details

Show Omega #
Instance details Defined in Synthesizer.Monad Methods showsPrec :: Int -> Omega -> ShowS # show :: Omega -> String # showList :: [Omega] -> ShowS #
Eq Omega #
Instance details Defined in Synthesizer.Monad Methods (==) :: Omega -> Omega -> Bool # (/=) :: Omega -> Omega -> Bool #
Show ([RestrictTag], Gamma, Omega) #
Instance details Defined in Synthesizer.Monad Methods showsPrec :: Int -> ([RestrictTag], Gamma, Omega) -> ShowS # show :: ([RestrictTag], Gamma, Omega) -> String # showList :: [([RestrictTag], Gamma, Omega)] -> ShowS #
MonadReader (Depth, [RestrictTag], Gamma, Omega) Synth #
Instance details Defined in Synthesizer.Monad Methods ask :: Synth (Depth, [RestrictTag], Gamma, Omega) # local :: ((Depth, [RestrictTag], Gamma, Omega) -> (Depth, [RestrictTag], Gamma, Omega)) -> Synth a -> Synth a # reader :: ((Depth, [RestrictTag], Gamma, Omega) -> a) -> Synth a #

takeOmegaOr :: Synth a -> (Prop -> Synth a) -> Synth a #

Take a proposition from the omega context: * If one exists, pass it to the 2nd argument (computation using proposition) * If none does, run the 1st argument (computation without proposition from omega)

In case a proposition is taken from omega, the computation run won't have it in the omega context anymore

inOmega :: Prop -> Synth a -> Synth a #

Run a computation with an additional proposition in omega

extendOmega :: [Prop] -> Synth a -> Synth a #

Extend a computation with additional propositions in omega

Restrictions

data RestrictTag #

Restrictions to conduct synthesis

Constructors

ConstructTy Type	Restriction on Constructing Type
DeconstructTy Type	Restriction on Deonstructing Type
DecideLeftBangR Type Type	Restriction on "Deciding-Left-Bang" on X to synthesize Y

Instances

Instances details

Show RestrictTag #
Instance details Defined in Synthesizer.Monad Methods showsPrec :: Int -> RestrictTag -> ShowS # show :: RestrictTag -> String # showList :: [RestrictTag] -> ShowS #
Eq RestrictTag #
Instance details Defined in Synthesizer.Monad Methods (==) :: RestrictTag -> RestrictTag -> Bool # (/=) :: RestrictTag -> RestrictTag -> Bool #
Show ([RestrictTag], Gamma, Omega) #
Instance details Defined in Synthesizer.Monad Methods showsPrec :: Int -> ([RestrictTag], Gamma, Omega) -> ShowS # show :: ([RestrictTag], Gamma, Omega) -> String # showList :: [([RestrictTag], Gamma, Omega)] -> ShowS #
MonadReader (Depth, [RestrictTag], Gamma, Omega) Synth #
Instance details Defined in Synthesizer.Monad Methods ask :: Synth (Depth, [RestrictTag], Gamma, Omega) # local :: ((Depth, [RestrictTag], Gamma, Omega) -> (Depth, [RestrictTag], Gamma, Omega)) -> Synth a -> Synth a # reader :: ((Depth, [RestrictTag], Gamma, Omega) -> a) -> Synth a #

addRestriction :: RestrictTag -> Synth a -> Synth a #

Run a computation with an additional restriction

guardRestricted :: RestrictTag -> Synth () #

Guard that a certain restriction exists

i.e. if the given restriction is already in place, the computation suceeds, otherwise, the given restriction isn't in place, and the computation fails with empty

guardNotRestricted :: RestrictTag -> Synth () #

Guard that a certain restriction hasn't been applied

i.e. if the given restriction doesn't exist, the computation suceeds, otherwise, the given restriction is already in place, and the computation fails with empty

Constraints (WIP)

getConstraints :: Synth [Ct] #

setConstraints :: [Ct] -> Synth () #

newWantedWithLoc :: CtLoc -> PredType -> TcM CtEvidence #

solveConstraintsWithEq :: Type -> Type -> Synth () #

Add a constraint to the list of constraints and solve it Failing if the constraints can't be solved with this addition

Names

fresh :: Synth SName #

Generate a fresh name

Example: a <- fresh return (var a)

Utilities

guardWith :: String -> Bool -> Synth () #

Like guard but emit given string as failure message upon failure

forMFairConj :: MonadLogic m => [t] -> (t -> m a) -> m [a] #

forM but instead of (>>=) use (>>-) for fair conjunction

See (>>-) in LogicT

liftTcM :: TcM a -> Synth a #

Lift a TcM computation into a Synth one

t4 :: (a, b, c, d) -> d #

Get 4th value of tuple of size 4

Other Types

type Depth = Int #

type SName = OccNameStr #

type Prop = (SName, Type) #

Orphan instances

Show Type #
Instance details Methods showsPrec :: Int -> Type -> ShowS # show :: Type -> String # showList :: [Type] -> ShowS #
Show Prop #
Instance details Methods showsPrec :: Int -> Prop -> ShowS # show :: Prop -> String # showList :: [Prop] -> ShowS #
Eq Type #
Instance details Methods (==) :: Type -> Type -> Bool # (/=) :: Type -> Type -> Bool #