amelia
/
cubical


{-# LANGUAGE LambdaCase #-}

{-# LANGUAGE DeriveAnyClass #-}

module Elab.Eval where


import Control.Monad.Reader

import Control.Exception


import qualified Data.Map.Strict as Map

import qualified Data.Set as Set

import qualified Data.Text as T

import Data.Traversable

import Data.Set (Set)

import Data.Typeable

import Data.Foldable

import Data.IORef

import Data.Maybe


import Elab.Monad


import Presyntax.Presyntax (Plicity(..))


import Syntax


import System.IO.Unsafe


eval :: Term -> ElabM Value

eval t = asks (flip evalWithEnv t)


forceIO :: MonadIO m => Value -> m Value

forceIO vl@(VNe (HMeta (MV _ cell)) args) = do

 solved <- liftIO $ readIORef cell

 case solved of

 Just vl -> forceIO $ foldl applProj vl (reverse args)

 Nothing -> pure vl

forceIO x = pure x


applProj :: Value -> Projection -> Value

applProj fun (PApp p arg) = vApp p fun arg

applProj fun PProj1 = vProj1 fun

applProj fun PProj2 = vProj2 fun


force :: Value -> Value

force = unsafePerformIO . forceIO


evalWithEnv :: ElabEnv -> Term -> Value

evalWithEnv env (Ref x) =

 case Map.lookup x (getEnv env) of

 Just (_, vl) -> vl

 _ -> error "variable not in scope when evaluating"

evalWithEnv env (App p f x) = vApp p (evalWithEnv env f) (evalWithEnv env x)


evalWithEnv env (Lam p s t) =

 VLam p $ Closure s $ \a ->

 evalWithEnv (ElabEnv (Map.insert (Bound s) (error "type of abs", a) (getEnv env))) t


evalWithEnv env (Pi p s d t) =

 VPi p (evalWithEnv env d) $ Closure s $ \a ->

 evalWithEnv (ElabEnv (Map.insert (Bound s) (error "type of abs", a) (getEnv env))) t


evalWithEnv _ (Meta m) = VNe (HMeta m) []


evalWithEnv env (Sigma s d t) =

 VSigma (evalWithEnv env d) $ Closure s $ \a ->

 evalWithEnv (ElabEnv (Map.insert (Bound s) (error "type of abs", a) (getEnv env))) t


evalWithEnv e (Pair a b) = VPair (evalWithEnv e a) (evalWithEnv e b)


evalWithEnv e (Proj1 a) = vProj1 (evalWithEnv e a)

evalWithEnv e (Proj2 a) = vProj2 (evalWithEnv e a)


evalWithEnv _ Type = VType


vApp :: Plicity -> Value -> Value -> Value

vApp p (VLam p' k) arg = assert (p == p') $ clCont k arg

vApp p (VNe h sp) arg = VNe h (PApp p arg:sp)

vApp _ x _ = error $ "can't apply " ++ show x


vProj1 :: Value -> Value

vProj1 (VPair a _) = a

vProj1 (VNe h sp) = VNe h (PProj1:sp)

vProj1 x = error $ "can't proj1 " ++ show x


vProj2 :: Value -> Value

vProj2 (VPair _ b) = b

vProj2 (VNe h sp) = VNe h (PProj2:sp)

vProj2 x = error $ "can't proj2 " ++ show x


data NotEqual = NotEqual Value Value

 deriving (Show, Typeable, Exception)


unify :: Value -> Value -> ElabM ()

unify topa topb = join $ go <$> forceIO topa <*> forceIO topb where

 go (VNe (HMeta mv) sp) rhs = solveMeta mv sp rhs


 go (VNe x a) (VNe x' a')

 | x == x', length a == length a' =

 traverse_ (uncurry unifySpine) (zip a a')

 | otherwise = fail


 go (VLam p (Closure _ k)) vl = do

 t <- VVar . Bound <$> newName

 unify (k t) (vApp p vl t)


 go vl (VLam p (Closure _ k)) = do

 t <- VVar . Bound <$> newName

 unify (vApp p vl t) (k t)


 go (VPair a b) vl = unify a (vProj1 vl) *> unify b (vProj2 vl)

 go vl (VPair a b) = unify (vProj1 vl) a *> unify (vProj2 vl) b


 go (VPi p d (Closure _ k)) (VPi p' d' (Closure _ k')) | p == p' = do

 t <- VVar . Bound <$> newName

 unify d d'

 unify (k t) (k' t)


 go (VSigma d (Closure _ k)) (VSigma d' (Closure _ k')) = do

 t <- VVar . Bound <$> newName

 unify d d'

 unify (k t) (k' t)


 go _ _ = fail


 fail = liftIO . throwIO $ NotEqual topa topb


 unifySpine (PApp a v) (PApp a' v')

 | a == a' = unify v v'

 unifySpine _ _ = fail


isConvertibleTo :: Value -> Value -> ElabM (Term -> Term)

VPi Im d (Closure _v k) `isConvertibleTo` ty = do

 meta <- newMeta d

 cont <- k meta `isConvertibleTo` ty

 pure (\f -> cont (App Ex f (quote meta)))

isConvertibleTo a b = do

 unify a b

 pure id


newMeta :: Value -> ElabM Value

newMeta _dom = do

 n <- newName

 c <- liftIO $ newIORef Nothing

 let m = MV n c


 env <- asks getEnv


 t <- for (Map.toList env) $ \(n, (_, c)) -> pure $

 case c of

 VVar n' | n == n' -> Just (PApp Ex (VVar n'))

 _ -> Nothing


 pure (VNe (HMeta m) (catMaybes t))


newName :: MonadIO m => m T.Text

newName = liftIO $ do

 x <- atomicModifyIORef _nameCounter $ \x -> (x + 1, x + 1)

 pure (T.pack (show x))


_nameCounter :: IORef Int

_nameCounter = unsafePerformIO $ newIORef 0

{-# NOINLINE _nameCounter #-}


solveMeta :: MV -> [Projection] -> Value -> ElabM ()

solveMeta m@(MV _ cell) sp rhs = do

 liftIO $ print (m, sp, rhs)

 names <- checkSpine Set.empty sp

 checkScope (Set.fromList (Bound <$> names)) rhs

 let tm = quote rhs

 lam = evalWithEnv emptyEnv $ foldr (Lam Ex) tm names

 liftIO . atomicModifyIORef' cell $ \case

 Just _ -> error "filled cell in solvedMeta"

 Nothing -> (Just lam, ())


checkScope :: Set Name -> Value -> ElabM ()

checkScope scope (VNe h sp) =

 do

 case h of

 HVar v ->

 unless (v `Set.member` scope) . liftIO . throwIO $

 NotInScope v

 HMeta{} -> pure ()

 traverse_ checkProj sp

 where

 checkProj (PApp _ t) = checkScope scope t

 checkProj PProj1 = pure ()

 checkProj PProj2 = pure ()


checkScope scope (VLam _ (Closure n k)) =

 checkScope (Set.insert (Bound n) scope) (k (VVar (Bound n)))


checkScope scope (VPi _ d (Closure n k)) = do

 checkScope scope d

 checkScope (Set.insert (Bound n) scope) (k (VVar (Bound n)))


checkScope scope (VSigma d (Closure n k)) = do

 checkScope scope d

 checkScope (Set.insert (Bound n) scope) (k (VVar (Bound n)))


checkScope s (VPair a b) = traverse_ (checkScope s) [a, b]


checkScope _ VType = pure ()


checkSpine :: Set Name -> [Projection] -> ElabM [T.Text]

checkSpine scope (PApp Ex (VVar n@(Bound t)):xs)

 | n `Set.member` scope = liftIO . throwIO $ NonLinearSpine n

 | otherwise = (t:) <$> checkSpine scope xs

checkSpine _ (p:_) = liftIO . throwIO $ SpineProj p

checkSpine _ [] = pure []


newtype NonLinearSpine = NonLinearSpine { getDupeName :: Name }

 deriving (Show, Typeable, Exception)


newtype SpineProjection = SpineProj { getSpineProjection :: Projection }

 deriving (Show, Typeable, Exception)