content: module SimplifyInterpreter (interpret', simplify') where
  
  import qualified Data.HashMap.Strict as M
  import qualified Data.HashSet as S
  import Language.Fixpoint.Solver.Interpreter (ICtx (..), Knowledge (..))
  import qualified Language.Fixpoint.Solver.Interpreter as Interpreter
  import Language.Fixpoint.Types.Environments (SEnv (..))
  import Language.Fixpoint.Types.Refinements (Expr)
  
  interpret' :: Expr -> Expr
  interpret' = Interpreter.interpret emptyConstMap emptyKnowledge emptyICtx emptySEnv
    where
      emptyConstMap = M.empty
      emptySEnv = SE M.empty
  
  simplify' :: Expr -> Expr
  simplify' = Interpreter.simplify emptyKnowledge emptyICtx
  
  emptyKnowledge :: Interpreter.Knowledge
  emptyKnowledge =
    Interpreter.KN
      { knSims = M.empty, -- :: M.HashMap (Symbol, Symbol) Rewrite
        knAms = M.empty, -- :: M.HashMap Symbol Equation
        knLams = [], -- :: ![(Symbol, Sort)]
        knSummary = [], -- :: ![(Symbol, Int)]
        knDCs = S.empty, -- :: !(S.HashSet Symbol)
        knAllDCs = S.empty, -- :: !(S.HashSet Symbol)
        knSels = M.empty, -- :: !SelectorMap
        knConsts = M.empty -- :: !ConstDCMap
      }
  
  emptyICtx :: Interpreter.ICtx
  emptyICtx =
    Interpreter.ICtx
      { icCands = S.empty, -- :: S.HashSet Expr
        icEquals = S.empty, -- :: EvAccum
        icSolved = S.empty, -- :: S.HashSet Expr
        icSimpl = M.empty, -- :: !ConstMap
        icSubcId = Nothing -- :: Maybe SubcId
      }
  