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.Typechecker
import Data.List

import public Control.Monad.Either
import public Control.Monad.State
import public Control.Monad.Reader


public export
data FromParserError =
    AnnotationNeeded PTerm
  | DuplicatesInEnum (List TagVal)
  | DimNotInScope PBaseName
  | QtyNotGlobal PQty
  | DimNameInTerm PBaseName

public export
interface LoadFile m where
  loadFile : (file : String) -> m PTopLevel

public export
0 CanError : (Type -> Type) -> Type
CanError = MonadError FromParserError

public export
0 HasNamespace : (Type -> Type) -> Type
HasNamespace = MonadReader Mods

public export
0 HasSeenFiles : (Type -> Type) -> Type
HasSeenFiles = MonadState (SortedSet String)

public export
0 FromParser : (Type -> Type) -> Type
FromParser m = (CanError m, HasNamespace m, HasSeenFiles 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 ->
                    Vect 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 (map (maybe Unused UN) xs) <$> fromPTermWith ds (ns <>< xs) t

  private
  fromPTermDScope : {s : Nat} -> CanError m =>
                    Context' BName d -> Context' BName n ->
                    Vect 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 (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



-- -- [todo] extend substitutions so they can do this injection. that's the sort of
-- -- thing they are for.
-- export
-- fromPDefinition : FromParser m => PDefinition -> m (Name, Definition Three)
-- fromPDefinition (MkPDef {name, qty, type, term}) =
--   pure (addMods !ask $ fromPName name, MkDef' {
--     qty, qtyGlobal = !(globalPQty qty),
--     type = T $ inject !(fromPTerm type),
--     term = Just $ T $ inject !(fromPTerm term)
--   })


-- export
-- fromPDecl : FromParser m => PDecl -> m (List (Name, Definition Three))
-- fromPDecl (PDef def) = singleton <$> fromPDefinition def
-- fromPDecl (PNs  ns)  = local (<+> ns.name) $
--   concat <$> assert_total traverse fromPDecl ns.decls


-- export covering
-- fromPTopLevel : (FromParser m, LoadFile m) =>
--                 PTopLevel -> m (List (Name, Definition Three))
-- fromPTopLevel (PD decl)    = fromPDecl decl
-- fromPTopLevel (PLoad file) =
--   if contains file !get then
--     pure []
--   else do
--     modify $ insert file
--     t <- loadFile file
--     fromPTopLevel t