From a221380d61bc08a23f10796be32275579f8dc13c Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 25 Aug 2023 18:09:06 +0200
Subject: [PATCH] more effect stuff, incl. ST

---
 lib/Quox/EffExtra.idr                |  95 ++++++++++-------
 lib/Quox/Equal.idr                   |  29 +-----
 lib/Quox/Name.idr                    |   8 --
 lib/Quox/Parser/FromParser.idr       | 146 ++++++++++++---------------
 lib/Quox/Parser/FromParser/Error.idr |   7 +-
 lib/Quox/Parser/LoadFile.idr         |  98 ++++++++++++++++++
 lib/Quox/Pretty.idr                  |  61 ++++++-----
 lib/Quox/ST.idr                      | 106 +++++++++++++++++++
 lib/Quox/Syntax/Term/Base.idr        |   5 +
 lib/Quox/Typechecker.idr             |   8 --
 lib/Quox/Whnf/Interface.idr          |   8 --
 lib/quox-lib.ipkg                    |   2 +
 tests/Tests/Equal.idr                |   2 +
 tests/Tests/FromPTerm.idr            |   2 +-
 tests/Tests/Reduce.idr               |   5 +
 tests/Tests/Typechecker.idr          |   1 +
 tests/TypingImpls.idr                |  16 +++
 17 files changed, 395 insertions(+), 204 deletions(-)
 create mode 100644 lib/Quox/Parser/LoadFile.idr
 create mode 100644 lib/Quox/ST.idr

diff --git a/lib/Quox/EffExtra.idr b/lib/Quox/EffExtra.idr
index e80a922..a40dbd1 100644
--- a/lib/Quox/EffExtra.idr
+++ b/lib/Quox/EffExtra.idr
@@ -2,6 +2,7 @@ module Quox.EffExtra
 
 import public Control.Eff
 
+import Quox.ST
 import Data.IORef
 
 
@@ -27,40 +28,14 @@ local_ = localAt_ ()
 
 
 export
-hasDrop : (0 neq : Not (a = b)) ->
-          (ha : Has a fs) => (hb : Has b fs) =>
-          Has a (drop fs hb)
-hasDrop neq {ha = Z}    {hb = Z}    = void $ neq Refl
-hasDrop neq {ha = S ha} {hb = Z}    = ha
-hasDrop neq {ha = Z}    {hb = S hb} = Z
-hasDrop neq {ha = S ha} {hb = S hb} = S $ hasDrop neq {ha, hb}
-
-private
-0 ioNotState : Not (IO = StateL _ _)
-ioNotState Refl impossible
+handleStateIORef : HasIO m => IORef st -> StateL lbl st a -> m a
+handleStateIORef r Get     = readIORef r
+handleStateIORef r (Put s) = writeIORef r s
 
 export
-runStateIORefAt : (0 lbl : tag) -> (Has IO fs, Has (StateL lbl s) fs) =>
-                  IORef s -> Eff fs a -> Eff (fs - StateL lbl s) a
-runStateIORefAt lbl ref act = do
-  let hh : Has IO (fs - StateL lbl s) := hasDrop ioNotState
-  (val, st) <- runStateAt lbl !(readIORef ref) act
-  writeIORef ref st $> val
-
-export %inline
-runStateIORef : (Has IO fs, Has (State s) fs) =>
-                IORef s -> Eff fs a -> Eff (fs - State s) a
-runStateIORef = runStateIORefAt ()
-
-
-export %inline
-evalStateAt : (0 lbl : tag) -> Has (StateL lbl s) fs =>
-              s -> Eff fs a -> Eff (fs - StateL lbl s) a
-evalStateAt lbl s act = map fst $ runStateAt lbl s act
-
-export %inline
-evalState : Has (State s) fs => s -> Eff fs a -> Eff (fs - State s) a
-evalState = evalStateAt ()
+handleStateSTRef : HasST m => STRef s st -> StateL lbl st a -> m s a
+handleStateSTRef r Get     = readRef r
+handleStateSTRef r (Put s) = writeRef r s
 
 
 
@@ -86,17 +61,61 @@ subsetTail = subsetWith S
 
 -- [fixme] allow the error to be anywhere in the effect list
 export
-wrapErrAt : Length fs => (0 lbl : tag) -> (e -> e) ->
-            Eff (ExceptL lbl e :: fs) a -> Eff (ExceptL lbl e :: fs) a
+wrapErrAt : Length fs => (0 lbl : tag) -> (e -> e') ->
+            Eff (ExceptL lbl e :: fs) a -> Eff (ExceptL lbl e' :: fs) a
 wrapErrAt lbl f act =
   rethrowAt lbl . mapFst f =<< lift @{subsetTail} (runExceptAt lbl act)
 
 export %inline
-wrapErr : Length fs => (e -> e) ->
-          Eff (Except e :: fs) a -> Eff (Except e :: fs) a
+wrapErr : Length fs => (e -> e') ->
+          Eff (Except e :: fs) a -> Eff (Except e' :: fs) a
 wrapErr = wrapErrAt ()
 
 
+export
+handleExcept : Functor m => (forall c. e -> m c) -> ExceptL lbl e a -> m a
+handleExcept thr (Err e) = thr e
+
+
+export
+handleReaderConst : Applicative m => r -> ReaderL lbl r a -> m a
+handleReaderConst x Ask = pure x
+
+
+public export
+record IOErr e a where
+  constructor IOE
+  fromIOErr : IO (Either e a)
+
+export
+Functor (IOErr e) where
+  map f (IOE e) = IOE $ map f <$> e
+
+export
+Applicative (IOErr e) where
+  pure x = IOE $ pure $ pure x
+  IOE f <*> IOE x = IOE [|f <*> x|]
+
+export
+Monad (IOErr e) where
+  IOE m >>= k = IOE $ do
+    case !m of
+      Left  err => pure $ Left err
+      Right x   => fromIOErr $ k x
+
+export
+MonadRec (IOErr e) where
+  tailRecM s (Access r) x k = IOE $ do
+    let IOE m = k s x
+    case !m of
+      Left  err           => pure $ Left err
+      Right (Cont s' p y) => fromIOErr $ tailRecM s' (r s' p) y k
+      Right (Done y)      => pure $ Right y
+
+export
+HasIO (IOErr e) where
+  liftIO = IOE . map Right
+
 export %inline
-runIO : (MonadRec io, HasIO io) => Eff [IO] a -> io a
-runIO act = runEff act [liftIO]
+ioLeft : e -> IOErr e a
+ioLeft = IOE . pure . Left
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 7010c23..9fe713e 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -20,33 +20,6 @@ public export
 EqualInner : List (Type -> Type)
 EqualInner = [ErrorEff, NameGen, EqModeState]
 
-export
-runEqualWith_ : EqMode -> NameSuf ->
-                Eff EqualInner a -> (Either Error a, NameSuf)
-runEqualWith_ mode suf act =
-  extract $
-  runNameGenWith suf $
-  runExcept $
-  evalState mode act
-
-export
-runEqualInner : EqMode -> Eff EqualInner a -> Either Error a
-runEqualInner mode act = fst $ runEqualWith_ mode 0 act
-
-
-export
-runEqualWith : NameSuf -> Definitions ->
-               Eff Equal a -> (Either Error a, NameSuf)
-runEqualWith suf defs act =
-  extract $
-  runStateAt GEN suf $
-  runReaderAt DEFS defs $
-  runExcept act
-
-export
-runEqual : Definitions -> Eff Equal a -> Either Error a
-runEqual defs act = fst $ runEqualWith 0 defs act
-
 
 export %inline
 mode : Has EqModeState fs => Eff fs EqMode
@@ -631,7 +604,7 @@ parameters (loc : Loc) (ctx : TyContext d n)
   parameters (mode : EqMode)
     private
     fromInner : Eff EqualInner a -> Eff Equal a
-    fromInner act = lift $ evalState mode act
+    fromInner = lift . map fst . runState mode
 
     private
     eachFace : Applicative f => (EqContext n -> DSubst d 0 -> f ()) -> f ()
diff --git a/lib/Quox/Name.idr b/lib/Quox/Name.idr
index 57c6754..a8c9803 100644
--- a/lib/Quox/Name.idr
+++ b/lib/Quox/Name.idr
@@ -169,14 +169,6 @@ public export
 NameGen : Type -> Type
 NameGen = StateL GEN NameSuf
 
-export
-runNameGenWith : Has NameGen fs =>
-                 NameSuf -> Eff fs a -> Eff (fs - NameGen) (a, NameSuf)
-runNameGenWith = runStateAt GEN
-
-export
-runNameGen : Has NameGen fs => Eff fs a -> Eff (fs - NameGen) a
-runNameGen = map fst . runNameGenWith 0
 
 ||| generate a fresh name with the given base
 export
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index c296d26..f307f73 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -1,60 +1,45 @@
 ||| take freshly-parsed input, scope check, type check, add to env
 module Quox.Parser.FromParser
 
+import public Quox.Parser.FromParser.Error as Quox.Parser.FromParser
+
 import Quox.Parser.Syntax
 import Quox.Parser.Parser
+import Quox.Parser.LoadFile
 import Quox.Typechecker
 
 import Data.List
 import Data.Maybe
 import Data.SnocVect
 import Quox.EffExtra
+import Quox.ST
 
 import System.File
 import System.Path
 import Data.IORef
 
-import public Quox.Parser.FromParser.Error as Quox.Parser.FromParser
-
-%default total
-
 %hide Typing.Error
 %hide Lexer.Error
 %hide Parser.Error
 
+%default total
+
 
 public export
 NDefinition : Type
 NDefinition = (Name, Definition)
 
-public export
-IncludePath : Type
-IncludePath = List String
-
-public export
-SeenFiles : Type
-SeenFiles = SortedSet String
-
 
 public export
 data StateTag = NS | SEEN
 
 public export
 FromParserPure : List (Type -> Type)
-FromParserPure =
-  [Except Error, DefsState, StateL NS Mods, NameGen]
-
-public export
-LoadFile' : List (Type -> Type)
-LoadFile' = [IO, StateL SEEN SeenFiles, Reader IncludePath]
-
-public export
-LoadFile : List (Type -> Type)
-LoadFile = LoadFile' ++ [Except Error]
+FromParserPure = [Except Error, DefsState, StateL NS Mods, NameGen]
 
 public export
 FromParserIO : List (Type -> Type)
-FromParserIO = FromParserPure ++ LoadFile'
+FromParserIO = LoadFile :: FromParserPure
 
 
 parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
@@ -113,11 +98,10 @@ fromV : Context' PatVar d -> Context' PatVar n ->
         PName -> Maybe Universe -> Loc -> Eff FromParserPure (Term d n)
 fromV ds ns x u loc = fromName bound free ns x where
   bound : Var n -> Eff FromParserPure (Term d n)
-  bound i = do whenJust u $ \u => throw $ DisplacedBoundVar loc x
-               pure $ E $ B i loc
+  bound i = unless (isNothing u) (throw $ DisplacedBoundVar loc x) $> BT i loc
+
   free : PName -> Eff FromParserPure (Term d n)
-  free x = do x <- avoidDim ds loc x
-              resolveName !(getAt NS) loc x u
+  free x = resolveName !(getAt NS) loc !(avoidDim ds loc x) u
 
 mutual
   export
@@ -282,44 +266,51 @@ fromPTerm = fromPTermWith [<] [<]
 
 
 export
-globalPQty : Loc -> (q : Qty) -> Eff [Except Error] (So $ isGlobal q)
-globalPQty loc pi = case choose $ isGlobal pi of
-  Left  y => pure y
+globalPQty : Has (Except Error) fs => (q : Qty) -> Loc -> Eff fs GQty
+globalPQty pi loc = case choose $ isGlobal pi of
+  Left  y => pure $ Element pi y
   Right _ => throw $ QtyNotGlobal loc pi
 
-
 export
-fromPBaseNameNS : PBaseName -> Eff [StateL NS Mods] Name
+fromPBaseNameNS : Has (StateL NS Mods) fs => PBaseName -> Eff fs Name
 fromPBaseNameNS name = pure $ addMods !(getAt NS) $ fromPBaseName name
 
+
 private
 liftTC : Eff TC a -> Eff FromParserPure a
-liftTC act = do
-  res <- lift $ runExcept $ runReaderAt DEFS !(getAt DEFS) act
-  rethrow $ mapFst WrapTypeError res
+liftTC tc = runEff tc $ with Union.(::)
+  [handleExcept $ \e => throw $ WrapTypeError e,
+   handleReaderConst !(getAt DEFS),
+   \g => send g]
+
+private
+addDef : Has DefsState fs => Name -> GQty -> Term 0 0 -> Term 0 0 -> Loc ->
+         Eff fs NDefinition
+addDef name gqty type term loc = do
+  let def = mkDef gqty type term loc
+  modifyAt DEFS $ insert name def
+  pure (name, def)
+
 
 export covering
 fromPDef : PDefinition -> Eff FromParserPure NDefinition
 fromPDef (MkPDef qty pname ptype pterm defLoc) = do
-  name <- lift $ fromPBaseNameNS pname
-  qtyGlobal <- lift $ globalPQty qty.loc qty.val
-  let gqty = Element qty.val qtyGlobal
-      sqty = globalToSubj gqty
-  type <- lift $ traverse fromPTerm ptype
-  term <- lift $ fromPTerm pterm
+  name <- fromPBaseNameNS pname
+  gqty <- globalPQty qty.val qty.loc
+  let sqty = globalToSubj gqty
+  type <- traverse fromPTerm ptype
+  term <- fromPTerm pterm
   case type of
     Just type => do
-      liftTC $ checkTypeC empty type Nothing
-      liftTC $ ignore $ checkC empty sqty term type
-      let def = mkDef gqty type term defLoc
-      modifyAt DEFS $ insert name def
-      pure (name, def)
+      ignore $ liftTC $ do
+        checkTypeC empty type Nothing
+        checkC empty sqty term type
+      addDef name gqty type term defLoc
     Nothing => do
-      let E elim = term | _ => throw $ AnnotationNeeded term.loc empty term
+      let E elim = term
+        | _ => throw $ AnnotationNeeded term.loc empty term
       res <- liftTC $ inferC empty sqty elim
-      let def = mkDef gqty res.type term defLoc
-      modifyAt DEFS $ insert name def
-      pure (name, def)
+      addDef name gqty res.type term defLoc
 
 export covering
 fromPDecl : PDecl -> Eff FromParserPure (List NDefinition)
@@ -327,24 +318,11 @@ fromPDecl (PDef def) = singleton <$> fromPDef def
 fromPDecl (PNs  ns)  =
   localAt NS (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls
 
-
-export covering
-loadFile : Loc -> String -> Eff LoadFile (Maybe String)
-loadFile loc file =
-  if contains file !(getAt SEEN) then
-    pure Nothing
-  else do
-    Just ifile <- firstExists (map (</> file) !ask)
-      | Nothing => throw $ LoadError loc file FileNotFound
-    case !(readFile ifile) of
-      Right res => modifyAt SEEN (insert file) $> Just res
-      Left  err => throw $ LoadError loc ifile err
-
 mutual
   export covering
   loadProcessFile : Loc -> String -> Eff FromParserIO (List NDefinition)
   loadProcessFile loc file =
-    case !(lift $ loadFile loc file) of
+    case !(loadFile loc file) of
       Just inp => do
         tl <- either (throw . WrapParseError file) pure $ lexParseInput file inp
         concat <$> traverse fromPTopLevel tl
@@ -356,27 +334,31 @@ mutual
   fromPTopLevel (PD    decl)     = lift $ fromPDecl decl
   fromPTopLevel (PLoad file loc) = loadProcessFile loc file
 
+
 export
 fromParserPure : NameSuf -> Definitions ->
                  Eff FromParserPure a ->
-                 (Either Error (a, Definitions), NameSuf)
-fromParserPure suf defs act =
-  extract $
-  runStateAt GEN suf $
-  runExcept $
-  evalStateAt NS [<] $
-  runStateAt DEFS defs act
+                 Either Error (a, NameSuf, Definitions)
+fromParserPure suf defs act = runSTErr $ do
+  suf  <- newRef suf
+  defs <- newRef defs
+  res  <- runEff act $ with Union.(::)
+    [handleExcept (\e => stLeft e),
+     handleStateSTRef defs,
+     handleStateSTRef !(newRef [<]),
+     handleStateSTRef suf]
+  pure (res, !(readRef suf), !(readRef defs))
 
-export
+
+export covering
 fromParserIO : (MonadRec io, HasIO io) =>
-               IncludePath ->
-               IORef SeenFiles -> IORef NameSuf -> IORef Definitions ->
+               IncludePath -> IORef SeenSet ->
+               IORef NameSuf -> IORef Definitions ->
                Eff FromParserIO a -> io (Either Error a)
-fromParserIO inc seen suf defs act =
-  runIO $
-  runStateIORefAt GEN suf $
-  runExcept $
-  evalStateAt NS [<] $
-  runStateIORefAt SEEN seen $
-  runStateIORefAt DEFS defs $
-  runReader inc act
+fromParserIO inc seen suf defs act = liftIO $ fromIOErr $ do
+  runEff act $ with Union.(::)
+    [handleLoadFileIOE LoadError seen inc,
+     handleExcept (\e => ioLeft e),
+     handleStateIORef defs,
+     handleStateIORef !(newIORef [<]),
+     handleStateIORef suf]
diff --git a/lib/Quox/Parser/FromParser/Error.idr b/lib/Quox/Parser/FromParser/Error.idr
index 6bc2b0b..f6c7e53 100644
--- a/lib/Quox/Parser/FromParser/Error.idr
+++ b/lib/Quox/Parser/FromParser/Error.idr
@@ -1,6 +1,7 @@
 module Quox.Parser.FromParser.Error
 
 import Quox.Parser.Parser
+import Quox.Parser.LoadFile
 import Quox.Typing
 import System.File
 
@@ -28,7 +29,7 @@ data Error =
   | DimNameInTerm Loc PBaseName
   | DisplacedBoundVar Loc PName
   | WrapTypeError TypeError
-  | LoadError Loc String FileError
+  | LoadError Loc FilePath FileError
   | WrapParseError String ParseError
 
 
@@ -100,9 +101,9 @@ parameters (showContext : Bool)
   prettyError (WrapTypeError err) =
     Typing.prettyError showContext $ trimContext 2 err
 
-  prettyError (LoadError loc str err) = pure $
+  prettyError (LoadError loc file err) = pure $
     vsep [!(prettyLoc loc),
-          "couldn't load file" <++> text str,
+          "couldn't load file" <++> text file,
           text $ show err]
 
   prettyError (WrapParseError file err) =
diff --git a/lib/Quox/Parser/LoadFile.idr b/lib/Quox/Parser/LoadFile.idr
new file mode 100644
index 0000000..2935fb5
--- /dev/null
+++ b/lib/Quox/Parser/LoadFile.idr
@@ -0,0 +1,98 @@
+module Quox.Parser.LoadFile
+
+import Quox.Loc
+import Quox.EffExtra
+import Data.IORef
+import Data.SortedSet
+import System.File
+import System.Path
+
+
+%default total
+
+public export
+FilePath : Type
+FilePath = String
+
+
+public export
+data LoadFileL : (lbl : k) -> Type -> Type where
+  [search lbl]
+  Seen    : FilePath -> LoadFileL lbl Bool
+  SetSeen : FilePath -> LoadFileL lbl ()
+  DoLoad  : Loc -> FilePath -> LoadFileL lbl String
+
+public export
+LoadFile : Type -> Type
+LoadFile = LoadFileL ()
+
+
+export
+seenAt : (0 lbl : k) -> Has (LoadFileL lbl) fs => FilePath -> Eff fs Bool
+seenAt lbl file = send $ Seen {lbl} file
+
+export %inline
+seen : Has LoadFile fs => FilePath -> Eff fs Bool
+seen = seenAt ()
+
+
+export
+setSeenAt : (0 lbl : k) -> Has (LoadFileL lbl) fs => FilePath -> Eff fs ()
+setSeenAt lbl file = send $ SetSeen {lbl} file
+
+export %inline
+setSeen : Has LoadFile fs => FilePath -> Eff fs ()
+setSeen = setSeenAt ()
+
+
+export
+doLoadAt : (0 lbl : k) -> Has (LoadFileL lbl) fs =>
+           Loc -> FilePath -> Eff fs String
+doLoadAt lbl loc file = send $ DoLoad {lbl} loc file
+
+export %inline
+doLoad : Has LoadFile fs => Loc -> FilePath -> Eff fs String
+doLoad = doLoadAt ()
+
+
+public export
+SeenSet : Type
+SeenSet = SortedSet FilePath
+
+public export
+IncludePath : Type
+IncludePath = List String
+
+public export
+ErrorWrapper : Type -> Type
+ErrorWrapper e = Loc -> FilePath -> FileError -> e
+
+export covering
+readFileFrom : HasIO io => IncludePath -> FilePath ->
+               io (Either FileError String)
+readFileFrom inc f =
+  case !(firstExists $ map (</> f) inc) of
+    Just path => readFile path
+    Nothing   => pure $ Left $ FileNotFound
+
+export covering
+handleLoadFileIOE : ErrorWrapper e ->
+                    IORef SeenSet -> IncludePath ->
+                    LoadFileL lbl a -> IOErr e a
+handleLoadFileIOE inj seen inc = \case
+  Seen    f   => contains f <$> readIORef seen
+  SetSeen f   => modifyIORef seen $ insert f
+  DoLoad  l f => readFileFrom inc f >>= either (ioLeft . inj l f) pure
+
+
+export
+loadFileAt : (0 lbl : k) -> Has (LoadFileL lbl) fs =>
+             Loc -> FilePath -> Eff fs (Maybe String)
+loadFileAt lbl loc file =
+  if !(seenAt lbl file)
+     then pure Nothing
+     else Just <$> doLoadAt lbl loc file <* setSeenAt lbl file
+
+export
+loadFile : Has LoadFile fs => Loc -> FilePath -> Eff fs (Maybe String)
+loadFile = loadFileAt ()
diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr
index f90e5ec..1da3743 100644
--- a/lib/Quox/Pretty.idr
+++ b/lib/Quox/Pretty.idr
@@ -3,6 +3,7 @@ module Quox.Pretty
 import Quox.Loc
 import Quox.Name
 
+import Quox.ST
 import public Text.PrettyPrint.Bernardy
 import public Text.PrettyPrint.Bernardy.Core.Decorate
 import public Quox.EffExtra
@@ -65,11 +66,12 @@ export %inline
 runPrettyWith : PPrec -> Flavor -> (HL -> Highlight) -> Nat ->
                 Eff Pretty a -> a
 runPrettyWith prec flavor highlight indent act =
-  extract $
-  evalStateAt PREC prec $
-  runReaderAt FLAVOR flavor $
-  runReaderAt HIGHLIGHT highlight $
-  runReaderAt INDENT indent act
+  runST $ do
+    runEff act $ with Union.(::)
+      [handleStateSTRef !(newRef prec),
+       handleReaderConst flavor,
+       handleReaderConst highlight,
+       handleReaderConst indent]
 
 
 export %inline
@@ -101,26 +103,27 @@ runPrettyColor = runPrettyWith Outer Unicode highlightSGR 2
 
 
 export %inline
-hl : {opts : _} -> HL -> Doc opts -> Eff Pretty (Doc opts)
+hl : {opts : LayoutOpts} -> HL -> Doc opts -> Eff Pretty (Doc opts)
 hl h doc = asksAt HIGHLIGHT $ \f => decorate (f h) doc
 
 
 export %inline
-indentD : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
+indentD : {opts : LayoutOpts} -> Doc opts -> Eff Pretty (Doc opts)
 indentD doc = pure $ indent !(askAt INDENT) doc
 
 export %inline
-hangD : {opts : _} -> Doc opts -> Doc opts -> Eff Pretty (Doc opts)
+hangD : {opts : LayoutOpts} -> Doc opts -> Doc opts -> Eff Pretty (Doc opts)
 hangD d1 d2 = pure $ hangSep !(askAt INDENT) d1 d2
 
 export %inline
-hangDSingle : {opts : _} -> Doc opts -> Doc opts -> Eff Pretty (Doc opts)
+hangDSingle : {opts : LayoutOpts} -> Doc opts -> Doc opts ->
+              Eff Pretty (Doc opts)
 hangDSingle d1 d2 =
   pure $ ifMultiline (d1 <++> d2) (vappend d1 !(indentD d2))
 
 
 export
-tightDelims : {opts : _} -> (l, r : String) -> (inner : Doc opts) ->
+tightDelims : {opts : LayoutOpts} -> (l, r : String) -> (inner : Doc opts) ->
               Eff Pretty (Doc opts)
 tightDelims l r inner = do
   l <- hl Delim $ text l
@@ -128,7 +131,7 @@ tightDelims l r inner = do
   pure $ hcat [l, inner, r]
 
 export
-looseDelims : {opts : _} -> (l, r : String) -> (inner : Doc opts) ->
+looseDelims : {opts : LayoutOpts} -> (l, r : String) -> (inner : Doc opts) ->
               Eff Pretty (Doc opts)
 looseDelims l r inner = do
   l <- hl Delim $ text l
@@ -138,39 +141,39 @@ looseDelims l r inner = do
   pure $ ifMultiline short long
 
 export %inline
-parens : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
+parens : {opts : LayoutOpts} -> Doc opts -> Eff Pretty (Doc opts)
 parens = tightDelims "(" ")"
 
 export %inline
-bracks : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
+bracks : {opts : LayoutOpts} -> Doc opts -> Eff Pretty (Doc opts)
 bracks = tightDelims "[" "]"
 
 export %inline
-braces : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
+braces : {opts : LayoutOpts} -> Doc opts -> Eff Pretty (Doc opts)
 braces = looseDelims "{" "}"
 
 export %inline
-tightBraces : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
+tightBraces : {opts : LayoutOpts} -> Doc opts -> Eff Pretty (Doc opts)
 tightBraces = tightDelims "{" "}"
 
 export %inline
-parensIf : {opts : _} -> Bool -> Doc opts -> Eff Pretty (Doc opts)
+parensIf : {opts : LayoutOpts} -> Bool -> Doc opts -> Eff Pretty (Doc opts)
 parensIf True  = parens
 parensIf False = pure
 
 
 ||| uses hsep only if the whole list fits on one line
 export
-sepSingle : {opts : _} -> List (Doc opts) -> Doc opts
+sepSingle : {opts : LayoutOpts} -> List (Doc opts) -> Doc opts
 sepSingle xs = ifMultiline (hsep xs) (vsep xs)
 
 export
-fillSep : {opts : _} -> List (Doc opts) -> Doc opts
+fillSep : {opts : LayoutOpts} -> List (Doc opts) -> Doc opts
 fillSep []        = empty
 fillSep (x :: xs) = foldl (\x, y => sep [x, y]) x xs
 
 export
-exceptLast : {opts : _} -> (Doc opts -> Doc opts) ->
+exceptLast : {opts : LayoutOpts} -> (Doc opts -> Doc opts) ->
              List (Doc opts) -> List (Doc opts)
 exceptLast f []        = []
 exceptLast f [x]       = [x]
@@ -198,7 +201,7 @@ ifUnicode uni asc =
     Ascii   => asc
 
 export %inline
-parensIfM : {opts : _} -> PPrec -> Doc opts -> Eff Pretty (Doc opts)
+parensIfM : {opts : LayoutOpts} -> PPrec -> Doc opts -> Eff Pretty (Doc opts)
 parensIfM d doc = parensIf (!(getAt PREC) > d) doc
 
 export %inline
@@ -211,7 +214,7 @@ prettyName : Name -> Doc opts
 prettyName = text . toDots
 
 export
-prettyFree : {opts : _} -> Name -> Eff Pretty (Doc opts)
+prettyFree : {opts : LayoutOpts} -> Name -> Eff Pretty (Doc opts)
 prettyFree = hl Free . prettyName
 
 export
@@ -219,11 +222,11 @@ prettyBind' : BindName -> Doc opts
 prettyBind' = text . baseStr . name
 
 export
-prettyTBind : {opts : _} -> BindName -> Eff Pretty (Doc opts)
+prettyTBind : {opts : LayoutOpts} -> BindName -> Eff Pretty (Doc opts)
 prettyTBind = hl TVar . prettyBind'
 
 export
-prettyDBind : {opts : _} -> BindName -> Eff Pretty (Doc opts)
+prettyDBind : {opts : LayoutOpts} -> BindName -> Eff Pretty (Doc opts)
 prettyDBind = hl DVar . prettyBind'
 
 
@@ -232,7 +235,7 @@ export %inline
 typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
 eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
 ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD :
-  {opts : _} -> Eff Pretty (Doc opts)
+  {opts : LayoutOpts} -> Eff Pretty (Doc opts)
 typeD     = hl Syntax . text =<< ifUnicode "★" "Type"
 arrowD    = hl Delim  . text =<< ifUnicode "→" "->"
 darrowD   = hl Delim  . text =<< ifUnicode "⇒" "=>"
@@ -261,14 +264,16 @@ pipeD     = hl Syntax $ text "|"
 
 
 export
-prettyApp : {opts : _} -> Nat -> Doc opts -> List (Doc opts) -> Doc opts
+prettyApp : {opts : LayoutOpts} -> Nat -> Doc opts ->
+            List (Doc opts) -> Doc opts
 prettyApp ind f args =
       hsep (f :: args)
   <|> hsep [f, vsep args]
   <|> vsep (f :: map (indent ind) args)
 
 export
-prettyAppD : {opts : _} -> Doc opts -> List (Doc opts) -> Eff Pretty (Doc opts)
+prettyAppD : {opts : LayoutOpts} -> Doc opts -> List (Doc opts) ->
+             Eff Pretty (Doc opts)
 prettyAppD f args = pure $ prettyApp !(askAt INDENT) f args
 
 
@@ -288,7 +293,7 @@ quoteTag tag =
   "\"" ++ escapeString tag ++ "\""
 
 export
-prettyBounds : {opts : _} -> Bounds -> Eff Pretty (Doc opts)
+prettyBounds : {opts : LayoutOpts} -> Bounds -> Eff Pretty (Doc opts)
 prettyBounds (MkBounds l1 c1 l2 c2) =
   hcat <$> sequence
     [hl TVar $ text $ show l1, colonD,
@@ -297,7 +302,7 @@ prettyBounds (MkBounds l1 c1 l2 c2) =
      hl DVar $ text $ show c2, colonD]
 
 export
-prettyLoc : {opts : _} -> Loc -> Eff Pretty (Doc opts)
+prettyLoc : {opts : LayoutOpts} -> Loc -> Eff Pretty (Doc opts)
 prettyLoc (L NoLoc) =
   hcat <$> sequence [hl TVarErr "no location", colonD]
 prettyLoc (L (YesLoc file b)) =
diff --git a/lib/Quox/ST.idr b/lib/Quox/ST.idr
new file mode 100644
index 0000000..a900c7f
--- /dev/null
+++ b/lib/Quox/ST.idr
@@ -0,0 +1,106 @@
+module Quox.ST
+
+import Data.IORef
+import Control.MonadRec
+
+
+export
+Tag : Type
+Tag = () -- shhh don't tell anyone
+
+export
+record ST (s : Tag) a where
+  constructor MkST
+  action : IO a
+%name ST st
+
+export
+runST : (forall s. ST s a) -> a
+runST st = unsafePerformIO (st {s = ()}).action
+
+export %inline Functor (ST s) where map f st = MkST $ map f st.action
+
+export %inline
+Applicative (ST s) where
+  pure = MkST . pure
+  f <*> x = MkST $ f.action <*> x.action
+
+export %inline Monad (ST s) where m >>= k = MkST $ m.action >>= action . k
+
+export %inline
+MonadRec (ST s) where
+  tailRecM s (Access r) x k = MkST $ do
+    let MkST yy = k s x
+    case !yy of
+      Done y      => pure y
+      Cont s2 p y => let MkST z = tailRecM s2 (r s2 p) y k in z
+
+
+public export
+interface HasST (0 m : Tag -> Type -> Type) where
+  liftST : ST s a -> m s a
+
+export %inline HasST ST where liftST = id
+
+export
+record STRef (s : Tag) a where
+  constructor MkSTRef
+  ref : IORef a
+%name STRef r
+
+export %inline
+newRef : HasST m => a -> m s (STRef s a)
+newRef x = liftST $ MkST $ MkSTRef <$> newIORef x
+
+export %inline
+readRef : HasST m => STRef s a -> m s a
+readRef r = liftST $ MkST $ readIORef r.ref
+
+export %inline
+writeRef : HasST m => STRef s a -> a -> m s ()
+writeRef r x = liftST $ MkST $ writeIORef r.ref x
+
+export %inline
+modifyRef : HasST m => STRef s a -> (a -> a) -> m s ()
+modifyRef r f = liftST $ MkST $ modifyIORef r.ref f
+
+
+public export
+record STErr e (s : Tag) a where
+  constructor STE
+  fromSTErr : ST s (Either e a)
+
+export
+Functor (STErr e s) where
+  map f (STE e) = STE $ map f <$> e
+
+export
+Applicative (STErr e s) where
+  pure x = STE $ pure $ pure x
+  STE f <*> STE x = STE [|f <*> x|]
+
+export
+Monad (STErr e s) where
+  STE m >>= k = STE $ do
+    case !m of
+      Left  err => pure $ Left err
+      Right x   => fromSTErr $ k x
+
+export
+MonadRec (STErr e s) where
+  tailRecM s (Access r) x k = STE $ do
+    let STE m = k s x
+    case !m of
+      Left  err           => pure $ Left err
+      Right (Cont s' p y) => fromSTErr $ tailRecM s' (r s' p) y k
+      Right (Done y)      => pure $ Right y
+
+export
+runSTErr : (forall s. STErr e s a) -> Either e a
+runSTErr ste = runST $ fromSTErr ste
+
+export %inline HasST (STErr e) where liftST = STE . map Right
+
+export
+stLeft : e -> STErr e s a
+stLeft e = STE $ pure $ Left e
diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 5682c73..1023dfd 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -324,6 +324,11 @@ public export %inline
 FT : Name -> Universe -> Loc -> Term d n
 FT x u loc = E $ F x u loc
 
+||| same as `B` but as a term
+public export %inline
+BT : Var n -> (loc : Loc) -> Term d n
+BT i loc = E $ B i loc
+
 ||| abbreviation for a bound variable like `BV 4` instead of
 ||| `B (VS (VS (VS (VS VZ))))`
 public export %inline
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index fa02277..ef0138a 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -16,14 +16,6 @@ public export
 0 TC : List (Type -> Type)
 TC = [ErrorEff, DefsReader, NameGen]
 
-export
-runTCWith : NameSuf -> Definitions -> Eff TC a -> (Either Error a, NameSuf)
-runTCWith = runEqualWith
-
-export
-runTC : Definitions -> Eff TC a -> Either Error a
-runTC = runEqual
-
 
 parameters (loc : Loc)
   export
diff --git a/lib/Quox/Whnf/Interface.idr b/lib/Quox/Whnf/Interface.idr
index dfefdd0..6c50074 100644
--- a/lib/Quox/Whnf/Interface.idr
+++ b/lib/Quox/Whnf/Interface.idr
@@ -15,14 +15,6 @@ public export
 Whnf : List (Type -> Type)
 Whnf = [NameGen, Except Error]
 
-export
-runWhnfWith : NameSuf -> Eff Whnf a -> (Either Error a, NameSuf)
-runWhnfWith suf act = extract $ runStateAt GEN suf $ runExcept act
-
-export
-runWhnf : Eff Whnf a -> Either Error a
-runWhnf = fst . runWhnfWith 0
-
 
 public export
 0 RedexTest : TermLike -> Type
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index 832f07d..6fd3882 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -14,6 +14,7 @@ modules =
   Quox.NatExtra,
   Quox.EffExtra,
   Quox.Decidable,
+  Quox.ST,
   Quox.No,
   Quox.Loc,
   Quox.OPE,
@@ -50,6 +51,7 @@ modules =
   Quox.Parser.Lexer,
   Quox.Parser.Syntax,
   Quox.Parser.Parser,
+  Quox.Parser.LoadFile,
   Quox.Parser.FromParser,
   Quox.Parser.FromParser.Error,
   Quox.Parser
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index 881320e..a263a2b 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -2,12 +2,14 @@ module Tests.Equal
 
 import Quox.Equal
 import Quox.Typechecker
+import Quox.ST
 import public TypingImpls
 import TAP
 import Quox.EffExtra
 import AstExtra
 
 
+
 defGlobals : Definitions
 defGlobals = fromList
   [("A", ^mkPostulate gzero (^TYPE 0)),
diff --git a/tests/Tests/FromPTerm.idr b/tests/Tests/FromPTerm.idr
index c4202eb..52c4b78 100644
--- a/tests/Tests/FromPTerm.idr
+++ b/tests/Tests/FromPTerm.idr
@@ -68,7 +68,7 @@ parameters {c : Bool} {auto _ : Show b}
 
 runFromParser : {default empty defs : Definitions} ->
                 Eff FromParserPure a -> Either FromParser.Error a
-runFromParser = map fst . fst . fromParserPure 0 defs
+runFromParser = map fst . fromParserPure 0 defs
 
 export
 tests : Test
diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr
index 53404e4..6848bb8 100644
--- a/tests/Tests/Reduce.idr
+++ b/tests/Tests/Reduce.idr
@@ -2,6 +2,7 @@ module Tests.Reduce
 
 import Quox.Syntax as Lib
 import Quox.Equal
+import Quox.ST
 import TypingImpls
 import AstExtra
 import TAP
@@ -11,6 +12,10 @@ import Control.Eff
 %hide Pretty.App
 
 
+runWhnf : Eff Whnf a -> Either Error a
+runWhnf act = runSTErr $ do
+  runEff act [handleStateSTRef !(newRef 0), handleExcept (\e => stLeft e)]
+
 parameters {0 isRedex : RedexTest tm} {auto _ : CanWhnf tm isRedex} {d, n : Nat}
            {auto _ : (Eq (tm d n), Show (tm d n))}
            {default empty defs : Definitions}
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index b845e5b..1365f3e 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -2,6 +2,7 @@ module Tests.Typechecker
 
 import Quox.Syntax
 import Quox.Typechecker as Lib
+import Quox.ST
 import public TypingImpls
 import TAP
 import Quox.EffExtra
diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr
index e84ed32..febb152 100644
--- a/tests/TypingImpls.idr
+++ b/tests/TypingImpls.idr
@@ -3,6 +3,9 @@ module TypingImpls
 import TAP
 import public Quox.Typing
 import public Quox.Pretty
+import Quox.Equal
+import Quox.Typechecker
+import Quox.ST
 import PrettyExtra
 
 import Derive.Prelude
@@ -19,3 +22,16 @@ ToInfo Error where
   toInfo err =
     let str = render (Opts 60) $ runPrettyDef $ prettyError True err in
     [("err", str)]
+
+
+export
+runEqual : Definitions -> Eff Equal a -> Either Error a
+runEqual defs act = runSTErr $ do
+  runEff act
+    [handleExcept (\e => stLeft e),
+     handleReaderConst defs,
+     handleStateSTRef !(newRef 0)]
+
+export
+runTC : Definitions -> Eff TC a -> Either Error a
+runTC = runEqual