module Core.Value import Core.Contextimport Core.Coreimport Core.Envimport Core.TT import Data.IntMap public exportrecord EvalOpts where  constructor MkEvalOpts  holesOnly : Bool -- only evaluate hole solutions  argHolesOnly : Bool -- only evaluate holes which are relevant arguments  removeAs : Bool -- reduce 'as' patterns (don't do this on LHS)  usedMetas : IntMap () -- Metavariables we're under, to detect cycles  evalAll : Bool -- evaluate everything, including private names  tcInline : Bool -- inline for totality checking  fuel : Maybe Nat -- Limit for recursion depth  reduceLimit : List (Name, Nat) -- reduction limits for given names. If not                     -- present, no limit exportdefaultOpts : EvalOptsdefaultOpts = MkEvalOpts False False True empty False False Nothing [] exportwithHoles : EvalOptswithHoles = MkEvalOpts True True False empty False False Nothing [] exportwithAll : EvalOptswithAll = MkEvalOpts False False True empty True False Nothing [] exportwithArgHoles : EvalOptswithArgHoles = MkEvalOpts False True False empty False False Nothing [] exporttcOnly : EvalOptstcOnly = record { tcInline = True } withArgHoles exportonLHS : EvalOptsonLHS = record { removeAs = False } defaultOpts mutual  public export  data LocalEnv : List Name -> List Name -> Type where       Nil  : LocalEnv free []       (::) : Closure free -> LocalEnv free vars -> LocalEnv free (x :: vars)   public export  data Closure : List Name -> Type where       MkClosure : (opts : EvalOpts) ->                   LocalEnv free vars ->                   Env Term free ->                   Term (vars ++ free) -> Closure free       MkNFClosure : NF free -> Closure free   -- The head of a value: things you can apply arguments to  public export  data NHead : List Name -> Type where       NLocal : Maybe Bool -> (idx : Nat) -> IsVar name idx vars ->                NHead vars       NRef   : NameType -> Name -> NHead vars       NMeta  : Name -> Int -> List (Closure vars) -> NHead vars   -- Values themselves. 'Closure' is an unevaluated thunk, which means  -- we can wait until necessary to reduce constructor arguments  public export  data NF : List Name -> Type where       NBind    : FC -> (x : Name) -> Binder (NF vars) ->                  (Defs -> Closure vars -> Core (NF vars)) -> NF vars       NApp     : FC -> NHead vars -> List (Closure vars) -> NF vars       NDCon    : FC -> Name -> (tag : Int) -> (arity : Nat) ->                  List (Closure vars) -> NF vars       NTCon    : FC -> Name -> (tag : Int) -> (arity : Nat) ->                  List (Closure vars) -> NF vars       NAs      : FC -> UseSide -> NF vars -> NF vars -> NF vars       NDelayed : FC -> LazyReason -> NF vars -> NF vars       NDelay   : FC -> LazyReason -> Closure vars -> Closure vars -> NF vars       NForce   : FC -> LazyReason -> NF vars -> List (Closure vars) -> NF vars       NPrimVal : FC -> Constant -> NF vars       NErased  : FC -> (imp : Bool) -> NF vars       NType    : FC -> NF vars exportgetLoc : NF vars -> FCgetLoc (NBind fc _ _ _) = fcgetLoc (NApp fc _ _) = fcgetLoc (NDCon fc _ _ _ _) = fcgetLoc (NTCon fc _ _ _ _) = fcgetLoc (NAs fc _ _ _) = fcgetLoc (NDelayed fc _ _) = fcgetLoc (NDelay fc _ _ _) = fcgetLoc (NForce fc _ _ _) = fcgetLoc (NPrimVal fc _) = fcgetLoc (NErased fc i) = fcgetLoc (NType fc) = fc