Safe Haskell | None |
---|
Chi
Contents
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.
- module AbsChi
- parse ∷ String → Exp
- pretty ∷ Exp → String
- add ∷ Exp
- fromNatural ∷ Natural → Exp
- toNatural ∷ Exp → Maybe Natural
- data Code a
- data Decode a
- runCode ∷ Code a → a
- runDecode ∷ Decode a → Maybe a
- asDecoder ∷ Code a → Decode a
- code ∷ Exp → Code Exp
- decode ∷ Exp → Decode Exp
- codeVar ∷ Variable → Code Exp
- codeCon ∷ Constructor → Code Exp
- decodeVar ∷ Exp → Decode Variable
- decodeCon ∷ Exp → Decode Constructor
- internalCode ∷ Code Exp
- free ∷ Exp → HashSet Variable
- bound ∷ Exp → HashSet Variable
- closed ∷ Gen Exp
- runSelfInterpreter ∷ (Exp → Exp) → Exp → Exp → [Exp] → Maybe Exp
- testEvaluation ∷ (Exp → Exp) → IO Bool
- testMultiplication ∷ (Exp → Exp) → Exp → IO Bool
- testSubstitution ∷ (Variable → Exp → Exp → Exp) → IO Bool
- testInternalSubstitution ∷ (Exp → Exp) → (Variable → Exp → Exp → Exp) → Exp → IO Bool
- testSelfInterpreterWith ∷ (Exp → Exp) → Exp → Exp → [Exp] → Bool
- testSelfInterpreter ∷ (Exp → Exp) → Exp → IO Bool
- testTuringMachineInterpreter ∷ (Exp → Exp) → Exp → IO Bool
The abstract syntax of χ
module AbsChi
Parsing and pretty-printing
An example
Conversions
fromNatural ∷ Natural → Exp #
Converts a Haskell natural number to its χ representation.
Decoding monad.
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())"))
codeCon ∷ Constructor → Code Exp #
Encodes constructors.
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
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.
Self-interpreters
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 selfInterpreteradd
[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.
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.
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.
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 selfInterpreteradd
[fromNatural
2,fromNatural
2]
Tests whether a purported implementation of evaluation and a purported self-interpreter are correctly implemented.
The test is, of course, incomplete.
testTuringMachineInterpreter #
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 # | |
Generic Exp # | |
Generic Variable # | |
Generic Constructor # | |
Hashable Variable # | |
Hashable Constructor # | |
Arbitrary Br # | A QuickCheck generator for branches. |
Arbitrary Exp # | A QuickCheck generator for arbitrary terms. |
Arbitrary Variable # | A QuickCheck generator for (a small number of) variables. |
Arbitrary Constructor # | A QuickCheck generator for (a small number of) constructors. |