0 | module Core.Metadata
  1 |
  2 | import Core.Binary
  3 | import Core.Context.Log
  4 | import Core.Env
  5 | import Core.Normalise
  6 | import Core.TTC
  7 |
  8 | import System.File
  9 | import Libraries.Data.NatSet
 10 | import Libraries.Data.PosMap
 11 |
 12 | import public Protocol.IDE.Decoration as Protocol.IDE
 13 |
 14 | %default covering
 15 |
 16 | export
 17 | nameDecoration : Name -> NameType -> Decoration
 18 | nameDecoration nm nt
 19 |   = ifThenElse (isUnsafeBuiltin nm) Postulate (nameTypeDecoration nt)
 20 |
 21 |   where
 22 |
 23 |   nameTypeDecoration : NameType -> Decoration
 24 |   nameTypeDecoration Bound        = Bound
 25 |   nameTypeDecoration Func         = Function
 26 |   nameTypeDecoration (DataCon {}) = Data
 27 |   nameTypeDecoration (TyCon {})   = Typ
 28 |
 29 |
 30 | public export
 31 | ASemanticDecoration : Type
 32 | ASemanticDecoration = (NonEmptyFC, Decoration, Maybe Name)
 33 |
 34 | public export
 35 | SemanticDecorations : Type
 36 | SemanticDecorations = List ASemanticDecoration
 37 |
 38 | TTC Decoration where
 39 |   toBuf Typ       = tag 0
 40 |   toBuf Function  = tag 1
 41 |   toBuf Data      = tag 2
 42 |   toBuf Keyword   = tag 3
 43 |   toBuf Bound     = tag 4
 44 |   toBuf Namespace = tag 5
 45 |   toBuf Postulate = tag 6
 46 |   toBuf Module    = tag 7
 47 |   toBuf Comment   = tag 8
 48 |   fromBuf
 49 |     = case !getTag of
 50 |         0 => pure Typ
 51 |         1 => pure Function
 52 |         2 => pure Data
 53 |         3 => pure Keyword
 54 |         4 => pure Bound
 55 |         5 => pure Namespace
 56 |         6 => pure Postulate
 57 |         7 => pure Module
 58 |         8 => pure Comment
 59 |         _ => corrupt "Decoration"
 60 |
 61 | public export
 62 | record Metadata where
 63 |        constructor MkMetadata
 64 |        -- Mapping from source annotation (location, typically) to
 65 |        -- the LHS defined at that location. Also record the outer environment
 66 |        -- length, since we don't want to case split on these.
 67 |        lhsApps : List (NonEmptyFC, (Nat, ClosedTerm))
 68 |        -- Mapping from annotation to the name defined with that annotation,
 69 |        -- and its type (so, giving the ability to get the types of locally
 70 |        -- defined names)
 71 |        -- The type is abstracted over the whole environment; the Nat gives
 72 |        -- the number of names which were in the environment at the time.
 73 |        names : List (NonEmptyFC, (Name, Nat, ClosedTerm))
 74 |        -- Mapping from annotation to the name that's declared there and
 75 |        -- its type; the Nat is as above
 76 |        tydecls : List (NonEmptyFC, (Name, Nat, ClosedTerm))
 77 |        -- Current lhs, if applicable, and a mapping from hole names to the
 78 |        -- lhs they're under. This is for expression search, to ensure that
 79 |        -- recursive calls have a smaller value as an argument.
 80 |        -- Also use this to get the name of the function being defined (i.e.
 81 |        -- to know what the recursive call is, if applicable)
 82 |        currentLHS : Maybe ClosedTerm
 83 |        holeLHS : List (Name, ClosedTerm)
 84 |        nameLocMap : PosMap (NonEmptyFC, Name)
 85 |        sourceIdent : OriginDesc
 86 |
 87 |        ||| Semantic Highlighting
 88 |        ||| Posmap of known semantic decorations
 89 |        semanticHighlighting : PosMap ASemanticDecoration
 90 |
 91 |        ||| Posmap of aliases (in `with` clauses the LHS disapear during
 92 |        ||| elaboration after making sure that they match their parents'
 93 |        semanticAliases : PosMap (NonEmptyFC, NonEmptyFC)
 94 |
 95 |        ||| Posmap of decorations to default to if the elaboration does not
 96 |        ||| produce any highlighting for this range
 97 |        semanticDefaults : PosMap ASemanticDecoration
 98 |
 99 |
100 | ||| Combine semanticHighlighting, semanticAliases, and semanticDefaults into
101 | ||| a single posmap with all the information
102 | export
103 | allSemanticHighlighting :
104 |   {auto c : Ref Ctxt Defs} ->
105 |   Metadata -> Core (PosMap ASemanticDecoration)
106 | allSemanticHighlighting meta = do
107 |     let semHigh = meta.semanticHighlighting
108 |     log "ide-mode.highlight" 19 $
109 |       "Semantic metadata is: " ++ show semHigh
110 |
111 |     let aliases
112 |           : List ASemanticDecoration
113 |           = flip foldMap meta.semanticAliases $ \ (from, to) =>
114 |               let decors = uncurry exactRange (snd to) semHigh in
115 |               map (\ ((fnm, loc), rest) => ((fnm, snd from), rest)) decors
116 |     log "ide-mode.highlight.alias" 19 $
117 |       "Semantic metadata from aliases is: " ++ show aliases
118 |
119 |     let defaults
120 |          : List ASemanticDecoration
121 |          = flip foldMap meta.semanticDefaults $ \ decor@((_, range), _) =>
122 |              case uncurry exactRange range semHigh of
123 |                [] => [decor]
124 |                _ => []
125 |
126 |     pure (fromList aliases `union` (fromList defaults `union` semHigh))
127 |
128 | covering
129 | Show Metadata where
130 |   show (MkMetadata apps names tydecls currentLHS holeLHS nameLocMap
131 |                    fname semanticHighlighting semanticAliases semanticDefaults) = """
132 |     Metadata:
133 |      lhsApps: \{ show apps }
134 |      names: \{ show names }
135 |      type declarations: \{ show tydecls }
136 |      current LHS: \{ show currentLHS }
137 |      holes: \{ show holeLHS }
138 |      nameLocMap: \{ show nameLocMap }
139 |      sourceIdent: \{ show fname }
140 |      semanticHighlighting: \{ show semanticHighlighting }
141 |      semanticAliases: \{ show semanticAliases }
142 |      semanticDefaults: \{ show semanticDefaults }
143 |     """
144 |
145 | export
146 | initMetadata : OriginDesc -> Metadata
147 | initMetadata finfo = MkMetadata
148 |   { lhsApps = []
149 |   , names = []
150 |   , tydecls = []
151 |   , currentLHS = Nothing
152 |   , holeLHS = []
153 |   , nameLocMap = empty
154 |   , sourceIdent = finfo
155 |   , semanticHighlighting = empty
156 |   , semanticAliases = empty
157 |   , semanticDefaults = empty
158 |   }
159 |
160 | -- A label for metadata in the global state
161 | export
162 | data MD : Type where
163 |
164 | TTC Metadata where
165 |   toBuf m
166 |       = do toBuf (lhsApps m)
167 |            toBuf (names m)
168 |            toBuf (tydecls m)
169 |            toBuf (holeLHS m)
170 |            toBuf (nameLocMap m)
171 |            toBuf (sourceIdent m)
172 |            toBuf (semanticHighlighting m)
173 |            toBuf (semanticAliases m)
174 |            toBuf (semanticDefaults m)
175 |
176 |   fromBuf
177 |       = do apps <- fromBuf
178 |            ns <- fromBuf
179 |            tys <- fromBuf
180 |            hlhs <- fromBuf
181 |            dlocs <- fromBuf
182 |            fname <- fromBuf
183 |            semhl <- fromBuf
184 |            semal <- fromBuf
185 |            semdef <- fromBuf
186 |            pure (MkMetadata apps ns tys Nothing hlhs dlocs fname semhl semal semdef)
187 |
188 | export
189 | addLHS : {vars : _} ->
190 |          {auto c : Ref Ctxt Defs} ->
191 |          {auto m : Ref MD Metadata} ->
192 |          FC -> Nat -> Env Term vars -> Term vars -> Core ()
193 | addLHS loc outerenvlen env tm
194 |     = do meta <- get MD
195 |          tm' <- toFullNames (bindEnv loc (toPat env) tm)
196 |          -- Put the lhs on the metadata if it's not empty
197 |          whenJust (isNonEmptyFC loc) $ \ neloc =>
198 |            put MD $ { lhsApps $= ((neloc, outerenvlen, tm') ::) } meta
199 |
200 |   where
201 |     toPat : Env Term vs -> Env Term vs
202 |     toPat (Lam fc c p ty :: bs) = PVar fc c p ty :: toPat bs
203 |     toPat (b :: bs) = b :: toPat bs
204 |     toPat [] = []
205 |
206 | -- For giving local variable names types, just substitute the name
207 | -- rather than storing the whole environment, otherwise we'll repeatedly
208 | -- store the environment and it'll get big.
209 | -- We'll need to rethink a bit if we want interactive editing to show
210 | -- the whole environment - perhaps store each environment just once
211 | -- along with its source span?
212 | -- In any case, one could always look at the other names to get their
213 | -- types directly!
214 | substEnv : {vars : _} ->
215 |            FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
216 | substEnv loc [] tm = tm
217 | substEnv {vars = x :: _} loc (b :: env) tm
218 |     = substEnv loc env (subst (Ref loc Bound x) tm)
219 |
220 | export
221 | addNameType : {vars : _} ->
222 |               {auto c : Ref Ctxt Defs} ->
223 |               {auto m : Ref MD Metadata} ->
224 |               FC -> Name -> Env Term vars -> Term vars -> Core ()
225 | addNameType loc n env tm
226 |     = do meta <- get MD
227 |          n' <- getFullName n
228 |
229 |          -- Add the name to the metadata if the file context is not empty
230 |          whenJust (isConcreteFC loc) $ \ neloc => do
231 |            put MD $ { names $= ((neloc, (n', 0, substEnv loc env tm)) ::) } meta
232 |            log "metadata.names" 7 $ show n' ++ " at line " ++ show (1 + startLine neloc)
233 |
234 | export
235 | addTyDecl : {vars : _} ->
236 |             {auto c : Ref Ctxt Defs} ->
237 |             {auto m : Ref MD Metadata} ->
238 |             FC -> Name -> Env Term vars -> Term vars -> Core ()
239 | addTyDecl loc n env tm
240 |     = do meta <- get MD
241 |          n' <- getFullName n
242 |
243 |          -- Add the type declaration to the metadata if the file context is not empty
244 |          whenJust (isNonEmptyFC loc) $ \ neloc =>
245 |            put MD $ { tydecls $= ( (neloc, (n', length env, bindEnv loc env tm)) ::) } meta
246 |
247 | export
248 | addNameLoc : {auto m : Ref MD Metadata} ->
249 |              {auto c : Ref Ctxt Defs} ->
250 |              FC -> Name -> Core ()
251 | addNameLoc loc n
252 |     = do meta <- get MD
253 |          n' <- getFullName n
254 |          whenJust (isConcreteFC loc) $ \neloc =>
255 |            put MD $ { nameLocMap $= insert (neloc, n') } meta
256 |
257 | export
258 | setHoleLHS : {auto m : Ref MD Metadata} -> ClosedTerm -> Core ()
259 | setHoleLHS tm = update MD { currentLHS := Just tm }
260 |
261 | export
262 | clearHoleLHS : {auto m : Ref MD Metadata} -> Core ()
263 | clearHoleLHS = update MD { currentLHS := Nothing }
264 |
265 | export
266 | withCurrentLHS : {auto c : Ref Ctxt Defs} ->
267 |                  {auto m : Ref MD Metadata} ->
268 |                  Name -> Core ()
269 | withCurrentLHS n
270 |     = do meta <- get MD
271 |          n' <- getFullName n
272 |          maybe (pure ())
273 |                (\lhs => put MD ({ holeLHS $= ((n', lhs) ::) } meta))
274 |                (currentLHS meta)
275 |
276 | findEntryWith : (NonEmptyFC -> a -> Bool) -> List (NonEmptyFC, a) -> Maybe (NonEmptyFC, a)
277 | findEntryWith = find . uncurry
278 |
279 | export
280 | findLHSAt : {auto m : Ref MD Metadata} ->
281 |             (NonEmptyFC -> ClosedTerm -> Bool) ->
282 |             Core (Maybe (NonEmptyFC, Nat, ClosedTerm))
283 | findLHSAt p
284 |     = do meta <- get MD
285 |          pure (findEntryWith (\ loc, tm => p loc (snd tm)) (lhsApps meta))
286 |
287 | export
288 | findTypeAt : {auto m : Ref MD Metadata} ->
289 |              (NonEmptyFC -> (Name, Nat, ClosedTerm) -> Bool) ->
290 |              Core (Maybe (Name, Nat, ClosedTerm))
291 | findTypeAt p
292 |     = do meta <- get MD
293 |          pure (map snd (findEntryWith p (names meta)))
294 |
295 | export
296 | findTyDeclAt : {auto m : Ref MD Metadata} ->
297 |                (NonEmptyFC -> (Name, Nat, ClosedTerm) -> Bool) ->
298 |                Core (Maybe (NonEmptyFC, Name, Nat, ClosedTerm))
299 | findTyDeclAt p
300 |     = do meta <- get MD
301 |          pure (findEntryWith p (tydecls meta))
302 |
303 | export
304 | findHoleLHS : {auto m : Ref MD Metadata} ->
305 |               Name -> Core (Maybe ClosedTerm)
306 | findHoleLHS hn
307 |     = do meta <- get MD
308 |          pure (lookupBy (\x, y => dropNS x == dropNS y) hn (holeLHS meta))
309 |
310 | export
311 | addSemanticDefault : {auto m : Ref MD Metadata} ->
312 |                      ASemanticDecoration -> Core ()
313 | addSemanticDefault asem = update MD { semanticDefaults $= insert asem }
314 |
315 | export
316 | addSemanticAlias : {auto m : Ref MD Metadata} ->
317 |                    NonEmptyFC -> NonEmptyFC -> Core ()
318 | addSemanticAlias from to = update MD { semanticAliases $= insert (from, to) }
319 |
320 | export
321 | addSemanticDecorations : {auto m : Ref MD Metadata} ->
322 |                          {auto c : Ref Ctxt Defs} ->
323 |    SemanticDecorations -> Core ()
324 | addSemanticDecorations decors
325 |     = do meta <- get MD
326 |          let posmap = meta.semanticHighlighting
327 |          let (newDecors,droppedDecors) =
328 |                span
329 |                  ( (meta.sourceIdent ==)
330 |                  . Builtin.fst
331 |                  . Builtin.fst )
332 |                  decors
333 |          unless (isNil droppedDecors)
334 |            $ log "ide-mode.highlight" 19 $ "ignored adding decorations to "
335 |                ++ show meta.sourceIdent ++ ": " ++ show droppedDecors
336 |          put MD $ {semanticHighlighting
337 |                      := (fromList newDecors) `union` posmap} meta
338 |
339 |
340 | -- Normalise all the types of the names, since they might have had holes
341 | -- when added and the holes won't necessarily get saved
342 | normaliseTypes : {auto m : Ref MD Metadata} ->
343 |                  {auto c : Ref Ctxt Defs} ->
344 |                  Core ()
345 | normaliseTypes
346 |     = do meta <- get MD
347 |          defs <- get Ctxt
348 |          ns' <- traverse (nfType defs) (names meta)
349 |          put MD ({ names := ns' } meta)
350 |   where
351 |     nfType : Defs -> (NonEmptyFC, (Name, Nat, ClosedTerm)) ->
352 |              Core (NonEmptyFC, (Name, Nat, ClosedTerm))
353 |     nfType defs (loc, (n, len, ty))
354 |        = pure (loc, (n, len, !(normaliseArgHoles defs Env.empty ty)))
355 |
356 | record TTMFile where
357 |   constructor MkTTMFile
358 |   version : Int
359 |   metadata : Metadata
360 |
361 | TTC TTMFile where
362 |   toBuf file
363 |       = do toBuf "TTM"
364 |            toBuf (version file)
365 |            toBuf (metadata file)
366 |
367 |   fromBuf
368 |       = do hdr <- fromBuf
369 |            when (hdr /= "TTM") $ corrupt "TTM header"
370 |            ver <- fromBuf
371 |            checkTTCVersion "" ver ttcVersion -- maybe change the interface to get the filename
372 |            md <- fromBuf
373 |            pure (MkTTMFile ver md)
374 |
375 | HasNames Metadata where
376 |   full gam md
377 |       = pure $ { lhsApps := !(traverse fullLHS $ md.lhsApps)
378 |                , names   := !(traverse fullTy $ md.names)
379 |                , tydecls := !(traverse fullTy $ md.tydecls)
380 |                , currentLHS := Nothing
381 |                , holeLHS := !(traverse fullHLHS $ md.holeLHS)
382 |                , nameLocMap := fromList !(traverse fullDecls (toList $ md.nameLocMap))
383 |                } md
384 |     where
385 |       fullLHS : (NonEmptyFC, (Nat, ClosedTerm)) -> Core (NonEmptyFC, (Nat, ClosedTerm))
386 |       fullLHS (fc, (i, tm)) = pure (fc, (i, !(full gam tm)))
387 |
388 |       fullTy : (NonEmptyFC, (Name, Nat, ClosedTerm)) -> Core (NonEmptyFC, (Name, Nat, ClosedTerm))
389 |       fullTy (fc, (n, i, tm)) = pure (fc, (!(full gam n), i, !(full gam tm)))
390 |
391 |       fullHLHS : (Name, ClosedTerm) -> Core (Name, ClosedTerm)
392 |       fullHLHS (n, tm) = pure (!(full gam n), !(full gam tm))
393 |
394 |       fullDecls : (NonEmptyFC, Name) -> Core (NonEmptyFC, Name)
395 |       fullDecls (fc, n) = pure (fc, !(full gam n))
396 |
397 |   resolved gam (MkMetadata lhs ns tys clhs hlhs dlocs fname semhl semal semdef)
398 |       = pure $ MkMetadata !(traverse resolvedLHS lhs)
399 |                           !(traverse resolvedTy ns)
400 |                           !(traverse resolvedTy tys)
401 |                           Nothing
402 |                           !(traverse resolvedHLHS hlhs)
403 |                           (fromList !(traverse resolvedDecls (toList dlocs)))
404 |                           fname
405 |                           semhl
406 |                           semal
407 |                           semdef
408 |     where
409 |       resolvedLHS : (NonEmptyFC, (Nat, ClosedTerm)) -> Core (NonEmptyFC, (Nat, ClosedTerm))
410 |       resolvedLHS (fc, (i, tm)) = pure (fc, (i, !(resolved gam tm)))
411 |
412 |       resolvedTy : (NonEmptyFC, (Name, Nat, ClosedTerm)) -> Core (NonEmptyFC, (Name, Nat, ClosedTerm))
413 |       resolvedTy (fc, (n, i, tm)) = pure (fc, (!(resolved gam n), i, !(resolved gam tm)))
414 |
415 |       resolvedHLHS : (Name, ClosedTerm) -> Core (Name, ClosedTerm)
416 |       resolvedHLHS (n, tm) = pure (!(resolved gam n), !(resolved gam tm))
417 |
418 |       resolvedDecls : (NonEmptyFC, Name) -> Core (NonEmptyFC, Name)
419 |       resolvedDecls (fc, n) = pure (fc, !(resolved gam n))
420 |
421 | export
422 | writeToTTM : {auto c : Ref Ctxt Defs} ->
423 |              {auto m : Ref MD Metadata} ->
424 |              (fname : String) ->
425 |              Core ()
426 | writeToTTM fname
427 |     = do normaliseTypes
428 |          buf <- initBinary
429 |          meta <- get MD
430 |          defs <- get Ctxt
431 |          toBuf (MkTTMFile ttcVersion !(full (gamma defs) meta))
432 |          Right ok <- coreLift $ writeToFile fname !(get Bin)
433 |              | Left err => throw (InternalError (fname ++ ": " ++ show err))
434 |          pure ()
435 |
436 | export
437 | readFromTTM : {auto m : Ref MD Metadata} ->
438 |               (fname : String) ->
439 |               Core ()
440 | readFromTTM fname
441 |     = do Right buf <- coreLift $ readFromFile fname
442 |              | Left err => throw (InternalError (fname ++ ": " ++ show err))
443 |          bin <- newRef Bin buf
444 |          ttm <- fromBuf
445 |          put MD (metadata ttm)
446 |
447 | ||| Read Metadata from given file
448 | export
449 | readMetadata : (fname : String) -> Core Metadata
450 | readMetadata fname
451 |   = do Right buf <- coreLift $ readFromFile fname
452 |              | Left err => throw (InternalError (fname ++ ": " ++ show err))
453 |        bin <- newRef Bin buf
454 |        MkTTMFile _ md <- fromBuf
455 |        pure md
456 |
457 | ||| Dump content of a .ttm file in human-readable format
458 | export
459 | dumpTTM : (filename : String) -> Core ()
460 | dumpTTM fname
461 |     = do md <- readMetadata fname
462 |          coreLift $ putStrLn $ show md
463 |