Skip to content

Commit

Permalink
feat: EvalFull use type-level let in BETA redex
Browse files Browse the repository at this point in the history
  • Loading branch information
@brprice
brprice committed Sep 12, 2022
1 parent d7f917d commit 6bc3080
Show file tree
Hide file tree
Showing 2 changed files with 63 additions and 75 deletions.
41 changes: 5 additions & 36 deletions primer/src/Primer/EvalFull.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,6 @@ import Primer.Typecheck.Utils (instantiateValCons', lookupConstructor, mkTAppCon
import Primer.Zipper (
ExprZ,
TypeZ,
bindersBelow,
bindersBelowTy,
down,
focus,
Expand Down Expand Up @@ -129,10 +128,8 @@ data Redex
ElideLet SomeLocal Expr
| -- (λx.t : S -> T) s ~> let x = s:S in t : T
Beta LVarName Expr Type Type Expr
| -- (Λa.t : ∀b.T) S ~> lettype b = S in (lettype a = S in t) : T for b not free in S,t
| -- (Λa.t : ∀b.T) S ~> (lettype a = S in t) : (lettype b = S in T)
BETA TyVarName Expr TyVarName Type Type
| -- (Λa.t : ∀b.T) S ~> letType c = b in letType b = c in (Λa.t : ∀b.T) S for b free in t or S, and fresh c
RenameBETA TyVarName Expr (Set Name)
| -- case C as : T of ... ; C xs -> e ; ... ~> let xs=as:As in e for constructor C of type T, where args have types As
-- also the non-annotated case, as we consider constructors to be synthesisable
-- case C as of ... ; C xs -> e ; ... ~> let xs=as:As in e for constructor C of type T, where args have types As
Expand Down Expand Up @@ -369,21 +366,8 @@ viewRedex tydefs globals dir = \case
Var _ (GlobalVarRef x) | Just (DefAST y) <- x `M.lookup` globals -> pure $ pure $ InlineGlobal x y
App _ (Ann _ (Lam _ x t) (TFun _ src tgt)) s -> pure $ pure $ Beta x t src tgt s
e@App{} -> pure . ApplyPrimFun . thd3 <$> tryPrimFun (M.mapMaybe defPrim globals) e
e@(APP _ (Ann _ (LAM _ a t) (TForall _ b _ ty1)) ty2) ->
-- We would like to say (Λa.t : ∀b.T) S ~> (letType a = S in t) : (letType b = S in T)
-- but we do not have letTypes inside types, so the best we can do is
-- (Λa.t : ∀b.T) S ~> letType b = S in ((letType a = S in t) : T)
-- We need to be careful if a /= b: as this can capture a 'b' inside 'S' or 't'.
-- Thus if necessary we do some renaming
-- (Λa.t : ∀b.T) S ~> letType c = b in letType b = c in (Λa.t : ∀b.T) S for b free in t or S, and fresh c
-- We then ensure the delicate property that we reduce the b=c first, then the BETA, then the c=b
let fvs = freeVars t <> S.map unLocalName (freeVarsTy ty2)
-- we only really need to avoid free things, but avoiding bound
-- things means we do not need to do any further renaming
bvs = bindersBelow (focus t) <> S.map unLocalName (bindersBelowTy $ focus ty2)
in if a /= b && S.member (unLocalName b) fvs
then pure $ pure $ RenameBETA b e (fvs <> bvs)
else pure $ pure $ BETA a t b ty1 ty2
-- (Λa.t : ∀b.T) S ~> (letType a = S in t) : (letType b = S in T)
APP _ (Ann _ (LAM _ a t) (TForall _ b _ ty1)) ty2 -> pure $ pure $ BETA a t b ty1 ty2
e | Just r <- viewCaseRedex tydefs e -> Just r
Ann _ t ty | Chk <- dir, concreteTy ty -> pure $ pure $ Upsilon t ty
_ -> Nothing
Expand Down Expand Up @@ -472,14 +456,6 @@ findRedex tydefs globals dir = go . focus
-- This case should have caught by the TC: a term var is bound by a lettype
LLetType _ _ -> Nothing
-- We have found something like
-- letType c=b in (Λa.t : ∀b.T) S
-- where inlining 'c' would block the BETA redex. Thus we do the BETA first
APP _ (Ann _ (LAM _ a t) (TForall _ b1 _ ty1)) ty2
| LLetType c (TVar _ b2) <- l
, b1 == b2
, S.member (unLocalName c) (freeVars t <> S.map unLocalName (freeVarsTy ty2)) ->
pure $ RExpr ez $ BETA a t b1 ty1 ty2
-- We have found something like
-- let x=y in let y=z in t
-- to substitute the 'x' inside 't' we would need to rename the 'let y'
-- binding, but that is implemented in terms of let:
Expand Down Expand Up @@ -546,15 +522,8 @@ runRedex = \case
ElideLet _ t -> pure t
-- (λx.t : S -> T) s ~> let x = s:S in t : T
Beta x t tyS tyT s -> let_ x (pure s `ann` pure tyS) (pure t) `ann` pure tyT
-- (Λa.t : ∀b.T) S ~> lettype b = S in (lettype a = S in t) : T
-- if b is not free in t or S
BETA a t b tyT tyS
| a == b -> letType a (pure tyS) $ pure t `ann` pure tyT
| otherwise -> letType b (regenerateTypeIDs tyS) $ letType a (pure tyS) (pure t) `ann` pure tyT
-- (Λa.t : ∀b.T) S ~> letType c = b in letType b = c in (Λa.t : ∀b.T) S for b free in t or S, and fresh c
RenameBETA b beta avoid -> do
c <- freshLocalName' avoid
letType c (tvar b) $ letType b (tvar c) $ pure beta
-- (Λa.t : ∀b.T) S ~> (lettype a = S in t) : (lettype b = S in T)
BETA a t b tyT tyS -> letType a (pure tyS) (pure t) `ann` tlet b (regenerateTypeIDs tyS) (pure tyT)
-- case C as : T of ... ; C xs -> e ; ... ~> let xs=as:As in e for constructor C of type T, where args have types As
-- (and also the non-annotated-constructor case)
-- Note that when forming the CaseRedex we checked that the variables @xs@ were fresh for @as@ and @As@,
Expand Down
97 changes: 58 additions & 39 deletions primer/test/Tests/EvalFull.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -581,60 +581,79 @@ unit_type_preservation_case_regression_ty =
unit_type_preservation_BETA_regression :: Assertion
unit_type_preservation_BETA_regression =
let (((exprA, expectedAs), (exprB, expectedBs)), maxID) = create $ do
let n = "a145"
-- The 'A' sequence previously captured in the type "S" above
let eA' b =
-- Λb x. (Λa λc (_ : a) : ∀b.(Nat -> b)) @(b -> Bool) x
eA <-
lAM "b" $
lam "x" $
( lAM "a" (lam "c" $ emptyHole `ann` tvar "a")
`ann` tforall "b" KType (tcon tNat `tfun` tvar "b")
)
`aPP` (tvar b `tapp` tcon tBool)
eA <- lAM "b" $ eA' "b"
-- Do some renaming to set up
expectA1 <- lAM "b" $ letType n (tvar "b") $ letType "b" (tvar n) $ eA' "b"
-- Resolve the renaming
expectA3 <- lAM "b" $ letType n (tvar "b") $ eA' n
`aPP` (tvar "b" `tapp` tcon tBool)
`app` lvar "x"
-- Do the BETA step
-- Λb x. ((lettype a = b Bool in λc (_ : a)) : (let b = b Bool in Nat -> b)) x
expectA1 <-
lAM "b" $
lam "x" $
( letType "a" (tvar "b" `tapp` tcon tBool) (lam "c" $ emptyHole `ann` tvar "a")
`ann` tlet "b" (tvar "b" `tapp` tcon tBool) (tcon tNat `tfun` tvar "b")
)
`app` lvar "x"
-- NB: the point of the ... `app` lvar x is to make the annotated term be in SYN position
-- so we reduce the type, rather than taking an upsilon step
-- Rename the let b
-- Λb. λx. ((lettype a = b Bool in λc (_ : a)) : (let c = b Bool in let b = c in Nat -> b)) x
let b' = "a132"
expectA2 <-
lAM "b" $
lam "x" $
( letType "a" (tvar "b" `tapp` tcon tBool) (lam "c" $ emptyHole `ann` tvar "a")
`ann` tlet b' (tvar "b" `tapp` tcon tBool) (tlet "b" (tvar b') $ tcon tNat `tfun` tvar "b")
)
`app` lvar "x"
-- Resolve the renaming
-- Λb. λx. ((lettype a = b Bool in λc (_ : a)) : (let c = b Bool in Nat -> c)) x
expectA4 <-
lAM "b" $
letType n (tvar "b") $
letType "b" (tvar n `tapp` tcon tBool) $
letType
"a"
(tvar n `tapp` tcon tBool)
(lam "c" $ emptyHole `ann` tvar "a")
`ann` (tcon tNat `tfun` tvar "b")
lam "x" $
( letType "a" (tvar "b" `tapp` tcon tBool) (lam "c" $ emptyHole `ann` tvar "a")
`ann` tlet b' (tvar "b" `tapp` tcon tBool) (tcon tNat `tfun` tvar b')
)
`app` lvar "x"
-- Resolve all the letTypes
expectA11 <-
-- Λb. λx. ((λc (_ : b Bool)) : (Nat -> b Bool)) x
expectA8 <-
lAM "b" $
lam "c" (emptyHole `ann` (tvar "b" `tapp` tcon tBool))
`ann` (tcon tNat `tfun` (tvar "b" `tapp` tcon tBool))
-- The 'B' sequence previously captured in the term "t" above
let eB' b =
( lAM "a" (gvar foo `aPP` (tvar b `tapp` tcon tBool))
`ann` tforall "b" KType (tcon tNat)
lam "x" $
( lam "c" (emptyHole `ann` (tvar "b" `tapp` tcon tBool))
`ann` (tcon tNat `tfun` (tvar "b" `tapp` tcon tBool))
)
`aPP` tcon tChar
eB <- lAM "b" $ eB' "b"
-- Do some renaming to set up
expectB1 <- lAM "b" $ letType n (tvar "b") $ letType "b" (tvar n) $ eB' "b"
-- Resolve the renaming
expectB3 <- lAM "b" $ letType n (tvar "b") $ eB' n
-- Do the BETA step
expectB4 <-
`app` lvar "x"
-- The 'B' sequence previously captured in the term "t" above
-- Λb. (Λa (foo @(b Bool) : ∀b.Nat) @Char
eB <-
lAM "b" $
( lAM "a" (gvar foo `aPP` (tvar "b" `tapp` tcon tBool))
`ann` tforall "b" KType (tcon tNat)
)
`aPP` tcon tChar
-- BETA step
-- Λb. (lettype a = Char in foo @(b Bool)) : (let b = Char in Nat)
expectB1 <-
lAM "b" $
letType n (tvar "b") $
letType "b" (tcon tChar) $
letType "a" (tcon tChar) (gvar foo `aPP` (tvar n `tapp` tcon tBool))
`ann` tcon tNat
-- Resolve all the letTypes (and elide an annotation)
expectB9 <- lAM "b" $ gvar foo `aPP` (tvar "b" `tapp` tcon tBool)
letType "a" (tcon tChar) (gvar foo `aPP` (tvar "b" `tapp` tcon tBool))
`ann` tlet "b" (tcon tChar) (tcon tNat)
-- Drop annotation and elide lettype
-- Λb. foo @(b Bool)
expectB3 <- lAM "b" $ gvar foo `aPP` (tvar "b" `tapp` tcon tBool)
-- Note that the reduction of eA and eB take slightly
-- different paths: we do not remove the annotation in eA
-- because it has an occurrence of a type variable and is thus
-- not "concrete"
pure
( (eA, [(1, expectA1), (3, expectA3), (4, expectA4), (11, expectA11)])
, (eB, [(1, expectB1), (3, expectB3), (4, expectB4), (9, expectB9)])
( (eA, [(1, expectA1), (2, expectA2), (4, expectA4), (8, expectA8)])
, (eB, [(1, expectB1), (3, expectB3)])
)
sA n = evalFullTest maxID builtinTypes mempty n Chk exprA
sB n = evalFullTest maxID builtinTypes mempty n Chk exprB
Expand Down Expand Up @@ -1232,7 +1251,7 @@ unit_prim_partial_map =
]
`ann` (tcon tList `tapp` tcon tChar)
<*> pure (M.singleton mapName mapDef)
s = evalFullTest maxID builtinTypes (gs <> primDefs) 65 Syn e
s = evalFullTest maxID builtinTypes (gs <> primDefs) 67 Syn e
in do
distinctIDs s
s <~==> Right r
Expand Down

0 comments on commit 6bc3080

Please sign in to comment.