Tighen up alias map and add full support for looping constructs.

These are a bit tricky to get right, as different iterations can
possibly introduce new dependencies. For example, a set of operators
could be cloning themselves into positions in a tuple.

For efficiency purposes, most loops should not have to run more
than once, otherwise we might hit exponential runtimes.

To make this work, the alias graph has been refined to respect
scoping; when a binding falls out of scope it is omitted from the
graph, and its dependencies are stitched back together.

This means what when we reach a ForEachFacts block, at the start
the accumulators won't alias each other, and, usually at the end
they won't either; so the first pass is used. Care must be taken
to make sure these graphs are actually the same.

It a dependent alias is found, that's fine, we rerun the initial
set of statements with a merged alias map, until we reach a fixpoint.

icicle-compiler/src/Icicle/Avalanche/Statement/Simp/Linear.hs

@@ -21,6 +21,7 @@ import              Icicle.Avalanche.Statement.Statement
 import              Icicle.Common.Base (Name)
 import              Icicle.Common.Exp
 import              Icicle.Common.Type (ValType (..))
+import              Icicle.Internal.Pretty
 
 import              P hiding (empty)
 
@@ -85,46 +86,42 @@ linearise s =
       -- If it's an array, we say that it aliases the one it points to in the future.
       Read nx na t@(ArrayT {}) ss -> do
         modifyBackwardsUsedRemoveBind nx na
-        -- Modify forwards before entering the block
-        modifyForwards $
-          overwrite nx na
+        Read nx na t <$>
+          scopedGo nx na ss
 
-        Read nx na t <$> go ss
 
       --
       -- It it's not an array, we don't mind and don't declare the alias.
       Read nx na t ss -> do
         modifyBackwardsUsedRemoveBind nx na
-        Read nx na t <$> go ss
+        Read nx na t <$>
+          scopedGo' nx ss
 
       --
       -- Let bindings are a lot like reads, if it looks like a reference, then add
       -- the alias.
       Let nm x ss | Just ref <- arrayReference x -> do
         modifyBackwardsUsedRemoveBind' nm x
-        -- Modify forwards before entering the block
-        modifyForwards $
-          overwrite nm ref
-
-        Let nm x <$> go ss
+        Let nm x <$>
+          scopedGo nm ref ss
 
       Let nm x ss -> do
         modifyBackwardsUsedRemoveBind' nm x
-        Let nm x <$> go ss
+        Let nm x <$>
+          scopedGo' nm ss
 
       --
       -- Initialisation is similar again to lets and reads.
       InitAccumulator acc@(Accumulator nm (ArrayT {}) x) ss | Just ref <- arrayReference x -> do
         modifyBackwardsUsedRemoveBind' nm x
-        -- Modify forwards before entering the block
-        modifyForwards $
-          overwrite nm ref
+        InitAccumulator acc <$>
+          scopedGo nm ref ss
 
-        InitAccumulator acc <$> go ss
 
       InitAccumulator acc@(Accumulator nm _ x) ss -> do
         modifyBackwardsUsedRemoveBind' nm x
-        InitAccumulator acc <$> go ss
+        InitAccumulator acc <$>
+          scopedGo' nm ss
 
       --
       -- Here's the key judgement and rewrite.
@@ -138,16 +135,17 @@ linearise s =
         aliased <- getPast
         used    <- getFuture
 
-        -- Do we need to add a new alias for this? If there are no
-        -- further references then we don't delete the copy, then
-        -- there technically should be an alias, but, on the other
-        -- hand, it doesn't matter, because there are no aliases which
-        -- refer to anything before this address or this address so no
-        -- path can be formed; on the other hand, if we do keep the
-        -- copy, then there's no alias required, because it's a fresh
-        -- memory location. Either way, we need to make the same
-        -- decision, because if we change the sent signals here based
-        -- on them, we won't be able to fix the Tardis.
+        --
+        -- Do we need to add a new alias for this?
+        -- Sequentially, it shouldn't matter to not include this, but
+        -- for loops it's important, as we need to check what aliases
+        -- are possible in future iterations.
+        -- We can't put this in the if condition, because if we change
+        -- the subsequent calculations depending on usage from the
+        -- future, we won't fix the Tardis.
+
+        modifyForwards $
+          overwrite n ref
 
         pure $
           if hasNoFurtherReferences n ref aliased used then do
@@ -156,13 +154,13 @@ linearise s =
             Write n x
 
       --
-      -- Otherwise, if the write is a reference, then we need
+      -- If the write is a reference, then we need
       -- to know that this memory location points to the old
       -- one in subsequent items in a block.
       Write n x | Just ref <- arrayReference x -> do
         modifyBackwardsUsed' x
         modifyForwards $
-          insert n ref
+          overwrite n ref
 
         pure $ Write n x
 
@@ -176,17 +174,23 @@ linearise s =
       Block xs ->
         Block <$> traverse go xs
 
+      --
+      -- Looping constructs.
+      -- Run until a fixpoint is reached.
       While a w vt x ss -> do
         modifyBackwardsUsed' x
-        While a w vt x <$> go ss
+        While a w vt x <$>
+          fixGo ss
 
       ForeachInts t n from to ss -> do
         modifyBackwardsUsed' from
         modifyBackwardsUsed' to
-        ForeachInts t n from to <$> go ss
+        ForeachInts t n from to <$>
+          fixGo ss
 
       ForeachFacts binds vt ss -> do
-        ForeachFacts binds vt <$> go ss
+        ForeachFacts binds vt <$>
+          fixGo ss
 
       x@(Output _ _ xts) -> do
         for_ xts $
@@ -213,6 +217,48 @@ linearise s =
       modifyBackwardsUsed' =
         modifyBackwardsUsed . freevars
 
+      --
+      -- This introduces the alias for name to ref, then when it goes
+      -- out of scope, deletes this name and remakes transient aliases
+      -- as direct ones.
+      scopedGo nm ref ss = do
+        modifyForwards (overwrite nm ref)
+        sS <- go ss
+        modifyForwards (delete nm)
+        pure sS
+
+      --
+      -- This doesn't actually introduce an alias into the map,
+      -- but if this is something like array_create, then we want
+      -- to remove the reference after it goes out of scope, so that
+      -- the new value stands alone.
+      scopedGo' nm ss = do
+        sS <- go ss
+        modifyForwards (delete nm)
+        pure sS
+
+      --
+      -- Loops are a bit tricky.
+      -- It's possible to write queries where after a pass is complete
+      -- accumulators depend on other accumulators initialised before
+      -- the loop began; so we need to reach a fixpoint on both the
+      -- initial alias map and the returned alias map.
+      --
+      -- If the maps don't match, rerun with the merged alias map on
+      -- the original statements. We need to use the original ones
+      -- because the pass might have deleted some copy operations which
+      -- are actually required given the new information.
+      fixGo ss = do
+        before <- getPast
+        sS     <- go ss
+        after  <- getPast
+        let merged = merge before after
+        if before == merged then
+          pure sS
+        else do
+          sendFuture merged
+          fixGo ss
+
 
 hasNoFurtherReferences :: Ord a => a -> a -> Graph a -> Set.Set a -> Bool
 hasNoFurtherReferences acc nx aliased used =
@@ -222,6 +268,7 @@ hasNoFurtherReferences acc nx aliased used =
 
     thoseAliases =
       search (Set.toList (Set.delete acc used)) aliased
+
   in
     Set.disjoint
       theseAliases
@@ -259,20 +306,43 @@ newtype Graph n =
   Graph (Map.Map n (Set.Set n))
  deriving (Eq, Ord, Show)
 
+instance Pretty n => Pretty (Graph n) where
+  pretty (Graph g) =
+    vsep (pretty <$> (Map.toList (Map.map Set.toList g)))
+
 empty :: Graph n
 empty =
   Graph Map.empty
 
-insert :: Ord n => n -> n -> Graph n -> Graph n
-insert from to (Graph g) =
-  Graph $
-    Map.alter (Just . maybe (Set.singleton to) (Set.insert to)) from g
-
 overwrite :: Ord n => n -> n -> Graph n -> Graph n
 overwrite from to (Graph g) =
   Graph $
     Map.insert from (Set.singleton to) g
 
+delete :: Ord n => n -> Graph n -> Graph n
+delete from (Graph g) =
+  let
+    transient =
+      fromMaybe Set.empty $
+        Map.lookup from g
+
+    addIfPoint k xs =
+      Set.delete k $ Set.delete from $
+        if Set.member from xs then
+          Set.union transient xs
+        else
+          xs
+
+    addIfPointOrNone k xs = do
+      found <- Just $ addIfPoint k xs
+      guard (not (Set.null found))
+      return found
+
+  in
+  Graph $
+    Map.mapMaybeWithKey addIfPointOrNone $
+      Map.delete from g
+
 match :: Ord n => n -> Graph n -> (Set.Set n, Graph n)
 match n (Graph g) =
   case Map.lookup n g of

icicle-compiler/test/Icicle/Test/Avalanche/Simp/Linear.hs

@@ -19,6 +19,7 @@ import           System.IO
 import           Icicle.Common.Base
 import           Icicle.Common.Exp
 import           Icicle.Common.Fresh
+import           Icicle.Internal.Pretty
 import           Icicle.Avalanche.Statement.Statement
 import qualified Icicle.Avalanche.Prim.Flat as Flat
 import qualified Icicle.Avalanche.Prim.Compounds as Flat
@@ -169,6 +170,38 @@ write_ref_out_of_scope_let_copy a_fresh = do
   Flat.FlatOps  {..} = Flat.flatOps a_fresh
   Flat.FlatCons {..} = Flat.flatCons a_fresh
 
+--
+-- On the first pass, it wouldn't need a copy; but we
+-- need one afterwards because acc1 and acc2 point to
+-- the same reference.
+write_loop :: a -> Fresh Var (Statement a Var Flat.Prim)
+write_loop a_fresh = do
+  fact   <- freshPrefix "facts"
+  acc1   <- freshPrefix "test_arr"
+  acc2   <- freshPrefix "test_arr"
+  acc3   <- freshPrefix "test_arr"
+  loc1   <- freshPrefix "loc"
+  loc2   <- freshPrefix "loc"
+  loc3   <- freshPrefix "loc"
+
+  return
+    $ initArr IntT acc1 (XValue a_fresh (ArrayT IntT) (VArray [VInt 1]))
+    $ initArr IntT acc2 (XValue a_fresh (ArrayT IntT) (VArray [VInt 2]))
+    $ initArr IntT acc3 (XValue a_fresh (ArrayT IntT) (VArray [VInt 3]))
+    $ ForeachFacts (FactBinds fact []) UnitT
+    $ readArr IntT loc1 acc1
+    $ readArr IntT loc2 acc2
+    $ readArr IntT loc3 acc3
+    $ Block [
+        Write acc3 (arrCpy IntT (xVar loc1))
+      , Write acc2 (arrCpy IntT (xVar loc2))
+      , Write acc1 (arrCpy IntT (xVar loc2))
+    ]
+
+ where
+  Flat.FlatOps  {..} = Flat.flatOps a_fresh
+  Flat.FlatCons {..} = Flat.flatCons a_fresh
+
 
 countCopies :: TransformX x => x () n Flat.Prim -> Integer
 countCopies a =
@@ -182,35 +215,40 @@ isCopy e =
     XPrim () (Flat.PrimArray (Flat.PrimArrayCopy _)) -> Const (Sum 1)
     _ -> plate isCopy e
 
+mkProp :: Integer -> (() -> Fresh Var (Statement () Var Flat.Prim)) -> Property
+mkProp expect prog
+ = withTests 1 . property $ do
+    let built  = testFresh "a" $ prog ()
+    let linear = linearise built
+    Hedgehog.annotate (show $ pretty built)
+    Hedgehog.annotate (show $ pretty linear)
+    ((=== expect) . countCopies)
+      linear
+
+
 prop_elides_copy :: Property
 prop_elides_copy
- = withTests 1 . property $ do
-     ((=== 0) . countCopies) $
-       linearise (testFresh "a" $ simple_copy_elide ())
+ = mkProp 0 simple_copy_elide
 
 prop_keeps_copy :: Property
 prop_keeps_copy
- = withTests 1 . property $ do
-     ((=== 1) . countCopies) $
-       linearise (testFresh "a" $ simple_copy_retain ())
+ = mkProp 1 simple_copy_retain
 
 prop_write_ref_copy :: Property
 prop_write_ref_copy
- = withTests 1 . property $ do
-     ((=== 1) . countCopies) $
-       linearise (testFresh "a" $ write_ref_copy ())
+ = mkProp 1 write_ref_copy
 
 prop_write_ref_in_if_copy :: Property
 prop_write_ref_in_if_copy
- = withTests 1 . property $ do
-     ((=== 2) . countCopies) $
-       linearise (testFresh "a" $ write_ref_in_if_copy ())
+ = mkProp 2 write_ref_in_if_copy
 
 prop_write_ref_out_of_scope_let_copy :: Property
 prop_write_ref_out_of_scope_let_copy
- = withTests 1 . property $ do
-     ((=== 1) . countCopies) $
-       linearise (testFresh "a" $ write_ref_out_of_scope_let_copy ())
+ = mkProp 2 write_ref_out_of_scope_let_copy
+
+prop_fact_loop :: Property
+prop_fact_loop
+ = mkProp 1 write_loop
 
 tests :: IO Bool
 tests =

icicle-compiler/test/test.hs

@@ -15,6 +15,7 @@ import qualified Icicle.Test.Core.Program.Condense
 
 import qualified Icicle.Test.Avalanche.EvalCommutes
 import qualified Icicle.Test.Avalanche.CheckCommutes
+import qualified Icicle.Test.Avalanche.Simp.Linear
 import qualified Icicle.Test.Avalanche.SimpCommutes
 import qualified Icicle.Test.Avalanche.Flatten
 import qualified Icicle.Test.Avalanche.Melt
@@ -96,6 +97,7 @@ avalanche =
     , Icicle.Test.Avalanche.Melt.tests
     , Icicle.Test.Avalanche.MeltPrim.tests
     , Icicle.Test.Avalanche.SimpCommutes.tests
+    , Icicle.Test.Avalanche.Simp.Linear.tests
     ]
 
 core :: TestSuite

icicle-source/src/Icicle/Source/Checker/Constraint.hs

@@ -171,13 +171,13 @@ constraintsQ env q
 
   -- Perform top-level discharge of any silly leftover Possibility or Temporality joins
   top = do
-   (q',_,cons) <- generateQ q env
+   (q',s,cons) <- generateQ q env
    case dischargeCS' dischargeC'toplevel cons of
     Left errs
      -> genHoistEither
       $ errorNoSuggestions (ErrorConstraintsNotSatisfied (annotOfQuery q) errs)
     Right (sub', cons')
-     -> let q'' = substTQ sub' q'
+     -> let q'' = substTQ (compose s sub') q'
         in  return (q'', cons')