Brainfuck.dcl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

definition module Brainfuck

import StdEnv, StdList

:: Command = INC | DEC | INCP | DECP | OUT | IN | IFZ | IFNZ
:: Program :== {Command}
:: InstrPointer :== Int

:: Cell :== Int
:: *Tape :== *{#Cell}
:: DataPointer :== Int

run :: Program *env -> *env | FileSystem env

read :: String -> Program