Merge pull request #69 from alexhumphreys/feat/fromDhall-ADTs-PR

add `fromDhall` deriving for ADTs

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

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

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))

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'

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

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

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!"))
 ```
 

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

samples/package.dhall → examples/package.dhall

@@ -1,5 +1,5 @@
 { package = "myidrispackage"
 , sourcedir = Some "./"
 , depends = Some ["contrib"]
-, modules = ["MyIdrisPackage.Main"]
+, modules = ["MyIdrisPackage.Main", "MyIdrisPackage.Foo"]
 }

idrall.ipkg

@@ -16,4 +16,5 @@ modules = Idrall.Expr
         , Idrall.Path
         , Idrall.TestHelper
         , Idrall.APIv1
+        , Idrall.API.V2
         , Idrall.Derive

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