content: {-# LANGUAGE CPP                        #-}
  {-# LANGUAGE DataKinds                  #-}
  {-# LANGUAGE FlexibleContexts           #-}
  {-# LANGUAGE GADTs                      #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE LambdaCase                 #-}
  {-# LANGUAGE MultiParamTypeClasses      #-}
  {-# LANGUAGE MultiWayIf                 #-}
  {-# LANGUAGE OverloadedStrings          #-}
  {-# LANGUAGE PatternSynonyms            #-}
  {-# LANGUAGE Rank2Types                 #-}
  {-# LANGUAGE ScopedTypeVariables        #-}
  {-# LANGUAGE StrictData                 #-}
  {-# LANGUAGE TemplateHaskell            #-}
  {-# LANGUAGE TupleSections              #-}
  {-# LANGUAGE TypeApplications           #-}
  {-# LANGUAGE TypeFamilies               #-}
  {-# LANGUAGE ViewPatterns               #-}
  
  -- | Translation from typechecked 'AST' to 'Term', while accumulating an
  -- execution graph to be used during symbolic analysis and model reporting.
  module Pact.Analyze.Translate where
  
  import qualified Algebra.Graph              as Alga
  import           Control.Applicative        (Alternative (empty))
  import           Control.Lens               (Lens', at, cons, makeLenses, snoc,
                                               to, toListOf, use, view, zoom,
                                               (%=), (%~), (+~), (.=), (.~),
                                               (<>~), (?=), (^.), (<&>), _1, (^..))
  import           Control.Monad              hiding (guard)
  import           Control.Monad.Except       (Except, MonadError, throwError)
  import           Control.Monad.Reader       (MonadReader (local),
                                               ReaderT (runReaderT))
  import           Control.Monad.State.Strict (MonadState, StateT, evalStateT,
                                               modify', runStateT)
  #if MIN_VERSION_base(4,20,0)
  import           Data.Foldable              (for_, foldlM)
  #else
  import           Data.Foldable              (foldl', for_, foldlM)
  #endif
  import           Data.List                  (sort)
  import           Data.List.Unsafe           (unsafeTail)
  import qualified Data.Map                   as Map
  import           Data.Map.Strict            (Map)
  import           Data.Maybe                 (fromMaybe, isNothing)
  import           Data.Proxy                 (Proxy)
  import           Data.Set                   (Set)
  import qualified Data.Set                   as Set
  import           Data.Text                  (Text)
  import qualified Data.Text                  as T
  import           Data.Traversable           (for)
  import           Data.Type.Equality         ((:~:) (Refl))
  import           GHC.TypeLits hiding (SSymbol)
  
  import qualified Pact.Types.Info as P
  import           Pact.Types.Lang
                   ( Info, Literal (..)
                   , Type (TyFun, TyPrim, TySchema, TyUser, TyVar, TyModule)
                   , SchemaPartial (PartialSchema)
                   )
  import qualified Pact.Types.Lang            as Pact
  import           Pact.Types.Persistence     (WriteType)
  import           Pact.Time                  (parseTime)
  import           Pact.Types.Typecheck       (AST, Named (..), Node, aId,
                                               aNode, aTy, tiName, _aTy)
  import qualified Pact.Types.Typecheck       as Pact
  import           Pact.Types.Util            (tShow,AsString(..))
  
  import           Pact.Analyze.Feature       hiding (TyFun, TyVar, Var, col,
                                               list, obj, str, time)
  import           Pact.Analyze.Patterns
  import           Pact.Analyze.Types
  import           Pact.Analyze.Util
  import Pact.Types.Pretty (renderCompactText)
  import Pact.Types.PactError
  
  -- * Translation types
  
  data TranslateFailure = TranslateFailure
    { _translateFailureInfo :: Info
    , _translateFailure     :: TranslateFailureNoLoc
    } deriving Show
  
  data TranslateFailureNoLoc
    = BranchesDifferentTypes EType EType
    | NonStringLitInBinding (AST Node)
    | EmptyBody
    | InvalidNativeInModule Text
    | MalformedArithOp Text [AST Node]
    | MalformedLogicalOp Text [AST Node]
    | MalformedComparison Text [AST Node]
    | NotConvertibleToSchema (Pact.Type Pact.UserType)
    | TypeMismatch EType EType
    | UnexpectedNode (AST Node)
    | UnexpectedPactNode (AST Node)
    | MissingConcreteType (Pact.Type Pact.UserType)
    | MonadFailure String
    | NonStaticColumns (AST Node)
    | BadNegationType (AST Node)
    | BadTimeType (AST Node)
    | FailedVarLookup Text
    | NoKeys (AST Node)
    | NoReadMsg (AST Node)
    | DeprecatedList Node
    | SimpleTypeRequired
    | TypeError Node
    | FreeVarInvariantViolation Text
    | UnhandledType Node (Pact.Type Pact.UserType)
    | SortLiteralObjError String (Existential (Core Term))
    | CapabilityNotFound CapName
    | BadPartialBind EType [String]
    | UnexpectedDefaultReadType EType EType
    | UnsupportedNonFatal Text
    | UnscopedCapability CapName
    | CapabilityNotManagedOrEvent CapName
    deriving (Eq, Show)
  
  describeTranslateFailureNoLoc :: TranslateFailureNoLoc -> RenderedOutput
  describeTranslateFailureNoLoc = \case
    BranchesDifferentTypes t1 t2 ->
      renderFatal $ "two branches unexpectedly have different types: (" <> tShow t1 <> ") vs (" <> tShow t2 <> ")"
    NonStringLitInBinding ast ->
      renderFatal $ "We only support analysis of binding forms (bind / with-read) binding string literals. Instead we found " <> tShow ast
    EmptyBody ->
      renderFatal $ "can't translate an empty body"
    InvalidNativeInModule native -> renderFatal ("Invalid native '" <> native <> "' in module code")
    MalformedArithOp op args ->
      renderFatal $ "Unsupported arithmetic op " <> op <> " with args " <> tShow args
    MalformedLogicalOp op args ->
      renderFatal $ "Unsupported logical op " <> op <> " with args " <> tShow args
    MalformedComparison op args ->
      renderFatal $ "Unsupported comparison op " <> op <> " with args " <> tShow args
    NotConvertibleToSchema ty ->
      renderFatal $ "Expected a schema, but found " <> tShow ty
    TypeMismatch ty1 ty2 ->
      renderFatal $ "Type mismatch: (" <> tShow ty1 <> ") vs (" <> tShow ty2 <> ")"
    UnexpectedNode ast ->
      renderFatal $ "Analysis doesn't support this construct yet: " <> renderCompactText ast
    UnexpectedPactNode ast ->
      renderFatal $ "Unexpected node in translation of a pact: " <> tShow ast
    MissingConcreteType ty ->
      renderFatal $ "The typechecker should always produce a concrete type, but we found " <> tShow ty
    MonadFailure str ->
      renderFatal $ "Translation failure: " <> T.pack str
    NonStaticColumns col ->
      renderFatal $ "We require all column (field) names to be concrete in order to do analysis. We found " <> tShow col
    BadNegationType node ->
      renderFatal $ "Invalid: negation of a non-integer / decimal: " <> tShow node
    BadTimeType node ->
      renderFatal $ "Invalid: days / hours / minutes applied to non-integer / decimal: " <> tShow node
    FailedVarLookup varName ->
      renderFatal $ "Failed to look up a variable (" <> varName <> "). This likely means the variable wasn't properly bound."
    NoKeys _node  ->
      renderFatal $ "`keys` is not yet supported"
    NoReadMsg _ ->
      renderFatal $ "`read-msg` is not yet supported"
    DeprecatedList node ->
      renderFatal $ "Analysis doesn't support the deprecated `list` function -- please update to literal list syntax: " <> tShow node
    SimpleTypeRequired ->
      renderFatal $ "Lists are currently limited to holding simply-typed objects"
    TypeError node ->
      renderFatal $ "\"impossible\" post-typechecker type error in node: " <> tShow node
    FreeVarInvariantViolation msg ->
      renderFatal $ msg
    UnhandledType node ty ->
      renderFatal $ "Found a type we don't know how to translate yet: " <> tShow ty <> " at node: " <> tShow node
    SortLiteralObjError msg tm ->
      renderFatal $ T.pack $ msg ++ show tm
    CapabilityNotFound (CapName cn) ->
      renderFatal $ "Found a reference to capability that does not exist: " <> T.pack cn
    BadPartialBind (EType objTy) columnNames ->
      renderFatal $ "Couldn't extract fields " <> tShow columnNames <> " from object of type " <> tShow objTy
    UnexpectedDefaultReadType (EType expected) (EType received) ->
      renderFatal $ "Bad type in a `with-default-read`: we expected " <> tShow expected <>
      " (the type of the provided default), but saw " <> tShow received <> " (based on the fields that were bound)."
    UnsupportedNonFatal msg ->
      renderWarn $ "Unsupported operation: " <> msg
    UnscopedCapability (CapName cap) ->
      renderWarn $ "Direct execution restricted by capability " <> T.pack cap
    CapabilityNotManagedOrEvent (CapName cap) ->
      renderFatal $ "Capability " <> T.pack cap <> " " <> "not managed or event"
  
  
  data TranslateEnv
    = TranslateEnv
      { _teInfo           :: Info
      , _teCapabilities   :: Map CapName Capability
      , _teNodeVars       :: Map Node (Munged, VarId)
      , _teRecoverability :: Recoverability
      , _teScopesEntered  :: Natural
  
      -- How to generate the next tag and vertex ids. Usually this is via @genId@
      -- (see @mkTranslateEnv@) but in testing these return a constant @0@.
      , _teGenTagId       :: forall m. MonadState TagId  m => m TagId
      , _teGenVertex      :: forall m. MonadState Vertex m => m Vertex
      }
  
  mkTranslateEnv :: Info -> [Capability] -> [Arg] -> TranslateEnv
  mkTranslateEnv info caps args
    = TranslateEnv info caps' nodeVars mempty 0 (genId id) (genId id)
    where
      -- NOTE: like in Check's moduleFunChecks, this assumes that toplevel
      -- function arguments are the only variables for which we do not use munged
      -- names:
      nodeVars = foldl'
        (\m (Arg nm vid node _ety) ->
          Map.insert node (coerceUnmungedToMunged nm, vid) m)
        Map.empty
        args
  
      caps' = Map.fromList $ caps <&> \c@(Capability _ capName _) -> (capName, c)
  
      coerceUnmungedToMunged :: Unmunged -> Munged
      coerceUnmungedToMunged (Unmunged nm) = Munged nm
  
  data TranslateState
    = TranslateState
      { _tsNextTagId     :: TagId
      , _tsNextVarId     :: VarId
      , _tsNextGuard     :: Guard
      , _tsGraph         :: Alga.Graph Vertex
        -- ^ The execution graph we've built so far. This is expanded upon as we
        -- translate an entire function.
      , _tsPathHead      :: Vertex
        -- ^ The "latest" vertex/current path of the graph. This starts out as
        -- the single initial vertex. it splits into two if we hit a conditional,
        -- and rejoins afterwards.
      , _tsNextVertex    :: Vertex
      , _tsEdgeEvents    :: Map Edge [TraceEvent]
        -- ^ Events added to each new 'Edge' upon creating a new 'Vertex' which
        -- closes/completes the 'Edge'.
      , _tsPendingEvents :: SnocList TraceEvent
        -- ^ Events being accumulated until the creation of the next 'Vertex'.
      , _tsCurrentPath   :: Path
        -- ^ Path to be associated with the 'Edge' formed by the creation of the
        -- next 'Vertex'.
      , _tsPathEdges     :: Map Path [Edge]
        -- ^ Graph edges corresponding to a given execution "path".
        --
        -- 'TraceSubpathStart's are emitted once for each path: at the start of
        -- an execution trace, and at the beginning of either side of a
        -- conditional. After a conditional, we resume the path from before the
        -- conditional. Either side of a conditional will contain a minimum of
        -- two edges: splitting away from the other branch, and then rejoining
        -- back to the other branch at the join point. The following program:
        --
        --     (defun test ()
        --       (if true 1 2))
        --
        -- will result in the following diagram, with six total edges (where /,
        -- \, and - are edges):
        --        .
        --       / \
        --     ->   ->
        --       \./
        --
        -- The initial edge leading into the conditional, two for each branch,
        -- and a final edge after the two branches have rejoined one another. We
        -- must have two edges for each branch so that we can unambiguously talk
        -- about either branch in our graph representation, where we only one
        -- permit one edge in a given direction between two vertices.
        --
        -- Also note that in the presence of nested conditionals, these
        -- "branch-out" and "rejoin" edges will not be contiguous in the graph on
        -- the side of the outer conditional which contains the nested
        -- conditional:
        --       ......
        --     _/  .   \_
        --      \ / \ _/
        --        \./
        --
        -- We track all of the edges for each path so that we can determine the
        -- subset of edges on the graph that form the upper bound for the edges
        -- that are reached during a particular execution trace. We say "upper
        -- bound" here because some traces will not execute entirely to the end
        -- of the program due to the use of e.g. @enforce@ and @enforce-keyset@.
        --
        -- There's one more scenario where we start subpaths: for each of the
        -- "cases" of an @enforce-one@. Here's an example with three cases:
        --
        --     (enforce-one [case-1 case-2 case-3])
        --
        --     \____        <- case-1 runs, always
        --      \___ ._     <- case-2 runs if case-1 fails
        --       \__        <- case-3 runs if case-2 fails
        --
        -- The \ edges correspond to the execution of each case. The _ edges
        -- correspond to successful exit early due to the lack of a failure.
        -- These three "success" edges all join together at the same vertex.
      , _tsFoundVars     :: [(VarId, Text, EType)]
  
        -- Vars representing nondeterministic choice between two branches. These
        -- are used for continuing on or rolling back in evaluation of pacts.
      , _tsStepChoices   :: [VarId]
      , _tsWarnings :: [TranslateFailure]
        -- ^ Non-fatal translation problems
      , _tsStaticCapsInScope :: Set CapName
        -- ^ Statically track caps possibly brought into scope
      }
  
  makeLenses ''TranslateFailure
  makeLenses ''TranslateEnv
  makeLenses ''TranslateState
  
  instance HasVarId TranslateState where
    varId = tsNextVarId
  
  class HasInfo e where
    envInfo :: Lens' e Info
  
  instance HasInfo Info where
    envInfo = id
  
  instance HasInfo TranslateEnv where
    envInfo = teInfo
  
  newtype TranslateM a
    = TranslateM
      { unTranslateM :: ReaderT TranslateEnv
                          (StateT TranslateState
                            (Except TranslateFailure))
                          a
      }
    deriving (Functor, Applicative, Monad, MonadReader TranslateEnv,
      MonadState TranslateState, MonadError TranslateFailure)
  
  failing :: String -> TranslateM a
  failing s = do
    info <- view envInfo
    throwError (TranslateFailure info (MonadFailure s))
  
  -- * Translation
  
  emit :: TraceEvent -> TranslateM ()
  emit event = modify' $ tsPendingEvents %~ flip snoc event
  
  -- | Call when entering a node to set the current context
  withNodeContext :: Node -> TranslateM a -> TranslateM a
  withNodeContext node = local (envInfo .~ nodeToInfo node)
  
  -- | Call when entering an ast node to set the current context
  withAstContext :: AST Node -> TranslateM a -> TranslateM a
  withAstContext ast = local (envInfo .~ astToInfo ast)
  
  withNestedRecoverability :: Recoverability -> TranslateM a -> TranslateM a
  withNestedRecoverability r = local $ teRecoverability <>~ r
  
  -- | Enter a pact step or rollback.
  --
  -- This differs from 'withNewScope' by not tracing a return value from the
  -- action (since steps don't return anything). When we're translating a step in
  -- isolation, for a single step analysis, we bind variables that come from the
  -- enclosing @defpact@, otherwise (when doing a whole-pact analysis), the
  -- pact-level variables will already be in scope. The 'ScopeType' should be
  -- 'StepScope' or 'RollbackScope'.
  withNewStep :: ScopeType -> [Located Binding] -> TranslateM a -> TranslateM a
  withNewStep scopeType bindings act = local (teScopesEntered +~ 1) $ do
    tid <- genTagId
    depth <- view teScopesEntered
    emit $ TracePushScope depth scopeType bindings
    res <- act
    emit $ TracePopScope depth scopeType tid $ EType SStr
    pure res
  
  -- | Enter a new scope, binding variables.
  withNewScope
    :: ScopeType
    -> [Located Binding]
    -> TranslateM ETerm
    -> TranslateM ETerm
  withNewScope scopeType bindings act = local (teScopesEntered +~ 1) $ do
    tid <- genTagId
    depth <- view teScopesEntered
    emit $ TracePushScope depth scopeType bindings
    res <- mapExistential (Return tid) <$> act
    let ty = existentialType res
    emit $ TracePopScope depth scopeType tid ty
    pure res
  
  genTagId :: TranslateM TagId
  genTagId = TranslateM $ zoom tsNextTagId $ join $ view teGenTagId
  
  nodeInfo :: Node -> Info
  nodeInfo node = node ^. aId . Pact.tiInfo
  
  startSubpath :: Path -> TranslateM ()
  startSubpath p = do
    tsCurrentPath .= p
    emit $ TraceSubpathStart p
  
  startNewSubpath :: TranslateM Path
  startNewSubpath = do
    p <- Path <$> genTagId
    startSubpath p
    pure p
  
  tagDbAccess
    :: (TableName -> ESchema -> Located TagId -> TraceEvent)
    -> TableName
    -> Node
    -> ESchema
    -> TranslateM TagId
  tagDbAccess mkEvent tname node schema = do
    tid <- genTagId
    emit $ mkEvent tname schema (Located (nodeInfo node) tid)
    pure tid
  
  tagRead :: TableName -> Node -> ESchema -> TranslateM TagId
  tagRead = tagDbAccess TraceRead
  
  tagWrite :: WriteType -> TableName -> Node -> ESchema -> TranslateM TagId
  tagWrite = tagDbAccess . TraceWrite
  
  tagYield :: EType -> TranslateM TagId
  tagYield ety = do
    tid <- genTagId
    emit $ TraceYield ety tid
    pure tid
  
  tagResume :: EType -> TranslateM TagId
  tagResume ety = do
    tid <- genTagId
    emit $ TraceResume ety tid
    pure tid
  
  tagAssert :: Node -> TranslateM TagId
  tagAssert node = do
    tid <- genTagId
    recov <- view teRecoverability
    emit $ TraceAssert recov $ Located (nodeInfo node) tid
    pure tid
  
  tagGuard :: Node -> TranslateM TagId
  tagGuard node = do
    tid <- genTagId
    recov <- view teRecoverability
    emit $ TraceGuard recov $ Located (nodeInfo node) tid
    pure tid
  
  -- Note: uses left-biased union to prefer new vars
  withNodeVars :: [Named Node] -> [Located Binding] -> TranslateM a -> TranslateM a
  withNodeVars namedNodes bindings = local (teNodeVars %~ Map.union nodeVars)
    where
      nodeVars :: Map Node (Munged, VarId)
      nodeVars = Map.fromList
        [ (node, (munged, vid))
        | ((Named _ node _), Located _ (Binding vid _ munged _))
            <- zip namedNodes bindings
        ]
  
  maybeTranslateUserType
    :: Maybe (Set Text)
    -- ^ Set of keys to keep (if this is a partial schema)
    -> Pact.UserType
    -> Maybe QType
  maybeTranslateUserType _ (Pact.UTModSpec _) = Just $ EType $ mkSObject (SingList SNil)
  maybeTranslateUserType _ (Pact.UTSchema (Pact.Schema _ _ [] _)) = Just $ EType $ mkSObject (SingList SNil)
  maybeTranslateUserType restrictKeys (Pact.UTSchema (Pact.Schema a b (Pact.Arg name ty _:tys) c)) = do
    subTy@(EType (SObject tys'))
      <- maybeTranslateUserType restrictKeys $ Pact.UTSchema $ Pact.Schema a b tys c
    EType ty' <- maybeTranslateType ty
  
    let keepThisKey = case restrictKeys of
          Nothing  -> True
          Just set -> name `Set.member` set
  
    if keepThisKey
    then
  
      withSing ty' $ withTypeable ty' $
        case someSymbolVal (T.unpack name) of
          SomeSymbol (_ :: Proxy sym) ->
            -- we can use @SObjectUnsafe@ here instead of @mkSObject@ because we
            -- @insert@ the new column.
            Just $ EType $ SObjectUnsafe $ SingList $
              insert (SSymbol @sym) ty' (UnSingList tys')
  
    else Just subTy
  
  maybeTranslateUserType' :: Pact.UserType -> Maybe EType
  maybeTranslateUserType' = maybeTranslateUserType Nothing >=> downcastQType
  
  maybeTranslateType :: Pact.Type Pact.UserType -> Maybe EType
  maybeTranslateType = maybeTranslateType' Nothing >=> downcastQType
  
  -- A helper to translate types that doesn't know how to handle user types
  -- itself
  maybeTranslateType'
    :: Maybe (Set Text)
    -- ^ Set of keys to keep (if this is a partial schema)
    -> Pact.Type Pact.UserType
    -> Maybe QType
  maybeTranslateType' restrictKeys = \case
    -- Note: TyUser vs TySchema
    --
    -- A user type holds a schema type (@TyUser TySchema{}@). A schema type can
    -- be @TyTable@, @TyObject@, or @TyBinding@.
    TyUser a -> maybeTranslateUserType restrictKeys a
  
    TySchema Pact.TyTable _ _ -> pure QTable
    TySchema _ ty' (PartialSchema keys)
      -> maybeTranslateType' (Just keys) ty'
    TySchema _ ty' _
      -> maybeTranslateType' Nothing ty'
  
    TyPrim Pact.TyBool        -> pure $ EType SBool
    TyPrim Pact.TyDecimal     -> pure $ EType SDecimal
    TyPrim Pact.TyInteger     -> pure $ EType SInteger
    TyPrim Pact.TyString      -> pure $ EType SStr
    TyPrim Pact.TyTime        -> pure $ EType STime
    TyPrim (Pact.TyGuard _)   -> pure $ EType SGuard
  
    TyVar (Pact.SchemaVar (Pact.TypeVarName "table")) -> pure QTable
  
    -- Pretend any and an unknown var are the same -- we can't analyze either of
    -- them.
    -- TODO(joel): revisit this assumption
    TyVar _                                           -> pure $ EType SAny
    Pact.TyAny                                        -> pure $ EType SAny
  
    Pact.TyList a -> do
      ty <- maybeTranslateType' Nothing a
      case ty of
        EType ty' -> pure $ EType $ SList ty'
        _         -> empty
  
    TyFun _             -> empty
  
    TyModule _ -> pure $ EType SStr -- modrefs are coerced to strings
  
  throwError'
    :: (MonadError TranslateFailure m, MonadReader r m, HasInfo r)
    => TranslateFailureNoLoc -> m a
  throwError' err = do
    info <- view envInfo
    throwError $ TranslateFailure info err
  
  -- | Generates a new 'Vertex'. Does *not* add this new 'Vertex' to the graph.
  genVertex :: TranslateM Vertex
  genVertex = TranslateM $ zoom tsNextVertex $ join $ view teGenVertex
  
  -- | Flushes-out events accumulated for the current edge of the execution path.
  flushEvents :: TranslateM [TraceEvent]
  flushEvents = use tsPendingEvents >>= \case
    ConsList pathEvents -> do
      tsPendingEvents .= mempty
      pure pathEvents
    _ -> failing "Pattern match failure"
  
  addPathEdge :: Path -> Edge -> TranslateM ()
  addPathEdge path e =
    tsPathEdges.at path %= pure . cons e . fromMaybe []
  
  extendPathTo :: Vertex -> TranslateM ()
  extendPathTo toV = do
    path <- use tsCurrentPath
    v    <- use tsPathHead
    tsGraph %= Alga.overlay (Alga.edge v toV)
    edgeTrace <- flushEvents
    let e = (v, toV)
    tsEdgeEvents.at e ?= edgeTrace
    addPathEdge path e
    tsPathHead .= toV
  
  -- | Extends the previous path head to a new 'Vertex', flushing accumulated
  -- events to 'tsEdgeEvents'.
  extendPath :: TranslateM Vertex
  extendPath = do
    v' <- genVertex
    extendPathTo v'
    pure v'
  
  -- | Extends multiple separate paths to a single join point. Assumes that each
  -- 'Vertex' was created via 'extendPath' before invocation, and thus
  -- 'tsPendingEvents' is currently empty.
  joinPaths :: [(Vertex, Path)] -> TranslateM ()
  joinPaths branches = do
    let vs = map fst branches
    v' <- genVertex
    tsPathHead .= v'
    tsGraph %= Alga.overlay (Alga.vertices vs `Alga.connect` pure v')
    for_ branches $ \(v, path) -> do
      isNewPath <- use $ tsPathEdges.at path.to isNothing
      let rejoinEdge = (v, v')
      tsEdgeEvents.at rejoinEdge ?= [TraceSubpathStart path | isNewPath]
      addPathEdge path rejoinEdge
  
  -- | When we bind a subset of fields in a type, we need to determine the sub-
  -- schema type.
  typeOfPartialBind
    :: SingTy ('TyObject schema) -> [(Named Node, AST Node)] -> TranslateM EType
  typeOfPartialBind objTy bindings = do
    columnNames <- for bindings $ \case
      (_, Pact.Prim _ (Pact.PrimLit (LString name))) -> pure $ T.unpack name
      (_, binding) -> throwError' $ NonStaticColumns binding
  
    -- The object keys are sorted so we must sort our binding names to match them
    -- in the correct order
    typeOfPartialBind' objTy (sort columnNames)
      ?? BadPartialBind (EType objTy) columnNames
  
  typeOfPartialBind'
    :: SingTy ('TyObject schema) -> [String] -> Maybe EType
  typeOfPartialBind' SObjectNil []
    = Just $ EType SObjectNil
  typeOfPartialBind' SObjectNil _
    = Nothing
  typeOfPartialBind' SObjectCons{} []
    = Just $ EType SObjectNil
  typeOfPartialBind' (SObjectCons k v schema') (name:names)
    | symbolVal k == name
    = do EType (SObject subschema)
           <- typeOfPartialBind' (SObjectUnsafe schema') names
         pure $ EType $ SObjectCons k v subschema
    | otherwise
    = typeOfPartialBind' (SObjectUnsafe schema') (name:names)
  typeOfPartialBind' _ _
    = vacuousMatch "pattern synonyms lead to an erroneous warning here"
  
  translateType
    :: (MonadError TranslateFailure m, MonadReader r m, HasInfo r)
    => Node -> m EType
  translateType node = case _aTy node of
    (maybeTranslateType -> Just ety) -> pure ety
    ty                               -> throwError' $ UnhandledType node ty
  
  translateArg
    :: ( MonadState s m
       , HasVarId s
       , MonadReader r m
       , HasInfo r
       , MonadError TranslateFailure m
       )
    => Named Node
    -> m Arg
  translateArg (Named nm node _) = do
    vid <- genVarId
    ety <- translateType node
    pure (Arg (Unmunged nm) vid node ety)
  
  translateBinding :: Named Node -> TranslateM (Located Binding)
  translateBinding (Named unmunged' node _) = do
    vid <- genVarId
    let munged = node ^. aId.tiName.to Munged
        info   = node ^. aId . Pact.tiInfo
    varType <- translateType node
    pure $ Located info $ Binding vid (Unmunged unmunged') munged varType
  
  translateBody :: [AST Node] -> TranslateM ETerm
  translateBody = \case
    []       -> do
      info <- view envInfo
      throwError $ TranslateFailure info EmptyBody
    [ast]    -> translateNode ast
    ast:asts -> do
      someExpr      <- translateNode ast
      Some ty exprs <- translateBody asts
      pure $ Some ty $ Sequence someExpr exprs
  
  -- Pact translation:
  --
  -- We translate steps in the order they'll be eventually evaluated, meaning we
  -- first translate each step, then each rollback. In the diagram we translate
  -- s1, s2, s3, r2, r1. Note that the c edges have no computation / translation.
  --
  --      src          sink
  --       +      /---->+
  --       |      |     ^
  --    s1 |      |     |
  --       |      | r1  |
  --       v  c2  |     |
  --       +----->+     |
  --       |      ^     |
  --    s2 |      |     |
  --       |      | r2  |
  --       v  c3  |     |
  --       +----->+     |
  --       |            |
  --    s3 |            |
  --       |            |
  --       v            |
  --       +------------/
  --
  -- This first diagram is for a pact with the following structure:
  --
  --     (defpact
  --       (step-with-rollback s1 r1)
  --       (step-with-rollback s2 r2)
  --       (step s3))
  --
  -- Note the numbering scheme:
  -- * steps are numbered how you might expect
  -- * rollbacks are numbered to match their corresponding step
  -- * cancels are numbered to match the step they're an alternative to
  --
  -- This means that if there are n step edges, there are:
  -- * n-1 cancel edges
  -- * from 0 to n-1 (inclusive) rollback edges
  --
  -- Furthermore, there are:
  -- * n vertices following a step (including the sink)
  -- * from 0 to n-1 (inclusive) vertices preceding a rollback
  --
  -- What if we drop the first rollback?
  --
  --     (defpact
  --       (step s1)
  --       (step-with-rollback s2 r2)
  --       (step s3))
  --
  -- The corresponding graph ends up looking like:
  --
  --      src    c2    sink
  --       +    /------>+
  --       |   /       /^
  --    s1 |  /       / |
  --       | /       /  |
  --       v/       /   |
  --       +       /    |
  --       |      /     |
  --    s2 |      |     |
  --       |      | r2  |
  --       v  c3  |     |
  --       +----->+     |
  --       |            |
  --    s3 |            |
  --       |            |
  --       v            |
  --       +------------/
  translatePact :: [AST Node] -> TranslateM [PactStep]
  translatePact nodes = do
    preStepsPath    <- use tsCurrentPath
    protoSteps      <- go True nodes
    postSnVertex    <- use tsPathHead
    snPath          <- use tsCurrentPath
    postLastCancelV <- genVertex
  
    (sinkV, cancels, rollbacks) <- foldlM
      (\(rightV, cancels, rollbacks) (_step, leftV, mRollback) -> do
        tsPathHead .= leftV
        emit TraceReset
        cancel <- (,) <$> startNewSubpath <*> genVarId
        emit $ TraceCancel $ _pathTag $ fst cancel
        extendPathTo rightV
        case mRollback of
          Nothing
            -> pure (rightV, cancel : cancels, Nothing : rollbacks)
          Just rollbackA -> withNewStep RollbackScope [] $ do
            rollback <- (,)
              <$> startNewSubpath
              <*> translateNode rollbackA
            postRollback <- extendPath
            pure (postRollback, cancel : cancels, Just rollback : rollbacks)
        )
      (postLastCancelV, [], [])
      -- all but the last step, in reverse order
      -- TODO: ?!?!?!?
      -- Arcane magic here, but the nested pact steps here may actually be empty
      -- in the case of a nested defpact execution from a module reference (interface empty body problem).
      -- The proper fix is recognizing the nested defpact dyn invoke and replacing it with
      -- the default value of what the invocation would return.
      -- For now, this unblocks the problem.
      (if null protoSteps then [] else unsafeTail $ reverse protoSteps)
  
    let steps = zipWith3
          (\(Step exec p e _ _) mCancel mRb -> Step exec p e mCancel mRb)
          (protoSteps ^.. traverse . _1)
          (Nothing : fmap Just cancels)
          (rollbacks <> [Nothing])
  
    tsStepChoices .= fmap snd cancels
  
    -- connect sink
    tsPathHead    .= postSnVertex
    tsCurrentPath .= snPath
    extendPathTo sinkV
  
    -- restore initial path
    tsCurrentPath .= preStepsPath
  
    pure steps
  
    where
      -- We don't generate a cancel var on the first step but we do for all
      -- subsequent steps.
      go firstStep = \case
        []       -> pure []
        ast:asts -> (:) <$> translateStep firstStep ast <*> go False asts
  
  translateStep
    :: Bool -> AST Node -> TranslateM (PactStep, Vertex, Maybe (AST Node))
  translateStep firstStep ast = case ast of
    AST_Step _node entity exec rollback _yr -> withNewStep StepScope [] $ do
      p <- if firstStep then use tsCurrentPath else startNewSubpath
      mEntity <- for entity $ \tm -> translateNode tm >>= \case
        Some SStr entity' -> pure entity'
        _ -> throwError' $ UnexpectedPactNode ast
      Some ty exec' <- translateNode exec
      postVertex    <- extendPath
      pure (Step (exec' , ty) p mEntity Nothing Nothing, postVertex, rollback)
    _ -> throwError' $ UnexpectedPactNode ast
  
  lookupCapability :: CapName -> TranslateM Capability
  lookupCapability capName = do
    mCap <- view $ teCapabilities.at capName
    case mCap of
      Just cap -> pure cap
      Nothing  -> throwError' $ CapabilityNotFound capName
  
  withTranslatedBindings
    :: [(Named Node, AST Node)]
    -> ([Located Binding] -> TranslateM ETerm)
    -> TranslateM ETerm
  withTranslatedBindings (unzip -> (bindingAs, rhsAs)) k = do
    bindingTs <- traverse translateBinding bindingAs
    rhsETs <- traverse translateNode rhsAs
  
    let -- Wrap the 'Term' body of clauses in a 'Let' for each of the bindings
        wrapWithLets :: Term a -> Term a
        wrapWithLets tm = foldr
          (\(rhsET, Located _ (Binding vid _ (Munged munged) _)) body' ->
            Let munged vid rhsET body')
          tm
          (zip rhsETs bindingTs)
  
    fmap (mapExistential wrapWithLets) $
      withNodeVars bindingAs bindingTs $
        k bindingTs
  
  translateObjBinding
    :: [(Named Node, AST Node)]
    -> SingTy ('TyObject m)
    -> [AST Node]
    -> ETerm
    -> TranslateM ETerm
  translateObjBinding pairs schema bodyA rhsT = do
    let bindingAs = map fst pairs
    bindingTs <- traverse translateBinding bindingAs
    cols <- for pairs $ \case
      (_, AST_StringLit colName) ->
        pure $ T.unpack colName
      (Named _ node _, x) ->
        withNodeContext node $ throwError' $ NonStringLitInBinding x
  
    -- We create one synthetic binding for the object, which then only the column
    -- bindings use.
    objBindingId <- genVarId
    let objVar = CoreTerm $ Var objBindingId "binding"
  
    --
    -- TODO: we might want to only create a single Let here, with a binding for
    --       each column. at the moment we create a new Let for each binding. a
    --       single let would be slightly more elegant for generating assertions
    --       for tags during evaluation as well. with this current elaboration,
    --       we would generate @n@ extra/unnecessary assertions for @n@ columns
    --       (because we currently generate @n+1@ lets -- one synthetic binding
    --       for the object, and one for each column.
    --
  
    let wrapWithLets :: Term a -> Term a
        wrapWithLets innerBody = Let "binding" objBindingId rhsT $
          -- NOTE: *left* fold for proper shadowing/overlapping name semantics:
          foldl'
            (\body ( colName
                   , Located _ (Binding vid _ (Munged varName) (EType ty))
                   ) ->
              let colTerm = StrLit @Term colName
                  rhs = Some ty $ CoreTerm $ ObjAt schema colTerm objVar
              in Let varName vid rhs body)
            innerBody
            (zip cols bindingTs)
  
    fmap (mapExistential wrapWithLets) $
      withNewScope ObjectScope bindingTs $
        withNodeVars bindingAs bindingTs $
          translateBody bodyA
  
  pattern EmptyList :: Term ('TyList a)
  pattern EmptyList = CoreTerm (Lit [])
  
  translateNamedGuard :: AST Node -> TranslateM ETerm
  translateNamedGuard strA = translateNode strA >>= \case
    Some SStr strT -> do
      tid <- tagGuard $ strA ^. aNode
      return $ Some SBool $ Enforce Nothing $ GuardPasses tid $ MkKsRefGuard strT
    _ -> unexpectedNode strA
  
  translateGuard :: AST Node -> TranslateM ETerm
  translateGuard guardA = translateNode guardA >>= \case
    Some SGuard guardT -> do
      tid <- tagGuard $ guardA ^. aNode
      return $ Some SBool $ Enforce Nothing $ GuardPasses tid guardT
    _ -> unexpectedNode guardA
  
  translateCapabilityApp
    :: Pact.ModuleName
    -> CapName
    -> [(Named Node, AST Node)]
    -> [AST Node]
    -> TranslateM ETerm
  translateCapabilityApp modName capName bindingsA appBodyA = do
    cap <- lookupCapability capName
    withTranslatedBindings bindingsA $ \bindingTs -> do
      withNewScope (CapabilityScope modName capName) bindingTs $ do
        let vids = toListOf (traverse.located.bVid) bindingTs
        fmap (mapExistential $ Granting cap vids) $
          translateBody appBodyA
  
  -- | translate cap and vars for HasGrant or cap guard creation
  translateCapRef
    :: Pact.ModuleName
    -> Text
    -> [Located Binding]
    -> TranslateM (Capability, [(Text, VarId)])
  translateCapRef modName funName bindingTs = do
      cap <- lookupCapability $ mkCapName modName funName
      let vars = (\b -> (_mungedName . _bmName $ b, _bVid b)) . _located <$>
                 bindingTs
      return (cap,vars)
  
  
  
  genGuard :: TranslateM Guard
  genGuard = do
    g <- use tsNextGuard
    tsNextGuard %= succ
    pure g
  
  translateNode :: AST Node -> TranslateM ETerm
  translateNode astNode = withAstContext astNode $ case astNode of
    AST_Let bindings body ->
      withTranslatedBindings bindings $ \bindingTs -> do
        withNewScope LetScope bindingTs $
          translateBody body
  
    AST_InlinedApp modName funName Pact.Defpact bindings body ->
      withTranslatedBindings bindings $ \bindingTs -> do
      withNewScope (PactScope modName funName) bindingTs $
          Some SStr . Pact <$> translatePact body
  
    AST_InlinedApp modName funName _ bindings body ->
      withTranslatedBindings bindings $ \bindingTs -> do
        withNewScope (FunctionScope modName funName) bindingTs $
          translateBody body
  
    AST_Var node -> do
      mVar     <- view $ teNodeVars.at node
      translateType node >>= \case
        EType ty -> do
          (Munged varName, vid) <- case mVar of
            Just x  -> pure x
            Nothing -> do
              vid <- genVarId
              let tcName = node ^. aId . tiName
              tsFoundVars %= cons (vid, tcName, EType ty)
              pure (Munged tcName, vid)
          pure $ Some ty $ CoreTerm $ Var vid varName
  
    -- Int
    AST_NegativeLit l -> case l of
      LInteger i -> pure $ Some SInteger $ inject @(Numerical Term) $
        IntUnaryArithOp Negate $ Lit' i
      LDecimal d -> pure $ Some SDecimal $ inject @(Numerical Term) $
        DecUnaryArithOp Negate $ Lit' $ fromPact decimalIso d
      _          -> throwError' $ BadNegationType astNode
  
    AST_Lit l -> case l of
      LInteger i -> pure $ Some SInteger $ Lit' i
      LBool b    -> pure $ Some SBool    $ Lit' b
      LString s  -> pure $ Some SStr     $ Lit' $ Str $ T.unpack s
      LDecimal d -> pure $ Some SDecimal $ Lit' $ fromPact decimalIso d
      LTime t    -> pure $ Some STime    $ Lit' $ fromPact timeIso t
  
    AST_NegativeVar node -> view (teNodeVars.at node) >>= \case
      Just (Munged name, vid) -> translateType node >>= \case
        EType ty -> do
          case ty of
            SInteger     -> pure $ Some SInteger $ inject $ IntUnaryArithOp Negate $
              CoreTerm $ Var vid name
            SDecimal -> pure $ Some SDecimal $ inject $ DecUnaryArithOp Negate $
              CoreTerm $ Var vid name
            _        -> throwError' $ BadNegationType astNode
      _ -> unexpectedNode astNode
  
    AST_Format formatStr vars -> translateNode formatStr >>= \case
      Some SStr formatStr' -> do
        vars' <- for vars translateNode
        pure $ Some SStr $ Format formatStr' vars'
      _ -> unexpectedNode astNode
  
    AST_FormatTime formatStr time -> translateNode formatStr >>= \case
      Some SStr formatStr' -> translateNode time >>= \case
        Some STime time' -> pure $ Some SStr $ FormatTime formatStr' time'
        _ -> unexpectedNode astNode
      _ -> unexpectedNode astNode
  
    AST_ParseTime formatStr timeStr -> translateNode formatStr >>= \case
      Some SStr formatStr' -> translateNode timeStr >>= \case
        Some SStr timeStr' -> pure $ Some STime $ ParseTime (Just formatStr') timeStr'
        _ -> unexpectedNode astNode
      _ -> unexpectedNode astNode
  
    AST_Time timeStr -> translateNode timeStr >>= \case
      Some SStr timeStr' -> pure $ Some STime $ ParseTime Nothing timeStr'
      _ -> unexpectedNode astNode
  
    AST_Hash val -> do
      Some ty val' <- translateNode val
      let
        wrap :: Core Term 'TyStr -> TranslateM ETerm
        wrap = pure . Some SStr . CoreTerm
  
        notStaticShim = do
          addWarning' (UnsupportedNonFatal "Call to `hash` is only implemented for string, bool, and integer, substituting hash of `hello pact`")
          wrap (StrHash (Lit' (Str "hello pact")))
  
      case ty of
        SStr       -> wrap (StrHash val')
        SBool      -> wrap (BoolHash val')
        SInteger   -> wrap (IntHash val')
        SDecimal   -> wrap (DecHash val')
        SList ty'  -> case ty' of
          SInteger -> wrap (ListHash SInteger val')
          SDecimal -> wrap (ListHash SDecimal val')
          SStr     -> wrap (ListHash SStr val')
          SBool    -> wrap (ListHash SBool val')
          SList lt' -> wrap (ListHash (SList lt') val')
          _otherwise ->  notStaticShim
        _otherwise -> notStaticShim
  
    AST_Keccak val -> translateNode val >>= \case
      Some (SList SStr) val' -> pure $ Some SStr $ CoreTerm $ Keccak256Hash val'
      _ -> unexpectedNode astNode
  
    AST_ReadKeyset nameA -> translateNode nameA >>= \case
      Some SStr nameT -> return $ Some SGuard $ ReadKeySet nameT
      _ -> unexpectedNode astNode
  
    AST_ReadDecimal nameA -> translateNode nameA >>= \case
      Some SStr nameT -> return $ Some SDecimal $ ReadDecimal nameT
      _ -> unexpectedNode astNode
  
    AST_ReadInteger nameA -> translateNode nameA >>= \case
      Some SStr nameT -> return $ Some SInteger $ ReadInteger nameT
      _ -> unexpectedNode astNode
  
    AST_ReadString nameA -> translateNode nameA >>= \case
      Some SStr nameT -> return $ Some SStr $ ReadString nameT
      _ -> unexpectedNode astNode
  
    AST_ReadMsg _ -> throwError' $ NoReadMsg astNode
  
    AST_PactId -> pure $ Some SStr PactId
  
    AST_ChainData node -> translateType node >>= \case
      EType objTy@(SObject _schema) -> pure $ Some objTy $ ChainData objTy
      _ -> unexpectedNode astNode
  
    AST_KeysetRefGuard strA -> translateNode strA >>= \case
      Some SStr strT -> pure $ Some SGuard $ MkKsRefGuard strT
      _ -> unexpectedNode astNode
  
    AST_CreatePactGuard strA -> translateNode strA >>= \case
      Some SStr strT -> pure $ Some SGuard $ MkPactGuard strT
      _ -> unexpectedNode astNode
  
    AST_CreateUserGuard (AST_InlinedApp modName funName _ bindings appBodyA) -> do
      guard <- genGuard
      body <- withTranslatedBindings bindings $ \bindingTs ->
        withNewScope (FunctionScope modName funName) bindingTs $
          translateBody appBodyA
      pure $ Some SGuard $ MkUserGuard guard body
  
    AST_CreateModuleGuard strA -> translateNode strA >>= \case
      Some SStr strT -> pure $ Some SGuard $ MkModuleGuard strT
      _ -> unexpectedNode astNode
  
    AST_CreateCapabilityGuard (AST_InlinedApp modName funName _ bindings _) ->
      withTranslatedBindings bindings $ \bindingTs -> do
        (cap,vars) <- translateCapRef modName funName bindingTs
        pure $ Some SGuard $ MkCapabilityGuard cap vars False
  
    AST_CreateCapabilityPactGuard (AST_InlinedApp modName funName _ bindings _) ->
      withTranslatedBindings bindings $ \bindingTs -> do
        (cap,vars) <- translateCapRef modName funName bindingTs
        pure $ Some SGuard $ MkCapabilityGuard cap vars True
  
    AST_Enforce _ cond -> translateNode cond >>= \case
      Some SBool condTerm -> do
        tid <- tagAssert $ cond ^. aNode
        pure $ Some SBool $ Enforce (Just tid) condTerm
      _ -> unexpectedNode astNode
  
    AST_EnforceGuard_Str strA -> translateNamedGuard strA
  
    AST_EnforceGuard_Guard guardA -> translateGuard guardA
  
    AST_EnforceKeyset_Str strA -> translateNamedGuard strA
  
    AST_EnforceKeyset_Guard guardA -> translateGuard guardA
  
    AST_EnforceOne node [] -> do
      -- we just emit an event equivalent to one for `(enforce false)` in this
      -- case:
      tid <- tagAssert node
      return $ Some SBool $ EnforceOne $ Left tid
  
    AST_EnforceOne _ casesA@(_:_) -> do
      let n = length casesA -- invariant: n > 0
          genPath = Path <$> genTagId
      preEnforcePath <- use tsCurrentPath
      -- Generate failure and success paths for each case. We generate and tag
      -- the final failure path, but don't include it in the graph.
      pathPairs <- replicateM n ((,) <$> genPath <*> genPath)
  
      let (failurePaths, successPaths) = unzip pathPairs
          -- we don't start a new path for the first case -- we *always* run it:
          newPaths :: [Maybe Path]
          newPaths = Nothing : fmap Just (take (pred n) failurePaths)
  
          recovs :: [Recoverability]
          recovs = (Recoverable <$> take (pred n) failurePaths)
                ++ [Unrecoverable]
  
      (terms, vertices) <- fmap unzip $
        for (zip3 casesA newPaths recovs) $ \(caseA, mNewPath, recov) -> do
          maybe (pure ()) startSubpath mNewPath
          withNestedRecoverability recov (translateNode caseA) >>= \case
            Some SBool caseT -> do
              postVertex <- extendPath
              pure (caseT, postVertex)
            _ -> unexpectedNode astNode
  
      joinPaths $ zip vertices successPaths
      tsCurrentPath .= preEnforcePath
      return $ Some SBool $ EnforceOne $ Right $ zip pathPairs terms
  
    AST_Days days -> do
      Some daysTy days' <- translateNode days
      case daysTy of
        SInteger -> pure $ Some SInteger $ inject $ IntArithOp Mul (60 * 60 * 24) days'
        SDecimal -> pure $ Some SDecimal $ inject $ DecArithOp Mul (60 * 60 * 24) days'
        _        -> throwError' $ BadTimeType astNode
  
    AST_Hours hours -> do
      Some hoursTy hours' <- translateNode hours
      case hoursTy of
        SInteger -> pure $ Some SInteger $ inject $ IntArithOp Mul (60 * 60) hours'
        SDecimal -> pure $ Some SDecimal $ inject $ DecArithOp Mul (60 * 60) hours'
        _        -> throwError' $ BadTimeType astNode
  
    AST_Minutes minutes -> do
      Some minutesTy minutes' <- translateNode minutes
      case minutesTy of
        SInteger -> pure $ Some SInteger $ inject $ IntArithOp Mul 60 minutes'
        SDecimal -> pure $ Some SDecimal $ inject $ DecArithOp Mul 60 minutes'
        _        -> throwError' $ BadTimeType astNode
  
    AST_NFun _node "time" [AST_Lit (LString timeLit)]
      | Just timeLit'
        <- parseTime Pact.simpleISO8601 (T.unpack timeLit)
      -> pure $ Some STime $ Lit' $ fromPact timeIso timeLit'
  
    AST_NFun_Basic SModulus [a, b] -> translateNode a >>= \case
      Some SInteger a' -> translateNode b >>= \case
        Some SInteger b' -> pure (Some SInteger (inject $ ModOp a' b'))
        _ -> unexpectedNode astNode
      _ -> unexpectedNode astNode
  
    AST_NFun_Basic fn@(toOp comparisonOpP -> Just op) args@[a, b] -> do
      aT <- translateNode a
      bT <- translateNode b
      case (aT, bT) of
  
        (Some (SList SAny) EmptyList, Some (SList ty) lst) -> do
          op' <- toOp eqNeqP fn ?? MalformedComparison fn args
          pure $ Some SBool $ CoreTerm $ ListEqNeq ty op' EmptyList lst
  
        (Some (SList ty) lst, Some (SList SAny) EmptyList) -> do
          op' <- toOp eqNeqP fn ?? MalformedComparison fn args
          pure $ Some SBool $ CoreTerm $ ListEqNeq ty op' lst EmptyList
  
        (Some (SList ta) a', Some (SList tb) b') -> do
          Refl <- singEq ta tb ?? TypeMismatch (EType ta) (EType tb)
          op'  <- toOp eqNeqP fn ?? MalformedComparison fn args
          pure $ Some SBool $ inject $ ListEqNeq ta op' a' b'
  
        (Some ta@SObjectUnsafe{} a', Some tb@SObjectUnsafe{} b') -> do
          op' <- toOp eqNeqP fn ?? MalformedComparison fn args
          pure $ Some SBool $ inject $ ObjectEqNeq ta tb op' a' b'
  
        (Some ta a', Some tb b') -> do
          Refl <- singEq ta tb ?? TypeMismatch (EType ta) (EType tb)
          pure $ Some SBool $ inject $ Comparison ta op a' b'
  
    AST_NFun_Basic fn@(toOp comparisonOpP -> Just _) args
      -> throwError' $ MalformedComparison fn args
  
    -- logical: not, and, or
  
    AST_NFun_Basic SLogicalNegation [a] -> translateNode a >>= \case
      Some SBool a' -> pure $ Some SBool $ inject $ Logical NotOp [a']
      _ -> unexpectedNode astNode
  
    AST_NFun_Basic fn args@[a, b]
      | fn == SLogicalConjunction || fn == SLogicalDisjunction -> do
        Some tyA a' <- translateNode a
        Some tyB b' <- translateNode b
        case (tyA, tyB) of
          (SBool, SBool) -> case fn of
            SLogicalConjunction -> pure $
              Some SBool $ inject $ Logical AndOp [a', b']
            SLogicalDisjunction -> pure $
              Some SBool $ inject $ Logical OrOp [a', b']
            _ -> error "impossible"
          _ -> throwError' $ MalformedLogicalOp fn args
  
    AST_NFun_Basic fn@(toOp logicalOpP -> Just _) args
      -> throwError' $ MalformedLogicalOp fn args
  
    -- arithmetic
  
    AST_NFun_Basic fn@(toOp roundingLikeOpP -> Just op) args@[a, b] -> do
        Some tyA a' <- translateNode a
        Some tyB b' <- translateNode b
        case (tyA, tyB, op) of
          (SDecimal, SInteger, Round)   -> pure $
            Some SDecimal $ inject $ RoundingLikeOp2 op a' b'
          (SDecimal, SInteger, Ceiling) -> pure $
            Some SDecimal $ inject $ RoundingLikeOp2 op a' b'
          (SDecimal, SInteger, Floor)   -> pure $
            Some SDecimal $ inject $ RoundingLikeOp2 op a' b'
          _ -> throwError' $ MalformedArithOp fn args
  
    AST_NFun_Basic fn@(toOp roundingLikeOpP -> Just op) args@[a] -> do
        Some ty a' <- translateNode a
        case ty of
          SDecimal -> pure $ Some SInteger $ inject $ RoundingLikeOp1 op a'
          _        -> throwError' $ MalformedArithOp fn args
  
    AST_NFun_Basic fn@(toOp castingLikeOpP -> Just op) args@[a] -> do
        Some ty a' <- translateNode a
        case ty of
          SInteger -> pure $ Some SDecimal $ inject $ CastingLikeOp op a'
          _        -> throwError' $ MalformedArithOp fn args
  
    -- trap sqrt here to shim
    AST_NFun node fn@"sqrt" as@[a] -> translateNode a >>= \a' -> case a' of
      (Some SInteger _) -> shimNative' node fn [] "original value" a'
      (Some SDecimal _) -> shimNative' node fn [] "original value" a'
      _ -> throwError' $ MalformedArithOp fn as
  
  
    AST_NFun_Basic fn@(toOp unaryArithOpP -> Just op) args@[a] -> do
        Some ty a' <- translateNode a
        case ty of
          SInteger -> pure $ Some SInteger $ inject $ IntUnaryArithOp op a'
          SDecimal -> pure $ Some SDecimal $ inject $ DecUnaryArithOp op a'
          _        -> throwError' $ MalformedArithOp fn args
  
    --
    -- NOTE: We don't use a feature symbol here because + is overloaded across
    -- multiple (3) features.
    --
    AST_NFun node fn@"+" args@[a, b] -> translateType node >>= \case
      EType retTy -> do
        aT <- translateNode a
        bT <- translateNode b
        case (aT, bT) of
          (Some ty1@SObjectUnsafe{} o1, Some ty2@SObjectUnsafe{} o2) -> do
            -- Feature 3: object merge
            pure $ Some retTy $ inject $ ObjMerge ty1 ty2 o1 o2
  
          (Some (SList tyA) a', Some (SList tyB) b') -> do
            Refl <- singEq tyA tyB ?? MalformedArithOp fn args
            -- Feature 4: list concatenation
            pure $ Some (SList tyA) $ inject $ ListConcat tyA a' b'
  
          (Some tyA a', Some tyB b') ->
            case (tyA, tyB) of
              -- Feature 1: string concatenation
              (SStr, SStr)         -> pure $ Some SStr $ inject $ StrConcat a' b'
              -- Feature 2: arithmetic addition
              (SInteger, SInteger) -> pure $ Some SInteger $ inject $ IntArithOp Add a' b'
              (SDecimal, SDecimal) -> pure $ Some SDecimal $ inject $ DecArithOp Add a' b'
              (SInteger, SDecimal) -> pure $ Some SDecimal $ inject $ IntDecArithOp Add a' b'
              (SDecimal, SInteger) -> pure $ Some SDecimal $ inject $ DecIntArithOp Add a' b'
              _ -> throwError' $ MalformedArithOp fn args
  
    AST_NFun_Basic fn@(toOp arithOpP -> Just op) args@[a, b] -> do
        Some tyA a' <- translateNode a
        Some tyB b' <- translateNode b
        case (tyA, tyB) of
          (SInteger, SInteger)         -> pure $
            Some SInteger $ inject $ IntArithOp op a' b'
          (SDecimal, SDecimal) -> pure $
            Some SDecimal $ inject $ DecArithOp op a' b'
          (SInteger, SDecimal)     -> pure $
            Some SDecimal $ inject $ IntDecArithOp op a' b'
          (SDecimal, SInteger)     -> pure $
            Some SDecimal $ inject $ DecIntArithOp op a' b'
          _ -> throwError' $ MalformedArithOp fn args
  
    AST_NFun_Basic fn@(toOp arithOpP -> Just _) args
      -> throwError' $ MalformedArithOp fn args
    --
    -- NOTE: We don't use a feature symbol here because `length` is overloaded
    -- across multiple (3) features.
    --
    AST_NFun node "length" [a] -> do
      Some ty a' <- translateNode a
      case ty of
        SStr ->
          pure $ Some SInteger $ CoreTerm $ StrLength a'
        SList sty ->
          pure $ Some SInteger $ CoreTerm $ ListLength sty a'
        SObjectUnsafe _ ->
          pure $ Some SInteger $ CoreTerm $ ObjLength ty a'
        _ ->
          throwError' $ TypeError node
  
    AST_NFun node (toOp writeTypeP -> Just writeType) [ShortTableName tn, row, obj] -> translateNode row >>= \case
      Some SStr row' -> translateNode obj >>= \case
        Some objTy@(SObject schema) obj' -> do
          let tname = TableName (T.unpack tn)
          tid                              <- tagWrite writeType tname node (ESchema schema)
          pure $ Some SStr $
            Write objTy writeType tid tname row' obj'
        _ -> unexpectedNode astNode
      _ -> unexpectedNode astNode
  
    AST_If _ cond tBranch fBranch -> translateNode cond >>= \case
      Some SBool cond' -> do
        preBranchPath <- use tsCurrentPath
        postTest      <- extendPath
  
        truePath  <- startNewSubpath
        Some ta a <- translateNode tBranch
        postTrue  <- extendPath
  
        tsPathHead .= postTest -- reset to before true branch
  
        falsePath <- startNewSubpath
        Some tb b <- translateNode fBranch
        postFalse <- extendPath
  
        joinPaths [(postTrue, truePath), (postFalse, falsePath)]
        tsCurrentPath .= preBranchPath -- reset to before conditional
        Refl <- singEq ta tb ?? BranchesDifferentTypes (EType ta) (EType tb)
        pure $ Some ta $ IfThenElse ta cond' (truePath, a) (falsePath, b)
      _ -> unexpectedNode astNode
  
    AST_NFun _node SStringToInteger [s] -> translateNode s >>= \case
      Some SStr s' -> pure $ Some SInteger $ CoreTerm $ StrToInt s'
      _ -> unexpectedNode astNode
  
    AST_NFun _node SStringToInteger [b, s] -> translateNode b >>= \case
      Some SInteger b' -> translateNode s >>= \case
        Some SStr s' -> pure $ Some SInteger $ CoreTerm $ StrToIntBase b' s'
        _ -> unexpectedNode astNode
      _ -> unexpectedNode astNode
  
    AST_NFun _node "pact-version" [] -> pure $ Some SStr PactVersion
  
    AST_Select node _tn _columns _filters -> translateType node >>= \case
      EType (SList tableSchema) -> do
        let elist = Some (SList tableSchema) EmptyList
        shimNative' node "select" [] "[]" elist
      _ -> unexpectedNode astNode
  
    AST_WithRead node table key bindings schemaNode body -> translateType schemaNode >>= \case
      EType rowTy@SObject{} -> translateNode key >>= \case
        Some SStr key' -> typeOfPartialBind rowTy bindings >>= \case
          EType partialReadTy@(SObject schema) -> do
            let tname = TableName (T.unpack table)
            tid <- tagRead tname node (ESchema schema)
            let readT = Some partialReadTy $ Read rowTy partialReadTy Nothing tid tname key'
  
            withNodeContext node $
              translateObjBinding bindings partialReadTy body readT
          _ -> unexpectedNode astNode
        _ -> unexpectedNode astNode
      _ -> unexpectedNode astNode
  
    AST_WithDefaultRead node table key bindings schemaNode defaultNode body -> translateType schemaNode >>= \case
      EType rowTy@SObject{} -> translateNode key >>= \case
        Some SStr key' -> translateNode defaultNode >>= \case
          Some defTy@SObject{} def -> typeOfPartialBind rowTy bindings >>= \case
            EType subsetTy@(SObject schema) -> do
              let tname = TableName (T.unpack table)
              tid <- tagRead tname node (ESchema schema)
  
              -- Expect the bound type to equal the provided default object type
              case singEq subsetTy defTy of
                Nothing -> throwError' $
                  UnexpectedDefaultReadType (EType defTy) (EType subsetTy)
                Just Refl -> do
                  let readT = Some subsetTy $
                        Read rowTy subsetTy (Just def) tid (TableName (T.unpack table)) key'
                  withNodeContext node $ translateObjBinding bindings defTy body readT
            _ -> unexpectedNode astNode
          _ -> unexpectedNode astNode
        _ -> unexpectedNode astNode
      _ -> unexpectedNode astNode
  
    AST_Bind node objectA bindings schemaNode body -> translateType schemaNode >>= \case
      EType objTy@SObject{} -> do
          objectT <- translateNode objectA
          withNodeContext node $
            translateObjBinding bindings objTy body objectT
      _ -> unexpectedNode astNode
  
    AST_WithCapability (AST_InlinedApp modName funName _ bindings appBodyA) withBodyA -> do
      let capName = mkCapName modName funName
      appET <- translateCapabilityApp modName capName bindings appBodyA
      Some ty withBodyT <- trackCapScope capName $
        translateBody withBodyA
      pure $ Some ty $ WithCapability appET withBodyT
  
    AST_RequireCapability node (AST_InlinedApp modName funName _ bindings _) ->
      withTranslatedBindings bindings $ \bindingTs -> do
        (cap@(Capability _ capName _), vars) <- translateCapRef modName funName bindingTs
        recov <- view teRecoverability
        tid <- genTagId
        inScope <- Set.member capName <$> use tsStaticCapsInScope
        if inScope then do
          emit $ TraceRequireGrant recov capName bindingTs $ Located (nodeInfo node) tid
          pure $ Some SBool $ Enforce Nothing $ HasGrant tid cap vars
          else do
          -- we have statically proven there is no way this capability can come into scope.
          -- Weirdly, we want to warn about this instead of fail, as in many cases this is
          -- intentional (functions "protected" from direct execution by a cap).
          -- TODO consider some kind of declaration that would make this happen for all
          -- properties of a defun. Right now properties are independent so there is
          -- no way to "inform" properties of a protected function that a capability is
          -- intentionally preventing direct execution.
          addWarning' $ UnscopedCapability capName
          pure $ Some SBool $ Lit' True
  
    AST_ComposeCapability (AST_InlinedApp modName funName _ bindings appBodyA) -> do
      let capName = mkCapName modName funName
      app <- translateCapabilityApp modName (mkCapName modName funName) bindings appBodyA
      tsStaticCapsInScope %= Set.insert capName
      return app
  
    AST_DiffTime a b -> translateNode a >>= \case
      Some STime a' -> translateNode b >>= \case
        Some STime b' -> pure $ Some SDecimal $ CoreTerm $ DiffTime a' b'
        _ -> unexpectedNode astNode
      _ -> unexpectedNode astNode
  
    AST_AddTime time seconds
      | seconds ^. aNode . aTy == TyPrim Pact.TyInteger ||
        seconds ^. aNode . aTy == TyPrim Pact.TyDecimal -> translateNode time >>= \case
          Some STime time' -> do
            Some ty seconds' <- translateNode seconds
  
            case ty of
              SInteger ->
                pure $ Some STime $ CoreTerm $ IntAddTime time' seconds'
              SDecimal ->
                pure $ Some STime $ CoreTerm $ DecAddTime time' seconds'
              _ -> failing $
                "Unexpected type for seconds in add-time " ++ show ty
          _ -> unexpectedNode astNode
  
    AST_Read node table key -> translateNode key >>= \case
      Some SStr key' -> translateType node >>= \case
        EType objTy@(SObject schema) -> do
          let tname = TableName (T.unpack table)
          tid <- tagRead tname node (ESchema schema)
          pure $ Some objTy $ Read objTy objTy Nothing tid tname key'
        _ -> unexpectedNode astNode
      _ -> unexpectedNode astNode
  
    -- Note: this won't match if the columns are not a list literal
    AST_ReadCols node table key columns -> translateNode key >>= \case
      Some SStr key' -> translateType node >>= \case
        -- this object type contains all the fields in the schema
        EType tableObjTy@(SObject tableSchema) -> do
  
          litColumns <- for columns $ \case
            AST_Lit (LString col) -> pure $ T.unpack col
            bad                   -> throwError' $ NonStaticColumns bad
  
          let columnSet = Set.fromList litColumns
  
              -- the filtered schema contains only the columns we want
              eFilteredSchema = foldrSingList
                (ESchema (SingList SNil))
                (\k ty (ESchema (SingList subSchema)) ->
                  if symbolVal k `Set.member` columnSet
                  then ESchema $ SingList (SCons k ty subSchema)
                  else ESchema (SingList subSchema))
                tableSchema
  
          let tname = TableName (T.unpack table)
  
          case eFilteredSchema of
            ESchema filteredSchema -> do
              let filteredObjTy = mkSObject filteredSchema
              tid <- tagRead tname node (ESchema tableSchema)
              pure $ Some filteredObjTy $
                CoreTerm $ ObjTake tableObjTy
                  (CoreTerm (LiteralList SStr (CoreTerm . Lit . Str <$> litColumns)))
                  (Read tableObjTy tableObjTy Nothing tid tname key')
        _ -> unexpectedNode astNode
      _ -> unexpectedNode astNode
  
    AST_At node index obj -> do
      obj' <- translateNode obj
      translateType node >>= \case
        EType ty -> case obj' of
          Some objTy@SObjectUnsafe{} obj'' -> translateNode index >>= \case
            Some SStr colName -> pure $ Some ty $ CoreTerm $ ObjAt objTy colName obj''
            _ -> unexpectedNode astNode
          Some (SList listOfTy) list -> translateNode index >>= \case
            Some SInteger index' -> pure $ Some listOfTy $ CoreTerm $ ListAt listOfTy index' list
            _ -> unexpectedNode astNode
          _ -> throwError' $ TypeError node
  
    AST_Obj _node (Pact.ObjectMap kvs) -> do
      kvs' <- for (Map.toList kvs) $ \(Pact.FieldKey k, v) -> do
        v' <- translateNode v
        pure (k, v')
      mkLiteralObject (fmap throwError' . SortLiteralObjError) kvs' >>= \case
        Some objTy'@SObject{} litObj -> pure $ Some objTy' $ CoreTerm litObj
        _ -> unexpectedNode astNode
  
    AST_NFun node "list" _ -> throwError' $ DeprecatedList node
  
    -- rs (2023-05-10): Note, we handle the empty list as a special case (see #1182)
    -- as the element type is otherwise inferred as `Any`.
    AST_List node [] -> translateType node >>= \case
      EType listTy -> case listTy of
        SList _ -> pure $ Some listTy $ CoreTerm $ Lit []
        _ -> throwError' $ TypeError node
  
    AST_List node elems -> do
      elems' <- traverse translateNode elems
      Some ty litList <- mkLiteralList elems' ?? TypeError node
      pure $ Some ty $ CoreTerm litList
  
    AST_Contains node val collection -> do
      Some needleTy needle <- translateNode val
      collection'          <- translateNode collection
      case collection' of
        Some SStr haystack -> case needleTy of
          SStr -> pure $ Some SBool $ CoreTerm $ StrContains needle haystack
          _    -> throwError' $ TypeError node
        Some (SList ty) haystack -> do
          Refl <- singEq needleTy ty ?? TypeError node
          pure $ Some SBool $ CoreTerm $ ListContains ty needle haystack
        Some objTy@SObject{} obj -> case needleTy of
          SStr -> pure $ Some SBool $ CoreTerm $ ObjContains objTy needle obj
          _    -> throwError' $ TypeError node
        Some _ _ -> throwError' $ TypeError node
  
    AST_Reverse _node list -> translateNode list >>= \case
      Some ty'@(SList elemTy) list' -> pure $ Some ty' $ CoreTerm $ ListReverse elemTy list'
      _ -> unexpectedNode astNode
  
    AST_Sort _node list -> translateNode list >>= \case
      Some ty'@(SList elemTy) list' -> pure $ Some ty' $ CoreTerm $ ListSort elemTy list'
      _ -> unexpectedNode astNode
  
    AST_Drop node numOrKeys list -> do
      elist       <- translateNode list
      translateType node >>= \case
        EType retTy -> case elist of
          Some ty'@(SList elemTy) list' -> translateNode numOrKeys >>= \case
            Some SInteger num -> pure $ Some ty' $ CoreTerm $ ListDrop elemTy num list'
            _ -> unexpectedNode astNode
          Some objTy@SObject{} obj -> case retTy of
            SObject{} -> translateNode numOrKeys >>= \case
              Some (SList SStr) keys -> pure $ Some retTy $ CoreTerm $ ObjDrop objTy keys obj
              _ -> unexpectedNode astNode
            _ -> throwError' $ TypeError node
          Some SStr str' -> translateNode numOrKeys >>= \case
            Some SInteger num -> pure $ Some SStr $ CoreTerm $ StrDrop num str'
            _ -> unexpectedNode astNode
          _ -> throwError' $ TypeError node
  
    AST_Take node numOrKeys list -> do
      elist       <- translateNode list
      translateType node >>= \case
        EType retTy -> case elist of
          Some ty'@(SList elemTy) list' -> translateNode numOrKeys >>= \case
            Some SInteger num -> pure $ Some ty' $ CoreTerm $ ListTake elemTy num list'
            _ -> unexpectedNode astNode
          Some objTy@SObject{} obj -> case retTy of
            SObject{} -> translateNode numOrKeys >>= \case
              Some (SList SStr) keys -> pure $ Some retTy $ CoreTerm $ ObjTake objTy keys obj
              _ -> unexpectedNode astNode
            _ -> unexpectedNode astNode
          Some SStr str' -> translateNode numOrKeys >>= \case
            Some SInteger num -> pure $ Some SStr $ CoreTerm $ StrTake num str'
            _ -> unexpectedNode astNode
          _ -> throwError' $ TypeError node
  
    AST_MakeList _node num a -> translateNode num >>= \case
      Some SInteger num' -> do
        Some ty       a'   <- translateNode a
        pure $ Some (SList ty) $ CoreTerm $ MakeList ty num' a'
      _ -> unexpectedNode astNode
  
    AST_NFun _node SIdentity [a] -> do
      Some tya a' <- translateNode a
      pure $ Some tya $ CoreTerm $ Identity tya a'
  
    AST_NFun _node SConstantly [ a, b ] -> do
      Some tya a' <- translateNode a
      Some tyb b' <- translateNode b
      pure $ Some tya $ CoreTerm $ Constantly tyb a' b'
  
    AST_NFun _node SCompose [ f, g, a ] -> do
      Some tya a' <- translateNode a
      avarLst     <- use tsFoundVars
      tsFoundVars .= []
  
      Some tyb f'  <- translateNode f
      (avid, _, _) <- captureFreeVar
  
      Some tyc g'  <- translateNode g
      (bvid, _, _) <- captureFreeVar
  
      -- important: we captured a, so we need to leave it free (by restoring
      -- tsFoundVars)
      tsFoundVars .= avarLst
  
      pure $ Some tyc $ CoreTerm $
        Compose tya tyb tyc a' (Open avid "a" f') (Open bvid "b" g')
  
    AST_NFun node SMap [ fun, l ] -> do
      Some bTy fun' <- translateNode fun
      captureFreeVar >>= \case
        (vid, varName, EType aType) -> translateNode l >>= \case
          Some (SList listTy) l' -> do
            Refl <- singEq listTy aType ?? TypeError node
            pure $ Some (SList bTy) $ CoreTerm $
              ListMap aType bTy (Open vid varName fun') l'
          _ -> unexpectedNode astNode
  
    AST_NFun node SFilter [ fun, l ] -> do
      translateNode fun >>= \case
        Some SBool fun' -> captureFreeVar >>= \case
          (vid, varName, EType aType) -> translateNode l >>= \case
            Some (SList listTy) l' -> do
              Refl <- singEq listTy aType ?? TypeError node
              pure $ Some (SList aType) $ CoreTerm $
                ListFilter aType (Open vid varName fun') l'
            _ -> unexpectedNode astNode
        _ -> unexpectedNode astNode
  
    AST_NFun node SFold [ fun, a, l ] -> do
      Some funTy fun' <- translateNode fun
  
      -- Note: The order of these variables is important. `a` should be the first
      -- variable we encounter when traversing `fun` (and `b` the second) because
      -- `a` is the first argument and `b` is the second.
      --
      -- TODO(joel): this doesn't seem to follow
      --
      -- `a` encountered first, `b` will be consed on top of it, resulting in the
      -- variables coming out backwards.
      liftM2 (,) captureFreeVar captureFreeVar >>= \case
        ((vidb, varNameb, EType tyb), (vida, varNamea, EType tya)) -> do
          Some aTy' a' <- translateNode a
          translateNode l >>= \case
            Some (SList listTy) l' -> do
              Refl <- singEq aTy' tya   ?? TypeError node
              Refl <- singEq aTy' funTy ?? TypeError node
              Refl <- singEq listTy tyb ?? TypeError node
              pure $ Some tya $ CoreTerm $
                ListFold tya tyb (Open vida varNamea (Open vidb varNameb fun')) a' l'
            _ -> unexpectedNode astNode
  
    AST_NFun _ name [ f, g, a ]
      | name == SAndQ || name == SOrQ -> do
      translateNode f >>= \case
        Some SBool f' -> do
          (fvid, fvarName, _) <- captureFreeVar
          translateNode g >>= \case
            Some SBool g' -> do
              (gvid, gvarName, _) <- captureFreeVar
              Some aTy' a' <- translateNode a
              pure $ Some SBool $ CoreTerm $ (if name == "and?" then AndQ else OrQ)
                aTy' (Open fvid fvarName f') (Open gvid gvarName g') a'
            _ -> unexpectedNode astNode
        _ -> unexpectedNode astNode
  
    AST_NFun _ SWhere [ field, fun, obj ] -> translateNode field >>= \case
      Some SStr field' -> do
        translateNode fun >>= \case
          Some SBool fun' -> captureFreeVar >>= \case
            (vid, varName, EType freeTy) -> translateNode obj >>= \case
              Some objTy@SObject{} obj' -> pure $ Some SBool $ CoreTerm $
                Where objTy freeTy field' (Open vid varName fun') obj'
              _ -> unexpectedNode astNode
          _ -> unexpectedNode astNode
      _ -> unexpectedNode astNode
  
    AST_NFun _ STypeof [tm] -> do
      Some ty tm' <- translateNode tm
      pure $ Some SStr $ CoreTerm $ Typeof ty tm'
  
    AST_ModRef _ refName refSpec ->
      -- modrefs are coerced to strings
      pure $ Some SStr $ CoreTerm $ Lit $ Str $ T.unpack
        (asString refName <>
         maybe "" (\ss -> "{" <> T.intercalate "," (map asString ss) <> "}") refSpec)
  
    -- NOTE: we ignore the optional target chain during analysis, for now at
    -- least.
    AST_NFun node "yield" (obj : _optionalTargetChain) -> do
      Some objTy obj' <- translateNode obj
      ety <- translateType node
      tid <- tagYield ety
      pure $ Some objTy $ Yield tid obj'
  
    -- Translate into a resume-and-bind
    AST_Resume node bindings schemaNode body -> translateType schemaNode >>= \case
      EType objTy@SObject{} -> typeOfPartialBind objTy bindings >>= \case
        ety@(EType partialReadTy@SObject{}) -> do
          tid <- tagResume ety
          withNodeContext node $ translateObjBinding bindings partialReadTy body $
            Some partialReadTy $ Resume tid
        _ -> unexpectedNode astNode
      _ -> unexpectedNode astNode
  
    AST_NFun node fn@"keys" [_a] -> do
      -- don't translate table arg, bad things happen
      shimNative astNode node fn []
  
    AST_NFun _node (toOp bitwiseOpP -> Just op) args -> do
      args' <- for args $ \arg -> translateNode arg >>= \case
        Some SInteger arg' -> pure arg'
        _ -> unexpectedNode astNode
      pure $ Some SInteger $ inject @(Numerical Term) $
        BitwiseOp op args'
  
    AST_Continue _node body -> do
      translateNode body
      -- translate and move on from nested defpact
      -- shimNative astNode node "continue" []
  
    AST_NFun node fn@"install-capability" [_] -> do
      -- current system does not grok managed caps yet, so
      -- not translating argument
      shimNative astNode node fn []
  
    AST_EmitEvent _node (AST_InlinedApp modName funName _ bindings _) ->
      withTranslatedBindings bindings $ \bindingTs -> do
        (Capability _ capName evOrMgt, _) <- translateCapRef modName funName bindingTs
        case evOrMgt of
          Nothing -> throwError' (CapabilityNotManagedOrEvent capName)
          -- RS: If a cap is managed or an event, we always succeed (by emitting `true`).
          Just _ -> pure (Some SBool $ Lit' True)
  
    AST_NFun _ "distinct" [xs] -> translateNode xs >>= \xs' -> case xs' of
      Some ty@(SList elemTy) l -> pure $ Some ty $ CoreTerm $ ListDistinct elemTy l
      _ -> unexpectedNode astNode
  
    AST_NFun _node _fn@"enumerate" args -> do
      args' <- for args $ \arg -> translateNode arg >>= \case
        Some SInteger i' -> pure i'
        _otherwise -> unexpectedNode astNode
      case args' of
        [from, to']       -> pure $ Some (SList SInteger) $ CoreTerm $ Enumerate from to' (Lit' 1)
        [from, to', step] -> pure $ Some (SList SInteger) $ CoreTerm $ Enumerate from to' step
        _otherwise -> unexpectedNode astNode
  
    AST_NFun node fn@"format" [a, b] -> translateNode a >>= \a' -> case a' of
      -- uncaught case is dynamic list, sub format string
      Some SStr _ -> shimNative' node fn [b] "format string" a'
      _ -> unexpectedNode astNode
  
    AST_CreatePrincipal guard -> translateNode guard >>= \case
      Some SGuard g -> pure (Some SStr (CreatePrincipal g))
      _ -> unexpectedNode astNode
  
    AST_ValidatePrincipal guard name -> translateNode guard >>= \case
      Some SGuard g -> translateNode name >>= \case
        Some SStr s -> pure $ Some SBool (ValidatePrincipal g s)
        _ -> unexpectedNode astNode
      _ -> unexpectedNode astNode
  
    AST_NFun _ "is-principal" [a] -> translateNode a >>= \xs' -> case xs' of
      Some SStr l -> pure $ Some SBool $ CoreTerm $ IsPrincipal l
      _otherwise -> unexpectedNode astNode
  
    AST_NFun _ "typeof-principal" [a] -> translateNode a >>= \xs' -> case xs' of
      Some SStr l -> pure $ Some SStr $ CoreTerm $ TypeOfPrincipal l
      _otherwise -> unexpectedNode astNode
  
    AST_NFun _ fn@"describe-namespace" _ ->
      throwError' (InvalidNativeInModule fn)
  
    AST_NFun node fn as -> shimNative astNode node fn as
  
    _ -> unexpectedNode astNode
  
  
  unexpectedNode :: AST Node -> TranslateM a
  unexpectedNode astNode =
    throwError' $ UnexpectedNode astNode
  
  shimNative :: AST Node -> Node -> Text -> [AST Node] -> TranslateM ETerm
  shimNative ast node fn args = do
    (r,m) <- case _aTy node of
      Pact.TyPrim p -> case p of
        Pact.TyInteger -> pure (Some SInteger $ Lit' 0, "0")
        Pact.TyDecimal -> pure (Some SDecimal $ Lit' 0.0, "0.0")
        Pact.TyBool -> pure (Some SBool $ Lit' True, "True")
        Pact.TyString -> pure (Some SStr $ Lit' "", "empty string")
        Pact.TyTime -> pure (Some STime $ Lit' 0, "epoch time")
        Pact.TyGuard {} -> unexpectedNode ast
      Pact.TyList lty -> pure $ (`fmap` slist lty) $ \case
        Nothing -> "empty list"
        Just t -> "empty " <> t <> " list"
      _ -> unexpectedNode ast
    shimNative' node fn args m r
    where
      slist lty = case lty of
        Pact.TyPrim p -> case p of
          Pact.TyInteger -> (Some (SList SInteger) EmptyList,Just "integer")
          Pact.TyDecimal -> (Some (SList SDecimal) EmptyList,Just "decimal")
          Pact.TyBool -> (Some (SList SBool) EmptyList,Just "bool")
          Pact.TyString -> (Some (SList SStr) EmptyList,Just "string")
          Pact.TyTime -> (Some (SList STime) EmptyList,Just "time")
          Pact.TyGuard {} -> (Some (SList SGuard) EmptyList,Just "guard")
        _ -> (Some (SList SAny) EmptyList,Nothing)
  
  shimNative' :: Node -> Text -> [AST Node] -> Text -> ETerm -> TranslateM ETerm
  shimNative' node fn args m r = do
    mapM_ translateNode args
    addWarning node $ UnsupportedNonFatal $
      (fn <> ": substituting " <> m)
    pure r
  
  
  -- | Accumulate a non-fatal translation issue
  addWarning :: P.HasInfo i => i -> TranslateFailureNoLoc -> TranslateM ()
  addWarning n w = tsWarnings %= (TranslateFailure (P.getInfo n) w:)
  
  -- | Accumulate a non-fatal translation issue warning on top-level node
  addWarning' :: TranslateFailureNoLoc -> TranslateM ()
  addWarning' w = view teInfo >>= \i -> addWarning i w
  
  -- | Implements cap scoping, which can accumulate further caps
  -- via compose-capability. Reverts state after running action.
  trackCapScope :: CapName -> TranslateM r -> TranslateM r
  trackCapScope capName act = do
    current <- use tsStaticCapsInScope
    tsStaticCapsInScope %= Set.insert capName
    r <- act
    tsStaticCapsInScope .= current
    return r
  
  captureFreeVar :: TranslateM (VarId, Text, EType)
  captureFreeVar = do
    vs <- use tsFoundVars
    case vs of
      v:vs' -> do
        tsFoundVars .= vs'
        pure v
      _ -> throwError' $ FreeVarInvariantViolation "expected var"
  
  expectNoFreeVars :: TranslateM ()
  expectNoFreeVars = do
    vars <- use tsFoundVars
    case vars of
      [] -> pure ()
      _  -> throwError' $ FreeVarInvariantViolation
        "invariant violation: free variable unexpectedly found"
  
  mkExecutionGraph :: Vertex -> Path -> TranslateState -> ExecutionGraph
  mkExecutionGraph vertex0 rootPath st = ExecutionGraph
      vertex0
      rootPath
      (_tsGraph st)
      (_tsEdgeEvents st)
      (_tsPathEdges st)
  
  runTranslation
    :: Pact.ModuleName
    -> Text
    -> Info
    -> [Capability]
    -> [Named Node]
    -> [AST Node]
    -> CheckableType
    -> Except TranslateFailure ([Arg], [VarId], ETerm, ExecutionGraph, [TranslateFailure])
  runTranslation modName funName info caps pactArgs body checkType = do
      (args, translationVid)     <- runArgsTranslation
      (tm, (stepChoices, graph, warnings)) <- runBodyTranslation args translationVid
      pure (args, stepChoices, tm, graph, warnings)
  
    where
      runArgsTranslation :: Except TranslateFailure ([Arg], VarId)
      runArgsTranslation = runStateT
        (runReaderT (traverse translateArg pactArgs) info)
        (VarId 1)
  
      argToBinding :: Arg -> Located Binding
      argToBinding (Arg unmunged vid node ety) =
        Located (node ^. aId . Pact.tiInfo) $
          Binding vid unmunged (node ^. aId.tiName.to Munged) ety
  
      runBodyTranslation
        :: [Arg]
        -> VarId
        -> Except TranslateFailure (ETerm, ([VarId], ExecutionGraph, [TranslateFailure]))
      runBodyTranslation args nextVarId =
        let vertex0    = 0
            nextVertex = succ vertex0
            path0      = Path 0
            nextTagId  = succ $ _pathTag path0
            nextGuard  = Guard 0
            graph0     = pure vertex0
            state0     = TranslateState nextTagId nextVarId nextGuard graph0
              vertex0 nextVertex Map.empty mempty path0 Map.empty [] [] [] mempty
            translation = do
              -- For our toplevel 'FunctionScope', we reuse variables we've
              -- already generated during argument translation:
              let bindingTs = fmap argToBinding args
  
              res <- case checkType of
                CheckDefun ->
                  withNewScope (FunctionScope modName funName) bindingTs $
                    translateBody body
                CheckDefpact ->
                  withNewScope (PactScope modName funName) bindingTs $
                    Some SStr . Pact <$> translatePact body
                CheckPactStep ->
                  withNewStep StepScope bindingTs $
                    translateBody body
                CheckDefconst
                  -> error "invariant violation: this cannot be a constant"
              _ <- extendPath -- form final edge for any remaining events
              expectNoFreeVars
              pure res
  
            handleState translateState =
              ( _tsStepChoices translateState
              , mkExecutionGraph vertex0 path0 translateState
              , _tsWarnings translateState
              )
        in fmap (fmap handleState) $ flip runStateT state0 $
             runReaderT (unTranslateM translation) (mkTranslateEnv info caps args)
  
  -- | Translate a node ignoring the execution graph. This is useful in cases
  -- where we don't show an execution trace. Those two places (currently) are:
  -- * Translating `defconst`s for use in properties. This is for use only in
  -- properties, as opposed to in execution.
  -- * Translating terms for property testing. Here we don't show a trace -- we
  -- just test that pact and analysis come to the same result.
  --
  -- TODO: is it possible for certain effects to work in `defconst` that we're
  --       not permitting here? e.g. in the pact repl, it seems that at least
  --       `read-keyset` works.
  --
  translateNodeNoGraph :: AST Node -> Except TranslateFailure ETerm
  translateNodeNoGraph node =
    let vertex0        = 0
        nextVertex     = succ vertex0
        path0          = Path 0
        nextTagId      = succ $ _pathTag path0
        nextGuard      = Guard 0
        graph0         = pure vertex0
        translateState = TranslateState nextTagId 0 nextGuard graph0 vertex0
          nextVertex Map.empty mempty path0 Map.empty [] [] [] mempty
  
        translateEnv = TranslateEnv dummyInfo Map.empty Map.empty mempty 0
          (pure 0) (pure 0)
  
    in (`evalStateT` translateState) $
         (`runReaderT` translateEnv) $
           unTranslateM $ translateNode node
  
  -- | Throw a translation failure when Nothing
  (??)
    :: (MonadError TranslateFailure m, MonadReader r m, HasInfo r)
    => Maybe a -> TranslateFailureNoLoc -> m a
  Just a  ?? _   = pure a
  Nothing ?? err = throwError' err
  infix 0 ??
  