0 | module Core.Normalise

  2 | import public Core.Normalise.Convert

  3 | import public Core.Normalise.Eval

  4 | import public Core.Normalise.Quote

  6 | import Core.Context.Log

  7 | import Core.Env

  8 | import Core.Value

 10 | %default covering

 15 | normalisePis : {auto c : Ref Ctxt Defs} ->

 16 |                {vars : Scope} ->

 17 |                Defs -> Env Term vars -> Term vars -> Core (Term vars)

 18 | normalisePis defs env tm

 19 |     = do tmnf <- nf defs env tm

 20 |          case tmnf of

 21 |               NBind _ _ (Pi {}) _ => quoteWithPi defs env tmnf

 22 |               _ => pure tm

 25 | glueBack : {auto c : Ref Ctxt Defs} ->

 26 |            {vars : _} ->

 27 |            Defs -> Env Term vars -> NF vars -> Glued vars

 28 | glueBack defs env nf

 29 |     = MkGlue False

 30 |              (do empty <- clearDefs defs

 31 |                  quote empty env nf)

 32 |              (const (pure nf))

 35 | glueClosure : {auto c : Ref Ctxt Defs} ->

 36 |               {vars : _} ->

 37 |               Defs -> Env Term vars -> Closure vars -> Glued vars

 38 | glueClosure defs env clos

 39 |     = MkGlue False

 40 |              (do empty <- clearDefs defs

 41 |                  quote empty env clos)

 42 |              (const (evalClosure defs clos))

 45 | normalise : {auto c : Ref Ctxt Defs} ->

 46 |             {free : _} ->

 47 |             Defs -> Env Term free -> Term free -> Core (Term free)

 48 | normalise defs env tm = quote defs env !(nf defs env tm)

 51 | normaliseOpts : {auto c : Ref Ctxt Defs} ->

 52 |                 {free : _} ->

 53 |                 EvalOpts -> Defs -> Env Term free -> Term free -> Core (Term free)

 54 | normaliseOpts opts defs env tm

 55 |     = quote defs env !(nfOpts opts defs env tm)

 58 | normaliseHoles : {auto c : Ref Ctxt Defs} ->

 59 |                  {free : _} ->

 60 |                  Defs -> Env Term free -> Term free -> Core (Term free)

 61 | normaliseHoles defs env tm

 62 |     = quote defs env !(nfOpts withHoles defs env tm)

 65 | normaliseLHS : {auto c : Ref Ctxt Defs} ->

 66 |                {free : _} ->

 67 |                Defs -> Env Term free -> Term free -> Core (Term free)

 68 | normaliseLHS defs env (Bind fc n b sc)

 69 |     = pure $ Bind fc n b !(normaliseLHS defs (b :: env) sc)

 70 | normaliseLHS defs env tm

 71 |     = quote defs env !(nfOpts onLHS defs env tm)

 74 | tryNormaliseSizeLimit : {auto c : Ref Ctxt Defs} ->

 75 |                      {free : _} ->

 76 |                      Defs -> Nat ->

 77 |                      Env Term free -> Term free -> Core (Term free)

 78 | tryNormaliseSizeLimit defs limit env tm

 79 |     = do tm' <- nf defs env tm

 80 |          quoteOpts (MkQuoteOpts False False (Just limit)) defs env tm'

 85 | normaliseSizeLimit : {auto c : Ref Ctxt Defs} ->

 86 |                      {free : _} ->

 87 |                      Defs -> Nat ->

 88 |                      Env Term free -> Term free -> Core (Term free)

 89 | normaliseSizeLimit defs limit env tm

 90 |     = catch (do tm' <- nf defs env tm

 91 |                 quoteOpts (MkQuoteOpts False False (Just limit)) defs env tm')

 92 |             (\err => pure tm)

 95 | normaliseArgHoles : {auto c : Ref Ctxt Defs} ->

 96 |                     {free : _} ->

 97 |                     Defs -> Env Term free -> Term free -> Core (Term free)

 98 | normaliseArgHoles defs env tm

 99 |     = quote defs env !(nfOpts withArgHoles defs env tm)

102 | normaliseAll : {auto c : Ref Ctxt Defs} ->

103 |                {free : _} ->

104 |                Defs -> Env Term free -> Term free -> Core (Term free)

105 | normaliseAll defs env tm

106 |     = quote defs env !(nfOpts withAll defs env tm)

112 | normaliseScope : {auto c : Ref Ctxt Defs} ->

113 |                  {free : _} ->

114 |                  Defs -> Env Term free -> Term free -> Core (Term free)

115 | normaliseScope defs env (Bind fc n b sc)

116 |     = pure $ Bind fc n b !(normaliseScope defs (b :: env) sc)

117 | normaliseScope defs env tm = normalise defs env tm

120 | etaContract : {auto _ : Ref Ctxt Defs} ->

121 |               {vars : _} -> Term vars -> Core (Term vars)

122 | etaContract tm = do

123 |   defs <- get Ctxt

124 |   logTerm "eval.eta" 5 "Attempting to eta contract subterms of" tm

125 |   nf <- normalise defs (mkEnv EmptyFC _) tm

126 |   logTerm "eval.eta" 5 "Evaluated to" nf

127 |   res <- mapTermM act tm

128 |   logTerm "eval.eta" 5 "Result of eta-contraction" res

129 |   pure res

131 |    where

133 |     act : {vars : _} -> Term vars -> Core (Term vars)

134 |     act tm = do

135 |       logTerm "eval.eta" 10 "  Considering" tm

136 |       case tm of

137 |         (Bind _ x (Lam {}) (App _ fn (Local _ _ Z _))) => do

138 |           logTerm "eval.eta" 10 "  Shrinking candidate" fn

139 |           let shrunk = shrink fn (Drop Refl)

140 |           case shrunk of

141 |             Nothing => do

142 |               log "eval.eta" 10 "  Failure!"

143 |               pure tm

144 |             Just tm' => do

145 |               logTerm "eval.eta" 10 "  Success!" tm'

146 |               pure tm'

147 |         _ => pure tm

150 | getValArity : Defs -> Env Term vars -> NF vars -> Core Nat

151 | getValArity defs env (NBind fc x (Pi {}) sc)

152 |     = pure (S !(getValArity defs env !(sc defs (toClosure defaultOpts env (Erased fc Placeholder)))))

153 | getValArity defs env val = pure 0

156 | getArity : {auto c : Ref Ctxt Defs} ->

157 |            {vars : _} ->

158 |            Defs -> Env Term vars -> Term vars -> Core Nat

159 | getArity defs env tm = getValArity defs env !(nf defs env tm)

163 | logNF : {vars : _} ->

164 |         {auto c : Ref Ctxt Defs} ->

165 |         LogTopic -> Nat -> Lazy String -> Env Term vars -> NF vars -> Core ()

166 | logNF s n msg env tmnf

167 |     = when !(logging s n) $

168 |         do defs <- get Ctxt

169 |            tm <- quote defs env tmnf

170 |            tm' <- toFullNames tm

171 |            logString s.topic n (msg ++ ": " ++ show tm')

176 | logTermNF' : {vars : _} ->

177 |              {auto c : Ref Ctxt Defs} ->

178 |              LogTopic ->

179 |              Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()

180 | logTermNF' s n msg env tm

181 |     = do defs <- get Ctxt

182 |          tmnf <- normaliseHoles defs env tm

183 |          tm' <- toFullNames tmnf

184 |          logString s.topic n (msg ++ ": " ++ show tm')

187 | logTermNF : {vars : _} ->

188 |             {auto c : Ref Ctxt Defs} ->

189 |             LogTopic ->

190 |             Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()

191 | logTermNF s n msg env tm

192 |     = when !(logging s n) $ logTermNF' s n msg env tm

195 | logGlue : {vars : _} ->

196 |           {auto c : Ref Ctxt Defs} ->

197 |           LogTopic ->

198 |           Nat -> Lazy String -> Glued vars -> Core ()

199 | logGlue s n msg gtm

200 |     = when !(logging s n) $

201 |         do defs <- get Ctxt

202 |            tm <- getTerm gtm

203 |            tm' <- toFullNames tm

204 |            logString s.topic n (msg ++ ": " ++ show tm')

207 | logGlueNF : {vars : _} ->

208 |             {auto c : Ref Ctxt Defs} ->

209 |             LogTopic ->

210 |             Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()

211 | logGlueNF s n msg env gtm

212 |     = when !(logging s n) $

213 |         do defs <- get Ctxt

214 |            tm <- getTerm gtm

215 |            tmnf <- normaliseHoles defs env tm

216 |            tm' <- toFullNames tmnf

217 |            logString s.topic n (msg ++ ": " ++ show tm')

220 | logEnv : {vars : _} ->

221 |          {auto c : Ref Ctxt Defs} ->

222 |          LogTopic ->

223 |          Nat -> String -> Env Term vars -> Core ()

224 | logEnv s n msg env

225 |     = when !(logging s n) $

226 |         do logString s.topic n msg

227 |            dumpEnv env

229 |   where

231 |     dumpEnv : {vs : Scope} -> Env Term vs -> Core ()

232 |     dumpEnv [] = pure ()

233 |     dumpEnv {vs = x :: _} (Let _ c val ty :: bs)

234 |         = do logTermNF' s n (msg ++ ": let " ++ show x) bs val

235 |              logTermNF' s n (msg ++ ":" ++ show c ++ " " ++ show x) bs ty

236 |              dumpEnv bs

237 |     dumpEnv {vs = x :: _} (b :: bs)

238 |         = do logTermNF' s n (msg ++ ":" ++ show (multiplicity b) ++ " " ++

239 |                            show (piInfo b) ++ " " ++

240 |                            show x) bs (binderType b)

241 |              dumpEnv bs

242 | replace' : {auto c : Ref Ctxt Defs} ->

243 |            {vars : _} ->

244 |            Int -> Defs -> Env Term vars ->

245 |            (lhs : NF vars) -> (parg : Term vars) -> (exp : NF vars) ->

246 |            Core (Term vars)

247 | replace' {vars} tmpi defs env lhs parg tm

248 |     = if !(convert defs env lhs tm)

249 |          then pure parg

250 |          else repSub tm

251 |   where

252 |     repArg : (Closure vars) -> Core (Term vars)

253 |     repArg c

254 |         = do tmnf <- evalClosure defs c

255 |              replace' tmpi defs env lhs parg tmnf

257 |     repSub : NF vars -> Core (Term vars)

258 |     repSub (NBind fc x b scfn)

259 |         = do b' <- traverse (\c => repSub !(evalClosure defs c)) b

260 |              let x' = MN "tmp" tmpi

261 |              sc' <- replace' (tmpi + 1) defs env lhs parg

262 |                              !(scfn defs (toClosure defaultOpts env (Ref fc Bound x')))

263 |              pure (Bind fc x b' (refsToLocals (Add x x' None) sc'))

264 |     repSub (NApp fc hd [])

265 |         = do empty <- clearDefs defs

266 |              quote empty env (NApp fc hd [])

267 |     repSub (NApp fc hd args)

268 |         = do args' <- traverse (traversePair repArg) args

269 |              pure $ applyStackWithFC

270 |                         !(replace' tmpi defs env lhs parg (NApp fc hd []))

271 |                         args'

272 |     repSub (NDCon fc n t a args)

273 |         = do args' <- traverse (traversePair repArg) args

274 |              empty <- clearDefs defs

275 |              pure $ applyStackWithFC

276 |                         !(quote empty env (NDCon fc n t a []))

277 |                         args'

278 |     repSub (NTCon fc n a args)

279 |         = do args' <- traverse (traversePair repArg) args

280 |              empty <- clearDefs defs

281 |              pure $ applyStackWithFC

282 |                         !(quote empty env (NTCon fc n a []))

283 |                         args'

284 |     repSub (NAs fc s a p)

285 |         = do a' <- repSub a

286 |              p' <- repSub p

287 |              pure (As fc s a' p')

288 |     repSub (NDelayed fc r tm)

289 |         = do tm' <- repSub tm

290 |              pure (TDelayed fc r tm')

291 |     repSub (NDelay fc r ty tm)

292 |         = do ty' <- replace' tmpi defs env lhs parg !(evalClosure defs ty)

293 |              tm' <- replace' tmpi defs env lhs parg !(evalClosure defs tm)

294 |              pure (TDelay fc r ty' tm')

295 |     repSub (NForce fc r tm args)

296 |         = do args' <- traverse (traversePair repArg) args

297 |              tm' <- repSub tm

298 |              pure $ applyStackWithFC (TForce fc r tm') args'

299 |     repSub (NErased fc (Dotted t))

300 |         = do t' <- repSub t

301 |              pure (Erased fc (Dotted t'))

302 |     repSub tm = do empty <- clearDefs defs

303 |                    quote empty env tm

306 | replace : {auto c : Ref Ctxt Defs} ->

307 |           {vars : _} ->

308 |           Defs -> Env Term vars ->

309 |           (orig : NF vars) -> (new : Term vars) -> (tm : NF vars) ->

310 |           Core (Term vars)

311 | replace = replace' 0

316 | normalisePrims : {auto c : Ref Ctxt Defs} -> {vs : _} ->

317 |                  -- size heuristic for when to unfold

318 |                  (Constant -> Bool) ->

319 |                  -- view to check whether an argument is a constant

320 |                  (arg -> Maybe Constant) ->

321 |                  -- Reduce everything (True) or just public export (False)

322 |                  Bool ->

323 |                  -- list of primitives

324 |                  List Name ->

325 |                  -- view of the potential redex

326 |                  (n : Name) ->          -- function name

327 |                  (args : List arg) ->   -- arguments from inside out (arg1, ..., argk)

328 |                  -- actual term to evaluate if needed

329 |                  (tm : Term vs) ->      -- original term (n arg1 ... argk)

330 |                  Env Term vs ->         -- evaluation environment

331 |                  -- output only evaluated if primitive

332 |                  Core (Maybe (Term vs))

333 | normalisePrims boundSafe viewConstant all prims n args tm env

334 |    = do let True = isPrimName prims !(getFullName n) -- is a primitive

335 |               | _ => pure Nothing

336 |         let (mc :: _) = reverse args -- with at least one argument

337 |               | _ => pure Nothing

338 |         let (Just c) = viewConstant mc -- that is a constant

339 |               | _ => pure Nothing

340 |         let True = boundSafe c -- that we should expand

341 |               | _ => pure Nothing

342 |         defs <- get Ctxt

343 |         tm <- if all

344 |                  then normaliseAll defs env tm

345 |                  else normalise defs env tm

346 |         pure (Just tm)