Safe Haskell	None

Chi

Contents

The abstract syntax of χ
Parsing and pretty-printing
An example
Conversions
Free and bound variables
Self-interpreters
Some testing procedures
Orphan instances

Description

A wrapper module that exports the generated abstract syntax of χ as well as some definitions that may be useful when testing χ code or interpreters.

Synopsis

The abstract syntax of χ

module AbsChi

Parsing and pretty-printing

parse ∷ String → Exp #

Tries to parse a χ program. If parsing fails, then an exception is raised.

pretty ∷ Exp → String #

Pretty-prints a χ program.

An example

add ∷ Exp #

A χ program for addition of natural numbers.

Conversions

fromNatural ∷ Natural → Exp #

Converts a Haskell natural number to its χ representation.

toNatural ∷ Exp → Maybe Natural #

Tries to convert the given χ expression to a natural number.

data Code a #

Encoding monad.

Instances

Monad Code #
Methods (>>=) ∷ Code a → (a → Code b) → Code b (>>) ∷ Code a → Code b → Code b return ∷ a → Code a fail ∷ String → Code a
Functor Code #
Methods fmap ∷ (a → b) → Code a → Code b (<$) ∷ a → Code b → Code a
Applicative Code #
Methods pure ∷ a → Code a (<>) ∷ Code (a → b) → Code a → Code b (>) ∷ Code a → Code b → Code b (<*) ∷ Code a → Code b → Code a

data Decode a #

Decoding monad.

Instances

Monad Decode #
Methods (>>=) ∷ Decode a → (a → Decode b) → Decode b (>>) ∷ Decode a → Decode b → Decode b return ∷ a → Decode a fail ∷ String → Decode a
Functor Decode #
Methods fmap ∷ (a → b) → Decode a → Decode b (<$) ∷ a → Decode b → Decode a
Applicative Decode #
Methods pure ∷ a → Decode a (<>) ∷ Decode (a → b) → Decode a → Decode b (>) ∷ Decode a → Decode b → Decode b (<*) ∷ Decode a → Decode b → Decode a
Alternative Decode #
Methods empty ∷ Decode a (<\|>) ∷ Decode a → Decode a → Decode a some ∷ Decode a → Decode [a] many ∷ Decode a → Decode [a]

runCode ∷ Code a → a #

Runs a coder.

Note that coding might not give consistent results if you invoke runCode multiple times. For instance, the following code will return False:

  runCode (code (parse "Succ(Zero())"))
    ==
  runCode (do
    code (parse "Zero()")
    code (parse "Succ(Zero())"))

runDecode ∷ Decode a → Maybe a #

Runs a decoder. Note that decoders can fail.

asDecoder ∷ Code a → Decode a #

Turns a coder into a decoder.

Example usage:

  do e <- asDecoder (code e)
     decode (eval (Apply selfInterpreter e))

code ∷ Exp → Code Exp #

Encodes expressions.

decode ∷ Exp → Decode Exp #

Decodes expressions.

codeVar ∷ Variable → Code Exp #

Encodes variables.

codeCon ∷ Constructor → Code Exp #

Encodes constructors.

decodeVar ∷ Exp → Decode Variable #

Decodes variables.

decodeCon ∷ Exp → Decode Constructor #

Decodes constructors.

internalCode ∷ Code Exp #

An internal implementation of coding.

Example usage:

  runCode $ do
    ic <- internalCode
    ce <- code e
    return (eval (Apply ic ce))

Free and bound variables

free ∷ Exp → HashSet Variable #

The term's free variables.

bound ∷ Exp → HashSet Variable #

Bound variables that actually occur bound in the term (not in a binder). For λx.x a singleton set containing x is returned, but for λx.Nil() the empty set is returned.

closed ∷ Gen Exp #

A QuickCheck generator for closed terms.

Self-interpreters

runSelfInterpreter #

Arguments

∷ (Exp → Exp)	An implementation of evaluation.
→ Exp	The self-interpreter.
→ Exp	The program to be evaluated (not in coded form).
→ [Exp]	The program's arguments (not in coded form).
→ Maybe Exp

Uses a self-interpreter to evaluate a program applied to some arguments.

If the self-interpreter terminates, and the result can be decoded, then this result is returned.

Example usage:

  do n <- runSelfInterpreter eval selfInterpreter add
            [fromNatural 2, fromNatural 2]
     toNatural n

Some testing procedures

testEvaluation ∷ (Exp → Exp) → IO Bool #

Tests whether a purported implementation of evaluation can evaluate addition of two natural numbers (add) correctly.

The test is, of course, incomplete.

testMultiplication #

Arguments

∷ (Exp → Exp)	Evaluation.
→ Exp	Multiplication. The program should take two natural numbers as input and produce a natural number as its result.
→ IO Bool

Tests whether a purported implementation of evaluation and a purported implementation of multiplication of two natural numbers are correct.

The test is, of course, incomplete.

testSubstitution ∷ (Variable → Exp → Exp → Exp) → IO Bool #

Tests a purported implementation of substitution.

The substitution operation takes three arguments, x, e and e', where e is closed, and should substitute e for every free occurrence of x in e'.

The test is designed for substitution operations that are implemented exactly like in the χ specification. In particular, the substitution operation should not rename any bound variables.

The test is, of course, incomplete.

testInternalSubstitution #

Arguments

∷ (Exp → Exp)	Evaluation.
→ (Variable → Exp → Exp → Exp)	Substitution.
→ Exp	Internal substitution.
→ IO Bool

Tests whether an implementation of internal substitution matches an implementation of substitution.

The test is, of course, incomplete.

testSelfInterpreterWith #

Arguments

∷ (Exp → Exp)	Evaluation.
→ Exp	The self-interpreter.
→ Exp	The program to be evaluated (not in coded form).
→ [Exp]	The arguments (not in coded form).
→ Bool

Tests if the result of the given self-interpreter matches that of the given evaluator for a program applied to some arguments.

Note that no result is returned if some program crashes or fails to terminate.

Example usage:

  testSelfInterpreterWith eval selfInterpreter add
    [fromNatural 2, fromNatural 2]

testSelfInterpreter #

Arguments

∷ (Exp → Exp)	Evaluation.
→ Exp	The self-interpreter.
→ IO Bool

Tests whether a purported implementation of evaluation and a purported self-interpreter are correctly implemented.

The test is, of course, incomplete.

testTuringMachineInterpreter #

Arguments

∷ (Exp → Exp)	Evaluation.
→ Exp	The Turing machine interpreter.
→ IO Bool

Tests whether a purported implementation of evaluation and a purported Turing machine interpreter are correctly implemented. The Turing machine interpreter should satisfy the specification given in Assignment 6.

The test is, of course, incomplete.

Orphan instances

Generic Br #
Associated Types type Rep Br ∷ ★ → ★ Methods from ∷ Br → Rep Br x to ∷ Rep Br x → Br
Generic Exp #
Associated Types type Rep Exp ∷ ★ → ★ Methods from ∷ Exp → Rep Exp x to ∷ Rep Exp x → Exp
Generic Variable #
Associated Types type Rep Variable ∷ ★ → ★ Methods from ∷ Variable → Rep Variable x to ∷ Rep Variable x → Variable
Generic Constructor #
Associated Types type Rep Constructor ∷ ★ → ★ Methods from ∷ Constructor → Rep Constructor x to ∷ Rep Constructor x → Constructor
Hashable Variable #
Methods hashWithSalt ∷ Int → Variable → Int hash ∷ Variable → Int
Hashable Constructor #
Methods hashWithSalt ∷ Int → Constructor → Int hash ∷ Constructor → Int
Arbitrary Br #	A QuickCheck generator for branches.
Methods arbitrary ∷ Gen Br shrink ∷ Br → [Br]
Arbitrary Exp #	A QuickCheck generator for arbitrary terms.
Methods arbitrary ∷ Gen Exp shrink ∷ Exp → [Exp]
Arbitrary Variable #	A QuickCheck generator for (a small number of) variables.
Methods arbitrary ∷ Gen Variable shrink ∷ Variable → [Variable]
Arbitrary Constructor #	A QuickCheck generator for (a small number of) constructors.
Methods arbitrary ∷ Gen Constructor shrink ∷ Constructor → [Constructor]