[ treeless ] replace n+k patterns by guards

src/full/Agda/Compiler/MAlonzo/Compiler.hs

@@ -443,30 +443,25 @@ compilePrim s =
     T.PMod -> fakeExp "(Prelude.mod :: Integer -> Integer -> Integer)"
     T.PSub -> fakeExp "((Prelude.-) :: Integer -> Integer -> Integer)"
     T.PAdd -> fakeExp "((Prelude.+) :: Integer -> Integer -> Integer)"
+    T.PGeq -> fakeExp "((Prelude.>=) :: Integer -> Integer -> Bool)"
     -- primitives only used by NPlusKToPrims transformation, which MAlonzo doesn't use
-    T.PGeq -> __IMPOSSIBLE__
     T.PIf  -> __IMPOSSIBLE__
 
 alt :: T.TAlt -> CC HS.Alt
 alt a = do
   case a of
-    (T.TACon {}) -> do
+    T.TACon {} -> do
       intros (T.aArity a) $ \xs -> do
         hConNm <- lift $ conhqn $ T.aCon a
         mkAlt (HS.PApp hConNm $ map HS.PVar xs)
-    (T.TAPlus { T.aSucs = k, T.aBody = b }) ->
-        -- Turn  n + k -> b
-        -- into  n' | n' >= k -> let n = n' - k in b
-      freshNames 1 $ \[n'] ->
-      intros     1 $ \[n] -> do
-        b <- term b
-        let qn' = HS.Var (HS.UnQual n')
-            ik  = hsTypedInt k
-            g = [HS.Qualifier $ hsPrimOpApp ">=" qn' ik]
-            body = hsLet n (hsPrimOpApp "-" qn' ik) b
-        return $ HS.Alt dummy (HS.PVar n') (HS.GuardedRhss [HS.GuardedRhs dummy g body]) (HS.BDecls [])
-    (T.TALit { T.aLit = (LitQName _ q) }) -> mkAlt (litqnamepat q)
-    (T.TALit {}) -> mkAlt (HS.PLit HS.Signless $ hslit $ T.aLit a)
+    T.TAGuard g b -> do
+      g <- term g
+      b <- term b
+      return $ HS.Alt dummy HS.PWildCard
+                      (HS.GuardedRhss [HS.GuardedRhs dummy [HS.Qualifier g] b])
+                      (HS.BDecls [])
+    T.TALit { T.aLit = (LitQName _ q) } -> mkAlt (litqnamepat q)
+    T.TALit {} -> mkAlt (HS.PLit HS.Signless $ hslit $ T.aLit a)
   where
     mkAlt :: HS.Pat -> CC HS.Alt
     mkAlt pat = do

src/full/Agda/Compiler/Treeless/Erase.hs

@@ -88,7 +88,7 @@ eraseTerms = runE . erase
     eraseAlt a = case a of
       TALit l b   -> TALit l   <$> erase b
       TACon c a b -> TACon c a <$> erase b
-      TAPlus k b  -> TAPlus k  <$> erase b
+      TAGuard g b -> TAGuard   <$> erase g <*> erase b
 
 data TypeInfo = Empty | Erasable | NotErasable
   deriving (Eq, Show)

src/full/Agda/Compiler/Treeless/NPlusK.hs

@@ -66,19 +66,26 @@ transform isZero isSuc = tr
             TACon c 1 b | isSuc c  ->
               case tr b of
                 -- Collapse nested n+k patterns
-                TCase 0 _ d bs' -> map sucBranch bs' ++ [TAPlus 1 d]
-                b -> [TAPlus 1 b]
+                TCase 0 _ d bs' -> map sucBranch bs' ++ [nPlusKAlt 1 d]
+                b -> [nPlusKAlt 1 b]
               where
                 sucBranch (TALit (LitNat r i) b) = TALit (LitNat r (i + 1)) $ applySubst (str __IMPOSSIBLE__) b
-                sucBranch (TAPlus k b) = TAPlus (k + 1) $ applySubst (liftS 1 $ str __IMPOSSIBLE__) b
-                sucBranch TACon{} = __IMPOSSIBLE__
-                sucBranch TALit{} = __IMPOSSIBLE__
+                sucBranch alt | Just (k, b) <- nPlusKView alt = nPlusKAlt (k + 1) $ applySubst (liftS 1 $ str __IMPOSSIBLE__) b
+                sucBranch _ = __IMPOSSIBLE__
+
+                nPlusKAlt k b = TAGuard (tOp PGeq (TVar e) (tInt k)) $
+                                TLet (tOp PSub (TVar e) (tInt k)) b
+
+                nPlusKView (TAGuard (TApp (TPrim PGeq) [TVar 0, (TLit (LitNat _ k))])
+                                    (TLet (TApp (TPrim PSub) [TVar 0, (TLit (LitNat _ j))]) b))
+                  | k == j = Just (k, b)
+                nPlusKView _ = Nothing
 
                 str err = compactS err [Nothing]
 
             TACon c a b -> [TACon c a (tr b)]
             TALit{}     -> [b]
-            TAPlus{}    -> __IMPOSSIBLE__
+            TAGuard{}   -> __IMPOSSIBLE__
 
       TVar{}    -> t
       TDef{}    -> t

src/full/Agda/Compiler/Treeless/NPlusKToPrims.hs

@@ -32,17 +32,13 @@ convertNPlusK = tr
           (plusAlts, otherAlts) = splitAlts alts
 
           guardedAlt :: TAlt -> TTerm -> TTerm
-          guardedAlt (TAPlus{aSucs = k, aBody = body}) cont =
-            TApp (TPrim PIf)
-              [ tOp PGeq (TVar sc) (tInt k)
-              , TLet (tOp PSub (TVar sc) (tInt k)) (tr body)
-              , cont
-              ]
+          guardedAlt (TAGuard g body) cont =
+            TApp (TPrim PIf) [tr g, tr body, cont]
           guardedAlt _ _ = __IMPOSSIBLE__
 
           def' = foldr guardedAlt (tr def) plusAlts
 
-          trAlt (TAPlus{}) = __IMPOSSIBLE__
+          trAlt (TAGuard{}) = __IMPOSSIBLE__
           trAlt a = a { aBody = tr (aBody a) }
 
       TVar{}    -> t
@@ -59,8 +55,8 @@ convertNPlusK = tr
       TApp a bs               -> TApp (tr a) (map tr bs)
       TLet e b                -> TLet (tr e) (tr b)
 
--- | Split alts into TAPlus alts and other alts.
+-- | Split alts into TAGuard alts and other alts.
 splitAlts :: [TAlt] -> ([TAlt], [TAlt])
-splitAlts = partition isPlusAlt
-  where isPlusAlt (TAPlus _ _) = True
-        isPlusAlt _ = False
+splitAlts = partition isGuardAlt
+  where isGuardAlt (TAGuard _ _) = True
+        isGuardAlt _ = False

src/full/Agda/Compiler/Treeless/Pretty.hs

@@ -126,10 +126,9 @@ pTerm t = case t of
       <*> pTerm' 0 def
     where
       pAlt (TALit l b) = pAlt' <$> pTerm' 0 (TLit l) <*> pTerm' 0 b
-      pAlt (TAPlus k b) =
-        withName $ \ x -> bindName x $
-        pAlt' <$> pTerm' 0 (tOp PAdd (TVar 0) (tInt k))
-              <*> pTerm' 0 b
+      pAlt (TAGuard g b) =
+        pAlt' <$> ((text "_" <+> text "|" <+>) <$> pTerm' 0 g)
+              <*> (pTerm' 0 b)
       pAlt (TACon c a b) =
         withNames a $ \ xs -> bindNames xs $
         pAlt' <$> pTerm' 0 (TApp (TCon c) [TVar i | i <- reverse [0..a - 1]])

src/full/Agda/Compiler/Treeless/Simplify.hs

@@ -87,18 +87,15 @@ simplify FunctionKit{..} = simpl
 
     simplAlt (TACon c a b) = TACon c a <$> underLams a (simpl b)
     simplAlt (TALit l b)   = TALit l   <$> simpl b
-    simplAlt (TAPlus k b)  = TAPlus k  <$> underLam (simpl b)
+    simplAlt (TAGuard g b) = TAGuard   <$> simpl g <*> simpl b
 
     tCase :: Int -> CaseType -> TTerm -> [TAlt] -> S TTerm
     tCase x t d bs
       | isUnreachable d =
         case reverse bs' of
           [] -> pure d
           TALit _ b   : as  -> pure $ tCase' x t b (reverse as)
-          TAPlus k b  : as  -> do
-                 -- TODO: retraversing the body (quadratic in nesting level!)
-            b <- simpl (TLet (tOp PSub (TVar x) (tInt k)) b)
-            pure $ tCase' x t b (reverse as)
+          TAGuard _ b : as  -> pure $ tCase' x t b (reverse as)
           TACon c a b : _   -> pure $ tCase' x t d bs'
       | otherwise = pure $ TCase x t d bs'
       where

src/full/Agda/Compiler/Treeless/Subst.hs

@@ -36,4 +36,4 @@ instance Subst TTerm TTerm where
 instance Subst TTerm TAlt where
   applySubst rho (TACon c i b)  = TACon c i (applySubst (liftS i rho) b)
   applySubst rho (TALit l b)  = TALit l (applySubst rho b)
-  applySubst rho (TAPlus k b) = TAPlus k (applySubst (liftS 1 rho) b)
+  applySubst rho (TAGuard g b) = TAGuard (applySubst rho g) (applySubst rho b)

src/full/Agda/Syntax/Treeless.hs

@@ -102,8 +102,8 @@ data TAlt
   -- ^ Matches on the given constructor. If the match succeeds,
   -- the pattern variables are prepended to the current environment
   -- (pushes all existing variables aArity steps further away)
-  | TAPlus   { aSucs :: Integer, aBody :: TTerm }
-  -- ^ n+k pattern
+  | TAGuard  { aGuard :: TTerm, aBody :: TTerm }
+  -- ^ Binds no variables
   | TALit    { aLit :: Literal,   aBody:: TTerm }
   deriving (Typeable, Show, Eq, Ord)
 
@@ -124,5 +124,6 @@ instance Unreachable TAlt where
   isUnreachable = isUnreachable . aBody
 
 instance Unreachable TTerm where
-  isUnreachable (TError (TUnreachable{})) = True
+  isUnreachable (TError TUnreachable{}) = True
+  isUnreachable (TLet _ b) = isUnreachable b
   isUnreachable _ = False