Skip to content

Commit

Permalink
Merge pull request #108 from mattpolzin/as-text
Browse files Browse the repository at this point in the history
Add support for resolving an import as plain text.
  • Loading branch information
mattpolzin authored Oct 16, 2023
2 parents ecb9f0c + ca62835 commit 6deee64
Show file tree
Hide file tree
Showing 5 changed files with 52 additions and 27 deletions.
65 changes: 42 additions & 23 deletions Idrall/Resolve.idr
Original file line number Diff line number Diff line change
Expand Up @@ -45,29 +45,25 @@ alreadyImported fc xs x = case elem x xs of
False => pure ()
True => Left (CyclicImportError fc ((show x) ++ " in " ++ (show xs)))

mutual
resolveEnvVar : FC -> (history : List FilePath) -> Maybe FilePath -> String -> IOEither Error (Expr Void)
resolveEnvVar fc h p x = do
str <- readEnvVar fc x
expr <- mapErr (parseErrorHandler fc) (liftEither (parseWith Nothing str))
resolve h p (fst expr)
||| Read a file in the IOEither monad.
readFile' : FC -> String -> IOEither Error String
readFile' fc filePath =
let contents = MkIOEither (readFile filePath) in
mapErr (fileErrorHandler fc filePath) contents

resolveLocalFile : FC -> (history : List FilePath) -> (current : Maybe FilePath) -> (next : FilePath) -> IOEither Error (Expr Void)
resolveLocalFile fc h current next =
let combinedFilePaths = combinePaths current next in
go combinedFilePaths
where
readFile' : String -> IOEither Error String
readFile' x =
let contents = MkIOEither (readFile x) in
mapErr (fileErrorHandler fc x) contents
go : FilePath -> IOEither Error (Expr Void)
go p = do
liftEither (alreadyImported fc h (normaliseFilePath p))
let fp = canonicalFilePath p
str <- readFile' fp
expr <- mapErr (parseErrorHandler fc) (liftEither (parseWith (Just fp) str))
resolve (normaliseFilePath p :: h) (Just p) (fst expr)
record LocalFile where
constructor MkLocalFile
filePath : FilePath
contents : String

readLocalFile : FC -> (history : List FilePath) -> (current : Maybe FilePath) -> (next : FilePath) -> IOEither Error LocalFile
readLocalFile fc h current next = do
let combinedFilePaths = combinePaths current next
liftEither (alreadyImported fc h (normaliseFilePath combinedFilePaths))
let fp = canonicalFilePath combinedFilePaths
MkLocalFile combinedFilePaths <$> readFile' fc fp

mutual

export
covering
Expand Down Expand Up @@ -261,10 +257,33 @@ mutual
resolve h p (EEmbed fc (Raw (EnvVar x))) = resolveEnvVar fc h p x
resolve h p (EEmbed fc (Raw (Http x))) = MkIOEither (pure (Left (ErrorMessage fc "TODO http imports not implemented")))
resolve h p (EEmbed fc (Raw Missing)) = MkIOEither (pure (Left (ErrorMessage fc "No valid imports")))
resolve h p (EEmbed fc (Text a)) = MkIOEither (pure (Left (ErrorMessage fc "TODO as Text not implemented")))
resolve h p (EEmbed fc (Text a)) = resolveImportAsText fc h p a
resolve h p (EEmbed fc (Location a)) = MkIOEither (pure (Left (ErrorMessage fc "TODO as Location not implemented")))
resolve h p (EEmbed fc (Resolved x)) = MkIOEither (pure (Left (ErrorMessage fc "Already resolved")))
resolveImportAsText : FC -> (history : List FilePath) -> Maybe FilePath -> ImportStatement -> IOEither Error (Expr Void)
resolveImportAsText fc h p importStatement = do
str <- resolveImportToStr fc h p importStatement
pure $ ETextLit fc (MkChunks [] str)
where
resolveImportToStr : FC -> (history : List FilePath) -> Maybe FilePath -> ImportStatement -> IOEither Error String
resolveImportToStr fc h p (LocalFile fp) = contents <$> readLocalFile fc h p fp
resolveImportToStr fc h p (EnvVar str) = readEnvVar fc str
resolveImportToStr fc h p (Http str) = MkIOEither (pure (Left (ErrorMessage fc "TODO http imports not implemented")))
resolveImportToStr fc h p Missing = MkIOEither (pure (Left (ErrorMessage fc "No valid imports")))
resolveEnvVar : FC -> (history : List FilePath) -> Maybe FilePath -> String -> IOEither Error (Expr Void)
resolveEnvVar fc h p x = do
str <- readEnvVar fc x
expr <- mapErr (parseErrorHandler fc) (liftEither (parseWith Nothing str))
resolve h p (fst expr)
resolveLocalFile : FC -> (history : List FilePath) -> (current : Maybe FilePath) -> (next : FilePath) -> IOEither Error (Expr Void)
resolveLocalFile fc h current next = do
MkLocalFile filePath contents <- readLocalFile fc h current next
expr <- mapErr (parseErrorHandler fc) (liftEither (parseWith (Just $ canonicalFilePath filePath) contents))
resolve (normaliseFilePath filePath :: h) (Just filePath) (fst expr)
resolveRecord : (history : List FilePath)
-> Maybe FilePath
-> List (FieldName, Expr ImportStatement)
Expand Down
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -81,10 +81,10 @@ Most language features are in and should be working relatively correctly. The im
### Imports
- [x] Keyword: missing
- [x] Operator: ?
- [ ] Keyword: as Text
- [x] Keyword: as Text
- [ ] Keyword: using
- [x] Local imports (/path/to/file.dhall)
- [ ] Environment variables
- [x] Environment variables
- [ ] HTTP imports
- [ ] Semantic integrity checks

Expand Down
4 changes: 2 additions & 2 deletions tests/idrall/idrall002/expected
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,13 @@ Main> Testing: ../../../dhall-lang/tests/type-inference/success/CacheImportsA.dh
7| : https://test.dhall-lang.org/random-string as Text
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

../../../dhall-lang/tests/type-inference/success/CacheImportsA.dhall:(7, 7)-(7, 56)ErrorMessage: "TODO as Text not implemented"
../../../dhall-lang/tests/type-inference/success/CacheImportsA.dhall:(7, 7)-(7, 56)ErrorMessage: "TODO http imports not implemented"

Testing: ../../../dhall-lang/tests/type-inference/success/CacheImportsCanonicalizeA.dhall
6| : https://test.dhall-lang.org/random-string as Text
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

../../../dhall-lang/tests/type-inference/success/CacheImportsCanonicalizeA.dhall:(6, 7)-(6, 56)ErrorMessage: "TODO as Text not implemented"
../../../dhall-lang/tests/type-inference/success/CacheImportsCanonicalizeA.dhall:(6, 7)-(6, 56)ErrorMessage: "TODO http imports not implemented"

Testing: ../../../dhall-lang/tests/type-inference/success/accessEncodedTypeA.dhall
Testing: ../../../dhall-lang/tests/type-inference/success/accessTypeA.dhall
Expand Down
5 changes: 5 additions & 0 deletions tests/idrall/idrall003/Imports.idr
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,13 @@ testImportEnv : IOEither Error Value
testImportEnv = do
roundTripEval "env:IDRALL_TEST"

testImportEnvAsText : IOEither Error Value
testImportEnvAsText = do
roundTripEval "env:IDRALL_TEST as Text"

main : IO ()
main = do
putStrLn !(showIOEither testImport)
putStrLn !(showIOEither testImportFail)
putStrLn !(showIOEither testImportEnv)
putStrLn !(showIOEither testImportEnvAsText)
1 change: 1 addition & 0 deletions tests/idrall/idrall003/expected
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
Main> Success: (VNaturalLit 3)
Error: //tmp/./importFailB.dhall:(0, 0)-(0, 19)CyclicImportError: (MkFilePath (Absolute ["", "tmp"]) Just "importFailA.dhall") in [(MkFilePath (Absolute ["", "tmp"]) Just "importFailB.dhall"), (MkFilePath (Absolute ["", "tmp"]) Just "importFailA.dhall")]
Success: (VBoolLit True)
Success: (VTextLit (MkVChunks [] "True"))
Main>

0 comments on commit 6deee64

Please sign in to comment.