Skip to content

Commit 6ea96ed

Browse files
brendanzabbrendanzab
committed
Define isomorphisms between Formats and FormatOfs
1 parent 7299eaa commit 6ea96ed

File tree

6 files changed

+207
-42
lines changed

6 files changed

+207
-42
lines changed

‎experiments/idris/fathom.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ package fathom
1616
modules = Fathom
1717
, Fathom.Base
1818
, Fathom.Data.Bit
19+
, Fathom.Data.Iso
1920
, Fathom.Data.Sing
2021
, Fathom.Data.Refine
2122
, Fathom.Data.Word

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

Lines changed: 50 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,11 @@ module Fathom.Closed.IndexedInductive
55

66

77
import Data.Colist
8+
import Data.DPair
89
import Data.Vect
910

1011
import Fathom.Base
12+
import Fathom.Data.Iso
1113
import Fathom.Data.Sing
1214

1315

@@ -18,7 +20,7 @@ import Fathom.Data.Sing
1820

1921
||| Universe of format descriptions indexed by their machine representations
2022
public export
21-
data FormatOf : (0 A : Type) -> Type where
23+
data FormatOf : Type -> Type where
2224
End : FormatOf Unit
2325
Fail : FormatOf Void
2426
Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
@@ -64,6 +66,29 @@ decode (Bind f1 f2) buffer = do
6466
(y, buffer'') <- decode (f2 x) buffer'
6567
Just ((x ** y), buffer'')
6668
69+
-- export
70+
-- decode : {0 A, S : Type} -> (f : FormatOf A) -> Decode (A, Colist S) (Colist S)
71+
-- decode End
72+
-- = \buffer => case buffer of
73+
-- [] => Just ((), [])
74+
-- _::_ => Nothing
75+
-- decode Fail
76+
-- = const Nothing
77+
-- decode (Pure x)
78+
-- = pure (MkSing x)
79+
-- decode (Skip f _)
80+
-- = do _ <- decode f
81+
-- pure ()
82+
-- decode (Repeat 0 f) = pure []
83+
-- decode (Repeat (S len) f)
84+
-- = do x <- decode f
85+
-- xs <- decode (Repeat len f)
86+
-- pure (x :: xs)
87+
-- decode (Bind f1 f2)
88+
-- = do x <- decode f1
89+
-- y <- decode (f2 x)
90+
-- pure (x ** y)
91+
6792
6893
export
6994
encode : {0 A, S : Type} -> (f : FormatOf A) -> Encode A (Colist S)
@@ -107,16 +132,40 @@ toFormat : {0 A : Type} -> FormatOf A -> Format
107132
toFormat f = MkFormat A f
108133
109134
135+
public export
136+
toFormatOfIso : Iso Format (Exists FormatOf)
137+
toFormatOfIso = MkIso
138+
{ to = \f => Evidence _ (toFormatOf f)
139+
, from = \(Evidence _ f) => toFormat f
140+
, toFrom = \(Evidence _ _) => Refl
141+
, fromTo = \(MkFormat _ _) => Refl
142+
}
143+
144+
145+
||| Convert a format description into an indexed format description with an
146+
||| equality proof that the representation is the same as the index.
110147
public export
111148
toFormatOfEq : {0 A : Type} -> (f : Format ** f.Rep = A) -> FormatOf A
112149
toFormatOfEq (f ** prf) = rewrite sym prf in f.format
113150
114151
152+
||| Convert an indexed format description to a existential format description,
153+
||| along with a proof that the representation is the same as the index.
115154
public export
116155
toFormatEq : {0 A : Type} -> FormatOf A -> (f : Format ** f.Rep = A)
117156
toFormatEq f = (MkFormat A f ** Refl)
118157
119158
159+
public export
160+
toFormatOfEqIso : Iso (Exists (\a => (f : Format ** f.Rep = a))) (Exists FormatOf)
161+
toFormatOfEqIso = MkIso
162+
{ to = \(Evidence _f) => Evidence _ (toFormatOfEq f)
163+
, from = \(Evidence _ f) => Evidence _ (toFormatEq f)
164+
, toFrom = \(Evidence _ _) => Refl
165+
, fromTo = \(Evidence _ ((MkFormat _ _) ** Refl)) => Refl
166+
}
167+
168+
120169
-----------------
121170
-- EXPERIMENTS --
122171
-----------------

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

Lines changed: 27 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,11 @@ module Fathom.Closed.IndexedInductiveCustom
55

66

77
import Data.Colist
8+
import Data.DPair
89
import Data.Vect
910

1011
import Fathom.Base
12+
import Fathom.Data.Iso
1113

1214

1315
---------------------------------
@@ -30,7 +32,7 @@ record CustomFormat where
3032

3133
||| Universe of format descriptions indexed by their machine representations
3234
public export
33-
data FormatOf : (0 A : Type) -> Type where
35+
data FormatOf : (A : Type) -> Type where
3436
End : FormatOf Unit
3537
Fail : FormatOf Void
3638
Pure : {0 A : Type} -> (x : A) -> FormatOf A
@@ -122,16 +124,40 @@ toFormat : {0 A : Type} -> FormatOf A -> Format
122124
toFormat f = MkFormat A f
123125
124126
127+
public export
128+
toFormatOfIso : Iso Format (Exists FormatOf)
129+
toFormatOfIso = MkIso
130+
{ to = \f => Evidence _ (toFormatOf f)
131+
, from = \(Evidence _ f) => toFormat f
132+
, toFrom = \(Evidence _ _) => Refl
133+
, fromTo = \(MkFormat _ _) => Refl
134+
}
135+
136+
137+
||| Convert a format description into an indexed format description with an
138+
||| equality proof that the representation is the same as the index.
125139
public export
126140
toFormatOfEq : {0 A : Type} -> (f : Format ** f.Rep = A) -> FormatOf A
127141
toFormatOfEq (f ** prf) = rewrite sym prf in f.format
128142
129143
144+
||| Convert an indexed format description to a existential format description,
145+
||| along with a proof that the representation is the same as the index.
130146
public export
131147
toFormatEq : {0 A : Type} -> FormatOf A -> (f : Format ** f.Rep = A)
132148
toFormatEq f = (MkFormat A f ** Refl)
133149
134150
151+
public export
152+
toFormatOfEqIso : Iso (Exists (\a => (f : Format ** f.Rep = a))) (Exists FormatOf)
153+
toFormatOfEqIso = MkIso
154+
{ to = \(Evidence _f) => Evidence _ (toFormatOfEq f)
155+
, from = \(Evidence _ f) => Evidence _ (toFormatEq f)
156+
, toFrom = \(Evidence _ _) => Refl
157+
, fromTo = \(Evidence _ ((MkFormat _ _) ** Refl)) => Refl
158+
}
159+
160+
135161
--------------------
136162
-- CUSTOM FORMATS --
137163
--------------------

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

Lines changed: 25 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,9 +23,11 @@ module Fathom.Closed.InductiveRecursive
2323

2424

2525
import Data.Colist
26+
import Data.DPair
2627
import Data.Vect
2728

2829
import Fathom.Base
30+
import Fathom.Data.Iso
2931
import Fathom.Data.Sing
3032

3133
-- import Fathom.Open.Record
@@ -134,7 +136,7 @@ encode (Bind f1 f2) (x ** y) = do
134136
135137
||| A format description refined with a fixed representation
136138
public export
137-
data FormatOf : (0 A : Type) -> Type where
139+
data FormatOf : (A : Type) -> Type where
138140
MkFormatOf : (f : Format) -> FormatOf (Rep f)
139141
140142
@@ -153,16 +155,38 @@ toFormat : {0 A : Type} -> FormatOf A -> Format
153155
toFormat (MkFormatOf f) = f
154156
155157
158+
public export
159+
toFormatOfIso : Iso Format (Exists FormatOf)
160+
toFormatOfIso = MkIso
161+
{ to = \f => Evidence _ (toFormatOf f)
162+
, from = \(Evidence _ f) => toFormat f
163+
, toFrom = \(Evidence _ (MkFormatOf _)) => Refl
164+
, fromTo = \_ => Refl
165+
}
166+
167+
168+
||| Convert a format description into an indexed format description with an
169+
||| equality proof that the representation is the same as the index.
156170
public export
157171
toFormatOfEq : {0 A : Type} -> (f : Format ** Rep f = A) -> FormatOf A
158172
toFormatOfEq (f ** prf) = rewrite sym prf in MkFormatOf f
159173
160174
175+
||| Convert an indexed format description to a existential format description,
176+
||| along with a proof that the representation is the same as the index.
161177
public export
162178
toFormatEq : {0 A : Type} -> FormatOf A -> (f : Format ** Rep f = A)
163179
toFormatEq (MkFormatOf f) = (f ** Refl)
164180
165181
182+
public export
183+
toFormatOfEqIso : Iso (Exists (\a => (f : Format ** Rep f = a))) (Exists FormatOf)
184+
toFormatOfEqIso = MkIso
185+
{ to = \(Evidence _ f) => Evidence _ (toFormatOfEq f)
186+
, from = \(Evidence _ f) => Evidence _ (toFormatEq f)
187+
, toFrom = \(Evidence _ (MkFormatOf _)) => Refl
188+
, fromTo = \(Evidence _ (f ** Refl)) => Refl
189+
}
166190
export
167191
either : (cond : Bool) -> (f1 : Format) -> (f2 : Format) -> FormatOf (if cond then Rep f1 else Rep f2)
168192
either True f1 _ = MkFormatOf f1

0 commit comments

Comments
 (0)