Use better names
This commit is contained in:
Martin Fredin
parent
9730552eab
commit
2b7715714e
1 changed files with 250 additions and 250 deletions
|
|
@ -38,7 +38,6 @@ import qualified TypeChecker.TypeCheckerIr as T
|
||||||
--
|
--
|
||||||
-- TODO
|
-- TODO
|
||||||
-- • Fix problems with types in Pattern/Branch in TypeCheckerIr
|
-- • Fix problems with types in Pattern/Branch in TypeCheckerIr
|
||||||
-- • Use applyEnvExp consistently
|
|
||||||
-- • Fix the different type getters functions (e.g. partitionType) functions
|
-- • Fix the different type getters functions (e.g. partitionType) functions
|
||||||
|
|
||||||
data EnvElem = EnvVar LIdent Type -- ^ Term variable typing. x : A
|
data EnvElem = EnvVar LIdent Type -- ^ Term variable typing. x : A
|
||||||
|
|
@ -169,161 +168,156 @@ typecheckInj (Inj inj_name inj_typ) name tvars
|
||||||
-- | Γ ⊢ e ↑ A ⊣ Δ
|
-- | Γ ⊢ e ↑ A ⊣ Δ
|
||||||
-- Under input context Γ, e checks against input type A, with output context ∆
|
-- Under input context Γ, e checks against input type A, with output context ∆
|
||||||
check :: Exp -> Type -> Tc (T.ExpT' Type)
|
check :: Exp -> Type -> Tc (T.ExpT' Type)
|
||||||
check exp typ
|
|
||||||
|
|
||||||
-- Γ,α ⊢ e ↑ A ⊣ Δ,α,Θ
|
-- Γ,α ⊢ e ↑ A ⊣ Δ,α,Θ
|
||||||
-- ------------------- ∀I
|
-- ------------------- ∀I
|
||||||
-- Γ ⊢ e ↑ ∀α.A ⊣ Δ
|
-- Γ ⊢ e ↑ ∀α.A ⊣ Δ
|
||||||
| TAll tvar t <- typ = do
|
check e (TAll alpha a) = do
|
||||||
let env_tvar = EnvTVar tvar
|
let env_tvar = EnvTVar alpha
|
||||||
insertEnv env_tvar
|
insertEnv env_tvar
|
||||||
exp' <- check exp t
|
e' <- check e a
|
||||||
(env_l, _) <- gets (splitOn env_tvar . env)
|
(env_l, _) <- gets (splitOn env_tvar . env)
|
||||||
putEnv env_l
|
putEnv env_l
|
||||||
pure exp'
|
apply e'
|
||||||
|
|
||||||
-- Γ,(x:A) ⊢ e ↑ B ⊢ Δ,(x:A),Θ
|
-- Γ,(x:A) ⊢ e ↑ B ⊢ Δ,(x:A),Θ
|
||||||
-- --------------------------- →I
|
-- --------------------------- →I
|
||||||
-- Γ ⊢ λx.e ↑ A → B ⊣ Δ
|
-- Γ ⊢ λx.e ↑ A → B ⊣ Δ
|
||||||
| EAbs name e <- exp
|
check (EAbs x e) (TFun a b) = do
|
||||||
, TFun t1 t2 <- typ = do
|
let env_var = EnvVar x a
|
||||||
let env_var = EnvVar name t1
|
insertEnv env_var
|
||||||
insertEnv env_var
|
e' <- check e b
|
||||||
e' <- check e t2
|
(env_l, _) <- gets (splitOn env_var . env)
|
||||||
(env_l, _) <- gets (splitOn env_var . env)
|
putEnv env_l
|
||||||
putEnv env_l
|
apply (T.EAbs (coerce x) e', TFun a b)
|
||||||
pure (T.EAbs (coerce name) e', typ)
|
|
||||||
|
|
||||||
-- Γ,α ⊢ e ↓ A ⊣ Θ Θ ⊢ [Θ]A <: [Θ]B ⊣ Δ
|
-- Γ,α ⊢ e ↓ A ⊣ Θ Θ ⊢ [Θ]A <: [Θ]B ⊣ Δ
|
||||||
-- -------------------------------------- Sub
|
-- -------------------------------------- Sub
|
||||||
-- Γ ⊢ e ↑ B ⊣ Δ
|
-- Γ ⊢ e ↑ B ⊣ Δ
|
||||||
| otherwise = do
|
check e b = do
|
||||||
(exp', t) <- infer exp
|
(e', a) <- infer e
|
||||||
typ' <- apply typ
|
b' <- apply b
|
||||||
subtype t typ'
|
subtype a b'
|
||||||
apply (exp', t)
|
apply (e', b)
|
||||||
|
|
||||||
-- | Γ ⊢ e ↓ A ⊣ Δ
|
-- | Γ ⊢ e ↓ A ⊣ Δ
|
||||||
-- Under input context Γ, e infers output type A, with output context ∆
|
-- Under input context Γ, e infers output type A, with output context ∆
|
||||||
infer :: Exp -> Tc (T.ExpT' Type)
|
infer :: Exp -> Tc (T.ExpT' Type)
|
||||||
infer = \case
|
|
||||||
|
|
||||||
ELit lit -> pure (T.ELit lit, litType lit)
|
infer (ELit lit) = apply (T.ELit lit, litType lit)
|
||||||
|
|
||||||
-- Γ ∋ (x : A) Γ ∌ (x : A)
|
-- Γ ∋ (x : A) Γ ∌ (x : A)
|
||||||
-- ------------- Var --------------------- Var'
|
-- ------------- Var --------------------- Var'
|
||||||
-- Γ ⊢ x ↓ A ⊣ Γ Γ ⊢ x ↓ ά ⊣ Γ,(x : ά)
|
-- Γ ⊢ x ↓ A ⊣ Γ Γ ⊢ x ↓ ά ⊣ Γ,(x : ά)
|
||||||
EVar x -> do
|
infer (EVar x) = do
|
||||||
t <- fromMaybeM extend $ liftA2 (<|>) (lookupEnv x) (lookupSig x)
|
a <- fromMaybeM extend $ liftA2 (<|>) (lookupEnv x) (lookupSig x)
|
||||||
apply (T.EVar (coerce x), t)
|
apply (T.EVar (coerce x), a)
|
||||||
where
|
where
|
||||||
extend = do
|
extend = do
|
||||||
t <- TEVar <$> fresh
|
alpha <- TEVar <$> fresh
|
||||||
insertEnv (EnvVar x t)
|
insertEnv (EnvVar x alpha)
|
||||||
pure t
|
pure alpha
|
||||||
|
|
||||||
EInj name -> do
|
infer (EInj kappa) = do
|
||||||
t <- maybeToRightM ("Unknown constructor: " ++ show name)
|
t <- maybeToRightM ("Unknown constructor: " ++ show kappa)
|
||||||
=<< lookupInj name
|
=<< lookupInj kappa
|
||||||
apply (T.EInj $ coerce name, t)
|
apply (T.EInj $ coerce kappa, t)
|
||||||
|
|
||||||
-- Γ ⊢ A Γ ⊢ e ↑ A ⊣ Δ
|
-- Γ ⊢ A Γ ⊢ e ↑ A ⊣ Δ
|
||||||
-- --------------------- Anno
|
-- --------------------- Anno
|
||||||
-- Γ ⊢ (e : A) ↓ A ⊣ Δ
|
-- Γ ⊢ (e : A) ↓ A ⊣ Δ
|
||||||
EAnn e t -> do
|
infer (EAnn e a) = do
|
||||||
_ <- gets $ (`wellFormed` t) . env
|
_ <- gets $ (`wellFormed` a) . env
|
||||||
(e', _) <- check e t
|
(e', _) <- check e a
|
||||||
apply (e', t)
|
apply (e', a)
|
||||||
|
|
||||||
-- Γ ⊢ e₁ ↓ A ⊣ Θ Γ ⊢ [Θ]A • ⇓ C ⊣ Δ
|
-- Γ ⊢ e₁ ↓ A ⊣ Θ Γ ⊢ [Θ]A • ⇓ C ⊣ Δ
|
||||||
-- ----------------------------------- →E
|
-- ----------------------------------- →E
|
||||||
-- Γ ⊢ e₁ e₂ ↓ C ⊣ Δ
|
-- Γ ⊢ e₁ e₂ ↓ C ⊣ Δ
|
||||||
EApp e1 e2 -> do
|
infer (EApp e1 e2) = do
|
||||||
(e1', t) <- infer e1
|
e1'@(_, a) <- infer e1
|
||||||
(e2', t'') <- applyInfer t e2
|
(e2', c) <- applyInfer a e2
|
||||||
apply (T.EApp (e1', t) e2', t'')
|
apply (T.EApp e1' e2', c)
|
||||||
|
|
||||||
-- Γ,ά,έ,(x:ά) ⊢ e ↑ έ ⊣ Δ,(x:ά),Θ
|
-- Γ,ά,έ,(x:ά) ⊢ e ↑ έ ⊣ Δ,(x:ά),Θ
|
||||||
-- ------------------------------- →I
|
-- ------------------------------- →I
|
||||||
-- Γ ⊢ λx.e ↓ ά → έ ⊣ Δ
|
-- Γ ⊢ λx.e ↓ ά → έ ⊣ Δ
|
||||||
EAbs name e -> do
|
infer (EAbs name e) = do
|
||||||
tevar1 <- fresh
|
alpha <- fresh
|
||||||
tevar2 <- fresh
|
epsilon <- fresh
|
||||||
insertEnv $ EnvTEVar tevar1
|
insertEnv $ EnvTEVar alpha
|
||||||
insertEnv $ EnvTEVar tevar2
|
insertEnv $ EnvTEVar epsilon
|
||||||
let env_var = EnvVar name (TEVar tevar1)
|
let env_var = EnvVar name (TEVar alpha)
|
||||||
insertEnv env_var
|
insertEnv env_var
|
||||||
e' <- check e $ TEVar tevar2
|
e' <- check e $ TEVar epsilon
|
||||||
dropTrailing env_var
|
dropTrailing env_var
|
||||||
let t_exp = on TFun TEVar tevar1 tevar2
|
apply (T.EAbs (coerce name) e', on TFun TEVar alpha epsilon)
|
||||||
apply (T.EAbs (coerce name) e', t_exp)
|
|
||||||
|
|
||||||
|
-- Γ ⊢ rhs ↓ A ⊣ Θ Θ,(x:A) ⊢ e ↑ C ⊣ Δ,(x:A),Θ
|
||||||
|
-- -------------------------------------------- LetI
|
||||||
|
-- Γ ⊢ let x = rhs in e ↑ C ⊣ Δ
|
||||||
|
infer (ELet (Bind x vars rhs) e) = do
|
||||||
|
(rhs', a) <- infer $ foldr EAbs rhs vars
|
||||||
|
let env_var = EnvVar x a
|
||||||
|
insertEnv env_var
|
||||||
|
e'@(_, c) <- infer e
|
||||||
|
(env_l, _) <- gets (splitOn env_var . env)
|
||||||
|
putEnv env_l
|
||||||
|
apply (T.ELet (T.Bind (coerce x, a) [] (rhs', a)) e', c)
|
||||||
|
|
||||||
-- Γ ⊢ e ↓ A ⊣ Θ Θ,(x:A) ⊢ e' ↑ C ⊣ Δ,(x:A),Θ
|
-- Γ ⊢ e₁ ↑ Int ⊣ Θ Θ ⊢ e₂ ↑ Int
|
||||||
-- -------------------------------------------- LetI
|
-- --------------------------- +I
|
||||||
-- Γ ⊢ let x=e in e' ↑ C ⊣ Δ
|
-- Γ ⊢ e₁ + e₂ ↓ Int ⊣ Δ
|
||||||
ELet (Bind name [] rhs) e -> do -- TODO vars
|
infer (EAdd e1 e2) = do
|
||||||
(rhs', t_rhs) <- infer rhs
|
e1' <- check e1 int
|
||||||
let env_var = EnvVar name t_rhs
|
e2' <- check e2 int
|
||||||
insertEnv env_var
|
apply (T.EAdd e1' e2', int)
|
||||||
(e', t) <- infer e
|
|
||||||
(env_l, _) <- gets (splitOn env_var . env)
|
|
||||||
putEnv env_l
|
|
||||||
apply (T.ELet (T.Bind (coerce name, t_rhs) [] (rhs', t_rhs)) (e',t), t)
|
|
||||||
|
|
||||||
-- Γ ⊢ e₁ ↑ Int ⊣ Θ Θ ⊢ e₂ ↑ Int
|
-- Θ ⊢ Π ∷ A ↓ C ⊣ Δ
|
||||||
-- --------------------------- +I
|
-- Γ ⊢ e ↓ A ⊣ Θ Δ ⊢ Π covers [Δ]A TODO
|
||||||
-- Γ ⊢ e₁ + e₂ ↓ Int ⊣ Δ
|
-- ---------------------------------------
|
||||||
EAdd e1 e2 -> (, int) <$> onM T.EAdd (`check` int) e1 e2
|
-- Γ ⊢ case e of Π ↓ C ⊣ Δ
|
||||||
|
infer (ECase scrut branches) = do
|
||||||
-- Θ ⊢ Π ∷ A ↓ C ⊣ Δ
|
(scrut', t_scrut) <- infer scrut
|
||||||
-- Γ ⊢ e ↓ A ⊣ Θ Δ ⊢ Π covers [Δ]A TODO
|
(branches', t_return) <- inferBranches branches t_scrut
|
||||||
-- ---------------------------------------
|
apply (T.ECase (scrut', t_scrut) branches', t_return)
|
||||||
-- Γ ⊢ case e of Π ↓ C ⊣ Δ
|
|
||||||
ECase scrut branches -> do
|
|
||||||
(scrut', t_scrut) <- infer scrut
|
|
||||||
(branches', t_return) <- inferBranches branches t_scrut
|
|
||||||
apply (T.ECase (scrut', t_scrut) branches', t_return)
|
|
||||||
|
|
||||||
-- | Γ ⊢ A • e ⇓ C ⊣ Δ
|
-- | Γ ⊢ A • e ⇓ C ⊣ Δ
|
||||||
-- Under input context Γ , applying a function of type A to e infers type C, with output context ∆
|
-- Under input context Γ , applying a function of type A to e infers type C, with output context ∆
|
||||||
-- Instantiate existential type variables until there is an arrow type.
|
-- Instantiate existential type variables until there is an arrow type.
|
||||||
applyInfer :: Type -> Exp -> Tc (T.ExpT' Type, Type)
|
applyInfer :: Type -> Exp -> Tc (T.ExpT' Type, Type)
|
||||||
applyInfer typ exp = case typ of
|
|
||||||
|
|
||||||
-- Γ,ά ⊢ [ά/α]A • e ⇓ C ⊣ Δ
|
-- Γ,ά ⊢ [ά/α]A • e ⇓ C ⊣ Δ
|
||||||
-- ------------------------ ∀App
|
-- ------------------------ ∀App
|
||||||
-- Γ ⊢ ∀α.A • e ⇓ C ⊣ Δ
|
-- Γ ⊢ ∀α.A • e ⇓ C ⊣ Δ
|
||||||
TAll tvar t -> do
|
applyInfer (TAll alpha a) e = do
|
||||||
tevar <- fresh
|
alpha' <- fresh
|
||||||
insertEnv $ EnvTEVar tevar
|
insertEnv $ EnvTEVar alpha'
|
||||||
let t' = substitute tvar tevar t
|
applyInfer (substitute alpha alpha' a) e
|
||||||
applyInfer t' exp
|
|
||||||
|
|
||||||
-- Γ[ά₂,ά₁,(ά=ά₁→ά₂)] ⊢ e ↑ ά₁ ⊣ Δ
|
-- Γ[ά₂,ά₁,(ά=ά₁→ά₂)] ⊢ e ↑ ά₁ ⊣ Δ
|
||||||
-- ------------------------------- άApp
|
-- ------------------------------- άApp
|
||||||
-- Γ[ά] ⊢ ά • e ⇓ ά₂ ⊣ Δ
|
-- Γ[ά] ⊢ ά • e ⇓ ά₂ ⊣ Δ
|
||||||
TEVar tevar -> do
|
applyInfer (TEVar alpha) e = do
|
||||||
tevar1 <- fresh
|
alpha1 <- fresh
|
||||||
tevar2 <- fresh
|
alpha2 <- fresh
|
||||||
let env_tevar1 = EnvTEVar tevar1
|
(env_l, env_r) <- gets (splitOn (EnvTEVar alpha) . env)
|
||||||
env_tevar2 = EnvTEVar tevar2
|
putEnv $ (env_l
|
||||||
t_fun = on TFun TEVar tevar1 tevar2
|
:|> EnvTEVar alpha2
|
||||||
env_tevar_solved = EnvTEVarSolved tevar t_fun
|
:|> EnvTEVar alpha1
|
||||||
(env_l, env_r) <- gets (splitOn (EnvTEVar tevar) . env)
|
:|> EnvTEVarSolved alpha (on TFun TEVar alpha1 alpha2)
|
||||||
putEnv $
|
) <> env_r
|
||||||
(env_l :|> env_tevar2 :|> env_tevar1 :|> env_tevar_solved) <> env_r
|
e' <- check e $ TEVar alpha1
|
||||||
expT' <- check exp $ TEVar tevar1
|
apply (e', TEVar alpha2)
|
||||||
apply (expT', TEVar tevar2)
|
|
||||||
|
|
||||||
-- Γ ⊢ e ↑ A ⊣ Δ
|
-- Γ ⊢ e ↑ A ⊣ Δ
|
||||||
-- --------------------- →App
|
-- --------------------- →App
|
||||||
-- Γ ⊢ A → C • e ⇓ C ⊣ Δ
|
-- Γ ⊢ A → C • e ⇓ C ⊣ Δ
|
||||||
TFun t1 t2 -> do
|
applyInfer (TFun a c) e = do
|
||||||
exp' <- check exp t1
|
exp' <- check e a
|
||||||
apply (exp', t2)
|
apply (exp', c)
|
||||||
|
|
||||||
_ -> throwError ("Cannot apply type " ++ show typ ++ " with expression " ++ show exp)
|
applyInfer a e = throwError ("Cannot apply type " ++ show a ++ " with expression " ++ show e)
|
||||||
|
|
||||||
---------------------------------------------------------------------------
|
---------------------------------------------------------------------------
|
||||||
-- * Pattern matching
|
-- * Pattern matching
|
||||||
|
|
@ -435,59 +429,58 @@ checkPattern patt t_patt = case patt of
|
||||||
-- | Γ ⊢ A <: B ⊣ Δ
|
-- | Γ ⊢ A <: B ⊣ Δ
|
||||||
-- Under input context Γ, type A is a subtype of B, with output context ∆
|
-- Under input context Γ, type A is a subtype of B, with output context ∆
|
||||||
subtype :: Type -> Type -> Tc ()
|
subtype :: Type -> Type -> Tc ()
|
||||||
|
subtype (TLit lit1) (TLit lit2) | lit1 == lit2 = pure ()
|
||||||
|
|
||||||
|
-- -------------------- <:Var
|
||||||
|
-- Γ[α] ⊢ α <: α ⊣ Γ[α]
|
||||||
|
subtype (TVar alpha) (TVar alpha') | alpha == alpha' = pure ()
|
||||||
|
|
||||||
|
-- -------------------- <:Exvar
|
||||||
|
-- Γ[ά] ⊢ ά <: ά ⊣ Γ[ά]
|
||||||
|
subtype (TEVar alpha) (TEVar alpha') | alpha == alpha' = pure ()
|
||||||
|
|
||||||
|
-- Γ ⊢ B₁ <: A₁ ⊣ Θ Θ ⊢ [Θ]A₂ <: [Θ]B₂ ⊣ Δ
|
||||||
|
-- ----------------------------------------- <:→
|
||||||
|
-- Γ ⊢ A₁ → A₂ <: B₁ → B₂ ⊣ Δ
|
||||||
|
subtype (TFun a1 a2) (TFun b1 b2) = do
|
||||||
|
subtype b1 a1
|
||||||
|
a2' <- apply a2
|
||||||
|
b2' <- apply b2
|
||||||
|
subtype a2' b2'
|
||||||
|
|
||||||
|
-- Γ, α ⊢ A <: B ⊣ Δ,α,Θ
|
||||||
|
-- --------------------- <:∀R
|
||||||
|
-- Γ ⊢ A <: ∀α. B ⊣ Δ
|
||||||
|
subtype a (TAll alpha b) = do
|
||||||
|
let env_tvar = EnvTVar alpha
|
||||||
|
insertEnv env_tvar
|
||||||
|
subtype a b
|
||||||
|
dropTrailing env_tvar
|
||||||
|
|
||||||
|
-- Γ,▶ ά,ά ⊢ [ά/α]A <: B ⊣ Δ,▶ ά,Θ
|
||||||
|
-- ------------------------------- <:∀L
|
||||||
|
-- Γ ⊢ ∀α.A <: B ⊣ Δ
|
||||||
|
subtype (TAll alpha a) b = do
|
||||||
|
alpha' <- fresh
|
||||||
|
let env_marker = EnvMark alpha'
|
||||||
|
insertEnv env_marker
|
||||||
|
insertEnv $ EnvTEVar alpha'
|
||||||
|
let a' = substitute alpha alpha' a
|
||||||
|
subtype a' b
|
||||||
|
dropTrailing env_marker
|
||||||
|
|
||||||
|
-- ά ∉ FV(A) Γ[ά] ⊢ ά :=< A ⊣ Δ
|
||||||
|
-- ------------------------------ <:instantiateL
|
||||||
|
-- Γ[ά] ⊢ ά <: A ⊣ Δ
|
||||||
|
subtype (TEVar alpha) a | notElem alpha $ frees a = instantiateL alpha a
|
||||||
|
|
||||||
|
-- ά ∉ FV(A) Γ[ά] ⊢ A =:< ά ⊣ Δ
|
||||||
|
-- ------------------------------ <:instantiateR
|
||||||
|
-- Γ[ά] ⊢ A <: ά ⊣ Δ
|
||||||
|
subtype a (TEVar alpha) | notElem alpha $ frees a = instantiateR a alpha
|
||||||
|
|
||||||
|
|
||||||
subtype t1 t2 = case (t1, t2) of
|
subtype t1 t2 = case (t1, t2) of
|
||||||
|
|
||||||
(TLit lit1, TLit lit2) | lit1 == lit2 -> pure ()
|
|
||||||
|
|
||||||
-- -------------------- <:Var
|
|
||||||
-- Γ[α] ⊢ α <: α ⊣ Γ[α]
|
|
||||||
(TVar tvar1, TVar tvar2) | tvar1 == tvar2 -> pure ()
|
|
||||||
|
|
||||||
-- -------------------- <:Exvar
|
|
||||||
-- Γ[ά] ⊢ ά <: ά ⊣ Γ[ά]
|
|
||||||
(TEVar tevar1, TEVar tevar2) | tevar1 == tevar2 -> pure ()
|
|
||||||
|
|
||||||
-- Γ ⊢ B₁ <: A₁ ⊣ Θ Θ ⊢ [Θ]A₂ <: [Θ]B₂ ⊣ Δ
|
|
||||||
-- ----------------------------------------- <:→
|
|
||||||
-- Γ ⊢ A₁ → A₂ <: B₁ → B₂ ⊣ Δ
|
|
||||||
(TFun a1 a2, TFun b1 b2) -> do
|
|
||||||
subtype b1 a1
|
|
||||||
a2' <- apply a2
|
|
||||||
b2' <- apply b2
|
|
||||||
subtype a2' b2'
|
|
||||||
|
|
||||||
-- Γ, α ⊢ A <: B ⊣ Δ,α,Θ
|
|
||||||
-- --------------------- <:∀R
|
|
||||||
-- Γ ⊢ A <: ∀α. B ⊣ Δ
|
|
||||||
(a, TAll tvar b) -> do
|
|
||||||
let env_tvar = EnvTVar tvar
|
|
||||||
insertEnv env_tvar
|
|
||||||
subtype a b
|
|
||||||
dropTrailing env_tvar
|
|
||||||
|
|
||||||
-- Γ,▶ ά,ά ⊢ [ά/α]A <: B ⊣ Δ,▶ ά,Θ
|
|
||||||
-- ------------------------------- <:∀L
|
|
||||||
-- Γ ⊢ ∀α.A <: B ⊣ Δ
|
|
||||||
(TAll tvar a, b) -> do
|
|
||||||
tevar <- fresh
|
|
||||||
let env_marker = EnvMark tevar
|
|
||||||
insertEnv env_marker
|
|
||||||
insertEnv $ EnvTEVar tevar
|
|
||||||
let a' = substitute tvar tevar a
|
|
||||||
subtype a' b
|
|
||||||
dropTrailing env_marker
|
|
||||||
|
|
||||||
-- ά ∉ FV(A) Γ[ά] ⊢ ά :=< A ⊣ Δ
|
|
||||||
-- ------------------------------ <:instantiateL
|
|
||||||
-- Γ[ά] ⊢ ά <: A ⊣ Δ
|
|
||||||
(TEVar tevar, typ) | notElem tevar $ frees typ -> instantiateL tevar typ
|
|
||||||
|
|
||||||
-- ά ∉ FV(A) Γ[ά] ⊢ A =:< ά ⊣ Δ
|
|
||||||
-- ------------------------------ <:instantiateR
|
|
||||||
-- Γ[ά] ⊢ A <: ά ⊣ Δ
|
|
||||||
(typ, TEVar tevar) | notElem tevar $ frees typ -> instantiateR typ tevar
|
|
||||||
|
|
||||||
|
|
||||||
(TData name1 typs1, TData name2 typs2)
|
(TData name1 typs1, TData name2 typs2)
|
||||||
|
|
||||||
-- D₁ = D₂
|
-- D₁ = D₂
|
||||||
|
|
@ -524,99 +517,106 @@ subtype t1 t2 = case (t1, t2) of
|
||||||
-- | Γ ⊢ ά :=< A ⊣ Δ
|
-- | Γ ⊢ ά :=< A ⊣ Δ
|
||||||
-- Under input context Γ, instantiate ά such that ά <: A, with output context ∆
|
-- Under input context Γ, instantiate ά such that ά <: A, with output context ∆
|
||||||
instantiateL :: TEVar -> Type -> Tc ()
|
instantiateL :: TEVar -> Type -> Tc ()
|
||||||
instantiateL tevar typ = gets env >>= go
|
instantiateL alpha a = gets env >>= \env -> go env alpha a
|
||||||
where
|
where
|
||||||
go env
|
go env alpha tau
|
||||||
|
| isMono tau
|
||||||
|
, (env_l, env_r) <- splitOn (EnvTEVar alpha) env
|
||||||
|
, Right _ <- wellFormed env_l tau
|
||||||
|
= putEnv $ (env_l :|> EnvTEVarSolved alpha tau) <> env_r
|
||||||
|
|
||||||
-- Γ ⊢ τ
|
-- Γ ⊢ τ
|
||||||
-- ----------------------------- InstLSolve
|
-- ----------------------------- InstLSolve
|
||||||
-- Γ,ά,Γ' ⊢ ά :=< τ ⊣ Γ,(ά=τ),Γ'
|
-- Γ,ά,Γ' ⊢ ά :=< τ ⊣ Γ,(ά=τ),Γ'
|
||||||
| isMono typ
|
go env alpha tau
|
||||||
, (env_l, env_r) <- splitOn (EnvTEVar tevar) env
|
| isMono tau
|
||||||
, Right _ <- wellFormed env_l typ
|
, (env_l, env_r) <- splitOn (EnvTEVar alpha) env
|
||||||
= putEnv $ (env_l :|> EnvTEVarSolved tevar typ) <> env_r
|
, Right _ <- wellFormed env_l tau
|
||||||
|
= putEnv $ (env_l :|> EnvTEVarSolved alpha tau) <> env_r
|
||||||
|
|
||||||
| TEVar tevar' <- typ = instReach tevar tevar'
|
-- ----------------------------- InstLReach
|
||||||
|
-- Γ[ά][έ] ⊢ ά :=< έ ⊣ Γ[ά][έ=ά]
|
||||||
|
go env alpha (TEVar epsilon) = do
|
||||||
|
let (env_l, env_r) = splitOn (EnvTEVar epsilon) env
|
||||||
|
putEnv $ (env_l :|> EnvTEVarSolved epsilon (TEVar alpha)) <> env_r
|
||||||
|
|
||||||
-- Γ[ά₂ά₁,(ά=ά₁→ά₂)] ⊢ A₁ =:< ά₁ ⊣ Θ Θ ⊢ ά₂ :=< [Θ]A₂ ⊣ Δ
|
-- Γ[ά₂ά₁,(ά=ά₁→ά₂)] ⊢ A₁ =:< ά₁ ⊣ Θ Θ ⊢ ά₂ :=< [Θ]A₂ ⊣ Δ
|
||||||
-- ------------------------------------------------------- InstLArr
|
-- ------------------------------------------------------- InstLArr
|
||||||
-- Γ[ά] ⊢ ά :=< A₁ → A₂ ⊣ Δ
|
-- Γ[ά] ⊢ ά :=< A₁ → A₂ ⊣ Δ
|
||||||
| TFun t1 t2 <- typ = do
|
go _ alpha (TFun a1 a2) = do
|
||||||
tevar1 <- fresh
|
alpha1 <- fresh
|
||||||
tevar2 <- fresh
|
alpha2 <- fresh
|
||||||
insertEnv $ EnvTEVar tevar2
|
insertEnv $ EnvTEVar alpha2
|
||||||
insertEnv $ EnvTEVar tevar1
|
insertEnv $ EnvTEVar alpha1
|
||||||
insertEnv $ EnvTEVarSolved tevar (on TFun TEVar tevar1 tevar2)
|
insertEnv $ EnvTEVarSolved alpha (on TFun TEVar alpha1 alpha2)
|
||||||
instantiateR t1 tevar1
|
instantiateR a1 alpha1
|
||||||
instantiateL tevar2 =<< apply t2
|
instantiateL alpha2 =<< apply a2
|
||||||
|
|
||||||
-- Γ[ά],ε ⊢ ά :=< E ⊣ Δ,ε,Δ'
|
-- Γ[ά],ε ⊢ ά :=< E ⊣ Δ,ε,Δ'
|
||||||
-- ------------------------- InstLAIIR
|
-- ------------------------- InstLAIIR
|
||||||
-- Γ[ά] ⊢ ά :=< ∀ε.Ε ⊣ Δ
|
-- Γ[ά] ⊢ ά :=< ∀ε.Ε ⊣ Δ
|
||||||
| TAll tvar t <- typ = do
|
go env tevar (TAll tvar t) = do
|
||||||
instantiateL tevar t
|
instantiateL tevar t
|
||||||
let (env_l, _) = splitOn (EnvTVar tvar) env
|
let (env_l, _) = splitOn (EnvTVar tvar) env
|
||||||
putEnv env_l
|
putEnv env_l
|
||||||
|
|
||||||
| otherwise = error $ "Trying to instantiateL: " ++ ppT (TEVar tevar)
|
go _ alpha a = error $ "Trying to instantiateL: " ++ ppT (TEVar alpha)
|
||||||
++ " <: " ++ ppT typ
|
++ " <: " ++ ppT a
|
||||||
|
|
||||||
-- | Γ ⊢ A =:< ά ⊣ Δ
|
-- | Γ ⊢ A =:< ά ⊣ Δ
|
||||||
-- Under input context Γ, instantiate ά such that A <: ά, with output context ∆
|
-- Under input context Γ, instantiate ά such that A <: ά, with output context ∆
|
||||||
instantiateR :: Type -> TEVar -> Tc ()
|
instantiateR :: Type -> TEVar -> Tc ()
|
||||||
instantiateR typ tevar = gets env >>= go
|
instantiateR a alpha = gets env >>= \env -> go env a alpha
|
||||||
where
|
where
|
||||||
go env
|
|
||||||
|
|
||||||
-- Γ ⊢ τ
|
-- Γ ⊢ τ
|
||||||
-- ----------------------------- InstRSolve
|
-- ----------------------------- InstRSolve
|
||||||
-- Γ,ά,Γ' ⊢ τ =:< ά ⊣ Γ,(ά=τ),Γ'
|
-- Γ,ά,Γ' ⊢ τ =:< ά ⊣ Γ,(ά=τ),Γ'
|
||||||
| isMono typ
|
go env tau alpha
|
||||||
, (env_l, env_r) <- splitOn (EnvTEVar tevar) env
|
| isMono tau
|
||||||
, Right _ <- wellFormed env_l typ
|
, (env_l, env_r) <- splitOn (EnvTEVar alpha) env
|
||||||
= putEnv $ (env_l :|> EnvTEVarSolved tevar typ) <> env_r
|
, Right _ <- wellFormed env_l tau
|
||||||
|
= putEnv $ (env_l :|> EnvTEVarSolved alpha tau) <> env_r
|
||||||
|
|
||||||
|
--
|
||||||
|
-- ----------------------------- InstRReach
|
||||||
|
-- Γ[ά][έ] ⊢ έ =:< ά ⊣ Γ[ά][έ=ά]
|
||||||
|
go env (TEVar epsilon) alpha = do
|
||||||
|
let (env_l, env_r) = splitOn (EnvTEVar epsilon) env
|
||||||
|
putEnv $ (env_l :|> EnvTEVarSolved epsilon (TEVar alpha)) <> env_r
|
||||||
|
|
||||||
|
|
||||||
| TEVar tevar' <- typ = instReach tevar tevar'
|
|
||||||
|
|
||||||
-- Γ[ά₂ά₁,(ά=ά₁→ά₂)] ⊢ A₁ :=< ά₁ ⊣ Θ Θ ⊢ ά₂ =:< [Θ]A₂ ⊣ Δ
|
-- Γ[ά₂ά₁,(ά=ά₁→ά₂)] ⊢ A₁ :=< ά₁ ⊣ Θ Θ ⊢ ά₂ =:< [Θ]A₂ ⊣ Δ
|
||||||
-- ------------------------------------------------------- InstRArr
|
-- ------------------------------------------------------- InstRArr
|
||||||
-- Γ[ά] ⊢ ά =:< A₁ → A₂ ⊣ Δ
|
-- Γ[ά] ⊢ A₁ → A₂ =:< ά ⊣ Δ
|
||||||
| TFun t1 t2 <- typ = do
|
go _ (TFun a1 a2) alpha = do
|
||||||
tevar1 <- fresh
|
alpha1 <- fresh
|
||||||
tevar2 <- fresh
|
alpha2 <- fresh
|
||||||
insertEnv $ EnvTEVar tevar2
|
insertEnv $ EnvTEVar alpha2
|
||||||
insertEnv $ EnvTEVar tevar1
|
insertEnv $ EnvTEVar alpha1
|
||||||
insertEnv $ EnvTEVarSolved tevar (on TFun TEVar tevar1 tevar2)
|
insertEnv $ EnvTEVarSolved alpha (on TFun TEVar alpha1 alpha2)
|
||||||
instantiateL tevar1 t1
|
instantiateL alpha1 a1
|
||||||
t2' <- apply t2
|
a2' <- apply a2
|
||||||
instantiateR t2' tevar2
|
instantiateR a2' alpha2
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
-- Γ[ά],▶έ,ε ⊢ [έ/ε]E =:< ά ⊣ Δ,▶έ,Δ'
|
-- Γ[ά],▶έ,ε ⊢ [έ/ε]E =:< ά ⊣ Δ,▶έ,Δ'
|
||||||
-- ---------------------------------- InstRAIIL
|
-- ---------------------------------- InstRAIIL
|
||||||
-- Γ[ά] ⊢ ∀ε.Ε =:< ά ⊣ Δ
|
-- Γ[ά] ⊢ ∀ε.Ε =:< ά ⊣ Δ
|
||||||
| TAll tvar t <- typ = do
|
go env (TAll epsilon e) alpha = do
|
||||||
tevar' <- fresh
|
epsilon' <- fresh
|
||||||
insertEnv $ EnvMark tevar'
|
insertEnv $ EnvMark epsilon'
|
||||||
insertEnv $ EnvTVar tvar
|
insertEnv $ EnvTVar epsilon
|
||||||
let t' = substitute tvar tevar' t
|
instantiateR (substitute epsilon epsilon' e) alpha
|
||||||
instantiateR t' tevar
|
let (env_l, _) = splitOn (EnvMark epsilon') env
|
||||||
let (env_l, _) = splitOn (EnvTVar tvar) env
|
|
||||||
putEnv env_l
|
putEnv env_l
|
||||||
|
|
||||||
| otherwise = error $ "Trying to instantiateR: " ++ ppT typ ++ " <: "
|
go _ a alpha = error $ "Trying to instantiateR: " ++ ppT a ++ " <: "
|
||||||
++ ppT (TEVar tevar)
|
++ ppT (TEVar alpha)
|
||||||
|
|
||||||
|
|
||||||
-- ----------------------------- InstLReach
|
|
||||||
-- Γ[ά][έ] ⊢ ά :=< έ ⊣ Γ[ά][έ=ά]
|
|
||||||
--
|
|
||||||
-- ----------------------------- InstRReach
|
|
||||||
-- Γ[ά][έ] ⊢ έ =:< ά ⊣ Γ[ά][έ=ά]
|
|
||||||
instReach :: TEVar -> TEVar -> Tc ()
|
|
||||||
instReach tevar tevar' = do
|
|
||||||
(env_l, env_r) <- gets (splitOn (EnvTEVar tevar') . env)
|
|
||||||
let env_solved = EnvTEVarSolved tevar' $ TEVar tevar
|
|
||||||
putEnv $ (env_l :|> env_solved) <> env_r
|
|
||||||
|
|
||||||
|
|
||||||
---------------------------------------------------------------------------
|
---------------------------------------------------------------------------
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue