deriving

.gitignore

@@ -1,4 +1,5 @@
-build
 .build
+build
 depends
+*.ipkg
 *~

sirdi.json

@@ -10,7 +10,13 @@
 
       "deps" : [
         { "name" : "base",    "legacy" : true },
-        { "name" : "contrib", "legacy" : true }
+        { "name" : "contrib", "legacy" : true },
+        { "name" : "sop",
+          "git" : {
+            "url" : "https://git.rhiannon.website/rhi/idris2-sop",
+            "commit" : "defdbc74a28104a32149922ed9f9ee70099d4f59"
+          }
+        }
       ],
 
       "modules" : [

src/Quox/Lexer.idr

@@ -4,8 +4,10 @@ import Quox.Error
 
 import Data.String
 import public Text.Lexer
+import Generics.Derive
 
 %default total
+%language ElabReflection
 
 
 public export
@@ -25,25 +27,7 @@ data Punc
 | Times | Triangle
 | Wild
 
-puncRepr : Punc -> Nat
-puncRepr = \case
-  LParen => 0;  RParen   => 1;  LSquare => 2; RSquare => 3
-  LBrace => 4;  RBrace   => 5;  Comma   => 5
-  Colon  => 6;  DblColon => 7;  Arrow   => 8; DblArrow => 9
-  Times  => 10; Triangle => 11
-  Wild   => 12
-
-export Eq  Punc where (==)    = (==)    `on` puncRepr
-export Ord Punc where compare = compare `on` puncRepr
-
-export
-Show Punc where
-  show = \case
-    LParen  => "'('"; RParen   => "')'"; LSquare => "'['"; RSquare  => "']'"
-    LBrace  => "'{'"; RBrace   => "'}'"; Comma   => "','"
-    Colon   => "':'"; DblColon => "'∷'"; Arrow   => "'→'"; DblArrow => "'⇒'"
-    Times   => "'×'"; Triangle => "'⊲'"
-    Wild    => "'_'"
+%runElab derive "Punc" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 
 
@@ -52,19 +36,7 @@ data Kind
 = P Punc
 | Name | Symbol
 
-kindRepr : Kind -> (Nat, Nat)
-kindRepr (P p)   = (0, puncRepr p)
-kindRepr Name    = (1, 0)
-kindRepr Symbol  = (2, 0)
-
-export Eq  Kind where (==)    = (==)    `on` kindRepr
-export Ord Kind where compare = compare `on` kindRepr
-
-export
-Show Kind where
-  show (P p)  = show p
-  show Name   = "Name"
-  show Symbol = "Symbol"
+%runElab derive "Kind" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 
 export

src/Quox/Syntax/Dim.idr

@@ -6,8 +6,11 @@ import Quox.Pretty
 
 import Decidable.Equality
 import Control.Function
+import Generics.Derive
 
 %default total
+%language ElabReflection
+%hide SOP.from; %hide SOP.to
 
 
 public export
@@ -17,11 +20,7 @@ data DimConst = Zero | One
 private DCRepr : Type
 DCRepr = Nat
 
-private %inline dcrepr : DimConst -> DCRepr
-dcrepr e = case e of Zero => 0; One => 1
-
-export Eq  DimConst where (==) = (==) `on` dcrepr
-export Ord DimConst where compare = compare `on` dcrepr
+%runElab derive "DimConst" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 
 public export
@@ -30,11 +29,10 @@ data Dim : Nat -> Type where
   B : Var d -> Dim d
 %name Dim.Dim p, q
 
-private DRepr : Type
-DRepr = Nat
-
-private %inline drepr : Dim n -> DRepr
-drepr p = case p of K i => dcrepr i; B i => 2 + i.nat
+private %inline
+drepr : Dim n -> Either DimConst (Var n)
+drepr (K k) = Left k
+drepr (B x) = Right x
 
 export Eq  (Dim n) where (==) = (==) `on` drepr
 export Ord (Dim n) where compare = compare `on` drepr
@@ -86,8 +84,8 @@ export Uninhabited (One  = Zero) where uninhabited _ impossible
 export Uninhabited (B i = K e) where uninhabited _ impossible
 export Uninhabited (K e = B i) where uninhabited _ impossible
 
-public export %inline Injective B where injective Refl = Refl
-public export %inline Injective K where injective Refl = Refl
+public export %inline Injective Dim.B where injective Refl = Refl
+public export %inline Injective Dim.K where injective Refl = Refl
 
 public export
 DecEq DimConst where

src/Quox/Syntax/Qty.idr

@@ -3,22 +3,17 @@ module Quox.Syntax.Qty
 import Quox.Pretty
 
 import Data.Fin
+import Generics.Derive
 
 %default total
+%language ElabReflection
 
 
 public export
 data Qty = Zero | One | Any
 %name Qty.Qty pi, rh
 
-private Repr : Type
-Repr = Fin 3
-
-private %inline repr : Qty -> Repr
-repr pi = case pi of Zero => 0; One => 1; Any => 2
-
-export Eq  Qty where (==) = (==) `on` repr
-export Ord Qty where compare = compare `on` repr
+%runElab derive "Qty" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 
 export

src/Quox/Syntax/Universe.idr

@@ -3,8 +3,10 @@ module Quox.Syntax.Universe
 import Quox.Pretty
 
 import Data.Fin
+import Generics.Derive
 
 %default total
+%language ElabReflection
 
 
 ||| `UAny` doesn't show up in programs, but when checking something is
@@ -13,14 +15,7 @@ public export
 data Universe = U Nat | UAny
 %name Universe l
 
-private Repr : Type
-Repr = (Fin 2, Nat)
-
-private %inline repr : Universe -> Repr
-repr u = case u of U i => (0, i); UAny => (1, 0)
-
-export Eq  Universe where (==) = (==) `on` repr
-export Ord Universe where compare = compare `on` repr
+%runElab derive "Universe" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 export
 PrettyHL Universe where