From 52e54dcc3c9e7a42da4c35ff7cbfe6ddb8c3e662 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Fri, 20 Oct 2023 04:53:20 +0200 Subject: [PATCH] add PrettyVal stuff for parser AST --- exe/quox.ipkg | 2 +- lib/Quox/Loc.idr | 17 +++++++++++++++-- lib/Quox/Name.idr | 7 ++++--- lib/Quox/Parser/Syntax.idr | 20 +++++++++++--------- lib/Quox/PrettyValExtra.idr | 10 ++++++++++ lib/Quox/Syntax/Dim.idr | 3 ++- lib/Quox/Syntax/Qty.idr | 7 ++++--- lib/quox-lib.ipkg | 5 ++++- 8 files changed, 51 insertions(+), 20 deletions(-) create mode 100644 lib/Quox/PrettyValExtra.idr diff --git a/exe/quox.ipkg b/exe/quox.ipkg index e20197a..fed30f4 100644 --- a/exe/quox.ipkg +++ b/exe/quox.ipkg @@ -1,7 +1,7 @@ package quox version = 0 -depends = base, contrib, elab-util, sop, quox-lib +depends = base, contrib, elab-util, pretty-show, quox-lib executable = quox main = Main diff --git a/lib/Quox/Loc.idr b/lib/Quox/Loc.idr index cd63e2f..5776ec9 100644 --- a/lib/Quox/Loc.idr +++ b/lib/Quox/Loc.idr @@ -1,6 +1,7 @@ ||| file locations module Quox.Loc +import Quox.PrettyValExtra import public Text.Bounded import Data.SortedMap import Derive.Prelude @@ -12,12 +13,12 @@ public export FileName : Type FileName = String -%runElab derive "Bounds" [Ord] +%runElab derive "Bounds" [Ord, PrettyVal] public export data Loc_ = NoLoc | YesLoc FileName Bounds %name Loc_ loc -%runElab derive "Loc_" [Eq, Ord, Show] +%runElab derive "Loc_" [Eq, Ord, Show, PrettyVal] ||| a wrapper for locations which are always considered equal @@ -39,6 +40,18 @@ public export %inline makeLoc : FileName -> Bounds -> Loc makeLoc = L .: YesLoc +public export %inline +loc : FileName -> (sl, sc, el, ec : Int) -> Loc +loc file sl sc el ec = makeLoc file $ MkBounds sl sc el ec + +export +PrettyVal Loc where + prettyVal (L NoLoc) = Con "noLoc" [] + prettyVal (L (YesLoc file (MkBounds sl sc el ec))) = + Con "loc" [prettyVal file, + prettyVal sl, prettyVal sc, + prettyVal el, prettyVal ec] + export onlyStart_ : Loc_ -> Loc_ diff --git a/lib/Quox/Name.idr b/lib/Quox/Name.idr index ce34c29..6c81091 100644 --- a/lib/Quox/Name.idr +++ b/lib/Quox/Name.idr @@ -2,6 +2,7 @@ module Quox.Name import Quox.Loc import Quox.CharExtra +import Quox.PrettyValExtra import public Data.SnocList import Data.List import Control.Eff @@ -23,7 +24,7 @@ data BaseName = UN String -- user-given name | MN String NameSuf -- machine-generated name | Unused -- "_" -%runElab derive "BaseName" [Eq, Ord] +%runElab derive "BaseName" [Eq, Ord, PrettyVal] export baseStr : BaseName -> String @@ -66,7 +67,7 @@ record PName where constructor MakePName mods : Mods base : PBaseName -%runElab derive "PName" [Eq, Ord] +%runElab derive "PName" [Eq, Ord, PrettyVal] export %inline fromPName : PName -> Name @@ -97,7 +98,7 @@ record BindName where constructor BN val : BaseName loc_ : Loc -%runElab derive "BindName" [Eq, Ord, Show] +%runElab derive "BindName" [Eq, Ord, Show, PrettyVal] export Located BindName where n.loc = n.loc_ export Relocatable BindName where setLoc loc (BN x _) = BN x loc diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr index af92211..f2f6180 100644 --- a/lib/Quox/Parser/Syntax.idr +++ b/lib/Quox/Parser/Syntax.idr @@ -3,6 +3,7 @@ module Quox.Parser.Syntax import public Quox.Loc import public Quox.Syntax import public Quox.Definition +import Quox.PrettyValExtra import Derive.Prelude %hide TT.Name @@ -14,7 +15,7 @@ import Derive.Prelude public export data PatVar = Unused Loc | PV PBaseName Loc %name PatVar v -%runElab derive "PatVar" [Eq, Ord, Show] +%runElab derive "PatVar" [Eq, Ord, Show, PrettyVal] export Located PatVar where @@ -38,7 +39,7 @@ record PQty where val : Qty loc_ : Loc %name PQty qty -%runElab derive "PQty" [Eq, Ord, Show] +%runElab derive "PQty" [Eq, Ord, Show, PrettyVal] export Located PQty where q.loc = q.loc_ @@ -46,7 +47,7 @@ namespace PDim public export data PDim = K DimConst Loc | V PBaseName Loc %name PDim p, q - %runElab derive "PDim" [Eq, Ord, Show] + %runElab derive "PDim" [Eq, Ord, Show, PrettyVal] export Located PDim where @@ -56,7 +57,7 @@ Located PDim where public export data PTagVal = PT TagVal Loc %name PTagVal tag -%runElab derive "PTagVal" [Eq, Ord, Show] +%runElab derive "PTagVal" [Eq, Ord, Show, PrettyVal] namespace PTerm @@ -104,7 +105,7 @@ namespace PTerm | CaseBox PatVar PTerm Loc %name PCaseBody body -%runElab deriveMutual ["PTerm", "PCaseBody"] [Eq, Ord, Show] +%runElab deriveMutual ["PTerm", "PCaseBody"] [Eq, Ord, Show, PrettyVal] export Located PTerm where @@ -149,7 +150,7 @@ record PDefinition where term : PTerm loc_ : Loc %name PDefinition def -%runElab derive "PDefinition" [Eq, Ord, Show] +%runElab derive "PDefinition" [Eq, Ord, Show, PrettyVal] export Located PDefinition where def.loc = def.loc_ @@ -157,7 +158,7 @@ public export data PDeclMod = PFail (Maybe String) Loc %name PDeclMod mod -%runElab derive "PDeclMod" [Eq, Ord, Show] +%runElab derive "PDeclMod" [Eq, Ord, Show, PrettyVal] mutual public export @@ -180,7 +181,8 @@ mutual PDef PDefinition | PNs PNamespace %name PDeclBody decl -%runElab deriveMutual ["PNamespace", "PDecl", "PDeclBody"] [Eq, Ord, Show] +%runElab deriveMutual ["PNamespace", "PDecl", "PDeclBody"] + [Eq, Ord, Show, PrettyVal] export Located PNamespace where ns.loc = ns.loc_ @@ -194,7 +196,7 @@ Located PDeclBody where public export data PTopLevel = PD PDecl | PLoad String Loc %name PTopLevel t -%runElab derive "PTopLevel" [Eq, Ord, Show] +%runElab derive "PTopLevel" [Eq, Ord, Show, PrettyVal] export Located PTopLevel where diff --git a/lib/Quox/PrettyValExtra.idr b/lib/Quox/PrettyValExtra.idr new file mode 100644 index 0000000..afd210e --- /dev/null +++ b/lib/Quox/PrettyValExtra.idr @@ -0,0 +1,10 @@ +module Quox.PrettyValExtra + +import Derive.Prelude +import public Text.Show.Value +import public Text.Show.PrettyVal +import public Text.Show.PrettyVal.Derive + +%language ElabReflection + +%runElab derive "SnocList" [PrettyVal] diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr index 2229b6d..5f60a17 100644 --- a/lib/Quox/Syntax/Dim.idr +++ b/lib/Quox/Syntax/Dim.idr @@ -6,6 +6,7 @@ import Quox.Var import Quox.Syntax.Subst import Quox.Pretty import Quox.Context +import Quox.PrettyValExtra import Decidable.Equality import Control.Function @@ -18,7 +19,7 @@ import Derive.Prelude public export data DimConst = Zero | One %name DimConst e -%runElab derive "DimConst" [Eq, Ord, Show] +%runElab derive "DimConst" [Eq, Ord, Show, PrettyVal] ||| `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.idr b/lib/Quox/Syntax/Qty.idr index 5133eff..d0d3d79 100644 --- a/lib/Quox/Syntax/Qty.idr +++ b/lib/Quox/Syntax/Qty.idr @@ -6,6 +6,7 @@ module Quox.Syntax.Qty import Quox.Pretty import Quox.Decidable +import Quox.PrettyValExtra import Data.DPair import Derive.Prelude @@ -20,7 +21,7 @@ import Derive.Prelude ||| - ω (or #): don't care. an ω variable *can* also be used 0/1 time public export data Qty = Zero | One | Any -%runElab derive "Qty" [Eq, Ord, Show] +%runElab derive "Qty" [Eq, Ord, Show, PrettyVal] %name Qty.Qty pi, rh @@ -79,7 +80,7 @@ lub p q = if p == q then p else Any ||| for the subject of a typing judgment. see @qtt, §2.3 for more detail public export data SQty = SZero | SOne -%runElab derive "SQty" [Eq, Ord, Show] +%runElab derive "SQty" [Eq, Ord, Show, PrettyVal] %name Qty.SQty sg ||| "σ ⨴ π" @@ -96,7 +97,7 @@ subjMult sg _ = sg ||| at runtime at all or not public export data GQty = GZero | GAny -%runElab derive "GQty" [Eq, Ord, Show] +%runElab derive "GQty" [Eq, Ord, Show, PrettyVal] %name GQty rh public export diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg index de8d2f3..27063b1 100644 --- a/lib/quox-lib.ipkg +++ b/lib/quox-lib.ipkg @@ -5,7 +5,9 @@ authors = "rhiannon morris" sourceloc = "https://git.rhiannon.website/rhi/quox" license = "acsl" -depends = base, contrib, elab-util, sop, snocvect, eff, prettier +depends = + base, contrib, elab-util, sop, snocvect, eff, prettier, + pretty-show, parser-show modules = Text.PrettyPrint.Bernardy.Core.Decorate, @@ -14,6 +16,7 @@ modules = Quox.CharExtra, Quox.NatExtra, Quox.EffExtra, + Quox.PrettyValExtra, Quox.Decidable, Quox.No, Quox.Loc,