language-pts-0: Pure Type Systems

Safe HaskellNone
LanguageHaskell2010

Language.PTS.Script

Synopsis

Documentation

class (Specification s, Monad m) => Script s m | m -> s where Source #

Scripts, monads for writing bigger terms.

See churchBooleans for an example.

Minimal complete definition

defineChk_, defineInf_, example_, comment_, section_, subsection_, dumpDefs_

Methods

define_ Source #

Arguments

:: Sym

name

-> Term s

type

-> TermChk s Sym

term

-> m () 

Define a term with a type. Note, first argument is a type.

defineChk_ Source #

Arguments

:: Sym

name

-> Term s

type

-> TermChk s Sym

term

-> m () 

defineInf_ Source #

Arguments

:: Sym

name

-> Term s

term

-> m () 

example_ :: Term s -> m () Source #

Evaluate an example value.

comment_ :: String -> m () Source #

Write a comment to be output.

section_ :: String -> m () Source #

subsection_ :: String -> m () Source #

dumpDefs_ :: m () Source #

Dump definitions

Instances
(Specification s, Monad m) => Script s (ScriptT s m) Source # 
Instance details

Defined in Language.PTS.Script

Methods

define_ :: Sym -> Term s -> TermChk s Sym -> ScriptT s m () Source #

defineChk_ :: Sym -> Term s -> TermChk s Sym -> ScriptT s m () Source #

defineInf_ :: Sym -> Term s -> ScriptT s m () Source #

example_ :: Term s -> ScriptT s m () Source #

comment_ :: String -> ScriptT s m () Source #

section_ :: String -> ScriptT s m () Source #

subsection_ :: String -> ScriptT s m () Source #

dumpDefs_ :: ScriptT s m () Source #

spec_ :: Script s m => s -> m () Source #

Tell used specification. Helps type-inference.

($$) :: (a -> b) -> a -> b infixl 0 Source #

$ is infixr, $$ is infixl

runLoud :: ScriptT s IO () -> IO () Source #

runSilent :: ScriptT s IO () -> IO () Source #

runString :: ScriptT s (State ([String] -> [String])) () -> String Source #

data ScriptT s m a Source #

Instances
Monad m => MonadError Err (ScriptT s m) Source # 
Instance details

Defined in Language.PTS.Script

Methods

throwError :: Err -> ScriptT s m a Source #

catchError :: ScriptT s m a -> (Err -> ScriptT s m a) -> ScriptT s m a Source #

(Specification s, Monad m) => Script s (ScriptT s m) Source # 
Instance details

Defined in Language.PTS.Script

Methods

define_ :: Sym -> Term s -> TermChk s Sym -> ScriptT s m () Source #

defineChk_ :: Sym -> Term s -> TermChk s Sym -> ScriptT s m () Source #

defineInf_ :: Sym -> Term s -> ScriptT s m () Source #

example_ :: Term s -> ScriptT s m () Source #

comment_ :: String -> ScriptT s m () Source #

section_ :: String -> ScriptT s m () Source #

subsection_ :: String -> ScriptT s m () Source #

dumpDefs_ :: ScriptT s m () Source #

Monad m => Monad (ScriptT s m) Source # 
Instance details

Defined in Language.PTS.Script

Methods

(>>=) :: ScriptT s m a -> (a -> ScriptT s m b) -> ScriptT s m b Source #

(>>) :: ScriptT s m a -> ScriptT s m b -> ScriptT s m b Source #

return :: a -> ScriptT s m a Source #

fail :: String -> ScriptT s m a Source #

Functor m => Functor (ScriptT s m) Source # 
Instance details

Defined in Language.PTS.Script

Methods

fmap :: (a -> b) -> ScriptT s m a -> ScriptT s m b Source #

(<$) :: a -> ScriptT s m b -> ScriptT s m a Source #

Monad m => Applicative (ScriptT s m) Source # 
Instance details

Defined in Language.PTS.Script

Methods

pure :: a -> ScriptT s m a Source #

(<*>) :: ScriptT s m (a -> b) -> ScriptT s m a -> ScriptT s m b Source #

liftA2 :: (a -> b -> c) -> ScriptT s m a -> ScriptT s m b -> ScriptT s m c Source #

(*>) :: ScriptT s m a -> ScriptT s m b -> ScriptT s m b Source #

(<*) :: ScriptT s m a -> ScriptT s m b -> ScriptT s m a Source #

Monad m => MonadErr (ScriptT s m) Source # 
Instance details

Defined in Language.PTS.Script

Methods

throwErr :: Err -> ScriptT s m a Source #