diff options
| author | Camil Staps | 2016-06-10 08:45:09 +0200 |
|---|---|---|
| committer | Camil Staps | 2016-06-10 08:45:09 +0200 |
| commit | 09cf0f0791f8d05dbec240917e2010b161bb24f6 (patch) | |
| tree | a5f5ac3d5f17d75bbe3171c3528307e81a9ec3d9 /proof.icl | |
| parent | LaTeX formatting for derivation trees (diff) | |
Minimalistic prover
Diffstat (limited to 'proof.icl')
| -rw-r--r-- | proof.icl | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/proof.icl b/proof.icl new file mode 100644 index 0000000..3ea9b1a --- /dev/null +++ b/proof.icl @@ -0,0 +1,18 @@ +module proof + +import StdEnv, StdDebug + +from Data.Func import $ +import Data.Maybe + +import Smurf, SmurfParse + +Start = toString (devtree ass) +++ "\n" +where + ass (pgm, ip, st) + | pgm == [Tail,Tail] && st.stack == [Lit "bcd"] + = Just ([], [], {st & stack=[Lit "d"]}) + = Nothing + pgm = fromJust $ parse ['ittt'] + devtree ass + = fromJust (prover ass pgm zero { zero & input = [Lit "abcd"] } listIO) |