start on tying everything together

src/Foreign/Convertible/Deriving.agda

@@ -126,6 +126,9 @@ private
     fromClauses ← mapM (conversionClause (quote Convertible.from) (quote from)) (L.zip hsCons agdaCons)
     return $ pat-lam (toClauses ++ fromClauses) []
 
+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 ⊤

src/Foreign/HaskellTypes.agda

@@ -0,0 +1,29 @@
+
+module Foreign.HaskellTypes where
+
+open import Level using (Level)
+open import Data.Nat.Base using (ℕ)
+open import Data.List.Base using (List)
+
+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
+
+instance
+  -- Could make a macro for these kind of congruence instances.
+
+  iHasHsTypeℕ : HasHsType ℕ
+  iHasHsTypeℕ .HasHsType.HsType = ℕ
+
+  iHasHsTypeList : ⦃ HasHsType A ⦄ → HasHsType (List A)
+  iHasHsTypeList {A = A} .HasHsType.HsType = List (HsType A)
+
+  iHasHsTypeFun : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A → B)
+  iHasHsTypeFun {A = A} {B = B} .HasHsType.HsType = HsType A → HsType B

src/Foreign/Convertible/HaskellTypes.agda → src/Foreign/HaskellTypes/Deriving.agda

@@ -1,6 +1,6 @@
 -- {-# OPTIONS -v tc.unquote.def:10 -v tc.unquote.decl:10 -v tactic.hs-types:10 #-}
 
-module Foreign.Convertible.HaskellTypes where
+module Foreign.HaskellTypes.Deriving where
 
 open import Meta hiding (TC)
 
@@ -32,6 +32,7 @@ open import Class.Show.Instances
 open import Tactic.Derive.Show using (showName)
 
 open import Reflection.Utils
+open import Foreign.HaskellTypes
 
 {-
 
@@ -45,29 +46,24 @@ private variable
   l : Level
   A B : Set l
 
-record HasHsType (A : Set l) : Set₁ where
-  field
-    theHsType : Set
-
-open HasHsType
-
-HsType : (A : Set l) → ⦃ HasHsType A ⦄ → Set
-HsType _ ⦃ i ⦄ = i .HasHsType.theHsType
-
-instance
-  -- Could make a macro for these kind of congruence instances.
-
-  iHasHsTypeℕ : HasHsType ℕ
-  iHasHsTypeℕ .theHsType = ℕ
-
-  iHasHsTypeList : ⦃ HasHsType A ⦄ → HasHsType (List A)
-  iHasHsTypeList {A = A} .theHsType = List (HsType A)
-
-  iHasHsTypeFun : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A → B)
-  iHasHsTypeFun {A = A} {B = B} .theHsType = HsType A → HsType B
-
 NameEnv = List (Name × String)
 
+solveInstance : Term → TC Term
+solveInstance ty = do
+  iTerm@(meta iMeta _) ← newMeta ty
+    where _ → typeErrorFmt "Impossible"
+  debugPrintFmt "tactic.hs-types" 10 "getInstances %t : %t" iTerm =<< inferType iTerm
+  iSol ∷ _ ← getInstances iMeta
+    where [] → typeErrorFmt "No instance found for %t" ty
+  debugPrintFmt "tactic.hs-types" 10 "iSol = %t" iSol
+  unify iTerm iSol
+  pure iSol
+
+solveHsType : Term → TC Term
+solveHsType tm = do
+  inst ← solveInstance (quote HasHsType ∙⟦ tm ⟧)
+  normalise $ def (quote HsType) (vArg tm ∷ iArg inst ∷ [])
+
 private
   lookup : ⦃ DecEq A ⦄ → A → List (A × B) → Maybe B
   lookup x xs = proj₂ <$> findᵇ ((x ==_) ∘ proj₁) xs
@@ -97,15 +93,6 @@ private
   isThis f (def g []) = f == g
   isThis _ _ = false
 
-  computeHsTypeInst : Term → TC Term
-  computeHsTypeInst tm = do
-    iTerm@(meta iMeta _) ← checkType unknown (quote HasHsType ∙⟦ tm ⟧)
-      where _ → typeErrorFmt "Impossible"
-    iSol ∷ _ ← getInstances iMeta
-      where [] → typeErrorFmt "No instance found for %t" (quote HasHsType ∙⟦ tm ⟧)
-    unify iTerm iSol
-    normalise $ def (quote HsType) (vArg tm ∷ iArg iSol ∷ [])
-
   computeHsType : Name → Name → Term → TC Term
   computeHsType aThis hThis tm with isThis aThis tm
   ... | true = pure (hThis ∙)
@@ -118,20 +105,26 @@ private
     just ty′ ← pure (strengthen ty)
       where nothing → extendContext x a $ typeErrorFmt "%s free in computed HsType %t" x ty
     pure ty′
-  computeHsType _ _ tm | false = computeHsTypeInst tm
+  computeHsType _ _ tm | false = do
+    debugPrintFmt "tactic.hs-types" 10 "solving HsType %t" tm
+    ty ← solveHsType tm
+    debugPrintFmt "tactic.hs-types" 10 "HsType %t = %t" tm ty
+    pure ty
 
   makeHsCon : NameEnv → Name → Name → Name → TC (Name × Type)
   makeHsCon env agdaName hsName c = do
+    debugPrintFmt "tactic.hs-types" 10 "Making constructor %q : %q" c agdaName
     hsC  ← freshHsConName env c
     cTy  ← getType c
+    debugPrintFmt "tactic.hs-types" 10 "cTy = %t" cTy
     hsTy ← computeHsType agdaName hsName cTy
+    debugPrintFmt "tactic.hs-types" 10 "hsTy = %t" hsTy
     pure (hsC , hsTy)
 
   makeHsData : NameEnv → Name → ℕ → List Name → TC Name
   makeHsData env agdaName nPars constrs = do
     hsName ← freshHsTypeName env agdaName
-    let hsPars = 0  -- TODO
-    declareData hsName hsPars `Set
+    declareData hsName 0 `Set
     hsCons ← mapM (makeHsCon env agdaName hsName) constrs
     defineData hsName hsCons
     pure hsName
@@ -179,20 +172,22 @@ private
     (record-type c fs)  → typeErrorFmt "todo record"
     _                   → typeErrorFmt "%q is not a data or record type" d
 
-  doAutoHsType : NameEnv → Term → TC ⊤
-  doAutoHsType env hole = do
-    def (quote HasHsType) (_ ∷ vArg (d ∙) ∷ _) ← inferType hole
-      where t → typeErrorFmt "Expected HasHsType D, got %t" t
-    hs ← makeHsType env d
-    bindHsType hs
-    unify hole (`λ⟦ proj (quote theHsType) ⇒ hs ∙ ⟧)
+doAutoHsType : NameEnv → Name → Term → TC Term
+doAutoHsType env d hole = do
+  -- def (quote HasHsType) (_ ∷ vArg (d ∙) ∷ _) ← inferType hole
+  --   where t → typeErrorFmt "Expected HasHsType D, got %t" t
+  checkType hole (quote HasHsType ∙⟦ d ∙ ⟧)
+  hs ← makeHsType env d
+  bindHsType hs
+  unify hole (`λ⟦ proj (quote HasHsType.HsType) ⇒ hs ∙ ⟧)
+  pure (hs ∙)
 
 macro
-  autoHsType : Term → TC ⊤
-  autoHsType = doAutoHsType []
+  autoHsType : Name → Term → TC ⊤
+  autoHsType d hole = _ <$ doAutoHsType [] d hole
 
-  autoHsType' : NameEnv → Term → TC ⊤
-  autoHsType' = doAutoHsType
+  autoHsType' : Name → NameEnv → Term → TC ⊤
+  autoHsType' d env hole = _ <$ doAutoHsType env d hole
 
   _↦_ : Name → String → Term → TC ⊤
   x ↦ s = unify (quote (Data.Product._,_) ◆⟦ lit (name x) ∣ lit (string s) ⟧)

src/Foreign/Marshall.agda

@@ -0,0 +1,50 @@
+{-# OPTIONS -v tc.unquote.def:10 -v tc.unquote.decl:10 -v tactic.hs-types:10 #-}
+
+module Foreign.Marshall where
+
+open import Level using (Level; 0ℓ)
+open import Data.Nat.Base using (ℕ)
+open import Data.Unit using (⊤)
+open import Data.List using (List; []; _∷_)
+open import Function.Base
+
+open import Reflection hiding (_>>=_; _>>_)
+open import Reflection.Syntax
+
+open import Class.Monad
+
+open import Foreign.Convertible
+open import Foreign.HaskellTypes
+import Foreign.Convertible.Deriving
+import Foreign.HaskellTypes.Deriving
+
+open Foreign.Convertible.Deriving
+open Foreign.HaskellTypes.Deriving
+open Foreign.Convertible.Deriving public using (autoConvertible; ConvertibleType)
+open Foreign.HaskellTypes.Deriving public using (autoHsType; autoHsType')
+
+private
+  `Set = agda-sort (Sort.set (quote 0ℓ ∙))
+  doAutoMarshalling : Name → Term → TC ⊤
+  doAutoMarshalling d hole = do
+    hsTyMeta ← newMeta `Set
+    checkType hole (quote Convertible ∙⟦ d ∙ ∣ hsTyMeta ⟧)
+    hsTy ← solveHsType (d ∙)
+    unify hsTyMeta hsTy
+    patlam ← doPatternLambda hole
+    unify hole patlam
+
+macro
+  autoMarshall : Name → Term → TC ⊤
+  autoMarshall = doAutoMarshalling
+
+data Dummy : Set where
+  baseCase : Dummy
+  stepCase : ℕ → Dummy
+
+instance
+  iConvertible-ℕ = Convertible-Refl
+
+instance
+  iHsType-Dummy      = autoHsType Dummy
+  iMarshalling-Dummy = autoMarshall Dummy

src/Ledger/Foreign/LedgerTypes.agda

@@ -12,7 +12,8 @@ open import Foreign.Haskell.Coerce
 open import Foreign.Haskell.Either
 open import Data.Rational.Base
 
-open import Foreign.Convertible.HaskellTypes
+open import Foreign.HaskellTypes
+open import Foreign.HaskellTypes.Deriving
 open import Ledger.Transaction using (Tag)
 
 {-# FOREIGN GHC
@@ -84,8 +85,7 @@ HashProtected : Set → Set
 HashProtected A = Pair A GovActionID
 
 instance
-  iHsType-Tag : HasHsType Tag
-  iHsType-Tag = autoHsType
+  iHsType-Tag = autoHsType Tag
 
 RdmrPtr = Pair (HsType Tag) Ix
 ExUnits = Pair ℕ ℕ