HVM3 on Kind: initial Atomic Linker attempt

gistfile1.txt

// Higher-order Virtual Machine
// ============================

// Core Types
// ----------

data HVM/Pol {
  #Pos
  #Neg
}

data HVM/Term ~ (pol: HVM/Pol) {
  #Var{ uid: U64 } : (HVM/Term #Pos)
  #Sub{ uid: U64 } : (HVM/Term #Neg)
  #Nul : (HVM/Term #Pos)
  #Era : (HVM/Term #Neg)
  #Lam{ var: (HVM/Term #Neg) bod: (HVM/Term #Pos) } : (HVM/Term #Pos)
  #App{ arg: (HVM/Term #Pos) ret: (HVM/Term #Neg) } : (HVM/Term #Neg)
  #Sup{ tm1: (HVM/Term #Pos) tm2: (HVM/Term #Pos) } : (HVM/Term #Pos)
  #Dup{ dp1: (HVM/Term #Neg) dp2: (HVM/Term #Neg) } : (HVM/Term #Neg)
}

data HVM/Dex {
  #Dex{
    neg: (HVM/Term #Neg)
    pos: (HVM/Term #Pos)
  }
}

HVM/Bag : *
= (List HVM/Dex)

data HVM/Net {
  #Net{
    rot: (HVM/Term #Pos)
    bag: HVM/Bag
  }
}

// Runtime Types
// -------------

HVM/RTag : *
= U64

HVM/RLab  : * = U64
HVM/RLoc  : * = U64
HVM/RTerm : * = U64
HVM/RDex  : * = (Pair HVM/RTerm HVM/RTerm)
HVM/RBag  : * = (List (Pair U64 HVM/RDex))
HVM/RNod  : * = (List (Pair U64 HVM/RTerm))

data HVM/RNet {
  #RNet{
    rot: HVM/RTerm
    bag: HVM/RBag
    nod: HVM/RNod
  }
}

data HVM/RHeap {
  #RHeap{
    buff: (Map U64)
    rnod: (Pair U64 U64)
    rbag: (Pair U64 U64)
  }
}

HVM : * -> *
| A = (State HVM/RHeap A)

// Constants
// ---------

HVM/AIR : HVM/RTag = 0x00
HVM/VAR : HVM/RTag = 0x01
HVM/SUB : HVM/RTag = 0x02
HVM/NUL : HVM/RTag = 0x03
HVM/ERA : HVM/RTag = 0x04
HVM/LAM : HVM/RTag = 0x05
HVM/APP : HVM/RTag = 0x06
HVM/SUP : HVM/RTag = 0x07
HVM/DUP : HVM/RTag = 0x08

HVM/VOID : HVM/RTerm = 0x00000000_000000_00

HVM/RBAG : U64 = 0x1_0000_0000

// HVM Monad
// ---------

HVM/pure : ∀(A: *) A -> (HVM A)
= (State/pure HVM/RHeap)

HVM/bind : ∀(A: *) ∀(B: *) (HVM A) -> (A -> (HVM B)) -> (HVM B)
= (State/bind HVM/RHeap)

HVM/Monad : (Monad HVM)
= #Monad{
  pure: HVM/pure
  bind: HVM/bind
}

// Initialization
// --------------

HVM/Net/new : HVM/Net
= #Net{
  rot: #Nul
  bag: #Nil
}


HVM/RHeap/new : HVM/RHeap
= #RHeap{
  buff: {|0}
  rnod: #Pair{ 0 1 }
  rbag: #Pair{ 0 0 }
}

// Term
// ----

HVM/Term/is-sub : ∀(pol: HVM/Pol) (HVM/Term pol) -> Bool
| #Pos #Sub{uid} = #True
| pol  term      = #False

HVM/Term/is-var : ∀(pol: HVM/Pol) (HVM/Term pol) -> Bool
| #Pos #Var{uid} = #True
| pol  term      = #False

// RTerm
// -----


// TODO: implement HVM/RTerm/new
HVM/RTerm/new : HVM/RTag -> HVM/RLab -> HVM/RLoc -> HVM/RTerm
| tag lab loc = 
  let tag_enc = tag
  let lab_enc = (<< lab 8)
  let loc_enc = (<< loc 32)
  (| tag_enc (| lab_enc loc_enc))

HVM/RTerm/get-tag : ∀(x: U64) HVM/RTag
| x = (& x 0xFF)

HVM/RTerm/get-lab : ∀(x: U64) HVM/RLab
| x = (& (>> x 8) 0xFF_FFFF)

HVM/RTerm/get-loc : ∀(x: U64) HVM/RLoc
| x = (& (>> x 32) 0xFFFF_FFFF)

HVM/RTag/eq : HVM/RTag -> HVM/RTag -> Bool
| x y = (U64/to-bool (== x y))

HVM/RTag/pol : HVM/RTag -> (Maybe HVM/Pol)
| x = when HVM/RTag/eq x {
  HVM/VAR: #Some{#Pos}
  HVM/SUB: #Some{#Neg}
  HVM/NUL: #Some{#Pos}
  HVM/ERA: #Some{#Neg}
  HVM/LAM: #Some{#Pos}
  HVM/APP: #Some{#Neg}
  HVM/SUP: #Some{#Pos}
  HVM/DUP: #Some{#Neg}
} else {
  #None
}

HVM/port : U64 -> U64 -> U64
| n x = (+ n x)

HVM/get-rheap : (HVM HVM/RHeap)
= λrheap #Pair{ rheap rheap }

HVM/get-rbag-ini : (HVM U64)
| #RHeap{buff rnod #Pair{ini end}} = #Pair{#RHeap{buff rnod #Pair{ini end}} ini}

HVM/get-rbag-end : (HVM U64)
| #RHeap{buff rnod #Pair{ini end}} = #Pair{#RHeap{buff rnod #Pair{ini end}} end}

HVM/get-rnod-ini : (HVM U64)
| #RHeap{buff #Pair{ini end} rbag} = #Pair{#RHeap{buff #Pair{ini end} rbag} ini}

HVM/get-rnod-end : (HVM U64)
| #RHeap{buff #Pair{ini end} rbag} = #Pair{#RHeap{buff #Pair{ini end} rbag} end}

HVM/get-itrs : (HVM U64)
= do HVM {
  ask end = HVM/get-rbag-end
  ret (/ end 2)
}

// HVM Memory
// ----------

HVM/swap : HVM/RLoc -> HVM/RTerm -> (HVM HVM/RTerm)
| loc term #RHeap{buff rnod rbag} =
  put got = buff[loc] := term
  #Pair{#RHeap{buff rnod rbag} got}

HVM/get : U64 -> (HVM HVM/RTerm)
| loc #RHeap{buff rnod rbag} =
  get got = buff[loc]
  #Pair{#RHeap{buff rnod rbag} got}

HVM/set : U64 -> HVM/RTerm -> (HVM Unit)
| loc term = do HVM {
  ask (HVM/swap loc term)
  ret #Unit
}

HVM/del : U64 -> (HVM Unit)
| loc = do HVM {
  ask (HVM/swap loc HVM/VOID)
  ret #Unit
}

HVM/take_pos : U64 -> (HVM HVM/RTerm)
| loc = do HVM {
  (HVM/swap loc HVM/VOID)
}

HVM/take_neg : U64 -> (HVM HVM/RTerm)
| loc = do HVM {
  ask term = (HVM/swap loc (HVM/RTerm/new HVM/SUB 0 0))
  if (HVM/RTag/eq HVM/SUB (HVM/RTerm/get-tag term)) do HVM {
    ret term
  } else do HVM {
    ask (HVM/swap loc HVM/VOID)
    ret term
  }
}

HVM/init : U64 -> HVM/RTerm -> (HVM Unit)
| loc term = do HVM {
  ask old = (HVM/swap loc term)
  let air = (HVM/RTag/eq HVM/AIR (HVM/RTerm/get-tag old))
  if air do HVM {
    ret #Unit
  } else do HVM {
    ask (HVM/swap loc old)
    ret #Unit
  }
}

// Allocation
// ----------

HVM/alloc-rnod : U64 -> (HVM U64)
| arity #RHeap{buff #Pair{rnod_ini rnod_end} rbag} =
  #Pair{#RHeap{buff #Pair{rnod_ini (+ rnod_end arity)} rbag} rnod_end}

HVM/alloc-redex : (HVM U64)
| #RHeap{buff rnod #Pair{rbag_ini rbag_end}} =
  #Pair{#RHeap{buff rnod #Pair{rbag_ini (+ rbag_end 2)}} (+ HVM/RBAG rbag_end)}

HVM/next-redex : (HVM (Maybe U64))
| #RHeap{buff rnod #Pair{rbag_ini rbag_end}} =
  if (U64/to-bool (< rbag_ini rbag_end)) {
    #Pair{#RHeap{buff rnod #Pair{(+ rbag_ini 2) rbag_end}} #Some{(+ HVM/RBAG rbag_ini)}}
  } else {
    #Pair{#RHeap{buff rnod #Pair{rbag_ini rbag_end}} #None}
  }

HVM/push-redex : HVM/RDex -> (HVM Unit)
| #Pair{neg pos} = do HVM {
  ask loc = HVM/alloc-redex
  ask (HVM/set (+ loc 0) neg)
  ask (HVM/set (+ loc 1) pos)
  log #PUSH{(HVM/RTerm/get-tag neg) (HVM/RTerm/get-loc neg) (HVM/RTerm/get-tag pos) (HVM/RTerm/get-loc pos)}
  ret #Unit
}

HVM/pop-redex : (HVM (Maybe HVM/RDex))
= do HVM {
  ask loc = HVM/next-redex
  match loc {
    #None: do HVM {
      ret #None
    }
    #Some{loc}: do HVM {
      ask neg = (HVM/get (+ loc 0))
      ask pos = (HVM/get (+ loc 1))
      ask (HVM/set (+ loc 0) HVM/VOID)
      ask (HVM/set (+ loc 1) HVM/VOID)
      ret #Some{#Pair{ neg pos }}
    }
  }
}

// Injection
// ---------
// Writes core terms into runtime memory.

HVM/VarMap : * = (Map (Maybe U64))

HVM/inject-term : ∀(p: HVM/Pol) (HVM/Term p) -> (Maybe U64) -> HVM/VarMap -> (HVM (Pair HVM/VarMap HVM/RTerm))
| p #Lam{var bod} host vars = do HVM {
  ask lam             = (HVM/alloc-rnod 3)
  ask #Pair{vars var} = (HVM/inject-term #Neg var #Some{(HVM/port 1 lam)} vars)
  ask #Pair{vars bod} = (HVM/inject-term #Pos bod #Some{(HVM/port 2 lam)} vars)
  ask (HVM/init (HVM/port 1 lam) var)
  ask (HVM/init (HVM/port 2 lam) bod)
  ret #Pair{ vars (HVM/RTerm/new HVM/LAM 0 lam) }
}
| p #App{arg ret} host vars = do HVM {
  ask app             = (HVM/alloc-rnod 3)
  ask #Pair{vars arg} = (HVM/inject-term #Pos arg #Some{(HVM/port 1 app)} vars)
  ask #Pair{vars ret} = (HVM/inject-term #Neg ret #Some{(HVM/port 2 app)} vars)
  ask (HVM/init (HVM/port 1 app) arg)
  ask (HVM/init (HVM/port 2 app) ret)
  ret #Pair{ vars (HVM/RTerm/new HVM/APP 0 app) }
}
| p #Sup{tm1 tm2} host vars = do HVM {
  ask sup             = (HVM/alloc-rnod 3)
  ask #Pair{vars tm1} = (HVM/inject-term #Pos tm1 #Some{(HVM/port 1 sup)} vars)
  ask #Pair{vars tm2} = (HVM/inject-term #Pos tm2 #Some{(HVM/port 2 sup)} vars)
  ask (HVM/init (HVM/port 1 sup) tm1)
  ask (HVM/init (HVM/port 2 sup) tm2)
  ret #Pair{ vars (HVM/RTerm/new HVM/SUP 0 sup) }
}
| p #Dup{dp1 dp2} host vars = do HVM {
  ask dup             = (HVM/alloc-rnod 3)
  ask #Pair{vars dp1} = (HVM/inject-term #Neg dp1 #Some{(HVM/port 1 dup)} vars)
  ask #Pair{vars dp2} = (HVM/inject-term #Neg dp2 #Some{(HVM/port 2 dup)} vars)
  ask (HVM/init (HVM/port 1 dup) dp1)
  ask (HVM/init (HVM/port 2 dup) dp2)
  ret #Pair{ vars (HVM/RTerm/new HVM/DUP 0 dup) }
}
| p #Var{uid} #None vars = do HVM {
  ret log "ERR-B" #Pair{ vars HVM/VOID }
}
| p #Var{uid} #Some{host} vars = 
  put got = vars[uid] := #Some{host}
  match got {
    #None: do HVM { ret #Pair{ vars (HVM/RTerm/new HVM/NUL 0 0) } }
    #Some{neg_host}: do HVM { ret #Pair{ vars (HVM/RTerm/new HVM/VAR 0 neg_host) } }
  }
| p #Sub{uid} #None vars = do HVM {
  ret log "ERR-C" #Pair{ vars HVM/VOID }
}
| p #Sub{uid} #Some{host} vars = 
  put got = vars[uid] := #Some{host}
  match got {
    #None: do HVM { ret #Pair{ vars (HVM/RTerm/new HVM/SUB 0 host) } }
    #Some{pos_host}: do HVM {
      ask (HVM/set pos_host ((HVM/RTerm/new HVM/VAR 0 host)))
      ret #Pair{ vars (HVM/RTerm/new HVM/SUB 0 host) }
    }
  }
| p #Nul host vars = do HVM {
  ret #Pair{ vars (HVM/RTerm/new HVM/NUL 0 0) }
}
| p #Era host vars = do HVM {
  ret #Pair{ vars (HVM/RTerm/new HVM/ERA 0 0) }
}

HVM/inject-redex : HVM/Dex -> HVM/VarMap -> (HVM HVM/VarMap)
| #Dex{neg pos} vars = do HVM {
  ask #Pair{vars neg} = (HVM/inject-term #Neg neg #None vars)
  ask #Pair{vars pos} = (HVM/inject-term #Pos pos #None vars)
  ask (HVM/push-redex #Pair{neg pos})
  ret vars
}

HVM/inject-net : HVM/Net -> HVM/VarMap -> (HVM (Pair HVM/VarMap HVM/RTerm))
| #Net{rot bag} vars = do HVM {
  ask #Pair{vars rot} = (HVM/inject-term #Pos rot #Some{0} vars)
  ask vars = for dex in bag {
    (HVM/inject-redex dex vars)
  }
  ret #Pair{ vars rot }
}

HVM/do-inject-net : HVM/Net -> (HVM HVM/RTerm)
| net = do HVM {
  ask #Pair{x rot} = (HVM/inject-net net {|#None})
  ret rot
}

// Dumping
// -------
// Reads from runtime memory to handy containers.

HVM/dump : U64 -> U64 -> (HVM HVM/RNod)
| ini end = if (U64/to-bool (< ini end)) do HVM {
  ask head = (HVM/get ini)
  ask tail = (HVM/dump (+ 1 ini) end)
  ret #Cons{(ini,head) tail}
} else do HVM {
  ret #Nil
}

HVM/dump-rbag : (HVM HVM/RBag)
= do HVM {
  ask ini = HVM/get-rbag-ini
  ask end = HVM/get-rbag-end
  ask bag = (HVM/dump (+ HVM/RBAG ini) (+ HVM/RBAG end))
  use bag = (List/chunks-of _ #2 bag)
  use bag = (List/map _ _ bag (λirs
    use #Pair{ir0 ir1} = (Pair/from-list (Pair U64 HVM/RTerm) #Pair{0 HVM/VOID} irs)
    use #Pair{i0 r0}   = ir0
    use #Pair{i1 r1}   = ir1
    #Pair{i0 #Pair{r0 r1}}
  ))
  ret bag
}

HVM/dump-rnod : (HVM HVM/RNod)
= do HVM {
  ask ini = HVM/get-rnod-ini
  ask end = HVM/get-rnod-end
  (HVM/dump ini end)
}

HVM/dump-rnet : (HVM HVM/RNet)
= do HVM {
  ask rot = (HVM/get 0)
  ask bag = HVM/dump-rbag
  ask nod = HVM/dump-rnod
  ret #RNet{ rot bag nod }
}

// Recovery
// --------
// Reads from runtime memory to core terms.

HVM/recover-var : U64 -> HVM/RTerm -> (HVM (HVM/Term #Pos))
| var term = when HVM/RTag/eq (HVM/RTerm/get-tag term) {
  HVM/AIR: do HVM { ret log "ERR-D" #Nul }
  HVM/ERA: do HVM { ret log "ERR-E" #Nul }
  HVM/APP: do HVM { ret log "ERR-F" #Nul }
  HVM/DUP: do HVM { ret log "ERR-G" #Nul }
  HVM/VAR: (HVM/recover-term #Pos term)
  HVM/NUL: (HVM/recover-term #Pos term)
  HVM/LAM: (HVM/recover-term #Pos term)
  HVM/SUP: (HVM/recover-term #Pos term)
  HVM/SUB: if (U64/eq var (HVM/RTerm/get-loc term)) do HVM {
    ret #Var{(HVM/RTerm/get-loc term)}
  } else {
    (HVM/recover-term #Pos (HVM/RTerm/new HVM/SUB 0 (HVM/RTerm/get-loc term)))
  }
} else {
  do HVM { ret log "ERR-X" #Nul }
}

HVM/recover-sub : U64 -> HVM/RTerm -> (HVM (HVM/Term #Neg))
| sub term = when HVM/RTag/eq (HVM/RTerm/get-tag term) {
  HVM/AIR: do HVM { ret log "ERR-H" #Era }
  HVM/NUL: do HVM { ret log "ERR-I" #Era }
  HVM/LAM: do HVM { ret log "ERR-J" #Era }
  HVM/SUP: do HVM { ret log "ERR-K" #Era }
  HVM/VAR: (HVM/recover-term #Neg term)
  HVM/ERA: (HVM/recover-term #Neg term)
  HVM/APP: (HVM/recover-term #Neg term)
  HVM/DUP: (HVM/recover-term #Neg term)
  HVM/SUB: if (U64/eq sub (HVM/RTerm/get-loc term)) do HVM {
    ret #Sub{(HVM/RTerm/get-loc term)}
  } else {
    (HVM/recover-term #Neg (HVM/RTerm/new HVM/SUB 0 (HVM/RTerm/get-loc term)))
  }
} else {
  do HVM { ret log "ERR-X" #Era }
}

HVM/recover-term : ∀(p: HVM/Pol) (HVM/RTerm) -> (HVM (HVM/Term p))
| #Pos term = when HVM/RTag/eq (HVM/RTerm/get-tag term) {
  HVM/AIR: do HVM { ret #Nul }
  HVM/NUL: do HVM { ret #Nul }
  HVM/VAR: do HVM {
    ask got = (HVM/get (HVM/RTerm/get-loc term))
    (HVM/recover-var (HVM/RTerm/get-loc term) got)
  }
  HVM/LAM: do HVM {
    let loc = (HVM/RTerm/get-loc term)
    ask var = (HVM/get (HVM/port 1 loc))
    ask bod = (HVM/get (HVM/port 2 loc))
    ask var = (HVM/recover-term #Neg var)
    ask bod = (HVM/recover-term #Pos bod)
    ret #Lam{var bod}
  }
  HVM/SUP: do HVM {
    let loc = (HVM/RTerm/get-loc term)
    ask tm1 = (HVM/get (HVM/port 1 loc))
    ask tm2 = (HVM/get (HVM/port 2 loc))
    ask tm1 = (HVM/recover-term #Pos tm1)
    ask tm2 = (HVM/recover-term #Pos tm2)
    ret #Sup{tm1 tm2}
  }
  HVM/SUB: do HVM { ret log "ERR-L" #Nul }
  HVM/ERA: do HVM { ret log "ERR-M" #Nul }
  HVM/APP: do HVM { ret log "ERR-N" #Nul }
  HVM/DUP: do HVM { ret log "ERR-O" #Nul }
} else {
  do HVM { ret log "ERR-X" #Nul }
}
| #Neg term = when HVM/RTag/eq (HVM/RTerm/get-tag term) {
  HVM/AIR: do HVM { ret #Era }
  HVM/ERA: do HVM { ret #Era }
  HVM/SUB: do HVM {
    ask got = (HVM/get (HVM/RTerm/get-loc term))
    (HVM/recover-sub (HVM/RTerm/get-loc term) got)
  }
  HVM/APP: do HVM {
    let loc = (HVM/RTerm/get-loc term)
    ask arg = (HVM/get (HVM/port 1 loc))
    ask ret = (HVM/get (HVM/port 2 loc))
    ask arg = (HVM/recover-term #Pos arg)
    ask ret = (HVM/recover-term #Neg ret)
    ret #App{arg ret}
  }
  HVM/DUP: do HVM {
    let loc = (HVM/RTerm/get-loc term)
    ask dp1 = (HVM/get (HVM/port 1 loc))
    ask dp2 = (HVM/get (HVM/port 2 loc))
    ask dp1 = (HVM/recover-term #Neg dp1)
    ask dp2 = (HVM/recover-term #Neg dp2)
    ret #Dup{dp1 dp2}
  }
  HVM/VAR: do HVM { ret log "ERR-P" #Era }
  HVM/NUL: do HVM { ret log "ERR-Q" #Era }
  HVM/LAM: do HVM { ret log "ERR-R" #Era }
  HVM/SUP: do HVM { ret log "ERR-S" #Era }
} else {
  do HVM { ret log "ERR-X" #Era }
}

HVM/recover-rot : (HVM (HVM/Term #Pos))
= do HVM {
  ask rot = (HVM/get 0)
  (HVM/recover-term #Pos rot)
}

HVM/recover-bag : (HVM HVM/Bag)
= do HVM {
  ask rbag = HVM/dump-rbag
  let bag  = [] :: HVM/Bag
  ask bag  = for loc_rdx in rbag {
    let #Pair{loc rdx} = loc_rdx
    let #Pair{neg pos} = rdx
    ask neg = (HVM/recover-term #Neg neg)
    ask pos = (HVM/recover-term #Pos pos)
    ret #Cons{ #Dex{neg pos} bag }
  }
  ret bag
}

HVM/recover-net : (HVM HVM/Net)
= do HVM {
  ask rot = HVM/recover-rot
  ask bag = HVM/recover-bag
  ret #Net{ rot bag }
}

// Running
// -------

HVM/boot : HVM/Net -> (HVM Unit)
= λnet do HVM {
  ask rot = (HVM/do-inject-net net)
  ask (HVM/init 0 rot)
  ret #Unit
}

HVM/run : ∀(A: *) (HVM A) -> A
= λA λhvm match (hvm HVM/RHeap/new) {
  #Pair{net x}: x
}

// Showing
// -------

HVM/Term/to-string : ∀(p: HVM/Pol) (HVM/Term p) -> String
| #Pos #Var{uid}     = (String/join "" ["+" (U64/to-hex-string uid)])
| #Pos #Sub{uid}     = #void
| #Pos #Nul          = "+*"
| #Pos #Era          = #void
| #Pos #Lam{var bod} = (String/join "" ["+(" (HVM/Term/to-string #Neg var) " " (HVM/Term/to-string #Pos bod) ")"])
| #Pos #App{arg ret} = #void
| #Pos #Sup{tm1 tm2} = (String/join "" ["+{" (HVM/Term/to-string #Pos tm1) " " (HVM/Term/to-string #Pos tm2) "}"])
| #Pos #Dup{dp1 dp2} = #void
| #Neg #Var{uid}     = #void
| #Neg #Sub{uid}     = (String/join "" ["-" (U64/to-hex-string uid)])
| #Neg #Nul          = #void
| #Neg #Era          = "-*"
| #Neg #Lam{var bod} = #void
| #Neg #App{arg ret} = (String/join "" ["-(" (HVM/Term/to-string #Pos arg) " " (HVM/Term/to-string #Neg ret) ")"])
| #Neg #Sup{tm1 tm2} = #void
| #Neg #Dup{dp1 dp2} = (String/join "" ["-{" (HVM/Term/to-string #Neg dp1) " " (HVM/Term/to-string #Neg dp2) "}"])

HVM/Bag/to-string : HVM/Bag -> String
| #Nil                        = ""
| #Cons{#Dex{neg pos} rest} = (String/join "" ["\n& " (HVM/Term/to-string #Neg neg) " ~ " (HVM/Term/to-string #Pos pos) (HVM/Bag/to-string rest)])

HVM/Net/to-string : HVM/Net -> String
| #Net{rot bag} = (String/join "" [(HVM/Term/to-string #Pos rot) (HVM/Bag/to-string bag)])

HVM/RTag/to-string : HVM/RTag -> String
| tag = when HVM/RTag/eq tag {
  HVM/AIR: "AIR"
  HVM/VAR: "VAR"
  HVM/SUB: "SUB"
  HVM/NUL: "NUL"
  HVM/ERA: "ERA"
  HVM/LAM: "LAM"
  HVM/APP: "APP"
  HVM/SUP: "SUP"
  HVM/DUP: "DUP"
} else {
  "???"
}

HVM/RLab/to-string : U64 -> String
| loc = (String/pad-left (U64/to-hex-string loc) #6 '0')

HVM/RLoc/to-string : U64 -> String
| loc = (String/pad-left (U64/to-hex-string loc) #9 '0')

HVM/RTerm/to-string : HVM/RTerm -> String 
| term =
  let tag = (HVM/RTag/to-string (HVM/RTerm/get-tag term))
  let lab = (HVM/RLab/to-string (HVM/RTerm/get-lab term))
  let loc = (HVM/RLoc/to-string (HVM/RTerm/get-loc term))
  (String/join "" [tag ":" lab ":" loc])

HVM/RDex/to-string : HVM/RDex -> String
| #Pair{neg pos} = (String/join "" [(HVM/RTerm/to-string neg) " ~ " (HVM/RTerm/to-string pos)])

HVM/RBag/to-string : HVM/RBag -> String
| bag = (List/fold _ bag _ "" (λkv λtxt
  let #Pair{k v} = kv
  let addr       = (String/pad-left (U64/to-hex-string k) #9 '0')
  let dex        = (HVM/RDex/to-string v)
  (String/join "" [addr " → " dex "\n" txt])
))

HVM/RNod/to-string : HVM/RNod -> String
| nod = (List/fold _ nod _ "" (λkv λtxt
  let #Pair{k v} = kv
  let addr       = (String/pad-left (U64/to-hex-string k) #9 '0')
  let term       = (HVM/RTerm/to-string v)
  (String/join "" [addr " → " term "\n" txt])
))

HVM/RNet/to-string : HVM/RNet -> String
| #RNet{rot bag nod} = 
  (String/join "" [
    "ROT:\n" (HVM/RTerm/to-string rot) "\n"
    "BAG:\n" (HVM/RBag/to-string bag)
    "NOD:\n" (HVM/RNod/to-string nod)])

// Parser
// ------

HVM/parse-term : ∀(p: HVM/Pol) (Parser (HVM/Term p))
| #Pos = do Parser {
  ask Parser/skip-trivia
  //ask text = Parser/get-input
  //log (String/join "" ["[[" text "]]"])
  ask head = Parser/peek-one
  when (Maybe/eq-with _ U64/eq) head {
    #Some{'('} : do Parser {
      ask (Parser/consume "(")
      ask var = (HVM/parse-term #Neg)
      ask bod = (HVM/parse-term #Pos)
      ask (Parser/consume ")")
      ret #Lam { var bod }
    }
    #Some{'{'} : do Parser {
      ask (Parser/consume "{")
      ask tm1 = (HVM/parse-term #Pos)
      ask tm2 = (HVM/parse-term #Pos)
      ask (Parser/consume "}")
      ret #Sup { tm1 tm2 }
    }
    #Some{'*'} : do Parser {
      ask (Parser/consume "*")
      ret #Nul
    }
  } else {
    do Parser {
      ask name = Parser/parse-name
      ret #Var { (U64/from-bits (String/to-bits name)) }
    }
  }
}
| #Neg = do Parser {
  ask Parser/skip-trivia
  ask head = Parser/peek-one
  when (Maybe/eq-with _ U64/eq) head {
    #Some{'('} : do Parser {
      ask (Parser/consume "(")
      ask arg = (HVM/parse-term #Pos)
      ask ret = (HVM/parse-term #Neg)
      ask (Parser/consume ")")
      ret #App { arg ret }
    }
    #Some{'{'} : do Parser {
      ask (Parser/consume "{")
      ask dp1 = (HVM/parse-term #Neg)
      ask dp2 = (HVM/parse-term #Neg)
      ask (Parser/consume "}")
      ret #Dup { dp1 dp2 }
    }
    #Some{'*'} : do Parser {
      ask (Parser/consume "*")
      ret #Era
    }
  } else {
    do Parser {
      ask name = Parser/parse-name
      ret #Sub { (U64/from-bits (String/to-bits name)) }
    }
  }
}

HVM/parse-bag : (Parser HVM/Bag)
= do Parser {
  ask Parser/skip-trivia
  ask head = Parser/peek-one
  when (Maybe/eq-with _ U64/eq) head {
    #Some{'&'} : do Parser {
      ask (Parser/consume "&")
      ask neg = (HVM/parse-term #Neg)
      ask Parser/skip-trivia
      ask (Parser/consume "~")
      ask pos = (HVM/parse-term #Pos)
      ask rest = HVM/parse-bag
      ret #Cons{ #Dex{neg pos} rest }
    }
  } else {
    do Parser {
      ret #Nil
    }
  }
}

HVM/parse-net : (Parser HVM/Net)
= do Parser {
  ask rot = (HVM/parse-term #Pos)
  ask bag = HVM/parse-bag
  ret #Net{ rot bag }
}

HVM/do-parse-net : String -> HVM/Net
= λcode (Maybe/run _ (Parser/run _ HVM/parse-net code) HVM/Net/new)

// Linking
// -------

HVM/link : HVM/RTerm -> HVM/RTerm -> (HVM Unit)
| a b =
  let a_tag = (HVM/RTerm/get-tag a)
  let a_loc = (HVM/RTerm/get-loc a)
  let b_tag = (HVM/RTerm/get-tag b)
  let b_loc = (HVM/RTerm/get-loc b)
  //log #LINK{#View{(HVM/RTag/to-string a_tag)} a_loc #View{(HVM/RTag/to-string b_tag)} b_loc}
  if (HVM/RTag/eq a_tag HVM/SUB) do HVM {
    //log "X<~B" 
    ask x = (HVM/swap a_loc b)
    if (HVM/RTag/eq (HVM/RTerm/get-tag x) HVM/SUB) do HVM {
      log "link X<~P subs" 
      ret #Unit
    } else do HVM {
      log "link X<~P done" 
      ask b = (HVM/swap a_loc HVM/VOID)
      (HVM/link x b)
    }
  } else if (HVM/RTag/eq b_tag HVM/VAR) do HVM {
    //log "A~>X"
    ask x = (HVM/swap b_loc a)
    if (HVM/RTag/eq (HVM/RTerm/get-tag x) HVM/SUB) do HVM {
      log "link N~>X subs"
      ret #Unit
    } else do HVM {
      log "link N~>X done"
      ask a = (HVM/swap b_loc HVM/VOID)
      (HVM/link a x)
    }
  } else do HVM {
    log "link N~~P"
    ask (HVM/push-redex #Pair{a b})
    ret #Unit
  }

// Interaction
// -----------

HVM/interact : HVM/RTerm -> HVM/RTerm -> (HVM Unit)
| a b =
  let a_tag = (HVM/RTerm/get-tag a)
  let a_lab = (HVM/RTerm/get-lab a)
  let a_loc = (HVM/RTerm/get-loc a)
  let b_tag = (HVM/RTerm/get-tag b)
  let b_lab = (HVM/RTerm/get-lab b)
  let b_loc = (HVM/RTerm/get-loc b)
  when HVM/RTag/eq a_tag {
    HVM/APP: when HVM/RTag/eq b_tag {
      HVM/LAM: do HVM {
        log "APP-LAM"
        ask arg = (HVM/take_pos (HVM/port 1 a_loc))
        ask ret = (HVM/take_neg (HVM/port 2 a_loc))
        ask var = (HVM/take_neg (HVM/port 1 b_loc))
        ask bod = (HVM/take_pos (HVM/port 2 b_loc))
        ask (HVM/link var arg)
        ask (HVM/link ret bod)
        ret #Unit
      }
      HVM/SUP: do HVM {
        log "APP-SUP"
        ask arg = (HVM/take_pos (HVM/port 1 a_loc))
        ask ret = (HVM/take_neg (HVM/port 2 a_loc))
        ask tm1 = (HVM/take_pos (HVM/port 1 b_loc))
        ask tm2 = (HVM/take_pos (HVM/port 2 b_loc))
        ask dp1 = (HVM/alloc-rnod 3)
        ask dp2 = (HVM/alloc-rnod 3)
        ask cn1 = (HVM/alloc-rnod 3)
        ask cn2 = (HVM/alloc-rnod 3)
        ask (HVM/set (HVM/port 1 dp1) (HVM/RTerm/new HVM/SUB 0 (HVM/port 1 dp1)))
        ask (HVM/set (HVM/port 2 dp1) (HVM/RTerm/new HVM/SUB 0 (HVM/port 2 dp1)))
        ask (HVM/set (HVM/port 1 dp2) (HVM/RTerm/new HVM/VAR 0 (HVM/port 2 cn1)))
        ask (HVM/set (HVM/port 2 dp2) (HVM/RTerm/new HVM/VAR 0 (HVM/port 2 cn2)))
        ask (HVM/set (HVM/port 1 cn1) (HVM/RTerm/new HVM/VAR 0 (HVM/port 1 dp1)))
        ask (HVM/set (HVM/port 2 cn1) (HVM/RTerm/new HVM/SUB 0 (HVM/port 2 cn1)))
        ask (HVM/set (HVM/port 1 cn2) (HVM/RTerm/new HVM/VAR 0 (HVM/port 2 dp1)))
        ask (HVM/set (HVM/port 2 cn2) (HVM/RTerm/new HVM/SUB 0 (HVM/port 2 cn2)))
        ask (HVM/link (HVM/RTerm/new HVM/DUP 0 dp1) arg)
        ask (HVM/link ret (HVM/RTerm/new HVM/SUP 0 dp2))
        ask (HVM/link (HVM/RTerm/new HVM/APP 0 cn1) tm1)
        ask (HVM/link (HVM/RTerm/new HVM/APP 0 cn2) tm2)
        ret #Unit
      }
      HVM/NUL: do HVM {
        log "APP-NUL"
        ask arg = (HVM/take_pos (HVM/port 1 a_loc))
        ask ret = (HVM/take_neg (HVM/port 2 a_loc))
        ask (HVM/link (HVM/RTerm/new HVM/ERA 0 0) arg)
        ask (HVM/link ret (HVM/RTerm/new HVM/NUL 0 0))
        ret #Unit
      }
    } else { do HVM { ret #Unit } }
    HVM/DUP: when HVM/RTag/eq b_tag {
      HVM/SUP: do HVM {
        log "DUP-SUP"
        ask dp1 = (HVM/take_neg (HVM/port 1 a_loc))
        ask dp2 = (HVM/take_neg (HVM/port 2 a_loc))
        ask tm1 = (HVM/take_pos (HVM/port 1 b_loc))
        ask tm2 = (HVM/take_pos (HVM/port 2 b_loc))
        ask (HVM/link dp1 tm1)
        ask (HVM/link dp2 tm2)
        ret #Unit
      }
      HVM/LAM: do HVM {
        log "DUP-LAM"
        ask dp1 = (HVM/take_neg (HVM/port 1 a_loc))
        ask dp2 = (HVM/take_neg (HVM/port 2 a_loc))
        ask var = (HVM/take_neg (HVM/port 1 b_loc))
        ask bod = (HVM/take_pos (HVM/port 2 b_loc))
        ask co1 = (HVM/alloc-rnod 3)
        ask co2 = (HVM/alloc-rnod 3)
        ask du1 = (HVM/alloc-rnod 3)
        ask du2 = (HVM/alloc-rnod 3)
        ask (HVM/set (HVM/port 1 co1) (HVM/RTerm/new HVM/SUB 0 (HVM/port 1 co1)))
        ask (HVM/set (HVM/port 2 co1) (HVM/RTerm/new HVM/VAR 0 (HVM/port 1 du2)))
        ask (HVM/set (HVM/port 1 co2) (HVM/RTerm/new HVM/SUB 0 (HVM/port 1 co2)))
        ask (HVM/set (HVM/port 2 co2) (HVM/RTerm/new HVM/VAR 0 (HVM/port 2 du2)))
        ask (HVM/set (HVM/port 1 du1) (HVM/RTerm/new HVM/VAR 0 (HVM/port 1 co1)))
        ask (HVM/set (HVM/port 2 du1) (HVM/RTerm/new HVM/VAR 0 (HVM/port 1 co2)))
        ask (HVM/set (HVM/port 1 du2) (HVM/RTerm/new HVM/SUB 0 (HVM/port 1 du2)))
        ask (HVM/set (HVM/port 2 du2) (HVM/RTerm/new HVM/SUB 0 (HVM/port 2 du2)))
        ask (HVM/link dp1 (HVM/RTerm/new HVM/LAM 0 co1))
        ask (HVM/link dp2 (HVM/RTerm/new HVM/LAM 0 co2))
        ask (HVM/link var (HVM/RTerm/new HVM/SUP 0 du1))
        ask (HVM/link (HVM/RTerm/new HVM/DUP 0 du2) bod)
        ret #Unit
      }
      HVM/NUL: do HVM {
        log "DUP-NUL"
        ask dp1 = (HVM/take_neg (HVM/port 1 a_loc))
        ask dp2 = (HVM/take_neg (HVM/port 2 a_loc))
        ask (HVM/link dp1 (HVM/RTerm/new HVM/NUL 0 0))
        ask (HVM/link dp2 (HVM/RTerm/new HVM/NUL 0 0))
        ret #Unit
      }
    } else { do HVM { ret #Unit } }
    HVM/ERA: when HVM/RTag/eq b_tag {
      HVM/LAM: do HVM {
        log "ERA-LAM"
        ask var = (HVM/take_neg (HVM/port 1 b_loc))
        ask bod = (HVM/take_pos (HVM/port 2 b_loc))
        ask (HVM/link var (HVM/RTerm/new HVM/NUL 0 0))
        ask (HVM/link (HVM/RTerm/new HVM/ERA 0 0) bod)
        ret #Unit
      }
      HVM/SUP: do HVM {
        log "ERA-SUP"
        ask tm1 = (HVM/take_pos (HVM/port 1 b_loc))
        ask tm2 = (HVM/take_pos (HVM/port 2 b_loc))
        ask (HVM/link (HVM/RTerm/new HVM/ERA 0 0) tm1)
        ask (HVM/link (HVM/RTerm/new HVM/ERA 0 0) tm2)
        ret #Unit
      }
      HVM/NUL: do HVM {
        log "ERA-NUL"
        ret #Unit
      }
    } else { do HVM { ret #Unit } }
  } else { do HVM { ret #Unit } }

// Evaluation
// ----------

HVM/eval-one : (HVM Bool)
= do HVM {
  ask redex = HVM/pop-redex
  match redex {
    #Some{neg_pos}:
      let #Pair{neg pos} = neg_pos
      do HVM {
        //log #RULE{a b}
        ask (HVM/interact neg pos)
        ret #True
      }
    #None: do HVM {
      ret #False
    }
  }
}

HVM/eval-strict : (HVM Unit)
= λnet match (HVM/eval-one net) {
  #Pair{net changed}: match changed {
    #True: (HVM/eval-strict net)
    #False: #Pair{net #Unit}
  }
}

// Main
// ----

main
: String/View
= (HVM/run _ do HVM {

  // not^(2^4)(true) - 264 ITRS
  let f4 = "q
    & ((p (* p)) q) ~ (m o)
    & {(e f) (d e)} ~ (((* (a a)) ((b (* b)) c)) c)
    & {(h i) (g h)} ~ (d f)
    & {(k l) (j k)} ~ (g i)
    & {(n o) (m n)} ~ (j l)
  "

  // not^(2^8)(true) - 4120 ITRS
  let f8 = "cb
    & ((bb (* bb)) cb) ~ (y ab)
    & {(e f) (d e)} ~ (((* (a a)) ((b (* b)) c)) c)
    & {(h i) (g h)} ~ (d f)
    & {(k l) (j k)} ~ (g i)
    & {(n o) (m n)} ~ (j l)
    & {(q r) (p q)} ~ (m o)
    & {(t u) (s t)} ~ (p r)
    & {(w x) (v w)} ~ (s u)
    & {(z ab) (y z)} ~ (v x)
  "

  // not^(2^12)(true) - 65576 ITRS
  let fC = "ob
    & ((nb (* nb)) ob) ~ (kb mb)
    & {(e f) (d e)} ~ (((* (a a)) ((b (* b)) c)) c)
    & {(h i) (g h)} ~ (d f)
    & {(k l) (j k)} ~ (g i)
    & {(n o) (m n)} ~ (j l)
    & {(q r) (p q)} ~ (m o)
    & {(t u) (s t)} ~ (p r)
    & {(w x) (v w)} ~ (s u)
    & {(z ab) (y z)} ~ (v x)
    & {(cb db) (bb cb)} ~ (y ab)
    & {(fb gb) (eb fb)} ~ (bb db)
    & {(ib jb) (hb ib)} ~ (eb gb)
    & {(lb mb) (kb lb)} ~ (hb jb)
  "

  // not^(2^14)(true) - 262192 ITRS
  let fC = "ub
    & ((tb (* tb)) ub) ~ (qb sb)
    & {(e f) (d e)} ~ (((* (a a)) ((b (* b)) c)) c)
    & {(h i) (g h)} ~ (d f)
    & {(k l) (j k)} ~ (g i)
    & {(n o) (m n)} ~ (j l)
    & {(q r) (p q)} ~ (m o)
    & {(t u) (s t)} ~ (p r)
    & {(w x) (v w)} ~ (s u)
    & {(z ab) (y z)} ~ (v x)
    & {(cb db) (bb cb)} ~ (y ab)
    & {(fb gb) (eb fb)} ~ (bb db)
    & {(ib jb) (hb ib)} ~ (eb gb)
    & {(lb mb) (kb lb)} ~ (hb jb)
    & {(ob pb) (nb ob)} ~ (kb mb)
    & {(rb sb) (qb rb)} ~ (nb pb)"

  // not^(2^16)(true) - 1048632 ITRS
  let fG = "ac
    & ((zb (* zb)) ac) ~ (wb yb)
    & {(e f) (d e)} ~ (((* (a a)) ((b (* b)) c)) c)
    & {(h i) (g h)} ~ (d f)
    & {(k l) (j k)} ~ (g i)
    & {(n o) (m n)} ~ (j l)
    & {(q r) (p q)} ~ (m o)
    & {(t u) (s t)} ~ (p r)
    & {(w x) (v w)} ~ (s u)
    & {(z ab) (y z)} ~ (v x)
    & {(cb db) (bb cb)} ~ (y ab)
    & {(fb gb) (eb fb)} ~ (bb db)
    & {(ib jb) (hb ib)} ~ (eb gb)
    & {(lb mb) (kb lb)} ~ (hb jb)
    & {(ob pb) (nb ob)} ~ (kb mb)
    & {(rb sb) (qb rb)} ~ (nb pb)
    & {(ub vb) (tb ub)} ~ (qb sb)
    & {(xb yb) (wb xb)} ~ (tb vb)
  "

  let ops = "
    *
    & (* *) ~ (a *)
    & (* *) ~ (* a)
  "

  // Parses
  let net = (HVM/do-parse-net f8)

  // Sanity Check
  //log "[NET]"
  //log ((HVM/Net/to-string net) :: String)

  // Boots Net
  ask (HVM/boot net)

  // Normalizes
  ask HVM/eval-strict

  // Results
  ask itrs = HVM/get-itrs
  ask net  = HVM/recover-net
  //ask rnet = HVM/dump-rnet

  // Logs
  log "[ITRS]"
  log (U64/to-string itrs)
  log "[NET]"
  log (HVM/Net/to-string net)
  //log "[RNET]"
  //log (HVM/RNet/to-string rnet)

  // Returns result
  ret #View{"ok"}
})