de Bruijn memoizing translation unsound

Author: andreasabel

Makefile

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

src/HerBruijnVal.hs

@@ -269,7 +269,7 @@ evaluate2 expr env =
                     SigDef t v <- sigLookup' (uid x) <$> ask
                     return $ def x v t
       BApp t1 t2  -> Util.appM2 apply (evaluate' t1 env) (evaluate' t2 env)
-      BLam x t    -> (\z -> return $ HLam x z) =<< (evaluate' t env) 
+      BLam (Annotation x) t    -> (\z -> return $ HLam x z) =<< (evaluate' t env) 
                      -- HLam x <$> evaluate' t env
       BConstLam t -> (\z -> return $ HK z) =<< (evaluate' t env)
       BSort sort  -> return $ HSort sort

src/LocallyNamelessSyntax.hs

@@ -1,6 +1,7 @@
+{-# LANGUAGE DeriveFunctor #-}
 -- stuff taken from HerBruijnVal
 
-module LocallyNamelessSyntax (BTm(..), DBIndex(..), toLocallyNameless, fromLocallyNameless) where
+module LocallyNamelessSyntax (BTm(..), DBIndex(..), Annotation(..), toLocallyNameless, fromLocallyNameless) where
 
 import Data.Map (Map)
 import qualified Data.Map as Map
@@ -11,22 +12,33 @@ import Value
 
 -- * de Bruijn Terms
 
+newtype Annotation a = Annotation { annotation :: a }
+  deriving (Show, Functor)
+
+instance Eq (Annotation a) where
+  a == b = True
+
+instance Ord (Annotation a) where
+  a <= b = True
+
 data DBIndex = DBIndex { index :: Int, identifier :: A.Name }
-  deriving (Ord)
 
 instance Eq DBIndex where
   i == j = index i == index j
 
 instance Show DBIndex where
   show (DBIndex i x) = show x ++ "@" ++ show i
 
+instance Ord DBIndex where
+  compare i j = compare (index i) (index j)
+
 data BTm -- names are only used for quoting
   = B DBIndex     -- bound variable: de Bruijn index
   | BVar A.Name   -- free variable: name
   | BCon A.Name
   | BDef A.Name
   | BApp BTm BTm
-  | BLam A.Name BTm  -- name irrelevant for execution
+  | BLam (Annotation A.Name) BTm  -- name irrelevant for execution
   | BConstLam BTm -- these are lambdas, but not counted
   | BSort Value.Sort
   | BPi BTm BTm
@@ -49,11 +61,12 @@ fromLocallyNameless t =
     BDef x -> Ident $ Def x
     BApp t u -> App (fromLocallyNameless t) (fromLocallyNameless u)
     BPi u (BConstLam t) -> Pi Nothing (fromLocallyNameless u) (fromLocallyNameless t)
-    BPi u (BLam x t)    -> Pi (Just x) (fromLocallyNameless u) (fromLocallyNameless t)
+    BPi u (BLam (Annotation x) t)    -> Pi (Just x) (fromLocallyNameless u) (fromLocallyNameless t)
 
-    BLam x t -> Lam x Nothing $ fromLocallyNameless t
+    BLam (Annotation x) t -> Lam x Nothing $ fromLocallyNameless t
+    BConstLam t -> Lam A.noName Nothing $ fromLocallyNameless t
     BSort Type -> Typ
-    -- impossible: BConstLam t, BSort Kind
+    -- impossible:  BSort Kind
 
 -- * transformation, only used for evaluate2
 
@@ -81,7 +94,7 @@ toLocallyNameless = trans lbl_empty where
         Con x -> BCon x
         Def x -> BDef x
   trans lbl (App e1 e2) = BApp (trans lbl e1) (trans lbl e2)
-  trans lbl (Lam name _ e) = BLam name $ trans (insert_lbl name lbl) e
+  trans lbl (Lam name _ e) = BLam (Annotation name) $ trans (insert_lbl name lbl) e
   trans _ Typ = BSort Type
   trans lbl (Pi mname a b) = case mname of
     Just n -> 

src/Makefile

@@ -10,8 +10,8 @@ profflags=-prof -auto-all
 
 default : helf test
 
-current : helf
-	helf test/succeed/comments.elf
+current : 
+	helf test/succeed/z.elf
 
 helf : ../bin/helf
 

src/TGChecker.hs

@@ -3,7 +3,7 @@
 -- * environments as finite maps
 
 {-# LANGUAGE OverlappingInstances, IncoherentInstances, UndecidableInstances,
-    PatternGuards, TupleSections #-}
+    PatternGuards, TupleSections, TypeSynonymInstances, MultiParamTypeClasses #-}
 
 module TGChecker where
 
@@ -103,6 +103,13 @@ instance MonadCheckExpr Head Val Env EvalM CheckExprM where
   typeTrace tr cont  = -- traceM (showM tr) >>
     enterDoc (prettyM tr) cont
 
+{-
+  traceEval m = do
+    v <- m
+    traceM (showTG v) 
+    return v
+-}
+
   lookupGlobal x = symbType . sigLookup' (A.uid x) <$> asks globals
 
 --  lookupGlobal x = ReaderT $ \ sig -> return $ lookupSafe x sig

src/TermGraph.hs

@@ -179,7 +179,8 @@ type TDict a = Map a Term
 type TransM a = StateT (TDict a) ORefM
 type TransT a = StateT (TDict a)
 
-{-
+--  Direct translation from A.Expr
+
 addPredefs :: MonadTG m => TDict A.Expr -> m (TDict A.Expr)
 addPredefs dict = do
   ty <- predefType
@@ -191,19 +192,21 @@ trans ::  (Signature Term sig, MonadReader sig m, MonadTG m) =>
 trans rho e = -- trace ("translating " ++ show e) $ do
   evalStateT (transT e) =<< addPredefs 
                      (Map.mapKeysMonotonic (A.Ident . A.Var) rho)
--}
 
-addPredefs :: MonadTG m => TDict BTm -> m (TDict BTm)
-addPredefs dict = do
-  ty <- predefType
-  return $ Map.insert (BSort Type) ty dict
+{-
+-- Translation via BTm
 
 trans ::  (Signature Term sig, MonadReader sig m, MonadTG m) => 
   Env -> A.Expr -> m Term
 trans rho e = -- trace ("translating " ++ show e) $ do
   evalStateT (transB (toLocallyNameless e)) =<< addPredefs 
                      (Map.mapKeysMonotonic BVar rho)
 
+addPredefs :: MonadTG m => TDict BTm -> m (TDict BTm)
+addPredefs dict = do
+  ty <- predefType
+  return $ Map.insert (BSort Type) ty dict
+-}
 
 -- | From locally nameless to Term.
 transB ::  (Signature Term sig, MonadReader sig m, MonadTG m) => 
@@ -222,14 +225,18 @@ transB' e = do
             SigDef t v <- sigLookup' (A.uid x) <$> ask
             Right <$> (return $ def x t v) 
          BVar n -> -- free variable
---           fail ("transB': unbound variable " ++ A.suggestion n) 
+           fail ("transB': unbound variable " ++ A.suggestion n) 
 --           trace ("transB': unbound variable " ++ A.suggestion n) 
-           Right <$> (return $ Var n) -- only for binding in Lam and Pi
-         BLam n e    -> do
+--           Right <$> (return $ Var n) -- only for binding in Lam and Pi
+         BLam (Annotation n) e    -> do
            x <- transAddBind BVar n 
            Right . Abs x <$> transB e
          BConstLam e -> Right . K <$> transB e
-         BPi a b     -> Right <$> (Fun <$> transB a <*> transB b)
+         BPi a b     -> do
+           a <- transB a
+           b <- transB b
+           return $ Right $ Fun a b
+--         BPi a b     -> Right <$> (Fun <$> transB a <*> transB b)
    else do
     r <- transB f
     Right . App r <$> (mapM transB sp)
@@ -240,19 +247,20 @@ transG ::  (Signature Term sig, MonadReader sig m, MonadTG m, Ord a, Show a) =>
   (a -> TransT a m (Either Term Term')) -> a -> TransT a m Term
 transG transT' e = do
   dict <- get
+  -- traceM $ return ("? searching translation  for " ++ show e  ++ " in dict " ++ show dict)
   case Map.lookup e dict of  -- TODO compare upto alpha!
     Just r  -> do
       unlessM (atomic r) $ do
-        traceM $ return ("==> found translation for " ++ show e)
+        traceM $ return ("==> found translation " ++ show r ++ " for " ++ show e) --  ++ " in dict " ++ show (Map.keys dict))
       return r
     Nothing -> do
       rt <- transT' e
       case rt of
         Left  r -> return r
         Right t -> do
           r <- newORef t
-          -- traceM $ return ("adding translation for " ++ show e) 
-          put $ Map.insert e r dict
+          -- traceM $ return ("==> adding translation " ++ show r ++ " for " ++ show e) 
+          modify $ Map.insert e r
           return r
 
 transAddBind :: (Signature Term sig, MonadReader sig m, MonadTG m, Ord a) => 
@@ -389,7 +397,7 @@ prettyT r = do
     Nothing -> do
       d <- prettyT' =<< readORef r
       put $ Map.insert r d dict
-      return $ d -- text (show r ++ "@") <> d
+      return $ text (show r ++ "@") <> d
 
 prettyT' :: MonadORef m => Term' -> PrettyT m Doc
 prettyT' t = do
@@ -461,8 +469,10 @@ substT r = do
         traceM $ return ("==> fire subst of " ++ s' ++ " for " ++ s)
       return $ Just r'
     Just (Nothing) -> do
+{-
       x <- showTG r
-      -- traceM $ return ("skipping bound variable " ++ x ++ " with ref " ++ show r)
+      traceM $ return ("skipping bound variable " ++ x ++ " with ref " ++ show r)
+-}
       return Nothing
     Nothing  -> do
       mt <- substT' =<< readORef r

src/TypeCheck.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE TupleSections, UndecidableInstances, TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses, GeneralizedNewtypeDeriving, FlexibleContexts, FunctionalDependencies #-}
+
 -- A generic bidirectional type-checker for LF
 
 module TypeCheck where
@@ -100,6 +102,9 @@ class (Monad m, -- Scoping.Scope m,
   newError     :: TypeError val -> m a -> m a
   -- handleError  :: m a -> (TypeError val -> m a) -> m a
   typeTrace    :: TypeTrace val -> m a -> m a
+  typeTrace tr cont = cont   -- default: do not trace type checker
+  traceEval    :: m val -> m val
+  traceEval cont = cont      -- default: do not print evaluated term
 
 {-  Type checking   Gamma |- e <=: t
 
@@ -263,7 +268,7 @@ class (Monad m, -- Scoping.Scope m,
   {-# INLINE doCheckExpr #-}
 
   evalExpr    :: Expr -> m val
-  evalExpr     = doCheckExpr . doEval . evaluate' 
+  evalExpr     = doCheckExpr . traceEval . doEval . evaluate' 
 
 {- Rules for checking declarations