Language.Symantic.Compiling.Term

Type Term

data Term src ss ts vs t where

Constructors

Term :: Type src vs q -> Type src vs t -> TeSym ss ts (q #> t) -> Term src ss ts vs (q #> t)

Instances

AllocVars Type (Term src ss ts)

Methods

allocVarsL :: Len Type len -> a vs x -> a ((Type ++ len) vs) x

allocVarsR :: Len Type len -> a vs x -> a ((Type ++ vs) len) x

Inj_Source (TermT src ss ts vs) src => TypeOf Type (Term src ss ts vs)

Methods

typeOf :: a t -> Type (Term src ss ts vs) (SourceOf (a t)) (VarsOf (a t)) t

Source src => Eq (Term src ss ts vs t)

Methods

(==) :: Term src ss ts vs t -> Term src ss ts vs t -> Bool

(/=) :: Term src ss ts vs t -> Term src ss ts vs t -> Bool

Source src => Show (Term src ss ts vs t)

Methods

showsPrec :: Int -> Term src ss ts vs t -> ShowS

show :: Term src ss ts vs t -> String

showList :: [Term src ss ts vs t] -> ShowS

Source src => Sourced (Term src ss ts vs t)

Methods

sourceOf :: Term src ss ts vs t -> SourceOf (Term src ss ts vs t)

setSource :: Term src ss ts vs t -> SourceOf (Term src ss ts vs t) -> Term src ss ts vs t

LenVars (Term src ss ts vs t)

Methods

lenVars :: Term src ss ts vs t -> Len Type (VarsOf (Term src ss ts vs t))

ExpandFam (Term src ss ts vs t)

Methods

expandFam :: Term src ss ts vs t -> Term src ss ts vs t

ConstsOf (Term src ss ts vs t)

Methods

constsOf :: Term src ss ts vs t -> Set (ConstC (SourceOf (Term src ss ts vs t)))

type SourceOf (Term src ss ts vs t)

type SourceOf (Term src ss ts vs t) = src

type VarsOf (Term src ss ts vs t)

type VarsOf (Term src ss ts vs t) = vs

typeOfTerm :: Source src => Term src ss ts vs t -> Type src vs t

Type TermT

data TermT src ss ts vs

Term with existentialized Type.

Constructors

TermT (Term src ss ts vs t)

Instances

Source src => Show (TermT src ss ts vs)

Methods

showsPrec :: Int -> TermT src ss ts vs -> ShowS

show :: TermT src ss ts vs -> String

showList :: [TermT src ss ts vs] -> ShowS

Type TermVT

data TermVT src ss ts

Term with existentialized Vars and Type.

Constructors

TermVT (Term src ss ts vs t)

Instances

Source src => Eq (TermVT src ss ts)

Methods

(==) :: TermVT src ss ts -> TermVT src ss ts -> Bool

(/=) :: TermVT src ss ts -> TermVT src ss ts -> Bool

Source src => Show (TermVT src ss ts)

Methods

showsPrec :: Int -> TermVT src ss ts -> ShowS

show :: TermVT src ss ts -> String

showList :: [TermVT src ss ts] -> ShowS

Source src => Sourced (TermVT src ss ts)

Methods

sourceOf :: TermVT src ss ts -> SourceOf (TermVT src ss ts)

setSource :: TermVT src ss ts -> SourceOf (TermVT src ss ts) -> TermVT src ss ts

type SourceOf (TermVT src ss ts)

type SourceOf (TermVT src ss ts) = src

liftTermVT :: TermVT src ss '[] -> TermVT src ss ts

Type TermAVT

data TermAVT src ss

Like TermVT, but CtxTe-free.

Constructors

TermAVT (forall ts. Term src ss ts vs t)

Instances

Source src => Eq (TermAVT src ss)

Methods

(==) :: TermAVT src ss -> TermAVT src ss -> Bool

(/=) :: TermAVT src ss -> TermAVT src ss -> Bool

Source src => Show (TermAVT src ss)

Methods

showsPrec :: Int -> TermAVT src ss -> ShowS

show :: TermAVT src ss -> String

showList :: [TermAVT src ss] -> ShowS

Source src => Sourced (TermAVT src ss)

Methods

sourceOf :: TermAVT src ss -> SourceOf (TermAVT src ss)

setSource :: TermAVT src ss -> SourceOf (TermAVT src ss) -> TermAVT src ss

type SourceOf (TermAVT src ss)

type SourceOf (TermAVT src ss) = src

Type TeSym

newtype TeSym ss ts t

Symantic of a Term.

Constructors

TeSym (forall term. Syms ss term => Sym_Lambda term => QualOf t => CtxTe term ts -> term (UnQualOf t))

teSym :: forall s ss ts t. Inj_Sym ss s => (forall term. Sym (Proxy s) term => Sym_Lambda term => QualOf t => term (UnQualOf t)) -> TeSym ss ts t

Like TeSym, but CtxTe-free and using inj_Sym to be able to use Sym (Proxy s) inside.

Type family QualOf

type family QualOf (t :: Type) :: Constraint where ...

Qualification

Equations

QualOf (q #> t) = q

QualOf t = (() :: Constraint)

Type family UnQualOf

type family UnQualOf (t :: Type) :: Type where ...

Unqualification

Equations

UnQualOf (q #> t) = t

UnQualOf t = t

unQualTy :: Source src => Type src vs (t :: Type) -> (TypeK src vs Constraint, TypeK src vs Type)

Return Constraint and Type part of given Type.

unQualsTy :: Source src => Type src vs (t :: kt) -> TypeK src vs kt

Remove Constraints from given Type.

Type CtxTe

data CtxTe term hs where

GADT for an interpreting context: accumulating at each lambda abstraction the term of the introduced variable.

Constructors

CtxTeZ :: CtxTe term '[]

CtxTeS :: term t -> CtxTe term ts -> CtxTe term (t ': ts) infixr 5

Type TermDef

type TermDef s vs t = forall src ss ts. Source src => Inj_Sym ss s => Term src ss ts vs t

Convenient type alias for defining Term.

Type family Sym

type family Sym (s :: Type) :: (Type -> Type) -> Constraint

Type family Syms

type family Syms (ss :: [Type]) (term :: Type -> Type) :: Constraint where ...

Equations

Syms '[] term = ()

Syms (s ': ss) term = (Sym s term, Syms ss term)

Type Inj_Sym

type Inj_Sym ss s = Inj_SymP (Index ss (Proxy s)) ss s

Convenient type synonym wrapping Inj_SymP applied on the correct Index.

inj_Sym :: forall s ss ts t. Inj_Sym ss s => TeSym '[Proxy s] ts t -> TeSym ss ts t

Inject a given symantic s into a list of them, by returning a function which given a TeSym on s returns the same TeSym on ss.

Class Inj_SymP

class Inj_SymP p ss s where

Minimal complete definition

inj_SymP

Methods

inj_SymP :: TeSym '[Proxy s] ts t -> TeSym ss ts t

Instances

Inj_SymP k * Zero ((:) * (Proxy k s) ss) s

Methods

inj_SymP :: TeSym ((* ': Proxy Zero s) [*]) ts t -> TeSym ss ts t

Inj_SymP k * p ss s => Inj_SymP k * (Succ p) ((:) Type not_s ss) s

Methods

inj_SymP :: TeSym ((* ': Proxy (Succ p) s) [*]) ts t -> TeSym ss ts t

Class Sym_Lambda

class Sym_Lambda term where

Methods

apply :: term ((a -> b) -> a -> b)

Function application.

apply :: Sym_Lambda (UnT term) => Trans term => term ((a -> b) -> a -> b)

Function application.

app :: term (a -> b) -> term a -> term b infixr 0

Lambda application.

app :: Sym_Lambda (UnT term) => Trans term => term (arg -> res) -> term arg -> term res infixr 0

Lambda application.

lam :: (term a -> term b) -> term (a -> b)

Lambda abstraction.

lam :: Sym_Lambda (UnT term) => Trans term => (term arg -> term res) -> term (arg -> res)

Lambda abstraction.

let_ :: term var -> (term var -> term res) -> term res

Convenient lam and app wrapper.

lam1 :: (term a -> term b) -> term (a -> b)

Lambda abstraction beta-reducable without duplication (i.e. whose variable is used once at most), mainly useful in compiled Terms whose symantics are not a single term but a function between terms, which happens because those are more usable when used as an embedded DSL.

lam1 :: Sym_Lambda (UnT term) => Trans term => (term a -> term b) -> term (a -> b)

Lambda abstraction beta-reducable without duplication (i.e. whose variable is used once at most), mainly useful in compiled Terms whose symantics are not a single term but a function between terms, which happens because those are more usable when used as an embedded DSL.

qual :: proxy q -> term t -> term (q #> t)

Qualification.

Workaround used in readTermWithCtx.

qual :: Sym_Lambda (UnT term) => Trans term => proxy q -> term t -> term (q #> t)

Qualification.

Workaround used in readTermWithCtx.

Instances

Sym_Lambda View

Methods

apply :: View ((a -> b) -> a -> b)

app :: View (a -> b) -> View a -> View b

lam :: (View a -> View b) -> View (a -> b)

let_ :: View var -> (View var -> View res) -> View res

lam1 :: (View a -> View b) -> View (a -> b)

qual :: proxy q -> View t -> View (q #> t)

Sym_Lambda Eval

Methods

apply :: Eval ((a -> b) -> a -> b)

app :: Eval (a -> b) -> Eval a -> Eval b

lam :: (Eval a -> Eval b) -> Eval (a -> b)

let_ :: Eval var -> (Eval var -> Eval res) -> Eval res

lam1 :: (Eval a -> Eval b) -> Eval (a -> b)

qual :: proxy q -> Eval t -> Eval (q #> t)

Sym_Lambda term => Sym_Lambda (BetaT term)

lam1 adds annotations, app uses it

Methods

apply :: BetaT term ((a -> b) -> a -> b)

app :: BetaT term (a -> b) -> BetaT term a -> BetaT term b

lam :: (BetaT term a -> BetaT term b) -> BetaT term (a -> b)

let_ :: BetaT term var -> (BetaT term var -> BetaT term res) -> BetaT term res

lam1 :: (BetaT term a -> BetaT term b) -> BetaT term (a -> b)

qual :: proxy q -> BetaT term t -> BetaT term (q #> t)

(Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (Dup r1 r2)

Methods

apply :: Dup r1 r2 ((a -> b) -> a -> b)

app :: Dup r1 r2 (a -> b) -> Dup r1 r2 a -> Dup r1 r2 b

lam :: (Dup r1 r2 a -> Dup r1 r2 b) -> Dup r1 r2 (a -> b)

let_ :: Dup r1 r2 var -> (Dup r1 r2 var -> Dup r1 r2 res) -> Dup r1 r2 res

lam1 :: (Dup r1 r2 a -> Dup r1 r2 b) -> Dup r1 r2 (a -> b)

qual :: proxy q -> Dup r1 r2 t -> Dup r1 r2 (q #> t)

lam2 :: Sym_Lambda term => (term a -> term b -> term c) -> term (a -> b -> c)

lam3 :: Sym_Lambda term => (term a -> term b -> term c -> term d) -> term (a -> b -> c -> d)

lam4 :: Sym_Lambda term => (term a -> term b -> term c -> term d -> term e) -> term (a -> b -> c -> d -> e)