{-# LANGUAGE TupleSections, NamedFieldPuns #-}

module Extract where

{- extract to Fomega

Examples:
---------

MiniAgda

  data Vec (A : Set) : Nat -> Set
  { vnil  : Vec A zero
  ; vcons : [n : Nat] -> (head : A) -> (tail : Vec A n) -> Vec A (suc n)
  } fields head, tail

  fun length : [A : Set] -> [n : Nat] -> Vec A n -> <n : Nat>
  { length .A .zero    (vnil A)         = zero
  ; length .A .(suc n) (vcons A n a as) = suc (length A n as)
  }

Fomega

  data Vec (A : Set) : Set
  { vnil  : Vec A
  ; vcons : (head : A) -> (tail : Vec A) -> Vec A
  }

  fun head : [A : Set] -> Vec A -> A
  { head (vcons 'head 'tail) = 'head
  }

  fun tail : [A : Set] -> Vec A -> A
  { head (vcons 'head 'tail) = 'tail
  }

  fun length : [A : Set] -> Vec A -> Nat
  { length [A]  vnil             = zero
  ; length [A] (vcons [.A] a as) = suc (length [A] as)
  }


Bidirectional extraction
========================

Types

  Base ::= D As         data type
         | ?            inexpressible type

  A,B ::= Base | A -> B | [x:K] -> B | [] -> B  with erasure markers
  A0, B0 ::= Base | A0 -> B0 | [x:K0] -> B0     without erasure markers

  |.| erase erasure markers

Inference mode:

  Term extraction:  Gamma |- t :> A  --> e    |Gamma| |- e : |A|
  Type extraction:  Gamma |- T :> K  --> A    |Gamma| |- A : |K|
  Kind extraction:  Gamma |- U :> [] --> K    |Gamma| |- K : []

Checking mode:

  Term extraction:  Gamma |- t <: A  --> e    |Gamma| |- e : |A|
  Type extraction:  Gamma |- T <: K  --> A    |Gamma| |- A : |K|
  Kind extraction:  Gamma |- U <: [] --> K    |Gamma| |- K : []

Type and kind extraction keep erasure markers!

Checking abstraction:

  Relevant abstraction:
  Gamma, x:A |- t <: B --> e
  --------------------------------
  Gamma |- \x.t <: A -> B --> \x.e

  Type abstraction:
  Gamma, x:K |- t <: B --> e : B0
  ----------------------------------------
  Gamma |- \[x].t <: [x:K] -> B --> \[x].e
      also \xt

  Irrelevant abstraction:
  Gamma |- t : B --> e
  -------------------------------
  Gamma |- \[x].t : [] -> B --> e
      also \xt

  Relevant abstraction at unknown type:
  Gamma, x:? |- t : ? --> e
  --------------------------
  Gamma |- \x.t : ? --> \x.e

  Irrelevant abstraction at unknown type:
  Gamma |- t : ? --> e
  -------------------------
  Gamma |- \[x].t : ? --> e

Checking by inference:

  Gamma |- t :> A --> e    e : |A| <: |B| --> e'
  ----------------------------------------------
  Gamma |- t <: B --> e' : B0

Casting:

  ------------------ A0 does not contain ?
  e : A0 <: A0 --> e

  ----------------------- A0 != B0 or one does contain ?
  e : A0 <: B0 --> cast e

Inferring variable:

  ----------------------------
  Gamma |- x :> Gamma(x) --> x

Inferring application:

  Relevant application:
  Gamma |- t :> A -> B --> f     Gamma |- u <: A --> e
  ----------------------------------------------------
  Gamma |- t u :> B --> f e

  Type application:
  Gamma |- t :> [x:K] -> B --> f   Gamma |- u <: K --> A
  ------------------------------------------------------
  Gamma |- t [u] :> : B[A/x] --> f [A]
      also  t u

  Irrelevant application:
  Gamma |- t :> [] -> B --> f
  ---------------------------
  Gamma |- t [u] :> B --> f
      also  t u

  Relevant application at unknown type:
  Gamma |- t :> ? --> f     Gamma |- u <: ? --> e
  -----------------------------------------------
  Gamma |- t u :> ? --> f e

  Irrelevant application at unknown type:
  Gamma |- t :> ? --> f
  -------------------------
  Gamma |- t [u] :> ? --> f



-}

import Prelude hiding (pi, null)

#if !MIN_VERSION_base(4,8,0)
import Control.Applicative ((<$>), (<*>))
#endif
import Control.Monad.Except (runExceptT)
import Control.Monad.Reader (runReaderT)
import Control.Monad.State  (runStateT)

-- import Data.Char
import qualified Data.Traversable as Traversable
import qualified Data.Maybe as Maybe

import Text.PrettyPrint

import Polarity as Pol
import Abstract
import Value
import Eval
import TCM
import TraceError
import Util

traceExtrM :: Monad m => String -> m ()
traceExtrM :: forall (m :: * -> *). Monad m => String -> m ()
traceExtrM String
s = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

runExtract :: Signature -> TypeCheck a -> IO (Either TraceError (a, TCState))
runExtract :: forall a.
Signature -> TypeCheck a -> IO (Either TraceError (a, TCState))
runExtract Signature
sig TypeCheck a
k = ExceptT TraceError IO (a, TCState)
-> IO (Either TraceError (a, TCState))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ReaderT TCContext (ExceptT TraceError IO) (a, TCState)
-> TCContext -> ExceptT TraceError IO (a, TCState)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (TypeCheck a
-> TCState
-> ReaderT TCContext (ExceptT TraceError IO) (a, TCState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT TypeCheck a
k (Signature -> TCState
initWithSig Signature
sig)) TCContext
emptyContext)

-- extraction

type FExpr        = Expr
type FDeclaration = Declaration
type FClause      = Clause
type FPattern     = Pattern
type FConstructor = Constructor
type FTypeSig     = TypeSig
type FFun         = Fun
type FTelescope   = Telescope

type FTVal        = TVal

extractDecls :: [EDeclaration] -> TypeCheck [FDeclaration]
extractDecls :: [EDeclaration] -> TypeCheck [EDeclaration]
extractDecls [EDeclaration]
ds = [[EDeclaration]] -> [EDeclaration]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[EDeclaration]] -> [EDeclaration])
-> StateT
     TCState
     (ReaderT TCContext (ExceptT TraceError IO))
     [[EDeclaration]]
-> TypeCheck [EDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (EDeclaration -> TypeCheck [EDeclaration])
-> [EDeclaration]
-> StateT
     TCState
     (ReaderT TCContext (ExceptT TraceError IO))
     [[EDeclaration]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM EDeclaration -> TypeCheck [EDeclaration]
extractDecl [EDeclaration]
ds

extractDecl :: EDeclaration -> TypeCheck [FDeclaration]
extractDecl :: EDeclaration -> TypeCheck [EDeclaration]
extractDecl EDeclaration
d =
  case EDeclaration
d of
    MutualDecl Bool
_ [EDeclaration]
ds -> [EDeclaration] -> TypeCheck [EDeclaration]
extractDecls [EDeclaration]
ds -- TODO!
    OverrideDecl{} -> String -> TypeCheck [EDeclaration]
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck [EDeclaration])
-> String -> TypeCheck [EDeclaration]
forall a b. (a -> b) -> a -> b
$ String
"extractDecls internal error: overrides impossible"
    MutualFunDecl Bool
_ Co
co [Fun]
funs -> Co -> [Fun] -> TypeCheck [EDeclaration]
extractFuns Co
co [Fun]
funs
    FunDecl Co
co Fun
fun -> Co -> Fun -> TypeCheck [EDeclaration]
extractFun Co
co Fun
fun
    LetDecl Bool
evl Name
x Telescope
tel (Just FKind
t) FKind
e | Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel -> Bool -> Name -> FKind -> FKind -> TypeCheck [EDeclaration]
extractLet Bool
evl Name
x FKind
t FKind
e
    PatternDecl{}    -> [EDeclaration] -> TypeCheck [EDeclaration]
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    DataDecl Name
n Sized
_ Co
co [Pol]
_ Telescope
tel FKind
ty [Constructor]
cs [Name]
fields -> Name
-> Co
-> Telescope
-> FKind
-> [Constructor]
-> TypeCheck [EDeclaration]
extractDataDecl Name
n Co
co Telescope
tel FKind
ty [Constructor]
cs

extractFuns :: Co -> [Fun] -> TypeCheck [FDeclaration]
extractFuns :: Co -> [Fun] -> TypeCheck [EDeclaration]
extractFuns Co
co [Fun]
funs = do
  funs <- [[Fun]] -> [Fun]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Fun]] -> [Fun])
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [[Fun]]
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Fun
 -> StateT
      TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun])
-> [Fun]
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [[Fun]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Fun
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun]
extractFunTypeSig [Fun]
funs
  concat <$> mapM (extractFun co) funs

extractFun :: Co -> Fun -> TypeCheck [FDeclaration]
extractFun :: Co -> Fun -> TypeCheck [EDeclaration]
extractFun Co
co (Fun (TypeSig Name
n FKind
t) Name
n' Arity
ar [Clause]
cls) = do
  tv <- FKind -> TypeCheck TVal
whnf' FKind
t
  cls <- concat <$> mapM (extractClause n tv) cls
  return [ FunDecl co $ Fun (TypeSig n t) n' ar cls
         -- , LetDecl False (TypeSig n' t) (Var n)  -- no longer needed, since n and n' print the same
         ]

{- OLD
extractFun :: Co -> Fun -> TypeCheck [FDeclaration]
extractFun co (TypeSig n t, (ar, cls)) = extractIfTerm n $ do
  tv0 <- whnf' t
  t <- extractType tv0
  setExtrTyp n t
  let n' = mkExtName n
  setExtrTyp n' t
  tv <- whnf' t
  cls <- concat <$> mapM (extractClause n tv) cls
  return [ FunDecl co (TypeSig n t, (ar, cls))
         , LetDecl False (TypeSig n' t) (Var n)
         ]
-}
{-
extractFunTypeSigs :: [Fun] -> TypeCheck [Fun]
extractFunTypeSigs = mapM extractFunTypeSig
-}

-- only extract type sigs
extractFunTypeSig :: Fun -> TypeCheck [Fun]
extractFunTypeSig :: Fun
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun]
extractFunTypeSig (Fun ts :: TySig FKind
ts@(TypeSig Name
n FKind
t) Name
n' Arity
ar [Clause]
cls) = Name
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun]
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun]
forall a. Name -> TypeCheck [a] -> TypeCheck [a]
extractIfTerm Name
n (StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun]
 -> StateT
      TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun])
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun]
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun]
forall a b. (a -> b) -> a -> b
$ do
  ts@(TypeSig n t) <- TySig FKind -> TypeCheck (TySig FKind)
extractTypeSig TySig FKind
ts
  setExtrTyp n' t
  return [Fun ts n' ar cls]

extractLet :: Bool -> Name -> Type -> Expr -> TypeCheck [FDeclaration]
extractLet :: Bool -> Name -> FKind -> FKind -> TypeCheck [EDeclaration]
extractLet Bool
evl Name
n FKind
t FKind
e = Name -> TypeCheck [EDeclaration] -> TypeCheck [EDeclaration]
forall a. Name -> TypeCheck [a] -> TypeCheck [a]
extractIfTerm Name
n (TypeCheck [EDeclaration] -> TypeCheck [EDeclaration])
-> TypeCheck [EDeclaration] -> TypeCheck [EDeclaration]
forall a b. (a -> b) -> a -> b
$ do
  TypeSig n t <- TySig FKind -> TypeCheck (TySig FKind)
extractTypeSig (Name -> FKind -> TySig FKind
forall a. Name -> a -> TySig a
TypeSig Name
n FKind
t)
  e <- extractCheck e =<< whnf' t
  return [LetDecl evl n emptyTel (Just t) e]

extractTypeSig :: TypeSig -> TypeCheck FTypeSig
extractTypeSig :: TySig FKind -> TypeCheck (TySig FKind)
extractTypeSig (TypeSig Name
n FKind
t) = do
  t <- TVal -> TypeCheck FKind
extractType (TVal -> TypeCheck FKind) -> TypeCheck TVal -> TypeCheck FKind
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< FKind -> TypeCheck TVal
whnf' FKind
t
  setExtrTyp n t
  return $ TypeSig n t

extractIfTerm :: Name -> TypeCheck [a] -> TypeCheck [a]
extractIfTerm :: forall a. Name -> TypeCheck [a] -> TypeCheck [a]
extractIfTerm Name
n TypeCheck [a]
cont = do
  k <- SigDef -> Kind
symbolKind (SigDef -> Kind)
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Kind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => Name -> m SigDef
lookupSymb Name
n
  if k == NoKind || lowerKind k == SortC Tm then cont else return []

extractDataDecl :: Name -> Co -> Telescope -> Type -> [Constructor] -> TypeCheck [FDeclaration]
extractDataDecl :: Name
-> Co
-> Telescope
-> FKind
-> [Constructor]
-> TypeCheck [EDeclaration]
extractDataDecl Name
n Co
co Telescope
tel FKind
ty [Constructor]
cs = do
  -- k    <- extrTyp <$> lookupSymb n
  tel' <- Telescope -> TypeCheck Telescope
extractKindTel Telescope
tel
  Just core <- addBinds tel $ extractKind =<< whnf' ty
  -- (_, core) = typeToTele' (length tel') k
  cs   <- mapM (extractConstructor tel) cs
  return [DataDecl n NotSized co [] tel' core cs []]

extractConstructor :: Telescope -> Constructor -> TypeCheck FConstructor
extractConstructor :: Telescope
-> Constructor
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) Constructor
extractConstructor Telescope
tel0 (Constructor QName
n ParamPats
pars FKind
t) = do
{- fails for HEq
  -- 2012-01-22: remove irrelevant parameters
  let tel = filter (\ (TBind _ dom) -> not $ erased $ decor dom)  tel0
-}
  let tel :: Telescope
tel = Telescope
tel0
  -- compute full extracted constructor type and add to the signature
  t' <- TVal -> TypeCheck FKind
extractType (TVal -> TypeCheck FKind) -> TypeCheck TVal -> TypeCheck FKind
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Env -> FKind -> TypeCheck TVal
whnf Env
forall a. Environ a
emptyEnv (Telescope -> FKind -> FKind
teleToTypeErase Telescope
tel FKind
t)
  setExtrTypQ n t'
  let (tel',core) = typeToTele' (size tel) t'
  return $ Constructor n pars core
  -- compute type minus telescope
  -- TypeSig n <$> (extractType =<< whnf' t)

extractClause :: Name -> FTVal -> Clause -> TypeCheck [FClause]
extractClause :: Name
-> TVal
-> Clause
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
extractClause Name
f TVal
tv (Clause TeleVal
_ [Pattern]
pl Maybe FKind
Nothing) = [Clause]
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- discard absurd clauses
extractClause Name
f TVal
tv cl :: Clause
cl@(Clause TeleVal
vtel [Pattern]
pl (Just FKind
rhs)) = do
  String
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) ()
forall (m :: * -> *). Monad m => String -> m ()
traceM (String
"extracting clause " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
render (Name -> Clause -> Doc
forall a. Pretty a => a -> Clause -> Doc
prettyClause Name
f Clause
cl)
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n at type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TVal -> String
forall a. Show a => a -> String
show TVal
tv)
{-
  tel <- introPatterns pl tv0 $ \ _ _ -> do
           vtel <- getContextTele
           extractTeleVal vtel
  addBinds tel $
-}
  [Pattern]
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
forall a. [Pattern] -> TypeCheck a -> TypeCheck a
introPatVars [Pattern]
pl (StateT
   TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
 -> StateT
      TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause])
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
forall a b. (a -> b) -> a -> b
$
    TVal
-> [Pattern]
-> ([Pattern]
    -> TVal
    -> StateT
         TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause])
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
forall a.
TVal
-> [Pattern] -> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
extractPatterns TVal
tv [Pattern]
pl (([Pattern]
  -> TVal
  -> StateT
       TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause])
 -> StateT
      TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause])
-> ([Pattern]
    -> TVal
    -> StateT
         TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause])
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
forall a b. (a -> b) -> a -> b
$ \ [Pattern]
pl TVal
tv -> do
      rhs <- FKind -> TVal -> TypeCheck FKind
extractCheck FKind
rhs TVal
tv
      return [Clause vtel pl (Just rhs)] -- TODO: return FTelescope (type!)

-- the pattern variables are already in context
extractPatterns :: FTVal -> [Pattern] ->
                   ([FPattern] -> FTVal -> TypeCheck a) -> TypeCheck a
extractPatterns :: forall a.
TVal
-> [Pattern] -> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
extractPatterns TVal
tv [] [Pattern] -> TVal -> TypeCheck a
cont = [Pattern] -> TVal -> TypeCheck a
cont [] TVal
tv
extractPatterns TVal
tv (Pattern
p:[Pattern]
ps) [Pattern] -> TVal -> TypeCheck a
cont =
  TVal
-> Pattern -> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
forall a.
TVal
-> Pattern -> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
extractPattern TVal
tv Pattern
p (([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a)
-> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ [Pattern]
pl TVal
tv ->
    TVal
-> [Pattern] -> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
forall a.
TVal
-> [Pattern] -> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
extractPatterns TVal
tv [Pattern]
ps (([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a)
-> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ [Pattern]
ps TVal
tv ->
      [Pattern] -> TVal -> TypeCheck a
cont ([Pattern]
pl [Pattern] -> [Pattern] -> [Pattern]
forall a. [a] -> [a] -> [a]
++ [Pattern]
ps) TVal
tv

extractPattern :: FTVal -> Pattern ->
                  ([FPattern] -> FTVal -> TypeCheck a) -> TypeCheck a
extractPattern :: forall a.
TVal
-> Pattern -> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
extractPattern TVal
tv Pattern
p [Pattern] -> TVal -> TypeCheck a
cont = do
  String
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) ()
forall (m :: * -> *). Monad m => String -> m ()
traceM (String
"extracting pattern " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
render (Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
p) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" at type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TVal -> String
forall a. Show a => a -> String
show TVal
tv)
  fv <- TVal -> TypeCheck FunView
funView TVal
tv
  case fv of
    EraseArg TVal
tv -> [Pattern] -> TVal -> TypeCheck a
cont [] TVal
tv  -- skip erased patterns

    Forall Name
x Domain
dom TVal
fv -> do
      xv <- FKind -> TypeCheck TVal
whnf' (Pattern -> FKind
patternToExpr Pattern
p) -- pattern variables are already in scope
      bv <- app fv xv -- TODO!
      case p of
        ErasedP (VarP Name
y) -> Name -> Domain -> TypeCheck a -> TypeCheck a
forall a.
Name
-> Domain
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. MonadCxt m => Name -> Domain -> m a -> m a
setTypeOfName Name
y Domain
dom (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ [Pattern] -> TVal -> TypeCheck a
cont [] TVal
bv
        Pattern
_ -> [Pattern] -> TVal -> TypeCheck a
cont [] TVal
bv
{-
    Forall x ki env t -> new x ki $ \ xv ->
      cont [] =<< whnf (update env x xv) t -- TODO!
-}
    Arrow TVal
av TVal
bv -> TVal -> Pattern -> ([Pattern] -> TypeCheck a) -> TypeCheck a
forall a.
TVal -> Pattern -> ([Pattern] -> TypeCheck a) -> TypeCheck a
extractPattern' TVal
av Pattern
p (([Pattern] -> TVal -> TypeCheck a)
-> TVal -> [Pattern] -> TypeCheck a
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Pattern] -> TVal -> TypeCheck a
cont TVal
bv)

extractPattern' :: FTVal -> Pattern ->
                  ([FPattern] -> TypeCheck a) -> TypeCheck a
extractPattern' :: forall a.
TVal -> Pattern -> ([Pattern] -> TypeCheck a) -> TypeCheck a
extractPattern' TVal
av Pattern
p [Pattern] -> TypeCheck a
cont =
      case Pattern
p of
        VarP Name
y -> Name -> Domain -> TypeCheck a -> TypeCheck a
forall a.
Name
-> Domain
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. MonadCxt m => Name -> Domain -> m a -> m a
setTypeOfName Name
y (TVal -> Domain
forall a. a -> Dom a
defaultDomain TVal
av) (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$
          [Pattern] -> TypeCheck a
cont [Name -> Pattern
forall e. Name -> Pat e
VarP Name
y]
        PairP Pattern
p1 Pattern
p2 -> do
          view <- TVal -> TypeCheck ProdView
prodView TVal
av
          -- hack to avoid IMPOSSIBLE
          let (av1, av2) = case view of
                             Prod TVal
av1 TVal
av2 -> (TVal
av1, TVal
av2)
                             ProdView
_ -> (TVal
av, TVal
av) -- HACK
          extractPattern' av1 p1 $ \ [Pattern]
ps1 -> do
            TVal -> Pattern -> ([Pattern] -> TypeCheck a) -> TypeCheck a
forall a.
TVal -> Pattern -> ([Pattern] -> TypeCheck a) -> TypeCheck a
extractPattern' TVal
av2 Pattern
p2 (([Pattern] -> TypeCheck a) -> TypeCheck a)
-> ([Pattern] -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ [Pattern]
ps2 ->
               let ps :: [Pat e] -> [Pat e] -> [Pat e]
ps [] [Pat e]
ps2    = [Pat e]
ps2
                   ps [Pat e]
ps1 []    = [Pat e]
ps1
                   ps [Pat e
p1] [Pat e
p2] = [Pat e -> Pat e -> Pat e
forall e. Pat e -> Pat e -> Pat e
PairP Pat e
p1 Pat e
p2]
               in  [Pattern] -> TypeCheck a
cont ([Pattern] -> TypeCheck a) -> [Pattern] -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ [Pattern] -> [Pattern] -> [Pattern]
forall {e}. [Pat e] -> [Pat e] -> [Pat e]
ps [Pattern]
ps1 [Pattern]
ps2

{-
          case view of
            Prod av1 av2 ->
              extractPattern' av1 p1 $ \ [p1] -> do
                extractPattern' av2 p2 $ \ [p2] -> cont [PairP p1 p2]
            _ -> throwErrorMsg $ "extractPattern': IMPOSSIBLE: pattern " ++
                          show p ++ " : " ++ show av
-}
        ConP PatternInfo
pi QName
n [Pattern]
ps -> do
--          tv <- whnf' =<< extrTyp <$> lookupSymb n
          tv <- QName -> TVal -> TypeCheck TVal
extrConType QName
n TVal
av
          extractPatterns tv ps $ \ [Pattern]
ps TVal
_ ->
            [Pattern] -> TypeCheck a
cont [PatternInfo -> QName -> [Pattern] -> Pattern
forall e. PatternInfo -> QName -> [Pat e] -> Pat e
ConP PatternInfo
pi QName
n [Pattern]
ps]
        Pattern
_ -> [Pattern] -> TypeCheck a
cont []

extrConType :: QName -> FTVal -> TypeCheck FTVal
extrConType :: QName -> TVal -> TypeCheck TVal
extrConType QName
c TVal
av = do
  ConSig { conPars, extrTyp, dataPars } <- QName
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => QName -> m SigDef
lookupSymbQ QName
c
  traceExtrM ("extrConType " ++ show c ++ " has extrTyp = " ++ show extrTyp)
  tv <- whnf' extrTyp
  numPars <- maybe (return dataPars) (const $ throwErrorMsg $ "NYI: extrConType for pattern parameters") conPars
  case numPars of
   Int
0 -> TVal -> TypeCheck TVal
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return TVal
tv
   Int
_ -> do
    case TVal
av of
      VApp (VDef (DefId IdKind
DatK QName
d)) [TVal]
vs -> do
        DataSig { positivity } <- QName
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => QName -> m SigDef
lookupSymbQ QName
d
        traceExtrM ("extrConType " ++ show c ++ "; data type has positivity = " ++ show positivity)
        let pars a
0 [pol]
pols [TVal]
vs = []
            pars a
n (pol
pol:[pol]
pols) [TVal]
vs | pol -> Bool
forall pol. Polarity pol => pol -> Bool
erased pol
pol = TVal
VIrr TVal -> [TVal] -> [TVal]
forall a. a -> [a] -> [a]
: a -> [pol] -> [TVal] -> [TVal]
pars (a
na -> a -> a
forall a. Num a => a -> a -> a
-a
1) [pol]
pols [TVal]
vs
            pars a
n (pol
pol:[pol]
pols) (TVal
v:[TVal]
vs) = TVal
v TVal -> [TVal] -> [TVal]
forall a. a -> [a] -> [a]
: a -> [pol] -> [TVal] -> [TVal]
pars (a
na -> a -> a
forall a. Num a => a -> a -> a
-a
1) [pol]
pols [TVal]
vs
            pars a
n [pol]
pols [TVal]
vs = String -> [TVal]
forall a. HasCallStack => String -> a
error (String -> [TVal]) -> String -> [TVal]
forall a b. (a -> b) -> a -> b
$ String
"pars " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ [pol] -> String
forall a. Show a => a -> String
show [pol]
pols String -> String -> String
forall a. [a] -> [a] -> [a]
++ [TVal] -> String
forall a. Show a => a -> String
show [TVal]
vs
        piApps tv $ pars numPars positivity $ vs ++ repeat VIrr
{-
        let (pars, inds) = splitAt numPars vs
        piApps tv pars
-}
      TVal
_ -> TVal -> [TVal] -> TypeCheck TVal
piApps TVal
tv ([TVal] -> TypeCheck TVal) -> [TVal] -> TypeCheck TVal
forall a b. (a -> b) -> a -> b
$ Int -> TVal -> [TVal]
forall a. Int -> a -> [a]
replicate Int
numPars TVal
VIrr
--      _ -> throwErrorMsg $ "extrConType " ++ show c ++ ": expected datatype, found " ++ show av

-- extracting a term from a term -------------------------------------

extractInfer :: Expr -> TypeCheck (FExpr, FTVal)
extractInfer :: FKind -> TypeCheck (FKind, TVal)
extractInfer FKind
e = do
  case FKind
e of

    Var Name
x -> (Name -> FKind
Var Name
x,) (TVal -> (FKind, TVal))
-> (CxtE Domain -> TVal) -> CxtE Domain -> (FKind, TVal)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Domain -> TVal
forall a. Dom a -> a
typ (Domain -> TVal) -> (CxtE Domain -> Domain) -> CxtE Domain -> TVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtE Domain -> Domain
forall a. CxtE a -> a
domain (CxtE Domain -> (FKind, TVal))
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) (CxtE Domain)
-> TypeCheck (FKind, TVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) (CxtE Domain)
forall (m :: * -> *). MonadCxt m => Name -> m (CxtE Domain)
lookupName1 Name
x

    App FKind
f FKind
e0 -> do
      let (Bool
er, FKind
e) = FKind -> (Bool, FKind)
isErasedExpr FKind
e0
      (f, tv) <- FKind -> TypeCheck (FKind, TVal)
extractInfer FKind
f
      fv <- funView tv
      case fv of
        EraseArg TVal
bv -> (FKind, TVal) -> TypeCheck (FKind, TVal)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FKind
f,TVal
bv)
        Forall Name
x Domain
dom TVal
fv -> do
          e <- FKind -> TVal -> TypeCheck FKind
extractTypeAt FKind
e (Domain -> TVal
forall a. Dom a -> a
typ Domain
dom)
          bv <- app fv =<< whnf' e
          return $ (App f (erasedExpr e), bv)
        Arrow TVal
av TVal
bv -> (FKind, TVal) -> TypeCheck (FKind, TVal)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (if Bool
er then FKind
f else FKind -> FKind -> FKind
App FKind
f FKind
e, TVal
bv)
        FunView
NotFun -> (FKind, TVal) -> TypeCheck (FKind, TVal)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (if Bool
er then FKind
f else FKind -> FKind
castExpr FKind
f FKind -> FKind -> FKind
`App` FKind
e, TVal
VIrr)

    Def DefId
f -> (DefId -> FKind
Def DefId
f,) (TVal -> (FKind, TVal))
-> TypeCheck TVal -> TypeCheck (FKind, TVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do (FKind -> TypeCheck TVal
whnf' (FKind -> TypeCheck TVal)
-> (SigDef -> FKind) -> SigDef -> TypeCheck TVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigDef -> FKind
extrTyp) (SigDef -> TypeCheck TVal)
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
-> TypeCheck TVal
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => QName -> m SigDef
lookupSymbQ (DefId -> QName
idName DefId
f)

    Pair{} -> String -> TypeCheck (FKind, TVal)
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck (FKind, TVal))
-> String -> TypeCheck (FKind, TVal)
forall a b. (a -> b) -> a -> b
$ String
"extractInfer: IMPOSSIBLE: pair " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FKind -> String
forall a. Show a => a -> String
show FKind
e
    -- other expressions are erased or types

    FKind
_ -> (FKind, TVal) -> TypeCheck (FKind, TVal)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FKind
Irr, TVal
VIrr)

extractCheck :: Expr -> FTVal -> TypeCheck (FExpr)
extractCheck :: FKind -> TVal -> TypeCheck FKind
extractCheck FKind
e TVal
tv = do
  case FKind
e of
    Lam Dec
dec Name
y FKind
e -> do
      fv <- TVal -> TypeCheck FunView
funView TVal
tv
      case fv of
        EraseArg TVal
bv        -> FKind -> TVal -> TypeCheck FKind
extractCheck FKind
e TVal
bv -- discard lambda
        Forall Name
x Domain
dom TVal
fv    ->
          Dec -> Name -> FKind -> FKind
Lam (Domain -> Dec
forall a. Dom a -> Dec
decor Domain
dom) Name
y (FKind -> FKind) -> TypeCheck FKind -> TypeCheck FKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
            Name
-> Domain -> (Int -> TVal -> TypeCheck FKind) -> TypeCheck FKind
forall a.
Name
-> Domain
-> (Int
    -> TVal
    -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a.
MonadCxt m =>
Name -> Domain -> (Int -> TVal -> m a) -> m a
newWithGen Name
y Domain
dom ((Int -> TVal -> TypeCheck FKind) -> TypeCheck FKind)
-> (Int -> TVal -> TypeCheck FKind) -> TypeCheck FKind
forall a b. (a -> b) -> a -> b
$ \ Int
i TVal
xv ->
              FKind -> TVal -> TypeCheck FKind
extractCheck FKind
e (TVal -> TypeCheck FKind) -> TypeCheck TVal -> TypeCheck FKind
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TVal -> TVal -> TypeCheck TVal
app TVal
fv (Int -> TVal
VGen Int
i) -- no eta-expansion
        Arrow TVal
av TVal
bv        ->
          if Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased Dec
dec then FKind -> TVal -> TypeCheck FKind
extractCheck FKind
e TVal
bv
           else Dec -> Name -> FKind -> FKind
Lam Dec
dec Name
y (FKind -> FKind) -> TypeCheck FKind -> TypeCheck FKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
             Name -> Domain -> TypeCheck FKind -> TypeCheck FKind
forall a.
Name
-> Domain
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. MonadCxt m => Name -> Domain -> m a -> m a
new' Name
y (TVal -> Domain
forall a. a -> Dom a
defaultDomain TVal
av) (TypeCheck FKind -> TypeCheck FKind)
-> TypeCheck FKind -> TypeCheck FKind
forall a b. (a -> b) -> a -> b
$
               FKind -> TVal -> TypeCheck FKind
extractCheck FKind
e TVal
bv
        FunView
NotFun            -> FKind -> FKind
castExpr (FKind -> FKind) -> TypeCheck FKind -> TypeCheck FKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          if Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased Dec
dec then FKind -> TVal -> TypeCheck FKind
extractCheck FKind
e TVal
VIrr
           else Dec -> Name -> FKind -> FKind
Lam Dec
dec Name
y (FKind -> FKind) -> TypeCheck FKind -> TypeCheck FKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
             Name -> Domain -> TypeCheck FKind -> TypeCheck FKind
forall a.
Name
-> Domain
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. MonadCxt m => Name -> Domain -> m a -> m a
new' Name
y (TVal -> Domain
forall a. a -> Dom a
defaultDomain TVal
VIrr) (TypeCheck FKind -> TypeCheck FKind)
-> TypeCheck FKind -> TypeCheck FKind
forall a b. (a -> b) -> a -> b
$
               FKind -> TVal -> TypeCheck FKind
extractCheck FKind
e TVal
VIrr

    LLet (TBind Name
x Dom (Maybe FKind)
dom0) Telescope
tel FKind
e1 FKind
e2 | Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel -> do
      let dom :: Dom FKind
dom = (Maybe FKind -> FKind) -> Dom (Maybe FKind) -> Dom FKind
forall a b. (a -> b) -> Dom a -> Dom b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe FKind -> FKind
forall a. HasCallStack => Maybe a -> a
Maybe.fromJust Dom (Maybe FKind)
dom0
      if Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Dom FKind -> Dec
forall a. Dom a -> Dec
decor Dom FKind
dom) then FKind -> TVal -> TypeCheck FKind
extractCheck FKind
e2 TVal
tv else do -- discard let
       vdom <- (FKind -> TypeCheck TVal)
-> Dom FKind
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) Domain
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom a -> m (Dom b)
Traversable.mapM FKind -> TypeCheck TVal
whnf' Dom FKind
dom         -- MiniAgda type val
       dom  <- Traversable.mapM extractType vdom  -- Fomega type
       vdom <- Traversable.mapM whnf' dom         -- Fomega type val
       e1  <- extractCheck e1 (typ vdom)
       LLet (TBind x (fmap Just dom)) emptyTel e1 <$> do
         new' x vdom $ extractCheck e2 tv

    Pair FKind
e1 FKind
e2 -> do
      view <- TVal -> TypeCheck ProdView
prodView TVal
tv
      let (av1,av2) = case view of
                        Prod TVal
av1 TVal
av2 -> (TVal
av1, TVal
av2)
                        ProdView
_ -> (TVal
tv,TVal
tv) -- HACK!!
      Pair <$> extractCheck e1 av1 <*> extractCheck e2 av2
{-
      case view of
        Prod av1 av2 -> Pair <$> extractCheck e1 av1 <*> extractCheck e2 av2
        _ -> throwErrorMsg $ "extractCheck: tuple type expected " ++ show e ++ " : " ++ show tv
-}

    -- TODO: case

    FKind
_ -> TypeCheck FKind
fallback
  where
    fallback :: TypeCheck FKind
fallback = do
      (e,tv') <- FKind -> TypeCheck (FKind, TVal)
extractInfer FKind
e
      insertCast e tv tv'

insertCast :: FExpr -> FTVal -> FTVal -> TypeCheck FExpr
insertCast :: FKind -> TVal -> TVal -> TypeCheck FKind
insertCast FKind
e TVal
tv1 TVal
tv2 = TVal -> TVal -> TypeCheck FKind
forall {m :: * -> *}. Monad m => TVal -> TVal -> m FKind
loop TVal
tv1 TVal
tv2 where
  loop :: TVal -> TVal -> m FKind
loop TVal
tv1 TVal
tv2 =
    case (TVal
tv1,TVal
tv2) of
      (TVal
VIrr,TVal
_) -> FKind -> m FKind
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (FKind -> m FKind) -> FKind -> m FKind
forall a b. (a -> b) -> a -> b
$ FKind -> FKind
castExpr FKind
e
      (TVal
_,TVal
VIrr) -> FKind -> m FKind
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (FKind -> m FKind) -> FKind -> m FKind
forall a b. (a -> b) -> a -> b
$ FKind -> FKind
castExpr FKind
e
      (TVal, TVal)
_  -> FKind -> m FKind
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return FKind
e -- TODO!

funView :: FTVal -> TypeCheck FunView
funView :: TVal -> TypeCheck FunView
funView TVal
tv =
  case TVal
tv of
    -- erasure mark
    VQuant PiSigma
Pi Name
x Domain
dom TVal
fv | Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Domain -> Dec
forall a. Dom a -> Dec
decor Domain
dom) Bool -> Bool -> Bool
&& Domain -> TVal
forall a. Dom a -> a
typ Domain
dom TVal -> TVal -> Bool
forall a. Eq a => a -> a -> Bool
== TVal
VIrr ->
      TVal -> FunView
EraseArg (TVal -> FunView) -> TypeCheck TVal -> TypeCheck FunView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVal -> TVal -> TypeCheck TVal
app TVal
fv TVal
VIrr
    -- forall
    VQuant PiSigma
Pi Name
x Domain
dom TVal
fv | Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Domain -> Dec
forall a. Dom a -> Dec
decor Domain
dom) ->
      FunView -> TypeCheck FunView
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FunView -> TypeCheck FunView) -> FunView -> TypeCheck FunView
forall a b. (a -> b) -> a -> b
$ Name -> Domain -> TVal -> FunView
Forall Name
x Domain
dom TVal
fv
    -- function type
    VQuant PiSigma
Pi Name
x Domain
dom TVal
fv ->
      TVal -> TVal -> FunView
Arrow (Domain -> TVal
forall a. Dom a -> a
typ Domain
dom) (TVal -> FunView) -> TypeCheck TVal -> TypeCheck FunView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVal -> TVal -> TypeCheck TVal
app TVal
fv TVal
VIrr
    -- any other type can be a function type, but this needs casts!
    TVal
_ -> FunView -> TypeCheck FunView
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return FunView
NotFun -- $ Arrow VIrr VIrr

data FunView
  = Arrow    FTVal FTVal            -- A -> B
  | Forall   Name Domain FTVal      -- forall X:K. A
  | EraseArg FTVal                  -- [] -> B
  | NotFun                          -- ()

prodView :: FTVal -> TypeCheck ProdView
prodView :: TVal -> TypeCheck ProdView
prodView TVal
tv =
  case TVal
tv of
    VQuant PiSigma
Sigma Name
x Domain
dom TVal
fv -> TVal -> TVal -> ProdView
Prod (Domain -> TVal
forall a. Dom a -> a
typ Domain
dom) (TVal -> ProdView) -> TypeCheck TVal -> TypeCheck ProdView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVal -> TVal -> TypeCheck TVal
app TVal
fv TVal
VIrr
    TVal
_                     -> ProdView -> TypeCheck ProdView
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProdView -> TypeCheck ProdView) -> ProdView -> TypeCheck ProdView
forall a b. (a -> b) -> a -> b
$ ProdView
NotProd

data ProdView
  = Prod FTVal FTVal -- A * B
  | NotProd

-- extracting a kind from a value ------------------------------------

type FKind = Expr -- FKind ::= Set | FKind -> FKind | [Irr] -> FKind

star :: FKind
star :: FKind
star = Sort FKind -> FKind
Sort (Sort FKind -> FKind) -> Sort FKind -> FKind
forall a b. (a -> b) -> a -> b
$ FKind -> Sort FKind
forall a. a -> Sort a
Set FKind
Zero

extractSet :: Sort Val -> Maybe FKind
extractSet :: Sort TVal -> Maybe FKind
extractSet Sort TVal
s =
  case Sort TVal
s of
    SortC Class
_ -> Maybe FKind
forall a. Maybe a
Nothing
    Set TVal
_   -> FKind -> Maybe FKind
forall a. a -> Maybe a
Just (FKind -> Maybe FKind) -> FKind -> Maybe FKind
forall a b. (a -> b) -> a -> b
$ FKind
star
    CoSet TVal
_ -> FKind -> Maybe FKind
forall a. a -> Maybe a
Just (FKind -> Maybe FKind) -> FKind -> Maybe FKind
forall a b. (a -> b) -> a -> b
$ FKind
star

-- keep irrelevant entries
extractKindTel :: Telescope -> TypeCheck FTelescope
extractKindTel :: Telescope -> TypeCheck Telescope
extractKindTel (Telescope [TBind]
tel) = [TBind] -> Telescope
Telescope ([TBind] -> Telescope)
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind]
-> TypeCheck Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TBind]
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind]
loop [TBind]
tel where
  loop :: [TBind]
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind]
loop [] = [TBind]
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind]
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  loop (TBind Name
x Dom FKind
dom : [TBind]
tel) = do
    dom  <- (FKind -> TypeCheck TVal)
-> Dom FKind
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) Domain
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom a -> m (Dom b)
Traversable.mapM FKind -> TypeCheck TVal
whnf' Dom FKind
dom
    dom' <- extractKindDom dom
    if erased (decor dom') then
      newIrr x $
        (TBind x dom' :) <$> loop tel
     else newTyVar x (typ dom') $ \ Int
i -> do
        x <- Int
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Name
forall (m :: * -> *). MonadCxt m => Int -> m Name
nameOfGen Int
i
        (TBind x dom' :) <$> loop tel

{-
-- keep irrelevant entries
extractKindTel :: Telescope -> TypeCheck FTelescope
extractKindTel tel = do
  tv     <- whnf' (teleToType tel star)
  Just k <- extractKind tv
  let (tel, s) = typeToTele k
  return tel
  -- throw away erasure marks
  -- return $ filter (\ tb -> not $ erased $ decor $ boundDom tb) tel
-}

extractKindDom :: Domain -> TypeCheck (Dom FKind)
extractKindDom :: Domain
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) (Dom FKind)
extractKindDom Domain
dom =
  Dom FKind -> (FKind -> Dom FKind) -> Maybe FKind -> Dom FKind
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (FKind -> Dom FKind
forall a. a -> Dom a
defaultIrrDom FKind
Irr) FKind -> Dom FKind
forall a. a -> Dom a
defaultDomain (Maybe FKind -> Dom FKind)
-> TypeCheck (Maybe FKind)
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) (Dom FKind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    if Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Domain -> Dec
forall a. Dom a -> Dec
decor Domain
dom) then Maybe FKind -> TypeCheck (Maybe FKind)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FKind
forall a. Maybe a
Nothing
     else TVal -> TypeCheck (Maybe FKind)
extractKind (Domain -> TVal
forall a. Dom a -> a
typ Domain
dom)

extractKind :: TVal -> TypeCheck (Maybe FKind)
extractKind :: TVal -> TypeCheck (Maybe FKind)
extractKind TVal
tv =
  case TVal
tv of
    VSort Sort TVal
s -> Maybe FKind -> TypeCheck (Maybe FKind)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe FKind -> TypeCheck (Maybe FKind))
-> Maybe FKind -> TypeCheck (Maybe FKind)
forall a b. (a -> b) -> a -> b
$ Sort TVal -> Maybe FKind
extractSet Sort TVal
s
    VMeasured Measure TVal
mu TVal
vb -> TVal -> TypeCheck (Maybe FKind)
extractKind TVal
vb
    VGuard Bound TVal
beta TVal
vb -> TVal -> TypeCheck (Maybe FKind)
extractKind TVal
vb
    VQuant PiSigma
Pi Name
x Domain
dom TVal
fv -> Name
-> Domain -> TypeCheck (Maybe FKind) -> TypeCheck (Maybe FKind)
forall a.
Name
-> Domain
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. MonadCxt m => Name -> Domain -> m a -> m a
new' Name
x Domain
dom (TypeCheck (Maybe FKind) -> TypeCheck (Maybe FKind))
-> TypeCheck (Maybe FKind) -> TypeCheck (Maybe FKind)
forall a b. (a -> b) -> a -> b
$ do
       bv  <- TVal -> TVal -> TypeCheck TVal
app TVal
fv TVal
VIrr
       mk' <- extractKind bv
       case mk' of
         Maybe FKind
Nothing -> Maybe FKind -> TypeCheck (Maybe FKind)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FKind
forall a. Maybe a
Nothing
         Just FKind
k' -> do
           dom' <- Domain
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) (Dom FKind)
extractKindDom Domain
dom
           let x = String -> Name
fresh String
""
           return $ Just $ pi (TBind x dom') k'
    TVal
_ -> Maybe FKind -> TypeCheck (Maybe FKind)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FKind
forall a. Maybe a
Nothing

-- extracting a type constructor from a value ------------------------

type FType = Expr
{- FType ::= Irr                 -- not expressible in Fomega
           | D FTypes            -- data type
           | X FTypes            -- type variable
           | FType -> FType      -- function type
           | [X:FKind] -> FType  -- polymorphic type
           | [Irr] -> FType      -- erasure marker
 -}

-- tyVarName i = fresh $ "a" ++ show i

newTyVar :: Name -> FKind -> (Int -> TypeCheck a) -> TypeCheck a
newTyVar :: forall a. Name -> FKind -> (Int -> TypeCheck a) -> TypeCheck a
newTyVar Name
x FKind
k Int -> TypeCheck a
cont = Name -> Domain -> (Int -> TVal -> TypeCheck a) -> TypeCheck a
forall a.
Name
-> Domain
-> (Int
    -> TVal
    -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a.
MonadCxt m =>
Name -> Domain -> (Int -> TVal -> m a) -> m a
newWithGen Name
x (TVal -> Domain
forall a. a -> Dom a
defaultDomain (Env -> FKind -> TVal
VClos Env
forall a. Environ a
emptyEnv FKind
k)) ((Int -> TVal -> TypeCheck a) -> TypeCheck a)
-> (Int -> TVal -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$
  \ Int
i TVal
_ -> Int -> TypeCheck a
cont Int
i                  -- store kinds unevaluated

addFKindTel :: FTelescope -> TypeCheck a -> TypeCheck a
addFKindTel :: forall a. Telescope -> TypeCheck a -> TypeCheck a
addFKindTel (Telescope [TBind]
tel) = [TBind] -> TypeCheck a -> TypeCheck a
forall {a}. [TBind] -> TypeCheck a -> TypeCheck a
loop [TBind]
tel where
  loop :: [TBind] -> TypeCheck a -> TypeCheck a
loop []                  TypeCheck a
cont = TypeCheck a
cont
  loop (TBind Name
x Dom FKind
dom : [TBind]
tel) TypeCheck a
cont = Name -> FKind -> (Int -> TypeCheck a) -> TypeCheck a
forall a. Name -> FKind -> (Int -> TypeCheck a) -> TypeCheck a
newTyVar Name
x (Dom FKind -> FKind
forall a. Dom a -> a
typ Dom FKind
dom) ((Int -> TypeCheck a) -> TypeCheck a)
-> (Int -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ Int
_ ->
    [TBind] -> TypeCheck a -> TypeCheck a
loop [TBind]
tel TypeCheck a
cont

extractTeleVal :: TeleVal -> TypeCheck FTelescope
extractTeleVal :: TeleVal -> TypeCheck Telescope
extractTeleVal = [TBind] -> Telescope
Telescope ([TBind] -> Telescope)
-> (TeleVal
    -> StateT
         TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind])
-> TeleVal
-> TypeCheck Telescope
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> TeleVal
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind]
loop where
  loop :: TeleVal
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind]
loop []          = [TBind]
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind]
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  loop (TBinding TVal
tb : TeleVal
vtel) = do
    tb <- (TVal -> TypeCheck FKind)
-> TBinding TVal
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) TBind
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TBinding a -> m (TBinding b)
Traversable.mapM TVal -> TypeCheck FKind
extractType TBinding TVal
tb
    addBind tb $ do
      (tb :) <$> loop vtel

extractType :: TVal -> TypeCheck FType
extractType :: TVal -> TypeCheck FKind
extractType = FKind -> TVal -> TypeCheck FKind
extractTypeAt FKind
star

extractTypeAt :: FKind -> TVal -> TypeCheck FType
extractTypeAt :: FKind -> TVal -> TypeCheck FKind
extractTypeAt FKind
k TVal
tv = do
  case (TVal
tv,FKind
k) of

    (VMeasured Measure TVal
mu TVal
vb, FKind
_) -> FKind -> TVal -> TypeCheck FKind
extractTypeAt FKind
k TVal
vb
    (VGuard Bound TVal
beta TVal
vb, FKind
_) -> FKind -> TVal -> TypeCheck FKind
extractTypeAt FKind
k TVal
vb

    -- relevant function space / sigma type --> non-dependent
    (VQuant PiSigma
pisig Name
x Domain
dom TVal
fv, FKind
_) | Bool -> Bool
not (Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Domain -> Dec
forall a. Dom a -> Dec
decor Domain
dom)) -> do
      a <- TVal -> TypeCheck FKind
extractType (Domain -> TVal
forall a. Dom a -> a
typ Domain
dom)
      -- new' x dom $ do
      bv <- app fv VIrr
      b  <- extractType bv
      let x = String -> Name
fresh String
""
      return $ piSig pisig (TBind x (defaultDomain a)) b

    -- irrelevant function space --> forall or erasure marker
    (VQuant PiSigma
Pi Name
x Domain
dom TVal
fv, FKind
_) | Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Domain -> Dec
forall a. Dom a -> Dec
decor Domain
dom) -> do
      mk <- TVal -> TypeCheck (Maybe FKind)
extractKind (Domain -> TVal
forall a. Dom a -> a
typ Domain
dom)
      case mk of
        Maybe FKind
Nothing -> do -- new' x dom $ do
          bv <- TVal -> TVal -> TypeCheck TVal
app TVal
fv TVal
VIrr
          b  <- extractType bv
          let x = String -> Name
fresh String
""
          return $ pi (TBind x (defaultIrrDom Irr)) b
        Just FKind
k' -> do
          Name -> FKind -> (Int -> TypeCheck FKind) -> TypeCheck FKind
forall a. Name -> FKind -> (Int -> TypeCheck a) -> TypeCheck a
newTyVar Name
x FKind
k' ((Int -> TypeCheck FKind) -> TypeCheck FKind)
-> (Int -> TypeCheck FKind) -> TypeCheck FKind
forall a b. (a -> b) -> a -> b
$ \ Int
i -> do
            bv <- TVal -> TVal -> TypeCheck TVal
app TVal
fv (TVal -> TypeCheck TVal) -> TVal -> TypeCheck TVal
forall a b. (a -> b) -> a -> b
$ Int -> TVal
VGen Int
i
            b  <- extractType bv
            x  <- nameOfGen i
            return $ pi (TBind x (defaultIrrDom k')) b

    (VApp (VDef (DefId IdKind
DatK QName
n)) [TVal]
vs, FKind
_) -> do
      k  <- SigDef -> FKind
extrTyp (SigDef -> FKind)
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
-> TypeCheck FKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => QName -> m SigDef
lookupSymbQ QName
n  -- get kind of dname from signature
      as <- extractTypes k vs  -- turn vs into types as at kind k
      return $ foldl App (Def (DefId DatK n)) as

    (VGen Int
i,FKind
_) -> do
--      VClos _ k <- (typ . fromOne . domain) <$> lookupGen i  -- get kind of var from cxt
      Name -> FKind
Var (Name -> FKind)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Name
-> TypeCheck FKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Name
forall (m :: * -> *). MonadCxt m => Int -> m Name
nameOfGen Int
i
      -- return $ Var (tyVarName i)

    (VApp (VGen Int
i) [TVal]
vs,FKind
_) -> do
      VClos _ k <- (Domain -> TVal
forall a. Dom a -> a
typ (Domain -> TVal)
-> (CxtE (OneOrTwo Domain) -> Domain)
-> CxtE (OneOrTwo Domain)
-> TVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneOrTwo Domain -> Domain
forall a. OneOrTwo a -> a
fromOne (OneOrTwo Domain -> Domain)
-> (CxtE (OneOrTwo Domain) -> OneOrTwo Domain)
-> CxtE (OneOrTwo Domain)
-> Domain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtE (OneOrTwo Domain) -> OneOrTwo Domain
forall a. CxtE a -> a
domain) (CxtE (OneOrTwo Domain) -> TVal)
-> StateT
     TCState
     (ReaderT TCContext (ExceptT TraceError IO))
     (CxtE (OneOrTwo Domain))
-> TypeCheck TVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> StateT
     TCState
     (ReaderT TCContext (ExceptT TraceError IO))
     (CxtE (OneOrTwo Domain))
forall (m :: * -> *).
MonadCxt m =>
Int -> m (CxtE (OneOrTwo Domain))
lookupGen Int
i  -- get kind of var from cxt
      as <- extractTypes k vs  -- turn vs into types as at kind k
      x <- nameOfGen i
      return $ foldl App (Var x) as

    (VLam Name
x Env
env FKind
e, Quant PiSigma
Pi (TBind Name
_ Dom FKind
dom) FKind
k) | Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Dom FKind -> Dec
forall a. Dom a -> Dec
decor Dom FKind
dom) -> do
      tv <- Env -> FKind -> TypeCheck TVal
whnf (Env -> Name -> TVal -> Env
forall a. Environ a -> Name -> a -> Environ a
update Env
env Name
x TVal
VIrr) FKind
e
      extractTypeAt k tv

    (VLam Name
x Env
env FKind
e, Quant PiSigma
Pi (TBind Name
_ Dom FKind
dom) FKind
k) -> Name -> FKind -> (Int -> TypeCheck FKind) -> TypeCheck FKind
forall a. Name -> FKind -> (Int -> TypeCheck a) -> TypeCheck a
newTyVar Name
x (Dom FKind -> FKind
forall a. Dom a -> a
typ Dom FKind
dom) ((Int -> TypeCheck FKind) -> TypeCheck FKind)
-> (Int -> TypeCheck FKind) -> TypeCheck FKind
forall a b. (a -> b) -> a -> b
$ \ Int
i -> do
      tv <- Env -> FKind -> TypeCheck TVal
whnf (Env -> Name -> TVal -> Env
forall a. Environ a -> Name -> a -> Environ a
update Env
env Name
x (Int -> TVal
VGen Int
i)) FKind
e
      x  <- nameOfGen i
      Lam defaultDec x <$> extractTypeAt k tv

    (VLam{},FKind
_) -> String -> TypeCheck FKind
forall a. HasCallStack => String -> a
error (String -> TypeCheck FKind) -> String -> TypeCheck FKind
forall a b. (a -> b) -> a -> b
$ String
"panic! extractTypeAt " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (TVal, FKind) -> String
forall a. Show a => a -> String
show (TVal
tv,FKind
k)

    (VSing TVal
_ TVal
tv,FKind
_) -> FKind -> TVal -> TypeCheck FKind
extractTypeAt FKind
k TVal
tv

    (VUp TVal
v TVal
_,FKind
_)    -> FKind -> TVal -> TypeCheck FKind
extractTypeAt FKind
k TVal
v

    (TVal, FKind)
_ -> FKind -> TypeCheck FKind
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return FKind
Irr

extractTypes :: FKind -> [TVal] -> TypeCheck [FType]
extractTypes :: FKind -> [TVal] -> TypeCheck [FKind]
extractTypes FKind
k [TVal]
vs =
  case (FKind
k,[TVal]
vs) of
    (FKind
_, []) -> [FKind] -> TypeCheck [FKind]
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    (Quant PiSigma
Pi (TBind Name
_ Dom FKind
dom) FKind
k, TVal
v:[TVal]
vs) | Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Dom FKind -> Dec
forall a. Dom a -> Dec
decor Dom FKind
dom) -> FKind -> [TVal] -> TypeCheck [FKind]
extractTypes FKind
k [TVal]
vs
    (Quant PiSigma
Pi (TBind Name
_ Dom FKind
dom) FKind
k, TVal
v:[TVal]
vs) -> do
      v  <- TVal -> TypeCheck TVal
whnfClos TVal
v
      a  <- extractTypeAt (typ dom) v
      as <- extractTypes k vs
      return $ a : as
    (FKind, [TVal])
_ -> String -> TypeCheck [FKind]
forall a. HasCallStack => String -> a
error (String -> TypeCheck [FKind]) -> String -> TypeCheck [FKind]
forall a b. (a -> b) -> a -> b
$ String
"panic! extractTypes  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FKind -> String
forall a. Show a => a -> String
show FKind
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [TVal] -> String
forall a. Show a => a -> String
show [TVal]
vs

-- auxiliary functions -----------------------------------------------

{- this is setExtrTyp
addFTypeSig :: Name -> FType -> TypeCheck ()
addFTypeSig n t = modifySig n (\ item -> item { extrTyp = t })
-}