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