0 | module Core.Value

  2 | import Core.Context

  3 | import Core.Env

  5 | import Data.List.Quantifiers

  7 | %default covering

  9 | public export

 10 | data EvalOrder = CBV | CBN

 12 | public export

 13 | record EvalOpts where

 14 |   constructor MkEvalOpts

 15 |   holesOnly : Bool -- only evaluate hole solutions

 16 |   argHolesOnly : Bool -- only evaluate holes which are relevant arguments

 17 |   removeAs : Bool -- reduce 'as' patterns (don't do this on LHS)

 18 |   evalAll : Bool -- evaluate everything, including private names

 19 |   tcInline : Bool -- inline for totality checking

 20 |   fuel : Maybe Nat -- Limit for recursion depth

 21 |   reduceLimit : List (Name, Nat) -- reduction limits for given names. If not

 22 |                      -- present, no limit

 23 |   strategy : EvalOrder

 26 | defaultOpts : EvalOpts

 27 | defaultOpts = MkEvalOpts

 28 |     { holesOnly = False

 29 |     , argHolesOnly = False

 30 |     , removeAs = True

 31 |     , evalAll = False

 32 |     , tcInline = False

 33 |     , fuel = Nothing

 34 |     , reduceLimit = []

 35 |     , strategy = CBN

 36 |     }

 39 | withHoles : EvalOpts

 40 | withHoles = MkEvalOpts

 41 |     { holesOnly = True

 42 |     , argHolesOnly = True

 43 |     , removeAs = False

 44 |     , evalAll = False

 45 |     , tcInline = False

 46 |     , fuel = Nothing

 47 |     , reduceLimit = []

 48 |     , strategy = CBN

 49 |     }

 52 | withAll : EvalOpts

 53 | withAll = MkEvalOpts

 54 |     { holesOnly = False

 55 |     , argHolesOnly = False

 56 |     , removeAs = True

 57 |     , evalAll = True

 58 |     , tcInline = False

 59 |     , fuel = Nothing

 60 |     , reduceLimit = []

 61 |     , strategy = CBN

 62 |     }

 65 | withArgHoles : EvalOpts

 66 | withArgHoles = MkEvalOpts

 67 |     { holesOnly = False

 68 |     , argHolesOnly = True

 69 |     , removeAs = False

 70 |     , evalAll = False

 71 |     , tcInline = False

 72 |     , fuel = Nothing

 73 |     , reduceLimit = []

 74 |     , strategy = CBN

 75 |     }

 78 | tcOnly : EvalOpts

 79 | tcOnly = { tcInline := True } withArgHoles

 82 | onLHS : EvalOpts

 83 | onLHS = { removeAs := False } defaultOpts

 86 | cbn : EvalOpts

 87 | cbn = defaultOpts

 90 | cbv : EvalOpts

 91 | cbv = { strategy := CBV } defaultOpts

 94 |   -- TODO swap arguments and type as `Scope -> Scoped`

 95 |   public export

 96 |   LocalEnv : Scope -> Scope -> Type

 97 |   LocalEnv free = All (\_ => Closure free)

 99 |   public export

100 |   data Closure : Scoped where

101 |        MkClosure : {vars : _} ->

102 |                    (opts : EvalOpts) ->

103 |                    LocalEnv free vars ->

104 |                    Env Term free ->

105 |                    Term (Scope.addInner free vars) -> Closure free

106 |        MkNFClosure : EvalOpts -> Env Term free -> NF free -> Closure free

108 |   -- The head of a value: things you can apply arguments to

109 |   public export

110 |   data NHead : Scoped where

111 |        NLocal : Maybe Bool -> (idx : Nat) -> (0 p : IsVar nm idx vars) ->

112 |                 NHead vars

113 |        NRef   : NameType -> Name -> NHead vars

114 |        NMeta  : Name -> Int -> List (Closure vars) -> NHead vars

117 |   -- Values themselves. 'Closure' is an unevaluated thunk, which means

118 |   -- we can wait until necessary to reduce constructor arguments

119 |   public export

120 |   data NF : Scoped where

121 |        NBind    : FC -> (x : Name) -> Binder (Closure vars) ->

122 |                   (Defs -> Closure vars -> Core (NF vars)) -> NF vars

123 |        -- Each closure is associated with the file context of the App node that

124 |        -- had it as an argument. It's necessary so as to not lose file context

125 |        -- information when creating the normal form.

126 |        NApp     : FC -> NHead vars -> List (FC, Closure vars) -> NF vars

127 |        NDCon    : FC -> Name -> (tag : Int) -> (arity : Nat) ->

128 |                   List (FC, Closure vars) -> NF vars

129 |                   -- TODO it looks like the list of closures is stored in spine order, c.f. `getCaseBounds`

130 |        NTCon    : FC -> Name -> (arity : Nat) ->

131 |                   List (FC, Closure vars) -> NF vars

132 |        NAs      : FC -> UseSide -> NF vars -> NF vars -> NF vars

133 |        NDelayed : FC -> LazyReason -> NF vars -> NF vars

134 |        NDelay   : FC -> LazyReason -> Closure vars -> Closure vars -> NF vars

135 |        NForce   : FC -> LazyReason -> NF vars -> List (FC, Closure vars) -> NF vars

136 |        NPrimVal : FC -> Constant -> NF vars

137 |        NErased  : FC -> WhyErased (NF vars) -> NF vars

138 |        NType    : FC -> Name -> NF vars

140 | %name LocalEnv lenv

141 | %name Closure cl

142 | %name NHead hd

143 | %name NF nf

145 | public export

146 | ClosedClosure : Type

147 | ClosedClosure = Closure []

149 | public export

150 | ClosedNF : Type

151 | ClosedNF = NF []

153 | namespace LocalEnv

154 |   public export

155 |   empty : LocalEnv free Scope.empty

156 |   empty = []

159 | ntCon : FC -> Name -> Nat -> List (FC, Closure vars) -> NF vars

162 | ntCon fc (UN (Basic "Type")) Z [] = NType fc (MN "top" 0)

163 | ntCon fc n Z [] = case isConstantType n of

164 |   Just c => NPrimVal fc $ PrT c

165 |   Nothing => NTCon fc n Z []

166 | ntCon fc n arity args = NTCon fc n arity args

169 | getLoc : NF vars -> FC

170 | getLoc (NBind fc _ _ _) = fc

171 | getLoc (NApp fc _ _) = fc

172 | getLoc (NDCon fc _ _ _ _) = fc

173 | getLoc (NTCon fc _ _ _) = fc

174 | getLoc (NAs fc _ _ _) = fc

175 | getLoc (NDelayed fc _ _) = fc

176 | getLoc (NDelay fc _ _ _) = fc

177 | getLoc (NForce fc _ _ _) = fc

178 | getLoc (NPrimVal fc _) = fc

179 | getLoc (NErased fc i) = fc

180 | getLoc (NType fc _) = fc

183 | {free : _} -> Show (NHead free) where

184 |   show (NLocal _ idx p) = show (nameAt p) ++ "[" ++ show idx ++ "]"

185 |   show (NRef _ n) = show n

186 |   show (NMeta n _ args) = "?" ++ show n ++ "_[" ++ show (length args) ++ " closures]"

188 | Show (Closure free) where

189 |   show _ = "[closure]"

192 | HasNames (NHead free) where

193 |   full defs (NRef nt n) = NRef nt <$> full defs n

194 |   full defs hd = pure hd

196 |   resolved defs (NRef nt n) = NRef nt <$> resolved defs n

197 |   resolved defs hd = pure hd

200 | HasNames (NF free) where

201 |   full defs (NBind fc x bd f) = pure $ NBind fc x bd f

202 |   full defs (NApp fc hd xs) = pure $ NApp fc !(full defs hd) xs

203 |   full defs (NDCon fc n tag arity xs) = pure $ NDCon fc !(full defs n) tag arity xs

204 |   full defs (NTCon fc n arity xs) = pure $ NTCon fc !(full defs n) arity xs

205 |   full defs (NAs fc side nf nf1) = pure $ NAs fc side !(full defs nf) !(full defs nf1)

206 |   full defs (NDelayed fc lz nf) = pure $ NDelayed fc lz !(full defs nf)

207 |   full defs (NDelay fc lz cl cl1) = pure $ NDelay fc lz cl cl1

208 |   full defs (NForce fc lz nf xs) = pure $ NForce fc lz !(full defs nf) xs

209 |   full defs (NPrimVal fc cst) = pure $ NPrimVal fc cst

210 |   full defs (NErased fc imp) = pure $ NErased fc imp

211 |   full defs (NType fc n) = pure $ NType fc !(full defs n)

213 |   resolved defs (NBind fc x bd f) = pure $ NBind fc x bd f

214 |   resolved defs (NApp fc hd xs) = pure $ NApp fc !(resolved defs hd) xs

215 |   resolved defs (NDCon fc n tag arity xs) = pure $ NDCon fc !(resolved defs n) tag arity xs

216 |   resolved defs (NTCon fc n arity xs) = pure $ NTCon fc !(resolved defs n) arity xs

217 |   resolved defs (NAs fc side nf nf1) = pure $ NAs fc side !(resolved defs nf) !(resolved defs nf1)

218 |   resolved defs (NDelayed fc lz nf) = pure $ NDelayed fc lz !(resolved defs nf)

219 |   resolved defs (NDelay fc lz cl cl1) = pure $ NDelay fc lz cl cl1

220 |   resolved defs (NForce fc lz nf xs) = pure $ NForce fc lz !(resolved defs nf) xs

221 |   resolved defs (NPrimVal fc cst) = pure $ NPrimVal fc cst

222 |   resolved defs (NErased fc imp) = pure $ NErased fc imp

223 |   resolved defs (NType fc n) = pure $ NType fc !(resolved defs n)

227 | {free : _} -> Show (NF free) where

228 |   show (NBind _ x (Lam _ c info ty) _)

229 |     = "\\" ++ withPiInfo info (showCount c ++ show x ++ " : " ++ show ty) ++

230 |       " => [closure]"

231 |   show (NBind _ x (Let _ c val ty) _)

232 |     = "let " ++ showCount c ++ show x ++ " : " ++ show ty ++

233 |       " = " ++ show val ++ " in [closure]"

234 |   show (NBind _ x (Pi _ c info ty) _)

235 |     = withPiInfo info (showCount c ++ show x ++ " : " ++ show ty) ++

236 |       " -> [closure]"

237 |   show (NBind _ x (PVar _ c info ty) _)

238 |     = withPiInfo info ("pat " ++ showCount c ++ show x ++ " : " ++ show ty) ++

239 |       " => [closure]"

240 |   show (NBind _ x (PLet _ c val ty) _)

241 |     = "plet " ++ showCount c ++ show x ++ " : " ++ show ty ++

242 |       " = " ++ show val ++ " in [closure]"

243 |   show (NBind _ x (PVTy _ c ty) _)

244 |     = "pty " ++ showCount c ++ show x ++ " : " ++ show ty ++

245 |       " => [closure]"

246 |   show (NApp _ hd args) = show hd ++ " [" ++ show (length args) ++ " closures]"

247 |   show (NDCon _ n _ _ args) = show n ++ " [" ++ show (length args) ++ " closures]"

248 |   show (NTCon _ n _ args) = show n ++ " [" ++ show (length args) ++ " closures]"

249 |   show (NAs _ _ n tm) = show n ++ "@" ++ show tm

250 |   show (NDelayed _ _ tm) = "%Delayed " ++ show tm

251 |   show (NDelay {}) = "%Delay [closure]"

252 |   show (NForce _ _ tm args) = "%Force " ++ show tm ++ " [" ++ show (length args) ++ " closures]"

253 |   show (NPrimVal _ c) = show c

254 |   show (NErased {}) = "[__]"

255 |   show (NType {}) = "Type"