Use reflection to generate Haskell types (#488)

* first draft of generating Haskell version of types

* start on tying everything together

* macro to generate all the marshalling for a type in one go

* generate HsTypes for records

* wip: generate haskell types

* Turn off verbosity for inlining tactic

* Clean up and fixes of Haskell type generation

* Start on generating Ledger types

* Auto generating all the ledger types

* Better control over names of generated Haskell code

* Use GHC Rationals

* Hack for RoseTree-like recursive types

* More field prefixes

* Fix import in Lib.hs

* Tests pass!

* Macro to generate type aliases for HsTypes

* Fix minor things

* Remove `Ledger.Foreign.LedgerTypes`

* Cleanup

* Fix Haskell compilation

---------

Co-authored-by: whatisRT <[email protected]>

src/Foreign/Convertible.agda

@@ -1,12 +1,16 @@
 module Foreign.Convertible where
 
 open import Ledger.Prelude
+open import Foreign.HaskellTypes
 
 record Convertible (A B : Type) : Type where
   field to   : A → B
         from : B → A
 open Convertible ⦃...⦄ public
 
+HsConvertible : (A : Set) → ⦃ HasHsType A ⦄ → Set
+HsConvertible A = Convertible A (HsType A)
+
 Convertible-Refl : ∀ {A} → Convertible A A
 Convertible-Refl = λ where .to → id; .from → id
 
@@ -16,8 +20,6 @@ Convertible₁ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible (T A)
 Convertible₂ : (Type → Type → Type) → (Type → Type → Type) → Type₁
 Convertible₂ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible₁ (T A) (U B)
 
--- ** instances
-
 Functor⇒Convertible : ∀ {F : Type↑} → ⦃ Functor F ⦄ → Convertible₁ F F
 Functor⇒Convertible = λ where
   .to   → map to
@@ -28,6 +30,12 @@ Bifunctor⇒Convertible = λ where
   .to   → bimap to to
   .from → bimap from from
 
+_⨾_ : ∀ {A B C} → Convertible A B → Convertible B C → Convertible A C
+(c ⨾ c') .to   = c' .to   ∘ c  .to
+(c ⨾ c') .from = c  .from ∘ c' .from
+
+-- ** instances
+
 open import Foreign.Haskell
 open import Foreign.Haskell.Coerce using (coerce)
 

src/Foreign/Convertible/Deriving.agda

@@ -29,7 +29,10 @@ open import Class.Traversable
 open import Class.Show
 open import Class.MonadReader
 
+open import Tactic.Substitute
 open import Foreign.Convertible
+open import Foreign.HaskellTypes
+open import Foreign.HaskellTypes.Deriving
 
 private instance
   _ = Functor-M {TC}
@@ -45,48 +48,6 @@ private
   variable
     A B C : Set
 
-  -- There aren't any nice substitution functions (that I can find) in the standard library or
-  -- stdlib-meta. This one is cheating since we only want to substitute lzero, which is a closed
-  -- term that never gets applied to anything.
-
-  Subst : Set → Set
-  Subst A = ℕ → Term → A → A
-
-  substTerm : Subst Term
-  substArgs : Subst (Args Term)
-  substArg  : Subst (Arg Term)
-  substAbs  : Subst (Abs Term)
-  substSort : Subst Sort
-
-  substTerm x s (var y args) =
-    case compare x y of λ where
-      (less _ _)    → var (y ∸ 1) (substArgs x s args)
-      (equal _)     → s  -- cheating and dropping the args!
-      (greater _ _) → var y (substArgs x s args)
-  substTerm x s (con c args) = con c (substArgs x s args)
-  substTerm x s (def f args) = def f (substArgs x s args)
-  substTerm x s (lam v t) = lam v (substAbs x s t)
-  substTerm x s (pat-lam cs args₁) = unknown  -- ignoring for now
-  substTerm x s (pi a b) = pi (substArg x s a) (substAbs x s b)
-  substTerm x s (agda-sort s₁) = agda-sort (substSort x s s₁)
-  substTerm x s (lit l) = lit l
-  substTerm x s (meta m args) = meta m (substArgs x s args)
-  substTerm x s unknown = unknown
-
-  substArgs x s [] = []
-  substArgs x s (a ∷ as) = substArg x s a ∷ substArgs x s as
-
-  substArg x s (arg i t) = arg i (substTerm x s t)
-
-  substAbs x s (abs z t) = abs z (substTerm (ℕ.suc x) s t)
-
-  substSort x s (set t) = set (substTerm x s t)
-  substSort x s (lit n) = lit n
-  substSort x s (prop t) = prop (substTerm x s t)
-  substSort x s (propLit n) = propLit n
-  substSort x s (inf n) = inf n
-  substSort x s unknown = unknown
-
   TyViewTel = List (Abs (Arg Type))
 
   substTel : Subst TyViewTel
@@ -156,6 +117,9 @@ private
     fromClauses ← mapM (conversionClause (quote Convertible.from) (quote from)) (L.zip hsCons agdaCons)
     return $ toClauses ++ fromClauses
 
+  absurdClause : Name → Clause
+  absurdClause prj = absurd-clause (("x" , vArg unknown) ∷ []) (vArg (proj prj) ∷ vArg (absurd 0) ∷ [])
+
   -- Compute conversion clauses for the current goal and wrap them in a pattern lambda.
   patternLambda : TC Term
   patternLambda = do
@@ -165,7 +129,12 @@ private
     hsCons   ← getConstrsForType `B
     toClauses   ← mapM (conversionClause (quote Convertible.to)   (quote to)  ) (L.zip agdaCons hsCons)
     fromClauses ← mapM (conversionClause (quote Convertible.from) (quote from)) (L.zip hsCons agdaCons)
-    return $ pat-lam (toClauses ++ fromClauses) []
+    case toClauses ++ fromClauses of λ where
+      []  → return $ pat-lam (absurdClause (quote Convertible.to) ∷ absurdClause (quote Convertible.from) ∷ []) []
+      cls → return $ pat-lam cls []
+
+doPatternLambda : Term → R.TC Term
+doPatternLambda hole = patternLambda =<< initTCEnvWithGoal hole
 
 -- Deriving a Convertible instance. Usage
 --   unquoteDecl iName = deriveConvertible iName (quote AgdaTy) (quote HsTy)
@@ -181,8 +150,10 @@ deriveConvertible instName agdaName hsName = initUnquoteWithGoal ⦃ defaultTCOp
   return _
 
 -- Macros providing an alternative interface. Usage
---  iName : ConvertibleType AgdaTy HsTy
---  iName = autoConvertible
+--   iName : ConvertibleType AgdaTy HsTy
+--   iName = autoConvertible
+-- or
+--   iName = autoConvert AgdaTy
 macro
   ConvertibleType : Name → Name → Tactic
   ConvertibleType agdaName hsName = initTac ⦃ defaultTCOptions ⦄ $
@@ -191,3 +162,11 @@ macro
   autoConvertible : Tactic
   autoConvertible = initTac ⦃ defaultTCOptions ⦄ $
     unifyWithGoal =<< patternLambda
+
+  autoConvert : Name → Tactic
+  autoConvert d hole = do
+    hsTyMeta ← R.newMeta `Set
+    R.checkType hole $ quote Convertible ∙⟦ d ∙ ∣ hsTyMeta ⟧
+    hsTy ← solveHsType (d ∙)
+    R.unify hsTyMeta hsTy
+    R.unify hole =<< doPatternLambda hole

src/Foreign/HaskellTypes.agda

@@ -0,0 +1,52 @@
+
+module Foreign.HaskellTypes where
+
+open import Level using (Level)
+open import Data.Bool.Base using (Bool)
+open import Data.Nat.Base using (ℕ)
+open import Data.String.Base using (String)
+open import Data.List.Base using (List)
+open import Data.Maybe.Base using (Maybe)
+open import Data.Sum.Base using (_⊎_)
+open import Data.Product.Base using (_×_)
+open import Data.Unit using (⊤)
+
+open import Foreign.Haskell.Pair using (Pair)
+open import Foreign.Haskell.Either using (Either)
+
+private variable
+  l : Level
+  A B : Set l
+
+record HasHsType (A : Set l) : Set₁ where
+  field
+    HsType : Set
+
+HsType : (A : Set l) → ⦃ HasHsType A ⦄ → Set
+HsType _ ⦃ i ⦄ = i .HasHsType.HsType
+
+MkHsType : (A : Set l) (Hs : Set) → HasHsType A
+MkHsType A Hs .HasHsType.HsType = Hs
+
+instance
+
+  iHsTy-ℕ      = MkHsType ℕ ℕ
+  iHsTy-Bool   = MkHsType Bool Bool
+  iHsTy-⊤      = MkHsType ⊤ ⊤
+  iHsTy-String = MkHsType String String
+
+  -- Could make a macro for these kind of congruence instances.
+  iHsTy-List : ⦃ HasHsType A ⦄ → HasHsType (List A)
+  iHsTy-List {A = A} .HasHsType.HsType = List (HsType A)
+
+  iHsTy-Maybe : ⦃ HasHsType A ⦄ → HasHsType (Maybe A)
+  iHsTy-Maybe {A = A} .HasHsType.HsType = Maybe (HsType A)
+
+  iHsTy-Fun : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A → B)
+  iHsTy-Fun {A = A} {B = B} .HasHsType.HsType = HsType A → HsType B
+
+  iHsTy-Sum : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A ⊎ B)
+  iHsTy-Sum {A = A} {B = B} .HasHsType.HsType = Either (HsType A) (HsType B)
+
+  iHsTy-Pair : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A × B)
+  iHsTy-Pair {A = A} {B = B} .HasHsType.HsType = Pair (HsType A) (HsType B)