Skip to content

Commit b254beb

Browse files
WhatisRTWhatisRT
committed
Upstream Convertible, HasHsType and their Deriving strategies
Credit for the `Deriving` strategies goes to @UlfNorell
1 parent 318cc55 commit b254beb

File tree

6 files changed

+729
-0
lines changed

6 files changed

+729
-0
lines changed

‎Class/Convertible.agda‎

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
module Class.Convertible where
2+
3+
open import Function
4+
open import Class.HasHsType
5+
open import Class.Core
6+
open import Class.Functor
7+
open import Class.Bifunctor
8+
open import Data.Maybe
9+
open import Data.Product
10+
open import Data.Sum
11+
open import Data.List
12+
13+
record Convertible (A B : Set) : Set where
14+
field to : A → B
15+
from : B → A
16+
open Convertible ⦃...⦄ public
17+
18+
HsConvertible : (A : Set) → ⦃ HasHsType A ⦄ → Set
19+
HsConvertible A = Convertible A (HsType A)
20+
21+
Convertible-Refl : ∀ {A} → Convertible A A
22+
Convertible-Refl = λ where .to → id; .from → id
23+
24+
Convertible₁ : (Set → Set) → (Set → Set) → Set₁
25+
Convertible₁ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible (T A) (U B)
26+
27+
Convertible₂ : (Set → Set → Set) → (Set → Set → Set) → Set₁
28+
Convertible₂ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible₁ (T A) (U B)
29+
30+
Functor⇒Convertible : ∀ {F : Type↑} → ⦃ Functor F ⦄ → Convertible₁ F F
31+
Functor⇒Convertible = λ where
32+
.to → fmap to
33+
.from → fmap from
34+
35+
Bifunctor⇒Convertible : ∀ {F} → ⦃ Bifunctor F ⦄ → Convertible₂ F F
36+
Bifunctor⇒Convertible = λ where
37+
.to → bimap to to
38+
.from → bimap from from
39+
40+
_⨾_ : ∀ {A B C} → Convertible A B → Convertible B C → Convertible A C
41+
(c ⨾ c') .to = c' .to ∘ c .to
42+
(c ⨾ c') .from = c .from ∘ c' .from
43+
44+
-- ** instances
45+
46+
open import Foreign.Haskell
47+
open import Foreign.Haskell.Coerce using (coerce)
48+
49+
open import Data.Nat
50+
51+
instance
52+
Convertible-ℕ : Convertible ℕ ℕ
53+
Convertible-ℕ = λ where
54+
.to → id
55+
.from → id
56+
57+
Convertible-Maybe : Convertible₁ Maybe Maybe
58+
Convertible-Maybe = Functor⇒Convertible
59+
60+
Convertible-× : Convertible₂ _×_ _×_
61+
Convertible-× = Bifunctor⇒Convertible
62+
63+
Convertible-Pair : Convertible₂ _×_ Pair
64+
Convertible-Pair = λ where
65+
.to → coerce ∘ bimap to to
66+
.from → bimap from from ∘ coerce
67+
68+
Convertible-⊎ : Convertible₂ _⊎_ _⊎_
69+
Convertible-⊎ = Bifunctor⇒Convertible
70+
71+
Convertible-Either : Convertible₂ _⊎_ Either
72+
Convertible-Either = λ where
73+
.to → coerce ∘ bimap to to
74+
.from → bimap from from ∘ coerce
75+
76+
Convertible-List : Convertible₁ List List
77+
Convertible-List = λ where
78+
.to → fmap to
79+
.from → fmap from
80+
81+
Convertible-Fun : ∀ {A A' B B'} → ⦃ Convertible A A' ⦄ → ⦃ Convertible B B' ⦄ → Convertible (A → B) (A' → B')
82+
Convertible-Fun = λ where
83+
.to → λ f → to ∘ f ∘ from
84+
.from → λ f → from ∘ f ∘ to

‎Class/HasHsType.agda‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
module Class.HasHsType where
2+
3+
open import Level using (Level)
4+
open import Data.Bool.Base using (Bool)
5+
open import Data.Nat.Base using (ℕ)
6+
open import Data.String.Base using (String)
7+
open import Data.List.Base using (List)
8+
open import Data.Maybe.Base using (Maybe)
9+
open import Data.Sum.Base using (_⊎_)
10+
open import Data.Product.Base using (_×_)
11+
open import Data.Unit using (⊤)
12+
13+
open import Foreign.Haskell.Pair using (Pair)
14+
open import Foreign.Haskell.Either using (Either)
15+
16+
private variable
17+
l : Level
18+
A B : Set l
19+
20+
record HasHsType (A : Set l) : Set₁ where
21+
field
22+
HsType : Set
23+
24+
HsType : (A : Set l) → ⦃ HasHsType A ⦄ → Set
25+
HsType _ ⦃ i ⦄ = i .HasHsType.HsType
26+
27+
MkHsType : (A : Set l) (Hs : Set) → HasHsType A
28+
MkHsType A Hs .HasHsType.HsType = Hs
29+
30+
instance
31+
32+
iHsTy-ℕ = MkHsType ℕ ℕ
33+
iHsTy-Bool = MkHsType Bool Bool
34+
iHsTy-⊤ = MkHsType ⊤ ⊤
35+
iHsTy-String = MkHsType String String
36+
37+
-- Could make a macro for these kind of congruence instances.
38+
iHsTy-List : ⦃ HasHsType A ⦄ → HasHsType (List A)
39+
iHsTy-List {A = A} .HasHsType.HsType = List (HsType A)
40+
41+
iHsTy-Maybe : ⦃ HasHsType A ⦄ → HasHsType (Maybe A)
42+
iHsTy-Maybe {A = A} .HasHsType.HsType = Maybe (HsType A)
43+
44+
iHsTy-Fun : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A → B)
45+
iHsTy-Fun {A = A} {B = B} .HasHsType.HsType = HsType A → HsType B
46+
47+
iHsTy-Sum : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A ⊎ B)
48+
iHsTy-Sum {A = A} {B = B} .HasHsType.HsType = Either (HsType A) (HsType B)
49+
50+
iHsTy-Pair : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A × B)
51+
iHsTy-Pair {A = A} {B = B} .HasHsType.HsType = Pair (HsType A) (HsType B)

‎Reflection/Utils/Substitute.agda‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
module Reflection.Utils.Substitute where
2+
3+
open import MetaPrelude
4+
open import Meta
5+
6+
-- There aren't any nice substitution functions (that I can find) in the standard library or
7+
-- stdlib-meta. This one is cheating and only works for closed terms at either never gets
8+
-- applied, or where we can safely throw away the arguments (e.g. `unknown`).
9+
10+
Subst : Set → Set
11+
Subst A = ℕ → Term → A → A
12+
13+
substTerm : Subst Term
14+
substArgs : Subst (Args Term)
15+
substArg : Subst (Arg Term)
16+
substAbs : Subst (Abs Term)
17+
substSort : Subst Sort
18+
19+
substTerm x s (var y args) =
20+
case compare x y of λ where
21+
(less _ _) → var (y ∸ 1) (substArgs x s args)
22+
(equal _) → s -- cheating and dropping the args!
23+
(greater _ _) → var y (substArgs x s args)
24+
substTerm x s (con c args) = con c (substArgs x s args)
25+
substTerm x s (def f args) = def f (substArgs x s args)
26+
substTerm x s (lam v t) = lam v (substAbs x s t)
27+
substTerm x s (pat-lam cs args₁) = unknown -- ignoring for now
28+
substTerm x s (pi a b) = pi (substArg x s a) (substAbs x s b)
29+
substTerm x s (agda-sort s₁) = agda-sort (substSort x s s₁)
30+
substTerm x s (lit l) = lit l
31+
substTerm x s (meta m args) = meta m (substArgs x s args)
32+
substTerm x s unknown = unknown
33+
34+
substArgs x s [] = []
35+
substArgs x s (a ∷ as) = substArg x s a ∷ substArgs x s as
36+
37+
substArg x s (arg i t) = arg i (substTerm x s t)
38+
39+
substAbs x s (abs z t) = abs z (substTerm (ℕ.suc x) s t)
40+
41+
substSort x s (set t) = set (substTerm x s t)
42+
substSort x s (lit n) = lit n
43+
substSort x s (prop t) = prop (substTerm x s t)
44+
substSort x s (propLit n) = propLit n
45+
substSort x s (inf n) = inf n
46+
substSort x s unknown = unknown

‎Tactic.agda‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,3 +17,5 @@ open import Tactic.ReduceDec public
1717

1818
open import Tactic.Derive.DecEq public
1919
open import Tactic.Derive.Show public
20+
open import Tactic.Derive.Convertible
21+
open import Tactic.Derive.HsType

‎Tactic/Derive/Convertible.agda‎

Lines changed: 185 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,185 @@
1+
module Tactic.Derive.Convertible where
2+
3+
open import Level
4+
open import MetaPrelude
5+
open import Meta
6+
7+
import Data.List as L
8+
import Data.List.NonEmpty as NE
9+
import Data.String as S
10+
import Data.Product as P
11+
12+
open import Relation.Nullary
13+
open import Relation.Nullary.Decidable
14+
15+
open import Reflection.Tactic
16+
open import Reflection.AST.Term
17+
open import Reflection.AST.DeBruijn
18+
import Reflection.TCM as R
19+
open import Reflection.Utils
20+
open import Reflection.Utils.TCI
21+
import Function.Identity.Effectful as Identity
22+
23+
open import Class.DecEq
24+
open import Class.DecEq
25+
open import Class.Functor
26+
open import Class.Monad
27+
open import Class.MonadTC.Instances
28+
open import Class.Traversable
29+
open import Class.Show
30+
open import Class.MonadReader
31+
32+
open import Reflection.Utils.Substitute
33+
open import Class.Convertible
34+
open import Class.HasHsType
35+
open import Tactic.Derive.HsType
36+
37+
private instance
38+
_ = Functor-M {TC}
39+
40+
-- TODO: move to agda-stdlib-meta
41+
liftTC : ∀ {a} {A : Set a} → R.TC A → TC A
42+
liftTC m _ = m
43+
44+
private
45+
46+
open MonadReader ⦃...⦄
47+
48+
variable
49+
A B C : Set
50+
51+
TyViewTel = List (Abs (Arg Type))
52+
53+
substTel : Subst TyViewTel
54+
substTel x s [] = []
55+
substTel x s (abs z t ∷ tel) = abs z (substArg x s t) ∷ (substTel (ℕ.suc x) s tel)
56+
-- Note: `abs` is abused in TyViewTel and doesn't actually scope over the `t`
57+
58+
-- Substitute leading level parameters with lzero
59+
smashLevels : TyViewTel → ℕ × TyViewTel
60+
smashLevels (abs s (arg i (def (quote Level) [])) ∷ tel) =
61+
P.map ℕ.suc (substTel 0 (quote 0ℓ ∙)) $ smashLevels tel
62+
smashLevels tel = (0 , tel)
63+
64+
tyViewToTel : TyViewTel → Telescope
65+
tyViewToTel = L.map λ where (abs s a) → s , a
66+
67+
hideTyView : Abs (Arg A) → Abs (Arg A)
68+
hideTyView (abs s (arg (arg-info _ m) x)) = abs s (arg (arg-info hidden m) x)
69+
70+
-- The type of a Convertible instance. For parameterised types adds the appropriate instance
71+
-- arguments and instantiates level arguments to lzero. For instance,
72+
-- instanceType _⊎_ Hs.Either = {A B : Set} {a b : Set} → ⦃ Convertible A a ⦄ → ⦃ Convertible B b ⦄
73+
-- Convertible (A ⊎ B) (Hs.Either a b)
74+
instanceType : (agdaName hsName : Name) → TC TypeView
75+
instanceType agdaName hsName = do
76+
aLvls , agdaParams ← smashLevels <$> getParamsAndIndices agdaName
77+
hLvls , hsParams ← smashLevels <$> getParamsAndIndices hsName
78+
true ← return (length agdaParams == length hsParams)
79+
where false → liftTC $ R.typeErrorFmt "%q and %q have different number of parameters" agdaName hsName
80+
let n = length agdaParams
81+
l₀ = quote 0ℓ ∙
82+
agdaTy ← applyWithVisibility agdaName $ L.replicate aLvls l₀ ++ L.map ♯ (take n (downFrom (n + n)))
83+
hsTy ← applyWithVisibility hsName $ L.replicate hLvls l₀ ++ L.map ♯ (downFrom n)
84+
let instHead = weaken n $ quote Convertible ∙⟦ agdaTy ∣ hsTy ⟧
85+
tel = L.map hideTyView (agdaParams ++ hsParams) ++
86+
L.replicate n (abs "_" (iArg (quote Convertible ∙⟦ ♯ (n + n ∸ 1) ∣ ♯ (n ∸ 1) ⟧)))
87+
return $ tel , instHead
88+
89+
-- Compute one clause of the Convertible instance. For instance,
90+
-- conversionClause Convertible.to to ((c₁ , _) , (c₂ , _)) generates
91+
-- .to (c₁ x₁ .. xn) = c₂ (to x₁) .. (to xn)
92+
-- where the xi are the visible constructor arguments.
93+
conversionClause : Name → Name → (Name × Type) × (Name × Type) → TC Clause
94+
conversionClause prjP prjE ((fromC , fromTy) , (toC , toTy)) = do
95+
let isVis = λ { (abs _ (arg (arg-info visible _) _)) → true; _ → false }
96+
fromTel = L.filterᵇ isVis (proj₁ (viewTy fromTy))
97+
toTel = L.filterᵇ isVis (proj₁ (viewTy toTy))
98+
n = length fromTel
99+
mkCon c mkArg = Term.con c $ L.map (vArg ∘ mkArg ∘ ♯) (downFrom n)
100+
mkConP c mkArg = Pattern.con c $ L.map (vArg ∘ mkArg ∘ `_) (downFrom n)
101+
true ← return (n == length toTel)
102+
where false → liftTC $ R.typeErrorFmt "%q and %q have different number of arguments" fromC toC
103+
return $ clause (tyViewToTel $ L.map (λ where (abs x (arg i _)) → abs x (arg i unknown)) fromTel)
104+
(vArg (proj prjP) ∷ vArg (mkConP fromC id) ∷ [])
105+
(mkCon toC (prjE ∙⟦_⟧))
106+
107+
-- Compute the clauses of a convertible instance.
108+
instanceClauses : (agdaName hsName : Name) → TC (List Clause)
109+
instanceClauses agdaName hsName = do
110+
agdaCons ← getConstrs agdaName
111+
hsCons ← getConstrs hsName
112+
agdaPars ← length <$> getParamsAndIndices agdaName
113+
hsPars ← length <$> getParamsAndIndices hsName
114+
true ← return (length agdaCons == length hsCons)
115+
where false → liftTC $ R.typeErrorFmt "%q and %q have different number of constructors" agdaName hsName
116+
toClauses ← mapM (conversionClause (quote Convertible.to) (quote to) ) (L.zip agdaCons hsCons)
117+
fromClauses ← mapM (conversionClause (quote Convertible.from) (quote from)) (L.zip hsCons agdaCons)
118+
return $ toClauses ++ fromClauses
119+
120+
absurdClause : Name → Clause
121+
absurdClause prj = absurd-clause (("x" , vArg unknown) ∷ []) (vArg (proj prj) ∷ vArg (absurd 0) ∷ [])
122+
123+
-- Compute conversion clauses for the current goal and wrap them in a pattern lambda.
124+
patternLambda : TC Term
125+
patternLambda = do
126+
quote Convertible ∙⟦ `A ∣ `B ⟧ ← reduce =<< goalTy
127+
where t → liftTC $ R.typeErrorFmt "Expected Convertible A B, got %t" t
128+
agdaCons ← getConstrsForType `A
129+
hsCons ← getConstrsForType `B
130+
toClauses ← mapM (conversionClause (quote Convertible.to) (quote to) ) (L.zip agdaCons hsCons)
131+
fromClauses ← mapM (conversionClause (quote Convertible.from) (quote from)) (L.zip hsCons agdaCons)
132+
case toClauses ++ fromClauses of λ where
133+
[] → return $ pat-lam (absurdClause (quote Convertible.to) ∷ absurdClause (quote Convertible.from) ∷ []) []
134+
cls → return $ pat-lam cls []
135+
136+
doPatternLambda : Term → R.TC Term
137+
doPatternLambda hole = patternLambda =<< initTCEnvWithGoal hole
138+
139+
-- Deriving a Convertible instance. Usage
140+
-- unquoteDecl iName = deriveConvertible iName (quote AgdaTy) (quote HsTy)
141+
deriveConvertible : Name → Name → Name → R.TC ⊤
142+
deriveConvertible instName agdaName hsName = initUnquoteWithGoal ⦃ defaultTCOptions ⦄ (agda-sort (lit 0)) do
143+
agdaDef ← getDefinition agdaName
144+
hsDef ← getDefinition hsName
145+
-- instName ← freshName $ "Convertible" S.++ show hsName
146+
instTel , instTy ← instanceType agdaName hsName
147+
inst ← declareDef (iArg instName) (tyView (instTel , instTy))
148+
clauses ← instanceClauses agdaName hsName
149+
defineFun instName clauses
150+
return _
151+
152+
-- Macros providing an alternative interface. Usage
153+
-- iName : ConvertibleType AgdaTy HsTy
154+
-- iName = autoConvertible
155+
-- or
156+
-- iName = autoConvert AgdaTy
157+
macro
158+
ConvertibleType : Name → Name → Tactic
159+
ConvertibleType agdaName hsName = initTac ⦃ defaultTCOptions ⦄ $
160+
unifyWithGoal ∘ tyView =<< instanceType agdaName hsName
161+
162+
autoConvertible : Tactic
163+
autoConvertible = initTac ⦃ defaultTCOptions ⦄ $
164+
unifyWithGoal =<< patternLambda
165+
166+
autoConvert : Name → Tactic
167+
autoConvert d hole = do
168+
hsTyMeta ← R.newMeta `Set
169+
R.checkType hole $ quote Convertible ∙⟦ d ∙ ∣ hsTyMeta ⟧
170+
hsTy ← solveHsType (d ∙)
171+
R.unify hsTyMeta hsTy
172+
R.unify hole =<< doPatternLambda hole
173+
174+
-- Tests
175+
176+
private
177+
178+
record Test : Set where
179+
field f : ℕ
180+
g : Maybe ℕ
181+
h : List ℕ
182+
183+
instance
184+
HsTy-Test = autoHsType Test ⊣ withConstructor "MkTest" • fieldPrefix "t"
185+
Conv-Test = autoConvert Test

0 commit comments

Comments
 (0)