0 | module Idris.Syntax.TTC
  1 |
  2 | import public Core.Binary
  3 | import public Core.TTC
  4 |
  5 | import TTImp.TTImp
  6 | import TTImp.TTImp.TTC
  7 |
  8 | import Idris.Syntax
  9 |
 10 | import Data.SortedMap
 11 |
 12 | import Libraries.Data.ANameMap
 13 | import Libraries.Data.NameMap
 14 | import Libraries.Data.NatSet
 15 |
 16 | %default covering
 17 |
 18 | export
 19 | TTC IFaceInfo where
 20 |   toBuf (MkIFaceInfo ic impps ps cs ms ds)
 21 |       = do toBuf ic
 22 |            toBuf impps
 23 |            toBuf ps
 24 |            toBuf cs
 25 |            toBuf ms
 26 |            toBuf ds
 27 |
 28 |   fromBuf
 29 |       = do ic <- fromBuf
 30 |            impps <- fromBuf
 31 |            ps <- fromBuf
 32 |            cs <- fromBuf
 33 |            ms <- fromBuf
 34 |            ds <- fromBuf
 35 |            pure (MkIFaceInfo ic impps ps cs ms ds)
 36 |
 37 | export
 38 | TTC Fixity where
 39 |   toBuf InfixL = tag 0
 40 |   toBuf InfixR = tag 1
 41 |   toBuf Infix = tag 2
 42 |   toBuf Prefix = tag 3
 43 |
 44 |   fromBuf
 45 |       = case !getTag of
 46 |              0 => pure InfixL
 47 |              1 => pure InfixR
 48 |              2 => pure Infix
 49 |              3 => pure Prefix
 50 |              _ => corrupt "Fixity"
 51 |
 52 | export
 53 | TTC Import where
 54 |   toBuf (MkImport loc reexport path nameAs)
 55 |     = do toBuf loc
 56 |          toBuf reexport
 57 |          toBuf path
 58 |          toBuf nameAs
 59 |
 60 |   fromBuf
 61 |     = do loc <- fromBuf
 62 |          reexport <- fromBuf
 63 |          path <- fromBuf
 64 |          nameAs <- fromBuf
 65 |          pure (MkImport loc reexport path nameAs)
 66 |
 67 | export
 68 | TTC BindingModifier where
 69 |   toBuf NotBinding = tag 0
 70 |   toBuf Typebind = tag 1
 71 |   toBuf Autobind = tag 2
 72 |   fromBuf
 73 |       = case !getTag of
 74 |              0 => pure NotBinding
 75 |              1 => pure Typebind
 76 |              2 => pure Autobind
 77 |              _ => corrupt "binding"
 78 |
 79 | export
 80 | TTC FixityInfo where
 81 |   toBuf fx
 82 |       = do toBuf fx.fc
 83 |            toBuf fx.vis
 84 |            toBuf fx.bindingInfo
 85 |            toBuf fx.fix
 86 |            toBuf fx.precedence
 87 |   fromBuf
 88 |       = do fc <- fromBuf
 89 |            vis <- fromBuf
 90 |            binding <- fromBuf
 91 |            fix <- fromBuf
 92 |            prec <- fromBuf
 93 |            pure $ MkFixityInfo fc vis binding fix prec
 94 |
 95 |
 96 | export
 97 | TTC SyntaxInfo where
 98 |   toBuf syn
 99 |       = do toBuf (ANameMap.toList (fixities syn))
100 |            toBuf (filter (\n => elemBy (==) (fst n) (saveMod syn))
101 |                            (SortedMap.toList $ modDocstrings syn))
102 |            toBuf (filter (\n => elemBy (==) (fst n) (saveMod syn))
103 |                            (SortedMap.toList $ modDocexports syn))
104 |            toBuf (filter (\n => fst n `elem` saveIFaces syn)
105 |                            (ANameMap.toList (ifaces syn)))
106 |            toBuf (filter (\n => isJust (lookup (fst n) (saveDocstrings syn)))
107 |                            (ANameMap.toList (defDocstrings syn)))
108 |            toBuf (bracketholes syn)
109 |            toBuf (startExpr syn)
110 |            toBuf (holeNames syn)
111 |
112 |   fromBuf
113 |       = do fix <- fromBuf
114 |            moddstr <- fromBuf
115 |            modexpts <- fromBuf
116 |            ifs <- fromBuf
117 |            defdstrs <- fromBuf
118 |            bhs <- fromBuf
119 |            start <- fromBuf
120 |            hnames <- fromBuf
121 |            pure $ MkSyntax (fromList fix)
122 |                    [] (fromList moddstr) (fromList modexpts)
123 |                    [] (fromList ifs)
124 |                    empty (fromList defdstrs)
125 |                    bhs
126 |                    [] start
127 |                    hnames
128 |