packages feed

egison-5.1.0: hs-src/Language/Egison/Eval.hs

{- |
Module      : Language.Egison.Eval
Licence     : MIT

This module provides interface for evaluating Egison expressions.

Processing Flow (design/implementation.md):
  1. TopExpr (Parse result)
  2. expandLoads (File loading with caching)
  3. Environment Building Phase (Collect data constructors, type classes, instances, type signatures)
  4. Desugar (Syntactic desugaring)
  5-6. Type Inference Phase (Constraint generation, unification, TIExpr generation)
  7. TypedDesugar (Type-driven transformations: tensorMap insertion, type class expansion)
  8. Definition Binding (Recursive binding of all definitions)
  9. Evaluation (Pattern matching execution, expression evaluation, IO actions)
-}

module Language.Egison.Eval
  (
  -- * Eval Egison expressions
    evalExpr
  , evalTopExpr
  , evalTopExprStr
  , evalTopExprs
  , evalTopExprs'
  , evalTopExprsNoPrint
  , runExpr
  , runTopExpr
  , runTopExprStr
  , runTopExprs
  -- * Load Egison files
  , loadEgisonLibrary
  , loadEgisonFile
  -- * Load expansion
  , expandLoads
  ) where

import           Control.Monad              (foldM, forM_, when)
import           Data.IORef                 (newIORef)
import           Data.List                  (intercalate)
import           Control.Monad.Except       (throwError, catchError)
import           Control.Monad.Reader       (ask, asks)
import           Control.Monad.State
import           System.IO                  (hPutStrLn, stderr)

import           Language.Egison.AST
import           Language.Egison.CmdOptions
import           Language.Egison.Core
import           Language.Egison.Data
import           Language.Egison.Desugar (desugarExpr, desugarTopExpr, desugarTopExprs)
import           Language.Egison.EnvBuilder (buildEnvironments, EnvBuildResult(..))
import           Language.Egison.EvalState  (MonadEval (..), ConstructorEnv, PatternConstructorEnv)
import           Language.Egison.IExpr (TITopExpr(..), ITopExpr(..), IExpr(..), Var(..), stringToVar, stripTypeTopExpr)
import           Language.Egison.MathOutput (prettyMath)
import           Language.Egison.Parser
import qualified Language.Egison.Type.Types as Types
import           Language.Egison.Type.Infer (inferITopExpr, runInferWithWarningsAndState, InferState(..), initialInferStateWithConfig, permissiveInferConfig, defaultInferConfig, cfgMatcherConsistencyWarnings)
import           Language.Egison.Type.Env (TypeEnv, ClassEnv, PatternTypeEnv, extendEnvMany, envToList, classEnvToList, lookupInstances, patternEnvToList, mergeClassEnv, extendPatternEnv)
import           Language.Egison.Type.TypeClassExpand ()
import           Language.Egison.Type.TypedDesugar (desugarTypedTopExprT_TensorMapOnly, desugarTypedTopExprT_TypeClassOnly)
import           Language.Egison.Type.Error (TypeError, formatTypeError, formatTypeWarning)
import           Language.Egison.Type.Check (builtinEnv)
import           Language.Egison.Type.Pretty (prettyTypeScheme, prettyType)
import           Language.Egison.Pretty (prettyStr)
import           Language.Egison.EvalState (ConstructorInfo(..))
import qualified Data.HashMap.Strict as HashMap
import qualified Data.Set as Set


-- | Evaluate an Egison expression.
evalExpr :: Env -> Expr -> EvalM EgisonValue
evalExpr env expr = desugarExpr expr >>= evalExprDeep env

--------------------------------------------------------------------------------
-- Phase 1: expandLoads - File Loading with Caching
--------------------------------------------------------------------------------

-- | Expand all Load/LoadFile statements recursively into a flat list of TopExprs.
expandLoads :: [TopExpr] -> EvalM [TopExpr]
expandLoads [] = return []
expandLoads (expr:rest) = case expr of
  Load lib -> do
    libExprs <- loadLibraryFile lib
    expanded <- expandLoads libExprs
    restExpanded <- expandLoads rest
    return $ expanded ++ restExpanded
  LoadFile file -> do
    fileExprs <- loadFile file
    expanded <- expandLoads fileExprs
    restExpanded <- expandLoads rest
    return $ expanded ++ restExpanded
  _ -> do
    restExpanded <- expandLoads rest
    return $ expr : restExpanded

--------------------------------------------------------------------------------
-- Main Pipeline Entry Point
--------------------------------------------------------------------------------

-- | Evaluate an Egison top expression.
evalTopExpr :: Env -> TopExpr -> EvalM (Maybe EgisonValue, Env)
evalTopExpr env topExpr = do
  expanded <- expandLoads [topExpr]
  evalExpandedTopExprsTyped env expanded

-- | Evaluate expanded top expressions using typed pipeline
evalExpandedTopExprsTyped :: Env -> [TopExpr] -> EvalM (Maybe EgisonValue, Env)
evalExpandedTopExprsTyped env exprs = evalExpandedTopExprsTyped' env exprs False True

--------------------------------------------------------------------------------
-- Pipeline Accumulator
--------------------------------------------------------------------------------

-- | Accumulator used during per-expression fold in phases 3-8.
-- Separates value bindings, pattern function bindings, non-definition expressions,
-- and optional dump lists for --dump-typed / --dump-ti / --dump-tc flags.
data PipelineAccum = PipelineAccum
  { accumBindings       :: [(Var, IExpr)]
  , accumPatFuncBindings :: [(String, IExpr)]
  , accumNonDefExprs    :: [(ITopExpr, Bool)]
  , accumTypedExprs     :: [Maybe TITopExpr]
  , accumTiExprs        :: [Maybe TITopExpr]
  , accumTcExprs        :: [Maybe TITopExpr]
  }

emptyAccum :: PipelineAccum
emptyAccum = PipelineAccum [] [] [] [] [] []

-- | Classify an ITopExpr into one of the accumulator bins.
classifyITopExpr :: ITopExpr -> Bool -> PipelineAccum -> PipelineAccum
classifyITopExpr iExpr printValues acc = case iExpr of
  IDefine name expr ->
    acc { accumBindings = accumBindings acc ++ [(name, expr)] }
  IDefineMany defs ->
    acc { accumBindings = accumBindings acc ++ defs }
  IPatternFunctionDecl name _tyVars params _retType body ->
    let paramNames = map fst params
        patternFuncExpr = IPatternFuncExpr paramNames body
    in acc { accumPatFuncBindings = accumPatFuncBindings acc ++ [(name, patternFuncExpr)] }
  _ ->
    acc { accumNonDefExprs = accumNonDefExprs acc ++ [(iExpr, printValues)] }

--------------------------------------------------------------------------------
-- Phase 2-9: Environment Building → Desugar → Type Inference →
--            TypedDesugar → Binding → Evaluation
--------------------------------------------------------------------------------

-- | Evaluate expanded top expressions using the typed pipeline with optional printing.
evalExpandedTopExprsTyped' :: Env -> [TopExpr] -> Bool -> Bool -> EvalM (Maybe EgisonValue, Env)
evalExpandedTopExprsTyped' env exprs printValues shouldDumpTyped = do
  opts <- ask

  -- M4 (quotient mechanism, design/type-cas-quotient.md): macro-expand
  -- `declare cas-quotient` into ordinary defs/instances/assertions BEFORE
  -- environment building, so the generated instances and signatures flow
  -- through the normal prepass.
  exprs' <- expandCasQuotientDecls exprs

  -- Phase 2: Environment Building
  buildAndMergeEnvironments exprs' opts

  -- Pre-bind declared symbols. `declare symbol K` (uppercase) would
  -- otherwise fall through to the InductiveData fallback in IVarExpr at
  -- runtime, so any def whose body mentions `K` (e.g. `def W := 1/(1-K*r^2)`)
  -- would have to *capture* an env with K bound — but the IDeclareSymbol
  -- top expr is processed in Phase 9 (after recursiveBindAll), so without
  -- this pre-binding the def closure captures an env where K is missing.
  -- Binding here makes the symbol visible to subsequent defs and to the
  -- IDeclareSymbol pass itself (which is then a no-op).
  envWithSymbols <- preBindDeclaredSymbols env exprs'

  let permissive = not (optTypeCheckStrict opts)

  -- Phases 3-8: Desugar, type-infer, typed-desugar each expression.
  -- The definition names of the whole batch let the inferencer tell a
  -- forward reference (defined later in this load unit) apart from a
  -- genuinely unknown name when a variable is unbound.
  let batchDefNames = Set.fromList
        [ n | e <- exprs'
            , Just n <- [case e of
                           Define (VarWithIndices n' _) _ -> Just n'
                           DefineWithType tv _            -> Just (typedVarName tv)
                           _                              -> Nothing] ]
  accum <- foldM (processOneExpr opts permissive printValues batchDefNames) emptyAccum exprs'

  -- Dump typed ASTs before evaluation
  when (optDumpTyped opts && shouldDumpTyped) $
    dumpPhaseExprs "Typed AST (Phase 5-6: Type Inference)" "End of Typed AST" (accumTypedExprs accum)
  when (optDumpTi opts && shouldDumpTyped) $
    dumpPhaseExprs "Typed AST after TensorMap Insertion (Phase 7a)" "End of TensorMap Insertion AST" (accumTiExprs accum)
  when (optDumpTc opts && shouldDumpTyped) $
    dumpPhaseExprs "Typed AST after Type Class Expansion (Phase 7b)" "End of Type Class Expansion AST" (accumTcExprs accum)

  -- Phase 8: Bind all definitions together (supports mutual recursion)
  envWithPatFuncs <- recursiveBindAll envWithSymbols (accumBindings accum) (accumPatFuncBindings accum)

  -- Phase 9: Evaluate non-definition expressions in order.
  -- We catch each expression's error so that subsequent expressions still
  -- run (so a single failed `assertEqual` doesn't hide errors in later
  -- assertions). But we COLLECT the errors and re-throw at the end so the
  -- outer EvalM resolves to `Left` — required for `cabal test`'s
  -- `assertEvalM` to report the test as failed.
  (lastVal, finalEnv, collectedErrs) <-
    foldM (\(lastVal, currentEnv, errsAcc) (iExpr, shouldPrint) -> do
      evalResult <- catchError
        (Right <$> evalTopExpr' currentEnv iExpr)
        (\err -> do
          liftIO $ hPutStrLn stderr $ "Evaluation error: " ++ show err
          return $ Left err)

      case evalResult of
        Left err -> return (lastVal, currentEnv, err : errsAcc)
        Right (mVal, env'') -> do
          when shouldPrint $ case mVal of
            Nothing -> return ()
            Just val -> valueToStr val >>= liftIO . putStrLn
          return (mVal, env'', errsAcc)
    ) (Nothing, envWithPatFuncs, []) (accumNonDefExprs accum)

  -- If any expression produced an error, surface the FIRST one so the
  -- outer EvalM is `Left`. The full set has already been streamed to
  -- stderr above. Re-throw only when we collected something to avoid
  -- spurious failures on success paths.
  case reverse collectedErrs of
    []      -> return ()
    (err:_) -> throwError err

  return (lastVal, finalEnv)

--------------------------------------------------------------------------------
-- M4: cas-quotient macro expansion (design/type-cas-quotient.md q1-q4)
--------------------------------------------------------------------------------

-- | Expand `declare cas-quotient Q := Base by reduce` into ordinary
-- definitions, instances, and congruence-law assertions:
--
--   def reduceQ := <reduce>                      (user AST, spliced directly)
--   def projQ (x : MathValue) : Q := casQuotientCast (reduceQ x)
--   def reprQ (v : Q) : MathValue := casQuotientCast v
--   instance Eq/AddSemigroup/../Ring Q           (homomorphic ops:
--                                                 projQ (reprQ a ∘' reprQ b))
--   assertEqual ... (q4: idempotence + congruence over a sample battery)
--
-- Nominal typing (q1) comes from registering Q in the cas-type alias
-- environment as Q -> TInductive Q [], so every annotation seam maps the
-- bare name to an opaque type that unifies only with itself and joins no
-- subtype order (D4: quotients live outside the tower; `declare
-- cas-subtype` rejects them as non-CAS types).
--
-- Notes: crossing is explicit (projQ / reprQ). The homomorphic delegation
-- is sound because reduce is a ring-homomorphism kernel projection (checked
-- by the generated congruence assertions); non-homomorphic operations
-- (inv, gcd, comparisons) must be defined on Q directly (pattern 2).
expandCasQuotientDecls :: [TopExpr] -> EvalM [TopExpr]
expandCasQuotientDecls exprs = concat <$> mapM expand exprs
  where
    expand (DeclareCasQuotient name _baseTE reduceExpr) = do
      aliases <- getCasTypeAliasEnv
      ctorEnv <- getConstructorEnv
      when (Set.member name Types.reservedCasTypeNames) $ throwError $ Default $
        "declare cas-quotient: name clashes with a builtin type: " ++ name
      when (HashMap.member name aliases) $ throwError $ Default $
        "declare cas-quotient: name is already declared (cas-type alias or quotient): " ++ name
      when (any ((== name) . ctorTypeName) (HashMap.elems ctorEnv)) $
        throwError $ Default $
          "declare cas-quotient: name clashes with an inductive type: " ++ name
      -- q1: nominal registration through the alias environment
      setCasTypeAliasEnv (HashMap.insert name (Types.TInductive name []) aliases)
      generated <- readTopExprs (casQuotientTemplate name)
      return (Define (VarWithIndices ("reduce" ++ name) []) reduceExpr : generated)
    expand e = return [e]

-- | The generated program for one quotient declaration (q2/q3/q4).
-- Kept as concrete source text and re-parsed: every piece is ordinary
-- Egison, which keeps the mechanism a plain macro.
casQuotientTemplate :: String -> String
casQuotientTemplate q = unlines
  [ "def proj" ++ q ++ " (x : MathValue) : " ++ q ++ " := casQuotientCast (" ++ red ++ " x)"
  , "def repr" ++ q ++ " (v : " ++ q ++ ") : MathValue := casQuotientCast v"
  , "instance Eq " ++ q ++ " where"
  , "  (==) a b := (" ++ red ++ " ((repr" ++ q ++ " a) -' (repr" ++ q ++ " b))) = 0"
  , "  (/=) a b := not ((" ++ red ++ " ((repr" ++ q ++ " a) -' (repr" ++ q ++ " b))) = 0)"
  , "instance AddSemigroup " ++ q ++ " where"
  , "  (+) a b := proj" ++ q ++ " ((repr" ++ q ++ " a) +' (repr" ++ q ++ " b))"
  , "instance AddMonoid " ++ q ++ " where"
  , "  zero := proj" ++ q ++ " 0"
  , "instance AddGroup " ++ q ++ " where"
  , "  neg a := proj" ++ q ++ " (0 -' (repr" ++ q ++ " a))"
  , "instance MulSemigroup " ++ q ++ " where"
  , "  (*) a b := proj" ++ q ++ " ((repr" ++ q ++ " a) *' (repr" ++ q ++ " b))"
  , "instance MulMonoid " ++ q ++ " where"
  , "  one := proj" ++ q ++ " 1"
  , "instance Ring " ++ q
  , "assertEqual \"cas-quotient " ++ q ++ ": reduce is idempotent (sample battery)\""
  , "  (map (\\s -> " ++ red ++ " (" ++ red ++ " s)) " ++ battery ++ ")"
  , "  (map (\\s -> " ++ red ++ " s) " ++ battery ++ ")"
  , "assertEqual \"cas-quotient " ++ q ++ ": reduce is a congruence for +' (sample battery)\""
  , "  (map (\\p -> " ++ red ++ " ((fst p) +' (snd p))) " ++ pairs ++ ")"
  , "  (map (\\p -> " ++ red ++ " ((" ++ red ++ " (fst p)) +' (" ++ red ++ " (snd p)))) " ++ pairs ++ ")"
  , "assertEqual \"cas-quotient " ++ q ++ ": reduce is a congruence for *' (sample battery)\""
  , "  (map (\\p -> " ++ red ++ " ((fst p) *' (snd p))) " ++ pairs ++ ")"
  , "  (map (\\p -> " ++ red ++ " ((" ++ red ++ " (fst p)) *' (" ++ red ++ " (snd p)))) " ++ pairs ++ ")"
  ]
  where
    red = "reduce" ++ q
    battery = "[0, 1, -1, 2, 5, 12]"
    pairs = "[(0, 1), (1, 2), (-1, 5), (2, 12), (5, -1), (12, 7)]"

--------------------------------------------------------------------------------
-- Phase 2: Environment Building & Merging
--------------------------------------------------------------------------------

buildAndMergeEnvironments :: [TopExpr] -> EgisonOpts -> EvalM ()
buildAndMergeEnvironments exprs opts = do
  currentTypeEnv <- getTypeEnv
  currentClassEnv <- getClassEnv
  currentPatternEnv <- getPatternEnv
  currentPatternFuncEnv <- getPatternFuncEnv

  envResult <- buildEnvironments exprs

  let newTypeEnv = ebrTypeEnv envResult
      baseTypeEnv = if null (envToList currentTypeEnv) then builtinEnv else currentTypeEnv
      mergedTypeEnv = extendEnvMany (envToList newTypeEnv) baseTypeEnv
      mergedClassEnv = mergeClassEnv currentClassEnv (ebrClassEnv envResult)
      patternConstructorEnv = ebrPatternConstructorEnv envResult
      newPatternFuncEnv = ebrPatternTypeEnv envResult
      mergedPatternEnv = foldr (\(name, scheme) e -> extendPatternEnv name scheme e)
                               (foldr (\(name, scheme) e -> extendPatternEnv name scheme e)
                                      currentPatternEnv
                                      (patternEnvToList patternConstructorEnv))
                               (patternEnvToList newPatternFuncEnv)
      mergedPatternFuncEnv = foldr (\(name, scheme) e -> extendPatternEnv name scheme e)
                                   currentPatternFuncEnv
                                   (patternEnvToList newPatternFuncEnv)

  setTypeEnv mergedTypeEnv
  setClassEnv mergedClassEnv
  setPatternEnv mergedPatternEnv
  setPatternFuncEnv mergedPatternFuncEnv

  -- Phase alpha (extensible CAS tower): persist `declare cas-type` aliases so
  -- Desugar (this batch) and later load batches can expand annotation types.
  prevAliases <- getCasTypeAliasEnv
  setCasTypeAliasEnv (HashMap.union (ebrCasTypeAliases envResult) prevAliases)

  -- Phase beta: persist `declare cas-subtype` edges (D1-checked in EnvBuilder).
  prevEdges <- getCasSubtypeEdges
  setCasSubtypeEdges (prevEdges ++ ebrCasSubtypeEdges envResult)

  -- Phase 7.4/7.5/6.3: surface declaration counts and names to the runtime
  -- so that inspection primitives (`numReductionRules`, `ruleNames`,
  -- `numDerivativeRules`, `derivativeNames`) can read them. The full data
  -- (LHS/RHS Exprs) is in EnvBuildResult and not yet plumbed; only counts
  -- and names propagate.
  prevR <- getReductionRulesCount
  setReductionRulesCount (prevR + length (ebrReductionRules envResult))
  prevD <- getDerivativeRulesCount
  setDerivativeRulesCount (prevD + length (ebrDerivativeRules envResult))
  prevRNames <- getReductionRuleNames
  setReductionRuleNames (prevRNames ++
    [ n | (Just n, _, _, _) <- ebrReductionRules envResult ])
  prevDNames <- getDerivativeRuleNames
  setDerivativeRuleNames (prevDNames ++
    [ n | (n, _) <- ebrDerivativeRules envResult ])

  forM_ (HashMap.toList (ebrConstructorEnv envResult)) $ \(ctorName, ctorInfo) ->
    registerConstructor ctorName ctorInfo

  when (optDumpEnv opts) $
    dumpEnvironment mergedTypeEnv mergedClassEnv (ebrConstructorEnv envResult)
                    (ebrPatternConstructorEnv envResult) (ebrPatternTypeEnv envResult)

  when (optDumpDesugared opts) $ do
    desugaredExprs <- desugarTopExprs exprs
    dumpDesugared (map Just desugaredExprs)

--------------------------------------------------------------------------------
-- Per-Expression Pipeline (Phases 3-8)
--------------------------------------------------------------------------------

processOneExpr :: EgisonOpts -> Bool -> Bool -> Set.Set String -> PipelineAccum -> TopExpr -> EvalM PipelineAccum
processOneExpr opts permissive printValues batchDefNames acc expr = do
  currentTypeEnv <- getTypeEnv
  currentClassEnv <- getClassEnv

  mITopExpr <- desugarTopExpr expr

  case mITopExpr of
    Nothing -> return acc
    Just iTopExpr -> do
      -- Phase 5-6: Type Inference
      let inferConfig = (if permissive then permissiveInferConfig else defaultInferConfig)
                          { cfgMatcherConsistencyWarnings = optMatcherConsistencyWarnings opts }
      currentPatternEnv' <- getPatternEnv
      currentPatternFuncEnv' <- getPatternFuncEnv
      currentPatternFuncStructEnv' <- getPatternFuncStructEnv
      currentCasEdges <- getCasSubtypeEdges
      let patternFuncBindings = [(stringToVar name, scheme) | (name, scheme) <- patternEnvToList currentPatternFuncEnv']
          enrichedTypeEnv = extendEnvMany patternFuncBindings currentTypeEnv
          initState = (initialInferStateWithConfig inferConfig) {
            inferEnv = enrichedTypeEnv,
            inferClassEnv = currentClassEnv,
            inferPatternEnv = currentPatternEnv',
            inferPatternFuncEnv = currentPatternFuncEnv',
            inferPatternFuncStructEnv = currentPatternFuncStructEnv',
            inferCasSubtypeEdges = currentCasEdges,
            inferBatchDefNames = batchDefNames
          }
      (result, warnings, finalState) <- liftIO $
        runInferWithWarningsAndState (inferITopExpr iTopExpr) initState

      when (not (null warnings)) $
        liftIO $ mapM_ (hPutStrLn stderr . formatTypeWarning) warnings

      setTypeEnv (inferEnv finalState)
      setClassEnv (inferClassEnv finalState)
      setPatternEnv (inferPatternEnv finalState)
      setPatternFuncEnv (inferPatternFuncEnv finalState)
      setPatternFuncStructEnv (inferPatternFuncStructEnv finalState)

      case result of
        Left err -> handleTypeError err acc expr printValues

        Right (Nothing, _subst) ->
          return acc

        Right (Just tiTopExpr, _subst) ->
          runTypedDesugaring opts acc tiTopExpr printValues

-- | Handle type error: fall back to untyped evaluation in permissive mode.
handleTypeError :: TypeError -> PipelineAccum -> TopExpr -> Bool -> EvalM PipelineAccum
handleTypeError err acc expr printValues = do
  liftIO $ hPutStrLn stderr $ "Type error:\n" ++ formatTypeError err
  topExpr' <- desugarTopExpr expr
  case topExpr' of
    Nothing      -> return acc
    Just iExpr   -> return $ classifyITopExpr iExpr printValues acc

-- | Run TensorMap insertion and TypeClass expansion (Phase 7a-7b),
-- then classify the resulting ITopExpr.
runTypedDesugaring :: EgisonOpts -> PipelineAccum -> TITopExpr -> Bool -> EvalM PipelineAccum
runTypedDesugaring opts acc tiTopExpr printValues = do
  let acc1 = if optDumpTyped opts
             then acc { accumTypedExprs = accumTypedExprs acc ++ [Just tiTopExpr] }
             else acc

  -- Phase 7a: TensorMap Insertion
  mAfterTensor <- desugarTypedTopExprT_TensorMapOnly tiTopExpr
  case mAfterTensor of
    Nothing -> return acc1
    Just afterTensor -> do
      let acc2 = if optDumpTi opts
                 then acc1 { accumTiExprs = accumTiExprs acc1 ++ [Just afterTensor] }
                 else acc1

      -- Phase 7b: Type Class Expansion
      mAfterTC <- desugarTypedTopExprT_TypeClassOnly afterTensor
      case mAfterTC of
        Nothing -> return acc2
        Just afterTC -> do
          let acc3 = if optDumpTc opts
                     then acc2 { accumTcExprs = accumTcExprs acc2 ++ [Just afterTC] }
                     else acc2
              iTopExprExpanded = stripTypeTopExpr afterTC
          return $ classifyITopExpr iTopExprExpanded printValues acc3

--------------------------------------------------------------------------------
-- Remaining public API
--------------------------------------------------------------------------------

evalTopExprStr :: Env -> TopExpr -> EvalM (Maybe String, Env)
evalTopExprStr env topExpr = do
  (val, env') <- evalTopExpr env topExpr
  case val of
    Nothing  -> return (Nothing, env')
    Just val -> do str <- valueToStr val
                   return (Just str, env')

valueToStr :: EgisonValue -> EvalM String
valueToStr val = do
  mathValue <- asks optMathValue
  case mathValue of
    Nothing   -> return (show val)
    Just lang -> return (prettyMath lang val)

-- | Evaluate Egison top expressions.
evalTopExprs :: Env -> [TopExpr] -> EvalM Env
evalTopExprs env exprs = evalTopExprs' env exprs True True

-- | Evaluate Egison top expressions with control over printing and dumping.
evalTopExprs' :: Env -> [TopExpr] -> Bool -> Bool -> EvalM Env
evalTopExprs' env exprs printValues shouldDumpTyped = do
  expanded <- expandLoads exprs
  (_, env') <- evalExpandedTopExprsTyped' env expanded printValues shouldDumpTyped
  return env'

-- | Evaluate Egison top expressions without printing.
evalTopExprsNoPrint :: Env -> [TopExpr] -> EvalM Env
evalTopExprsNoPrint env exprs = evalTopExprs' env exprs False True

-- | Evaluate an Egison expression. Input is a Haskell string.
runExpr :: Env -> String -> EvalM EgisonValue
runExpr env input =
  readExpr input >>= evalExpr env

-- | Evaluate an Egison top expression. Input is a Haskell string.
runTopExpr :: Env -> String -> EvalM (Maybe EgisonValue, Env)
runTopExpr env input =
  readTopExpr input >>= evalTopExpr env

-- | Evaluate an Egison top expression. Input is a Haskell string.
runTopExprStr :: Env -> String -> EvalM (Maybe String, Env)
runTopExprStr env input =
  readTopExpr input >>= evalTopExprStr env

-- | Evaluate Egison top expressions. Input is a Haskell string.
runTopExprs :: Env -> String -> EvalM Env
runTopExprs env input =
  readTopExprs input >>= evalTopExprs env

-- | Load an Egison file.
loadEgisonFile :: Env -> FilePath -> EvalM Env
loadEgisonFile env path = do
  (_, env') <- evalTopExpr env (LoadFile path)
  return env'

-- | Load an Egison library.
loadEgisonLibrary :: Env -> FilePath -> EvalM Env
loadEgisonLibrary env path = do
  (_, env') <- evalTopExpr env (Load path)
  return env'


--
-- Helper functions
--

collectDefs :: EgisonOpts -> [ITopExpr] -> EvalM ([(Var, IExpr)], [(String, IExpr)], [ITopExpr])
collectDefs opts exprs = collectDefs' opts exprs [] [] []
  where
    collectDefs' :: EgisonOpts -> [ITopExpr] -> [(Var, IExpr)] -> [(String, IExpr)] -> [ITopExpr] -> EvalM ([(Var, IExpr)], [(String, IExpr)], [ITopExpr])
    collectDefs' opts (expr:exprs) bindings patFuncBindings rest =
      case expr of
        IDefine name expr -> collectDefs' opts exprs ((name, expr) : bindings) patFuncBindings rest
        IDefineMany defs  -> collectDefs' opts exprs (defs ++ bindings) patFuncBindings rest
        IPatternFunctionDecl name _tyVars params _retType body ->
          let paramNames = map fst params
              patternFuncExpr = IPatternFuncExpr paramNames body
          in collectDefs' opts exprs bindings ((name, patternFuncExpr) : patFuncBindings) rest
        ITest{}     -> collectDefs' opts exprs bindings patFuncBindings (expr : rest)
        IExecute{}  -> collectDefs' opts exprs bindings patFuncBindings (expr : rest)
        ILoadFile _ | optNoIO opts -> throwError (Default "No IO support")
        ILoadFile file -> do
          exprs' <- loadFile file >>= desugarTopExprs
          collectDefs' opts (exprs' ++ exprs) bindings patFuncBindings rest
        ILoad _ | optNoIO opts -> throwError (Default "No IO support")
        ILoad file -> do
          exprs' <- loadLibraryFile file >>= desugarTopExprs
          collectDefs' opts (exprs' ++ exprs) bindings patFuncBindings rest
        _ -> collectDefs' opts exprs bindings patFuncBindings rest
    collectDefs' _ [] bindings patFuncBindings rest = return (bindings, patFuncBindings, reverse rest)

evalTopExpr' :: Env -> ITopExpr -> EvalM (Maybe EgisonValue, Env)
evalTopExpr' env (IDefine name expr) = do
  env' <- recursiveBind env [(name, expr)]
  return (Nothing, env')
evalTopExpr' env (IDefineMany defs) = do
  env' <- recursiveBind env defs
  return (Nothing, env')
evalTopExpr' env (ITest expr) = do
  pushFuncName (stringToVar "<stdin>")
  val <- evalExprDeep env expr
  popFuncName
  return (Just val, env)
evalTopExpr' env (IExecute expr) = do
  pushFuncName (stringToVar "<stdin>")
  io <- evalExprShallow env expr
  case io of
    Value (IOFunc m) -> m >> popFuncName >> return (Nothing, env)
    _                -> throwErrorWithTrace (TypeMismatch "io" io)
evalTopExpr' env (ILoad file) = do
  opts <- ask
  when (optNoIO opts) $ throwError (Default "No IO support")
  exprs <- loadLibraryFile file >>= desugarTopExprs
  (bindings, patFuncBindings, _) <- collectDefs opts exprs
  env' <- recursiveBindAll env bindings patFuncBindings
  return (Nothing, env')
evalTopExpr' env (ILoadFile file) = do
  opts <- ask
  when (optNoIO opts) $ throwError (Default "No IO support")
  exprs <- loadFile file >>= desugarTopExprs
  (bindings, patFuncBindings, _) <- collectDefs opts exprs
  env' <- recursiveBindAll env bindings patFuncBindings
  return (Nothing, env')
evalTopExpr' env (IDeclareSymbol _names _mType) = do
  -- Symbols are pre-bound by `preBindDeclaredSymbols` before Phase 8 so
  -- that def closures (e.g. `def W := 1/(1-K*r^2)`) capture an env where
  -- the declared symbols are visible. This case is therefore a no-op.
  return (Nothing, env)
evalTopExpr' _env (IPatternFunctionDecl name _ _ _ _) = do
  throwError $ Default $ "Pattern function " ++ name ++ " should have been converted to IPatternFuncExpr"

-- | Walk the input top exprs, collect every name from `declare symbol`,
-- and bind each to a CAS symbol value in the env. This MUST run before
-- Phase 8 (recursiveBindAll) so def closures capture an env in which the
-- declared symbols resolve correctly — particularly important for
-- uppercase names (`K`, `M`, `G`, …), which otherwise hit the
-- InductiveData fallback in `evalExprShallow env (IVarExpr name)` and
-- cause "Expected number, but found: K" at the first arithmetic use.
preBindDeclaredSymbols :: Env -> [TopExpr] -> EvalM Env
preBindDeclaredSymbols env exprs = do
  let names = concatMap collect exprs
  if null names
    then return env
    else do
      bindings <- mapM mkBinding names
      return $ extendEnv env bindings
  where
    collect :: TopExpr -> [String]
    collect (DeclareSymbol ns _) = ns
    collect _                    = []

    mkBinding :: String -> EvalM Binding
    mkBinding name = do
      ref <- liftIO $ newIORef (WHNF (Value (symbolCASData "" name)))
      return (stringToVar name, ref)

--------------------------------------------------------------------------------
-- Environment Dumping
--------------------------------------------------------------------------------

-- | Dump environment information after Phase 2 (Environment Building)
dumpEnvironment :: TypeEnv -> ClassEnv -> ConstructorEnv -> PatternConstructorEnv -> PatternTypeEnv -> EvalM ()
dumpEnvironment typeEnv classEnv ctorEnv patternCtorEnv patternEnv = do
  liftIO $ do
    putStrLn "=== Environment Information (Phase 2: Environment Building) ==="
    putStrLn ""
    
    -- 1. Type Signatures
    putStrLn "--- Type Signatures ---"
    let typeBindings = envToList typeEnv
    if null typeBindings
      then putStrLn "  (none)"
      else forM_ typeBindings $ \(Var varName indices, scheme) ->
        let displayName = if null indices 
                          then varName
                          else varName ++ concatMap (const "_") indices
        in putStrLn $ "  " ++ displayName ++ " : " ++ prettyTypeScheme scheme
    putStrLn ""
    
    -- 2. Type Classes
    putStrLn "--- Type Classes ---"
    let classBindings = classEnvToList classEnv
    if null classBindings
      then putStrLn "  (none)"
      else forM_ classBindings $ \(className, classInfo) -> do
        let paramName = case Types.classParam classInfo of
              Types.TyVar name -> name
        putStrLn $ "  class " ++ className ++ " " ++ paramName ++ " where"
        forM_ (Types.classMethods classInfo) $ \(methName, methType) ->
          putStrLn $ "    " ++ methName ++ " : " ++ prettyType methType
    putStrLn ""
    
    -- 3. Instances
    putStrLn "--- Type Class Instances ---"
    let allInstances = concatMap (\(clsName, _) -> 
          map (\inst -> (clsName, inst)) (lookupInstances clsName classEnv)) classBindings
    if null allInstances
      then putStrLn "  (none)"
      else forM_ allInstances $ \(className, instInfo) -> do
        let contextStr = if null (Types.instContext instInfo)
              then ""
              else let showConstraint (Types.Constraint cls tys) = cls ++ concatMap (\t -> " " ++ prettyType t) tys
                   in intercalate ", " (map showConstraint (Types.instContext instInfo)) ++ " => "
        putStrLn $ "  instance " ++ contextStr ++ className ++ " " ++ prettyType (Types.instType instInfo)
    putStrLn ""
    
    -- 4. Data Constructors
    putStrLn "--- Data Constructors ---"
    let ctorBindings = HashMap.toList ctorEnv
    if null ctorBindings
      then putStrLn "  (none)"
      else forM_ ctorBindings $ \(ctorName, ctorInfo) -> do
        let typeParams = ctorTypeParams ctorInfo
        let retType = if null typeParams
              then ctorTypeName ctorInfo
              else ctorTypeName ctorInfo ++ " " ++ unwords typeParams
        let ctorType = if null (ctorArgTypes ctorInfo)
              then retType
              else intercalate " -> " (map prettyType (ctorArgTypes ctorInfo) ++ [retType])
        putStrLn $ "  " ++ ctorName ++ " : " ++ ctorType
    putStrLn ""
    
    -- 5. Pattern Constructors
    putStrLn "--- Pattern Constructors ---"
    let patternCtorBindings = patternEnvToList patternCtorEnv
    if null patternCtorBindings
      then putStrLn "  (none)"
      else forM_ patternCtorBindings $ \(ctorName, scheme) ->
        putStrLn $ "  " ++ ctorName ++ " : " ++ prettyTypeScheme scheme
    putStrLn ""
    
    -- 6. Pattern Functions
    putStrLn "--- Pattern Functions ---"
    let patternBindings = patternEnvToList patternEnv
    if null patternBindings
      then putStrLn "  (none)"
      else forM_ patternBindings $ \(name, scheme) ->
        putStrLn $ "  " ++ name ++ " : " ++ prettyTypeScheme scheme
    putStrLn ""
    
    putStrLn "=== End of Environment Information ==="

-- | Dump desugared AST after Phase 3 (Desugaring)
dumpDesugared :: [Maybe ITopExpr] -> EvalM ()
dumpDesugared desugaredExprs = do
  liftIO $ do
    putStrLn "=== Desugared AST (Phase 3: Desugaring) ==="
    putStrLn ""
    if null desugaredExprs
      then putStrLn "  (none)"
      else forM_ (zip [1 :: Int ..] desugaredExprs) $ \(i :: Int, mExpr) ->
        case mExpr of
          Nothing -> putStrLn $ "  [" ++ show i ++ "] (skipped)"
          Just expr -> putStrLn $ "  [" ++ show i ++ "] " ++ prettyStr expr
    putStrLn ""
    putStrLn "=== End of Desugared AST ==="

-- | Generic dump for typed AST phases (--dump-typed, --dump-ti, --dump-tc).
dumpPhaseExprs :: String -> String -> [Maybe TITopExpr] -> EvalM ()
dumpPhaseExprs header footer exprs = liftIO $ do
  putStrLn $ "=== " ++ header ++ " ==="
  putStrLn ""
  if null exprs
    then putStrLn "  (none)"
    else forM_ (zip [1 :: Int ..] exprs) $ \(i :: Int, mExpr) ->
      case mExpr of
        Nothing -> putStrLn $ "  [" ++ show i ++ "] (skipped)"
        Just expr -> putStrLn $ "  [" ++ show i ++ "] " ++ prettyStr expr
  putStrLn ""
  putStrLn $ "=== " ++ footer ++ " ==="