Safe Haskell	None
Language	Haskell2010

Language.PTS.Smart

Description

Using magic of type-classes we can make...

Synopsis

class TermConv t where
class ValueConv v where
class Convert u v | v -> u where
class CanApp u v w | w -> u v where
(@@@) :: (TermConv t, TermConv t') => TermInf s a -> t s a -> t' s a
apps_ :: CanApp u v u => u s a -> [v s a] -> u s a
class Convert u v => CanPi u v | v -> u where
forall_ :: (CanPi u v, CanSort u, Specification s) => Sym -> u s Sym -> v s Sym
foralls_ :: (CanPi u v, CanPi u u, CanSort u, Specification s) => [Sym] -> u s Sym -> v s Sym
class CanSort u where
class CanLam u where
lams_ :: CanLam u => [Sym] -> u s Sym -> u s Sym
ann_ :: TermChk s a -> TermInf s a -> TermInf s a
(-:-) :: TermChk s a -> TermInf s a -> TermInf s a
let_ :: [(Sym, Term s)] -> Term s -> Term s
(.=) :: a -> b -> (a, b)

Documentation

class TermConv t where Source #

Minimal complete definition

toTermChk, fromTermInf

Methods

toTermChk :: t s a -> TermChk s a Source #

fromTermInf :: TermInf s a -> t s a Source #

Instances

TermConv TermChk Source #
Instance details Defined in Language.PTS.Smart Methods toTermChk :: TermChk s a -> TermChk s a Source # fromTermInf :: TermInf s a -> TermChk s a Source #
TermConv TermInf Source #
Instance details Defined in Language.PTS.Smart Methods toTermChk :: TermInf s a -> TermChk s a Source # fromTermInf :: TermInf s a -> TermInf s a Source #

class ValueConv v where Source #

Minimal complete definition

toValueIntro

Methods

toValueIntro :: v err s a -> ValueIntro err s a Source #

Instances

ValueConv ValueElim Source #
Instance details Defined in Language.PTS.Smart Methods toValueIntro :: ValueElim err s a -> ValueIntro err s a Source #
ValueConv ValueIntro Source #
Instance details Defined in Language.PTS.Smart Methods toValueIntro :: ValueIntro err s a -> ValueIntro err s a Source #

class Convert u v | v -> u where Source #

Minimal complete definition

convert

Methods

convert :: u s a -> v s a Source #

Instances

Convert TermInf TermChk Source #
Instance details Defined in Language.PTS.Smart Methods convert :: TermInf s a -> TermChk s a Source #
Convert TermInf TermInf Source #
Instance details Defined in Language.PTS.Smart Methods convert :: TermInf s a -> TermInf s a Source #
Convert (ValueIntro err) (ValueIntro err) Source #
Instance details Defined in Language.PTS.Smart Methods convert :: ValueIntro err s a -> ValueIntro err s a Source #

class CanApp u v w | w -> u v where Source #

Minimal complete definition

(@@)

Methods

(@@) :: u s a -> v s a -> w s a infixl 3 Source #

Left-associative $ for terms and values.

Instances

CanApp TermInf TermChk TermChk Source #
Instance details Defined in Language.PTS.Smart Methods (@@) :: TermInf s a -> TermChk s a -> TermChk s a Source #
CanApp TermInf TermChk TermInf Source #
Instance details Defined in Language.PTS.Smart Methods (@@) :: TermInf s a -> TermChk s a -> TermInf s a Source #
CanApp (ValueElim err) (ValueIntro err) (ValueIntro err) Source #
Instance details Defined in Language.PTS.Smart Methods (@@) :: ValueElim err s a -> ValueIntro err s a -> ValueIntro err s a Source #
CanApp (ValueElim err) (ValueIntro err) (ValueElim err) Source #
Instance details Defined in Language.PTS.Smart Methods (@@) :: ValueElim err s a -> ValueIntro err s a -> ValueElim err s a Source #

(@@@) :: (TermConv t, TermConv t') => TermInf s a -> t s a -> t' s a infixl 3 Source #

More polymorphic @@.

apps_ :: CanApp u v u => u s a -> [v s a] -> u s a Source #

class Convert u v => CanPi u v | v -> u where Source #

Minimal complete definition

pi_, (~>), sigma_

Methods

pi_ :: Sym -> u s Sym -> u s Sym -> v s Sym Source #

(~>) :: Specification s => u s a -> u s a -> v s a infixr 2 Source #

non-dependent function space.

\[ \alpha \to \beta ::= \Pi (- : \alpha). \beta \]

sigma_ :: Sym -> u s Sym -> u s Sym -> v s Sym Source #

Instances

CanPi TermInf TermChk Source #
Instance details Defined in Language.PTS.Smart Methods pi_ :: Sym -> TermInf s Sym -> TermInf s Sym -> TermChk s Sym Source # (~>) :: Specification s => TermInf s a -> TermInf s a -> TermChk s a Source # sigma_ :: Sym -> TermInf s Sym -> TermInf s Sym -> TermChk s Sym Source #
CanPi TermInf TermInf Source #
Instance details Defined in Language.PTS.Smart Methods pi_ :: Sym -> TermInf s Sym -> TermInf s Sym -> TermInf s Sym Source # (~>) :: Specification s => TermInf s a -> TermInf s a -> TermInf s a Source # sigma_ :: Sym -> TermInf s Sym -> TermInf s Sym -> TermInf s Sym Source #
CanPi (ValueIntro err) (ValueIntro err) Source #
Instance details Defined in Language.PTS.Smart Methods pi_ :: Sym -> ValueIntro err s Sym -> ValueIntro err s Sym -> ValueIntro err s Sym Source # (~>) :: Specification s => ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a Source # sigma_ :: Sym -> ValueIntro err s Sym -> ValueIntro err s Sym -> ValueIntro err s Sym Source #

forall_ :: (CanPi u v, CanSort u, Specification s) => Sym -> u s Sym -> v s Sym Source #

Polymorphic, rank-1 types.

\[ \forall \alpha. F\,\alpha ::= \Pi (\alpha : \star). F\,\alpha \]

foralls_ :: (CanPi u v, CanPi u u, CanSort u, Specification s) => [Sym] -> u s Sym -> v s Sym Source #

class CanSort u where Source #

Minimal complete definition

sort_

Methods

sort_ :: s -> u s a Source #

Instances

CanSort TermChk Source #
Instance details Defined in Language.PTS.Smart Methods sort_ :: s -> TermChk s a Source #
CanSort TermInf Source #
Instance details Defined in Language.PTS.Smart Methods sort_ :: s -> TermInf s a Source #
CanSort (ValueIntro err) Source #
Instance details Defined in Language.PTS.Smart Methods sort_ :: s -> ValueIntro err s a Source #

class CanLam u where Source #

Minimal complete definition

lam_

Methods

lam_ :: Sym -> u s Sym -> u s Sym Source #

Instances

CanLam TermChk Source #
Instance details Defined in Language.PTS.Smart Methods lam_ :: Sym -> TermChk s Sym -> TermChk s Sym Source #

lams_ :: CanLam u => [Sym] -> u s Sym -> u s Sym Source #

ann_ :: TermChk s a -> TermInf s a -> TermInf s a Source #

Add annotation only to non-inferrable terms. (So we don't end in Ann ('Inf (Ann ...)) tower.

(-:-) :: TermChk s a -> TermInf s a -> TermInf s a infixr 1 Source #

let_ :: [(Sym, Term s)] -> Term s -> Term s Source #

Let-bindings.

(.=) :: a -> b -> (a, b) infix 0 Source #

An alternative name for pair.

>>> :set -XOverloadedStrings