Skip to content

Commit ed44595

Browse files
brendanzabbrendanzab
committed
Use the Subset type from the Idris base library
1 parent b5b4439 commit ed44595

File tree

6 files changed

+27
-44
lines changed

6 files changed

+27
-44
lines changed

‎experiments/idris/fathom.ipkg‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,6 @@ modules = Fathom
1818
, Fathom.Data.Bit
1919
, Fathom.Data.Iso
2020
, Fathom.Data.Sing
21-
, Fathom.Data.Refine
2221
, Fathom.Data.Word
2322
, Fathom.Closed.IndexedInductive
2423
, Fathom.Closed.IndexedInductiveCustom

‎experiments/idris/src/Fathom/Closed/IndexedInductive.idr‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -145,22 +145,22 @@ toFormatOfIso = MkIso
145145
||| Convert a format description into an indexed format description with an
146146
||| equality proof that the representation is the same as the index.
147147
public export
148-
toFormatOfEq : {0 A : Type} -> (f : Format ** f.Rep = A) -> FormatOf A
149-
toFormatOfEq (f ** prf) = rewrite sym prf in f.format
148+
toFormatOfEq : {0 A : Type} -> (Subset Format (\f => f.Rep = A)) -> FormatOf A
149+
toFormatOfEq (Element f prf) = rewrite sym prf in f.format
150150
151151
152152
||| Convert an indexed format description to a existential format description,
153153
||| along with a proof that the representation is the same as the index.
154154
public export
155-
toFormatEq : {0 A : Type} -> FormatOf A -> (f : Format ** f.Rep = A)
156-
toFormatEq f = (MkFormat A f ** Refl)
155+
toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => f.Rep = A))
156+
toFormatEq f = Element (MkFormat A f) Refl
157157
158158
159159
public export
160-
toFormatOfEqIso : Iso (Exists (\a => (f : Format ** f.Rep = a))) (Exists FormatOf)
160+
toFormatOfEqIso : Iso (Exists (\a => (Subset Format (\f => f.Rep = a)))) (Exists FormatOf)
161161
toFormatOfEqIso = MkIso
162-
{ to = \(Evidence _f) => Evidence _ (toFormatOfEq f)
162+
{ to = \(Evidence _ f) => Evidence _ (toFormatOfEq f)
163163
, from = \(Evidence _ f) => Evidence _ (toFormatEq f)
164164
, toFrom = \(Evidence _ _) => Refl
165-
, fromTo = \(Evidence _ ((MkFormat _ _) ** Refl)) => Refl
165+
, fromTo = \(Evidence _ (Element (MkFormat _ _) Refl)) => Refl
166166
}

‎experiments/idris/src/Fathom/Closed/IndexedInductiveCustom.idr‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -138,24 +138,24 @@ toFormatOfIso = MkIso
138138
||| Convert a format description into an indexed format description with an
139139
||| equality proof that the representation is the same as the index.
140140
public export
141-
toFormatOfEq : {0 A : Type} -> (f : Format ** f.Rep = A) -> FormatOf A
142-
toFormatOfEq (f ** prf) = rewrite sym prf in f.format
141+
toFormatOfEq : {0 A : Type} -> (Subset Format (\f => f.Rep = A)) -> FormatOf A
142+
toFormatOfEq (Element f prf) = rewrite sym prf in f.format
143143
144144
145145
||| Convert an indexed format description to a existential format description,
146146
||| along with a proof that the representation is the same as the index.
147147
public export
148-
toFormatEq : {0 A : Type} -> FormatOf A -> (f : Format ** f.Rep = A)
149-
toFormatEq f = (MkFormat A f ** Refl)
148+
toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => f.Rep = A))
149+
toFormatEq f = Element (MkFormat A f) Refl
150150
151151
152152
public export
153-
toFormatOfEqIso : Iso (Exists (\a => (f : Format ** f.Rep = a))) (Exists FormatOf)
153+
toFormatOfEqIso : Iso (Exists (\a => (Subset Format (\f => f.Rep = a)))) (Exists FormatOf)
154154
toFormatOfEqIso = MkIso
155-
{ to = \(Evidence _f) => Evidence _ (toFormatOfEq f)
155+
{ to = \(Evidence _ f) => Evidence _ (toFormatOfEq f)
156156
, from = \(Evidence _ f) => Evidence _ (toFormatEq f)
157157
, toFrom = \(Evidence _ _) => Refl
158-
, fromTo = \(Evidence _ ((MkFormat _ _) ** Refl)) => Refl
158+
, fromTo = \(Evidence _ (Element (MkFormat _ _) Refl)) => Refl
159159
}
160160
161161

‎experiments/idris/src/Fathom/Closed/InductiveRecursive.idr‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -150,22 +150,22 @@ toFormatOfIso = MkIso
150150
||| Convert a format description into an indexed format description with an
151151
||| equality proof that the representation is the same as the index.
152152
public export
153-
toFormatOfEq : {0 A : Type} -> (f : Format ** Rep f = A) -> FormatOf A
154-
toFormatOfEq (f ** prf) = rewrite sym prf in MkFormatOf f
153+
toFormatOfEq : {0 A : Type} -> (Subset Format (\f => Rep f = A)) -> FormatOf A
154+
toFormatOfEq (Element f prf) = rewrite sym prf in MkFormatOf f
155155
156156
157157
||| Convert an indexed format description to a existential format description,
158158
||| along with a proof that the representation is the same as the index.
159159
public export
160-
toFormatEq : {0 A : Type} -> FormatOf A -> (f : Format ** Rep f = A)
161-
toFormatEq (MkFormatOf f) = (f ** Refl)
160+
toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => Rep f = A))
161+
toFormatEq (MkFormatOf f) = Element f Refl
162162
163163
164164
public export
165-
toFormatOfEqIso : Iso (Exists (\a => (f : Format ** Rep f = a))) (Exists FormatOf)
165+
toFormatOfEqIso : Iso (Exists (\a => (Subset Format (\f => Rep f = a)))) (Exists FormatOf)
166166
toFormatOfEqIso = MkIso
167167
{ to = \(Evidence _ f) => Evidence _ (toFormatOfEq f)
168168
, from = \(Evidence _ f) => Evidence _ (toFormatEq f)
169169
, toFrom = \(Evidence _ (MkFormatOf _)) => Refl
170-
, fromTo = \(Evidence _ (f ** Refl)) => Refl
170+
, fromTo = \(Evidence _ (Element _ Refl)) => Refl
171171
}

‎experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr‎

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ import Data.Vect
1111

1212
import Fathom.Base
1313
import Fathom.Data.Iso
14-
import Fathom.Data.Refine
1514
import Fathom.Data.Sing
1615

1716

@@ -190,24 +189,24 @@ toFormatOfIso = MkIso
190189
||| Convert a format description into an indexed format description with an
191190
||| equality proof that the representation is the same as the index.
192191
public export
193-
toFormatOfEq : {0 A : Type} -> (f : Format ** Rep f = A) -> FormatOf A
194-
toFormatOfEq (f ** prf) = rewrite sym prf in MkFormatOf f
192+
toFormatOfEq : {0 A : Type} -> (Subset Format (\f => Rep f = A)) -> FormatOf A
193+
toFormatOfEq (Element f prf) = rewrite sym prf in MkFormatOf f
195194
196195
197196
||| Convert an indexed format description to a existential format description,
198197
||| along with a proof that the representation is the same as the index.
199198
public export
200-
toFormatEq : {0 A : Type} -> FormatOf A -> (f : Format ** Rep f = A)
201-
toFormatEq (MkFormatOf f) = (f ** Refl)
199+
toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => Rep f = A))
200+
toFormatEq (MkFormatOf f) = Element f Refl
202201
203202
204203
public export
205-
toFormatOfEqIso : Iso (Exists (\a => (f : Format ** Rep f = a))) (Exists FormatOf)
204+
toFormatOfEqIso : Iso (Exists (\a => (Subset Format (\f => Rep f = a)))) (Exists FormatOf)
206205
toFormatOfEqIso = MkIso
207-
{ to = \(Evidence _f) => Evidence _ (toFormatOfEq f)
206+
{ to = \(Evidence _ f) => Evidence _ (toFormatOfEq f)
208207
, from = \(Evidence _ f) => Evidence _ (toFormatEq f)
209208
, toFrom = \(Evidence _ (MkFormatOf _)) => Refl
210-
, fromTo = \(Evidence _ (_ ** Refl)) => Refl
209+
, fromTo = \(Evidence _ (Element _ Refl)) => Refl
211210
}
212211
213212

‎experiments/idris/src/Fathom/Data/Refine.idr‎

Lines changed: 0 additions & 15 deletions
This file was deleted.

0 commit comments

Comments
 (0)