flocc-pffb

Stabilityexperimental
Maintainerdeveloper@flocc.net
Safe HaskellNone

Compiler.Types2.TermLanguage

Description

For more information please see http://www.flocc.net/

Synopsis

Documentation

trcUnifyCon :: Show a => a -> a

Tracer function for debugging displaying all constraints as they are unified

trcUnifySub :: Show a => a -> a

data Term l t

Data type for term language

Constructors

Var Idx 
UniVar Idx 
Ref Idx 
Term t [Term l t] 
LVar [l] Idx 
LUniVar [l] Idx 
LRef [l] Idx 
LTerm [l] t [Term l t] 

Instances

Eq t => Eq (Term l t) 
Ord t => Ord (Term l t) 
(Read l, Read t) => Read (Term l t) 
(Show l, Show t) => Show (Term l t) 
VarsIn (Term l t) 
Mappable (Term l t) 
(ShowP l, ShowP t) => ShowP (Term l t)

Implementation of show for terms

showPLabels :: ShowP l => [l] -> String

showLabels :: Show l => [l] -> String

getLabels :: Term l t -> [l]

labelTerm :: l -> Term l t -> Term l t

addLabelsToTerm :: [l] -> Term l t -> Term l t

addLabelsToTermRec :: [l] -> Term l t -> Term l t

labelTermRec :: l -> Term l t -> Term l t

stripTermLabels :: Term l t -> Term l t

mapTermM :: Monad m => (Term l t -> m (Term l t)) -> Term l t -> m (Term l t)

applyVarSubst takes a map of substitutions and a var id |and returns the substituted value if there is one, or |Var i if there isn't.

mapTermM f term. Applies f to all subterms, and then to the new terms |created by them.

termContains :: Eq t => t -> Term l t -> Bool

Allows terms to be compared

percentTermConcrete :: Term l t -> Float

Returns the percentage of the current term that is |concrete (i.e. not a term var).

getSubTerms :: (Ord t, Show t, Show l) => t -> Int -> Term l t -> Set (Term l t)

getSubTerms name offset. Gets all the nth type parameters of terms called |name.

data Scheme l t

Data type for term schemes, qualified terms in the language |(those with bound variables)

Constructors

Scheme [Idx] (Term l t) 

Instances

Eq t => Eq (Scheme l t) 
(Read l, Read t) => Read (Scheme l t) 
(Show l, Show t) => Show (Scheme l t) 
(ShowP t, ShowP l) => ShowP (Scheme l t)

Display a term scheme

Display a term scheme

getSchemeTerm :: Scheme l t -> Term l t

getFreeVarIdsInScheme :: Scheme l t -> [Idx]

Returns a list of free variables in a term scheme

generalizeTerm :: TermEnv l t -> Term l t -> Scheme l t

Generalize a term to make it a scheme

instantiateUniVars :: Monad m => Term l t -> StateT IdxSet m (Term l t)

Instantiates all unique vars with different ids, such that |two different unique vars will never equal each other.

instantiateScheme :: (Eq t, Monad m) => Scheme l t -> StateT IdxSet m (Term l t)

Instantiates a term scheme by replacing every qualified term variable |with a new variable.

applyToScheme :: (Term l t -> Term l t) -> Scheme l t -> Scheme l t

Applies a function that takes a Term to a Scheme containing a term

renumberScheme :: Eq t => Scheme l t -> Scheme l t

renumberScheme takes a scheme and replaces all integer var ids |with new 1-based ints.

renumberSchemes :: Eq t => [Scheme l t] -> [Scheme l t]

renumberSchemes takes a list of schemes and replaces all bound |integer var ids with new 1-based ones, and all free variables with |integer var ids that start at the number after the new maximum bound var id.

data IdTree

IdTree is a succinct type for simple id trees.

Constructors

IdTup [IdTree] 
IdLeaf Idx 
IdBlank 

getIdsInIdTree :: IdTree -> [Idx]

getIdsInIdTree takes an IdTree and returns a lift of |all id values it contains

getIdExprIdPairs :: (IdTree, Expr) -> [(Idx, Idx)]

getIdExprIdPairs zips together an IdTree and a tuple expression tree |returning a lift of pairs of id tree ids to expression ids.

data SchemeEx l t

SchemeEx is a type that extends term schemes to |have an extra tree of bound variables that can be |used within the term.

Constructors

SchemeEx IdTree (Scheme l t) 

Instances

Eq t => Eq (SchemeEx l t) 
(Read l, Read t) => Read (SchemeEx l t) 
(Show l, Show t) => Show (SchemeEx l t) 
(ShowP l, ShowP t) => ShowP (SchemeEx l t) 

getFreeVarIdsInSchemeEx :: SchemeEx l t -> [Idx]

Returns a list of free variables in a term scheme

generalizeTermEx :: TermEnv l t -> Term l t -> SchemeEx l t

Generalize a term to make it a SchemeEx

instantiateSchemeEx :: (Eq t, Monad m) => SchemeEx l t -> Expr -> StateT IdxSet m (Term l t)

Instantiates a term SchemeEx by replacing every qualified term variable |with a new variable, and every function application qualified variable |with a ref to that var id (or expression id).

instantiateSchemeEx2 :: (Eq t, Show t, Monad m, Show l) => SchemeEx l t -> StateT IdxSet m (Term l t)

instantiateSchemeEx2 takes an extended term scheme and returns a term.

schemeEnvToSchemeExEnv :: TermEnv l t -> [(Idx, SchemeEx l t)]

schemeEnvToSchemeExEnv

type TermEnv l t = [(Idx, Scheme l t)]

getFreeVarIdsInEnv :: TermEnv l t -> [Idx]

Get all unbound term vars in an environment

mapTermEnv :: (Scheme l t -> Scheme l t) -> TermEnv l t -> TermEnv l t

filterTermEnv :: ((Idx, Scheme l t) -> Bool) -> TermEnv l t -> TermEnv l t

lookupTerm :: (Show t, Show l) => TermEnv l t -> Idx -> Scheme l t

addTermToEnv :: TermEnv l t -> Scheme l t -> Idx -> TermEnv l t

updateTermInEnv :: TermEnv l t -> Scheme l t -> Idx -> TermEnv l t

Updates an entry in an environment to a new term, or adds it if it |doesn't already exist.

bindTermInState :: Monad a => Scheme l t -> Idx -> StateT (TermEnv l t) a (Scheme l t)

rebindTermInState :: Monad a => Scheme l t -> Idx -> StateT (TermEnv l t) a (Scheme l t)

Binds a new term to an id that already has a binding.

showTermFromEnv :: (Show t, Show l) => TermEnv l t -> Idx -> String

monadicOr :: Monad m => Bool -> Bool -> m Bool

occursInTerm :: Eq t => Term l t -> Term l t -> State (TermEnv l t) Bool

For terms a, b returns True iff a occurs somewhere in b

occursInTermTrans :: Eq t => Monad m => Term l t -> Term l t -> StateT (TermEnv l t) m Bool

occursInTermIgnoreRefs :: Eq t => Term l t -> Term l t -> Bool

For terms a, b returns True iff a occurs somewhere in b, ignoring ref nodes

newTermVarFromState :: Monad a => StateT IdxSet a (Term l t)

Returns a var with a new idx

bindNewTermVarInState :: Monad a => Idx -> StateT (TermEnv l t) (StateT IdxSet a) (Term l t)

Creates a new term var and binds it in the state env

type GenerateIdFunction = State IdxSet Idx

A function that generates a new Idx

renewTermVarIdsMemorized :: Term l t -> StateT (State IdxSet Idx, [(Idx, Idx)]) (State IdxSet) (Term l t)

Picks freshs var ids for all vars, whilst maintaining equalities within the term

renewTermVarIdsWithSubs :: Monad a => Term l t -> StateT IdxSet a (Term l t, [Subst (Term l t)])

Picks fresh var ids for all vars, returning the new term with vars substituted, and |the list of substitutions it applied

renewTermVarIds :: Monad a => Term l t -> StateT IdxSet a (Term l t)

data Subst t

Picks fresh var ids for vars in each term in the environment such that |no variable is used in more than one term in the environment, but |variable patterns are preserved for each term. renewTermVarsInEnv :: Monad a => TermEnv t -> StateT IdxSet a (TermEnv t) renewTermVarsInEnv env = do env' mapM (\(i,t) - do t' <- renewTermVarIds t ; return (i,t')) env return env'

Constructors

t :|-> t 

Instances

Eq t => Eq (Subst t) 
Show t => Show (Subst t) 
ShowP t => ShowP (Subst t) 

forAllSubs :: (Subst t -> a -> a) -> [Subst t] -> a -> a

Apply the function cumulatively to the argument |once for every argument in the subst list |in order of list left to right.

subInTerm :: Eq t => Subst (Term l t) -> Term l t -> Term l t

subInTermReturnAffected :: Eq t => Subst (Term l t) -> Term l t -> Either (Term l t) (Term l t)

Substitutes all occurances in term, returning the term in the left if it was affected |or in the right if it was not

subInScheme :: (Eq t, Show t, Show l) => Subst (Term l t) -> Scheme l t -> Scheme l t

If the substitution would substitute a bound variable, ignore it. |This is safe as in the unlikely event that a substitution involves the same |variable id as a qualified variable, the fact that its not free ensures it |was never supposed to be substituted as it should have no external visibility.

data Constr t

Constructors

t :=: t 

Instances

Functor Constr 
Eq t => Eq (Constr t) 
Read t => Read (Constr t) 
Show t => Show (Constr t) 
ShowP t => ShowP (Constr t) 

type WeightedConstr t = (Constr t, Int)

subInConstr :: Eq t => Subst (Term l t) -> Constr (Term l t) -> Constr (Term l t)

occursInConstr :: Eq t => Term l t -> Constr (Term l t) -> State (TermEnv l t) Bool

type UnifierExtension l t = TermEnv l t -> Constr (Term l t) -> Either [Constr (Term l t)] (Constr (Term l t))

A function that tries to expand a constraint, returning left with the expansion list |if it could, or right if it failed.

defaultUnifierExtension :: UnifierExtension l t

Always returns failure for the constraint

monadicUnify :: (Eq t, Show t, Show l) => [t] -> [Constr (Term l t)] -> StateT (UnifierExtension l t) (State (TermEnv l t)) (Either [Subst (Term l t)] (Constr (Term l t)))

Unify the set of constraints given the term environment used to resolve Ref terms, returns either |the set of substitutions in the left, or the constraint it failed on in the right. |monadicUnify ignoreToks constrs. ignoreToks are a list of tokens who's terms shouldn't be |unified by shape (i.e. broken down into constraints between parameters).

unifyConstraintsEx :: (Eq t, Show t, Show l) => [Constr (Term l t)] -> TermEnv l t -> UnifierExtension l t -> Either [Subst (Term l t)] (Constr (Term l t))

Unifies a set of constraints where a unifier extension function can be used

unifyConstraints :: (Eq t, Show t, Show l) => [Constr (Term l t)] -> TermEnv l t -> Either [Subst (Term l t)] (Constr (Term l t))

Unifies a set of constraints

type MonadicUnifierExtension l t m = TermEnv l t -> Constr (Term l t) -> m (Either [Constr (Term l t)] (Constr (Term l t)))

The type for a unifier extension that is monadic

type IdentityUnifierExtension l t = MonadicUnifierExtension l t Identity

The type of a unifier extention that only uses the Identity monadic

defaultMonadicUnifierExtension :: Monad m => MonadicUnifierExtension l t m

Default monadic unifier extension just fails of the constraint

monadicUnifyTrans :: (Eq t, Show t, Monad m, Show l) => [t] -> [Constr (Term l t)] -> StateT (MonadicUnifierExtension l t m) (StateT (TermEnv l t) m) (Either [Subst (Term l t)] (Constr (Term l t), [Subst (Term l t)]))

The unify function that permits nesting of monads |monadicUnifyTrans ignoreToks constrs. ignoreToks is a |list of tokens that shouldn't be broken down into a list |of constraints between their parameters.

unifyConstraintsEx2 :: (Eq t, Show t, Monad m, Show l) => [Constr (Term l t)] -> TermEnv l t -> MonadicUnifierExtension l t m -> m (Either [Subst (Term l t)] (Constr (Term l t), [Subst (Term l t)]))

Unifies a set of constraints where a monad can be passed to the extension function

monadicUnifyTrans2 :: (Eq t, Show t, Monad m, Show l) => [Constr (Term l t)] -> StateT (MonadicUnifierExtension l t m, Set Idx) (StateT (TermEnv l t) m) (Either [Subst (Term l t)] (Constr (Term l t)))

The unify function that permits nesting of monads, and takes a set of terminal |var ids which should not be expanded. This allows unification to ke place |for a subexpression rather than the entire program.

unifyConstraintsEx3 :: (Eq t, Show t, Monad m, Show l) => [Constr (Term l t)] -> TermEnv l t -> MonadicUnifierExtension l t m -> Set Idx -> m (Either [Subst (Term l t)] (Constr (Term l t)))

Unifies a set of constraints where a monad can be passed to the extension function, |and where a set of terminal var ids that won't be simplified during unification |can be passed to the constraint solver.

data FunctionToken t

Base class for tokens for term languages with function types and tuples

Constructors

FunTok 
TupTok 
Tok t 

Instances

labelArgTerm :: (Show l, Show t) => l -> Term l (FunctionToken t) -> Term l (FunctionToken t)

labelArgTermRec :: (Show l, Show t) => l -> Term l (FunctionToken t) -> Term l (FunctionToken t)

labelRanTerm :: (Show l, Show t) => l -> Term l (FunctionToken t) -> Term l (FunctionToken t)

labelRanTermRec :: (Show l, Show t) => l -> Term l (FunctionToken t) -> Term l (FunctionToken t)

showFunctionTerm :: (Show t, Show l) => Term l (FunctionToken t) -> String

Pretty print function term

showFunctionScheme :: (Show t, Show l) => Scheme l (FunctionToken t) -> String

Pretty print function scheme

type TermEnvStack l t = [TermEnv l t]

Type of a function that performs some var substitution on a FuncTokTerm type RenewFuncVarIdsFunction a t = Monad a => GenerateIdFunction -> FuncTokTerm t -> StateT [(Idx, Idx)] (StateT IdxSet a) (FuncTokTerm t)

Renews terms, whenever it comes across a new var it checks to see |if a there already exists a substitution for it, and if not creates a replacement renewFunVarIdsInTermMemorize :: (RenewFuncVarIdsFunction t) -> RenewFuncVarIdsFunction t renewFunVarIdsInTermMemorize funf genf term = case term of (Term FunTok [dom, ran]) -> funf genf term _ -> do return undefined

Renews terms, whenever comes across a var that exists in the substituion list |it substitutes it, otherwise it leaves it alone renewFunVarIdsInTermLookup :: (RenewFuncVarIdsFunction t) -> RenewFuncVarIdsFunction t renewFunVarIdsInTermLookup funf genf term = case term of (Term FunTok [dom, ran]) -> funf genf term _ -> do return undefined --(union [])

A stack of term environments

pushTermEnvInState :: Monad a => TermEnv l t -> StateT (TermEnvStack l t) a (TermEnv l t)

popTermEnvInState :: Monad a => StateT (TermEnvStack l t) a (TermEnvStack l t)

peekTermEnvInState :: Monad a => StateT (TermEnvStack l t) a (TermEnv l t)

lookupTermFromStack :: (Show t, Show l) => TermEnvStack l t -> Idx -> Maybe (Term l t)

lookupTermFromStackInState :: (Show t, Show l, Monad a) => Idx -> StateT (TermEnvStack l t) a (Maybe (Term l t))

lookupTermFromHeadInState :: (Show t, Show l, Monad a) => Idx -> StateT (TermEnvStack l t) a (Maybe (Term l t))

addTermToStackInState :: Monad a => Term l t -> Idx -> StateT (TermEnvStack l t) a ()

Adds a term binding to the TermEnvStack in the state

schemeModifier :: (Term l t -> Term l t) -> Scheme l t -> Scheme l t

modifyTermInStack :: (Term l t -> Term l t) -> Idx -> TermEnvStack l t -> Maybe (TermEnvStack l t)

Changes a term in one of the stack frames

modifyTermInStackOrError :: (Show t, Show l) => (Term l t -> Term l t) -> Idx -> TermEnvStack l t -> TermEnvStack l t

Changes term in stack frame or raises error if no term with the given id exists

modifyTermInStackState :: (Monad a, Show t, Show l) => (Term l t -> Term l t) -> Idx -> StateT (TermEnvStack l t) a ()

Changes a term in one of the stack frames in the state, or if no var with that id exists |in the stack, raises an error