From 88fbbd327a789baa6eaf48be8f09a2ab3ceb9169 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 26 May 2021 12:42:55 -0700
Subject: [PATCH 1/2] Defer `CallStack` computations by representing them as
 data constructors.

This avoids expensive calls to `combineCallStacks` in the common case;
the actual call stack values are only computed in the case where they
need to be printed out.
---
 src/Cryptol/Backend/Monad.hs | 45 ++++++++++++++++++++++++++++++------
 1 file changed, 38 insertions(+), 7 deletions(-)

diff --git a/src/Cryptol/Backend/Monad.hs b/src/Cryptol/Backend/Monad.hs
index 6665aaf45..ffbed712f 100644
--- a/src/Cryptol/Backend/Monad.hs
+++ b/src/Cryptol/Backend/Monad.hs
@@ -63,12 +63,33 @@ ready a = Ready a
 
 -- | The type of dynamic call stacks for the interpreter.
 --   New frames are pushed onto the right side of the sequence.
-type CallStack = Seq (Name, Range)
+data CallStack
+  = EmptyCallStack
+  | CombineCallStacks !CallStack !CallStack
+  | PushCallFrame !Name !Range !CallStack
+
+instance Semigroup CallStack where
+  (<>) = CombineCallStacks
+
+instance Monoid CallStack where
+  mempty = EmptyCallStack
+
+type CallStack' = Seq (Name, Range)
+
+evalCallStack :: CallStack -> CallStack'
+evalCallStack stk =
+  case stk of
+    EmptyCallStack -> mempty
+    CombineCallStacks appstk fnstk -> combineCallStacks' (evalCallStack appstk) (evalCallStack fnstk)
+    PushCallFrame n r stk1 -> pushCallFrame' n r (evalCallStack stk1)
 
 -- | Pretty print a call stack with each call frame on a separate
 --   line, with most recent call frames at the top.
 displayCallStack :: CallStack -> Doc
-displayCallStack = vcat . map f . toList . Seq.reverse
+displayCallStack = displayCallStack' . evalCallStack
+
+displayCallStack' :: CallStack' -> Doc
+displayCallStack' = vcat . map f . toList . Seq.reverse
   where
   f (nm,rng)
     | rng == emptyRange = pp nm
@@ -92,7 +113,13 @@ combineCallStacks ::
   CallStack {- ^ call stack of the application context -} ->
   CallStack {- ^ call stack of the function being applied -} ->
   CallStack
-combineCallStacks appstk fnstk = appstk <> dropCommonPrefix appstk fnstk
+combineCallStacks appstk fnstk = CombineCallStacks appstk fnstk
+
+combineCallStacks' ::
+  CallStack' {- ^ call stack of the application context -} ->
+  CallStack' {- ^ call stack of the function being applied -} ->
+  CallStack'
+combineCallStacks' appstk fnstk = appstk <> dropCommonPrefix appstk fnstk
   where
   dropCommonPrefix _  Seq.Empty = Seq.Empty
   dropCommonPrefix Seq.Empty fs = fs
@@ -102,9 +129,12 @@ combineCallStacks appstk fnstk = appstk <> dropCommonPrefix appstk fnstk
 
 -- | Add a call frame to the top of a call stack
 pushCallFrame :: Name -> Range -> CallStack -> CallStack
-pushCallFrame nm rng stk@( _ Seq.:|> (nm',rng'))
+pushCallFrame nm rng stk = PushCallFrame nm rng stk
+
+pushCallFrame' :: Name -> Range -> CallStack' -> CallStack'
+pushCallFrame' nm rng stk@( _ Seq.:|> (nm',rng'))
   | nm == nm', rng == rng' = stk
-pushCallFrame nm rng stk = stk Seq.:|> (nm,rng)
+pushCallFrame' nm rng stk = stk Seq.:|> (nm,rng)
 
 
 -- | The monad for Cryptol evaluation.
@@ -417,11 +447,12 @@ data EvalErrorEx =
  deriving Typeable
 
 instance PP EvalErrorEx where
-  ppPrec _ (EvalErrorEx stk ex) = vcat ([ pp ex ] ++ callStk)
+  ppPrec _ (EvalErrorEx stk0 ex) = vcat ([ pp ex ] ++ callStk)
 
    where
+    stk = evalCallStack stk0
     callStk | Seq.null stk = []
-            | otherwise = [ text "-- Backtrace --", displayCallStack stk ]
+            | otherwise = [ text "-- Backtrace --", displayCallStack' stk ]
 
 instance Show EvalErrorEx where
   show = show . pp

From cbfc6c771c17c5edb31db142f3f6159559aed26a Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 26 May 2021 16:03:18 -0700
Subject: [PATCH 2/2] Add special cases to `combineCallStacks`.

---
 src/Cryptol/Backend/Monad.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Cryptol/Backend/Monad.hs b/src/Cryptol/Backend/Monad.hs
index ffbed712f..b821fb035 100644
--- a/src/Cryptol/Backend/Monad.hs
+++ b/src/Cryptol/Backend/Monad.hs
@@ -113,6 +113,8 @@ combineCallStacks ::
   CallStack {- ^ call stack of the application context -} ->
   CallStack {- ^ call stack of the function being applied -} ->
   CallStack
+combineCallStacks appstk EmptyCallStack = appstk
+combineCallStacks EmptyCallStack fnstk = fnstk
 combineCallStacks appstk fnstk = CombineCallStacks appstk fnstk
 
 combineCallStacks' ::