Skip to content

fix: AddConField, SetConFieldType robustness #441

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mergify merged 2 commits into from
May 11, 2022
Merged

fix: AddConField, SetConFieldType robustness #441

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4511478
fix: AddConField robustness
brprice May 9, 2022
ca41c79
fix: SetConFieldType robustness
brprice May 9, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
57 changes: 31 additions & 26 deletions primer/src/Primer/App.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,7 @@ import Primer.Core (
)
import Primer.Core.DSL (create, emptyHole, tEmptyHole)
import qualified Primer.Core.DSL as DSL
import Primer.Core.Transform (foldApp, renameVar, unfoldApp, unfoldTApp)
import Primer.Core.Transform (foldApp, renameVar, unfoldAPP, unfoldApp, unfoldTApp)
import Primer.Core.Utils (freeVars, _freeTmVars, _freeTyVars, _freeVarsTy)
import Primer.Eval (EvalDetail, EvalError)
import qualified Primer.Eval as Eval
Expand Down Expand Up @@ -690,18 +690,19 @@ applyProgAction prog mdefName = \case
type_
updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateDecons <=< updateCons)
updateCons e = case unfoldApp e of
(e'@(Con _ con'), args) | con' == con -> do
m' <- DSL.meta
case adjustAt index (Hole m') args of
Just args' -> foldApp e' =<< traverse (descendM updateCons) args'
Nothing -> do
-- The constructor is not applied as far as the changed field,
-- so the full application still typechecks, but its type has changed.
-- Thus, we put the whole thing in to a hole.
Hole <$> DSL.meta <*> (foldApp e' =<< traverse (descendM updateCons) args)
_ ->
-- NB we can't use `transformM` here because we'd end up seeing incomplete applications before full ones
descendM updateCons e
(h, args) -> case unfoldAPP h of
(Con _ con', _tyArgs) | con' == con -> do
m' <- DSL.meta
case adjustAt index (Hole m') args of
Just args' -> foldApp h =<< traverse (descendM updateCons) args'
Nothing -> do
-- The constructor is not applied as far as the changed field,
-- so the full application still typechecks, but its type has changed.
-- Thus, we put the whole thing in to a hole.
Hole <$> DSL.meta <*> (foldApp h =<< traverse (descendM updateCons) args)
_ ->
-- NB we can't use `transformM` here because we'd end up seeing incomplete applications before full ones
descendM updateCons e
updateDecons = transformCaseBranches prog type_ $
traverse $ \cb@(CaseBranch vc binds e) ->
if vc == con
Expand Down Expand Up @@ -740,20 +741,24 @@ applyProgAction prog mdefName = \case
)
)
type_
updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateDecons <=< updateCons)
-- NB: we must updateDecons first, as transformCaseBranches may do
-- synthesis of the scrutinee's type, using the old typedef. Thus we must
-- not update the scrutinee before this happens.
updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateCons <=< updateDecons)
updateCons e = case unfoldApp e of
(e'@(Con _ con'), args) | con' == con -> do
m' <- DSL.meta
case insertAt index (EmptyHole m') args of
Just args' -> foldApp e' =<< traverse (descendM updateCons) args'
Nothing ->
-- The constructor is not applied as far as the field immediately prior to the new one,
-- so the full application still typechecks, but its type has changed.
-- Thus, we put the whole thing in to a hole.
Hole <$> DSL.meta <*> (foldApp e' =<< traverse (descendM updateCons) args)
_ ->
-- NB we can't use `transformM` here because we'd end up seeing incomplete applications before full ones
descendM updateCons e
(h, args) -> case unfoldAPP h of
(Con _ con', _tyArgs) | con' == con -> do
m' <- DSL.meta
case insertAt index (EmptyHole m') args of
Just args' -> foldApp h =<< traverse (descendM updateCons) args'
Nothing ->
-- The constructor is not applied as far as the field immediately prior to the new one,
-- so the full application still typechecks, but its type has changed.
-- Thus, we put the whole thing in to a hole.
Hole <$> DSL.meta <*> (foldApp h =<< traverse (descendM updateCons) args)
_ ->
-- NB we can't use `transformM` here because we'd end up seeing incomplete applications before full ones
descendM updateCons e
updateDecons = transformCaseBranches prog type_ $
traverse $ \cb@(CaseBranch vc binds e) ->
if vc == con
Expand Down
61 changes: 54 additions & 7 deletions primer/test/Tests/Action/Prog.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,6 @@ import Primer.Core.DSL (
con,
create,
emptyHole,
gvar,
hole,
lAM,
lam,
Expand Down Expand Up @@ -909,7 +908,11 @@ unit_SetConFieldType :: Assertion
unit_SetConFieldType =
progActionTest
( defaultProgEditableTypeDefs . sequence . pure $ do
x <- con cA `app` lvar "x" `app` (gvar (gvn "y") `ann` tcon (tcn "Bool"))
x <-
con cA `aPP` tEmptyHole `aPP` tEmptyHole
`app` con (vcn "True")
`app` con (vcn "True")
`app` con (vcn "True")
astDef "def" x <$> tEmptyHole
)
[SetConFieldType tT cA 1 $ TCon () (tcn "Int")]
Expand All @@ -923,7 +926,10 @@ unit_SetConFieldType =
forgetIDs (astDefExpr def)
@?= forgetIDs
( fst . create $
con cA `app` lvar "x" `app` hole (gvar (gvn "y") `ann` tcon (tcn "Bool"))
con cA `aPP` tEmptyHole `aPP` tEmptyHole
`app` con (vcn "True")
`app` hole (con (vcn "True"))
`app` con (vcn "True")
)

unit_SetConFieldType_partial_app :: Assertion
Expand Down Expand Up @@ -1016,7 +1022,16 @@ unit_AddConField :: Assertion
unit_AddConField =
progActionTest
( defaultProgEditableTypeDefs $ do
x <- con cA `app` con (vcn "True")
x <-
case_
( con cA `aPP` tEmptyHole `aPP` tEmptyHole
`app` con (vcn "True")
`app` con (vcn "True")
`app` con (vcn "True")
)
[ branch cA [("p", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole
, branch cB [("x", Nothing)] emptyHole
]
sequence
[ astDef "def" x <$> tEmptyHole
]
Expand All @@ -1032,7 +1047,16 @@ unit_AddConField =
forgetIDs (astDefExpr def)
@?= forgetIDs
( fst . create $
con cA `app` con (vcn "True") `app` emptyHole
case_
( con cA `aPP` tEmptyHole `aPP` tEmptyHole
`app` con (vcn "True")
`app` emptyHole
`app` con (vcn "True")
`app` con (vcn "True")
)
[ branch cA [("p", Nothing), ("a24", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole
, branch cB [("x", Nothing)] emptyHole
]
)

unit_AddConField_partial_app :: Assertion
Expand All @@ -1053,8 +1077,31 @@ unit_AddConField_partial_app =
hole $ con cA `app` con (vcn "True")
)

unit_AddConField_case :: Assertion
unit_AddConField_case =
unit_AddConField_partial_app_end :: Assertion
unit_AddConField_partial_app_end =
progActionTest
( defaultProgEditableTypeDefs $ do
x <- con cA `app` con (vcn "True")
sequence
[ astDef "def" x <$> tEmptyHole
]
)
[AddConField tT cA 1 $ TCon () (tcn "Int")]
$ expectSuccess $ \_ prog' -> do
td <- findTypeDef tT prog'
astTypeDefConstructors td
@?= [ ValCon cA [TCon () (tcn "Bool"), TCon () (tcn "Int"), TCon () (tcn "Bool"), TCon () (tcn "Bool")]
, ValCon cB [TVar () "b"]
]
def <- findDef (gvn "def") prog'
forgetIDs (astDefExpr def)
@?= forgetIDs
( fst . create $
con cA `app` con (vcn "True") `app` emptyHole
)

unit_AddConField_case_ann :: Assertion
unit_AddConField_case_ann =
progActionTest
( defaultProgEditableTypeDefs $ do
x <-
Expand Down