0 | module Core.Normalise.Eval

  2 | import Core.Case.CaseTree

  3 | import Core.Context.Log

  4 | import Core.Env

  5 | import Core.Primitives

  6 | import Core.Value

  8 | import Data.Vect

 10 | import Libraries.Data.WithDefault

 12 | %default covering

 17 | public export

 18 | data Glued : Scoped where

 19 |      MkGlue : (fromTerm : Bool) -> -- is it built from the term; i.e. can

 20 |                                    -- we read the term straight back?

 21 |               Core (Term vars) -> (Ref Ctxt Defs -> Core (NF vars)) -> Glued vars

 24 | isFromTerm : Glued vars -> Bool

 25 | isFromTerm (MkGlue ft _ _) = ft

 28 | getTerm : Glued vars -> Core (Term vars)

 29 | getTerm (MkGlue _ tm _) = tm

 32 | getNF : {auto c : Ref Ctxt Defs} -> Glued vars -> Core (NF vars)

 33 | getNF {c} (MkGlue _ _ nf) = nf c

 35 | public export

 36 | Stack : Scoped

 37 | Stack vars = List (FC, Closure vars)

 39 | evalWithOpts : {auto c : Ref Ctxt Defs} ->

 40 |                {free, vars : _} ->

 41 |                Defs -> EvalOpts ->

 42 |                Env Term free -> LocalEnv free vars ->

 43 |                Term (vars ++ free) -> Stack free -> Core (NF free)

 46 | evalClosure : {auto c : Ref Ctxt Defs} ->

 47 |               {free : _} -> Defs -> Closure free -> Core (NF free)

 50 | evalArg : {auto c : Ref Ctxt Defs} -> {free : _} -> Defs -> Closure free -> Core (NF free)

 51 | evalArg defs c = evalClosure defs c

 54 | toClosure : EvalOpts -> Env Term outer -> Term outer -> Closure outer

 55 | toClosure opts env tm = MkClosure opts LocalEnv.empty env tm

 57 | mkClosure : {vars : _} ->

 58 |             EvalOpts ->

 59 |             LocalEnv free vars -> Env Term free ->

 60 |             Term (vars ++ free) -> Closure free

 61 | mkClosure opts locs env tm@(Local _ _ idx prf)

 62 |     = fromMaybe (MkClosure opts locs env tm) (getLocal idx prf locs)

 63 |   where

 64 |     getLocal : {vars : _} ->

 65 |                (idx : Nat) -> (0 p : IsVar nm idx (vars ++ free)) ->

 66 |                LocalEnv free vars ->

 67 |                Maybe (Closure free)

 68 |     getLocal idx prf [] = Nothing

 69 |     getLocal Z First (x :: locs) = Just x

 70 |     getLocal (S idx) (Later p) (_ :: locs) = getLocal idx p locs

 71 | mkClosure opts locs env tm = MkClosure opts locs env tm

 73 | updateLimit : NameType -> Name -> EvalOpts -> Core (Maybe EvalOpts)

 74 | updateLimit Func n opts

 75 |     = pure $ if isNil (reduceLimit opts)

 76 |          then Just opts

 77 |          else case lookup n (reduceLimit opts) of

 78 |                    Nothing => Nothing

 79 |                    Just Z => Nothing

 80 |                    Just (S k) =>

 81 |                       Just ({ reduceLimit $= set n k } opts)

 82 |   where

 83 |     set : Name -> Nat -> List (Name, Nat) -> List (Name, Nat)

 84 |     set n v [] = []

 85 |     set n v ((x, l) :: xs)

 86 |         = if x == n

 87 |              then (x, v) :: xs

 88 |              else (x, l) :: set n v xs

 89 | updateLimit t n opts = pure (Just opts)

 91 | data CaseResult a

 92 |      = Result a

 93 |      | NoMatch -- case alternative didn't match anything

 94 |      | GotStuck -- alternative matched, but got stuck later

 96 | record TermWithEnv (free : Scope) where

 97 |     constructor MkTermEnv

 98 |     { varsEnv : Scope }

 99 |     locEnv : LocalEnv free varsEnv

100 |     term : Term $ Scope.addInner free varsEnv

102 | parameters (defs : Defs) (topopts : EvalOpts)

103 |   mutual

104 |     eval : {auto c : Ref Ctxt Defs} ->

105 |            {free, vars : _} ->

106 |            Env Term free -> LocalEnv free vars ->

107 |            Term (vars ++ free) -> Stack free -> Core (NF free)

108 |     eval env locs (Local fc mrig idx prf) stk

109 |         = evalLocal env fc mrig idx prf stk locs

110 |     eval env locs (Ref fc nt fn) stk

111 |         = evalRef env False fc nt fn stk (NApp fc (NRef nt fn) stk)

112 |     eval {vars} {free} env locs (Meta fc name idx args) stk

113 |         = evalMeta env fc name idx (closeArgs args) stk

114 |       where

115 |         -- Yes, it's just a map, but specialising it by hand since we

116 |         -- use this a *lot* and it saves the run time overhead of making

117 |         -- a closure and calling APPLY.

118 |         closeArgs : List (Term (Scope.addInner free vars)) -> List (Closure free)

119 |         closeArgs [] = []

120 |         closeArgs (t :: ts) = mkClosure topopts locs env t :: closeArgs ts

121 |     eval env locs (Bind fc x (Lam _ r _ ty) scope) (thunk :: stk)

122 |         = eval env (snd thunk :: locs) scope stk

123 |     eval env locs (Bind fc x b@(Let _ r val ty) scope) stk

124 |         = if (holesOnly topopts || argHolesOnly topopts) && not (tcInline topopts)

125 |              then do let b' = map (mkClosure topopts locs env) b

126 |                      pure $ NBind fc x b'

127 |                         (\defs', arg => evalWithOpts defs' topopts

128 |                                                 env (arg :: locs) scope stk)

129 |              else eval env (mkClosure topopts locs env val :: locs) scope stk

130 |     eval env locs (Bind fc x b scope) stk

131 |         = do let b' = map (mkClosure topopts locs env) b

132 |              pure $ NBind fc x b'

133 |                       (\defs', arg => evalWithOpts defs' topopts

134 |                                               env (arg :: locs) scope stk)

135 |     eval env locs (App fc fn arg) stk

136 |         = case strategy topopts of

137 |                CBV => do arg' <- eval env locs arg []

138 |                          eval env locs fn ((fc, MkNFClosure topopts env arg') :: stk)

139 |                CBN => eval env locs fn ((fc, mkClosure topopts locs env arg) :: stk)

140 |     eval env locs (As fc s n tm) stk

141 |         = if removeAs topopts

142 |              then eval env locs tm stk

143 |              else do n' <- eval env locs n stk

144 |                      tm' <- eval env locs tm stk

145 |                      pure (NAs fc s n' tm')

146 |     eval env locs (TDelayed fc r ty) stk

147 |         = do ty' <- eval env locs ty stk

148 |              pure (NDelayed fc r ty')

149 |     eval env locs (TDelay fc r ty tm) stk

150 |         = pure (NDelay fc r (mkClosure topopts locs env ty)

151 |                             (mkClosure topopts locs env tm))

152 |     eval env locs (TForce fc r tm) stk

153 |         = do tm' <- eval env locs tm []

154 |              case tm' of

155 |                   NDelay fc r _ arg =>

156 |                       eval env (arg :: locs) (Local {name = UN (Basic "fvar")} fc Nothing _ First) stk

157 |                   _ => pure (NForce fc r tm' stk)

158 |     eval env locs (PrimVal fc c) stk = pure $ NPrimVal fc c

159 |     eval env locs (Erased fc a) stk

160 |       = NErased fc <$> traverse @{%search} @{CORE} (\ t => eval env locs t stk) a

161 |     eval env locs (TType fc u) stk = pure $ NType fc u

163 |     -- Apply an evaluated argument (perhaps cached from an earlier evaluation)

164 |     -- to a stack

165 |     export

166 |     applyToStack : {auto c : Ref Ctxt Defs} ->

167 |                    {free : _} ->

168 |                    Env Term free ->

169 |                    NF free -> Stack free -> Core (NF free)

170 |     applyToStack env (NBind fc _ (Lam {}) sc) (arg :: stk)

171 |         = do arg' <- sc defs $ snd arg

172 |              applyToStack env arg' stk

173 |     applyToStack env (NBind fc x b@(Let _ r val ty) sc) stk

174 |         = if (holesOnly topopts || argHolesOnly topopts) && not (tcInline topopts)

175 |              then pure (NBind fc x b

176 |                               (\defs', arg => applyToStack env !(sc defs' arg) stk))

177 |              else applyToStack env !(sc defs val) stk

178 |     applyToStack env (NBind fc x b sc) stk

179 |         = pure (NBind fc x b

180 |                       (\defs', arg => applyToStack env !(sc defs' arg) stk))

181 |     applyToStack env (NApp fc (NRef nt fn) args) stk

182 |         = evalRef env False fc nt fn (args ++ stk)

183 |                   (NApp fc (NRef nt fn) (args ++ stk))

184 |     applyToStack env (NApp fc (NLocal mrig idx p) args) stk

185 |         = evalLocal env fc mrig _ p (args ++ stk) LocalEnv.empty

186 |     applyToStack env (NApp fc (NMeta n i args) args') stk

187 |         = evalMeta env fc n i args (args' ++ stk)

188 |     applyToStack env (NDCon fc n t a args) stk

189 |         = pure $ NDCon fc n t a (args ++ stk)

190 |     applyToStack env (NTCon fc n a args) stk

191 |         = pure $ NTCon fc n a (args ++ stk)

192 |     applyToStack env (NAs fc s p t) stk

193 |        = if removeAs topopts

194 |             then applyToStack env t stk

195 |             else do p' <- applyToStack env p []

196 |                     t' <- applyToStack env t stk

197 |                     pure (NAs fc s p' t')

198 |     applyToStack env (NDelayed fc r tm) stk

199 |        = do tm' <- applyToStack env tm stk

200 |             pure (NDelayed fc r tm')

201 |     applyToStack env nf@(NDelay fc r ty tm) stk

202 |        = pure nf -- stack should always be empty here!

203 |     applyToStack env (NForce fc r tm args) stk

204 |        = do tm' <- applyToStack env tm []

205 |             case tm' of

206 |                  NDelay fc r _ arg =>

207 |                     eval env [arg] (Local {name = UN (Basic "fvar")} fc Nothing _ First) stk

208 |                  _ => pure (NForce fc r tm' (args ++ stk))

209 |     applyToStack env nf@(NPrimVal fc _) _ = pure nf

210 |     applyToStack env (NErased fc a) stk

211 |       = NErased fc <$> traverse @{%search} @{CORE} (\ t => applyToStack env t stk) a

212 |     applyToStack env nf@(NType fc _) _ = pure nf

214 |     evalLocClosure : {auto c : Ref Ctxt Defs} ->

215 |                      {free : _} ->

216 |                      Env Term free ->

217 |                      FC -> Maybe Bool ->

218 |                      Stack free ->

219 |                      Closure free ->

220 |                      Core (NF free)

221 |     evalLocClosure env fc mrig stk (MkClosure opts locs' env' tm')

222 |         = evalWithOpts defs opts env' locs' tm' stk

223 |     evalLocClosure {free} env fc mrig stk (MkNFClosure opts env' nf)

224 |         = applyToStack env' nf stk

226 |     evalLocal : {auto c : Ref Ctxt Defs} ->

227 |                 {free : _} ->

228 |                 Env Term free ->

229 |                 FC -> Maybe Bool ->

230 |                 (idx : Nat) -> (0 p : IsVar nm idx (vars ++ free)) ->

231 |                 Stack free ->

232 |                 LocalEnv free vars ->

233 |                 Core (NF free)

234 |     -- If it's one of the free variables, we are done unless the free

235 |     -- variable maps to a let-binding

236 |     evalLocal env fc mrig idx prf stk []

237 |         = if not (holesOnly topopts || argHolesOnly topopts)

238 |              -- if we know it's not a let, no point in even running `getBinder`

239 |              && fromMaybe True mrig

240 |              then

241 |                case getBinder prf env of

242 |                     Let _ _ val _ => eval env LocalEnv.empty val stk

243 |                     _ => pure $ NApp fc (NLocal mrig idx prf) stk

244 |              else pure $ NApp fc (NLocal mrig idx prf) stk

245 |     evalLocal env fc mrig Z First stk (x :: locs)

246 |         = evalLocClosure env fc mrig stk x

247 |     evalLocal env fc mrig (S idx) (Later p) stk (_ :: locs)

248 |         = evalLocal env fc mrig idx p stk locs

250 |     updateLocal : EvalOpts -> Env Term free ->

251 |                   (idx : Nat) -> (0 p : IsVar nm idx (vars ++ free)) ->

252 |                   LocalEnv free vars -> NF free ->

253 |                   LocalEnv free vars

254 |     updateLocal opts env Z First (x :: locs) nf

255 |         = MkNFClosure opts env nf :: locs

256 |     updateLocal opts env (S idx) (Later p) (x :: locs) nf

257 |         = x :: updateLocal opts env idx p locs nf

258 |     updateLocal _ _ _ _ locs nf = locs

260 |     evalMeta : {auto c : Ref Ctxt Defs} ->

261 |                {free : _} ->

262 |                Env Term free ->

263 |                FC -> Name -> Int -> List (Closure free) ->

264 |                Stack free -> Core (NF free)

265 |     evalMeta env fc nm i args stk

266 |         = let args' = if isNil stk then map (EmptyFC,) args

267 |                          else map (EmptyFC,) args ++ stk

268 |                         in

269 |               evalRef env True fc Func (Resolved i) args'

270 |                           (NApp fc (NMeta nm i args) stk)

272 |     -- The commented out logging here might still be useful one day, but

273 |     -- evalRef is used a lot and even these tiny checks turn out to be

274 |     -- worth skipping if we can

275 |     evalRef : {auto c : Ref Ctxt Defs} ->

276 |               {free : _} ->

277 |               Env Term free ->

278 |               (isMeta : Bool) ->

279 |               FC -> NameType -> Name -> Stack free -> (def : Lazy (NF free)) ->

280 |               Core (NF free)

281 |     evalRef env meta fc (DataCon tag arity) fn stk def

282 |         = do -- logC "eval.ref.data" 50 $ do fn' <- toFullNames fn -- Can't use ! here, it gets lifted too far

283 |              --                             pure $ "Found data constructor: " ++ show fn'

284 |              pure $ NDCon fc fn tag arity stk

285 |     evalRef env meta fc (TyCon arity) fn stk def

286 |         = do -- logC "eval.ref.type" 50 $ do fn' <- toFullNames fn

287 |              --                             pure $ "Found type constructor: " ++ show fn'

288 |              pure $ ntCon fc fn arity stk

289 |     evalRef env meta fc Bound fn stk def

290 |         = do -- logC "eval.ref.bound" 50 $ do fn' <- toFullNames fn

291 |              --                              pure $ "Found bound variable: " ++ show fn'

292 |              pure def

293 |     evalRef env meta fc nt@Func n stk def

294 |         = do -- logC "eval.ref" 50 $ do n' <- toFullNames n

295 |              --                        pure $ "Found function: " ++ show n'

296 |              Just res <- lookupCtxtExact n (gamma defs)

297 |                   | Nothing => do logC "eval.stuck.outofscope" 5 $ do n' <- toFullNames n

298 |                                                                       pure $ "Stuck function: " ++ show n'

299 |                                   pure def

300 |              let redok1 = evalAll topopts

301 |              let redok2 = reducibleInAny (currentNS defs :: nestedNS defs)

302 |                                          (fullname res)

303 |                                          (collapseDefault $ visibility res)

304 |              -- want to shortcut that second check, if we're evaluating

305 |              -- everything, so don't let bind unless we need that log!

306 |              let redok = redok1 || redok2

307 |              checkTimer -- If we're going to time out anywhere, it'll be

308 |                         -- when evaluating something recursive, so this is a

309 |                         -- good place to check

310 |              unless redok2 $ logC "eval.stuck" 5 $ do n' <- toFullNames n

311 |                                                       pure $ "Stuck function: \{show n'}"

312 |              if redok

313 |                 then do

314 |                    Just opts' <- updateLimit nt n topopts

315 |                         | Nothing => do log "eval.stuck" 10 $ "Function \{show n} past reduction limit"

316 |                                         pure def -- name is past reduction limit

317 |                    nf <- evalDef env opts' meta fc

318 |                            (multiplicity res) (definition res) (flags res) stk def

319 |                    -- logC "eval.ref" 50 $ do n' <- toFullNames n

320 |                    --                         nf <- toFullNames nf

321 |                    --                         pure "Reduced \{show n'} to \{show nf}"

322 |                    pure nf

323 |                 else pure def

325 |     -- TODO note the list of closures is stored RTL

326 |     getCaseBound : List (Closure free) ->

327 |                    (args : Scope) ->

328 |                    LocalEnv free more ->

329 |                    Maybe (LocalEnv free (Scope.addInner more args))

330 |     getCaseBound []            []        loc = Just loc

331 |     getCaseBound []            (_ :: _)  loc = Nothing -- mismatched arg length

332 |     getCaseBound (arg :: args) []        loc = Nothing -- mismatched arg length

333 |     getCaseBound (arg :: args) (n :: ns) loc = (arg ::) <$> getCaseBound args ns loc

335 |     -- Returns the case term from the matched pattern with the LocalEnv (arguments from constructor pattern ConCase)

336 |     evalConAlt : {auto c : Ref Ctxt Defs} ->

337 |                  {more, free : _} ->

338 |                  Env Term free ->

339 |                  LocalEnv free more -> EvalOpts -> FC ->

340 |                  Stack free ->

341 |                  (args : List Name) ->

342 |                  List (Closure free) ->

343 |                  CaseTree (Scope.addInner more args) ->

344 |                  Core (CaseResult (TermWithEnv free))

345 |     evalConAlt env loc opts fc stk args args' sc

346 |          = do let Just bound = getCaseBound args' args loc

347 |                    | Nothing => pure GotStuck

348 |               evalTree env bound opts fc stk sc

350 |     tryAlt : {auto c : Ref Ctxt Defs} ->

351 |              {free, more : _} ->

352 |              Env Term free ->

353 |              LocalEnv free more -> EvalOpts -> FC ->

354 |              Stack free -> NF free -> CaseAlt more ->

355 |              Core (CaseResult (TermWithEnv free))

356 |     -- Dotted values should still reduce at compile time

357 |     tryAlt {more} env loc opts fc stk (NErased _ (Dotted tm)) alt

358 |          = tryAlt {more} env loc opts fc stk tm alt

359 |     -- Ordinary constructor matching

360 |     tryAlt {more} env loc opts fc stk (NDCon _ nm tag' arity args') (ConCase x tag args sc)

361 |          = if tag == tag'

362 |               then evalConAlt env loc opts fc stk args (map snd args') sc

363 |               else pure NoMatch

364 |     -- Type constructor matching, in typecase

365 |     tryAlt {more} env loc opts fc stk (NTCon _ nm arity args') (ConCase nm' tag args sc)

366 |          = if nm == nm'

367 |               then evalConAlt env loc opts fc stk args (map snd args') sc

368 |               else pure NoMatch

369 |     -- Primitive type matching, in typecase

370 |     tryAlt env loc opts fc stk (NPrimVal _ c) (ConCase nm tag args sc)

371 |          = case args of -- can't just test for it in the `if` for typing reasons

372 |              [] => if UN (Basic $ show c) == nm

373 |                    then evalTree env loc opts fc stk sc

374 |                    else pure NoMatch

375 |              _ => pure NoMatch

376 |     -- Type of type matching, in typecase

377 |     tryAlt env loc opts fc stk (NType {}) (ConCase (UN (Basic "Type")) tag [] sc)

378 |          = evalTree env loc opts fc stk sc

379 |     tryAlt env loc opts fc stk (NType {}) (ConCase {})

380 |          = pure NoMatch

381 |     -- Arrow matching, in typecase

382 |     tryAlt {more}

383 |            env loc opts fc stk (NBind pfc x (Pi fc' r e aty) scty) (ConCase (UN (Basic "->")) tag [s,t] sc)

384 |        = evalConAlt {more} env loc opts fc stk [s,t]

385 |                   [aty,

386 |                    MkNFClosure opts env (NBind pfc x (Lam fc' r e aty) scty)]

387 |                   sc

388 |     tryAlt {more}

389 |            env loc opts fc stk (NBind pfc x (Pi fc' r e aty) scty) (ConCase nm tag args sc)

390 |        = pure NoMatch

391 |     -- Delay matching

392 |     tryAlt env loc opts fc stk (NDelay _ _ ty arg) (DelayCase tyn argn sc)

393 |          = evalTree env (ty :: arg :: loc) opts fc stk sc

394 |     -- Constant matching

395 |     tryAlt env loc opts fc stk (NPrimVal _ c') (ConstCase c sc)

396 |          = if c == c' then evalTree env loc opts fc stk sc

397 |                       else pure NoMatch

398 |     -- Default case matches against any *concrete* value

399 |     tryAlt env loc opts fc stk val (DefaultCase sc)

400 |          = if concrete val

401 |               then evalTree env loc opts fc stk sc

402 |               else pure GotStuck

403 |       where

404 |         concrete : NF free -> Bool

405 |         concrete (NDCon {}) = True

406 |         concrete (NTCon {}) = True

407 |         concrete (NPrimVal {}) = True

408 |         concrete (NBind {}) = True

409 |         concrete (NType {}) = True

410 |         concrete (NDelay {}) = True

411 |         concrete _ = False

412 |     tryAlt _ _ _ _ _ _ _ = pure GotStuck

414 |     findAlt : {auto c : Ref Ctxt Defs} ->

415 |               {args, free : _} ->

416 |               Env Term free ->

417 |               LocalEnv free args -> EvalOpts -> FC ->

418 |               Stack free -> NF free -> List (CaseAlt args) ->

419 |               Core (CaseResult (TermWithEnv free))

420 |     findAlt env loc opts fc stk val [] = do

421 |       log "eval.casetree.stuck" 2 "Ran out of alternatives"

422 |       pure GotStuck

423 |     findAlt env loc opts fc stk val (x :: xs)

424 |          = do res@(Result {}) <- tryAlt env loc opts fc stk val x

425 |                    | NoMatch => findAlt env loc opts fc stk val xs

426 |                    | GotStuck => do

427 |                        logC "eval.casetree.stuck" 5 $ do

428 |                          val <- toFullNames val

429 |                          x <- toFullNames x

430 |                          pure $ "Got stuck matching \{show val} against \{show x}"

431 |                        pure GotStuck

432 |               pure res

434 |     evalTree : {auto c : Ref Ctxt Defs} ->

435 |                {args, free : _} -> Env Term free -> LocalEnv free args ->

436 |                EvalOpts -> FC ->

437 |                Stack free -> CaseTree args ->

438 |                Core (CaseResult (TermWithEnv free))

439 |     evalTree env loc opts fc stk (Case {name} idx x _ alts)

440 |       = do xval <- evalLocal env fc Nothing idx (embedIsVar x) [] loc

441 |            -- we have not defined quote yet (it depends on eval itself) so we show the NF

442 |            -- i.e. only the top-level constructor.

443 |            logC "eval.casetree" 5 $ do

444 |              xval <- toFullNames xval

445 |              pure "Evaluated \{show name} to \{show xval}"

446 |            let loc' = updateLocal opts env idx (embedIsVar x) loc xval

447 |            findAlt env loc' opts fc stk xval alts

448 |     evalTree env loc opts fc stk (STerm _ tm)

449 |           = pure (Result $ MkTermEnv loc $ embed tm)

450 |     evalTree env loc opts fc stk _ = pure GotStuck

452 |     -- Take arguments from the stack, as long as there's enough.

453 |     -- Returns the arguments, and the rest of the stack

454 |     takeFromStack : (arity : Nat) -> Stack free ->

455 |                     Maybe (Vect arity (Closure free), Stack free)

456 |     takeFromStack arity stk = takeStk arity stk []

457 |       where

458 |         takeStk : (remain : Nat) -> Stack free ->

459 |                   Vect got (Closure free) ->

460 |                   Maybe (Vect (got + remain) (Closure free), Stack free)

461 |         takeStk {got} Z stk acc = Just (rewrite plusZeroRightNeutral got in

462 |                                     reverse acc, stk)

463 |         takeStk (S k) [] acc = Nothing

464 |         takeStk {got} (S k) (arg :: stk) acc

465 |            = rewrite sym (plusSuccRightSucc got k) in

466 |                      takeStk k stk (snd arg :: acc)

468 |     argsFromStack : (args : List Name) ->

469 |                     Stack free ->

470 |                     Maybe (LocalEnv free args, Stack free)

471 |     argsFromStack [] stk = Just ([], stk)

472 |     argsFromStack (n :: ns) [] = Nothing

473 |     argsFromStack (n :: ns) (arg :: args)

474 |          = do (loc', stk') <- argsFromStack ns args

475 |               pure (snd arg :: loc', stk')

477 |     evalOp : {auto c : Ref Ctxt Defs} ->

478 |              {arity, free : _} ->

479 |              (Vect arity (NF free) -> Maybe (NF free)) ->

480 |              Stack free -> (def : Lazy (NF free)) ->

481 |              Core (NF free)

482 |     evalOp {arity} fn stk def

483 |         = case takeFromStack arity stk of

484 |                -- Stack must be exactly the right height

485 |                Just (args, []) =>

486 |                   do argsnf <- evalAll args

487 |                      pure $ case fn argsnf of

488 |                           Nothing => def

489 |                           Just res => res

490 |                _ => pure def

491 |       where

492 |         -- No traverse for Vect in Core...

493 |         evalAll : Vect n (Closure free) -> Core (Vect n (NF free))

494 |         evalAll [] = pure []

495 |         evalAll (c :: cs) = pure $ !(evalClosure defs c) :: !(evalAll cs)

497 |     evalDef : {auto c : Ref Ctxt Defs} ->

498 |               {free : _} ->

499 |               Env Term free -> EvalOpts ->

500 |               (isMeta : Bool) -> FC ->

501 |               RigCount -> Def -> List DefFlag ->

502 |               Stack free -> (def : Lazy (NF free)) ->

503 |               Core (NF free)

504 |     evalDef env opts meta fc rigd (PMDef r args tree _ _) flags stk def

505 |        -- If evaluating the definition fails (e.g. due to a case being

506 |        -- stuck) return the default.

507 |        -- We can use the definition if one of the following is true:

508 |        --   + The 'alwayReduce' flag (r) is set

509 |        --   + We're not in 'holesOnly', 'argHolesOnly' or 'tcInline'

510 |        --         (that's the default mode)

511 |        --   + It's a metavariable and not in Rig0

512 |        --   + It's a metavariable and we're not in 'argHolesOnly'

513 |        --   + It's inlinable and we're in 'tcInline'

514 |         = if alwaysReduce r

515 |              || (not (holesOnly opts || argHolesOnly opts || tcInline opts))

516 |              || (meta && not (isErased rigd))

517 |              || (meta && holesOnly opts)

518 |              || (tcInline opts && elem TCInline flags)

519 |              then case argsFromStack args stk of

520 |                        Nothing => do logC "eval.def.underapplied" 50 $ do

521 |                                        def <- toFullNames def

522 |                                        pure "Cannot reduce under-applied \{show def}"

523 |                                      pure def

524 |                        Just (locs', stk') =>

525 |                             do (Result (MkTermEnv newLoc res)) <- evalTree env locs' opts fc stk' tree

526 |                                     | _ => do logC "eval.def.stuck" 50 $ do

527 |                                                 def <- toFullNames def

528 |                                                 pure "evalTree failed on \{show def}"

529 |                                               pure def

530 |                                case fuel opts of

531 |                                     Nothing => evalWithOpts defs opts env newLoc res stk'

532 |                                     Just Z => log "eval.def.stuck" 50 "Recursion depth limit exceeded"

533 |                                               >> pure def

534 |                                     Just (S k) =>

535 |                                         do let opts' = { fuel := Just k } opts

536 |                                            evalWithOpts defs opts' env newLoc res stk'

537 |              else do -- logC "eval.def.stuck" 50 $ do

538 |                      --   def <- toFullNames def

539 |                      --   pure $ unlines [ "Refusing to reduce \{show def}:"

540 |                      --                  , "  holesOnly   : \{show $ holesOnly opts}"

541 |                      --                  , "  argHolesOnly: \{show $ argHolesOnly opts}"

542 |                      --                  , "  tcInline    : \{show $ tcInline opts}"

543 |                      --                  , "  meta        : \{show meta}"

544 |                      --                  , "  rigd        : \{show rigd}"

545 |                      --                  ]

546 |                      pure def

547 |     evalDef env opts meta fc rigd (Builtin op) flags stk def

548 |         = evalOp (getOp op) stk def

549 |     -- All other cases, use the default value, which is already applied to

550 |     -- the stack

551 |     evalDef env opts meta fc rigd def flags stk orig = do

552 |       logC "eval.def.stuck" 50 $ do

553 |         orig <- toFullNames orig

554 |         pure "Cannot reduce def \{show orig}: it is a \{show def}"

555 |       pure orig

559 | evalWithOpts {vars} defs opts = eval {vars} defs opts

561 | evalClosure defs (MkClosure opts locs env tm)

562 |     = eval defs opts env locs tm []

563 | evalClosure defs (MkNFClosure opts env nf)

564 |     = applyToStack defs opts env nf []

567 | evalClosureWithOpts : {auto c : Ref Ctxt Defs} ->

568 |                       {free : _} ->

569 |                       Defs -> EvalOpts -> Closure free -> Core (NF free)

570 | evalClosureWithOpts defs opts (MkClosure _ locs env tm)

571 |     = eval defs opts env locs tm []

572 | evalClosureWithOpts defs opts (MkNFClosure _ env nf)

573 |     = applyToStack defs opts env nf []

576 | nf : {auto c : Ref Ctxt Defs} ->

577 |      {vars : _} ->

578 |      Defs -> Env Term vars -> Term vars -> Core (NF vars)

579 | nf defs env tm = eval defs defaultOpts env LocalEnv.empty tm []

582 | nfOpts : {auto c : Ref Ctxt Defs} ->

583 |          {vars : _} ->

584 |          EvalOpts -> Defs -> Env Term vars -> Term vars -> Core (NF vars)

585 | nfOpts opts defs env tm = eval defs opts env LocalEnv.empty tm []

588 | gnf : {vars : _} ->

589 |       Env Term vars -> Term vars -> Glued vars

590 | gnf env tm

591 |     = MkGlue True

592 |              (pure tm)

593 |              (\c => do defs <- get Ctxt

594 |                        nf defs env tm)

597 | gnfOpts : {vars : _} ->

598 |           EvalOpts -> Env Term vars -> Term vars -> Glued vars

599 | gnfOpts opts env tm

600 |     = MkGlue True

601 |              (pure tm)

602 |              (\c => do defs <- get Ctxt

603 |                        nfOpts opts defs env tm)

606 | gType : FC -> Name -> Glued vars

607 | gType fc u = MkGlue True (pure (TType fc u)) (const (pure (NType fc u)))

610 | gErased : FC -> Glued vars

611 | gErased fc = MkGlue True (pure (Erased fc Placeholder)) (const (pure (NErased fc Placeholder)))

615 | continueNF : {auto c : Ref Ctxt Defs} ->

616 |              {vars : _} ->

617 |              Defs -> Env Term vars -> NF vars -> Core (NF vars)

618 | continueNF defs env stuck

619 |    = applyToStack defs defaultOpts env stuck []