0 | module TTImp.Elab.RunElab

  2 | import Core.Directory

  3 | import Core.Env

  4 | import Core.Metadata

  5 | import Core.Reflect

  6 | import Core.Unify

  7 | import Core.Value

  9 | import Idris.Resugar

 10 | import Idris.REPL.Opts

 11 | import Idris.Pretty

 12 | import Idris.Syntax

 14 | import Libraries.Data.NameMap

 15 | import Libraries.Data.WithDefault

 16 | import Libraries.Text.PrettyPrint.Prettyprinter.Doc -- for PageWidth

 17 | import Libraries.Utils.Path

 19 | import TTImp.Elab.Check

 20 | import TTImp.Elab.Delayed

 21 | import TTImp.Reflect

 22 | import TTImp.TTImp

 23 | import TTImp.TTImp.Functor

 24 | import TTImp.Unelab

 26 | import System.File.Meta

 28 | %default covering

 30 | record NameInfo where

 31 |   constructor MkNameInfo

 32 |   nametype : NameType

 34 | lookupNameInfo : Name -> Context -> Core (List (Name, NameInfo))

 35 | lookupNameInfo n ctxt

 36 |     = do res <- lookupCtxtName n ctxt

 37 |          pure (map (\ (n, i, gd) =>

 38 |                       (n, MkNameInfo { nametype = getDefNameType gd } ))

 39 |                    res)

 41 | Reflect NameInfo where

 42 |   reflect fc defs lhs env inf

 43 |       = do nt <- reflect fc defs lhs env (nametype inf)

 44 |            appCon fc defs (reflectiontt "MkNameInfo") [nt]

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

 47 |                GlobalDef -> Core (List Name)

 48 | deepRefersTo def = do

 49 |   defs <- get Ctxt

 50 |   map nub $ clos empty defs $ refs' defs def

 51 |   -- we don't start with `[defs.fullname]` to distinguish between recursive and non-recursive definitions

 52 |   where

 53 |     refs' : Defs -> GlobalDef -> List Name

 54 |     refs' defs def = keys (refersTo def)

 56 |     refs : Defs -> Name -> Core (List Name)

 57 |     refs defs n = maybe [] (refs' defs) <$> lookupCtxtExact n (gamma defs)

 59 |     clos : NameMap () -> Defs -> List Name -> Core (List Name)

 60 |     clos all _    []      = pure (keys all)

 61 |     clos all defs (n::ns) = case lookup n all of

 62 |       Just _  => clos all defs ns

 63 |       Nothing => do

 64 |         let all' = insert n () all

 65 |         let ns' = !(refs defs n) ++ ns

 66 |         clos all' defs ns'

 69 | elabScript : {vars : _} ->

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

 71 |              {auto m : Ref MD Metadata} ->

 72 |              {auto u : Ref UST UState} ->

 73 |              {auto s : Ref Syn SyntaxInfo} ->

 74 |              {auto o : Ref ROpts REPLOpts} ->

 75 |              RigCount -> FC -> NestedNames vars ->

 76 |              Env Term vars -> NF vars -> Maybe (Glued vars) ->

 77 |              Core (NF vars)

 78 | elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp

 79 |     = do defs <- get Ctxt

 80 |          fnm <- toFullNames nm

 81 |          case fnm of

 82 |               NS ns (UN (Basic n))

 83 |                  => if ns == reflectionNS

 84 |                       then elabCon defs n (map snd args)

 85 |                              `catch` \case -- wrap into `RunElabFail` any non-elab error

 86 |                                e@(BadRunElab {})  => throw e

 87 |                                e@(RunElabFail {}) => throw e

 88 |                                e                  => throw $ RunElabFail e

 89 |                       else failWith defs $ "bad reflection namespace " ++ show ns

 90 |               _ => failWith defs $ "bad fullnames " ++ show fnm

 91 |   where

 92 |     failWith : Defs -> String -> Core a

 93 |     failWith defs desc

 94 |       = do empty <- clearDefs defs

 95 |            throw (BadRunElab fc env !(quote empty env script) desc)

 97 |     scriptRet : Reflect a => a -> Core (NF vars)

 98 |     scriptRet tm

 99 |         = do defs <- get Ctxt

100 |              nfOpts withAll defs env !(reflect fc defs False env tm)

102 |     reifyFC : Defs -> Closure vars -> Core FC

103 |     reifyFC defs mbfc = pure $ case !(evalClosure defs mbfc >>= reify defs) of

104 |       EmptyFC => fc

105 |       x       => x

107 |     -- parses and resolves `Language.Reflection.LookupDir`

108 |     lookupDir : Defs -> NF vars -> Core String

109 |     lookupDir defs (NDCon _ conName _ _ [])

110 |         = do defs <- get Ctxt

111 |              NS ns (UN (Basic n)) <- toFullNames conName

112 |                | fnm => failWith defs $ "bad lookup dir fullnames " ++ show fnm

113 |              let True = ns == reflectionNS

114 |                | False => failWith defs $ "bad lookup dir namespace " ++ show ns

115 |              let wd = defs.options.dirs.working_dir

116 |              let sd = maybe wd (\sd => joinPath [wd, sd]) defs.options.dirs.source_dir

117 |              let modDir : Bool -> Core String := \doParent => do

118 |                             syn <- get Syn

119 |                             let parentIfNeeded = if doParent then parent else pure

120 |                             let moduleSuffix = toList $ (head' syn.saveMod >>= parentIfNeeded) <&> toPath

121 |                             pure $ joinPath $ sd :: moduleSuffix

122 |              case n of

123 |                "ProjectDir"       => pure wd

124 |                "SourceDir"        => pure sd

125 |                "CurrentModuleDir" => modDir True

126 |                "SubmodulesDir"    => modDir False

127 |                "BuildDir"         => pure $ joinPath [wd, defs.options.dirs.build_dir]

128 |                _ => failWith defs $ "bad lookup dir value"

129 |     lookupDir defs lk

130 |         = do defs <- get Ctxt

131 |              empty <- clearDefs defs

132 |              throw (BadRunElab fc env !(quote empty env lk) "lookup dir is not a data value")

134 |     validatePath : Defs -> String -> Core ()

135 |     validatePath defs path = do

136 |       let True = isRelative path

137 |         | False => failWith defs $ "path must be relative"

138 |       let True = pathDoesNotEscape 0 $ splitPath path

139 |         | False => failWith defs $ "path must not escape the directory"

140 |       pure ()

141 |       where

142 |         pathDoesNotEscape : (depth : Nat) -> List String -> Bool

143 |         pathDoesNotEscape _     []           = True

144 |         pathDoesNotEscape Z     (".."::rest) = False

145 |         pathDoesNotEscape (S n) (".."::rest) = pathDoesNotEscape n rest

146 |         pathDoesNotEscape n     ("." ::rest) = pathDoesNotEscape n rest

147 |         pathDoesNotEscape n     (_   ::rest) = pathDoesNotEscape (S n) rest

149 |     elabCon : Defs -> String -> List (Closure vars) -> Core (NF vars)

150 |     elabCon defs "Pure" [_,val]

151 |         = do empty <- clearDefs defs

152 |              evalClosure empty val

153 |     elabCon defs "Map" [_,_,fm,act]

154 |         -- fm : A -> B

155 |         -- elab : A

156 |         = do act <- elabScript rig fc nest env !(evalClosure defs act) exp

157 |              act <- quote defs env act

158 |              fm <- evalClosure defs fm

159 |              applyToStack defs withHoles env fm [(getLoc act, toClosure withAll env act)]

160 |     elabCon defs "Ap" [_,_,actF,actX]

161 |         -- actF : Elab (A -> B)

162 |         -- actX : Elab A

163 |         = do actF <- elabScript rig fc nest env !(evalClosure defs actF) exp

164 |              actX <- elabScript rig fc nest env !(evalClosure defs actX) exp

165 |              actX <- quote defs env actX

166 |              applyToStack defs withHoles env actF [(getLoc actX, toClosure withAll env actX)]

167 |     elabCon defs "Bind" [_,_,act,k]

168 |         -- act : Elab A

169 |         -- k : A -> Elab B

170 |         -- 1) Run elabScript on act stripping off Elab

171 |         -- 2) Evaluate the resulting act

172 |         -- 3) apply k to the result of (2)

173 |         -- 4) Run elabScript on the result stripping off Elab

174 |         = do act <- elabScript rig fc nest env

175 |                                 !(evalClosure defs act) exp

176 |              act <- quote defs env act

177 |              k <- evalClosure defs k

178 |              r <- applyToStack defs withAll env k [(getLoc act, toClosure withAll env act)]

179 |              elabScript rig fc nest env r exp

180 |     elabCon defs "Fail" [_, mbfc, msg]

181 |         = do msg' <- evalClosure defs msg

182 |              throw $ RunElabFail $ GenericMsg !(reifyFC defs mbfc) !(reify defs msg')

183 |     elabCon defs "Warn" [mbfc, msg]

184 |         = do msg' <- evalClosure defs msg

185 |              recordWarning $ GenericWarn !(reifyFC defs mbfc) !(reify defs msg')

186 |              scriptRet ()

187 |     elabCon defs "Try" [_, elab1, elab2]

188 |         = tryUnify (do constart <- getNextEntry

189 |                        res <- elabScript rig fc nest env !(evalClosure defs elab1) exp

190 |                        -- We ensure that all of the constraints introduced during the elab script

191 |                        -- have been solved. This guarantees that we do not mistakenly succeed even

192 |                        -- though e.g. a proof search got delayed.

193 |                        solveConstraintsAfter constart inTerm LastChance

194 |                        pure res)

195 |                    (elabScript rig fc nest env !(evalClosure defs elab2) exp)

196 |     elabCon defs "LogMsg" [topic, verb, str]

197 |         = do topic' <- evalClosure defs topic

198 |              verb' <- evalClosure defs verb

199 |              unverifiedLogC !(reify defs topic') !(reify defs verb') $

200 |                   do str' <- evalClosure defs str

201 |                      reify defs str'

202 |              scriptRet ()

203 |     elabCon defs "LogTerm" [topic, verb, str, tm]

204 |         = do topic' <- evalClosure defs topic

205 |              verb' <- evalClosure defs verb

206 |              unverifiedLogC !(reify defs topic') !(reify defs verb') $

207 |                   do str' <- evalClosure defs str

208 |                      tm' <- evalClosure defs tm

209 |                      pure $ !(reify defs str') ++ ": " ++

210 |                              show (the RawImp !(reify defs tm'))

211 |              scriptRet ()

212 |     elabCon defs "LogSugaredTerm" [topic, verb, str, tm]

213 |         = do topic' <- evalClosure defs topic

214 |              verb' <- evalClosure defs verb

215 |              unverifiedLogC !(reify defs topic') !(reify defs verb') $

216 |                   do str' <- evalClosure defs str

217 |                      tm' <- reify defs !(evalClosure defs tm)

218 |                      ptm <- pterm (map defaultKindedName tm')

219 |                      pure $ !(reify defs str') ++ ": " ++ show ptm

220 |              scriptRet ()

221 |     elabCon defs "ResugarTerm" [maxLineWidth, tm]

222 |         = do ptm <- pterm . map defaultKindedName =<< reify defs !(evalClosure defs tm)

223 |              mlw : Maybe Nat <- reify defs !(evalClosure defs maxLineWidth)

224 |              let pw = maybe Unbounded (\w => AvailablePerLine (cast w) 1) mlw

225 |              scriptRet $ render' pw Nothing $ pretty {ann=IdrisSyntax} ptm

226 |     elabCon defs "Check" [exp, ttimp]

227 |         = do exp' <- evalClosure defs exp

228 |              ttimp' <- evalClosure defs ttimp

229 |              tidx <- resolveName (UN $ Basic "[elaborator script]")

230 |              e <- newRef EST (initEState tidx env)

231 |              (checktm, _) <- runDelays (const True) $

232 |                      check rig (initElabInfo InExpr) nest env !(reify defs ttimp')

233 |                            (Just (glueBack defs env exp'))

234 |              empty <- clearDefs defs

235 |              nf empty env checktm

236 |     elabCon defs "Quote" [exp, tm]

237 |         = do tm' <- evalClosure defs tm

238 |              defs <- get Ctxt

239 |              empty <- clearDefs defs

240 |              scriptRet $ map rawName !(unelabUniqueBinders env !(quote empty env tm'))

241 |     elabCon defs "Lambda" [x, _, scope]

242 |         = do empty <- clearDefs defs

243 |              NBind bfc x (Lam fc' c p ty) sc <- evalClosure defs scope

244 |                    | _ => failWith defs "Not a lambda"

245 |              n <- genVarName "x"

246 |              sc' <- sc defs (toClosure withAll env (Ref bfc Bound n))

247 |              qsc <- quote empty env sc'

248 |              let lamsc = refToLocal n x qsc

249 |              qp <- quotePi p

250 |              qty <- quote empty env ty

251 |              let env' = Lam fc' c qp qty :: env

253 |              runsc <- elabScript rig fc (weaken nest) env'

254 |                                  !(nf defs env' lamsc) Nothing -- (map weaken exp)

255 |              nf empty env (Bind bfc x (Lam fc' c qp qty) !(quote empty env' runsc))

256 |        where

257 |          quotePi : PiInfo (Closure vars) -> Core (PiInfo (Term vars))

258 |          quotePi Explicit = pure Explicit

259 |          quotePi Implicit = pure Implicit

260 |          quotePi AutoImplicit = pure AutoImplicit

261 |          quotePi (DefImplicit t) = failWith defs "Can't add default lambda"

262 |     elabCon defs "Goal" []

263 |         = do let Just gty = exp

264 |                  | Nothing => nfOpts withAll defs env

265 |                                      !(reflect fc defs False env (the (Maybe RawImp) Nothing))

266 |              ty <- getTerm gty

267 |              scriptRet (Just $ map rawName $ !(unelabUniqueBinders env ty))

268 |     elabCon defs "LocalVars" []

269 |         = scriptRet vars

270 |     elabCon defs "GenSym" [str]

271 |         = do str' <- evalClosure defs str

272 |              n <- genVarName !(reify defs str')

273 |              scriptRet n

274 |     elabCon defs "InCurrentNS" [n]

275 |         = do n' <- evalClosure defs n

276 |              nsn <- inCurrentNS !(reify defs n')

277 |              scriptRet nsn

278 |     elabCon defs "GetType" [n]

279 |         = do n' <- evalClosure defs n

280 |              res <- lookupTyName !(reify defs n') (gamma defs)

281 |              scriptRet !(traverse unelabType res)

282 |       where

283 |         unelabType : (Name, Int, ClosedTerm) -> Core (Name, RawImp)

284 |         unelabType (n, _, ty)

285 |             = pure (n, map rawName !(unelabUniqueBinders Env.empty ty))

286 |     elabCon defs "GetInfo" [n]

287 |         = do n' <- evalClosure defs n

288 |              res <- lookupNameInfo !(reify defs n') (gamma defs)

289 |              scriptRet res

290 |     elabCon defs "GetVis" [n]

291 |         = do dn <- reify defs !(evalClosure defs n)

292 |              ds <- lookupCtxtName dn (gamma defs)

293 |              scriptRet $ map (\(n,_,d) => (n, collapseDefault $ visibility d)) ds

294 |     elabCon defs "GetLocalType" [n]

295 |         = do n' <- evalClosure defs n

296 |              n <- reify defs n'

297 |              case defined n env of

298 |                   Just (MkIsDefined rigb lv) =>

299 |                        do let binder = getBinder lv env

300 |                           let bty = binderType binder

301 |                           scriptRet $ map rawName !(unelabUniqueBinders env bty)

302 |                   _ => failWith defs $ show n ++ " is not a local variable"

303 |     elabCon defs "GetCons" [n]

304 |         = do n' <- evalClosure defs n

305 |              cn <- reify defs n'

306 |              Just (TCon _ _ _ _ _ cons _) <-

307 |                      lookupDefExact cn (gamma defs)

308 |                  | _ => failWith defs $ show cn ++ " is not a type"

309 |              scriptRet $ fromMaybe [] cons

310 |     elabCon defs "GetReferredFns" [n]

311 |         = do dn <- reify defs !(evalClosure defs n)

312 |              Just def <- lookupCtxtExact dn (gamma defs)

313 |                  | Nothing => failWith defs $ show dn ++ " is not a definition"

314 |              ns <- deepRefersTo def

315 |              scriptRet ns

316 |     elabCon defs "GetCurrentFn" []

317 |         = do defs <- get Ctxt

318 |              scriptRet defs.defsStack

319 |     elabCon defs "GetFC" []

320 |         = scriptRet fc

321 |     elabCon defs "Declare" [d]

322 |         = do d' <- evalClosure defs d

323 |              decls <- reify defs d'

324 |              List.traverse_ (processDecl [] (MkNested []) Env.empty) decls

325 |              scriptRet ()

326 |     elabCon defs "ReadFile" [lk, pth]

327 |         = do pathPrefix <- lookupDir defs !(evalClosure defs lk)

328 |              path <- reify defs !(evalClosure defs pth)

329 |              validatePath defs path

330 |              let fullPath = joinPath [pathPrefix, path]

331 |              True <- coreLift $ exists fullPath

332 |                | False => scriptRet $ Nothing {ty=String}

333 |              contents <- readFile fullPath

334 |              scriptRet $ Just contents

335 |     elabCon defs "WriteFile" [lk, pth, contents]

336 |         = do pathPrefix <- lookupDir defs !(evalClosure defs lk)

337 |              path <- reify defs !(evalClosure defs pth)

338 |              validatePath defs path

339 |              contents <- reify defs !(evalClosure defs contents)

340 |              let fullPath = joinPath [pathPrefix, path]

341 |              whenJust (parent fullPath) ensureDirectoryExists

342 |              writeFile fullPath contents

343 |              scriptRet ()

344 |     elabCon defs "IdrisDir" [lk]

345 |         = do evalClosure defs lk >>= lookupDir defs >>= scriptRet

346 |     elabCon defs n args = failWith defs $ "unexpected Elab constructor " ++ n ++

347 |                                           ", or incorrect count of arguments: " ++ show (length args)

348 | elabScript rig fc nest env script exp

349 |     = do defs <- get Ctxt

350 |          empty <- clearDefs defs

351 |          throw (BadRunElab fc env !(quote empty env script) "script is not a data value")

354 | checkRunElab : {vars : _} ->

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

356 |                {auto m : Ref MD Metadata} ->

357 |                {auto u : Ref UST UState} ->

358 |                {auto e : Ref EST (EState vars)} ->

359 |                {auto s : Ref Syn SyntaxInfo} ->

360 |                {auto o : Ref ROpts REPLOpts} ->

361 |                RigCount -> ElabInfo ->

362 |                NestedNames vars -> Env Term vars ->

363 |                FC -> (requireExtension : Bool) -> RawImp -> Maybe (Glued vars) ->

364 |                Core (Term vars, Glued vars)

365 | checkRunElab rig elabinfo nest env fc reqExt script exp

366 |     = do expected <- mkExpected exp

367 |          defs <- get Ctxt

368 |          unless (not reqExt || isExtension ElabReflection defs) $

369 |              throw (GenericMsg fc "%language ElabReflection not enabled")

370 |          let n = NS reflectionNS (UN $ Basic "Elab")

371 |          elabtt <- appCon fc defs n [expected]

372 |          (stm, sty) <- runDelays (const True) $

373 |                            check rig elabinfo nest env script (Just (gnf env elabtt))

374 |          solveConstraints inTerm Normal

375 |          defs <- get Ctxt -- checking might have resolved some holes

376 |          nfstm <- nfOpts withAll defs env stm

377 |          ntm <- logTime 2 "Elaboration script" $

378 |                   elabScript rig fc nest env nfstm $ Just (gnf env expected)

379 |          defs <- get Ctxt -- might have updated as part of the script

380 |          empty <- clearDefs defs

381 |          pure (!(quote empty env ntm), gnf env expected)

382 |   where

383 |     mkExpected : Maybe (Glued vars) -> Core (Term vars)

384 |     mkExpected (Just ty) = pure !(getTerm ty)

385 |     mkExpected Nothing

386 |         = do nm <- genName "scriptTy"

387 |              u <- uniVar fc

388 |              metaVar fc erased env nm (TType fc u)