From 54ba4e237f47396084b0783525de909dfa5a08a4 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 15 Mar 2023 15:53:39 +0100 Subject: [PATCH] use snoclists in pretty printing i think the names were in the wrong sometimes!!! --- lib/Quox/Pretty.idr | 13 +++++++------ lib/Quox/Syntax/Subst.idr | 2 +- lib/Quox/Syntax/Term/Pretty.idr | 12 ++++++------ lib/Quox/Syntax/Var.idr | 19 ++++++++++++------- 4 files changed, 26 insertions(+), 20 deletions(-) diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr index d6e23a5..9deb2d4 100644 --- a/lib/Quox/Pretty.idr +++ b/lib/Quox/Pretty.idr @@ -7,6 +7,7 @@ import Text.PrettyPrint.Prettyprinter.Render.String import Text.PrettyPrint.Prettyprinter.Render.Terminal import public Data.String import Data.DPair +import Data.SnocList import public Control.Monad.Identity import public Control.Monad.Reader @@ -127,9 +128,9 @@ public export record PrettyEnv where constructor MakePrettyEnv ||| names of bound dimension variables - dnames : List Name + dnames : SnocList BaseName ||| names of bound term variables - tnames : List Name + tnames : SnocList BaseName ||| use non-ascii characters for syntax unicode : Bool ||| surrounding precedence level @@ -154,13 +155,13 @@ withPrec d = local {prec := d} public export data BinderSort = T | D export %inline -unders : HasEnv m => BinderSort -> List BaseName -> m a -> m a -unders T xs = local {prec := Outer, tnames $= (map unq xs ++)} -unders D xs = local {prec := Outer, dnames $= (map unq xs ++)} +unders : HasEnv m => BinderSort -> SnocList BaseName -> m a -> m a +unders T xs = local {prec := Outer, tnames $= (++ xs)} +unders D xs = local {prec := Outer, dnames $= (++ xs)} export %inline under : HasEnv m => BinderSort -> BaseName -> m a -> m a -under t x = unders t [x] +under t x = unders t [< x] public export diff --git a/lib/Quox/Syntax/Subst.idr b/lib/Quox/Syntax/Subst.idr index 6e6ecd4..157698f 100644 --- a/lib/Quox/Syntax/Subst.idr +++ b/lib/Quox/Syntax/Subst.idr @@ -121,7 +121,7 @@ one x = fromVect [x] export prettySubstM : Pretty.HasEnv m => (pr : f to -> m (Doc HL)) -> - (names : List Name) -> (bnd : HL) -> (op, cl : Doc HL) -> + (names : SnocList BaseName) -> (bnd : HL) -> (op, cl : Doc HL) -> Subst f from to -> m (Doc HL) prettySubstM pr names bnd op cl th = encloseSep (hl Delim op) (hl Delim cl) (hl Delim "; ") <$> diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index a6f5984..bcc4f69 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -55,7 +55,7 @@ prettyBindType qtys x s arr t = do export prettyArm : PrettyHL a => Pretty.HasEnv m => - BinderSort -> List BaseName -> Doc HL -> a -> m (Doc HL) + BinderSort -> SnocList BaseName -> Doc HL -> a -> m (Doc HL) prettyArm sort xs pat body = do body <- withPrec Outer $ unders sort xs $ prettyM body pure $ hang 2 $ sep [pat <++> !darrowD, body] @@ -67,7 +67,7 @@ prettyLams lam sort names body = do let var = case sort of T => TVar; D => DVar header <- sequence $ [hlF var $ prettyM x | x <- names] let header = sep $ maybe header (:: header) lam - parensIfM Outer =<< prettyArm sort names header body + parensIfM Outer =<< prettyArm sort (cast names) header body export prettyApps : PrettyHL f => PrettyHL a => Pretty.HasEnv m => @@ -88,14 +88,14 @@ prettyTuple = map (parens . align . separate commaD) . traverse prettyM export prettyArms : PrettyHL a => Pretty.HasEnv m => - List (List BaseName, Doc HL, a) -> m (Doc HL) + List (SnocList BaseName, Doc HL, a) -> m (Doc HL) prettyArms = map (braces . asep) . traverse (\(xs, l, r) => prettyArm T xs l r) export prettyCase : PrettyHL a => PrettyHL b => PrettyHL c => PrettyHL q => Pretty.HasEnv m => - q -> a -> BaseName -> b -> List (List BaseName, Doc HL, c) -> + q -> a -> BaseName -> b -> List (SnocList BaseName, Doc HL, c) -> m (Doc HL) prettyCase pi elim r ret arms = do elim <- prettyQtyBinds [pi] elim @@ -170,10 +170,10 @@ parameters (showSubsts : Bool) prettyApps Nothing fun args prettyM (CasePair pi p (S [r] ret) (S [x, y] body)) = do pat <- parens . separate commaD <$> traverse (hlF TVar . prettyM) [x, y] - prettyCase pi p r ret.term [([x, y], pat, body.term)] + prettyCase pi p r ret.term [([< x, y], pat, body.term)] prettyM (CaseEnum pi t (S [r] ret) arms) = prettyCase pi t r ret.term - [([], prettyTag t, b) | (t, b) <- SortedMap.toList arms] + [([<], prettyTag t, b) | (t, b) <- SortedMap.toList arms] prettyM (e :% d) = let GotDArgs {fun, args, _} = getDArgs' e [d] in prettyApps (Just "@") fun args diff --git a/lib/Quox/Syntax/Var.idr b/lib/Quox/Syntax/Var.idr index 3102898..3852fc3 100644 --- a/lib/Quox/Syntax/Var.idr +++ b/lib/Quox/Syntax/Var.idr @@ -41,6 +41,12 @@ export Uninhabited (VZ = VS i) where uninhabited _ impossible export Uninhabited (VS i = VZ) where uninhabited _ impossible +private +lookupS : Nat -> SnocList a -> Maybe a +lookupS _ [<] = Nothing +lookupS Z (sx :< x) = Just x +lookupS (S i) (sx :< x) = lookupS i sx + parameters {auto _ : Pretty.HasEnv m} private prettyIndex : Nat -> m (Doc a) @@ -58,17 +64,16 @@ parameters {auto _ : Pretty.HasEnv m} ||| highlighted as `hlok`. Otherwise it is just printed as a number highlighted ||| as `hlerr`. export - prettyVar' : HL -> HL -> List Name -> Nat -> m (Doc HL) + prettyVar' : HL -> HL -> SnocList BaseName -> Nat -> m (Doc HL) prettyVar' hlok hlerr names i = - case inBounds i names of - Yes _ => hlF' hlok [|prettyM (index i names) <+> prettyIndex i|] - No _ => pure $ hl hlerr $ "#" <+> pretty i + case lookupS i names of + Just x => hlF' hlok $ prettyM x + Nothing => pure $ hl hlerr $ "#" <+> pretty i - export %inline - prettyVar : HL -> HL -> List Name -> Var n -> m (Doc HL) + export + prettyVar : HL -> HL -> SnocList BaseName -> Var n -> m (Doc HL) prettyVar hlok hlerr names i = prettyVar' hlok hlerr names i.nat - public export fromNatWith : (i : Nat) -> (0 p : i `LT` n) -> Var n fromNatWith Z (LTESucc _) = VZ