0 | module Core.FC
  1 |
  2 | import Core.Name.Namespace
  3 |
  4 | import Data.Maybe
  5 | import Libraries.Text.Bounded
  6 | import Libraries.Text.PrettyPrint.Prettyprinter
  7 |
  8 | %default total
  9 |
 10 | ------------------------------------------------------------------------
 11 | -- Types
 12 |
 13 | public export
 14 | FilePos : Type
 15 | FilePos = (Int, Int)
 16 |
 17 | showPos : FilePos -> String
 18 | showPos (l, c) = show (l + 1) ++ ":" ++ show (c + 1)
 19 |
 20 | public export
 21 | FileName : Type
 22 | FileName = String
 23 |
 24 | public export
 25 | data VirtualIdent : Type where
 26 |   Interactive : VirtualIdent
 27 |
 28 | public export
 29 | Eq VirtualIdent where
 30 |   Interactive == Interactive = True
 31 |
 32 | export
 33 | Show VirtualIdent where
 34 |   show Interactive = "(Interactive)"
 35 |
 36 | public export
 37 | data OriginDesc : Type where
 38 |   ||| Anything that originates in physical Idris source files is assigned a
 39 |   ||| `PhysicalIdrSrc modIdent`,
 40 |   |||   where `modIdent` is the top-level module identifier of that file.
 41 |   PhysicalIdrSrc : (ident : ModuleIdent) -> OriginDesc
 42 |   ||| Anything parsed from a package file is decorated with `PhysicalPkgSrc fname`,
 43 |   |||   where `fname` is path to the package file.
 44 |   PhysicalPkgSrc : (fname : FileName) -> OriginDesc
 45 |   Virtual : (ident : VirtualIdent) -> OriginDesc
 46 |
 47 | public export
 48 | Eq OriginDesc where
 49 |   PhysicalIdrSrc ident == PhysicalIdrSrc ident' = ident == ident'
 50 |   PhysicalPkgSrc fname == PhysicalPkgSrc fname' = fname == fname'
 51 |   Virtual ident        == Virtual ident'        = ident == ident'
 52 |   _                    == _                     = False
 53 |
 54 | export
 55 | Show OriginDesc where
 56 |   show (PhysicalIdrSrc ident) = show ident
 57 |   show (PhysicalPkgSrc fname) = show fname
 58 |   show (Virtual ident) = show ident
 59 |
 60 | ||| A file context is a filename together with starting and ending positions.
 61 | ||| It's often carried by AST nodes that might have been created from a source
 62 | ||| file or by the compiler. That makes it useful to have the notion of
 63 | ||| `EmptyFC` as part of the type.
 64 | public export
 65 | data FC = MkFC        OriginDesc FilePos FilePos
 66 |         | ||| Virtual FCs are FC attached to desugared/generated code. They can help with marking
 67 |           ||| errors, but we shouldn't attach semantic highlighting metadata to them.
 68 |           MkVirtualFC OriginDesc FilePos FilePos
 69 |         | EmptyFC
 70 |
 71 | %name FC fc
 72 |
 73 | ||| A version of a file context that cannot be empty
 74 | public export
 75 | NonEmptyFC : Type
 76 | NonEmptyFC = (OriginDesc, FilePos, FilePos)
 77 |
 78 | ------------------------------------------------------------------------
 79 | -- Conversion between NonEmptyFC and FC
 80 |
 81 | ||| NonEmptyFC always embeds into FC
 82 | export
 83 | justFC : NonEmptyFC -> FC
 84 | justFC (fname, start, end) = MkFC fname start end
 85 |
 86 | ||| A view checking whether an arbitrary FC happens to be non-empty
 87 | export
 88 | isNonEmptyFC : FC -> Maybe NonEmptyFC
 89 | isNonEmptyFC (MkFC fn start end) = Just (fn, start, end)
 90 | isNonEmptyFC (MkVirtualFC fn start end) = Just (fn, start, end)
 91 | isNonEmptyFC EmptyFC = Nothing
 92 |
 93 | ||| A view checking whether an arbitrary FC originates from a source location
 94 | export
 95 | isConcreteFC : FC -> Maybe NonEmptyFC
 96 | isConcreteFC (MkFC fn start end) = Just (fn, start, end)
 97 | isConcreteFC _ = Nothing
 98 |
 99 | ||| Turn an FC into a virtual one
100 | export
101 | virtualiseFC : FC -> FC
102 | virtualiseFC (MkFC fn start end) = MkVirtualFC fn start end
103 | virtualiseFC fc = fc
104 |
105 | export
106 | defaultFC : NonEmptyFC
107 | defaultFC = (Virtual Interactive, (0, 0), (0, 0))
108 |
109 | export
110 | replFC : FC
111 | replFC = justFC defaultFC
112 |
113 | export
114 | toNonEmptyFC : FC -> NonEmptyFC
115 | toNonEmptyFC = fromMaybe defaultFC . isNonEmptyFC
116 |
117 | ------------------------------------------------------------------------
118 | -- Projections
119 |
120 | export
121 | origin : NonEmptyFC -> OriginDesc
122 | origin (fn, _, _) = fn
123 |
124 | export
125 | startPos : NonEmptyFC -> FilePos
126 | startPos (_, s, _) = s
127 |
128 | export
129 | startLine : NonEmptyFC -> Int
130 | startLine = fst . startPos
131 |
132 | export
133 | startCol : NonEmptyFC -> Int
134 | startCol = snd . startPos
135 |
136 | export
137 | endPos : NonEmptyFC -> FilePos
138 | endPos (_, _, e) = e
139 |
140 | export
141 | endLine : NonEmptyFC -> Int
142 | endLine = fst . endPos
143 |
144 | export
145 | endCol : NonEmptyFC -> Int
146 | endCol = snd . endPos
147 |
148 | ------------------------------------------------------------------------
149 | -- Smart constructors
150 |
151 | export
152 | boundToFC : OriginDesc -> WithBounds t -> FC
153 | boundToFC mbModIdent b = MkFC mbModIdent (start b) (end b)
154 |
155 | export
156 | (.toFC) : (o : OriginDesc) => WithBounds t -> FC
157 | x.toFC = boundToFC o x
158 |
159 | export
160 | boundToFC' : OriginDesc -> Bounds -> FC
161 | boundToFC' mbModIdent b = MkFC mbModIdent (startBounds b) (endBounds b)
162 |
163 | ------------------------------------------------------------------------
164 | -- Predicates
165 |
166 | --- Return whether a given file position is within the file context (assuming we're
167 | --- in the right file)
168 | export
169 | within : FilePos -> NonEmptyFC -> Bool
170 | within (x, y) (_, start, end)
171 |    = (x, y) >= start && (x, y) <= end
172 |
173 | -- Return whether a given line is on the same line as the file context (assuming
174 | -- we're in the right file)
175 | export
176 | onLine : Int -> NonEmptyFC -> Bool
177 | onLine x (_, start, end)
178 |    = x >= fst start && x <= fst end
179 |
180 | ------------------------------------------------------------------------
181 | -- Constant values
182 |
183 | export
184 | emptyFC : FC
185 | emptyFC = EmptyFC
186 |
187 | ------------------------------------------------------------------------
188 | -- Basic operations
189 | export
190 | mergeFC : FC -> FC -> Maybe FC
191 | mergeFC (MkFC fname1 start1 end1) (MkFC fname2 start2 end2) =
192 |   if fname1 == fname2
193 |   then Just $ MkFC fname1 (min start1 start2) (max end1 end2)
194 |   else Nothing
195 | mergeFC _ _ = Nothing
196 |
197 |
198 | %name FC fc
199 |
200 | ------------------------------------------------------------------------
201 | -- Instances
202 |
203 | export
204 | Eq FC where
205 |   (==) (MkFC n s e) (MkFC n' s' e') = n == n' && s == s' && e == e'
206 |   (==) (MkVirtualFC n s e) (MkVirtualFC n' s' e') = n == n' && s == s' && e == e'
207 |   (==) EmptyFC EmptyFC = True
208 |   (==) _ _ = False
209 |
210 | export
211 | Show FC where
212 |   show EmptyFC = "EmptyFC"
213 |   show (MkFC ident startPos endPos) = show ident ++ ":" ++
214 |              showPos startPos ++ "--" ++
215 |              showPos endPos
216 |   show (MkVirtualFC ident startPos endPos) = show ident ++ ":" ++
217 |              showPos startPos ++ "--" ++
218 |              showPos endPos
219 |
220 | prettyPos : FilePos -> Doc Void
221 | prettyPos = pretty . showPos
222 |
223 | export
224 | Pretty Void FC where
225 |   pretty EmptyFC = pretty "EmptyFC"
226 |   pretty (MkFC ident startPos endPos) = byShow ident <+> colon
227 |                  <+> prettyPos startPos <+> pretty "--"
228 |                  <+> prettyPos endPos
229 |   pretty (MkVirtualFC ident startPos endPos) = byShow ident <+> colon
230 |                  <+> prettyPos startPos <+> pretty "--"
231 |                  <+> prettyPos endPos
232 |