From ba3612d836e480cb2c12da5b1500b610f169ece5 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 2 May 2022 22:38:37 +0200 Subject: [PATCH 1/2] %default total --- src/Quox/Lexer.idr | 2 ++ src/Quox/NatExtra.idr | 2 ++ src/Quox/OPE.idr | 2 ++ src/Quox/Reduce.idr | 2 ++ src/Quox/Syntax/Qty.idr | 2 ++ src/Quox/Syntax/Term/Pretty.idr | 1 + src/Quox/Syntax/Term/Reduce.idr | 2 ++ src/Quox/Syntax/Term/Subst.idr | 2 ++ 8 files changed, 15 insertions(+) diff --git a/src/Quox/Lexer.idr b/src/Quox/Lexer.idr index d2baaa0..7e11b4e 100644 --- a/src/Quox/Lexer.idr +++ b/src/Quox/Lexer.idr @@ -5,6 +5,8 @@ import Quox.Error import Data.String import public Text.Lexer +%default total + public export record Error where diff --git a/src/Quox/NatExtra.idr b/src/Quox/NatExtra.idr index f17179f..9e7d5de 100644 --- a/src/Quox/NatExtra.idr +++ b/src/Quox/NatExtra.idr @@ -2,6 +2,8 @@ module Quox.NatExtra import public Data.Nat +%default total + public export data LTE' : Nat -> Nat -> Type where diff --git a/src/Quox/OPE.idr b/src/Quox/OPE.idr index b3a381d..0f50df0 100644 --- a/src/Quox/OPE.idr +++ b/src/Quox/OPE.idr @@ -6,6 +6,8 @@ import Quox.NatExtra import Data.Nat +%default total + public export data OPE : Nat -> Nat -> Type where diff --git a/src/Quox/Reduce.idr b/src/Quox/Reduce.idr index 50f4038..8e25794 100644 --- a/src/Quox/Reduce.idr +++ b/src/Quox/Reduce.idr @@ -2,6 +2,8 @@ module Quox.Reduce import public Quox.Syntax +%default total + public export data IsRedexT : Term d n -> Type where diff --git a/src/Quox/Syntax/Qty.idr b/src/Quox/Syntax/Qty.idr index cea9af9..652b1e0 100644 --- a/src/Quox/Syntax/Qty.idr +++ b/src/Quox/Syntax/Qty.idr @@ -4,6 +4,8 @@ import Quox.Pretty import Data.Fin +%default total + public export data Qty = Zero | One | Any diff --git a/src/Quox/Syntax/Term/Pretty.idr b/src/Quox/Syntax/Term/Pretty.idr index 59d0578..1386cd2 100644 --- a/src/Quox/Syntax/Term/Pretty.idr +++ b/src/Quox/Syntax/Term/Pretty.idr @@ -7,6 +7,7 @@ import Quox.Pretty import Data.Vect +%default total parameters {auto _ : Pretty.HasEnv m} diff --git a/src/Quox/Syntax/Term/Reduce.idr b/src/Quox/Syntax/Term/Reduce.idr index 267304a..f0266ef 100644 --- a/src/Quox/Syntax/Term/Reduce.idr +++ b/src/Quox/Syntax/Term/Reduce.idr @@ -3,6 +3,8 @@ module Quox.Syntax.Term.Reduce import Quox.Syntax.Term.Base import Quox.Syntax.Term.Subst +%default total + mutual ||| true if a term has a closure or dimension closure at the top level, diff --git a/src/Quox/Syntax/Term/Subst.idr b/src/Quox/Syntax/Term/Subst.idr index 1b76225..8e48065 100644 --- a/src/Quox/Syntax/Term/Subst.idr +++ b/src/Quox/Syntax/Term/Subst.idr @@ -2,6 +2,8 @@ module Quox.Syntax.Term.Subst import Quox.Syntax.Term.Base +%default total + export FromVar (Elim d) where fromVar = B export FromVar (Term d) where fromVar = E . fromVar From ce3342f330484e826abbcbc0808ea3bd2f52a28a Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 2 May 2022 22:40:28 +0200 Subject: [PATCH 2/2] 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