0 | module Core.Normalise.Quote

  2 | import Core.Context

  3 | import Core.Env

  4 | import Core.Normalise.Eval

  5 | import Core.Value

  7 | %default covering

 10 | data QVar : Type where

 12 | public export

 13 | record QuoteOpts where

 14 |   constructor MkQuoteOpts

 15 |   topLevel : Bool -- At the top level application

 16 |   patterns : Bool -- only quote as far as is useful to get LHS patterns.

 17 |                   -- That means, stop on encountering a block function or

 18 |                   -- local

 19 |   sizeLimit : Maybe Nat

 21 | public export

 22 | interface Quote tm where

 23 |     quote : {auto c : Ref Ctxt Defs} ->

 24 |             {vars : Scope} ->

 25 |             Defs -> Env Term vars -> tm vars -> Core (Term vars)

 26 |     quoteLHS : {auto c : Ref Ctxt Defs} ->

 27 |                {vars : Scope} ->

 28 |                Defs -> Env Term vars -> tm vars -> Core (Term vars)

 29 |     quoteOpts : {auto c : Ref Ctxt Defs} ->

 30 |                 {vars : Scope} ->

 31 |                 QuoteOpts -> Defs -> Env Term vars -> tm vars -> Core (Term vars)

 33 |     quoteGen : {auto c : Ref Ctxt Defs} ->

 34 |                {vars : _} ->

 35 |                Ref QVar Int -> QuoteOpts ->

 36 |                Defs -> Env Term vars -> tm vars -> Core (Term vars)

 38 |     quote defs env tm

 39 |         = do q <- newRef QVar 0

 40 |              quoteGen q (MkQuoteOpts True False Nothing) defs env tm

 42 |     quoteLHS defs env tm

 43 |         = do q <- newRef QVar 0

 44 |              quoteGen q (MkQuoteOpts True True Nothing) defs env tm

 46 |     quoteOpts opts defs env tm

 47 |         = do q <- newRef QVar 0

 48 |              quoteGen q opts defs env tm

 51 | genName : {auto q : Ref QVar Int} -> String -> Core Name

 52 | genName n

 53 |     = do i <- get QVar

 54 |          put QVar (i + 1)

 55 |          pure (MN n i)

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

 59 |               {bound, free : _} ->

 60 |               Ref QVar Int -> QuoteOpts -> Defs -> Bounds bound ->

 61 |               Env Term free -> Closure free ->

 62 |               Core (Term (bound ++ free))

 63 |   quoteArg q opts defs bounds env a

 64 |       = quoteGenNF q opts defs bounds env !(evalClosure defs a)

 66 |   quoteArgWithFC : {auto c : Ref Ctxt Defs} ->

 67 |                    {bound, free : _} ->

 68 |                    Ref QVar Int -> QuoteOpts -> Defs -> Bounds bound ->

 69 |                    Env Term free -> (FC, Closure free) ->

 70 |                    Core ((FC, Term (bound ++ free)))

 71 |   quoteArgWithFC q opts defs bounds env

 72 |        = traversePair (quoteArg q opts defs bounds env)

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

 75 |               {bound, free : _} ->

 76 |               Ref QVar Int -> QuoteOpts -> Defs -> Bounds bound ->

 77 |               Env Term free -> List (Closure free) ->

 78 |               Core (List (Term (bound ++ free)))

 79 |   quoteArgs q opts defs bounds env = traverse (quoteArg q opts defs bounds env)

 81 |   quoteArgsWithFC : {auto c : Ref Ctxt Defs} ->

 82 |                     {bound, free : _} ->

 83 |                     Ref QVar Int -> QuoteOpts -> Defs -> Bounds bound ->

 84 |                     Env Term free -> List (FC, Closure free) ->

 85 |                     Core (List (FC, Term (bound ++ free)))

 86 |   quoteArgsWithFC q opts defs bounds env

 87 |       = traverse (quoteArgWithFC q opts defs bounds env)

 89 |   quoteHead : {auto c : Ref Ctxt Defs} ->

 90 |               {bound, free : _} ->

 91 |               Ref QVar Int -> QuoteOpts -> Defs ->

 92 |               FC -> Bounds bound -> Env Term free -> NHead free ->

 93 |               Core (Term (bound ++ free))

 94 |   quoteHead {bound} q opts defs fc bounds env (NLocal mrig _ prf)

 95 |       = let MkVar prf' = addLater bound prf in

 96 |             pure $ Local fc mrig _ prf'

 97 |     where

 98 |       addLater : {idx : _} ->

 99 |                  (ys : List Name) -> (0 p : IsVar n idx xs) ->

100 |                  Var (ys ++ xs)

101 |       addLater [] isv = MkVar isv

102 |       addLater (x :: xs) isv

103 |           = let MkVar isv' = addLater xs isv in

104 |                 MkVar (Later isv')

105 |   quoteHead q opts defs fc bounds env (NRef Bound (MN n i))

106 |       = pure $ case findName bounds of

107 |              Just (MkVar p) => Local fc Nothing _ (embedIsVar p)

108 |              Nothing => Ref fc Bound (MN n i)

109 |     where

110 |       findName : Bounds bound' -> Maybe (Var bound')

111 |       findName None = Nothing

112 |       findName (Add x (MN n' i') ns)

113 |           = if i == i' -- this uniquely identifies it, given how we

114 |                        -- generated the names, and is a faster test!

115 |                then Just first

116 |                else do MkVar p <-findName ns

117 |                        Just (MkVar (Later p))

118 |       findName (Add x _ ns)

119 |           = do MkVar p <-findName ns

120 |                Just (MkVar (Later p))

121 |   quoteHead q opts defs fc bounds env (NRef nt n) = pure $ Ref fc nt n

122 |   quoteHead q opts defs fc bounds env (NMeta n i args)

123 |       = do args' <- quoteArgs q opts defs bounds env args

124 |            pure $ Meta fc n i args'

126 |   quotePi : {auto c : Ref Ctxt Defs} ->

127 |             {bound, free : _} ->

128 |             Ref QVar Int -> QuoteOpts -> Defs -> Bounds bound ->

129 |             Env Term free -> PiInfo (Closure free) ->

130 |             Core (PiInfo (Term (bound ++ free)))

131 |   quotePi q opts defs bounds env Explicit = pure Explicit

132 |   quotePi q opts defs bounds env Implicit = pure Implicit

133 |   quotePi q opts defs bounds env AutoImplicit = pure AutoImplicit

134 |   quotePi q opts defs bounds env (DefImplicit t)

135 |       = do t' <- quoteGenNF q opts defs bounds env !(evalClosure defs t)

136 |            pure (DefImplicit t')

138 |   quoteBinder : {auto c : Ref Ctxt Defs} ->

139 |                 {bound, free : _} ->

140 |                 Ref QVar Int -> QuoteOpts -> Defs -> Bounds bound ->

141 |                 Env Term free -> Binder (Closure free) ->

142 |                 Core (Binder (Term (bound ++ free)))

143 |   quoteBinder q opts defs bounds env (Lam fc r p ty)

144 |       = do ty' <- quoteGenNF q opts defs bounds env !(evalClosure defs ty)

145 |            p' <- quotePi q opts defs bounds env p

146 |            pure (Lam fc r p' ty')

147 |   quoteBinder q opts defs bounds env (Let fc r val ty)

148 |       = do val' <- quoteGenNF q opts defs bounds env !(evalClosure defs val)

149 |            ty' <- quoteGenNF q opts defs bounds env !(evalClosure defs ty)

150 |            pure (Let fc r val' ty')

151 |   quoteBinder q opts defs bounds env (Pi fc r p ty)

152 |       = do ty' <- quoteGenNF q opts defs bounds env !(evalClosure defs ty)

153 |            p' <- quotePi q opts defs bounds env p

154 |            pure (Pi fc r p' ty')

155 |   quoteBinder q opts defs bounds env (PVar fc r p ty)

156 |       = do ty' <- quoteGenNF q opts defs bounds env !(evalClosure defs ty)

157 |            p' <- quotePi q opts defs bounds env p

158 |            pure (PVar fc r p' ty')

159 |   quoteBinder q opts defs bounds env (PLet fc r val ty)

160 |       = do val' <- quoteGenNF q opts defs bounds env !(evalClosure defs val)

161 |            ty' <- quoteGenNF q opts defs bounds env !(evalClosure defs ty)

162 |            pure (PLet fc r val' ty')

163 |   quoteBinder q opts defs bounds env (PVTy fc r ty)

164 |       = do ty' <- quoteGenNF q opts defs bounds env !(evalClosure defs ty)

165 |            pure (PVTy fc r ty')

167 |   quoteGenNF : {auto c : Ref Ctxt Defs} ->

168 |                {bound, vars : _} ->

169 |                Ref QVar Int -> QuoteOpts ->

170 |                Defs -> Bounds bound ->

171 |                Env Term vars -> NF vars -> Core (Term (bound ++ vars))

172 |   quoteGenNF q opts defs bound env (NBind fc n b sc)

173 |       = do var <- genName "qv"

174 |            sc' <- quoteGenNF q opts defs (Add n var bound) env

175 |                        !(sc defs (toClosure defaultOpts env (Ref fc Bound var)))

176 |            b' <- quoteBinder q opts defs bound env b

177 |            pure (Bind fc n b' sc')

178 |   quoteGenNF q opts defs bound env (NApp fc f args)

179 |       = do f' <- quoteHead q opts defs fc bound env f

180 |            opts' <- case sizeLimit opts of

181 |                          Nothing => pure opts

182 |                          Just Z => throw (InternalError "Size limit exceeded")

183 |                          Just (S k) => pure ({ sizeLimit := Just k } opts)

184 |            args' <- if patterns opts && not (topLevel opts) && isRef f

185 |                        then do empty <- clearDefs defs

186 |                                quoteArgsWithFC q opts' empty bound env args

187 |                                else quoteArgsWithFC q ({ topLevel := False } opts')

188 |                                                     defs bound env args

189 |            pure $ applyStackWithFC f' args'

190 |     where

191 |       isRef : NHead vars -> Bool

192 |       isRef (NRef {}) = True

193 |       isRef _ = False

194 |   quoteGenNF q opts defs bound env (NDCon fc n t ar args)

195 |       = do args' <- quoteArgsWithFC q opts defs bound env args

196 |            pure $ applyStackWithFC (Ref fc (DataCon t ar) n) args'

197 |   quoteGenNF q opts defs bound env (NTCon fc n ar args)

198 |       = do args' <- quoteArgsWithFC q opts defs bound env args

199 |            pure $ applyStackWithFC (Ref fc (TyCon ar) n) args'

200 |   quoteGenNF q opts defs bound env (NAs fc s n pat)

201 |       = do n' <- quoteGenNF q opts defs bound env n

202 |            pat' <- quoteGenNF q opts defs bound env pat

203 |            pure (As fc s n' pat')

204 |   quoteGenNF q opts defs bound env (NDelayed fc r arg)

205 |       = do argQ <- quoteGenNF q opts defs bound env arg

206 |            pure (TDelayed fc r argQ)

207 |   quoteGenNF q opts defs bound env (NDelay fc r ty arg)

208 |       = do argNF <- evalClosure defs (toHolesOnly arg)

209 |            argQ <- quoteGenNF q opts defs bound env argNF

210 |            tyNF <- evalClosure defs (toHolesOnly ty)

211 |            tyQ <- quoteGenNF q opts defs bound env tyNF

212 |            pure (TDelay fc r tyQ argQ)

213 |     where

214 |       toHolesOnly : Closure vs -> Closure vs

215 |       toHolesOnly (MkClosure opts locs env tm)

216 |           = MkClosure ({ holesOnly := True,

217 |                          argHolesOnly := True } opts)

218 |                       locs env tm

219 |       toHolesOnly c = c

220 |   quoteGenNF q opts defs bound env (NForce fc r arg args)

221 |       = do args' <- quoteArgsWithFC q opts defs bound env args

222 |            case arg of

223 |                 NDelay fc _ _ arg =>

224 |                    do argNF <- evalClosure defs arg

225 |                       pure $ applyStackWithFC !(quoteGenNF q opts defs bound env argNF) args'

226 |                 _ => do arg' <- quoteGenNF q opts defs bound env arg

227 |                         pure $ applyStackWithFC (TForce fc r arg') args'

228 |   quoteGenNF q opts defs bound env (NPrimVal fc c) = pure $ PrimVal fc c

229 |   quoteGenNF q opts defs bound env (NErased fc t)

230 |     = Erased fc <$> traverse @{%search} @{CORE} (\ nf => quoteGenNF q opts defs bound env nf) t

231 |   quoteGenNF q opts defs bound env (NType fc u) = pure $ TType fc u

234 | Quote NF where

235 |   quoteGen q opts defs env tm = quoteGenNF q opts defs None env tm

238 | Quote Term where

239 |   quoteGen q opts defs env tm = pure tm

242 | Quote Closure where

243 |   quoteGen q opts defs env c = quoteGen q opts defs env !(evalClosure defs c)

245 | quoteWithPiGen : {auto _ : Ref Ctxt Defs} ->

246 |                  {bound, vars : _} ->

247 |                  Ref QVar Int -> QuoteOpts -> Defs -> Bounds bound ->

248 |                  Env Term vars -> NF vars -> Core (Term (bound ++ vars))

249 | quoteWithPiGen q opts defs bound env (NBind fc n (Pi bfc c p ty) sc)

250 |     = do var <- genName "qv"

251 |          empty <- clearDefs defs

252 |          sc' <- quoteWithPiGen q opts defs (Add n var bound) env

253 |                      !(sc defs (toClosure defaultOpts env (Ref fc Bound var)))

254 |          ty' <- quoteGenNF q opts empty bound env !(evalClosure empty ty)

255 |          p' <- quotePi q opts empty bound env p

256 |          pure (Bind fc n (Pi bfc c p' ty') sc')

257 | quoteWithPiGen q opts defs bound env (NErased fc t)

258 |   = Erased fc <$> traverse @{%search} @{CORE} (quoteWithPiGen q opts defs bound env) t

259 | quoteWithPiGen q opts defs bound env tm

260 |     = do empty <- clearDefs defs

261 |          quoteGenNF q opts empty bound env tm

266 | quoteWithPi : {auto c : Ref Ctxt Defs} ->

267 |               {vars : Scope} ->

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

269 | quoteWithPi defs env tm

270 |     = do q <- newRef QVar 0

271 |          quoteWithPiGen q (MkQuoteOpts True False Nothing) defs None env tm