quox/lib/Quox/Parser/FromParser.idr
2023-03-26 14:40:54 +02:00

271 lines
7.5 KiB
Idris

||| take freshly-parsed input, translate it to core, and check it
module Quox.Parser.FromParser
import Quox.Parser.Syntax
import Quox.Parser.Parser
import Quox.Typechecker
import Data.List
import Data.SnocVect
import public Control.Monad.Either
import public Control.Monad.State
import public Control.Monad.Reader
import System.File
import System.Path
%hide Context.(<$>)
%hide Context.(<*>)
public export
0 Defs : Type
Defs = Definitions Three
public export
data FromParserError =
AnnotationNeeded PTerm
| DuplicatesInEnum (List TagVal)
| DimNotInScope PBaseName
| QtyNotGlobal PQty
| DimNameInTerm PBaseName
| TypeError (Typing.Error Three)
| LoadError String FileError
| ParseError Parser.Error
public export
0 CanError : (Type -> Type) -> Type
CanError = MonadError FromParserError
public export
0 HasDefsRW : (Type -> Type) -> Type
HasDefsRW = MonadState Defs
public export
0 HasNamespace : (Type -> Type) -> Type
HasNamespace = MonadReader Mods
public export
0 LoadFile : (Type -> Type) -> Type
LoadFile m =
(HasIO m, MonadReader (List String) m, MonadState (SortedSet String) m)
-- reader for include paths, state for seen files
public export
0 FromParser : (Type -> Type) -> Type
FromParser m =
(CanError m, HasDefsRW m, HasNamespace m, LoadFile m)
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
fromPDimWith : CanError m =>
Context' BName d -> PDim -> m (Dim d)
fromPDimWith ds (K e) = pure $ K e
fromPDimWith ds (V i) =
fromBaseName (pure . B) (const $ throwError $ DimNotInScope i) ds i
private
avoidDim : CanError m => Context' BName d -> PName -> m (Term q d n)
avoidDim ds x =
fromName (const $ throwError $ DimNameInTerm x.base)
(pure . FT . fromPName) ds x
mutual
export
fromPTermWith : CanError m =>
Context' BName d -> Context' BName n ->
PTerm -> m (Term Three 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) =>
map E $ Base.CasePair pi
<$> fromPTermElim ds ns pair
<*> fromPTermTScope ds ns [< r] ret
<*> fromPTermTScope ds ns [< x, y] body
Case pi tag (r, ret) (CaseEnum arms) =>
map E $ Base.CaseEnum pi
<$> fromPTermElim ds ns tag
<*> fromPTermTScope ds ns [< r] ret
<*> assert_total fromPTermEnumArms ds ns arms
Nat => pure Nat
Zero => pure Zero
Succ n => [|Succ $ fromPTermWith ds ns n|]
Case pi nat (r, ret) (CaseNat zer (s, pi', ih, suc)) =>
Prelude.map E $ Base.CaseNat pi pi'
<$> 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
throwError $ 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
s :% p =>
map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p
V x =>
fromName (pure . E . B) (avoidDim ds) ns x
s :# a =>
map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a
private
fromPTermEnumArms : CanError m =>
Context' BName d -> Context' BName n ->
List (TagVal, PTerm) -> m (CaseEnumArms Three d n)
fromPTermEnumArms ds ns =
map SortedMap.fromList . traverse (traverse $ fromPTermWith ds ns)
private
fromPTermElim : CanError m =>
Context' BName d -> Context' BName n ->
PTerm -> m (Elim Three d n)
fromPTermElim ds ns e =
case !(fromPTermWith ds ns e) of
E e => pure e
_ => throwError $ AnnotationNeeded e
-- [todo] use SN if the var is named but still unused
private
fromPTermTScope : {s : Nat} -> CanError m =>
Context' BName d -> Context' BName n ->
SnocVect s BName ->
PTerm -> m (ScopeTermN s Three d n)
fromPTermTScope ds ns xs t =
if all isNothing xs then
SN <$> fromPTermWith ds ns t
else
SY (fromSnocVect $ map (maybe Unused UN) xs)
<$> fromPTermWith ds (ns ++ xs) t
private
fromPTermDScope : {s : Nat} -> CanError m =>
Context' BName d -> Context' BName n ->
SnocVect s BName ->
PTerm -> m (DScopeTermN s Three d n)
fromPTermDScope ds ns xs t =
if all isNothing xs then
SN <$> fromPTermWith ds ns t
else
SY (fromSnocVect $ map (maybe Unused UN) xs)
<$> fromPTermWith (ds ++ xs) ns t
export %inline
fromPTerm : CanError m => PTerm -> m (Term Three 0 0)
fromPTerm = fromPTermWith [<] [<]
export
globalPQty : CanError m => (q : PQty) -> m (IsGlobal q)
globalPQty pi = case isGlobal pi of
Yes y => pure y
No n => throwError $ QtyNotGlobal pi
export
fromPNameNS : HasNamespace m => PName -> m Name
fromPNameNS name = asks $ \ns => addMods ns $ fromPName name
private
injTC : (CanError m, HasDefsRW m) => (forall m'. CanTC Three m' => m' a) -> m a
injTC act =
either (throwError . TypeError) pure $
runReaderT {m = Either _} !get act
export
fromPDef : (CanError m, HasDefsRW m, HasNamespace m) => PDefinition -> m ()
fromPDef (MkPDef qty pname ptype pterm) = do
name <- fromPNameNS pname
qtyGlobal <- globalPQty qty
let sqty = globalToSubj $ Element qty qtyGlobal
type <- traverse fromPTerm ptype
term <- fromPTerm pterm
case type of
Just type => do
injTC $ checkTypeC empty type Nothing
injTC $ ignore $ checkC empty sqty term type
modify $ insert name $ mkDef qty type term
Nothing => do
let E elim = term | _ => throwError $ AnnotationNeeded pterm
res <- injTC $ inferC empty sqty elim
modify $ insert name $ mkDef qty res.type term
export
fromPDecl : FromParser m => PDecl -> m ()
fromPDecl (PDef def) = fromPDef def
fromPDecl (PNs ns) =
local (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls
export
loadFile : (LoadFile m, CanError m) => String -> m (Maybe String)
loadFile file =
if contains file !get then
pure Nothing
else do
Just file <- firstExists (map (</> file) !ask)
| Nothing => throwError $ LoadError file FileNotFound
case !(readFile file) of
Right res => pure $ Just res
Left err => throwError $ LoadError file err
||| populates the `defs` field of the state
export
fromPTopLevel : FromParser m => PTopLevel -> m ()
fromPTopLevel (PD decl) = fromPDecl decl
fromPTopLevel (PLoad file) =
case !(loadFile file) of
Just inp => do
tl <- either (throwError . ParseError) pure $ lexParseInput inp
traverse_ fromPTopLevel tl
Nothing => pure ()