Language.Symantic.Compiling.Beta

Beta-reduction of Terms.

Documentation

betaTerm :: forall src ss es vs fun arg. SourceInj (TypeVT src) src => Constable (->) => Term src ss es vs (fun :: Type) -> Term src ss es vs (arg :: Type) -> Either (Error_Beta src) (TermT src ss es vs)

Term application: apply second given TermT to the first, applying embedded TeSyms, or return an error.

betaTerms :: SourceInj (TypeVT src) src => Constable (->) => BinTree (TermVT src ss es) -> Either (Error_Beta src) (TermVT src ss es)

Collapse given BinTree of TermVTs to compute a resulting TermVT, if possible.

Type Error_Beta

data Error_Beta src

Constructors

Error_Beta_Term_not_a_function (TypeVT src)

Error_Beta_Type_mismatch (TypeVT src) (TypeVT src)

Error_Beta_Unify (Error_Unify src)

Cannot unify the expected Type of the argument of the function, with the Type of the argument.

Instances

Source src => Eq (Error_Beta src)

Methods

(==) :: Error_Beta src -> Error_Beta src -> Bool

(/=) :: Error_Beta src -> Error_Beta src -> Bool

Source src => Show (Error_Beta src)

Methods

showsPrec :: Int -> Error_Beta src -> ShowS

show :: Error_Beta src -> String

showList :: [Error_Beta src] -> ShowS

ErrorInj (Error_Unify src) (Error_Beta src)

Methods

errorInj :: Error_Unify src -> Error_Beta src

ErrorInj (Error_Beta src) (Error_Beta src)

Methods

errorInj :: Error_Beta src -> Error_Beta src

ErrorInj (Error_Beta src) (Error_Term src)

Methods

errorInj :: Error_Beta src -> Error_Term src