module Core.Normalise import Core.CaseTreeimport Core.Contextimport Core.Coreimport Core.Envimport Core.Optionsimport Core.Primitivesimport Core.TTimport Core.Value import Data.IntMapimport Data.Vect %default covering -- A pair of a term and its normal form. This could be constructed either-- from a term (via 'gnf') or a normal form (via 'glueBack') but the other-- part will only be constructed when needed, because it's in Core.public exportdata Glued : List Name -> Type where     MkGlue : (fromTerm : Bool) -> -- is it built from the term; i.e. can                                   -- we read the term straight back?              Core (Term vars) -> (Ref Ctxt Defs -> Core (NF vars)) -> Glued vars exportisFromTerm : Glued vars -> BoolisFromTerm (MkGlue ft _ _) = ft exportgetTerm : Glued vars -> Core (Term vars)getTerm (MkGlue _ tm _) = tm exportgetNF : {auto c : Ref Ctxt Defs} -> Glued vars -> Core (NF vars)getNF {c} (MkGlue _ _ nf) = nf c Stack : List Name -> TypeStack vars = List (Closure vars) evalWithOpts : {vars : _} ->               Defs -> EvalOpts ->               Env Term free -> LocalEnv free vars ->               Term (vars ++ free) -> Stack free -> Core (NF free) exportevalClosure : Defs -> Closure free -> Core (NF free) exportevalArg : Defs -> Closure free -> Core (NF free)evalArg defs c = evalClosure defs c exporttoClosure : EvalOpts -> Env Term outer -> Term outer -> Closure outertoClosure opts env tm = MkClosure opts [] env tm useMeta : FC -> Name -> Defs -> EvalOpts -> Core EvalOptsuseMeta fc (Resolved i) defs opts    = case lookup i (usedMetas opts) of           Nothing => pure (record { usedMetas $= insert i () } opts)           Just _ => throw (CyclicMeta fc (Resolved i))useMeta fc n defs opts    = do let Just i = getNameID n (gamma defs)              | Nothing => throw (UndefinedName fc n)         useMeta fc (Resolved i) defs opts parameters (defs : Defs, topopts : EvalOpts)  mutual    eval : {vars : _} ->           Env Term free -> LocalEnv free vars ->           Term (vars ++ free) -> Stack free -> Core (NF free)    eval env locs (Local fc mrig idx prf) stk        = evalLocal env fc mrig idx prf stk locs    eval env locs (Ref fc nt fn) stk        = evalRef env False fc nt fn stk (NApp fc (NRef nt fn) stk)    eval {vars} {free} env locs (Meta fc name idx args) stk        = evalMeta env fc name idx (closeArgs args) stk      where        -- Yes, it's just a map, but specialising it by hand since we        -- use this a *lot* and it saves the run time overhead of making        -- a closure and calling APPLY.        closeArgs : List (Term (vars ++ free)) -> List (Closure free)        closeArgs [] = []        closeArgs (t :: ts) = MkClosure topopts locs env t :: closeArgs ts    eval env locs (Bind fc x (Lam r _ ty) scope) (thunk :: stk)        = eval env (thunk :: locs) scope stk    eval env locs (Bind fc x b@(Let r val ty) scope) stk        = if holesOnly topopts || argHolesOnly topopts             then do b' <- traverse (\tm => eval env locs tm []) b                     pure $ NBind fc x b'                        (\defs', arg => evalWithOpts defs' topopts                                                env (arg :: locs) scope stk)             else eval env (MkClosure topopts locs env val :: locs) scope stk    eval env locs (Bind fc x b scope) stk        = do b' <- traverse (\tm => eval env locs tm []) b             pure $ NBind fc x b'                      (\defs', arg => evalWithOpts defs' topopts                                              env (arg :: locs) scope stk)    eval env locs (App fc fn arg) stk        = eval env locs fn (MkClosure topopts locs env arg :: stk)    eval env locs (As fc s n tm) stk        = if removeAs topopts             then eval env locs tm stk             else do n' <- eval env locs n stk                     tm' <- eval env locs tm stk                     pure (NAs fc s n' tm')    eval env locs (TDelayed fc r ty) stk        = do ty' <- eval env locs ty stk             pure (NDelayed fc r ty')    eval env locs (TDelay fc r ty tm) stk        = pure (NDelay fc r (MkClosure topopts locs env ty)                            (MkClosure topopts locs env tm))    eval env locs (TForce fc r tm) stk        = do tm' <- eval env locs tm []             case tm' of                  NDelay fc r _ arg =>                      eval env (arg :: locs) (Local {name = UN "fvar"} fc Nothing _ First) stk                  _ => pure (NForce fc r tm' stk)    eval env locs (PrimVal fc c) stk = pure $ NPrimVal fc c    eval env locs (Erased fc i) stk = pure $ NErased fc i    eval env locs (TType fc) stk = pure $ NType fc     evalLocClosure : Env Term free ->                     FC -> Maybe Bool ->                     Stack free ->                     Closure free ->                     Core (NF free)    evalLocClosure env fc mrig stk (MkClosure opts locs' env' tm')        = evalWithOpts defs opts env' locs' tm' stk    evalLocClosure {free} env fc mrig stk (MkNFClosure nf)        = applyToStack nf stk      where        applyToStack : NF free -> Stack free -> Core (NF free)        applyToStack (NBind fc _ (Lam r e ty) sc) (arg :: stk)            = do arg' <- sc defs arg                 applyToStack arg' stk        applyToStack (NApp fc (NRef nt fn) args) stk            = evalRef env False fc nt fn (args ++ stk)                      (NApp fc (NRef nt fn) args)        applyToStack (NApp fc (NLocal mrig idx p) args) stk          = evalLocal env fc mrig _ p (args ++ stk) []        applyToStack (NDCon fc n t a args) stk            = pure $ NDCon fc n t a (args ++ stk)        applyToStack (NTCon fc n t a args) stk            = pure $ NTCon fc n t a (args ++ stk)        applyToStack nf _ = pure nf     evalLocal : {vars : _} ->                Env Term free ->                FC -> Maybe Bool ->                (idx : Nat) -> .(IsVar name idx (vars ++ free)) ->                Stack free ->                LocalEnv free vars ->                Core (NF free)    -- If it's one of the free variables, we are done unless the free    -- variable maps to a let-binding    evalLocal {vars = []} env fc mrig idx prf stk locs        = if not (holesOnly topopts || argHolesOnly topopts)             -- if we know it's not a let, no point in even running `getBinder`             && fromMaybe True mrig             then               case getBinder prf env of                    Let _ val _ => eval env [] val stk                    _ => pure $ NApp fc (NLocal mrig idx prf) stk             else pure $ NApp fc (NLocal mrig idx prf) stk    evalLocal env fc mrig Z First stk (x :: locs)        = evalLocClosure env fc mrig stk x    evalLocal {vars = x :: xs} {free}              env fc mrig (S idx) (Later p) stk (_ :: locs)        = evalLocal {vars = xs} env fc mrig idx p stk locs     evalMeta : Env Term free ->               FC -> Name -> Int -> List (Closure free) ->               Stack free -> Core (NF free)    evalMeta env fc nm i args stk        = evalRef env True fc Func (Resolved i) (args ++ stk)                  (NApp fc (NMeta nm i args) stk)     evalRef : Env Term free ->              (isMeta : Bool) ->              FC -> NameType -> Name -> Stack free -> (def : Lazy (NF free)) ->              Core (NF free)    evalRef env meta fc (DataCon tag arity) fn stk def        = pure $ NDCon fc fn tag arity stk    evalRef env meta fc (TyCon tag arity) fn stk def        = pure $ NTCon fc fn tag arity stk    evalRef env meta fc Bound fn stk def        = pure def    evalRef env meta fc nt n stk def        = do Just res <- lookupCtxtExact n (gamma defs)                  | Nothing => pure def             let redok = evalAll topopts ||                         reducibleInAny (currentNS defs :: nestedNS defs)                                        (fullname res)                                        (visibility res)             if redok                then do                   opts' <- if noCycles res                               then useMeta fc n defs topopts                               else pure topopts                   evalDef env opts' meta fc                           (multiplicity res) (definition res) (flags res) stk def                else pure def     getCaseBound : List (Closure free) ->                   (args : List Name) ->                   LocalEnv free more ->                   Maybe (LocalEnv free (args ++ more))    getCaseBound []            []        loc = Just loc    getCaseBound []            (_ :: _)  loc = Nothing -- mismatched arg length    getCaseBound (arg :: args) []        loc = Nothing -- mismatched arg length    getCaseBound (arg :: args) (n :: ns) loc = (arg ::) <$> getCaseBound args ns loc     evalConAlt : Env Term free ->                 LocalEnv free more -> EvalOpts -> FC ->                 Stack free ->                 (args : List Name) ->                 List (Closure free) ->                 CaseTree (args ++ more) ->                 (default : Core (NF free)) ->                 Core (NF free)    evalConAlt env loc opts fc stk args args' sc def         = maybe def (\bound => evalTree env bound opts fc stk sc def)                     (getCaseBound args' args loc)     tryAlt : Env Term free ->             LocalEnv free more -> EvalOpts -> FC ->             Stack free -> NF free -> CaseAlt more ->             (default : Core (NF free)) -> Core (NF free)    -- Ordinary constructor matching    tryAlt {more} env loc opts fc stk (NDCon _ nm tag' arity args') (ConCase x tag args sc) def         = if tag == tag'              then evalConAlt env loc opts fc stk args args' sc def              else def    -- Type constructor matching, in typecase    tryAlt {more} env loc opts fc stk (NTCon _ nm tag' arity args') (ConCase nm' tag args sc) def         = if nm == nm'              then evalConAlt env loc opts fc stk args args' sc def              else def    -- Primitive type matching, in typecase    tryAlt env loc opts fc stk (NPrimVal _ c) (ConCase (UN x) tag [] sc) def         = if show c == x              then evalTree env loc opts fc stk sc def              else def    -- Type of type matching, in typecase    tryAlt env loc opts fc stk (NType _) (ConCase (UN "Type") tag [] sc) def         = evalTree env loc opts fc stk sc def    -- Arrow matching, in typecase    tryAlt {more}           env loc opts fc stk (NBind pfc x (Pi r e aty) scty) (ConCase (UN "->") tag [s,t] sc) def       = evalConAlt {more} env loc opts fc stk [s,t]                  [MkNFClosure aty,                   MkNFClosure (NBind pfc x (Lam r e aty) scty)]                  sc def    -- Delay matching    tryAlt env loc opts fc stk (NDelay _ _ ty arg) (DelayCase tyn argn sc) def         = evalTree env (ty :: arg :: loc) opts fc stk sc def    -- Constant matching    tryAlt env loc opts fc stk (NPrimVal _ c') (ConstCase c sc) def         = if c == c' then evalTree env loc opts fc stk sc def                      else def    -- Default case matches against any *concrete* value    tryAlt env loc opts fc stk val (DefaultCase sc) def         = if concrete val              then evalTree env loc opts fc stk sc def              else def      where        concrete : NF free -> Bool        concrete (NDCon _ _ _ _ _) = True        concrete (NTCon _ _ _ _ _) = True        concrete (NPrimVal _ _) = True        concrete (NBind _ _ _ _) = True        concrete (NType _) = True        concrete _ = False    tryAlt _ _ _ _ _ _ _ def = def     findAlt : Env Term free ->              LocalEnv free args -> EvalOpts -> FC ->              Stack free -> NF free -> List (CaseAlt args) ->              (default : Core (NF free)) -> Core (NF free)    findAlt env loc opts fc stk val [] def = def    findAlt env loc opts fc stk val (x :: xs) def         = tryAlt env loc opts fc stk val x (findAlt env loc opts fc stk val xs def)     evalTree : Env Term free -> LocalEnv free args ->               EvalOpts -> FC ->               Stack free -> CaseTree args ->               (default : Core (NF free)) -> Core (NF free)    evalTree env loc opts fc stk (Case idx x _ alts) def      = do xval <- evalLocal env fc Nothing idx (varExtend x) [] loc           findAlt env loc opts fc stk xval alts def    evalTree env loc opts fc stk (STerm tm) def          = do case fuel opts of                    Nothing => evalWithOpts defs opts env loc (embed tm) stk                    Just Z => def                    Just (S k) =>                         do let opts' = record { fuel = Just k } opts                            evalWithOpts defs opts' env loc (embed tm) stk    evalTree env loc opts fc stk _ def = def     -- Take arguments from the stack, as long as there's enough.    -- Returns the arguments, and the rest of the stack    takeFromStack : (arity : Nat) -> Stack free ->                    Maybe (Vect arity (Closure free), Stack free)    takeFromStack arity stk = takeStk arity stk []      where        takeStk : (remain : Nat) -> Stack free ->                  Vect got (Closure free) ->                  Maybe (Vect (got + remain) (Closure free), Stack free)        takeStk {got} Z stk acc = Just (rewrite plusZeroRightNeutral got in                                    reverse acc, stk)        takeStk (S k) [] acc = Nothing        takeStk {got} (S k) (arg :: stk) acc           = rewrite sym (plusSuccRightSucc got k) in                     takeStk k stk (arg :: acc)     argsFromStack : (args : List Name) ->                    Stack free ->                    Maybe (LocalEnv free args, Stack free)    argsFromStack [] stk = Just ([], stk)    argsFromStack (n :: ns) [] = Nothing    argsFromStack (n :: ns) (arg :: args)         = do (loc', stk') <- argsFromStack ns args              pure (arg :: loc', stk')     evalOp : (Vect arity (NF free) -> Maybe (NF free)) ->             Stack free -> (def : Lazy (NF free)) ->             Core (NF free)    evalOp {arity} fn stk def        = case takeFromStack arity stk of               -- Stack must be exactly the right height               Just (args, []) =>                  do argsnf <- evalAll args                     case fn argsnf of                          Nothing => pure def                          Just res => pure res               _ => pure def      where        -- No traverse for Vect in Core...        evalAll : Vect n (Closure free) -> Core (Vect n (NF free))        evalAll [] = pure []        evalAll (c :: cs) = pure $ !(evalClosure defs c) :: !(evalAll cs)     evalDef : Env Term free -> EvalOpts ->              (isMeta : Bool) -> FC ->              RigCount -> Def -> List DefFlag ->              Stack free -> (def : Lazy (NF free)) ->              Core (NF free)    evalDef env opts meta fc rigd (PMDef r args tree _ _) flags stk def       -- If evaluating the definition fails (e.g. due to a case being       -- stuck) return the default.       -- We can use the definition if one of the following is true:       --   + The 'alwayReduce' flag (r) is set       --   + We're not in 'holesOnly', 'argHolesOnly' or 'tcInline'       --         (that's the default mode)       --   + It's a metavariable and not in Rig0       --   + It's a metavariable and we're not in 'argHolesOnly'       --   + It's inlinable and we're in 'tcInline'        = if alwaysReduce r             || (not (holesOnly opts || argHolesOnly opts || tcInline opts))             || (meta && rigd /= Rig0)             || (meta && holesOnly opts)             || (tcInline opts && elem TCInline flags)             then case argsFromStack args stk of                       Nothing => pure def                       Just (locs', stk') =>                            evalTree env locs' opts fc stk' tree (pure def)             else pure def    evalDef env opts meta fc rigd (Builtin op) flags stk def        = evalOp (getOp op) stk def    -- All other cases, use the default value, which is already applied to    -- the stack    evalDef env opts _ _ _ _ _ stk def = pure def -- Make sure implicit argument order is right... 'vars' is used so we'll-- write it explicitly, but it does appear after the parameters in 'eval'!evalWithOpts {vars} defs opts = eval {vars} defs opts evalClosure defs (MkClosure opts locs env tm)    = eval defs opts env locs tm []evalClosure defs (MkNFClosure nf) = pure nf exportnf : Defs -> Env Term vars -> Term vars -> Core (NF vars)nf defs env tm = eval defs defaultOpts env [] tm [] exportnfOpts : EvalOpts -> Defs -> Env Term vars -> Term vars -> Core (NF vars)nfOpts opts defs env tm = eval defs opts env [] tm [] exportgnf : Env Term vars -> Term vars -> Glued varsgnf env tm    = MkGlue True             (pure tm)             (\c => do defs <- get Ctxt                       nf defs env tm) exportgnfOpts : EvalOpts -> Env Term vars -> Term vars -> Glued varsgnfOpts opts env tm    = MkGlue True             (pure tm)             (\c => do defs <- get Ctxt                       nfOpts opts defs env tm) exportgType : FC -> Glued varsgType fc = MkGlue True (pure (TType fc)) (const (pure (NType fc))) exportgErased : FC -> Glued varsgErased fc = MkGlue True (pure (Erased fc False)) (const (pure (NErased fc False))) exportdata QVar : Type where public exportinterface Quote (tm : List Name -> Type) where    quote : Defs -> Env Term vars -> tm vars -> Core (Term vars)    quoteGen : Ref QVar Int -> Defs -> Env Term vars -> tm vars -> Core (Term vars)     quote defs env tm        = do q <- newRef QVar 0             quoteGen q defs env tm genName : {auto q : Ref QVar Int} -> String -> Core NamegenName n    = do i <- get QVar         put QVar (i + 1)         pure (MN n i) mutual  quoteArgs : {bound : _} ->              Ref QVar Int -> Defs -> Bounds bound ->              Env Term free -> List (Closure free) ->              Core (List (Term (bound ++ free)))  quoteArgs q defs bounds env [] = pure []  quoteArgs q defs bounds env (a :: args)      = pure $ (!(quoteGenNF q defs bounds env !(evalClosure defs a)) ::                !(quoteArgs q defs bounds env args))   quoteHead : {bound : _} ->              Ref QVar Int -> Defs ->              FC -> Bounds bound -> Env Term free -> NHead free ->              Core (Term (bound ++ free))  quoteHead {bound} q defs fc bounds env (NLocal mrig _ prf)      = let MkVar prf' = addLater bound prf in            pure $ Local fc mrig _ prf'    where      addLater : (ys : List Name) -> IsVar n idx xs ->                 Var (ys ++ xs)      addLater [] isv = MkVar isv      addLater (x :: xs) isv          = let MkVar isv' = addLater xs isv in                MkVar (Later isv')  quoteHead q defs fc bounds env (NRef Bound (MN n i))      = case findName bounds of             Just (MkVar p) => pure $ Local fc Nothing _ (varExtend p)             Nothing => pure $ Ref fc Bound (MN n i)    where      findName : Bounds bound' -> Maybe (Var bound')      findName None = Nothing      findName (Add x (MN n' i') ns)          = if i == i' -- this uniquely identifies it, given how we                       -- generated the names, and is a faster test!               then Just (MkVar First)               else do MkVar p <-findName ns                       Just (MkVar (Later p))      findName (Add x _ ns)          = do MkVar p <-findName ns               Just (MkVar (Later p))  quoteHead q defs fc bounds env (NRef nt n) = pure $ Ref fc nt n  quoteHead q defs fc bounds env (NMeta n i args)      = do args' <- quoteArgs q defs bounds env args           pure $ Meta fc n i args'   quotePi : {bound : _} ->            Ref QVar Int -> Defs -> Bounds bound ->            Env Term free -> PiInfo (NF free) ->            Core (PiInfo (Term (bound ++ free)))  quotePi q defs bounds env Explicit = pure Explicit  quotePi q defs bounds env Implicit = pure Implicit  quotePi q defs bounds env AutoImplicit = pure AutoImplicit  quotePi q defs bounds env (DefImplicit t)      = do t' <- quoteGenNF q defs bounds env t           pure (DefImplicit t')   quoteBinder : {bound : _} ->                Ref QVar Int -> Defs -> Bounds bound ->                Env Term free -> Binder (NF free) ->                Core (Binder (Term (bound ++ free)))  quoteBinder q defs bounds env (Lam r p ty)      = do ty' <- quoteGenNF q defs bounds env ty           p' <- quotePi q defs bounds env p           pure (Lam r p' ty')  quoteBinder q defs bounds env (Let r val ty)      = do val' <- quoteGenNF q defs bounds env val           ty' <- quoteGenNF q defs bounds env ty           pure (Let r val' ty')

Lines 1–500 of 1000. Load more