Skip to content

Instantly share code, notes, and snippets.

@VictorTaelin

VictorTaelin/question.txt

Created May 6, 2025 21:55
Show Gist options
  • Save VictorTaelin/0272a84276154563d004a45e243dcc47 to your computer and use it in GitHub Desktop.
Save VictorTaelin/0272a84276154563d004a45e243dcc47 to your computer and use it in GitHub Desktop.
Download ZIP
Insanely hard prompt - question and answer
Raw
question.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
_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
_VAL_ = 0x1A :: 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 == _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"
| tag == _VAL_ = "VAL"
| 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,...)}
{-./Type.hs-}
module Inject where
import Control.Monad (foldM, when, forM_)
import Control.Monad.State
import Data.Bits (shiftL, (.|.))
import Data.Char (ord)
import Data.List (foldr)
import Data.Word
import Debug.Trace
import Foreign
import Type
import qualified Data.Map.Strict as MS
type InjectM a = StateT InjectState HVM a
data InjectState = InjectState
{ args :: MS.Map String Term -- maps var names to binder locations
, vars :: [(String, Loc)] -- list of (var name, usage location) pairs
}
emptyState :: InjectState
emptyState = InjectState MS.empty []
-- injectCore :: Book -> Core -> Loc -> InjectM ()
-- injectCore _ Era loc = do
-- lift $ set loc (termNew _ERA_ 0 0)
-- injectCore _ (Var nam) loc = do
-- argsMap <- gets args
-- case MS.lookup nam argsMap of
-- Just term -> do
-- lift $ set loc term
-- when (head nam /= '&') $ do
-- modify $ \s -> s { args = MS.delete nam (args s) }
-- Nothing -> do
-- modify $ \s -> s { vars = (nam, loc) : vars s }
-- injectCore book (Let mod nam val bod) loc = do
-- let_node <- lift $ allocNode 2
-- modify $ \s -> s { args = MS.insert nam (termNew _VAR_ 0 (let_node + 0)) (args s) }
-- injectCore book val (let_node + 0)
-- injectCore book bod (let_node + 1)
-- lift $ set loc (termNew _LET_ (fromIntegral $ fromEnum mod) let_node)
-- injectCore book (Lam vr0 bod) loc = do
-- lam <- lift $ allocNode 1
-- modify $ \s -> s { args = MS.insert vr0 (termNew _VAR_ 0 (lam + 0)) (args s) }
-- injectCore book bod (lam + 0)
-- lift $ set loc (termNew _LAM_ 0 lam)
-- injectCore book (App fun arg) loc = do
-- app <- lift $ allocNode 2
-- injectCore book fun (app + 0)
-- injectCore book arg (app + 1)
-- lift $ set loc (termNew _APP_ 0 app)
-- injectCore book (Sup lab tm0 tm1) loc = do
-- sup <- lift $ allocNode 2
-- injectCore book tm0 (sup + 0)
-- injectCore book tm1 (sup + 1)
-- lift $ set loc (termNew _SUP_ lab sup)
-- injectCore book (Dup lab dp0 dp1 val bod) loc = do
-- dup <- lift $ allocNode 1
-- modify $ \s -> s
-- { args = MS.insert dp0 (termNew _DP0_ lab dup)
-- $ MS.insert dp1 (termNew _DP1_ lab dup) (args s)
-- }
-- injectCore book val (dup + 0)
-- injectCore book bod loc
-- injectCore book (Ref nam fid arg) loc = do
-- let ari = funArity book fid
-- let lab = fromIntegral fid
-- when (ari /= fromIntegral (length arg)) $ do
-- error $ "Arity mismatch on term: " ++ show (Ref nam fid arg) ++ ". Expected " ++ show ari ++ ", got " ++ show (length arg) ++ "."
-- ref <- lift $ allocNode (fromIntegral ari)
-- sequence_ [injectCore book x (ref + i) | (i,x) <- zip [0..] arg]
-- lift $ set loc (termNew _REF_ lab ref)
-- injectCore book (Ctr nam fds) loc = do
-- let ari = length fds
-- let cid = mget (ctrToCid book) nam
-- let lab = fromIntegral cid
-- ctr <- lift $ allocNode (fromIntegral ari)
-- sequence_ [injectCore book fd (ctr + ix) | (ix,fd) <- zip [0..] fds]
-- lift $ set loc (termNew _CTR_ lab ctr)
-- injectCore book tm@(Mat kin val mov css) loc = do
-- mat <- lift $ allocNode (1 + fromIntegral (length css))
-- injectCore book val (mat + 0)
-- forM_ (zip [0..] css) $ \ (idx, (ctr, fds, bod)) -> do
-- injectCore book (foldr (\x b -> Lam x b) (foldr (\x b -> Lam x b) bod (map fst mov)) fds) (mat + 1 + fromIntegral idx)
-- let tag = case kin of { SWI -> _SWI_ ; (MAT _) -> _MAT_ ; (IFL _) -> _IFL_ }
-- let lab = case kin of { SWI -> fromIntegral $ length css ; (MAT cid) -> fromIntegral cid ; (IFL cid) -> fromIntegral cid }
-- trm <- return $ termNew tag lab mat
-- ret <- foldM (\mat (_, val) -> do
-- app <- lift $ allocNode 2
-- lift $ set (app + 0) mat
-- injectCore book val (app + 1)
-- return $ termNew _APP_ 0 app)
-- trm
-- mov
-- lift $ set loc ret
-- injectCore book (W32 val) loc = do
-- lift $ set loc (termNew _W32_ 0 (fromIntegral val))
-- injectCore book (Chr val) loc = do
-- lift $ set loc (termNew _CHR_ 0 (fromIntegral $ ord val))
-- injectCore book (Op2 opr nm0 nm1) loc = do
-- opx <- lift $ allocNode 2
-- injectCore book nm0 (opx + 0)
-- injectCore book nm1 (opx + 1)
-- lift $ set loc (termNew _OPX_ (fromIntegral $ fromEnum opr) opx)
-- injectCore _ Set loc = do
-- lift $ set loc (termNew _SET_ 0 0)
-- injectCore book (All typ bod) loc = do
-- all_node <- lift $ allocNode 2
-- injectCore book typ (all_node + 0)
-- injectCore book bod (all_node + 1)
-- lift $ set loc (termNew _ALL_ 0 all_node)
-- injectCore book (Adt nam fds) loc = do
-- let ari = length fds
-- let cid = mget (ctrToCid book) nam
-- let lab = fromIntegral cid
-- adt <- lift $ allocNode (fromIntegral ari)
-- sequence_ [injectCore book fd (adt + ix) | (ix,fd) <- zip [0..] fds]
-- lift $ set loc (termNew _ADT_ lab adt)
-- injectCore _ U32 loc = do
-- lift $ set loc (termNew _W32_ 0 0)
-- doInjectCoreAt :: Book -> Core -> Loc -> [(String,Term)] -> HVM Term
-- doInjectCoreAt book core host argList = do
-- (_, state) <- runStateT (injectCore book core host) (emptyState { args = MS.fromList argList })
-- foldM (\m (name, loc) -> do
-- case MS.lookup name (args state) of
-- Just term -> do
-- set loc term
-- return $ MS.delete name m
-- Nothing -> do
-- error $ "Unbound variable: \n\x1b[2m" ++ name ++ "\n\x1b[0mIn term:\n\x1b[2m" ++ Data.List.take 1024 (show core) ++ "...\x1b[0m")
-- (args state)
-- (vars state)
-- got host
-- UPDATED:
injectCore :: Book -> Core -> Loc -> InjectM ()
injectCore _ Era loc = do
lift $ set loc (termNew _ERA_ 0 0)
injectCore _ (Var x) loc = do
argsMap <- gets args
case MS.lookup x argsMap of
Just term -> do
lift $ set loc term
when (head x /= '&') $ do
modify $ \s -> s { args = MS.delete x (args s) }
Nothing -> do
modify $ \s -> s { vars = (x, loc) : vars s }
injectCore book (Ref x i xs) loc = do
let ari = funArity book i
let lab = fromIntegral i
when (ari /= fromIntegral (length xs)) $ do
error $ "Arity mismatch on term: " ++ show (Ref x i xs) ++ ". Expected " ++ show ari ++ ", got " ++ show (length xs) ++ "."
ref <- lift $ allocNode (fromIntegral ari)
sequence_ [injectCore book x (ref + i) | (i,x) <- zip [0..] xs]
lift $ set loc (termNew _REF_ lab ref)
injectCore book (Let m x v f) loc = do
let_node <- lift $ allocNode 2
modify $ \s -> s { args = MS.insert x (termNew _VAR_ 0 (let_node + 0)) (args s) }
injectCore book v (let_node + 0)
injectCore book f (let_node + 1)
lift $ set loc (termNew _LET_ (fromIntegral $ fromEnum m) let_node)
injectCore _ Era loc = do
lift $ set loc (termNew _ERA_ 0 0)
injectCore book (Sup l a b) loc = do
sup <- lift $ allocNode 2
injectCore book a (sup + 0)
injectCore book b (sup + 1)
lift $ set loc (termNew _SUP_ l sup)
injectCore book (Dup l x y v f) loc = do
dup <- lift $ allocNode 1
modify $ \s -> s
{ args = MS.insert x (termNew _DP0_ l dup)
$ MS.insert y (termNew _DP1_ l dup) (args s)
}
injectCore book v (dup + 0)
injectCore book f loc
injectCore _ Set loc = do
lift $ set loc (termNew _SET_ 0 0)
injectCore _ Emp loc = do
lift $ set loc (termNew _EMP_ 0 0)
injectCore book (Efq c ms) loc = do
efq <- lift $ allocNode 1
injectCore book c (efq + 0)
applyMoves book (termNew _EFQ_ 0 efq) ms loc
injectCore _ Uni loc = do
lift $ set loc (termNew _UNI_ 0 0)
injectCore _ Nil loc = do
lift $ set loc (termNew _NIL_ 0 0)
injectCore book (Use c ms b) loc = do
use <- lift $ allocNode 2
injectCore book c (use + 0)
injectCore book b (use + 1)
applyMoves book (termNew _USE_ 0 use) ms loc
injectCore _ U32 loc = do
lift $ set loc (termNew _U32_ 0 0)
injectCore _ (W32 n) loc = do
lift $ set loc (termNew _W32_ 0 (fromIntegral n))
injectCore book (Swi c ms z s) loc = do
swi <- lift $ allocNode 3
injectCore book c (swi + 0)
injectCore book z (swi + 1)
injectCore book s (swi + 2)
applyMoves book (termNew _SWI_ 0 swi) ms loc
injectCore book (Op2 o a b) loc = do
opx <- lift $ allocNode 2
injectCore book a (opx + 0)
injectCore book b (opx + 1)
lift $ set loc (termNew _OPX_ (fromIntegral $ fromEnum o) opx)
injectCore book (Sig _A _B) loc = do
sig <- lift $ allocNode 2
injectCore book _A (sig + 0)
injectCore book _B (sig + 1)
lift $ set loc (termNew _SIG_ 0 sig)
injectCore book (Tup a b) loc = do
tup <- lift $ allocNode 2
injectCore book a (tup + 0)
injectCore book b (tup + 1)
lift $ set loc (termNew _TUP_ 0 tup)
injectCore book (Get c ms b) loc = do
get <- lift $ allocNode 2
injectCore book c (get + 0)
injectCore book b (get + 1)
applyMoves book (termNew _GET_ 0 get) ms loc
injectCore book (All _A _B) loc = do
all_node <- lift $ allocNode 2
injectCore book _A (all_node + 0)
injectCore book _B (all_node + 1)
lift $ set loc (termNew _ALL_ 0 all_node)
injectCore book (Lam x f) loc = do
lam <- lift $ allocNode 1
modify $ \s -> s { args = MS.insert x (termNew _VAR_ 0 (lam + 0)) (args s) }
injectCore book f (lam + 0)
lift $ set loc (termNew _LAM_ 0 lam)
injectCore book (App f x) loc = do
app <- lift $ allocNode 2
injectCore book f (app + 0)
injectCore book x (app + 1)
lift $ set loc (termNew _APP_ 0 app)
injectCore book (Ann c x t) loc = do
ann <- lift $ allocNode 2
injectCore book x (ann + 0)
injectCore book t (ann + 1)
lift $ set loc (termNew _ANN_ (if c then 1 else 0) ann)
applyMoves :: Book -> Term -> [Move] -> Loc -> InjectM ()
applyMoves book base ms loc = do
result <- foldM (\term (_, v) -> do
app <- lift $ allocNode 2
lift $ set (app + 0) term
injectCore book v (app + 1)
return $ termNew _APP_ 0 app)
base
ms
lift $ set loc result
doInjectCoreAt :: Book -> Core -> Loc -> [(String,Term)] -> HVM Term
doInjectCoreAt book core host argList = do
(_, state) <- runStateT (injectCore book core host) (emptyState { args = MS.fromList argList })
_ <- foldM (\m (name, loc) -> do
case MS.lookup name m of
Just term -> do
set loc term
return $ MS.delete name m
Nothing -> do
error $ "Unbound variable: \n\x1b[2m" ++ name ++ "\n\x1b[0mIn term:\n\x1b[2m" ++ Prelude.take 1024 (show core) ++ "...\x1b[0m")
(args state)
(vars state)
got host
{-./Type.hs-}
{-./Foreign.hs-}
-- module Reduce where
-- import Control.Monad (when, forM, forM_)
-- import Data.Word
-- import Collapse
-- import Extract
-- import Foreign
-- import Inject
-- import Type
-- import System.Exit
-- import qualified Data.Map.Strict as MS
-- reduceAt :: Bool -> (Book -> Loc -> HVM Term)
-- reduceAt debug book host = do
-- term <- got host
-- let tag = termTag term
-- let lab = termLab term
-- let loc = termLoc term
-- when debug $ do
-- root <- doExtractCoreAt gotT book 0
-- core <- doExtractCoreAt gotT book host
-- putStrLn $ "reduce: " ++ showTerm term
-- -- putStrLn $ "---------------- CORE: "
-- -- putStrLn $ showCore core
-- putStrLn $ "---------------- ROOT: "
-- putStrLn $ showCore (doLiftDups root)
-- case tag of
-- t | t == _LET_ -> do
-- case modeT lab of
-- LAZY -> do
-- val <- got (loc + 0)
-- cont host (reduceLet term val)
-- STRI -> do
-- val <- reduceAt debug book (loc + 0)
-- cont host (reduceLet term val)
-- t | t == _APP_ -> do
-- fun <- reduceAt debug book (loc + 0)
-- case termTag fun of
-- t | t == _ERA_ -> cont host (reduceAppEra term fun)
-- t | t == _LAM_ -> cont host (reduceAppLam term fun)
-- t | t == _SUP_ -> cont host (reduceAppSup term fun)
-- t | t == _CTR_ -> cont host (reduceAppCtr term fun)
-- t | t == _W32_ -> cont host (reduceAppW32 term fun)
-- t | t == _CHR_ -> cont host (reduceAppW32 term fun)
-- _ -> set (loc + 0) fun >> return term
-- t | t == _MAT_ -> do
-- val <- reduceAt debug book (loc + 0)
-- case termTag val of
-- t | t == _ERA_ -> cont host (reduceMatEra term val)
-- t | t == _LAM_ -> cont host (reduceMatLam term val)
-- t | t == _SUP_ -> cont host (reduceMatSup term val)
-- t | t == _CTR_ -> cont host (reduceMatCtr term val)
-- t | t == _W32_ -> cont host (reduceMatW32 term val)
-- t | t == _CHR_ -> cont host (reduceMatW32 term val)
-- _ -> set (loc + 0) val >> return term
-- t | t == _IFL_ -> do
-- val <- reduceAt debug book (loc + 0)
-- case termTag val of
-- t | t == _ERA_ -> cont host (reduceMatEra term val)
-- t | t == _LAM_ -> cont host (reduceMatLam term val)
-- t | t == _SUP_ -> cont host (reduceMatSup term val)
-- t | t == _CTR_ -> cont host (reduceMatCtr term val)
-- t | t == _W32_ -> cont host (reduceMatW32 term val)
-- t | t == _CHR_ -> cont host (reduceMatW32 term val)
-- _ -> set (loc + 0) val >> return term
-- t | t == _SWI_ -> do
-- val <- reduceAt debug book (loc + 0)
-- case termTag val of
-- t | t == _ERA_ -> cont host (reduceMatEra term val)
-- t | t == _LAM_ -> cont host (reduceMatLam term val)
-- t | t == _SUP_ -> cont host (reduceMatSup term val)
-- t | t == _CTR_ -> cont host (reduceMatCtr term val)
-- t | t == _W32_ -> cont host (reduceMatW32 term val)
-- t | t == _CHR_ -> cont host (reduceMatW32 term val)
-- _ -> set (loc + 0) val >> return term
-- t | t == _OPX_ -> do
-- val <- reduceAt debug book (loc + 0)
-- case termTag val of
-- t | t == _ERA_ -> cont host (reduceOpxEra term val)
-- t | t == _LAM_ -> cont host (reduceOpxLam term val)
-- t | t == _SUP_ -> cont host (reduceOpxSup term val)
-- t | t == _CTR_ -> cont host (reduceOpxCtr term val)
-- t | t == _W32_ -> cont host (reduceOpxW32 term val)
-- t | t == _CHR_ -> cont host (reduceOpxW32 term val)
-- _ -> set (loc + 0) val >> return term
-- t | t == _OPY_ -> do
-- val <- reduceAt debug book (loc + 0)
-- case termTag val of
-- t | t == _ERA_ -> cont host (reduceOpyEra term val)
-- t | t == _LAM_ -> cont host (reduceOpyLam term val)
-- t | t == _SUP_ -> cont host (reduceOpySup term val)
-- t | t == _CTR_ -> cont host (reduceOpyCtr term val)
-- t | t == _W32_ -> cont host (reduceOpyW32 term val)
-- t | t == _CHR_ -> cont host (reduceOpyW32 term val)
-- _ -> set (loc + 0) val >> return term
-- t | t == _DP0_ -> do
-- sb0 <- got (loc + 0)
-- if termGetBit sb0 == 0
-- then do
-- val <- reduceAt debug book (loc + 0)
-- case termTag val of
-- t | t == _ERA_ -> cont host (reduceDupEra term val)
-- t | t == _LAM_ -> cont host (reduceDupLam term val)
-- t | t == _SUP_ -> cont host (reduceDupSup term val)
-- t | t == _CTR_ -> cont host (reduceDupCtr term val)
-- t | t == _W32_ -> cont host (reduceDupW32 term val)
-- t | t == _CHR_ -> cont host (reduceDupW32 term val)
-- _ -> set (loc + 0) val >> return term
-- else do
-- set host (termRemBit sb0)
-- reduceAt debug book host
-- t | t == _DP1_ -> do
-- sb1 <- got (loc + 0)
-- if termGetBit sb1 == 0
-- then do
-- val <- reduceAt debug book (loc + 0)
-- case termTag val of
-- t | t == _ERA_ -> cont host (reduceDupEra term val)
-- t | t == _LAM_ -> cont host (reduceDupLam term val)
-- t | t == _SUP_ -> cont host (reduceDupSup term val)
-- t | t == _CTR_ -> cont host (reduceDupCtr term val)
-- t | t == _W32_ -> cont host (reduceDupW32 term val)
-- t | t == _CHR_ -> cont host (reduceDupW32 term val)
-- _ -> set (loc + 0) val >> return term
-- else do
-- set host (termRemBit sb1)
-- reduceAt debug book host
-- t | t == _VAR_ -> do
-- sub <- got (loc + 0)
-- if termGetBit sub == 0
-- then return term
-- else do
-- set host (termRemBit sub)
-- reduceAt debug book host
-- t | t == _REF_ -> do
-- reduceRefAt book host
-- reduceAt debug book host
-- _ -> do
-- return term
-- where
-- cont host action = do
-- ret <- action
-- set host ret
-- reduceAt debug book host
-- gotT :: Book -> Loc -> HVM Term
-- gotT book host = got host
-- reduceRefAt :: Book -> Loc -> HVM Term
-- reduceRefAt book host = do
-- term <- got host
-- let lab = termLab term
-- let loc = termLoc term
-- let fid = fromIntegral lab
-- let ari = funArity book fid
-- case lab of
-- x | x == _DUP_F_ -> reduceRefAt_DupF book host loc ari
-- x | x == _SUP_F_ -> reduceRefAt_SupF book host loc ari
-- x | x == _LOG_F_ -> reduceRefAt_LogF book host loc ari
-- otherwise -> case MS.lookup fid (fidToFun book) of
-- Just ((copy, args), core) -> do
-- incItr
-- when (length args /= fromIntegral ari) $ do
-- putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@" ++ mget (fidToNam book) fid ++ "'."
-- exitFailure
-- argTerms <- if ari == 0
-- then return []
-- else forM (zip [0..] args) $ \(i, (strict, _)) -> do
-- term <- got (loc + i)
-- if strict
-- then reduceAt False book (loc + i)
-- else return term
-- doInjectCoreAt book core host $ zip (map snd args) argTerms
-- Nothing -> do
-- putStrLn $ "RUNTIME_ERROR: Function ID " ++ show fid ++ " not found in fidToFun book."
-- exitFailure
-- -- Primitive: Dynamic Dup `@DUP(lab val λdp0λdp1(bod))`
-- reduceRefAt_DupF :: Book -> Loc -> Loc -> Word16 -> HVM Term
-- reduceRefAt_DupF book host loc ari = do
-- incItr
-- when (ari /= 3) $ do
-- putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@DUP'."
-- exitFailure
-- lab <- reduceAt False book (loc + 0)
-- val <- got (loc + 1)
-- bod <- got (loc + 2)
-- dup <- allocNode 1
-- case termTag lab of
-- t | t == _W32_ -> do
-- when (termLoc lab > 0xFFFFFF) $ do
-- error "RUNTIME_ERROR: dynamic DUP label too large"
-- -- Create the DUP node with value
-- set (dup + 0) val
-- -- Create first APP node for (APP bod DP0)
-- app1 <- allocNode 2
-- set (app1 + 0) bod
-- set (app1 + 1) (termNew _DP0_ (termLoc lab) dup)
-- -- Create second APP node for (APP (APP bod DP0) DP1)
-- app2 <- allocNode 2
-- set (app2 + 0) (termNew _APP_ 0 app1)
-- set (app2 + 1) (termNew _DP1_ (termLoc lab) dup)
-- let ret = termNew _APP_ 0 app2
-- set host ret
-- return ret
-- _ -> do
-- core <- doExtractCoreAt gotT book (loc + 0)
-- putStrLn $ "RUNTIME_ERROR: dynamic DUP without numeric label: " ++ showTerm lab
-- putStrLn $ showCore (doLiftDups core)
-- exitFailure
-- -- Primitive: Dynamic Sup `@SUP(lab tm0 tm1)`
-- reduceRefAt_SupF :: Book -> Loc -> Loc -> Word16 -> HVM Term
-- reduceRefAt_SupF book host loc ari = do
-- incItr
-- when (ari /= 3) $ do
-- putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@SUP'."
-- exitFailure
-- lab <- reduceAt False book (loc + 0)
-- tm0 <- got (loc + 1)
-- tm1 <- got (loc + 2)
-- sup <- allocNode 2
-- case termTag lab of
-- t | t == _W32_ -> do
-- when (termLoc lab > 0xFFFFFF) $ do
-- error "RUNTIME_ERROR: dynamic SUP label too large"
-- let ret = termNew _SUP_ (termLoc lab) sup
-- set (sup + 0) tm0
-- set (sup + 1) tm1
-- set host ret
-- return ret
-- _ -> error "RUNTIME_ERROR: dynamic SUP without numeric label."
-- -- Primitive: Logger `@LOG(msg)`
-- -- Will extract the term and log it.
-- -- Returns 0.
-- reduceRefAt_LogF :: Book -> Loc -> Loc -> Word16 -> HVM Term
-- reduceRefAt_LogF book host loc ari = do
-- incItr
-- when (ari /= 1) $ do
-- putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@LOG'."
-- exitFailure
-- msg <- doExtractCoreAt gotT book (loc + 0)
-- putStrLn $ showCore (doLiftDups msg)
-- -- msgs <- doCollapseFlatAt gotT book (loc + 0)
-- -- forM_ msgs $ \msg -> do
-- -- putStrLn $ showCore msg
-- let ret = termNew _W32_ 0 0
-- set host ret
-- return ret
-- -- Primitive: Fresh `@FRESH`
-- -- Returns a fresh dup label.
-- reduceRefAt_FreshF :: Book -> Loc -> Loc -> Word16 -> HVM Term
-- reduceRefAt_FreshF book host loc ari = do
-- incItr
-- when (ari /= 0) $ do
-- putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@Fresh'."
-- exitFailure
-- num <- fromIntegral <$> fresh
-- let ret = termNew _W32_ 0 num
-- set host ret
-- return ret
-- reduceCAt :: Bool -> (Book -> Loc -> HVM Term)
-- reduceCAt = \ _ _ host -> reduceAtC host
-- UPDATED:
module Reduce where
import Control.Monad (when, forM, forM_)
import Data.Word
import Collapse
import Extract
import Foreign
import Inject
import Type
import System.Exit
import qualified Data.Map.Strict as MS
reduceAt :: Bool -> Book -> Loc -> HVM Term
reduceAt debug book host = do
term <- got host
let tag = termTag term
let lab = termLab term
let loc = termLoc term
when debug $ do
root <- doExtractCoreAt gotT book 0
core <- doExtractCoreAt gotT book host
putStrLn $ "reduce: " ++ showTerm term
-- putStrLn $ "---------------- CORE: "
-- putStrLn $ showCore core
putStrLn $ "---------------- ROOT: "
putStrLn $ showCore (doLiftDups root)
case tag of
t | t == _LET_ -> do
case modeT lab of
LAZY -> do
val <- got (loc + 0)
cont host (reduceLet term val)
STRI -> do
val <- reduceAt debug book (loc + 0)
cont host (reduceLet term val)
t | t == _APP_ -> do
fun <- reduceAt debug book (loc + 0)
case termTag fun of
t | t == _ERA_ -> cont host (reduceAppEra term fun)
t | t == _LAM_ -> cont host (reduceAppLam term fun)
t | t == _SUP_ -> cont host (reduceAppSup term fun)
t | t == _NIL_ -> cont host (reduceAppNil term fun)
t | t == _TUP_ -> cont host (reduceAppTup term fun)
t | t == _W32_ -> cont host (reduceAppW32 term fun)
t | t == _SET_ -> cont host (reduceAppTyp term fun)
t | t == _EMP_ -> cont host (reduceAppTyp term fun)
t | t == _UNI_ -> cont host (reduceAppTyp term fun)
t | t == _U32_ -> cont host (reduceAppTyp term fun)
t | t == _SIG_ -> cont host (reduceAppTyp term fun)
t | t == _ALL_ -> cont host (reduceAppTyp term fun)
_ -> set (loc + 0) fun >> return term
t | t == _USE_ -> do
val <- reduceAt debug book (loc + 0)
case termTag val of
t | t == _ERA_ -> cont host (reduceUseEra term val)
t | t == _SUP_ -> cont host (reduceUseSup term val)
t | t == _LAM_ -> cont host (reduceUseLam term val)
t | t == _NIL_ -> cont host (reduceUseNil term val)
t | t == _TUP_ -> cont host (reduceUseTup term val)
t | t == _W32_ -> cont host (reduceUseW32 term val)
t | t == _SET_ -> cont host (reduceUseTyp term val)
t | t == _EMP_ -> cont host (reduceUseTyp term val)
t | t == _UNI_ -> cont host (reduceUseTyp term val)
t | t == _U32_ -> cont host (reduceUseTyp term val)
t | t == _SIG_ -> cont host (reduceUseTyp term val)
t | t == _ALL_ -> cont host (reduceUseTyp term val)
_ -> set (loc + 0) val >> return term
t | t == _GET_ -> do
val <- reduceAt debug book (loc + 0)
case termTag val of
t | t == _ERA_ -> cont host (reduceGetEra term val)
t | t == _SUP_ -> cont host (reduceGetSup term val)
t | t == _NIL_ -> cont host (reduceGetNil term val)
t | t == _TUP_ -> cont host (reduceGetTup term val)
t | t == _LAM_ -> cont host (reduceGetLam term val)
t | t == _W32_ -> cont host (reduceGetW32 term val)
t | t == _SET_ -> cont host (reduceGetTyp term val)
t | t == _EMP_ -> cont host (reduceGetTyp term val)
t | t == _UNI_ -> cont host (reduceGetTyp term val)
t | t == _U32_ -> cont host (reduceGetTyp term val)
t | t == _SIG_ -> cont host (reduceGetTyp term val)
t | t == _ALL_ -> cont host (reduceGetTyp term val)
_ -> set (loc + 0) val >> return term
t | t == _SWI_ -> do
val <- reduceAt debug book (loc + 0)
case termTag val of
t | t == _ERA_ -> cont host (reduceSwiEra term val)
t | t == _SUP_ -> cont host (reduceSwiSup term val)
t | t == _NIL_ -> cont host (reduceSwiNil term val)
t | t == _TUP_ -> cont host (reduceSwiTup term val)
t | t == _LAM_ -> cont host (reduceSwiLam term val)
t | t == _W32_ -> cont host (reduceSwiW32 term val)
t | t == _SET_ -> cont host (reduceSwiTyp term val)
t | t == _EMP_ -> cont host (reduceSwiTyp term val)
t | t == _UNI_ -> cont host (reduceSwiTyp term val)
t | t == _U32_ -> cont host (reduceSwiTyp term val)
t | t == _SIG_ -> cont host (reduceSwiTyp term val)
t | t == _ALL_ -> cont host (reduceSwiTyp term val)
_ -> set (loc + 0) val >> return term
t | t == _OPX_ -> do
val <- reduceAt debug book (loc + 0)
case termTag val of
t | t == _ERA_ -> cont host (reduceOpxEra term val)
t | t == _LAM_ -> cont host (reduceOpxLam term val)
t | t == _SUP_ -> cont host (reduceOpxSup term val)
t | t == _NIL_ -> cont host (reduceOpxNil term val)
t | t == _TUP_ -> cont host (reduceOpxTup term val)
t | t == _W32_ -> cont host (reduceOpxW32 term val)
t | t == _SET_ -> cont host (reduceOpxTyp term val)
t | t == _EMP_ -> cont host (reduceOpxTyp term val)
t | t == _UNI_ -> cont host (reduceOpxTyp term val)
t | t == _U32_ -> cont host (reduceOpxTyp term val)
t | t == _SIG_ -> cont host (reduceOpxTyp term val)
t | t == _ALL_ -> cont host (reduceOpxTyp term val)
_ -> set (loc + 0) val >> return term
t | t == _OPY_ -> do
val <- reduceAt debug book (loc + 0)
case termTag val of
t | t == _ERA_ -> cont host (reduceOpyEra term val)
t | t == _LAM_ -> cont host (reduceOpyLam term val)
t | t == _SUP_ -> cont host (reduceOpySup term val)
t | t == _NIL_ -> cont host (reduceOpyNil term val)
t | t == _TUP_ -> cont host (reduceOpyTup term val)
t | t == _W32_ -> cont host (reduceOpyW32 term val)
t | t == _SET_ -> cont host (reduceOpyTyp term val)
t | t == _EMP_ -> cont host (reduceOpyTyp term val)
t | t == _UNI_ -> cont host (reduceOpyTyp term val)
t | t == _U32_ -> cont host (reduceOpyTyp term val)
t | t == _SIG_ -> cont host (reduceOpyTyp term val)
t | t == _ALL_ -> cont host (reduceOpyTyp term val)
_ -> set (loc + 0) val >> return term
t | t == _DP0_ -> do
sb0 <- got (loc + 0)
if termGetBit sb0 == 0
then do
val <- reduceAt debug book (loc + 0)
case termTag val of
t | t == _ERA_ -> cont host (reduceDupEra term val)
t | t == _LAM_ -> cont host (reduceDupLam term val)
t | t == _SUP_ -> cont host (reduceDupSup term val)
t | t == _NIL_ -> cont host (reduceDupNil term val)
t | t == _TUP_ -> cont host (reduceDupTup term val)
t | t == _W32_ -> cont host (reduceDupW32 term val)
t | t == _SET_ -> cont host (reduceDupSet term val)
t | t == _EMP_ -> cont host (reduceDupEmp term val)
t | t == _UNI_ -> cont host (reduceDupUni term val)
t | t == _U32_ -> cont host (reduceDupU32 term val)
t | t == _SIG_ -> cont host (reduceDupSig term val)
t | t == _ALL_ -> cont host (reduceDupAll term val)
_ -> set (loc + 0) val >> return term
else do
set host (termRemBit sb0)
reduceAt debug book host
t | t == _DP1_ -> do
sb1 <- got (loc + 0)
if termGetBit sb1 == 0
then do
val <- reduceAt debug book (loc + 0)
case termTag val of
t | t == _ERA_ -> cont host (reduceDupEra term val)
t | t == _LAM_ -> cont host (reduceDupLam term val)
t | t == _SUP_ -> cont host (reduceDupSup term val)
t | t == _NIL_ -> cont host (reduceDupNil term val)
t | t == _TUP_ -> cont host (reduceDupTup term val)
t | t == _W32_ -> cont host (reduceDupW32 term val)
t | t == _SET_ -> cont host (reduceDupSet term val)
t | t == _EMP_ -> cont host (reduceDupEmp term val)
t | t == _UNI_ -> cont host (reduceDupUni term val)
t | t == _U32_ -> cont host (reduceDupU32 term val)
t | t == _SIG_ -> cont host (reduceDupSig term val)
t | t == _ALL_ -> cont host (reduceDupAll term val)
_ -> set (loc + 0) val >> return term
else do
set host (termRemBit sb1)
reduceAt debug book host
t | t == _VAR_ -> do
sub <- got (loc + 0)
if termGetBit sub == 0
then return term
else do
set host (termRemBit sub)
reduceAt debug book host
t | t == _REF_ -> do
reduceRefAt book host
reduceAt debug book host
_ -> do
return term
where
cont host action = do
ret <- action
set host ret
reduceAt debug book host
gotT :: Book -> Loc -> HVM Term
gotT book host = got host
reduceRefAt :: Book -> Loc -> HVM Term
reduceRefAt book host = do
term <- got host
let lab = termLab term
let loc = termLoc term
let fid = fromIntegral lab
let ari = funArity book fid
case lab of
x | x == _DUP_F_ -> reduceRefAt_DupF book host loc ari
x | x == _SUP_F_ -> reduceRefAt_SupF book host loc ari
x | x == _LOG_F_ -> reduceRefAt_LogF book host loc ari
otherwise -> case MS.lookup fid (fidToFun book) of
Just ((copy, args), core) -> do
incItr
when (length args /= fromIntegral ari) $ do
putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@" ++ mget (fidToNam book) fid ++ "'."
exitFailure
argTerms <- if ari == 0
then return []
else forM (zip [0..] args) $ \(i, (strict, _)) -> do
term <- got (loc + i)
if strict
then reduceAt False book (loc + i)
else return term
doInjectCoreAt book core host $ zip (map snd args) argTerms
Nothing -> do
putStrLn $ "RUNTIME_ERROR: Function ID " ++ show fid ++ " not found in fidToFun book."
exitFailure
-- Primitive: Dynamic Dup `@DUP(lab val λdp0λdp1(bod))`
reduceRefAt_DupF :: Book -> Loc -> Loc -> Word16 -> HVM Term
reduceRefAt_DupF book host loc ari = do
incItr
when (ari /= 3) $ do
putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@DUP'."
exitFailure
lab <- reduceAt False book (loc + 0)
val <- got (loc + 1)
bod <- got (loc + 2)
dup <- allocNode 1
case termTag lab of
t | t == _W32_ -> do
when (termLoc lab > 0xFFFFFF) $ do
error "RUNTIME_ERROR: dynamic DUP label too large"
-- Create the DUP node with value
set (dup + 0) val
-- Create first APP node for (APP bod DP0)
app1 <- allocNode 2
set (app1 + 0) bod
set (app1 + 1) (termNew _DP0_ (termLoc lab) dup)
-- Create second APP node for (APP (APP bod DP0) DP1)
app2 <- allocNode 2
set (app2 + 0) (termNew _APP_ 0 app1)
set (app2 + 1) (termNew _DP1_ (termLoc lab) dup)
let ret = termNew _APP_ 0 app2
set host ret
return ret
_ -> do
core <- doExtractCoreAt gotT book (loc + 0)
putStrLn $ "RUNTIME_ERROR: dynamic DUP without numeric label: " ++ showTerm lab
putStrLn $ showCore (doLiftDups core)
exitFailure
-- Primitive: Dynamic Sup `@SUP(lab tm0 tm1)`
reduceRefAt_SupF :: Book -> Loc -> Loc -> Word16 -> HVM Term
reduceRefAt_SupF book host loc ari = do
incItr
when (ari /= 3) $ do
putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@SUP'."
exitFailure
lab <- reduceAt False book (loc + 0)
tm0 <- got (loc + 1)
tm1 <- got (loc + 2)
sup <- allocNode 2
case termTag lab of
t | t == _W32_ -> do
when (termLoc lab > 0xFFFFFF) $ do
error "RUNTIME_ERROR: dynamic SUP label too large"
let ret = termNew _SUP_ (termLoc lab) sup
set (sup + 0) tm0
set (sup + 1) tm1
set host ret
return ret
_ -> error "RUNTIME_ERROR: dynamic SUP without numeric label."
-- Primitive: Logger `@LOG(msg)`
-- Will extract the term and log it.
-- Returns 0.
reduceRefAt_LogF :: Book -> Loc -> Loc -> Word16 -> HVM Term
reduceRefAt_LogF book host loc ari = do
incItr
when (ari /= 1) $ do
putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@LOG'."
exitFailure
msg <- doExtractCoreAt gotT book (loc + 0)
putStrLn $ showCore (doLiftDups msg)
-- msgs <- doCollapseFlatAt gotT book (loc + 0)
-- forM_ msgs $ \msg -> do
-- putStrLn $ showCore msg
let ret = termNew _W32_ 0 0
set host ret
return ret
-- Primitive: Fresh `@FRESH`
-- Returns a fresh dup label.
reduceRefAt_FreshF :: Book -> Loc -> Loc -> Word16 -> HVM Term
reduceRefAt_FreshF book host loc ari = do
incItr
when (ari /= 0) $ do
putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@Fresh'."
exitFailure
num <- fromIntegral <$> fresh
let ret = termNew _W32_ 0 num
set host ret
return ret
reduceCAt :: Bool -> Book -> Loc -> HVM Term
reduceCAt = \ _ _ host -> reduceAtC host
reduce :: Bool -> Book -> Term -> HVM Term
reduce debug book term = do
loc <- allocNode 1
set loc term
reduceAt debug book loc
{-./Type.hs-}
{-./Check.hs-}
-- [># LANGUAGE OverloadedStrings #<]
-- [># LANGUAGE TemplateHaskell #<]
-- module Main where
-- import Network.Socket as Network
-- import System.IO (hSetEncoding, utf8, hPutStrLn, stderr)
-- import Control.Exception (try, fromException, SomeException, finally, AsyncException(UserInterrupt))
-- import Control.Monad (guard, when, foldM, forM_, unless)
-- import Data.FileEmbed
-- import Data.List (partition, isPrefixOf, take, find)
-- import Data.Word
-- import Foreign.C.Types
-- import Foreign.LibFFI
-- import Foreign.LibFFI.Types
-- import GHC.Clock
-- import GHC.Conc
-- import Collapse
-- import Compile
-- import Extract
-- import Foreign
-- import Inject
-- import Parse
-- import Reduce
-- import Type
-- import System.Environment (getArgs)
-- import System.Exit (exitWith, ExitCode(ExitSuccess, ExitFailure))
-- import System.IO
-- import System.IO (readFile')
-- import System.IO.Unsafe (unsafePerformIO)
-- import System.IO.Error (tryIOError)
-- import System.Posix.DynamicLinker
-- import System.Process (callCommand)
-- import Text.Printf
-- import Data.IORef
-- import qualified Data.Map.Strict as MS
-- import Text.Read (readMaybe)
-- runtime_c :: String
-- runtime_c = $(embedStringFile "./src/Runtime.c")
-- -- Main
-- -- ----
-- data RunMode
-- = Normalize
-- | Collapse (Maybe Int)
-- deriving Eq
-- main :: IO ()
-- main = do
-- args <- getArgs
-- result <- case args of
-- ("run" : file : rest) -> do
-- let (flags, sArgs) = partition ("-" `isPrefixOf`) rest
-- let compiled = "-c" `elem` flags
-- let collapseFlag = Data.List.find (isPrefixOf "-C") flags >>= parseCollapseFlag
-- let stats = "-s" `elem` flags
-- let debug = "-d" `elem` flags
-- let hideQuotes = "-Q" `elem` flags
-- let mode = case collapseFlag of { Just n -> Collapse n ; Nothing -> Normalize }
-- cliRun file debug compiled mode stats hideQuotes sArgs
-- ("serve" : file : rest) -> do
-- let (flags, _) = partition ("-" `isPrefixOf`) rest
-- let compiled = "-c" `elem` flags
-- let collapseFlag = Data.List.find (isPrefixOf "-C") flags >>= parseCollapseFlag
-- let stats = "-s" `elem` flags
-- let debug = "-d" `elem` flags
-- let hideQuotes = "-Q" `elem` flags
-- let mode = case collapseFlag of { Just n -> Collapse n ; Nothing -> Normalize }
-- cliServe file debug compiled mode stats hideQuotes
-- ["help"] -> printHelp
-- _ -> printHelp
-- case result of
-- Left err -> do
-- putStrLn err
-- exitWith (ExitFailure 1)
-- Right _ -> do
-- exitWith ExitSuccess
-- parseCollapseFlag :: String -> Maybe (Maybe Int)
-- parseCollapseFlag ('-':'C':rest) =
-- case rest of
-- "" -> Just Nothing
-- n -> Just (readMaybe n)
-- parseCollapseFlag _ = Nothing
-- printHelp :: IO (Either String ())
-- printHelp = do
-- putStrLn "HVM usage:"
-- putStrLn " hvm help # Shows this help message"
-- putStrLn " hvm run <file> [flags] [args...] # Evals main"
-- putStrLn " hvm serve <file> [flags] # Starts socket server on port 8080"
-- putStrLn " -c # Runs with compiled mode (fast)"
-- putStrLn " -C # Collapse the result to a list of λ-Terms"
-- putStrLn " -CN # Same as above, but show only first N results"
-- putStrLn " -s # Show statistics"
-- putStrLn " -d # Print execution steps (debug mode)"
-- putStrLn " -Q # Hide quotes in output"
-- return $ Right ()
-- -- CLI Commands
-- -- ------------
-- cliRun :: FilePath -> Bool -> Bool -> RunMode -> Bool -> Bool -> [String] -> IO (Either String ())
-- cliRun filePath debug compiled mode showStats hideQuotes strArgs = do
-- book <- loadBook filePath compiled
-- -- Abort when main isn't present
-- when (not $ MS.member "main" (namToFid book)) $ do
-- putStrLn "Error: 'main' not found."
-- exitWith (ExitFailure 1)
-- -- Abort when wrong number of strArgs
-- let ((_, mainArgs), _) = mget (fidToFun book) (mget (namToFid book) "main")
-- when (length strArgs /= length mainArgs) $ do
-- putStrLn $ "Error: 'main' expects " ++ show (length mainArgs)
-- ++ " arguments, found " ++ show (length strArgs)
-- exitWith (ExitFailure 1)
-- -- Normalize main
-- init <- getMonotonicTimeNSec
-- root <- injectMain book strArgs
-- rxAt <- if compiled
-- then return (reduceCAt debug)
-- else return (reduceAt debug)
-- vals <- case mode of
-- Collapse _ -> doCollapseFlatAt rxAt book 0
-- Normalize -> do
-- core <- doExtractCoreAt rxAt book 0
-- return [(doLiftDups core)]
-- -- Print results
-- case mode of
-- Collapse limit -> do
-- lastItrs <- newIORef 0
-- let limitedVals = maybe id Data.List.take limit vals
-- forM_ limitedVals $ \ term -> do
-- currItrs <- getItr
-- prevItrs <- readIORef lastItrs
-- let output = if hideQuotes then removeQuotes (show term) else show term
-- printf "%s\n" output
-- writeIORef lastItrs currItrs
-- putStrLn ""
-- Normalize -> do
-- let output = if hideQuotes
-- then removeQuotes (show (head vals))
-- else show (head vals)
-- putStrLn output
-- -- Prints total time
-- end <- getMonotonicTimeNSec
-- -- Show stats
-- when showStats $ do
-- itrs <- getItr
-- size <- getLen
-- let time = fromIntegral (end - init) / (10^9) :: Double
-- let mips = (fromIntegral itrs / 1000000.0) / time
-- printf "WORK: %llu interactions\n" itrs
-- printf "TIME: %.7f seconds\n" time
-- printf "SIZE: %llu nodes\n" size
-- printf "PERF: %.3f MIPS\n" mips
-- return ()
-- -- Finalize
-- hvmFree
-- return $ Right ()
-- cliServe :: FilePath -> Bool -> Bool -> RunMode -> Bool -> Bool -> IO (Either String ())
-- cliServe filePath debug compiled mode showStats hideQuotes = do
-- book <- loadBook filePath compiled
-- -- Abort when main isn't present
-- when (not $ MS.member "main" (namToFid book)) $ do
-- putStrLn "Error: 'main' not found."
-- exitWith (ExitFailure 1)
-- putStrLn "HVM serve mode. Listening on port 8080."
-- sock <- socket AF_INET Stream 0
-- setSocketOption sock ReuseAddr 1
-- Network.bind sock (SockAddrInet 8080 0)
-- listen sock 5
-- putStrLn "Server started. Listening on port 8080."
-- serverLoop sock book `finally` do
-- close sock
-- hvmFree
-- putStrLn "\nServer terminated."
-- return $ Right ()
-- where
-- serverLoop sock book = do
-- result <- try $ do
-- (conn, _) <- accept sock
-- h <- socketToHandle conn ReadWriteMode
-- hSetBuffering h LineBuffering
-- hSetEncoding h utf8
-- input <- hGetLine h
-- unless (input == "exit" || input == "quit") $ do
-- oldSize <- getLen
-- root <- injectMain book [input]
-- rxAt <- if compiled then return (reduceCAt debug) else return (reduceAt debug)
-- vals <- case mode of
-- Collapse _ -> doCollapseFlatAt rxAt book 0
-- Normalize -> do
-- core <- doExtractCoreAt rxAt book 0
-- return [doLiftDups core]
-- let output = case mode of
-- Collapse limit -> do
-- let limitedVals = maybe id Data.List.take limit vals
-- let outputs = map (\term -> if hideQuotes then removeQuotes (show term) else show term) limitedVals
-- unlines outputs
-- Normalize -> do
-- let result = head vals
-- if hideQuotes then removeQuotes (show result) else show result
-- hPutStrLn h output
-- setLen oldSize
-- when showStats $ do
-- itrs <- getItr
-- size <- getLen
-- hPutStrLn h $ "WORK: " ++ show itrs ++ " interactions"
-- hPutStrLn h $ "SIZE: " ++ show size ++ " nodes"
-- setItr 0
-- hClose h
-- case result of
-- Left e -> case fromException e of
-- Just UserInterrupt -> return () -- Exit loop on Ctrl+C
-- _ -> do
-- hPutStrLn stderr $ "Connection error: " ++ show (e :: SomeException)
-- serverLoop sock book
-- Right _ -> serverLoop sock book
-- -- Load and initialize a book from a file
-- loadBook :: FilePath -> Bool -> IO Book
-- loadBook filePath compiled = do
-- hvmInit
-- code <- readFile' filePath
-- book <- doParseBook filePath code
-- forM_ (MS.toList (cidToAri book)) $ \ (cid, ari) -> do
-- hvmSetCari cid (fromIntegral ari)
-- forM_ (MS.toList (cidToLen book)) $ \ (cid, len) -> do
-- hvmSetClen cid (fromIntegral len)
-- forM_ (MS.toList (cidToADT book)) $ \ (cid, adt) -> do
-- hvmSetCadt cid (fromIntegral adt)
-- forM_ (MS.toList (fidToFun book)) $ \ (fid, ((_, args), _)) -> do
-- hvmSetFari fid (fromIntegral $ length args)
-- when compiled $ do
-- let decls = compileHeaders book
-- let funcs = map (\ (fid, _) -> compile book fid) (MS.toList (fidToFun book))
-- let mainC = unlines $ [runtime_c] ++ [decls] ++ funcs ++ [genMain book]
-- -- Try to use a cached .so file
-- callCommand "mkdir -p .build"
-- let fName = last $ words $ map (\c -> if c == '/' then ' ' else c) filePath
-- let cPath = ".build/" ++ fName ++ ".c"
-- let oPath = ".build/" ++ fName ++ ".so"
-- oldCFile <- tryIOError (readFile' cPath)
-- bookLib <- if oldCFile == Right mainC then do
-- dlopen oPath [RTLD_NOW]
-- else do
-- writeFile cPath mainC
-- callCommand $ "gcc -O2 -fPIC -shared " ++ cPath ++ " -o " ++ oPath
-- dlopen oPath [RTLD_NOW]
-- forM_ (MS.keys (fidToFun book)) $ \ fid -> do
-- funPtr <- dlsym bookLib (mget (fidToNam book) fid ++ "_f")
-- hvmDefine fid funPtr
-- -- Link compiled state
-- hvmGotState <- hvmGetState
-- hvmSetState <- dlsym bookLib "hvm_set_state"
-- callFFI hvmSetState retVoid [argPtr hvmGotState]
-- return book
-- genMain :: Book -> String
-- genMain book =
-- let mainFid = mget (namToFid book) "main"
-- registerFuncs = unlines [" hvm_define(" ++ show fid ++ ", " ++ mget (fidToNam book) fid ++ "_f);" | fid <- MS.keys (fidToFun book)]
-- in unlines
-- [ "int main() {"
-- , " hvm_init();"
-- , registerFuncs
-- , " clock_t start = clock();"
-- , " Term root = term_new(REF, "++show mainFid++", 0);"
-- , " normal(root);"
-- , " double time = (double)(clock() - start) / CLOCKS_PER_SEC * 1000;"
-- , " printf(\"WORK: %\"PRIu64\" interactions\\n\", get_itr());"
-- , " printf(\"TIME: %.3fs seconds\\n\", time / 1000.0);"
-- , " printf(\"SIZE: %llu nodes\\n\", get_len());"
-- , " printf(\"PERF: %.3f MIPS\\n\", (get_itr() / 1000000.0) / (time / 1000.0));"
-- , " hvm_free();"
-- , " return 0;"
-- , "}"
-- ]
-- -- Parse arguments and create a term with the given function name
-- injectMain :: Book -> [String] -> IO Term
-- injectMain book args = do
-- (book, parsedArgs) <- foldM (\(b, as) str -> do
-- (b', a) <- doParseArgument str b
-- return (b', a:as)) (book, []) args
-- let fid = mget (namToFid book) "main"
-- let main = Ref "main" fid (reverse parsedArgs)
-- root <- doInjectCoreAt book main 0 []
-- return root
-- removeQuotes :: String -> String
-- removeQuotes s = case s of
-- '"':rest -> init rest -- Remove first and last quote if present
-- _ -> s -- Otherwise return as-is
-- TASK: update Main.hs fully
-- COMPLETE UPDATED MAIN.HS:
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
module Main where
import Network.Socket as Network
import System.IO (hSetEncoding, utf8, hPutStrLn, stderr)
import Control.Exception (try, fromException, SomeException, finally, AsyncException(UserInterrupt))
import Control.Monad (guard, when, foldM, forM_, unless)
import Data.FileEmbed
import Data.List (partition, isPrefixOf, take, find)
import Data.Word
import Foreign.C.Types
import Foreign.LibFFI
import Foreign.LibFFI.Types
import GHC.Clock
import GHC.Conc
import Check
import Collapse
import Compile
import Extract
import Foreign
import Inject
import Parse
import Reduce
import Type
import System.Environment (getArgs)
import System.Exit (exitWith, ExitCode(ExitSuccess, ExitFailure))
import System.IO
import System.IO (readFile')
import System.IO.Unsafe (unsafePerformIO)
import System.IO.Error (tryIOError)
import System.Posix.DynamicLinker
import System.Process (callCommand)
import Text.Printf
import Data.IORef
import qualified Data.Map.Strict as MS
import Text.Read (readMaybe)
runtime_c :: String
runtime_c = $(embedStringFile "./src/Runtime.c")
-- Main
-- ----
data RunMode
= Normalize
| Collapse (Maybe Int)
deriving Eq
main :: IO ()
main = do
args <- getArgs
result <- case args of
("run" : file : rest) -> do
let (flags, sArgs) = partition ("-" `isPrefixOf`) rest
let compiled = "-c" `elem` flags
let collapseFlag = Data.List.find (isPrefixOf "-C") flags >>= parseCollapseFlag
let stats = "-s" `elem` flags
let debug = "-d" `elem` flags
let hideQuotes = "-Q" `elem` flags
let mode = case collapseFlag of { Just n -> Collapse n ; Nothing -> Normalize }
cliRun file debug compiled mode stats hideQuotes sArgs
("serve" : file : rest) -> do
let (flags, _) = partition ("-" `isPrefixOf`) rest
let compiled = "-c" `elem` flags
let collapseFlag = Data.List.find (isPrefixOf "-C") flags >>= parseCollapseFlag
let stats = "-s" `elem` flags
let debug = "-d" `elem` flags
let hideQuotes = "-Q" `elem` flags
let mode = case collapseFlag of { Just n -> Collapse n ; Nothing -> Normalize }
cliServe file debug compiled mode stats hideQuotes
["help"] -> printHelp
_ -> printHelp
case result of
Left err -> do
putStrLn err
exitWith (ExitFailure 1)
Right _ -> do
exitWith ExitSuccess
parseCollapseFlag :: String -> Maybe (Maybe Int)
parseCollapseFlag ('-':'C':rest) =
case rest of
"" -> Just Nothing
n -> Just (readMaybe n)
parseCollapseFlag _ = Nothing
printHelp :: IO (Either String ())
printHelp = do
putStrLn "HVM usage:"
putStrLn " hvm help # Shows this help message"
putStrLn " hvm run <file> [flags] [args...] # Evals main"
putStrLn " hvm serve <file> [flags] # Starts socket server on port 8080"
putStrLn " -c # Runs with compiled mode (fast)"
putStrLn " -C # Collapse the result to a list of λ-Terms"
putStrLn " -CN # Same as above, but show only first N results"
putStrLn " -s # Show statistics"
putStrLn " -d # Print execution steps (debug mode)"
putStrLn " -Q # Hide quotes in output"
return $ Right ()
-- CLI Commands
-- ------------
cliRun :: FilePath -> Bool -> Bool -> RunMode -> Bool -> Bool -> [String] -> IO (Either String ())
cliRun filePath debug compiled mode showStats hideQuotes strArgs = do
book <- loadBook filePath compiled
-- Abort when main isn't present
when (not $ MS.member "main" (namToFid book)) $ do
putStrLn "Error: 'main' not found."
exitWith (ExitFailure 1)
-- Abort when wrong number of strArgs
let ((_, mainArgs), _) = mget (fidToFun book) (mget (namToFid book) "main")
when (length strArgs /= length mainArgs) $ do
putStrLn $ "Error: 'main' expects " ++ show (length mainArgs)
++ " arguments, found " ++ show (length strArgs)
exitWith (ExitFailure 1)
-- Normalize main
init <- getMonotonicTimeNSec
root <- injectMain book strArgs
rxAt <- if compiled
then return (reduceCAt debug)
else return (reduceAt debug)
vals <- case mode of
Collapse _ -> doCollapseFlatAt rxAt book 0
Normalize -> do
core <- doExtractCoreAt rxAt book 0
return [(doLiftDups core)]
-- Print results
case mode of
Collapse limit -> do
lastItrs <- newIORef 0
let limitedVals = maybe id Data.List.take limit vals
forM_ limitedVals $ \ term -> do
currItrs <- getItr
prevItrs <- readIORef lastItrs
let output = if hideQuotes then removeQuotes (show term) else show term
printf "%s\n" output
writeIORef lastItrs currItrs
putStrLn ""
Normalize -> do
let output = if hideQuotes
then removeQuotes (show (head vals))
else show (head vals)
putStrLn output
-- Type check all nullary functions with annotated bodies
forM_ (MS.toList (fidToFun book)) $ \ (fid, ((_, args), body)) -> do
when (null args) $ do
case body of
Ann _ term typ -> do
printf "Checking @%s...\n" (mget (fidToNam book) fid)
hFlush stdout
-- Inject the term and type into fresh locations
termLoc <- allocNode 1
typeLoc <- allocNode 1
termTerm <- doInjectCoreAt book term termLoc []
typeTerm <- doInjectCoreAt book typ typeLoc []
-- Run the type check and store in a fresh location
result <- check 0 termTerm typeTerm
resultLoc <- allocNode 1
set resultLoc result
-- Collapse and print the result
collapsed <- doCollapseFlatAt rxAt book resultLoc
-- use unicode check / X symbols
if length collapsed > 0
then putStrLn "✓"
else putStrLn "✗"
_ -> return ()
-- Prints total time
end <- getMonotonicTimeNSec
-- Show stats
when showStats $ do
itrs <- getItr
size <- getLen
let time = fromIntegral (end - init) / (10^9) :: Double
let mips = (fromIntegral itrs / 1000000.0) / time
printf "WORK: %llu interactions\n" itrs
printf "TIME: %.7f seconds\n" time
printf "SIZE: %llu nodes\n" size
printf "PERF: %.3f MIPS\n" mips
return ()
-- Finalize
hvmFree
return $ Right ()
cliServe :: FilePath -> Bool -> Bool -> RunMode -> Bool -> Bool -> IO (Either String ())
cliServe filePath debug compiled mode showStats hideQuotes = do
book <- loadBook filePath compiled
-- Abort when main isn't present
when (not $ MS.member "main" (namToFid book)) $ do
putStrLn "Error: 'main' not found."
exitWith (ExitFailure 1)
putStrLn "HVM serve mode. Listening on port 8080."
sock <- socket AF_INET Stream 0
setSocketOption sock ReuseAddr 1
Network.bind sock (SockAddrInet 8080 0)
listen sock 5
putStrLn "Server started. Listening on port 8080."
serverLoop sock book `finally` do
close sock
hvmFree
putStrLn "\nServer terminated."
return $ Right ()
where
serverLoop sock book = do
result <- try $ do
(conn, _) <- accept sock
h <- socketToHandle conn ReadWriteMode
hSetBuffering h LineBuffering
hSetEncoding h utf8
input <- hGetLine h
unless (input == "exit" || input == "quit") $ do
oldSize <- getLen
root <- injectMain book [input]
rxAt <- if compiled then return (reduceCAt debug) else return (reduceAt debug)
vals <- case mode of
Collapse _ -> doCollapseFlatAt rxAt book 0
Normalize -> do
core <- doExtractCoreAt rxAt book 0
return [doLiftDups core]
let output = case mode of
Collapse limit -> do
let limitedVals = maybe id Data.List.take limit vals
let outputs = map (\term -> if hideQuotes then removeQuotes (show term) else show term) limitedVals
unlines outputs
Normalize -> do
let result = head vals
if hideQuotes then removeQuotes (show result) else show result
hPutStrLn h output
setLen oldSize
when showStats $ do
itrs <- getItr
size <- getLen
hPutStrLn h $ "WORK: " ++ show itrs ++ " interactions"
hPutStrLn h $ "SIZE: " ++ show size ++ " nodes"
setItr 0
hClose h
case result of
Left e -> case fromException e of
Just UserInterrupt -> return () -- Exit loop on Ctrl+C
_ -> do
hPutStrLn stderr $ "Connection error: " ++ show (e :: SomeException)
serverLoop sock book
Right _ -> serverLoop sock book
-- Load and initialize a book from a file
loadBook :: FilePath -> Bool -> IO Book
loadBook filePath compiled = do
hvmInit
code <- readFile' filePath
book <- doParseBook filePath code
forM_ (MS.toList (fidToFun book)) $ \ (fid, ((_, args), _)) -> do
hvmSetFari fid (fromIntegral $ length args)
when compiled $ do
let decls = compileHeaders book
let funcs = map (\ (fid, _) -> compile book fid) (MS.toList (fidToFun book))
let mainC = unlines $ [runtime_c] ++ [decls] ++ funcs ++ [genMain book]
-- Try to use a cached .so file
callCommand "mkdir -p .build"
let fName = last $ words $ map (\c -> if c == '/' then ' ' else c) filePath
let cPath = ".build/" ++ fName ++ ".c"
let oPath = ".build/" ++ fName ++ ".so"
oldCFile <- tryIOError (readFile' cPath)
bookLib <- if oldCFile == Right mainC then do
dlopen oPath [RTLD_NOW]
else do
writeFile cPath mainC
callCommand $ "gcc -O2 -fPIC -shared " ++ cPath ++ " -o " ++ oPath
dlopen oPath [RTLD_NOW]
forM_ (MS.keys (fidToFun book)) $ \ fid -> do
funPtr <- dlsym bookLib (mget (fidToNam book) fid ++ "_f")
hvmDefine fid funPtr
-- Link compiled state
hvmGotState <- hvmGetState
hvmSetState <- dlsym bookLib "hvm_set_state"
callFFI hvmSetState retVoid [argPtr hvmGotState]
return book
genMain :: Book -> String
genMain book =
let mainFid = mget (namToFid book) "main"
registerFuncs = unlines [" hvm_define(" ++ show fid ++ ", " ++ mget (fidToNam book) fid ++ "_f);" | fid <- MS.keys (fidToFun book)]
in unlines
[ "int main() {"
, " hvm_init();"
, registerFuncs
, " clock_t start = clock();"
, " Term root = term_new(REF, "++show mainFid++", 0);"
, " normal(root);"
, " double time = (double)(clock() - start) / CLOCKS_PER_SEC * 1000;"
, " printf(\"WORK: %\"PRIu64\" interactions\\n\", get_itr());"
, " printf(\"TIME: %.3fs seconds\\n\", time / 1000.0);"
, " printf(\"SIZE: %llu nodes\\n\", get_len());"
, " printf(\"PERF: %.3f MIPS\\n\", (get_itr() / 1000000.0) / (time / 1000.0));"
, " hvm_free();"
, " return 0;"
, "}"
]
-- Parse arguments and create a term with the given function name
injectMain :: Book -> [String] -> IO Term
injectMain book args = do
(book, parsedArgs) <- foldM (\(b, as) str -> do
(b', a) <- doParseArgument str b
return (b', a:as)) (book, []) args
let fid = mget (namToFid book) "main"
let main = Ref "main" fid (reverse parsedArgs)
root <- doInjectCoreAt book main 0 []
return root
removeQuotes :: String -> String
removeQuotes s = case s of
'"':rest -> init rest -- Remove first and last quote if present
_ -> s -- Otherwise return as-is
-- 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 Extract
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
debug :: Term -> IO ()
debug term = do
core <- toCore term
putStr $ concatMap (\c -> if c == '\n' then "; " else [c]) $ show core
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)
-- | 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
loc <- allocNode 1
set loc 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)
-- | Gets a fresh label and increments the counter
genFreshLabel :: IO Lab
genFreshLabel = do
lab <- readIORef freshLabelCounter
modifyIORef' freshLabelCounter (+1)
pure lab
-- | Create a DUP node with a fresh label
makeDupFresh :: Term -> IO (Term, Term)
makeDupFresh term = do
-- Get a fresh label
freshLab <- genFreshLabel
makeDup freshLab term
-- | 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
-- 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
putStrLn $ "== " ++ showTerm a
putStrLn $ ".. " ++ showTerm b
if a == b
then pure nilT
else equalGo dep a b
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
var0 <- makeNode _W32_ (fromIntegral dep) []
var1 <- makeNode _W32_ (fromIntegral dep) []
aApp <- makeNode _APP_ 0 [a, var0]
bApp <- makeNode _APP_ 0 [b, var1]
aRes <- whnf aApp
bRes <- whnf bApp
equalGo (dep+1) aRes bRes
| 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 term = do
-- putStr "infer: " ; debug term ; putStrLn ""
putStrLn $ "infer: " ++ showTerm term
inferGo dep term
inferGo :: Int -> Term -> IO Term
inferGo dep term
| tTag term == _SUP_ = do
a <- field term 0
b <- field term 1
aType <- infer dep a
bType <- infer dep b
makeNode _SUP_ (tLab term) [aType, bType]
| tTag term == _VAR_ = do
sub <- got (termLoc term)
if termGetBit sub == 0
then do
putStr "(cant-infer-var)"
pure eraT
else do
infer dep (termRemBit sub)
| 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
if termLab term == 0
then do -- already checked
tm <- field term 0
ty <- field term 1
pure ty
else do
tm <- field term 0
ty <- field term 1
rc <- check dep tm 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 term goal0 = do
goal <- whnf goal0
-- putStr "check: " ; debug term ; putStr " :: " ; debug goal ; putStrLn ""
putStrLn $ "check: " ++ showTerm term ++ " :: " ++ showTerm goal
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 == _VAR_ = do
sub <- got (termLoc term)
if termGetBit sub == 0
then do
putStr "(cant-infer-var)"
pure eraT
else do
check dep (termRemBit sub) goal
| 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 do
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
a <- field goal 0
b <- field goal 1
(a0, a1) <- makeDupFresh a
-- Create fresh variables for the lambda binding
-- NOTE: temporarily, we will use W32 to simulate bruijn indices
-- this causes nums to identify with vars, but is otherwise fine
let var0 = termNew _W32_ 0 (fromIntegral dep)
let var1 = termNew _W32_ 0 (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 [term, ann0]
appB <- makeNode _APP_ 0 [b, ann1]
appF_nf <- reduceAppLam appF term
-- appF_nf <- return appF
appB_nf <- whnf appB
-- print $ showTerm b
-- print $ showTerm appB
-- print $ showTerm appB_nf
-- print $ showTerm appF
-- Check with increased depth
check (dep + 1) appF_nf 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 <- genFreshLabel
(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 attempting to type-check the following HVM3 file:
-- @main = <λx.x : ∀x:U32.U32>
-- yet, when running the `hvm` command on that file, I get:
-- <λa.a : ∀U32.λb.U32>
-- Checking @main...
-- check: term_new(LAM,0x000000,0x00000009) :: term_new(ALL,0x000000,0x0000000a)
-- check: term_new(VAR,0x000000,0x00000009) :: term_new(U32,0x000000,0x00000000)
-- check: term_new(ANN,0x000000,0x0000000e) :: term_new(U32,0x000000,0x00000000)
-- infer: term_new(ANN,0x000000,0x0000000e)
-- == term_new(LAM,0x000000,0x00000016)
-- .. term_new(U32,0x000000,0x00000000)
-- (type-mismatch)✗
-- WORK: 5 interactions
-- TIME: 0.0004910 seconds
-- SIZE: 28 nodes
-- this is unexpected. instead, I expected this term to type-check fine.
-- in particular, that equality should be U32 == U32, not LAM == U32.
-- that means there is some error in my code.
-- reason about the issue, find the exact location of the error, and
-- propose the simplest change that will fix this specific issue.
@VictorTaelin
Copy link
Author

Answer

the issue is on the makeDup function:

-- | 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
  loc <- allocNode 1
  set loc 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)

it is allocating a location for the DUP node, but it is returning DP0/DP1 links
pointing to 0, instead of that location. this causes incorrect DUP interactions,
which, in turn, make that lambda show up there.

the solution is to replace t0 and t1 by:

  let t0 = termNew _DP0_ lab loc
  let t1 = termNew _DP1_ lab loc

note that, in isolation, spotting that this function is wrong is not hard, but realizing that it is the underlying cause for the issue that I reported absolutely is. if an AI hyper-focuses on the issue at hands, it will only succeeds if it has extraordinary debugging skills

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment