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.Syntax
|
||||||
import public Quox.Reduce
|
import public Quox.Reduce
|
||||||
import Control.Monad.Either
|
import Control.Monad.Either
|
||||||
|
import Generics.Derive
|
||||||
|
|
||||||
%default total
|
%default total
|
||||||
|
%language ElabReflection
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
data Mode = Equal | Sub
|
data Mode = Equal | Sub
|
||||||
|
%runElab derive "Mode" [Generic, Meta, Eq, Ord, DecEq, Show]
|
||||||
export %inline Show Mode where show Equal = "Equal"; show Sub = "Sub"
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
data Error
|
data Error
|
||||||
|
|
|
@ -2,22 +2,18 @@ module Quox.Name
|
||||||
|
|
||||||
import public Data.SnocList
|
import public Data.SnocList
|
||||||
import Data.List
|
import Data.List
|
||||||
|
import Generics.Derive
|
||||||
|
|
||||||
|
%hide TT.Name
|
||||||
|
|
||||||
%default total
|
%default total
|
||||||
|
%language ElabReflection
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
data BaseName =
|
data BaseName
|
||||||
UN String -- user-given name
|
= UN String -- user-given name
|
||||||
|
%runElab derive "BaseName" [Generic, Meta, Eq, Ord, DecEq]
|
||||||
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
|
|
||||||
|
|
||||||
export
|
export
|
||||||
Show BaseName where
|
Show BaseName where
|
||||||
|
@ -38,15 +34,7 @@ record Name where
|
||||||
constructor MakeName
|
constructor MakeName
|
||||||
mods : SnocList String
|
mods : SnocList String
|
||||||
base : BaseName
|
base : BaseName
|
||||||
|
%runElab derive "Name" [Generic, Meta, Eq, Ord]
|
||||||
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
|
|
||||||
|
|
||||||
export
|
export
|
||||||
Show Name where
|
Show Name where
|
||||||
|
|
|
@ -10,8 +10,12 @@ import Data.DPair
|
||||||
|
|
||||||
import public Control.Monad.Identity
|
import public Control.Monad.Identity
|
||||||
import public Control.Monad.Reader
|
import public Control.Monad.Reader
|
||||||
|
import Generics.Derive
|
||||||
|
|
||||||
%default total
|
%default total
|
||||||
|
%language ElabReflection
|
||||||
|
|
||||||
|
%hide TT.Name
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
|
@ -26,58 +30,23 @@ defPrettyOpts = MakePrettyOpts {unicode = True, color = True}
|
||||||
|
|
||||||
public export
|
public export
|
||||||
data HL
|
data HL
|
||||||
= Delim
|
= Delim
|
||||||
| TVar
|
| Free | TVar | TVarErr
|
||||||
| TVarErr
|
| Dim | DVar | DVarErr
|
||||||
| Dim
|
| Qty
|
||||||
| DVar
|
| Syntax
|
||||||
| DVarErr
|
%runElab derive "HL" [Generic, Meta, Eq, Ord, DecEq, Show]
|
||||||
| 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
|
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
data PPrec
|
data PPrec
|
||||||
= Outer
|
= Outer
|
||||||
| Ann -- right of "::"
|
| Ann -- right of "::"
|
||||||
| AnnL -- left of "::"
|
| AnnL -- left of "::"
|
||||||
-- ...
|
-- ...
|
||||||
| App -- term/dimension application
|
| App -- term/dimension application
|
||||||
| SApp -- substitution application
|
| SApp -- substitution application
|
||||||
| Arg -- argument to nonfix function
|
| Arg -- argument to nonfix function
|
||||||
|
%runElab derive "PPrec" [Generic, Meta, Eq, Ord, DecEq, Show]
|
||||||
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
|
|
||||||
|
|
||||||
|
|
||||||
export %inline
|
export %inline
|
||||||
|
@ -100,6 +69,7 @@ hlF' = map . hl'
|
||||||
export %inline
|
export %inline
|
||||||
parens : Doc HL -> Doc HL
|
parens : Doc HL -> Doc HL
|
||||||
parens doc = hl Delim "(" <+> doc <+> hl Delim ")"
|
parens doc = hl Delim "(" <+> doc <+> hl Delim ")"
|
||||||
|
%hide Symbols.parens
|
||||||
|
|
||||||
export %inline
|
export %inline
|
||||||
parensIf : Bool -> Doc HL -> Doc HL
|
parensIf : Bool -> Doc HL -> Doc HL
|
||||||
|
@ -138,7 +108,8 @@ record PrettyEnv where
|
||||||
||| surrounding precedence level
|
||| surrounding precedence level
|
||||||
prec : PPrec
|
prec : PPrec
|
||||||
|
|
||||||
public export HasEnv : (Type -> Type) -> Type
|
public export
|
||||||
|
HasEnv : (Type -> Type) -> Type
|
||||||
HasEnv = MonadReader PrettyEnv
|
HasEnv = MonadReader PrettyEnv
|
||||||
|
|
||||||
export %inline
|
export %inline
|
||||||
|
|
|
@ -17,9 +17,6 @@ public export
|
||||||
data DimConst = Zero | One
|
data DimConst = Zero | One
|
||||||
%name DimConst e
|
%name DimConst e
|
||||||
|
|
||||||
private DCRepr : Type
|
|
||||||
DCRepr = Nat
|
|
||||||
|
|
||||||
%runElab derive "DimConst" [Generic, Meta, Eq, Ord, DecEq, Show]
|
%runElab derive "DimConst" [Generic, Meta, Eq, Ord, DecEq, Show]
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -18,7 +18,6 @@ data Punc
|
||||||
| Arrow | DblArrow
|
| Arrow | DblArrow
|
||||||
| Times | Triangle
|
| Times | Triangle
|
||||||
| Wild
|
| Wild
|
||||||
|
|
||||||
%runElab derive "Punc" [Generic, Meta, Eq, Ord, DecEq, Show]
|
%runElab derive "Punc" [Generic, Meta, Eq, Ord, DecEq, Show]
|
||||||
|
|
||||||
|
|
||||||
|
@ -26,7 +25,6 @@ public export
|
||||||
data Keyword
|
data Keyword
|
||||||
= Lam | Let | In | Case | Of | Omega
|
= Lam | Let | In | Case | Of | Omega
|
||||||
| Pi | Sigma | W
|
| Pi | Sigma | W
|
||||||
|
|
||||||
%runElab derive "Keyword" [Generic, Meta, Eq, Ord, DecEq, Show]
|
%runElab derive "Keyword" [Generic, Meta, Eq, Ord, DecEq, Show]
|
||||||
|
|
||||||
|
|
||||||
|
@ -34,7 +32,6 @@ data Keyword
|
||||||
||| quantity & dimension constants
|
||| quantity & dimension constants
|
||||||
public export
|
public export
|
||||||
data Number = Zero | One | Other Nat
|
data Number = Zero | One | Other Nat
|
||||||
|
|
||||||
%runElab derive "Number" [Generic, Meta, Eq, Ord, DecEq, Show]
|
%runElab derive "Number" [Generic, Meta, Eq, Ord, DecEq, Show]
|
||||||
|
|
||||||
|
|
||||||
|
@ -44,7 +41,6 @@ data Token
|
||||||
| K Keyword
|
| K Keyword
|
||||||
| Name String | Symbol String
|
| Name String | Symbol String
|
||||||
| N Number | TYPE Nat
|
| N Number | TYPE Nat
|
||||||
|
|
||||||
%runElab derive "Token" [Generic, Meta, Eq, Ord, DecEq, Show]
|
%runElab derive "Token" [Generic, Meta, Eq, Ord, DecEq, Show]
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -1,4 +1,4 @@
|
||||||
module Quox.CharExtra
|
module Quox.Unicode
|
||||||
|
|
||||||
import Generics.Derive
|
import Generics.Derive
|
||||||
|
|
||||||
|
@ -133,3 +133,8 @@ isWhitespace : Char -> Bool
|
||||||
isWhitespace ch =
|
isWhitespace ch =
|
||||||
ch == '\t' || ch == '\r' || ch == '\n' ||
|
ch == '\t' || ch == '\r' || ch == '\n' ||
|
||||||
case genCat ch of Separator _ => True; _ => False
|
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 =
|
modules =
|
||||||
Quox.NatExtra,
|
Quox.NatExtra,
|
||||||
Quox.CharExtra,
|
Quox.Unicode,
|
||||||
Quox.OPE,
|
Quox.OPE,
|
||||||
Quox.Pretty,
|
Quox.Pretty,
|
||||||
Quox.Syntax,
|
Quox.Syntax,
|
||||||
|
|
|
@ -2,7 +2,7 @@ module Tests
|
||||||
|
|
||||||
import Options
|
import Options
|
||||||
import TAP
|
import TAP
|
||||||
import Tests.CharExtra
|
import Tests.Unicode
|
||||||
import Tests.Lexer
|
import Tests.Lexer
|
||||||
import Tests.Parser
|
import Tests.Parser
|
||||||
import Tests.Equal
|
import Tests.Equal
|
||||||
|
@ -10,7 +10,7 @@ import System
|
||||||
|
|
||||||
|
|
||||||
allTests = [
|
allTests = [
|
||||||
CharExtra.tests,
|
Unicode.tests,
|
||||||
Lexer.tests,
|
Lexer.tests,
|
||||||
Parser.tests,
|
Parser.tests,
|
||||||
Equal.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