Implement sorting of floated expressions

1 files changed, 26 insertions, 90 deletions

diff --git a/test/Main.hs b/test/Main.hs
index e7b303b..1a8d8e1 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -5,110 +5,46 @@
 {-# LANGUAGE StandaloneDeriving #-}
 module Main where
 
-import Data.Type.Equality
-
 import Data.Expr.SharingRecovery
 
+import Arith
 
-data Typ t where
-  TInt :: Typ Int
-  TBool :: Typ Bool
-  TPair :: Typ a -> Typ b -> Typ (a, b)
-  TFun :: Typ a -> Typ b -> Typ (a -> b)
-deriving instance Show (Typ t)
-
-instance TestEquality Typ where
-  testEquality TInt TInt = Just Refl
-  testEquality TBool TBool = Just Refl
-  testEquality (TPair a b) (TPair a' b')
-    | Just Refl <- testEquality a a'
-    , Just Refl <- testEquality b b'
-    = Just Refl
-  testEquality (TFun a b) (TFun a' b')
-    | Just Refl <- testEquality a a'
-    , Just Refl <- testEquality b b'
-    = Just Refl
-  testEquality _ _ = Nothing
-
-class KnownType t where τ :: Typ t
-instance KnownType Int where τ = TInt
-instance KnownType Bool where τ = TBool
-instance (KnownType a, KnownType b) => KnownType (a, b) where τ = TPair τ τ
-instance (KnownType a, KnownType b) => KnownType (a -> b) where τ = TFun τ τ
 
-data PrimOp a b where
-  POAddI :: PrimOp (Int, Int) Int
-  POMulI :: PrimOp (Int, Int) Int
-  POEqI :: PrimOp (Int, Int) Bool
-deriving instance Show (PrimOp a b)
+-- TODO: test cyclic expressions
 
-data Fixity = Infix | Prefix
-  deriving (Show)
 
-primOpPrec :: PrimOp a b -> (Int, (Int, Int))
-primOpPrec POAddI = (6, (6, 7))
-primOpPrec POMulI = (7, (7, 8))
-primOpPrec POEqI = (4, (5, 5))
+a_bin :: (KnownType a, KnownType b, KnownType c)
+      => PrimOp (a, b) c
+      -> PHOASExpr Typ v ArithF a
+      -> PHOASExpr Typ v ArithF b
+      -> PHOASExpr Typ v ArithF c
+a_bin op a b = PHOASOp τ (A_Prim op (PHOASOp τ (A_Pair a b)))
 
-prettyPrimOp :: Fixity -> PrimOp a b -> ShowS
-prettyPrimOp fix op =
-  let s = case op of
-            POAddI -> "+"
-            POMulI -> "*"
-            POEqI -> "=="
-  in showString $ case fix of
-       Infix -> s
-       Prefix -> "(" ++ s ++ ")"
+lam :: (KnownType a, KnownType b)
+    => (PHOASExpr Typ v f a -> PHOASExpr Typ v f b) -> PHOASExpr Typ v f (a -> b)
+lam f = PHOASLam τ τ $ \arg -> f (PHOASVar τ arg)
 
-data ArithF r t where
-  A_Prim :: PrimOp a b -> r a -> ArithF r b
-  A_Pair :: r a -> r b -> ArithF r (a, b)
-  A_If :: r Bool -> r a -> r a -> ArithF r a
-deriving instance (forall a. Show (r a)) => Show (ArithF r t)
+(+!) :: PHOASExpr Typ v ArithF Int -> PHOASExpr Typ v ArithF Int -> PHOASExpr Typ v ArithF Int
+(+!) = a_bin POAddI
 
-instance Functor1 ArithF
-instance Traversable1 ArithF where
-  traverse1 f (A_Prim op x) = A_Prim op <$> f x
-  traverse1 f (A_Pair x y) = A_Pair <$> f x <*> f y
-  traverse1 f (A_If x y z) = A_If <$> f x <*> f y <*> f z
-
-prettyArithF :: Monad m
-             => (forall a. Int -> BExpr typ env ArithF a -> m ShowS)
-             -> Int -> ArithF (BExpr typ env ArithF) t -> m ShowS
-prettyArithF pr d = \case
-  A_Prim op (BOp _ (A_Pair a b)) -> do
-    let (dop, (dopL, dopR)) = primOpPrec op
-    a' <- pr dopL a
-    b' <- pr dopR b
-    return $ showParen (d > dop) $ a' . showString " " . prettyPrimOp Infix op . showString " " . b'
-  A_Prim op arg -> do
-    arg' <- pr 11 arg
-    return $ showParen (d > 10) $ prettyPrimOp Prefix op . showString " " . arg'
-  A_Pair a b -> do
-    a' <- pr 0 a
-    b' <- pr 0 b
-    return $ showString "(" . a' . showString ", " . b' . showString ")"
-  A_If a b c -> do
-    a' <- pr 0 a
-    b' <- pr 0 b
-    c' <- pr 0 c
-    return $ showParen (d > 0) $ showString "if " . a' . showString " then " . b' . showString " else " . c'
+(*!) :: PHOASExpr Typ v ArithF Int -> PHOASExpr Typ v ArithF Int -> PHOASExpr Typ v ArithF Int
+(*!) = a_bin POMulI
 
 -- λx. x + x
 ea_1 :: PHOASExpr Typ v ArithF (Int -> Int)
-ea_1 =
-  PHOASLam τ τ $ \arg ->
-    PHOASOp τ (A_Prim POAddI
-      (PHOASOp τ (A_Pair (PHOASVar τ arg) (PHOASVar τ arg))))
+ea_1 = lam $ \arg -> arg +! arg
 
 -- λx. let y = x + x in y * y
 ea_2 :: PHOASExpr Typ v ArithF (Int -> Int)
-ea_2 =
-  PHOASLam τ τ $ \arg ->
-    let y = PHOASOp τ (A_Prim POAddI
-              (PHOASOp τ (A_Pair (PHOASVar τ arg) (PHOASVar τ arg))))
-    in PHOASOp τ (A_Prim POMulI
-         (PHOASOp τ (A_Pair y y)))
+ea_2 = lam $ \arg -> let y = arg +! arg
+                     in y *! y
+
+ea_3 :: PHOASExpr Typ v ArithF (Int -> Int)
+ea_3 = lam $ \arg ->
+  let y = arg +! arg
+      x = y *! arg
+  -- in (y +! x) +! (x +! y)
+  in (x +! y) +! (y +! x)
 
 main :: IO ()
-main = putStrLn $ prettyBExpr prettyArithF (sharingRecovery ea_2)
+main = putStrLn $ prettyBExpr prettyArithF (sharingRecovery ea_3)