quox/lib/Quox/Parser/FromParser.idr

351 lines
9.9 KiB
Idris
Raw Normal View History

||| take freshly-parsed input, translate it to core, and check it
module Quox.Parser.FromParser
import Quox.Parser.Syntax
2023-03-13 14:33:09 -04:00
import Quox.Parser.Parser
import Quox.Typechecker
import Data.List
import Data.SnocVect
2023-03-31 13:23:30 -04:00
import Quox.EffExtra
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 17:43:25 -04:00
import public Quox.Parser.FromParser.Error as Quox.Parser.FromParser
2023-03-31 13:23:30 -04:00
%default total
%hide Typing.Error
%hide Lexer.Error
%hide Parser.Error
public export
2023-04-01 13:16:43 -04:00
0 NDefinition : Type
NDefinition = (Name, Definition)
public export
2023-03-31 13:23:30 -04:00
0 IncludePath : Type
IncludePath = List String
2023-03-13 14:33:09 -04:00
public export
2023-03-31 13:23:30 -04:00
0 SeenFiles : Type
SeenFiles = SortedSet String
2023-03-13 14:33:09 -04:00
public export
data StateTag = NS | SEEN
public export
0 FromParserPure : List (Type -> Type)
FromParserPure =
[Except Error, StateL DEFS Definitions, StateL NS Mods]
public export
2023-03-31 13:23:30 -04:00
0 FromParserEff : List (Type -> Type)
FromParserEff =
2023-04-01 13:16:43 -04:00
[Except Error, StateL DEFS Definitions, StateL NS Mods,
2023-03-31 13:23:30 -04:00
Reader IncludePath, StateL SEEN SeenFiles, IO]
2023-03-31 13:23:30 -04:00
public export
0 FromParser : Type -> Type
FromParser = Eff FromParserEff
parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
(xs : Context' BName n)
private
fromBaseName : PBaseName -> m a
fromBaseName x = maybe (f $ MakePName [<] x) b $ Context.find (== 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' BName d -> PDim -> Eff fs (Dim d)
fromPDimWith ds (K e) = pure $ K e
fromPDimWith ds (V i) =
2023-03-31 13:23:30 -04:00
fromBaseName (pure . B) (const $ throw $ DimNotInScope i) ds i
private
2023-03-31 13:23:30 -04:00
avoidDim : Has (Except Error) fs =>
Context' BName d -> PName -> Eff fs Name
avoidDim ds x =
fromName (const $ throw $ DimNameInTerm x.base) (pure . fromPName) ds x
private
resolveName : Mods -> Name -> Eff FromParserPure (Term d n)
resolveName ns x =
let here = addMods ns x in
if isJust $ lookup here !(getAt DEFS) then
pure $ FT here
else do
let ns :< _ = ns
| _ => throw $ TermNotInScope x
resolveName ns x
mutual
export
fromPTermWith : Context' BName d -> Context' BName n ->
PTerm -> Eff FromParserPure (Term d n)
fromPTermWith ds ns t0 = case t0 of
TYPE k =>
pure $ TYPE $ k
Pi pi x s t =>
Pi pi <$> fromPTermWith ds ns s
<*> fromPTermTScope ds ns [< x] t
Lam x s =>
Lam <$> fromPTermTScope ds ns [< x] s
s :@ t =>
map E $ (:@) <$> fromPTermElim ds ns s <*> fromPTermWith ds ns t
Sig x s t =>
Sig <$> fromPTermWith ds ns s <*> fromPTermTScope ds ns [< x] t
Pair s t =>
Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t
Case pi pair (r, ret) (CasePair (x, y) body) =>
2023-04-15 09:13:01 -04:00
map E $ CasePair pi
<$> fromPTermElim ds ns pair
<*> fromPTermTScope ds ns [< r] ret
<*> fromPTermTScope ds ns [< x, y] body
Case pi tag (r, ret) (CaseEnum arms) =>
2023-04-15 09:13:01 -04:00
map E $ CaseEnum pi
<$> fromPTermElim ds ns tag
<*> fromPTermTScope ds ns [< r] ret
<*> assert_total fromPTermEnumArms ds ns arms
2023-03-26 08:40:54 -04:00
Nat => pure Nat
Zero => pure Zero
Succ n => [|Succ $ fromPTermWith ds ns n|]
Case pi nat (r, ret) (CaseNat zer (s, pi', ih, suc)) =>
2023-04-15 09:13:01 -04:00
map E $ CaseNat pi 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
Enum strs =>
let set = SortedSet.fromList strs in
if length strs == length (SortedSet.toList set) then
pure $ Enum set
else
2023-03-31 13:23:30 -04:00
throw $ DuplicatesInEnum strs
Tag str => pure $ Tag str
Eq (i, ty) s t =>
Eq <$> fromPTermDScope ds ns [< i] ty
<*> fromPTermWith ds ns s
<*> fromPTermWith ds ns t
DLam i s =>
DLam <$> fromPTermDScope ds ns [< i] s
2023-03-31 13:11:35 -04:00
BOX q ty => BOX q <$> fromPTermWith ds ns ty
Box val => Box <$> fromPTermWith ds ns val
Case pi box (r, ret) (CaseBox b body) =>
2023-04-15 09:13:01 -04:00
map E $ CaseBox pi
2023-03-31 13:11:35 -04:00
<$> fromPTermElim ds ns box
<*> fromPTermTScope ds ns [< r] ret
<*> fromPTermTScope ds ns [< b] body
s :% p =>
map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p
V x =>
fromName (pure . E . B) (resolveName !(getAt NS) <=< avoidDim ds) ns x
s :# a =>
map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a
2023-04-15 09:13:01 -04:00
Coe (i, ty) p q val =>
map E $ Coe
<$> fromPTermDScope ds ns [< i] ty
<*> fromPDimWith ds p
<*> fromPDimWith ds q
<*> fromPTermWith ds ns val
Comp (i, ty) p q val r (j0, val0) (j1, val1) =>
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
private
fromPTermEnumArms : Context' BName d -> Context' BName n ->
List (TagVal, PTerm) ->
Eff FromParserPure (CaseEnumArms d n)
fromPTermEnumArms ds ns =
map SortedMap.fromList . traverse (traverse $ fromPTermWith ds ns)
private
fromPTermElim : Context' BName d -> Context' BName 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 name ds) (map name ns) in
throw $ AnnotationNeeded ctx t
where
name : BName -> BaseName
name = maybe Unused UN
-- [todo] use SN if the var is named but still unused
private
fromPTermTScope : {s : Nat} -> Context' BName d -> Context' BName n ->
SnocVect s BName -> PTerm ->
Eff FromParserPure (ScopeTermN s d n)
fromPTermTScope ds ns xs t =
if all isNothing xs then
SN <$> fromPTermWith ds ns t
else
ST (fromSnocVect $ map (maybe Unused UN) xs)
<$> fromPTermWith ds (ns ++ xs) t
private
fromPTermDScope : {s : Nat} -> Context' BName d -> Context' BName n ->
SnocVect s BName -> PTerm ->
Eff FromParserPure (DScopeTermN s d n)
fromPTermDScope ds ns xs t =
if all isNothing xs then
SN <$> fromPTermWith ds ns t
else
DST (fromSnocVect $ map (maybe Unused UN) xs)
<$> fromPTermWith (ds ++ xs) ns t
export %inline
fromPTerm : PTerm -> Eff FromParserPure (Term 0 0)
fromPTerm = fromPTermWith [<] [<]
export
2023-03-31 13:23:30 -04:00
globalPQty : Has (Except Error) fs =>
2023-04-01 13:16:43 -04:00
(q : Qty) -> Eff fs (So $ isGlobal q)
globalPQty pi = case choose $ isGlobal pi of
Left y => pure y
Right _ => throw $ QtyNotGlobal pi
2023-03-13 14:33:09 -04:00
export
fromPBaseNameNS : Has (StateL NS Mods) fs => PBaseName -> Eff fs Name
fromPBaseNameNS name = pure $ addMods !(getAt NS) $ fromPBaseName name
2023-03-13 14:33:09 -04:00
private
injTC : (Has (StateL DEFS Definitions) fs, Has (Except Error) fs) =>
2023-04-01 13:16:43 -04:00
TC a -> Eff fs a
2023-04-24 17:19:15 -04:00
injTC act = rethrow $ mapFst WrapTypeError $ runTC !(getAt DEFS) act
2023-03-31 13:23:30 -04:00
export covering
2023-04-01 13:16:43 -04:00
fromPDef : (Has (StateL DEFS Definitions) fs,
2023-03-31 13:23:30 -04:00
Has (StateL NS Mods) fs,
Has (Except Error) fs) =>
2023-04-01 13:16:43 -04:00
PDefinition -> Eff fs NDefinition
2023-03-13 14:33:09 -04:00
fromPDef (MkPDef qty pname ptype pterm) = do
name <- fromPBaseNameNS pname
2023-03-13 14:33:09 -04:00
qtyGlobal <- globalPQty qty
2023-04-01 13:16:43 -04:00
let gqty = Element qty qtyGlobal
let sqty = globalToSubj gqty
type <- lift $ traverse fromPTerm ptype
term <- lift $ fromPTerm pterm
2023-03-13 14:33:09 -04:00
case type of
Just type => do
injTC $ checkTypeC empty type Nothing
injTC $ ignore $ checkC empty sqty term type
2023-04-01 13:16:43 -04:00
let def = mkDef gqty type term
2023-03-31 13:23:30 -04:00
modifyAt DEFS $ insert name def
pure (name, def)
2023-03-13 14:33:09 -04:00
Nothing => do
let E elim = term | t => throw $ AnnotationNeeded empty t
2023-03-13 14:33:09 -04:00
res <- injTC $ inferC empty sqty elim
2023-04-01 13:16:43 -04:00
let def = mkDef gqty res.type term
2023-03-31 13:23:30 -04:00
modifyAt DEFS $ insert name def
pure (name, def)
export covering
2023-04-01 13:16:43 -04:00
fromPDecl : (Has (StateL DEFS Definitions) fs,
2023-03-31 13:23:30 -04:00
Has (StateL NS Mods) fs,
Has (Except Error) fs) =>
2023-04-01 13:16:43 -04:00
PDecl -> Eff fs (List NDefinition)
2023-03-31 13:23:30 -04:00
fromPDecl (PDef def) = singleton <$> fromPDef def
2023-03-13 14:33:09 -04:00
fromPDecl (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
2023-03-31 13:23:30 -04:00
export covering
loadFile : (Has IO fs,
Has (StateL SEEN SeenFiles) fs,
Has (Reader IncludePath) fs,
Has (Except Error) fs) =>
String -> Eff fs (Maybe String)
2023-03-13 14:33:09 -04:00
loadFile file =
2023-03-31 13:23:30 -04:00
if contains file !(getAt SEEN) then
2023-03-13 14:33:09 -04:00
pure Nothing
else do
2023-04-17 17:59:02 -04:00
Just ifile <- firstExists (map (</> file) !ask)
2023-03-31 13:23:30 -04:00
| Nothing => throw $ LoadError file FileNotFound
2023-04-17 17:59:02 -04:00
case !(readFile ifile) of
2023-03-31 13:23:30 -04:00
Right res => modifyAt SEEN (insert file) $> Just res
2023-04-17 17:59:02 -04:00
Left err => throw $ LoadError ifile err
2023-03-31 13:23:30 -04:00
parameters {auto _ : (Has IO fs,
Has (StateL SEEN SeenFiles) fs,
Has (Reader IncludePath) fs,
Has (Except Error) fs,
2023-04-01 13:16:43 -04:00
Has (StateL DEFS Definitions) fs,
2023-03-31 13:23:30 -04:00
Has (StateL NS Mods) fs)}
mutual
export covering
2023-04-01 13:16:43 -04:00
loadProcessFile : String -> Eff fs (List NDefinition)
2023-03-31 13:23:30 -04:00
loadProcessFile file =
case !(loadFile file) of
Just inp => do
2023-04-24 17:19:15 -04:00
tl <- either (throw . WrapParseError file) pure $ lexParseInput 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-04-01 13:16:43 -04:00
fromPTopLevel : PTopLevel -> Eff fs (List NDefinition)
2023-03-31 13:23:30 -04:00
fromPTopLevel (PD decl) = fromPDecl decl
fromPTopLevel (PLoad file) = loadProcessFile file
2023-03-13 14:33:09 -04:00
export
fromParserPure : Definitions ->
Eff FromParserPure a ->
Either Error (a, Definitions)
fromParserPure defs act =
extract $
runExcept $
evalStateAt NS [<] $
runStateAt DEFS defs act
2023-03-13 14:33:09 -04:00
export
2023-03-31 13:23:30 -04:00
fromParserIO : (MonadRec io, HasIO io) =>
2023-04-01 13:16:43 -04:00
IncludePath -> IORef SeenFiles -> IORef Definitions ->
2023-03-31 13:23:30 -04:00
FromParser a -> io (Either Error a)
fromParserIO inc seen defs act =
runIO $
runExcept $
evalStateAt NS [<] $
runStateIORefAt SEEN seen $
runStateIORefAt DEFS defs $
runReader inc act