derive impls where possible

lib/Quox/Equal.idr

@@ -3,14 +3,15 @@ module Quox.Equal
 import public Quox.Syntax
 import public Quox.Reduce
 import Control.Monad.Either
+import Generics.Derive
 
 %default total
+%language ElabReflection
 
 
 public export
 data Mode = Equal | Sub
-
-export %inline Show Mode where show Equal = "Equal"; show Sub = "Sub"
+%runElab derive "Mode" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 public export
 data Error

lib/Quox/Name.idr

@@ -2,22 +2,18 @@ module Quox.Name
 
 import public Data.SnocList
 import Data.List
+import Generics.Derive
+
+%hide TT.Name
 
 %default total
+%language ElabReflection
 
 
 public export
-data BaseName =
-    UN String -- user-given name
-
-private BRepr : Type
-BRepr = String
-
-private %inline brepr : BaseName -> BRepr
-brepr (UN x) = x
-
-export Eq  BaseName where (==) = (==) `on` brepr
-export Ord BaseName where compare = compare `on` brepr
+data BaseName
+= UN String -- user-given name
+%runElab derive "BaseName" [Generic, Meta, Eq, Ord, DecEq]
 
 export
 Show BaseName where
@@ -38,15 +34,7 @@ record Name where
   constructor MakeName
   mods : SnocList String
   base : BaseName
-
-private Repr : Type
-Repr = (SnocList String, BRepr)
-
-private %inline repr : Name -> Repr
-repr x = (x.mods, brepr x.base)
-
-export Eq  Name where (==) = (==) `on` repr
-export Ord Name where compare = compare `on` repr
+%runElab derive "Name" [Generic, Meta, Eq, Ord]
 
 export
 Show Name where

lib/Quox/Pretty.idr

@@ -10,8 +10,12 @@ import Data.DPair
 
 import public Control.Monad.Identity
 import public Control.Monad.Reader
+import Generics.Derive
 
 %default total
+%language ElabReflection
+
+%hide TT.Name
 
 
 public export
@@ -26,58 +30,23 @@ defPrettyOpts = MakePrettyOpts {unicode = True, color = True}
 
 public export
 data HL
-  = Delim
-  | TVar
-  | TVarErr
-  | Dim
-  | DVar
-  | DVarErr
-  | Qty
-  | Free
-  | Syntax
-
-private HLRepr : Type
-HLRepr = Nat
-
-private %inline hlRepr : HL -> Nat
-hlRepr Delim   = 0
-hlRepr TVar    = 1
-hlRepr TVarErr = 2
-hlRepr Dim     = 3
-hlRepr DVar    = 4
-hlRepr DVarErr = 5
-hlRepr Qty     = 6
-hlRepr Free    = 7
-hlRepr Syntax  = 8
-
-export %inline Eq  HL where (==) = (==) `on` hlRepr
-export %inline Ord HL where compare = compare `on` hlRepr
-
+= Delim
+| Free | TVar | TVarErr
+| Dim  | DVar | DVarErr
+| Qty
+| Syntax
+%runElab derive "HL" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 public export
 data PPrec
-  = Outer
-  | Ann  -- right of "::"
-  | AnnL -- left  of "::"
+= Outer
+| Ann  -- right of "::"
+| AnnL -- left  of "::"
   -- ...
-  | App  -- term/dimension application
-  | SApp -- substitution application
-  | Arg  -- argument to nonfix function
-
-private PrecRepr : Type
-PrecRepr = Nat
-
-private %inline precRepr : PPrec -> PrecRepr
-precRepr Outer = 0
-precRepr Ann   = 1
-precRepr AnnL  = 2
--- ...
-precRepr App   = 98
-precRepr SApp  = 99
-precRepr Arg   = 100
-
-export %inline Eq  PPrec where (==) = (==) `on` precRepr
-export %inline Ord PPrec where compare = compare `on` precRepr
+| App  -- term/dimension application
+| SApp -- substitution application
+| Arg  -- argument to nonfix function
+%runElab derive "PPrec" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 
 export %inline
@@ -100,6 +69,7 @@ hlF' = map . hl'
 export %inline
 parens : Doc HL -> Doc HL
 parens doc = hl Delim "(" <+> doc <+> hl Delim ")"
+%hide Symbols.parens
 
 export %inline
 parensIf : Bool -> Doc HL -> Doc HL
@@ -138,7 +108,8 @@ record PrettyEnv where
   ||| surrounding precedence level
   prec    : PPrec
 
-public export HasEnv : (Type -> Type) -> Type
+public export
+HasEnv : (Type -> Type) -> Type
 HasEnv = MonadReader PrettyEnv
 
 export %inline

lib/Quox/Syntax/Dim.idr

@@ -17,9 +17,6 @@ public export
 data DimConst = Zero | One
 %name DimConst e
 
-private DCRepr : Type
-DCRepr = Nat
-
 %runElab derive "DimConst" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 

lib/Quox/Token.idr

@@ -18,7 +18,6 @@ data Punc
 | Arrow | DblArrow
 | Times | Triangle
 | Wild
-
 %runElab derive "Punc" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 
@@ -26,7 +25,6 @@ public export
 data Keyword
 = Lam | Let | In | Case | Of | Omega
 | Pi | Sigma | W
-
 %runElab derive "Keyword" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 
@@ -34,7 +32,6 @@ data Keyword
 ||| quantity & dimension constants
 public export
 data Number = Zero | One | Other Nat
-
 %runElab derive "Number" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 
@@ -44,7 +41,6 @@ data Token
 | K Keyword
 | Name String | Symbol String
 | N Number | TYPE Nat
-
 %runElab derive "Token" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 

lib/Quox/Unicode.idr

@@ -1,4 +1,4 @@
-module Quox.CharExtra
+module Quox.Unicode
 
 import Generics.Derive
 
@@ -133,3 +133,8 @@ isWhitespace : Char -> Bool
 isWhitespace ch =
   ch == '\t' || ch == '\r' || ch == '\n' ||
   case genCat ch of Separator _ => True; _ => False
+
+
+export
+%foreign "scheme:string-normalize-nfc"
+normalizeNfc : String -> String

lib/quox-lib.ipkg

@@ -9,7 +9,7 @@ depends = base, contrib, elab-util, sop, snocvect
 
 modules =
   Quox.NatExtra,
-  Quox.CharExtra,
+  Quox.Unicode,
   Quox.OPE,
   Quox.Pretty,
   Quox.Syntax,

tests/Tests.idr

@@ -2,7 +2,7 @@ module Tests
 
 import Options
 import TAP
-import Tests.CharExtra
+import Tests.Unicode
 import Tests.Lexer
 import Tests.Parser
 import Tests.Equal
@@ -10,7 +10,7 @@ import System
 
 
 allTests = [
-  CharExtra.tests,
+  Unicode.tests,
   Lexer.tests,
   Parser.tests,
   Equal.tests

tests/Tests/CharExtra.idr

@@ -1,56 +0,0 @@
-module Tests.CharExtra
-
-import Quox.NatExtra
-import Quox.CharExtra
-import Data.List
-import Data.String
-import Data.Maybe
-import TAP
-
-
-escape : Char -> Maybe String
-escape '\'' = Nothing
-escape c =
-  if ord c > 0xFF then Nothing else
-  case unpack $ show c of
-       '\'' :: '\\' :: cs => pack . ('\\' ::) <$> init' cs
-       _                  => Nothing
-
-display : Char -> String
-display c =
-  let ord = cast c {to = Nat} in
-  let c'  = fromMaybe (singleton c) $ escape c in
-  if 0x20 <= ord && ord <= 0xFF then
-    "｢\{c'}｣"
-  else
-    let codepoint = padLeft 4 '0' $ showHex ord in
-    "｢\{c'}｣ (U+\{codepoint})"
-
-testOne : (Char -> Bool) -> Char -> Test
-testOne pred c = test (display c) $ unless (pred c) $ Left ()
-
-testAll : String -> (Char -> Bool) -> List Char -> Test
-testAll label pred chars = label :- map (testOne pred) chars
-
-
-tests = "char extras" :- [
-  testAll "id starts" isIdStart
-    ['a', 'á', '𝕕', '개', 'ʨ', '𒁙', '𝟙'],
-  testAll "not id starts" (not . isIdStart)
-    ['0', '_', '-', '‿', ' ', '[', ',', '.', '\1'],
-  testAll "id continuations" isIdCont
-    ['a', 'á', '𝕕', '개', 'ʨ', '𒁙', '0', '\''],
-  testAll "not id continuations" (not . isIdCont)
-    ['_', '‿', ' ', '[', ',', '.', '\1'],
-  testAll "id connectors" isIdConnector
-    ['_', '‿'],
-  testAll "not id connectors" (not . isIdConnector)
-    ['a', ' ', ',', '-'],
-  testAll "white space" isWhitespace
-    [' ', '\t', '\r', '\n',
-     '\x2028', -- line separator
-     '\x2029'  -- paragraph separator
-    ],
-  testAll "not white space" (not . isWhitespace)
-    ['a', '-', '_', '\1']
-]

tests/Tests/Unicode.idr

@@ -0,0 +1,90 @@
+module Tests.Unicode
+
+import Quox.NatExtra
+import Quox.Unicode
+import Data.List
+import Data.String
+import Data.Maybe
+import TAP
+
+
+maxLatin1 = '\xFF'
+
+escape : Char -> Maybe String
+escape '\'' = Nothing
+escape c =
+  if c > maxLatin1 then Nothing else
+  case unpack $ show c of
+       '\'' :: '\\' :: cs => pack . ('\\' ::) <$> init' cs
+       _                  => Nothing
+
+codepoint : Char -> String
+codepoint = padLeft 4 '0' . showHex . cast
+
+display : Char -> String
+display c =
+  let c'  = fromMaybe (singleton c) $ escape c in
+  if '\x20' <= c && c <= maxLatin1
+     then "｢\{c'}｣"
+     else "｢\{c'}｣ (U+\{codepoint c})"
+
+displayS' : String -> String
+displayS' =
+  foldMap (\c => if c <= maxLatin1 then singleton c else "\\x\{codepoint c}") .
+  unpack
+
+displayS : String -> String
+displayS str =
+  if all (<= maxLatin1) (unpack str)
+     then "｢\{str}｣"
+     else "｢\{str}｣ (\"\{displayS' str}\")"
+
+testOneChar : (Char -> Bool) -> Char -> Test
+testOneChar pred c = test (display c) $ unless (pred c) $ Left ()
+
+testAllChars : String -> (Char -> Bool) -> List Char -> Test
+testAllChars label pred chars = label :- map (testOneChar pred) chars
+
+
+testNfc : String -> String -> Test
+testNfc input result =
+  test (displayS input) $
+  let norm = normalizeNfc input in
+  unless (norm == result) $
+  Left [("expected", displayS result), ("received", displayS norm)]
+
+testAlreadyNfc : String -> Test
+testAlreadyNfc input = testNfc input input
+
+
+
+tests = "unicode" :- [
+  "general categories" :- [
+    testAllChars "id starts" isIdStart
+      ['a', 'á', '𝕕', '개', 'ʨ', '𒁙', '𝟙'],
+    testAllChars "not id starts" (not . isIdStart)
+      ['0', '_', '-', '‿', ' ', '[', ',', '.', '\1'],
+    testAllChars "id continuations" isIdCont
+      ['a', 'á', '𝕕', '개', 'ʨ', '𒁙', '0', '\''],
+    testAllChars "not id continuations" (not . isIdCont)
+      ['_', '‿', ' ', '[', ',', '.', '\1'],
+    testAllChars "id connectors" isIdConnector
+      ['_', '‿'],
+    testAllChars "not id connectors" (not . isIdConnector)
+      ['a', ' ', ',', '-'],
+    testAllChars "white space" isWhitespace
+      [' ', '\t', '\r', '\n',
+       '\x2028', -- line separator
+       '\x2029'  -- paragraph separator
+      ],
+    testAllChars "not white space" (not . isWhitespace)
+      ['a', '-', '_', '\1']
+  ],
+
+  "normalisation" :- [
+    testNfc        "e\x301" "é",
+    testAlreadyNfc "é",
+    testAlreadyNfc ""
+    -- idk if this is wrong it's chez's fault. or unicode's
+  ]
+]