replace Pretty.M with a MonadReader constraint

src/Quox/Pretty.idr

@@ -109,26 +109,25 @@ record PrettyEnv where
   ||| surrounding precedence level
   prec    : PPrec
 
-public export
-0 M : Type -> Type
-M = Reader PrettyEnv
+public export %inline 0 HasEnv : (Type -> Type) -> Type
+HasEnv = MonadReader PrettyEnv
 
 export
-ifUnicode : (uni, asc : Lazy a) -> M a
+ifUnicode : HasEnv m => (uni, asc : Lazy a) -> m a
 ifUnicode uni asc = if unicode !ask then [|uni|] else [|asc|]
 
 export
-parensIfM : PPrec -> Doc HL -> M (Doc HL)
+parensIfM : HasEnv m => PPrec -> Doc HL -> m (Doc HL)
 parensIfM d doc = pure $ parensIf (prec !ask > d) doc
 
 export
-withPrec : PPrec -> M a -> M a
+withPrec : HasEnv m => PPrec -> m a -> m a
 withPrec d = local {prec := d}
 
 public export data BinderSort = T | D
 
 export
-under : BinderSort -> Name -> M a -> M a
+under : HasEnv m => BinderSort -> Name -> m a -> m a
 under s x = local $
   {prec := Outer} .
   (case s of T => {tnames $= (x ::)}; D => {dnames $= (x ::)})
@@ -136,10 +135,10 @@ under s x = local $
 
 public export
 interface PrettyHL a where
-  prettyM : a -> M (Doc HL)
+  prettyM : HasEnv m => a -> m (Doc HL)
 
 public export %inline
-pretty0M : PrettyHL a => a -> M (Doc HL)
+pretty0M : (PrettyHL a, HasEnv m) => a -> m (Doc HL)
 pretty0M = local {prec := Outer} . prettyM
 
 public export %inline

src/Quox/Syntax/Dim.idr

@@ -35,7 +35,7 @@ DSubst = Subst Dim
 
 
 export %inline
-prettyDSubst : DSubst from to -> Pretty.M (Doc HL)
+prettyDSubst : Pretty.HasEnv m => DSubst from to -> m (Doc HL)
 prettyDSubst th =
   prettySubstM prettyM (dnames !ask) DVar
     !(ifUnicode "⟨" "<") !(ifUnicode "⟩" ">") th

src/Quox/Syntax/Qty.idr

@@ -28,7 +28,7 @@ PrettyHL Qty where
       Many => ifUnicode "𝛚" "*"
 
 export %inline
-prettyQtyBinds : List Qty -> M (Doc HL)
+prettyQtyBinds : Pretty.HasEnv m => List Qty -> m (Doc HL)
 prettyQtyBinds =
   map (align . sep) .
   traverse (\pi => [|pretty0M pi <++> pure (hl Delim "|")|])

src/Quox/Syntax/Shift.idr

@@ -164,7 +164,7 @@ compViaNatCorrect by (SS bz) =
 ||| * `unicode : Bool` is whether to use unicode characters in the output
 ||| * `prec : PPrec` is the surrounding precedence level
 export
-prettyShift : (bnd : HL) -> Shift from to -> Pretty.M (Doc HL)
+prettyShift : Pretty.HasEnv m => (bnd : HL) -> Shift from to -> m (Doc HL)
 prettyShift bnd by =
   parensIfM Outer $ hsep $
     [hl bnd   !(ifUnicode "𝑖"  "i"), hl Delim !(ifUnicode "≔" ":="),

src/Quox/Syntax/Subst.idr

@@ -96,21 +96,21 @@ push th = fromVar VZ ::: (th . shift 1)
 ||| * `unicode : Bool` is whether to use unicode characters in the output
 |||   (also passed into `pr`)
 export
-prettySubstM : (pr : f to -> Pretty.M (Doc HL)) ->
-               (names : List Name) ->
-               (bnd : HL) -> (op, cl : Doc HL) ->
-               Subst f from to -> Pretty.M (Doc HL)
+prettySubstM : Pretty.HasEnv m =>
+               (pr : f to -> m (Doc HL)) ->
+               (names : List Name) -> (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 "; ") <$>
     withPrec Outer (go 0 th)
  where
-  go1 : Nat -> f to -> Pretty.M (Doc HL)
+  go1 : Nat -> f to -> m (Doc HL)
   go1 i t = pure $ hang 2 $ sep
     [hsep [!(prettyVar' bnd bnd names i),
            hl Delim !(ifUnicode "≔" ":=")],
      !(pr t)]
 
-  go : forall from. Nat -> Subst f from to -> Pretty.M (List (Doc HL))
+  go : forall from. Nat -> Subst f from to -> m (List (Doc HL))
   go _ (Shift SZ) = pure []
   go _ (Shift by) = [|pure (prettyShift bnd by)|]
   go i (t ::: th) = [|go1 i t :: go (S i) th|]

src/Quox/Syntax/Term.idr

@@ -106,18 +106,19 @@ getArgs : Elim d n -> (Elim d n, List (Term d n))
 getArgs e = getArgs' e []
 
 
+parameters {auto _ : Pretty.HasEnv m}
+  private %inline arrowD : m (Doc HL)
+  arrowD = hlF Syntax $ ifUnicode "→" "->"
+
+  private %inline lamD : m (Doc HL)
+  lamD = hlF Syntax $ ifUnicode "λ" "fun"
+
+  private %inline annD : m (Doc HL)
+  annD = hlF Syntax $ ifUnicode "⦂" "::"
+
 private %inline typeD : Doc HL
 typeD = hl Syntax "Type"
 
-private %inline arrowD : Pretty.M (Doc HL)
-arrowD = hlF Syntax $ ifUnicode "→" "->"
-
-private %inline lamD : Pretty.M (Doc HL)
-lamD = hlF Syntax $ ifUnicode "λ" "fun"
-
-private %inline annD : Pretty.M (Doc HL)
-annD = hlF Syntax $ ifUnicode "⦂" "::"
-
 private %inline colonD : Doc HL
 colonD = hl Syntax ":"
 
@@ -165,11 +166,11 @@ mutual
         [|withPrec SApp (prettyM e) </> prettyDSubst th|]
 
   export covering
-  prettyTSubst : TSubst d from to -> Pretty.M (Doc HL)
+  prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
   prettyTSubst s = prettySubstM prettyM (tnames !ask) TVar "[" "]" s
 
   export covering
-  prettyBinder : List Qty -> Name -> Term d n -> Pretty.M (Doc HL)
+  prettyBinder : Pretty.HasEnv m => List Qty -> Name -> Term d n -> m (Doc HL)
   prettyBinder pis x a =
     pure $ parens $ hang 2 $
       !(prettyQtyBinds pis) <//>

src/Quox/Syntax/Var.idr

@@ -30,31 +30,32 @@ export Ord  (Var n) where compare i j = compare i.nat j.nat
 export Show (Var n) where showPrec d i = showCon d "V" $ showArg i.nat
 
 
-private
-prettyIndex : Nat -> Pretty.M (Doc a)
-prettyIndex i =
-  ifUnicode (pretty $ pack $ map sup $ unpack $ show i) (":" <+> pretty i)
- where
-  sup : Char -> Char
-  sup c = case c of
-    '0' => '⁰'; '1' => '¹'; '2' => '²'; '3' => '³'; '4' => '⁴'
-    '5' => '⁵'; '6' => '⁶'; '7' => '⁷'; '8' => '⁸'; '9' => '⁹'; _ => c
+parameters {auto _ : Pretty.HasEnv m}
+  private
+  prettyIndex : Nat -> m (Doc a)
+  prettyIndex i =
+    ifUnicode (pretty $ pack $ map sup $ unpack $ show i) (":" <+> pretty i)
+   where
+    sup : Char -> Char
+    sup c = case c of
+      '0' => '⁰'; '1' => '¹'; '2' => '²'; '3' => '³'; '4' => '⁴'
+      '5' => '⁵'; '6' => '⁶'; '7' => '⁷'; '8' => '⁸'; '9' => '⁹'; _ => c
 
-||| `prettyVar hlok hlerr names i` pretty prints the de Bruijn index `i`.
-|||
-||| If it is within the bounds of `names`, then it uses the name at that index,
-||| highlighted as `hlok`. Otherwise it is just printed as a number highlighted
-||| as `hlerr`.
-export
-prettyVar' : HL -> HL -> List Name -> Nat -> Pretty.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
+  ||| `prettyVar hlok hlerr names i` pretty prints the de Bruijn index `i`.
+  |||
+  ||| If it is within the bounds of `names`, then it uses the name at that index,
+  ||| 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' hlok hlerr names i =
+    case inBounds i names of
+         Yes _ => hlF' hlok [|prettyM (index i names) <+> prettyIndex i|]
+         No  _ => pure $ hl hlerr $ pretty i
 
-export %inline
-prettyVar : HL -> HL -> List Name -> Var n -> Pretty.M (Doc HL)
-prettyVar hlok hlerr names i = prettyVar' hlok hlerr names i.nat
+  export %inline
+  prettyVar : HL -> HL -> List Name -> Var n -> m (Doc HL)
+  prettyVar hlok hlerr names i = prettyVar' hlok hlerr names i.nat
 
 
 public export