From fc3c2dc8ab061ed569feb2b922acc79c265d5ec9 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 2 Mar 2023 19:52:32 +0100 Subject: [PATCH] =?UTF-8?q?sop=20=E2=86=92=20elab-util?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- lib/Quox/CharExtra.idr | 18 +++++++++--------- lib/Quox/Lexer.idr | 8 ++++---- lib/Quox/Name.idr | 6 +++--- lib/Quox/Pretty.idr | 6 +++--- lib/Quox/Syntax/Dim.idr | 5 ++--- lib/Quox/Syntax/Qty/Three.idr | 16 ++++++++++++++-- lib/Quox/Syntax/Universe.idr | 4 ++-- lib/Quox/Typing.idr | 6 ++---- lib/quox-lib.ipkg | 2 +- 9 files changed, 40 insertions(+), 31 deletions(-) diff --git a/lib/Quox/CharExtra.idr b/lib/Quox/CharExtra.idr index 708261f..b9a3572 100644 --- a/lib/Quox/CharExtra.idr +++ b/lib/Quox/CharExtra.idr @@ -1,6 +1,6 @@ module Quox.CharExtra -import Generics.Derive +import Derive.Prelude %default total @@ -10,38 +10,38 @@ import Generics.Derive namespace Letter public export data Letter = Uppercase | Lowercase | Titlecase | Modifier | Other - %runElab derive "Letter" [Generic, Meta, Eq, Ord, DecEq, Show] + %runElab derive "Letter" [Eq, Ord, Show] namespace Mark public export data Mark = NonSpacing | SpacingCombining | Enclosing - %runElab derive "Mark" [Generic, Meta, Eq, Ord, DecEq, Show] + %runElab derive "Mark" [Eq, Ord, Show] namespace Number public export data Number = Decimal | Letter | Other - %runElab derive "Number" [Generic, Meta, Eq, Ord, DecEq, Show] + %runElab derive "Number" [Eq, Ord, Show] namespace Punctuation public export data Punctuation = Connector | Dash | Open | Close | InitialQuote | FinalQuote | Other - %runElab derive "Punctuation" [Generic, Meta, Eq, Ord, DecEq, Show] + %runElab derive "Punctuation" [Eq, Ord, Show] namespace Symbol public export data Symbol = Math | Currency | Modifier | Other - %runElab derive "Symbol" [Generic, Meta, Eq, Ord, DecEq, Show] + %runElab derive "Symbol" [Eq, Ord, Show] namespace Separator public export data Separator = Space | Line | Paragraph - %runElab derive "Separator" [Generic, Meta, Eq, Ord, DecEq, Show] + %runElab derive "Separator" [Eq, Ord, Show] namespace Other public export data Other = Control | Format | Surrogate | PrivateUse | NotAssigned - %runElab derive "Other" [Generic, Meta, Eq, Ord, DecEq, Show] + %runElab derive "Other" [Eq, Ord, Show] public export @@ -53,7 +53,7 @@ data GeneralCategory | Symbol Symbol | Separator Separator | Other Other -%runElab derive "GeneralCategory" [Generic, Meta, Eq, Ord, DecEq, Show] +%runElab derive "GeneralCategory" [Eq, Ord, Show] private %foreign "scheme:(lambda (c) (symbol->string (char-general-category c)))" diff --git a/lib/Quox/Lexer.idr b/lib/Quox/Lexer.idr index 2b2cb9f..163f065 100644 --- a/lib/Quox/Lexer.idr +++ b/lib/Quox/Lexer.idr @@ -6,7 +6,7 @@ import Data.String.Extra import Data.SortedMap import Text.Lexer import Text.Lexer.Tokenizer -import Generics.Derive +import Derive.Prelude %hide TT.Name @@ -22,7 +22,7 @@ import Generics.Derive ||| @ TYPE "Type" or "★" with subscript public export data Token = R String | I Name | N Nat | S String | T String | TYPE Nat -%runElab derive "Token" [Generic, Meta, Eq, Ord, DecEq, Show] +%runElab derive "Token" [Eq, Ord, Show] -- token or whitespace private @@ -37,8 +37,8 @@ record Error where line, col : Int ||| `Nothing` if the error is at the end of the input char : Maybe Char -%runElab derive "StopReason" [Generic, Meta, Eq, Ord, DecEq, Show] -%runElab derive "Error" [Generic, Meta, Eq, Ord, DecEq, Show] +%runElab derive "StopReason" [Eq, Ord, Show] +%runElab derive "Error" [Eq, Ord, Show] skip : Lexer -> Tokenizer TokenW diff --git a/lib/Quox/Name.idr b/lib/Quox/Name.idr index 3387522..372c9f1 100644 --- a/lib/Quox/Name.idr +++ b/lib/Quox/Name.idr @@ -2,7 +2,7 @@ module Quox.Name import public Data.SnocList import Data.List -import Generics.Derive +import Derive.Prelude %hide TT.Name @@ -13,7 +13,7 @@ import Generics.Derive public export data BaseName = UN String -- user-given name -%runElab derive "BaseName" [Generic, Meta, Eq, Ord, DecEq] +%runElab derive "BaseName" [Eq, Ord] export Show BaseName where @@ -34,7 +34,7 @@ record Name where constructor MakeName mods : SnocList String base : BaseName -%runElab derive "Name" [Generic, Meta, Eq, Ord, DecEq] +%runElab derive "Name" [Eq, Ord] export Show Name where diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr index fddcc81..211d0c0 100644 --- a/lib/Quox/Pretty.idr +++ b/lib/Quox/Pretty.idr @@ -10,7 +10,7 @@ import Data.DPair import public Control.Monad.Identity import public Control.Monad.Reader -import Generics.Derive +import Derive.Prelude %default total %language ElabReflection @@ -36,7 +36,7 @@ data HL | Qty | Syntax | Tag -%runElab derive "HL" [Generic, Meta, Eq, Ord, DecEq, Show] +%runElab derive "HL" [Eq, Ord, Show] public export data PPrec @@ -49,7 +49,7 @@ data PPrec | App -- term/dimension application | SApp -- substitution application | Arg -- argument to nonfix function -%runElab derive "PPrec" [Generic, Meta, Eq, Ord, DecEq, Show] +%runElab derive "PPrec" [Eq, Ord, Show] export %inline diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr index fe0c974..54faaa6 100644 --- a/lib/Quox/Syntax/Dim.idr +++ b/lib/Quox/Syntax/Dim.idr @@ -6,18 +6,17 @@ import Quox.Pretty import Decidable.Equality import Control.Function -import Generics.Derive +import Derive.Prelude %default total %language ElabReflection -%hide SOP.from; %hide SOP.to public export data DimConst = Zero | One %name DimConst e -%runElab derive "DimConst" [Generic, Meta, Eq, Ord, DecEq, Show] +%runElab derive "DimConst" [Eq, Ord, Show] ||| `ends l r e` returns `l` if `e` is `Zero`, or `r` if it is `One`. public export diff --git a/lib/Quox/Syntax/Qty/Three.idr b/lib/Quox/Syntax/Qty/Three.idr index 2bc6585..47cb1a4 100644 --- a/lib/Quox/Syntax/Qty/Three.idr +++ b/lib/Quox/Syntax/Qty/Three.idr @@ -2,7 +2,7 @@ module Quox.Syntax.Qty.Three import Quox.Pretty import public Quox.Syntax.Qty -import Generics.Derive +import Derive.Prelude %default total %language ElabReflection @@ -12,7 +12,7 @@ public export data Three = Zero | One | Any %name Three pi, rh -%runElab derive "Three" [Generic, Meta, Eq, Ord, DecEq, Show] +%runElab derive "Three" [Eq, Ord, Show] export @@ -23,6 +23,18 @@ PrettyHL Three where One => ifUnicode "𝟭" "1" Any => ifUnicode "𝛚" "*" +public export +DecEq Three where + decEq Zero Zero = Yes Refl + decEq Zero One = No $ \case _ impossible + decEq Zero Any = No $ \case _ impossible + decEq One Zero = No $ \case _ impossible + decEq One One = Yes Refl + decEq One Any = No $ \case _ impossible + decEq Any Zero = No $ \case _ impossible + decEq Any One = No $ \case _ impossible + decEq Any Any = Yes Refl + public export plus : Three -> Three -> Three diff --git a/lib/Quox/Syntax/Universe.idr b/lib/Quox/Syntax/Universe.idr index ff315b8..6275eb9 100644 --- a/lib/Quox/Syntax/Universe.idr +++ b/lib/Quox/Syntax/Universe.idr @@ -3,7 +3,7 @@ module Quox.Syntax.Universe import Quox.Pretty import Data.Fin -import Generics.Derive +import Derive.Prelude %default total %language ElabReflection @@ -15,7 +15,7 @@ public export data Universe = U Nat | UAny %name Universe l -%runElab derive "Universe" [Generic, Meta, Eq, Ord, DecEq, Show] +%runElab derive "Universe" [Eq, Ord, Show] export PrettyHL Universe where diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr index 4cace58..a0be896 100644 --- a/lib/Quox/Typing.idr +++ b/lib/Quox/Typing.idr @@ -6,11 +6,9 @@ import public Quox.Reduce import public Data.SortedMap import public Control.Monad.Either -import Generics.Derive +import Derive.Prelude %hide TT.Name -%hide SOP.from -%hide SOP.to %default total %language ElabReflection @@ -103,7 +101,7 @@ InferResult eqs q d n = IfConsistent eqs $ InferResult' q d n public export data EqMode = Equal | Sub | Super -%runElab derive "EqMode" [Generic, Meta, Eq, Ord, DecEq, Show] +%runElab derive "EqMode" [Eq, Ord, Show] public export diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg index 454d54d..484d0da 100644 --- a/lib/quox-lib.ipkg +++ b/lib/quox-lib.ipkg @@ -5,7 +5,7 @@ authors = "rhiannon morris" sourceloc = "https://git.rhiannon.website/rhi/quox" license = "acsl" -depends = base, contrib, elab-util, sop, snocvect +depends = base, contrib, elab-util, snocvect modules = Quox.NatExtra,