From fca75377a07543690b318b30367113e45d588115 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 11 Apr 2024 22:08:07 +0200 Subject: [PATCH] =?UTF-8?q?MakeName=20=E2=87=92=20MkName=20for=20consisten?= =?UTF-8?q?cy?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- lib/Quox/Name.idr | 18 +++++++++--------- lib/Quox/Parser/FromParser.idr | 2 +- lib/Quox/Parser/Parser.idr | 6 +++--- lib/Quox/Untyped/Scheme.idr | 8 ++++---- tests/Tests/Lexer.idr | 10 +++++----- tests/Tests/Parser.idr | 8 ++++---- tests/Tests/PrettyTerm.idr | 4 ++-- 7 files changed, 28 insertions(+), 28 deletions(-) diff --git a/lib/Quox/Name.idr b/lib/Quox/Name.idr index 6c81091..8686e54 100644 --- a/lib/Quox/Name.idr +++ b/lib/Quox/Name.idr @@ -43,14 +43,14 @@ Mods = SnocList String public export record Name where - constructor MakeName + constructor MkName mods : Mods base : BaseName %runElab derive "Name" [Eq, Ord] public export %inline unq : BaseName -> Name -unq = MakeName [<] +unq = MkName [<] ||| add some namespaces to the beginning of a name public export %inline @@ -64,31 +64,31 @@ PBaseName = String public export record PName where - constructor MakePName + constructor MkPName mods : Mods base : PBaseName %runElab derive "PName" [Eq, Ord, PrettyVal] export %inline fromPName : PName -> Name -fromPName p = MakeName p.mods $ UN p.base +fromPName p = MkName p.mods $ UN p.base export %inline toPName : Name -> PName -toPName p = MakePName p.mods $ baseStr p.base +toPName p = MkPName p.mods $ baseStr p.base export %inline fromPBaseName : PBaseName -> Name -fromPBaseName = MakeName [<] . UN +fromPBaseName = MkName [<] . UN export Show PName where - show (MakePName mods base) = + show (MkPName mods base) = show $ concat $ intersperse "." $ toList $ mods :< base export Show Name where show = show . toPName -export FromString PName where fromString = MakePName [<] +export FromString PName where fromString = MkPName [<] export FromString Name where fromString = fromPBaseName @@ -116,7 +116,7 @@ export fromListP : List1 String -> PName fromListP (x ::: xs) = go [<] x xs where go : SnocList String -> String -> List String -> PName - go mods x [] = MakePName mods x + go mods x [] = MkPName mods x go mods x (y :: ys) = go (mods :< x) y ys export %inline diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr index 88017fd..08a7210 100644 --- a/lib/Quox/Parser/FromParser.idr +++ b/lib/Quox/Parser/FromParser.idr @@ -75,7 +75,7 @@ parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a) (xs : Context' PatVar n) private fromBaseName : PBaseName -> m a - fromBaseName x = maybe (f $ MakePName [<] x) b $ + fromBaseName x = maybe (f $ MkPName [<] x) b $ Context.find (\y => y.name == Just x) xs private diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr index b34599c..44b5833 100644 --- a/lib/Quox/Parser/Parser.idr +++ b/lib/Quox/Parser/Parser.idr @@ -124,7 +124,7 @@ qname = terminalMatch "name" `(Name n) `(n) ||| unqualified name export baseName : Grammar True PBaseName -baseName = terminalMatch "unqualified name" `(Name (MakePName [<] b)) `(b) +baseName = terminalMatch "unqualified name" `(Name (MkPName [<] b)) `(b) ||| dimension constant (0 or 1) export @@ -152,8 +152,8 @@ qty fname = withLoc fname [|PQ qtyVal|] export exactName : String -> Grammar True () exactName name = terminal "expected '\{name}'" $ \case - Name (MakePName [<] x) => guard $ x == name - _ => Nothing + Name (MkPName [<] x) => guard $ x == name + _ => Nothing ||| pattern var (unqualified name or _) diff --git a/lib/Quox/Untyped/Scheme.idr b/lib/Quox/Untyped/Scheme.idr index c5a528d..b193598 100644 --- a/lib/Quox/Untyped/Scheme.idr +++ b/lib/Quox/Untyped/Scheme.idr @@ -113,13 +113,13 @@ makeIdBase mods str = joinBy "." $ toList $ mods :< str export makeId : Name -> Id -makeId (MakeName mods (UN str)) = I (makeIdBase mods str) 0 -makeId (MakeName mods (MN str k)) = I (makeIdBase mods str) 0 -makeId (MakeName mods Unused) = I (makeIdBase mods "_") 0 +makeId (MkName mods (UN str)) = I (makeIdBase mods str) 0 +makeId (MkName mods (MN str k)) = I (makeIdBase mods str) 0 +makeId (MkName mods Unused) = I (makeIdBase mods "_") 0 export makeIdB : BindName -> Id -makeIdB (BN name _) = makeId $ MakeName [<] name +makeIdB (BN name _) = makeId $ MkName [<] name private bump : Id -> Id diff --git a/tests/Tests/Lexer.idr b/tests/Tests/Lexer.idr index 549de46..40fd9a8 100644 --- a/tests/Tests/Lexer.idr +++ b/tests/Tests/Lexer.idr @@ -71,7 +71,7 @@ tests = "lexer" :- [ lexes "δελτα" [Name "δελτα"], lexes "★★" [Name "★★"], lexes "Types" [Name "Types"], - lexes "a.b.c.d.e" [Name $ MakePName [< "a","b","c","d"] "e"], + lexes "a.b.c.d.e" [Name $ MkPName [< "a","b","c","d"] "e"], lexes "normalïse" [Name "normalïse"], -- ↑ replace i + combining ¨ with precomposed ï lexes "map#" [Name "map#"], @@ -90,16 +90,16 @@ tests = "lexer" :- [ lexes "***" [Name "***"], lexes "+**" [Name "+**"], lexes "+#" [Name "+#"], - lexes "+.+.+" [Name $ MakePName [< "+", "+"] "+"], - lexes "a.+" [Name $ MakePName [< "a"] "+"], - lexes "+.a" [Name $ MakePName [< "+"] "a"], + lexes "+.+.+" [Name $ MkPName [< "+", "+"] "+"], + lexes "a.+" [Name $ MkPName [< "a"] "+"], + lexes "+.a" [Name $ MkPName [< "+"] "a"], lexes "+a" [Name "+", Name "a"], lexes "x." [Name "x", Reserved "."], lexes "&." [Name "&", Reserved "."], lexes ".x" [Reserved ".", Name "x"], - lexes "a.b.c." [Name $ MakePName [< "a", "b"] "c", Reserved "."], + lexes "a.b.c." [Name $ MkPName [< "a", "b"] "c", Reserved "."], lexes "case" [Reserved "case"], lexes "caseω" [Reserved "caseω"], diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr index 4c0dc0f..e4f6d88 100644 --- a/tests/Tests/Parser.idr +++ b/tests/Tests/Parser.idr @@ -63,9 +63,9 @@ tests = "parser" :- [ "names" :- [ parsesAs (const qname) "x" - (MakePName [<] "x"), + (MkPName [<] "x"), parsesAs (const qname) "Data.List.length" - (MakePName [< "Data", "List"] "length"), + (MkPName [< "Data", "List"] "length"), parseFails (const qname) "_" ], @@ -124,7 +124,7 @@ tests = "parser" :- [ parseMatch term "f" `(V "f" {}), parseMatch term "f.x.y" - `(V (MakePName [< "f", "x"] "y") {}), + `(V (MkPName [< "f", "x"] "y") {}), parseMatch term "f x" `(App (V "f" {}) (V "x" {}) _), parseMatch term "f x y" @@ -526,7 +526,7 @@ tests = "parser" :- [ PSucceed False Nothing _] PSucceed _), PD (PDef $ MkPDef (PQ Any _) "y" - (PConcrete Nothing (V (MakePName [< "a"] "x") Nothing _)) + (PConcrete Nothing (V (MkPName [< "a"] "x") Nothing _)) PSucceed False Nothing _)]), parseMatch input #" load "a.quox"; def b = a.b "# `([PLoad "a.quox" _, diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr index 7856e12..b15cadc 100644 --- a/tests/Tests/PrettyTerm.idr +++ b/tests/Tests/PrettyTerm.idr @@ -37,8 +37,8 @@ tests = "pretty printing terms" :- [ "free vars" :- [ testPrettyE1 [<] [<] (^F "x" 0) "x", testPrettyE [<] [<] (^F "x" 1) "x¹" "x^1", - testPrettyE1 [<] [<] (^F (MakeName [< "A", "B", "C"] "x") 0) "A.B.C.x", - testPrettyE [<] [<] (^F (MakeName [< "A", "B", "C"] "x") 2) + testPrettyE1 [<] [<] (^F (MkName [< "A", "B", "C"] "x") 0) "A.B.C.x", + testPrettyE [<] [<] (^F (MkName [< "A", "B", "C"] "x") 2) "A.B.C.x²" "A.B.C.x^2" ],