BF.fs

module BF

// Natural number
type N = abstract member Value : int

[<StructuredFormatDisplay("{IntValue}")>]
type Z = Z with
  member z.IntValue = 0
  interface N with member z.Value = 0

[<StructuredFormatDisplay("{IntValue}")>]
type S<'n when 'n :> N> = S of 'n with
  interface N with member x.Value = match x with S(x) -> 1 + x.Value
  member z.IntValue = (z :> N).Value

type N1 = Z S
type N2 = N1 S
type N3 = N2 S
type N4 = N3 S
type N5 = N4 S
type N6 = N5 S
type N7 = N6 S
type N8 = N7 S
type N9 = N8 S
type N10 = N9 S

[<AutoOpen>]
module Ns =
  let n1 : N1 = S(Z)
  let n2 : N2 = S(n1)
  let n3 : N3 = S(n2)
  let n4 : N4 = S(n3)
  let n5 : N5 = S(n4)
  let n6 : N6 = S(n5)
  let n7 : N7 = S(n6)
  let n8 : N8 = S(n7)
  let n9 : N9 = S(n8)
  let n10 : N10 = S(n9)

// List
type L =
  abstract member ToList : obj list

[<StructuredFormatDisplay("{ListValue}")>]
type E = E with
  interface L with member e.ToList = []
  member e.ListValue = (e :> L).ToList |> List.map (sprintf "%A")

[<StructuredFormatDisplay("{ListValue}")>]
type C<'a, 'b> when 'b :> L = C of 'a * 'b with
  interface L with
    member c.ToList = match c with C(a, b) -> (box a) :: b.ToList

  member c.ListValue = (c :> L).ToList |> List.map (sprintf "%A")

// A tape with a current pointer: 'l for everything on the left,
// 'x for current value, 'r for right
type Tape<'l, 'x, 'r> when 'l :> L and 'r :> L = Tape of 'l * 'x * 'r

type D = interface end
type Left = Left with interface D
type Right = Right with interface D

type Shift<'d, 't1, 't2> =
  abstract member Shifted : 't2

type ShiftLE<'x, 'r> when 'r :> L = ShiftLE of Tape<E, 'x, 'r> with
  interface Shift<Left, Tape<E, 'x, 'r>, Tape<E, 'x, 'r>> with
    member s.Shifted =
      match s with ShiftLE(Tape(E, x, r)) -> Tape(E, x, r)

type ShiftRE<'l, 'x> when 'l :> L = ShiftRE of Tape<'l, 'x, E> with
  interface Shift<Right, Tape<'l, 'x, E>, Tape<'l, 'x, E>> with
    member s.Shifted =
      match s with ShiftRE(Tape(l, x, E)) -> Tape(l, x, E)

type ShiftL<'a, 'l, 'x, 'r> when 'l :> L and 'r :> L = ShiftL of Tape<C<'a, 'l>, 'x, 'r> with
  interface Shift<Left, Tape<C<'a, 'l>, 'x, 'r>, Tape<'l, 'a, C<'x, 'r>>> with
    member s.Shifted =
      match s with ShiftL(Tape(C(a, l), x, r)) -> Tape(l, a, C(x, r))

type ShiftR<'a, 'l, 'x, 'r> when 'l :> L and 'r :> L = ShiftR of Tape<'l, 'x, C<'a, 'r>> with
  interface Shift<Right, Tape<'l, 'x, C<'a, 'r>>, Tape<C<'x, 'l>, 'a, 'r>> with
    member s.Shifted =
      match s with ShiftR(Tape(l, x, C(a, r))) -> Tape(C(x, l), a, r)

type ShiftN<'d, 'n, 't1, 't2> =
  abstract member Shifted : 't2

type ShiftZ<'d, 't> = ShiftZ of 't with
  interface ShiftN<'d, Z, 't, 't> with
    member s.Shifted = match s with ShiftZ(tape) -> tape

type ShiftS<'d, 'n, 't1, 'ti, 't2, 's, 'sn>
    when 's :> Shift<'d, 't1, 'ti>
    and 'sn :> ShiftN<'d, 'n, 'ti, 't2>
    and 'n :> N = ShiftS of 's * 'sn with
  interface ShiftN<'d, S<'n>, 't1, 't2> with
    member ss.Shifted = match ss with | ShiftS(s, sn) -> sn.Shifted

type Z with
  static member inline (<<<-) (Z, (Tape(_ : ^tl, _ : ^x, _ : ^tr) as tape)) =
    ShiftZ(tape) :> ShiftN<_, _, _, _>
  static member inline (->>>) (Z, (Tape(_ : ^tl, _ : ^x, _ : ^tr) as tape)) =
    ShiftZ(tape) :> ShiftN<_, _, _, _>

  static member inline (-) (n, Z) = n

type S<'n> with
  static member inline (-) (S(n), S(m)) = n - m

  static member inline (<<<-)(S(n), tape) =
    let shift = ShiftL(tape) :> Shift<_, _, _>
    let res = shift.Shifted
    let si : ShiftN<_, _, _, _> = n <<<- res
    ShiftS(shift, si) :> ShiftN<_, _, _, _>

  static member inline (->>>)(S(n), tape) =
    let shift = ShiftR(tape) :> Shift<_, _, _>
    let res = shift.Shifted
    let si : ShiftN<_, _, _, _> = n ->>> res
    ShiftS(shift, si) :> ShiftN<_, _, _, _>

let testShift() =
  let tape = Tape(C(n3, C(n4, C(n5, C(n6, E)))), n7, C(n8, C(n9, E)))

  printfn "--------------------"
  printfn "testShift()"
  let inline p (x : #ShiftN<_, _, _, _>) = printfn "%A" x.Shifted
  (n4 <<<- tape) |> p
  (n3 <<<- tape) |> p
  (n2 <<<- tape) |> p
  (n1 <<<- tape) |> p
  (Z <<<- tape) |> p
  (Z ->>> tape) |> p
  (n1 ->>> tape) |> p
  (n2 ->>> tape) |> p

do testShift()

// Intermediate instruction set
type I = interface end

// Increment cell
type Inc = Inc with interface I
// Decrement cell
type Dec = Dec with interface I
// Move to previous cell
type MoveL = MoveL with interface I
// Move to next cell
type MoveR = MoveR with interface I
// Unconditional relative jump
type Jmp<'d, 'rel> when 'rel :> N = Jmp of 'd * 'rel with interface I
// Conditional (when non-zero) relative jump
type CondJ<'d, 'rel> when 'rel :> N = CondJ of 'd * 'rel with interface I
// End program
type End = End with interface I

type State<'code, 'data> = State of 'code * 'data

type Step<'state1, 'state2> =
  abstract member StepResult : 'state2

type StepInc<'cl, 'cr, 'tl, 'x, 'tr>
    when 'cl :> L and 'cr :> L
    and 'tl :> L and 'tr :> L and 'x :> N
    = StepInc of State<Tape<'cl, Inc, 'cr>, Tape<'tl, 'x, 'tr>> with
  interface Step<State<Tape<'cl, Inc, 'cr>, Tape<'tl, 'x, 'tr>>,
                 State<Tape<'cl, Inc, 'cr>, Tape<'tl, 'x S, 'tr>>> with
    member si.StepResult =
      match si with
      | StepInc(State(code, Tape(tl, x, tr))) -> State(code, Tape(tl, S x, tr))

type StepDec<'cl, 'cr, 'tl, 'x, 'tr>
    when 'cl :> L and 'cr :> L
    and 'tl :> L and 'tr :> L and 'x :> N
    = StepDec of State<Tape<'cl, Dec, 'cr>, Tape<'tl, 'x S, 'tr>> with
  interface Step<State<Tape<'cl, Dec, 'cr>, Tape<'tl, 'x S, 'tr>>,
                 State<Tape<'cl, Dec, 'cr>, Tape<'tl, 'x, 'tr>>> with
    member si.StepResult =
      match si with
      | StepDec(State(code, Tape(tl, S x, tr))) -> State(code, Tape(tl, x, tr))

type StepDecZ<'cl, 'cr, 'tl, 'tr>
    when 'cl :> L and 'cr :> L
    and 'tl :> L and 'tr :> L
    = StepDecZ of State<Tape<'cl, Dec, 'cr>, Tape<'tl, Z, 'tr>> with
  interface Step<State<Tape<'cl, Dec, 'cr>, Tape<'tl, Z, 'tr>>,
                 State<Tape<'cl, Dec, 'cr>, Tape<'tl, Z, 'tr>>> with
    member si.StepResult =
      match si with
      | StepDecZ(State(code, Tape(tl, Z, tr))) -> State(code, Tape(tl, Z, tr))

type StepMoveL<'cl, 'cr, 'tape0, 'tape1, 'sl>
    when 'cl :> L and 'cr :> L
    and 'sl :> Shift<Left, 'tape0, 'tape1>
    = StepMoveL of State<Tape<'cl, MoveL, 'cr>, 'tape0> * 'sl with
  interface Step<State<Tape<'cl, MoveL, 'cr>, 'tape0>,
                 State<Tape<'cl, MoveL, 'cr>, 'tape1>> with
    member si.StepResult =
      match si with
      | StepMoveL(State(code, data), sl) -> State(code, sl.Shifted)

type StepMoveR<'cl, 'cr, 'tape0, 'tape1, 'sr>
    when 'cl :> L and 'cr :> L
    and 'sr :> Shift<Right, 'tape0, 'tape1>
    = StepMoveR of State<Tape<'cl, MoveR, 'cr>, 'tape0> * 'sr with
  interface Step<State<Tape<'cl, MoveR, 'cr>, 'tape0>,
                 State<Tape<'cl, MoveR, 'cr>, 'tape1>> with
    member si.StepResult =
      match si with
      | StepMoveR(State(code, data), sr) -> State(code, sr.Shifted)

type StepJmp<'d, 'rel, 'cl, 'cr, 'sn, 'code1, 'data>
    when 'rel :> N and 'cl :> L and 'cr :> L
    and 'sn :> ShiftN<'d, 'rel, Tape<'cl, Jmp<'d, 'rel>, 'cr>, 'code1>
    = StepJmp of State<Tape<'cl, Jmp<'d, 'rel>, 'cr>, 'data> * 'sn with
  interface Step<State<Tape<'cl, Jmp<'d, 'rel>, 'cr>, 'data>,
                 State<'code1, 'data>> with
    member si.StepResult =
      match si with
      | StepJmp(State(code, data), sn) -> State(sn.Shifted, data)

type StepCondJZ<'d, 'rel, 'cl, 'cr, 'tl, 'tr>
    when 'rel :> N and 'cl :> L and 'cr :> L
    and 'tl :> L and 'tr :> L
    = StepCondJZ of State<Tape<'cl, CondJ<'d, 'rel>, 'cr>, Tape<'tl, Z, 'tr>> with
  interface Step<State<Tape<'cl, CondJ<'d, 'rel>, 'cr>, Tape<'tl, Z, 'tr>>,
                 State<Tape<'cl, CondJ<'d, 'rel>, 'cr>, Tape<'tl, Z, 'tr>>> with
    member si.StepResult =
      match si with
      | StepCondJZ(state) -> state

type StepCondJS<'d, 'rel, 'cl, 'cr, 'tl, 'tr, 'n, 'sn, 'code1>
    when 'rel :> N and 'cl :> L and 'cr :> L
    and 'tl :> L and 'tr :> L and 'n :> N
    and 'sn :> ShiftN<'d, 'rel, Tape<'cl, CondJ<'d, 'rel>, 'cr>, 'code1>
    = StepCondJS of State<Tape<'cl, CondJ<'d, 'rel>, 'cr>, Tape<'tl, 'n S, 'tr>> * 'sn with
  interface Step<State<Tape<'cl, CondJ<'d, 'rel>, 'cr>, Tape<'tl, 'n S, 'tr>>,
                 State<'code1, Tape<'tl, 'n S, 'tr>>> with
    member si.StepResult =
      match si with
      | StepCondJS(State(code, data), sn) -> State(sn.Shifted, data)

type StepEnd<'cl, 'cr, 'code>
    when 'cl :> L and 'cr :> L = StepEnd of State<Tape<'cl, End, 'cr>, 'code> with
  interface Step<State<Tape<'cl, End, 'cr>, 'code>, End> with
    member si.StepResult = End

type IncPC<'state, 'state1> =
  abstract member IncResult : 'state1

type IncPCS<'sr, 'code, 'code1, 'data>
    when 'sr :> Shift<Right, 'code, 'code1>
    = IncPCS of State<'code, 'data> * 'sr with
  interface IncPC<State<'code, 'data>, State<'code1, 'data>> with
    member i.IncResult =
      match i with IncPCS(State(code, data), sr) -> State(sr.Shifted, data)

type State<'code, 'data> with
  static member inline INCPC(End) = End

  static member inline INCPC(State(code, data : ^data)) =
    let shifted = ShiftR(code) :> Shift<_, _, _>
    IncPCS(State(code, data), shifted) :> IncPC<_, _>

  static member inline STEP(state : State<Tape< ^cl, Inc, ^cr>, Tape< ^tl, ^x, ^tr>>) =
    StepInc(state) :> Step<_, _>

  static member inline STEP(state : State<Tape< ^cl, Dec, ^cr>, Tape< ^tl, ^x S, ^tr>>) =
    StepDec(state) :> Step<_, _>

  static member inline STEP(state : State<Tape<'cl, Dec, 'cr>, Tape<'tl, Z, 'tr>>) =
    StepDecZ(state) :> Step<_, _>

  static member inline STEP(State(code, data) : State<Tape< ^cl, End, ^cr>, _>) =
    StepEnd(State(code, data)) :> Step<_, _>

  static member inline STEP(State(code, data) : State<Tape< ^cl, MoveL, ^cr>, _>) =
    let sr = ShiftL(data) :> Shift<_, _, _>
    StepMoveL(State(code, data), sr) :> Step<_, _>

  static member inline STEP(State(code, data) : State<Tape< ^cl, MoveR, ^cr>, _>) =
    let sr = ShiftR(data) :> Shift<_, _, _>
    StepMoveR(State(code, data), sr) :> Step<_, _>

  static member inline STEP(State(Tape(_ : ^cl , Jmp(Left, rel : ^rel), _ : ^cr) as code,
                                  data : ^data) as state)
      : Step<State<Tape< ^cl, Jmp<Left, ^rel>, ^cr>, ^data>, State< ^code1, ^data>> =
    let sn = rel <<<- code
    StepJmp(state, sn) :> Step<_, _>

  static member inline STEP(State(Tape(_ : ^cl , Jmp(Right, rel : ^rel), _ : ^cr) as code,
                                  data : ^data) as state)
      : Step<State<Tape< ^cl, Jmp<Right, ^rel>, ^cr>, ^data>, State< ^code1, ^data>> =
    let sn = rel ->>> code
    StepJmp(state, sn) :> Step<_, _>

  static member inline STEP(state) = StepCondJZ(state) :> Step<_, _>

  static member inline STEP(State(Tape(_, CondJ(Left, rel : ^rel), _) as code, data) as state)
      : Step<State<Tape< ^cl, CondJ<Left, ^rel>, ^cr>, Tape<_, _ S, _>>, State<_, _>> =
    let sn = rel <<<- code
    StepCondJS(state, sn) :> Step<_, _>

  static member inline STEP(State(Tape(_ : ^cl , CondJ(Right, rel : ^rel), _ : ^cr) as code,
                                  data : Tape<_, _ S, _>) as state)
      : Step<State<Tape< ^cl, CondJ<Right, ^rel>, ^cr>, _>, State< ^code1, _>> =
    let sn = rel ->>> code
    StepCondJS(state, sn) :> Step<_, _>

  // Helper
  static member inline (!!!) (s : ^State) : ^StateResult =
    let s : Step< ^State, _> = ( ^State : (static member STEP : ^State -> _) s)
    let sr : ^SR = s.StepResult
    !!!! sr

  // Helper
  static member inline (!!!!) (sr : ^SR) : ^Result =
    let incpc : IncPC<_, _> = ( ^SR : (static member INCPC : ^SR -> _) sr)
    incpc.IncResult

  // Run and trace program to completion
  static member inline (!!!!!) (s) : C< ^Result, _> =
    C(s, !!!!! (!!! s))

type End with
  static member inline INCPC(End) = End
  static member inline (!!!!)(End) = End
  static member inline (!!!!!)(End) = C(End, E)

type C<'a, 'b> with
  static member inline (!!>)(C(a, E)) = a
  static member inline (!!>)(C(a, b)) = !!> b

  static member inline (!!>>)(C(a, C(_, E))) = a
  static member inline (!!>>)(C(a, b)) = !!>> b


#nowarn "1125"
//let s = State(Tape(E, Inc, C(MoveR, C(Inc, C(MoveL, C(Inc, C(Jmp(Left, n2), E)))))),
//              Tape(C(Z, C(Z, C(Z, C(Z, E)))), Z, C(Z, C(Z, C(Z, C(Z, E))))))
//let s = State(Tape(C(MoveL, C(Inc, C(MoveR, C(Inc, C(Inc, E))))), Jmp(Left, n5), C(MoveR, C(MoveR, E))),
//              Tape(C(Z, E), Z, C(Z, C(Z, E))))

// Program to compute 3 + 4: [->+<]+
let s =
  State(Tape(C(Dec, E),
             Dec,
             C(MoveR, C(Inc, C(MoveL, C(CondJ(Left, n5), C(MoveR, C(End, E))))))),
        Tape(E, n3, C(n4, E)))

// Run the entire program (s2 is a list of program states)
let s2 = !!!!! s

let finalState : State<_, Tape<C<Z,E>, N7, E>> = !!>> s2

let testRun() =
  printfn "--------------------"
  printfn "testRun()"
  printfn "finalState = %A" finalState
  printfn ""
  printfn "s2 = %A" s2
  printfn ""

  let inline p x = printfn "state = %A" x; x
  printfn "--------------------"
  printfn "s(init) = %A" s
  // Running the proram step by step (each s has a different type)
  let s = !!! s |> p
  let s = !!! s |> p
  let s = !!! s |> p
  let s = !!! s |> p
  let s = !!! s |> p
  let s = !!! s |> p
  let s = !!! s |> p
  let s = !!! s |> p
  let s = !!! s |> p
  let s = !!! s |> p
  let s = !!! s |> p
  let s = !!! s |> p
  let s = !!! s |> p
  let s = !!! s |> p
  let s = !!! s |> p
  // Final state: [0 7]
  //                 ^
  let s : State<_, Tape<C<Z,E>, N7, E>> = !!! s |> p
  let s1 = !!! s |> p
  let s : End = State.STEP(s).StepResult
  ()

do testRun()

// List reverser
type Rev<'l> when 'l :> L = Rev of 'l

type C<'a, 'b> with
  static member inline (><><) (C(x, l), Rev(r)) = l ><>< Rev(C(x, r))

type E with
  static member inline (><><) (E, Rev(r)) = r

let testReverse : C<N3, C<N2, C<N1, E>>> =
  C(n1, C(n2, C(n3, E))) ><>< Rev(E)

// BF to intermediate instruction set translator
module BFT =
  type SI = interface end

  type Plus = Plus with
    interface SI
    static member inline (!!-) Plus = Inc

  type Minus = Minus with
    interface SI
    static member inline (!!-) Minus = Dec

  type Lt = Lt with
    interface SI
    static member inline (!!-) Lt = MoveL

  type Gt = Gt with
    interface SI
    static member inline (!!-) Gt = MoveR

  type Open = Open
  type Close = Close

  type TransState<'pos, 'openStack, 'code, 'trans>
      when 'pos :> N and 'code :> L and 'trans :> L
      = TS of 'pos * 'openStack * 'code * 'trans with
    // (!!->) advances TransState by one step
    static member inline (!!->) (TS(pos, openStack, E, trans) as ts) =
      End

    static member inline (!!->) (TS(pos, openStack, C(Open, cs), trans) as ts) =
      TS(pos, C(pos, openStack), cs, trans)

    static member inline (!!->) (TS(pos, C(pos0, openStack), C(Close, cs), trans) as ts) =
      TS(S pos, openStack, cs, C(CondJ(Left, S(pos - pos0)), trans))

    static member inline (!!->) (TS(pos, openStack,
                                    C(si : ^x when ^x :> SI, cs), trans) as ts) =
      TS(S pos, openStack, cs, C(!!- si, trans))

    static member inline (!!!!!) ts =
      C(ts, !!!!! (!!-> ts))

  type InitTransState<'code when 'code :> L> = TransState<Z, E, 'code, E>

  // Translate from BF to intermediate
  let inline translate x =
    let step = !!>> !!!!! x
    match step with TS(_, _, _, trans) -> C(End, trans) ><>< Rev(E)

  let example : InitTransState<_> =
    TS(Z, E, C(Open, C(Minus, C(Gt, C(Plus, C(Lt, C(Close, C(Gt, E))))))), E)

  let e' = !!>> !!!!! example

  let translated = translate example
  let s' = State((n1 ->>> Tape(E, Dec, translated)).Shifted, Tape(E, n3, C(n4, E)))
  let test = s' = s // true

  let finalState' = !!>> !!!!! s'
  let test1 = finalState = finalState' // true

  printfn ""
  printfn "test=%A test1=%A" test test1

  let infiniteLoopExample : InitTransState<_> =
    TS(Z, E, C(Minus, C(Open, C(Plus, C(Close, E)))), E)
  let infiniteLoopTranslated = translate infiniteLoopExample

  let n = n1
  let s'' = State((n1 ->>> Tape(E, Dec, infiniteLoopTranslated)).Shifted, Tape(E, n, E))
  // Uncomment to get a compiler error
  //let finalState'' = !!>> !!!!! s''