Generate Haskell code from the Agda spec

docs/agda-spec/src/Foreign/Convertible.agda

@@ -0,0 +1,82 @@
+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
+
+Convertible₁ : (Type → Type) → (Type → Type) → Type₁
+Convertible₁ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible (T A) (U B)
+
+Convertible₂ : (Type → Type → Type) → (Type → Type → Type) → Type₁
+Convertible₂ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible₁ (T A) (U B)
+
+Functor⇒Convertible : ∀ {F : Type↑} → ⦃ Functor F ⦄ → Convertible₁ F F
+Functor⇒Convertible = λ where
+  .to   → map to
+  .from → map from
+
+Bifunctor⇒Convertible : ∀ {F} → ⦃ Bifunctor F ⦄ → Convertible₂ F F
+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)
+
+instance
+  Convertible-Maybe : Convertible₁ Maybe Maybe
+  Convertible-Maybe = Functor⇒Convertible
+
+  Convertible-× : Convertible₂ _×_ _×_
+  Convertible-× = Bifunctor⇒Convertible
+
+  Convertible-Pair : Convertible₂ _×_ Pair
+  Convertible-Pair = λ where
+    .to   → coerce ∘ bimap to to
+    .from → bimap from from ∘ coerce
+
+  Convertible-⊎ : Convertible₂ _⊎_ _⊎_
+  Convertible-⊎ = Bifunctor⇒Convertible
+
+  Convertible-Either : Convertible₂ _⊎_ Either
+  Convertible-Either = λ where
+    .to   → coerce ∘ bimap to to
+    .from → bimap from from ∘ coerce
+
+  Convertible-FinSet : Convertible₁ ℙ_ List
+  Convertible-FinSet = λ where
+    .to   → map to   ∘ setToList
+    .from → fromList ∘ map from
+
+  Convertible-Map : ∀ {K K' V V'} → ⦃ DecEq K ⦄
+    → ⦃ Convertible K K' ⦄ → ⦃ Convertible V V' ⦄
+    → Convertible (K ⇀ V) (List $ Pair K' V')
+  Convertible-Map = λ where
+    .to   → to        ∘ proj₁
+    .from → fromListᵐ ∘ map from
+
+  Convertible-List : Convertible₁ List List
+  Convertible-List = λ where
+    .to   → map to
+    .from → map from
+
+  Convertible-Fun : ∀ {A A' B B'} → ⦃ Convertible A A' ⦄ → ⦃ Convertible B B' ⦄ → Convertible (A → B) (A' → B')
+  Convertible-Fun = λ where
+    .to   → λ f → to   ∘ f ∘ from
+    .from → λ f → from ∘ f ∘ to

docs/agda-spec/src/Foreign/Convertible/Deriving.agda

@@ -0,0 +1,172 @@
+module Foreign.Convertible.Deriving where
+
+open import Level
+open import MetaPrelude
+open import Meta
+
+import Data.List as L
+import Data.List.NonEmpty as NE
+import Data.String as S
+import Data.Product as P
+
+open import Relation.Nullary
+open import Relation.Nullary.Decidable
+
+open import Reflection.Tactic
+open import Reflection.AST.Term
+open import Reflection.AST.DeBruijn
+import Reflection.TCM as R
+open import Reflection.Utils
+open import Reflection.Utils.TCI
+import Function.Identity.Effectful as Identity
+
+open import Class.DecEq
+open import Class.DecEq
+open import Class.Functor
+open import Class.Monad
+open import Class.MonadTC.Instances
+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}
+
+-- TODO: move to agda-stdlib-meta
+liftTC : ∀ {a} {A : Set a} → R.TC A → TC A
+liftTC m _ = m
+
+private
+
+  open MonadReader ⦃...⦄
+
+  variable
+    A B C : Set
+
+  TyViewTel = List (Abs (Arg Type))
+
+  substTel : Subst TyViewTel
+  substTel x s [] = []
+  substTel x s (abs z t ∷ tel) = abs z (substArg x s t) ∷ (substTel (ℕ.suc x) s tel)
+    -- Note: `abs` is abused in TyViewTel and doesn't actually scope over the `t`
+
+  -- Substitute leading level parameters with lzero
+  smashLevels : TyViewTel → ℕ × TyViewTel
+  smashLevels (abs s (arg i (def (quote Level) [])) ∷ tel) =
+    P.map ℕ.suc (substTel 0 (quote 0ℓ ∙)) $ smashLevels tel
+  smashLevels tel = (0 , tel)
+
+  tyViewToTel : TyViewTel → Telescope
+  tyViewToTel = L.map λ where (abs s a) → s , a
+
+  hideTyView : Abs (Arg A) → Abs (Arg A)
+  hideTyView (abs s (arg (arg-info _ m) x)) = abs s (arg (arg-info hidden m) x)
+
+  -- The type of a Convertible instance. For parameterised types adds the appropriate instance
+  -- arguments and instantiates level arguments to lzero. For instance,
+  -- instanceType _⊎_ Hs.Either = {A B : Set} {a b : Set} → ⦃ Convertible A a ⦄ → ⦃ Convertible B b ⦄
+  --                              Convertible (A ⊎ B) (Hs.Either a b)
+  instanceType : (agdaName hsName : Name) → TC TypeView
+  instanceType agdaName hsName = do
+    aLvls , agdaParams ← smashLevels <$> getParamsAndIndices agdaName
+    hLvls , hsParams   ← smashLevels <$> getParamsAndIndices hsName
+    true ← return (length agdaParams == length hsParams)
+      where false → liftTC $ R.typeErrorFmt "%q and %q have different number of parameters" agdaName hsName
+    let n = length agdaParams
+        l₀ = quote 0ℓ ∙
+    agdaTy ← applyWithVisibility agdaName $ L.replicate aLvls l₀ ++ L.map ♯ (take n (downFrom (n + n)))
+    hsTy   ← applyWithVisibility hsName   $ L.replicate hLvls l₀ ++ L.map ♯ (downFrom n)
+    let instHead = weaken n $ quote Convertible ∙⟦ agdaTy ∣ hsTy ⟧
+        tel      = L.map hideTyView (agdaParams ++ hsParams) ++
+                   L.replicate n (abs "_" (iArg (quote Convertible ∙⟦ ♯ (n + n ∸ 1) ∣ ♯ (n ∸ 1) ⟧)))
+    return $ tel , instHead
+
+  -- Compute one clause of the Convertible instance. For instance,
+  -- conversionClause Convertible.to to ((c₁ , _) , (c₂ , _)) generates
+  -- .to (c₁ x₁ .. xn) = c₂ (to x₁) .. (to xn)
+  -- where the xi are the visible constructor arguments.
+  conversionClause : Name → Name → (Name × Type) × (Name × Type) → TC Clause
+  conversionClause prjP prjE ((fromC , fromTy) , (toC , toTy)) = do
+    let isVis   = λ { (abs _ (arg (arg-info visible _) _)) → true; _ → false }
+        fromTel = L.filterᵇ isVis (proj₁ (viewTy fromTy))
+        toTel   = L.filterᵇ isVis (proj₁ (viewTy toTy))
+        n       = length fromTel
+        mkCon  c mkArg = Term.con c    $ L.map (vArg ∘ mkArg ∘ ♯)  (downFrom n)
+        mkConP c mkArg = Pattern.con c $ L.map (vArg ∘ mkArg ∘ `_) (downFrom n)
+    true ← return (n == length toTel)
+      where false → liftTC $ R.typeErrorFmt "%q and %q have different number of arguments" fromC toC
+    return $ clause (tyViewToTel $ L.map (λ where (abs x (arg i _)) → abs x (arg i unknown)) fromTel)
+                    (vArg (proj prjP) ∷ vArg (mkConP fromC id) ∷ [])
+                    (mkCon toC (prjE ∙⟦_⟧))
+
+  -- Compute the clauses of a convertible instance.
+  instanceClauses : (agdaName hsName : Name) → TC (List Clause)
+  instanceClauses agdaName hsName = do
+    agdaCons ← getConstrs agdaName
+    hsCons   ← getConstrs hsName
+    agdaPars ← length <$> getParamsAndIndices agdaName
+    hsPars   ← length <$> getParamsAndIndices hsName
+    true ← return (length agdaCons == length hsCons)
+      where false → liftTC $ R.typeErrorFmt "%q and %q have different number of constructors" agdaName hsName
+    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 $ 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
+    quote Convertible ∙⟦ `A ∣ `B ⟧ ← reduce =<< goalTy
+      where t → liftTC $ R.typeErrorFmt "Expected Convertible A B, got %t" t
+    agdaCons ← getConstrsForType `A
+    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)
+    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)
+deriveConvertible : Name → Name → Name → R.TC ⊤
+deriveConvertible instName agdaName hsName = initUnquoteWithGoal ⦃ defaultTCOptions ⦄ (agda-sort (lit 0)) do
+  agdaDef ← getDefinition agdaName
+  hsDef   ← getDefinition hsName
+  -- instName ← freshName $ "Convertible" S.++ show hsName
+  instTel , instTy ← instanceType agdaName hsName
+  inst    ← declareDef (iArg instName) (tyView (instTel , instTy))
+  clauses ← instanceClauses agdaName hsName
+  defineFun instName clauses
+  return _
+
+-- Macros providing an alternative interface. Usage
+--   iName : ConvertibleType AgdaTy HsTy
+--   iName = autoConvertible
+-- or
+--   iName = autoConvert AgdaTy
+macro
+  ConvertibleType : Name → Name → Tactic
+  ConvertibleType agdaName hsName = initTac ⦃ defaultTCOptions ⦄ $
+    unifyWithGoal ∘ tyView =<< instanceType agdaName hsName
+
+  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

docs/agda-spec/src/Foreign/Convertible/DerivingTest.agda

@@ -0,0 +1,86 @@
+
+module Foreign.Convertible.DerivingTest where
+
+open import Level
+open import MetaPrelude
+open import Meta
+
+import Data.List as L
+import Data.List.NonEmpty as NE
+import Data.String as S
+import Data.Product as P
+
+open import Relation.Nullary
+open import Relation.Nullary.Decidable
+
+open import Reflection.Tactic
+open import Reflection.AST.Term
+open import Reflection.AST.DeBruijn
+import Reflection.TCM as R
+open import Reflection.Utils
+open import Reflection.Utils.TCI
+import Function.Identity.Effectful as Identity
+
+open import Class.DecEq
+open import Class.DecEq
+open import Class.Functor
+open import Class.Monad
+open import Class.MonadTC.Instances
+open import Class.Traversable
+open import Class.Show
+open import Class.MonadReader
+
+open import Foreign.Convertible
+open import Foreign.Convertible.Deriving
+
+-- Tests
+
+open import Data.Maybe.Base
+open import Data.Sum.Base
+
+data HsMaybe (a : Set) : Set where
+  just    : (x : a) → HsMaybe a
+  nothing : HsMaybe a
+
+data HsEither (a b : Set) : Set where
+  left : a → HsEither a b
+  right : b → HsEither a b
+
+-- We should be able to generate this
+ConvertibleMaybe : ∀ {a a'} → ⦃ Convertible a a' ⦄ → Convertible (Maybe a) (HsMaybe a')
+ConvertibleMaybe .to (just x)   = just (to x)
+ConvertibleMaybe .to nothing    = nothing
+ConvertibleMaybe .from (just x) = just (from x)
+ConvertibleMaybe .from nothing  = nothing
+
+-- With deriveConvertible
+unquoteDecl iConvertMaybe  = deriveConvertible iConvertMaybe (quote Maybe) (quote HsMaybe)
+
+-- or with ConvertibleType and autoConvertible
+instance
+  iConvertEither : ConvertibleType _⊎_ HsEither
+  iConvertEither = autoConvertible
+
+instance
+  ConvertibleNat = Convertible-Refl {ℕ}
+
+test : ℕ ⊎ Maybe ℕ → HsEither ℕ (HsMaybe ℕ)
+test = to
+
+_ : test (inj₂ (just 5)) ≡ right (just 5)
+_ = refl
+
+-- There was a problem due to Agda#7182 with record types in parameterised modules.
+
+module Param (A : Set) where
+  record AgdaThing : Set where
+    field theThing : A
+
+record HsThing : Set where
+  field theThing : ℕ
+
+open Param ℕ
+unquoteDecl iConvertThing = deriveConvertible iConvertThing (quote AgdaThing) (quote HsThing)
+
+convThing : Convertible AgdaThing HsThing
+convThing = autoConvertible

docs/agda-spec/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)