Compare commits
2 Commits
c743a99356
...
cde2a9b0d6
Author | SHA1 | Date |
---|---|---|
rhiannon morris | cde2a9b0d6 | |
rhiannon morris | 274ecfb58c |
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
@ -27,32 +31,11 @@ defPrettyOpts = MakePrettyOpts {unicode = True, color = True}
|
|||
public export
|
||||
data HL
|
||||
= Delim
|
||||
| TVar
|
||||
| TVarErr
|
||||
| Dim
|
||||
| DVar
|
||||
| DVarErr
|
||||
| Free | 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
|
||||
|
||||
%runElab derive "HL" [Generic, Meta, Eq, Ord, DecEq, Show]
|
||||
|
||||
public export
|
||||
data PPrec
|
||||
|
@ -63,21 +46,7 @@ data PPrec
|
|||
| 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
|
||||
%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
|
||||
|
|
|
@ -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]
|
||||
|
||||
|
||||
|
|
|
@ -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]
|
||||
|
||||
|
||||
|
|
|
@ -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
|
|
@ -9,7 +9,7 @@ depends = base, contrib, elab-util, sop, snocvect
|
|||
|
||||
modules =
|
||||
Quox.NatExtra,
|
||||
Quox.CharExtra,
|
||||
Quox.Unicode,
|
||||
Quox.OPE,
|
||||
Quox.Pretty,
|
||||
Quox.Syntax,
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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']
|
||||
]
|
|
@ -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
|
||||
]
|
||||
]
|
Loading…
Reference in New Issue