From 5a1376bac33db0ba90ec012ab8534114c4a7aceb Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 21 Mar 2023 13:33:57 +0000 Subject: [PATCH 01/13] feat: comprehensiveWellTyped has fully-saturated constructors This is a step towards all constructors being (fully) saturated, at which point we can update the typechecker to enforce that invariant. (Both versions of the testsuite currently pass, but when non-saturated constructors are rejected the old version would fail.) --- primer/src/Primer/Examples.hs | 14 +- .../Beginner-Editable.fragment | 218 +++++++- .../Beginner-NonEditable.fragment | 80 ++- .../M.comprehensive/Expert-Editable.fragment | 528 +++++++++++++++++- .../Expert-NonEditable.fragment | 80 ++- .../Intermediate-Editable.fragment | 222 +++++++- .../Intermediate-NonEditable.fragment | 80 ++- 7 files changed, 1127 insertions(+), 95 deletions(-) diff --git a/primer/src/Primer/Examples.hs b/primer/src/Primer/Examples.hs index 607f910b5..d3aa1dd86 100644 --- a/primer/src/Primer/Examples.hs +++ b/primer/src/Primer/Examples.hs @@ -270,12 +270,14 @@ comprehensive' typeable modName = do ( app ( aPP ( if typeable - then -- TODO (saturated constructors) this line is - -- only acceptible (i.e. makes a well typed - -- example) because constructors currently - -- need not be fully-saturated, and are - -- synthesisable. - con B.cLeft [tcon B.tBool] [] + then + lAM "b" (lam "x" $ con B.cLeft [tcon B.tBool, tvar "b"] [lvar "x"]) + `ann` tforall + "b" + KType + ( tcon B.tBool + `tfun` (tcon B.tEither `tapp` tcon B.tBool `tapp` tvar "b") + ) else letType "b" diff --git a/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment index 82856f700..914189190 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment @@ -554,6 +554,69 @@ Output , NoInput DeleteExpr ] ) + , + ( 26 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 27 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "p" + , context = Nothing + } + , Option + { option = "q" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , Input RenameLam + ( Options + { opts = + [ Option + { option = "p" + , context = Nothing + } + , Option + { option = "q" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteExpr + ] + ) , ( 28 , @@ -576,12 +639,13 @@ Output , free = FreeVarName } ) + , NoInput MakeCase , NoInput Raise , NoInput DeleteExpr ] ) , - ( 29 + ( 31 , [ Input MakeLam ( Options @@ -608,7 +672,33 @@ Output ] ) , - ( 30 + ( 41 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 42 , [ Input MakeLam ( Options @@ -635,7 +725,34 @@ Output ] ) , - ( 31 + ( 43 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeCase + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 44 , [ Input RenamePattern ( Options @@ -663,7 +780,7 @@ Output ] ) , - ( 32 + ( 45 , [ Input MakeLam ( Options @@ -690,7 +807,7 @@ Output ] ) , - ( 33 + ( 46 , [ Input MakeLam ( Options @@ -717,7 +834,7 @@ Output ] ) , - ( 34 + ( 47 , [ Input MakeLam ( Options @@ -800,7 +917,7 @@ Output ] ) , - ( 35 + ( 48 , [ Input MakeLam ( Options @@ -827,7 +944,7 @@ Output ] ) , - ( 36 + ( 49 , [ Input MakeLam ( Options @@ -922,24 +1039,64 @@ Output ] ) , - ( 26 + ( 29 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 27 + ( 30 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 37 + ( 32 + , + [ NoInput MakeFun + , NoInput DeleteType + ] + ) + , + ( 33 , [ NoInput MakeFun , NoInput AddInput + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 34 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 35 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 36 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 37 + , + [ NoInput MakeFun + , NoInput Raise , NoInput DeleteType ] ) @@ -961,6 +1118,21 @@ Output ) , ( 40 + , + [ NoInput MakeFun + , NoInput DeleteType + ] + ) + , + ( 50 + , + [ NoInput MakeFun + , NoInput AddInput + , NoInput DeleteType + ] + ) + , + ( 51 , [ NoInput MakeFun , NoInput Raise @@ -968,7 +1140,7 @@ Output ] ) , - ( 41 + ( 52 , [ NoInput MakeFun , NoInput Raise @@ -976,7 +1148,7 @@ Output ] ) , - ( 42 + ( 53 , [ NoInput MakeFun , NoInput Raise @@ -984,7 +1156,7 @@ Output ] ) , - ( 43 + ( 54 , [ NoInput MakeFun , NoInput Raise @@ -992,7 +1164,23 @@ Output ] ) , - ( 44 + ( 55 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 56 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 57 , [ NoInput MakeFun , NoInput Raise diff --git a/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment index 7e5455083..1a69e1d3f 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment @@ -58,15 +58,15 @@ Output , [] ) , - ( 28 + ( 26 , [] ) , - ( 29 + ( 27 , [] ) , - ( 30 + ( 28 , [] ) , @@ -74,23 +74,39 @@ Output , [] ) , - ( 32 + ( 41 , [] ) , - ( 33 + ( 42 , [] ) , - ( 34 + ( 43 , [] ) , - ( 35 + ( 44 , [] ) , - ( 36 + ( 45 + , [] + ) + , + ( 46 + , [] + ) + , + ( 47 + , [] + ) + , + ( 48 + , [] + ) + , + ( 49 , [] ) , @@ -106,11 +122,31 @@ Output , [] ) , - ( 26 + ( 29 , [] ) , - ( 27 + ( 30 + , [] + ) + , + ( 32 + , [] + ) + , + ( 33 + , [] + ) + , + ( 34 + , [] + ) + , + ( 35 + , [] + ) + , + ( 36 , [] ) , @@ -130,19 +166,35 @@ Output , [] ) , - ( 41 + ( 50 , [] ) , - ( 42 + ( 51 , [] ) , - ( 43 + ( 52 , [] ) , - ( 44 + ( 53 + , [] + ) + , + ( 54 + , [] + ) + , + ( 55 + , [] + ) + , + ( 56 + , [] + ) + , + ( 57 , [] ) ] diff --git a/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment index 4a9d23f02..c3d672681 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment @@ -1143,6 +1143,117 @@ Output ) , NoInput MakeApp , NoInput MakeAPP + , Input MakeLAM + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput RemoveAnn + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 26 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , NoInput MakeAPP + , Input MakeLAM + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeAnn + , Input RenameLAM + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 27 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "p" + , context = Nothing + } + , Option + { option = "q" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , NoInput MakeAPP , Input MakeLAM ( Options { opts = @@ -1163,6 +1274,21 @@ Output } ) , NoInput MakeAnn + , Input RenameLam + ( Options + { opts = + [ Option + { option = "p" + , context = Nothing + } + , Option + { option = "q" + , context = Nothing + } + ] + , free = FreeVarName + } + ) , NoInput Raise , NoInput DeleteExpr ] @@ -1189,6 +1315,7 @@ Output , free = FreeVarName } ) + , NoInput MakeCase , NoInput MakeApp , NoInput MakeAPP , Input MakeLAM @@ -1216,7 +1343,7 @@ Output ] ) , - ( 29 + ( 31 , [ Input MakeLam ( Options @@ -1265,7 +1392,55 @@ Output ] ) , - ( 30 + ( 41 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , NoInput MakeAPP + , Input MakeLAM + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeAnn + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 42 , [ Input MakeLam ( Options @@ -1314,7 +1489,56 @@ Output ] ) , - ( 31 + ( 43 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeCase + , NoInput MakeApp + , NoInput MakeAPP + , Input MakeLAM + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeAnn + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 44 , [ Input RenamePattern ( Options @@ -1342,7 +1566,7 @@ Output ] ) , - ( 32 + ( 45 , [ Input MakeLam ( Options @@ -1391,7 +1615,7 @@ Output ] ) , - ( 33 + ( 46 , [ Input MakeLam ( Options @@ -1440,7 +1664,7 @@ Output ] ) , - ( 34 + ( 47 , [ Input MakeLam ( Options @@ -1688,7 +1912,7 @@ Output ] ) , - ( 35 + ( 48 , [ Input MakeLam ( Options @@ -1737,7 +1961,7 @@ Output ] ) , - ( 36 + ( 49 , [ Input MakeLam ( Options @@ -1920,7 +2144,7 @@ Output ] ) , - ( 26 + ( 29 , [ NoInput MakeFun , NoInput MakeTApp @@ -1947,7 +2171,7 @@ Output ] ) , - ( 27 + ( 30 , [ NoInput MakeFun , NoInput MakeTApp @@ -1973,8 +2197,278 @@ Output , NoInput DeleteType ] ) + , + ( 32 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , Input RenameForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput DeleteType + ] + ) + , + ( 33 + , + [ NoInput MakeFun + , NoInput AddInput + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 34 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 35 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 36 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteType + ] + ) , ( 37 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 38 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 39 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 40 + , + [ NoInput MakeFun + , NoInput MakeTApp + , Input MakeForall + ( Options + { opts = + [ Option + { option = "α" + , context = Nothing + } + , Option + { option = "γ" + , context = Nothing + } + , Option + { option = "β1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput DeleteType + ] + ) + , + ( 50 , [ NoInput MakeFun , NoInput AddInput @@ -2002,7 +2496,7 @@ Output ] ) , - ( 38 + ( 51 , [ NoInput MakeFun , NoInput MakeTApp @@ -2030,7 +2524,7 @@ Output ] ) , - ( 39 + ( 52 , [ NoInput MakeFun , NoInput MakeTApp @@ -2077,7 +2571,7 @@ Output ] ) , - ( 40 + ( 53 , [ NoInput MakeFun , NoInput MakeTApp @@ -2105,7 +2599,7 @@ Output ] ) , - ( 41 + ( 54 , [ NoInput MakeFun , NoInput MakeTApp @@ -2133,7 +2627,7 @@ Output ] ) , - ( 42 + ( 55 , [ NoInput MakeFun , NoInput MakeTApp @@ -2161,7 +2655,7 @@ Output ] ) , - ( 43 + ( 56 , [ NoInput MakeFun , NoInput MakeTApp @@ -2189,7 +2683,7 @@ Output ] ) , - ( 44 + ( 57 , [ NoInput MakeFun , NoInput MakeTApp diff --git a/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment index 7e5455083..1a69e1d3f 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment @@ -58,15 +58,15 @@ Output , [] ) , - ( 28 + ( 26 , [] ) , - ( 29 + ( 27 , [] ) , - ( 30 + ( 28 , [] ) , @@ -74,23 +74,39 @@ Output , [] ) , - ( 32 + ( 41 , [] ) , - ( 33 + ( 42 , [] ) , - ( 34 + ( 43 , [] ) , - ( 35 + ( 44 , [] ) , - ( 36 + ( 45 + , [] + ) + , + ( 46 + , [] + ) + , + ( 47 + , [] + ) + , + ( 48 + , [] + ) + , + ( 49 , [] ) , @@ -106,11 +122,31 @@ Output , [] ) , - ( 26 + ( 29 , [] ) , - ( 27 + ( 30 + , [] + ) + , + ( 32 + , [] + ) + , + ( 33 + , [] + ) + , + ( 34 + , [] + ) + , + ( 35 + , [] + ) + , + ( 36 , [] ) , @@ -130,19 +166,35 @@ Output , [] ) , - ( 41 + ( 50 , [] ) , - ( 42 + ( 51 , [] ) , - ( 43 + ( 52 , [] ) , - ( 44 + ( 53 + , [] + ) + , + ( 54 + , [] + ) + , + ( 55 + , [] + ) + , + ( 56 + , [] + ) + , + ( 57 , [] ) ] diff --git a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment index 016dba77e..0f7a2163e 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment @@ -854,6 +854,71 @@ Output , NoInput DeleteExpr ] ) + , + ( 26 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 27 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "p" + , context = Nothing + } + , Option + { option = "q" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , Input RenameLam + ( Options + { opts = + [ Option + { option = "p" + , context = Nothing + } + , Option + { option = "q" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput Raise + , NoInput DeleteExpr + ] + ) , ( 28 , @@ -876,13 +941,14 @@ Output , free = FreeVarName } ) + , NoInput MakeCase , NoInput MakeApp , NoInput Raise , NoInput DeleteExpr ] ) , - ( 29 + ( 31 , [ Input MakeLam ( Options @@ -910,7 +976,34 @@ Output ] ) , - ( 30 + ( 41 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeApp + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 42 , [ Input MakeLam ( Options @@ -938,7 +1031,35 @@ Output ] ) , - ( 31 + ( 43 + , + [ Input MakeLam + ( Options + { opts = + [ Option + { option = "z" + , context = Nothing + } + , Option + { option = "x1" + , context = Nothing + } + , Option + { option = "y1" + , context = Nothing + } + ] + , free = FreeVarName + } + ) + , NoInput MakeCase + , NoInput MakeApp + , NoInput Raise + , NoInput DeleteExpr + ] + ) + , + ( 44 , [ Input RenamePattern ( Options @@ -966,7 +1087,7 @@ Output ] ) , - ( 32 + ( 45 , [ Input MakeLam ( Options @@ -994,7 +1115,7 @@ Output ] ) , - ( 33 + ( 46 , [ Input MakeLam ( Options @@ -1022,7 +1143,7 @@ Output ] ) , - ( 34 + ( 47 , [ Input MakeLam ( Options @@ -1249,7 +1370,7 @@ Output ] ) , - ( 35 + ( 48 , [ Input MakeLam ( Options @@ -1277,7 +1398,7 @@ Output ] ) , - ( 36 + ( 49 , [ Input MakeLam ( Options @@ -1373,24 +1494,64 @@ Output ] ) , - ( 26 + ( 29 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 27 + ( 30 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 37 + ( 32 + , + [ NoInput MakeFun + , NoInput DeleteType + ] + ) + , + ( 33 , [ NoInput MakeFun , NoInput AddInput + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 34 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 35 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 36 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 37 + , + [ NoInput MakeFun + , NoInput Raise , NoInput DeleteType ] ) @@ -1412,6 +1573,21 @@ Output ) , ( 40 + , + [ NoInput MakeFun + , NoInput DeleteType + ] + ) + , + ( 50 + , + [ NoInput MakeFun + , NoInput AddInput + , NoInput DeleteType + ] + ) + , + ( 51 , [ NoInput MakeFun , NoInput Raise @@ -1419,7 +1595,7 @@ Output ] ) , - ( 41 + ( 52 , [ NoInput MakeFun , NoInput Raise @@ -1427,7 +1603,7 @@ Output ] ) , - ( 42 + ( 53 , [ NoInput MakeFun , NoInput Raise @@ -1435,7 +1611,7 @@ Output ] ) , - ( 43 + ( 54 , [ NoInput MakeFun , NoInput Raise @@ -1443,7 +1619,23 @@ Output ] ) , - ( 44 + ( 55 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 56 + , + [ NoInput MakeFun + , NoInput Raise + , NoInput DeleteType + ] + ) + , + ( 57 , [ NoInput MakeFun , NoInput Raise diff --git a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment index 7e5455083..1a69e1d3f 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment @@ -58,15 +58,15 @@ Output , [] ) , - ( 28 + ( 26 , [] ) , - ( 29 + ( 27 , [] ) , - ( 30 + ( 28 , [] ) , @@ -74,23 +74,39 @@ Output , [] ) , - ( 32 + ( 41 , [] ) , - ( 33 + ( 42 , [] ) , - ( 34 + ( 43 , [] ) , - ( 35 + ( 44 , [] ) , - ( 36 + ( 45 + , [] + ) + , + ( 46 + , [] + ) + , + ( 47 + , [] + ) + , + ( 48 + , [] + ) + , + ( 49 , [] ) , @@ -106,11 +122,31 @@ Output , [] ) , - ( 26 + ( 29 , [] ) , - ( 27 + ( 30 + , [] + ) + , + ( 32 + , [] + ) + , + ( 33 + , [] + ) + , + ( 34 + , [] + ) + , + ( 35 + , [] + ) + , + ( 36 , [] ) , @@ -130,19 +166,35 @@ Output , [] ) , - ( 41 + ( 50 , [] ) , - ( 42 + ( 51 , [] ) , - ( 43 + ( 52 , [] ) , - ( 44 + ( 53 + , [] + ) + , + ( 54 + , [] + ) + , + ( 55 + , [] + ) + , + ( 56 + , [] + ) + , + ( 57 , [] ) ] From a0bef7d960b9431aac54fc9ee44ac915b3ac7149 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 4 Apr 2023 12:27:27 +0100 Subject: [PATCH 02/13] feat: Tests.Action.Prog uses saturated constructor action This is preperation for removal of the `ConstructCon` action, which will make no sense once the typechecker enforces all constructors to be fully saturated. --- primer/test/Tests/Action/Prog.hs | 30 +++++++++++------------------- 1 file changed, 11 insertions(+), 19 deletions(-) diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 22f703439..55a2c235b 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -29,6 +29,7 @@ import Primer.Action ( Branch, Child1, Child2, + ConChild, Parent ), ) @@ -121,7 +122,7 @@ import Primer.Module (Module (Module, moduleDefs, moduleName, moduleTypes), buil import Primer.Name import Primer.Primitives (PrimDef (IntAdd, ToUpper), primitiveGVar, tChar) import Primer.Test.TestM (TestM, evalTestM) -import Primer.Test.Util (LogMsg, assertNoSevereLogs, constructCon, constructTCon, zeroIDs, zeroTypeIDs) +import Primer.Test.Util (LogMsg, assertNoSevereLogs, constructSaturatedCon, constructTCon, zeroIDs, zeroTypeIDs) import Primer.Test.Util qualified as Util import Primer.TypeDef (ASTTypeDef (..), TypeDef (..), ValCon (..), forgetTypeDefMetadata, typeDefAST) import Primer.Typecheck ( @@ -1448,27 +1449,18 @@ unit_cross_module_actions = , ConstructVar (GlobalVarRef $ qualifyM "foo") , Move Parent , Move Child2 - , ConstructApp - , Move Child1 - , constructCon (qualifyM "C") - , Move Parent - , Move Child2 - , constructCon cZero + , constructSaturatedCon (qualifyM "C") + , Move $ ConChild 0 + , constructSaturatedCon cZero , Move Parent , Move Parent , ConstructCase , Move (Branch (qualifyM "C")) - , ConstructApp - , Move Child1 - , constructCon (qualifyM "C") - , Move Parent - , Move Child2 - , ConstructApp - , Move Child1 - , constructCon cSucc - , Move Parent - , Move Child2 - , ConstructVar (LocalVarRef "a38") + , constructSaturatedCon (qualifyM "C") + , Move $ ConChild 0 + , constructSaturatedCon cSucc + , Move $ ConChild 0 + , ConstructVar (LocalVarRef "a42") ] ] handleAndTC [RenameDef (qualifyM "foo") "bar"] @@ -1504,7 +1496,7 @@ unit_cross_module_actions = , ConstructVar $ GlobalVarRef $ qualifyName (ModuleName ["AnotherModule"]) "bar" , Move Parent , Move Child2 - , constructCon cTrue + , constructSaturatedCon cTrue ] ] -- Copy-paste within the sig of bar to make bar :: Bool -> Bool From f6b91f118401a5b827d0e5015ae3440699946619 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 21 Mar 2023 17:58:48 +0000 Subject: [PATCH 03/13] feat: MakeConSat nullary options and levels Prior to this commit, "Insert a saturated constructor" did not offer nullary constructors. Nullary constructors were offered only by "Insert a constructor". With this commit, "Insert a saturated constructor" now always offers nullary constructors, and in beginner mode only offers nullary constructors. This change is with a view to merging "Insert a saturated constructor" and "Insert a constructor" actions. This commit changes the data we emit via the OpenAPI endpoints. However, it obeys the same schema (and consumers are expected to not care about the exact data we emit), and is thus not a breaking change. Note that it does not affect the actions stored in undo logs, and thus will not break programs loaded from older databases that were created with older versions of primer. --- primer/src/Primer/Action/Available.hs | 2 +- .../M.comprehensive/Expert-Editable.fragment | 45 +++++++++++++++++++ .../Intermediate-Editable.fragment | 45 +++++++++++++++++++ 3 files changed, 91 insertions(+), 1 deletion(-) diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs index 05f48bcb4..d720a0b50 100644 --- a/primer/src/Primer/Action/Available.hs +++ b/primer/src/Primer/Action/Available.hs @@ -340,7 +340,7 @@ options typeDefs defs cxt level def mNodeSel = \case pure . noFree . map (globalOpt . valConName . snd) - . filter (uncurry hasArgsCon) + . filter (not . (&& level == Beginner) . uncurry hasArgsCon) . concatMap (\td -> (td,) <$> astTypeDefConstructors td) . mapMaybe (typeDefAST . snd) $ Map.toList typeDefs diff --git a/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment index c3d672681..80910c8b5 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment @@ -457,6 +457,16 @@ Output ( Options { opts = [ Option + { option = "True" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "False" + , context = Just + ( "Builtins" :| [] ) + } + , Option { option = "Left" , context = Just ( "Builtins" :| [] ) @@ -486,6 +496,11 @@ Output , context = Just ( "Builtins" :| [] ) } + , Option + { option = "Zero" + , context = Just + ( "Builtins" :| [] ) + } , Option { option = "Succ" , context = Just @@ -697,6 +712,16 @@ Output ( Options { opts = [ Option + { option = "True" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "False" + , context = Just + ( "Builtins" :| [] ) + } + , Option { option = "Left" , context = Just ( "Builtins" :| [] ) @@ -726,6 +751,11 @@ Output , context = Just ( "Builtins" :| [] ) } + , Option + { option = "Zero" + , context = Just + ( "Builtins" :| [] ) + } , Option { option = "Succ" , context = Just @@ -1780,6 +1810,16 @@ Output ( Options { opts = [ Option + { option = "True" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "False" + , context = Just + ( "Builtins" :| [] ) + } + , Option { option = "Left" , context = Just ( "Builtins" :| [] ) @@ -1809,6 +1849,11 @@ Output , context = Just ( "Builtins" :| [] ) } + , Option + { option = "Zero" + , context = Just + ( "Builtins" :| [] ) + } , Option { option = "Succ" , context = Just diff --git a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment index 0f7a2163e..d0e312f15 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment @@ -331,6 +331,16 @@ Output ( Options { opts = [ Option + { option = "True" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "False" + , context = Just + ( "Builtins" :| [] ) + } + , Option { option = "Left" , context = Just ( "Builtins" :| [] ) @@ -360,6 +370,11 @@ Output , context = Just ( "Builtins" :| [] ) } + , Option + { option = "Zero" + , context = Just + ( "Builtins" :| [] ) + } , Option { option = "Succ" , context = Just @@ -550,6 +565,16 @@ Output ( Options { opts = [ Option + { option = "True" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "False" + , context = Just + ( "Builtins" :| [] ) + } + , Option { option = "Left" , context = Just ( "Builtins" :| [] ) @@ -579,6 +604,11 @@ Output , context = Just ( "Builtins" :| [] ) } + , Option + { option = "Zero" + , context = Just + ( "Builtins" :| [] ) + } , Option { option = "Succ" , context = Just @@ -1259,6 +1289,16 @@ Output ( Options { opts = [ Option + { option = "True" + , context = Just + ( "Builtins" :| [] ) + } + , Option + { option = "False" + , context = Just + ( "Builtins" :| [] ) + } + , Option { option = "Left" , context = Just ( "Builtins" :| [] ) @@ -1288,6 +1328,11 @@ Output , context = Just ( "Builtins" :| [] ) } + , Option + { option = "Zero" + , context = Just + ( "Builtins" :| [] ) + } , Option { option = "Succ" , context = Just From 042b23cc25cb1669892e7198ac78f4a9ee9502ce Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 21 Mar 2023 17:54:05 +0000 Subject: [PATCH 04/13] feat!: remove ConstructCon, MakeCon actions as non-saturated We leave ConstructSaturatedCon, ConstructRefinedCon and MakeConSat which create saturated constructors. Note that they behave the same for nullary constructors, and inserting a non-applied constructor (which has arguments) will not make sense when all constructors must be saturated. This is a step towards all constructors being saturated, at which point we can update the typechecker to enforce that invariant. BREAKING CHANGE: this removes an action that may be stored in the undo log of a program from a database created with an older version of primer. This will break loading old databases. --- .../test/outputs/OpenAPI/openapi.json | 2 - primer/src/Primer/Action.hs | 11 -- primer/src/Primer/Action/Actions.hs | 2 - primer/src/Primer/Action/Available.hs | 15 +- primer/src/Primer/Action/Priorities.hs | 4 - primer/test/Tests/Action.hs | 27 ++- .../Beginner-Editable.fragment | 12 +- .../M.comprehensive/Expert-Editable.fragment | 186 ------------------ .../Intermediate-Editable.fragment | 186 ------------------ primer/testlib/Primer/Test/Util.hs | 6 +- 10 files changed, 22 insertions(+), 429 deletions(-) diff --git a/primer-service/test/outputs/OpenAPI/openapi.json b/primer-service/test/outputs/OpenAPI/openapi.json index 297e72d98..a3cb60972 100644 --- a/primer-service/test/outputs/OpenAPI/openapi.json +++ b/primer-service/test/outputs/OpenAPI/openapi.json @@ -170,7 +170,6 @@ }, "InputAction": { "enum": [ - "MakeCon", "MakeConSat", "MakeInt", "MakeChar", @@ -1063,7 +1062,6 @@ "required": true, "schema": { "enum": [ - "MakeCon", "MakeConSat", "MakeInt", "MakeChar", diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index f8f870362..d39cd4266 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -69,7 +69,6 @@ import Primer.Core.DSL ( branch, case_, con, - con0, emptyHole, hole, lAM, @@ -350,7 +349,6 @@ applyAction' a = case a of RemoveAnn -> termAction removeAnn "there are no annotations in types" ConstructLam x -> termAction (constructLam x) "cannot construct function in type" ConstructLAM x -> termAction (constructLAM x) "cannot construct function in type" - ConstructCon c -> termAction (constructCon c) "cannot construct con in type" ConstructPrim p -> termAction (constructPrim p) "cannot construct primitive literal in type" ConstructSaturatedCon c -> termAction (constructSatCon c) "cannot construct con in type" ConstructRefinedCon c -> termAction (constructRefinedCon c) "cannot construct con in type" @@ -614,12 +612,6 @@ constructLAM mx ze = do result <- flip replace ze <$> lAM x (pure (target ze)) moveExpr Child1 result --- TODO (saturated constructors) this action will make no sense once full-saturation is enforced -constructCon :: ActionM m => QualifiedText -> ExprZ -> m ExprZ -constructCon c ze = case target ze of - EmptyHole{} -> flip replace ze <$> con0 (unsafeMkGlobalName c) - e -> throwError $ NeedEmptyHole (ConstructCon c) e - constructPrim :: ActionM m => PrimCon -> ExprZ -> m ExprZ constructPrim p ze = case target ze of EmptyHole{} -> flip replace ze <$> prim p @@ -971,9 +963,6 @@ toProgActionInput :: Available.InputAction -> Either ActionError [ProgAction] toProgActionInput def defName mNodeSel opt0 = \case - Available.MakeCon -> do - opt <- optGlobal - toProg [ConstructCon opt] Available.MakeConSat -> do ref <- offerRefined opt <- optGlobal diff --git a/primer/src/Primer/Action/Actions.hs b/primer/src/Primer/Action/Actions.hs index cf4124e5b..902de34fc 100644 --- a/primer/src/Primer/Action/Actions.hs +++ b/primer/src/Primer/Action/Actions.hs @@ -58,8 +58,6 @@ data Action ConstructLam (Maybe Text) | -- | Construct a type abstraction "big-lambda" ConstructLAM (Maybe Text) - | -- | Put a constructor in an empty hole - ConstructCon QualifiedText | -- | Put a literal in an empty hole ConstructPrim PrimCon | -- | Put a constructor applied to a saturated spine in an empty hole diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs index d720a0b50..e3ec29151 100644 --- a/primer/src/Primer/Action/Available.hs +++ b/primer/src/Primer/Action/Available.hs @@ -122,8 +122,7 @@ data NoInputAction -- | An action which requires extra data (often a name) before it can be applied. data InputAction - = MakeCon - | MakeConSat + = MakeConSat | MakeInt | MakeChar | MakeVar @@ -202,14 +201,13 @@ forExpr tydefs l expr = EmptyHole{} -> annotate <> [ Input MakeVar - , Input MakeCon + , Input MakeConSat ] <> mwhen (Map.member tInt tydefs) [Input MakeInt] <> mwhen (Map.member tChar tydefs) [Input MakeChar] <> mwhen (l /= Beginner) [ Input MakeVarSat - , Input MakeConSat , Input MakeLet , Input MakeLetRec , NoInput EnterHole @@ -328,14 +326,6 @@ options :: -- or found but didn't correspond to the expected sort of entity (type/expr/pattern). Maybe Options options typeDefs defs cxt level def mNodeSel = \case - MakeCon -> - pure - . noFree - . map (globalOpt . valConName . snd) - . filter (not . (&& level == Beginner) . uncurry hasArgsCon) - . concatMap (\td -> (td,) <$> astTypeDefConstructors td) - . mapMaybe (typeDefAST . snd) - $ Map.toList typeDefs MakeConSat -> pure . noFree @@ -461,7 +451,6 @@ sortByPriority l = DuplicateDef -> P.duplicate DeleteDef -> P.delete Input a -> case a of - MakeCon -> P.useValueCon MakeConSat -> P.useSaturatedValueCon MakeInt -> P.makeInt MakeChar -> P.makeChar diff --git a/primer/src/Primer/Action/Priorities.hs b/primer/src/Primer/Action/Priorities.hs index 3398eca85..12d09c847 100644 --- a/primer/src/Primer/Action/Priorities.hs +++ b/primer/src/Primer/Action/Priorities.hs @@ -31,7 +31,6 @@ module Primer.Action.Priorities ( makeLambda, useVar, - useValueCon, makeInt, makeChar, makeCase, @@ -73,9 +72,6 @@ makeLambda _ = 5 useVar :: Level -> Int useVar _ = 10 -useValueCon :: Level -> Int -useValueCon _ = 11 - makeCase :: Level -> Int makeCase _ = 12 diff --git a/primer/test/Tests/Action.hs b/primer/test/Tests/Action.hs index 3baa34fb8..22f07c2cb 100644 --- a/primer/test/Tests/Action.hs +++ b/primer/test/Tests/Action.hs @@ -39,7 +39,6 @@ import Primer.Primitives (tChar, tInt) import Primer.Test.TestM (evalTestM) import Primer.Test.Util ( clearMeta, - constructCon, constructRefinedCon, constructSaturatedCon, constructTCon, @@ -242,7 +241,7 @@ unit_8 = , Move Parent , ConstructApp , Move Child2 - , constructCon cTrue + , constructSaturatedCon cTrue ] (app (ann (lam "x" (lvar "x")) (tfun (tcon tBool) (tcon tBool))) (con0 cTrue)) @@ -253,7 +252,7 @@ unit_9 = emptyHole [ ConstructLet (Just "x") , Move Child1 - , constructCon cTrue + , constructSaturatedCon cTrue , Move Parent , Move Child2 , ConstructVar $ LocalVarRef "x" @@ -401,7 +400,7 @@ unit_bad_constructor = (const True) NoSmartHoles emptyHole - [ConstructCon (["M"], "NotARealConstructor")] + [ConstructSaturatedCon (["M"], "NotARealConstructor")] unit_bad_type_constructor :: Assertion unit_bad_type_constructor = @@ -425,7 +424,7 @@ unit_insert_expr_in_type = (const True) NoSmartHoles (ann emptyHole tEmptyHole) - [EnterType, constructCon cTrue] + [EnterType, constructSaturatedCon cTrue] unit_bad_lambda :: Assertion unit_bad_lambda = @@ -440,7 +439,7 @@ unit_enter_emptyHole = actionTest NoSmartHoles emptyHole - [EnterHole, constructCon cTrue] + [EnterHole, constructSaturatedCon cTrue] (hole $ con0 cTrue) unit_enter_nonEmptyHole :: Assertion @@ -448,7 +447,7 @@ unit_enter_nonEmptyHole = actionTest NoSmartHoles (hole emptyHole) - [Move Child1, constructCon cTrue] + [Move Child1, constructSaturatedCon cTrue] (hole $ con0 cTrue) unit_bad_enter_hole :: Assertion @@ -476,7 +475,7 @@ unit_case_create = , Move Child1 , ConstructCase , Move (Branch cTrue) - , constructCon cZero + , constructSaturatedCon cZero ] ( ann ( lam "x" $ @@ -540,7 +539,7 @@ unit_case_move_branch_1 = , Move Child1 , Move Child1 , Move (Branch cZero) - , constructCon cZero + , constructSaturatedCon cZero , Move Parent , Move (Branch cSucc) , ConstructVar $ LocalVarRef "n" @@ -574,7 +573,7 @@ unit_case_move_branch_2 = [ Move Child1 , Move Child1 , Move (Branch cZero) - , constructCon cZero + , constructSaturatedCon cZero , Move Parent , Move (Branch cSucc) , ConstructVar $ LocalVarRef "n" @@ -759,7 +758,7 @@ unit_case_create_smart_on_term = , ConstructVar $ LocalVarRef "x" , ConstructCase , Move (Branch cTrue) - , constructCon cZero + , constructSaturatedCon cZero ] ( ann ( lam @@ -787,7 +786,7 @@ unit_case_create_smart_on_hole = , ConstructVar $ LocalVarRef "x" , Move Parent , Move (Branch cTrue) - , constructCon cZero + , constructSaturatedCon cZero ] ( ann ( lam @@ -814,7 +813,7 @@ unit_case_change_smart_scrutinee_type = [ Move Child1 , Move Child1 , Delete - , constructCon cZero + , constructSaturatedCon cZero ] ( ann ( case_ @@ -891,7 +890,7 @@ unit_constructLAM = actionTest NoSmartHoles (emptyHole `ann` tEmptyHole) - [Move Child1, ConstructLAM (Just "a"), constructCon cTrue] + [Move Child1, ConstructLAM (Just "a"), constructSaturatedCon cTrue] (lAM "a" (con0 cTrue) `ann` tEmptyHole) unit_construct_TForall :: Assertion diff --git a/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment index 914189190..1489cd997 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment @@ -253,7 +253,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -275,7 +276,6 @@ Output , free = FreeNone } ) - , NoInput MakeCase , Input MakeInt ( Options { opts = [] @@ -328,7 +328,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -350,7 +351,6 @@ Output , free = FreeNone } ) - , NoInput MakeCase , Input MakeInt ( Options { opts = [] @@ -878,7 +878,8 @@ Output , free = FreeNone } ) - , Input MakeCon + , NoInput MakeCase + , Input MakeConSat ( Options { opts = [ Option @@ -900,7 +901,6 @@ Output , free = FreeNone } ) - , NoInput MakeCase , Input MakeInt ( Options { opts = [] diff --git a/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment index 80910c8b5..4de57b843 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment @@ -390,68 +390,6 @@ Output , free = FreeNone } ) - , Input MakeCon - ( Options - { opts = - [ Option - { option = "True" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "False" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Left" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Right" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nil" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Cons" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nothing" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Just" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Zero" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Succ" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "MakePair" - , context = Just - ( "Builtins" :| [] ) - } - ] - , free = FreeNone - } - ) , NoInput MakeCase , Input MakeConSat ( Options @@ -645,68 +583,6 @@ Output , free = FreeNone } ) - , Input MakeCon - ( Options - { opts = - [ Option - { option = "True" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "False" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Left" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Right" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nil" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Cons" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nothing" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Just" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Zero" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Succ" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "MakePair" - , context = Just - ( "Builtins" :| [] ) - } - ] - , free = FreeNone - } - ) , NoInput MakeCase , Input MakeConSat ( Options @@ -1743,68 +1619,6 @@ Output , free = FreeNone } ) - , Input MakeCon - ( Options - { opts = - [ Option - { option = "True" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "False" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Left" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Right" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nil" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Cons" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nothing" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Just" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Zero" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Succ" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "MakePair" - , context = Just - ( "Builtins" :| [] ) - } - ] - , free = FreeNone - } - ) , NoInput MakeCase , Input MakeConSat ( Options diff --git a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment index d0e312f15..a97cc4bec 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment @@ -264,68 +264,6 @@ Output , free = FreeNone } ) - , Input MakeCon - ( Options - { opts = - [ Option - { option = "True" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "False" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Left" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Right" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nil" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Cons" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nothing" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Just" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Zero" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Succ" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "MakePair" - , context = Just - ( "Builtins" :| [] ) - } - ] - , free = FreeNone - } - ) , NoInput MakeCase , Input MakeConSat ( Options @@ -498,68 +436,6 @@ Output , free = FreeNone } ) - , Input MakeCon - ( Options - { opts = - [ Option - { option = "True" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "False" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Left" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Right" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nil" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Cons" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nothing" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Just" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Zero" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Succ" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "MakePair" - , context = Just - ( "Builtins" :| [] ) - } - ] - , free = FreeNone - } - ) , NoInput MakeCase , Input MakeConSat ( Options @@ -1222,68 +1098,6 @@ Output , free = FreeNone } ) - , Input MakeCon - ( Options - { opts = - [ Option - { option = "True" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "False" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Left" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Right" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nil" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Cons" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Nothing" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Just" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Zero" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "Succ" - , context = Just - ( "Builtins" :| [] ) - } - , Option - { option = "MakePair" - , context = Just - ( "Builtins" :| [] ) - } - ] - , free = FreeNone - } - ) , NoInput MakeCase , Input MakeConSat ( Options diff --git a/primer/testlib/Primer/Test/Util.hs b/primer/testlib/Primer/Test/Util.hs index 99ecb7ccf..003d90711 100644 --- a/primer/testlib/Primer/Test/Util.hs +++ b/primer/testlib/Primer/Test/Util.hs @@ -5,7 +5,6 @@ module Primer.Test.Util ( assertException, primDefs, constructTCon, - constructCon, constructRefinedCon, constructSaturatedCon, tcn, @@ -41,7 +40,7 @@ import Primer.API ( runPrimerM, ) import Primer.Action ( - Action (ConstructCon, ConstructRefinedCon, ConstructSaturatedCon, ConstructTCon), + Action (ConstructRefinedCon, ConstructSaturatedCon, ConstructTCon), ) import Primer.Core ( Expr', @@ -88,9 +87,6 @@ primDefs = Map.mapKeys primitive $ moduleDefs primitiveModule constructTCon :: TyConName -> Action constructTCon = ConstructTCon . toQualText -constructCon :: ValConName -> Action -constructCon = ConstructCon . toQualText - constructSaturatedCon :: ValConName -> Action constructSaturatedCon = ConstructSaturatedCon . toQualText From 3d1ec200abafe6af150453dfd8fc234ed24c6863 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 21 Mar 2023 12:33:48 +0000 Subject: [PATCH 05/13] feat: unit_inc uses fully-saturated constructors This is a step towards all constructors being saturated, at which point we can update the typechecker to enforce that invariant. --- primer/test/Tests/Typecheck.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs index ae9edbec6..f677a7568 100644 --- a/primer/test/Tests/Typecheck.hs +++ b/primer/test/Tests/Typecheck.hs @@ -221,7 +221,7 @@ unit_inc :: Assertion unit_inc = expectTyped $ ann - (lam "n" (app (con0 cSucc) (lvar "n"))) + (lam "n" (con cSucc [] [lvar "n"])) (tfun (tcon tNat) (tcon tNat)) unit_compose_nat :: Assertion From 72210ef3b39789a7bcdf3701dd97b13e77ea0ac8 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 21 Mar 2023 15:48:44 +0000 Subject: [PATCH 06/13] feat: Gen.Core.Typed only emits fully-saturated constructors This is a step towards all constructors being saturated, at which point we can update the typechecker to enforce that invariant. --- primer/gen/Primer/Gen/Core/Typed.hs | 26 +++++--------------------- 1 file changed, 5 insertions(+), 21 deletions(-) diff --git a/primer/gen/Primer/Gen/Core/Typed.hs b/primer/gen/Primer/Gen/Core/Typed.hs index 7ca5bebe7..d53a1fcc9 100644 --- a/primer/gen/Primer/Gen/Core/Typed.hs +++ b/primer/gen/Primer/Gen/Core/Typed.hs @@ -79,7 +79,6 @@ import Primer.TypeDef ( ValCon (..), typeDefKind, typeDefParameters, - valConType, ) import Primer.Typecheck ( Cxt (), @@ -234,17 +233,12 @@ genSyns ty = do let locals' = map (first (Var () . LocalVarRef)) $ M.toList localTms globals <- asks globalCxt let globals' = map (first (Var () . GlobalVarRef)) $ M.toList globals - -- TODO (saturated constructors) when saturation is enforced, constructors should not appear on the left of an app node - cons <- asks allCons - let cons' = map (first (\c -> Con () c [] [])) $ M.toList cons - let hsPure = locals' ++ globals' ++ cons' - primCons <- fmap (bimap (PrimCon ()) (TCon ())) <<$>> genPrimCon - let hs = map pure hsPure ++ primCons + let hs = locals' ++ globals' pure $ if null hs then Nothing else Just $ do - (he, hT) <- Gen.choice hs + (he, hT) <- Gen.element hs cxt <- ask runExceptT (refine cxt ty hT) >>= \case -- This error case indicates a bug. Crash and fail loudly! @@ -275,7 +269,7 @@ genSyns ty = do genCon = instantiateValCons ty >>= \case Left TDIHoleType -> - asks allCons' <&> \case + asks allCons <&> \case -- We have no constraints, generate any ctor m | null m -> Nothing cons -> Just $ do @@ -390,24 +384,14 @@ genSyn :: GenT WT (ExprG, TypeG) -- of any type genSyn = genSyns (TEmptyHole ()) -allCons :: Cxt -> M.Map ValConName (Type' ()) -allCons cxt = M.fromList $ concatMap (uncurry consForTyDef) $ M.assocs $ typeDefs cxt - where - consForTyDef tc = \case - TypeDefAST td -> map (\vc -> (valConName vc, valConType tc td vc)) (astTypeDefConstructors td) - TypeDefPrim _ -> [] - --- TODO (saturated constructors) when saturation is enforced, allCons should be --- no longer needed, and we can rename allCons' - -- | Returns each ADT constructor's name along with its "telescope" of arguments: -- - the parameters of the datatype (which are type arguments to the constructor) -- - the types of its fields (and the names of the parameters scope over this) -- - the ADT it belongs to (if @c@ maps to @([(p1,k1),(p2,k2)],_,T)@ in the -- returned map, then @c [A,B] _ ∈ T A B@ for any @A@ of kind @k1@ and @B@ -- of kind @k2@) -allCons' :: Cxt -> M.Map ValConName ([(TyVarName, Kind)], [Type' ()], TyConName) -allCons' cxt = M.fromList $ concatMap (uncurry consForTyDef) $ M.assocs $ typeDefs cxt +allCons :: Cxt -> M.Map ValConName ([(TyVarName, Kind)], [Type' ()], TyConName) +allCons cxt = M.fromList $ concatMap (uncurry consForTyDef) $ M.assocs $ typeDefs cxt where consForTyDef tc = \case TypeDefAST td -> From 586e529d921656f7703d896fd1eaa9bbc78b28bc Mon Sep 17 00:00:00 2001 From: Ben Price Date: Wed, 12 Apr 2023 19:16:01 +0100 Subject: [PATCH 07/13] feat: unit_RenameCon_clash uses fully-saturated constructors This is a step towards all constructors being saturated, at which point we can update the typechecker to enforce that invariant. --- primer/test/Tests/Action/Prog.hs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 55a2c235b..79670bcf3 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -957,7 +957,16 @@ unit_RenameCon_clash = x <- hole ( hole - (con0 cA) + ( con + cA + [ tEmptyHole + , tEmptyHole + ] + [ emptyHole + , emptyHole + , emptyHole + ] + ) ) astDef "def" x <$> tEmptyHole ] From 66487f726ec6cd0f4d164261790e05cf68470e40 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Mon, 27 Mar 2023 18:27:46 +0100 Subject: [PATCH 08/13] fix!: ConstructRefinedCon at arrow type gave unsaturated constructor This is the last step towards all constructors being saturated. We can now update the typechecker to enforce that invariant. BREAKING CHANGE: this changes the interpretation of an action that may be stored in program's undo logs. This may break the undo action of programs loaded from a database which was created by an earlier version of primer. --- primer/src/Primer/Action.hs | 11 ++++++++--- primer/test/Tests/Action.hs | 14 +++++++++----- 2 files changed, 17 insertions(+), 8 deletions(-) diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index d39cd4266..5ac8af53b 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -659,14 +659,19 @@ constructRefinedCon c ze = do case target ze of EmptyHole{} -> breakLR <<$>> getRefinedApplications cxt cTy tgtTy >>= \case + Just (Just (tys, tms)) + | length tys == numTyArgs && length tms == numTmArgs -> + flip replace ze <$> con n (pure <$> tys) (pure <$> tms) + -- If the refinement is not saturated, just give a saturated constructor + -- This could happen when refining @Cons@ to fit in a hole of type @List Nat -> List Nat@ + -- as we get the "type" of @Cons@ being @∀a. a -> List a -> List a@ + -- and thus a refinement of @Nat, _@. + | otherwise -> flip replace ze <$> hole (con n (replicate numTyArgs tEmptyHole) (replicate numTmArgs emptyHole)) -- See Note [No valid refinement] Nothing -> flip replace ze <$> hole (con n (replicate numTyArgs tEmptyHole) (replicate numTmArgs emptyHole)) -- TODO (saturated constructors): when constructors are checkable the above will not be valid -- since the inside of a hole must be synthesisable (see Note [Holes and bidirectionality]) - -- TODO (saturated constructors): when saturation is enforced, the Just Just case may not be valid - -- if the target type is not an applied-ADT Just Nothing -> throwError $ InternalFailure "Types of constructors always have type abstractions before term abstractions" - Just (Just (tys, tms)) -> flip replace ze <$> con n (pure <$> tys) (pure <$> tms) e -> throwError $ NeedEmptyHole (ConstructRefinedCon c) e getTypeCache :: MonadError ActionError m => Expr -> m TypeCache diff --git a/primer/test/Tests/Action.hs b/primer/test/Tests/Action.hs index 22f07c2cb..2f45b1196 100644 --- a/primer/test/Tests/Action.hs +++ b/primer/test/Tests/Action.hs @@ -1100,24 +1100,28 @@ unit_refine_mismatch_var = $ hole (lvar "cons" `aPP` tEmptyHole `app` emptyHole `app` emptyHole) `ann` tcon tBool ) --- Note @cons @? ∈ ? -> List ? -> List ? ~ ? -> ?@, --- thus inserting a refined @cons@ in a hole of type @? -> ?@ may not refine as --- much as you may expect! +-- Constructors are saturated, so if the hole has an arrow type, when we insert +-- a constructor it cannot match the arrow, so it is inserted into a hole unit_refine_arr_1 :: Assertion unit_refine_arr_1 = actionTest NoSmartHoles (emptyHole `ann` (tEmptyHole `tfun` tEmptyHole)) [Move Child1, constructRefinedCon cCons] - (con cCons [tEmptyHole] [] `ann` (tEmptyHole `tfun` tEmptyHole)) + (hole (con cCons [tEmptyHole] [emptyHole, emptyHole]) `ann` (tEmptyHole `tfun` tEmptyHole)) +-- TODO (saturated constructors) update this comment for ctors-dont-store-indices ('Cons Nat') and ctors-are-chk +-- +-- Constructors are fully saturated, so even if the hole has type +-- @List Nat -> List Nat@, when we insert a @Cons@ constructor, we end up with +-- @{? Cons @? ? ? ?}@ unit_refine_arr_2 :: Assertion unit_refine_arr_2 = actionTest NoSmartHoles (emptyHole `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat))) [Move Child1, constructRefinedCon cCons] - (con cCons [tcon tNat] [emptyHole] `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat))) + (hole (con cCons [tEmptyHole] [emptyHole, emptyHole]) `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat))) unit_primitive_1 :: Assertion unit_primitive_1 = From eff6ee12538f6b153932741267a095eb9260d880 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 21 Mar 2023 00:24:24 +0000 Subject: [PATCH 09/13] feat!: typechecker enforces saturation Some tests also need updating: - We also remove a couple of tests that need unsaturated constructors (i.e. partially applied constructors). - A couple of fragile name also needed updating. - A tests checking acceptance of under-saturated constructors now checks they are rejected (at hole types). Added a test an unsaturated constructor is rejected (at a concrete type). BREAKING CHANGE: this will reject some programs that were previously accepted. This will break loading databases created by older versions of primer. --- primer/src/Primer/Core.hs | 39 ++++++++++------- primer/src/Primer/Typecheck.hs | 50 ++++++++++++++------- primer/src/Primer/Typecheck/TypeError.hs | 5 +++ primer/test/Tests/Action/Prog.hs | 56 +----------------------- primer/test/Tests/Typecheck.hs | 15 +++++-- 5 files changed, 75 insertions(+), 90 deletions(-) diff --git a/primer/src/Primer/Core.hs b/primer/src/Primer/Core.hs index 9e05ec887..bca61e2b7 100644 --- a/primer/src/Primer/Core.hs +++ b/primer/src/Primer/Core.hs @@ -224,6 +224,7 @@ data Expr' a b -- become synthesisable. -- Note [Synthesisable constructors] +-- -- Whilst our calculus is heavily inspired by bidirectional type systems -- (especially McBride's principled rendition), we do not treat constructors -- in this fashion. However, we are in the middle of changing the treatment @@ -236,30 +237,36 @@ data Expr' a b -- changed, due to asymmetries between construction and matching.) -- -- We represent a constructor-applied-to-a-spine as a thing (and one can infer --- its type), but do not insist that it is fully saturated. --- Thus one has `Cons` is a term, and we can derive the synthesis --- judgement `Cons ∈ ∀a. a -> List a -> List a`, but also that `Cons @a`, --- `Cons @a x` and `Cons @a x y` are terms (for type `a` and terms `x, y`), with --- the obvious synthesised types. This is a temporary situation, and we aim to --- enforce full saturation (and no type applications) in due course. +-- its type), where we insist that it is fully saturated. +-- Thus whilst `Cons` is a term, it is ill-typed. The only well-formed +-- `Cons` usages are `Cons @A x xs`, which synthesises `List A` +-- when `A ∋ x` and `List A ∋ xs`. +-- +-- Whilst this may be a bit inconsistent with the treatment of +-- functions, it has the advantage of symmetry with construction and +-- matching. (I.e. every time one sees a particular constructor, it +-- has the same form: a head of that constructor, and the same number +-- of (term) fields.) +-- TODO (saturated constructors): technically, a construction will +-- have type arguments/indices and a match will not, but this is +-- temporary, as we will soon remove indices (which will require +-- constructors to be only checkable, rather than synthesisable). -- --- For comparison, the bidirectional view would be that constructors must --- always be fully applied, and one can only subject them to a typechecking --- judgement where the type is an input. --- Thus `List Int ∋ Cons 2 Nil`, but `Cons` and `Cons 2` are ill-typed. --- Under this view, one needs to be aware of the difference between, say, +-- Thus one needs to be aware of the difference between, say, -- a globally-defined function, and a constructor "of the same type". -- For example, one can partially apply an addition function and map it -- across a list: `map (1 +) [2,3]` is well-typed, but one cannot map -- the `Succ` constructor in the same way. --- (Notice, however, that since one will always know what type one is --- considering, the constructor does not need any type applications --- corresponding to the parameters of its datatype.) -- Clearly one could eta-expand, (and if necessary add an annotation) to -- use as constructor non-saturatedly: e.g. write `map (λn . Succ n) [2,3]`. -- --- In effect, we just bake (various stages of) this translation into the core. --- To do this, we require constructor names to be unique across different types. +-- For comparison, the bidirectional view would be that constructors +-- must always be fully applied (which is the same as our treatment), +-- and one can only subject them to a typechecking judgement where the +-- type is an input (which is different to our treatment), and they do +-- not need to store their indices/type applications (different to our +-- treatment). +-- Thus `List Int ∋ Cons 2 Nil`, but `Cons 2 Nil` does not synthesise a type. -- Note [Case] -- We use a list for compatibility and ease of JSON diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index 2edea202d..fb651e7d4 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -117,8 +117,8 @@ import Primer.Core ( _exprTypeMeta, _typeMeta, ) -import Primer.Core.DSL (S, apps', branch, create', emptyHole, meta, meta') -import Primer.Core.Transform (decomposeAppCon, decomposeTAppCon, mkTAppCon) +import Primer.Core.DSL (S, branch, create', emptyHole, meta, meta') +import Primer.Core.Transform (decomposeTAppCon, mkTAppCon) import Primer.Core.Utils ( alphaEqTy, forgetTypeMetadata, @@ -143,14 +143,13 @@ import Primer.Module ( ) import Primer.Name (Name, NameCounter) import Primer.Primitives (primConName) -import Primer.Subst (substTy) +import Primer.Subst (substTy, substTySimul) import Primer.TypeDef ( ASTTypeDef (astTypeDefConstructors, astTypeDefParameters), TypeDef (..), TypeDefMap, ValCon (valConArgs, valConName), typeDefAST, - valConType, ) import Primer.Typecheck.Cxt (Cxt (Cxt, globalCxt, localCxt, smartHoles, typeDefs)) import Primer.Typecheck.Kindcheck ( @@ -499,20 +498,27 @@ synth = \case EmptyHole i -> pure $ annSynth0 (TEmptyHole ()) i EmptyHole -- We assume that constructor names are unique -- See Note [Synthesisable constructors] in Core.hs - Con i c [] [] -> do - asks (flip lookupConstructor c . typeDefs) >>= \case - Just (vc, tc, td) -> let t = valConType tc td vc in pure $ annSynth3 t i Con c [] [] - Nothing -> throwError' $ UnknownConstructor c Con i c tys tms -> do - -- TODO (saturated constructors) for now we synth exactly the same as the application tree, - -- but take care not to actually change the shape of the program. - -- This will change when full-saturation is enforced - elab <- apps' (pure $ Con i c [] []) $ (Right . pure <$> tys) ++ (Left . pure <$> tms) - (ty, e) <- synth elab - (tys', tms') <- case decomposeAppCon e of - Just (_, _, tys', tms') -> pure (tys', tms') - Nothing -> throwError' $ InternalError "saturated constructor: elaborated term is not ctor-headed" - pure $ annSynth3 ty i Con c tys' tms' + -- When C is a constructor of some ADT T with parameters ps with kinds ks, where C has args of types Rs[ps] + (adtName, params, argTys0) <- + asks (flip lookupConstructor c . typeDefs) >>= \case + Just (vc, tc, td) -> pure (tc, astTypeDefParameters td, valConArgs vc) + Nothing -> throwError' $ UnknownConstructor c + -- And |ps| = |As| and k ∋ A for each matching element + tys'Sub <- ensureJust (UnsaturatedConstructor c) $ zipWithExactM (\(p, k) ty -> (p,) <$> checkKind' k ty) params tys + -- Note that being unsaturated is a fatal error and SmartHoles will not try to recover + -- (this is a design decision -- we put the burden onto code that builds ASTs, + -- e.g. the action code is responsible for only creating saturated constructors) + let tys' = snd <$> tys'Sub + let tys'SubNoMeta = second forgetTypeMetadata <$> tys'Sub + let tys'NoMeta = snd <$> tys'SubNoMeta + -- And |rs| = |Rs| and R[As] ∋ r for each matching element + argTys <- traverse (substTySimul (M.fromList tys'SubNoMeta)) argTys0 + -- Fatal error, see comments on UnsaturatedConstructor error above + tms' <- ensureJust (UnsaturatedConstructor c) $ zipWithExactM check argTys tms + -- Then C @As rs ∈ T As + let synthedType = foldl' (TApp ()) (TCon () adtName) tys'NoMeta + pure $ annSynth3 synthedType i Con c tys' tms' -- When synthesising a hole, we first check that the expression inside it -- synthesises a type successfully (see Note [Holes and bidirectionality]). -- TODO: we would like to remove this hole (leaving e) if possible, but I @@ -567,6 +573,16 @@ synth = \case annSynth3 t i c = annSynth2 t i . flip c annSynth4 t i c = annSynth3 t i . flip c +zipWithExactM :: Applicative f => (a -> b -> f c) -> [a] -> [b] -> Maybe (f [c]) +zipWithExactM _ [] [] = Just $ pure [] +zipWithExactM _ [] _ = Nothing +zipWithExactM _ _ [] = Nothing +zipWithExactM f (x : xs) (y : ys) = ((:) <$> f x y <*>) <$> zipWithExactM f xs ys + +ensureJust :: MonadNestedError e e' m => e -> Maybe (m a) -> m a +ensureJust e Nothing = throwError' e +ensureJust _ (Just x) = x + -- There is a hard-wired map 'primConName' which associates each PrimCon to -- its PrimTypeDef (by name -- PrimTypeDefs have hardwired names). -- However, these PrimTypeDefs may or may not be in the Cxt. diff --git a/primer/src/Primer/Typecheck/TypeError.hs b/primer/src/Primer/Typecheck/TypeError.hs index bba989e62..3b5ae2624 100644 --- a/primer/src/Primer/Typecheck/TypeError.hs +++ b/primer/src/Primer/Typecheck/TypeError.hs @@ -14,6 +14,11 @@ data TypeError | UnknownVariable TmVarRef | TmVarWrongSort Name -- type var instead of term var | UnknownConstructor ValConName + | -- TODO (saturated constructors) eventually constructors will not store type arguments + + -- | Constructors (term-level) must be saturated. + -- This error catches both under- and over-saturation (of both type and term arguments). + UnsaturatedConstructor ValConName | -- | Cannot use a PrimCon when either no type of the appropriate name is -- in scope, or it is a user-defined type PrimitiveTypeNotInScope TyConName diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 79670bcf3..06be5f5ec 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -1155,19 +1155,6 @@ unit_SetConFieldType_nehole_2 = (tcon $ tcn "Bool") (hole $ con0 $ vcn "True") -unit_SetConFieldType_partial_app :: Assertion -unit_SetConFieldType_partial_app = - progActionTest - ( defaultProgEditableTypeDefs $ do - x <- lam "x" $ con cA [tEmptyHole, tEmptyHole] [lvar "x"] - sequence - [ astDef "def" x <$> tcon (tcn "Bool") `tfun` (tcon (tcn "Bool") `tfun` (tcon (tcn "Bool") `tfun` ((tcon tT `tapp` tEmptyHole) `tapp` tEmptyHole))) - ] - ) - [SetConFieldType tT cA 1 $ TCon () (tcn "Int")] - $ expectError - (@?= ConNotSaturated cA) - unit_SetConFieldType_case :: Assertion unit_SetConFieldType_case = progActionTest @@ -1284,50 +1271,11 @@ unit_AddConField = , con0 (vcn "True") ] ) - [ branch cA [("p", Nothing), ("a45", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole + [ branch cA [("p", Nothing), ("a40", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole , branch cB [("r", Nothing), ("x", Nothing)] emptyHole ] ) -unit_AddConField_partial_app :: Assertion -unit_AddConField_partial_app = - progActionTest - ( defaultProgEditableTypeDefs $ do - x <- - con cA [tEmptyHole, tEmptyHole] [con0 (vcn "True")] - sequence - [ astDef "def" x <$> tEmptyHole - ] - ) - [AddConField tT cA 2 $ TCon () (tcn "Int")] - $ expectError - (@?= ConNotSaturated cA) - -unit_AddConField_partial_app_end :: Assertion -unit_AddConField_partial_app_end = - progActionTest - ( defaultProgEditableTypeDefs $ do - x <- - con cA [tEmptyHole, tEmptyHole] [con0 (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 [TApp () (TApp () (TCon () tT) (TVar () "b")) (TVar () "a"), TVar () "b"] - ] - def <- findDef (gvn "def") prog' - forgetMetadata (astDefExpr def) - @?= forgetMetadata - ( create' $ - con cA [tEmptyHole, tEmptyHole] [con0 (vcn "True"), emptyHole] - ) - unit_AddConField_case_ann :: Assertion unit_AddConField_case_ann = progActionTest @@ -1469,7 +1417,7 @@ unit_cross_module_actions = , Move $ ConChild 0 , constructSaturatedCon cSucc , Move $ ConChild 0 - , ConstructVar (LocalVarRef "a42") + , ConstructVar (LocalVarRef "a37") ] ] handleAndTC [RenameDef (qualifyM "foo") "bar"] diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs index f677a7568..169d81919 100644 --- a/primer/test/Tests/Typecheck.hs +++ b/primer/test/Tests/Typecheck.hs @@ -154,15 +154,17 @@ unit_const = unit_true :: Assertion unit_true = expectTyped $ con0 cTrue --- An empty hole accepts under-saturated constructors +-- An empty hole rejects under-saturated constructors unit_unsat_con_hole_1 :: Assertion -unit_unsat_con_hole_1 = expectTyped $ con cSucc [] [] `ann` tEmptyHole +unit_unsat_con_hole_1 = + (con cSucc [] [] `ann` tEmptyHole) + `expectFailsWith` \_ -> UnsaturatedConstructor cSucc -- An empty hole rejects over-saturated constructors unit_unsat_con_hole_2 :: Assertion unit_unsat_con_hole_2 = (con cSucc [] [emptyHole, emptyHole] `ann` tEmptyHole) - `expectFailsWith` const (TypeDoesNotMatchArrow $ TCon () tNat) + `expectFailsWith` \_ -> UnsaturatedConstructor cSucc -- A hole-headed TApp accepts saturated constructors unit_con_hole_app_type_1 :: Assertion @@ -224,6 +226,13 @@ unit_inc = (lam "n" (con cSucc [] [lvar "n"])) (tfun (tcon tNat) (tcon tNat)) +unit_inc_unsat :: Assertion +unit_inc_unsat = + ann + (lam "n" (app (con0 cSucc) (lvar "n"))) + (tfun (tcon tNat) (tcon tNat)) + `expectFailsWith` const (UnsaturatedConstructor cSucc) + unit_compose_nat :: Assertion unit_compose_nat = expectTyped $ From 00151a176fb16d0eabce9c436e3c11dfb3f76782 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Sat, 22 Apr 2023 21:10:31 +0100 Subject: [PATCH 10/13] refactor: decomposeAppCon can be a trivial match; inline it --- primer/src/Primer/Core/Transform.hs | 13 ------------- primer/src/Primer/Eval/Redex.hs | 7 ++++--- 2 files changed, 4 insertions(+), 16 deletions(-) diff --git a/primer/src/Primer/Core/Transform.hs b/primer/src/Primer/Core/Transform.hs index 7e052a9f8..d4a64b4a5 100644 --- a/primer/src/Primer/Core/Transform.hs +++ b/primer/src/Primer/Core/Transform.hs @@ -6,7 +6,6 @@ module Primer.Core.Transform ( unfoldApp, foldApp, unfoldAPP, - decomposeAppCon, unfoldTApp, decomposeTAppCon, foldTApp, @@ -31,7 +30,6 @@ import Primer.Core ( TmVarRef (..), TyVarName, Type' (..), - ValConName, bindName, typesInExpr, ) @@ -234,17 +232,6 @@ unfoldAPP = second reverse . go go (APP _ f x) = let (g, args) = go f in (g, x : args) go e = (e, []) --- | Decompose @C @A @B x y z@ to @(C,[A,B],[x,y,z])@ -decomposeAppCon :: Expr' a b -> Maybe (ValConName, a, [Type' b], [Expr' a b]) -decomposeAppCon = - unfoldApp <&> first unfoldAPP <&> \case - -- TODO (saturated constructors): This is suspicious (we reorder types and terms), but - -- (a) for well-typed terms, either tms0 or tys will be empty (since constructors only have top-level foralls) - -- (b) the situation that constructors can be on the left of an app or aPP node is temporary - -- and shortly decomposeAppCon will become a trivial match on the 'Con' constructor. - ((Con m c tys0 tms0, tys), tms) -> Just (c, m, tys0 ++ tys, tms0 ++ tms) - _ -> Nothing - -- | Unfold a nested type-level application into the application head and a list of arguments. unfoldTApp :: Type' a -> (Type' a, [Type' a]) unfoldTApp = second reverse . go diff --git a/primer/src/Primer/Eval/Redex.hs b/primer/src/Primer/Eval/Redex.hs index 538fdfd19..8def0bb4f 100644 --- a/primer/src/Primer/Eval/Redex.hs +++ b/primer/src/Primer/Eval/Redex.hs @@ -60,6 +60,7 @@ import Primer.Core ( Ann, App, Case, + Con, LAM, Lam, Let, @@ -89,7 +90,7 @@ import Primer.Core ( getID, ) import Primer.Core.DSL (ann, letType, let_, letrec, lvar, tlet, tvar) -import Primer.Core.Transform (decomposeAppCon, decomposeTAppCon) +import Primer.Core.Transform (decomposeTAppCon) import Primer.Core.Utils ( alphaEqTy, concreteTy, @@ -549,8 +550,8 @@ viewCaseRedex tydefs = \case <|> pure (formCaseRedex c abstractArgTys tyargs args patterns br (orig, expr, cID)) _ -> mzero where - extractCon expr = case decomposeAppCon expr of - Just (c, m, params, as) -> pure (c, getID m, params, as) + extractCon = \case + Con m c params as -> pure (c, getID m, params, as) _ -> mzero extractBranch c brs = case find (\(CaseBranch n _ _) -> n == c) brs of From 8c5b164c2fefab58434db321c72498f101d67096 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Wed, 19 Apr 2023 20:57:22 +0100 Subject: [PATCH 11/13] refactor: remove special case in primitives now constructors are saturated --- primer/src/Primer/Primitives.hs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/primer/src/Primer/Primitives.hs b/primer/src/Primer/Primitives.hs index 27312b7ba..7b4fc1337 100644 --- a/primer/src/Primer/Primitives.hs +++ b/primer/src/Primer/Primitives.hs @@ -35,7 +35,7 @@ import Primer.Builtins ( import Primer.Builtins.DSL (bool_, maybe_, nat) import Primer.Core ( Expr, - Expr' (App, Con, PrimCon), + Expr' (Con, PrimCon), GVarName, GlobalName, ID, @@ -274,7 +274,5 @@ primFunDef def args = case def of exprToNat = \case Con _ c [] [] | c == cZero -> Just 0 Con _ c [] [x] | c == cSucc -> succ <$> exprToNat x - -- TODO (saturated constructors) this line will be unneeded when saturation is enforced - App _ (Con _ c [] []) x | c == cSucc -> succ <$> exprToNat x _ -> Nothing err = Left $ PrimFunError def args From 2b014de31f5758992a45519765cb87fa33467c18 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Wed, 19 Apr 2023 21:36:17 +0100 Subject: [PATCH 12/13] refactor: simplify typedef actions now constructors are saturated Also remove dead code `foldApp` and `unfoldAPP`. --- primer/src/Primer/App.hs | 41 +++++------------------------ primer/src/Primer/Core/Transform.hs | 19 ------------- 2 files changed, 7 insertions(+), 53 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index dcb3cc647..85ffbe5a7 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -144,7 +144,7 @@ import Primer.Core ( ) import Primer.Core.DSL (S, ann, create, emptyHole, hole, tEmptyHole, tvar) import Primer.Core.DSL qualified as DSL -import Primer.Core.Transform (foldApp, renameVar, unfoldAPP, unfoldApp, unfoldTApp) +import Primer.Core.Transform (renameVar, unfoldTApp) import Primer.Core.Utils (freeVars, generateTypeIDs, regenerateExprIDs, regenerateTypeIDs, _freeTmVars, _freeTyVars, _freeVarsTy) import Primer.Def ( ASTDef (..), @@ -798,25 +798,12 @@ applyProgAction prog mdefName = \case (_, Nothing, Just c) -> hole $ pure x `ann` generateTypeIDs c -- This last case means that the input program had no (useful) metadata (_, Nothing, Nothing) -> hole $ pure x `ann` tEmptyHole - in case (e, unfoldApp e) of - (Con m con' tys tms, _) | con' == con -> do + in case e of + Con m con' tys tms | con' == con -> do adjustAtA index enhole tms >>= \case Just args' -> Con m con' tys <$> traverse (descendM updateCons) args' Nothing -> throwError $ ConNotSaturated con - -- TODO (saturated constructors) this deconstruction of application nodes can be removed once full-saturation is enforced - -- (it currently assumes that constructors will either be fully saturated or have no syntactic arguments) - (_, (h, args)) -> case unfoldAPP h of - (Con _ con' [] [], _tyArgs) | con' == con -> do - adjustAtA index enhole args >>= \case - 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 + _ -> descendM updateCons e updateDecons = transformCaseBranches prog type_ $ traverse $ \cb@(CaseBranch vc binds e) -> if vc == con @@ -858,27 +845,13 @@ applyProgAction prog mdefName = \case -- 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 (e, unfoldApp e) of - (Con m con' tys tms, _) | con' == con -> do + updateCons e = case e of + Con m con' tys tms | con' == con -> do m' <- DSL.meta case insertAt index (EmptyHole m') tms of Just args' -> Con m con' tys <$> traverse (descendM updateCons) args' Nothing -> throwError $ ConNotSaturated con - -- TODO (saturated constructors) this deconstruction of application nodes can be removed once full-saturation is enforced - -- (it currently assumes that constructors will either be fully saturated or have no syntactic arguments) - (_, (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 + _ -> descendM updateCons e updateDecons = transformCaseBranches prog type_ $ traverse $ \cb@(CaseBranch vc binds e) -> if vc == con diff --git a/primer/src/Primer/Core/Transform.hs b/primer/src/Primer/Core/Transform.hs index d4a64b4a5..ebb5542c4 100644 --- a/primer/src/Primer/Core/Transform.hs +++ b/primer/src/Primer/Core/Transform.hs @@ -4,8 +4,6 @@ module Primer.Core.Transform ( renameTyVar, renameTyVarExpr, unfoldApp, - foldApp, - unfoldAPP, unfoldTApp, decomposeTAppCon, foldTApp, @@ -15,16 +13,13 @@ module Primer.Core.Transform ( import Foreword -import Control.Monad.Fresh (MonadFresh) import Data.Data (Data) import Data.Generics.Uniplate.Data (descendM) import Data.List.NonEmpty qualified as NE import Optics (Field2 (_2), getting, noneOf, notElemOf, to, traverseOf, (%)) import Primer.Core ( CaseBranch' (..), - Expr, Expr' (..), - ID, LVarName, LocalName (unLocalName), TmVarRef (..), @@ -33,7 +28,6 @@ import Primer.Core ( bindName, typesInExpr, ) -import Primer.Core.DSL (meta) import Primer.Core.Meta (TyConName) import Primer.Core.Utils (_freeVars, _freeVarsTy) @@ -219,19 +213,6 @@ unfoldApp = second reverse . go go (App _ f x) = let (g, args) = go f in (g, x : args) go e = (e, []) --- | Fold an application head and a list of arguments into a single expression. -foldApp :: (Foldable t, MonadFresh ID m) => Expr -> t Expr -> m Expr -foldApp = foldlM $ \a b -> do - m <- meta - pure $ App m a b - --- | Unfold a nested term-level type application into the application head and a list of arguments. -unfoldAPP :: Expr' a b -> (Expr' a b, [Type' b]) -unfoldAPP = second reverse . go - where - go (APP _ f x) = let (g, args) = go f in (g, x : args) - go e = (e, []) - -- | Unfold a nested type-level application into the application head and a list of arguments. unfoldTApp :: Type' a -> (Type' a, [Type' a]) unfoldTApp = second reverse . go From 251c13d8e54aa92258706c4513a1b58928c00444 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Wed, 19 Apr 2023 21:42:40 +0100 Subject: [PATCH 13/13] refactor: further simplify typedef actions now constructors are saturated In the handlers for `SetConFieldType` and `AddConField` we can now use `transformM` instead of manually doing the recursion. This change was enabled by the previous commit, which removed the handling of non-saturated constructors. Prior to that we had to recurse top-down, since for an unsaturated term such as `C x xs` (which would be represented as `App (App (Con "C" [] []) (Var "x")) (Var "xs")) we need to act on the outer `App` node and then recurse into the arguments (here, `x` and `xs`). Note that we must not act on the "inner" `App` node, since we would then believe that the constructor is only applied to one argument. Thus `transformM` is inappropriate as it is a bottom-up traversal, and we must hand-roll the traversal with `descendM`. Since we now know that all constructors are saturated, we know that the above situation is imposible, and the representation must in fact be `Con "C" [] [Var "x", Var "xs"]`. This sidesteps all the issues, enabling us to use the standard bottom-up traversal `transformM`. --- primer/src/Primer/App.hs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 85ffbe5a7..3454e99da 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -64,7 +64,7 @@ import Control.Monad.Fresh (MonadFresh (..)) import Control.Monad.Log (MonadLog, WithSeverity) import Control.Monad.NestedError (MonadNestedError, throwError') import Data.Data (Data) -import Data.Generics.Uniplate.Operations (descendM, transform, transformM) +import Data.Generics.Uniplate.Operations (transform, transformM) import Data.Generics.Uniplate.Zipper ( fromZipper, ) @@ -772,7 +772,7 @@ applyProgAction prog mdefName = \case ) type_ updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateDecons <=< updateCons) - updateCons e = + updateCons = let typecache = _typecache % _Just -- Previously the @index@th argument @t@ to this -- constructor would have been typechecked against the old @@ -798,12 +798,12 @@ applyProgAction prog mdefName = \case (_, Nothing, Just c) -> hole $ pure x `ann` generateTypeIDs c -- This last case means that the input program had no (useful) metadata (_, Nothing, Nothing) -> hole $ pure x `ann` tEmptyHole - in case e of + in transformM $ \case Con m con' tys tms | con' == con -> do adjustAtA index enhole tms >>= \case - Just args' -> Con m con' tys <$> traverse (descendM updateCons) args' + Just args' -> pure $ Con m con' tys args' Nothing -> throwError $ ConNotSaturated con - _ -> descendM updateCons e + e -> pure e updateDecons = transformCaseBranches prog type_ $ traverse $ \cb@(CaseBranch vc binds e) -> if vc == con @@ -845,13 +845,13 @@ applyProgAction prog mdefName = \case -- 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 e of + updateCons = transformM $ \case Con m con' tys tms | con' == con -> do m' <- DSL.meta case insertAt index (EmptyHole m') tms of - Just args' -> Con m con' tys <$> traverse (descendM updateCons) args' + Just args' -> pure $ Con m con' tys args' Nothing -> throwError $ ConNotSaturated con - _ -> descendM updateCons e + e -> pure e updateDecons = transformCaseBranches prog type_ $ traverse $ \cb@(CaseBranch vc binds e) -> if vc == con