From 5c07bcb3cb2457c2816775b7c7f9cf00a090cdcf Mon Sep 17 00:00:00 2001
From: Lorenzobattistela <lorenzobattistela@gmail.com>
Date: Mon, 4 Aug 2025 17:12:03 -0300
Subject: [PATCH 1/5] new collapser

---
 src/HVM/Collapse.hs | 457 +++++++++++++++++++-------------------------
 1 file changed, 195 insertions(+), 262 deletions(-)

diff --git a/src/HVM/Collapse.hs b/src/HVM/Collapse.hs
index f21bc15..c67f889 100644
--- a/src/HVM/Collapse.hs
+++ b/src/HVM/Collapse.hs
@@ -1,11 +1,17 @@
 {-./Type.hs-}
 {-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ViewPatterns #-}
 
 module HVM.Collapse where
 
 import Control.Monad (ap, forM, forM_)
 import Control.Monad.IO.Class
 import Data.Char (chr, ord)
+import qualified Data.Kind as DK
 import Data.IORef
 import Data.Bits ((.&.), xor, (.|.), complement, shiftR)
 import Data.Word
@@ -18,6 +24,136 @@ import System.IO.Unsafe (unsafeInterleaveIO)
 import qualified Data.IntMap.Strict as IM
 import qualified Data.Map.Strict as MS
 
+data CTerm
+  = CVar String
+  | CRef String Word16 [CTerm]
+  | CEra
+  | CLam String CTerm
+  | CApp CTerm CTerm
+  | CSup Word32 CTerm CTerm
+  | CCtr String [CTerm]
+  | CU32 Word32
+  | CChr Char
+  | COp2 Oper CTerm CTerm
+  | CLet LetT String CTerm CTerm
+  | CMat MatT CTerm [(String, CTerm)] [(String, [String], CTerm)]
+  | CInc CTerm
+  | CDec CTerm
+  | CCol Word32 Int CTerm -- Internal "selection tag"
+  deriving (Eq)
+
+data Nat = Z | S Nat
+
+data SNat :: Nat -> DK.Type where
+  SZ :: SNat Z
+  SS :: SNat n -> SNat (S n)
+
+type family Add (n :: Nat) (m :: Nat) :: Nat where
+  Add Z     m = m
+  Add (S n) m = S (Add n m)
+
+addSNat :: SNat n -> SNat m -> SNat (Add n m)
+addSNat SZ     m = m
+addSNat (SS n) m = SS (addSNat n m)
+
+type family CtrT (n :: Nat) :: DK.Type where
+  CtrT Z     = CTerm
+  CtrT (S p) = CTerm -> CtrT p
+
+data SomeSNat where SomeSNat :: SNat n -> SomeSNat
+toSomeSNat :: Int -> SomeSNat
+toSomeSNat 0 = SomeSNat SZ
+toSomeSNat n = case toSomeSNat (n-1) of SomeSNat s -> SomeSNat (SS s)
+
+withSNat :: Int -> (forall n. SNat n -> r) -> r
+withSNat n f = case toSomeSNat n of SomeSNat s -> f s
+
+-- Recursive, type-safe builder functions
+buildCtr :: SNat n -> String -> CtrT n
+buildCtr s k = buildCtr' s [] where
+  buildCtr' :: SNat m -> [CTerm] -> CtrT m
+  buildCtr' SZ     acc = CCtr k (reverse acc)
+  buildCtr' (SS s') acc = \arg -> buildCtr' s' (arg : acc)
+
+buildRef :: SNat n -> String -> Word16 -> CtrT n
+buildRef s k i = buildRef' s [] where
+  buildRef' :: SNat m -> [CTerm] -> CtrT m
+  buildRef' SZ      acc = CRef k i (reverse acc)
+  buildRef' (SS s') acc = \arg -> buildRef' s' (arg : acc)
+
+data SemiTerm where
+  SemiTerm :: SNat k -> (CTerm -> CtrT k) -> SemiTerm
+
+-- An initial term with no hole.
+start :: SemiTerm
+start = SemiTerm SZ id
+
+-- Replaces the leftmost hole in S, by a term T with N holes.
+-- When T has no holes (N=0):
+-- - If S has a leftmost hole: fill it.
+-- - Else: apply S to T, extending the spine.
+-- Examples:
+-- - extend (_,_) X     ~> (X,_)     -- fill the leftmost hole
+-- - extend (A,_) (_,X) ~> (A,(_,X)) -- fill the leftmost hole
+-- - extend (A,B) X     ~> ((A,B) X) -- extend the spine
+extend :: SemiTerm -> SNat n -> CtrT n -> SemiTerm
+extend (SemiTerm k l) n ctr = case k of
+  SZ    -> SemiTerm n               (ini l n ctr)
+  SS k' -> SemiTerm (addSNat n k')  (ext k' l n ctr)
+  where ini :: (CTerm -> CTerm) -> SNat n -> CtrT n -> (CTerm -> CtrT n)
+        ext :: SNat k -> (CTerm -> CtrT (S k)) -> SNat n -> CtrT n -> CtrT (S (Add n k))
+        ini   l SZ      ctr = \k -> CApp (l k) ctr
+        ini   l (SS n') ctr = \x -> ini l n' (ctr x)
+        ext _ l SZ      ctr = l ctr
+        ext k l (SS n') ctr = \x -> ext k l n' (ctr x)
+
+-- Fills remaining holes with a placeholder variable.
+complete :: SemiTerm -> CTerm
+complete (SemiTerm SZ     l) = l (CVar "F")
+complete (SemiTerm (SS p) l) = complete (SemiTerm p (l (CVar "X")))
+
+
+wnf :: CTerm -> CTerm
+wnf (CCol l i x) = col l i x
+wnf v            = v
+
+col :: Word32 -> Int -> CTerm -> CTerm
+col l i (wnf -> CSup r x y)   = if l == r then [x, y] !! i else CSup r (col l i x) (col l i y)
+col l i (wnf -> CLam n f)     = CLam n (col l i f)
+col l i (wnf -> CApp f x)     = CApp (col l i f) (col l i x)
+col l i (wnf -> CCtr k xs)    = CCtr k (map (col l i) xs)
+col l i (wnf -> CRef k r xs)  = CRef k r (map (col l i) xs)
+col l i (wnf -> COp2 o a b)   = COp2 o (col l i a) (col l i b)
+col l i (wnf -> CLet m n v b) = CLet m n (col l i v) (col l i b)
+col l i (wnf -> CMat t s ms cs) = CMat t (col l i s) (map (fmap (col l i)) ms) (map (\(c,vs,b) -> (c,vs,col l i b)) cs)
+col l i (wnf -> CInc x)       = CInc (col l i x)
+col l i (wnf -> CDec x)       = CDec (col l i x)
+col l i (wnf -> x)            = x
+
+collapse :: [CTerm] -> SemiTerm -> CTerm
+collapse [] semi = case complete semi of CApp _ x -> x; term -> term
+collapse ((wnf -> tm) : tms) semi =
+  case tm of
+    CSup l a b  -> CSup l (collapse (a : map (CCol l 0) tms) semi)
+                        (collapse (b : map (CCol l 1) tms) semi)
+    CCol l i x  -> collapse (x : tms) $ extend semi (SS SZ) (CCol l i)
+    CVar k      -> collapse tms $ extend semi SZ (CVar k)
+    CEra        -> CEra
+    CLam x f    -> collapse (f : tms) $ extend semi (SS SZ) (\b -> CLam x b)
+    CApp f x    -> collapse (f : x : tms) semi
+    COp2 o a b  -> collapse (a : b : tms) $ extend semi (SS (SS SZ)) (COp2 o)
+    CCtr k xs   -> withSNat (length xs) $ \sNat -> collapse (xs ++ tms) $ extend semi sNat (buildCtr sNat k)
+    CRef k i xs -> withSNat (length xs) $ \sNat -> collapse (xs ++ tms) $ extend semi sNat (buildRef sNat k i)
+    CU32 n      -> collapse tms $ extend semi SZ (CU32 n)
+    CChr c      -> collapse tms $ extend semi SZ (CChr c)
+    CInc x      -> collapse (x : tms) $ extend semi (SS SZ) CInc
+    CDec x      -> collapse (x : tms) $ extend semi (SS SZ) CDec
+    CLet m k v b-> collapse (v : b : tms) $ extend semi (SS (SS SZ)) (CLet m k)
+    CMat t v m c-> collapse tms $ extend semi SZ (CMat t v m c)
+    _           -> tm
+
+
+
 -- The Collapse Monad 
 -- ------------------
 -- See: https://gist.github.com/VictorTaelin/60d3bc72fb4edefecd42095e44138b41
@@ -29,61 +165,9 @@ data Bin
   | E
   deriving Show
 
--- A Collapse is a tree of superposed values
-data Collapse a
-  = CSup !Lab (Collapse a) (Collapse a)
-  | CInc (Collapse a)
-  | CDec (Collapse a)
-  | CVal !a
-  | CEra
-  deriving Show
-
-bind :: Collapse a -> (a -> Collapse b) -> Collapse b
-bind k f = fork k IM.empty where
-  -- fork :: Collapse a -> IntMap (Bin -> Bin) -> Collapse b
-  fork CEra         paths = CEra
-  fork (CVal v)     paths = pass (f v) (IM.map (\x -> x E) paths)
-  fork (CInc x)     paths = CInc (fork x paths)
-  fork (CDec x)     paths = CDec (fork x paths)
-  fork (CSup k x y) paths =
-    let lft = fork x $ IM.alter (\x -> Just (maybe (putO id) putO x)) (fromIntegral k) paths in
-    let rgt = fork y $ IM.alter (\x -> Just (maybe (putI id) putI x)) (fromIntegral k) paths in
-    CSup k lft rgt 
-  -- pass :: Collapse b -> IntMap Bin -> Collapse b
-  pass CEra         paths = CEra
-  pass (CVal v)     paths = CVal v
-  pass (CInc x)     paths = CInc (pass x paths)
-  pass (CDec x)     paths = CDec (pass x paths)
-  pass (CSup k x y) paths = case IM.lookup (fromIntegral k) paths of
-    Just (O p) -> pass x (IM.insert (fromIntegral k) p paths)
-    Just (I p) -> pass y (IM.insert (fromIntegral k) p paths)
-    Just E     -> CSup k (pass x paths) (pass y paths)
-    Nothing    -> CSup k (pass x paths) (pass y paths)
-  -- putO :: (Bin -> Bin) -> (Bin -> Bin)
-  putO bs = \x -> bs (O x)
-  -- putI :: (Bin -> Bin) -> (Bin -> Bin) 
-  putI bs = \x -> bs (I x)
-
-instance Functor Collapse where
-  fmap f (CVal v)     = CVal (f v)
-  fmap f (CSup k x y) = CSup k (fmap f x) (fmap f y)
-  fmap f (CInc x)     = CInc (fmap f x)
-  fmap f (CDec x)     = CDec (fmap f x)
-  fmap _ CEra         = CEra
-
-instance Applicative Collapse where
-  pure  = CVal
-  (<*>) = ap
-
-instance Monad Collapse where
-  return = pure
-  (>>=)  = bind
-
 -- Dup Collapser
 -- -------------
-
 collapseDupsAt :: IM.IntMap [Int] -> ReduceAt -> Book -> Loc -> HVM Core
-
 collapseDupsAt state@(paths) reduceAt book host = unsafeInterleaveIO $ do
   term <- reduceAt book host
   case termTag term of
@@ -242,98 +326,24 @@ collapseDupsAt state@(paths) reduceAt book host = unsafeInterleaveIO $ do
       return $ Dec val0
 
     tag -> do
-      return $ Var "?"
+      return $ Var ("?" ++ show tag)
       -- exitFailure
 
--- Sup Collapser
--- -------------
-
-collapseSups :: Book -> Core -> Collapse Core
-
-collapseSups book core = case core of
-
-  Var name -> do
-    return $ Var name
-
-  Ref name fid args -> do
-    args <- mapM (collapseSups book) args
-    return $ Ref name fid args
-
-  Lam name body -> do
-    body <- collapseSups book body
-    return $ Lam name body
-
-  App fun arg -> do
-    fun <- collapseSups book fun
-    arg <- collapseSups book arg
-    return $ App fun arg
-
-  Dup lab x y val body -> do
-    val <- collapseSups book val
-    body <- collapseSups book body
-    return $ Dup lab x y val body
-
-  Ctr nam fields -> do
-    fields <- mapM (collapseSups book) fields
-    return $ Ctr nam fields
-
-  Mat kin val mov css -> do
-    val <- collapseSups book val
-    mov <- mapM (\(key, expr) -> do
-      expr <- collapseSups book expr
-      return (key, expr)) mov
-    css <- mapM (\(ctr, fds, bod) -> do
-      bod <- collapseSups book bod
-      return (ctr, fds, bod)) css
-    return $ Mat kin val mov css
-
-  U32 val -> do
-    return $ U32 val
-
-  Chr val -> do
-    return $ Chr val
-
-  Op2 op x y -> do
-    x <- collapseSups book x
-    y <- collapseSups book y
-    return $ Op2 op x y
-
-  Let mode name val body -> do
-    val <- collapseSups book val
-    body <- collapseSups book body
-    return $ Let mode name val body
-
-  Era -> do
-    CEra
-
-  Sup lab tm0 tm1 -> do
-    let tm0' = collapseSups book tm0
-    let tm1' = collapseSups book tm1
-    CSup lab tm0' tm1'
-
-  Inc val -> do
-    let val' = collapseSups book val
-    CInc val'
-
-  Dec val -> do
-    let val' = collapseSups book val
-    CDec val'
-
 -- Tree Collapser
 -- --------------
 
-doCollapseAt :: ReduceAt -> Book -> Loc -> HVM (Collapse Core)
+doCollapseAt :: ReduceAt -> Book -> Loc -> HVM Core
 doCollapseAt reduceAt book host = do
-  -- namesRef <- newIORef MS.empty
-  let state = (IM.empty)
-  core <- collapseDupsAt state reduceAt book host
-  return $ collapseSups book core
+  -- Step 1: Read the low-level representation into a high-level Core term.
+  initialCore <- collapseDupsAt IM.empty reduceAt book host
+  -- Step 2: Convert to our internal CTerm AST.
+  let initialCTerm = coreToCTerm initialCore
+  -- Step 3: Run the new, powerful collapse algorithm.
+  let collapsedCTerm = collapse [initialCTerm] start
+  -- Step 4: Convert the resulting Sup-tree back to the public Core type.
+  let finalCore = ctermToCore collapsedCTerm
+  return finalCore
 
--- Simple Queue
--- ------------
--- Allows pushing to an end, and popping from another.
--- Simple purely functional implementation.
--- Includes sqPop and sqPut.
 
 data SQ a = SQ [a] [a]
 
@@ -348,132 +358,55 @@ sqPop (SQ (x:xs) ys) = Just (x, SQ xs ys)
 sqPut :: a -> SQ a -> SQ a
 sqPut x (SQ xs ys) = SQ xs (x:ys)
 
--- Priority Queue
--- --------------
--- A stable min-heap implemented with a radix tree.
--- Orders by an Int priority and a unique Word64 key.
--- Based on IntPSQ from the the psqueues library (https://hackage.haskell.org/package/psqueues-0.2.8.1)
-
-data PQ p v
-    = Bin !Word64 !p v !Word64 !(PQ p v) !(PQ p v)
-    | Tip !Word64 !p v
-    | Nil
-
-pqPush :: Ord p => Word64 -> p -> v -> PQ p v -> PQ p v
-pqPush k1 p1 x1 t = case t of
-  Nil                                      -> Tip k1 p1 x1
-  (Tip k2 p2 x2)
-    | (p1, k1) < (p2, k2)                  -> link k1 p1 x1 k2 (Tip k2 p2 x2) Nil
-    | otherwise                            -> link k2 p2 x2 k1 (Tip k1 p1 x1) Nil
-  (Bin k2 p2 x2 m l r)
-    | nomatch k1 k2 m, (p1, k1) < (p2, k2) -> link k1 p1 x1 k2 (Bin k2 p2 x2 m l r) Nil
-    | nomatch k1 k2 m                      -> link k2 p2 x2 k1 (Tip k1 p1 x1) (pqMerge m l r)
-    | (p1, k1) < (p2, k2), zero k2 m       -> Bin k1 p1 x1 m (pqPush k2 p2 x2 l) r
-    | (p1, k1) < (p2, k2)                  -> Bin k1 p1 x1 m l (pqPush k2 p2 x2 r)
-    | zero k1 m                            -> Bin k2 p2 x2 m (pqPush k1 p1 x1 l) r
-    | otherwise                            -> Bin k2 p2 x2 m l (pqPush k1 p1 x1 r)
-  where
-    nomatch :: Word64 -> Word64 -> Word64 -> Bool
-    nomatch k1 k2 m =
-      let maskW = complement (m-1) `xor` m
-      in (k1 .&. maskW) /= (k2 .&. maskW)
-
-    zero :: Word64 -> Word64 -> Bool
-    zero i m = i .&. m == 0
-
-    link :: Word64 -> p -> v -> Word64 -> (PQ p v) -> (PQ p v) -> (PQ p v)
-    link k p x k' fst snd =
-      let m = highestBitMask (k `xor` k')
-      in if zero m k'
-         then Bin k p x m fst snd
-         else Bin k p x m snd fst
-
-    highestBitMask :: Word64 -> Word64
-    highestBitMask x1 =
-      let x2 = x1 .|. x1 `shiftR` 1
-          x3 = x2 .|. x2 `shiftR` 2
-          x4 = x3 .|. x3 `shiftR` 4
-          x5 = x4 .|. x4 `shiftR` 8
-          x6 = x5 .|. x5 `shiftR` 16
-          x7 = x6 .|. x6 `shiftR` 32
-      in x7 `xor` (x7 `shiftR` 1)
-
-pqPop :: Ord p => PQ p v -> Maybe (Word64, p, v, PQ p v)
-pqPop t = case t of
-  Nil             -> Nothing
-  Tip k p x       -> Just (k, p, x, Nil)
-  Bin k p x m l r -> Just (k, p, x, pqMerge m l r)
-
-pqMerge :: Ord p => Word64 -> PQ p v -> PQ p v -> PQ p v
-pqMerge m l r = case (l, r) of
-  (Nil, r)                     -> r
-  (l, Nil)                     -> l
-  (Tip lk lp lx, Tip rk rp rx)
-    | (lp, lk) < (rp, rk)      -> Bin lk lp lx m Nil r
-    | otherwise                -> Bin rk rp rx m l Nil
-  (Tip lk lp lx, Bin rk rp rx rm rl rr)
-    | (lp, lk) < (rp, rk)      -> Bin lk lp lx m Nil r
-    | otherwise                -> Bin rk rp rx m l (pqMerge rm rl rr)
-  (Bin lk lp lx lm ll lr, Tip rk rp rx)
-    | (lp, lk) < (rp, rk)      -> Bin lk lp lx m (pqMerge lm ll lr) r
-    | otherwise                -> Bin rk rp rx m l Nil
-  (Bin lk lp lx lm ll lr, Bin rk rp rx rm rl rr)
-    | (lp, lk) < (rp, rk)      -> Bin lk lp lx m (pqMerge lm ll lr) r
-    | otherwise                -> Bin rk rp rx m l (pqMerge rm rl rr)
-
-
--- Flattener
--- ---------
-
-flattenDFS :: Collapse a -> [a]
-flattenDFS (CSup k a b) = flatten a ++ flatten b
-flattenDFS (CVal x)     = [x]
-flattenDFS (CInc x)     = flattenDFS x
-flattenDFS (CDec x)     = flattenDFS x
-flattenDFS CEra         = []
-
-flattenBFS :: Collapse a -> [a]
-flattenBFS term = go term (sqNew :: SQ (Collapse a)) where
+flatten :: CTerm -> [CTerm]
+flatten term = go term (sqNew :: SQ CTerm) where
   go (CSup k a b) sq = go CEra (sqPut b $ sqPut a $ sq)
-  go (CVal x)     sq = x : go CEra sq
-  go (CInc x)     sq = go x sq
-  go (CDec x)     sq = go x sq
-  go CEra         sq = case sqPop sq of
-    Just (v,sq) -> go v sq
-    Nothing     -> []
-
--- Priority-Queue Flattener
--- ------------------------
--- * priority starts at 0
--- * since PQ is a min-queue, we invert the scoers:
--- * passing through (CInc t) subs 1 ; (CDec t) adds 1
--- * when no Inc/Dec are present every node has priority == depth
---   hence the order matches plain BFS exactly (stable heap).
-
-flattenPRI :: Collapse a -> [a]
-flattenPRI term = go 1 (Tip 0 0 term) where
-  go i pq = case pqPop pq of
-    Nothing -> []
-    Just (_, pri, node, pq') -> case node of
-      CEra   -> go i pq'
-      CVal v -> v : go i pq'
-      CInc t -> go (i + 1) (pqPush i (pri - 1) t pq')
-      CDec t -> go (i + 1) (pqPush i (pri + 1) t pq')
-      CSup _ a b ->
-        let pq1 = (pqPush (i + 0) (pri + 1) a pq')
-            pq2 = (pqPush (i + 1) (pri + 1) b pq1)
-        in go (i + 2) pq2
-
--- Default Flattener
--- -----------------
-
-flatten :: Collapse a -> [a]
-flatten = flattenPRI
-
--- Flat Collapser
--- --------------
+  go CEra         sq = case sqPop sq of { Just (v,sq) -> go v sq ; Nothing -> [] }
+  go x            sq = x : go CEra sq
 
 doCollapseFlatAt :: ReduceAt -> Book -> Loc -> HVM [Core]
 doCollapseFlatAt reduceAt book host = do
-  coll <- doCollapseAt reduceAt book host
-  return $ flatten coll
+  initialCore <- collapseDupsAt IM.empty reduceAt book host
+  let initialCTerm = coreToCTerm initialCore
+  let collapsedCTerm = collapse [initialCTerm] start
+  let flattenedCTerms = flatten collapsedCTerm
+  let finalCores = map ctermToCore flattenedCTerms
+  return finalCores
+
+-- Convert Core to CTerm
+coreToCTerm :: Core -> CTerm
+coreToCTerm core = case core of
+  Var name        -> CVar name
+  Ref name fid args -> CRef name fid (map coreToCTerm args)
+  Era             -> CEra
+  Lam name body   -> CLam name (coreToCTerm body)
+  App fun arg     -> CApp (coreToCTerm fun) (coreToCTerm arg)
+  Sup lab a b     -> CSup lab (coreToCTerm a) (coreToCTerm b)
+  Ctr name fields -> CCtr name (map coreToCTerm fields)
+  U32 val         -> CU32 val
+  Chr val         -> CChr val
+  Op2 oper a b    -> COp2 oper (coreToCTerm a) (coreToCTerm b)
+  Let m n v f     -> CLet m n (coreToCTerm v) (coreToCTerm f)
+  Mat t v m c     -> CMat t (coreToCTerm v) (map (fmap coreToCTerm) m) (map (\(cn,vs,b) -> (cn,vs,coreToCTerm b)) c)
+  Inc x           -> CInc (coreToCTerm x)
+  Dec x           -> CDec (coreToCTerm x)
+  _               -> error "coreToCTerm: unsupported Core construct"
+
+-- Convert CTerm to Core
+ctermToCore :: CTerm -> Core
+ctermToCore cterm = case cterm of
+  CVar name       -> Var name
+  CRef name fid args -> Ref name fid (map ctermToCore args)
+  CEra            -> Era
+  CLam name body  -> Lam name (ctermToCore body)
+  CApp fun arg    -> App (ctermToCore fun) (ctermToCore arg)
+  CSup lab a b    -> Sup lab (ctermToCore a) (ctermToCore b)
+  CCtr name fields-> Ctr name (map ctermToCore fields)
+  CU32 val        -> U32 val
+  CChr val        -> Chr val
+  COp2 oper a b   -> Op2 oper (ctermToCore a) (ctermToCore b)
+  CLet m n v f    -> Let m n (ctermToCore v) (ctermToCore f)
+  CMat t v m c    -> Mat t (ctermToCore v) (map (fmap ctermToCore) m) (map (\(cn,vs,b) -> (cn,vs,ctermToCore b)) c)
+  CInc x          -> Inc (ctermToCore x)
+  CDec x          -> Dec (ctermToCore x)
+  _               -> error "ctermToCore: unsupported CTerm construct"

From 0d729fc7a3a44615bdbfa011af46239497b0580f Mon Sep 17 00:00:00 2001
From: Lorenzobattistela <lorenzobattistela@gmail.com>
Date: Mon, 4 Aug 2025 17:17:57 -0300
Subject: [PATCH 2/5] add priority flattening

---
 src/HVM/Collapse.hs | 98 ++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 97 insertions(+), 1 deletion(-)

diff --git a/src/HVM/Collapse.hs b/src/HVM/Collapse.hs
index c67f889..37ca665 100644
--- a/src/HVM/Collapse.hs
+++ b/src/HVM/Collapse.hs
@@ -358,6 +358,102 @@ sqPop (SQ (x:xs) ys) = Just (x, SQ xs ys)
 sqPut :: a -> SQ a -> SQ a
 sqPut x (SQ xs ys) = SQ xs (x:ys)
 
+-- Priority Queue
+-- --------------
+-- A stable min-heap implemented with a radix tree.
+data PQ p v
+    = Bin !Word64 !p v !Word64 !(PQ p v) !(PQ p v)
+    | Tip !Word64 !p v
+    | Nil
+    deriving Show
+
+pqPush :: Ord p => Word64 -> p -> v -> PQ p v -> PQ p v
+pqPush k1 p1 x1 t = case t of
+  Nil -> Tip k1 p1 x1
+  (Tip k2 p2 x2)
+    | (p1, k1) < (p2, k2) -> link k1 p1 x1 k2 (Tip k2 p2 x2) Nil
+    | otherwise           -> link k2 p2 x2 k1 (Tip k1 p1 x1) Nil
+  (Bin k2 p2 x2 m l r)
+    | nomatch k1 k2 m, (p1, k1) < (p2, k2) -> link k1 p1 x1 k2 (Bin k2 p2 x2 m l r) Nil
+    | nomatch k1 k2 m                     -> link k2 p2 x2 k1 (Tip k1 p1 x1) (pqMerge m l r)
+    | (p1, k1) < (p2, k2), zero k2 m      -> Bin k1 p1 x1 m (pqPush k2 p2 x2 l) r
+    | (p1, k1) < (p2, k2)                 -> Bin k1 p1 x1 m l (pqPush k2 p2 x2 r)
+    | zero k1 m                           -> Bin k2 p2 x2 m (pqPush k1 p1 x1 l) r
+    | otherwise                           -> Bin k2 p2 x2 m l (pqPush k1 p1 x1 r)
+  where
+    nomatch :: Word64 -> Word64 -> Word64 -> Bool
+    nomatch k1 k2 m =
+      let maskW = complement (m-1) `xor` m
+      in (k1 .&. maskW) /= (k2 .&. maskW)
+
+    zero :: Word64 -> Word64 -> Bool
+    zero i m = i .&. m == 0
+
+    link :: Word64 -> p -> v -> Word64 -> (PQ p v) -> (PQ p v) -> (PQ p v)
+    link k p x k' fst snd =
+      let m = highestBitMask (k `xor` k')
+      in if zero m k'
+         then Bin k p x m fst snd
+         else Bin k p x m snd fst
+
+    highestBitMask :: Word64 -> Word64
+    highestBitMask x1 =
+      let x2 = x1 .|. x1 `shiftR` 1
+          x3 = x2 .|. x2 `shiftR` 2
+          x4 = x3 .|. x3 `shiftR` 4
+          x5 = x4 .|. x4 `shiftR` 8
+          x6 = x5 .|. x5 `shiftR` 16
+          x7 = x6 .|. x6 `shiftR` 32
+      in x7 `xor` (x7 `shiftR` 1)
+
+pqPop :: Ord p => PQ p v -> Maybe (Word64, p, v, PQ p v)
+pqPop t = case t of
+  Nil             -> Nothing
+  Tip k p x       -> Just (k, p, x, Nil)
+  Bin k p x m l r -> Just (k, p, x, pqMerge m l r)
+
+pqMerge :: Ord p => Word64 -> PQ p v -> PQ p v -> PQ p v
+pqMerge m l r = case (l, r) of
+  (Nil, r) -> r
+  (l, Nil) -> l
+  (Tip lk lp lx, Tip rk rp rx)
+    | (lp, lk) < (rp, rk) -> Bin lk lp lx m Nil r
+    | otherwise           -> Bin rk rp rx m l Nil
+  (Tip lk lp lx, Bin rk rp rx rm rl rr)
+    | (lp, lk) < (rp, rk) -> Bin lk lp lx m Nil r
+    | otherwise           -> Bin rk rp rx m l (pqMerge rm rl rr)
+  (Bin lk lp lx lm ll lr, Tip rk rp rx)
+    | (lp, lk) < (rp, rk) -> Bin lk lp lx m (pqMerge lm ll lr) r
+    | otherwise           -> Bin rk rp rx m l Nil
+  (Bin lk lp lx lm ll lr, Bin rk rp rx rm rl rr)
+    | (lp, lk) < (rp, rk) -> Bin lk lp lx m (pqMerge lm ll lr) r
+    | otherwise           -> Bin rk rp rx m l (pqMerge rm rl rr)
+
+-- Flattener 
+-- ---------------------------------------
+-- Traverses the CTerm tree, returning a list of non-superposed terms.
+-- It correctly handles Inc/Dec to adjust priority without including
+-- them in the final output.
+flattenPRI :: CTerm -> [CTerm]
+flattenPRI term = go 1 (Tip 0 0 term) where
+  -- The go loop takes a unique key 'i' and the priority queue 'pq'.
+  go :: Word64 -> PQ Int CTerm -> [CTerm]
+  go i pq = case pqPop pq of
+    Nothing -> []
+    Just (_, pri, node, pq') -> case node of
+      -- Traversal-control nodes: these are consumed to guide the search.
+      CEra -> go i pq'
+      CInc t -> go (i + 1) (pqPush i (pri - 1) t pq')
+      CDec t -> go (i + 1) (pqPush i (pri + 1) t pq')
+      CSup _ a b ->
+        let pq1 = pqPush (i + 0) (pri + 1) a pq'
+            pq2 = pqPush (i + 1) (pri + 1) b pq1
+        in go (i + 2) pq2
+      
+      -- Value nodes: any other constructor is a terminal value for the
+      -- flattening process and is added to the result list.
+      val -> val : go i pq'
+
 flatten :: CTerm -> [CTerm]
 flatten term = go term (sqNew :: SQ CTerm) where
   go (CSup k a b) sq = go CEra (sqPut b $ sqPut a $ sq)
@@ -369,7 +465,7 @@ doCollapseFlatAt reduceAt book host = do
   initialCore <- collapseDupsAt IM.empty reduceAt book host
   let initialCTerm = coreToCTerm initialCore
   let collapsedCTerm = collapse [initialCTerm] start
-  let flattenedCTerms = flatten collapsedCTerm
+  let flattenedCTerms = flattenPRI collapsedCTerm
   let finalCores = map ctermToCore flattenedCTerms
   return finalCores
 

From 025870a4d9c6152f164ff36424846402c3d7230a Mon Sep 17 00:00:00 2001
From: Lorenzobattistela <lorenzobattistela@gmail.com>
Date: Tue, 5 Aug 2025 18:50:16 -0300
Subject: [PATCH 3/5] fix collapse bug giving incorrect results
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The superposition collapse algorithm is responsible for handling
superposed values (marked with
SUP nodes) in the computation tree. When a computation contains
superpositions, the algorithm
must eventually "collapse" them.

In the `examples/enum_primes` example, the program generates a
superposition that produces two possible
results: λa ((a 853) 947) and λa ((a 947) 853). These are lambda
functions that, when given an
argument a, apply it to two numbers in different orders.

The bug was that the new collapse algorithm was producing just 947 and
853 - raw numbers without
the lambda wrapper or application structure. This happened because the
algorithm was collapsing
superpositions too eagerly during the initial tree traversal.

The new algorithm uses a sophisticated type-safe builder pattern that
processes terms
recursively. When it encountered a superposition (CSup), it would
immediately apply a "collapse
selection" mechanism (CCol) that forces branch selection based on
context. This works perfectly
for nested superpositions that need to be resolved based on their
surrounding context.

However, for top-level superpositions (those that should remain in the
final result), this eager
collapse was incorrect. The algorithm was destroying the lambda and
application structure that
wrapped the superposed values, leaving only the bare numeric values.

The fix identifies when we're processing top-level terms (when the tms
list is empty) and handles
  them differently:

1. For top-level superpositions (CSup): Instead of using the
context-dependent collapse
mechanism, preserve the superposition structure and process each branch
independently
2. For top-level lambdas (CLam): Process the lambda body independently
to preserve its internal
structure
3. For top-level applications (CApp): Process the function and argument
independently to maintain
  the application structure

This preserves the complete term structure for top-level expressions
while still using the
optimized collapse mechanism for nested superpositions where
context-dependent resolution is
correct.

The key insight is distinguishing between:
- Nested superpositions: Should be collapsed based on surrounding
context (original behavior)
- Top-level superpositions: Should be preserved for the final flattening
step (fixed behavior)
---
 src/HVM/Collapse.hs | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/HVM/Collapse.hs b/src/HVM/Collapse.hs
index 37ca665..4a24e0b 100644
--- a/src/HVM/Collapse.hs
+++ b/src/HVM/Collapse.hs
@@ -134,13 +134,19 @@ collapse :: [CTerm] -> SemiTerm -> CTerm
 collapse [] semi = case complete semi of CApp _ x -> x; term -> term
 collapse ((wnf -> tm) : tms) semi =
   case tm of
-    CSup l a b  -> CSup l (collapse (a : map (CCol l 0) tms) semi)
-                        (collapse (b : map (CCol l 1) tms) semi)
+    CSup l a b  -> if null tms 
+                     then CSup l (collapse [a] start) (collapse [b] start)
+                     else CSup l (collapse (a : map (CCol l 0) tms) semi)
+                                 (collapse (b : map (CCol l 1) tms) semi)
     CCol l i x  -> collapse (x : tms) $ extend semi (SS SZ) (CCol l i)
     CVar k      -> collapse tms $ extend semi SZ (CVar k)
     CEra        -> CEra
-    CLam x f    -> collapse (f : tms) $ extend semi (SS SZ) (\b -> CLam x b)
-    CApp f x    -> collapse (f : x : tms) semi
+    CLam x f    -> if null tms
+                     then CLam x (collapse [f] start)
+                     else collapse (f : tms) $ extend semi (SS SZ) (\b -> CLam x b)
+    CApp f x    -> if null tms
+                     then CApp (collapse [f] start) (collapse [x] start)
+                     else collapse (f : x : tms) semi
     COp2 o a b  -> collapse (a : b : tms) $ extend semi (SS (SS SZ)) (COp2 o)
     CCtr k xs   -> withSNat (length xs) $ \sNat -> collapse (xs ++ tms) $ extend semi sNat (buildCtr sNat k)
     CRef k i xs -> withSNat (length xs) $ \sNat -> collapse (xs ++ tms) $ extend semi sNat (buildRef sNat k i)

From e1b5e9e7aa0321b4fe3c2a4381131d53e9780ca5 Mon Sep 17 00:00:00 2001
From: Lorenzobattistela <lorenzobattistela@gmail.com>
Date: Wed, 6 Aug 2025 08:15:01 -0300
Subject: [PATCH 4/5] new collapse

---
 src/HVM/Collapse.hs | 192 ++++++++++++++++++++++++++++----------------
 1 file changed, 122 insertions(+), 70 deletions(-)

diff --git a/src/HVM/Collapse.hs b/src/HVM/Collapse.hs
index 4a24e0b..ee2fcf8 100644
--- a/src/HVM/Collapse.hs
+++ b/src/HVM/Collapse.hs
@@ -5,6 +5,8 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 module HVM.Collapse where
 
@@ -12,6 +14,7 @@ import Control.Monad (ap, forM, forM_)
 import Control.Monad.IO.Class
 import Data.Char (chr, ord)
 import qualified Data.Kind as DK
+import Unsafe.Coerce (unsafeCoerce)
 import Data.IORef
 import Data.Bits ((.&.), xor, (.|.), complement, shiftR)
 import Data.Word
@@ -61,6 +64,7 @@ type family CtrT (n :: Nat) :: DK.Type where
   CtrT (S p) = CTerm -> CtrT p
 
 data SomeSNat where SomeSNat :: SNat n -> SomeSNat
+
 toSomeSNat :: Int -> SomeSNat
 toSomeSNat 0 = SomeSNat SZ
 toSomeSNat n = case toSomeSNat (n-1) of SomeSNat s -> SomeSNat (SS s)
@@ -68,19 +72,6 @@ toSomeSNat n = case toSomeSNat (n-1) of SomeSNat s -> SomeSNat (SS s)
 withSNat :: Int -> (forall n. SNat n -> r) -> r
 withSNat n f = case toSomeSNat n of SomeSNat s -> f s
 
--- Recursive, type-safe builder functions
-buildCtr :: SNat n -> String -> CtrT n
-buildCtr s k = buildCtr' s [] where
-  buildCtr' :: SNat m -> [CTerm] -> CtrT m
-  buildCtr' SZ     acc = CCtr k (reverse acc)
-  buildCtr' (SS s') acc = \arg -> buildCtr' s' (arg : acc)
-
-buildRef :: SNat n -> String -> Word16 -> CtrT n
-buildRef s k i = buildRef' s [] where
-  buildRef' :: SNat m -> [CTerm] -> CtrT m
-  buildRef' SZ      acc = CRef k i (reverse acc)
-  buildRef' (SS s') acc = \arg -> buildRef' s' (arg : acc)
-
 data SemiTerm where
   SemiTerm :: SNat k -> (CTerm -> CtrT k) -> SemiTerm
 
@@ -114,62 +105,123 @@ complete (SemiTerm (SS p) l) = complete (SemiTerm p (l (CVar "X")))
 
 
 wnf :: CTerm -> CTerm
+wnf (CApp f x)   = app f x
 wnf (CCol l i x) = col l i x
 wnf v            = v
 
+app :: CTerm -> CTerm -> CTerm
+app (wnf -> CLam k f)   (wnf -> x) = wnf $ substCTerm k x f
+app (wnf -> CSup l x y) (wnf -> v) = CSup l (CApp x (CCol l 0 v)) (CApp y (CCol l 1 v))
+app f                   x          = CApp f x
+
+substCTerm :: String -> CTerm -> CTerm -> CTerm
+substCTerm var val term = case term of
+  CVar v | v == var -> val
+  CVar v            -> CVar v
+  CRef n f args     -> CRef n f (map (substCTerm var val) args)
+  CEra              -> CEra
+  CLam v b | v /= var -> CLam v (substCTerm var val b)
+  CLam v b          -> CLam v b
+  CApp f x          -> CApp (substCTerm var val f) (substCTerm var val x)
+  CSup l a b        -> CSup l (substCTerm var val a) (substCTerm var val b)
+  CCtr n fields     -> CCtr n (map (substCTerm var val) fields)
+  CU32 v            -> CU32 v
+  CChr c            -> CChr c
+  COp2 o a b        -> COp2 o (substCTerm var val a) (substCTerm var val b)
+  CLet m v e b | v /= var -> CLet m v (substCTerm var val e) (substCTerm var val b)
+  CLet m v e b      -> CLet m v (substCTerm var val e) b
+  CMat t v m c      -> CMat t (substCTerm var val v) 
+                          (map (\(k,e) -> (k, substCTerm var val e)) m)
+                          (map (\(cn,vs,b) -> if var `elem` vs then (cn,vs,b) else (cn,vs,substCTerm var val b)) c)
+  CInc x            -> CInc (substCTerm var val x)
+  CDec x            -> CDec (substCTerm var val x)
+  CCol l i x        -> CCol l i (substCTerm var val x)
+
 col :: Word32 -> Int -> CTerm -> CTerm
-col l i (wnf -> CSup r x y)   = if l == r then [x, y] !! i else CSup r (col l i x) (col l i y)
-col l i (wnf -> CLam n f)     = CLam n (col l i f)
-col l i (wnf -> CApp f x)     = CApp (col l i f) (col l i x)
-col l i (wnf -> CCtr k xs)    = CCtr k (map (col l i) xs)
-col l i (wnf -> CRef k r xs)  = CRef k r (map (col l i) xs)
-col l i (wnf -> COp2 o a b)   = COp2 o (col l i a) (col l i b)
-col l i (wnf -> CLet m n v b) = CLet m n (col l i v) (col l i b)
-col l i (wnf -> CMat t s ms cs) = CMat t (col l i s) (map (fmap (col l i)) ms) (map (\(c,vs,b) -> (c,vs,col l i b)) cs)
-col l i (wnf -> CInc x)       = CInc (col l i x)
-col l i (wnf -> CDec x)       = CDec (col l i x)
-col l i (wnf -> x)            = x
+col l i (wnf -> CVar k)     = CVar k
+col l i (wnf -> CLam k f)   = CLam k (CCol l i f)
+col l i (wnf -> CApp f x)   = CApp f x
+col l i (wnf -> CCtr n fs)  = CCtr n (map (CCol l i) fs)
+col l i (wnf -> CEra)       = CEra
+col l i (wnf -> CSup r x y) = if l == r then [x,y] !! i else CSup r (CCol l i x) (CCol l i y)
+col l i (wnf -> CCol r j x) = CCol l i (CCol r j x)
+col l i (wnf -> CU32 v)     = CU32 v
+col l i (wnf -> CChr c)     = CChr c
+col l i (wnf -> COp2 o a b) = COp2 o (CCol l i a) (CCol l i b)
+col l i (wnf -> CRef n f args) = CRef n f (map (CCol l i) args)
+col l i (wnf -> CLet m v e b) = CLet m v (CCol l i e) (CCol l i b)
+col l i (wnf -> CMat t v m c) = CMat t (CCol l i v) 
+                                   (map (\(k,e) -> (k, CCol l i e)) m)
+                                   (map (\(cn,vs,b) -> (cn,vs,CCol l i b)) c)
+col l i (wnf -> CInc x)     = CInc (CCol l i x)
+col l i (wnf -> CDec x)     = CDec (CCol l i x)
 
 collapse :: [CTerm] -> SemiTerm -> CTerm
-collapse [] semi = case complete semi of CApp _ x -> x; term -> term
+collapse [] semi =
+  case complete semi of
+    CApp _ x  -> x
+    otherwise -> error "unreachable"
 collapse ((wnf -> tm) : tms) semi =
   case tm of
-    CSup l a b  -> if null tms 
-                     then CSup l (collapse [a] start) (collapse [b] start)
-                     else CSup l (collapse (a : map (CCol l 0) tms) semi)
-                                 (collapse (b : map (CCol l 1) tms) semi)
-    CCol l i x  -> collapse (x : tms) $ extend semi (SS SZ) (CCol l i)
-    CVar k      -> collapse tms $ extend semi SZ (CVar k)
-    CEra        -> CEra
-    CLam x f    -> if null tms
-                     then CLam x (collapse [f] start)
-                     else collapse (f : tms) $ extend semi (SS SZ) (\b -> CLam x b)
-    CApp f x    -> if null tms
-                     then CApp (collapse [f] start) (collapse [x] start)
-                     else collapse (f : x : tms) semi
-    COp2 o a b  -> collapse (a : b : tms) $ extend semi (SS (SS SZ)) (COp2 o)
-    CCtr k xs   -> withSNat (length xs) $ \sNat -> collapse (xs ++ tms) $ extend semi sNat (buildCtr sNat k)
-    CRef k i xs -> withSNat (length xs) $ \sNat -> collapse (xs ++ tms) $ extend semi sNat (buildRef sNat k i)
-    CU32 n      -> collapse tms $ extend semi SZ (CU32 n)
-    CChr c      -> collapse tms $ extend semi SZ (CChr c)
-    CInc x      -> collapse (x : tms) $ extend semi (SS SZ) CInc
-    CDec x      -> collapse (x : tms) $ extend semi (SS SZ) CDec
-    CLet m k v b-> collapse (v : b : tms) $ extend semi (SS (SS SZ)) (CLet m k)
-    CMat t v m c-> collapse tms $ extend semi SZ (CMat t v m c)
-    _           -> tm
-
-
-
--- The Collapse Monad 
--- ------------------
--- See: https://gist.github.com/VictorTaelin/60d3bc72fb4edefecd42095e44138b41
-
--- A bit-string
-data Bin
-  = O Bin
-  | I Bin
-  | E
-  deriving Show
+    CVar k       -> collapse tms $ extend semi SZ (CVar k)
+    CLam k f     -> 
+      let f' = substCTerm k (CVar k) f
+      in collapse (f' : tms) $ extend semi (SS SZ) (\body -> CLam k body)
+    CApp f x     -> collapse (f : x : tms) $ extend semi (SS (SS SZ)) CApp
+    CCtr n fields -> 
+      let arity = length fields
+      in withSNat arity $ \snat ->
+        collapse (fields ++ tms) $ extend semi snat (unsafeCoerce $ buildCtr n arity)
+    CEra         -> CEra
+    CSup l a b   -> CSup l (collapse (a : map (CCol l 0) tms) semi) (collapse (b : map (CCol l 1) tms) semi)
+    CCol l i x   -> collapse (x : tms) $ extend semi (SS SZ) (CCol l i)
+    CU32 v       -> collapse tms $ extend semi SZ (CU32 v)
+    CChr c       -> collapse tms $ extend semi SZ (CChr c)
+    COp2 o a b   -> collapse (a : b : tms) $ extend semi (SS (SS SZ)) (COp2 o)
+    CRef n f args -> 
+      let arity = length args
+      in withSNat arity $ \snat ->
+        collapse (args ++ tms) $ extend semi snat (unsafeCoerce $ buildRef n f arity)
+    CLet m v e b -> collapse (e : b : tms) $ extend semi (SS (SS SZ)) (CLet m v)
+    CMat t v m c -> 
+      let moves = map snd m
+          movesArity = length moves
+      in withSNat (1 + movesArity) $ \snat ->
+        collapse (v : moves ++ tms) $ extend semi snat (unsafeCoerce $ buildMat t (map fst m) c (1 + movesArity))
+    CInc x       -> collapse (x : tms) $ extend semi (SS SZ) CInc
+    CDec x       -> collapse (x : tms) $ extend semi (SS SZ) CDec
+
+buildCtr :: forall n. String -> Int -> CtrT n
+buildCtr name = go where
+  go :: Int -> CtrT n
+  go 0 = unsafeCoerce (CCtr name [])
+  go n = unsafeCoerce $ \x -> unsafeCoerce $ buildCtrAux name (n-1) [x]
+  
+  buildCtrAux :: String -> Int -> [CTerm] -> CTerm
+  buildCtrAux name 0 acc = CCtr name (reverse acc)
+  buildCtrAux name n acc = unsafeCoerce $ \x -> buildCtrAux name (n-1) (x:acc)
+
+buildRef :: forall n. String -> Word16 -> Int -> CtrT n
+buildRef name fid = go where
+  go :: Int -> CtrT n
+  go 0 = unsafeCoerce (CRef name fid [])
+  go n = unsafeCoerce $ \x -> unsafeCoerce $ buildRefAux name fid (n-1) [x]
+  
+  buildRefAux :: String -> Word16 -> Int -> [CTerm] -> CTerm  
+  buildRefAux name fid 0 acc = CRef name fid (reverse acc)
+  buildRefAux name fid n acc = unsafeCoerce $ \x -> buildRefAux name fid (n-1) (x:acc)
+
+buildMat :: forall n. MatT -> [String] -> [(String, [String], CTerm)] -> Int -> CtrT n
+buildMat t moveKeys cases = go where
+  go :: Int -> CtrT n
+  go 1 = unsafeCoerce $ \v -> CMat t v [] cases
+  go n = unsafeCoerce $ buildMatAux t moveKeys cases n Nothing []
+  
+  buildMatAux :: MatT -> [String] -> [(String, [String], CTerm)] -> Int -> Maybe CTerm -> [CTerm] -> CTerm
+  buildMatAux t mk cs 1 (Just v) moves = CMat t v (zip mk (reverse moves)) cs
+  buildMatAux t mk cs n Nothing moves = unsafeCoerce $ \v -> buildMatAux t mk cs (n-1) (Just v) moves
+  buildMatAux t mk cs n (Just v) moves = unsafeCoerce $ \m -> buildMatAux t mk cs (n-1) (Just v) (m:moves)
+
 
 -- Dup Collapser
 -- -------------
@@ -337,19 +389,19 @@ collapseDupsAt state@(paths) reduceAt book host = unsafeInterleaveIO $ do
 
 -- Tree Collapser
 -- --------------
-
-doCollapseAt :: ReduceAt -> Book -> Loc -> HVM Core
-doCollapseAt reduceAt book host = do
+--
+-- doCollapseAt :: ReduceAt -> Book -> Loc -> HVM Core
+-- doCollapseAt reduceAt book host = do
   -- Step 1: Read the low-level representation into a high-level Core term.
-  initialCore <- collapseDupsAt IM.empty reduceAt book host
+--   initialCore <- collapseDupsAt IM.empty reduceAt book host
   -- Step 2: Convert to our internal CTerm AST.
-  let initialCTerm = coreToCTerm initialCore
+--   let initialCTerm = coreToCTerm initialCore
   -- Step 3: Run the new, powerful collapse algorithm.
-  let collapsedCTerm = collapse [initialCTerm] start
+--   let collapsedCTerm = collapse [initialCTerm] start
   -- Step 4: Convert the resulting Sup-tree back to the public Core type.
-  let finalCore = ctermToCore collapsedCTerm
-  return finalCore
-
+--   let finalCore = ctermToCore collapsedCTerm
+--   return finalCore
+--
 
 data SQ a = SQ [a] [a]
 

From 54079aaa9dc4e9131e9f67ab44c987219ed13a66 Mon Sep 17 00:00:00 2001
From: Lorenzobattistela <lorenzobattistela@gmail.com>
Date: Wed, 6 Aug 2025 08:22:47 -0300
Subject: [PATCH 5/5] unneeded subst

---
 src/HVM/Collapse.hs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/HVM/Collapse.hs b/src/HVM/Collapse.hs
index ee2fcf8..bc897d2 100644
--- a/src/HVM/Collapse.hs
+++ b/src/HVM/Collapse.hs
@@ -165,8 +165,7 @@ collapse ((wnf -> tm) : tms) semi =
   case tm of
     CVar k       -> collapse tms $ extend semi SZ (CVar k)
     CLam k f     -> 
-      let f' = substCTerm k (CVar k) f
-      in collapse (f' : tms) $ extend semi (SS SZ) (\body -> CLam k body)
+      collapse (f : tms) $ extend semi (SS SZ) (CLam k)
     CApp f x     -> collapse (f : x : tms) $ extend semi (SS (SS SZ)) CApp
     CCtr n fields -> 
       let arity = length fields