quox/lib/Quox/Parser/FromParser.idr

||| 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


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

    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 $ mkDef0 qty type term
    Nothing => do
      let E elim = term | _ => throwError $ AnnotationNeeded pterm
      res <- injTC $ inferC empty sqty elim
      modify $ insert name $ mkDef0 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 ()