0 | module TTImp.Elab.Local

  2 | import Core.Env

  3 | import Core.Metadata

  4 | import Core.Unify

  6 | import Idris.REPL.Opts

  7 | import Idris.Syntax

  9 | import TTImp.Elab.Check

 10 | import TTImp.TTImp

 12 | import Libraries.Data.NameMap

 13 | import Libraries.Data.WithDefault

 15 | %default covering

 18 | localHelper : {vars : _} ->

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

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

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

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

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

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

 25 |              NestedNames vars -> Env Term vars ->

 26 |              List ImpDecl -> (NestedNames vars -> Core a) ->

 27 |              Core a

 28 | localHelper {vars} nest env nestdecls_in func

 29 |     = do est <- get EST

 30 |          let f = defining est

 31 |          defs <- get Ctxt

 32 |          gdef <- lookupCtxtExact (Resolved (defining est)) (gamma defs)

 33 |          let vis  = maybe Public (collapseDefault . visibility) gdef

 34 |          let mult = maybe linear GlobalDef.multiplicity gdef

 36 |          -- If the parent function is public, the nested definitions need

 37 |          -- to be public too

 38 |          let nestdeclsVis =

 39 |                if vis == Public

 40 |                   then map setPublic nestdecls_in

 41 |                   else nestdecls_in

 43 |          -- If the parent function is erased, then the nested definitions

 44 |          -- will be erased too

 45 |          let nestdeclsMult =

 46 |            if mult == erased

 47 |               then map setErased nestdeclsVis

 48 |               else nestdeclsVis

 50 |          let defNames = definedInBlock emptyNS nestdeclsMult

 51 |          names' <- traverse (applyEnv f) defNames

 52 |          let nest' = { names $= (names' ++) } nest

 53 |          -- TODO is this comment still up-to-date?

 54 |          -- For the local definitions, don't allow access to linear things

 55 |          -- unless they're explicitly passed.

 56 |          -- This is because, at the moment, we don't have any mechanism of

 57 |          -- ensuring the nested definition is used exactly once

 58 |          let env' = eraseLinear env

 59 |          -- We don't want to keep rechecking delayed elaborators in the

 60 |          -- locals block, because they're not going to make progress until

 61 |          -- we come out again, so save them

 62 |          ust <- get UST

 63 |          let olddelayed = delayedElab ust

 64 |          put UST ({ delayedElab := [] } ust)

 65 |          defs <- get Ctxt

 66 |          -- store the local hints, so we can reset them after we've elaborated

 67 |          -- everything

 68 |          let oldhints = localHints defs

 70 |          let nestdecls = map (updateName nest') nestdeclsMult

 71 |          log "elab.def.local" 20 $ show nestdecls

 73 |          traverse_ (processDecl [] nest' env') nestdecls

 74 |          update UST { delayedElab := olddelayed }

 75 |          res <- func nest'

 76 |          update Ctxt { localHints := oldhints }

 77 |          pure res

 78 |   where

 79 |     applyEnv : Int -> Name ->

 80 |                Core (Name, (Maybe Name, List (Var vars), FC -> NameType -> Term vars))

 81 |     applyEnv outer inner

 82 |           = do ust <- get UST

 83 |                put UST ({ nextName $= (+1) } ust)

 84 |                let nestedName_in = Nested (outer, nextName ust) inner

 85 |                nestedName <- inCurrentNS nestedName_in

 86 |                n' <- addName nestedName

 87 |                pure (inner, (Just nestedName, reverse (allVars env),

 88 |                         \fc, nt => applyToFull fc

 89 |                                (Ref fc nt (Resolved n')) env))

 91 |     -- Update the names in the declarations to the new 'nested' names.

 92 |     -- When we encounter the names in elaboration, we'll update to an

 93 |     -- application of the nested name.

 94 |     updateTyName : NestedNames vars -> ImpTy -> ImpTy

 95 |     updateTyName nest ty

 96 |         = update "tyname" (map (mapNestedName nest)) ty

 98 |     updateDataName : NestedNames vars -> ImpData -> ImpData

 99 |     updateDataName nest (MkImpData loc' n tycons dopts dcons)

100 |         = MkImpData loc' (mapNestedName nest n) tycons dopts

101 |                          (map (updateTyName nest) dcons)

102 |     updateDataName nest (MkImpLater loc' n tycons)

103 |         = MkImpLater loc' (mapNestedName nest n) tycons

105 |     updateFieldName : NestedNames vars -> IField -> IField

106 |     updateFieldName nest field

107 |         = update "name" (map (mapNestedName nest)) field

109 |     updateRecordName : NestedNames vars -> ImpRecordData Name -> ImpRecordData Name

110 |     updateRecordName nest (MkImpRecord header body)

111 |         = let updatedTyName = (update "name" (map (mapNestedName nest)) header)

112 |               updatedConName = (update "name" (map (mapNestedName nest)) body)

113 |               updatedParameters = (map (map (updateFieldName nest)) updatedConName)

114 |           in MkImpRecord updatedTyName updatedParameters

116 |     updateRecordNS : NestedNames vars -> Maybe String -> Maybe String

117 |     updateRecordNS _    Nothing   = Nothing

118 |     updateRecordNS nest (Just ns) = Just $ show $ mapNestedName nest (UN $ mkUserName ns)

120 |     updateName : NestedNames vars -> ImpDecl -> ImpDecl

121 |     updateName nest (IClaim claim)

122 |          = IClaim $ map {type $= updateTyName nest} claim

123 |     updateName nest (IDef loc' n cs)

124 |          = IDef loc' (mapNestedName nest n) cs

125 |     updateName nest (IData loc' vis mbt d)

126 |          = IData loc' vis mbt (updateDataName nest d)

127 |     updateName nest (IRecord loc' ns vis mbt imprecord)

128 |          = IRecord loc' (updateRecordNS nest ns) vis mbt (map (updateRecordName nest) imprecord)

129 |     updateName nest i = i

131 |     setPublic : ImpDecl -> ImpDecl

132 |     setPublic (IClaim claim)

133 |         = IClaim $ map {vis := Public} claim

134 |     setPublic (IData fc _ mbt d) = IData fc (specified Public) mbt d

135 |     setPublic (IRecord fc c _ mbt r) = IRecord fc c (specified Public) mbt r

136 |     setPublic (IParameters fc ps decls)

137 |         = IParameters fc ps (map setPublic decls)

138 |     setPublic (INamespace fc ps decls)

139 |         = INamespace fc ps (map setPublic decls)

140 |     setPublic d = d

142 |     setErased : ImpDecl -> ImpDecl

143 |     setErased (IClaim claim)

144 |         = IClaim $ map {rig := erased} claim

145 |     setErased (IParameters fc ps decls)

146 |         = IParameters fc ps (map setErased decls)

147 |     setErased (INamespace fc ps decls)

148 |         = INamespace fc ps (map setErased decls)

149 |     setErased d = d

152 | checkLocal : {vars : _} ->

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

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

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

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

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

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

159 |              RigCount -> ElabInfo ->

160 |              NestedNames vars -> Env Term vars ->

161 |              FC -> List ImpDecl -> (scope : RawImp) ->

162 |              (expTy : Maybe (Glued vars)) ->

163 |              Core (Term vars, Glued vars)

164 | checkLocal {vars} rig elabinfo nest env fc nestdecls_in scope expty

165 |     = localHelper nest env nestdecls_in $ \nest' => check rig elabinfo nest' env scope expty

167 | getLocalTerm : {vars : _} ->

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

169 |                FC -> Env Term vars -> Term vars -> List Name ->

170 |                Core (Term vars, List (Var vars))

171 | getLocalTerm fc env f [] = pure (f, [])

172 | getLocalTerm fc env f (a :: as)

173 |     = case defined a env of

174 |            Just (MkIsDefined rigb lv) =>

175 |                 do (tm, vs) <- getLocalTerm fc env

176 |                                    (App fc f (Local fc Nothing _ lv)) as

177 |                    pure (tm, MkVar lv :: vs)

178 |            Nothing => throw (InternalError "Case Local failed")

181 | checkCaseLocal : {vars : _} ->

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

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

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

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

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

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

188 |                  RigCount -> ElabInfo ->

189 |                  NestedNames vars -> Env Term vars ->

190 |                  FC -> Name -> Name -> List Name -> RawImp ->

191 |                  (expTy : Maybe (Glued vars)) ->

192 |                  Core (Term vars, Glued vars)

193 | checkCaseLocal {vars} rig elabinfo nest env fc uname iname args sc expty

194 |     = do defs <- get Ctxt

195 |          Just def <- lookupCtxtExact iname (gamma defs)

196 |               | Nothing => check rig elabinfo nest env sc expty

197 |          let nt = getDefNameType def

198 |          let name = Ref fc nt iname

199 |          (app, args) <- getLocalTerm fc env name args

200 |          log "elab.local" 5 $ "Updating case local " ++ show uname ++ " " ++ show args

201 |          logTermNF "elab.local" 5 "To" env app

202 |          let nest' = { names $= ((uname, (Just iname, args,

203 |                                          (\fc, nt => app))) :: ) }

204 |                      nest

205 |          check rig elabinfo nest' env sc expty