Skip to content

Instantly share code, notes, and snippets.

@VictorTaelin

VictorTaelin/gemini_debuggingt.txt

Created May 6, 2025 17:02
Show Gist options
  • Save VictorTaelin/54f73328a93c109c22c3722bf331b152 to your computer and use it in GitHub Desktop.
Save VictorTaelin/54f73328a93c109c22c3722bf331b152 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gemini_debuggingt.txt
-- OldCheck:
-- (omitted)
# The Interaction Calculus
The [Interaction Calculus](https://github.com/VictorTaelin/Interaction-Calculus)
is a minimal term rewriting system inspired by the Lambda Calculus (λC), but
with some key differences:
1. Vars are affine: they can only occur up to one time.
2. Vars are global: they can occur anywhere in the program.
3. There is a new core primitive: the superposition.
An Interaction Calculus term is defined by the following grammar:
haskell
Term ::=
| VAR: Name
| ERA: "*"
| LAM: "λ" Name "." Term
| APP: "(" Term " " Term ")"
| SUP: "&" Label "{" Term "," Term "}"
| DUP: "!" "&" Label "{" Name "," Name "}" "=" Term ";" Term
Where:
- VAR represents a variable.
- ERA represents an erasure.
- LAM represents a lambda.
- APP represents a application.
- SUP represents a superposition.
- DUP represents a duplication.
Lambdas are curried, and work like their λC counterpart, except with a relaxed
scope, and with affine usage. Applications eliminate lambdas, like in λC,
through the beta-reduce (APP-LAM) interaction.
Superpositions work like pairs. Duplications eliminate superpositions through
the DUP-SUP interaction, which works exactly like a pair projection.
What makes SUPs and DUPs unique is how they interact with LAMs and APPs. When a
SUP is applied to an argument, it reduces through the APP-SUP interaction, and
when a LAM is projected, it reduces through the DUP-LAM interaction. This gives
a computational behavior for every possible interaction: there are no runtime
errors on the core Interaction Calculus.
The 'Label' is a numeric value that affects some interactions, like DUP-SUP,
causing terms to commute, instead of annihilate. Read Lafont's Interaction
Combinators paper to learn more.
The core interaction rules are listed below:
haskell
(* a)
----- APP-ERA
*
(λx.f a)
-------- APP-LAM
x <- a
f
(&L{a,b} c)
----------------- APP-SUP
! &L{c0,c1} = c;
&L{(a c0),(b c1)}
! &L{r,s} = *;
K
-------------- DUP-ERA
r <- *
s <- *
K
! &L{r,s} = λx.f;
K
----------------- DUP-LAM
r <- λx0.f0
s <- λx1.f1
x <- &L{x0,x1}
! &L{f0,f1} = f;
K
! &L{x,y} = &L{a,b};
K
-------------------- DUP-SUP (if equal labels)
x <- a
y <- b
K
! &L{x,y} = &R{a,b};
K
-------------------- DUP-SUP (if different labels)
x <- &R{a0,b0}
y <- &R{a1,b1}
! &L{a0,a1} = a;
! &L{b0,b1} = b;
K
Where x <- t stands for a global substitution of x by t.
Since variables are affine, substitutions can be implemented efficiently by just
inserting an entry in a global substitution map (sub[var] = value). There is
no need to traverse the target term, or to handle name capture, as long as fresh
variable names are globally unique. Thread-safe substitutions can be performed
with a single atomic-swap.
Below is a pseudocode implementation of these interaction rules:
python
def app_lam(app, lam):
sub[lam.nam] = app.arg
return lam.bod
def app_sup(app, sup):
x0 = fresh()
x1 = fresh()
a0 = App(sup.lft, Var(x0))
a1 = App(sup.rgt, Var(x1))
return Dup(sup.lab, x0, x1, app.arg, Sup(a0, a1))
def dup_lam(dup, lam):
x0 = fresh()
x1 = fresh()
f0 = fresh()
f1 = fresh()
sub[dup.lft] = Lam(x0, Var(f0))
sub[dup.rgt] = Lam(x1, Var(f1))
sub[lam.nam] = Sup(dup.lab, Var(x0), Var(x1))
return Dup(dup.lab, f0, f1, lam.bod, dup.bod)
def dup_sup(dup, sup):
if dup.lab == sup.lab:
sub[dup.lft] = sup.lft
sub[dup.rgt] = sup.rgt
return dup.bod
Terms can be reduced to weak head normal form, which means reducing until the
outermost constructor is a value (LAM, SUP, etc.), or until no more reductions
are possible. Example:
python
def whnf(term):
while True:
match term:
case Var(nam):
if nam in sub:
term = sub[nam]
else:
return term
case App(fun, arg):
fun = whnf(fun)
match fun.tag:
case LAM: term = app_lam(term, fun)
case SUP: term = app_sup(term, fun)
case _ : return App(fun, arg)
case Dup(lft, rgt, val, bod):
val = whnf(val)
match val.tag:
case LAM: term = dup_lam(term, val)
case SUP: term = dup_sup(term, val)
case _ : return Dup(lft, rgt, val, bod)
case _:
return term
Terms can be reduced to full normal form by recursively taking the whnf:
python
def normal(term):
term = whnf(term)
match term:
case Lam(nam, bod):
bod_nf = normal(bod)
return Lam(nam, bod_nf)
case App(fun, arg):
fun_nf = normal(fun)
arg_nf = normal(arg)
return App(fun_nf, arg_nf)
...
case _:
return term
Below are some normalization examples.
Example 0: (simple λ-term)
haskell
(λx.λt.(t x) λy.y)
------------------ APP-LAM
λt.(t λy.y)
Example 1: (larger λ-term)
haskell
(λb.λt.λf.((b f) t) λT.λF.T)
---------------------------- APP-LAM
λt.λf.((λT.λF.T f) t)
----------------------- APP-LAM
λt.λf.(λF.t f)
-------------- APP-LAM
λt.λf.t
Example 2: (global scopes)
haskell
{x,(λx.λy.y λk.k)}
------------------ APP-LAM
{λk.k,λy.y}
Example 3: (superposition)
haskell
!{a,b} = {λx.x,λy.y}; (a b)
--------------------------- DUP-SUP
(λx.x λy.y)
----------- APP-LAM
λy.y
Example 4: (overlap)
haskell
({λx.x,λy.y} λz.z)
------------------ APP-SUP
! {x0,x1} = λz.z; {(λx.x x0),(λy.y x1)}
--------------------------------------- DUP-LAM
! {f0,f1} = {r,s}; {(λx.x λr.f0),(λy.y λs.f1)}
---------------------------------------------- DUP-SUP
{(λx.x λr.r),(λy.y λs.s)}
------------------------- APP-LAM
{λr.r,(λy.y λs.s)}
------------------ APP-LAM
{λr.r,λs.s}
Example 5: (default test term)
The following term can be used to test all interactions:
haskell
((λf.λx.!{f0,f1}=f;(f0 (f1 x)) λB.λT.λF.((B F) T)) λa.λb.a)
----------------------------------------------------------- 16 interactions
λa.λb.a
# Collapsing
An Interaction Calculus term can be collapsed to a superposed tree of pure
Lambda Calculus terms without SUPs and DUPs, by extending the evaluator with the
following collapse interactions:
haskell
λx.*
------ ERA-LAM
x <- *
*
(f *)
----- ERA-APP
*
λx.&L{f0,f1}
----------------- SUP-LAM
x <- &L{x0,x1}
&L{λx0.f0,λx1.f1}
(f &L{x0,x1})
------------------- SUP-APP
!&L{f0,f1} = f;
&L{(f0 x0),(f1 x1)}
&R{&L{x0,x1},y}
----------------------- SUP-SUP-X (if R>L)
!&R{y0,y1} = y;
&L{&R{x0,x1},&R{y0,y1}}
&R{x,&L{y0,y1}}
----------------------- SUP-SUP-Y (if R>L)
!&R{x0,x1} = x;
&L{&R{x0,x1},&R{y0,y1}}
!&L{x0,x1} = x; K
----------------- DUP-VAR
x0 <- x
x1 <- x
K
!&L{a0,a1} = (f x); K
--------------------- DUP-APP
a0 <- (f0 x0)
a1 <- (f1 x1)
!&L{f0,f1} = f;
!&L{x0,x1} = x;
K
module Type where
import Data.Word
import Foreign.Ptr
import Control.Applicative ((<|>))
import Control.Monad (forM)
import Data.Char (chr, ord)
import Data.Char (intToDigit)
import Data.IORef
import Data.List
import Data.Word
import Numeric (showIntAtBase)
import System.IO.Unsafe (unsafePerformIO)
import qualified Data.Map.Strict as MS hiding (map)
-- Core Types
-- ----------
type Tag = Word8
type Lab = Word32
type Loc = Word32
type Term = Word64
type FnID = Word16
type Name = String
type Move = (Name, Core) -- !x = term
data LetT = LAZY | STRI deriving (Eq, Enum)
data MatT = SWI | MAT Word16 | IFL Word16 deriving (Show, Eq)
-- **Note: we're refactoring HVM3's Code Type.**
-- OLD TYPE:
-- data Core
-- = Var Name -- x
-- | Ref Name Word16 [Core] -- @fn
-- | Era -- *
-- | Sup Lab Core Core -- &L{a b}
-- | Dup Lab Name Name Core Core -- ! &L{a b} = v body
-- | Set -- Set
-- | All Core Core -- ∀A.B
-- | Lam Name Core -- λx(F)
-- | App Core Core -- (f x)
-- | Adt Name [Core] -- #Typ{a b ...}
-- | Ctr Name [Core] -- #Ctr{a b ...}
-- | U32 -- U32
-- | W32 Word32 -- 123
-- | Chr Char -- 'a'
-- | Op2 Oper Core Core -- (+ a b)
-- | Let LetT Name Core Core -- ! x = v body
-- | Mat MatT Core [Move] [Case] -- ~ v !moves { cases }
-- deriving (Eq)
-- NEW TYPE:
data Core
= Var Name -- x
| Ref Name FnID [Core] -- @fun(a,b...)
| Let LetT Name Core Core -- !x=v;f
| Era -- *
| Sup Lab Core Core -- &L{a,b}
| Dup Lab Name Name Core Core -- !&L{a,b}=v;f
| Set -- Set
| Emp -- ⊥
| Efq Core [Move] -- ~x!ms{}
| Uni -- ⊤
| Nil -- ()
| Use Core [Move] Core -- ~x!ms{():f}
| U32 -- U32
| W32 Word32 -- 12345
| Swi Core [Move] Core Core -- ~x!ms{0:z;+:s}
| Op2 Oper Core Core -- (+ a b)
| Sig Core Core -- ΣA.B
| Tup Core Core -- (a,b)
| Get Core [Move] Core -- ~x!ms{(,):f}
| All Core Core -- ∀A.B
| Lam Name Core -- λx.F
| App Core Core -- (f x)
| Ann Bool Core Core -- <x:T>
deriving (Eq)
-- The changes include:
-- - Addition of Type-Formers, like Emp, All, Sig, etc.
-- - Addition of empty: Emp/Efq
-- - Addition of unit: Uni/Nil/Use
-- - Addition of pairs: Sig/Tup/Get (behaves like a 0-label Sup/Dup)
-- - Removal of ADT/CTR, in favor of more primitive types
-- - Removal of CHR (which was just another W32)
-- - Removal of the generic MAT, in favor of specific pattern-matches:
-- - - Efq: for the Empty type
-- - - Use: for the Unit type
-- - - Swi: for the U32 type
-- - - Get: for the Sigma type
-- - For simplicity, now, SWI is always ~x{0:z;+:s} (no multi-number switch)
-- - FWD has been removed (it was unused)
-- **Our goal is to update the whole codebase to reflect this change.**
--
-- INSTRUCTIONS:
--
-- When asked to fill below a commented-out code, you must rewrite it completely, updating it to comply to the changes above.
-- Remove discarded cases (like CTR), keep old cases (like Lam/App) verbatin (important: don't change existing definitions!), include new/missing cases (like Tup).
-- Preserve original comments and everything else. Avoid loss of information.
--
-- When asked to implement a missing interaction, reason about it longer, to make sure you get it right.
-- For example, the missing DUP-ALL interaction is:
-- !&L{x0,x1}=∀A.B
-- ----------------- DUP-ALL
-- !&L{A0,A1}=A
-- !&L{B0,B1}=B
-- &L{∀A0.B0,∀A1.B1}
-- Because All doesn't bind a variable.
-- Getting these right demands reasoning.
--
-- NOTES:
--
-- The following terms bind variables:
-- - λx.f: a lambda binds 'x' in its body, 'f'
-- - !x=v;f; a let binds 'x' in its body, 'f'
-- The following terms DO NOT bind variables:
-- - ~x{}
-- - ~x{():f}
-- - ~x{(,):f}
-- - ~x{0:z;+:s}
-- - ΣA.B
-- - ∀A.B
-- Instead, we use lambdas *inside* them. For example:
-- @id = λx.~x{0:0;+:λp.(+ 1 @id(p))}
-- @fst = λx.~x{(,):λa.λb.a}
-- Below is the complete list of new elims/intros/types:
-- Eliminators:
-- - APP
-- - USE
-- - GET
-- - SWI
-- - DUP
-- - OPX
-- - OPY
-- Introducers:
-- - ERA
-- - SUP
-- - NIL
-- - W32
-- - TUP
-- - LAM
-- Type-Formers:
-- - SET
-- - EMP
-- - UNI
-- - U32
-- - SIG
-- - ALL
-- STYLE GUIDE:
-- - Always order cases in the SAME order as they were defined on the Core type.
-- - As much as possible, favor SINGLE-LETTER field names, or TWO-LETTER field names (on list-like fields), inspired by the letters used in the comments on the Core type.
-- - For example, instead of format (Use moves body) = ..., write format (Use ms b) = ...
-- - Since Haskell doesn't accept uppercase variable names, prepend an underscore. Example: format (All _A _B) = ....
-- - Do NOT use the ' (apostrophe) character in variable names. Prefer underscores. Example: a_ instead of a'
-- - In general, attempt to mimic the original coding style as close as possible.
-- - KEEP COMMENTS, ERROR HANDLERS, ETC. FROM THE ORIGINAL CODE - DON'T LOSE INFORMATION
data Oper
= OP_ADD | OP_SUB | OP_MUL | OP_DIV
| OP_MOD | OP_EQ | OP_NE | OP_LT
| OP_GT | OP_LTE | OP_GTE | OP_AND
| OP_OR | OP_XOR | OP_LSH | OP_RSH
deriving (Eq, Enum)
-- A top-level function, including:
-- - copy: true when ref-copy mode is enabled
-- - args: a list of (isArgStrict, argName) pairs
-- - core: the function's body
-- Note: ref-copy improves C speed, but increases interaction count
type Func = ((Bool, [(Bool,String)]), Core)
-- Set of labels in a function's body
type HasLab = (MS.Map Lab ())
-- data Book = Book
-- { fidToFun :: MS.Map Word16 Func -- func id to Func object
-- , fidToLab :: MS.Map Word16 HasLab -- func id to dup labels used
-- , fidToNam :: MS.Map Word16 Name -- func id to name
-- , namToFid :: MS.Map Name Word16 -- func name to id
-- , cidToAri :: MS.Map Word16 Word16 -- ctor id to field count (arity)
-- , cidToLen :: MS.Map Word16 Word16 -- ctor id to cases length (ADT ctors)
-- , cidToCtr :: MS.Map Word16 Name -- ctor id to name
-- , ctrToCid :: MS.Map Name Word16 -- ctor name to id
-- , cidToADT :: MS.Map Word16 Word16 -- ctor id to ADT id (first ADT cid)
-- , freshLab :: Lab -- auto dup label counter
-- } deriving (Show, Eq)
data Book = Book
{ fidToFun :: MS.Map FnID Func -- func id to Func object
, fidToLab :: MS.Map FnID HasLab -- func id to dup labels used
, fidToNam :: MS.Map FnID Name -- func id to name
, namToFid :: MS.Map Name FnID -- func name to id
, freshLab :: Lab -- auto dup label counter
} deriving (Show, Eq)
-- Runtime Types
-- -------------
type HVM = IO
-- Constants
-- ---------
-- -- Tags
-- _DP0_ = 0x00 :: Tag
-- _DP1_ = 0x01 :: Tag
-- _VAR_ = 0x02 :: Tag
-- _FWD_ = 0x03 :: Tag
-- _REF_ = 0x04 :: Tag
-- _LET_ = 0x05 :: Tag
-- _APP_ = 0x06 :: Tag
-- _MAT_ = 0x08 :: Tag
-- _IFL_ = 0x09 :: Tag
-- _SWI_ = 0x0A :: Tag
-- _OPX_ = 0x0B :: Tag
-- _OPY_ = 0x0C :: Tag
-- _ERA_ = 0x0D :: Tag
-- _LAM_ = 0x0E :: Tag
-- _SUP_ = 0x0F :: Tag
-- _CTR_ = 0x10 :: Tag
-- _W32_ = 0x11 :: Tag
-- _CHR_ = 0x12 :: Tag
-- Tags
_DP0_ = 0x00 :: Tag
_DP1_ = 0x01 :: Tag
_VAR_ = 0x02 :: Tag
_REF_ = 0x03 :: Tag
_LET_ = 0x04 :: Tag
_ERA_ = 0x05 :: Tag
_SUP_ = 0x06 :: Tag
_DUP_ = 0x07 :: Tag
_SET_ = 0x08 :: Tag
_EMP_ = 0x09 :: Tag
_EFQ_ = 0x0A :: Tag
_UNI_ = 0x0B :: Tag
_NIL_ = 0x0C :: Tag
_USE_ = 0x0D :: Tag
_U32_ = 0x0E :: Tag
_W32_ = 0x0F :: Tag
_SWI_ = 0x10 :: Tag
_OPX_ = 0x11 :: Tag
_OPY_ = 0x12 :: Tag
_SIG_ = 0x13 :: Tag
_TUP_ = 0x14 :: Tag
_GET_ = 0x15 :: Tag
_ALL_ = 0x16 :: Tag
_LAM_ = 0x17 :: Tag
_APP_ = 0x18 :: Tag
_ANN_ = 0x19 :: Tag
-- Let Types
modeT :: Lab -> LetT
modeT 0x00 = LAZY
modeT 0x01 = STRI
modeT mode = error $ "unknown mode: " ++ show mode
-- Primitive Functions
_DUP_F_ = 0xFFFF :: Lab
_SUP_F_ = 0xFFFE :: Lab
_LOG_F_ = 0xFFFD :: Lab
primitives :: [(String, Word16)]
primitives =
[ ("SUP", fromIntegral _SUP_F_)
, ("DUP", fromIntegral _DUP_F_)
, ("LOG", fromIntegral _LOG_F_)
]
-- Utils
-- -----
-- Getter function for maps
mget :: (Ord k, Show k) => MS.Map k a -> k -> a
mget map key =
case MS.lookup key map of
Just val -> val
Nothing -> error $ "key not found: " ++ show key
funArity :: Book -> Word16 -> Word16
funArity book fid
| fid == fromIntegral _SUP_F_ = 3
| fid == fromIntegral _DUP_F_ = 3
| fid == fromIntegral _LOG_F_ = 1
| otherwise = case MS.lookup fid (fidToFun book) of
Just ((_, args), _) ->
fromIntegral (length args)
Nothing ->
error $ "Function ID not found: " ++ show fid
-- Stringification
-- ---------------
padLeft :: String -> Int -> Char -> String
padLeft str n c = replicate (n - length str) c ++ str
showHex :: Word64 -> String
showHex x = showIntAtBase 16 intToDigit (fromIntegral x) ""
showName :: Int -> String
showName n = go (n + 1) "" where
go n ac | n == 0 = ac
| otherwise = go q (chr (ord 'a' + r) : ac)
where (q,r) = quotRem (n - 1) 26
-- showTag :: Tag -> String
-- showTag tag
-- | tag == _DP0_ = "DP0"
-- | tag == _DP1_ = "DP1"
-- | tag == _VAR_ = "VAR"
-- | tag == _FWD_ = "FWD"
-- | tag == _REF_ = "REF"
-- | tag == _LET_ = "LET"
-- | tag == _APP_ = "APP"
-- | tag == _MAT_ = "MAT"
-- | tag == _IFL_ = "IFL"
-- | tag == _SWI_ = "SWI"
-- | tag == _OPX_ = "OPX"
-- | tag == _OPY_ = "OPY"
-- | tag == _ERA_ = "ERA"
-- | tag == _LAM_ = "LAM"
-- | tag == _SUP_ = "SUP"
-- | tag == _CTR_ = "CTR"
-- | tag == _W32_ = "W32"
-- | tag == _CHR_ = "CHR"
-- | otherwise = error $ "unknown tag: " ++ show tag
showTag :: Tag -> String
showTag tag
| tag == _DP0_ = "DP0"
| tag == _DP1_ = "DP1"
| tag == _VAR_ = "VAR"
| tag == _REF_ = "REF"
| tag == _LET_ = "LET"
| tag == _ERA_ = "ERA"
| tag == _SUP_ = "SUP"
| tag == _DUP_ = "DUP"
| tag == _SET_ = "SET"
| tag == _EMP_ = "EMP"
| tag == _EFQ_ = "EFQ"
| tag == _UNI_ = "UNI"
| tag == _NIL_ = "NIL"
| tag == _USE_ = "USE"
| tag == _U32_ = "U32"
| tag == _W32_ = "W32"
| tag == _SWI_ = "SWI"
| tag == _OPX_ = "OPX"
| tag == _OPY_ = "OPY"
| tag == _SIG_ = "SIG"
| tag == _TUP_ = "TUP"
| tag == _GET_ = "GET"
| tag == _ALL_ = "ALL"
| tag == _LAM_ = "LAM"
| tag == _APP_ = "APP"
| tag == _ANN_ = "ANN"
| otherwise = error $ "unknown tag: " ++ show tag
showLab :: Lab -> String
showLab lab = padLeft (showHex (fromIntegral lab)) 6 '0'
showLoc :: Loc -> String
showLoc loc = padLeft (showHex (fromIntegral loc)) 8 '0'
instance Show Oper where
show OP_ADD = "+"
show OP_SUB = "-"
show OP_MUL = "*"
show OP_DIV = "/"
show OP_MOD = "%"
show OP_EQ = "=="
show OP_NE = "!="
show OP_LT = "<"
show OP_GT = ">"
show OP_LTE = "<="
show OP_GTE = ">="
show OP_AND = "&"
show OP_OR = "|"
show OP_XOR = "^"
show OP_LSH = "<<"
show OP_RSH = ">>"
instance Show LetT where
show LAZY = ""
show STRI = "."
showCore :: Core -> String
showCore = format
where
format :: Core -> String
format (Var k) = k
format (Ref k i xs) =
let xs' = intercalate " " (map showCore xs) in
concat ["@", k, "(", xs', ")"]
format (Let m k v f) =
let v' = showCore v in
let f' = showCore f in
if k == "" then
concat [v', "\n", f']
else
concat ["! ", show m, k, " = ", v', "\n", f']
format Era = "*"
format (Sup l a b) =
let a' = showCore a in
let b' = showCore b in
concat ["&", show l, "{", a', ",", b', "}"]
format (Dup l x y v f) =
let v' = showCore v in
let f' = showCore f in
concat ["! &", show l, "{", x, ",", y, "} = ", v', "\n", f']
format Set = "Set"
format Emp = "⊥"
format (Efq c ms) =
let c' = showCore c in
let ms' = concatMap (\(k,v) -> concat [" !", k, "=", showCore v]) ms in
concat ["~", c', ms', "{}"]
format Uni = "⊤"
format Nil = "()"
format (Use c ms b) =
let c' = showCore c in
let ms' = concatMap (\(k,v) -> concat [" !", k, "=", showCore v]) ms in
let b' = showCore b in
concat ["~", c', ms', "{():", b', "}"]
format U32 = "U32"
format (W32 v) = show v
format (Swi c ms z s) =
let c' = showCore c in
let ms' = concatMap (\(k,v) -> concat [" !", k, "=", showCore v]) ms in
let z' = showCore z in
let s' = showCore s in
concat ["~", c', ms', "{0:", z', ";+:", s', "}"]
format (Op2 o a b) =
let a' = showCore a in
let b' = showCore b in
concat ["(", show o, " ", a', " ", b', ")"]
format (Sig _A _B) =
let a' = showCore _A in
let b' = showCore _B in
concat ["Σ", a', ".", b']
format (Tup a b) =
let a' = showCore a in
let b' = showCore b in
concat ["(", a', ",", b', ")"]
format (Get c ms b) =
let c' = showCore c in
let ms' = concatMap (\(k,v) -> concat [" !", k, "=", showCore v]) ms in
let b' = showCore b in
concat ["~", c', ms', "{(,):", b', "}"]
format (All _A _B) =
let a' = showCore _A in
let b' = showCore _B in
concat ["∀", a', ".", b']
format (Lam x f) =
let f' = showCore f in
concat ["λ", x, ".", f']
format (App f x) =
let f' = showCore f in
let x' = showCore x in
concat ["(", f', " ", x', ")"]
format (Ann c x t) =
let x' = showCore x in
let t' = showCore t in
concat ["<", x', " : ", t', ">"]
renamer :: IORef (MS.Map String String) -> Core -> IO Core
renamer names core = case core of
Var k -> do
k' <- genName names k
return $ Var k'
Ref k i xs -> do
xs' <- mapM (renamer names) xs
return $ Ref k i xs'
Let m k v f -> do
k' <- genName names k
v' <- renamer names v
f' <- renamer names f
return $ Let m k' v' f'
Era ->
return Era
Sup l a b -> do
a' <- renamer names a
b' <- renamer names b
return $ Sup l a' b'
Dup l x y v f -> do
x' <- genName names x
y' <- genName names y
v' <- renamer names v
f' <- renamer names f
return $ Dup l x' y' v' f'
Set ->
return Set
Emp ->
return Emp
Efq c ms -> do
c' <- renamer names c
ms' <- forM ms $ \(k,v) -> do v' <- renamer names v; return (k,v')
return $ Efq c' ms'
Uni ->
return Uni
Nil ->
return Nil
Use c ms b -> do
c' <- renamer names c
ms' <- forM ms $ \(k,v) -> do v' <- renamer names v; return (k,v')
b' <- renamer names b
return $ Use c' ms' b'
U32 ->
return U32
W32 v ->
return $ W32 v
Swi c ms z s -> do
c' <- renamer names c
ms' <- forM ms $ \(k,v) -> do v' <- renamer names v; return (k,v')
z' <- renamer names z
s' <- renamer names s
return $ Swi c' ms' z' s'
Op2 o a b -> do
a' <- renamer names a
b' <- renamer names b
return $ Op2 o a' b'
Sig _A _B -> do
_A' <- renamer names _A
_B' <- renamer names _B
return $ Sig _A' _B'
Tup a b -> do
a' <- renamer names a
b' <- renamer names b
return $ Tup a' b'
Get c ms b -> do
c' <- renamer names c
ms' <- forM ms $ \(k,v) -> do v' <- renamer names v; return (k,v')
b' <- renamer names b
return $ Get c' ms' b'
All _A _B -> do
_A' <- renamer names _A
_B' <- renamer names _B
return $ All _A' _B'
Lam x f -> do
x' <- genName names x
f' <- renamer names f
return $ Lam x' f'
App f x -> do
f' <- renamer names f
x' <- renamer names x
return $ App f' x'
Ann c x t -> do
x' <- renamer names x
t' <- renamer names t
return $ Ann c x' t'
rename :: Core -> Core
rename core = unsafePerformIO $ do
names <- newIORef MS.empty
renamer names core
genName :: IORef (MS.Map String String) -> String -> IO String
genName names name =
atomicModifyIORef' names $ \map ->
case MS.lookup name map of
Just val -> (map, val)
Nothing ->
let new = showName (MS.size map)
map' = MS.insert name new map
in (map', new)
instance Show Core where
show = showCore . rename
-- COMPLETE INTERACTION TABLE (updated)
-- @foo(a,b...)
-- ----------------- REF
-- book[foo](a,b...)
-- Let:
-- ! x = v ; f
-- ----------- LET
-- x <- v
-- f
-- (* a)
-- ----- APP-ERA
-- *
-- (λx.f a)
-- -------- APP-LAM
-- x <- a
-- f
-- (&L{f0,f1} a)
-- ------------------- APP-SUP
-- ! &L{a0,a1} = a;
-- &L{(f0 x0),(f1 x1)}
-- (() a)
-- ------ APP-NIL
-- error
-- ((f0,f1) a)
-- ----------- APP-TUP
-- error
-- (123 a)
-- ------- APP-W32
-- error
-- (T a)
-- ----- APP-TYP
-- error
-- ~*{():f}
-- -------- USE-ERA
-- *
-- ~&L{a,b}{():f}
-- ----------------------- USE-SUP
-- ! &L{f0,f1} = f;
-- &L{~a{():f0},~b{():f1}}
-- ~λx.g{():f}
-- ----------- USE-LAM
-- error
-- ~(){():f}
-- --------- USE-NIL
-- f
-- ~(p,q){():f}
-- ------------ USE-TUP
-- error
-- ~123{():f}
-- ---------- USE-W32
-- error
-- ~T{():f}
-- -------- USE-TYP
-- error
-- ~*{(,):f}
-- --------- GET-ERA
-- *
-- ~&L{a,b}{(,): f}
-- ------------------------- GET-SUP
-- ! &L{f0,f1} = f;
-- &L{~a{(,):f0},~b{(,):f1}}
-- ~(){(,):f}
-- ---------- GET-NIL
-- error
-- ~(a,b){(,):f}
-- ------------- GET-TUP
-- (f a b)
-- ~λx.g{(,):f}
-- ------------ GET-LAM
-- error
-- ~123{(,):f}
-- ----------- GET-W32
-- error
-- ~TYP{(,):f}
-- ----------- GET-TYP
-- error
-- ~*{0:z;+:s}
-- ----------- SWI-ERA
-- *
-- ~&L{a,b}{0:z;+:s}
-- ------------------------------- SWI-SUP
-- ! &L{z0,z1} = z;
-- ! &L{s0,s1} = s;
-- &L{~a{0:z0;+:s0},~b{0:z1;+:s1}}
-- ~(){0:z;+:s}
-- ------------ SWI-NIL
-- error
-- ~(a,b){0:z;+:s}
-- --------------- SWI-TUP
-- error
-- ~λx.g{0:z;+:s}
-- -------------- SWI-LAM
-- error
-- ~n{0:z;+:s}
-- ----------- SWI-W32
-- if n = 0:
-- z
-- else:
-- (s (n-1))
-- ~T{0:z;+:s}
-- ----------- SWI-TYP
-- error
-- ! &L{r,s} = *
-- ------------- DUP-ERA
-- r <- *
-- s <- *
-- ! &L{x,y} = &L{a,b}
-- ------------------- DUP-SUP
-- x <- a
-- y <- b
-- ! &L{r,s} = λx.f
-- ---------------- DUP-LAM
-- r <- λx0.f0
-- s <- λx1.f1
-- x <- &L{x0,x1}
-- ! &L{f0,f1} = f
-- ! &L{x,y} = ()
-- -------------- DUP-NIL
-- x <- ()
-- y <- ()
-- ! &L{x,y} = (a,b)
-- ----------------- DUP-TUP
-- ! &L{a0,a1} = a
-- ! &L{b0,b1} = b
-- x <- &L{a0,b0}
-- y <- &L{a1,b1}
-- ! &L{x,y} = 123
-- --------------- DUP-W32
-- x <- 123
-- y <- 123
-- ! &L{x,y} = Set
-- --------------- DUP-SET
-- x <- Set
-- y <- Set
-- ! &L{x,y} = ⊥
-- ------------- DUP-EMP
-- x <- ⊥
-- y <- ⊥
-- ! &L{x,y} = ⊤
-- ------------- DUP-UNI
-- x <- ⊤
-- y <- ⊤
-- ! &L{x,y} = U32
-- -------------- DUP-U32
-- x <- U32
-- y <- U32
-- ! &L{x,y} = ΣA.B
-- ----------------- DUP-SIG
-- ! &L{A0,A1} = A
-- ! &L{B0,B1} = B
-- x <- ΣA0.B0
-- y <- ΣA1.B1
-- ! &L{x,y} = ∀A.B
-- ----------------- DUP-ALL
-- ! &L{A0,A1} = A
-- ! &L{B0,B1} = B
-- x <- ∀A0.B0
-- y <- ∀A1.B1
-- (<op * y)
-- --------- OPX-ERA
-- *
-- (<op λx.f y)
-- ----------- OPX-LAM
-- error
-- (<op &L{a,b} y)
-- ------------------------- OPX-SUP
-- ! &L{y0,y1} = y;
-- &L{(<op a y0),(<op b y1)}
-- (<op () y)
-- ---------- OPX-NIL
-- error
-- (<op (x0,x1) y)
-- --------------- OPX-TUP
-- error
-- (<op x y)
-- --------- OPX-W32
-- (>op y x)
-- (<op T y)
-- --------- OPX-TYP
-- error
-- (>op x *)
-- --------- OPY-ERA
-- *
-- (>op x λy.f)
-- ------------ OPY-LAM
-- error
-- (>op x &L{y0,y1})
-- ----------------------- OPY-SUP
-- &L{>op(x y0),>op(x y1)}
-- (>op x ())
-- ---------- OPY-NIL
-- error
-- (>op x (y0,y1))
-- --------------- OPY-TUP
-- error
-- (>op x y)
-- --------- OPY-W32
-- x <op> y
-- (>op x T)
-- --------- OPY-TYP
-- error
-- ! &L{x,y} = @foo(a,b...)
-- ------------------------ DUP-REF-COPY (when &L not in @foo)
-- ! &L{a0,a1} = a
-- ! &L{b0,b1} = b
-- ...
-- x <- @foo(a0,b0...)
-- y <- @foo(a1,b1...)
-- @foo(&L{ax,ay},b,c...)
-- ---------------------- REF-SUP-COPY (when @L not in @foo)
-- ! &L{bx,by} = b
-- ! &L{cx,by} = c
-- ...
-- &L{@foo(ax,bx,cx...),@foo(ay,by,cy,...)}
//./../IC.md//
//./Type.hs//
//#include <inttypes.h>
//#include <stdint.h>
//#include <stdio.h>
//#include <stdlib.h>
//#include <sys/mman.h>
//#include <unistd.h>
//#include <time.h>
//#include <stdbool.h>
//#define MAX_HEAP_SIZE (1ULL << 32)
//#define MAX_STACK_SIZE (1ULL << 28)
//typedef uint8_t Tag;
//typedef uint32_t Lab;
//typedef uint32_t Loc;
//typedef uint64_t Term;
//typedef uint16_t u16;
//typedef uint32_t u32;
//typedef uint64_t u64;
//// Runtime Types
//// -------------
//typedef struct {
//Term* sbuf; // reduction stack buffer
//u64* spos; // reduction stack position
//Term* heap; // global node buffer
//u64* size; // global node buffer position
//u64* itrs; // interaction count
//u64* frsh; // fresh dup label count
//Term (*book[65536])(Term); // functions
//u16 cari[65536]; // arity of each constructor
//u16 clen[65536]; // case length of each constructor
//u16 cadt[65536]; // ADT id of each constructor
//u16 fari[65536]; // arity of each function
//} State;
//static State HVM = {
//.sbuf = NULL,
//.spos = NULL,
//.heap = NULL,
//.size = NULL,
//.itrs = NULL,
//.frsh = NULL,
//.book = {NULL},
//.cari = {0},
//.clen = {0},
//.cadt = {0},
//.fari = {0},
//};
//// Constants
//// ---------
//#define DP0 0x00
//#define DP1 0x01
//#define VAR 0x02
//#define SUB 0x03
//#define REF 0x04
//#define LET 0x05
//#define APP 0x06
//#define MAT 0x08
//#define IFL 0x09
//#define SWI 0x0A
//#define OPX 0x0B
//#define OPY 0x0C
//#define ERA 0x0D
//#define LAM 0x0E
//#define SUP 0x0F
//#define CTR 0x10
//#define W32 0x11
//#define CHR 0x12
//#define OP_ADD 0x00
//#define OP_SUB 0x01
//#define OP_MUL 0x02
//#define OP_DIV 0x03
//#define OP_MOD 0x04
//#define OP_EQ 0x05
//#define OP_NE 0x06
//#define OP_LT 0x07
//#define OP_GT 0x08
//#define OP_LTE 0x09
//#define OP_GTE 0x0A
//#define OP_AND 0x0B
//#define OP_OR 0x0C
//#define OP_XOR 0x0D
//#define OP_LSH 0x0E
//#define OP_RSH 0x0F
//#define DUP_F 0xFFFF
//#define SUP_F 0xFFFE
//#define LOG_F 0xFFFD
//#define LAZY 0x0
//#define STRI 0x1
//#define VOID 0x00000000000000
//// Heap
//// ----
//void set_len(u64 size) {
//*HVM.size = size;
//}
//void set_itr(u64 itrs) {
//*HVM.itrs = itrs;
//}
//u64 get_len() {
//return *HVM.size;
//}
//u64 get_itr() {
//return *HVM.itrs;
//}
//u64 fresh() {
//return (*HVM.frsh)++;
//}
//// Terms
//// ------
//Term term_new(Tag tag, Lab lab, Loc loc) {
//Term tag_enc = tag;
//Term lab_enc = ((Term)lab) << 8;
//Term loc_enc = ((Term)loc) << 32;
//return tag_enc | lab_enc | loc_enc;
//}
//Tag term_tag(Term x) {
//return x & 0x7F;
//}
//Lab term_lab(Term x) {
//return (x >> 8) & 0xFFFFFF;
//}
//Loc term_loc(Term x) {
//return (x >> 32) & 0xFFFFFFFF;
//}
//u64 term_get_bit(Term x) {
//return (x >> 7) & 1;
//}
//Term term_set_bit(Term term) {
//return term | (1ULL << 7);
//}
//Term term_rem_bit(Term term) {
//return term & ~(1ULL << 7);
//}
//Term term_set_loc(Term x, Loc loc) {
//return (x & 0x00000000FFFFFFFF) | (((Term)loc) << 32);
//}
//_Bool term_is_atom(Term term) {
//switch (term_tag(term)) {
//case ERA:
//case W32:
//case CHR: return 1;
//default: return 0;
//}
//}
//// Atomics
//// -------
//Term swap(Loc loc, Term term) {
//Term val = HVM.heap[loc];
//HVM.heap[loc] = term;
//if (val == 0) {
//printf("SWAP 0 at %08llx\n", (u64)loc);
//exit(0);
//}
//return val;
//}
//Term got(Loc loc) {
//Term val = HVM.heap[loc];
//if (val == 0) {
//printf("GOT 0 at %08llx\n", (u64)loc);
//exit(0);
//}
//return val;
//}
//void set(Loc loc, Term term) {
//HVM.heap[loc] = term;
//}
//void sub(Loc loc, Term term) {
//set(loc, term_set_bit(term));
//}
//Term take(Loc loc) {
//return swap(loc, VOID);
//}
//// Allocation
//// ----------
//Loc alloc_node(Loc arity) {
//if (*HVM.size + arity > MAX_HEAP_SIZE) {
//printf("Heap memory limit exceeded\n");
//exit(1);
//}
//u64 old = *HVM.size;
//*HVM.size += arity;
//return old;
//}
//void inc_itr() {
//(*HVM.itrs)++;
//}
//// Stack
//// ----
//void spush(Term term, Term* sbuf, u64* spos) {
//if (*spos >= MAX_STACK_SIZE) {
//printf("Stack memory limit exceeded\n");
//exit(1);
//}
//sbuf[(*spos)++] = term;
//}
//Term spop(Term* sbuf, u64* spos) {
//return sbuf[--(*spos)];
//}
//// Stringification
//// ---------------
//void print_tag(Tag tag) {
//switch (tag) {
//case VAR: printf("VAR"); break;
//case DP0: printf("DP0"); break;
//case DP1: printf("DP1"); break;
//case APP: printf("APP"); break;
//case LAM: printf("LAM"); break;
//case ERA: printf("ERA"); break;
//case SUP: printf("SUP"); break;
//case REF: printf("REF"); break;
//case LET: printf("LET"); break;
//case CTR: printf("CTR"); break;
//case MAT: printf("MAT"); break;
//case IFL: printf("IFL"); break;
//case SWI: printf("SWI"); break;
//case W32: printf("W32"); break;
//case CHR: printf("CHR"); break;
//case OPX: printf("OPX"); break;
//case OPY: printf("OPY"); break;
//default : printf("???"); break;
//}
//}
//void print_term(Term term) {
//printf("term_new(");
//print_tag(term_tag(term));
//printf(",0x%06llx,0x%08llx)", (u64)term_lab(term), (u64)term_loc(term));
//}
//void print_heap() {
//for (Loc i = 0; i < *HVM.size; i++) {
//Term term = got(i);
//if (term != 0) {
//printf("set(0x%08llx, ", (u64)i);
//print_term(term);
//printf(");\n");
//}
//}
//}
//// Evaluation
//// ----------
//// @foo(&L{ax ay} b c ...)
//// ----------------------- REF-SUP-COPY (when @L not in @foo)
//// ! &L{bx by} = b
//// ! &L{cx cy} = b
//// ...
//// &L{@foo(ax bx cx ...) @foo(ay by cy ...)}
//Term reduce_ref_sup(Term ref, u16 idx) {
//inc_itr();
//Loc ref_loc = term_loc(ref);
//Lab ref_lab = term_lab(ref);
//u16 fun_id = ref_lab;
//u16 arity = HVM.fari[fun_id];
//if (idx >= arity) {
//printf("ERROR: Invalid index in reduce_ref_sup\n");
//exit(1);
//}
//Term sup = got(ref_loc + idx);
//if (term_tag(sup) != SUP) {
//printf("ERROR: Expected SUP at index %u\n", idx);
//exit(1);
//}
//Lab sup_lab = term_lab(sup);
//Loc sup_loc = term_loc(sup);
//Term sup0 = got(sup_loc + 0);
//Term sup1 = got(sup_loc + 1);
//// Allocate space for new REF node arguments for the second branch
//Loc ref1_loc = alloc_node(arity);
//for (u64 i = 0; i < arity; ++i) {
//if (i != idx) {
//// Duplicate argument
//Term arg = got(ref_loc + i);
//Loc dup_loc = alloc_node(1);
//set(dup_loc + 0, arg);
//set(ref_loc + i, term_new(DP0, sup_lab, dup_loc));
//set(ref1_loc + i, term_new(DP1, sup_lab, dup_loc));
//} else {
//// Set the SUP components directly
//set(ref_loc + i, sup0);
//set(ref1_loc + i, sup1);
//}
//}
//// Create new REF nodes
//Term ref0 = term_new(REF, ref_lab, ref_loc);
//Term ref1 = term_new(REF, ref_lab, ref1_loc);
//// Reuse sup_loc to create the new SUP node
//set(sup_loc + 0, ref0);
//set(sup_loc + 1, ref1);
//return term_new(SUP, sup_lab, sup_loc);
//}
//// @foo(a b c ...)
//// -------------------- REF
//// book[foo](a b c ...)
//Term reduce_ref(Term ref) {
////printf("reduce_ref "); print_term(ref); printf("\n");
////printf("call %d %p\n", term_loc(ref), HVM.book[term_loc(ref)]);
//inc_itr();
//return HVM.book[term_lab(ref)](ref);
//}
//// ! x = val
//// bod
//// --------- LET
//// x <- val
//// bod
//Term reduce_let(Term let, Term val) {
////printf("reduce_let "); print_term(let); printf("\n");
//inc_itr();
//Loc let_loc = term_loc(let);
//Term bod = got(let_loc + 1);
//sub(let_loc + 0, val);
//return bod;
//}
//// (* a)
//// ------- APP-ERA
//// *
//Term reduce_app_era(Term app, Term era) {
////printf("reduce_app_era "); print_term(app); printf("\n");
//inc_itr();
//return era;
//}
//// (λx(body) arg)
//// ---------------- APP-LAM
//// x <- arg
//// body
//Term reduce_app_lam(Term app, Term lam) {
//inc_itr();
//Loc app_loc = term_loc(app);
//Loc lam_loc = term_loc(lam);
//Term bod = got(lam_loc + 0);
//Term arg = got(app_loc + 1);
//sub(lam_loc + 0, arg);
//return bod;
//}
//// (&L{a b} c)
//// --------------------- APP-SUP
//// ! &L{x0 x1} = c
//// &L{(a x0) (b x1)}
//Term reduce_app_sup(Term app, Term sup) {
////printf("reduce_app_sup "); print_term(app); printf("\n");
//inc_itr();
//Loc app_loc = term_loc(app);
//Loc sup_loc = term_loc(sup);
//Lab sup_lab = term_lab(sup);
//Term arg = got(app_loc + 1);
////Term tm0 = got(sup_loc + 0);
//Term tm1 = got(sup_loc + 1);
//Loc loc = alloc_node(3);
//Loc ap0 = sup_loc;
//Loc ap1 = loc + 0;
//Loc su0 = app_loc;
//Loc dup = loc + 2;
////set(ap0 + 0, tm0)
//set(ap0 + 1, term_new(DP0, sup_lab, dup));
//set(ap1 + 0, tm1);
//set(ap1 + 1, term_new(DP1, sup_lab, dup));
//// Reuse app_loc for the result superposition
//set(su0 + 0, term_new(APP, 0, ap0));
//set(su0 + 1, term_new(APP, 0, ap1));
//set(dup + 0, arg);
//return term_new(SUP, sup_lab, su0);
//// return term_set_loc(sup, su0);
//}
//// &L(#{x y z ...} a)
//// ------------------ APP-CTR
//// ⊥
//Term reduce_app_ctr(Term app, Term ctr) {
////printf("reduce_app_ctr "); print_term(app); printf("\n");
//printf("invalid:app-ctr");
//exit(0);
//}
//// &L(123 a)
//// --------- APP-W32
//// ⊥
//Term reduce_app_u32(Term app, Term u32) {
////printf("reduce_app_u32 "); print_term(app); printf("\n");
//printf("invalid:app-u32");
//exit(0);
//}
//// ! &L{x y} = *
//// ------------- DUP-ERA
//// x <- *
//// y <- *
//Term reduce_dup_era(Term dup, Term era) {
////printf("reduce_dup_era "); print_term(dup); printf("\n");
//inc_itr();
//Loc dup_loc = term_loc(dup);
//sub(dup_loc + 0, era);
//return era;
//}
//// ! &L{r s} = λx(f)
//// ------------------- DUP-LAM
//// ! &L{f0 f1} = f
//// r <- λx0(f0)
//// s <- λx1(f1)
//// x <- &L{x0 x1}
//Term reduce_dup_lam(Term dup, Term lam) {
////printf("reduce_dup_lam "); print_term(dup); printf("\n");
//inc_itr();
//Loc dup_loc = term_loc(dup);
//Loc lam_loc = term_loc(lam);
//Lab dup_lab = term_lab(dup);
//Term bod = got(lam_loc + 0);
//Loc loc = alloc_node(5);
//Loc lm0 = loc + 0;
//Loc lm1 = loc + 1;
//Loc su0 = loc + 2;
//Loc du0 = loc + 4;
//sub(lam_loc + 0, term_new(SUP, dup_lab, su0));
//set(lm0 + 0, term_new(DP0, dup_lab, du0));
//set(lm1 + 0, term_new(DP1, dup_lab, du0));
//set(su0 + 0, term_new(VAR, 0, lm0));
//set(su0 + 1, term_new(VAR, 0, lm1));
//set(du0 + 0, bod);
//if (term_tag(dup) == DP0) {
//sub(dup_loc + 0, term_new(LAM, 0, lm1));
//return term_new(LAM, 0, lm0);
//} else {
//sub(dup_loc + 0, term_new(LAM, 0, lm0));
//return term_new(LAM, 0, lm1);
//}
//}
//// ! &L{x y} = &R{a b}
//// ------------------- DUP-SUP
//// if L == R:
//// x <- a
//// y <- b
//// else:
//// x <- &R{a0 b0}
//// y <- &R{a1 b1}
//// ! &L{a0 a1} = a
//// ! &L{b0 b1} = b
//Term reduce_dup_sup(Term dup, Term sup) {
////printf("reduce_dup_sup %u %u | %llu ", term_lab(dup), term_lab(sup), *HVM.spos); print_term(dup); printf(" "); print_term(sup); printf("\n");
//inc_itr();
//Loc dup_loc = term_loc(dup);
//Lab dup_lab = term_lab(dup);
//Lab sup_lab = term_lab(sup);
//Loc sup_loc = term_loc(sup);
//if (dup_lab == sup_lab) {
//Term tm0 = got(sup_loc + 0);
//Term tm1 = got(sup_loc + 1);
//if (term_tag(dup) == DP0) {
//sub(dup_loc + 0, tm1);
//return tm0;
//} else {
//sub(dup_loc + 0, tm0);
//return tm1;
//}
//} else {
//Loc loc = alloc_node(4);
//Loc du0 = sup_loc + 0;
//Loc du1 = sup_loc + 1;
//Loc su0 = loc + 0;
//Loc su1 = loc + 2;
////Term tm0 = got(sup_loc + 0);
////Term tm1 = got(sup_loc + 1);
////set(du0 + 0, tm0);
////set(du1 + 0, tm1);
//set(su0 + 0, term_new(DP0, dup_lab, du0));
//set(su0 + 1, term_new(DP0, dup_lab, du1));
//set(su1 + 0, term_new(DP1, dup_lab, du0));
//set(su1 + 1, term_new(DP1, dup_lab, du1));
//if (term_tag(dup) == DP0) {
//sub(dup_loc + 0, term_new(SUP, sup_lab, su1));
//return term_new(SUP, sup_lab, su0);
//} else {
//sub(dup_loc + 0, term_new(SUP, sup_lab, su0));
//return term_new(SUP, sup_lab, su1);
//}
//}
//}
//// ! &L{x y} = #{a b c ...}
//// ------------------------ DUP-CTR
//// ! &L{a0 a1} = a
//// ! &L{b0 b1} = b
//// ! &L{c0 c1} = c
//// ...
//// x <- #{a0 b0 c0 ...}
//// y <- #{a1 b1 c1 ...}
//Term reduce_dup_ctr(Term dup, Term ctr) {
////printf("reduce_dup_ctr "); print_term(dup); printf("\n");
//inc_itr();
//Loc dup_loc = term_loc(dup);
//Lab dup_lab = term_lab(dup);
//Loc ctr_loc = term_loc(ctr);
//Lab ctr_lab = term_lab(ctr);
//u64 ctr_ari = HVM.cari[ctr_lab];
//Loc loc = alloc_node(ctr_ari * 2);
////Loc ctr0 = alloc_node(ctr_ari);
//Loc ctr0 = ctr_loc;
//Loc ctr1 = loc + 0;
//for (u64 i = 0; i < ctr_ari; i++) {
//Loc du0 = loc + ctr_ari + i;
//set(du0 + 0, got(ctr_loc + i));
//set(ctr0 + i, term_new(DP0, dup_lab, du0));
//set(ctr1 + i, term_new(DP1, dup_lab, du0));
//}
//if (term_tag(dup) == DP0) {
//sub(dup_loc + 0, term_new(CTR, ctr_lab, ctr1));
//return term_new(CTR, ctr_lab, ctr0);
//} else {
//sub(dup_loc + 0, term_new(CTR, ctr_lab, ctr0));
//return term_new(CTR, ctr_lab, ctr1);
//}
//}
//// ! &L{x y} = 123
//// --------------- DUP-W32
//// x <- 123
//// y <- 123
//Term reduce_dup_u32(Term dup, Term u32) {
////printf("reduce_dup_u32 "); print_term(dup); printf("\n");
//inc_itr();
//Loc dup_loc = term_loc(dup);
//sub(dup_loc + 0, u32);
//return u32;
//}
//// ! &L{x y} = @foo(a b c ...)
//// --------------------------- DUP-REF-COPY (when &L not in @foo)
//// ! &L{a0 a1} = a
//// ! &L{b0 b1} = b
//// ! &L{c0 c1} = c
//// ...
//// x <- @foo(a0 b0 c0 ...)
//// y <- @foo(a1 b1 c1 ...)
//Term reduce_dup_ref(Term dup, Term ref) {
////printf("reduce_dup_ref "); print_term(dup); printf("\n");
//inc_itr();
//Loc dup_loc = term_loc(dup);
//Lab dup_lab = term_lab(dup);
//Loc ref_loc = term_loc(ref);
//Lab ref_lab = term_lab(ref);
//u64 ref_ari = HVM.fari[ref_lab];
//Loc loc = alloc_node(ref_ari * 2);
//Loc ref0 = ref_loc;
//Loc ref1 = loc + 0;
//for (u64 i = 0; i < ref_ari; i++) {
//Loc du0 = loc + ref_ari + i;
//set(du0 + 0, got(ref_loc + i));
//set(ref0 + i, term_new(DP0, dup_lab, du0));
//set(ref1 + i, term_new(DP1, dup_lab, du0));
//}
//if (term_tag(dup) == DP0) {
//sub(dup_loc + 0, term_new(REF, ref_lab, ref1));
//return term_new(REF, ref_lab, ref0);
//} else {
//sub(dup_loc + 0, term_new(REF, ref_lab, ref0));
//return term_new(REF, ref_lab, ref1);
//}
//}
//// ~ * {K0 K1 K2 ...}
//// ------------------ MAT-ERA
//// *
//Term reduce_mat_era(Term mat, Term era) {
////printf("reduce_mat_era "); print_term(mat); printf("\n");
//inc_itr();
//return era;
//}
//// ~ λx(x) {K0 K1 K2 ...}
//// ------------------------ MAT-LAM
//// ⊥
//Term reduce_mat_lam(Term mat, Term lam) {
////printf("reduce_mat_lam "); print_term(mat); printf("\n");
//printf("invalid:mat-lam");
//exit(0);
//}
//// ~ &L{x y} {K0 K1 K2 ...}
//// ------------------------ MAT-SUP
//// ! &L{k0a k0b} = K0
//// ! &L{k1a k1b} = K1
//// ! &L{k2a k2b} = K2
//// ...
//// &L{ ~ x {K0a K1a K2a ...}
//// ~ y {K0b K1b K2b ...} }
//Term reduce_mat_sup(Term mat, Term sup) {
////printf("reduce_mat_sup "); print_term(mat); printf("\n");
//inc_itr();
//Tag mat_tag = term_tag(mat);
//Lab mat_lab = term_lab(mat);
//Loc mat_loc = term_loc(mat);
//Loc sup_loc = term_loc(sup);
//Lab sup_lab = term_lab(sup);
//Term tm0 = got(sup_loc + 0);
//Term tm1 = got(sup_loc + 1);
//u64 mat_len = mat_tag == SWI ? mat_lab : mat_tag == IFL ? 2 : HVM.clen[mat_lab];
//Loc loc = alloc_node(1 + mat_len + mat_len);
//Loc mat0 = mat_loc;
//Loc mat1 = loc + 0;
//Loc sup0 = sup_loc;
//set(mat0 + 0, tm0);
//set(mat1 + 0, tm1);
//for (u64 i = 0; i < mat_len; i++) {
//Loc du0 = loc + 1 + mat_len + i;
//set(du0 + 0, got(mat_loc + 1 + i));
//set(mat0 + 1 + i, term_new(DP0, sup_lab, du0));
//set(mat1 + 1 + i, term_new(DP1, sup_lab, du0));
//}
//set(sup0 + 0, term_new(mat_tag, mat_lab, mat0));
//set(sup0 + 1, term_new(mat_tag, mat_lab, mat1));
//return term_new(SUP, sup_lab, sup0);
//}
//Term reduce_mat_ctr(Term mat, Term ctr) {
//inc_itr();
//Tag mat_tag = term_tag(mat);
//Loc mat_loc = term_loc(mat);
//Lab mat_lab = term_lab(mat);
//// If-Let
//if (mat_tag == IFL) {
//Loc ctr_loc = term_loc(ctr);
//Lab ctr_lab = term_lab(ctr);
//u64 mat_ctr = mat_lab;
//u64 ctr_num = ctr_lab;
//u64 ctr_ari = HVM.cari[ctr_num];
//if (mat_ctr == ctr_num) {
//Term app = got(mat_loc + 1);
//Loc loc = alloc_node(ctr_ari * 2);
//for (u64 i = 0; i < ctr_ari; i++) {
//Loc new_app = loc + i * 2;
//set(new_app + 0, app);
//set(new_app + 1, got(ctr_loc + i));
//app = term_new(APP, 0, new_app);
//}
//return app;
//} else {
//Term app = got(mat_loc + 2);
//Loc new_app = mat_loc;
//set(new_app + 0, app);
//set(new_app + 1, ctr);
//app = term_new(APP, 0, new_app);
//return app;
//}
//// Match
//} else {
//Loc ctr_loc = term_loc(ctr);
//Lab ctr_lab = term_lab(ctr);
//u64 ctr_num = ctr_lab;
//u64 ctr_ari = HVM.cari[ctr_num];
//u64 mat_ctr = mat_lab;
//u64 cse_idx = ctr_num - mat_ctr;
//Term app = got(mat_loc + 1 + cse_idx);
//Loc loc = alloc_node(ctr_ari * 2);
//for (u64 i = 0; i < ctr_ari; i++) {
//Loc new_app = loc + i * 2;
//set(new_app + 0, app);
//set(new_app + 1, got(ctr_loc + i));
//app = term_new(APP, 0, new_app);
//}
//return app;
//}
//}
//// ~ num {K0 K1 K2 ... KN}
//// ----------------------- MAT-W32
//// if n < N: Kn
//// else : KN(num-N)
//Term reduce_mat_u32(Term mat, Term u32) {
////printf("reduce_mat_u32 "); print_term(mat); printf("\n");
//inc_itr();
//Loc mat_loc = term_loc(mat);
//Lab mat_lab = term_lab(mat);
//u64 mat_len = mat_lab;
//u64 u32_val = term_loc(u32);
//if (u32_val < mat_len - 1) {
//return got(mat_loc + 1 + u32_val);
//} else {
//Term fn = got(mat_loc + mat_len);
//Loc app = mat_loc;
//set(app + 0, fn);
//set(app + 1, term_new(u32, 0, u32_val - (mat_len - 1)));
//return term_new(APP, 0, app);
//}
//}
//// <op(* b)
//// -------- OPX-ERA
//// *
//Term reduce_opx_era(Term opx, Term era) {
////printf("reduce_opx_era "); print_term(opx); printf("\n");
//inc_itr();
//return era;
//}
//// <op(λx(B) y)
//// --------------- OPX-LAM
//// ⊥
//Term reduce_opx_lam(Term opx, Term lam) {
////printf("reduce_opx_lam "); print_term(opx); printf("\n");
//printf("invalid:opx-lam");
//exit(0);
//}
//// <op(&L{x0 x1} y)
//// ------------------------- OPX-SUP
//// ! &L{y0 y1} = y
//// &L{<op(x0 y0) <op(x1 y1)}
//Term reduce_opx_sup(Term opx, Term sup) {
////printf("reduce_opx_sup "); print_term(opx); printf("\n");
//inc_itr();
//Loc opx_loc = term_loc(opx);
//Loc sup_loc = term_loc(sup);
//Lab sup_lab = term_lab(sup);
//Term nmy = got(opx_loc + 1);
//Term tm0 = got(sup_loc + 0);
//Term tm1 = got(sup_loc + 1);
//Loc loc = alloc_node(3);
//Loc op0 = opx_loc;
//Loc op1 = sup_loc;
//Loc su0 = loc + 0;
//Loc du0 = loc + 2;
//set(op0 + 0, tm0);
//set(op0 + 1, term_new(DP0, sup_lab, du0));
//set(op1 + 0, tm1);
//set(op1 + 1, term_new(DP1, sup_lab, du0));
//set(su0 + 0, term_new(OPX, term_lab(opx), op0));
//set(su0 + 1, term_new(OPX, term_lab(opx), op1));
//set(du0 + 0, nmy);
//return term_new(SUP, sup_lab, su0);
//}
//// <op(#{x0 x1 x2...} y)
//// --------------------- OPX-CTR
//// ⊥
//Term reduce_opx_ctr(Term opx, Term ctr) {
////printf("reduce_opx_ctr "); print_term(opx); printf("\n");
//printf("invalid:opx-ctr");
//exit(0);
//}
//// <op(x0 x1)
//// ---------- OPX-W32
//// >op(x0 x1)
//Term reduce_opx_u32(Term opx, Term nmx) {
////printf("reduce_opx_u32 "); print_term(opx); printf("\n");
//inc_itr();
//Lab opx_lab = term_lab(opx);
//Loc opx_loc = term_loc(opx);
//Term nmy = got(opx_loc + 1);
//set(opx_loc + 0, nmy);
//set(opx_loc + 1, nmx);
//return term_new(OPY, opx_lab, opx_loc);
//}
//// >op(a *)
//// -------- OPY-ERA
//// *
//Term reduce_opy_era(Term opy, Term era) {
////printf("reduce_opy_era "); print_term(opy); printf("\n");
//inc_itr();
//return era;
//}
//// >op(a λx(B))
//// ------------ OPY-LAM
//// *
//Term reduce_opy_lam(Term opy, Term era) {
////printf("reduce_opy_lam "); print_term(opy); printf("\n");
//printf("invalid:opy-lam");
//exit(0);
//}
//// >op(a &L{x y})
//// --------------------- OPY-SUP
//// &L{>op(a x) >op(a y)}
//Term reduce_opy_sup(Term opy, Term sup) {
////printf("reduce_opy_sup "); print_term(opy); printf("\n");
//inc_itr();
//Loc opy_loc = term_loc(opy);
//Loc sup_loc = term_loc(sup);
//Lab sup_lab = term_lab(sup);
//Term nmx = got(opy_loc + 1);
//Term tm0 = got(sup_loc + 0);
//Term tm1 = got(sup_loc + 1);
//Loc op0 = sup_loc;
//Loc op1 = opy_loc;
//Loc su0 = alloc_node(2);
////set(op0 + 0, tm0);
//set(op0 + 1, nmx);
//set(op1 + 0, tm1);
////set(op1 + 1, nmx);
//set(su0 + 0, term_new(OPY, term_lab(opy), op0));
//set(su0 + 1, term_new(OPY, term_lab(opy), op1));
//return term_new(SUP, sup_lab, su0);
//}
//// >op(#{x y z ...} b)
//// ---------------------- OPY-CTR
//// ⊥
//Term reduce_opy_ctr(Term opy, Term ctr) {
////printf("reduce_opy_ctr "); print_term(opy); printf("\n");
//printf("invalid:opy-ctr");
//exit(0);
//}
//// >op(x y)
//// --------- OPY-W32
//// x op y
//Term reduce_opy_u32(Term opy, Term val) {
////printf("reduce_opy_u32 "); print_term(opy); printf("\n");
//inc_itr();
//Loc opy_loc = term_loc(opy);
//Tag t = term_tag(val);
//u32 x = term_loc(got(opy_loc + 1));
//u32 y = term_loc(val);
//u32 result;
//switch (term_lab(opy)) {
//case OP_ADD: result = x + y; break;
//case OP_SUB: result = x - y; break;
//case OP_MUL: result = x * y; break;
//case OP_DIV: result = x / y; break;
//case OP_MOD: result = x % y; break;
//case OP_EQ: result = x == y; break;
//case OP_NE: result = x != y; break;
//case OP_LT: result = x < y; break;
//case OP_GT: result = x > y; break;
//case OP_LTE: result = x <= y; break;
//case OP_GTE: result = x >= y; break;
//case OP_AND: result = x & y; break;
//case OP_OR: result = x | y; break;
//case OP_XOR: result = x ^ y; break;
//case OP_LSH: result = x << y; break;
//case OP_RSH: result = x >> y; break;
//default: {
//printf("invalid:opy-u32");
//exit(0);
//}
//}
//return term_new(t, 0, result);
//}
//Term reduce(Term term) {
//if (term_tag(term) >= ERA) return term;
//Term next = term;
//u64 stop = *HVM.spos;
//u64 spos = stop;
//Term* sbuf = HVM.sbuf;
//while (1) {
////printf("NEXT "); print_term(term); printf("\n");
////printf("PATH ");
////for (u64 i = 0; i < *spos; ++i) {
////print_tag(term_tag(HVM.sbuf[i]));
////printf(" ");
////}
////printf(" ~ %p", HVM.sbuf);
////printf("\n");
//Tag tag = term_tag(next);
//Lab lab = term_lab(next);
//Loc loc = term_loc(next);
//// On variables: substitute
//// On eliminators: move to field
//switch (tag) {
//case LET: {
//switch (lab) {
//case LAZY: {
//next = reduce_let(next, got(loc + 0));
//continue;
//}
//case STRI: {
//spush(next, sbuf, &spos);
//next = got(loc + 0);
//continue;
//}
//default: {
//printf("invalid:let");
//exit(0);
//}
//}
//}
//case APP:
//case MAT:
//case IFL:
//case SWI:
//case OPX:
//case OPY: {
//spush(next, sbuf, &spos);
//next = got(loc + 0);
//continue;
//}
//case DP0:
//case DP1: {
//Term sub = got(loc + 0);
//if (term_get_bit(sub) == 0) {
//spush(next, sbuf, &spos);
//next = sub;
//continue;
//} else {
//next = term_rem_bit(sub);
//continue;
//}
//}
//case VAR: {
//Term sub = got(loc);
//if (term_get_bit(sub) == 0) {
//break;
//} else {
//next = term_rem_bit(sub);
//continue;
//}
//}
//case REF: {
//*HVM.spos = spos;
//next = reduce_ref(next);
//spos = *HVM.spos;
//continue;
//}
//default: break;
//}
//// Empty stack: term is in WHNF
//if (spos == stop) {
//*HVM.spos = spos;
//return next;
//}
//// Interaction Dispatcher
//Term prev = spop(sbuf, &spos);
//Tag ptag = term_tag(prev);
//Lab plab = term_lab(prev);
//Loc ploc = term_loc(prev);
//switch (ptag) {
//case LET: {
//next = reduce_let(prev, next);
//continue;
//}
//case APP: {
//switch (tag) {
//case ERA: next = reduce_app_era(prev, next); continue;
//case LAM: next = reduce_app_lam(prev, next); continue;
//case SUP: next = reduce_app_sup(prev, next); continue;
//case CTR: next = reduce_app_ctr(prev, next); continue;
//case W32: next = reduce_app_u32(prev, next); continue;
//case CHR: next = reduce_app_u32(prev, next); continue;
//default: break;
//}
//}
//case DP0:
//case DP1: {
//switch (tag) {
//case ERA: next = reduce_dup_era(prev, next); continue;
//case LAM: next = reduce_dup_lam(prev, next); continue;
//case SUP: next = reduce_dup_sup(prev, next); continue;
//case CTR: next = reduce_dup_ctr(prev, next); continue;
//case W32: next = reduce_dup_u32(prev, next); continue;
//case CHR: next = reduce_dup_u32(prev, next); continue;
//default: break;
//}
//}
//case MAT:
//case IFL:
//case SWI: {
//switch (tag) {
//case ERA: next = reduce_mat_era(prev, next); continue;
//case LAM: next = reduce_mat_lam(prev, next); continue;
//case SUP: next = reduce_mat_sup(prev, next); continue;
//case CTR: next = reduce_mat_ctr(prev, next); continue;
//case W32: next = reduce_mat_u32(prev, next); continue;
//case CHR: next = reduce_mat_u32(prev, next); continue;
//default: break;
//}
//}
//case OPX: {
//switch (tag) {
//case ERA: next = reduce_opx_era(prev, next); continue;
//case LAM: next = reduce_opx_lam(prev, next); continue;
//case SUP: next = reduce_opx_sup(prev, next); continue;
//case CTR: next = reduce_opx_ctr(prev, next); continue;
//case W32: next = reduce_opx_u32(prev, next); continue;
//case CHR: next = reduce_opx_u32(prev, next); continue;
//default: break;
//}
//}
//case OPY: {
//switch (tag) {
//case ERA: next = reduce_opy_era(prev, next); continue;
//case LAM: next = reduce_opy_lam(prev, next); continue;
//case SUP: next = reduce_opy_sup(prev, next); continue;
//case CTR: next = reduce_opy_ctr(prev, next); continue;
//case W32: next = reduce_opy_u32(prev, next); continue;
//case CHR: next = reduce_opy_u32(prev, next); continue;
//default: break;
//}
//}
//default: break;
//}
//// No interaction: push term back to stack
//spush(prev, sbuf, &spos);
//// Update parent chain
//while (spos > stop) {
//Term host = spop(sbuf, &spos);
//Tag htag = term_tag(host);
//Lab hlab = term_lab(host);
//Loc hloc = term_loc(host);
//set(hloc + 0, next);
//next = host;
//}
//*HVM.spos = spos;
//return next;
//}
//}
//Term reduce_at(Loc host) {
//Term tm0 = got(host);
//if (term_tag(tm0) >= ERA) {
//return tm0;
//}
//Term tm1 = reduce(tm0);
//set(host, tm1);
//return tm1;
//}
//Term normal(Term term) {
//Term wnf = reduce(term);
//Tag tag = term_tag(wnf);
//Lab lab = term_lab(wnf);
//Loc loc = term_loc(wnf);
//switch (tag) {
//case LAM: {
//Term bod = got(loc + 0);
//bod = normal(bod);
//set(term_loc(wnf) + 1, bod);
//return wnf;
//}
//case APP: {
//Term fun = got(loc + 0);
//Term arg = got(loc + 1);
//fun = normal(fun);
//arg = normal(arg);
//set(term_loc(wnf) + 0, fun);
//set(term_loc(wnf) + 1, arg);
//return wnf;
//}
//case SUP: {
//Term tm0 = got(loc + 0);
//Term tm1 = got(loc + 1);
//tm0 = normal(tm0);
//tm1 = normal(tm1);
//set(term_loc(wnf) + 0, tm0);
//set(term_loc(wnf) + 1, tm1);
//return wnf;
//}
//case DP0:
//case DP1: {
//Term val = got(loc + 0);
//val = normal(val);
//set(term_loc(wnf) + 0, val);
//return wnf;
//}
//case CTR: {
//u64 cid = lab;
//u64 ari = HVM.cari[cid];
//for (u64 i = 0; i < ari; i++) {
//Term arg = got(loc + i);
//arg = normal(arg);
//set(term_loc(wnf) + i, arg);
//}
//return wnf;
//}
//case MAT:
//case IFL:
//case SWI: {
//u64 len = tag == SWI ? lab : tag == IFL ? 2 : HVM.clen[lab];
//for (u64 i = 0; i <= len; i++) {
//Term arg = got(loc + i);
//arg = normal(arg);
//set(term_loc(wnf) + i, arg);
//}
//return wnf;
//}
//default:
//return wnf;
//}
//}
//// Primitives
//// ----------
//// Primitive: Dynamic Sup @SUP(lab tm0 tm1)
//// Allocates a new SUP node with given label.
//Term SUP_f(Term ref) {
//Loc ref_loc = term_loc(ref);
//Term lab = reduce(got(ref_loc + 0));
//Term lab_val = term_loc(lab);
//if (term_tag(lab) != W32) {
//printf("ERROR:non-numeric-sup-label\n");
//}
//if (lab_val > 0xFFFF) {
//printf("ERROR:sup-label-too-large\n");
//}
//Term tm0 = got(ref_loc + 1);
//Term tm1 = got(ref_loc + 2);
//Loc sup = alloc_node(2);
//Term ret = term_new(SUP, lab_val, sup);
//set(sup + 0, tm0);
//set(sup + 1, tm1);
//*HVM.itrs += 1;
//return ret;
//}
//// Primitive: Dynamic Dup @DUP(lab val λdp0λdp1(bod))
//// Creates a DUP node with given label.
//Term DUP_f(Term ref) {
//Loc ref_loc = term_loc(ref);
//Term lab = reduce(got(ref_loc + 0));
//Term lab_val = term_loc(lab);
//if (term_tag(lab) != W32) {
//printf("ERROR:non-numeric-dup-label\n");
//}
//if (lab_val > 0xFFFF) {
//printf("ERROR:dup-label-too-large\n");
//}
//Term val = got(ref_loc + 1);
//Term bod = got(ref_loc + 2);
//Loc dup = alloc_node(1);
//set(dup + 0, val);
//if (term_tag(bod) == LAM) {
//Loc lam0 = term_loc(bod);
//Term bod0 = got(lam0 + 0);
//if (term_tag(bod0) == LAM) {
//Loc lam1 = term_loc(bod0);
//Term bod1 = got(lam1 + 0);
//sub(lam0 + 0, term_new(DP0, lab_val, dup));
//sub(lam1 + 0, term_new(DP1, lab_val, dup));
//*HVM.itrs += 3;
//return bod1;
//}
//}
//Loc app0 = alloc_node(2);
//set(app0 + 0, bod);
//set(app0 + 1, term_new(DP0, lab_val, dup));
//Loc app1 = alloc_node(2);
//set(app1 + 0, term_new(APP, 0, app0));
//set(app1 + 1, term_new(DP1, lab_val, dup));
//*HVM.itrs += 1;
//return term_new(APP, 0, app1);
//}
//Term LOG_f(Term ref) {
//printf("TODO: LOG_f");
//exit(0);
//}
//void *alloc_huge(size_t size) {
//void *ptr = mmap(NULL, size, PROT_READ | PROT_WRITE,
//MAP_PRIVATE | MAP_ANONYMOUS | MAP_NORESERVE,
//-1, 0);
//if (ptr == MAP_FAILED) {
//perror("mmap failed");
//return NULL;
//}
//return ptr;
//}
//// Runtime Memory
//// --------------
//void hvm_init() {
//HVM.sbuf = alloc_huge(MAX_STACK_SIZE * sizeof(Term));
//HVM.heap = alloc_huge(MAX_HEAP_SIZE * sizeof(Term));
//HVM.spos = alloc_huge(sizeof(u64));
//HVM.size = alloc_huge(sizeof(u64));
//HVM.itrs = alloc_huge(sizeof(u64));
//HVM.frsh = alloc_huge(sizeof(u64));
//#define CHECK_ALLOC(ptr, name) if (!(ptr)) { printf(name " alloc failed\n"); allocs_failed++; }
//int allocs_failed = 0; // Track if any allocation failed
//CHECK_ALLOC(HVM.sbuf, "sbuf");
//CHECK_ALLOC(HVM.heap, "heap");
//CHECK_ALLOC(HVM.spos, "spos");
//CHECK_ALLOC(HVM.size, "size");
//CHECK_ALLOC(HVM.itrs, "itrs");
//CHECK_ALLOC(HVM.frsh, "frsh");
//if (allocs_failed > 0) {
//printf("hvm_init alloc's failed: %d allocations failed\n", allocs_failed);
//exit(1);
//}
//#undef CHECK_ALLOC
//*HVM.spos = 0;
//*HVM.size = 1;
//*HVM.itrs = 0;
//*HVM.frsh = 0x20;
//HVM.book[SUP_F] = SUP_f;
//HVM.book[DUP_F] = DUP_f;
//HVM.book[LOG_F] = LOG_f;
//for (int i = 0; i < 65536; i++) {
//HVM.cari[i] = 0;
//HVM.clen[i] = 0;
//HVM.cadt[i] = 0;
//HVM.fari[i] = 0;
//}
//}
//void hvm_munmap(void *ptr, size_t size, const char *name) {
//if (ptr != MAP_FAILED) {
//if (munmap(ptr, size) == -1) {
//perror("munmap failed");
//} else {
//// printf("Successfully unmapped %s\n", name);
//}
//} else {
//printf("%s is already null or invalid.\n", name);
//}
//}
//void hvm_free() {
//hvm_munmap(HVM.sbuf, MAX_STACK_SIZE * sizeof(Term), "sbuf");
//hvm_munmap(HVM.heap, MAX_HEAP_SIZE * sizeof(Term), "heap");
//hvm_munmap(HVM.spos, sizeof(u64), "spos");
//hvm_munmap(HVM.size, sizeof(u64), "size");
//hvm_munmap(HVM.itrs, sizeof(u64), "itrs");
//hvm_munmap(HVM.frsh, sizeof(u64), "frsh");
//}
//State* hvm_get_state() {
//return &HVM;
//}
//void hvm_set_state(State* hvm) {
//HVM.sbuf = hvm->sbuf;
//HVM.spos = hvm->spos;
//HVM.heap = hvm->heap;
//HVM.size = hvm->size;
//HVM.itrs = hvm->itrs;
//HVM.frsh = hvm->frsh;
//for (int i = 0; i < 65536; i++) {
//HVM.book[i] = hvm->book[i];
//HVM.fari[i] = hvm->fari[i];
//HVM.cari[i] = hvm->cari[i];
//HVM.clen[i] = hvm->clen[i];
//HVM.cadt[i] = hvm->cadt[i];
//}
//}
//void hvm_define(u16 fid, Term (*func)()) {
////printf("defined %llu %p\n", fid, func);
//HVM.book[fid] = func;
//}
//void hvm_set_cari(u16 cid, u16 arity) {
//HVM.cari[cid] = arity;
//}
//void hvm_set_fari(u16 fid, u16 arity) {
//HVM.fari[fid] = arity;
//}
//void hvm_set_clen(u16 cid, u16 cases) {
//HVM.clen[cid] = cases;
//}
//void hvm_set_cadt(u16 cid, u16 adt) {
//HVM.cadt[cid] = adt;
//}
// GOAL: our goal now is to fully rewrite Runtime.c taking in account the changes made to the Core type
// do it below.
// COMPLETE, UPDATED RUNTIME.C FILE:
//#include <inttypes.h>
//#include <stdint.h>
//#include <stdio.h>
//#include <stdlib.h>
//#include <sys/mman.h>
//#include <unistd.h>
//#include <time.h>
//#include <stdbool.h>
//#define MAX_HEAP_SIZE (1ULL << 32)
//#define MAX_STACK_SIZE (1ULL << 28)
//typedef uint8_t Tag;
//typedef uint32_t Lab;
//typedef uint32_t Loc;
//typedef uint64_t Term;
//typedef uint16_t u16;
//typedef uint32_t u32;
//typedef uint64_t u64;
//// Runtime Types
//// -------------
//typedef struct {
//Term* sbuf; // reduction stack buffer
//u64* spos; // reduction stack position
//Term* heap; // global node buffer
//u64* size; // global node buffer position
//u64* itrs; // interaction count
//u64* frsh; // fresh dup label count
//Term (*book[65536])(Term); // functions
//u16 fari[65536]; // arity of each function
//} State;
//static State HVM = {
//.sbuf = NULL,
//.spos = NULL,
//.heap = NULL,
//.size = NULL,
//.itrs = NULL,
//.frsh = NULL,
//.book = {NULL},
//.fari = {0},
//};
//// Constants
//// ---------
//#define DP0 0x00
//#define DP1 0x01
//#define VAR 0x02
//#define REF 0x03
//#define LET 0x04
//#define ERA 0x05
//#define SUP 0x06
//#define DUP 0x07
//#define SET 0x08
//#define EMP 0x09
//#define EFQ 0x0A
//#define UNI 0x0B
//#define NIL 0x0C
//#define USE 0x0D
//#define U32 0x0E
//#define W32 0x0F
//#define SWI 0x10
//#define OPX 0x11
//#define OPY 0x12
//#define SIG 0x13
//#define TUP 0x14
//#define GET 0x15
//#define ALL 0x16
//#define LAM 0x17
//#define APP 0x18
//#define OP_ADD 0x00
//#define OP_SUB 0x01
//#define OP_MUL 0x02
//#define OP_DIV 0x03
//#define OP_MOD 0x04
//#define OP_EQ 0x05
//#define OP_NE 0x06
//#define OP_LT 0x07
//#define OP_GT 0x08
//#define OP_LTE 0x09
//#define OP_GTE 0x0A
//#define OP_AND 0x0B
//#define OP_OR 0x0C
//#define OP_XOR 0x0D
//#define OP_LSH 0x0E
//#define OP_RSH 0x0F
//#define DUP_F 0xFFFF
//#define SUP_F 0xFFFE
//#define LOG_F 0xFFFD
//#define LAZY 0x0
//#define STRI 0x1
//#define VOID 0x00000000000000
//// Heap
//// ----
//void set_len(u64 size) {
//*HVM.size = size;
//}
//void set_itr(u64 itrs) {
//*HVM.itrs = itrs;
//}
//u64 get_len() {
//return *HVM.size;
//}
//u64 get_itr() {
//return *HVM.itrs;
//}
//u64 fresh() {
//return (*HVM.frsh)++;
//}
//// Terms
//// ------
//Term term_new(Tag tag, Lab lab, Loc loc) {
//Term tag_enc = tag;
//Term lab_enc = ((Term)lab) << 8;
//Term loc_enc = ((Term)loc) << 32;
//return tag_enc | lab_enc | loc_enc;
//}
//Tag term_tag(Term x) {
//return x & 0x7F;
//}
//Lab term_lab(Term x) {
//return (x >> 8) & 0xFFFFFF;
//}
//Loc term_loc(Term x) {
//return (x >> 32) & 0xFFFFFFFF;
//}
//u64 term_get_bit(Term x) {
//return (x >> 7) & 1;
//}
//Term term_set_bit(Term term) {
//return term | (1ULL << 7);
//}
//Term term_rem_bit(Term term) {
//return term & ~(1ULL << 7);
//}
//Term term_set_loc(Term x, Loc loc) {
//return (x & 0x00000000FFFFFFFF) | (((Term)loc) << 32);
//}
//_Bool term_is_atom(Term term) {
//switch (term_tag(term)) {
//case ERA:
//case W32:
//case NIL:
//case SET:
//case EMP:
//case UNI:
//case U32: return 1;
//default: return 0;
//}
//}
//// Atomics
//// -------
//Term swap(Loc loc, Term term) {
//Term val = HVM.heap[loc];
//HVM.heap[loc] = term;
//if (val == 0) {
//printf("SWAP 0 at %08llx\n", (u64)loc);
//exit(0);
//}
//return val;
//}
//Term got(Loc loc) {
//Term val = HVM.heap[loc];
//if (val == 0) {
//printf("GOT 0 at %08llx\n", (u64)loc);
//exit(0);
//}
//return val;
//}
//void set(Loc loc, Term term) {
//HVM.heap[loc] = term;
//}
//void sub(Loc loc, Term term) {
//set(loc, term_set_bit(term));
//}
//Term take(Loc loc) {
//return swap(loc, VOID);
//}
//// Allocation
//// ----------
//Loc alloc_node(Loc arity) {
//if (*HVM.size + arity > MAX_HEAP_SIZE) {
//printf("Heap memory limit exceeded\n");
//exit(1);
//}
//u64 old = *HVM.size;
//*HVM.size += arity;
//return old;
//}
//void inc_itr() {
//(*HVM.itrs)++;
//}
//// Stack
//// ----
//void spush(Term term, Term* sbuf, u64* spos) {
//if (*spos >= MAX_STACK_SIZE) {
//printf("Stack memory limit exceeded\n");
//exit(1);
//}
//sbuf[(*spos)++] = term;
//}
//Term spop(Term* sbuf, u64* spos) {
//return sbuf[--(*spos)];
//}
//// Stringification
//// ---------------
//void print_tag(Tag tag) {
//switch (tag) {
//case VAR: printf("VAR"); break;
//case DP0: printf("DP0"); break;
//case DP1: printf("DP1"); break;
//case REF: printf("REF"); break;
//case LET: printf("LET"); break;
//case ERA: printf("ERA"); break;
//case SUP: printf("SUP"); break;
//case DUP: printf("DUP"); break;
//case SET: printf("SET"); break;
//case EMP: printf("EMP"); break;
//case EFQ: printf("EFQ"); break;
//case UNI: printf("UNI"); break;
//case NIL: printf("NIL"); break;
//case USE: printf("USE"); break;
//case U32: printf("U32"); break;
//case W32: printf("W32"); break;
//case SWI: printf("SWI"); break;
//case OPX: printf("OPX"); break;
//case OPY: printf("OPY"); break;
//case SIG: printf("SIG"); break;
//case TUP: printf("TUP"); break;
//case GET: printf("GET"); break;
//case ALL: printf("ALL"); break;
//case LAM: printf("LAM"); break;
//case APP: printf("APP"); break;
//default : printf("???"); break;
//}
//}
//void print_term(Term term) {
//printf("term_new(");
//print_tag(term_tag(term));
//printf(",0x%06llx,0x%08llx)", (u64)term_lab(term), (u64)term_loc(term));
//}
//void print_heap() {
//for (Loc i = 0; i < *HVM.size; i++) {
//Term term = got(i);
//if (term != 0) {
//printf("set(0x%08llx, ", (u64)i);
//print_term(term);
//printf(");\n");
//}
//}
//}
//// Evaluation
//// ----------
//// @foo(&L{ax ay} b c ...)
//// ----------------------- REF-SUP-COPY (when @L not in @foo)
//// ! &L{bx by} = b
//// ! &L{cx cy} = b
//// ...
//// &L{@foo(ax bx cx ...) @foo(ay by cy ...)}
//// @foo(a b c ...)
//// -------------------- REF
//// book[foo](a b c ...)
//Term reduce_ref(Term ref) {
//inc_itr();
//return HVM.book[term_lab(ref)](ref);
//}
//// ! x = val
//// bod
//// --------- LET
//// x <- val
//// bod
//Term reduce_let(Term let, Term val) {
////printf("reduce_let "); print_term(let); printf("\n");
//inc_itr();
//Loc let_loc = term_loc(let);
//Term bod = got(let_loc + 1);
//sub(let_loc + 0, val);
//return bod;
//}
//// (* a)
//// ------- APP-ERA
//// *
//Term reduce_app_era(Term app, Term era) {
////printf("reduce_app_era "); print_term(app); printf("\n");
//inc_itr();
//return era;
//}
//// (λx.f a)
//// -------- APP-LAM
//// x <- a
//// f
//Term reduce_app_lam(Term app, Term lam) {
//inc_itr();
//Loc app_loc = term_loc(app);
//Loc lam_loc = term_loc(lam);
//Term bod = got(lam_loc + 0);
//Term arg = got(app_loc + 1);
//sub(lam_loc + 0, arg);
//return bod;
//}
//// (&L{a,b} c)
//// ----------------- APP-SUP
//// ! &L{c0,c1} = c;
//// &L{(a c0),(b c1)}
//Term reduce_app_sup(Term app, Term sup) {
////printf("reduce_app_sup "); print_term(app); printf("\n");
//inc_itr();
//Loc app_loc = term_loc(app);
//Loc sup_loc = term_loc(sup);
//Lab sup_lab = term_lab(sup);
//Term arg = got(app_loc + 1);
//Term tm1 = got(sup_loc + 1);
//Loc loc = alloc_node(3);
//Loc ap0 = sup_loc;
//Loc ap1 = loc + 0;
//Loc su0 = app_loc;
//Loc dup = loc + 2;
//set(ap0 + 1, term_new(DP0, sup_lab, dup));
//set(ap1 + 0, tm1);
//set(ap1 + 1, term_new(DP1, sup_lab, dup));
//set(su0 + 0, term_new(APP, 0, ap0));
//set(su0 + 1, term_new(APP, 0, ap1));
//set(dup + 0, arg);
//return term_new(SUP, sup_lab, su0);
//}
//// (() a)
//// ------ APP-NIL
//// error
//Term reduce_app_nil(Term app, Term nil) {
//printf("invalid:app-nil");
//exit(0);
//}
//// ((a,b) c)
//// --------- APP-TUP
//// error
//Term reduce_app_tup(Term app, Term tup) {
//printf("invalid:app-tup");
//exit(0);
//}
//// (123 a)
//// ------- APP-W32
//// error
//Term reduce_app_w32(Term app, Term w32) {
//printf("invalid:app-w32");
//exit(0);
//}
//// (T a)
//// ----- APP-TYP
//// error
//Term reduce_app_typ(Term app, Term typ) {
//printf("invalid:app-typ");
//exit(0);
//}
//// ~*{():f}
//// -------- USE-ERA
//// *
//Term reduce_use_era(Term use, Term era) {
//inc_itr();
//return era;
//}
//// ~&L{a,b}{():f}
//// ----------------------- USE-SUP
//// ! &L{f0,f1} = f;
//// &L{~a{():f0},~b{():f1}}
//Term reduce_use_sup(Term use, Term sup) {
//inc_itr();
//Loc use_loc = term_loc(use);
//Loc sup_loc = term_loc(sup);
//Lab sup_lab = term_lab(sup);
//Term f = got(use_loc + 1);
//Term a = got(sup_loc + 0);
//Term b = got(sup_loc + 1);
//Loc loc = alloc_node(3);
//Loc us0 = sup_loc;
//Loc us1 = loc + 0;
//Loc su0 = use_loc;
//Loc dup = loc + 2;
//set(us0 + 0, a);
//set(us0 + 1, term_new(DP0, sup_lab, dup));
//set(us1 + 0, b);
//set(us1 + 1, term_new(DP1, sup_lab, dup));
//set(su0 + 0, term_new(USE, 0, us0));
//set(su0 + 1, term_new(USE, 0, us1));
//set(dup + 0, f);
//return term_new(SUP, sup_lab, su0);
//}
//// ~λx.g{():f}
//// ----------- USE-LAM
//// error
//Term reduce_use_lam(Term use, Term lam) {
//printf("invalid:use-lam");
//exit(0);
//}
//// ~(){():f}
//// --------- USE-NIL
//// f
//Term reduce_use_nil(Term use, Term nil) {
//inc_itr();
//Loc use_loc = term_loc(use);
//Term f = got(use_loc + 1);
//return f;
//}
//// ~(p,q){():f}
//// ------------ USE-TUP
//// error
//Term reduce_use_tup(Term use, Term tup) {
//printf("invalid:use-tup");
//exit(0);
//}
//// ~123{():f}
//// ---------- USE-W32
//// error
//Term reduce_use_w32(Term use, Term w32) {
//printf("invalid:use-w32");
//exit(0);
//}
//// ~T{():f}
//// -------- USE-TYP
//// error
//Term reduce_use_typ(Term use, Term typ) {
//printf("invalid:use-typ");
//exit(0);
//}
//// ~*{(,):f}
//// --------- GET-ERA
//// *
//Term reduce_get_era(Term get, Term era) {
//inc_itr();
//return era;
//}
//// ~&L{a,b}{(,): f}
//// ------------------------- GET-SUP
//// ! &L{f0,f1} = f;
//// &L{~a{(,):f0},~b{(,):f1}}
//Term reduce_get_sup(Term get, Term sup) {
//inc_itr();
//Loc get_loc = term_loc(get);
//Loc sup_loc = term_loc(sup);
//Lab sup_lab = term_lab(sup);
//Term f = got(get_loc + 1);
//Term a = got(sup_loc + 0);
//Term b = got(sup_loc + 1);
//Loc loc = alloc_node(3);
//Loc gt0 = sup_loc;
//Loc gt1 = loc + 0;
//Loc su0 = get_loc;
//Loc dup = loc + 2;
//set(gt0 + 0, a);
//set(gt0 + 1, term_new(DP0, sup_lab, dup));
//set(gt1 + 0, b);
//set(gt1 + 1, term_new(DP1, sup_lab, dup));
//set(su0 + 0, term_new(GET, 0, gt0));
//set(su0 + 1, term_new(GET, 0, gt1));
//set(dup + 0, f);
//return term_new(SUP, sup_lab, su0);
//}
//// ~(){(,):f}
//// ---------- GET-NIL
//// error
//Term reduce_get_nil(Term get, Term nil) {
//printf("invalid:get-nil");
//exit(0);
//}
//// ~(a,b){(,):f}
//// ------------- GET-TUP
//// (f a b)
//Term reduce_get_tup(Term get, Term tup) {
//inc_itr();
//Loc get_loc = term_loc(get);
//Loc tup_loc = term_loc(tup);
//Term f = got(get_loc + 1);
//Term a = got(tup_loc + 0);
//Term b = got(tup_loc + 1);
//Loc app1 = alloc_node(2);
//Loc app2 = get_loc;
//set(app1 + 0, f);
//set(app1 + 1, a);
//set(app2 + 0, term_new(APP, 0, app1));
//set(app2 + 1, b);
//return term_new(APP, 0, app2);
//}
//// ~λx.g{(,):f}
//// ------------ GET-LAM
//// error
//Term reduce_get_lam(Term get, Term lam) {
//printf("invalid:get-lam");
//exit(0);
//}
//// ~123{(,):f}
//// ----------- GET-W32
//// error
//Term reduce_get_w32(Term get, Term w32) {
//printf("invalid:get-w32");
//exit(0);
//}
//// ~TYP{(,):f}
//// ----------- GET-TYP
//// error
//Term reduce_get_typ(Term get, Term typ) {
//printf("invalid:get-typ");
//exit(0);
//}
//// ~*{0:z;+:s}
//// ----------- SWI-ERA
//// *
//Term reduce_swi_era(Term swi, Term era) {
//inc_itr();
//return era;
//}
//// ~&L{a,b}{0:z;+:s}
//// ------------------------------- SWI-SUP
//// ! &L{z0,z1} = z;
//// ! &L{s0,s1} = s;
//// &L{~a{0:z0;+:s0},~b{0:z1;+:s1}}
////Term reduce_swi_sup(Term swi, Term sup) {
////inc_itr();
////Loc swi_loc = term_loc(swi);
////Loc sup_loc = term_loc(sup);
////Lab sup_lab = term_lab(sup);
////Term z = got(swi_loc + 1);
////Term s = got(swi_loc + 2);
////Term a = got(sup_loc + 0);
////Term b = got(sup_loc + 1);
////Loc loc = alloc_node(5);
////Loc sw0 = sup_loc;
////Loc sw1 = loc + 0;
////Loc su0 = swi_loc;
////Loc dz = loc + 2;
////Loc ds = loc + 3;
////set(sw0 + 0, a);
////set(sw0 + 1, term_new(DP0, sup_lab, dz));
////set(sw0 + 2, term_new(DP0, sup_lab, ds));
////set(sw1 + 0, b);
////set(sw1 + 1, term_new(DP1, sup_lab, dz));
////set(sw1 + 2, term_new(DP1, sup_lab, ds));
////set(su0 + 0, term_new(SWI, 0, sw0));
////set(su0 + 1, term_new(SWI, 0, sw1));
////set(dz + 0, z);
////set(ds + 0, s);
////return term_new(SUP, sup_lab, su0);
////}
//// BUG: the function above is INCORRECT. it is re-using a SUP node for a SWI
//// node, but a SUP node has only 2 fields, not 3. this will cause memory errors.
//// you MUST reuse the input sup node for the output sup node, and you MUST reuse
//// the input swi node for one of the output swi nodes - just like the original
//// reduce_mat_sup function did. fix it:
//Term reduce_swi_sup(Term swi, Term sup) {
//// Correct implementation that reuses the given SUP/SWI nodes
//inc_itr();
//// Locations / labels
//Loc swi_loc = term_loc(swi); // original SWI (will become SWI0)
//Loc sup_loc = term_loc(sup); // SUP we will reuse
//Lab sup_lab = term_lab(sup); // label of the SUP
//Lab swi_lab = term_lab(swi); // (unused, still preserve)
//// Extract SWI arms
//Term z = got(swi_loc + 1);
//Term s = got(swi_loc + 2);
//// Extract SUP branches
//Term a = got(sup_loc + 0);
//Term b = got(sup_loc + 1);
//// Allocate:
//// - 3 cells for the second SWI (swi1)
//// - 1 cell for dup(z) (dupz)
//// - 1 cell for dup(s) (dups)
//Loc loc = alloc_node(5);
//Loc swi1 = loc; // 3 cells (value,z,s)
//Loc dupz = loc + 3; // 1 cell
//Loc dups = loc + 4; // 1 cell
//// Store originals inside dup nodes
//set(dupz + 0, z);
//set(dups + 0, s);
//// Build SWI0 (reuse swi_loc)
//set(swi_loc + 0, a);
//set(swi_loc + 1, term_new(DP0, sup_lab, dupz));
//set(swi_loc + 2, term_new(DP0, sup_lab, dups));
//// Build SWI1 (new node)
//set(swi1 + 0, b);
//set(swi1 + 1, term_new(DP1, sup_lab, dupz));
//set(swi1 + 2, term_new(DP1, sup_lab, dups));
//// Build resulting SUP (reuse sup_loc)
//set(sup_loc + 0, term_new(SWI, swi_lab, swi_loc));
//set(sup_loc + 1, term_new(SWI, swi_lab, swi1));
//return term_new(SUP, sup_lab, sup_loc);
//}
//// ~(){0:z;+:s}
//// ------------ SWI-NIL
//// error
//Term reduce_swi_nil(Term swi, Term nil) {
//printf("invalid:swi-nil");
//exit(0);
//}
//// ~(a,b){0:z;+:s}
//// --------------- SWI-TUP
//// error
//Term reduce_swi_tup(Term swi, Term tup) {
//printf("invalid:swi-tup");
//exit(0);
//}
//// ~λx.g{0:z;+:s}
//// -------------- SWI-LAM
//// error
//Term reduce_swi_lam(Term swi, Term lam) {
//printf("invalid:swi-lam");
//exit(0);
//}
//// ~n{0:z;+:s}
//// ----------- SWI-W32
//// if n = 0:
//// z
//// else:
//// (s (n-1))
//Term reduce_swi_w32(Term swi, Term w32) {
//inc_itr();
//Loc swi_loc = term_loc(swi);
//u32 val = term_loc(w32);
//Term z = got(swi_loc + 1);
//Term s = got(swi_loc + 2);
//if (val == 0) {
//return z;
//} else {
//Loc app = swi_loc;
//set(app + 0, s);
//set(app + 1, term_new(W32, 0, val - 1));
//return term_new(APP, 0, app);
//}
//}
//// ~T{0:z;+:s}
//// ----------- SWI-TYP
//// error
//Term reduce_swi_typ(Term swi, Term typ) {
//printf("invalid:swi-typ");
//exit(0);
//}
//// ! &L{r,s} = *
//// ------------- DUP-ERA
//// r <- *
//// s <- *
//Term reduce_dup_era(Term dup, Term era) {
////printf("reduce_dup_era "); print_term(dup); printf("\n");
//inc_itr();
//Loc dup_loc = term_loc(dup);
//sub(dup_loc + 0, era);
//return era;
//}
//// ! &L{x,y} = &L{a,b}
//// ------------------- DUP-SUP
//// x <- a
//// y <- b
//Term reduce_dup_sup(Term dup, Term sup) {
////printf("reduce_dup_sup %u %u | %llu ", term_lab(dup), term_lab(sup), *HVM.spos); print_term(dup); printf(" "); print_term(sup); printf("\n");
//inc_itr();
//Loc dup_loc = term_loc(dup);
//Lab dup_lab = term_lab(dup);
//Lab sup_lab = term_lab(sup);
//Loc sup_loc = term_loc(sup);
//if (dup_lab == sup_lab) {
//Term tm0 = got(sup_loc + 0);
//Term tm1 = got(sup_loc + 1);
//if (term_tag(dup) == DP0) {
//sub(dup_loc + 0, tm1);
//return tm0;
//} else {
//sub(dup_loc + 0, tm0);
//return tm1;
//}
//} else {
//Loc loc = alloc_node(4);
//Loc du0 = sup_loc + 0;
//Loc du1 = sup_loc + 1;
//Loc su0 = loc + 0;
//Loc su1 = loc + 2;
//set(su0 + 0, term_new(DP0, dup_lab, du0));
//set(su0 + 1, term_new(DP0, dup_lab, du1));
//set(su1 + 0, term_new(DP1, dup_lab, du0));
//set(su1 + 1, term_new(DP1, dup_lab, du1));
//if (term_tag(dup) == DP0) {
//sub(dup_loc + 0, term_new(SUP, sup_lab, su1));
//return term_new(SUP, sup_lab, su0);
//} else {
//sub(dup_loc + 0, term_new(SUP, sup_lab, su0));
//return term_new(SUP, sup_lab, su1);
//}
//}
//}
//// ! &L{r s} = λx.f
//// ---------------- DUP-LAM
//// r <- λx0.f0
//// s <- λx1.f1
//// x <- &L{x0,x1}
//// ! &L{f0,f1} = f
//Term reduce_dup_lam(Term dup, Term lam) {
////printf("reduce_dup_lam "); print_term(dup); printf("\n");
//inc_itr();
//Loc dup_loc = term_loc(dup);
//Loc lam_loc = term_loc(lam);
//Lab dup_lab = term_lab(dup);
//Term bod = got(lam_loc + 0);
//Loc loc = alloc_node(5);
//Loc lm0 = loc + 0;
//Loc lm1 = loc + 1;
//Loc su0 = loc + 2;
//Loc du0 = loc + 4;
//sub(lam_loc + 0, term_new(SUP, dup_lab, su0));
//set(lm0 + 0, term_new(DP0, dup_lab, du0));
//set(lm1 + 0, term_new(DP1, dup_lab, du0));
//set(su0 + 0, term_new(VAR, 0, lm0));
//set(su0 + 1, term_new(VAR, 0, lm1));
//set(du0 + 0, bod);
//if (term_tag(dup) == DP0) {
//sub(dup_loc + 0, term_new(LAM, 0, lm1));
//return term_new(LAM, 0, lm0);
//} else {
//sub(dup_loc + 0, term_new(LAM, 0, lm0));
//return term_new(LAM, 0, lm1);
//}
//}
//// ! &L{x,y} = ()
//// -------------- DUP-NIL
//// x <- ()
//// y <- ()
//Term reduce_dup_nil(Term dup, Term nil) {
//inc_itr();
//Loc dup_loc = term_loc(dup);
//sub(dup_loc + 0, nil);
//return nil;
//}
//// ! &L{x,y} = (a,b)
//// ----------------- DUP-TUP
//// ! &L{a0,a1} = a
//// ! &L{b0,b1} = b
//// x <- (a0,b0)
//// y <- (a1,b1)
//Term reduce_dup_tup(Term dup, Term tup) {
//inc_itr();
//Loc dup_loc = term_loc(dup);
//Lab dup_lab = term_lab(dup);
//Loc tup_loc = term_loc(tup);
//Term a = got(tup_loc + 0);
//Term b = got(tup_loc + 1);
//Loc loc = alloc_node(6);
//Loc tup0 = loc + 0;
//Loc tup1 = loc + 2;
//Loc dupa = loc + 4;
//Loc dupb = loc + 5;
//set(dupa + 0, a);
//set(dupb + 0, b);
//set(tup0 + 0, term_new(DP0, dup_lab, dupa));
//set(tup0 + 1, term_new(DP0, dup_lab, dupb));
//set(tup1 + 0, term_new(DP1, dup_lab, dupa));
//set(tup1 + 1, term_new(DP1, dup_lab, dupb));
//if (term_tag(dup) == DP0) {
//sub(dup_loc + 0, term_new(TUP, 0, tup1));
//return term_new(TUP, 0, tup0);
//} else {
//sub(dup_loc + 0, term_new(TUP, 0, tup0));
//return term_new(TUP, 0, tup1);
//}
//}
//// ! &L{x,y} = 123
//// --------------- DUP-W32
//// x <- 123
//// y <- 123
//Term reduce_dup_w32(Term dup, Term w32) {
////printf("reduce_dup_w32 "); print_term(dup); printf("\n");
//inc_itr();
//Loc dup_loc = term_loc(dup);
//sub(dup_loc + 0, w32);
//return w32;
//}
//// ! &L{x,y} = Set
//// --------------- DUP-SET
//// x <- Set
//// y <- Set
//Term reduce_dup_set(Term dup, Term set) {
//inc_itr();
//Loc dup_loc = term_loc(dup);
//sub(dup_loc + 0, set);
//return set;
//}
//// ! &L{x,y} = ⊥
//// ------------- DUP-EMP
//// x <- ⊥
//// y <- ⊥
//Term reduce_dup_emp(Term dup, Term emp) {
//inc_itr();
//Loc dup_loc = term_loc(dup);
//sub(dup_loc + 0, emp);
//return emp;
//}
//// ! &L{x,y} = ⊤
//// ------------- DUP-UNI
//// x <- ⊤
//// y <- ⊤
//Term reduce_dup_uni(Term dup, Term uni) {
//inc_itr();
//Loc dup_loc = term_loc(dup);
//sub(dup_loc + 0, uni);
//return uni;
//}
//// ! &L{x,y} = U32
//// -------------- DUP-U32
//// x <- U32
//// y <- U32
//Term reduce_dup_u32(Term dup, Term u32) {
//inc_itr();
//Loc dup_loc = term_loc(dup);
//sub(dup_loc + 0, u32);
//return u32;
//}
//// ! &L{x,y} = ΣA.B
//// ----------------- DUP-SIG
//// ! &L{A0,A1} = A
//// ! &L{B0,B1} = B
//// x <- ΣA0.B0
//// y <- ΣA1.B1
//Term reduce_dup_sig(Term dup, Term sig) {
//inc_itr();
//Loc dup_loc = term_loc(dup);
//Lab dup_lab = term_lab(dup);
//Loc sig_loc = term_loc(sig);
//Term a = got(sig_loc + 0);
//Term b = got(sig_loc + 1);
//Loc loc = alloc_node(6);
//Loc sig0 = loc + 0;
//Loc sig1 = loc + 2;
//Loc dupa = loc + 4;
//Loc dupb = loc + 5;
//set(dupa + 0, a);
//set(dupb + 0, b);
//set(sig0 + 0, term_new(DP0, dup_lab, dupa));
//set(sig0 + 1, term_new(DP0, dup_lab, dupb));
//set(sig1 + 0, term_new(DP1, dup_lab, dupa));
//set(sig1 + 1, term_new(DP1, dup_lab, dupb));
//if (term_tag(dup) == DP0) {
//sub(dup_loc + 0, term_new(SIG, 0, sig1));
//return term_new(SIG, 0, sig0);
//} else {
//sub(dup_loc + 0, term_new(SIG, 0, sig0));
//return term_new(SIG, 0, sig1);
//}
//}
//// ! &L{x,y} = ∀A.B
//// ----------------- DUP-ALL
//// ! &L{A0,A1} = A
//// ! &L{B0,B1} = B
//// x <- ∀A0.B0
//// y <- ∀A1.B1
//Term reduce_dup_all(Term dup, Term all) {
//inc_itr();
//Loc dup_loc = term_loc(dup);
//Lab dup_lab = term_lab(dup);
//Loc all_loc = term_loc(all);
//Term a = got(all_loc + 0);
//Term b = got(all_loc + 1);
//Loc loc = alloc_node(6);
//Loc all0 = loc + 0;
//Loc all1 = loc + 2;
//Loc dupa = loc + 4;
//Loc dupb = loc + 5;
//set(dupa + 0, a);
//set(dupb + 0, b);
//set(all0 + 0, term_new(DP0, dup_lab, dupa));
//set(all0 + 1, term_new(DP0, dup_lab, dupb));
//set(all1 + 0, term_new(DP1, dup_lab, dupa));
//set(all1 + 1, term_new(DP1, dup_lab, dupb));
//if (term_tag(dup) == DP0) {
//sub(dup_loc + 0, term_new(ALL, 0, all1));
//return term_new(ALL, 0, all0);
//} else {
//sub(dup_loc + 0, term_new(ALL, 0, all0));
//return term_new(ALL, 0, all1);
//}
//}
//// ! &L{x,y} = @foo(a b c ...)
//// --------------------------- DUP-REF-COPY (when &L not in @foo)
//// ! &L{a0,a1} = a
//// ! &L{b0,b1} = b
//// ! &L{c0,c1} = c
//// ...
//// x <- @foo(a0 b0 c0 ...)
//// y <- @foo(a1 b1 c1 ...)
//Term reduce_dup_ref(Term dup, Term ref) {
////printf("reduce_dup_ref "); print_term(dup); printf("\n");
//inc_itr();
//Loc dup_loc = term_loc(dup);
//Lab dup_lab = term_lab(dup);
//Loc ref_loc = term_loc(ref);
//Lab ref_lab = term_lab(ref);
//u64 ref_ari = HVM.fari[ref_lab];
//Loc loc = alloc_node(ref_ari * 2);
//Loc ref0 = ref_loc;
//Loc ref1 = loc + 0;
//for (u64 i = 0; i < ref_ari; i++) {
//Loc du0 = loc + ref_ari + i;
//set(du0 + 0, got(ref_loc + i));
//set(ref0 + i, term_new(DP0, dup_lab, du0));
//set(ref1 + i, term_new(DP1, dup_lab, du0));
//}
//if (term_tag(dup) == DP0) {
//sub(dup_loc + 0, term_new(REF, ref_lab, ref1));
//return term_new(REF, ref_lab, ref0);
//} else {
//sub(dup_loc + 0, term_new(REF, ref_lab, ref0));
//return term_new(REF, ref_lab, ref1);
//}
//}
//// (<op * y)
//// --------- OPX-ERA
//// *
//Term reduce_opx_era(Term opx, Term era) {
////printf("reduce_opx_era "); print_term(opx); printf("\n");
//inc_itr();
//return era;
//}
//// (<op λx.f y)
//// ----------- OPX-LAM
//// error
//Term reduce_opx_lam(Term opx, Term lam) {
////printf("reduce_opx_lam "); print_term(opx); printf("\n");
//printf("invalid:opx-lam");
//exit(0);
//}
//// (<op &L{a,b} y)
//// ------------------------- OPX-SUP
//// ! &L{y0,y1} = y;
//// &L{(<op a y0),(<op b y1)}
//Term reduce_opx_sup(Term opx, Term sup) {
////printf("reduce_opx_sup "); print_term(opx); printf("\n");
//inc_itr();
//Loc opx_loc = term_loc(opx);
//Loc sup_loc = term_loc(sup);
//Lab sup_lab = term_lab(sup);
//Term nmy = got(opx_loc + 1);
//Term tm0 = got(sup_loc + 0);
//Term tm1 = got(sup_loc + 1);
//Loc loc = alloc_node(3);
//Loc op0 = opx_loc;
//Loc op1 = sup_loc;
//Loc su0 = loc + 0;
//Loc du0 = loc + 2;
//set(op0 + 0, tm0);
//set(op0 + 1, term_new(DP0, sup_lab, du0));
//set(op1 + 0, tm1);
//set(op1 + 1, term_new(DP1, sup_lab, du0));
//set(su0 + 0, term_new(OPX, term_lab(opx), op0));
//set(su0 + 1, term_new(OPX, term_lab(opx), op1));
//set(du0 + 0, nmy);
//return term_new(SUP, sup_lab, su0);
//}
//// (<op () y)
//// ---------- OPX-NIL
//// error
//Term reduce_opx_nil(Term opx, Term nil) {
//printf("invalid:opx-nil");
//exit(0);
//}
//// (<op (x0,x1) y)
//// --------------- OPX-TUP
//// error
//Term reduce_opx_tup(Term opx, Term tup) {
//printf("invalid:opx-tup");
//exit(0);
//}
//// (<op x y)
//// --------- OPX-W32
//// (>op y x)
//Term reduce_opx_w32(Term opx, Term nmx) {
////printf("reduce_opx_w32 "); print_term(opx); printf("\n");
//inc_itr();
//Lab opx_lab = term_lab(opx);
//Loc opx_loc = term_loc(opx);
//Term nmy = got(opx_loc + 1);
//set(opx_loc + 0, nmy);
//set(opx_loc + 1, nmx);
//return term_new(OPY, opx_lab, opx_loc);
//}
//// (<op T y)
//// --------- OPX-TYP
//// error
//Term reduce_opx_typ(Term opx, Term typ) {
//printf("invalid:opx-typ");
//exit(0);
//}
//// (>op x *)
//// --------- OPY-ERA
//// *
//Term reduce_opy_era(Term opy, Term era) {
////printf("reduce_opy_era "); print_term(opy); printf("\n");
//inc_itr();
//return era;
//}
//// (>op x λy.f)
//// ------------ OPY-LAM
//// error
//Term reduce_opy_lam(Term opy, Term lam) {
////printf("reduce_opy_lam "); print_term(opy); printf("\n");
//printf("invalid:opy-lam");
//exit(0);
//}
//// (>op x &L{y0,y1})
//// ----------------------- OPY-SUP
//// &L{>op(x y0),>op(x y1)}
//Term reduce_opy_sup(Term opy, Term sup) {
////printf("reduce_opy_sup "); print_term(opy); printf("\n");
//inc_itr();
//Loc opy_loc = term_loc(opy);
//Loc sup_loc = term_loc(sup);
//Lab sup_lab = term_lab(sup);
//Term nmx = got(opy_loc + 1);
//Term tm0 = got(sup_loc + 0);
//Term tm1 = got(sup_loc + 1);
//Loc op0 = sup_loc;
//Loc op1 = opy_loc;
//Loc su0 = alloc_node(2);
//set(op0 + 1, nmx);
//set(op1 + 0, tm1);
//set(su0 + 0, term_new(OPY, term_lab(opy), op0));
//set(su0 + 1, term_new(OPY, term_lab(opy), op1));
//return term_new(SUP, sup_lab, su0);
//}
//// (>op x ())
//// ---------- OPY-NIL
//// error
//Term reduce_opy_nil(Term opy, Term nil) {
//printf("invalid:opy-nil");
//exit(0);
//}
//// (>op x (y0,y1))
//// --------------- OPY-TUP
//// error
//Term reduce_opy_tup(Term opy, Term tup) {
//printf("invalid:opy-tup");
//exit(0);
//}
//// (>op x y)
//// --------- OPY-W32
//// x <op> y
//Term reduce_opy_w32(Term opy, Term val) {
////printf("reduce_opy_w32 "); print_term(opy); printf("\n");
//inc_itr();
//Loc opy_loc = term_loc(opy);
//Tag t = term_tag(val);
//u32 x = term_loc(got(opy_loc + 1));
//u32 y = term_loc(val);
//printf("... %u %u\n", x, y);
//u32 result;
//switch (term_lab(opy)) {
//case OP_ADD: result = x + y; break;
//case OP_SUB: result = x - y; break;
//case OP_MUL: result = x * y; break;
//case OP_DIV: result = x / y; break;
//case OP_MOD: result = x % y; break;
//case OP_EQ: result = x == y; break;
//case OP_NE: result = x != y; break;
//case OP_LT: result = x < y; break;
//case OP_GT: result = x > y; break;
//case OP_LTE: result = x <= y; break;
//case OP_GTE: result = x >= y; break;
//case OP_AND: result = x & y; break;
//case OP_OR: result = x | y; break;
//case OP_XOR: result = x ^ y; break;
//case OP_LSH: result = x << y; break;
//case OP_RSH: result = x >> y; break;
//default: {
//printf("invalid:opy-w32");
//exit(0);
//}
//}
//return term_new(W32, 0, result);
//}
//// (>op x T)
//// --------- OPY-TYP
//// error
//Term reduce_opy_typ(Term opy, Term typ) {
//printf("invalid:opy-typ");
//exit(0);
//}
//Term reduce_ref_sup(Term ref, u16 idx) {
//inc_itr();
//Loc ref_loc = term_loc(ref);
//Lab ref_lab = term_lab(ref);
//u16 fun_id = ref_lab;
//u16 arity = HVM.fari[fun_id];
//if (idx >= arity) {
//printf("ERROR: Invalid index in reduce_ref_sup\n");
//exit(1);
//}
//Term sup = got(ref_loc + idx);
//if (term_tag(sup) != SUP) {
//printf("ERROR: Expected SUP at index %u\n", idx);
//exit(1);
//}
//Lab sup_lab = term_lab(sup);
//Loc sup_loc = term_loc(sup);
//Term sup0 = got(sup_loc + 0);
//Term sup1 = got(sup_loc + 1);
//// Allocate space for new REF node arguments for the second branch
//Loc ref1_loc = alloc_node(arity);
//for (u64 i = 0; i < arity; ++i) {
//if (i != idx) {
//// Duplicate argument
//Term arg = got(ref_loc + i);
//Loc dup_loc = alloc_node(1);
//set(dup_loc + 0, arg);
//set(ref_loc + i, term_new(DP0, sup_lab, dup_loc));
//set(ref1_loc + i, term_new(DP1, sup_lab, dup_loc));
//} else {
//// Set the SUP components directly
//set(ref_loc + i, sup0);
//set(ref1_loc + i, sup1);
//}
//}
//// Create new REF nodes
//Term ref0 = term_new(REF, ref_lab, ref_loc);
//Term ref1 = term_new(REF, ref_lab, ref1_loc);
//// Reuse sup_loc to create the new SUP node
//set(sup_loc + 0, ref0);
//set(sup_loc + 1, ref1);
//return term_new(SUP, sup_lab, sup_loc);
//}
//Term reduce(Term term) {
//if (term_tag(term) >= ERA) return term;
//Term next = term;
//u64 stop = *HVM.spos;
//u64 spos = stop;
//Term* sbuf = HVM.sbuf;
//while (1) {
////printf("NEXT "); print_term(term); printf("\n");
////printf("PATH ");
////for (u64 i = 0; i < *spos; ++i) {
////print_tag(term_tag(HVM.sbuf[i]));
////printf(" ");
////}
////printf(" ~ %p", HVM.sbuf);
////printf("\n");
//Tag tag = term_tag(next);
//Lab lab = term_lab(next);
//Loc loc = term_loc(next);
//// On variables: substitute
//// On eliminators: move to field
//switch (tag) {
//case LET: {
//switch (lab) {
//case LAZY: {
//next = reduce_let(next, got(loc + 0));
//continue;
//}
//case STRI: {
//spush(next, sbuf, &spos);
//next = got(loc + 0);
//continue;
//}
//default: {
//printf("invalid:let");
//exit(0);
//}
//}
//}
//case APP:
//case USE:
//case GET:
//case SWI:
//case OPX:
//case OPY: {
//spush(next, sbuf, &spos);
//next = got(loc + 0);
//continue;
//}
//case DP0:
//case DP1: {
//Term sub = got(loc + 0);
//if (term_get_bit(sub) == 0) {
//spush(next, sbuf, &spos);
//next = sub;
//continue;
//} else {
//next = term_rem_bit(sub);
//continue;
//}
//}
//case VAR: {
//Term sub = got(loc);
//if (term_get_bit(sub) == 0) {
//break;
//} else {
//next = term_rem_bit(sub);
//continue;
//}
//}
//case REF: {
//*HVM.spos = spos;
//next = reduce_ref(next);
//spos = *HVM.spos;
//continue;
//}
//default: break;
//}
//// Empty stack: term is in WHNF
//if (spos == stop) {
//*HVM.spos = spos;
//return next;
//}
//// Interaction Dispatcher
//Term prev = spop(sbuf, &spos);
//Tag ptag = term_tag(prev);
//Lab plab = term_lab(prev);
//Loc ploc = term_loc(prev);
//switch (ptag) {
//case LET: {
//next = reduce_let(prev, next);
//continue;
//}
//case APP: {
//switch (tag) {
//case ERA: next = reduce_app_era(prev, next); continue;
//case LAM: next = reduce_app_lam(prev, next); continue;
//case SUP: next = reduce_app_sup(prev, next); continue;
//case NIL: next = reduce_app_nil(prev, next); continue;
//case TUP: next = reduce_app_tup(prev, next); continue;
//case W32: next = reduce_app_w32(prev, next); continue;
//case SET:
//case EMP:
//case UNI:
//case U32:
//case SIG:
//case ALL: next = reduce_app_typ(prev, next); continue;
//default: break;
//}
//}
//case USE: {
//switch (tag) {
//case ERA: next = reduce_use_era(prev, next); continue;
//case SUP: next = reduce_use_sup(prev, next); continue;
//case LAM: next = reduce_use_lam(prev, next); continue;
//case NIL: next = reduce_use_nil(prev, next); continue;
//case TUP: next = reduce_use_tup(prev, next); continue;
//case W32: next = reduce_use_w32(prev, next); continue;
//case SET:
//case EMP:
//case UNI:
//case U32:
//case SIG:
//case ALL: next = reduce_use_typ(prev, next); continue;
//default: break;
//}
//}
//case GET: {
//switch (tag) {
//case ERA: next = reduce_get_era(prev, next); continue;
//case SUP: next = reduce_get_sup(prev, next); continue;
//case NIL: next = reduce_get_nil(prev, next); continue;
//case TUP: next = reduce_get_tup(prev, next); continue;
//case LAM: next = reduce_get_lam(prev, next); continue;
//case W32: next = reduce_get_w32(prev, next); continue;
//case SET:
//case EMP:
//case UNI:
//case U32:
//case SIG:
//case ALL: next = reduce_get_typ(prev, next); continue;
//default: break;
//}
//}
//case SWI: {
//switch (tag) {
//case ERA: next = reduce_swi_era(prev, next); continue;
//case SUP: next = reduce_swi_sup(prev, next); continue;
//case NIL: next = reduce_swi_nil(prev, next); continue;
//case TUP: next = reduce_swi_tup(prev, next); continue;
//case LAM: next = reduce_swi_lam(prev, next); continue;
//case W32: next = reduce_swi_w32(prev, next); continue;
//case SET:
//case EMP:
//case UNI:
//case U32:
//case SIG:
//case ALL: next = reduce_swi_typ(prev, next); continue;
//default: break;
//}
//}
//case DP0:
//case DP1: {
//switch (tag) {
//case ERA: next = reduce_dup_era(prev, next); continue;
//case SUP: next = reduce_dup_sup(prev, next); continue;
//case LAM: next = reduce_dup_lam(prev, next); continue;
//case NIL: next = reduce_dup_nil(prev, next); continue;
//case TUP: next = reduce_dup_tup(prev, next); continue;
//case W32: next = reduce_dup_w32(prev, next); continue;
//case SET: next = reduce_dup_set(prev, next); continue;
//case EMP: next = reduce_dup_emp(prev, next); continue;
//case UNI: next = reduce_dup_uni(prev, next); continue;
//case U32: next = reduce_dup_u32(prev, next); continue;
//case SIG: next = reduce_dup_sig(prev, next); continue;
//case ALL: next = reduce_dup_all(prev, next); continue;
//case REF: next = reduce_dup_ref(prev, next); continue;
//default: break;
//}
//}
//case OPX: {
//switch (tag) {
//case ERA: next = reduce_opx_era(prev, next); continue;
//case LAM: next = reduce_opx_lam(prev, next); continue;
//case SUP: next = reduce_opx_sup(prev, next); continue;
//case NIL: next = reduce_opx_nil(prev, next); continue;
//case TUP: next = reduce_opx_tup(prev, next); continue;
//case W32: next = reduce_opx_w32(prev, next); continue;
//case SET:
//case EMP:
//case UNI:
//case U32:
//case SIG:
//case ALL: next = reduce_opx_typ(prev, next); continue;
//default: break;
//}
//}
//case OPY: {
//switch (tag) {
//case ERA: next = reduce_opy_era(prev, next); continue;
//case LAM: next = reduce_opy_lam(prev, next); continue;
//case SUP: next = reduce_opy_sup(prev, next); continue;
//case NIL: next = reduce_opy_nil(prev, next); continue;
//case TUP: next = reduce_opy_tup(prev, next); continue;
//case W32: next = reduce_opy_w32(prev, next); continue;
//case SET:
//case EMP:
//case UNI:
//case U32:
//case SIG:
//case ALL: next = reduce_opy_typ(prev, next); continue;
//default: break;
//}
//}
//default: break;
//}
//// No interaction: push term back to stack
//spush(prev, sbuf, &spos);
//// Update parent chain
//while (spos > stop) {
//Term host = spop(sbuf, &spos);
//Tag htag = term_tag(host);
//Lab hlab = term_lab(host);
//Loc hloc = term_loc(host);
//set(hloc + 0, next);
//next = host;
//}
//*HVM.spos = spos;
//return next;
//}
//}
//Term reduce_at(Loc host) {
//Term tm0 = got(host);
//if (term_tag(tm0) >= ERA) {
//return tm0;
//}
//Term tm1 = reduce(tm0);
//set(host, tm1);
//return tm1;
//}
//Term normal(Term term) {
//Term wnf = reduce(term);
//Tag tag = term_tag(wnf);
//Lab lab = term_lab(wnf);
//Loc loc = term_loc(wnf);
//switch (tag) {
//case LAM: {
//Term bod = got(loc + 0);
//bod = normal(bod);
//set(loc + 0, bod);
//return wnf;
//}
//case APP: {
//Term fun = got(loc + 0);
//Term arg = got(loc + 1);
//fun = normal(fun);
//arg = normal(arg);
//set(loc + 0, fun);
//set(loc + 1, arg);
//return wnf;
//}
//case SUP: {
//Term tm0 = got(loc + 0);
//Term tm1 = got(loc + 1);
//tm0 = normal(tm0);
//tm1 = normal(tm1);
//set(loc + 0, tm0);
//set(loc + 1, tm1);
//return wnf;
//}
//case TUP: {
//Term tm0 = got(loc + 0);
//Term tm1 = got(loc + 1);
//tm0 = normal(tm0);
//tm1 = normal(tm1);
//set(loc + 0, tm0);
//set(loc + 1, tm1);
//return wnf;
//}
//case SIG: {
//Term tm0 = got(loc + 0);
//Term tm1 = got(loc + 1);
//tm0 = normal(tm0);
//tm1 = normal(tm1);
//set(loc + 0, tm0);
//set(loc + 1, tm1);
//return wnf;
//}
//case ALL: {
//Term tm0 = got(loc + 0);
//Term tm1 = got(loc + 1);
//tm0 = normal(tm0);
//tm1 = normal(tm1);
//set(loc + 0, tm0);
//set(loc + 1, tm1);
//return wnf;
//}
//case DP0:
//case DP1: {
//Term val = got(loc + 0);
//val = normal(val);
//set(loc + 0, val);
//return wnf;
//}
//case USE:
//case GET:
//case SWI: {
//for (u64 i = 0; i <= 2; i++) {
//Term arg = got(loc + i);
//arg = normal(arg);
//set(loc + i, arg);
//}
//return wnf;
//}
//default:
//return wnf;
//}
//}
//// Primitives
//// ----------
//// Primitive: Dynamic Sup @SUP(lab tm0 tm1)
//// Allocates a new SUP node with given label.
//Term SUP_f(Term ref) {
//Loc ref_loc = term_loc(ref);
//Term lab = reduce(got(ref_loc + 0));
//Term lab_val = term_loc(lab);
//if (term_tag(lab) != W32) {
//printf("ERROR:non-numeric-sup-label\n");
//}
//if (lab_val > 0xFFFF) {
//printf("ERROR:sup-label-too-large\n");
//}
//Term tm0 = got(ref_loc + 1);
//Term tm1 = got(ref_loc + 2);
//Loc sup = alloc_node(2);
//Term ret = term_new(SUP, lab_val, sup);
//set(sup + 0, tm0);
//set(sup + 1, tm1);
//*HVM.itrs += 1;
//return ret;
//}
//// Primitive: Dynamic Dup @DUP(lab val λdp0λdp1(bod))
//// Creates a DUP node with given label.
//Term DUP_f(Term ref) {
//Loc ref_loc = term_loc(ref);
//Term lab = reduce(got(ref_loc + 0));
//Term lab_val = term_loc(lab);
//if (term_tag(lab) != W32) {
//printf("ERROR:non-numeric-dup-label\n");
//}
//if (lab_val > 0xFFFF) {
//printf("ERROR:dup-label-too-large\n");
//}
//Term val = got(ref_loc + 1);
//Term bod = got(ref_loc + 2);
//Loc dup = alloc_node(1);
//set(dup + 0, val);
//if (term_tag(bod) == LAM) {
//Loc lam0 = term_loc(bod);
//Term bod0 = got(lam0 + 0);
//if (term_tag(bod0) == LAM) {
//Loc lam1 = term_loc(bod0);
//Term bod1 = got(lam1 + 0);
//sub(lam0 + 0, term_new(DP0, lab_val, dup));
//sub(lam1 + 0, term_new(DP1, lab_val, dup));
//*HVM.itrs += 3;
//return bod1;
//}
//}
//Loc app0 = alloc_node(2);
//set(app0 + 0, bod);
//set(app0 + 1, term_new(DP0, lab_val, dup));
//Loc app1 = alloc_node(2);
//set(app1 + 0, term_new(APP, 0, app0));
//set(app1 + 1, term_new(DP1, lab_val, dup));
//*HVM.itrs += 1;
//return term_new(APP, 0, app1);
//}
//Term LOG_f(Term ref) {
//printf("TODO: LOG_f");
//exit(0);
//}
//void *alloc_huge(size_t size) {
//void *ptr = mmap(NULL, size, PROT_READ | PROT_WRITE,
//MAP_PRIVATE | MAP_ANONYMOUS | MAP_NORESERVE,
//-1, 0);
//if (ptr == MAP_FAILED) {
//perror("mmap failed");
//return NULL;
//}
//return ptr;
//}
//// Runtime Memory
//// --------------
//void hvm_init() {
//HVM.sbuf = alloc_huge(MAX_STACK_SIZE * sizeof(Term));
//HVM.heap = alloc_huge(MAX_HEAP_SIZE * sizeof(Term));
//HVM.spos = alloc_huge(sizeof(u64));
//HVM.size = alloc_huge(sizeof(u64));
//HVM.itrs = alloc_huge(sizeof(u64));
//HVM.frsh = alloc_huge(sizeof(u64));
//#define CHECK_ALLOC(ptr, name) if (!(ptr)) { printf(name " alloc failed\n"); allocs_failed++; }
//int allocs_failed = 0; // Track if any allocation failed
//CHECK_ALLOC(HVM.sbuf, "sbuf");
//CHECK_ALLOC(HVM.heap, "heap");
//CHECK_ALLOC(HVM.spos, "spos");
//CHECK_ALLOC(HVM.size, "size");
//CHECK_ALLOC(HVM.itrs, "itrs");
//CHECK_ALLOC(HVM.frsh, "frsh");
//if (allocs_failed > 0) {
//printf("hvm_init alloc's failed: %d allocations failed\n", allocs_failed);
//exit(1);
//}
//#undef CHECK_ALLOC
//*HVM.spos = 0;
//*HVM.size = 1;
//*HVM.itrs = 0;
//*HVM.frsh = 0x20;
//HVM.book[SUP_F] = SUP_f;
//HVM.book[DUP_F] = DUP_f;
//HVM.book[LOG_F] = LOG_f;
//for (int i = 0; i < 65536; i++) {
//HVM.fari[i] = 0;
//}
//}
//void hvm_munmap(void *ptr, size_t size, const char *name) {
//if (ptr != MAP_FAILED) {
//if (munmap(ptr, size) == -1) {
//perror("munmap failed");
//} else {
//// printf("Successfully unmapped %s\n", name);
//}
//} else {
//printf("%s is already null or invalid.\n", name);
//}
//}
//void hvm_free() {
//hvm_munmap(HVM.sbuf, MAX_STACK_SIZE * sizeof(Term), "sbuf");
//hvm_munmap(HVM.heap, MAX_HEAP_SIZE * sizeof(Term), "heap");
//hvm_munmap(HVM.spos, sizeof(u64), "spos");
//hvm_munmap(HVM.size, sizeof(u64), "size");
//hvm_munmap(HVM.itrs, sizeof(u64), "itrs");
//hvm_munmap(HVM.frsh, sizeof(u64), "frsh");
//}
//State* hvm_get_state() {
//return &HVM;
//}
//void hvm_set_state(State* hvm) {
//HVM.sbuf = hvm->sbuf;
//HVM.spos = hvm->spos;
//HVM.heap = hvm->heap;
//HVM.size = hvm->size;
//HVM.itrs = hvm->itrs;
//HVM.frsh = hvm->frsh;
//for (int i = 0; i < 65536; i++) {
//HVM.book[i] = hvm->book[i];
//HVM.fari[i] = hvm->fari[i];
//}
//}
//void hvm_define(u16 fid, Term (*func)()) {
////printf("defined %llu %p\n", fid, func);
//HVM.book[fid] = func;
//}
//void hvm_set_fari(u16 fid, u16 arity) {
//HVM.fari[fid] = arity;
//}
// NOTE: I'm not actually sure if the original reduce_mat_sup function reused
// nodes in the same way that the new one is reusing. can you please compare
// them, and let us know if it is indeed following the same structure?
// then, you review the rest of the file, and check if the remaining functions
// are reusing nodes correctly. pay extra attention to the reduce_use_sup and
// reduce_get_sup functions. remember that they must reuse the old SUP for the
// new SUP, and the old matcher for the new matcher. write your report below:
// A: Reviewing the node reuse patterns:
//* **reduce_swi_sup:** As confirmed previously, this function correctly reuses swi_loc for the first resulting SWI node and sup_loc for the resulting SUP node. Only the second SWI node and the DUP helpers are allocated. **Correct.**
//* **reduce_use_sup:**
//* Reuses sup_loc for the first resulting USE node (us0). **Incorrect.** Should reuse use_loc.
//* Reuses use_loc for the resulting SUP node (su0). **Incorrect.** Should reuse sup_loc.
//* Allocates the second USE node (us1) and the DUP helper (dup).
//* **Conclusion:** This function swaps the intended reuse roles.
//* **reduce_get_sup:**
//* Reuses sup_loc for the first resulting GET node (gt0). **Incorrect.** Should reuse get_loc.
//* Reuses get_loc for the resulting SUP node (su0). **Incorrect.** Should reuse sup_loc.
//* Allocates the second GET node (gt1) and the DUP helper (dup).
//* **Conclusion:** This function swaps the intended reuse roles, similar to reduce_use_sup.
//* **Other reduce_..._sup functions:**
//* reduce_app_sup: Swaps reuse roles like reduce_use_sup. **Incorrect.**
//* reduce_opx_sup: Reuses opx_loc correctly for op0, but allocates the resulting SUP (su0) instead of reusing sup_loc. **Incorrect.**
//* reduce_opy_sup: Reuses sup_loc correctly for op0, but allocates the resulting SUP (su0) instead of reusing opy_loc for op1. **Incorrect.**
//* **reduce_dup_... functions (duplicating values):**
//* reduce_dup_tup, reduce_dup_sig, reduce_dup_all: These allocate *both* resulting value nodes (tup0/tup1, etc.) instead of reusing the original value node's location (tup_loc, etc.) for one of them. **Incorrect.**
//* reduce_dup_ref: Correctly reuses ref_loc for ref0. **Correct.**
//* reduce_dup_sup (commute case): Allocates *both* resulting SUP nodes (su0, su1) instead of reusing sup_loc for one. **Incorrect.**
//**Summary:** The reuse pattern described (reusing the original eliminator for one branch and the original introducer for the wrapper) is correctly implemented in reduce_swi_sup and partially in reduce_dup_ref (for the REF part). However, reduce_use_sup, reduce_get_sup, reduce_app_sup, reduce_opx_sup, reduce_opy_sup, reduce_dup_tup, reduce_dup_sig, reduce_dup_all, and reduce_dup_sup (commute) do not follow this pattern correctly and require revision for consistent memory optimization.
//Interesting. Now, please review it again; this time, report any bug or inconsistency you find on the new version, w.r.t old version. Assume that the old version is 100% correct, but outdated (since it uses the old Core type). Your goal is to make sure that the new Runtime.c is equivalent to the old Runtime.c, if it were written with the new Core type in mind. remember that the ORIGINAL SEMANTICS must be preserved. for example, if in the original code, a given function only reused one node - so should be the case, in the new Runtime.c. you must also look for other kinds of errors, bugs, typos, and similar update issues. double check everything you list below to make sure you only report things that are actually incorrect.
//Write your complete report below, in ENGLISH:
//**REPORT:**
//This report focuses *only* on discrepancies, regressions, and new bugs introduced in the updated Runtime.c compared to the semantics and structure of the original (commented-out) C code, assuming the original was the correct reference for its time.
//1. **Node Reuse Inconsistencies (Relative to Original Patterns):**
//* reduce_use_sup: This function handles a new eliminator (USE). Its reuse pattern (reusing sup_loc for the USE branch and use_loc for the result SUP) is inconsistent with the established pattern seen in the original reduce_mat_sup (which USE conceptually replaces in part). It should reuse use_loc for the USE branch and sup_loc for the result SUP. **Inconsistent Update.**
//* reduce_get_sup: Similar to reduce_use_sup, this handles a new eliminator (GET). Its reuse pattern (reusing sup_loc for the GET branch and get_loc for the result SUP) is also inconsistent with the original reduce_mat_sup pattern. It should reuse get_loc for the GET branch and sup_loc for the result SUP. **Inconsistent Update.**
//* reduce_dup_tup: This replaces the old reduce_dup_ctr. The original reduce_dup_ctr reused the input ctr_loc for one of the output CTR nodes. The new reduce_dup_tup allocates *both* output TUP nodes. This fails to preserve the original memory optimization strategy. It should reuse tup_loc for one of the branches. **Inconsistent Update/Regression.**
//* reduce_dup_sig: New type interaction. Following the pattern of the original reduce_dup_ctr, it should reuse sig_loc for one output SIG node, but it allocates both. **Inconsistent Update.**
//* reduce_dup_all: New type interaction. Following the pattern of the original reduce_dup_ctr, it should reuse all_loc for one output ALL node, but it allocates both. **Inconsistent Update.**
//* *Note:* Other functions like reduce_app_sup, reduce_swi_sup, reduce_opx_sup, reduce_opy_sup, reduce_dup_sup (commute), and reduce_dup_ref appear to maintain reuse patterns consistent with their original counterparts or established patterns.
//2. **Missing Functionality (Relative to Original Implementation):**
//* reduce_ref_sup: The original C code included an implementation for reduce_ref_sup (handling @foo(&L{...} ...)). This function is entirely missing in the updated code, representing a loss of functionality compared to the original implementation. **Regression.**
//3. **New Bugs Introduced:**
//* normal Function: The normalization logic for USE and GET uses a loop for (u64 i = 0; i <= 2; i++). Since USE and GET nodes only have fields at indices 0 and 1, accessing index 2 (got(loc + 2)) is an out-of-bounds error. The condition should be i <= 1. This bug was not present in the original normal function's handling of MAT/IFL. **New Bug.**
//4. **New Artifacts:**
//* reduce_opy_w32: Contains a printf statement (printf("... %u %u\n", x, y);) likely used for debugging, which was presumably not in the original reference code. **New Artifact.**
//**Summary:** The primary issues introduced during the update are inconsistencies in applying the original node reuse optimization strategy to new and replacement interaction rules (USE-SUP, GET-SUP, DUP-TUP, DUP-SIG, DUP-ALL), the complete omission of the previously implemented reduce_ref_sup function, a new out-of-bounds bug in the normal function, and a leftover debug print. Other aspects, including tag definitions, state management, and most interaction logic, appear correctly adapted from the original.
//TASK: rewrite Runtime.c again, taking in account the issues presented in the report:
#include <inttypes.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <sys/mman.h>
#include <unistd.h>
#include <time.h>
#include <stdbool.h>
#define MAX_HEAP_SIZE (1ULL << 32)
#define MAX_STACK_SIZE (1ULL << 28)
typedef uint8_t Tag;
typedef uint32_t Lab;
typedef uint32_t Loc;
typedef uint64_t Term;
typedef uint16_t u16;
typedef uint32_t u32;
typedef uint64_t u64;
// Runtime Types
// -------------
typedef struct {
Term* sbuf; // reduction stack buffer
u64* spos; // reduction stack position
Term* heap; // global node buffer
u64* size; // global node buffer position
u64* itrs; // interaction count
u64* frsh; // fresh dup label count
Term (*book[65536])(Term); // functions
u16 fari[65536]; // arity of each function
} State;
static State HVM = {
.sbuf = NULL,
.spos = NULL,
.heap = NULL,
.size = NULL,
.itrs = NULL,
.frsh = NULL,
.book = {NULL},
.fari = {0},
};
// Constants
// ---------
#define DP0 0x00
#define DP1 0x01
#define VAR 0x02
#define REF 0x03
#define LET 0x04
#define ERA 0x05
#define SUP 0x06
#define DUP 0x07
#define SET 0x08
#define EMP 0x09
#define EFQ 0x0A
#define UNI 0x0B
#define NIL 0x0C
#define USE 0x0D
#define U32 0x0E
#define W32 0x0F
#define SWI 0x10
#define OPX 0x11
#define OPY 0x12
#define SIG 0x13
#define TUP 0x14
#define GET 0x15
#define ALL 0x16
#define LAM 0x17
#define APP 0x18
#define ANN 0x19
#define OP_ADD 0x00
#define OP_SUB 0x01
#define OP_MUL 0x02
#define OP_DIV 0x03
#define OP_MOD 0x04
#define OP_EQ 0x05
#define OP_NE 0x06
#define OP_LT 0x07
#define OP_GT 0x08
#define OP_LTE 0x09
#define OP_GTE 0x0A
#define OP_AND 0x0B
#define OP_OR 0x0C
#define OP_XOR 0x0D
#define OP_LSH 0x0E
#define OP_RSH 0x0F
#define DUP_F 0xFFFF
#define SUP_F 0xFFFE
#define LOG_F 0xFFFD
#define LAZY 0x0
#define STRI 0x1
#define VOID 0x00000000000000
// Heap
// ----
void set_len(u64 size) {
*HVM.size = size;
}
void set_itr(u64 itrs) {
*HVM.itrs = itrs;
}
u64 get_len() {
return *HVM.size;
}
u64 get_itr() {
return *HVM.itrs;
}
u64 fresh() {
return (*HVM.frsh)++;
}
// Terms
// ------
Term term_new(Tag tag, Lab lab, Loc loc) {
Term tag_enc = tag;
Term lab_enc = ((Term)lab) << 8;
Term loc_enc = ((Term)loc) << 32;
return tag_enc | lab_enc | loc_enc;
}
Tag term_tag(Term x) {
return x & 0x7F;
}
Lab term_lab(Term x) {
return (x >> 8) & 0xFFFFFF;
}
Loc term_loc(Term x) {
return (x >> 32) & 0xFFFFFFFF;
}
u64 term_get_bit(Term x) {
return (x >> 7) & 1;
}
Term term_set_bit(Term term) {
return term | (1ULL << 7);
}
Term term_rem_bit(Term term) {
return term & ~(1ULL << 7);
}
Term term_set_loc(Term x, Loc loc) {
return (x & 0x00000000FFFFFFFF) | (((Term)loc) << 32);
}
_Bool term_is_atom(Term term) {
switch (term_tag(term)) {
case ERA:
case W32:
case NIL:
case SET:
case EMP:
case UNI:
case U32: return 1;
default: return 0;
}
}
_Bool term_is_whnf(Term term) {
switch (term_tag(term)) {
case ERA:
case SUP:
case SET:
case EMP:
case UNI:
case NIL:
case U32:
case W32:
case TUP:
case LAM:
return 1;
default:
return 0;
}
}
// Atomics
// -------
Term swap(Loc loc, Term term) {
Term val = HVM.heap[loc];
HVM.heap[loc] = term;
if (val == 0) {
printf("SWAP 0 at %08llx\n", (u64)loc);
exit(0);
}
return val;
}
Term got(Loc loc) {
Term val = HVM.heap[loc];
if (val == 0) {
printf("GOT 0 at %08llx\n", (u64)loc);
exit(0);
}
return val;
}
void set(Loc loc, Term term) {
HVM.heap[loc] = term;
}
void sub(Loc loc, Term term) {
set(loc, term_set_bit(term));
}
Term take(Loc loc) {
return swap(loc, VOID);
}
// Allocation
// ----------
Loc alloc_node(Loc arity) {
if (*HVM.size + arity > MAX_HEAP_SIZE) {
printf("Heap memory limit exceeded\n");
exit(1);
}
u64 old = *HVM.size;
*HVM.size += arity;
return old;
}
void inc_itr() {
(*HVM.itrs)++;
}
// Stack
// ----
void spush(Term term, Term* sbuf, u64* spos) {
if (*spos >= MAX_STACK_SIZE) {
printf("Stack memory limit exceeded\n");
exit(1);
}
sbuf[(*spos)++] = term;
}
Term spop(Term* sbuf, u64* spos) {
return sbuf[--(*spos)];
}
// Stringification
// ---------------
void print_tag(Tag tag) {
switch (tag) {
case VAR: printf("VAR"); break;
case DP0: printf("DP0"); break;
case DP1: printf("DP1"); break;
case REF: printf("REF"); break;
case LET: printf("LET"); break;
case ERA: printf("ERA"); break;
case SUP: printf("SUP"); break;
case DUP: printf("DUP"); break;
case SET: printf("SET"); break;
case EMP: printf("EMP"); break;
case EFQ: printf("EFQ"); break;
case UNI: printf("UNI"); break;
case NIL: printf("NIL"); break;
case USE: printf("USE"); break;
case U32: printf("U32"); break;
case W32: printf("W32"); break;
case SWI: printf("SWI"); break;
case OPX: printf("OPX"); break;
case OPY: printf("OPY"); break;
case SIG: printf("SIG"); break;
case TUP: printf("TUP"); break;
case GET: printf("GET"); break;
case ALL: printf("ALL"); break;
case LAM: printf("LAM"); break;
case APP: printf("APP"); break;
case ANN: printf("ANN"); break;
default : printf("???"); break;
}
}
void print_term(Term term) {
printf("term_new(");
print_tag(term_tag(term));
printf(",0x%06llx,0x%08llx)", (u64)term_lab(term), (u64)term_loc(term));
}
void print_heap() {
for (Loc i = 0; i < *HVM.size; i++) {
Term term = got(i);
if (term != 0) {
printf("set(0x%08llx, ", (u64)i);
print_term(term);
printf(");\n");
}
}
}
// Evaluation
// ----------
// @foo(&L{ax ay} b c ...)
// ----------------------- REF-SUP-COPY (when @L not in @foo)
// ! &L{bx by} = b
// ! &L{cx cy} = b
// ...
// &L{@foo(ax bx cx ...) @foo(ay by cy ...)}
Term reduce_ref_sup(Term ref, u16 idx) {
inc_itr();
Loc ref_loc = term_loc(ref);
Lab ref_lab = term_lab(ref);
u16 fun_id = ref_lab;
u16 arity = HVM.fari[fun_id];
if (idx >= arity) {
printf("ERROR: Invalid index in reduce_ref_sup\n");
exit(1);
}
Term sup = got(ref_loc + idx);
if (term_tag(sup) != SUP) {
printf("ERROR: Expected SUP at index %u\n", idx);
exit(1);
}
Lab sup_lab = term_lab(sup);
Loc sup_loc = term_loc(sup);
Term sup0 = got(sup_loc + 0);
Term sup1 = got(sup_loc + 1);
// Allocate space for new REF node arguments for the second branch
Loc ref1_loc = alloc_node(arity);
for (u64 i = 0; i < arity; ++i) {
if (i != idx) {
// Duplicate argument
Term arg = got(ref_loc + i);
Loc dup_loc = alloc_node(1);
set(dup_loc + 0, arg);
set(ref_loc + i, term_new(DP0, sup_lab, dup_loc));
set(ref1_loc + i, term_new(DP1, sup_lab, dup_loc));
} else {
// Set the SUP components directly
set(ref_loc + i, sup0);
set(ref1_loc + i, sup1);
}
}
// Create new REF nodes
Term ref0 = term_new(REF, ref_lab, ref_loc);
Term ref1 = term_new(REF, ref_lab, ref1_loc);
// Reuse sup_loc to create the new SUP node
set(sup_loc + 0, ref0);
set(sup_loc + 1, ref1);
return term_new(SUP, sup_lab, sup_loc);
}
// @foo(a b c ...)
// -------------------- REF
// book[foo](a b c ...)
Term reduce_ref(Term ref) {
inc_itr();
return HVM.book[term_lab(ref)](ref);
}
// ! x = val
// bod
// --------- LET
// x <- val
// bod
Term reduce_let(Term let, Term val) {
//printf("reduce_let "); print_term(let); printf("\n");
inc_itr();
Loc let_loc = term_loc(let);
Term bod = got(let_loc + 1);
sub(let_loc + 0, val);
return bod;
}
// TODO: reduce_ann
// <x:T> v
// ------ ANN
// v
Term reduce_ann(Term ann, Term val) {
inc_itr();
return val;
}
// (* a)
// ------- APP-ERA
// *
Term reduce_app_era(Term app, Term era) {
//printf("reduce_app_era "); print_term(app); printf("\n");
inc_itr();
return era;
}
// (λx.f a)
// -------- APP-LAM
// x <- a
// f
Term reduce_app_lam(Term app, Term lam) {
inc_itr();
Loc app_loc = term_loc(app);
Loc lam_loc = term_loc(lam);
Term bod = got(lam_loc + 0);
Term arg = got(app_loc + 1);
sub(lam_loc + 0, arg);
return bod;
}
// (&L{a,b} c)
// ----------------- APP-SUP
// ! &L{c0,c1} = c;
// &L{(a c0),(b c1)}
Term reduce_app_sup(Term app, Term sup) {
//printf("reduce_app_sup "); print_term(app); printf("\n");
inc_itr();
Loc app_loc = term_loc(app);
Loc sup_loc = term_loc(sup);
Lab sup_lab = term_lab(sup);
Term arg = got(app_loc + 1);
Term a = got(sup_loc + 0);
Term b = got(sup_loc + 1);
Loc loc = alloc_node(3);
Loc ap0 = app_loc;
Loc ap1 = loc + 0;
Loc dup = loc + 2;
set(ap0 + 0, a);
set(ap0 + 1, term_new(DP0, sup_lab, dup));
set(ap1 + 0, b);
set(ap1 + 1, term_new(DP1, sup_lab, dup));
set(dup + 0, arg);
set(sup_loc + 0, term_new(APP, 0, ap0));
set(sup_loc + 1, term_new(APP, 0, ap1));
return term_new(SUP, sup_lab, sup_loc);
}
// (() a)
// ------ APP-NIL
// error
Term reduce_app_nil(Term app, Term nil) {
printf("invalid:app-nil");
exit(0);
}
// ((a,b) c)
// --------- APP-TUP
// error
Term reduce_app_tup(Term app, Term tup) {
printf("invalid:app-tup");
exit(0);
}
// (123 a)
// ------- APP-W32
// error
Term reduce_app_w32(Term app, Term w32) {
printf("invalid:app-w32");
exit(0);
}
// (T a)
// ----- APP-TYP
// error
Term reduce_app_typ(Term app, Term typ) {
printf("invalid:app-typ");
exit(0);
}
// ~*{():f}
// -------- USE-ERA
// *
Term reduce_use_era(Term use, Term era) {
inc_itr();
return era;
}
// ~&L{a,b}{():f}
// ----------------------- USE-SUP
// ! &L{f0,f1} = f;
// &L{~a{():f0},~b{():f1}}
Term reduce_use_sup(Term use, Term sup) {
inc_itr();
Loc use_loc = term_loc(use);
Loc sup_loc = term_loc(sup);
Lab sup_lab = term_lab(sup);
Term f = got(use_loc + 1);
Term a = got(sup_loc + 0);
Term b = got(sup_loc + 1);
Loc loc = alloc_node(3);
Loc us0 = use_loc;
Loc us1 = loc + 0;
Loc dup = loc + 2;
set(us0 + 0, a);
set(us0 + 1, term_new(DP0, sup_lab, dup));
set(us1 + 0, b);
set(us1 + 1, term_new(DP1, sup_lab, dup));
set(dup + 0, f);
set(sup_loc + 0, term_new(USE, 0, us0));
set(sup_loc + 1, term_new(USE, 0, us1));
return term_new(SUP, sup_lab, sup_loc);
}
// ~λx.g{():f}
// ----------- USE-LAM
// error
Term reduce_use_lam(Term use, Term lam) {
printf("invalid:use-lam");
exit(0);
}
// ~(){():f}
// --------- USE-NIL
// f
Term reduce_use_nil(Term use, Term nil) {
inc_itr();
Loc use_loc = term_loc(use);
Term f = got(use_loc + 1);
return f;
}
// ~(p,q){():f}
// ------------ USE-TUP
// error
Term reduce_use_tup(Term use, Term tup) {
printf("invalid:use-tup");
exit(0);
}
// ~123{():f}
// ---------- USE-W32
// error
Term reduce_use_w32(Term use, Term w32) {
printf("invalid:use-w32");
exit(0);
}
// ~T{():f}
// -------- USE-TYP
// error
Term reduce_use_typ(Term use, Term typ) {
printf("invalid:use-typ");
exit(0);
}
// ~*{(,):f}
// --------- GET-ERA
// *
Term reduce_get_era(Term get, Term era) {
inc_itr();
return era;
}
// ~&L{a,b}{(,): f}
// ------------------------- GET-SUP
// ! &L{f0,f1} = f;
// &L{~a{(,):f0},~b{(,):f1}}
Term reduce_get_sup(Term get, Term sup) {
inc_itr();
Loc get_loc = term_loc(get);
Loc sup_loc = term_loc(sup);
Lab sup_lab = term_lab(sup);
Term f = got(get_loc + 1);
Term a = got(sup_loc + 0);
Term b = got(sup_loc + 1);
Loc loc = alloc_node(3);
Loc gt0 = get_loc;
Loc gt1 = loc + 0;
Loc dup = loc + 2;
set(gt0 + 0, a);
set(gt0 + 1, term_new(DP0, sup_lab, dup));
set(gt1 + 0, b);
set(gt1 + 1, term_new(DP1, sup_lab, dup));
set(dup + 0, f);
set(sup_loc + 0, term_new(GET, 0, gt0));
set(sup_loc + 1, term_new(GET, 0, gt1));
return term_new(SUP, sup_lab, sup_loc);
}
// ~(){(,):f}
// ---------- GET-NIL
// error
Term reduce_get_nil(Term get, Term nil) {
printf("invalid:get-nil");
exit(0);
}
// ~(a,b){(,):f}
// ------------- GET-TUP
// (f a b)
Term reduce_get_tup(Term get, Term tup) {
inc_itr();
Loc get_loc = term_loc(get);
Loc tup_loc = term_loc(tup);
Term f = got(get_loc + 1);
Term a = got(tup_loc + 0);
Term b = got(tup_loc + 1);
Loc app1 = alloc_node(2);
Loc app2 = get_loc;
set(app1 + 0, f);
set(app1 + 1, a);
set(app2 + 0, term_new(APP, 0, app1));
set(app2 + 1, b);
return term_new(APP, 0, app2);
}
// ~λx.g{(,):f}
// ------------ GET-LAM
// error
Term reduce_get_lam(Term get, Term lam) {
printf("invalid:get-lam");
exit(0);
}
// ~123{(,):f}
// ----------- GET-W32
// error
Term reduce_get_w32(Term get, Term w32) {
printf("invalid:get-w32");
exit(0);
}
// ~TYP{(,):f}
// ----------- GET-TYP
// error
Term reduce_get_typ(Term get, Term typ) {
printf("invalid:get-typ");
exit(0);
}
// ~*{0:z;+:s}
// ----------- SWI-ERA
// *
Term reduce_swi_era(Term swi, Term era) {
inc_itr();
return era;
}
// ~&L{a,b}{0:z;+:s}
// ------------------------------- SWI-SUP
// ! &L{z0,z1} = z;
// ! &L{s0,s1} = s;
// &L{~a{0:z0;+:s0},~b{0:z1;+:s1}}
Term reduce_swi_sup(Term swi, Term sup) {
// Correct implementation that reuses the given SUP/SWI nodes
inc_itr();
// Locations / labels
Loc swi_loc = term_loc(swi); // original SWI (will become SWI0)
Loc sup_loc = term_loc(sup); // SUP we will reuse
Lab sup_lab = term_lab(sup); // label of the SUP
Lab swi_lab = term_lab(swi); // (unused, still preserve)
// Extract SWI arms
Term z = got(swi_loc + 1);
Term s = got(swi_loc + 2);
// Extract SUP branches
Term a = got(sup_loc + 0);
Term b = got(sup_loc + 1);
// Allocate:
// - 3 cells for the second SWI (swi1)
// - 1 cell for dup(z) (dupz)
// - 1 cell for dup(s) (dups)
Loc loc = alloc_node(5);
Loc swi1 = loc; // 3 cells (value,z,s)
Loc dupz = loc + 3; // 1 cell
Loc dups = loc + 4; // 1 cell
// Store originals inside dup nodes
set(dupz + 0, z);
set(dups + 0, s);
// Build SWI0 (reuse swi_loc)
set(swi_loc + 0, a);
set(swi_loc + 1, term_new(DP0, sup_lab, dupz));
set(swi_loc + 2, term_new(DP0, sup_lab, dups));
// Build SWI1 (new node)
set(swi1 + 0, b);
set(swi1 + 1, term_new(DP1, sup_lab, dupz));
set(swi1 + 2, term_new(DP1, sup_lab, dups));
// Build resulting SUP (reuse sup_loc)
set(sup_loc + 0, term_new(SWI, swi_lab, swi_loc));
set(sup_loc + 1, term_new(SWI, swi_lab, swi1));
return term_new(SUP, sup_lab, sup_loc);
}
// ~(){0:z;+:s}
// ------------ SWI-NIL
// error
Term reduce_swi_nil(Term swi, Term nil) {
printf("invalid:swi-nil");
exit(0);
}
// ~(a,b){0:z;+:s}
// --------------- SWI-TUP
// error
Term reduce_swi_tup(Term swi, Term tup) {
printf("invalid:swi-tup");
exit(0);
}
// ~λx.g{0:z;+:s}
// -------------- SWI-LAM
// error
Term reduce_swi_lam(Term swi, Term lam) {
printf("invalid:swi-lam");
exit(0);
}
// ~n{0:z;+:s}
// ----------- SWI-W32
// if n = 0:
// z
// else:
// (s (n-1))
Term reduce_swi_w32(Term swi, Term w32) {
inc_itr();
Loc swi_loc = term_loc(swi);
u32 val = term_loc(w32);
Term z = got(swi_loc + 1);
Term s = got(swi_loc + 2);
if (val == 0) {
return z;
} else {
Loc app = swi_loc;
set(app + 0, s);
set(app + 1, term_new(W32, 0, val - 1));
return term_new(APP, 0, app);
}
}
// ~T{0:z;+:s}
// ----------- SWI-TYP
// error
Term reduce_swi_typ(Term swi, Term typ) {
printf("invalid:swi-typ");
exit(0);
}
// ! &L{r,s} = *
// ------------- DUP-ERA
// r <- *
// s <- *
Term reduce_dup_era(Term dup, Term era) {
//printf("reduce_dup_era "); print_term(dup); printf("\n");
inc_itr();
Loc dup_loc = term_loc(dup);
sub(dup_loc + 0, era);
return era;
}
// ! &L{x,y} = &L{a,b}
// ------------------- DUP-SUP
// x <- a
// y <- b
Term reduce_dup_sup(Term dup, Term sup) {
//printf("reduce_dup_sup %u %u | %llu ", term_lab(dup), term_lab(sup), *HVM.spos); print_term(dup); printf(" "); print_term(sup); printf("\n");
inc_itr();
Loc dup_loc = term_loc(dup);
Lab dup_lab = term_lab(dup);
Lab sup_lab = term_lab(sup);
Loc sup_loc = term_loc(sup);
if (dup_lab == sup_lab) {
Term tm0 = got(sup_loc + 0);
Term tm1 = got(sup_loc + 1);
if (term_tag(dup) == DP0) {
sub(dup_loc + 0, tm1);
return tm0;
} else {
sub(dup_loc + 0, tm0);
return tm1;
}
} else {
Loc loc = alloc_node(4);
Loc du0 = sup_loc + 0;
Loc du1 = sup_loc + 1;
Loc su0 = loc + 0;
Loc su1 = loc + 2;
set(su0 + 0, term_new(DP0, dup_lab, du0));
set(su0 + 1, term_new(DP0, dup_lab, du1));
set(su1 + 0, term_new(DP1, dup_lab, du0));
set(su1 + 1, term_new(DP1, dup_lab, du1));
if (term_tag(dup) == DP0) {
sub(dup_loc + 0, term_new(SUP, sup_lab, su1));
return term_new(SUP, sup_lab, su0);
} else {
sub(dup_loc + 0, term_new(SUP, sup_lab, su0));
return term_new(SUP, sup_lab, su1);
}
}
}
// ! &L{r s} = λx.f
// ---------------- DUP-LAM
// r <- λx0.f0
// s <- λx1.f1
// x <- &L{x0,x1}
// ! &L{f0,f1} = f
Term reduce_dup_lam(Term dup, Term lam) {
//printf("reduce_dup_lam "); print_term(dup); printf("\n");
inc_itr();
Loc dup_loc = term_loc(dup);
Loc lam_loc = term_loc(lam);
Lab dup_lab = term_lab(dup);
Term bod = got(lam_loc + 0);
Loc loc = alloc_node(5);
Loc lm0 = loc + 0;
Loc lm1 = loc + 1;
Loc su0 = loc + 2;
Loc du0 = loc + 4;
sub(lam_loc + 0, term_new(SUP, dup_lab, su0));
set(lm0 + 0, term_new(DP0, dup_lab, du0));
set(lm1 + 0, term_new(DP1, dup_lab, du0));
set(su0 + 0, term_new(VAR, 0, lm0));
set(su0 + 1, term_new(VAR, 0, lm1));
set(du0 + 0, bod);
if (term_tag(dup) == DP0) {
sub(dup_loc + 0, term_new(LAM, 0, lm1));
return term_new(LAM, 0, lm0);
} else {
sub(dup_loc + 0, term_new(LAM, 0, lm0));
return term_new(LAM, 0, lm1);
}
}
// ! &L{x,y} = ()
// -------------- DUP-NIL
// x <- ()
// y <- ()
Term reduce_dup_nil(Term dup, Term nil) {
inc_itr();
Loc dup_loc = term_loc(dup);
sub(dup_loc + 0, nil);
return nil;
}
// ! &L{x,y} = (a,b)
// ----------------- DUP-TUP
// ! &L{a0,a1} = a
// ! &L{b0,b1} = b
// x <- (a0,b0)
// y <- (a1,b1)
Term reduce_dup_tup(Term dup, Term tup) {
inc_itr();
Loc dup_loc = term_loc(dup);
Lab dup_lab = term_lab(dup);
Loc tup_loc = term_loc(tup);
Term a = got(tup_loc + 0);
Term b = got(tup_loc + 1);
Loc loc = alloc_node(4);
Loc tup1 = loc + 0;
Loc dupa = loc + 2;
Loc dupb = loc + 3;
set(dupa + 0, a);
set(dupb + 0, b);
set(tup_loc + 0, term_new(DP0, dup_lab, dupa));
set(tup_loc + 1, term_new(DP0, dup_lab, dupb));
set(tup1 + 0, term_new(DP1, dup_lab, dupa));
set(tup1 + 1, term_new(DP1, dup_lab, dupb));
if (term_tag(dup) == DP0) {
sub(dup_loc + 0, term_new(TUP, 0, tup1));
return term_new(TUP, 0, tup_loc);
} else {
sub(dup_loc + 0, term_new(TUP, 0, tup_loc));
return term_new(TUP, 0, tup1);
}
}
// ! &L{x,y} = 123
// --------------- DUP-W32
// x <- 123
// y <- 123
Term reduce_dup_w32(Term dup, Term w32) {
//printf("reduce_dup_w32 "); print_term(dup); printf("\n");
inc_itr();
Loc dup_loc = term_loc(dup);
sub(dup_loc + 0, w32);
return w32;
}
// ! &L{x,y} = Set
// --------------- DUP-SET
// x <- Set
// y <- Set
Term reduce_dup_set(Term dup, Term set) {
inc_itr();
Loc dup_loc = term_loc(dup);
sub(dup_loc + 0, set);
return set;
}
// ! &L{x,y} = ⊥
// ------------- DUP-EMP
// x <- ⊥
// y <- ⊥
Term reduce_dup_emp(Term dup, Term emp) {
inc_itr();
Loc dup_loc = term_loc(dup);
sub(dup_loc + 0, emp);
return emp;
}
// ! &L{x,y} = ⊤
// ------------- DUP-UNI
// x <- ⊤
// y <- ⊤
Term reduce_dup_uni(Term dup, Term uni) {
inc_itr();
Loc dup_loc = term_loc(dup);
sub(dup_loc + 0, uni);
return uni;
}
// ! &L{x,y} = U32
// -------------- DUP-U32
// x <- U32
// y <- U32
Term reduce_dup_u32(Term dup, Term u32) {
inc_itr();
Loc dup_loc = term_loc(dup);
sub(dup_loc + 0, u32);
return u32;
}
// ! &L{x,y} = ΣA.B
// ----------------- DUP-SIG
// ! &L{A0,A1} = A
// ! &L{B0,B1} = B
// x <- ΣA0.B0
// y <- ΣA1.B1
Term reduce_dup_sig(Term dup, Term sig) {
inc_itr();
Loc dup_loc = term_loc(dup);
Lab dup_lab = term_lab(dup);
Loc sig_loc = term_loc(sig);
Term a = got(sig_loc + 0);
Term b = got(sig_loc + 1);
Loc loc = alloc_node(4);
Loc sig1 = loc + 0;
Loc dupa = loc + 2;
Loc dupb = loc + 3;
set(dupa + 0, a);
set(dupb + 0, b);
set(sig_loc + 0, term_new(DP0, dup_lab, dupa));
set(sig_loc + 1, term_new(DP0, dup_lab, dupb));
set(sig1 + 0, term_new(DP1, dup_lab, dupa));
set(sig1 + 1, term_new(DP1, dup_lab, dupb));
if (term_tag(dup) == DP0) {
sub(dup_loc + 0, term_new(SIG, 0, sig1));
return term_new(SIG, 0, sig_loc);
} else {
sub(dup_loc + 0, term_new(SIG, 0, sig_loc));
return term_new(SIG, 0, sig1);
}
}
// ! &L{x,y} = ∀A.B
// ----------------- DUP-ALL
// ! &L{A0,A1} = A
// ! &L{B0,B1} = B
// x <- ∀A0.B0
// y <- ∀A1.B1
Term reduce_dup_all(Term dup, Term all) {
inc_itr();
Loc dup_loc = term_loc(dup);
Lab dup_lab = term_lab(dup);
Loc all_loc = term_loc(all);
Term a = got(all_loc + 0);
Term b = got(all_loc + 1);
Loc loc = alloc_node(4);
Loc all1 = loc + 0;
Loc dupa = loc + 2;
Loc dupb = loc + 3;
set(dupa + 0, a);
set(dupb + 0, b);
set(all_loc + 0, term_new(DP0, dup_lab, dupa));
set(all_loc + 1, term_new(DP0, dup_lab, dupb));
set(all1 + 0, term_new(DP1, dup_lab, dupa));
set(all1 + 1, term_new(DP1, dup_lab, dupb));
if (term_tag(dup) == DP0) {
sub(dup_loc + 0, term_new(ALL, 0, all1));
return term_new(ALL, 0, all_loc);
} else {
sub(dup_loc + 0, term_new(ALL, 0, all_loc));
return term_new(ALL, 0, all1);
}
}
// ! &L{x,y} = @foo(a b c ...)
// --------------------------- DUP-REF-COPY (when &L not in @foo)
// ! &L{a0,a1} = a
// ! &L{b0,b1} = b
// ! &L{c0,c1} = c
// ...
// x <- @foo(a0 b0 c0 ...)
// y <- @foo(a1 b1 c1 ...)
Term reduce_dup_ref(Term dup, Term ref) {
//printf("reduce_dup_ref "); print_term(dup); printf("\n");
inc_itr();
Loc dup_loc = term_loc(dup);
Lab dup_lab = term_lab(dup);
Loc ref_loc = term_loc(ref);
Lab ref_lab = term_lab(ref);
u64 ref_ari = HVM.fari[ref_lab];
Loc loc = alloc_node(ref_ari * 2);
Loc ref0 = ref_loc;
Loc ref1 = loc + 0;
for (u64 i = 0; i < ref_ari; i++) {
Loc du0 = loc + ref_ari + i;
set(du0 + 0, got(ref_loc + i));
set(ref0 + i, term_new(DP0, dup_lab, du0));
set(ref1 + i, term_new(DP1, dup_lab, du0));
}
if (term_tag(dup) == DP0) {
sub(dup_loc + 0, term_new(REF, ref_lab, ref1));
return term_new(REF, ref_lab, ref0);
} else {
sub(dup_loc + 0, term_new(REF, ref_lab, ref0));
return term_new(REF, ref_lab, ref1);
}
}
// (<op * y)
// --------- OPX-ERA
// *
Term reduce_opx_era(Term opx, Term era) {
//printf("reduce_opx_era "); print_term(opx); printf("\n");
inc_itr();
return era;
}
// (<op λx.f y)
// ----------- OPX-LAM
// error
Term reduce_opx_lam(Term opx, Term lam) {
//printf("reduce_opx_lam "); print_term(opx); printf("\n");
printf("invalid:opx-lam");
exit(0);
}
// (<op &L{a,b} y)
// ------------------------- OPX-SUP
// ! &L{y0,y1} = y;
// &L{(<op a y0),(<op b y1)}
Term reduce_opx_sup(Term opx, Term sup) {
//printf("reduce_opx_sup "); print_term(opx); printf("\n");
inc_itr();
Loc opx_loc = term_loc(opx);
Loc sup_loc = term_loc(sup);
Lab sup_lab = term_lab(sup);
Term nmy = got(opx_loc + 1);
Term tm0 = got(sup_loc + 0);
Term tm1 = got(sup_loc + 1);
Loc loc = alloc_node(3);
Loc op0 = opx_loc;
Loc op1 = loc + 0;
Loc du0 = loc + 2;
set(op0 + 0, tm0);
set(op0 + 1, term_new(DP0, sup_lab, du0));
set(op1 + 0, tm1);
set(op1 + 1, term_new(DP1, sup_lab, du0));
set(du0 + 0, nmy);
set(sup_loc + 0, term_new(OPX, term_lab(opx), op0));
set(sup_loc + 1, term_new(OPX, term_lab(opx), op1));
return term_new(SUP, sup_lab, sup_loc);
}
// (<op () y)
// ---------- OPX-NIL
// error
Term reduce_opx_nil(Term opx, Term nil) {
printf("invalid:opx-nil");
exit(0);
}
// (<op (x0,x1) y)
// --------------- OPX-TUP
// error
Term reduce_opx_tup(Term opx, Term tup) {
printf("invalid:opx-tup");
exit(0);
}
// (<op x y)
// --------- OPX-W32
// (>op y x)
Term reduce_opx_w32(Term opx, Term nmx) {
//printf("reduce_opx_w32 "); print_term(opx); printf("\n");
inc_itr();
Lab opx_lab = term_lab(opx);
Loc opx_loc = term_loc(opx);
Term nmy = got(opx_loc + 1);
set(opx_loc + 0, nmy);
set(opx_loc + 1, nmx);
return term_new(OPY, opx_lab, opx_loc);
}
// (<op T y)
// --------- OPX-TYP
// error
Term reduce_opx_typ(Term opx, Term typ) {
printf("invalid:opx-typ");
exit(0);
}
// (>op x *)
// --------- OPY-ERA
// *
Term reduce_opy_era(Term opy, Term era) {
//printf("reduce_opy_era "); print_term(opy); printf("\n");
inc_itr();
return era;
}
// (>op x λy.f)
// ------------ OPY-LAM
// error
Term reduce_opy_lam(Term opy, Term lam) {
//printf("reduce_opy_lam "); print_term(opy); printf("\n");
printf("invalid:opy-lam");
exit(0);
}
// (>op x &L{y0,y1})
// ----------------------- OPY-SUP
// &L{>op(x y0),>op(x y1)}
Term reduce_opy_sup(Term opy, Term sup) {
//printf("reduce_opy_sup "); print_term(opy); printf("\n");
inc_itr();
Loc opy_loc = term_loc(opy);
Loc sup_loc = term_loc(sup);
Lab sup_lab = term_lab(sup);
Term nmx = got(opy_loc + 1);
Term tm0 = got(sup_loc + 0);
Term tm1 = got(sup_loc + 1);
Loc op0 = opy_loc;
Loc op1 = alloc_node(2);
set(op0 + 0, nmx);
set(op0 + 1, tm0);
set(op1 + 0, nmx);
set(op1 + 1, tm1);
set(sup_loc + 0, term_new(OPY, term_lab(opy), op0));
set(sup_loc + 1, term_new(OPY, term_lab(opy), op1));
return term_new(SUP, sup_lab, sup_loc);
}
// (>op x ())
// ---------- OPY-NIL
// error
Term reduce_opy_nil(Term opy, Term nil) {
printf("invalid:opy-nil");
exit(0);
}
// (>op x (y0,y1))
// --------------- OPY-TUP
// error
Term reduce_opy_tup(Term opy, Term tup) {
printf("invalid:opy-tup");
exit(0);
}
// (>op x y)
// --------- OPY-W32
// x <op> y
Term reduce_opy_w32(Term opy, Term val) {
//printf("reduce_opy_w32 "); print_term(opy); printf("\n");
inc_itr();
Loc opy_loc = term_loc(opy);
Tag t = term_tag(val);
u32 x = term_loc(got(opy_loc + 1));
u32 y = term_loc(val);
u32 result;
switch (term_lab(opy)) {
case OP_ADD: result = x + y; break;
case OP_SUB: result = x - y; break;
case OP_MUL: result = x * y; break;
case OP_DIV: result = x / y; break;
case OP_MOD: result = x % y; break;
case OP_EQ: result = x == y; break;
case OP_NE: result = x != y; break;
case OP_LT: result = x < y; break;
case OP_GT: result = x > y; break;
case OP_LTE: result = x <= y; break;
case OP_GTE: result = x >= y; break;
case OP_AND: result = x & y; break;
case OP_OR: result = x | y; break;
case OP_XOR: result = x ^ y; break;
case OP_LSH: result = x << y; break;
case OP_RSH: result = x >> y; break;
default: {
printf("invalid:opy-w32");
exit(0);
}
}
return term_new(W32, 0, result);
}
// (>op x T)
// --------- OPY-TYP
// error
Term reduce_opy_typ(Term opy, Term typ) {
printf("invalid:opy-typ");
exit(0);
}
Term reduce(Term term) {
if (term_is_whnf(term)) {
return term;
}
Term next = term;
u64 stop = *HVM.spos;
u64 spos = stop;
Term* sbuf = HVM.sbuf;
while (1) {
//printf("NEXT "); print_term(term); printf("\n");
//printf("PATH ");
//for (u64 i = 0; i < *spos; ++i) {
//print_tag(term_tag(HVM.sbuf[i]));
//printf(" ");
//}
//printf(" ~ %p", HVM.sbuf);
//printf("\n");
Tag tag = term_tag(next);
Lab lab = term_lab(next);
Loc loc = term_loc(next);
// On variables: substitute
// On eliminators: move to field
switch (tag) {
case LET: {
switch (lab) {
case LAZY: {
next = reduce_let(next, got(loc + 0));
continue;
}
case STRI: {
spush(next, sbuf, &spos);
next = got(loc + 0);
continue;
}
default: {
printf("invalid:let");
exit(0);
}
}
}
case APP:
case USE:
case GET:
case SWI:
case OPX:
case OPY: {
spush(next, sbuf, &spos);
next = got(loc + 0);
continue;
}
case DP0:
case DP1: {
Term sub = got(loc + 0);
if (term_get_bit(sub) == 0) {
spush(next, sbuf, &spos);
next = sub;
continue;
} else {
next = term_rem_bit(sub);
continue;
}
}
case VAR: {
Term sub = got(loc);
if (term_get_bit(sub) == 0) {
break;
} else {
next = term_rem_bit(sub);
continue;
}
}
case REF: {
*HVM.spos = spos;
next = reduce_ref(next);
spos = *HVM.spos;
continue;
}
default: break;
}
// Empty stack: term is in WHNF
if (spos == stop) {
*HVM.spos = spos;
return next;
}
// Interaction Dispatcher
Term prev = spop(sbuf, &spos);
Tag ptag = term_tag(prev);
Lab plab = term_lab(prev);
Loc ploc = term_loc(prev);
switch (ptag) {
case LET: {
next = reduce_let(prev, next);
continue;
}
case ANN: {
next = reduce_ann(prev, next);
continue;
}
case APP: {
switch (tag) {
case ERA: next = reduce_app_era(prev, next); continue;
case LAM: next = reduce_app_lam(prev, next); continue;
case SUP: next = reduce_app_sup(prev, next); continue;
case NIL: next = reduce_app_nil(prev, next); continue;
case TUP: next = reduce_app_tup(prev, next); continue;
case W32: next = reduce_app_w32(prev, next); continue;
case SET:
case EMP:
case UNI:
case U32:
case SIG:
case ALL: next = reduce_app_typ(prev, next); continue;
default: break;
}
}
case USE: {
switch (tag) {
case ERA: next = reduce_use_era(prev, next); continue;
case SUP: next = reduce_use_sup(prev, next); continue;
case LAM: next = reduce_use_lam(prev, next); continue;
case NIL: next = reduce_use_nil(prev, next); continue;
case TUP: next = reduce_use_tup(prev, next); continue;
case W32: next = reduce_use_w32(prev, next); continue;
case SET:
case EMP:
case UNI:
case U32:
case SIG:
case ALL: next = reduce_use_typ(prev, next); continue;
default: break;
}
}
case GET: {
switch (tag) {
case ERA: next = reduce_get_era(prev, next); continue;
case SUP: next = reduce_get_sup(prev, next); continue;
case NIL: next = reduce_get_nil(prev, next); continue;
case TUP: next = reduce_get_tup(prev, next); continue;
case LAM: next = reduce_get_lam(prev, next); continue;
case W32: next = reduce_get_w32(prev, next); continue;
case SET:
case EMP:
case UNI:
case U32:
case SIG:
case ALL: next = reduce_get_typ(prev, next); continue;
default: break;
}
}
case SWI: {
switch (tag) {
case ERA: next = reduce_swi_era(prev, next); continue;
case SUP: next = reduce_swi_sup(prev, next); continue;
case NIL: next = reduce_swi_nil(prev, next); continue;
case TUP: next = reduce_swi_tup(prev, next); continue;
case LAM: next = reduce_swi_lam(prev, next); continue;
case W32: next = reduce_swi_w32(prev, next); continue;
case SET:
case EMP:
case UNI:
case U32:
case SIG:
case ALL: next = reduce_swi_typ(prev, next); continue;
default: break;
}
}
case DP0:
case DP1: {
switch (tag) {
case ERA: next = reduce_dup_era(prev, next); continue;
case SUP: next = reduce_dup_sup(prev, next); continue;
case LAM: next = reduce_dup_lam(prev, next); continue;
case NIL: next = reduce_dup_nil(prev, next); continue;
case TUP: next = reduce_dup_tup(prev, next); continue;
case W32: next = reduce_dup_w32(prev, next); continue;
case SET: next = reduce_dup_set(prev, next); continue;
case EMP: next = reduce_dup_emp(prev, next); continue;
case UNI: next = reduce_dup_uni(prev, next); continue;
case U32: next = reduce_dup_u32(prev, next); continue;
case SIG: next = reduce_dup_sig(prev, next); continue;
case ALL: next = reduce_dup_all(prev, next); continue;
case REF: next = reduce_dup_ref(prev, next); continue;
default: break;
}
}
case OPX: {
switch (tag) {
case ERA: next = reduce_opx_era(prev, next); continue;
case LAM: next = reduce_opx_lam(prev, next); continue;
case SUP: next = reduce_opx_sup(prev, next); continue;
case NIL: next = reduce_opx_nil(prev, next); continue;
case TUP: next = reduce_opx_tup(prev, next); continue;
case W32: next = reduce_opx_w32(prev, next); continue;
case SET:
case EMP:
case UNI:
case U32:
case SIG:
case ALL: next = reduce_opx_typ(prev, next); continue;
default: break;
}
}
case OPY: {
switch (tag) {
case ERA: next = reduce_opy_era(prev, next); continue;
case LAM: next = reduce_opy_lam(prev, next); continue;
case SUP: next = reduce_opy_sup(prev, next); continue;
case NIL: next = reduce_opy_nil(prev, next); continue;
case TUP: next = reduce_opy_tup(prev, next); continue;
case W32: next = reduce_opy_w32(prev, next); continue;
case SET:
case EMP:
case UNI:
case U32:
case SIG:
case ALL: next = reduce_opy_typ(prev, next); continue;
default: break;
}
}
default: break;
}
// No interaction: push term back to stack
spush(prev, sbuf, &spos);
// Update parent chain
while (spos > stop) {
Term host = spop(sbuf, &spos);
Tag htag = term_tag(host);
Lab hlab = term_lab(host);
Loc hloc = term_loc(host);
set(hloc + 0, next);
next = host;
}
*HVM.spos = spos;
return next;
}
}
Term reduce_at(Loc host) {
Term tm0 = got(host);
if (term_is_whnf(tm0)) {
return tm0;
}
Term tm1 = reduce(tm0);
set(host, tm1);
return tm1;
}
Term normal(Term term) {
Term wnf = reduce(term);
Tag tag = term_tag(wnf);
Lab lab = term_lab(wnf);
Loc loc = term_loc(wnf);
switch (tag) {
case LAM: {
Term bod = got(loc + 0);
bod = normal(bod);
set(loc + 0, bod);
return wnf;
}
case APP: {
Term fun = got(loc + 0);
Term arg = got(loc + 1);
fun = normal(fun);
arg = normal(arg);
set(loc + 0, fun);
set(loc + 1, arg);
return wnf;
}
case SUP: {
Term tm0 = got(loc + 0);
Term tm1 = got(loc + 1);
tm0 = normal(tm0);
tm1 = normal(tm1);
set(loc + 0, tm0);
set(loc + 1, tm1);
return wnf;
}
case TUP: {
Term tm0 = got(loc + 0);
Term tm1 = got(loc + 1);
tm0 = normal(tm0);
tm1 = normal(tm1);
set(loc + 0, tm0);
set(loc + 1, tm1);
return wnf;
}
case SIG: {
Term tm0 = got(loc + 0);
Term tm1 = got(loc + 1);
tm0 = normal(tm0);
tm1 = normal(tm1);
set(loc + 0, tm0);
set(loc + 1, tm1);
return wnf;
}
case ALL: {
Term tm0 = got(loc + 0);
Term tm1 = got(loc + 1);
tm0 = normal(tm0);
tm1 = normal(tm1);
set(loc + 0, tm0);
set(loc + 1, tm1);
return wnf;
}
case DP0:
case DP1: {
Term val = got(loc + 0);
val = normal(val);
set(loc + 0, val);
return wnf;
}
case USE:
case GET:
case SWI: {
for (u64 i = 0; i <= 1; i++) {
Term arg = got(loc + i);
arg = normal(arg);
set(loc + i, arg);
}
return wnf;
}
default:
return wnf;
}
}
// Primitives
// ----------
// Primitive: Dynamic Sup @SUP(lab tm0 tm1)
// Allocates a new SUP node with given label.
Term SUP_f(Term ref) {
Loc ref_loc = term_loc(ref);
Term lab = reduce(got(ref_loc + 0));
Term lab_val = term_loc(lab);
if (term_tag(lab) != W32) {
printf("ERROR:non-numeric-sup-label\n");
}
if (lab_val > 0xFFFF) {
printf("ERROR:sup-label-too-large\n");
}
Term tm0 = got(ref_loc + 1);
Term tm1 = got(ref_loc + 2);
Loc sup = alloc_node(2);
Term ret = term_new(SUP, lab_val, sup);
set(sup + 0, tm0);
set(sup + 1, tm1);
*HVM.itrs += 1;
return ret;
}
// Primitive: Dynamic Dup @DUP(lab val λdp0λdp1(bod))
// Creates a DUP node with given label.
Term DUP_f(Term ref) {
Loc ref_loc = term_loc(ref);
Term lab = reduce(got(ref_loc + 0));
Term lab_val = term_loc(lab);
if (term_tag(lab) != W32) {
printf("ERROR:non-numeric-dup-label\n");
}
if (lab_val > 0xFFFF) {
printf("ERROR:dup-label-too-large\n");
}
Term val = got(ref_loc + 1);
Term bod = got(ref_loc + 2);
Loc dup = alloc_node(1);
set(dup + 0, val);
if (term_tag(bod) == LAM) {
Loc lam0 = term_loc(bod);
Term bod0 = got(lam0 + 0);
if (term_tag(bod0) == LAM) {
Loc lam1 = term_loc(bod0);
Term bod1 = got(lam1 + 0);
sub(lam0 + 0, term_new(DP0, lab_val, dup));
sub(lam1 + 0, term_new(DP1, lab_val, dup));
*HVM.itrs += 3;
return bod1;
}
}
Loc app0 = alloc_node(2);
set(app0 + 0, bod);
set(app0 + 1, term_new(DP0, lab_val, dup));
Loc app1 = alloc_node(2);
set(app1 + 0, term_new(APP, 0, app0));
set(app1 + 1, term_new(DP1, lab_val, dup));
*HVM.itrs += 1;
return term_new(APP, 0, app1);
}
Term LOG_f(Term ref) {
printf("TODO: LOG_f");
exit(0);
}
void *alloc_huge(size_t size) {
void *ptr = mmap(NULL, size, PROT_READ | PROT_WRITE,
MAP_PRIVATE | MAP_ANONYMOUS | MAP_NORESERVE,
-1, 0);
if (ptr == MAP_FAILED) {
perror("mmap failed");
return NULL;
}
return ptr;
}
// Runtime Memory
// --------------
void hvm_init() {
HVM.sbuf = alloc_huge(MAX_STACK_SIZE * sizeof(Term));
HVM.heap = alloc_huge(MAX_HEAP_SIZE * sizeof(Term));
HVM.spos = alloc_huge(sizeof(u64));
HVM.size = alloc_huge(sizeof(u64));
HVM.itrs = alloc_huge(sizeof(u64));
HVM.frsh = alloc_huge(sizeof(u64));
#define CHECK_ALLOC(ptr, name) if (!(ptr)) { printf(name " alloc failed\n"); allocs_failed++; }
int allocs_failed = 0; // Track if any allocation failed
CHECK_ALLOC(HVM.sbuf, "sbuf");
CHECK_ALLOC(HVM.heap, "heap");
CHECK_ALLOC(HVM.spos, "spos");
CHECK_ALLOC(HVM.size, "size");
CHECK_ALLOC(HVM.itrs, "itrs");
CHECK_ALLOC(HVM.frsh, "frsh");
if (allocs_failed > 0) {
printf("hvm_init alloc's failed: %d allocations failed\n", allocs_failed);
exit(1);
}
#undef CHECK_ALLOC
*HVM.spos = 0;
*HVM.size = 1;
*HVM.itrs = 0;
*HVM.frsh = 0x20;
HVM.book[SUP_F] = SUP_f;
HVM.book[DUP_F] = DUP_f;
HVM.book[LOG_F] = LOG_f;
for (int i = 0; i < 65536; i++) {
HVM.fari[i] = 0;
}
}
void hvm_munmap(void *ptr, size_t size, const char *name) {
if (ptr != MAP_FAILED) {
if (munmap(ptr, size) == -1) {
perror("munmap failed");
} else {
// printf("Successfully unmapped %s\n", name);
}
} else {
printf("%s is already null or invalid.\n", name);
}
}
void hvm_free() {
hvm_munmap(HVM.sbuf, MAX_STACK_SIZE * sizeof(Term), "sbuf");
hvm_munmap(HVM.heap, MAX_HEAP_SIZE * sizeof(Term), "heap");
hvm_munmap(HVM.spos, sizeof(u64), "spos");
hvm_munmap(HVM.size, sizeof(u64), "size");
hvm_munmap(HVM.itrs, sizeof(u64), "itrs");
hvm_munmap(HVM.frsh, sizeof(u64), "frsh");
}
State* hvm_get_state() {
return &HVM;
}
void hvm_set_state(State* hvm) {
HVM.sbuf = hvm->sbuf;
HVM.spos = hvm->spos;
HVM.heap = hvm->heap;
HVM.size = hvm->size;
HVM.itrs = hvm->itrs;
HVM.frsh = hvm->frsh;
for (int i = 0; i < 65536; i++) {
HVM.book[i] = hvm->book[i];
HVM.fari[i] = hvm->fari[i];
}
}
void hvm_define(u16 fid, Term (*func)()) {
//printf("defined %llu %p\n", fid, func);
HVM.book[fid] = func;
}
void hvm_set_fari(u16 fid, u16 arity) {
HVM.fari[fid] = arity;
}
-- TASK: write below a complete bidirectional type checker, based on OldCheck
-- the types must be:
-- infer : Int → Term → IO (Result Term)
-- check : Int → Term → Term → IO (Result ())
-- make it a 1-to-1 correspondence to OldCheck
-- (omitted)
-- this is a good start, but:
-- - 1. the style of this file doesn't match the rest of the codebase. refactor its style completely.
-- - 2. many infer/check cases are missing. remember to consult the original OldCheck file to learn how each case should work. this file should remain a close correspondence to it.
-- rewrite the file again, addressing these issues:
-- (omitted)
-- the file above is better, but it still has some issues.
-- first: termEqual must be renamed to just equal
-- second: due to how superpositions work on HVM, we need to update the equal
-- function to handle SUPs, as follows:
-- &L{a0,a1} == b
-- ----------------------- EQUAL-SUP-VAL
-- ! &L{b0,b1} = b;
-- &L{a0 == a1 , b0 == b1}
-- a == &L{b0,b1}
-- ----------------------- EQUAL-VAL-SUP
-- ! &L{a0,a1} = a;
-- &L{a0 == a1 , b0 == b1}
-- Now, since EQL can now return a SUP, its return type can't be Bool anymore - it has to be Term.
-- As such, we will return () (One) when the terms are equal, and * (Era) otherwise.
-- Similarly, the infer and check functions must be updated:
-- infer d &L{x0,x1}
-- --------------------------- INFER-SUP
-- &L{infer d x0 , infer d x1}
-- check d &L{x0,x1} t
-- ------------------------------- CHECK-SUP-VAL
-- &L{check d x0 t , check d x1 t}
-- check d x &L{t0,t1}
-- ------------------------------- CHECK-SUP-VAL
-- &L{check d x t0 , check d x t1}
-- These interactions should be incorporated into equal, infer and check, directly.
-- That is, when a term is a SUP, we must return a SUP of both recursive calls.
-- Note that, since infer/equal can also return SUPs, their return can't be Result anymore.
-- Instead, their type will be:
-- infer :: Int -> Term -> IO Term
-- check :: Int -> Term -> Term -> IO Term
-- infer and check will simply return the type (when well-typed) or * (Era) otherwise.
-- check will either return () (One) (when well-typed), or * (Era) otherwise.
-- to report errors, we will just use a print (not an Error type)
-- Finally, since equal returns a Term rather than a Bool, we must also properly
-- match on its return, and dispatch SUP interactions accordingly. for better style,
-- create an auxiliary validate function that will do that part.
-- Also, note there is a logic error in your code.
-- The check function does NOT call whnf on the term, only on the goal.
-- Why did you invent that whnf call out of nowhere?
-- Double check the rest of the code to avoid errors like that.
-- Also, this style is terrible:
-- foo :: ...
-- foo ... x ... = do
-- x_nf <- whnf x
-- let xTag = tTag x_nf
-- case () of
-- _ | xTag == _XYZ_ -> ...
--
-- Instead, let's do it as follows:
-- 1. *BEFORE* calling foo, we take the whnf of the
-- 2. Then, we write foo like:
-- foo :: ...
-- foo ... x ...
-- | tTag x == _XYZ = ...
-- | ...
--
-- use this style in ALL functions, including equal.
-- NEVER use case () again.
-- Also, the following style is terrible:
-- foo = pure Something
-- Instead, let's ALWAYS use a do block, like:
-- foo = do
-- pure Something
-- Also, in many cases, you're allocating nodes like:
-- sup <- allocNode 2
-- set (sup + 0) dp0
-- set (sup + 1) dp1
-- That is very repetitive and error prone. Instead, create a function:
-- makeNode TAG LAB [children]
-- And use it through your code.
-- Complete updated file:
-- (omitted)
-- this initial implementation is good. there is a problem, though.
-- it is NOT exactly aligned with the OldCheck file.
-- for example, on OldCheck, the LAM-ALL case is:
-- #LAM{f}: ~ goal !f {
-- #ALL{A B}:
-- ! &{A0 A1}=A
-- ~ @check((+ dep 1) (f #ANN{#VAR{dep} A0}) #APP{B #ANN{#VAR{dep} A1}}) {
-- #Done{_}: #Done{1}
-- #Fail{e}: #Fail{e}
-- }
-- goal: #Fail{#TypeMismatch{#LAM{f} #ALL{#VAR{0} #LAM{λx.#VAR{0}}} goal}}
-- }
-- yet, on this file, it is:
-- | tTag tm == _LAM_ && tTag goal == _ALL_ = do
-- bod <- field tm 0
-- aTy <- field goal 0
-- bTy <- field goal 1
-- var <- makeNode _VAR_ (fromIntegral dep) [eraT]
-- app <- makeNode _APP_ 0 [bTy, var]
-- bTy <- whnf app
-- bOk <- checkGo (dep+1) bod bTy
-- if tTag bOk == _ERA_
-- then pure eraT
-- else pure nilT
-- problems:
-- - 'tm' should be named 'term', since that's how it is on OldCheck
-- - we should first match '_LAM_', then, inside it, match '_ALL_', preserving the OldCheck structure
-- - the body check must be check (dep+1) (App f (Ann (Var dep) A0) ) (App B (Ann (Var dep) A1)),
-- where A0 and A1 are cloned variables (with a fresh DUP node). instead, what you have is:
-- check (dep+1) f (App B (Var dep)), which is absolutely NOT the same.
-- - across the implementation, there are many instances like this one, where the new checker is not
-- a 1-to-1 correspondence with the old one, as it was supposed to be.
-- your goal is to rewrite Checker.hs again, from scratch, in order to address this issue.
-- make sure to consult OldCheck to learn how the infer/check functions should be structured.
-- remember that equal, both are already correct - no need to change them.
-- write the updated, complete Check.hs file below:
-- (omitted)
-- in the code above, you're using 'ann' more than once. this is NOT ALLOWED.
-- HVM is linear! instead, what you need to do is: use a DUP node to clone
-- 'a', and then make separate ANN's. again, notice how, on OldCheck, we do:
-- ! &{A0 A1}=A
-- this creates a DUP NODE that CLONES 'A' as 'A0' and 'A1'.
-- you're struggling very hard with linearity, so, please, reason about it.
-- then, write below the FIXED version of every defective case:
-- (omitted)
-- OK, this approach does look sensible. now, let's apply this idea to the
-- entire code, in the format we used previously. reimplement the entire file,
-- from scratch, to include the new logic. remember that you ALWAYS need to dup
-- a variable that you use more than once!
-- also, in your reimplementation, attempt to be more consistent with variable
-- names and alignment. for example, this is not fine:
-- lam <- makeNode _LAM_ 0 [setT]
-- allSet <- makeNode _ALL_ 0 [setT, lam]
-- because 'lam' and 'allSet' don't align.
-- now, proceed to rewrite the COMPLETE Check.hs file below:
-- also:
-- 1. for some reason, 'infer' and 'check' are NOT in the proposed structure.
-- infer has been written like:
-- infer dep term0 = do
-- term <- whnf term0
-- case tTag term of
-- t | t == _XYZ_ -> do
-- ...
-- while the correct structure is:
-- infer dep term0 = ... take whnf then call inferGo ...
-- ...
-- inferGo dep tm
-- | tTag tm == _XYZ_ = do
-- ...
-- the same is true for 'check'.
-- also, matching on SUP should NOT be separated from the other cases.
-- that makes absolutely no sense. do not do that.
-- complete, fixed file below:
-- (omitted)
-- ok, this looks great. now, review the code above and:
-- - 1. check if there is still any occurrence of a HVM-side Term being accidentally cloned in Haskell (i.e., by using its variable more than once)
-- - 2. review the code for bugs and issues in general
-- report below all your findings, in English:
-- • The helper dup2 is only creating the two DP-links; it never allocates the
-- actual _DUP_ node that owns them, so the run-time sharing discipline is
-- broken.
-- • dup2 always returns the fixed label 1 (getLabAuto is a stub). Every call
-- therefore re-uses the same label, violating the “fresh label per DUP”
-- rule.
-- • In inferGo (_SIG_, _APP_) and checkGo (_SIG_), the argument a/x is used
-- once before the call to dup2 and then twice inside the DP0/DP1 links,
-- yielding three usages of the same linear value. The DUP must be performed
-- before the very first consumption, not afterwards.
-- • both and equalGo forward the term b (or a) to two recursive calls without
-- duplicating it, so the same run-time pointer is consumed twice.
-- • In the _LAM_ ▸ _ALL_ rule we create two fresh variables (var0 / var1) but
-- use the original type a three times (once for check, twice in ANN) after a
-- single dup2; same linearity issue.
-- • Node construction for DP0/DP1 uses makeNode, but the tag set should be
-- _VAR_ when exposing the binder to the body; DP0/DP1 must live only inside
-- the DUP structure.
-- • Shadowing: in the _APP_ branch new bindings named “a” and “b” override the
-- outer ones, which is confusing and error-prone.
-- NOTE: no - this is actually fine and desirable. use shadowing whenever
-- possible. avoid prefixing names with ' and similar symbols.
-- • getLabAuto is only a placeholder; without a real fresh-label mechanism the
-- interpreter will emit duplicated labels and break reductions that depend
-- on label uniqueness.
-- let's fix this by importing the book in ALL functions (both, etc.)
-- • makeNode is used to create DP0 / DP1 links with a child list of length 1;
-- but a DP-link is *not* an allocated node: it is supposed to be a leaf term
-- (termNew tag lab loc=0). Allocating memory for them wastes space.
-- NOTE: that's correct. DUP nodes are allocated and store the duplicated term,
-- but the DP0/DP1 terms are leaves.
-- • Several inference branches (_REF_, _USE_, _GET_, _SWI_, …) still return
-- eraT after printing a message, whereas OldCheck propagated a #Fail
-- containing a structured error; the new checker therefore loses error
-- information.
-- NOTE: that's okay for now
-- • equalGo / both treat NIL as the only One value. They should also return a
-- SUP-tree when either side is a SUP of Ones, exactly like the other rules.
-- NOTE: what do you mean by that? I'm confused.
-- Fixing the points above requires:
-- – Implementing a real fresh-label supply and wrapping DP0/DP1 inside a
-- proper _DUP_ node.
-- – Performing DUP *before* the first duplicated use.
-- – Never forwarding the same Term to two different consumers without a DUP.
-- – Removing the stray debugging prints or turning them into proper error
-- nodes.
-- – Cleaning up variable shadowing and always using fresh names.
-- TASK: rewrite Check.hs from scratch, again, in order to address these issues.
-- Complete refactored Check.hs file. Remember to increment the fresh label.
-- Write the complete, final version below:
-- COMPLETE CHECK.HS:
-- (omitted)
-- this is still wrong. note that on rules like:
-- | tTag a == _SUP_ = do
-- a0 <- field a 0
-- a1 <- field a 1
-- -- Need to duplicate b because it's used twice
-- (b0, b1) <- makeDup bookRef b
-- r0 <- both bookRef a0 b0
-- r1 <- both bookRef a1 b1
-- makeNode _SUP_ (tLab a) [r0, r1]
-- we need to use the SAME label for the new dup, and the returned SUP.
-- reason about this and update the code to reflect this change verywhere it applies
-- (...)
-- I now believe that we should NOT use the freshLab field from the Book. in
-- fact, I removed it. we should still receive it so we can pass to reduce later
-- on. but, for now, let's instead use a global no-inline counter implemented
-- inside this file itself, for the fresh label generation.
-- final Check.hs:
module Check where
import Control.Monad (when)
import Data.IORef (IORef, readIORef, modifyIORef', newIORef)
import Data.Word
import System.IO.Unsafe (unsafePerformIO)
import Foreign
import Reduce
import Type
-- Global counter for fresh labels
{-# NOINLINE freshLabelCounter #-}
freshLabelCounter :: IORef Lab
freshLabelCounter = unsafePerformIO $ newIORef 0xC00000
-- Constants
setT, empT, uniT, u32T, nilT, eraT :: Term
setT = termNew _SET_ 0 0
empT = termNew _EMP_ 0 0
uniT = termNew _UNI_ 0 0
u32T = termNew _U32_ 0 0
nilT = termNew _NIL_ 0 0
eraT = termNew _ERA_ 0 0
-- Runtime helpers
whnf :: Term -> IO Term
whnf = reduceC
field :: Term -> Int -> IO Term
field t i = do
got (tLoc t + fromIntegral i)
-- | Allocates a node and fills its children, returning the parent Term.
-- If the list of children is empty we return a leaf term (loc = 0).
makeNode :: Tag -> Lab -> [Term] -> IO Term
makeNode tag lab cs
| null cs = do
pure (termNew tag lab 0)
| otherwise = do
ptr <- allocNode (fromIntegral (length cs))
mapM_ (\ (i, c) -> set (ptr + fromIntegral i) c) (zip [0 ..] cs)
pure (termNew tag lab ptr)
-- | Gets a fresh label and increments the counter
getFreshLabel :: IO Lab
getFreshLabel = do
lab <- readIORef freshLabelCounter
modifyIORef' freshLabelCounter (+1)
pure lab
-- | Create a DUP node that holds the original term, and return two DP0/DP1 terms
-- with the specified label
makeDup :: Lab -> Term -> IO (Term, Term)
makeDup lab term = do
-- Create a DUP node to hold the original term
dup <- makeNode _DUP_ lab [term]
-- Create the DP0/DP1 terms (leaf terms with the shared label)
let t0 = termNew _DP0_ lab 0
let t1 = termNew _DP1_ lab 0
-- Return the DP0/DP1 terms
pure (t0, t1)
-- | Create a DUP node with a fresh label
makeDupFresh :: Term -> IO (Term, Term)
makeDupFresh term = do
-- Get a fresh label
freshLab <- getFreshLabel
makeDup freshLab term
-- Structural equality - returns nilT for equal, eraT for not equal
equal :: Int -> Term -> Term -> IO Term
equal dep a0 b0 = do
a <- whnf a0
b <- whnf b0
if a == b
then pure nilT
else equalGo dep a b
-- | Boolean 'and', but for One|Era.
both :: Term -> Term -> IO Term
both a b
| tTag a == _SUP_ = do
a0 <- field a 0
a1 <- field a 1
-- Use the SUP's label when duplicating b
(b0, b1) <- makeDup (tLab a) b
r0 <- both a0 b0
r1 <- both a1 b1
makeNode _SUP_ (tLab a) [r0, r1]
| tTag b == _SUP_ = do
b0 <- field b 0
b1 <- field b 1
-- Use the SUP's label when duplicating a
(a0, a1) <- makeDup (tLab b) a
r0 <- both a0 b0
r1 <- both a1 b1
makeNode _SUP_ (tLab b) [r0, r1]
| tTag a == _NIL_ && tTag b == _NIL_ = do
pure nilT
| otherwise = do
pure eraT
equalGo :: Int -> Term -> Term -> IO Term
equalGo dep a b
| tTag a == _SUP_ = do
a0 <- field a 0
a1 <- field a 1
(b0, b1) <- makeDup (tLab a) b
r0 <- equalGo dep a0 b0
r1 <- equalGo dep a1 b1
makeNode _SUP_ (tLab a) [r0, r1]
| tTag b == _SUP_ = do
b0 <- field b 0
b1 <- field b 1
(a0, a1) <- makeDup (tLab b) a
r0 <- equalGo dep a0 b0
r1 <- equalGo dep a1 b1
makeNode _SUP_ (tLab b) [r0, r1]
| tTag a == _ERA_ && tTag b == _ERA_ = do
pure nilT
| tTag a == _SET_ && tTag b == _SET_ = do
pure nilT
| tTag a == _EMP_ && tTag b == _EMP_ = do
pure nilT
| tTag a == _UNI_ && tTag b == _UNI_ = do
pure nilT
| tTag a == _NIL_ && tTag b == _NIL_ = do
pure nilT
| tTag a == _U32_ && tTag b == _U32_ = do
pure nilT
| tTag a == _W32_ && tTag b == _W32_ = do
if tLab a == tLab b
then pure nilT
else pure eraT
| tTag a == _SIG_ && tTag b == _SIG_ = do
ax <- field a 0
ay <- field a 1
bx <- field b 0
by <- field b 1
rx <- equalGo dep ax bx
ry <- equalGo dep ay by
both rx ry
| tTag a == _TUP_ && tTag b == _TUP_ = do
ax <- field a 0
ay <- field a 1
bx <- field b 0
by <- field b 1
rx <- equalGo dep ax bx
ry <- equalGo dep ay by
both rx ry
| tTag a == _ALL_ && tTag b == _ALL_ = do
aa <- field a 0
ab <- field a 1
ba <- field b 0
bb <- field b 1
ra <- equalGo dep aa ba
rb <- equalGo dep ab bb
both ra rb
| tTag a == _LAM_ && tTag b == _LAM_ = do
ab <- field a 0
bb <- field b 0
equalGo (dep+1) ab bb
| tTag a == _APP_ && tTag b == _APP_ = do
af <- field a 0
ax <- field a 1
bf <- field b 0
bx <- field b 1
rf <- equalGo dep af bf
rx <- equalGo dep ax bx
both rf rx
| tTag a == _ANN_ && tTag b == _ANN_ = do
av <- field a 0
at <- field a 1
bv <- field b 0
bt <- field b 1
rv <- equalGo dep av bv
rt <- equalGo dep at bt
both rv rt
| otherwise = do
pure eraT
-- Inference
infer :: Int -> Term -> IO Term
infer dep term0 = do
term <- whnf term0
inferGo dep term
inferGo :: Int -> Term -> IO Term
inferGo dep term
| tTag term == _SUP_ = do
a <- field term 0
b <- field term 1
aType <- inferGo dep a
bType <- inferGo dep b
makeNode _SUP_ (tLab term) [aType, bType]
| tTag term == _VAR_ = do
putStr "(cant-infer-var)"
pure eraT
| tTag term == _REF_ = do
putStr "(cant-infer-ref)"
pure eraT
| tTag term == _LET_ = do
val <- field term 0
bod <- field term 1
valType <- infer dep val
if tTag valType == _ERA_
then pure eraT
else infer (dep+1) bod
| tTag term == _ERA_ = do
pure setT
| tTag term == _SET_ = do
pure setT
| tTag term == _EMP_ = do
pure setT
| tTag term == _EFQ_ = do
x <- field term 0
rc <- check dep x empT
if tTag rc == _ERA_
then pure eraT
else do
lamB <- makeNode _LAM_ 0 [empT]
makeNode _ALL_ 0 [empT, lamB]
| tTag term == _UNI_ = do
pure setT
| tTag term == _NIL_ = do
pure uniT
| tTag term == _USE_ = do
putStr "(cant-infer-use)"
pure eraT
| tTag term == _U32_ = do
pure setT
| tTag term == _W32_ = do
pure u32T
| tTag term == _SWI_ = do
putStr "(cant-infer-swi)"
pure eraT
| tTag term == _OPX_ || tTag term == _OPY_ = do
putStr "(cant-infer-op)"
pure eraT
| tTag term == _SIG_ = do
a <- field term 0
b <- field term 1
(a0, a1) <- makeDupFresh a
aOk <- check dep a0 setT
if tTag aOk == _ERA_
then pure eraT
else do
lamT <- makeNode _LAM_ 0 [setT]
allT <- makeNode _ALL_ 0 [a1, lamT]
bOk <- check dep b allT
if tTag bOk == _ERA_
then pure eraT
else pure setT
| tTag term == _TUP_ = do
a <- field term 0
b <- field term 1
aType <- infer dep a
if tTag aType == _ERA_
then pure eraT
else do
bType <- infer dep b
if tTag bType == _ERA_
then pure eraT
else do
lamB <- makeNode _LAM_ 0 [bType]
makeNode _SIG_ 0 [aType, lamB]
| tTag term == _GET_ = do
putStr "(cant-infer-get)"
pure eraT
| tTag term == _ALL_ = do
a <- field term 0
b <- field term 1
aOk <- check dep a setT
if tTag aOk == _ERA_
then pure eraT
else do
lamT <- makeNode _LAM_ 0 [setT]
allT <- makeNode _ALL_ 0 [setT, lamT]
bOk <- check dep b allT
if tTag bOk == _ERA_
then pure eraT
else pure setT
| tTag term == _LAM_ = do
putStr "(cant-infer-lam)"
pure eraT
| tTag term == _APP_ = do
f <- field term 0
x <- field term 1
(x0, x1) <- makeDupFresh x
fType <- infer dep f
if tTag fType == _ERA_
then pure eraT
else do
fTypeNf <- whnf fType
if tTag fTypeNf /= _ALL_
then do
putStr "(non-fun-app)"
pure eraT
else do
a <- field fTypeNf 0
b <- field fTypeNf 1
xOk <- check dep x0 a
if tTag xOk == _ERA_
then pure eraT
else do
app <- makeNode _APP_ 0 [b, x1]
whnf app
| tTag term == _ANN_ = do
x <- field term 0
ty <- field term 1
rc <- check dep x ty
if tTag rc == _ERA_
then pure eraT
else pure ty
| otherwise = do
putStr $ "(cant-infer-unknown)"
pure eraT
-- Checking
check :: Int -> Term -> Term -> IO Term
check dep term0 goal0 = do
term <- whnf term0
goal <- whnf goal0
checkGo dep term goal
checkGo :: Int -> Term -> Term -> IO Term
checkGo dep term goal
| tTag term == _SUP_ = do
a <- field term 0
b <- field term 1
-- Use the SUP's label when duplicating goal
(goal0, goal1) <- makeDup (tLab term) goal
ra <- checkGo dep a goal0
rb <- checkGo dep b goal1
makeNode _SUP_ (tLab term) [ra, rb]
| tTag goal == _SUP_ = do
a <- field goal 0
b <- field goal 1
-- Use the SUP's label when duplicating term
(term0, term1) <- makeDup (tLab goal) term
ra <- checkGo dep term0 a
rb <- checkGo dep term1 b
makeNode _SUP_ (tLab goal) [ra, rb]
| tTag term == _ERA_ = do
pure nilT
| tTag term == _NIL_ && tTag goal == _UNI_ = do
pure nilT
| tTag term == _W32_ && tTag goal == _U32_ = do
pure nilT
| tTag term == _SET_ && tTag goal == _SET_ = do
pure nilT
| tTag term == _EMP_ && tTag goal == _SET_ = do
pure nilT
| tTag term == _UNI_ && tTag goal == _SET_ = do
pure nilT
| tTag term == _U32_ && tTag goal == _SET_ = do
pure nilT
| tTag term == _SIG_ && tTag goal == _SET_ = do
a <- field term 0
b <- field term 1
-- Duplicate 'a' before first use
(a0, a1) <- makeDupFresh a
aOk <- check dep a0 setT
if tTag aOk == _ERA_
then pure eraT
else do
lamT <- makeNode _LAM_ 0 [setT]
allT <- makeNode _ALL_ 0 [a1, lamT]
bOk <- check dep b allT
if tTag bOk == _ERA_
then pure eraT
else pure nilT
| tTag term == _ALL_ && tTag goal == _SET_ = do
a <- field term 0
b <- field term 1
aOk <- check dep a setT
if tTag aOk == _ERA_
then pure eraT
else do
lamT <- makeNode _LAM_ 0 [setT]
allT <- makeNode _ALL_ 0 [setT, lamT]
bOk <- check dep b allT
if tTag bOk == _ERA_
then pure eraT
else pure nilT
| tTag term == _LAM_ && tTag goal == _ALL_ = do
print "a"
f <- field term 0
a <- field goal 0
b <- field goal 1
(a0, a1) <- makeDupFresh a
-- Create fresh variables for the lambda binding
var0 <- makeNode _VAR_ (fromIntegral dep) []
var1 <- makeNode _VAR_ (fromIntegral dep) []
-- Annotate variables with types
ann0 <- makeNode _ANN_ 0 [var0, a0]
ann1 <- makeNode _ANN_ 0 [var1, a1]
-- Apply function body and type body to variable
appF <- makeNode _APP_ 0 [f, ann0]
appB <- makeNode _APP_ 0 [b, ann1]
appB_nf <- whnf appB
print $ showTerm b
-- Check with increased depth
check (dep + 1) appF appB_nf
| tTag term == _TUP_ && tTag goal == _SIG_ = do
a <- field term 0
b <- field term 1
aTy <- field goal 0
bTy <- field goal 1
-- Duplicate 'a' before first use
(a0, a1) <- makeDupFresh a
-- Check first component
aOk <- check dep a0 aTy
if tTag aOk == _ERA_
then pure eraT
else do
-- Apply dependent type to first component
app <- makeNode _APP_ 0 [bTy, a1]
bTyA <- whnf app
-- Check second component
bOk <- check dep b bTyA
if tTag bOk == _ERA_
then pure eraT
else pure nilT
| tTag term == _EFQ_ = do
c <- field term 0
rc <- check dep c empT
if tTag rc == _ERA_
then pure eraT
else pure nilT
| tTag term == _USE_ = do
c <- field term 0
f <- field term 1
rc <- check dep c uniT
if tTag rc == _ERA_
then pure eraT
else do
rf <- check dep f goal
if tTag rf == _ERA_
then pure eraT
else pure nilT
| tTag term == _GET_ = do
c <- field term 0
f <- field term 1
cType <- infer dep c
if tTag cType == _ERA_
then pure eraT
else do
cTypeNf <- whnf cType
if tTag cTypeNf /= _SIG_
then do
putStr "(expected-pair-type)"
pure eraT
else do
rf <- check dep f goal
if tTag rf == _ERA_
then pure eraT
else pure nilT
| tTag term == _SWI_ = do
c <- field term 0
z <- field term 1
s <- field term 2
rc <- check dep c u32T
if tTag rc == _ERA_
then pure eraT
else do
-- Get a fresh label for duplicating the goal
freshLab <- getFreshLabel
(goal0, goal1) <- makeDup freshLab goal
rz <- check dep z goal0
if tTag rz == _ERA_
then pure eraT
else do
rs <- check dep s goal1
if tTag rs == _ERA_
then pure eraT
else pure nilT
| otherwise = do
ty <- infer dep term
if tTag ty == _ERA_
then pure eraT
else do
eq <- equal dep ty goal
if tTag eq == _NIL_
then pure nilT
else do
putStr "(type-mismatch)"
pure eraT
-- PROBLEM: I'm trying to type-check the following file:
-- @main = <λx.123 : ∀x:U32.U32>
-- But I get the following error:
-- Press ENTER or type command to continue
-- <λa.123 : ∀U32.λb.U32>
-- Checking @main... "a"
-- "term_new(LAM,0x000000,0x0000000c)"
-- invalid:app-w32 1.02 real 0.76 user 0.10 sys
-- Why?
just answer below why this bug is happening and nothing else
The bug "invalid:app-w32" occurs because the term (123 ann0) (where 123 is the body of the lambda λx.123, and ann0 is a fresh annotated variable representing x:U32) is being evaluated by whnf (via Reduce.hs or Runtime.c). The Interaction Calculus runtime (and HVM) does not allow a number (like 123, a W32 term) to be in the function position of an application; this is a runtime error.
Here's the trace of why this happens in your Check.hs:
Initial Check: You are checking @main = <λx.123 : ∀x:U32.U32>. The inferGo rule for _ANN_ is invoked.
x (term being annotated) = λx.123
ty (the annotation type) = ∀x:U32.U32
This rule calls: check dep (λx.123) (∀x:U32.U32)
check function call:
check :: Int -> Term -> Term -> IO Term
check dep term0 goal0 = do
term <- whnf term0 -- term0 is λx.123. whnf(λx.123) is λx.123. (OK so far)
goal <- whnf goal0 -- goal0 is ∀x:U32.U32. whnf(∀x:U32.U32) is ∀x:U32.U32. (OK so far)
checkGo dep term goal
Use code with caution.
Haskell
So, checkGo dep (λx.123) (∀x:U32.U32) is called.
checkGo for _LAM_ and _ALL_: This rule matches.
term = λx.123
goal = ∀x:U32.U32
Inside this rule:
f (lambda body) = 123
a (quantified type in ∀) = U32
b (type body in ∀) = λb'.U32 (where b' is the type variable)
An application appF is constructed: appF = (f ann0) = (123 ann0).
A type appB_nf is constructed (and normalized): appB_nf = whnf((b ann1)) = U32.
Then, a recursive call to check is made: check (dep + 1) appF appB_nf, which is check (dep + 1) (123 ann0) U32.
Recursive check function call:
term0 is now (123 ann0).
goal0 is now U32.
check :: Int -> Term -> Term -> IO Term
check dep term0 goal0 = do
term <- whnf term0 -- HERE IS THE PROBLEM: term0 is (123 ann0).
-- whnf((123 ann0)) is called.
-- The HVM runtime attempts to reduce (123 ann0).
-- Since 123 is a W32, this triggers the reduce_app_w32 rule,
-- which prints "invalid:app-w32" and exits.
goal <- whnf goal0
checkGo dep term goal
Use code with caution.
Haskell
The whnf call on term0 at the beginning of your check function (and similarly in your infer function) is too eager. It attempts to normalize the term being checked before its syntactic structure is analyzed by checkGo. When checkGo's LAM-ALL rule constructs an application appF that would be ill-formed at runtime (like applying a number), and this appF is passed back to check, this initial whnf call triggers the runtime error.
The type checker should instead try to infer the type of (123 ann0). The inferGo rule for _APP_ would find that 123 has type U32, which is not a function type (∀...), and correctly report a type error like "(non-fun-app)" without trying to evaluate (123 ann0). This requires infer (and check) not to whnf their main term argument immediately upon entry, but rather pass it structurally to inferGo/checkGo, which can then decide if whnf is needed for specific sub-parts or specific rules.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment