Switch to using records for singletons

Author: brendanzab

experiments/idris/src/Fathom/Base.idr

@@ -19,21 +19,29 @@ record Refine (0 A : Type) (0 P : A -> Type) where
   ||| The wrapped value
   value : A
   ||| The proof of the proposition
-  0 prf : P value
+  {auto 0 prf : P value}
 
 ||| Refine a value with a proposition
 public export
 refine : {0 A : Type} -> {0 P : A -> Type} -> (value : A) -> {auto 0 prf : P value} -> Refine A P
-refine value {prf} = MkRefine { value, prf }
+refine value = MkRefine { value }
 
 
 ||| Singleton types
 |||
 ||| Inspired by [this type](https://agda.readthedocs.io/en/v2.5.4.1/language/with-abstraction.html#the-inspect-idiom)
 ||| from the Agda docs.
 public export
-data Sing : {0 A : Type} -> (x : A) -> Type where
-  MkSing : {0 A : Type} -> {0 x : A} -> (0 y : A) -> {auto 0 prf : x = y} -> Sing x
+record Sing {0 A : Type} (x : A) where
+  constructor MkSing
+  0 value : A
+  {auto 0 prf : x = value}
+
+
+||| Convert a singleton back to its underlying value
+public export
+sing : {0 A : Type} -> {0 x : A} -> (0 value : A) -> {auto 0 prf : x = value} -> Sing x
+sing value = MkSing { value }
 
 ||| Convert a singleton back to its underlying value
 public export

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

@@ -37,7 +37,7 @@ decode End [] = Just ((), [])
 decode End (_::_) = Nothing
 decode Fail _ = Nothing
 decode (Pure x) buffer =
-  Just (MkSing x, buffer)
+  Just (sing x, buffer)
 decode (Skip f _) buffer = do
   (x, buffer') <- decode f buffer
   Just ((), buffer')

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

@@ -87,7 +87,7 @@ decode End [] = Just ((), [])
 decode End (_::_) = Nothing
 decode Fail _ = Nothing
 decode (Pure x) buffer =
-  Just (MkSing x, buffer)
+  Just (sing x, buffer)
 decode (Skip f _) buffer = do
   (x, buffer') <- decode f buffer
   Just ((), buffer')
@@ -173,7 +173,7 @@ orPure' False _ def = refine (Pure def)
 
 foo : (cond : Bool) -> (f : Format) -> Rep f -> Format
 foo cond f def = case orPure cond (toFormatOf f) def of
-  MkRefine f' prf =>
+  MkRefine f' {prf} =>
     Bind f' (\x => case cond of
       True => ?todo1
       False => ?todo2)

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

@@ -64,7 +64,7 @@ decode End [] = Just ((), [])
 decode End (_::_) = Nothing
 decode Fail _ = Nothing
 decode (Pure x) buffer =
-  Just (MkSing x, buffer)
+  Just (sing x, buffer)
 decode (Skip f _) buffer = do
   (x, buffer') <- decode f buffer
   Just ((), buffer')
@@ -150,7 +150,7 @@ orPure' False _ def = refine (Pure def)
 
 foo : (cond : Bool) -> (f : Format) -> Rep f -> Format
 foo cond f def = case orPure cond (toFormatOf f) def of
-  MkRefine f' prf =>
+  MkRefine f' {prf} =>
     Bind f' (\x => case cond of
       True => ?todo1
       False => ?todo2)

experiments/idris/src/Fathom/Open/Record.idr

@@ -57,7 +57,7 @@ pure x = MkFormat { Rep, decode, encode } where
   Rep = Sing x
 
   decode : Decode Rep BitStream
-  decode buffer = Just (MkSing x, buffer)
+  decode buffer = Just (sing x, buffer)
 
   encode : Encode Rep BitStream
   encode (MkSing _) buffer = Just buffer