tricu/src/Check/Core.hs

module Check.Core
  ( ImportedView(..)
  , importedViewsFromResolvedModules
  , importedViewsFromResolvedModulesEither
  , checkProgramWithEnvAndImportedViews
  , checkSourceWithEnv
  , checkSourceWithEnvAndImportedViews
  , lowerSource
  , lowerSourceWithDebug
  , lowerSourceWithImportedViews
  , lowerSourceWithImportedViewsDebug
  , lowerViewExpr
  ) where

import Control.Applicative ((<|>))
import Control.Monad.State.Strict
import Data.Char (isDigit)
import Data.Maybe (mapMaybe)
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.Text as T

import ContentStore.Alias (ObjectRef(..))
import Eval (evalTricu, result)
import Module.Resolver
  ( ResolvedExport(..)
  , ResolvedModule(..)
  )
import Parser (parseTricu)
import Research

data ImportedView = ImportedView
  { importedViewName       :: String
  , importedViewType       :: ViewType
  , importedViewProvenance :: ViewProvenance
  } deriving (Show, Eq)

-- Convert module-resolution metadata into checker evidence inputs. The loader
-- decodes a portable view artifact into a syntactic ViewType, but this function
-- does not judge compatibility or policy. It only says: this resolved imported
-- name has an advertised view fact that should be emitted into the typed program.
importedViewsFromResolvedModules :: (ObjectRef -> IO (Maybe ViewType)) -> [ResolvedModule] -> IO [ImportedView]
importedViewsFromResolvedModules loadView = importedViewsFromResolvedModulesEither loadViewEither
  where
    loadViewEither ref = do
      mView <- loadView ref
      pure $ maybe (Left "artifact not found or could not be decoded") Right mView

importedViewsFromResolvedModulesEither :: (ObjectRef -> IO (Either String ViewType)) -> [ResolvedModule] -> IO [ImportedView]
importedViewsFromResolvedModulesEither loadView modules = concat <$> mapM fromModule modules
  where
    fromModule m = concat <$> mapM fromExport (resolvedModuleExports m)

    fromExport ex = case resolvedExportView ex of
      Nothing -> pure []
      Just ref -> do
        eView <- loadView ref
        case eView of
          Left err -> errorWithoutStackTrace $
            "View Contract artifact invalid for imported export "
            ++ show (resolvedExportLocalName ex)
            ++ " (kind " ++ showRefKind ref ++ ", hash " ++ showRefHash ref ++ "): "
            ++ err
          Right view -> pure [ImportedView (resolvedExportLocalName ex) view (maybe ViewUnchecked id (resolvedExportProvenance ex))]

    showRefKind = T.unpack . objectRefKind
    showRefHash = T.unpack . objectRefHash

checkSourceWithEnv :: Env -> String -> IO String
checkSourceWithEnv checkerEnv = checkSourceWithEnvAndImportedViews checkerEnv []

checkSourceWithEnvAndImportedViews :: Env -> [ImportedView] -> String -> IO String
checkSourceWithEnvAndImportedViews checkerEnv imports source =
  checkProgramWithEnvAndImportedViews checkerEnv imports (parseTricu source)

checkProgramWithEnvAndImportedViews :: Env -> [ImportedView] -> [TricuAST] -> IO String
checkProgramWithEnvAndImportedViews checkerEnv imports asts = do
  case lowerProgramWithImportedViewsDebugInEnv checkerEnv imports asts of
    Left err -> pure err
    Right (typedProgramSource, debugNames) -> do
      let input =
            "matchResult " ++
            "(diag env : renderDiagnostic diag) " ++
            "(exec env : matchResult (runtimeDiag runtimeEnv : renderDiagnostic runtimeDiag) (_ runtimeEnv : \"ok\") (runChecked exec)) " ++
            "(checkTypedProgramWith policyStrict " ++ parens typedProgramSource ++ ")"
      let env = evalTricu checkerEnv (parseTricu input)
      pure $ case toString (result env) of
        Right s -> annotateDiagnostic debugNames s
        Left _  -> formatT Decode (result env)

-- Debug names are a frontend-only side table. The portable checker renders
-- canonical numeric-symbol diagnostics; the CLI annotates that presentation
-- afterward without feeding labels back into checker semantics.
annotateDiagnostic :: Map.Map Integer String -> String -> String
annotateDiagnostic debugNames message =
  case words message of
    ("symbol" : symText : rest)
      | all isDigit symText
      , Just label <- Map.lookup (read symText) debugNames ->
          "symbol " ++ symText ++ " (" ++ label ++ ") " ++ unwords rest
    _ -> message

viewExprHasParametricBinder :: ViewExpr -> Bool
viewExprHasParametricBinder expr = case expr of
  VEVar _ -> True
  VEVarId _ -> True
  VEList items -> any viewExprHasParametricBinder items
  VEApp fn arg -> viewExprHasParametricBinder fn || viewExprHasParametricBinder arg
  VEForall binders body -> not (null binders) || viewExprHasParametricBinder body
  VEExists binders body -> not (null binders) || viewExprHasParametricBinder body
  VEName _ -> False
  VEInt _ -> False
  VEString _ -> False
  VERaw _ -> False

rawTaintedDefinitions :: Set.Set String -> [TricuAST] -> Map.Map String String
rawTaintedDefinitions allowedExternalFacts asts = fixedPoint initiallyRaw
  where
    allowedFacts = allowedExternalFacts
    definitions = Map.fromList
      [ (name, (args, body))
      | ast <- asts
      , Just (name, args, body) <- [definitionBody ast]
      ]
    localNames = Map.keysSet definitions
    initiallyRaw = Map.mapMaybeWithKey
      (\name (args, body) ->
        if name `Set.member` allowedFacts
          then Nothing
          else definitionUnsafeBaseReason localNames allowedFacts (Set.fromList args) body)
      definitions

    fixedPoint tainted =
      let tainted' = Map.mapMaybeWithKey (transitiveReason tainted) definitions
          combined = Map.union tainted tainted'
      in if combined == tainted then tainted else fixedPoint combined

    transitiveReason tainted name (args, body)
      | name `Map.member` tainted = Nothing
      | name `Set.member` allowedFacts = Nothing
      | otherwise = case filter (`Map.member` tainted) (astFreeRefs (foldr Set.delete localNames args) body) of
          helper : _ -> Just $ "depends on raw-tainted local helper " ++ show helper ++ " (" ++ tainted Map.! helper ++ ")"
          [] -> Nothing

    definitionBody ast = case ast of
      SDef name args body -> Just (name, args, body)
      SDefAnn name args _ body -> Just (name, defArgNames args, body)
      _ -> Nothing

definitionUnsafeBaseReason :: Set.Set String -> Set.Set String -> Set.Set String -> TricuAST -> Maybe String
definitionUnsafeBaseReason localNames allowedExternalFacts bound ast = case ast of
  SVar name _
    | name `Set.member` bound -> Nothing
    | name `Set.member` localNames -> Nothing
    | name `Set.member` allowedExternalFacts -> Nothing
    | name == "triage" -> Just "uses raw triage directly"
    | otherwise -> Just $ "depends on unchecked or unknown external name " ++ show name
  SInt _ -> Nothing
  SStr _ -> Nothing
  SList items -> firstJust (map (definitionUnsafeBaseReason localNames allowedExternalFacts bound) items)
  SDef _ args body -> definitionUnsafeBaseReason localNames allowedExternalFacts (foldr Set.insert bound args) body
  SDefAnn _ args _ body -> definitionUnsafeBaseReason localNames allowedExternalFacts (foldr Set.insert bound (defArgNames args)) body
  SApp fn arg -> definitionUnsafeBaseReason localNames allowedExternalFacts bound fn <|> definitionUnsafeBaseReason localNames allowedExternalFacts bound arg
  TLeaf -> Just "uses raw t directly"
  TStem _ -> Just "uses raw t directly"
  TFork _ _ -> Just "uses raw t directly"
  SLambda args body -> definitionUnsafeBaseReason localNames allowedExternalFacts (foldr Set.insert bound args) body
  SEmpty -> Nothing
  SImport _ _ -> Nothing

firstJust :: [Maybe a] -> Maybe a
firstJust [] = Nothing
firstJust (Just x : _) = Just x
firstJust (Nothing : xs) = firstJust xs

astFreeRefs :: Set.Set String -> TricuAST -> [String]
astFreeRefs candidates ast = case ast of
  SVar name _ | name `Set.member` candidates -> [name]
  SVar _ _ -> []
  SInt _ -> []
  SStr _ -> []
  SList items -> concatMap (astFreeRefs candidates) items
  SDef _ args body -> astFreeRefs (foldr Set.delete candidates args) body
  SDefAnn _ args _ body -> astFreeRefs (foldr Set.delete candidates (defArgNames args)) body
  SApp fn arg -> astFreeRefs candidates fn ++ astFreeRefs candidates arg
  TLeaf -> []
  TStem inner -> astFreeRefs candidates inner
  TFork left right -> astFreeRefs candidates left ++ astFreeRefs candidates right
  SLambda args body -> astFreeRefs (foldr Set.delete candidates args) body
  SEmpty -> []
  SImport _ _ -> []

defArgNames :: [DefArg] -> [String]
defArgNames = mapMaybe defArgName
  where
    defArgName (DefBinder name _) = Just name
    defArgName (DefPhantom _) = Nothing

lowerSource :: String -> Either String String
lowerSource = lowerProgram . parseTricu

lowerSourceWithDebug :: String -> Either String (String, Map.Map Integer String)
lowerSourceWithDebug = lowerProgramWithDebug . parseTricu

lowerSourceWithImportedViews :: [ImportedView] -> String -> Either String String
lowerSourceWithImportedViews imports = lowerProgramWithImportedViews imports . parseTricu

lowerSourceWithImportedViewsDebug :: [ImportedView] -> String -> Either String (String, Map.Map Integer String)
lowerSourceWithImportedViewsDebug imports = lowerProgramWithImportedViewsDebug imports . parseTricu

-- Symbol allocation is intentionally deterministic so emitted view-tree
-- nodes are stable and lower-only tests can inspect them directly:
--
-- * top-level definitions receive symbols 0..n-1 in source order;
-- * local binders, literals, application results, and synthetic typed nodes
--   are allocated monotonically from nextSym;
-- * external names are allocated on first reference and then reused.
--
-- Symbols are view-tree node identifiers only. Checker semantics remain in
-- lib/view.tri; the frontend only emits typed/checkable structure about these
-- symbols.
data LowerState = LowerState
  { nextSym :: Integer
  , topSyms :: Map.Map String Integer
  , scopes :: [Map.Map String Integer]
  , externSyms :: Map.Map String Integer
  , knownNodeViews :: Map.Map Integer ViewExpr
  , nodePayloads :: Map.Map Integer T
  , debugNames :: Map.Map Integer String
  , rawTaintedDefs :: Map.Map String String
  }

type LowerM a = StateT LowerState (Either String) a

lowerProgram :: [TricuAST] -> Either String String
lowerProgram asts = fst <$> lowerProgramWithDebug asts

lowerProgramWithDebug :: [TricuAST] -> Either String (String, Map.Map Integer String)
lowerProgramWithDebug = lowerProgramWithImportedViewsDebug []

lowerProgramWithImportedViews :: [ImportedView] -> [TricuAST] -> Either String String
lowerProgramWithImportedViews imports asts = fst <$> lowerProgramWithImportedViewsDebug imports asts

lowerProgramWithImportedViewsDebug :: [ImportedView] -> [TricuAST] -> Either String (String, Map.Map Integer String)
lowerProgramWithImportedViewsDebug = lowerProgramWithImportedViewsDebugInEnv Map.empty

lowerProgramWithImportedViewsDebugInEnv :: Env -> [ImportedView] -> [TricuAST] -> Either String (String, Map.Map Integer String)
lowerProgramWithImportedViewsDebugInEnv checkerEnvForLowering imports asts = do
  let definitions = [ def | def <- asts, isDefinition def ]
      topNames = map definitionName definitions
      tops = Map.fromList (zip topNames [0..])
      topCount = Map.size tops
      importCandidates = Set.fromList (map importedViewName imports) `Set.difference` Set.fromList topNames
      usedImportNames = Set.fromList (concatMap (astFreeRefs importCandidates) asts)
      activeImports = filter (\imported -> importedViewName imported `Set.member` usedImportNames) imports
      importedSyms = Map.fromList
        [ (importedViewName imported, fromIntegral (topCount + idx))
        | (idx, imported) <- zip [0..] activeImports
        ]
      topDebug = Map.fromList [ (sym, name) | (name, sym) <- Map.toList tops ]
      importDebug = Map.fromList
        [ (sym, "imported " ++ name)
        | (name, sym) <- Map.toList importedSyms
        ]
      localFactByName = Map.fromList [(importedViewName imported, imported) | imported <- imports, importedViewName imported `elem` topNames]
      trustedLocalFacts =
        [ (sym, viewTypeToExpr (importedViewType imported), importedViewProvenance imported)
        | (name, sym) <- Map.toList tops
        , Just imported <- [Map.lookup name localFactByName]
        , importedViewProvenance imported `elem` [ViewChecked, ViewTrusted]
        ]
      trustedLocalKnown = Map.fromList [(sym, view) | (sym, view, _) <- trustedLocalFacts]
      importKnown = Map.fromList
        [ (sym, viewTypeToExpr (importedViewType imported))
        | imported <- activeImports
        , Just sym <- [Map.lookup (importedViewName imported) importedSyms]
        ]
      payloads = Map.fromList $
        [ (sym, term)
        | (name, sym) <- Map.toList tops
        , Just term <- [Map.lookup name checkerEnvForLowering]
        ] ++
        [ (sym, term)
        | (name, sym) <- Map.toList importedSyms
        , Just term <- [Map.lookup name checkerEnvForLowering]
        ]
      annotated = [ def | def@SDefAnn {} <- asts ]
      allowedExternalFacts = Set.fromList
        [ importedViewName imported
        | imported <- imports
        , importedViewProvenance imported `elem` [ViewChecked, ViewTrusted]
        ]
      taintedDefs = rawTaintedDefinitions allowedExternalFacts asts
      initialState = LowerState
        { nextSym = fromIntegral (Map.size tops + Map.size importedSyms)
        , topSyms = tops
        , scopes = []
        , externSyms = importedSyms
        , knownNodeViews = Map.union trustedLocalKnown importKnown
        , nodePayloads = payloads
        , debugNames = Map.union topDebug importDebug
        , rawTaintedDefs = taintedDefs
        }
  (localNodes, finalState) <- runStateT (lowerAnnotatedProgram annotated) initialState
  trustedLocalNodes <- mapM (lowerImportedView (nodePayloads finalState)) trustedLocalFacts
  importNodes <- mapM (lowerImportedView (nodePayloads finalState))
    [ (sym, viewTypeToExpr (importedViewType imported), importedViewProvenance imported)
    | imported <- activeImports
    , Just sym <- [Map.lookup (importedViewName imported) importedSyms]
    ]
  let nodes = trustedLocalNodes ++ importNodes ++ localNodes
      rootSym = if null nodes then 0 else nextSym finalState - 1
      typedProgramSource =
        "typedProgram " ++ show rootSym ++ " [" ++ unwords (map parens nodes) ++ "]"
  pure (typedProgramSource, debugNames finalState)
lowerImportedView :: Map.Map Integer T -> (Integer, ViewExpr, ViewProvenance) -> Either String String
lowerImportedView payloadsBySym (sym, view, provenance) = do
  viewExpr <- lowerViewExpr view
  let payload = maybe "t" treeSource (Map.lookup sym payloadsBySym)
  pure $ "typedValueWithProvenance " ++ show sym ++ " " ++ parens viewExpr ++ " " ++ payload ++ " " ++ viewProvenanceSource provenance

lowerAnnotatedProgram :: [TricuAST] -> LowerM [String]
lowerAnnotatedProgram defs = do
  declarations <- concat <$> mapM lowerDefinitionDeclaration defs
  flows <- concat <$> mapM lowerDefinitionFlow defs
  pure (declarations ++ flows)

lowerDefinitionDeclaration :: TricuAST -> LowerM [String]
lowerDefinitionDeclaration (SDefAnn name args ret _) = do
  let (_, _, declaredView) = canonicalDefinitionViews args ret
  tainted <- gets rawTaintedDefs
  if viewExprHasParametricBinder declaredView && name `Map.member` tainted
    then liftEither (Left $ "parametric View definition " ++ show name ++ " depends on raw intensional Tree Calculus machinery (" ++ tainted Map.! name ++ "); use a trusted eliminator boundary instead")
    else do
      sym <- symbolForTop name
      recordKnown sym declaredView
      node <- typedValueNode sym declaredView
      pure [node]
lowerDefinitionDeclaration _ = liftEither (Left "internal check error: expected annotated definition")

lowerDefinitionFlow :: TricuAST -> LowerM [String]
lowerDefinitionFlow (SDefAnn _ args ret body) = withDefinitionScope args $ do
  let (flowArgs, flowRet, _) = canonicalDefinitionViews args ret
  binderNodes <- concat <$> mapM lowerBinderDeclaration flowArgs
  let phantomViews = map lowerPhantomArgType (phantomArgs flowArgs)
  (returnArgs, returnResult) <- lowerReturnObligation flowRet
  bodyNodes <- lowerBodyWithPhantoms (phantomViews ++ returnArgs) returnResult body
  pure (binderNodes ++ bodyNodes)
lowerDefinitionFlow _ = liftEither (Left "internal check error: expected annotated definition")

viewAnyType :: ViewExpr
viewAnyType = VEName "Any"

canonicalDefinitionViews :: [DefArg] -> Maybe ViewExpr -> ([DefArg], Maybe ViewExpr, ViewExpr)
canonicalDefinitionViews args ret =
  let rawView = declaredDefinitionView args ret
      vars = Set.toList (freeViewVars rawView)
      binderIds = zip vars [0..]
      binderMap = Map.fromList binderIds
      mappedArgs = map (mapDefArgView (rewriteViewVars binderMap)) args
      mappedRet = fmap (rewriteViewVars binderMap) ret
      mappedView = declaredDefinitionView mappedArgs mappedRet
      binders = map snd binderIds
      declaredView = if null vars then mappedView else VEForall binders mappedView
  in (mappedArgs, mappedRet, declaredView)

declaredDefinitionView :: [DefArg] -> Maybe ViewExpr -> ViewExpr
declaredDefinitionView args ret =
  case map argType args of
    [] -> resultType
    views -> viewExprFn views resultType
  where
    resultType = maybe viewAnyType id ret

mapDefArgView :: (ViewExpr -> ViewExpr) -> DefArg -> DefArg
mapDefArgView f (DefBinder name mTy) = DefBinder name (fmap f mTy)
mapDefArgView f (DefPhantom ty) = DefPhantom (f ty)

argType :: DefArg -> ViewExpr
argType (DefBinder _ Nothing) = viewAnyType
argType (DefBinder _ (Just ty)) = ty
argType (DefPhantom ty) = ty

emitDeclaration :: Integer -> [String] -> String -> LowerM String
emitDeclaration sym [] retExpr = do
  payload <- payloadSourceFor sym
  pure $ "typedValue " ++ show sym ++ " " ++ parens retExpr ++ " " ++ payload
emitDeclaration sym views retExpr = do
  payload <- payloadSourceFor sym
  pure $ "typedValue " ++ show sym ++ " (viewFn [" ++ unwords (map parens views) ++ "] " ++ parens retExpr ++ ") " ++ payload

typedValueNode :: Integer -> ViewExpr -> LowerM String
typedValueNode sym view = typedValueNodeWithProvenance sym view ViewChecked

typedValueNodeWithProvenance :: Integer -> ViewExpr -> ViewProvenance -> LowerM String
typedValueNodeWithProvenance sym view provenance = do
  viewExpr <- liftEither (lowerViewExpr view)
  payload <- payloadSourceFor sym
  pure ("typedValueWithProvenance " ++ show sym ++ " " ++ parens viewExpr ++ " " ++ payload ++ " " ++ viewProvenanceSource provenance)

typedRequireNode :: Integer -> ViewExpr -> LowerM String
typedRequireNode sym view = do
  viewExpr <- liftEither (lowerViewExpr view)
  payload <- payloadSourceFor sym
  pure ("typedRequire " ++ show sym ++ " " ++ parens viewExpr ++ " " ++ payload)

viewProvenanceSource :: ViewProvenance -> String
viewProvenanceSource ViewChecked = "viewProvenanceChecked"
viewProvenanceSource ViewTrusted = "viewProvenanceTrusted"
viewProvenanceSource ViewUnchecked = "viewProvenanceUnchecked"

declareKnown :: Integer -> ViewExpr -> LowerM String
declareKnown sym view = do
  recordKnown sym view
  typedValueNode sym view

declareKnownWithPayload :: Integer -> ViewExpr -> T -> LowerM String
declareKnownWithPayload sym view payload = do
  recordPayload sym payload
  declareKnown sym view

declareKnownFresh :: ViewExpr -> LowerM (Integer, [String])
declareKnownFresh view = do
  sym <- freshSym
  node <- declareKnown sym view
  pure (sym, [node])

declareKnownFreshWithPayload :: ViewExpr -> T -> LowerM (Integer, [String])
declareKnownFreshWithPayload view payload = do
  sym <- freshSym
  node <- declareKnownWithPayload sym view payload
  pure (sym, [node])

declareAndRequireFresh :: ViewExpr -> LowerM (Integer, [String])
declareAndRequireFresh view = do
  sym <- freshSym
  declareNode <- declareKnown sym view
  requireNode <- typedRequireNode sym view
  pure (sym, [declareNode, requireNode])

declareAndRequireFreshWithPayload :: ViewExpr -> T -> LowerM (Integer, [String])
declareAndRequireFreshWithPayload view payload = do
  sym <- freshSym
  declareNode <- declareKnownWithPayload sym view payload
  requireNode <- typedRequireNode sym view
  pure (sym, [declareNode, requireNode])

lowerBinderDeclaration :: DefArg -> LowerM [String]
lowerBinderDeclaration (DefBinder name mTy) = do
  sym <- symbolForLocal name
  node <- declareKnown sym (maybe viewAnyType id mTy)
  pure [node]
lowerBinderDeclaration (DefPhantom _) = pure []

lowerBodyWithPhantoms :: [ViewExpr] -> ViewExpr -> TricuAST -> LowerM [String]
lowerBodyWithPhantoms [] _ SLambda {} = pure []
lowerBodyWithPhantoms [] expected body =
  lowerExprAgainst body expected
lowerBodyWithPhantoms phantomViews expected (SLambda params body) =
  lowerLambdaSpine phantomViews expected params body
lowerBodyWithPhantoms phantomViews expected body =
  lowerExprAgainst body (residualViewExpr phantomViews expected)

lowerLambdaSpine :: [ViewExpr] -> ViewExpr -> [String] -> TricuAST -> LowerM [String]
lowerLambdaSpine phantomViews expected [] body = lowerBodyWithPhantoms phantomViews expected body
lowerLambdaSpine [] _ _ _ = pure []
lowerLambdaSpine (view : views) expected (param : params) body =
  withLocalBinder param $ \paramSym -> do
    declareParam <- declareKnown paramSym view
    restNodes <- lowerLambdaSpine views expected params body
    pure (declareParam : restNodes)

residualViewExpr :: [ViewExpr] -> ViewExpr -> ViewExpr
residualViewExpr [] resultView = resultView
residualViewExpr args resultView = viewExprFn args resultView

phantomArgs :: [DefArg] -> [DefArg]
phantomArgs [] = []
phantomArgs (DefPhantom ty : rest) = DefPhantom ty : phantomArgs rest
phantomArgs (_ : rest) = phantomArgs rest

lowerPhantomArgType :: DefArg -> ViewExpr
lowerPhantomArgType (DefPhantom ty) = ty
lowerPhantomArgType _ = error "internal check error: expected phantom arg"

lowerReturnObligation :: Maybe ViewExpr -> LowerM ([ViewExpr], ViewExpr)
lowerReturnObligation Nothing = pure ([], viewAnyType)
lowerReturnObligation (Just ty) = pure (peelFnObligation ty)

peelFnObligation :: ViewExpr -> ([ViewExpr], ViewExpr)
peelFnObligation ty = case viewExprFnParts ty of
  Just (args, resultView) ->
    let (restArgs, finalResult) = peelFnObligation resultView
    in (args ++ restArgs, finalResult)
  Nothing -> ([], ty)

withDefinitionScope :: [DefArg] -> LowerM a -> LowerM a
withDefinitionScope args action = do
  binderEntries <- mapM allocateBinder [ name | DefBinder name _ <- args ]
  modify $ \st -> st { scopes = Map.fromList binderEntries : scopes st }
  resultValue <- action
  modify $ \st -> st { scopes = drop 1 (scopes st) }
  pure resultValue

allocateBinder :: String -> LowerM (String, Integer)
allocateBinder name = do
  sym <- freshSym
  recordDebugName sym name
  pure (name, sym)

withLocalBinder :: String -> (Integer -> LowerM a) -> LowerM a
withLocalBinder name action = do
  sym <- freshSym
  recordDebugName sym name
  withLocalAlias name sym (action sym)

withLocalAlias :: String -> Integer -> LowerM a -> LowerM a
withLocalAlias name sym action = do
  modify $ \st -> st { scopes = Map.singleton name sym : scopes st }
  resultValue <- action
  modify $ \st -> st { scopes = drop 1 (scopes st) }
  pure resultValue

recordKnown :: Integer -> ViewExpr -> LowerM ()
recordKnown sym view =
  modify $ \st -> st { knownNodeViews = Map.insert sym view (knownNodeViews st) }

recordPayload :: Integer -> T -> LowerM ()
recordPayload sym payload =
  modify $ \st -> st { nodePayloads = Map.insert sym payload (nodePayloads st) }

payloadFor :: Integer -> LowerM (Maybe T)
payloadFor sym = do
  st <- get
  pure (Map.lookup sym (nodePayloads st))

payloadSourceFor :: Integer -> LowerM String
payloadSourceFor sym = maybe "t" treeSource <$> payloadFor sym

knownNodeViewFor :: Integer -> LowerM (Maybe ViewExpr)
knownNodeViewFor sym = do
  st <- get
  pure (Map.lookup sym (knownNodeViews st))

recordDebugName :: Integer -> String -> LowerM ()
recordDebugName sym label =
  modify $ \st -> st { debugNames = Map.insertWith keepExisting sym label (debugNames st) }
  where
    keepExisting _ old = old

lowerExpr :: TricuAST -> LowerM (Integer, [String])
lowerExpr expr = do
  (sym, nodes, _) <- lowerExprKnown expr
  pure (sym, nodes)

lowerExprAgainst :: TricuAST -> ViewExpr -> LowerM [String]
lowerExprAgainst body expected = do
  (_, nodes, _) <- lowerExprKnownAgainst body expected
  pure nodes

lowerExprKnownAgainst :: TricuAST -> ViewExpr -> LowerM (Integer, [String], Maybe ViewExpr)
lowerExprKnownAgainst expr expected = case (expr, viewExprAsType expected) of
  (SApp (SApp (SVar "pair" _) left) right, Just (VTPair leftView rightView)) ->
    let leftExpr = viewTypeToExpr leftView
        rightExpr = viewTypeToExpr rightView
    in lowerUnshadowedConstructor "pair" expr expected $ do
      (_, leftNodes, _) <- lowerExprKnownAgainst left leftExpr
      (_, rightNodes, _) <- lowerExprKnownAgainst right rightExpr
      (sym, nodes) <- declareAndRequireFresh expected
      pure (sym, leftNodes ++ rightNodes ++ nodes, Just expected)
  (SApp (SVar "just" _) value, Just (VTMaybe elemView)) ->
    let elemExpr = viewTypeToExpr elemView
    in lowerUnshadowedConstructor "just" expr expected $ do
      (_, valueNodes, _) <- lowerExprKnownAgainst value elemExpr
      (sym, nodes) <- declareAndRequireFresh expected
      pure (sym, valueNodes ++ nodes, Just expected)
  (SVar "nothing" _, Just (VTMaybe _)) ->
    lowerUnshadowedConstructor "nothing" expr expected $ do
      (sym, nodes) <- declareAndRequireFresh expected
      pure (sym, nodes, Just expected)
  (SApp (SApp (SVar "ok" _) value) rest, Just (VTResult _ okView)) ->
    lowerUnshadowedConstructor "ok" expr expected $
      lowerResultConstructor expected (viewTypeToExpr okView) value rest
  (SApp (SApp (SVar "err" _) value) rest, Just (VTResult errView _)) ->
    lowerUnshadowedConstructor "err" expr expected $
      lowerResultConstructor expected (viewTypeToExpr errView) value rest
  (SApp (SLambda [name] body) value, _) -> do
    (valueSym, valueNodes, _) <- lowerExprKnown value
    bodyResult <- withLocalAlias name valueSym (lowerExprKnownAgainst body expected)
    let (bodySym, bodyNodes, bodyKnown) = bodyResult
    pure (bodySym, valueNodes ++ bodyNodes, bodyKnown)
  (SList items, Just (VTList elemView)) -> do
    let elemExpr = viewTypeToExpr elemView
    lowered <- mapM (`lowerExprKnownAgainst` elemExpr) items
    let itemNodes = concat [ nodes | (_, nodes, _) <- lowered ]
    (sym, nodes) <- declareAndRequireFresh expected
    pure (sym, itemNodes ++ nodes, Just expected)
  (SLambda _ _, _) ->
    case peelFnObligation expected of
      ([], _) -> lowerExprKnownAndRequire expr expected
      (argViews, resultView) -> lowerLambdaAgainst argViews resultView expr
  _ -> lowerExprKnownAndRequire expr expected

lowerUnshadowedConstructor :: String -> TricuAST -> ViewExpr -> LowerM (Integer, [String], Maybe ViewExpr) -> LowerM (Integer, [String], Maybe ViewExpr)
lowerUnshadowedConstructor name fallback expected lowerCtor = do
  ctorIsUnbound <- nameIsUnbound name
  if ctorIsUnbound
    then lowerCtor
    else lowerExprKnownAndRequire fallback expected

lowerResultConstructor :: ViewExpr -> ViewExpr -> TricuAST -> TricuAST -> LowerM (Integer, [String], Maybe ViewExpr)
lowerResultConstructor expected valueView value rest = do
  (_, valueNodes, _) <- lowerExprKnownAgainst value valueView
  (_, restNodes, _) <- lowerExprKnown rest
  (sym, nodes) <- declareAndRequireFresh expected
  pure (sym, valueNodes ++ restNodes ++ nodes, Just expected)

lowerExprKnownAndRequire :: TricuAST -> ViewExpr -> LowerM (Integer, [String], Maybe ViewExpr)
lowerExprKnownAndRequire body expected = do
  (bodySym, bodyNodes, known) <- lowerExprKnown body
  requireNode <- typedRequireNode bodySym expected
  pure (bodySym, bodyNodes ++ [requireNode], known)

lowerLambdaAgainst :: [ViewExpr] -> ViewExpr -> TricuAST -> LowerM (Integer, [String], Maybe ViewExpr)
lowerLambdaAgainst argViews resultView (SLambda params body) = do
  nodes <- lowerLambdaSpine argViews resultView params body
  sym <- freshSym
  let fnView = residualViewExpr argViews resultView
  declareNode <- declareKnown sym fnView
  pure (sym, nodes ++ [declareNode], Just fnView)
lowerLambdaAgainst argViews resultView body =
  lowerExprKnownAndRequire body (residualViewExpr argViews resultView)

lowerExprKnown :: TricuAST -> LowerM (Integer, [String], Maybe ViewExpr)
lowerExprKnown (SVar name _) = do
  sym <- symbolForName name
  known <- knownNodeViewFor sym
  pure (sym, [], known)
lowerExprKnown (SStr s) = do
  let view = VEName "String"
  (sym, nodes) <- declareKnownFreshWithPayload view (ofString s)
  recordDebugName sym "string literal"
  pure (sym, nodes, Just view)
lowerExprKnown (SInt n)
  | n >= 0 && n <= 255 = do
      let view = VEName "Byte"
      (sym, nodes) <- declareKnownFreshWithPayload view (ofNumber n)
      recordDebugName sym "byte literal"
      pure (sym, nodes, Just view)
  | otherwise = do
      sym <- freshSym
      pure (sym, [], Nothing)
lowerExprKnown TLeaf = do
  let view = VEName "Unit"
  (sym, nodes) <- declareKnownFreshWithPayload view Leaf
  recordDebugName sym "unit literal"
  pure (sym, nodes, Just view)
lowerExprKnown (SList items) = do
  (sym, nodes, view, _) <- lowerListLiteral items
  pure (sym, nodes, Just view)
lowerExprKnown (SApp (SLambda [name] body) value) = do
  (valueSym, valueNodes, known) <- lowerExprKnown value
  bodyResult <- withLocalAlias name valueSym (lowerExprKnown body)
  let (bodySym, bodyNodes, bodyKnown) = bodyResult
  pure (bodySym, valueNodes ++ bodyNodes, bodyKnown)
lowerExprKnown (SApp func arg) = do
  (funcSym, funcNodes, funcKnown) <- lowerExprKnown func
  (argSym, argNodes, _) <- lowerApplicationArgument funcKnown arg
  outSym <- freshSym
  recordDebugName outSym (applicationDebugLabel func)
  funcPayload <- payloadFor funcSym
  argPayload <- payloadFor argSym
  case (funcPayload, argPayload) of
    (Just f, Just a) -> recordPayload outSym (apply f a)
    _ -> pure ()
  applyPayload <- payloadSourceFor outSym
  let applyNode = "typedApply " ++ show outSym ++ " " ++ show funcSym ++ " " ++ show argSym ++ " " ++ applyPayload
      outKnown = applicationResultView funcKnown
  mapM_ (recordKnown outSym) outKnown
  pure (outSym, funcNodes ++ argNodes ++ [applyNode], outKnown)
lowerExprKnown (SLambda params body) = do
  nodes <- lowerUnannotatedLambda params body
  sym <- freshSym
  pure (sym, nodes, Nothing)
lowerExprKnown _ = do
  sym <- freshSym
  pure (sym, [], Nothing)

lowerListLiteral :: [TricuAST] -> LowerM (Integer, [String], ViewExpr, [Integer])
lowerListLiteral items = do
  lowered <- mapM lowerExprKnown items
  let itemSyms = [ itemSym | (itemSym, _, _) <- lowered ]
      itemNodes = concat [ nodes | (_, nodes, _) <- lowered ]
      view = listLiteralView [ known | (_, _, known) <- lowered ]
  itemPayloads <- mapM payloadFor itemSyms
  let mPayload = ofList <$> sequence itemPayloads
  (sym, declareNodes) <- case mPayload of
    Just payload -> declareKnownFreshWithPayload view payload
    Nothing -> declareKnownFresh view
  pure (sym, itemNodes ++ declareNodes, view, itemSyms)

lowerApplicationArgument :: Maybe ViewExpr -> TricuAST -> LowerM (Integer, [String], Maybe ViewExpr)
lowerApplicationArgument (Just fnView) arg =
  case viewExprFnParts fnView of
    Just (argView : _, _)
      | containsViewVar argView -> lowerExprKnown arg
      | otherwise -> lowerExprKnownAgainst arg argView
    _ -> lowerExprKnown arg
lowerApplicationArgument _ arg =
  lowerExprKnown arg

containsViewVar :: ViewExpr -> Bool
containsViewVar view = case view of
  VEVar _ -> True
  VEVarId _ -> True
  VEList items -> any containsViewVar items
  VEApp f a -> containsViewVar f || containsViewVar a
  VEForall _ body -> containsViewVar body
  VEExists _ body -> containsViewVar body
  _ -> False

applicationDebugLabel :: TricuAST -> String
applicationDebugLabel func =
  case applicationHeadName func of
    Just name -> name ++ " application result"
    Nothing   -> "application result"

applicationHeadName :: TricuAST -> Maybe String
applicationHeadName (SVar name _) = Just name
applicationHeadName (SApp func _) = applicationHeadName func
applicationHeadName _ = Nothing

applicationResultView :: Maybe ViewExpr -> Maybe ViewExpr
applicationResultView (Just fnView) = case viewExprFnParts fnView of
  Just (_ : restArgs, resultView) ->
    Just $ case restArgs of
      [] -> resultView
      _  -> viewExprFn restArgs resultView
  _ -> Nothing
applicationResultView _ = Nothing

listLiteralView :: [Maybe ViewExpr] -> ViewExpr
listLiteralView [] = viewExprList viewAnyType
listLiteralView (Just firstView : rest)
  | all (== Just firstView) rest = viewExprList firstView
listLiteralView _ = viewExprList viewAnyType

lowerUnannotatedLambda :: [String] -> TricuAST -> LowerM [String]
lowerUnannotatedLambda [] body = do
  (_, nodes) <- lowerExpr body
  pure nodes
lowerUnannotatedLambda (param : params) body =
  withLocalBinder param $ \paramSym -> do
    declareParam <- declareKnown paramSym viewAnyType
    restNodes <- lowerUnannotatedLambda params body
    pure (declareParam : restNodes)

symbolForTop :: String -> LowerM Integer
symbolForTop name = do
  st <- get
  case Map.lookup name (topSyms st) of
    Just sym -> pure sym
    Nothing -> liftEither (Left $ "internal check error: missing top-level symbol: " ++ name)

symbolForLocal :: String -> LowerM Integer
symbolForLocal name = do
  st <- get
  case lookupInScopes name (scopes st) of
    Just sym -> pure sym
    Nothing -> liftEither (Left $ "internal check error: missing local symbol: " ++ name)

symbolForName :: String -> LowerM Integer
symbolForName name = do
  st <- get
  case lookupInScopes name (scopes st) of
    Just sym -> pure sym
    Nothing -> case Map.lookup name (topSyms st) of
      Just sym -> pure sym
      Nothing -> symbolForExternal name

symbolForExternal :: String -> LowerM Integer
symbolForExternal name = do
  st <- get
  case Map.lookup name (externSyms st) of
    Just sym -> pure sym
    Nothing -> do
      sym <- freshSym
      recordDebugName sym ("external " ++ name)
      modify $ \st' -> st' { externSyms = Map.insert name sym (externSyms st') }
      pure sym

nameIsUnbound :: String -> LowerM Bool
nameIsUnbound name = do
  st <- get
  pure $ case lookupInScopes name (scopes st) of
    Just _ -> False
    Nothing -> Map.notMember name (topSyms st)

lookupInScopes :: String -> [Map.Map String Integer] -> Maybe Integer
lookupInScopes _ [] = Nothing
lookupInScopes name (scope : rest) =
  case Map.lookup name scope of
    Just sym -> Just sym
    Nothing -> lookupInScopes name rest

freshSym :: LowerM Integer
freshSym = do
  st <- get
  let sym = nextSym st
  put st { nextSym = sym + 1 }
  pure sym

isDefinition :: TricuAST -> Bool
isDefinition SDef {} = True
isDefinition SDefAnn {} = True
isDefinition _ = False

definitionName :: TricuAST -> String
definitionName (SDef name _ _) = name
definitionName (SDefAnn name _ _ _) = name
definitionName _ = error "definitionName: expected top-level definition"

liftEither :: Either String a -> LowerM a
liftEither value = StateT $ \st -> case value of
  Left err -> Left err
  Right resultValue -> Right (resultValue, st)

lowerArgView :: DefArg -> LowerM String
lowerArgView (DefBinder _ Nothing) = pure "viewAny"
lowerArgView (DefBinder _ (Just ty)) = liftEither (lowerViewExpr ty)
lowerArgView (DefPhantom ty) = liftEither (lowerViewExpr ty)

viewTypeToExpr :: ViewType -> ViewExpr
viewTypeToExpr view = case view of
  VTName name -> VEName name
  VTVar varId -> VEVarId varId
  VTRef n -> VEApp (VEName "Ref") (VEInt n)
  VTRefText s -> VEApp (VEName "Ref") (VEString s)
  VTList item -> VEApp (VEName "List") (viewTypeToExpr item)
  VTMaybe item -> VEApp (VEName "Maybe") (viewTypeToExpr item)
  VTPair left right -> VEApp (VEApp (VEName "Pair") (viewTypeToExpr left)) (viewTypeToExpr right)
  VTResult err ok -> VEApp (VEApp (VEName "Result") (viewTypeToExpr err)) (viewTypeToExpr ok)
  VTGuarded base guard -> VEApp (VEApp (VEName "viewGuarded") (viewTypeToExpr base)) (VERaw (treeSource guard))
  VTForall binders body -> VEForall binders (viewTypeToExpr body)
  VTExists binders body -> VEExists binders (viewTypeToExpr body)
  VTFn args resultView -> viewExprFn (map viewTypeToExpr args) (viewTypeToExpr resultView)

viewExprFn :: [ViewExpr] -> ViewExpr -> ViewExpr
viewExprFn args resultView = VEApp (VEApp (VEName "Fn") (VEList args)) resultView

viewExprList :: ViewExpr -> ViewExpr
viewExprList = VEApp (VEName "List")

viewExprFnParts :: ViewExpr -> Maybe ([ViewExpr], ViewExpr)
viewExprFnParts (VEForall _ body) = viewExprFnParts body
viewExprFnParts (VEApp (VEApp (VEName "Fn") (VEList args)) resultView) = Just (args, resultView)
viewExprFnParts _ = Nothing

viewExprAsType :: ViewExpr -> Maybe ViewType
viewExprAsType view = case view of
  VEName name -> Just (VTName name)
  VEVar _ -> Nothing
  VEVarId varId -> Just (VTVar varId)
  VEApp (VEName "Ref") (VEInt n) -> Just (VTRef n)
  VEApp (VEName "Ref") (VEString s) -> Just (VTRefText s)
  VEApp (VEName "List") item -> VTList <$> viewExprAsType item
  VEApp (VEName "Maybe") item -> VTMaybe <$> viewExprAsType item
  VEApp (VEApp (VEName "Pair") left) right -> VTPair <$> viewExprAsType left <*> viewExprAsType right
  VEApp (VEApp (VEName "Result") err) ok -> VTResult <$> viewExprAsType err <*> viewExprAsType ok
  VEApp (VEApp (VEName "Fn") (VEList args)) resultView -> VTFn <$> mapM viewExprAsType args <*> viewExprAsType resultView
  VEForall binders body -> VTForall binders <$> viewExprAsType body
  VEExists binders body -> VTExists binders <$> viewExprAsType body
  _ -> Nothing

lowerViewExpr :: ViewExpr -> Either String String
lowerViewExpr ty = case ty of
  VEName "Any" -> Right "viewAny"
  VEName "Bool" -> Right "viewBool"
  VEName "String" -> Right "viewString"
  VEName "Byte" -> Right "viewByte"
  VEName "Unit" -> Right "viewUnit"
  VEName name -> Right name
  VEVar name -> Right $ "viewVar " ++ show name
  VEVarId varId -> Right $ "viewVar " ++ show varId
  VEInt n -> Right (show n)
  VEString s -> Right (show s)
  VEList items -> do
    itemExprs <- mapM lowerViewExpr items
    Right $ "[" ++ unwords (map parens itemExprs) ++ "]"
  VEApp (VEName "Ref") (VEInt n) -> Right $ "viewRef " ++ show n
  VEApp (VEName "Ref") (VEString s) -> Right $ "viewRef " ++ show s
  VEApp (VEName "List") elemView -> do
    elemExpr <- lowerViewExpr elemView
    Right $ "viewList " ++ parens elemExpr
  VEApp (VEName "Maybe") elemView -> do
    elemExpr <- lowerViewExpr elemView
    Right $ "viewMaybe " ++ parens elemExpr
  VEApp (VEApp (VEName "Pair") left) right -> do
    l <- lowerViewExpr left
    r <- lowerViewExpr right
    Right $ "viewPair " ++ parens l ++ " " ++ parens r
  VEApp (VEApp (VEName "Result") err) ok -> do
    e <- lowerViewExpr err
    a <- lowerViewExpr ok
    Right $ "viewResult " ++ parens e ++ " " ++ parens a
  VEApp (VEApp (VEName "Fn") (VEList args)) resultView -> do
    as <- mapM lowerViewExpr args
    r <- lowerViewExpr resultView
    Right $ "viewFn [" ++ unwords (map parens as) ++ "] " ++ parens r
  VEApp func arg -> do
    f <- lowerViewExpr func
    a <- lowerViewExpr arg
    Right $ parens f ++ " " ++ parens a
  VEForall binders body -> do
    bodyExpr <- lowerViewExpr body
    Right $ "viewForall " ++ lowerStringList binders ++ " " ++ parens bodyExpr
  VEExists binders body -> do
    bodyExpr <- lowerViewExpr body
    Right $ "viewExists " ++ lowerStringList binders ++ " " ++ parens bodyExpr
  VERaw raw -> Right raw

lowerStringList :: [Integer] -> String
lowerStringList items = "[" ++ unwords (map (parens . show) items) ++ "]"

quantifyFreeViewVars :: ViewExpr -> ViewExpr
quantifyFreeViewVars view =
  let vars = Set.toList (freeViewVars view)
      binderIds = zip vars [0..]
      binderMap = Map.fromList binderIds
      body = rewriteViewVars binderMap view
      binders = map snd binderIds
  in if null vars then view else VEForall binders body

rewriteViewVars :: Map.Map String Integer -> ViewExpr -> ViewExpr
rewriteViewVars binderMap view = case view of
  VEVar name -> maybe (VEVar name) VEVarId (Map.lookup name binderMap)
  VEList items -> VEList (map (rewriteViewVars binderMap) items)
  VEApp f a -> VEApp (rewriteViewVars binderMap f) (rewriteViewVars binderMap a)
  VEForall binders body -> VEForall binders (rewriteViewVars binderMap body)
  VEExists binders body -> VEExists binders (rewriteViewVars binderMap body)
  _ -> view

freeViewVars :: ViewExpr -> Set.Set String
freeViewVars view = case view of
  VEVar name -> Set.singleton name
  VEVarId _ -> Set.empty
  VEList items -> Set.unions (map freeViewVars items)
  VEApp f a -> Set.union (freeViewVars f) (freeViewVars a)
  VEForall _ body -> freeViewVars body
  VEExists _ body -> freeViewVars body
  _ -> Set.empty

treeSource :: T -> String
treeSource Leaf = "t"
treeSource (Stem x) = "(t " ++ treeSource x ++ ")"
treeSource (Fork x y) = "(t " ++ treeSource x ++ " " ++ treeSource y ++ ")"

parens :: String -> String
parens s = "(" ++ s ++ ")"