3863 llvm term cache (#3882)

This PR introduces a cache for the terms returned from calls to
`Booster.LLVM.Internal.API.simplify`. Unpacking now uses a term store
for the unpacked terms, and recognises shared terms by a shallow index
into this store, using `TermF Int` as the map key (where the `Int` are
indexes of symbol application/injection arguments in the term store).

In small targeted tests using requests from MX-backend proofs , memory
consumption was noticeably reduced, also resulting in better
performance.

Currently, the cache only lives for the duration of one LLVM call (not
across different calls), no global variables or unsafe IO is required.

Fixes #3863

Author: jberthold

booster/library/Booster/LLVM/Internal.hs

@@ -51,7 +51,7 @@ import System.Posix.DynamicLinker qualified as Linker
 
 import Booster.LLVM.TH (dynamicBindings)
 import Booster.Pattern.Base
-import Booster.Pattern.Binary hiding (Block)
+import Booster.Pattern.Binary
 import Booster.Pattern.Util (sortOfTerm)
 import Booster.Trace
 import Booster.Trace qualified as Trace

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -501,12 +501,9 @@ llvmSimplify term = do
                                 withTermContext result $
                                     emitEquationTrace t Nothing (Just "LLVM") Nothing $
                                         Success result
-                        toCache LLVM t result
                         pure result
-        | otherwise = do
-            result <- cb t
-            toCache LLVM t result
-            pure result
+        | otherwise =
+            cb t
 
 ----------------------------------------
 -- Interface functions