alpha equality for sharing optimization

Author: andreasabel

Makefile

@@ -13,7 +13,7 @@ bench : helf
 	$(time) $(helf) examples/ltal/w32_sig_semant.elf
 
 current : helf
-	$(helf) test/succeed/z.elf
+	$(helf) test/succeed/y.elf
 
 helf : 
 	make -C src helf

src/Abstract.hs

@@ -1,12 +1,18 @@
-{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, TypeSynonymInstances #-}
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, TypeSynonymInstances, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
 
 module Abstract where
 
 import Prelude hiding (foldr)
 
+import Control.Monad.Reader
+
 import Data.Set (Set)
 import qualified Data.Set as Set 
 
+-- import Data.Map (Map)
+-- import qualified Data.Map as Map 
+import qualified Data.IntMap as M 
+
 import Data.Foldable
 import Data.Traversable
 
@@ -104,6 +110,102 @@ appView = loop [] where
   loop acc f         = (f, acc)
 -}
 
+-- * alpha equality
+
+newtype Alpha a = Alpha a
+  deriving (Functor)
+
+instance Show a => Show (Alpha a) where
+  show (Alpha a) = show a
+
+instance Ord (Alpha Expr) where
+  compare (Alpha e) (Alpha e') = aCompare e e'
+
+instance Ord (Alpha a) => Eq (Alpha a) where
+  a == a' = compare a a' == EQ
+  -- (Alpha e) == (Alpha e') = aeq e e' Map.empty
+
+type IMap = M.IntMap UID -- map directed from left to right
+type Cmp = Reader IMap
+
+class OrdAlpha a where
+  aCompare :: a -> a -> Ordering
+  aCompare e1 e2 = runReader (acmp e1 e2) M.empty
+
+--   acmp :: MonadReader IMap m => a -> a -> m Ordering
+  acmp :: a -> a -> Cmp Ordering
+  acmp e1 e2 = return $ aCompare e1 e2
+
+instance OrdAlpha Name where
+  acmp (Name x _) (Name y _) 
+    | x == y = return EQ
+    | otherwise = do
+        m <- ask
+        case M.lookup x m of
+          Nothing -> return $ compare x y
+          Just y' -> return $ compare y' y
+
+-- | Just look at UID
+instance OrdAlpha Ident where
+  acmp x y = acmp (name x) (name y)
+
+instance OrdAlpha Expr where
+  acmp e e' = case (e, e') of
+
+    (Ident x, Ident x') -> acmp x x'
+    (Ident _, _) -> return LT
+    (_, Ident _) -> return GT
+
+    (App f e, App f' e') -> lexM [ acmp f f', acmp e e' ]
+    (App _ _, _) -> return LT
+    (_, App _ _) -> return GT
+
+    (Pi Nothing a b, Pi Nothing a' b') -> acmp (a,b) (a',b')
+    (Pi Nothing _ _, _) -> return LT
+    (_, Pi Nothing _ _) -> return GT
+
+    (Pi (Just x) a b, Pi (Just x') a' b') -> lexM 
+      [ acmp a a'
+      , local (M.insert (uid x) (uid x')) $ acmp b b' ]
+    (Pi (Just _) _ _, _) -> return LT
+    (_, Pi (Just _) _ _) -> return GT
+
+    (Lam x a e, Lam x' a' e') -> lexM 
+      [ acmp a a'
+      , local (M.insert (uid x) (uid x')) $ acmp e e' ]
+    (Lam _ _ _, _) -> return LT
+    (_, Lam _ _ _) -> return GT
+
+    (Typ, Typ)   -> return EQ
+{-
+    (Typ, _)     -> return LT
+    (_, Typ)     -> return GT
+-}
+
+-- | Lexicographic comparison
+instance (OrdAlpha a, OrdAlpha b) => OrdAlpha (a,b) where
+  acmp (a1,b1) (a2,b2) = lexM [acmp a1 a2, acmp b1 b2]
+
+-- | Use only for lists of equal length!
+instance (OrdAlpha a) => OrdAlpha [a] where
+  acmp as bs = lexM $ zipWith acmp as bs
+
+instance (OrdAlpha a) => OrdAlpha (Maybe a) where
+  acmp Nothing Nothing   = return EQ
+  acmp Nothing (Just _)  = return LT
+  acmp (Just _) Nothing  = return GT
+  acmp (Just a) (Just b) = acmp a b
+
+-- | Lazy lexicographic combination..
+lexM :: Monad m => [m Ordering] -> m Ordering
+lexM []     = return EQ
+lexM (m:ms) = do
+  o <- m
+  case o of
+     LT -> return LT
+     GT -> return GT
+     EQ -> lexM ms
+
 -- * Queries
 
 globalIds :: Expr -> Set Ident

src/TermGraph.hs

@@ -17,6 +17,7 @@ import Debug.Trace
 import Text.PrettyPrint
 
 import ORef
+import Abstract (Alpha(..))
 import qualified Abstract as A
 import Signature
 import Util hiding (pretty)
@@ -181,17 +182,17 @@ type TransT a = StateT (TDict a)
 
 --  Direct translation from A.Expr
 
-addPredefs :: MonadTG m => TDict A.Expr -> m (TDict A.Expr)
+addPredefs :: MonadTG m => TDict AExpr -> m (TDict AExpr)
 addPredefs dict = do
   ty <- predefType
-  return $ Map.insert A.Typ ty dict
+  return $ Map.insert (Alpha A.Typ) ty dict
 
 
 trans ::  (Signature Term sig, MonadReader sig m, MonadTG m) => 
   Env -> A.Expr -> m Term
 trans rho e = -- trace ("translating " ++ show e) $ do
   evalStateT (transT e) =<< addPredefs 
-                     (Map.mapKeysMonotonic (A.Ident . A.Var) rho)
+                     (Map.mapKeysMonotonic (Alpha . A.Ident . A.Var) rho)
 
 {-
 -- Translation via BTm
@@ -291,13 +292,15 @@ con x t = Atom (A.Con x) t []
 def :: A.Name -> Type -> Term -> Term'
 def x t v = Def x t v []
 
+type AExpr = Alpha A.Expr
+
 transT :: (Signature Term sig, MonadReader sig m, MonadTG m) => 
-  A.Expr -> TransT A.Expr m Term
-transT = transG (Right <.> transT')
+  A.Expr -> TransT AExpr m Term
+transT e = transG (Right <.> transT') (Alpha e)
 
 transT' ::  (Signature Term sig, MonadReader sig m, MonadTG m) => 
-  A.Expr -> TransT A.Expr m Term'
-transT' e = do
+  AExpr -> TransT AExpr m Term'
+transT' (Alpha e) = do
   let (f, sp) = appView e
   if null sp then 
       case f of
@@ -311,7 +314,7 @@ transT' e = do
 --           return $ Var n -- only for binding in Lam and Pi
          -- A.Typ             -> predefType  -- impossible case
          A.Lam n _ e       -> do
-           x <- transAddBind (A.Ident . A.Var) n 
+           x <- transAddBind (Alpha . A.Ident . A.Var) n 
            Abs x <$> transT e
 --       A.Lam n _ e       -> Abs <$> transT (A.Ident $ A.Var n) <*> transT e
          A.Pi Nothing  a b -> Fun <$> transT a <*> (newORef =<< K <$> transT b)

test/succeed/y.elf

@@ -0,0 +1,7 @@
+%% 2011-11-09 
+
+tm : type.
+abs : (tm -> tm) -> tm.
+
+eq : tm -> tm -> type.
+eq/id : eq (abs [x]x) (abs [y]y).