idana: Cleanup

2 files changed, 22 insertions, 75 deletions

diff --git a/src/Analysis/Identity.hs b/src/Analysis/Identity.hs
index 7e10481..020ca34 100644
--- a/src/Analysis/Identity.hs
+++ b/src/Analysis/Identity.hs
@@ -30,32 +30,6 @@ data ValId t where
   VIScal :: Int -> ValId (TScal t)
   VIAccum :: Int -> ValId (TAccum t)
 
-  -- | We don't know what this consists of, but it's a value, and let's just
-  -- give it an ID nevertheless.
-  VIThing :: STy t -> Int -> ValId t
-
-instance Eq (ValId t) where
-  VINil         == VINil           = True
-  VINil         == _               = False
-  VIPair a b    == VIPair a' b'    = a == a' && b == b'
-  VIPair{}      == _               = False
-  VIEither a    == VIEither a'     = a == a'
-  VIEither{}    == _               = False
-  VIEither' a b == VIEither' a' b' = a == a' && b == b'
-  VIEither'{}   == _               = False
-  VIMaybe a     == VIMaybe a'      = a == a'
-  VIMaybe{}     == _               = False
-  VIMaybe' a    == VIMaybe' a'     = a == a'
-  VIMaybe'{}    == _               = False
-  VIArr i is    == VIArr i' is'    = i == i' && is == is'
-  VIArr{}       == _               = False
-  VIScal i      == VIScal i'       = i == i'
-  VIScal{}      == _               = False
-  VIAccum i     == VIAccum i'      = i == i'
-  VIAccum{}     == _               = False
-  VIThing _ i   == VIThing _ i'    = i == i'
-  VIThing{}     == _               = False
-
 instance PrettyX ValId where
   prettyX = \case
     VINil -> ""
@@ -69,7 +43,6 @@ instance PrettyX ValId where
     VIArr i is -> 'A' : show i ++ "[" ++ intercalate "," (map show (toList is)) ++ "]"
     VIScal i -> show i
     VIAccum i -> 'C' : show i
-    VIThing _ i -> '{' : show i ++ "}"
 
 -- | Symbolic partial evaluation.
 identityAnalysis :: SList STy env -> Expr x env t -> Expr ValId env t
@@ -95,15 +68,13 @@ idana env expr = case expr of
 
   EFst _ e -> do
     (v, e') <- idana env e
-    v' <- case v of VIPair v1 _ -> pure v1
-                    _ -> genIds (typeOf expr)
-    pure (v', EFst v' e')
+    let VIPair v1 _ = v
+    pure (v1, EFst v1 e')
 
   ESnd _ e -> do
     (v, e') <- idana env e
-    v' <- case v of VIPair _ v2 -> pure v2
-                    _ -> genIds (typeOf expr)
-    pure (v', ESnd v' e')
+    let VIPair _ v2 = v
+    pure (v2, ESnd v2 e')
 
   ENil _ -> pure (VINil, ENil VINil)
 
@@ -136,13 +107,6 @@ idana env expr = case expr of
         (_, e3') <- idana (v1'r `SCons` env) e3
         res <- genIds (typeOf expr)
         pure (res, ECase res e1' e2' e3')
-      VIThing _ _ -> do
-        x2 <- genIds t1
-        x3 <- genIds t2
-        (v2, e2') <- idana (x2 `SCons` env) e2
-        (v3, e3') <- idana (x3 `SCons` env) e3
-        res <- unify v2 v3
-        pure (res, ECase res e1' e2' e3')
 
   ENothing _ t -> pure (VIMaybe Nothing, ENothing (VIMaybe Nothing) t)
 
@@ -169,12 +133,6 @@ idana env expr = case expr of
         (v1, e1') <- idana env e1
         res <- unify v1 v2
         pure (res, EMaybe res e1' e2' e3')
-      VIThing _ _ -> do
-        (v1, e1') <- idana env e1
-        scrap <- genIds t1
-        (v2, e2') <- idana (scrap `SCons` env) e2
-        res <- unify v1 v2
-        pure (res, EMaybe res e1' e2' e3')
 
   EConstArr _ dim t arr -> do
     x1 <- VIArr <$> genId <*> vecReplicateA dim genId
@@ -189,19 +147,19 @@ idana env expr = case expr of
 
   EFold1Inner _ e1 e2 e3 -> do
     let t1 = typeOf e1
-        STArr dim _ = typeOf e3
     x1 <- genIds t1
     x2 <- genIds t1
     (_, e1') <- idana (x1 `SCons` x2 `SCons` env) e1
     (_, e2') <- idana env e2
     (v3, e3') <- idana env e3
-    res <- VIArr <$> genId <*> (vecTail <$> valArrShape dim v3)
+    let VIArr _ (_ :< sh) = v3
+    res <- VIArr <$> genId <*> pure sh
     pure (res, EFold1Inner res e1' e2' e3')
 
   ESum1Inner _ e1 -> do
-    let STArr dim _ = typeOf e1
     (v1, e1') <- idana env e1
-    res <- VIArr <$> genId <*> (vecTail <$> valArrShape dim v1)
+    let VIArr _ (_ :< sh) = v1
+    res <- VIArr <$> genId <*> pure sh
     pure (res, ESum1Inner res e1')
 
   EUnit _ e1 -> do
@@ -210,22 +168,23 @@ idana env expr = case expr of
     pure (res, EUnit res e1')
 
   EReplicate1Inner _ e1 e2 -> do
-    let STArr dim _ = typeOf e2
     (v1, e1') <- idana env e1
+    let VIScal v1' = v1
     (v2, e2') <- idana env e2
-    res <- VIArr <$> genId <*> ((valScalId v1 :<) <$> valArrShape dim v2)
+    let VIArr _ sh = v2
+    res <- VIArr <$> genId <*> pure (v1' :< sh)
     pure (res, EReplicate1Inner res e1' e2')
 
   EMaximum1Inner _ e1 -> do
-    let STArr dim _ = typeOf e1
     (v1, e1') <- idana env e1
-    res <- VIArr <$> genId <*> (vecTail <$> valArrShape dim v1)
+    let VIArr _ (_ :< sh) = v1
+    res <- VIArr <$> genId <*> pure sh
     pure (res, EMaximum1Inner res e1')
 
   EMinimum1Inner _ e1 -> do
-    let STArr dim _ = typeOf e1
     (v1, e1') <- idana env e1
-    res <- VIArr <$> genId <*> (vecTail <$> valArrShape dim v1)
+    let VIArr _ (_ :< sh) = v1
+    res <- VIArr <$> genId <*> pure sh
     pure (res, EMinimum1Inner res e1')
 
   EConst _ t val -> do
@@ -238,10 +197,10 @@ idana env expr = case expr of
     pure (res, EIdx0 res e1')
 
   EIdx1 _ e1 e2 -> do
-    let STArr dim _ = typeOf e1
     (v1, e1') <- idana env e1
+    let VIArr _ sh = v1
     (_, e2') <- idana env e2
-    res <- VIArr <$> genId <*> (vecTail <$> valArrShape dim v1)
+    res <- VIArr <$> genId <*> pure (vecInit sh)
     pure (res, EIdx1 res e1' e2')
 
   EIdx _ e1 e2 -> do
@@ -253,7 +212,8 @@ idana env expr = case expr of
   EShape _ e1 -> do
     let STArr dim _ = typeOf e1
     (v1, e1') <- idana env e1
-    res <- vecToShids dim <$> valArrShape dim v1
+    let VIArr _ sh = v1
+        res = vecToShids dim sh
     pure (res, EShape res e1')
 
   EOp _ (op :: SOp a t) e1 -> do
@@ -337,10 +297,6 @@ unify (VIMaybe' a) (VIMaybe' b) = VIMaybe' <$> unify a b
 unify (VIArr i is) (VIArr j js) = VIArr <$> unifyID i j <*> vecZipWithA unifyID is js
 unify (VIScal i) (VIScal j) = VIScal <$> unifyID i j
 unify (VIAccum i) (VIAccum j) = VIAccum <$> unifyID i j
-unify (VIThing t i) (VIThing _ j) | i == j = pure $ VIThing t i
-                                  | otherwise = genIds t
-unify (VIThing t _) _ = genIds t
-unify _ (VIThing t _) = genIds t
 
 unifyID :: Int -> Int -> IdGen Int
 unifyID i j | i == j = pure i
@@ -358,17 +314,7 @@ genIds STAccum{} = VIAccum <$> genId
 shidsToVec :: SNat n -> ValId (Tup (Replicate n TIx)) -> IdGen (Vec n Int)
 shidsToVec SZ _ = pure VNil
 shidsToVec (SS n) (VIPair is (VIScal i)) = (i :<) <$> shidsToVec n is
-shidsToVec (SS n) (VIPair is (VIThing _ i)) = (i :<) <$> shidsToVec n is
-shidsToVec n VIThing{} = vecReplicateA n genId
 
 vecToShids :: SNat n -> Vec n Int -> ValId (Tup (Replicate n TIx))
 vecToShids SZ VNil = VINil
 vecToShids (SS n) (i :< is) = VIPair (vecToShids n is) (VIScal i)
-
-valScalId :: ValId (TScal t) -> Int
-valScalId (VIScal i) = i
-valScalId (VIThing _ i) = i
-
-valArrShape :: SNat n -> ValId (TArr n t) -> IdGen (Vec n Int)
-valArrShape _ (VIArr _ v) = pure v
-valArrShape n _ = vecReplicateA n genId
diff --git a/src/Data.hs b/src/Data.hs
index d83c206..1304a5f 100644
--- a/src/Data.hs
+++ b/src/Data.hs
@@ -139,8 +139,9 @@ vecZipWithA :: Applicative f => (a -> b -> f c) -> Vec n a -> Vec n b -> f (Vec
 vecZipWithA _ VNil VNil = pure VNil
 vecZipWithA f (x :< xs) (y :< ys) = (:<) <$> f x y <*> vecZipWithA f xs ys
 
-vecTail :: Vec (S n) a -> Vec n a
-vecTail (_ :< xs) = xs
+vecInit :: Vec (S n) a -> Vec n a
+vecInit (_ :< VNil) = VNil
+vecInit (x :< xs@(_ :< _)) = x :< vecInit xs
 
 unsafeCoerceRefl :: a :~: b
 unsafeCoerceRefl = unsafeCoerce Refl