blob: 3ea9b1ad7a3ed9cfeb077c10eb9d993e32fb5725 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
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)
|
