Skip to content

Commit

Permalink
feat: Implement actions for editing type parameter kinds
Browse files Browse the repository at this point in the history
The implementation of this is rather ad-hoc (arguably hacky), because some of the machinery used for other actions, in particular `Primer.Zipper`, only supports expressions and types, but not kinds. This is something which should be revisited imminently.

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
  • Loading branch information
georgefst committed Aug 7, 2023
1 parent 63b0dd8 commit 257cb77
Show file tree
Hide file tree
Showing 8 changed files with 115 additions and 8 deletions.
2 changes: 2 additions & 0 deletions primer/src/Primer/Action.hs
Original file line number Diff line number Diff line change
Expand Up @@ -471,6 +471,8 @@ applyAction' a = case a of
RenameCaseBinding x -> \case
InBind (BindCase z) -> InBind . BindCase <$> renameCaseBinding x z
_ -> throwError $ CustomFailure a "cannot rename this node - not a case binding"
ConstructKType -> const $ throwError $ CustomFailure ConstructKType "kind edits currently only allowed in typedefs"
ConstructKFun -> const $ throwError $ CustomFailure ConstructKFun "kind edits currently only allowed in typedefs"
where
termAction f s = \case
InExpr ze -> InExpr <$> f ze
Expand Down
4 changes: 4 additions & 0 deletions primer/src/Primer/Action/Actions.hs
Original file line number Diff line number Diff line change
Expand Up @@ -107,6 +107,10 @@ data Action
RenameForall Text
| -- | Rename a case binding
RenameCaseBinding Text
| -- | Construct the kind KType
ConstructKType
| -- | Construct a function kind
ConstructKFun
deriving stock (Eq, Show, Read, Generic)
deriving (FromJSON, ToJSON) via PrimerJSON Action
deriving anyclass (NFData)
1 change: 1 addition & 0 deletions primer/src/Primer/Action/Errors.hs
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,7 @@ data ActionError
| NeedTypeDefConsSelection
| NeedTypeDefConsFieldSelection
| NeedTypeDefParamSelection
| NeedTypeDefParamKindSelection
| NoNodeSelection
| ValConNotFound TyConName ValConName
| FieldIndexOutOfBounds ValConName Int
Expand Down
2 changes: 2 additions & 0 deletions primer/src/Primer/Action/ProgAction.hs
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,8 @@ data ProgAction
SigAction [Action]
| -- | Execute a sequence of actions on the type of a field of a constructor in a typedef
ConFieldAction TyConName ValConName Int [Action]
| -- | Execute a sequence of actions on the kind of a parameter in a typedef
ParamKindAction TyConName TyVarName ID [Action]
| SetSmartHoles SmartHoles
| -- | CopyPaste (d,i) as
-- remembers the tree in def d, node i
Expand Down
44 changes: 41 additions & 3 deletions primer/src/Primer/App.hs
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ import Optics (
)
import Optics.State.Operators ((<<%=))
import Primer.Action (
Action,
Action (..),
ActionError (..),
ProgAction (..),
applyAction',
Expand Down Expand Up @@ -139,7 +139,7 @@ import Primer.Core (
GVarName,
GlobalName (baseName, qualifiedModule),
ID (..),
Kind' (KType),
Kind' (..),
KindMeta,
LocalName (LocalName, unLocalName),
Meta (..),
Expand Down Expand Up @@ -168,7 +168,7 @@ import Primer.Core (
_type,
_typeMetaLens,
)
import Primer.Core.DSL (S, create, emptyHole, tEmptyHole)
import Primer.Core.DSL (S, create, emptyHole, kfun, khole, ktype, tEmptyHole)
import Primer.Core.DSL qualified as DSL
import Primer.Core.Transform (renameTyVar, renameVar, unfoldTApp)
import Primer.Core.Utils (freeVars, generateKindIDs, generateTypeIDs, regenerateExprIDs, regenerateTypeIDs, _freeTmVars, _freeTyVars, _freeVarsTy)
Expand Down Expand Up @@ -988,6 +988,44 @@ applyProgAction prog = \case
}
}
)
ParamKindAction tyName paramName id actions -> editModuleOfCrossType (Just tyName) prog $ \(mod, mods) defName def -> do
def' <-
def
& traverseOf
#astTypeDefParameters
( maybe (throwError $ ParamNotFound paramName) pure
<=< findAndAdjustA
((== paramName) . fst)
( traverseOf _2 $
flip
( foldlM $ flip \case
ConstructKType -> modifyKind $ const ktype
ConstructKFun -> modifyKind \k -> ktype `kfun` pure k
Delete -> modifyKind $ const khole
a -> const $ throwError $ ActionError $ CustomFailure a "unexpected non-kind action"
)
actions
)
)
let mod' = mod & over #moduleTypes (Map.insert defName $ TypeDefAST def')
imports = progImports prog
smartHoles = progSmartHoles prog
mods' <-
runExceptT
( runReaderT
(checkEverything smartHoles (CheckEverything{trusted = imports, toCheck = mod' : mods}))
(buildTypingContextFromModules (mod : mods <> imports) smartHoles)
)
>>= either (throwError . ActionError) pure
pure (mods', Nothing)
where
modifyKind f k =
if getID k == id
then f k
else case k of
KHole _ -> pure k
KType _ -> pure k
KFun m k1 k2 -> KFun m <$> modifyKind f k1 <*> modifyKind f k2
SetSmartHoles smartHoles ->
pure $ prog & #progSmartHoles .~ smartHoles
CopyPasteSig fromIds setup -> case mdefName of
Expand Down
2 changes: 2 additions & 0 deletions primer/src/Primer/Core/DSL.hs
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ module Primer.Core.DSL (
tfun,
tapp,
tvar,
khole,
ktype,
kfun,
meta,
Expand Down Expand Up @@ -79,6 +80,7 @@ import Primer.Core (
import Primer.Core.DSL.Meta (S, create, create', meta, meta')
import Primer.Core.DSL.Type (
kfun,
khole,
ktype,
tEmptyHole,
tapp,
Expand Down
6 changes: 5 additions & 1 deletion primer/src/Primer/Core/DSL/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ module Primer.Core.DSL.Type (
tapp,
tvar,
tcon',
khole,
ktype,
kfun,
) where
Expand All @@ -27,7 +28,7 @@ import Primer.Core.Meta (
)
import Primer.Core.Type (
Kind,
Kind' (KFun, KType),
Kind' (KFun, KHole, KType),
Type,
Type' (..),
)
Expand Down Expand Up @@ -62,6 +63,9 @@ tvar v = TVar <$> meta <*> pure v
tcon' :: MonadFresh ID m => NonEmpty Name -> Name -> m Type
tcon' m n = tcon $ qualifyName (ModuleName m) n

khole :: MonadFresh ID m => m Kind
khole = KHole <$> kmeta

ktype :: MonadFresh ID m => m Kind
ktype = KType <$> kmeta

Expand Down
62 changes: 58 additions & 4 deletions primer/test/Tests/Action/Prog.hs
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@ import Primer.Action (
ConstructApp,
ConstructArrowL,
ConstructCase,
ConstructKFun,
ConstructKType,
ConstructLet,
ConstructTCon,
ConstructVar,
Expand Down Expand Up @@ -82,12 +84,13 @@ import Primer.Core (
GVarName,
GlobalName (baseName),
ID,
Kind' (KType),
Kind' (..),
Meta (..),
ModuleName (ModuleName, unModuleName),
Pattern (PatCon),
TmVarRef (..),
TyConName,
TyVarName,
Type,
Type' (..),
ValConName,
Expand Down Expand Up @@ -1175,6 +1178,51 @@ unit_ConFieldAction =
]
)

unit_ParamKindAction_1 :: Assertion
unit_ParamKindAction_1 =
progActionTest
( defaultProgEditableTypeDefs (pure [])
)
[ParamKindAction tT pB 30 [ConstructKFun]]
$ expectSuccess
$ \_ prog' -> do
td <- findTypeDef tT prog'
astTypeDefParameters td
@?= [ ("a", KType ())
, ("b", KFun () (KType ()) (KType ()))
]

unit_ParamKindAction_2 :: Assertion
unit_ParamKindAction_2 =
progActionTest
( defaultProgEditableTypeDefs (pure [])
)
[ ParamKindAction tT pB 30 [ConstructKFun]
, ParamKindAction tT pB 5 [ConstructKType]
]
$ expectSuccess
$ \_ prog' -> do
td <- findTypeDef tT prog'
astTypeDefParameters td
@?= [ ("a", KType ())
, ("b", KFun () (KType ()) (KType ()))
]

unit_ParamKindAction_3 :: Assertion
unit_ParamKindAction_3 =
progActionTest
( defaultProgEditableTypeDefs (pure [])
)
[ ParamKindAction tT pA 29 [Delete]
]
$ expectSuccess
$ \_ prog' -> do
td <- findTypeDef tT prog'
astTypeDefParameters td
@?= [ ("a", KHole ())
, ("b", KType ())
]

-- Check that we see name hints from imported modules
-- (This differs from the tests in Tests.Question by testing the actual action,
-- rather than the underlying functionality)
Expand Down Expand Up @@ -1482,7 +1530,8 @@ findDef d p = maybe (assertFailure "couldn't find def") pure $ defAST =<< findGl

-- We use the same type definition for all tests related to editing type definitions
-- (This is added to `defaultFullProg`)
-- The qualified name for this is recorded in 'tT', and its constructors are 'cA' and 'cB'
-- The qualified name for this is recorded in 'tT', its constructors are 'cA' and 'cB',
-- and its parameters in `pA` and `pB`.
defaultProgEditableTypeDefs :: MonadFresh ID f => f [(Name, ASTDef)] -> f Prog
defaultProgEditableTypeDefs ds = do
p <- defaultFullProg
Expand All @@ -1495,11 +1544,10 @@ defaultProgEditableTypeDefs ds = do
pure $
TypeDefAST
ASTTypeDef
{ astTypeDefParameters = [("a", ka), ("b", kb)]
{ astTypeDefParameters = [(pA, ka), (pB, kb)]
, astTypeDefConstructors = [ValCon cA fieldsA, ValCon cB fieldsB]
, astTypeDefNameHints = []
}

pure $
p
& (#progModules % _head % #moduleTypes) %~ (Map.singleton (baseName tT) td <>)
Expand All @@ -1514,6 +1562,12 @@ cA = vcn "A"
cB :: ValConName
cB = vcn "B"

pA :: TyVarName
pA = "a"

pB :: TyVarName
pB = "b"

unit_good_defaultFullProg :: Assertion
unit_good_defaultFullProg = checkProgWellFormed defaultFullProg

Expand Down

0 comments on commit 257cb77

Please sign in to comment.