more effect stuff, incl. ST
This commit is contained in:
parent
4b6b3853a1
commit
a221380d61
17 changed files with 395 additions and 204 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 ()
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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) =
|
||||
|
|
|
|||
98
lib/Quox/Parser/LoadFile.idr
Normal file
98
lib/Quox/Parser/LoadFile.idr
Normal file
|
|
@ -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 ()
|
||||
|
|
@ -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)) =
|
||||
|
|
|
|||
106
lib/Quox/ST.idr
Normal file
106
lib/Quox/ST.idr
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)),
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue