Call stacks

cryptol-remote-api/src/CryptolServer/Data/Expression.hs

@@ -318,6 +318,7 @@ readBack :: PrimMap -> TC.Type -> Value -> Eval Expression
 readBack prims ty val =
   let tbl = primTable theEvalOpts in
   let ?evalPrim = \i -> Right <$> Map.lookup i tbl in
+  let ?range = emptyRange in -- TODO?
   case TC.tNoUser ty of
     TC.TRec tfs ->
       Record . HM.fromList <$>
@@ -369,7 +370,7 @@ readBack prims ty val =
 
 
 observe :: Eval a -> Method ServerState a
-observe e = liftIO (runEval e)
+observe e = liftIO (runEval mempty e)
 
 mkEApp :: Expr PName -> [Expr PName] -> Expr PName
 mkEApp f args = foldl EApp f args

cryptol.cabal

@@ -171,6 +171,7 @@ library
                        Cryptol.Eval.Concrete,
                        Cryptol.Eval.Env,
                        Cryptol.Eval.Generic,
+                       Cryptol.Eval.Prims,
                        Cryptol.Eval.Reference,
                        Cryptol.Eval.SBV,
                        Cryptol.Eval.Type,

cryptol/REPL/Haskeline.hs

@@ -48,38 +48,38 @@ import           Prelude.Compat
 crySession :: Maybe FilePath -> Bool -> REPL CommandExitCode
 crySession mbBatch stopOnError =
   do settings <- io (setHistoryFile (replSettings isBatch))
-     let act = runInputTBehavior behavior settings (withInterrupt loop)
+     let act = runInputTBehavior behavior settings (withInterrupt (loop 1))
      if isBatch then asBatch act else act
   where
   (isBatch,behavior) = case mbBatch of
     Nothing   -> (False,defaultBehavior)
     Just path -> (True,useFile path)
 
-  loop :: InputT REPL CommandExitCode
-  loop =
+  loop :: Int -> InputT REPL CommandExitCode
+  loop lineNum =
     do ln <- getInputLines =<< MTL.lift getPrompt
        case ln of
          NoMoreLines -> return CommandOk
          Interrupted
            | isBatch && stopOnError -> return CommandError
-           | otherwise -> loop
-         NextLine line
-           | all isSpace line -> loop
-           | otherwise        -> doCommand line
-
-  doCommand txt =
-    case parseCommand findCommandExact txt of
-      Nothing | isBatch && stopOnError  -> return CommandError
-              | otherwise -> loop -- say somtething?
+           | otherwise -> loop lineNum
+         NextLine ls
+           | all (all isSpace) ls -> loop (lineNum + length ls)
+           | otherwise            -> doCommand lineNum ls
+
+  doCommand lineNum txt =
+    case parseCommand findCommandExact (unlines txt) of
+      Nothing | isBatch && stopOnError -> return CommandError
+              | otherwise -> loop (lineNum + length txt)  -- say somtething?
       Just cmd -> join $ MTL.lift $
-        do status <- handleInterrupt (handleCtrlC CommandError) (runCommand cmd)
+        do status <- handleInterrupt (handleCtrlC CommandError) (runCommand lineNum mbBatch cmd)
            case status of
              CommandError | isBatch && stopOnError -> return (return status)
              _ -> do goOn <- shouldContinue
-                     return (if goOn then loop else return status)
+                     return (if goOn then loop (lineNum + length txt) else return status)
 
 
-data NextLine = NextLine String | NoMoreLines | Interrupted
+data NextLine = NextLine [String] | NoMoreLines | Interrupted
 
 getInputLines :: String -> InputT REPL NextLine
 getInputLines = handleInterrupt (MTL.lift (handleCtrlC Interrupted)) . loop []
@@ -91,7 +91,7 @@ getInputLines = handleInterrupt (MTL.lift (handleCtrlC Interrupted)) . loop []
          Nothing -> return NoMoreLines
          Just l
            | not (null l) && last l == '\\' -> loop (init l : ls) newPropmpt
-           | otherwise -> return $ NextLine $ unlines $ reverse $ l : ls
+           | otherwise -> return $ NextLine $ reverse $ l : ls
 
 loadCryRC :: Cryptolrc -> REPL CommandExitCode
 loadCryRC cryrc =
@@ -201,7 +201,7 @@ canDisplayColor = io (hSupportsANSI stdout)
 cryptolCommand :: CompletionFunc REPL
 cryptolCommand cursor@(l,r)
   | ":" `isPrefixOf` l'
-  , Just (cmd,rest) <- splitCommand l' = case nub (findCommand cmd) of
+  , Just (_,cmd,rest) <- splitCommand l' = case nub (findCommand cmd) of
 
       [c] | null rest && not (any isSpace l') -> do
             return (l, cmdComp cmd c)

src/Cryptol/Backend.hs

@@ -35,31 +35,28 @@ import Data.Kind (Type)
 import Data.Ratio ( (%), numerator, denominator )
 
 import Cryptol.Backend.FloatHelpers (BF)
-import Cryptol.Backend.Monad ( PPOpts(..), EvalError(..) )
-import Cryptol.TypeCheck.AST(Name)
+import Cryptol.Backend.Monad
+  ( PPOpts(..), EvalError(..), CallStack, pushCallFrame )
+import Cryptol.ModuleSystem.Name(Name)
+import Cryptol.Parser.Position
 import Cryptol.Utils.PP
 
 
 invalidIndex :: Backend sym => sym -> Integer -> SEval sym a
-invalidIndex sym = raiseError sym . InvalidIndex . Just
+invalidIndex sym i = raiseError sym (InvalidIndex (Just i))
 
 cryUserError :: Backend sym => sym -> String -> SEval sym a
-cryUserError sym = raiseError sym . UserError
+cryUserError sym msg = raiseError sym (UserError msg)
 
 cryNoPrimError :: Backend sym => sym -> Name -> SEval sym a
-cryNoPrimError sym = raiseError sym . NoPrim
-
+cryNoPrimError sym nm = raiseError sym (NoPrim nm)
 
 {-# INLINE sDelay #-}
 -- | Delay the given evaluation computation, returning a thunk
 --   which will run the computation when forced.  Raise a loop
 --   error if the resulting thunk is forced during its own evaluation.
-sDelay :: Backend sym => sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
-sDelay sym msg m =
-  let msg'  = maybe "" ("while evaluating "++) msg
-      retry = raiseError sym (LoopError msg')
-   in sDelayFill sym m retry
-
+sDelay :: Backend sym => sym -> SEval sym a -> SEval sym (SEval sym a)
+sDelay sym m = sDelayFill sym m Nothing ""
 
 -- | Representation of rational numbers.
 --     Invariant: denominator is not 0
@@ -234,13 +231,23 @@ class MonadIO (SEval sym) => Backend sym where
   --   which will run the computation when forced.  Run the 'retry'
   --   computation instead if the resulting thunk is forced during
   --   its own evaluation.
-  sDelayFill :: sym -> SEval sym a -> SEval sym a -> SEval sym (SEval sym a)
+  sDelayFill :: sym -> SEval sym a -> Maybe (SEval sym a) -> String -> SEval sym (SEval sym a)
 
   -- | Begin evaluating the given computation eagerly in a separate thread
   --   and return a thunk which will await the completion of the given computation
   --   when forced.
   sSpark :: sym -> SEval sym a -> SEval sym (SEval sym a)
 
+  -- | Push a call frame on to the current call stack while evaluating the given action
+  sPushFrame :: sym -> Name -> Range -> SEval sym a -> SEval sym a
+  sPushFrame sym nm rng m = sModifyCallStack sym (pushCallFrame nm rng) m
+
+  -- | Apply the given function to the current call stack while evaluating the given action
+  sModifyCallStack :: sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
+
+  -- | Retrieve the current evaluation call stack
+  sGetCallStack :: sym -> SEval sym CallStack
+
   -- | Merge the two given computations according to the predicate.
   mergeEval ::
      sym ->
@@ -257,7 +264,6 @@ class MonadIO (SEval sym) => Backend sym where
   -- | Indiciate that an error condition exists
   raiseError :: sym -> EvalError -> SEval sym a
 
-
   -- ==== Pretty printing  ====
   -- | Pretty-print an individual bit
   ppBit :: sym -> SBit sym -> Doc
@@ -674,7 +680,7 @@ class MonadIO (SEval sym) => Backend sym where
     SInteger sym ->
     SEval sym (SBit sym)
 
-  -- | Multiplicitive inverse in (Z n).
+  -- | Multiplicative inverse in (Z n).
   --   PRECONDITION: the modulus is a prime
   znRecip ::
     sym ->

src/Cryptol/Backend/Concrete.hs

@@ -136,10 +136,12 @@ instance Backend Concrete where
   type SFloat Concrete = FP.BF
   type SEval Concrete = Eval
 
-  raiseError _ err = io (X.throwIO err)
+  raiseError _ err =
+    do stk <- getCallStack
+       io (X.throwIO (EvalErrorEx stk err))
 
   assertSideCondition _ True _ = return ()
-  assertSideCondition _ False err = io (X.throwIO err)
+  assertSideCondition sym False err = raiseError sym err
 
   wordLen _ (BV w _) = w
   wordAsChar _ (BV _ x) = Just $! integerToChar x
@@ -157,9 +159,11 @@ instance Backend Concrete where
        y <- my
        f c x y
 
-  sDeclareHole _ = blackhole
+  sDeclareHole _ rng = blackhole rng
   sDelayFill _ = delayFill
   sSpark _ = evalSpark
+  sModifyCallStack _ f m = modifyCallStack f m
+  sGetCallStack _ = getCallStack
 
   ppBit _ b | b         = text "True"
             | otherwise = text "False"
@@ -393,6 +397,3 @@ fpRoundMode sym w =
     Right a  -> pure a
 
 
-
-
-