From 451147815dfd8aef0a7913f691b6f1f0edfe1da2 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Mon, 9 May 2022 18:01:33 +0100 Subject: [PATCH 1/2] fix: AddConField robustness There are two fixes here. Firstly, ensure that updating case branches is robust when the scrutinee is also updated (due to being an application of the given constructor). Secondly, handle the case of an application of a constructor of a parameterised type, i.e. where the spine includes type applications. --- primer/src/Primer/App.hs | 32 ++++++++++++--------- primer/test/Tests/Action/Prog.hs | 49 +++++++++++++++++++++++++++++--- 2 files changed, 63 insertions(+), 18 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index d5684bed6..a8e203f63 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -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 @@ -740,20 +740,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 diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index cdb31334d..3ce0e04dd 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -1016,7 +1016,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 ] @@ -1032,7 +1041,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 @@ -1053,8 +1071,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 <- From ca41c79c043eeb834435806bdf6c65883ceb8582 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Mon, 9 May 2022 18:29:10 +0100 Subject: [PATCH 2/2] fix: SetConFieldType robustness The fix for AddConField and parameterised types from the previous commit is also needed for SetConFieldType. (The other, about updating both a case scrutinee and a case branch, is not, since the modification to the scrutinee will not affect type inference.) --- primer/src/Primer/App.hs | 25 +++++++++++++------------ primer/test/Tests/Action/Prog.hs | 12 +++++++++--- 2 files changed, 22 insertions(+), 15 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index a8e203f63..afaeb537e 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -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 diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 3ce0e04dd..50cafd414 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -86,7 +86,6 @@ import Primer.Core.DSL ( con, create, emptyHole, - gvar, hole, lAM, lam, @@ -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")] @@ -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