From c544b7c22b2d7eb3b8af3e404f1423fa54f76969 Mon Sep 17 00:00:00 2001 From: Alex Humphreys Date: Sun, 27 Jun 2021 13:17:40 +0200 Subject: [PATCH] add `fromDhall` deriving for ADTs Also update the docs for how to use the elaborator reflection interface. --- Idrall/API/V2.idr | 24 +++++++ Idrall/APIv1.idr | 13 ++++ Idrall/Derive.idr | 83 +++++++++++++++++-------- Idrall/Error.idr | 2 + Idrall/Eval.idr | 11 ++++ Idrall/IOEither.idr | 4 ++ README.md | 39 ++++++++++-- examples.txt | 6 -- examples/Package.idr | 23 +++++++ {samples => examples}/if-function.dhall | 0 {samples => examples}/package.dhall | 2 +- idrall.ipkg | 1 + tests/Main.idr | 10 ++- tests/derive/derive001/Derive.idr | 60 +++++++++++++++--- tests/derive/derive001/expected | 6 +- tests/examples/example001/.gitignore | 2 + tests/examples/example001/expected | 1 + tests/examples/example001/run | 5 ++ 18 files changed, 241 insertions(+), 51 deletions(-) create mode 100644 Idrall/API/V2.idr delete mode 100644 examples.txt create mode 100644 examples/Package.idr rename {samples => examples}/if-function.dhall (100%) rename {samples => examples}/package.dhall (59%) create mode 100644 tests/examples/example001/.gitignore create mode 100644 tests/examples/example001/expected create mode 100644 tests/examples/example001/run diff --git a/Idrall/API/V2.idr b/Idrall/API/V2.idr new file mode 100644 index 0000000..ea2e3c5 --- /dev/null +++ b/Idrall/API/V2.idr @@ -0,0 +1,24 @@ +module Idrall.API.V2 + +import Idrall.Value +import public Idrall.Expr +import public Idrall.Error +import public Idrall.Derive +import public Idrall.IOEither +import Idrall.APIv1 + +import System.Path -- TODO make public export in System.Directory.Tree? + +liftMaybe : Maybe a -> IOEither Error a +liftMaybe Nothing = MkIOEither $ pure $ Left $ FromDhallError "failed to convert from dhall" +liftMaybe (Just x) = pure x + +export +deriveFromDhallString : FromDhall ty => String -> IOEither Error ty +deriveFromDhallString x = do + e <- roundTripCheckEvalQuote $ x + liftMaybe $ fromDhall e + +export +deriveFromDhallFile : FromDhall a => Path -> IOEither Error a +deriveFromDhallFile = deriveFromDhallString . show diff --git a/Idrall/APIv1.idr b/Idrall/APIv1.idr index 4b2752b..9d997f9 100644 --- a/Idrall/APIv1.idr +++ b/Idrall/APIv1.idr @@ -50,6 +50,19 @@ evalQuote x = do e <- quote [] v pure e +export +roundTripEvalQuote : String -> IOEither Error (Expr Void) +roundTripEvalQuote x = do + xE <- exprFromString x + liftEither (evalQuote xE) + +export +roundTripCheckEvalQuote : String -> IOEither Error (Expr Void) +roundTripCheckEvalQuote x = do + xV <- roundTripCheckEval x + xE <- liftEither (quote [] xV) + pure $ xE + export roundTripEvalQuoteConv : String -> String -> IOEither Error () roundTripEvalQuoteConv x y = do diff --git a/Idrall/Derive.idr b/Idrall/Derive.idr index 1b2092a..5cae0d3 100644 --- a/Idrall/Derive.idr +++ b/Idrall/Derive.idr @@ -5,6 +5,7 @@ import Data.List1 import public Data.String import Idrall.Expr +import Idrall.Eval %language ElabReflection @@ -86,7 +87,10 @@ getArgs (IPi _ _ _ (Just n) argTy retTy) = ((n, argTy) ::) <$> getArgs retTy getArgs (IPi _ _ _ Nothing _ _) = fail $ "All arguments must be explicitly named" getArgs _ = pure [] -logCons : (List (Name, List (Name, TTImp))) -> Elab () +Cons : Type +Cons = (List (Name, List (Name, TTImp))) + +logCons : Cons -> Elab () logCons [] = pure () logCons (x :: xs) = do more x @@ -95,13 +99,13 @@ where go : List (Name, TTImp) -> Elab () go [] = pure () go ((n, t) :: ys) = do - logMsg "" 7 ("Name: " ++ show n) - logTerm "" 7 "Type" t + logMsg "" 7 ("ArgName: " ++ show n) + logTerm "" 7 "ArgType" t go ys more : (Name, List (Name, TTImp)) -> Elab () - more (n, xs) = do - logMsg "" 7 ("name1: " ++ show n) - go xs + more (constructor', args) = do + logMsg "" 7 ("Constructor: " ++ show constructor') + go args public export interface FromDhall a where @@ -127,6 +131,10 @@ FromDhall Double where fromDhall (EDoubleLit x) = pure x fromDhall _ = neutral +export +FromDhall String where + fromDhall x = strFromExpr x + export FromDhall a => FromDhall (List a) where fromDhall (EListLit _ xs) = pure $ !(traverse fromDhall xs) @@ -138,17 +146,25 @@ FromDhall a => FromDhall (Maybe a) where fromDhall ENone = neutral fromDhall _ = neutral +||| Used with FromDhall interface, to dervice implementations +||| for ADTs or Records +public export +data IdrisType + = ADT + | Record + export -deriveFromDhall : (name : Name) -> Elab () -deriveFromDhall n = - do [(n, _)] <- getType n +deriveFromDhall : IdrisType -> (name : Name) -> Elab () +deriveFromDhall it n = + do [(name, _)] <- getType n | _ => fail "Ambiguous name" - let funName = UN ("fromDhall" ++ show (stripNs n)) - let objName = UN ("__impl_fromDhall" ++ show (stripNs n)) + let funName = UN ("fromDhall" ++ show (stripNs name)) + let objName = UN ("__impl_fromDhall" ++ show (stripNs name)) - conNames <- getCons n + conNames <- getCons name -- get the constructors of the record + -- cons : (List (Name, List (Name, TTImp))) cons <- for conNames $ \n => do [(conName, conImpl)] <- getType n | _ => fail $ show n ++ "constructor must be in scope and unique" @@ -159,14 +175,8 @@ deriveFromDhall n = argName <- genReadableSym "arg" - -- given constructors, lookup names in json object for those constructors - clauses <- traverse (\(cn, as) => genClause funName cn argName (reverse as)) cons + clauses <- genClauses it funName argName cons - -- create function from JSON to Maybe Example - -- using the above clauses as patterns - let name = n - let clauses = [patClause `(~(var funName) (ERecordLit ~(bindvar $ show argName))) - (foldl (\acc, x => `(~x <|> ~acc)) `(Nothing) (clauses))] let funClaim = IClaim EmptyFC MW Export [Inline] (MkTy EmptyFC EmptyFC funName `(Expr Void -> Maybe ~(var name))) -- add a catch all pattern let funDecl = IDef EmptyFC funName (clauses ++ [patClause `(~(var funName) ~implicit') `(Nothing)]) @@ -185,14 +195,37 @@ deriveFromDhall n = let objDecl = IDef EmptyFC objName [(PatClause EmptyFC (var objName) objrhs)] declare [objClaim, objDecl] where - ||| moved from where clause - genClause : Name -> Name -> Name -> List (Name, TTImp) -> Elab (TTImp) - genClause funName t m xs = do + ||| moved from where clause, used for record constuctors + genClauseRecord : Name -> Name -> List (Name, TTImp) -> Elab (TTImp) + genClauseRecord constructor' arg xs = do let rhs = foldr (\(n, type), acc => let name = primStr $ (show n) in case type of `(Prelude.Types.Maybe _) => do - `(~acc <*> (pure $ lookup (MkFieldName ~name) ~(var m) >>= fromDhall)) - _ => `(~acc <*> (lookup (MkFieldName ~name) ~(var m) >>= fromDhall))) - `(pure ~(var t)) xs + `(~acc <*> (pure $ lookup (MkFieldName ~name) ~(var arg) >>= fromDhall)) + _ => `(~acc <*> (lookup (MkFieldName ~name) ~(var arg) >>= fromDhall))) + `(pure ~(var constructor')) xs pure (rhs) + genClauseADT : Name -> Name -> Name -> List (Name, TTImp) -> Elab (TTImp, TTImp) + genClauseADT funName constructor' arg xs = + let cn = primStr (show $ stripNs constructor') + debug = show $ constructor' + debug2 = show $ map fst xs + lhs = `(~(var funName) (EApp (EField (EUnion xs) (MkFieldName ~cn)) ~(bindvar $ show arg))) + in do + case xs of + [] => pure $ (lhs, `(pure ~(var constructor'))) + ((n, `(Prelude.Types.Maybe _)) :: []) => pure $ (lhs, `(pure ~(var constructor') <*> fromDhall ~(var arg))) + ((n, _) :: []) => pure $ (lhs, `(pure ~(var constructor') <*> fromDhall ~(var arg))) + (x :: _) => fail $ "too many args for constructor: " ++ show constructor' + genClauses : IdrisType -> Name -> Name -> Cons -> Elab (List Clause) + genClauses ADT funName arg cons = do + -- given constructors, lookup fields in dhall unions for those constructors + clausesADT <- traverse (\(cn, as) => genClauseADT funName cn arg (reverse as)) cons + pure $ map (\x => patClause (fst x) (snd x)) clausesADT + genClauses Record funName arg cons = do + -- given constructors, lookup names in dhall records for those constructors + clausesRecord <- traverse (\(cn, as) => genClauseRecord cn arg (reverse as)) cons + -- create clause from dhall to `Maybe a` using the above clauses as the rhs + pure $ pure $ patClause `(~(var funName) (ERecordLit ~(bindvar $ show arg))) + (foldl (\acc, x => `(~x <|> ~acc)) `(Nothing) (clausesRecord)) diff --git a/Idrall/Error.idr b/Idrall/Error.idr index 46ee250..df21527 100644 --- a/Idrall/Error.idr +++ b/Idrall/Error.idr @@ -29,6 +29,7 @@ data Error | InvalidRecordCompletion String | CyclicImportError String | EnvVarError String + | FromDhallError String | NestedError Error Error public export @@ -60,5 +61,6 @@ Show Error where show (InvalidRecordCompletion str) = "InvalidRecordCompletion: " ++ str show (CyclicImportError str) = "CyclicImportError: " ++ str show (EnvVarError str) = "EnvVarError " ++ show str + show (FromDhallError str) = "FromDhallError " ++ show str show (NestedError e e') = show e ++ "\n" ++ show e' diff --git a/Idrall/Eval.idr b/Idrall/Eval.idr index d3dc957..0da27c7 100644 --- a/Idrall/Eval.idr +++ b/Idrall/Eval.idr @@ -578,6 +578,17 @@ mutual convErr : (Show x) => x -> x -> Either Error a convErr x y = Left $ AlphaEquivError $ show x ++ "\n not alpha equivalent to:\n" ++ show y + export + strFromExpr : Expr Void -> Maybe String + strFromExpr (ETextLit (MkChunks [] x)) = pure x + strFromExpr (ETextLit (MkChunks (start :: xs) end)) = + let mid = traverse go xs in + pure $ !(go start) ++ (foldl (<+>) "" !mid) ++ end + where + go : (String, Expr Void) -> Maybe String + go (x, e) = pure $ x ++ !(strFromExpr e) + strFromExpr _ = Nothing + export strFromChunks : List (String, Value) -> Maybe String strFromChunks [] = Just neutral diff --git a/Idrall/IOEither.idr b/Idrall/IOEither.idr index ddd7178..931b055 100644 --- a/Idrall/IOEither.idr +++ b/Idrall/IOEither.idr @@ -31,6 +31,10 @@ export liftEither : Either e a -> IOEither e a liftEither = MkIOEither . pure +export +liftIOEither : IOEither e a -> IO (Either e a) +liftIOEither (MkIOEither x) = x + export mapErr : (e -> e') -> IOEither e a -> IOEither e' a mapErr f (MkIOEither x) = MkIOEither (do diff --git a/README.md b/README.md index 5ab1177..c2d012f 100644 --- a/README.md +++ b/README.md @@ -8,11 +8,38 @@ Parse, evaluate, check/infer types of Dhall expressions. ## Status -Still a work in progress, but for a given dhall expression with not much imports, this should be able to parse/type check and attempt evaluation. Type checker is complete (one test is failing but that is due to [this Idris2 issue](https://github.com/idris-lang/Idris2/issues/29). Need to start running the other tests like parsing/normalisation etc. Everything around imports needs some work, and also not sure what the API should look like. +Still a work in progress, but for a given dhall expression with not much imports, idrall should be able to parse/type check and attempt evaluation. Type checker is pretty complete (one test is failing but that is due to [this Idris2 issue](https://github.com/idris-lang/Idris2/issues/29). Need to start running the other tests like parsing/normalisation etc. Everything around imports needs some work. There's now an elaborator reflection, but it's pretty new so will see how it handles. -## Usage (very alpha, YMMV) +## Derive Usage (WIP) -These are all janky names and subject to change. +For an example of how to do a whole `parse -> resolve -> typecheck -> eval` pass of a dhall file, and marshall it into an idris type, check out the file [`./examples/Package.idr`](https://github.com/alexhumphreys/idrall/blob/master/examples/Package.idr) + +There Is a `FromDhall` interface that you can use elaborator reflection to derive. You can use it for both ADTs and Records like so: + +``` +-- ADT example +data ExADT1 + = Foo + | Bar Bool + | Baz (Maybe Bool) + +%runElab (deriveFromDhall ADT `{{ ExADT1 }}) + +-- Record example +record ExRec1 where + constructor MkExRec1 + mn : Maybe Nat + +%runElab (deriveFromDhall Record `{{ ExRec1 }}) +``` + +There's implementations of `FromDhall` for `String`, `Nat`, `Integer`, `Bool`, `Double`, and `List`/`Maybe` of those. That interface gives you the `fromDhall` function you can use on dhall expression to get a `Maybe` of your Idris ADT or Record. See the `./tests/derive` dir for some examples. + +The behaviour of this isn't thought out yet. For example, the `deriveFromDhall ADT` function ignores the dhall union and just looks for matching constructors. Also `deriveFromDhall Record` ignores extra fields on the dhall record. This behaviour may change. Also, as the elaborator reflection returns a `Maybe`, there's no good error messages when `fromDhall` fails, so that'll need updating. + +## Indepth Usage (very alpha, YMMV) + +Functions for parsing/evaluating/typechecking/resolving dhall expressions, should you need to ve a lot of control over how those things happen. These are all janky names and subject to change. There's some functions in `Idrall/APIv1.idr` that expose the parsing/type checking/evaluation. The `valueFromString` function takes a dhall string, infers it's type, then evaluates it. If you have `idris2` installed you can run the following shell commands (prefixed with a `$`) from the root dir of this repo: @@ -21,10 +48,10 @@ $ idris2 Idrall/APIv1.idr -p contrib --client ':exec doStuff valueFromString "{h Success: (VNaturalLit 5) ``` -You can also create local dhall files, like the one provided at `samples/if-function.dhall`: +You can also create local dhall files, like the one provided at `examples/if-function.dhall`: ``` -$ cat samples/if-function.dhall +$ cat examples/if-function.dhall let f = λ(x : Bool) → if x then "it's true!" @@ -35,7 +62,7 @@ in f True and use `valueFromString` to evaluate them as follows. Note the path in the string: ``` -$ idris2 Idrall/APIv1.idr -p contrib --client ':exec doStuff valueFromString "./samples/if-function.dhall"' +$ idris2 Idrall/APIv1.idr -p contrib --client ':exec doStuff valueFromString "./examples/if-function.dhall"' Success: (VTextLit (MkVChunks [] "it's true!")) ``` diff --git a/examples.txt b/examples.txt deleted file mode 100644 index 894ebba..0000000 --- a/examples.txt +++ /dev/null @@ -1,6 +0,0 @@ -:exec doStuff roundTripEval "(λ(x : Natural) → 2 + 3 + x) 10" -:exec doStuff roundTripSynth "True" -:exec doStuff roundTripSynth "Natural" -:exec doStuff roundTripEval "./foo.dhall" -:exec doStuff roundTripSynth "./foo.dhall" -:exec doStuff roundTripSynth "env:IDRALL_TEST" diff --git a/examples/Package.idr b/examples/Package.idr new file mode 100644 index 0000000..0a74df5 --- /dev/null +++ b/examples/Package.idr @@ -0,0 +1,23 @@ +module Main + +import Idrall.API.V2 + +import Language.Reflection +%language ElabReflection + +record Package where + constructor MkPackage + package : String + sourceDir : Maybe String + depends : Maybe (List String) + modules : List String +%runElab (deriveFromDhall Record `{{ Package }}) + +Show Package where + show (MkPackage package sourceDir depends modules) = + "MkPackage \{show package} \{show sourceDir} \{show depends} \{show modules}" + +main : IO () +main = do + package <- liftIOEither $ deriveFromDhallString {ty=Package} "./package.dhall" + putStrLn $ show package diff --git a/samples/if-function.dhall b/examples/if-function.dhall similarity index 100% rename from samples/if-function.dhall rename to examples/if-function.dhall diff --git a/samples/package.dhall b/examples/package.dhall similarity index 59% rename from samples/package.dhall rename to examples/package.dhall index 5c4b4d6..d3fae70 100644 --- a/samples/package.dhall +++ b/examples/package.dhall @@ -1,5 +1,5 @@ { package = "myidrispackage" , sourcedir = Some "./" , depends = Some ["contrib"] -, modules = ["MyIdrisPackage.Main"] +, modules = ["MyIdrisPackage.Main", "MyIdrisPackage.Foo"] } diff --git a/idrall.ipkg b/idrall.ipkg index 096d9d9..f73569f 100644 --- a/idrall.ipkg +++ b/idrall.ipkg @@ -16,4 +16,5 @@ modules = Idrall.Expr , Idrall.Path , Idrall.TestHelper , Idrall.APIv1 + , Idrall.API.V2 , Idrall.Derive diff --git a/tests/Main.idr b/tests/Main.idr index 7bd484d..4b7d31e 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -16,7 +16,7 @@ import Test.Golden %default covering allTests : TestPool -allTests = MkTestPool "dhall-lang tests" [] +allTests = MkTestPool "dhall-lang tests" [] Default [ "idrall001" , "idrall002" , "idrall003" @@ -25,14 +25,20 @@ allTests = MkTestPool "dhall-lang tests" [] ] deriveTests : TestPool -deriveTests = MkTestPool "derive tests" [] +deriveTests = MkTestPool "derive tests" [] Default [ "derive001" ] +examplesTests : TestPool +examplesTests = MkTestPool "examples tests" [] Default + [ "example001" + ] + main : IO () main = runner [ testPaths "idrall" allTests , testPaths "derive" deriveTests + , testPaths "examples" examplesTests ] where testPaths : String -> TestPool -> TestPool diff --git a/tests/derive/derive001/Derive.idr b/tests/derive/derive001/Derive.idr index bd5f816..fa4b4bf 100644 --- a/tests/derive/derive001/Derive.idr +++ b/tests/derive/derive001/Derive.idr @@ -13,31 +13,71 @@ import Language.Reflection %language ElabReflection -record Example3 where - constructor MkExample3 +record ExRec1 where + constructor MkExRec1 mn : Maybe Nat n : Nat i : Integer b : Bool + d : Double lb : List Bool + st : String + mst : Maybe String -- a6 : Nat -Show Example3 where - show (MkExample3 mn n i b lb) = - "(MkExample3 \{show mn} \{show n} \{show i} \{show b} \{show lb})" +Show ExRec1 where + show (MkExRec1 mn n i b d lb st mst) = + "(MkExample3 \{show mn} \{show n} \{show i} \{show b} \{show d} \{show lb} \{show st} \{show mst})" -%runElab (deriveFromDhall `{{ Example3 }}) +%runElab (deriveFromDhall Record `{{ ExRec1 }}) -bar3 : Maybe Example3 -bar3 = fromDhall +exRec1 : Maybe ExRec1 +exRec1 = fromDhall (ERecordLit $ fromList [ (MkFieldName "mn", ENaturalLit 3) , (MkFieldName "n", ENaturalLit 4) , (MkFieldName "i", EIntegerLit 5) , (MkFieldName "b", EBoolLit True) + , (MkFieldName "d", EDoubleLit 2.0) , (MkFieldName "lb", EListLit (Just EBool) [EBoolLit True, EBoolLit False]) - -- , (MkFieldName "a7", EBoolLit True) + , (MkFieldName "st", (ETextLit (MkChunks [] "hello"))) + , (MkFieldName "mst", (ETextLit (MkChunks [] "hello"))) ]) +data ExADT1 + = Foo + | Bar Bool + | Baz (Maybe Bool) + +Show ExADT1 where + show Foo = "Foo" + show (Bar x) = "(Bar \{show x})" + show (Baz x) = "(Baz \{show x})" + +%runElab (deriveFromDhall ADT `{{ ExADT1 }}) + +exADT1 : Maybe ExADT1 +exADT1 = fromDhall + (EApp (EField (EUnion $ fromList []) (MkFieldName "Foo")) $ ENaturalLit 3) +exADT2 : Maybe ExADT1 +exADT2 = fromDhall + (EApp (EField (EUnion $ fromList []) (MkFieldName "Bar")) $ EBoolLit True) +exADT3 : Maybe ExADT1 +exADT3 = fromDhall + (EApp (EField (EUnion $ fromList []) (MkFieldName "Baz")) $ ESome $ EBoolLit True) + +exADT4 : Maybe ExADT1 +exADT4 = fromDhall + (EApp (EField + ( EUnion $ fromList + [ ((MkFieldName "Bar"), Just EBool) + , ((MkFieldName "Foo"), Just ENatural) + ] + ) (MkFieldName "Foo")) (ENaturalLit 3)) + +putLines : Show a => List a -> IO () +putLines = putStrLn . fastAppend . (intersperse "\n") . map show + main : IO () -main = do printLn $ show bar3 +main = do putLines [exRec1] + putLines [exADT1, exADT2, exADT3, exADT4] diff --git a/tests/derive/derive001/expected b/tests/derive/derive001/expected index 5e4c558..1b5cd1d 100644 --- a/tests/derive/derive001/expected +++ b/tests/derive/derive001/expected @@ -1 +1,5 @@ -"Just (MkExample3 Just 3 4 5 True [True, False])" +Just (MkExample3 Just 3 4 5 True 2.0 [True, False] "hello" Just "hello") +Just Foo +Just (Bar True) +Just (Baz Just True) +Just Foo diff --git a/tests/examples/example001/.gitignore b/tests/examples/example001/.gitignore new file mode 100644 index 0000000..84feca9 --- /dev/null +++ b/tests/examples/example001/.gitignore @@ -0,0 +1,2 @@ +Package.idr +package.dhall diff --git a/tests/examples/example001/expected b/tests/examples/example001/expected new file mode 100644 index 0000000..bf1ab01 --- /dev/null +++ b/tests/examples/example001/expected @@ -0,0 +1 @@ +Right MkPackage "myidrispackage" Nothing Nothing ["MyIdrisPackage.Main", "MyIdrisPackage.Foo"] diff --git a/tests/examples/example001/run b/tests/examples/example001/run new file mode 100644 index 0000000..7c65b46 --- /dev/null +++ b/tests/examples/example001/run @@ -0,0 +1,5 @@ +cp ../../../examples/Package.idr . +cp ../../../examples/package.dhall . +idris2 --no-banner --no-color --console-width 0 -p contrib -p idrall Package.idr --exec main + +rm -rf build