quox/lib/Quox/Parser/FromParser.idr

405 lines
12 KiB
Idris
Raw Normal View History

2023-05-01 21:06:25 -04:00
||| take freshly-parsed input, scope check, type check, add to env
module Quox.Parser.FromParser
2023-08-25 12:09:06 -04:00
import public Quox.Parser.FromParser.Error as Quox.Parser.FromParser
import Quox.Pretty
import Quox.Parser.Syntax
2023-03-13 14:33:09 -04:00
import Quox.Parser.Parser
2023-08-26 15:07:10 -04:00
import public Quox.Parser.LoadFile
import Quox.Typechecker
import Data.List
2023-05-14 13:58:46 -04:00
import Data.Maybe
import Data.SnocVect
2023-03-31 13:23:30 -04:00
import Quox.EffExtra
2023-09-18 18:41:47 -04:00
import Control.Monad.ST.Extra
2023-03-13 14:33:09 -04:00
import System.File
import System.Path
2023-03-31 13:23:30 -04:00
import Data.IORef
2023-03-13 14:33:09 -04:00
2023-03-31 13:23:30 -04:00
%hide Typing.Error
%hide Lexer.Error
%hide Parser.Error
2023-08-25 12:09:06 -04:00
%default total
2023-03-31 13:23:30 -04:00
public export
NDefinition : Type
2023-04-01 13:16:43 -04:00
NDefinition = (Name, Definition)
2023-03-13 14:33:09 -04:00
public export
data StateTag = NS | SEEN
public export
FromParserPure : List (Type -> Type)
2023-08-25 12:09:06 -04:00
FromParserPure = [Except Error, DefsState, StateL NS Mods, NameGen]
2023-05-01 21:06:25 -04:00
public export
FromParserIO : List (Type -> Type)
2023-08-25 12:09:06 -04:00
FromParserIO = LoadFile :: FromParserPure
export
fromParserPure : NameSuf -> Definitions ->
Eff FromParserPure a ->
Either Error (a, NameSuf, Definitions)
fromParserPure suf defs act = runSTErr $ do
suf <- liftST $ newSTRef suf
defs <- liftST $ newSTRef defs
res <- runEff act $ with Union.(::)
[handleExcept (\e => stLeft e),
handleStateSTRef defs,
handleStateSTRef !(liftST $ newSTRef [<]),
handleStateSTRef suf]
pure (res, !(liftST $ readSTRef suf), !(liftST $ readSTRef defs))
export covering
fromParserIO : (MonadRec io, HasIO io) =>
IncludePath -> IORef SeenSet ->
IORef NameSuf -> IORef Definitions ->
Eff FromParserIO a -> io (Either Error a)
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]
parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
(xs : Context' PatVar n)
private
fromBaseName : PBaseName -> m a
fromBaseName x = maybe (f $ MakePName [<] x) b $
Context.find (\y => y.name == Just x) xs
private
fromName : PName -> m a
fromName x = if null x.mods then fromBaseName x.base else f x
export
2023-03-31 13:23:30 -04:00
fromPDimWith : Has (Except Error) fs =>
Context' PatVar d -> PDim -> Eff fs (Dim d)
2023-05-01 21:06:25 -04:00
fromPDimWith ds (K e loc) = pure $ K e loc
fromPDimWith ds (V i loc) =
fromBaseName (\i => pure $ B i loc)
(const $ throw $ DimNotInScope loc i) ds i
private
2023-03-31 13:23:30 -04:00
avoidDim : Has (Except Error) fs =>
2023-05-01 21:06:25 -04:00
Context' PatVar d -> Loc -> PName -> Eff fs Name
avoidDim ds loc x =
fromName (const $ throw $ DimNameInTerm loc x.base) (pure . fromPName) ds x
private
2023-05-21 14:09:34 -04:00
resolveName : Mods -> Loc -> Name -> Maybe Universe ->
Eff FromParserPure (Term d n)
resolveName ns loc x u =
let here = addMods ns x in
if isJust $ lookup here !(getAt DEFS) then
2023-05-21 14:09:34 -04:00
pure $ FT here (fromMaybe 0 u) loc
else do
let ns :< _ = ns
2023-05-01 21:06:25 -04:00
| _ => throw $ TermNotInScope loc x
2023-05-21 14:09:34 -04:00
resolveName ns loc x u
export
2023-05-01 21:06:25 -04:00
fromPatVar : PatVar -> BindName
fromPatVar (Unused loc) = BN Unused loc
fromPatVar (PV x loc) = BN (UN x) loc
export
fromPQty : PQty -> Qty
fromPQty (PQ q _) = q
export
fromPTagVal : PTagVal -> TagVal
fromPTagVal (PT t _) = t
2023-05-21 14:09:34 -04:00
private
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)
2023-08-25 12:09:06 -04:00
bound i = unless (isNothing u) (throw $ DisplacedBoundVar loc x) $> BT i loc
2023-05-21 14:09:34 -04:00
free : PName -> Eff FromParserPure (Term d n)
2023-08-25 12:09:06 -04:00
free x = resolveName !(getAt NS) loc !(avoidDim ds loc x) u
2023-05-21 14:09:34 -04:00
mutual
export
fromPTermWith : Context' PatVar d -> Context' PatVar n ->
PTerm -> Eff FromParserPure (Term d n)
fromPTermWith ds ns t0 = case t0 of
2023-05-01 21:06:25 -04:00
TYPE k loc =>
pure $ TYPE k loc
2023-05-01 21:06:25 -04:00
Pi pi x s t loc =>
Pi (fromPQty pi)
<$> fromPTermWith ds ns s
<*> fromPTermTScope ds ns [< x] t
2023-05-01 21:06:25 -04:00
<*> pure loc
2023-05-01 21:06:25 -04:00
Lam x s loc =>
Lam <$> fromPTermTScope ds ns [< x] s <*> pure loc
2023-05-01 21:06:25 -04:00
App s t loc =>
map E $ App
<$> fromPTermElim ds ns s
<*> fromPTermWith ds ns t
<*> pure loc
2023-05-01 21:06:25 -04:00
Sig x s t loc =>
Sig <$> fromPTermWith ds ns s
<*> fromPTermTScope ds ns [< x] t
<*> pure loc
2023-05-01 21:06:25 -04:00
Pair s t loc =>
Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t <*> pure loc
2023-05-01 21:06:25 -04:00
Case pi pair (r, ret) (CasePair (x, y) body _) loc =>
map E $ CasePair (fromPQty pi)
<$> fromPTermElim ds ns pair
<*> fromPTermTScope ds ns [< r] ret
<*> fromPTermTScope ds ns [< x, y] body
2023-05-01 21:06:25 -04:00
<*> pure loc
2023-09-18 15:52:51 -04:00
Fst pair loc =>
map E $ Fst <$> fromPTermElim ds ns pair <*> pure loc
Snd pair loc =>
map E $ Snd <$> fromPTermElim ds ns pair <*> pure loc
2023-05-01 21:06:25 -04:00
Case pi tag (r, ret) (CaseEnum arms _) loc =>
map E $ CaseEnum (fromPQty pi)
<$> fromPTermElim ds ns tag
<*> fromPTermTScope ds ns [< r] ret
<*> assert_total fromPTermEnumArms loc ds ns arms
2023-05-01 21:06:25 -04:00
<*> pure loc
2023-05-01 21:06:25 -04:00
Nat loc => pure $ Nat loc
Zero loc => pure $ Zero loc
Succ n loc => [|Succ (fromPTermWith ds ns n) (pure loc)|]
2023-03-26 08:40:54 -04:00
2023-05-01 21:06:25 -04:00
Case pi nat (r, ret) (CaseNat zer (s, pi', ih, suc) _) loc =>
map E $ CaseNat (fromPQty pi) (fromPQty pi')
2023-03-26 08:40:54 -04:00
<$> fromPTermElim ds ns nat
<*> fromPTermTScope ds ns [< r] ret
<*> fromPTermWith ds ns zer
<*> fromPTermTScope ds ns [< s, ih] suc
2023-05-01 21:06:25 -04:00
<*> pure loc
2023-03-26 08:40:54 -04:00
Enum strs loc => do
let set = SortedSet.fromList strs
unless (length strs == length (SortedSet.toList set)) $
throw $ DuplicatesInEnumType loc strs
pure $ Enum set loc
2023-05-01 21:06:25 -04:00
Tag str loc => pure $ Tag str loc
2023-05-01 21:06:25 -04:00
Eq (i, ty) s t loc =>
Eq <$> fromPTermDScope ds ns [< i] ty
<*> fromPTermWith ds ns s
<*> fromPTermWith ds ns t
2023-05-01 21:06:25 -04:00
<*> pure loc
2023-05-01 21:06:25 -04:00
DLam i s loc =>
DLam <$> fromPTermDScope ds ns [< i] s <*> pure loc
2023-05-01 21:06:25 -04:00
DApp s p loc =>
map E $ DApp
<$> fromPTermElim ds ns s
<*> fromPDimWith ds p
<*> pure loc
2023-05-01 21:06:25 -04:00
BOX q ty loc => BOX (fromPQty q) <$> fromPTermWith ds ns ty <*> pure loc
2023-03-31 13:11:35 -04:00
2023-05-01 21:06:25 -04:00
Box val loc => Box <$> fromPTermWith ds ns val <*> pure loc
2023-03-31 13:11:35 -04:00
2023-05-01 21:06:25 -04:00
Case pi box (r, ret) (CaseBox b body _) loc =>
map E $ CaseBox (fromPQty pi)
2023-03-31 13:11:35 -04:00
<$> fromPTermElim ds ns box
<*> fromPTermTScope ds ns [< r] ret
<*> fromPTermTScope ds ns [< b] body
2023-05-01 21:06:25 -04:00
<*> pure loc
2023-03-31 13:11:35 -04:00
2023-05-21 14:09:34 -04:00
V x u loc => fromV ds ns x u loc
2023-05-01 21:06:25 -04:00
Ann s a loc =>
map E $ Ann
<$> fromPTermWith ds ns s
<*> fromPTermWith ds ns a
<*> pure loc
2023-05-01 21:06:25 -04:00
Coe (i, ty) p q val loc =>
2023-04-15 09:13:01 -04:00
map E $ Coe
<$> fromPTermDScope ds ns [< i] ty
<*> fromPDimWith ds p
<*> fromPDimWith ds q
<*> fromPTermWith ds ns val
2023-05-01 21:06:25 -04:00
<*> pure loc
2023-04-15 09:13:01 -04:00
2023-05-01 21:06:25 -04:00
Comp (i, ty) p q val r (j0, val0) (j1, val1) loc =>
map E $ CompH'
2023-04-15 09:13:01 -04:00
<$> fromPTermDScope ds ns [< i] ty
<*> fromPDimWith ds p
<*> fromPDimWith ds q
<*> fromPTermWith ds ns val
<*> fromPDimWith ds r
<*> fromPTermDScope ds ns [< j0] val0
<*> fromPTermDScope ds ns [< j1] val1
2023-05-01 21:06:25 -04:00
<*> pure loc
2023-04-15 09:13:01 -04:00
private
fromPTermEnumArms : Loc -> Context' PatVar d -> Context' PatVar n ->
List (PTagVal, PTerm) ->
Eff FromParserPure (CaseEnumArms d n)
fromPTermEnumArms loc ds ns arms = do
res <- SortedMap.fromList <$>
traverse (bitraverse (pure . fromPTagVal) (fromPTermWith ds ns)) arms
unless (length (keys res) == length arms) $
throw $ DuplicatesInEnumCase loc (map (fromPTagVal . fst) arms)
pure res
private
fromPTermElim : Context' PatVar d -> Context' PatVar n ->
PTerm -> Eff FromParserPure (Elim d n)
fromPTermElim ds ns e =
case !(fromPTermWith ds ns e) of
E e => pure e
t => let ctx = MkNameContexts (map fromPatVar ds) (map fromPatVar ns) in
2023-05-01 21:06:25 -04:00
throw $ AnnotationNeeded t.loc ctx t
private
fromPTermTScope : {s : Nat} -> Context' PatVar d -> Context' PatVar n ->
SnocVect s PatVar -> PTerm ->
Eff FromParserPure (ScopeTermN s d n)
fromPTermTScope ds ns xs t =
if all isUnused xs then
SN <$> fromPTermWith ds ns t
else
ST (fromSnocVect $ map fromPatVar xs) <$> fromPTermWith ds (ns ++ xs) t
private
fromPTermDScope : {s : Nat} -> Context' PatVar d -> Context' PatVar n ->
SnocVect s PatVar -> PTerm ->
Eff FromParserPure (DScopeTermN s d n)
fromPTermDScope ds ns xs t =
if all isUnused xs then
SN <$> fromPTermWith ds ns t
else
DST (fromSnocVect $ map fromPatVar xs) <$> fromPTermWith (ds ++ xs) ns t
export %inline
fromPTerm : PTerm -> Eff FromParserPure (Term 0 0)
fromPTerm = fromPTermWith [<] [<]
export
2023-08-25 12:09:06 -04:00
globalPQty : Has (Except Error) fs => (q : Qty) -> Loc -> Eff fs GQty
globalPQty pi loc = case toGlobal pi of
Just g => pure g
Nothing => throw $ QtyNotGlobal loc pi
2023-03-13 14:33:09 -04:00
export
2023-08-25 12:09:06 -04:00
fromPBaseNameNS : Has (StateL NS Mods) fs => PBaseName -> Eff fs Name
fromPBaseNameNS name = pure $ addMods !(getAt NS) $ fromPBaseName name
2023-08-25 12:09:06 -04:00
2023-03-13 14:33:09 -04:00
private
2023-08-24 13:55:57 -04:00
liftTC : Eff TC a -> Eff FromParserPure a
2023-08-25 12:09:06 -04:00
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)
2023-03-31 13:23:30 -04:00
export covering
fromPDef : PDefinition -> Eff FromParserPure NDefinition
2023-05-01 21:06:25 -04:00
fromPDef (MkPDef qty pname ptype pterm defLoc) = do
2023-08-25 12:09:06 -04:00
name <- fromPBaseNameNS pname
gqty <- globalPQty qty.val qty.loc
let sqty = globalToSubj gqty
type <- traverse fromPTerm ptype
term <- fromPTerm pterm
2023-03-13 14:33:09 -04:00
case type of
Just type => do
2023-08-25 12:09:06 -04:00
ignore $ liftTC $ do
checkTypeC empty type Nothing
checkC empty sqty term type
addDef name gqty type term defLoc
2023-03-13 14:33:09 -04:00
Nothing => do
2023-08-25 12:09:06 -04:00
let E elim = term
| _ => throw $ AnnotationNeeded term.loc empty term
2023-05-01 21:06:25 -04:00
res <- liftTC $ inferC empty sqty elim
2023-08-25 12:09:06 -04:00
addDef name gqty res.type term defLoc
2023-03-31 13:23:30 -04:00
public export
data HasFail = NoFail | AnyFail | FailWith String
export
hasFail : List PDeclMod -> HasFail
hasFail [] = NoFail
hasFail (PFail str _ :: _) = maybe AnyFail FailWith str
2023-03-31 13:23:30 -04:00
export covering
fromPDecl : PDecl -> Eff FromParserPure (List NDefinition)
export covering
fromPDeclBody : PDeclBody -> Eff FromParserPure (List NDefinition)
fromPDeclBody (PDef def) = singleton <$> fromPDef def
fromPDeclBody (PNs ns) =
2023-03-31 13:23:30 -04:00
localAt NS (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls
2023-03-13 14:33:09 -04:00
export covering
expectFail : PDeclBody -> Eff FromParserPure Error
expectFail body =
case fromParserPure !(getAt GEN) !(getAt DEFS) $ fromPDeclBody body of
Left err => pure err
Right _ => throw $ ExpectedFail body.loc
fromPDecl (MkPDecl mods decl loc) = case hasFail mods of
NoFail => fromPDeclBody decl
AnyFail => expectFail decl $> []
FailWith str => do
err <- expectFail decl
let msg = runPretty $ prettyError False err {opts = Opts 10_000} -- w/e
if str `isInfixOf` renderInfinite msg
then pure []
else throw $ WrongFail str err loc
mutual
2023-03-31 13:23:30 -04:00
export covering
2023-05-01 21:06:25 -04:00
loadProcessFile : Loc -> String -> Eff FromParserIO (List NDefinition)
loadProcessFile loc file =
2023-08-25 12:09:06 -04:00
case !(loadFile loc file) of
2023-03-31 13:23:30 -04:00
Just inp => do
tl <- either (throw . WrapParseError file) pure $ lexParseInput file inp
2023-03-31 13:23:30 -04:00
concat <$> traverse fromPTopLevel tl
Nothing => pure []
||| populates the `defs` field of the state
export covering
2023-05-01 21:06:25 -04:00
fromPTopLevel : PTopLevel -> Eff FromParserIO (List NDefinition)
fromPTopLevel (PD decl) = lift $ fromPDecl decl
fromPTopLevel (PLoad file loc) = loadProcessFile loc file