idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-16 07:34:45 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #1769 from andrevidela/fix-fromString-interpolation

Browse Source 
Remove `fromString` calls from interpolated strings
This commit is contained in:
André Videla 2021-07-25 17:18:20 +00:00 committed by GitHub
commit aa77b7f33e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 11 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/Idris/Desugar.idr
View File

@ -334,8 +334,18 @@ mutual
pure $ Implicit fc False
desugarB side ps (PMultiline fc indent lines)
= addFromString fc !(expandString side ps fc !(trimMultiline fc indent lines))
-- We only add `fromString` if we are looking at a plain string literal.
-- Interpolated string literals don't have a `fromString` call since they
-- are always concatenated with other strings and therefore can never use
-- another `fromString` implementation that differs from `id`.
desugarB side ps (PString fc [])
= addFromString fc (IPrimVal fc (Str ""))
desugarB side ps (PString fc [StrLiteral fc' str])
= addFromString fc (IPrimVal fc' (Str str))
desugarB side ps (PString fc strs)
= addFromString fc !(expandString side ps fc strs)
= expandString side ps fc strs
desugarB side ps (PDoBlock fc ns block)
= expandDo side ps fc ns block
desugarB side ps (PBang fc term)