From ce3342f330484e826abbcbc0808ea3bd2f52a28a Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 2 May 2022 22:40:28 +0200 Subject: [PATCH] deriving --- .gitignore | 3 ++- sirdi.json | 8 +++++++- src/Quox/Lexer.idr | 36 ++++-------------------------------- src/Quox/Syntax/Dim.idr | 22 ++++++++++------------ src/Quox/Syntax/Qty.idr | 11 +++-------- src/Quox/Syntax/Universe.idr | 11 +++-------- 6 files changed, 29 insertions(+), 62 deletions(-) diff --git a/.gitignore b/.gitignore index 23ee719..afc6d59 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ -build .build +build depends +*.ipkg *~ diff --git a/sirdi.json b/sirdi.json index 649f028..0a192c5 100644 --- a/sirdi.json +++ b/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" : [ diff --git a/src/Quox/Lexer.idr b/src/Quox/Lexer.idr index 7e11b4e..feaaaf4 100644 --- a/src/Quox/Lexer.idr +++ b/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 diff --git a/src/Quox/Syntax/Dim.idr b/src/Quox/Syntax/Dim.idr index 57b8b88..d5fe1c1 100644 --- a/src/Quox/Syntax/Dim.idr +++ b/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 diff --git a/src/Quox/Syntax/Qty.idr b/src/Quox/Syntax/Qty.idr index 652b1e0..a9bdbd9 100644 --- a/src/Quox/Syntax/Qty.idr +++ b/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 diff --git a/src/Quox/Syntax/Universe.idr b/src/Quox/Syntax/Universe.idr index 9b3ba1e..10d6075 100644 --- a/src/Quox/Syntax/Universe.idr +++ b/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