From 7ba553f0d9d1018db90a97d2f01779faded256a2 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Mon, 17 Apr 2023 23:19:00 +0100 Subject: [PATCH 01/32] fix: Avoid long IDs for nodes in type of primitive def Signed-off-by: George Thomas --- primer/src/Primer/API.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index 75342e7df..bdd00ef78 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -676,7 +676,7 @@ viewProg p = flip evalState (0 :: Int) . traverseOf _typeMeta \() -> do n <- get put $ n + 1 - pure $ "primtype_" <> show d' <> "_" <> show n + pure $ "primtype_" <> Name.unName (Core.baseName name) <> "_" <> show n } ) <$> Map.assocs (moduleDefsQualified m) From ba08a345aa81fb8f0df204a5145a5d22c3ae373e Mon Sep 17 00:00:00 2001 From: George Thomas Date: Mon, 17 Apr 2023 13:40:56 +0100 Subject: [PATCH 02/32] refactor: Move selection types to `App.Base` This will be necessary in order to make use of them in actions-related modules. Signed-off-by: George Thomas --- primer/src/Primer/App.hs | 36 ++------------------------------ primer/src/Primer/App/Base.hs | 39 +++++++++++++++++++++++++++++++++++ 2 files changed, 41 insertions(+), 34 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 2a879b779..04dade189 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -48,8 +48,6 @@ module Primer.App ( handleEvalFullRequest, importModules, MutationRequest (..), - Selection (..), - NodeSelection (..), EvalReq (..), EvalResp (..), EvalFullReq (..), @@ -63,7 +61,6 @@ import Foreword hiding (mod) 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 (transform, transformM) import Data.Generics.Uniplate.Zipper ( fromZipper, @@ -78,10 +75,8 @@ import Optics ( Field3 (_3), ReversibleOptic (re), ifoldMap, - lens, mapped, over, - set, traverseOf, traversed, view, @@ -107,7 +102,9 @@ import Primer.Action.ProgError (ProgError (..)) import Primer.App.Base ( Editable (..), Level (..), + NodeSelection (..), NodeType (..), + Selection (..), ) import Primer.Core ( Bind' (Bind), @@ -115,10 +112,8 @@ import Primer.Core ( CaseBranch' (CaseBranch), Expr, Expr' (Case, Con, EmptyHole, Hole, Var), - ExprMeta, GVarName, GlobalName (baseName, qualifiedModule), - HasID (_id), ID (..), LocalName (LocalName, unLocalName), Meta (..), @@ -415,33 +410,6 @@ newtype Log = Log {unlog :: [[ProgAction]]} defaultLog :: Log defaultLog = Log mempty --- | Describes what interface element the user has selected. --- A definition in the left hand nav bar, and possibly a node in that definition. -data Selection = Selection - { selectedDef :: GVarName - -- ^ the ID of some ASTDef - , selectedNode :: Maybe NodeSelection - } - deriving stock (Eq, Show, Read, Generic, Data) - deriving (FromJSON, ToJSON) via PrimerJSON Selection - deriving anyclass (NFData) - --- | A selected node, in the body or type signature of some definition. --- We have the following invariant: @nodeType = SigNode ==> isRight meta@ -data NodeSelection = NodeSelection - { nodeType :: NodeType - , meta :: Either ExprMeta TypeMeta - } - deriving stock (Eq, Show, Read, Generic, Data) - deriving (FromJSON, ToJSON) via PrimerJSON NodeSelection - deriving anyclass (NFData) - -instance HasID NodeSelection where - _id = - lens - (either getID getID . meta) - (flip $ \id -> over #meta $ bimap (set _id id) (set _id id)) - -- | The type of requests which can mutate the application state. data MutationRequest = Undo diff --git a/primer/src/Primer/App/Base.hs b/primer/src/Primer/App/Base.hs index 6f4f834f5..c123fd1b1 100644 --- a/primer/src/Primer/App/Base.hs +++ b/primer/src/Primer/App/Base.hs @@ -1,14 +1,26 @@ +{-# LANGUAGE OverloadedLabels #-} + -- | Definitions needed to build the app. -- These are not part of the core language, but we may want to use them in dependencies of 'Primer.App'. module Primer.App.Base ( Level (..), Editable (..), NodeType (..), + Selection (..), + NodeSelection (..), ) where import Protolude import Data.Data (Data) +import Optics +import Primer.Core ( + ExprMeta, + GVarName, + HasID (..), + TypeMeta, + getID, + ) import Primer.JSON ( CustomJSON (CustomJSON), FromJSON, @@ -38,3 +50,30 @@ data NodeType = BodyNode | SigNode deriving stock (Eq, Show, Read, Bounded, Enum, Generic, Data) deriving (FromJSON, ToJSON) via PrimerJSON NodeType deriving anyclass (NFData) + +-- | Describes what interface element the user has selected. +-- A definition in the left hand nav bar, and possibly a node in that definition. +data Selection = Selection + { selectedDef :: GVarName + -- ^ the ID of some ASTDef + , selectedNode :: Maybe NodeSelection + } + deriving stock (Eq, Show, Read, Generic, Data) + deriving (FromJSON, ToJSON) via PrimerJSON Selection + deriving anyclass (NFData) + +-- | A selected node, in the body or type signature of some definition. +-- We have the following invariant: @nodeType = SigNode ==> isRight meta@ +data NodeSelection = NodeSelection + { nodeType :: NodeType + , meta :: Either ExprMeta TypeMeta + } + deriving stock (Eq, Show, Read, Generic, Data) + deriving (FromJSON, ToJSON) via PrimerJSON NodeSelection + deriving anyclass (NFData) + +instance HasID NodeSelection where + _id = + lens + (either getID getID . meta) + (flip $ \id -> over #meta $ bimap (set _id id) (set _id id)) From 0ac9c7154968aa883ca269cb2df01f0ae6e5f977 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Mon, 17 Apr 2023 14:46:16 +0100 Subject: [PATCH 03/32] refactor: Parameterise selection types We parameterise this way, rather than parameterising `ExprMeta` and `TypeMeta` separately, since we otherwise wouldn't be able to reconstruct even a basic `Selection' ID` from the OpenAPI API, without clients knowing whether a particular ID corresponds to a type or term. We want clients to be able to be dumber than that. Note that, for `Selection`, we use a synonym for the non-parameterised version, but not for `NodeSelection`, and we will not in future for `DefSelection` and `TypeDefSelection`. That's because this synonym is actually widely useful, and we use it in several modules to make things more readable. With `NodeSelection` etc. we never really require such a synonym, and we avoid it because of all the ceremony it would add, particularly around imports. Signed-off-by: George Thomas --- primer/src/Primer/API.hs | 4 +++- primer/src/Primer/App.hs | 3 ++- primer/src/Primer/App/Base.hs | 28 ++++++++++++++-------------- primer/src/Primer/Core/Meta.hs | 6 ++++++ primer/test/Tests/Action/Prog.hs | 2 +- primer/test/Tests/Serialization.hs | 3 ++- primer/test/Tests/Typecheck.hs | 2 +- 7 files changed, 29 insertions(+), 19 deletions(-) diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index bdd00ef78..44dab8b91 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -139,6 +139,7 @@ import Primer.Core ( CaseBranch' (..), Expr, Expr' (..), + ExprMeta, GVarName, GlobalName (..), HasID (..), @@ -152,6 +153,7 @@ import Primer.Core ( TyVarName, Type, Type' (..), + TypeMeta, ValConName, getID, unLocalName, @@ -1164,5 +1166,5 @@ data NodeSelection = NodeSelection deriving (FromJSON, ToJSON) via PrimerJSON NodeSelection deriving anyclass (NFData) -viewNodeSelection :: App.NodeSelection -> NodeSelection +viewNodeSelection :: App.NodeSelection (Either ExprMeta TypeMeta) -> NodeSelection viewNodeSelection sel@App.NodeSelection{nodeType} = NodeSelection{nodeType, id = getID sel} diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 04dade189..a5f308eba 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -104,7 +104,8 @@ import Primer.App.Base ( Level (..), NodeSelection (..), NodeType (..), - Selection (..), + Selection, + Selection' (..), ) import Primer.Core ( Bind' (Bind), diff --git a/primer/src/Primer/App/Base.hs b/primer/src/Primer/App/Base.hs index c123fd1b1..962ee9f3e 100644 --- a/primer/src/Primer/App/Base.hs +++ b/primer/src/Primer/App/Base.hs @@ -6,7 +6,8 @@ module Primer.App.Base ( Level (..), Editable (..), NodeType (..), - Selection (..), + Selection, + Selection' (..), NodeSelection (..), ) where @@ -53,27 +54,26 @@ data NodeType = BodyNode | SigNode -- | Describes what interface element the user has selected. -- A definition in the left hand nav bar, and possibly a node in that definition. -data Selection = Selection +type Selection = Selection' (Either ExprMeta TypeMeta) + +data Selection' a = Selection { selectedDef :: GVarName -- ^ the ID of some ASTDef - , selectedNode :: Maybe NodeSelection + , selectedNode :: Maybe (NodeSelection a) } - deriving stock (Eq, Show, Read, Generic, Data) - deriving (FromJSON, ToJSON) via PrimerJSON Selection + deriving stock (Eq, Show, Read, Functor, Generic, Data) + deriving (FromJSON, ToJSON) via PrimerJSON (Selection' a) deriving anyclass (NFData) -- | A selected node, in the body or type signature of some definition. -- We have the following invariant: @nodeType = SigNode ==> isRight meta@ -data NodeSelection = NodeSelection +data NodeSelection a = NodeSelection { nodeType :: NodeType - , meta :: Either ExprMeta TypeMeta + , meta :: a } - deriving stock (Eq, Show, Read, Generic, Data) - deriving (FromJSON, ToJSON) via PrimerJSON NodeSelection + deriving stock (Eq, Show, Read, Functor, Generic, Data) + deriving (FromJSON, ToJSON) via PrimerJSON (NodeSelection a) deriving anyclass (NFData) -instance HasID NodeSelection where - _id = - lens - (either getID getID . meta) - (flip $ \id -> over #meta $ bimap (set _id id) (set _id id)) +instance HasID a => HasID (NodeSelection a) where + _id = lens (getID . meta) (flip $ over #meta . set _id) diff --git a/primer/src/Primer/Core/Meta.hs b/primer/src/Primer/Core/Meta.hs index c9101b8ec..161a473be 100644 --- a/primer/src/Primer/Core/Meta.hs +++ b/primer/src/Primer/Core/Meta.hs @@ -159,6 +159,12 @@ instance HasID ID where instance HasID (Meta a) where _id = position @1 +instance (HasID a, HasID b) => HasID (Either a b) where + _id = + lens + (either getID getID) + (flip $ \id -> bimap (set _id id) (set _id id)) + -- This instance is used in 'Primer.Zipper', but it would be an orphan if we defined it there. instance HasID a => HasID (Zipper a a) where _id = lens getter setter diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 63f45d80d..348d100c5 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -42,7 +42,7 @@ import Primer.App ( ProgAction (..), ProgError (..), Question (GenerateName, VariablesInScope), - Selection (..), + Selection' (..), appIdCounter, appNameCounter, appProg, diff --git a/primer/test/Tests/Serialization.hs b/primer/test/Tests/Serialization.hs index 3594a1f08..47f2bc4c6 100644 --- a/primer/test/Tests/Serialization.hs +++ b/primer/test/Tests/Serialization.hs @@ -20,7 +20,8 @@ import Primer.App ( Prog (..), ProgAction (BodyAction, MoveToDef), ProgError (NoDefSelected), - Selection (..), + Selection, + Selection' (..), defaultLog, ) import Primer.Builtins (tNat) diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs index 58f4d8ec2..b1b7eaadd 100644 --- a/primer/test/Tests/Typecheck.hs +++ b/primer/test/Tests/Typecheck.hs @@ -799,7 +799,7 @@ instance Eq (TypeCacheAlpha [Module]) where (==) = tcaFunctorial instance Eq (TypeCacheAlpha ExprMeta) where (==) = tcaFunctorial -instance Eq (TypeCacheAlpha App.NodeSelection) where +instance Eq (TypeCacheAlpha (App.NodeSelection (Either ExprMeta TypeMeta))) where TypeCacheAlpha (App.NodeSelection t1 m1) == TypeCacheAlpha (App.NodeSelection t2 m2) = t1 == t2 && ((==) `on` first TypeCacheAlpha) m1 m2 instance Eq (TypeCacheAlpha App.Selection) where From 355463ce4150f2fa2ba7e286988d960cb3951a50 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Mon, 17 Apr 2023 21:26:13 +0100 Subject: [PATCH 04/32] refactor!: Rename selection fields This will significantly decrease the amount of breakage when we unify our selection types. Signed-off-by: George Thomas --- primer/src/Primer/API.hs | 2 +- primer/src/Primer/App.hs | 15 ++++++++------- primer/src/Primer/App/Base.hs | 8 +++++--- primer/test/Tests/Action/Prog.hs | 5 +++-- .../outputs/serialization/edit_response_2.json | 4 ++-- primer/test/outputs/serialization/prog.json | 4 ++-- primer/test/outputs/serialization/selection.json | 4 ++-- 7 files changed, 23 insertions(+), 19 deletions(-) diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index 44dab8b91..73f44638c 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -1155,7 +1155,7 @@ data Selection = Selection deriving anyclass (NFData) viewSelection :: App.Selection -> Selection -viewSelection App.Selection{..} = Selection{def = selectedDef, node = viewNodeSelection <$> selectedNode} +viewSelection App.Selection{..} = Selection{def = def, node = viewNodeSelection <$> node} -- | 'App.NodeSelection' without any node metadata. data NodeSelection = NodeSelection diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index a5f308eba..3b8b46e41 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -1,5 +1,6 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE ViewPatterns #-} -- This module defines the high level application functions. @@ -323,8 +324,8 @@ newEmptyProgImporting imported = , progSelection = Just Selection - { selectedDef = qualifyName moduleName defName - , selectedNode = Nothing + { def = qualifyName moduleName defName + , node = Nothing } } , nextID @@ -521,7 +522,7 @@ handleEditRequest actions = do go :: (Prog, Maybe GVarName) -> ProgAction -> m (Prog, Maybe GVarName) go (prog, mdef) a = applyProgAction prog mdef a <&> \prog' -> - (prog', selectedDef <$> progSelection prog') + (prog', (.def) <$> progSelection prog') -- | Handle an eval request (we assume that all such requests are implicitly in a synthesisable context) handleEvalRequest :: @@ -1383,8 +1384,8 @@ tcWholeProg p = do newSel <- case oldSel of Nothing -> pure Nothing Just s -> do - let defName_ = s ^. #selectedDef - updatedNode <- case s ^. #selectedNode of + let defName_ = s.def + updatedNode <- case s.node of Nothing -> pure Nothing Just sel@NodeSelection{nodeType} -> do n <- runExceptT $ focusNode p' defName_ $ getID sel @@ -1395,8 +1396,8 @@ tcWholeProg p = do pure $ Just $ Selection - { selectedDef = defName_ - , selectedNode = updatedNode + { def = defName_ + , node = updatedNode } pure $ p'{progSelection = newSel} diff --git a/primer/src/Primer/App/Base.hs b/primer/src/Primer/App/Base.hs index 962ee9f3e..e591b7b3a 100644 --- a/primer/src/Primer/App/Base.hs +++ b/primer/src/Primer/App/Base.hs @@ -1,4 +1,6 @@ {-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE OverloadedRecordDot #-} +{-# LANGUAGE NoFieldSelectors #-} -- | Definitions needed to build the app. -- These are not part of the core language, but we may want to use them in dependencies of 'Primer.App'. @@ -57,9 +59,9 @@ data NodeType = BodyNode | SigNode type Selection = Selection' (Either ExprMeta TypeMeta) data Selection' a = Selection - { selectedDef :: GVarName + { def :: GVarName -- ^ the ID of some ASTDef - , selectedNode :: Maybe (NodeSelection a) + , node :: Maybe (NodeSelection a) } deriving stock (Eq, Show, Read, Functor, Generic, Data) deriving (FromJSON, ToJSON) via PrimerJSON (Selection' a) @@ -76,4 +78,4 @@ data NodeSelection a = NodeSelection deriving anyclass (NFData) instance HasID a => HasID (NodeSelection a) where - _id = lens (getID . meta) (flip $ over #meta . set _id) + _id = lens (getID . (.meta)) (flip $ over #meta . set _id) diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 348d100c5..90d661594 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -1,4 +1,5 @@ {-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE OverloadedRecordDot #-} module Tests.Action.Prog where @@ -1323,7 +1324,7 @@ unit_rename_module = Left err -> assertFailure $ show err Right p -> do fmap (unModuleName . moduleName) (progModules p) @?= [["Module2"]] - selectedDef <$> progSelection p @?= Just (qualifyName (ModuleName ["Module2"]) "main") + (.def) <$> progSelection p @?= Just (qualifyName (ModuleName ["Module2"]) "main") case fmap (Map.assocs . moduleDefsQualified) (progModules p) of [[(n, DefAST d)]] -> do let expectedName = qualifyName (ModuleName ["Module2"]) "main" @@ -1506,7 +1507,7 @@ unit_sh_lost_id = Just def -> case astDefExpr <$> defAST def of Just (Var m (GlobalVarRef f)) | f == foo -> case progSelection prog' of - Just Selection{selectedDef, selectedNode = Just sel} -> + Just Selection{def = selectedDef, node = Just sel} -> unless (selectedDef == foo && getID sel == getID m) $ assertFailure "expected selection to point at the recursive reference" _ -> assertFailure "expected the selection to point at some node" diff --git a/primer/test/outputs/serialization/edit_response_2.json b/primer/test/outputs/serialization/edit_response_2.json index 5fd634d7a..6f9f6749d 100644 --- a/primer/test/outputs/serialization/edit_response_2.json +++ b/primer/test/outputs/serialization/edit_response_2.json @@ -147,13 +147,13 @@ } ], "progSelection": { - "selectedDef": { + "def": { "baseName": "main", "qualifiedModule": [ "M" ] }, - "selectedNode": { + "node": { "meta": { "Left": [ 0, diff --git a/primer/test/outputs/serialization/prog.json b/primer/test/outputs/serialization/prog.json index 02b6dc308..f7dff71af 100644 --- a/primer/test/outputs/serialization/prog.json +++ b/primer/test/outputs/serialization/prog.json @@ -146,13 +146,13 @@ } ], "progSelection": { - "selectedDef": { + "def": { "baseName": "main", "qualifiedModule": [ "M" ] }, - "selectedNode": { + "node": { "meta": { "Left": [ 0, diff --git a/primer/test/outputs/serialization/selection.json b/primer/test/outputs/serialization/selection.json index 0ac964006..2fe4a279a 100644 --- a/primer/test/outputs/serialization/selection.json +++ b/primer/test/outputs/serialization/selection.json @@ -1,11 +1,11 @@ { - "selectedDef": { + "def": { "baseName": "main", "qualifiedModule": [ "M" ] }, - "selectedNode": { + "node": { "meta": { "Left": [ 0, From 580a73806c96660470ed1fe4eb7de0698fd73530 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Tue, 16 May 2023 12:15:55 +0100 Subject: [PATCH 05/32] refactor!: Don't use API-specific selection types This removes some boilerplate where we converted between types which are essentially the same. That boilerplate would have become much bigger once we extend selections to cover type definitions. Despite the previous commit, there is one small breaking change, seen in `openapi.json` (`meta` instead of `id`). Signed-off-by: George Thomas --- primer-service/src/Primer/OpenAPI.hs | 28 +++++++++--- primer-service/test/Tests/OpenAPI.hs | 9 ++-- .../test/outputs/OpenAPI/openapi.json | 4 +- primer/src/Primer/API.hs | 44 ++++--------------- 4 files changed, 37 insertions(+), 48 deletions(-) diff --git a/primer-service/src/Primer/OpenAPI.hs b/primer-service/src/Primer/OpenAPI.hs index 91db986b5..2e4c7f6da 100644 --- a/primer-service/src/Primer/OpenAPI.hs +++ b/primer-service/src/Primer/OpenAPI.hs @@ -10,6 +10,12 @@ module Primer.OpenAPI ( import Foreword import Data.Aeson ( + FromJSON, + GFromJSON, + GToEncoding, + GToJSON, + ToJSON, + Zero, toJSON, ) import Data.OpenApi ( @@ -27,6 +33,7 @@ import Data.OpenApi.Internal.Schema ( rename, timeSchema, ) +import Data.Text qualified as T import Data.Time ( UTCTime (..), fromGregorian, @@ -42,9 +49,8 @@ import Primer.API ( Module, NewSessionReq, NodeBody, - NodeSelection (..), Prog, - Selection (..), + Selection, Tree, ) import Primer.API qualified as API @@ -56,7 +62,7 @@ import Primer.API.NodeFlavor ( ) import Primer.API.RecordPair (RecordPair) import Primer.Action.Available qualified as Available -import Primer.App (NodeType) +import Primer.App (NodeSelection, NodeType) import Primer.App.Base (Level) import Primer.Core ( GlobalName, @@ -71,10 +77,14 @@ import Primer.Database ( Session, SessionName, ) -import Primer.JSON (CustomJSON, PrimerJSON) +import Primer.JSON (CustomJSON (CustomJSON), PrimerJSON) import Primer.Name (Name) import Servant.API (FromHttpApiData (parseQueryParam), ToHttpApiData (toQueryParam)) +newtype PrimerJSONNamed (s :: Symbol) a = PrimerJSONNamed a +deriving via PrimerJSON a instance (Generic a, GFromJSON Zero (Rep a)) => FromJSON (PrimerJSONNamed s a) +deriving via PrimerJSON a instance (Generic a, GToJSON Zero (Rep a), GToEncoding Zero (Rep a)) => ToJSON (PrimerJSONNamed s a) + -- $orphanInstances -- -- We define some OpenApi orphan instances in primer-service, to avoid @@ -89,6 +99,12 @@ instance where declareNamedSchema _ = genericDeclareNamedSchema (fromAesonOptions (aesonOptions @os)) (Proxy @a) +instance + (Typeable a, Generic a, GToSchema (Rep a), KnownSymbol s) => + ToSchema (PrimerJSONNamed s a) + where + declareNamedSchema _ = rename (Just $ T.pack $ symbolVal $ Proxy @s) <$> declareNamedSchema (Proxy @(PrimerJSON a)) + instance ToSchema SessionName deriving via PrimerJSON Session instance ToSchema Session @@ -146,8 +162,8 @@ deriving via PrimerJSON Available.FreeInput instance ToSchema Available.FreeInpu deriving via PrimerJSON Available.Options instance ToSchema Available.Options deriving via PrimerJSON Available.Action instance ToSchema Available.Action deriving via PrimerJSON ApplyActionBody instance ToSchema ApplyActionBody -deriving via PrimerJSON Selection instance ToSchema Selection -deriving via PrimerJSON NodeSelection instance ToSchema NodeSelection +deriving via PrimerJSONNamed "Selection" Selection instance ToSchema Selection +deriving via PrimerJSONNamed "NodeSelection" (NodeSelection ID) instance ToSchema (NodeSelection ID) deriving via PrimerJSON NodeType instance ToSchema NodeType deriving via PrimerJSON Level instance ToSchema Level deriving via PrimerJSON NewSessionReq instance ToSchema NewSessionReq diff --git a/primer-service/test/Tests/OpenAPI.hs b/primer-service/test/Tests/OpenAPI.hs index a00773e92..3ea78addc 100644 --- a/primer-service/test/Tests/OpenAPI.hs +++ b/primer-service/test/Tests/OpenAPI.hs @@ -30,9 +30,8 @@ import Primer.API ( Module (Module), NewSessionReq (..), NodeBody (BoxBody, NoBody, PrimBody, TextBody), - NodeSelection (..), Prog (Prog), - Selection (..), + Selection, Tree, viewTreeExpr, viewTreeType, @@ -45,7 +44,7 @@ import Primer.API.NodeFlavor ( ) import Primer.API.RecordPair (RecordPair (RecordPair)) import Primer.Action.Available qualified as Available -import Primer.App (Level, NodeType) +import Primer.App (Level, NodeSelection (NodeSelection), NodeType, Selection' (Selection)) import Primer.Core (GVarName, ID (ID), ModuleName, PrimCon (PrimChar, PrimInt)) import Primer.Database ( LastModified (..), @@ -224,7 +223,7 @@ tasty_Module = testToJSON $ evalExprGen 0 genModule genNodeType :: ExprGen NodeType genNodeType = G.enumBounded -genNodeSelection :: ExprGen NodeSelection +genNodeSelection :: ExprGen (NodeSelection ID) genNodeSelection = NodeSelection <$> genNodeType <*> genID genSelection :: ExprGen Selection @@ -307,7 +306,7 @@ instance Arbitrary ApplyActionBody where arbitrary = ApplyActionBody <$> arbitrary <*> arbitrary instance Arbitrary Selection where arbitrary = hedgehog $ evalExprGen 0 genSelection -instance Arbitrary NodeSelection where +instance Arbitrary (NodeSelection ID) where arbitrary = hedgehog $ evalExprGen 0 genNodeSelection instance Arbitrary a => Arbitrary (NonEmpty a) where arbitrary = (:|) <$> arbitrary <*> arbitrary diff --git a/primer-service/test/outputs/OpenAPI/openapi.json b/primer-service/test/outputs/OpenAPI/openapi.json index a67c94034..e9f401427 100644 --- a/primer-service/test/outputs/OpenAPI/openapi.json +++ b/primer-service/test/outputs/OpenAPI/openapi.json @@ -413,7 +413,7 @@ }, "NodeSelection": { "properties": { - "id": { + "meta": { "maximum": 9223372036854775807, "minimum": -9223372036854775808, "type": "integer" @@ -424,7 +424,7 @@ }, "required": [ "nodeType", - "id" + "meta" ], "type": "object" }, diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index 73f44638c..94d869526 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -62,10 +62,7 @@ module Primer.API ( viewTreeType, viewTreeExpr, getApp, - Selection (..), - viewSelection, - NodeSelection (..), - viewNodeSelection, + Selection, undoAvailable, redoAvailable, Name (..), @@ -139,7 +136,6 @@ import Primer.Core ( CaseBranch' (..), Expr, Expr' (..), - ExprMeta, GVarName, GlobalName (..), HasID (..), @@ -153,7 +149,6 @@ import Primer.Core ( TyVarName, Type, Type' (..), - TypeMeta, ValConName, getID, unLocalName, @@ -654,7 +649,7 @@ viewProg :: App.Prog -> Prog viewProg p = Prog { modules = map (viewModule True) (progModules p) <> map (viewModule False) (progImports p) - , selection = viewSelection <$> progSelection p + , selection = getID <<$>> progSelection p , undoAvailable = not $ null $ unlog $ progLog p , redoAvailable = not $ null $ unlog $ redoLog p } @@ -1040,10 +1035,10 @@ availableActions = curry3 $ logAPI (noError AvailableActions) $ \(sid, level, se case selection.node of Nothing -> pure $ Available.forDef (snd <$> allDefs) level editable selection.def - Just NodeSelection{..} -> do + Just App.NodeSelection{..} -> do pure $ case nodeType of - SigNode -> Available.forSig level editable type_ id - BodyNode -> Available.forBody (snd <$> allTypeDefs) level editable expr id + SigNode -> Available.forSig level editable type_ meta + BodyNode -> Available.forBody (snd <$> allTypeDefs) level editable expr meta actionOptions :: (MonadIO m, MonadThrow m, MonadAPILog l m) => @@ -1057,7 +1052,7 @@ actionOptions = curry4 $ logAPI (noError ActionOptions) $ \(sid, level, selectio let prog = appProg app allDefs = progAllDefs prog allTypeDefs = progAllTypeDefs prog - nodeSel = selection.node <&> \s -> (s.nodeType, s.id) + nodeSel = selection.node <&> \s -> (s.nodeType, s.meta) def' <- snd <$> findASTDef allDefs selection.def maybe (throwM $ ActionOptionsNoID nodeSel) pure $ Available.options @@ -1090,7 +1085,7 @@ applyActionNoInput = curry3 $ logAPI (noError ApplyActionNoInput) $ \(sid, selec (snd <$> progAllDefs prog) def selection.def - (selection.node <&> \s -> (s.nodeType, s.id)) + (selection.node <&> \s -> (s.nodeType, s.meta)) action applyActions sid actions @@ -1108,7 +1103,7 @@ applyActionInput = curry3 $ logAPI (noError ApplyActionInput) $ \(sid, body, act toProgActionInput def body.selection.def - (body.selection.node <&> \s -> (s.nodeType, s.id)) + (body.selection.node <&> \s -> (s.nodeType, s.meta)) body.option action applyActions sid actions @@ -1146,25 +1141,4 @@ redo = >>= either (throwM . RedoError) (pure . viewProg) -- | 'App.Selection' without any node metadata. -data Selection = Selection - { def :: GVarName - , node :: Maybe NodeSelection - } - deriving stock (Eq, Show, Read, Generic) - deriving (FromJSON, ToJSON) via PrimerJSON Selection - deriving anyclass (NFData) - -viewSelection :: App.Selection -> Selection -viewSelection App.Selection{..} = Selection{def = def, node = viewNodeSelection <$> node} - --- | 'App.NodeSelection' without any node metadata. -data NodeSelection = NodeSelection - { nodeType :: NodeType - , id :: ID - } - deriving stock (Eq, Show, Read, Generic) - deriving (FromJSON, ToJSON) via PrimerJSON NodeSelection - deriving anyclass (NFData) - -viewNodeSelection :: App.NodeSelection (Either ExprMeta TypeMeta) -> NodeSelection -viewNodeSelection sel@App.NodeSelection{nodeType} = NodeSelection{nodeType, id = getID sel} +type Selection = App.Selection' ID From 7ef54d279052f7fd3088f3874a4ec52579acb8fa Mon Sep 17 00:00:00 2001 From: George Thomas Date: Thu, 20 Apr 2023 23:36:52 +0100 Subject: [PATCH 06/32] refactor: Make further use of new deriving helper Signed-off-by: George Thomas --- primer-service/src/Primer/OpenAPI.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/primer-service/src/Primer/OpenAPI.hs b/primer-service/src/Primer/OpenAPI.hs index 2e4c7f6da..8417c5fa2 100644 --- a/primer-service/src/Primer/OpenAPI.hs +++ b/primer-service/src/Primer/OpenAPI.hs @@ -136,8 +136,7 @@ deriving via Text instance (ToSchema Name) -- at the openapi level, so api consumers do not have to deal with -- three identical types. Note that our openapi interface is a -- simplified view, so this collapse is in the correct spirit. -instance ToSchema (GlobalName 'ADefName) where - declareNamedSchema _ = rename (Just "GlobalName") <$> declareNamedSchema (Proxy @(PrimerJSON (GlobalName 'ADefName))) +deriving via PrimerJSONNamed "GlobalName" (GlobalName 'ADefName) instance ToSchema (GlobalName 'ADefName) deriving via GlobalName 'ADefName instance ToSchema (GlobalName 'ATyCon) deriving via GlobalName 'ADefName instance ToSchema (GlobalName 'AValCon) From 0a679750885e9eccd35ee1cb17544f6802bcfcc2 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Thu, 20 Apr 2023 23:37:09 +0100 Subject: [PATCH 07/32] refactor: Applying actions takes selection Signed-off-by: George Thomas --- primer/src/Primer/API.hs | 30 ++++--------------- primer/src/Primer/Action.hs | 42 +++++++++++++-------------- primer/src/Primer/Action/Available.hs | 25 +++++++++------- primer/test/Tests/Action/Available.hs | 22 +++++++------- 4 files changed, 52 insertions(+), 67 deletions(-) diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index 94d869526..808dc1deb 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -255,7 +255,7 @@ data PrimerErr | UnexpectedPrimDef GVarName | AddDefError ModuleName (Maybe Text) ProgError | AddTypeDefError TyConName [ValConName] ProgError - | ActionOptionsNoID (Maybe (NodeType, ID)) + | ActionOptionsNoID Selection | ToProgActionError Available.Action ActionError | ApplyActionError [ProgAction] ProgError | UndoError ProgError @@ -1052,17 +1052,9 @@ actionOptions = curry4 $ logAPI (noError ActionOptions) $ \(sid, level, selectio let prog = appProg app allDefs = progAllDefs prog allTypeDefs = progAllTypeDefs prog - nodeSel = selection.node <&> \s -> (s.nodeType, s.meta) - def' <- snd <$> findASTDef allDefs selection.def - maybe (throwM $ ActionOptionsNoID nodeSel) pure $ - Available.options - (snd <$> allTypeDefs) - (snd <$> allDefs) - (progCxt prog) - level - def' - nodeSel - action + def <- snd <$> findASTDef allDefs selection.def + maybe (throwM $ ActionOptionsNoID selection) pure $ + Available.options (snd <$> allTypeDefs) (snd <$> allDefs) (progCxt prog) level def selection action findASTDef :: MonadThrow m => Map GVarName (Editable, Def.Def) -> GVarName -> m (Editable, ASTDef) findASTDef allDefs def = case allDefs Map.!? def of @@ -1081,12 +1073,7 @@ applyActionNoInput = curry3 $ logAPI (noError ApplyActionNoInput) $ \(sid, selec def <- snd <$> findASTDef (progAllDefs prog) selection.def actions <- either (throwM . ToProgActionError (Available.NoInput action)) pure $ - toProgActionNoInput - (snd <$> progAllDefs prog) - def - selection.def - (selection.node <&> \s -> (s.nodeType, s.meta)) - action + toProgActionNoInput (snd <$> progAllDefs prog) def selection action applyActions sid actions applyActionInput :: @@ -1100,12 +1087,7 @@ applyActionInput = curry3 $ logAPI (noError ApplyActionInput) $ \(sid, body, act def <- snd <$> findASTDef (progAllDefs prog) body.selection.def actions <- either (throwM . ToProgActionError (Available.Input action)) pure $ - toProgActionInput - def - body.selection.def - (body.selection.node <&> \s -> (s.nodeType, s.meta)) - body.option - action + toProgActionInput def body.selection body.option action applyActions sid actions data ApplyActionBody = ApplyActionBody diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index 1d0e7c6dc..e968efd8c 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -35,7 +35,7 @@ import Primer.Action.Actions (Action (..), Movement (..), QualifiedText) import Primer.Action.Available qualified as Available import Primer.Action.Errors (ActionError (..)) import Primer.Action.ProgAction (ProgAction (..)) -import Primer.App.Base (NodeType (..)) +import Primer.App.Base (NodeSelection (..), NodeType (..), Selection' (..)) import Primer.Core ( Expr, Expr' (..), @@ -859,11 +859,10 @@ renameForall b zt = case target zt of toProgActionNoInput :: DefMap -> ASTDef -> - GVarName -> - Maybe (NodeType, ID) -> + Selection' ID -> Available.NoInputAction -> Either ActionError [ProgAction] -toProgActionNoInput defs def defName mNodeSel = \case +toProgActionNoInput defs def sel = \case Available.MakeCase -> toProgAction [ConstructCase] Available.MakeApp -> @@ -878,7 +877,7 @@ toProgActionNoInput defs def defName mNodeSel = \case toProgAction [ConvertLetToLetrec] Available.Raise -> do id <- mid - pure [MoveToDef defName, CopyPasteBody (defName, id) [SetCursor id, Move Parent, Delete]] + pure [MoveToDef sel.def, CopyPasteBody (sel.def, id) [SetCursor id, Move Parent, Delete]] Available.EnterHole -> toProgAction [EnterHole] Available.RemoveHole -> @@ -911,34 +910,33 @@ toProgActionNoInput defs def defName mNodeSel = \case toProgAction [ConstructTApp, Move Child1] Available.RaiseType -> do id <- mid - pure [MoveToDef defName, CopyPasteSig (defName, id) [SetCursor id, Move Parent, Delete]] + pure [MoveToDef sel.def, CopyPasteSig (sel.def, id) [SetCursor id, Move Parent, Delete]] Available.DeleteType -> toProgAction [Delete] Available.DuplicateDef -> let sigID = getID $ astDefType def bodyID = getID $ astDefExpr def - copyName = uniquifyDefName (qualifiedModule defName) (unName (baseName defName) <> "Copy") defs + copyName = uniquifyDefName (qualifiedModule sel.def) (unName (baseName sel.def) <> "Copy") defs in pure - [ CreateDef (qualifiedModule defName) (Just copyName) - , CopyPasteSig (defName, sigID) [] - , CopyPasteBody (defName, bodyID) [] + [ CreateDef (qualifiedModule sel.def) (Just copyName) + , CopyPasteSig (sel.def, sigID) [] + , CopyPasteBody (sel.def, bodyID) [] ] Available.DeleteDef -> - pure [DeleteDef defName] + pure [DeleteDef sel.def] where - toProgAction actions = toProg' actions defName <$> maybeToEither NoNodeSelection mNodeSel - mid = maybeToEither NoNodeSelection $ snd <$> mNodeSel + toProgAction actions = toProg' actions sel.def <$> maybeToEither NoNodeSelection sel.node + mid = maybeToEither NoNodeSelection $ (.meta) <$> sel.node -- | Convert a high-level 'Available.InputAction', and associated 'Available.Option', -- to a concrete sequence of 'ProgAction's. toProgActionInput :: ASTDef -> - GVarName -> - Maybe (NodeType, ID) -> + Selection' ID -> Available.Option -> Available.InputAction -> Either ActionError [ProgAction] -toProgActionInput def defName mNodeSel opt0 = \case +toProgActionInput def sel opt0 = \case Available.MakeCon -> do opt <- optGlobal toProg [ConstructSaturatedCon opt] @@ -994,9 +992,9 @@ toProgActionInput def defName mNodeSel opt0 = \case toProg [RenameForall opt] Available.RenameDef -> do opt <- optNoCxt - pure [RenameDef defName opt] + pure [RenameDef sel.def opt] where - mid = maybeToEither NoNodeSelection $ snd <$> mNodeSel + mid = maybeToEither NoNodeSelection $ (.meta) <$> sel.node optVar = case opt0.context of Just q -> GlobalVarRef $ unsafeMkGlobalName (q, opt0.option) Nothing -> LocalVarRef $ unsafeMkLocalName opt0.option @@ -1009,7 +1007,7 @@ toProgActionInput def defName mNodeSel opt0 = \case optGlobal = case opt0.context of Nothing -> Left $ NeedLocal opt0 Just q -> pure (q, opt0.option) - toProg actions = toProg' actions defName <$> maybeToEither NoNodeSelection mNodeSel + toProg actions = toProg' actions sel.def <$> maybeToEither NoNodeSelection sel.node offerRefined = do id <- mid -- If we have a useful type, offer the refine action, otherwise offer the saturate action. @@ -1022,10 +1020,10 @@ toProgActionInput def defName mNodeSel opt0 = \case Just (sm, _) -> Left $ NeedType sm Nothing -> Left $ IDNotFound id -toProg' :: [Action] -> GVarName -> (NodeType, ID) -> [ProgAction] -toProg' actions defName (nt, id) = +toProg' :: [Action] -> GVarName -> NodeSelection ID -> [ProgAction] +toProg' actions defName sel = [ MoveToDef defName - , (SetCursor id : actions) & case nt of + , (SetCursor sel.meta : actions) & case sel.nodeType of SigNode -> SigAction BodyNode -> BodyAction ] diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs index 278aada79..74a97c481 100644 --- a/primer/src/Primer/Action/Available.hs +++ b/primer/src/Primer/Action/Available.hs @@ -1,4 +1,5 @@ {-# LANGUAGE BlockArguments #-} +{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE NoFieldSelectors #-} -- | Compute all the possible actions which can be performed on a definition. @@ -33,7 +34,9 @@ import Primer.Action.Priorities qualified as P import Primer.App.Base ( Editable (..), Level (..), + NodeSelection (..), NodeType (..), + Selection' (..), ) import Primer.Core ( Expr, @@ -320,12 +323,12 @@ options :: Cxt -> Level -> ASTDef -> - Maybe (NodeType, ID) -> + Selection' ID -> InputAction -> -- | Returns 'Nothing' if an ID was required but not passed, passed but not found in the tree, -- 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 +options typeDefs defs cxt level def sel = \case MakeCon -> pure . noFree @@ -395,23 +398,23 @@ options typeDefs defs cxt level def mNodeSel = \case (first (localOpt . unLocalName) <$> locals) <> (first globalOpt <$> globals) findNode = do - (nt, id) <- mNodeSel - case nt of - BodyNode -> fst <$> findNodeWithParent id (astDefExpr def) - SigNode -> TypeNode <$> findType id (astDefType def) + s <- sel.node + case s.nodeType of + BodyNode -> fst <$> findNodeWithParent s.meta (astDefExpr def) + SigNode -> TypeNode <$> findType s.meta (astDefType def) genNames typeOrKind = do - z <- focusNode =<< mNodeSel + z <- focusNode =<< sel.node pure $ map localOpt $ flip runReader cxt $ case z of Left zE -> generateNameExpr typeOrKind zE Right zT -> generateNameTy typeOrKind zT varsInScope = do - nodeSel <- mNodeSel + nodeSel <- sel.node focusNode nodeSel <&> \case Left zE -> variablesInScopeExpr defs zE Right zT -> (variablesInScopeTy zT, [], []) - focusNode (nt, id) = case nt of - BodyNode -> Left . locToEither <$> focusOn id (astDefExpr def) - SigNode -> fmap Right $ focusOnTy id $ astDefType def + focusNode nodeSel = case nodeSel.nodeType of + BodyNode -> Left . locToEither <$> focusOn nodeSel.meta (astDefExpr def) + SigNode -> fmap Right $ focusOnTy nodeSel.meta $ astDefType def -- Extract the source of the function type we were checked at -- i.e. the type that a lambda-bound variable would have here lamVarTy = \case diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs index 5c16f2862..53da67dfb 100644 --- a/primer/test/Tests/Action/Available.hs +++ b/primer/test/Tests/Action/Available.hs @@ -49,8 +49,10 @@ import Primer.App ( EditAppM, Editable (..), Level (Beginner, Expert, Intermediate), + NodeSelection (..), NodeType (..), ProgError (ActionError, DefAlreadyExists), + Selection' (..), appProg, checkAppWellFormed, checkProgWellFormed, @@ -191,12 +193,12 @@ mkTests deps (defName, DefAST def') = in testGroup testName $ enumeratePairs <&> \(level, mut) -> - let defActions = map (offered level Nothing) $ Available.forDef defs level mut d + let defActions = map (offered level $ Selection defName Nothing) $ Available.forDef defs level mut d bodyActions = map ( \id -> ( id - , map (offered level (Just (BodyNode, id))) $ + , map (offered level $ Selection defName $ Just $ NodeSelection BodyNode id) $ Available.forBody typeDefs level @@ -211,7 +213,7 @@ mkTests deps (defName, DefAST def') = map ( \id -> ( id - , map (offered level (Just (SigNode, id))) $ Available.forSig level mut (astDefType def) id + , map (offered level (Selection defName $ Just $ NodeSelection SigNode id)) $ Available.forSig level mut (astDefType def) id ) ) . toListOf (_typeMeta % _id) @@ -275,7 +277,7 @@ tasty_available_actions_accepted = withTests 500 $ DefAST{} -> label "AST" DefPrim{} -> label "Prim" (loc, acts) <- - fmap snd . forAllWithT fst $ + fmap (first (Selection defName) . snd) . forAllWithT fst $ Gen.frequency $ catMaybes [ Just (1, pure ("actionsForDef", (Nothing, Available.forDef (snd <$> allDefs) l defMut defName))) @@ -284,13 +286,13 @@ tasty_available_actions_accepted = withTests 500 $ ids = ty ^.. typeIDs i <- Gen.element ids let hedgehogMsg = "actionsForDefSig id " <> show i - pure (hedgehogMsg, (Just (SigNode, i), Available.forSig l defMut ty i)) + pure (hedgehogMsg, (Just $ NodeSelection SigNode i, Available.forSig l defMut ty i)) , defAST def <&> \d' -> (7,) $ do let expr = astDefExpr d' ids = expr ^.. exprIDs i <- Gen.element ids let hedgehogMsg = "actionsForDefBody id " <> show i - pure (hedgehogMsg, (Just (BodyNode, i), Available.forBody (snd <$> progAllTypeDefs (appProg a)) l defMut expr i)) + pure (hedgehogMsg, (Just $ NodeSelection BodyNode i, Available.forBody (snd <$> progAllTypeDefs (appProg a)) l defMut expr i)) ] case acts of [] -> label "no offered actions" >> success @@ -302,7 +304,7 @@ tasty_available_actions_accepted = withTests 500 $ def' <- maybe (annotate "primitive def" >> failure) pure $ defAST def progActs <- either (\e -> annotateShow e >> failure) pure $ - toProgActionNoInput (map snd $ progAllDefs $ appProg a) def' defName loc act' + toProgActionNoInput (map snd $ progAllDefs $ appProg a) def' loc act' actionSucceeds (handleEditRequest progActs) a Available.Input act' -> do def' <- maybe (annotate "primitive def" >> failure) pure $ defAST def @@ -327,7 +329,7 @@ tasty_available_actions_accepted = withTests 500 $ [] -> annotate "no options" >> success options -> do opt <- forAllT $ Gen.choice options - progActs <- either (\e -> annotateShow e >> failure) pure $ toProgActionInput def' defName loc (snd opt) act' + progActs <- either (\e -> annotateShow e >> failure) pure $ toProgActionInput def' loc (snd opt) act' actionSucceedsOrCapture (fst opt) (handleEditRequest progActs) a where runEditAppMLogs :: @@ -600,7 +602,7 @@ offeredActionTest' sh l inputDef position action = do Left a -> pure $ if Available.NoInput a `elem` offered - then Right $ toProgActionNoInput (foldMap' moduleDefsQualified $ progModules prog) exprDef exprDefName (Just (BodyNode, id)) a + then Right $ toProgActionNoInput (foldMap' moduleDefsQualified $ progModules prog) exprDef (Selection exprDefName $ Just $ NodeSelection BodyNode id) a else Left $ ActionNotOffered (Available.NoInput a) offered Right (a, o) -> do if Available.Input a `elem` offered @@ -609,7 +611,7 @@ offeredActionTest' sh l inputDef position action = do Just os -> pure $ if o `elem` os.opts - then Right $ toProgActionInput exprDef exprDefName (Just (BodyNode, id)) o a + then Right $ toProgActionInput exprDef (Selection exprDefName $ Just $ NodeSelection BodyNode id) o a else Left $ OptionNotOffered o os.opts else pure $ Left $ ActionNotOffered (Available.Input a) offered action'' <- for action' $ \case From 6b9606d5a239d7a50421ba3ca156246484c9d0ce Mon Sep 17 00:00:00 2001 From: George Thomas Date: Sun, 23 Apr 2023 23:18:30 +0100 Subject: [PATCH 08/32] feat: Add canonical names to prim type def parameters This will make it easier to output typedefs in the API, due to increased uniformity with AST typedefs. Note that these names aren't even currently used anywhere since we don't actually have any higher-kinded primitives, only ints and chars. These would be used if we added, for example, `IO` or `Array` primitives, in which case the names would be likely useful at least for _displaying_ primitive typedefs, even though they don't actually scope over anything like they do for ASTs. Signed-off-by: George Thomas --- primer/src/Primer/TypeDef.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/primer/src/Primer/TypeDef.hs b/primer/src/Primer/TypeDef.hs index 8c8c123eb..d1c04fb8f 100644 --- a/primer/src/Primer/TypeDef.hs +++ b/primer/src/Primer/TypeDef.hs @@ -54,7 +54,7 @@ type TypeDefMap = Map TyConName (TypeDef ()) -- | Definition of a primitive data type data PrimTypeDef = PrimTypeDef - { primTypeDefParameters :: [Kind] + { primTypeDefParameters :: [(TyVarName, Kind)] , primTypeDefNameHints :: [Name] } deriving stock (Eq, Show, Read, Data, Generic) @@ -94,16 +94,16 @@ typeDefNameHints :: TypeDef b -> [Name] typeDefNameHints = \case TypeDefPrim t -> primTypeDefNameHints t TypeDefAST t -> astTypeDefNameHints t -typeDefParameters :: TypeDef b -> [Kind] +typeDefParameters :: TypeDef b -> [(TyVarName, Kind)] typeDefParameters = \case TypeDefPrim t -> primTypeDefParameters t - TypeDefAST t -> snd <$> astTypeDefParameters t + TypeDefAST t -> astTypeDefParameters t typeDefAST :: TypeDef b -> Maybe (ASTTypeDef b) typeDefAST = \case TypeDefPrim _ -> Nothing TypeDefAST t -> Just t typeDefKind :: TypeDef b -> Kind -typeDefKind = foldr KFun KType . typeDefParameters +typeDefKind = foldr (KFun . snd) KType . typeDefParameters -- | A traversal over the contstructor fields in an typedef. _typedefFields :: Traversal (TypeDef b) (TypeDef c) (Type' b) (Type' c) From dd4c4a5f0cd078681d851e420abe2d82cffa63b2 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Mon, 24 Apr 2023 00:09:04 +0100 Subject: [PATCH 09/32] feat!: Output typedefs in API modules Signed-off-by: George Thomas --- primer-service/src/Primer/OpenAPI.hs | 6 +++ primer-service/test/Tests/OpenAPI.hs | 17 ++++++- .../test/outputs/OpenAPI/openapi.json | 51 ++++++++++++++++++- primer/src/Primer/API.hs | 49 ++++++++++++++++-- primer/src/Primer/Module.hs | 6 ++- 5 files changed, 121 insertions(+), 8 deletions(-) diff --git a/primer-service/src/Primer/OpenAPI.hs b/primer-service/src/Primer/OpenAPI.hs index 8417c5fa2..ce4028e6c 100644 --- a/primer-service/src/Primer/OpenAPI.hs +++ b/primer-service/src/Primer/OpenAPI.hs @@ -52,6 +52,8 @@ import Primer.API ( Prog, Selection, Tree, + TypeDef, + ValCon, ) import Primer.API qualified as API import Primer.API.NodeFlavor ( @@ -71,6 +73,7 @@ import Primer.Core ( LVarName, ModuleName, PrimCon, + TyVarName, ) import Primer.Database ( LastModified, @@ -141,6 +144,7 @@ deriving via GlobalName 'ADefName instance ToSchema (GlobalName 'ATyCon) deriving via GlobalName 'ADefName instance ToSchema (GlobalName 'AValCon) deriving via Name instance (ToSchema LVarName) +deriving via Name instance (ToSchema TyVarName) deriving via PrimerJSON (RecordPair a b) instance (ToSchema a, ToSchema b) => ToSchema (RecordPair a b) deriving via PrimerJSON Tree instance ToSchema Tree deriving via PrimerJSON API.Name instance ToSchema API.Name @@ -150,6 +154,8 @@ deriving via PrimerJSON NodeFlavorTextBody instance ToSchema NodeFlavorTextBody deriving via PrimerJSON NodeFlavorPrimBody instance ToSchema NodeFlavorPrimBody deriving via PrimerJSON NodeFlavorBoxBody instance ToSchema NodeFlavorBoxBody deriving via PrimerJSON NodeFlavorNoBody instance ToSchema NodeFlavorNoBody +deriving via PrimerJSON TypeDef instance ToSchema TypeDef +deriving via PrimerJSON ValCon instance ToSchema ValCon deriving via PrimerJSON Def instance ToSchema Def deriving via NonEmpty Name instance ToSchema ModuleName deriving via PrimerJSON Module instance ToSchema Module diff --git a/primer-service/test/Tests/OpenAPI.hs b/primer-service/test/Tests/OpenAPI.hs index 3ea78addc..ce0ac6c00 100644 --- a/primer-service/test/Tests/OpenAPI.hs +++ b/primer-service/test/Tests/OpenAPI.hs @@ -33,6 +33,8 @@ import Primer.API ( Prog (Prog), Selection, Tree, + TypeDef (..), + ValCon (..), viewTreeExpr, viewTreeType, ) @@ -63,6 +65,7 @@ import Primer.Gen.Core.Raw ( genModuleName, genName, genTyConName, + genTyVarName, genType, genValConName, ) @@ -206,6 +209,18 @@ tasty_NodeFlavorNoBody = testToJSON $ G.enumBounded @_ @NodeFlavorNoBody genDef :: ExprGen Def genDef = Def <$> genGVarName <*> genExprTree <*> G.maybe genTypeTree +genTypeDef :: ExprGen TypeDef +genTypeDef = + TypeDef + <$> genTyConName + <*> G.list (R.linear 0 3) genTyVarName + <*> G.list (R.linear 0 3) genName + <*> G.maybe + ( G.list + (R.linear 0 3) + (ValCon <$> genValConName <*> G.list (R.linear 0 3) genTypeTree) + ) + tasty_Def :: Property tasty_Def = testToJSON $ evalExprGen 0 genDef @@ -214,7 +229,7 @@ genModule = Module <$> genModuleName <*> G.bool - <*> G.list (R.linear 0 3) genTyConName + <*> G.list (R.linear 0 3) genTypeDef <*> G.list (R.linear 0 3) genDef tasty_Module :: Property diff --git a/primer-service/test/outputs/OpenAPI/openapi.json b/primer-service/test/outputs/OpenAPI/openapi.json index e9f401427..0ba620e7b 100644 --- a/primer-service/test/outputs/OpenAPI/openapi.json +++ b/primer-service/test/outputs/OpenAPI/openapi.json @@ -224,7 +224,7 @@ }, "types": { "items": { - "$ref": "#/components/schemas/GlobalName" + "$ref": "#/components/schemas/TypeDef" }, "type": "array" } @@ -716,10 +716,59 @@ ], "type": "object" }, + "TypeDef": { + "properties": { + "constructors": { + "items": { + "$ref": "#/components/schemas/ValCon" + }, + "type": "array" + }, + "name": { + "$ref": "#/components/schemas/GlobalName" + }, + "nameHints": { + "items": { + "type": "string" + }, + "type": "array" + }, + "params": { + "items": { + "type": "string" + }, + "type": "array" + } + }, + "required": [ + "name", + "params", + "nameHints" + ], + "type": "object" + }, "UUID": { "example": "00000000-0000-0000-0000-000000000000", "format": "uuid", "type": "string" + }, + "ValCon": { + "properties": { + "fields": { + "items": { + "$ref": "#/components/schemas/Tree" + }, + "type": "array" + }, + "name": { + "$ref": "#/components/schemas/GlobalName" + } + }, + "required": [ + "name", + "fields" + ], + "type": "object" } } }, diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index 808dc1deb..bac2c5643 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -36,6 +36,8 @@ module Primer.API ( viewProg, Prog (Prog), Module (Module), + TypeDef (TypeDef), + ValCon (ValCon), Def (Def), getProgram, getProgram', @@ -207,10 +209,11 @@ import Primer.Log ( PureLog, runPureLog, ) -import Primer.Module (moduleDefsQualified, moduleName, moduleTypesQualified) +import Primer.Module (moduleDefsQualified, moduleName, moduleTypesQualifiedMeta) import Primer.Name qualified as Name import Primer.Primitives (primDefType) -import Primer.TypeDef (ASTTypeDef (ASTTypeDef), ValCon (ValCon)) +import Primer.TypeDef (ASTTypeDef (ASTTypeDef), astTypeDefConstructors, typeDefNameHints, typeDefParameters) +import Primer.TypeDef qualified as TypeDef import StmContainers.Map qualified as StmMap -- | The API environment. @@ -622,7 +625,7 @@ data Prog = Prog data Module = Module { modname :: ModuleName , editable :: Bool - , types :: [TyConName] + , types :: [TypeDef] , -- We don't use Map Name Def as it is rather redundant since each -- Def carries a name field, and it is difficult to enforce that -- "the keys of this object match the name field of the @@ -633,6 +636,25 @@ data Module = Module deriving (ToJSON, FromJSON) via PrimerJSON Module deriving anyclass (NFData) +data TypeDef = TypeDef + { name :: TyConName + , params :: [TyVarName] + , nameHints :: [Name.Name] + , constructors :: Maybe [ValCon] + -- ^ a `Nothing` here indicates a primitive type (whereas `Just []` is `Void`) + } + deriving stock (Generic, Show, Read) + deriving (ToJSON, FromJSON) via PrimerJSON TypeDef + deriving anyclass (NFData) + +data ValCon = ValCon + { name :: ValConName + , fields :: [Tree] + } + deriving stock (Generic, Show, Read) + deriving (ToJSON, FromJSON) via PrimerJSON ValCon + deriving anyclass (NFData) + -- | This type is the api's view of a 'Primer.Core.Def' -- (this is expected to evolve as we flesh out the API) data Def = Def @@ -658,7 +680,24 @@ viewProg p = Module { modname = moduleName m , editable = e - , types = fst <$> Map.assocs (moduleTypesQualified m) + , types = + ( \(name, d) -> + TypeDef + { name + , params = fst <$> typeDefParameters d + , nameHints = typeDefNameHints d + , constructors = case d of + TypeDef.TypeDefPrim _ -> Nothing + TypeDef.TypeDefAST t -> + Just $ + astTypeDefConstructors t <&> \(TypeDef.ValCon nameCon argsCon) -> + ValCon + { name = nameCon + , fields = viewTreeType' . over _typeMeta (show . view _id) <$> argsCon + } + } + ) + <$> Map.assocs (moduleTypesQualifiedMeta m) , defs = ( \(name, d) -> Def @@ -1018,7 +1057,7 @@ createTypeDef :: createTypeDef = curry3 $ logAPI (noError CreateTypeDef) \(sid, tyconName, valcons) -> - edit sid (App.Edit [App.AddTypeDef tyconName $ ASTTypeDef [] (map (`ValCon` []) valcons) []]) + edit sid (App.Edit [App.AddTypeDef tyconName $ ASTTypeDef [] (map (`TypeDef.ValCon` []) valcons) []]) >>= either (throwM . AddTypeDefError tyconName valcons) (pure . viewProg) availableActions :: diff --git a/primer/src/Primer/Module.hs b/primer/src/Primer/Module.hs index 35213bd2f..2f31cc452 100644 --- a/primer/src/Primer/Module.hs +++ b/primer/src/Primer/Module.hs @@ -2,6 +2,7 @@ module Primer.Module ( Module (..), qualifyTyConName, moduleTypesQualified, + moduleTypesQualifiedMeta, qualifyDefName, moduleDefsQualified, insertDef, @@ -77,7 +78,10 @@ qualifyTyConName :: Module -> Name -> TyConName qualifyTyConName m = qualifyName (moduleName m) moduleTypesQualified :: Module -> TypeDefMap -moduleTypesQualified m = mapKeys (qualifyTyConName m) $ forgetTypeDefMetadata <$> moduleTypes m +moduleTypesQualified = map forgetTypeDefMetadata . moduleTypesQualifiedMeta + +moduleTypesQualifiedMeta :: Module -> Map TyConName (TypeDef TypeMeta) +moduleTypesQualifiedMeta m = mapKeys (qualifyTyConName m) $ moduleTypes m qualifyDefName :: Module -> Name -> GVarName qualifyDefName m = qualifyName (moduleName m) From b1c22505a621e5662c5cba1c53507d91bf31c5e5 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Wed, 26 Apr 2023 18:17:33 +0100 Subject: [PATCH 10/32] feat: Expose available actions for typedefs Note that no new unit tests are added. This is because the underlying `ProgAction`s are already well-tested, e.g. in `unit_RenameType`. In due course, the property test `tasty_available_actions_accepted` will be generalised to cover typedef actions, which will therefore check that all of these new actions can be applied without error whenever they are available. We don't yet expose actions for constructor fields (i.e. `Available.forTypeDefConsFieldNode` always returns `[]`), since making this work will, unlike the other positions, require changes to the core of the library. We _could_ actually make all the `for*`s part of one definition, now that `Selection` is in `App.Base`. But we do actually use the individual functions in some tests, and with them separate, we have slightly more control, in that we don't need to provide as much context. Note that most of the changes in this commit are actually knock-on effects of generalising `Selection` to cover type defs. Signed-off-by: George Thomas --- primer-service/exe-server/Main.hs | 2 + primer-service/src/Primer/OpenAPI.hs | 9 +- primer-service/src/Primer/Server.hs | 2 + primer-service/test/Tests/OpenAPI.hs | 36 +++- .../test/outputs/OpenAPI/openapi.json | 162 ++++++++++++++++-- primer/src/Primer/API.hs | 53 ++++-- primer/src/Primer/Action.hs | 115 +++++++++++-- primer/src/Primer/Action/Available.hs | 85 ++++++++- primer/src/Primer/Action/Errors.hs | 10 +- primer/src/Primer/Action/Priorities.hs | 10 ++ primer/src/Primer/App.hs | 70 ++++++-- primer/src/Primer/App/Base.hs | 65 ++++++- primer/test/Tests/Action/Available.hs | 23 +-- primer/test/Tests/Action/Prog.hs | 17 +- primer/test/Tests/Serialization.hs | 14 +- primer/test/Tests/Typecheck.hs | 20 ++- .../serialization/edit_response_2.json | 43 ++--- primer/test/outputs/serialization/prog.json | 43 ++--- .../test/outputs/serialization/selection.json | 43 ++--- 19 files changed, 662 insertions(+), 160 deletions(-) diff --git a/primer-service/exe-server/Main.hs b/primer-service/exe-server/Main.hs index d5410f85a..81c26f213 100644 --- a/primer-service/exe-server/Main.hs +++ b/primer-service/exe-server/Main.hs @@ -344,7 +344,9 @@ instance ConvertLogMessage SomeException LogMsg where instance ConvertLogMessage PrimerErr LogMsg where convert (DatabaseErr e) = LogMsg e convert (UnknownDef e) = LogMsg $ show e + convert (UnknownTypeDef e) = LogMsg $ show e convert (UnexpectedPrimDef e) = LogMsg $ show e + convert (UnexpectedPrimTypeDef e) = LogMsg $ show e convert (AddDefError m n e) = LogMsg $ show (m, n, e) convert (AddTypeDefError tc vcs e) = LogMsg $ show (tc, vcs, e) convert (ActionOptionsNoID e) = LogMsg $ show e diff --git a/primer-service/src/Primer/OpenAPI.hs b/primer-service/src/Primer/OpenAPI.hs index ce4028e6c..39f9bc2ff 100644 --- a/primer-service/src/Primer/OpenAPI.hs +++ b/primer-service/src/Primer/OpenAPI.hs @@ -64,8 +64,8 @@ import Primer.API.NodeFlavor ( ) import Primer.API.RecordPair (RecordPair) import Primer.Action.Available qualified as Available -import Primer.App (NodeSelection, NodeType) -import Primer.App.Base (Level) +import Primer.App (DefSelection, NodeSelection, NodeType, TypeDefSelection) +import Primer.App.Base (Level, TypeDefConsFieldSelection (..), TypeDefConsSelection (..), TypeDefNodeSelection) import Primer.Core ( GlobalName, GlobalNameKind (ADefName, ATyCon, AValCon), @@ -168,6 +168,11 @@ deriving via PrimerJSON Available.Options instance ToSchema Available.Options deriving via PrimerJSON Available.Action instance ToSchema Available.Action deriving via PrimerJSON ApplyActionBody instance ToSchema ApplyActionBody deriving via PrimerJSONNamed "Selection" Selection instance ToSchema Selection +deriving via PrimerJSONNamed "TypeDefSelection" (TypeDefSelection ID) instance ToSchema (TypeDefSelection ID) +deriving via PrimerJSONNamed "TypeDefNodeSelection" (TypeDefNodeSelection ID) instance ToSchema (TypeDefNodeSelection ID) +deriving via PrimerJSONNamed "TypeDefConsSelection" (TypeDefConsSelection ID) instance ToSchema (TypeDefConsSelection ID) +deriving via PrimerJSONNamed "TypeDefConsFieldSelection" (TypeDefConsFieldSelection ID) instance ToSchema (TypeDefConsFieldSelection ID) +deriving via PrimerJSONNamed "DefSelection" (DefSelection ID) instance ToSchema (DefSelection ID) deriving via PrimerJSONNamed "NodeSelection" (NodeSelection ID) instance ToSchema (NodeSelection ID) deriving via PrimerJSON NodeType instance ToSchema NodeType deriving via PrimerJSON Level instance ToSchema Level diff --git a/primer-service/src/Primer/Server.hs b/primer-service/src/Primer/Server.hs index 88096a9e4..7372457cb 100644 --- a/primer-service/src/Primer/Server.hs +++ b/primer-service/src/Primer/Server.hs @@ -343,6 +343,8 @@ serve ss q v port logger = do DatabaseErr msg -> err500{errBody = encode msg} UnknownDef d -> err404{errBody = "Unknown definition: " <> encode (globalNamePretty d)} UnexpectedPrimDef d -> err400{errBody = "Unexpected primitive definition: " <> encode (globalNamePretty d)} + UnknownTypeDef d -> err404{errBody = "Unknown type definition: " <> encode (globalNamePretty d)} + UnexpectedPrimTypeDef d -> err400{errBody = "Unexpected primitive type definition: " <> encode (globalNamePretty d)} AddDefError m md pe -> err400{errBody = "Error while adding definition (" <> s <> "): " <> show pe} where s = encode $ case md of diff --git a/primer-service/test/Tests/OpenAPI.hs b/primer-service/test/Tests/OpenAPI.hs index ce0ac6c00..80a639f25 100644 --- a/primer-service/test/Tests/OpenAPI.hs +++ b/primer-service/test/Tests/OpenAPI.hs @@ -46,7 +46,17 @@ import Primer.API.NodeFlavor ( ) import Primer.API.RecordPair (RecordPair (RecordPair)) import Primer.Action.Available qualified as Available -import Primer.App (Level, NodeSelection (NodeSelection), NodeType, Selection' (Selection)) +import Primer.App ( + DefSelection (..), + Level, + NodeSelection (..), + NodeType, + Selection' (..), + TypeDefConsFieldSelection (TypeDefConsFieldSelection), + TypeDefConsSelection (..), + TypeDefSelection (..), + ) +import Primer.App.Base (TypeDefNodeSelection (..)) import Primer.Core (GVarName, ID (ID), ModuleName, PrimCon (PrimChar, PrimInt)) import Primer.Database ( LastModified (..), @@ -241,8 +251,30 @@ genNodeType = G.enumBounded genNodeSelection :: ExprGen (NodeSelection ID) genNodeSelection = NodeSelection <$> genNodeType <*> genID +genDefSelection :: ExprGen (DefSelection ID) +genDefSelection = DefSelection <$> genGVarName <*> G.maybe genNodeSelection + +genTypeDefSelection :: ExprGen (TypeDefSelection ID) +genTypeDefSelection = + TypeDefSelection + <$> genTyConName + <*> G.maybe + ( G.choice + [ TypeDefParamNodeSelection <$> genTyVarName + , TypeDefConsNodeSelection + <$> ( TypeDefConsSelection + <$> genValConName + <*> G.maybe (TypeDefConsFieldSelection <$> G.integral (R.linear 0 3) <*> genID) + ) + ] + ) + genSelection :: ExprGen Selection -genSelection = Selection <$> genGVarName <*> G.maybe genNodeSelection +genSelection = + G.choice + [ SelectionDef <$> genDefSelection + , SelectionTypeDef <$> genTypeDefSelection + ] genProg :: Gen Prog genProg = evalExprGen 0 $ Prog <$> G.list (R.linear 0 3) genModule <*> G.maybe genSelection <*> G.bool <*> G.bool diff --git a/primer-service/test/outputs/OpenAPI/openapi.json b/primer-service/test/outputs/OpenAPI/openapi.json index 0ba620e7b..0f495fba2 100644 --- a/primer-service/test/outputs/OpenAPI/openapi.json +++ b/primer-service/test/outputs/OpenAPI/openapi.json @@ -100,6 +100,20 @@ ], "type": "object" }, + "DefSelection": { + "properties": { + "def": { + "$ref": "#/components/schemas/GlobalName" + }, + "node": { + "$ref": "#/components/schemas/NodeSelection" + } + }, + "required": [ + "def" + ], + "type": "object" + }, "EvalFullResp": { "oneOf": [ { @@ -187,7 +201,11 @@ "MakeTVar", "MakeForall", "RenameForall", - "RenameDef" + "RenameDef", + "RenameType", + "RenameCon", + "RenameTypeParam", + "AddCon" ], "type": "string" }, @@ -284,7 +302,8 @@ "RaiseType", "DeleteType", "DuplicateDef", - "DeleteDef" + "DeleteDef", + "AddConField" ], "type": "string" }, @@ -656,18 +675,44 @@ "type": "object" }, "Selection": { - "properties": { - "def": { - "$ref": "#/components/schemas/GlobalName" + "oneOf": [ + { + "properties": { + "contents": { + "$ref": "#/components/schemas/DefSelection" + }, + "tag": { + "enum": [ + "SelectionDef" + ], + "type": "string" + } + }, + "required": [ + "tag", + "contents" + ], + "type": "object" }, - "node": { - "$ref": "#/components/schemas/NodeSelection" + { + "properties": { + "contents": { + "$ref": "#/components/schemas/TypeDefSelection" + }, + "tag": { + "enum": [ + "SelectionTypeDef" + ], + "type": "string" + } + }, + "required": [ + "tag", + "contents" + ], + "type": "object" } - }, - "required": [ - "def" - ], - "type": "object" + ] }, "Session": { "properties": { @@ -747,6 +792,93 @@ ], "type": "object" }, + "TypeDefConsFieldSelection": { + "properties": { + "index": { + "maximum": 9223372036854775807, + "minimum": -9223372036854775808, + "type": "integer" + }, + "meta": { + "maximum": 9223372036854775807, + "minimum": -9223372036854775808, + "type": "integer" + } + }, + "required": [ + "index", + "meta" + ], + "type": "object" + }, + "TypeDefConsSelection": { + "properties": { + "con": { + "$ref": "#/components/schemas/GlobalName" + }, + "field": { + "$ref": "#/components/schemas/TypeDefConsFieldSelection" + } + }, + "required": [ + "con" + ], + "type": "object" + }, + "TypeDefNodeSelection": { + "oneOf": [ + { + "properties": { + "contents": { + "type": "string" + }, + "tag": { + "enum": [ + "TypeDefParamNodeSelection" + ], + "type": "string" + } + }, + "required": [ + "tag", + "contents" + ], + "type": "object" + }, + { + "properties": { + "contents": { + "$ref": "#/components/schemas/TypeDefConsSelection" + }, + "tag": { + "enum": [ + "TypeDefConsNodeSelection" + ], + "type": "string" + } + }, + "required": [ + "tag", + "contents" + ], + "type": "object" + } + ] + }, + "TypeDefSelection": { + "properties": { + "def": { + "$ref": "#/components/schemas/GlobalName" + }, + "node": { + "$ref": "#/components/schemas/TypeDefNodeSelection" + } + }, + "required": [ + "def" + ], + "type": "object" + }, "UUID": { "example": "00000000-0000-0000-0000-000000000000", "format": "uuid", @@ -1128,7 +1260,11 @@ "MakeTVar", "MakeForall", "RenameForall", - "RenameDef" + "RenameDef", + "RenameType", + "RenameCon", + "RenameTypeParam", + "AddCon" ], "type": "string" } diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index bac2c5643..22fe15aad 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -102,6 +102,7 @@ import Primer.Action (ActionError, ProgAction, toProgActionInput, toProgActionNo import Primer.Action.Available qualified as Available import Primer.App ( App, + DefSelection (..), EditAppM, Editable, EvalFullReq (..), @@ -109,10 +110,14 @@ import Primer.App ( EvalResp (..), Level, MutationRequest, + NodeSelection (..), NodeType (..), ProgError, QueryAppM, Question (GenerateName), + Selection' (..), + TypeDefConsSelection (..), + TypeDefSelection (..), appProg, handleEvalFullRequest, handleEvalRequest, @@ -133,6 +138,7 @@ import Primer.App ( unlog, ) import Primer.App qualified as App +import Primer.App.Base (TypeDefNodeSelection (..)) import Primer.Core ( Bind' (..), CaseBranch' (..), @@ -212,7 +218,7 @@ import Primer.Log ( import Primer.Module (moduleDefsQualified, moduleName, moduleTypesQualifiedMeta) import Primer.Name qualified as Name import Primer.Primitives (primDefType) -import Primer.TypeDef (ASTTypeDef (ASTTypeDef), astTypeDefConstructors, typeDefNameHints, typeDefParameters) +import Primer.TypeDef (ASTTypeDef (..), typeDefNameHints, typeDefParameters) import Primer.TypeDef qualified as TypeDef import StmContainers.Map qualified as StmMap @@ -255,7 +261,9 @@ runPrimerM = runReaderT . unPrimerM data PrimerErr = DatabaseErr Text | UnknownDef GVarName + | UnknownTypeDef TyConName | UnexpectedPrimDef GVarName + | UnexpectedPrimTypeDef TyConName | AddDefError ModuleName (Maybe Text) ProgError | AddTypeDefError TyConName [ValConName] ProgError | ActionOptionsNoID Selection @@ -1070,14 +1078,22 @@ availableActions = curry3 $ logAPI (noError AvailableActions) $ \(sid, level, se prog <- getProgram sid let allDefs = progAllDefs prog allTypeDefs = progAllTypeDefs prog - (editable, ASTDef{astDefType = type_, astDefExpr = expr}) <- findASTDef allDefs selection.def - case selection.node of - Nothing -> - pure $ Available.forDef (snd <$> allDefs) level editable selection.def - Just App.NodeSelection{..} -> do - pure $ case nodeType of - SigNode -> Available.forSig level editable type_ meta - BodyNode -> Available.forBody (snd <$> allTypeDefs) level editable expr meta + case selection of + SelectionDef sel -> do + (editable, ASTDef{astDefType = type_, astDefExpr = expr}) <- findASTDef allDefs sel.def + pure $ case sel.node of + Nothing -> Available.forDef (snd <$> allDefs) level editable sel.def + Just NodeSelection{..} -> case nodeType of + SigNode -> Available.forSig level editable type_ meta + BodyNode -> Available.forBody (snd <$> allTypeDefs) level editable expr meta + SelectionTypeDef sel -> do + (editable, _def) <- findASTTypeDef allTypeDefs sel.def + pure $ case sel.node of + Nothing -> Available.forTypeDef level editable + Just (TypeDefParamNodeSelection _) -> Available.forTypeDefParamNode level editable + Just (TypeDefConsNodeSelection s) -> case s.field of + Nothing -> Available.forTypeDefConsNode level editable + Just _ -> Available.forTypeDefConsFieldNode level editable actionOptions :: (MonadIO m, MonadThrow m, MonadAPILog l m) => @@ -1091,7 +1107,7 @@ actionOptions = curry4 $ logAPI (noError ActionOptions) $ \(sid, level, selectio let prog = appProg app allDefs = progAllDefs prog allTypeDefs = progAllTypeDefs prog - def <- snd <$> findASTDef allDefs selection.def + def <- snd <$> findASTTypeOrTermDef prog selection maybe (throwM $ ActionOptionsNoID selection) pure $ Available.options (snd <$> allTypeDefs) (snd <$> allDefs) (progCxt prog) level def selection action @@ -1101,6 +1117,19 @@ findASTDef allDefs def = case allDefs Map.!? def of Just (_, Def.DefPrim _) -> throwM $ UnexpectedPrimDef def Just (editable, Def.DefAST d) -> pure (editable, d) +findASTTypeDef :: MonadThrow m => Map TyConName (Editable, TypeDef.TypeDef ()) -> TyConName -> m (Editable, ASTTypeDef ()) +findASTTypeDef allTypeDefs def = case allTypeDefs Map.!? def of + Nothing -> throwM $ UnknownTypeDef def + Just (_, TypeDef.TypeDefPrim _) -> throwM $ UnexpectedPrimTypeDef def + Just (editable, TypeDef.TypeDefAST d) -> pure (editable, d) + +findASTTypeOrTermDef :: MonadThrow f => App.Prog -> Selection' a -> f (Editable, Either (ASTTypeDef ()) ASTDef) +findASTTypeOrTermDef prog = \case + App.SelectionTypeDef sel -> + Left <<$>> findASTTypeDef (progAllTypeDefs prog) sel.def + App.SelectionDef sel -> + Right <<$>> findASTDef (progAllDefs prog) sel.def + applyActionNoInput :: (MonadIO m, MonadThrow m, MonadAPILog l m) => SessionId -> @@ -1109,7 +1138,7 @@ applyActionNoInput :: PrimerM m Prog applyActionNoInput = curry3 $ logAPI (noError ApplyActionNoInput) $ \(sid, selection, action) -> do prog <- getProgram sid - def <- snd <$> findASTDef (progAllDefs prog) selection.def + def <- snd <$> findASTTypeOrTermDef prog selection actions <- either (throwM . ToProgActionError (Available.NoInput action)) pure $ toProgActionNoInput (snd <$> progAllDefs prog) def selection action @@ -1123,7 +1152,7 @@ applyActionInput :: PrimerM m Prog applyActionInput = curry3 $ logAPI (noError ApplyActionInput) $ \(sid, body, action) -> do prog <- getProgram sid - def <- snd <$> findASTDef (progAllDefs prog) body.selection.def + def <- snd <$> findASTTypeOrTermDef prog body.selection actions <- either (throwM . ToProgActionError (Available.Input action)) pure $ toProgActionInput def body.selection body.option action diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index e968efd8c..c397a4bed 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -35,7 +35,15 @@ import Primer.Action.Actions (Action (..), Movement (..), QualifiedText) import Primer.Action.Available qualified as Available import Primer.Action.Errors (ActionError (..)) import Primer.Action.ProgAction (ProgAction (..)) -import Primer.App.Base (NodeSelection (..), NodeType (..), Selection' (..)) +import Primer.App.Base ( + DefSelection (..), + NodeSelection (..), + NodeType (..), + Selection' (..), + TypeDefConsSelection (..), + TypeDefNodeSelection (..), + TypeDefSelection (..), + ) import Primer.Core ( Expr, Expr' (..), @@ -858,11 +866,11 @@ renameForall b zt = case target zt of -- | Convert a high-level 'Available.NoInputAction' to a concrete sequence of 'ProgAction's. toProgActionNoInput :: DefMap -> - ASTDef -> + Either (ASTTypeDef ()) ASTDef -> Selection' ID -> Available.NoInputAction -> Either ActionError [ProgAction] -toProgActionNoInput defs def sel = \case +toProgActionNoInput defs def0 sel0 = \case Available.MakeCase -> toProgAction [ConstructCase] Available.MakeApp -> @@ -876,7 +884,8 @@ toProgActionNoInput defs def sel = \case Available.LetToRec -> toProgAction [ConvertLetToLetrec] Available.Raise -> do - id <- mid + id <- nodeID + sel <- termSel pure [MoveToDef sel.def, CopyPasteBody (sel.def, id) [SetCursor id, Move Parent, Delete]] Available.EnterHole -> toProgAction [EnterHole] @@ -893,7 +902,8 @@ toProgActionNoInput defs def sel = \case -- resulting in a new argument type. The result type is unchanged. -- The cursor location is also unchanged. -- e.g. A -> B -> C ==> A -> B -> ? -> C - id <- mid + id <- nodeID + def <- termDef type_ <- case findType id $ astDefType def of Just t -> pure t Nothing -> case map fst $ findNodeWithParent id $ astDefExpr def of @@ -909,11 +919,14 @@ toProgActionNoInput defs def sel = \case Available.MakeTApp -> toProgAction [ConstructTApp, Move Child1] Available.RaiseType -> do - id <- mid + id <- nodeID + sel <- termSel pure [MoveToDef sel.def, CopyPasteSig (sel.def, id) [SetCursor id, Move Parent, Delete]] Available.DeleteType -> toProgAction [Delete] - Available.DuplicateDef -> + Available.DuplicateDef -> do + sel <- termSel + def <- termDef let sigID = getID $ astDefType def bodyID = getID $ astDefExpr def copyName = uniquifyDefName (qualifiedModule sel.def) (unName (baseName sel.def) <> "Copy") defs @@ -922,21 +935,50 @@ toProgActionNoInput defs def sel = \case , CopyPasteSig (sel.def, sigID) [] , CopyPasteBody (sel.def, bodyID) [] ] - Available.DeleteDef -> + Available.DeleteDef -> do + sel <- termSel pure [DeleteDef sel.def] + Available.AddConField -> do + (defName, sel) <- conSel + d <- typeDef + vc <- + maybe (Left $ ValConNotFound defName sel.con) pure + . find ((== sel.con) . valConName) + $ astTypeDefConstructors d + let index = length $ valConArgs vc -- for now, we always add on to the end + pure [AddConField defName sel.con index $ TEmptyHole ()] where - toProgAction actions = toProg' actions sel.def <$> maybeToEither NoNodeSelection sel.node - mid = maybeToEither NoNodeSelection $ (.meta) <$> sel.node + termSel = case sel0 of + SelectionDef s -> pure s + SelectionTypeDef _ -> Left NeedTermDefSelection + nodeID = do + sel <- termSel + maybeToEither NoNodeSelection $ (.meta) <$> sel.node + typeSel = case sel0 of + SelectionDef _ -> Left NeedTypeDefSelection + SelectionTypeDef s -> pure s + typeNodeSel = do + sel <- typeSel + maybe (Left NeedTypeDefNodeSelection) (pure . (sel.def,)) sel.node + conSel = + typeNodeSel >>= \case + (s0, TypeDefConsNodeSelection s) -> pure (s0, s) + _ -> Left NeedTypeDefConsSelection + toProgAction actions = do + sel <- termSel + toProg' actions sel.def <$> maybeToEither NoNodeSelection sel.node + termDef = first (const NeedTermDef) def0 + typeDef = either Right (Left . const NeedTypeDef) def0 -- | Convert a high-level 'Available.InputAction', and associated 'Available.Option', -- to a concrete sequence of 'ProgAction's. toProgActionInput :: - ASTDef -> + Either (ASTTypeDef ()) ASTDef -> Selection' ID -> Available.Option -> Available.InputAction -> Either ActionError [ProgAction] -toProgActionInput def sel opt0 = \case +toProgActionInput def0 sel0 opt0 = \case Available.MakeCon -> do opt <- optGlobal toProg [ConstructSaturatedCon opt] @@ -992,9 +1034,49 @@ toProgActionInput def sel opt0 = \case toProg [RenameForall opt] Available.RenameDef -> do opt <- optNoCxt + sel <- termSel pure [RenameDef sel.def opt] + Available.RenameType -> do + opt <- optNoCxt + td <- typeSel + pure [RenameType td.def opt] + Available.RenameCon -> do + opt <- optNoCxt + (defName, sel) <- conSel + pure [RenameCon defName sel.con opt] + Available.RenameTypeParam -> do + opt <- optNoCxt + (defName, sel) <- typeParamSel + pure [RenameTypeParam defName sel opt] + Available.AddCon -> do + opt <- optNoCxt + sel <- typeSel + d <- typeDef + let index = length $ astTypeDefConstructors d -- for now, we always add on the end + pure [AddCon sel.def index opt] where - mid = maybeToEither NoNodeSelection $ (.meta) <$> sel.node + termSel = case sel0 of + SelectionDef s -> pure s + SelectionTypeDef _ -> Left NeedTermDefSelection + nodeID = do + sel <- termSel + maybeToEither NoNodeSelection $ (.meta) <$> sel.node + typeSel = case sel0 of + SelectionDef _ -> Left NeedTypeDefSelection + SelectionTypeDef s -> pure s + typeNodeSel = do + sel <- typeSel + maybe (Left NeedTypeDefNodeSelection) (pure . (sel.def,)) sel.node + typeParamSel = + typeNodeSel >>= \case + (s0, TypeDefParamNodeSelection s) -> pure (s0, s) + _ -> Left NeedTypeDefParamSelection + conSel = + typeNodeSel >>= \case + (s0, TypeDefConsNodeSelection s) -> pure (s0, s) + _ -> Left NeedTypeDefConsSelection + termDef = first (const NeedTermDef) def0 + typeDef = either Right (Left . const NeedTypeDef) def0 optVar = case opt0.context of Just q -> GlobalVarRef $ unsafeMkGlobalName (q, opt0.option) Nothing -> LocalVarRef $ unsafeMkLocalName opt0.option @@ -1007,9 +1089,12 @@ toProgActionInput def sel opt0 = \case optGlobal = case opt0.context of Nothing -> Left $ NeedLocal opt0 Just q -> pure (q, opt0.option) - toProg actions = toProg' actions sel.def <$> maybeToEither NoNodeSelection sel.node + toProg actions = do + sel <- termSel + toProg' actions sel.def <$> maybeToEither NoNodeSelection sel.node offerRefined = do - id <- mid + id <- nodeID + def <- termDef -- If we have a useful type, offer the refine action, otherwise offer the saturate action. case findNodeWithParent id $ astDefExpr def of Just (ExprNode e, _) -> pure $ case e ^. _exprMetaLens ^? _type % _Just % _chkedAt of diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs index 74a97c481..cbc6b9613 100644 --- a/primer/src/Primer/Action/Available.hs +++ b/primer/src/Primer/Action/Available.hs @@ -15,10 +15,15 @@ module Primer.Action.Available ( FreeInput (..), Options (..), options, + forTypeDef, + forTypeDefParamNode, + forTypeDefConsNode, + forTypeDefConsFieldNode, ) where import Foreword +import Data.Either.Extra (eitherToMaybe) import Data.Map qualified as Map import Data.Set qualified as Set import Data.Tuple.Extra (fst3) @@ -32,6 +37,7 @@ import Optics ( ) import Primer.Action.Priorities qualified as P import Primer.App.Base ( + DefSelection (..), Editable (..), Level (..), NodeSelection (..), @@ -120,6 +126,7 @@ data NoInputAction | DeleteType | DuplicateDef | DeleteDef + | AddConField deriving stock (Eq, Ord, Show, Read, Enum, Bounded, Generic) deriving (ToJSON, FromJSON) via PrimerJSON NoInputAction @@ -143,6 +150,10 @@ data InputAction | MakeForall | RenameForall | RenameDef + | RenameType + | RenameCon + | RenameTypeParam + | AddCon deriving stock (Eq, Ord, Show, Read, Enum, Bounded, Generic) deriving (ToJSON, FromJSON) via PrimerJSON InputAction @@ -288,6 +299,48 @@ forType l type_ = ] delete = [NoInput DeleteType] +forTypeDef :: + Level -> + Editable -> + [Action] +forTypeDef _ NonEditable = mempty +forTypeDef l Editable = + sortByPriority + l + [ Input RenameType + , Input AddCon + ] + +forTypeDefParamNode :: + Level -> + Editable -> + [Action] +forTypeDefParamNode _ NonEditable = mempty +forTypeDefParamNode l Editable = + sortByPriority + l + [ Input RenameTypeParam + ] + +forTypeDefConsNode :: + Level -> + Editable -> + [Action] +forTypeDefConsNode _ NonEditable = mempty +forTypeDefConsNode l Editable = + sortByPriority + l + [ NoInput AddConField + , Input RenameCon + ] + +forTypeDefConsFieldNode :: + Level -> + Editable -> + [Action] +forTypeDefConsFieldNode _ NonEditable = mempty +forTypeDefConsFieldNode l Editable = sortByPriority l [] + -- | An input for an 'InputAction'. data Option = Option { option :: Text @@ -322,13 +375,13 @@ options :: DefMap -> Cxt -> Level -> - ASTDef -> + Either (ASTTypeDef ()) ASTDef -> Selection' ID -> InputAction -> -- | Returns 'Nothing' if an ID was required but not passed, passed but not found in the tree, -- or found but didn't correspond to the expected sort of entity (type/expr/pattern). Maybe Options -options typeDefs defs cxt level def sel = \case +options typeDefs defs cxt level def0 sel0 = \case MakeCon -> pure . noFree @@ -383,7 +436,18 @@ options typeDefs defs cxt level def sel = \case freeVar <$> genNames (Right $ Just k) RenameDef -> pure $ freeVar [] + RenameType -> + pure $ freeVar [] + RenameCon -> + pure $ freeVar [] + RenameTypeParam -> + pure $ freeVar [] + AddCon -> + pure $ freeVar [] where + defSel = case sel0 of + SelectionDef s -> pure s + SelectionTypeDef _ -> Nothing freeVar opts = Options{opts, free = FreeVarName} noFree opts = Options{opts, free = FreeNone} localOpt = flip Option Nothing . unName @@ -398,23 +462,29 @@ options typeDefs defs cxt level def sel = \case (first (localOpt . unLocalName) <$> locals) <> (first globalOpt <$> globals) findNode = do + sel <- defSel s <- sel.node + def <- eitherToMaybe def0 case s.nodeType of BodyNode -> fst <$> findNodeWithParent s.meta (astDefExpr def) SigNode -> TypeNode <$> findType s.meta (astDefType def) genNames typeOrKind = do + sel <- defSel z <- focusNode =<< sel.node pure $ map localOpt $ flip runReader cxt $ case z of Left zE -> generateNameExpr typeOrKind zE Right zT -> generateNameTy typeOrKind zT varsInScope = do + sel <- defSel nodeSel <- sel.node focusNode nodeSel <&> \case Left zE -> variablesInScopeExpr defs zE Right zT -> (variablesInScopeTy zT, [], []) - focusNode nodeSel = case nodeSel.nodeType of - BodyNode -> Left . locToEither <$> focusOn nodeSel.meta (astDefExpr def) - SigNode -> fmap Right $ focusOnTy nodeSel.meta $ astDefType def + focusNode nodeSel = do + def <- eitherToMaybe def0 + case nodeSel.nodeType of + BodyNode -> Left . locToEither <$> focusOn nodeSel.meta (astDefExpr def) + SigNode -> fmap Right $ focusOnTy nodeSel.meta $ astDefType def -- Extract the source of the function type we were checked at -- i.e. the type that a lambda-bound variable would have here lamVarTy = \case @@ -458,6 +528,7 @@ sortByPriority l = DeleteType -> P.delete DuplicateDef -> P.duplicate DeleteDef -> P.delete + AddConField -> P.addConField Input a -> case a of MakeCon -> P.useSaturatedValueCon MakeInt -> P.makeInt @@ -477,3 +548,7 @@ sortByPriority l = MakeForall -> P.constructForall RenameForall -> P.rename RenameDef -> P.rename + RenameType -> P.rename + AddCon -> P.addCon + RenameCon -> P.rename + RenameTypeParam -> P.rename diff --git a/primer/src/Primer/Action/Errors.hs b/primer/src/Primer/Action/Errors.hs index 9e6d705c4..9a3deb46c 100644 --- a/primer/src/Primer/Action/Errors.hs +++ b/primer/src/Primer/Action/Errors.hs @@ -13,7 +13,7 @@ import Data.Aeson (FromJSON (..), ToJSON (..)) import Primer.Action.Actions (Action) import Primer.Action.Available qualified as Available import Primer.Action.Movement (Movement) -import Primer.Core (Expr, GVarName, ID, LVarName, ModuleName, Type) +import Primer.Core (Expr, GVarName, ID, LVarName, ModuleName, TyConName, Type, ValConName) import Primer.JSON (CustomJSON (..), PrimerJSON) import Primer.Typecheck.TypeError (TypeError) import Primer.Zipper (SomeNode) @@ -63,6 +63,14 @@ data ActionError | NeedLocal Available.Option | NeedInt Available.Option | NeedChar Available.Option + | NeedTermDef + | NeedTypeDef + | NeedTermDefSelection + | NeedTypeDefSelection + | NeedTypeDefNodeSelection + | NeedTypeDefConsSelection + | NeedTypeDefParamSelection | NoNodeSelection + | ValConNotFound TyConName ValConName deriving stock (Eq, Show, Read, Generic) deriving (FromJSON, ToJSON) via PrimerJSON ActionError diff --git a/primer/src/Primer/Action/Priorities.hs b/primer/src/Primer/Action/Priorities.hs index 12d09c847..bbc84293c 100644 --- a/primer/src/Primer/Action/Priorities.hs +++ b/primer/src/Primer/Action/Priorities.hs @@ -55,6 +55,10 @@ module Primer.Action.Priorities ( constructTypeApp, constructForall, + -- * Type def actions. + addCon, + addConField, + -- * Generic actions. rename, duplicate, @@ -146,3 +150,9 @@ raise _ = 300 delete :: Level -> Int delete _ = maxBound + +addCon :: Level -> Int +addCon _ = 10 + +addConField :: Level -> Int +addConField _ = 10 diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 3b8b46e41..2f115b9cd 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE OverloadedLabels #-} {-# LANGUAGE OverloadedRecordDot #-} @@ -78,6 +80,7 @@ import Optics ( ifoldMap, mapped, over, + set, traverseOf, traversed, view, @@ -101,12 +104,17 @@ import Primer.Action ( ) import Primer.Action.ProgError (ProgError (..)) import Primer.App.Base ( + DefSelection (..), Editable (..), Level (..), NodeSelection (..), NodeType (..), Selection, Selection' (..), + TypeDefConsFieldSelection (..), + TypeDefConsSelection (..), + TypeDefNodeSelection (..), + TypeDefSelection (..), ) import Primer.Core ( Bind' (Bind), @@ -160,6 +168,7 @@ import Primer.Module ( insertDef, moduleDefsQualified, moduleTypesQualified, + moduleTypesQualifiedMeta, nextModuleID, primitiveModule, qualifyDefName, @@ -270,6 +279,11 @@ progAllTypeDefs p = foldMap' (fmap (Editable,) . moduleTypesQualified) (progModules p) <> foldMap' (fmap (NonEditable,) . moduleTypesQualified) (progImports p) +progAllTypeDefsMeta :: Prog -> Map TyConName (Editable, TypeDef TypeMeta) +progAllTypeDefsMeta p = + foldMap' (fmap (Editable,) . moduleTypesQualifiedMeta) (progModules p) + <> foldMap' (fmap (NonEditable,) . moduleTypesQualifiedMeta) (progImports p) + progAllDefs :: Prog -> Map GVarName (Editable, Def) progAllDefs p = foldMap' (fmap (Editable,) . moduleDefsQualified) (progModules p) @@ -322,11 +336,12 @@ newEmptyProgImporting imported = ] , progImports = imported' , progSelection = - Just - Selection - { def = qualifyName moduleName defName - , node = Nothing - } + Just $ + SelectionDef + DefSelection + { def = qualifyName moduleName defName + , node = Nothing + } } , nextID , toEnum 0 @@ -393,6 +408,9 @@ importModules ms = do allTypes :: Prog -> TypeDefMap allTypes = fmap snd . progAllTypeDefs +allTypesMeta :: Prog -> Map TyConName (TypeDef TypeMeta) +allTypesMeta = fmap snd . progAllTypeDefsMeta + -- | Get all definitions from all modules (including imports) allDefs :: Prog -> DefMap allDefs = fmap snd . progAllDefs @@ -522,7 +540,8 @@ handleEditRequest actions = do go :: (Prog, Maybe GVarName) -> ProgAction -> m (Prog, Maybe GVarName) go (prog, mdef) a = applyProgAction prog mdef a <&> \prog' -> - (prog', (.def) <$> progSelection prog') + -- TODO this ignores any selection from a type def selection + (prog', (.def) <$> ((\case SelectionDef s -> Just s; _ -> Nothing) =<< progSelection prog')) -- | Handle an eval request (we assume that all such requests are implicitly in a synthesisable context) handleEvalRequest :: @@ -564,7 +583,7 @@ applyProgAction prog mdefName = \case m <- lookupEditableModule (qualifiedModule d) prog case Map.lookup d $ moduleDefsQualified m of Nothing -> throwError $ DefNotFound d - Just _ -> pure $ prog & #progSelection ?~ Selection d Nothing + Just _ -> pure $ prog & #progSelection ?~ SelectionDef (DefSelection d Nothing) DeleteDef d -> editModuleCross (qualifiedModule d) prog $ \(m, ms) -> case deleteDef m d of Nothing -> throwError $ DefNotFound d @@ -587,7 +606,7 @@ applyProgAction prog mdefName = \case (traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr) (renameVar (GlobalVarRef d) (GlobalVarRef newName)) (m' : ms) - pure (renamedModules, Just $ Selection newName Nothing) + pure (renamedModules, Just $ SelectionDef $ DefSelection newName Nothing) CreateDef modName n -> editModule modName prog $ \mod -> do let defs = moduleDefs mod name <- case n of @@ -601,7 +620,7 @@ applyProgAction prog mdefName = \case expr <- newExpr ty <- newType let def = ASTDef expr ty - pure (insertDef mod name $ DefAST def, Just $ Selection (qualifyName modName name) Nothing) + pure (insertDef mod name $ DefAST def, Just $ SelectionDef $ DefSelection (qualifyName modName name) Nothing) AddTypeDef tc td -> editModuleSameSelection (qualifiedModule tc) prog $ \m -> do td' <- generateTypeDefIDs $ TypeDefAST td let tydefs' = moduleTypes m <> Map.singleton (baseName tc) td' @@ -830,8 +849,8 @@ applyProgAction prog mdefName = \case let meta = bimap (view _exprMetaLens . target) (view _typeMetaLens . target) $ locToEither z pure ( insertDef m defName (DefAST def') - , Just $ - Selection (qualifyDefName m defName) $ + , Just . SelectionDef $ + DefSelection (qualifyDefName m defName) $ Just NodeSelection { nodeType = BodyNode @@ -848,8 +867,8 @@ applyProgAction prog mdefName = \case meta = view _typeMetaLens node in pure ( mod' - , Just $ - Selection (qualifyDefName curMod defName) $ + , Just . SelectionDef $ + DefSelection (qualifyDefName curMod defName) $ Just NodeSelection { nodeType = SigNode @@ -1315,7 +1334,7 @@ copyPasteSig p (fromDefName, fromTyId) toDefName setup = do _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole" let newDef = oldDef{astDefType = fromZipper pasted} let newSel = NodeSelection SigNode (pasted ^. _target % _typeMetaLens % re _Right) - pure (insertDef mod toDefBaseName (DefAST newDef), Just (Selection toDefName $ Just newSel)) + pure (insertDef mod toDefBaseName (DefAST newDef), Just (SelectionDef $ DefSelection toDefName $ Just newSel)) liftError ActionError $ tcWholeProg finalProg -- We cannot use bindersAbove as that works on names only, and different scopes @@ -1383,7 +1402,7 @@ tcWholeProg p = do let oldSel = progSelection p newSel <- case oldSel of Nothing -> pure Nothing - Just s -> do + Just (SelectionDef s) -> do let defName_ = s.def updatedNode <- case s.node of Nothing -> pure Nothing @@ -1394,11 +1413,24 @@ tcWholeProg p = do (SigNode, Right (Right x)) -> pure $ Just $ NodeSelection SigNode $ x ^. _target % _typeMetaLens % re _Right _ -> pure Nothing -- something's gone wrong: expected a SigNode, but found it in the body, or vv, or just not found it pure $ - Just $ - Selection + Just . SelectionDef $ + DefSelection { def = defName_ , node = updatedNode } + Just (SelectionTypeDef s) -> + pure . Just . SelectionTypeDef $ + s & over (#node % mapped % #_TypeDefConsNodeSelection) \conSel -> + conSel & over #field \case + Nothing -> Nothing + Just fieldSel -> + flip (set #meta) fieldSel . (Right . (^. _typeMetaLens)) <$> do + -- If something goes wrong in finding the metadata, we just don't set a field selection. + -- This is similar to what we do when selection is in a term, above. + td <- Map.lookup s.def $ allTypesMeta p + tda <- typeDefAST td + vc <- find ((== conSel.con) . valConName) $ astTypeDefConstructors tda + atMay (valConArgs vc) fieldSel.index pure $ p'{progSelection = newSel} -- | Do a full check of a 'Prog', both the imports and the local modules @@ -1470,7 +1502,7 @@ copyPasteBody p (fromDefName, fromId) toDefName setup = do _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole" let newDef = oldDef{astDefExpr = unfocusExpr $ unfocusType pasted} let newSel = NodeSelection BodyNode (pasted ^. _target % _typeMetaLens % re _Right) - pure (insertDef mod toDefBaseName (DefAST newDef), Just (Selection toDefName $ Just newSel)) + pure (insertDef mod toDefBaseName (DefAST newDef), Just (SelectionDef $ DefSelection toDefName $ Just newSel)) (Left srcE, InExpr tgtE) -> do let sharedScope = if fromDefName == toDefName @@ -1527,7 +1559,7 @@ copyPasteBody p (fromDefName, fromId) toDefName setup = do _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole" let newDef = oldDef{astDefExpr = unfocusExpr pasted} let newSel = NodeSelection BodyNode (pasted ^. _target % _exprMetaLens % re _Left) - pure (insertDef mod toDefBaseName (DefAST newDef), Just (Selection toDefName $ Just newSel)) + pure (insertDef mod toDefBaseName (DefAST newDef), Just (SelectionDef $ DefSelection toDefName $ Just newSel)) liftError ActionError $ tcWholeProg finalProg lookupASTDef :: GVarName -> DefMap -> Maybe ASTDef diff --git a/primer/src/Primer/App/Base.hs b/primer/src/Primer/App/Base.hs index e591b7b3a..8f97e37a7 100644 --- a/primer/src/Primer/App/Base.hs +++ b/primer/src/Primer/App/Base.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE OverloadedLabels #-} {-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE NoFieldSelectors #-} @@ -10,6 +11,11 @@ module Primer.App.Base ( NodeType (..), Selection, Selection' (..), + TypeDefSelection (..), + TypeDefNodeSelection (..), + TypeDefConsSelection (..), + TypeDefConsFieldSelection (..), + DefSelection (..), NodeSelection (..), ) where @@ -21,7 +27,10 @@ import Primer.Core ( ExprMeta, GVarName, HasID (..), + TyConName, + TyVarName, TypeMeta, + ValConName, getID, ) import Primer.JSON ( @@ -54,21 +63,63 @@ data NodeType = BodyNode | SigNode deriving (FromJSON, ToJSON) via PrimerJSON NodeType deriving anyclass (NFData) --- | Describes what interface element the user has selected. --- A definition in the left hand nav bar, and possibly a node in that definition. +-- | Describes which element of a (type or term) definition the student has selected. +-- We have the following invariant: when this contains a `NodeSelection` with @nodeType = SigNode@, +-- or any `TypeDefConsFieldSelection`, then they will always have @meta = Right _@. type Selection = Selection' (Either ExprMeta TypeMeta) -data Selection' a = Selection +data Selection' a + = SelectionDef (DefSelection a) + | SelectionTypeDef (TypeDefSelection a) + deriving stock (Eq, Show, Read, Functor, Generic, Data) + deriving (FromJSON, ToJSON) via PrimerJSON (Selection' a) + deriving anyclass (NFData) + +-- | Some element of a type definition. +data TypeDefSelection a = TypeDefSelection + { def :: TyConName + , node :: Maybe (TypeDefNodeSelection a) + } + deriving stock (Eq, Show, Read, Functor, Generic, Data) + deriving (FromJSON, ToJSON) via PrimerJSON (TypeDefSelection a) + deriving anyclass (NFData) + +-- | Some element in a type definition, other than simply the definition itself. +data TypeDefNodeSelection a + = TypeDefParamNodeSelection TyVarName + | TypeDefConsNodeSelection (TypeDefConsSelection a) + deriving stock (Eq, Show, Read, Functor, Generic, Data) + deriving (FromJSON, ToJSON) via PrimerJSON (TypeDefNodeSelection a) + deriving anyclass (NFData) + +-- | Some element of a definition of a constructor. +data TypeDefConsSelection a = TypeDefConsSelection + { con :: ValConName + , field :: Maybe (TypeDefConsFieldSelection a) + } + deriving stock (Eq, Show, Read, Functor, Generic, Data) + deriving (FromJSON, ToJSON) via PrimerJSON (TypeDefConsSelection a) + deriving anyclass (NFData) + +-- | Some element of a field in the definition of a constructor. +data TypeDefConsFieldSelection a = TypeDefConsFieldSelection + { index :: Int + , meta :: a + } + deriving stock (Eq, Show, Read, Functor, Generic, Data) + deriving (FromJSON, ToJSON) via PrimerJSON (TypeDefConsFieldSelection a) + deriving anyclass (NFData) + +-- | Some element of a term definition. +data DefSelection a = DefSelection { def :: GVarName - -- ^ the ID of some ASTDef , node :: Maybe (NodeSelection a) } deriving stock (Eq, Show, Read, Functor, Generic, Data) - deriving (FromJSON, ToJSON) via PrimerJSON (Selection' a) + deriving (FromJSON, ToJSON) via PrimerJSON (DefSelection a) deriving anyclass (NFData) --- | A selected node, in the body or type signature of some definition. --- We have the following invariant: @nodeType = SigNode ==> isRight meta@ +-- | Some element of a node, in the body or type signature of a term definition. data NodeSelection a = NodeSelection { nodeType :: NodeType , meta :: a diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs index 53da67dfb..312cc7d4d 100644 --- a/primer/test/Tests/Action/Available.hs +++ b/primer/test/Tests/Action/Available.hs @@ -46,6 +46,7 @@ import Primer.Action.Available ( import Primer.Action.Available qualified as Available import Primer.App ( App, + DefSelection (..), EditAppM, Editable (..), Level (Beginner, Expert, Intermediate), @@ -189,16 +190,16 @@ mkTests deps (defName, DefAST def') = Available.Input a -> Input a . fromMaybe (error "id not found") - $ Available.options typeDefs defs cxt level def id a + $ Available.options typeDefs defs cxt level (Right def) id a in testGroup testName $ enumeratePairs <&> \(level, mut) -> - let defActions = map (offered level $ Selection defName Nothing) $ Available.forDef defs level mut d + let defActions = map (offered level $ SelectionDef $ DefSelection defName Nothing) $ Available.forDef defs level mut d bodyActions = map ( \id -> ( id - , map (offered level $ Selection defName $ Just $ NodeSelection BodyNode id) $ + , map (offered level $ SelectionDef $ DefSelection defName $ Just $ NodeSelection BodyNode id) $ Available.forBody typeDefs level @@ -213,7 +214,7 @@ mkTests deps (defName, DefAST def') = map ( \id -> ( id - , map (offered level (Selection defName $ Just $ NodeSelection SigNode id)) $ Available.forSig level mut (astDefType def) id + , map (offered level (SelectionDef $ DefSelection defName $ Just $ NodeSelection SigNode id)) $ Available.forSig level mut (astDefType def) id ) ) . toListOf (_typeMeta % _id) @@ -277,7 +278,7 @@ tasty_available_actions_accepted = withTests 500 $ DefAST{} -> label "AST" DefPrim{} -> label "Prim" (loc, acts) <- - fmap (first (Selection defName) . snd) . forAllWithT fst $ + fmap (first (SelectionDef . DefSelection defName) . snd) . forAllWithT fst $ Gen.frequency $ catMaybes [ Just (1, pure ("actionsForDef", (Nothing, Available.forDef (snd <$> allDefs) l defMut defName))) @@ -304,7 +305,7 @@ tasty_available_actions_accepted = withTests 500 $ def' <- maybe (annotate "primitive def" >> failure) pure $ defAST def progActs <- either (\e -> annotateShow e >> failure) pure $ - toProgActionNoInput (map snd $ progAllDefs $ appProg a) def' loc act' + toProgActionNoInput (map snd $ progAllDefs $ appProg a) (Right def') loc act' actionSucceeds (handleEditRequest progActs) a Available.Input act' -> do def' <- maybe (annotate "primitive def" >> failure) pure $ defAST def @@ -315,7 +316,7 @@ tasty_available_actions_accepted = withTests 500 $ (map snd $ progAllDefs $ appProg a) (progCxt $ appProg a) l - def' + (Right def') loc act' let opts' = [Gen.element $ (Offered,) <$> opts | not (null opts)] @@ -329,7 +330,7 @@ tasty_available_actions_accepted = withTests 500 $ [] -> annotate "no options" >> success options -> do opt <- forAllT $ Gen.choice options - progActs <- either (\e -> annotateShow e >> failure) pure $ toProgActionInput def' loc (snd opt) act' + progActs <- either (\e -> annotateShow e >> failure) pure $ toProgActionInput (Right def') loc (snd opt) act' actionSucceedsOrCapture (fst opt) (handleEditRequest progActs) a where runEditAppMLogs :: @@ -597,12 +598,12 @@ offeredActionTest' sh l inputDef position action = do let offered = case position of InBody _ -> Available.forBody cxt.typeDefs l Editable expr id InSig _ -> Available.forSig l Editable sig id - let options = Available.options cxt.typeDefs defs cxt l exprDef (Just (BodyNode, id)) + let options = Available.options cxt.typeDefs defs cxt l (Right exprDef) (SelectionDef $ DefSelection exprDefName $ Just $ NodeSelection BodyNode id) action' <- case action of Left a -> pure $ if Available.NoInput a `elem` offered - then Right $ toProgActionNoInput (foldMap' moduleDefsQualified $ progModules prog) exprDef (Selection exprDefName $ Just $ NodeSelection BodyNode id) a + then Right $ toProgActionNoInput (foldMap' moduleDefsQualified $ progModules prog) (Right exprDef) (SelectionDef $ DefSelection exprDefName $ Just $ NodeSelection BodyNode id) a else Left $ ActionNotOffered (Available.NoInput a) offered Right (a, o) -> do if Available.Input a `elem` offered @@ -611,7 +612,7 @@ offeredActionTest' sh l inputDef position action = do Just os -> pure $ if o `elem` os.opts - then Right $ toProgActionInput exprDef (Selection exprDefName $ Just $ NodeSelection BodyNode id) o a + then Right $ toProgActionInput (Right exprDef) (SelectionDef $ DefSelection exprDefName $ Just $ NodeSelection BodyNode id) o a else Left $ OptionNotOffered o os.opts else pure $ Left $ ActionNotOffered (Available.Input a) offered action'' <- for action' $ \case diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 90d661594..64d40db5e 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -36,6 +36,7 @@ import Primer.Action ( ) import Primer.App ( App, + DefSelection (..), Log (..), NodeSelection (..), NodeType (..), @@ -161,7 +162,7 @@ unit_move_to_def_main = progActionTest defaultEmptyProg [moveToDef "main"] $ prog' @?= prog { progLog = Log [[moveToDef "main"]] - , progSelection = Just $ Selection (gvn "main") Nothing + , progSelection = Just $ SelectionDef $ DefSelection (gvn "main") Nothing } -- Expression actions are tested in ActionTest - here we just check that we can modify the correct @@ -500,7 +501,7 @@ unit_construct_arrow_in_sig = TFun _ lhs _ -> -- Check that the selection is focused on the lhs, as we instructed case progSelection prog' of - Just (Selection d (Just sel@NodeSelection{nodeType = SigNode})) -> do + Just (SelectionDef (DefSelection d (Just sel@NodeSelection{nodeType = SigNode}))) -> do d @?= qualifyName mainModuleName "other" getID sel @?= getID lhs _ -> assertFailure "no selection" @@ -1324,7 +1325,11 @@ unit_rename_module = Left err -> assertFailure $ show err Right p -> do fmap (unModuleName . moduleName) (progModules p) @?= [["Module2"]] - (.def) <$> progSelection p @?= Just (qualifyName (ModuleName ["Module2"]) "main") + sel <- case progSelection p of + Just (SelectionDef s) -> pure s + Just (SelectionTypeDef _) -> assertFailure "typedef selected" + Nothing -> assertFailure "no selection" + sel.def @?= qualifyName (ModuleName ["Module2"]) "main" case fmap (Map.assocs . moduleDefsQualified) (progModules p) of [[(n, DefAST d)]] -> do let expectedName = qualifyName (ModuleName ["Module2"]) "main" @@ -1507,7 +1512,7 @@ unit_sh_lost_id = Just def -> case astDefExpr <$> defAST def of Just (Var m (GlobalVarRef f)) | f == foo -> case progSelection prog' of - Just Selection{def = selectedDef, node = Just sel} -> + Just (SelectionDef DefSelection{def = selectedDef, node = Just sel}) -> unless (selectedDef == foo && getID sel == getID m) $ assertFailure "expected selection to point at the recursive reference" _ -> assertFailure "expected the selection to point at some node" @@ -1545,8 +1550,8 @@ defaultEmptyProg = do in pure $ newEmptyProg' { progSelection = - Just $ - Selection (gvn "main") $ + Just . SelectionDef $ + DefSelection (gvn "main") $ Just NodeSelection { nodeType = BodyNode diff --git a/primer/test/Tests/Serialization.hs b/primer/test/Tests/Serialization.hs index 47f2bc4c6..24186a519 100644 --- a/primer/test/Tests/Serialization.hs +++ b/primer/test/Tests/Serialization.hs @@ -13,6 +13,7 @@ import Data.Map.Strict qualified as Map import Data.String (String) import Primer.Action (Action (Move, SetCursor), ActionError (IDNotFound), Movement (Child1)) import Primer.App ( + DefSelection (..), EvalResp (EvalResp, evalRespDetail, evalRespExpr, evalRespRedexes), Log (..), NodeSelection (..), @@ -152,12 +153,13 @@ fixtures = } selection :: Selection selection = - Selection (qualifyName modName defName) $ - Just - NodeSelection - { nodeType = BodyNode - , meta = Left exprMeta - } + SelectionDef $ + DefSelection (qualifyName modName defName) $ + Just + NodeSelection + { nodeType = BodyNode + , meta = Left exprMeta + } reductionDetail :: EvalDetail reductionDetail = BetaReduction $ diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs index b1b7eaadd..d5cfe39e9 100644 --- a/primer/test/Tests/Typecheck.hs +++ b/primer/test/Tests/Typecheck.hs @@ -18,6 +18,9 @@ import Primer.App ( progSmartHoles, redoLog ), + TypeDefConsFieldSelection (..), + TypeDefConsSelection (..), + TypeDefSelection (..), appIdCounter, appInit, appNameCounter, @@ -30,6 +33,7 @@ import Primer.App ( tcWholeProgWithImports, ) import Primer.App qualified as App +import Primer.App.Base (TypeDefNodeSelection (..)) import Primer.Builtins ( boolDef, cCons, @@ -782,6 +786,10 @@ tcaFunctorial :: (Functor f, Eq (f (TypeCacheAlpha a))) => TypeCacheAlpha (f a) tcaFunctorial = (==) `on` (fmap TypeCacheAlpha . unTypeCacheAlpha) instance Eq (TypeCacheAlpha a) => Eq (TypeCacheAlpha (Maybe a)) where (==) = tcaFunctorial +instance (Eq (TypeCacheAlpha a), Eq (TypeCacheAlpha b)) => Eq (TypeCacheAlpha (Either a b)) where + TypeCacheAlpha (Left a1) == TypeCacheAlpha (Left a2) = TypeCacheAlpha a1 == TypeCacheAlpha a2 + TypeCacheAlpha (Right b1) == TypeCacheAlpha (Right b2) = TypeCacheAlpha b1 == TypeCacheAlpha b2 + _ == _ = False instance (Eq (TypeCacheAlpha a), Eq b) => Eq (TypeCacheAlpha (Expr' (Meta a) b)) where (==) = (==) `on` (((_exprMeta % _type) %~ TypeCacheAlpha) . unTypeCacheAlpha) instance Eq (TypeCacheAlpha Def) where @@ -799,12 +807,22 @@ instance Eq (TypeCacheAlpha [Module]) where (==) = tcaFunctorial instance Eq (TypeCacheAlpha ExprMeta) where (==) = tcaFunctorial +instance Eq (TypeCacheAlpha TypeMeta) where + (==) = tcaFunctorial +instance Eq (TypeCacheAlpha Kind) where + TypeCacheAlpha k1 == TypeCacheAlpha k2 = k1 == k2 instance Eq (TypeCacheAlpha (App.NodeSelection (Either ExprMeta TypeMeta))) where TypeCacheAlpha (App.NodeSelection t1 m1) == TypeCacheAlpha (App.NodeSelection t2 m2) = t1 == t2 && ((==) `on` first TypeCacheAlpha) m1 m2 instance Eq (TypeCacheAlpha App.Selection) where - TypeCacheAlpha (App.Selection d1 n1) == TypeCacheAlpha (App.Selection d2 n2) = + TypeCacheAlpha (App.SelectionDef (App.DefSelection d1 n1)) == TypeCacheAlpha (App.SelectionDef (App.DefSelection d2 n2)) = d1 == d2 && TypeCacheAlpha n1 == TypeCacheAlpha n2 + TypeCacheAlpha (App.SelectionTypeDef (TypeDefSelection a1 (Just (TypeDefConsNodeSelection (TypeDefConsSelection n1 (Just (TypeDefConsFieldSelection b1 m1))))))) + == TypeCacheAlpha (App.SelectionTypeDef (TypeDefSelection a2 (Just (TypeDefConsNodeSelection (TypeDefConsSelection n2 (Just (TypeDefConsFieldSelection b2 m2))))))) = + a1 == a2 && b1 == b2 && n1 == n2 && TypeCacheAlpha m1 == TypeCacheAlpha m2 + TypeCacheAlpha (App.SelectionTypeDef (TypeDefSelection n1 s1)) == TypeCacheAlpha (App.SelectionTypeDef (TypeDefSelection n2 s2)) = + n1 == n2 && s1 == s2 + _ == _ = False instance Eq (TypeCacheAlpha Prog) where TypeCacheAlpha (Prog i1 m1 s1 sh1 l1 r1) == TypeCacheAlpha (Prog i2 m2 s2 sh2 l2 r2) = TypeCacheAlpha i1 == TypeCacheAlpha i2 diff --git a/primer/test/outputs/serialization/edit_response_2.json b/primer/test/outputs/serialization/edit_response_2.json index 6f9f6749d..ebdaa70a6 100644 --- a/primer/test/outputs/serialization/edit_response_2.json +++ b/primer/test/outputs/serialization/edit_response_2.json @@ -147,28 +147,31 @@ } ], "progSelection": { - "def": { - "baseName": "main", - "qualifiedModule": [ - "M" - ] - }, - "node": { - "meta": { - "Left": [ - 0, - { - "contents": { - "contents": [], - "tag": "TEmptyHole" - }, - "tag": "TCSynthed" - }, - null + "contents": { + "def": { + "baseName": "main", + "qualifiedModule": [ + "M" ] }, - "nodeType": "BodyNode" - } + "node": { + "meta": { + "Left": [ + 0, + { + "contents": { + "contents": [], + "tag": "TEmptyHole" + }, + "tag": "TCSynthed" + }, + null + ] + }, + "nodeType": "BodyNode" + } + }, + "tag": "SelectionDef" }, "progSmartHoles": "SmartHoles", "redoLog": { diff --git a/primer/test/outputs/serialization/prog.json b/primer/test/outputs/serialization/prog.json index f7dff71af..fcfeb7ab3 100644 --- a/primer/test/outputs/serialization/prog.json +++ b/primer/test/outputs/serialization/prog.json @@ -146,28 +146,31 @@ } ], "progSelection": { - "def": { - "baseName": "main", - "qualifiedModule": [ - "M" - ] - }, - "node": { - "meta": { - "Left": [ - 0, - { - "contents": { - "contents": [], - "tag": "TEmptyHole" - }, - "tag": "TCSynthed" - }, - null + "contents": { + "def": { + "baseName": "main", + "qualifiedModule": [ + "M" ] }, - "nodeType": "BodyNode" - } + "node": { + "meta": { + "Left": [ + 0, + { + "contents": { + "contents": [], + "tag": "TEmptyHole" + }, + "tag": "TCSynthed" + }, + null + ] + }, + "nodeType": "BodyNode" + } + }, + "tag": "SelectionDef" }, "progSmartHoles": "SmartHoles", "redoLog": { diff --git a/primer/test/outputs/serialization/selection.json b/primer/test/outputs/serialization/selection.json index 2fe4a279a..3f33224c0 100644 --- a/primer/test/outputs/serialization/selection.json +++ b/primer/test/outputs/serialization/selection.json @@ -1,24 +1,27 @@ { - "def": { - "baseName": "main", - "qualifiedModule": [ - "M" - ] - }, - "node": { - "meta": { - "Left": [ - 0, - { - "contents": { - "contents": [], - "tag": "TEmptyHole" - }, - "tag": "TCSynthed" - }, - null + "contents": { + "def": { + "baseName": "main", + "qualifiedModule": [ + "M" ] }, - "nodeType": "BodyNode" - } + "node": { + "meta": { + "Left": [ + 0, + { + "contents": { + "contents": [], + "tag": "TEmptyHole" + }, + "tag": "TCSynthed" + }, + null + ] + }, + "nodeType": "BodyNode" + } + }, + "tag": "SelectionDef" } \ No newline at end of file From b13def17e9417883d19ddad3c80f0c2565179880 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Thu, 27 Apr 2023 11:29:57 +0100 Subject: [PATCH 11/32] fix: Always omit nothing fields in JSON output This was motivated by a surprising deep equality failure on selections in a TypeScript frontend, due to a null field only present in one of the compared values. Signed-off-by: George Thomas --- primer/src/Primer/JSON.hs | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/primer/src/Primer/JSON.hs b/primer/src/Primer/JSON.hs index d72dec9a6..ef7a17428 100644 --- a/primer/src/Primer/JSON.hs +++ b/primer/src/Primer/JSON.hs @@ -13,8 +13,7 @@ import Data.Aeson ( ToJSON, ToJSONKey, ) -import Deriving.Aeson (CustomJSON (..)) -import Deriving.Aeson.Stock (Vanilla) +import Deriving.Aeson (CustomJSON (..), OmitNothingFields) -- | A type for Primer API JSON encodings. -- @@ -43,4 +42,10 @@ import Deriving.Aeson.Stock (Vanilla) -- -- * @SumTwoElemArray@ is unsupported by openapi3 as it is unrepresentable in -- a schema. -type PrimerJSON a = Vanilla a +type PrimerJSON a = + CustomJSON + '[ -- This protects some clients (e.g. TypeScript) from spurious equality failures + -- due to null-vs-omitted inconsistency. + OmitNothingFields + ] + a From 2ccdce038c2ef12d797b36eb6ff302411b22961c Mon Sep 17 00:00:00 2001 From: George Thomas Date: Thu, 27 Apr 2023 10:21:52 +0100 Subject: [PATCH 12/32] feat: Set better selections after performing typedef actions Signed-off-by: George Thomas --- primer/src/Primer/App.hs | 83 +++++++++++++++++++++++++++------------- 1 file changed, 56 insertions(+), 27 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 2f115b9cd..6b7d143de 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -621,28 +621,34 @@ applyProgAction prog mdefName = \case ty <- newType let def = ASTDef expr ty pure (insertDef mod name $ DefAST def, Just $ SelectionDef $ DefSelection (qualifyName modName name) Nothing) - AddTypeDef tc td -> editModuleSameSelection (qualifiedModule tc) prog $ \m -> do + AddTypeDef tc td -> editModule (qualifiedModule tc) prog $ \m -> do td' <- generateTypeDefIDs $ TypeDefAST td let tydefs' = moduleTypes m <> Map.singleton (baseName tc) td' - m{moduleTypes = tydefs'} - <$ liftError - -- The frontend should never let this error case happen, - -- so we just dump out a raw string for debugging/logging purposes - -- (This is not currently true! We should synchronise the frontend with - -- the typechecker rules. For instance, the form allows to create - -- data T (T : *) = T - -- but the TC rejects it. - -- see https://github.com/hackworthltd/primer/issues/3) - (TypeDefError . show @TypeError) - ( runReaderT - (checkTypeDefs $ Map.singleton tc (TypeDefAST td)) - (buildTypingContextFromModules (progAllModules prog) NoSmartHoles) - ) - RenameType old (unsafeMkName -> nameRaw) -> editModuleSameSelectionCross (qualifiedModule old) prog $ \(m, ms) -> do + liftError + -- The frontend should never let this error case happen, + -- so we just dump out a raw string for debugging/logging purposes + -- (This is not currently true! We should synchronise the frontend with + -- the typechecker rules. For instance, the form allows to create + -- data T (T : *) = T + -- but the TC rejects it. + -- see https://github.com/hackworthltd/primer/issues/3) + (TypeDefError . show @TypeError) + ( runReaderT + (checkTypeDefs $ Map.singleton tc (TypeDefAST td)) + (buildTypingContextFromModules (progAllModules prog) NoSmartHoles) + ) + pure + ( m{moduleTypes = tydefs'} + , Just $ SelectionTypeDef $ TypeDefSelection tc Nothing + ) + RenameType old (unsafeMkName -> nameRaw) -> editModuleCross (qualifiedModule old) prog $ \(m, ms) -> do when (new `elem` allTyConNames prog) $ throwError $ TypeDefAlreadyExists new m' <- traverseOf #moduleTypes updateType m let renamedInTypes = over (traversed % #moduleTypes) updateRefsInTypes $ m' : ms - pure $ over (traversed % #moduleDefs % traversed % #_DefAST) (updateDefBody . updateDefType) renamedInTypes + pure + ( over (traversed % #moduleDefs % traversed % #_DefAST) (updateDefBody . updateDefType) renamedInTypes + , Just $ SelectionTypeDef $ TypeDefSelection new Nothing + ) where new = qualifyName (qualifiedModule old) nameRaw updateType m = do @@ -672,10 +678,13 @@ applyProgAction prog mdefName = \case $ over (#_TCon % _2) updateName updateName n = if n == old then new else n RenameCon type_ old (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> new) -> - editModuleSameSelectionCross (qualifiedModule type_) prog $ \(m, ms) -> do + editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do when (new `elem` allValConNames prog) $ throwError $ ConAlreadyExists new m' <- updateType m - pure $ over (mapped % #moduleDefs) updateDefs (m' : ms) + pure + ( over (mapped % #moduleDefs) updateDefs (m' : ms) + , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefConsNodeSelection $ TypeDefConsSelection new Nothing + ) where updateType = alterTypeDef @@ -693,7 +702,12 @@ applyProgAction prog mdefName = \case . over (#_Case % _3 % traversed % #_CaseBranch % _1) updateName updateName n = if n == old then new else n RenameTypeParam type_ old (unsafeMkLocalName -> new) -> - editModuleSameSelection (qualifiedModule type_) prog updateType + editModule (qualifiedModule type_) prog $ \m -> do + m' <- updateType m + pure + ( m' + , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefParamNodeSelection new + ) where updateType = alterTypeDef @@ -721,13 +735,18 @@ applyProgAction prog mdefName = \case $ \(_, v) -> tvar $ updateName v updateName n = if n == old then new else n AddCon type_ index (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> con) -> - editModuleSameSelectionCross (qualifiedModule type_) prog $ \(m, ms) -> do + editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do when (con `elem` allValConNames prog) $ throwError $ ConAlreadyExists con m' <- updateType m - traverseOf - (traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr) - updateDefs - $ m' : ms + ms' <- + traverseOf + (traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr) + updateDefs + $ m' : ms + pure + ( ms' + , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefConsNodeSelection $ TypeDefConsSelection con Nothing + ) where updateDefs = transformCaseBranches prog type_ $ \bs -> do m' <- DSL.meta @@ -802,9 +821,19 @@ applyProgAction prog mdefName = \case e else pure cb AddConField type_ con index new -> - editModuleSameSelectionCross (qualifiedModule type_) prog $ \(m, ms) -> do + editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do m' <- updateType m - traverseOf (traversed % #moduleDefs) updateDefs (m' : ms) + ms' <- traverseOf (traversed % #moduleDefs) updateDefs (m' : ms) + pure + ( ms' + , Just + . SelectionTypeDef + . TypeDefSelection type_ + . Just + . TypeDefConsNodeSelection + . TypeDefConsSelection con + $ Nothing + ) where updateType = alterTypeDef From 17dbeb3f00100ec5d2d6b9cbaf3c56362be828c0 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Wed, 24 May 2023 12:54:53 +0100 Subject: [PATCH 13/32] feat: Add actions for modifying constructor field types Signed-off-by: George Thomas --- primer/src/Foreword.hs | 12 ++++ primer/src/Primer/API.hs | 18 +++--- primer/src/Primer/Action.hs | 77 ++++++++++++++++++++++--- primer/src/Primer/Action/Available.hs | 78 +++++++++++++++++--------- primer/src/Primer/Action/Errors.hs | 1 + primer/src/Primer/Action/ProgAction.hs | 2 + primer/src/Primer/Action/ProgError.hs | 1 + primer/src/Primer/App.hs | 44 ++++++++++++++- primer/src/Primer/App/Base.hs | 9 +++ primer/src/Primer/Typecheck/Cxt.hs | 2 +- primer/src/Primer/Zipper.hs | 2 +- primer/test/Tests/Action/Prog.hs | 34 +++++++++++ 12 files changed, 235 insertions(+), 45 deletions(-) diff --git a/primer/src/Foreword.hs b/primer/src/Foreword.hs index 1ed8aebf3..ab980f6fd 100644 --- a/primer/src/Foreword.hs +++ b/primer/src/Foreword.hs @@ -32,6 +32,8 @@ module Foreword ( curry4, unsafeMaximum, spanMaybe, + adjustAtA', + findAndAdjustA', ) where -- In general, we should defer to "Protolude"'s exports and avoid name @@ -130,6 +132,11 @@ adjustAtA n f xs = case splitAt n xs of (a, b : bs) -> f b <&> \b' -> Just $ a ++ [b'] ++ bs _ -> pure Nothing +adjustAtA' :: Applicative f => Int -> (a -> f (a, z)) -> [a] -> f (Maybe ([a], z)) +adjustAtA' n f xs = case splitAt n xs of + (a, b : bs) -> f b <&> \(b', z) -> Just (a ++ [b'] ++ bs, z) + _ -> pure Nothing + -- | Adjust the first element of the list which satisfies the -- predicate. Returns 'Nothing' if there is no such element. findAndAdjust :: (a -> Bool) -> (a -> a) -> [a] -> Maybe [a] @@ -143,6 +150,11 @@ findAndAdjustA p f = \case [] -> pure Nothing x : xs -> if p x then Just . (: xs) <$> f x else (x :) <<$>> findAndAdjustA p f xs +findAndAdjustA' :: Applicative m => (a -> Bool) -> (a -> m (a, z)) -> [a] -> m (Maybe ([a], z)) +findAndAdjustA' p f = \case + [] -> pure Nothing + x : xs -> if p x then (\(x', z) -> Just . (,z) . (: xs) $ x') <$> f x else first (x :) <<$>> findAndAdjustA' p f xs + -- | Change the type of an error. modifyError :: MonadError e' m => (e -> e') -> ExceptT e m a -> m a modifyError f = runExceptT >=> either (throwError . f) pure diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index 22fe15aad..4cafedc6b 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -127,6 +127,7 @@ import Primer.App ( newApp, progAllDefs, progAllTypeDefs, + progAllTypeDefsMeta, progCxt, progImports, progLog, @@ -157,6 +158,7 @@ import Primer.Core ( TyVarName, Type, Type' (..), + TypeMeta, ValConName, getID, unLocalName, @@ -218,7 +220,7 @@ import Primer.Log ( import Primer.Module (moduleDefsQualified, moduleName, moduleTypesQualifiedMeta) import Primer.Name qualified as Name import Primer.Primitives (primDefType) -import Primer.TypeDef (ASTTypeDef (..), typeDefNameHints, typeDefParameters) +import Primer.TypeDef (ASTTypeDef (..), forgetTypeDefMetadata, typeDefNameHints, typeDefParameters) import Primer.TypeDef qualified as TypeDef import StmContainers.Map qualified as StmMap @@ -1077,7 +1079,7 @@ availableActions :: availableActions = curry3 $ logAPI (noError AvailableActions) $ \(sid, level, selection) -> do prog <- getProgram sid let allDefs = progAllDefs prog - allTypeDefs = progAllTypeDefs prog + allTypeDefs = progAllTypeDefsMeta prog case selection of SelectionDef sel -> do (editable, ASTDef{astDefType = type_, astDefExpr = expr}) <- findASTDef allDefs sel.def @@ -1085,15 +1087,15 @@ availableActions = curry3 $ logAPI (noError AvailableActions) $ \(sid, level, se Nothing -> Available.forDef (snd <$> allDefs) level editable sel.def Just NodeSelection{..} -> case nodeType of SigNode -> Available.forSig level editable type_ meta - BodyNode -> Available.forBody (snd <$> allTypeDefs) level editable expr meta + BodyNode -> Available.forBody (forgetTypeDefMetadata . snd <$> allTypeDefs) level editable expr meta SelectionTypeDef sel -> do - (editable, _def) <- findASTTypeDef allTypeDefs sel.def + (editable, def) <- findASTTypeDef allTypeDefs sel.def pure $ case sel.node of Nothing -> Available.forTypeDef level editable Just (TypeDefParamNodeSelection _) -> Available.forTypeDefParamNode level editable Just (TypeDefConsNodeSelection s) -> case s.field of Nothing -> Available.forTypeDefConsNode level editable - Just _ -> Available.forTypeDefConsFieldNode level editable + Just field -> Available.forTypeDefConsFieldNode level editable def s.con field.index field.meta actionOptions :: (MonadIO m, MonadThrow m, MonadAPILog l m) => @@ -1117,16 +1119,16 @@ findASTDef allDefs def = case allDefs Map.!? def of Just (_, Def.DefPrim _) -> throwM $ UnexpectedPrimDef def Just (editable, Def.DefAST d) -> pure (editable, d) -findASTTypeDef :: MonadThrow m => Map TyConName (Editable, TypeDef.TypeDef ()) -> TyConName -> m (Editable, ASTTypeDef ()) +findASTTypeDef :: MonadThrow m => Map TyConName (Editable, TypeDef.TypeDef a) -> TyConName -> m (Editable, ASTTypeDef a) findASTTypeDef allTypeDefs def = case allTypeDefs Map.!? def of Nothing -> throwM $ UnknownTypeDef def Just (_, TypeDef.TypeDefPrim _) -> throwM $ UnexpectedPrimTypeDef def Just (editable, TypeDef.TypeDefAST d) -> pure (editable, d) -findASTTypeOrTermDef :: MonadThrow f => App.Prog -> Selection' a -> f (Editable, Either (ASTTypeDef ()) ASTDef) +findASTTypeOrTermDef :: MonadThrow f => App.Prog -> Selection -> f (Editable, Either (ASTTypeDef TypeMeta) ASTDef) findASTTypeOrTermDef prog = \case App.SelectionTypeDef sel -> - Left <<$>> findASTTypeDef (progAllTypeDefs prog) sel.def + Left <<$>> findASTTypeDef (progAllTypeDefsMeta prog) sel.def App.SelectionDef sel -> Right <<$>> findASTDef (progAllDefs prog) sel.def diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index c397a4bed..711b03c68 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -1,4 +1,6 @@ +{-# LANGUAGE BlockArguments #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE OverloadedLabels #-} {-# LANGUAGE OverloadedRecordDot #-} module Primer.Action ( @@ -17,6 +19,7 @@ module Primer.Action ( uniquifyDefName, toProgActionInput, toProgActionNoInput, + applyActionsToField, ) where import Foreword hiding (mod) @@ -27,10 +30,11 @@ import Data.Bifunctor.Swap qualified as Swap import Data.Generics.Product (typed) import Data.List (findIndex) import Data.List.NonEmpty qualified as NE +import Data.Map (insert) import Data.Map.Strict qualified as Map import Data.Set qualified as Set import Data.Text qualified as T -import Optics (set, (%), (?~), (^.), (^?), _Just) +import Optics (over, set, (%), (?~), (^.), (^?), _Just) import Primer.Action.Actions (Action (..), Movement (..), QualifiedText) import Primer.Action.Available qualified as Available import Primer.Action.Errors (ActionError (..)) @@ -40,6 +44,7 @@ import Primer.App.Base ( NodeSelection (..), NodeType (..), Selection' (..), + TypeDefConsFieldSelection (..), TypeDefConsSelection (..), TypeDefNodeSelection (..), TypeDefSelection (..), @@ -60,6 +65,7 @@ import Primer.Core ( Type' (..), TypeCache (..), TypeCacheBoth (..), + TypeMeta, ValConName, baseName, bindName, @@ -102,7 +108,7 @@ import Primer.Def ( Def (..), DefMap, ) -import Primer.Module (Module, insertDef) +import Primer.Module (Module (moduleTypes), insertDef) import Primer.Name (Name, NameCounter, unName, unsafeMkName) import Primer.Name.Fresh ( isFresh, @@ -238,6 +244,49 @@ applyActionsToTypeSig smartHoles imports (mod, mods) (defName, def) actions = -- In this case we just refocus on the top of the type. z -> maybe unwrapError pure (focusType (unfocusLoc z)) +applyActionsToField :: + (MonadFresh ID m, MonadFresh NameCounter m) => + SmartHoles -> + [Module] -> + (Module, [Module]) -> + (Name, ValConName, Int, ASTTypeDef TypeMeta) -> + [Action] -> + m (Either ActionError ([Module], TypeZ)) +applyActionsToField smartHoles imports (mod, mods) (tyName, conName', index, tyDef) actions = + runReaderT + go + (buildTypingContextFromModules (mod : mods <> imports) smartHoles) + & runExceptT + where + go :: ActionM m => m ([Module], TypeZ) + go = do + (valCons, zt) <- + (maybe (throwError $ InternalFailure "applyActionsToField: con name not found") pure =<<) $ + flip (findAndAdjustA' ((== conName') . valConName)) (astTypeDefConstructors tyDef) \(ValCon _ ts) -> do + (t, zt) <- + maybe (throwError $ InternalFailure "applyActionsToField: con field index out of bounds") pure + =<< flip (adjustAtA' index) ts \fieldType -> do + zt <- withWrappedType fieldType \zt -> + foldlM (\l -> local addParamsToCxt . flip applyActionAndSynth l) (InType zt) actions + pure (target (top zt), zt) + pure (ValCon conName' t, zt) + let mod' = mod{moduleTypes = insert tyName (TypeDefAST tyDef{astTypeDefConstructors = valCons}) $ moduleTypes mod} + (,zt) <$> checkEverything smartHoles (CheckEverything{trusted = imports, toCheck = mod' : mods}) + addParamsToCxt :: TC.Cxt -> TC.Cxt + addParamsToCxt = over #localCxt (<> Map.fromList (map (bimap unLocalName TC.K) $ astTypeDefParameters tyDef)) + withWrappedType :: ActionM m => Type -> (TypeZ -> m Loc) -> m TypeZ + withWrappedType ty f = do + wrappedType <- ann emptyHole (pure ty) + let unwrapError = throwError $ InternalFailure "applyActionsToField: failed to unwrap type" + wrapError = throwError $ InternalFailure "applyActionsToField: failed to wrap type" + focusedType = focusType $ focus wrappedType + case focusedType of + Nothing -> wrapError + Just wrappedTy -> + f wrappedTy >>= \case + InType zt -> pure zt + z -> maybe unwrapError pure (focusType (unfocusLoc z)) + data Refocus = Refocus { pre :: Loc , post :: Expr @@ -866,7 +915,7 @@ renameForall b zt = case target zt of -- | Convert a high-level 'Available.NoInputAction' to a concrete sequence of 'ProgAction's. toProgActionNoInput :: DefMap -> - Either (ASTTypeDef ()) ASTDef -> + Either (ASTTypeDef a) ASTDef -> Selection' ID -> Available.NoInputAction -> Either ActionError [ProgAction] @@ -964,16 +1013,22 @@ toProgActionNoInput defs def0 sel0 = \case typeNodeSel >>= \case (s0, TypeDefConsNodeSelection s) -> pure (s0, s) _ -> Left NeedTypeDefConsSelection + conFieldSel = do + (ty, s) <- conSel + maybe (Left NeedTypeDefConsFieldSelection) (pure . (ty,s.con,)) s.field toProgAction actions = do - sel <- termSel - toProg' actions sel.def <$> maybeToEither NoNodeSelection sel.node + case sel0 of + SelectionDef sel -> toProg' actions sel.def <$> maybeToEither NoNodeSelection sel.node + SelectionTypeDef _ -> do + (t, c, f) <- conFieldSel + pure [ConFieldAction t c f.index $ SetCursor f.meta : actions] termDef = first (const NeedTermDef) def0 typeDef = either Right (Left . const NeedTypeDef) def0 -- | Convert a high-level 'Available.InputAction', and associated 'Available.Option', -- to a concrete sequence of 'ProgAction's. toProgActionInput :: - Either (ASTTypeDef ()) ASTDef -> + Either (ASTTypeDef a) ASTDef -> Selection' ID -> Available.Option -> Available.InputAction -> @@ -1089,9 +1144,15 @@ toProgActionInput def0 sel0 opt0 = \case optGlobal = case opt0.context of Nothing -> Left $ NeedLocal opt0 Just q -> pure (q, opt0.option) + conFieldSel = do + (ty, s) <- conSel + maybe (Left NeedTypeDefConsFieldSelection) (pure . (ty,s.con,)) s.field toProg actions = do - sel <- termSel - toProg' actions sel.def <$> maybeToEither NoNodeSelection sel.node + case sel0 of + SelectionDef sel -> toProg' actions sel.def <$> maybeToEither NoNodeSelection sel.node + SelectionTypeDef _ -> do + (t, c, f) <- conFieldSel + pure [ConFieldAction t c f.index $ SetCursor f.meta : actions] offerRefined = do id <- nodeID def <- termDef diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs index cbc6b9613..245b0fd59 100644 --- a/primer/src/Primer/Action/Available.hs +++ b/primer/src/Primer/Action/Available.hs @@ -43,6 +43,11 @@ import Primer.App.Base ( NodeSelection (..), NodeType (..), Selection' (..), + TypeDefConsFieldSelection (..), + TypeDefConsSelection (..), + TypeDefNodeSelection (..), + TypeDefSelection (..), + getTypeDefConFieldType, ) import Primer.Core ( Expr, @@ -53,6 +58,8 @@ import Primer.Core ( ModuleName (unModuleName), Type, Type' (..), + TypeMeta, + ValConName, getID, unLocalName, _bindMeta, @@ -98,6 +105,7 @@ import Primer.Zipper ( focusOn, focusOnTy, locToEither, + target, ) -- | An offered action. @@ -337,9 +345,15 @@ forTypeDefConsNode l Editable = forTypeDefConsFieldNode :: Level -> Editable -> + ASTTypeDef TypeMeta -> + ValConName -> + Int -> + ID -> [Action] -forTypeDefConsFieldNode _ NonEditable = mempty -forTypeDefConsFieldNode l Editable = sortByPriority l [] +forTypeDefConsFieldNode _ NonEditable _ _ _ _ = mempty +forTypeDefConsFieldNode l Editable def con index id = + maybe mempty (sortByPriority l . forType l) $ + findType id =<< getTypeDefConFieldType def con index -- | An input for an 'InputAction'. data Option = Option @@ -375,7 +389,7 @@ options :: DefMap -> Cxt -> Level -> - Either (ASTTypeDef ()) ASTDef -> + Either (ASTTypeDef TypeMeta) ASTDef -> Selection' ID -> InputAction -> -- | Returns 'Nothing' if an ID was required but not passed, passed but not found in the tree, @@ -445,9 +459,6 @@ options typeDefs defs cxt level def0 sel0 = \case AddCon -> pure $ freeVar [] where - defSel = case sel0 of - SelectionDef s -> pure s - SelectionTypeDef _ -> Nothing freeVar opts = Options{opts, free = FreeVarName} noFree opts = Options{opts, free = FreeNone} localOpt = flip Option Nothing . unName @@ -461,30 +472,47 @@ options typeDefs defs cxt level def0 sel0 = \case pure $ (first (localOpt . unLocalName) <$> locals) <> (first globalOpt <$> globals) - findNode = do - sel <- defSel - s <- sel.node - def <- eitherToMaybe def0 - case s.nodeType of - BodyNode -> fst <$> findNodeWithParent s.meta (astDefExpr def) - SigNode -> TypeNode <$> findType s.meta (astDefType def) - genNames typeOrKind = do - sel <- defSel - z <- focusNode =<< sel.node - pure $ map localOpt $ flip runReader cxt $ case z of - Left zE -> generateNameExpr typeOrKind zE - Right zT -> generateNameTy typeOrKind zT - varsInScope = do - sel <- defSel - nodeSel <- sel.node - focusNode nodeSel <&> \case - Left zE -> variablesInScopeExpr defs zE - Right zT -> (variablesInScopeTy zT, [], []) + findNode = case sel0 of + SelectionDef sel -> do + nodeSel <- sel.node + def <- eitherToMaybe def0 + case nodeSel.nodeType of + BodyNode -> fst <$> findNodeWithParent nodeSel.meta (astDefExpr def) + SigNode -> TypeNode <$> findType nodeSel.meta (astDefType def) + SelectionTypeDef sel -> do + (_, zT) <- conField sel + pure $ TypeNode $ target zT + genNames typeOrKind = + map localOpt . flip runReader cxt <$> case sel0 of + SelectionDef sel -> do + z <- focusNode =<< sel.node + pure $ case z of + Left zE -> generateNameExpr typeOrKind zE + Right zT -> generateNameTy typeOrKind zT + SelectionTypeDef sel -> do + (_, zT) <- conField sel + pure $ generateNameTy typeOrKind zT + varsInScope = case sel0 of + SelectionDef sel -> do + nodeSel <- sel.node + focusNode nodeSel <&> \case + Left zE -> variablesInScopeExpr defs zE + Right zT -> (variablesInScopeTy zT, [], []) + SelectionTypeDef sel -> do + (def, zT) <- conField sel + pure (astTypeDefParameters def <> variablesInScopeTy zT, [], []) focusNode nodeSel = do def <- eitherToMaybe def0 case nodeSel.nodeType of BodyNode -> Left . locToEither <$> focusOn nodeSel.meta (astDefExpr def) SigNode -> fmap Right $ focusOnTy nodeSel.meta $ astDefType def + conField sel = do + (con, field) <- case sel of + TypeDefSelection _ (Just (TypeDefConsNodeSelection (TypeDefConsSelection con (Just field)))) -> + Just (con, field) + _ -> Nothing + def <- either Just (const Nothing) def0 + map (def,) $ focusOnTy field.meta =<< getTypeDefConFieldType def con field.index -- Extract the source of the function type we were checked at -- i.e. the type that a lambda-bound variable would have here lamVarTy = \case diff --git a/primer/src/Primer/Action/Errors.hs b/primer/src/Primer/Action/Errors.hs index 9a3deb46c..18b92789f 100644 --- a/primer/src/Primer/Action/Errors.hs +++ b/primer/src/Primer/Action/Errors.hs @@ -69,6 +69,7 @@ data ActionError | NeedTypeDefSelection | NeedTypeDefNodeSelection | NeedTypeDefConsSelection + | NeedTypeDefConsFieldSelection | NeedTypeDefParamSelection | NoNodeSelection | ValConNotFound TyConName ValConName diff --git a/primer/src/Primer/Action/ProgAction.hs b/primer/src/Primer/Action/ProgAction.hs index 47653b24e..e278ec36b 100644 --- a/primer/src/Primer/Action/ProgAction.hs +++ b/primer/src/Primer/Action/ProgAction.hs @@ -47,6 +47,8 @@ data ProgAction BodyAction [Action] | -- | Execute a sequence of actions on the type annotation of the definition SigAction [Action] + | -- | Execute a sequence of actions on the type of a field of a constructor in a typedef + ConFieldAction TyConName ValConName Int [Action] | SetSmartHoles SmartHoles | -- | CopyPaste (d,i) as -- remembers the tree in def d, node i diff --git a/primer/src/Primer/Action/ProgError.hs b/primer/src/Primer/Action/ProgError.hs index a2fa35c27..6b5ece12b 100644 --- a/primer/src/Primer/Action/ProgError.hs +++ b/primer/src/Primer/Action/ProgError.hs @@ -11,6 +11,7 @@ import Primer.Name (Name) data ProgError = NoDefSelected + | NoTypeDefSelected | DefNotFound GVarName | DefAlreadyExists GVarName | DefInUse GVarName diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 6b7d143de..eadcbcf91 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -34,6 +34,7 @@ module Primer.App ( progAllModules, progAllDefs, progAllTypeDefs, + progAllTypeDefsMeta, allValConNames, allTyConNames, progCxt, @@ -100,6 +101,7 @@ import Primer.Action ( ProgAction (..), applyAction', applyActionsToBody, + applyActionsToField, applyActionsToTypeSig, ) import Primer.Action.ProgError (ProgError (..)) @@ -115,6 +117,7 @@ import Primer.App.Base ( TypeDefConsSelection (..), TypeDefNodeSelection (..), TypeDefSelection (..), + getTypeDefConFieldType, ) import Primer.Core ( Bind' (Bind), @@ -904,6 +907,31 @@ applyProgAction prog mdefName = \case , meta = Right meta } ) + ConFieldAction tyName con index actions -> editModuleOfCrossType (Just tyName) prog $ \ms defName def -> do + let smartHoles = progSmartHoles prog + applyActionsToField smartHoles (progImports prog) ms (defName, con, index, def) actions >>= \case + Left err -> throwError $ ActionError err + Right (mod', zt) -> + pure + ( mod' + , Just $ + SelectionTypeDef + TypeDefSelection + { def = tyName + , node = + Just $ + TypeDefConsNodeSelection + TypeDefConsSelection + { con + , field = + Just + TypeDefConsFieldSelection + { index + , meta = Right $ zt ^. _target % _typeMetaLens + } + } + } + ) SetSmartHoles smartHoles -> pure $ prog & #progSmartHoles .~ smartHoles CopyPasteSig fromIds setup -> case mdefName of @@ -1033,6 +1061,19 @@ editModuleOfCross mdefName prog f = case mdefName of Just (DefAST def) -> f ms (baseName defname) def _ -> throwError $ DefNotFound defname +editModuleOfCrossType :: + MonadError ProgError m => + Maybe TyConName -> + Prog -> + ((Module, [Module]) -> Name -> ASTTypeDef TypeMeta -> m ([Module], Maybe Selection)) -> + m Prog +editModuleOfCrossType mdefName prog f = case mdefName of + Nothing -> throwError NoTypeDefSelected + Just defname -> editModuleCross (qualifiedModule defname) prog $ \ms@(m, _) -> + case Map.lookup (baseName defname) (moduleTypes m) of + Just (TypeDefAST def) -> f ms (baseName defname) def + _ -> throwError $ TypeDefNotFound defname + -- | Undo the last block of actions. -- -- If there are no actions in the log we return the program unchanged. @@ -1458,8 +1499,7 @@ tcWholeProg p = do -- This is similar to what we do when selection is in a term, above. td <- Map.lookup s.def $ allTypesMeta p tda <- typeDefAST td - vc <- find ((== conSel.con) . valConName) $ astTypeDefConstructors tda - atMay (valConArgs vc) fieldSel.index + getTypeDefConFieldType tda conSel.con fieldSel.index pure $ p'{progSelection = newSel} -- | Do a full check of a 'Prog', both the imports and the local modules diff --git a/primer/src/Primer/App/Base.hs b/primer/src/Primer/App/Base.hs index 8f97e37a7..0abf4544d 100644 --- a/primer/src/Primer/App/Base.hs +++ b/primer/src/Primer/App/Base.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE OverloadedLabels #-} {-# LANGUAGE OverloadedRecordDot #-} +{-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE NoFieldSelectors #-} -- | Definitions needed to build the app. @@ -17,6 +18,7 @@ module Primer.App.Base ( TypeDefConsFieldSelection (..), DefSelection (..), NodeSelection (..), + getTypeDefConFieldType, ) where import Protolude @@ -29,6 +31,7 @@ import Primer.Core ( HasID (..), TyConName, TyVarName, + Type', TypeMeta, ValConName, getID, @@ -39,6 +42,7 @@ import Primer.JSON ( PrimerJSON, ToJSON, ) +import Primer.TypeDef (ASTTypeDef, ValCon (..), astTypeDefConstructors) -- | The current programming "level". This setting determines which -- actions are displayed to the student, the labels on UI elements, @@ -130,3 +134,8 @@ data NodeSelection a = NodeSelection instance HasID a => HasID (NodeSelection a) where _id = lens (getID . (.meta)) (flip $ over #meta . set _id) + +getTypeDefConFieldType :: ASTTypeDef a -> ValConName -> Int -> Maybe (Type' a) +getTypeDefConFieldType def con index = + flip atMay index . valConArgs + =<< find ((== con) . valConName) (astTypeDefConstructors def) diff --git a/primer/src/Primer/Typecheck/Cxt.hs b/primer/src/Primer/Typecheck/Cxt.hs index 6ffd63c4d..ada1aad01 100644 --- a/primer/src/Primer/Typecheck/Cxt.hs +++ b/primer/src/Primer/Typecheck/Cxt.hs @@ -28,4 +28,4 @@ data Cxt = Cxt , globalCxt :: Map GVarName Type -- ^ global variables (i.e. IDs of top-level definitions) } - deriving stock (Show) + deriving stock (Show, Generic) diff --git a/primer/src/Primer/Zipper.hs b/primer/src/Primer/Zipper.hs index 5dad673eb..55d98d0e7 100644 --- a/primer/src/Primer/Zipper.hs +++ b/primer/src/Primer/Zipper.hs @@ -448,7 +448,7 @@ findNodeWithParent id x = do InBind (BindCase bz) -> (CaseBindNode $ caseBindZFocus bz, Just . ExprNode . target . unfocusCaseBind $ bz) -- | Find a sub-type in a larger type by its ID. -findType :: ID -> Type -> Maybe Type +findType :: (Data a, HasID a) => ID -> Type' a -> Maybe (Type' a) findType id ty = target <$> focusOnTy id ty -- | An AST node tagged with its "sort" - i.e. if it's a type or expression or binding etc. diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 64d40db5e..936726aa0 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -1287,6 +1287,40 @@ unit_AddConField_case_ann = ] ) +unit_ConFieldAction :: Assertion +unit_ConFieldAction = + progActionTest + ( defaultProgEditableTypeDefs $ do + e <- con cA $ replicate 3 $ con0 $ vcn "True" + t <- tEmptyHole + pure [astDef "def" e t] + ) + [ConFieldAction tT cA 1 [ConstructArrowL]] + $ expectSuccess + $ \_ prog' -> do + td <- findTypeDef tT prog' + def <- findDef (gvn "def") prog' + astTypeDefConstructors td + @?= [ ValCon + cA + [ TCon () (tcn "Bool") + , TFun () (TCon () (tcn "Bool")) (TEmptyHole ()) + , TCon () (tcn "Bool") + ] + , ValCon cB [TApp () (TApp () (TCon () tT) (TVar () "b")) (TVar () "a"), TVar () "b"] + ] + forgetMetadata (astDefExpr def) + @?= forgetMetadata + ( create' $ + do + con + cA + [ con0 $ vcn "True" + , hole $ con0 $ vcn "True" + , con0 $ vcn "True" + ] + ) + -- 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) From 04c3f839d87c3109c5d527c2b4ad962bcac3f132 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Mon, 15 May 2023 12:41:53 +0100 Subject: [PATCH 14/32] refactor: Abstract over labelling in available actions property test This will be necessary when we extend to typedefs, since we need to branch here, but can't use `label` in `GenT`. Signed-off-by: George Thomas --- primer/test/Tests/Action/Available.hs | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs index 312cc7d4d..304bcb69e 100644 --- a/primer/test/Tests/Action/Available.hs +++ b/primer/test/Tests/Action/Available.hs @@ -268,11 +268,15 @@ tasty_available_actions_accepted = withTests 500 $ let isMutable = \case Editable -> True NonEditable -> False - (defName, (defMut, def)) <- case partition (isMutable . fst . snd) $ Map.toList allDefs of - ([], []) -> discard - (mut, []) -> label "all mut" >> forAllT (Gen.element mut) - ([], immut) -> label "all immut" >> forAllT (Gen.element immut) - (mut, immut) -> label "mixed mut/immut" >> forAllT (Gen.frequency [(9, Gen.element mut), (1, Gen.element immut)]) + (defName, (defMut, def)) <- + maybe discard (\(t, x) -> label t >> pure x) + =<< forAllT + ( case partition (isMutable . fst . snd) $ Map.toList allDefs of + ([], []) -> pure Nothing + (mut, []) -> Just . ("all mut",) <$> Gen.element mut + ([], immut) -> Just . ("all immut",) <$> Gen.element immut + (mut, immut) -> Just . ("mixed mut/immut",) <$> Gen.frequency [(9, Gen.element mut), (1, Gen.element immut)] + ) collect defMut case def of DefAST{} -> label "AST" From 8ba35198f142476aa2d9d0d998f54cc5490545eb Mon Sep 17 00:00:00 2001 From: George Thomas Date: Mon, 15 May 2023 13:27:58 +0100 Subject: [PATCH 15/32] refactor: Match actual function names in hedgehog output This should have been done back when `forDef` etc. acquired their current names. Signed-off-by: George Thomas --- primer/test/Tests/Action/Available.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs index 304bcb69e..e67634315 100644 --- a/primer/test/Tests/Action/Available.hs +++ b/primer/test/Tests/Action/Available.hs @@ -285,18 +285,18 @@ tasty_available_actions_accepted = withTests 500 $ fmap (first (SelectionDef . DefSelection defName) . snd) . forAllWithT fst $ Gen.frequency $ catMaybes - [ Just (1, pure ("actionsForDef", (Nothing, Available.forDef (snd <$> allDefs) l defMut defName))) + [ Just (1, pure ("forDef", (Nothing, Available.forDef (snd <$> allDefs) l defMut defName))) , defAST def <&> \d' -> (2,) $ do let ty = astDefType d' ids = ty ^.. typeIDs i <- Gen.element ids - let hedgehogMsg = "actionsForDefSig id " <> show i + let hedgehogMsg = "forSig id " <> show i pure (hedgehogMsg, (Just $ NodeSelection SigNode i, Available.forSig l defMut ty i)) , defAST def <&> \d' -> (7,) $ do let expr = astDefExpr d' ids = expr ^.. exprIDs i <- Gen.element ids - let hedgehogMsg = "actionsForDefBody id " <> show i + let hedgehogMsg = "forBody id " <> show i pure (hedgehogMsg, (Just $ NodeSelection BodyNode i, Available.forBody (snd <$> progAllTypeDefs (appProg a)) l defMut expr i)) ] case acts of From d50be49cae8e44351ddfdaa31ae9017d9d671f68 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Tue, 16 May 2023 23:16:32 +0100 Subject: [PATCH 16/32] test: Extend available actions property test to cover typedefs Signed-off-by: George Thomas --- primer/test/Tests/Action/Available.hs | 109 ++++++++++++++++++++++---- 1 file changed, 94 insertions(+), 15 deletions(-) diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs index e67634315..4d131d453 100644 --- a/primer/test/Tests/Action/Available.hs +++ b/primer/test/Tests/Action/Available.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE BlockArguments #-} {-# LANGUAGE OverloadedLabels #-} {-# LANGUAGE OverloadedRecordDot #-} @@ -6,6 +7,7 @@ module Tests.Action.Available where import Foreword import Control.Monad.Log (WithSeverity) +import Data.Bitraversable (bitraverse) import Data.ByteString.Lazy.Char8 qualified as BS import Data.List.Extra (enumerate, partition) import Data.Map qualified as M @@ -14,6 +16,8 @@ import Data.Text qualified as T import Data.Text.Lazy qualified as TL import GHC.Err (error) import Hedgehog ( + GenT, + LabelName, PropertyT, annotate, annotateShow, @@ -54,6 +58,9 @@ import Primer.App ( NodeType (..), ProgError (ActionError, DefAlreadyExists), Selection' (..), + TypeDefConsSelection (TypeDefConsSelection), + TypeDefNodeSelection (TypeDefConsNodeSelection, TypeDefParamNodeSelection), + TypeDefSelection (TypeDefSelection), appProg, checkAppWellFormed, checkProgWellFormed, @@ -61,12 +68,14 @@ import Primer.App ( nextProgID, progAllDefs, progAllTypeDefs, + progAllTypeDefsMeta, progCxt, progImports, progModules, progSmartHoles, runEditAppM, ) +import Primer.App.Base (TypeDefConsFieldSelection (..)) import Primer.Builtins (builtinModuleName, cCons, cFalse, cTrue, tBool, tList, tNat) import Primer.Core ( Expr, @@ -130,6 +139,7 @@ import Primer.Module ( import Primer.Name (Name (unName)) import Primer.Test.TestM (evalTestM) import Primer.Test.Util (clearMeta, clearTypeMeta, testNoSevereLogs) +import Primer.TypeDef (ASTTypeDef (astTypeDefConstructors), TypeDef (TypeDefAST, TypeDefPrim), ValCon (..), astTypeDefParameters, typeDefAST) import Primer.Typecheck ( CheckEverythingRequest (CheckEverything, toCheck, trusted), SmartHoles (NoSmartHoles, SmartHoles), @@ -264,26 +274,91 @@ tasty_available_actions_accepted = withTests 500 $ -- We only test SmartHoles mode (which is the only supported user-facing -- mode - NoSmartHoles is only used for internal sanity testing etc) a <- forAllT $ genApp SmartHoles cxt + let allTypes = progAllTypeDefsMeta $ appProg a let allDefs = progAllDefs $ appProg a let isMutable = \case Editable -> True NonEditable -> False - (defName, (defMut, def)) <- - maybe discard (\(t, x) -> label t >> pure x) - =<< forAllT - ( case partition (isMutable . fst . snd) $ Map.toList allDefs of + let genDef :: Map name (Editable, def) -> GenT WT (Maybe (LabelName, (Editable, (name, def)))) + genDef m = + second (\(n, (e, t)) -> (e, (n, t))) + <<$>> case partition (isMutable . fst . snd) $ Map.toList m of ([], []) -> pure Nothing (mut, []) -> Just . ("all mut",) <$> Gen.element mut ([], immut) -> Just . ("all immut",) <$> Gen.element immut (mut, immut) -> Just . ("mixed mut/immut",) <$> Gen.frequency [(9, Gen.element mut), (1, Gen.element immut)] + (defMut, typeOrTermDef) <- + maybe discard (\(t, x) -> label t >> pure x) + =<< forAllT + ( Gen.choice + [ second (second Left) <<$>> genDef allTypes + , second (second Right) <<$>> genDef allDefs + ] ) collect defMut - case def of - DefAST{} -> label "AST" - DefPrim{} -> label "Prim" - (loc, acts) <- - fmap (first (SelectionDef . DefSelection defName) . snd) . forAllWithT fst $ - Gen.frequency $ + case typeOrTermDef of + Left (_, t) -> + label "type" >> case t of + TypeDefPrim{} -> label "Prim" + TypeDefAST{} -> label "AST" + Right (_, t) -> + label "term" >> case t of + DefPrim{} -> label "Prim" + DefAST{} -> label "AST" + (loc, acts) <- case typeOrTermDef of + Left (defName, def) -> + (fmap snd . forAllWithT fst) case typeDefAST def of + Nothing -> Gen.discard + Just def' -> + let typeDefSel = SelectionTypeDef . TypeDefSelection defName + forTypeDef = ("forTypeDef", (typeDefSel Nothing, Available.forTypeDef l defMut)) + in Gen.frequency + [ (1, pure forTypeDef) + , + ( 2 + , case astTypeDefParameters def' of + [] -> pure forTypeDef + ps -> do + (p, _) <- Gen.element ps + pure + ( "forTypeDefParamNode" + , + ( typeDefSel $ Just $ TypeDefParamNodeSelection p + , Available.forTypeDefParamNode l defMut + ) + ) + ) + , + ( 5 + , case astTypeDefConstructors def' of + [] -> pure forTypeDef + cs -> do + ValCon{valConName, valConArgs} <- Gen.element cs + let typeDefConsNodeSel = typeDefSel . Just . TypeDefConsNodeSelection . TypeDefConsSelection valConName + forTypeDefConsNode = ("forTypeDefConsNode", (typeDefConsNodeSel Nothing, Available.forTypeDefConsNode l defMut)) + case valConArgs of + [] -> pure forTypeDefConsNode + as -> + Gen.frequency + [ (1, pure forTypeDefConsNode) + , + ( 5 + , do + (n, t) <- Gen.element $ zip [0 ..] as + i <- Gen.element $ t ^.. typeIDs + pure + ( "forTypeDefConsFieldNode" + , + ( typeDefConsNodeSel . Just $ TypeDefConsFieldSelection n i + , Available.forTypeDefConsFieldNode l defMut def' valConName n i + ) + ) + ) + ] + ) + ] + Right (defName, def) -> + fmap (first (SelectionDef . DefSelection defName) . snd) . forAllWithT fst . Gen.frequency $ catMaybes [ Just (1, pure ("forDef", (Nothing, Available.forDef (snd <$> allDefs) l defMut defName))) , defAST def <&> \d' -> (2,) $ do @@ -299,20 +374,24 @@ tasty_available_actions_accepted = withTests 500 $ let hedgehogMsg = "forBody id " <> show i pure (hedgehogMsg, (Just $ NodeSelection BodyNode i, Available.forBody (snd <$> progAllTypeDefs (appProg a)) l defMut expr i)) ] + annotateShow loc case acts of [] -> label "no offered actions" >> success acts' -> do + def <- + bitraverse + (maybe (annotate "primitive type def" >> failure) pure . typeDefAST . snd) + (maybe (annotate "primitive def" >> failure) pure . defAST . snd) + typeOrTermDef action <- forAllT $ Gen.element acts' collect action case action of Available.NoInput act' -> do - def' <- maybe (annotate "primitive def" >> failure) pure $ defAST def progActs <- either (\e -> annotateShow e >> failure) pure $ - toProgActionNoInput (map snd $ progAllDefs $ appProg a) (Right def') loc act' + toProgActionNoInput (map snd $ progAllDefs $ appProg a) def loc act' actionSucceeds (handleEditRequest progActs) a Available.Input act' -> do - def' <- maybe (annotate "primitive def" >> failure) pure $ defAST def Available.Options{Available.opts, Available.free} <- maybe (annotate "id not found" >> failure) pure $ Available.options @@ -320,7 +399,7 @@ tasty_available_actions_accepted = withTests 500 $ (map snd $ progAllDefs $ appProg a) (progCxt $ appProg a) l - (Right def') + def loc act' let opts' = [Gen.element $ (Offered,) <$> opts | not (null opts)] @@ -334,7 +413,7 @@ tasty_available_actions_accepted = withTests 500 $ [] -> annotate "no options" >> success options -> do opt <- forAllT $ Gen.choice options - progActs <- either (\e -> annotateShow e >> failure) pure $ toProgActionInput (Right def') loc (snd opt) act' + progActs <- either (\e -> annotateShow e >> failure) pure $ toProgActionInput def loc (snd opt) act' actionSucceedsOrCapture (fst opt) (handleEditRequest progActs) a where runEditAppMLogs :: From d082c9ec03b3a111096c1151a88bbf1712bc4200 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Wed, 17 May 2023 00:21:21 +0100 Subject: [PATCH 17/32] `AddConField` - update TC Signed-off-by: George Thomas --- primer/src/Primer/App.hs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index eadcbcf91..40e55fc51 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -135,6 +135,8 @@ import Primer.Core ( TyConName, Type, Type' (..), + TypeCache (..), + TypeCacheBoth (..), TypeMeta, ValConName, getID, @@ -858,7 +860,8 @@ applyProgAction prog mdefName = \case updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateCons <=< updateDecons) updateCons = transformM $ \case Con m con' tms | con' == con -> do - m' <- DSL.meta + id <- fresh + let m' = Meta id (Just (TCEmb $ TCBoth (TEmptyHole ()) (TEmptyHole ()))) Nothing case insertAt index (EmptyHole m') tms of Just args' -> pure $ Con m con' args' Nothing -> throwError $ ConNotSaturated con @@ -867,7 +870,8 @@ applyProgAction prog mdefName = \case traverse $ \cb@(CaseBranch vc binds e) -> if vc == con then do - m' <- DSL.meta + id <- fresh + let m' = Meta id (Just (TCChkedAt (TEmptyHole ()))) Nothing newName <- LocalName <$> freshName (freeVars e) binds' <- maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (Bind m' newName) binds pure $ CaseBranch vc binds' e From e0c0b5dcb1001f1b2b9f05e9ad6dd94b7349e04f Mon Sep 17 00:00:00 2001 From: George Thomas Date: Wed, 17 May 2023 01:27:49 +0100 Subject: [PATCH 18/32] allow "renaming" a type to its old name Signed-off-by: George Thomas --- primer/src/Primer/App.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 40e55fc51..73b3932cd 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -647,7 +647,7 @@ applyProgAction prog mdefName = \case , Just $ SelectionTypeDef $ TypeDefSelection tc Nothing ) RenameType old (unsafeMkName -> nameRaw) -> editModuleCross (qualifiedModule old) prog $ \(m, ms) -> do - when (new `elem` allTyConNames prog) $ throwError $ TypeDefAlreadyExists new + when (new /= old && new `elem` allTyConNames prog) $ throwError $ TypeDefAlreadyExists new m' <- traverseOf #moduleTypes updateType m let renamedInTypes = over (traversed % #moduleTypes) updateRefsInTypes $ m' : ms pure From 40b11e31005e735a2caea9c8640a5310d6da16e2 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Wed, 17 May 2023 02:11:19 +0100 Subject: [PATCH 19/32] make `AddInput` work in con fields Signed-off-by: George Thomas --- primer/src/Primer/Action.hs | 35 ++++++++++++++++++--------- primer/src/Primer/Action/Errors.hs | 5 ++-- primer/test/Tests/Action/Available.hs | 3 ++- 3 files changed, 28 insertions(+), 15 deletions(-) diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index 711b03c68..3f791bc08 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -27,6 +27,7 @@ import Foreword hiding (mod) import Control.Monad.Fresh (MonadFresh) import Data.Aeson (Value) import Data.Bifunctor.Swap qualified as Swap +import Data.Data (Data) import Data.Generics.Product (typed) import Data.List (findIndex) import Data.List.NonEmpty qualified as NE @@ -914,6 +915,7 @@ renameForall b zt = case target zt of -- | Convert a high-level 'Available.NoInputAction' to a concrete sequence of 'ProgAction's. toProgActionNoInput :: + (HasID a, Data a) => DefMap -> Either (ASTTypeDef a) ASTDef -> Selection' ID -> @@ -947,18 +949,27 @@ toProgActionNoInput defs def0 sel0 = \case -- on the domain (left) side of the arrow. toProgAction [ConstructArrowL, Move Child1] Available.AddInput -> do - -- This action traverses the function type and adds a function arrow to the end of it, - -- resulting in a new argument type. The result type is unchanged. - -- The cursor location is also unchanged. - -- e.g. A -> B -> C ==> A -> B -> ? -> C - id <- nodeID - def <- termDef - type_ <- case findType id $ astDefType def of - Just t -> pure t - Nothing -> case map fst $ findNodeWithParent id $ astDefExpr def of - Just (TypeNode t) -> pure t - Just sm -> Left $ NeedType sm - Nothing -> Left $ IDNotFound id + type_ <- case def0 of + Left def -> do + (tName, vcName, field) <- conFieldSel + let id = field.meta + vc <- maybeToEither (ValConNotFound tName vcName) $ find ((== vcName) . valConName) $ astTypeDefConstructors def + t <- maybeToEither (FieldIndexOutOfBounds vcName field.index) $ flip atMay field.index $ valConArgs vc + case findType id t of + Just t' -> pure $ forgetTypeMetadata t' + Nothing -> Left $ IDNotFound id + Right def -> do + -- This action traverses the function type and adds a function arrow to the end of it, + -- resulting in a new argument type. The result type is unchanged. + -- The cursor location is also unchanged. + -- e.g. A -> B -> C ==> A -> B -> ? -> C + id <- nodeID + forgetTypeMetadata <$> case findType id $ astDefType def of + Just t -> pure t + Nothing -> case map fst $ findNodeWithParent id $ astDefExpr def of + Just (TypeNode t) -> pure t + Just sm -> Left $ NeedType sm + Nothing -> Left $ IDNotFound id l <- case type_ of TFun _ a b -> pure $ NE.length $ fst $ unfoldFun a b t -> Left $ NeedTFun t diff --git a/primer/src/Primer/Action/Errors.hs b/primer/src/Primer/Action/Errors.hs index 18b92789f..64f4fdb40 100644 --- a/primer/src/Primer/Action/Errors.hs +++ b/primer/src/Primer/Action/Errors.hs @@ -13,7 +13,7 @@ import Data.Aeson (FromJSON (..), ToJSON (..)) import Primer.Action.Actions (Action) import Primer.Action.Available qualified as Available import Primer.Action.Movement (Movement) -import Primer.Core (Expr, GVarName, ID, LVarName, ModuleName, TyConName, Type, ValConName) +import Primer.Core (Expr, GVarName, ID, LVarName, ModuleName, TyConName, Type', ValConName) import Primer.JSON (CustomJSON (..), PrimerJSON) import Primer.Typecheck.TypeError (TypeError) import Primer.Zipper (SomeNode) @@ -57,7 +57,7 @@ data ActionError -- The extra unit is to avoid having two constructors with a single -- TypeError field, breaking our MonadNestedError machinery... ImportFailed () TypeError - | NeedTFun Type + | NeedTFun (Type' ()) | NeedType SomeNode | NeedGlobal Available.Option | NeedLocal Available.Option @@ -73,5 +73,6 @@ data ActionError | NeedTypeDefParamSelection | NoNodeSelection | ValConNotFound TyConName ValConName + | FieldIndexOutOfBounds ValConName Int deriving stock (Eq, Show, Read, Generic) deriving (FromJSON, ToJSON) via PrimerJSON ActionError diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs index 4d131d453..9f525351e 100644 --- a/primer/test/Tests/Action/Available.hs +++ b/primer/test/Tests/Action/Available.hs @@ -86,6 +86,7 @@ import Primer.Core ( Kind (KFun, KType), ModuleName (ModuleName, unModuleName), Type, + TypeMeta, getID, mkSimpleModuleName, moduleNamePretty, @@ -686,7 +687,7 @@ offeredActionTest' sh l inputDef position action = do Left a -> pure $ if Available.NoInput a `elem` offered - then Right $ toProgActionNoInput (foldMap' moduleDefsQualified $ progModules prog) (Right exprDef) (SelectionDef $ DefSelection exprDefName $ Just $ NodeSelection BodyNode id) a + then Right $ toProgActionNoInput @TypeMeta (foldMap' moduleDefsQualified $ progModules prog) (Right exprDef) (SelectionDef $ DefSelection exprDefName $ Just $ NodeSelection BodyNode id) a else Left $ ActionNotOffered (Available.NoInput a) offered Right (a, o) -> do if Available.Input a `elem` offered From 0852e55955abb1870bfc6624fd7760567cccd631 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Tue, 23 May 2023 13:14:34 +0100 Subject: [PATCH 20/32] less strict duplicate name checking we never consistently checked these things in `applyProgAction`, and it would be awkward to do so. besides, why do we care? Signed-off-by: George Thomas --- primer/src/Primer/Action/ProgError.hs | 3 --- primer/src/Primer/App.hs | 4 ---- primer/src/Primer/Typecheck.hs | 9 +++------ primer/test/Tests/Action/Prog.hs | 26 +------------------------- 4 files changed, 4 insertions(+), 38 deletions(-) diff --git a/primer/src/Primer/Action/ProgError.hs b/primer/src/Primer/Action/ProgError.hs index 6b5ece12b..fe90e21cf 100644 --- a/primer/src/Primer/Action/ProgError.hs +++ b/primer/src/Primer/Action/ProgError.hs @@ -7,7 +7,6 @@ import Primer.Action.Errors (ActionError) import Primer.Core.Meta (GVarName, ModuleName, TyConName, TyVarName, ValConName) import Primer.Eval.EvalError (EvalError) import Primer.JSON (CustomJSON (..), PrimerJSON) -import Primer.Name (Name) data ProgError = NoDefSelected @@ -25,8 +24,6 @@ data ProgError ConNotSaturated ValConName | ParamNotFound TyVarName | ParamAlreadyExists TyVarName - | TyConParamClash Name - | ValConParamClash Name | ActionError ActionError | EvalError EvalError | -- | Currently copy/paste is only exposed in the frontend via select diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 73b3932cd..3adf3fdbe 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -662,7 +662,6 @@ applyProgAction prog mdefName = \case -- To relax this, we'd have to be careful about how it interacts with type-checking of primitive literals. maybe (throwError $ TypeDefIsPrim old) pure . typeDefAST =<< maybe (throwError $ TypeDefNotFound old) pure (Map.lookup (baseName old) m) - when (nameRaw `elem` map (unLocalName . fst) (astTypeDefParameters d0)) $ throwError $ TyConParamClash nameRaw pure $ Map.insert nameRaw (TypeDefAST d0) $ Map.delete (baseName old) m updateRefsInTypes = over @@ -720,9 +719,6 @@ applyProgAction prog mdefName = \case type_ updateParam def = do when (new `elem` map fst (astTypeDefParameters def)) $ throwError $ ParamAlreadyExists new - let nameRaw = unLocalName new - when (nameRaw == baseName type_) $ throwError $ TyConParamClash nameRaw - when (nameRaw `elem` map (baseName . valConName) (astTypeDefConstructors def)) $ throwError $ ValConParamClash nameRaw def & traverseOf #astTypeDefParameters diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index 87e3b9cd2..c8e6b83d7 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -103,7 +103,7 @@ import Primer.Core ( Expr' (..), ExprMeta, GVarName, - GlobalName (baseName, qualifiedModule), + GlobalName (qualifiedModule), ID, Kind (..), LVarName, @@ -356,11 +356,8 @@ checkTypeDefs tds = do ) "Module name of type and all constructors must be the same" assert - (distinct $ map (unLocalName . fst) params <> map (baseName . valConName) cons) - "Duplicate names in one tydef: between parameter-names and constructor-names" - assert - (notElem (baseName tc) $ map (unLocalName . fst) params) - "Duplicate names in one tydef: between type-def-name and parameter-names" + (distinct $ map (unLocalName . fst) params) + "Duplicate parameter names in one tydef" local (noSmartHoles . extendLocalCxtTys params) $ mapM_ (checkKind' KType <=< fakeMeta) $ concatMap valConArgs cons diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 936726aa0..01de984a2 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -420,31 +420,7 @@ unit_create_typedef_bad_5 = , astTypeDefNameHints = [] } in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] $ - expectError (@?= TypeDefError "InternalError \"Duplicate names in one tydef: between parameter-names and constructor-names\"") - --- Forbid clash between type name and parameter name -unit_create_typedef_bad_6 :: Assertion -unit_create_typedef_bad_6 = - let td = - ASTTypeDef - { astTypeDefParameters = [("T", KType)] - , astTypeDefConstructors = [] - , astTypeDefNameHints = [] - } - in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] $ - expectError (@?= TypeDefError "InternalError \"Duplicate names in one tydef: between type-def-name and parameter-names\"") - --- Forbid clash between parameter name and constructor name -unit_create_typedef_bad_7 :: Assertion -unit_create_typedef_bad_7 = - let td = - ASTTypeDef - { astTypeDefParameters = [("a", KType)] - , astTypeDefConstructors = [ValCon (vcn "a") []] - , astTypeDefNameHints = [] - } - in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] $ - expectError (@?= TypeDefError "InternalError \"Duplicate names in one tydef: between parameter-names and constructor-names\"") + expectError (@?= TypeDefError "InternalError \"Duplicate parameter names in one tydef\"") -- Forbid clash between type name and name of a primitive type unit_create_typedef_bad_prim :: Assertion From b7915eddb5b2d3069133487669d5f8676ddc08bc Mon Sep 17 00:00:00 2001 From: George Thomas Date: Tue, 23 May 2023 13:31:26 +0100 Subject: [PATCH 21/32] refactor - updateType' -- TODO rename `updateType` to `updateTypeDef` and this to `updateType`? in all branches? Signed-off-by: George Thomas --- primer/src/Primer/App.hs | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 3adf3fdbe..8794eed43 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -65,6 +65,7 @@ import Foreword hiding (mod) 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 (transform, transformM) import Data.Generics.Uniplate.Zipper ( fromZipper, @@ -666,21 +667,16 @@ applyProgAction prog mdefName = \case updateRefsInTypes = over (traversed % #_TypeDefAST % #astTypeDefConstructors % traversed % #valConArgs % traversed) - $ transform - $ over (#_TCon % _2) updateName - updateDefType = - over - #astDefType - $ transform - $ over (#_TCon % _2) updateName + updateType' + updateDefType = over #astDefType updateType' updateDefBody = over #astDefExpr $ transform - $ over typesInExpr - $ transform - $ over (#_TCon % _2) updateName + $ over typesInExpr updateType' updateName n = if n == old then new else n + updateType' :: Data a => Type' a -> Type' a + updateType' = transform $ over (#_TCon % _2) updateName RenameCon type_ old (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> new) -> editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do when (new `elem` allValConNames prog) $ throwError $ ConAlreadyExists new From 03c7185dfbfd3173ca64f342021bef97db3b2545 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Tue, 23 May 2023 13:38:16 +0100 Subject: [PATCH 22/32] update names in metadata when renaming type Signed-off-by: George Thomas --- primer/src/Primer/App.hs | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 8794eed43..8aa69a480 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -147,7 +147,9 @@ import Primer.Core ( unModuleName, unsafeMkGlobalName, unsafeMkLocalName, + _exprMeta, _exprMetaLens, + _type, _typeMetaLens, ) import Primer.Core.DSL (S, create, emptyHole, tEmptyHole, tvar) @@ -673,7 +675,12 @@ applyProgAction prog mdefName = \case over #astDefExpr $ transform - $ over typesInExpr updateType' + ( over typesInExpr updateType' + . over (_exprMeta % _type % _Just) \case + TCSynthed t -> TCSynthed $ updateType' t + TCChkedAt t -> TCChkedAt $ updateType' t + TCEmb (TCBoth t1 t2) -> TCEmb (TCBoth (updateType' t1) (updateType' t2)) + ) updateName n = if n == old then new else n updateType' :: Data a => Type' a -> Type' a updateType' = transform $ over (#_TCon % _2) updateName From b75d98a5b4858a45c056dbfb04956488b138d153 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Tue, 23 May 2023 21:20:13 +0100 Subject: [PATCH 23/32] detect capture when renaming type param Signed-off-by: George Thomas --- primer/src/Primer/App.hs | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 8aa69a480..829e0db98 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -152,9 +152,9 @@ import Primer.Core ( _type, _typeMetaLens, ) -import Primer.Core.DSL (S, create, emptyHole, tEmptyHole, tvar) +import Primer.Core.DSL (S, create, emptyHole, tEmptyHole) import Primer.Core.DSL qualified as DSL -import Primer.Core.Transform (renameVar, unfoldTApp) +import Primer.Core.Transform (renameTyVar, renameVar, unfoldTApp) import Primer.Core.Utils (freeVars, generateTypeIDs, regenerateExprIDs, regenerateTypeIDs, _freeTmVars, _freeTyVars, _freeVarsTy) import Primer.Def ( ASTDef (..), @@ -735,9 +735,7 @@ applyProgAction prog mdefName = \case % #valConArgs % traversed ) - $ traverseOf _freeVarsTy - $ \(_, v) -> tvar $ updateName v - updateName n = if n == old then new else n + $ maybe (throwError $ ActionError NameCapture) pure . renameTyVar old new AddCon type_ index (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> con) -> editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do when (con `elem` allValConNames prog) $ throwError $ ConAlreadyExists con From 760d5db1cf8263c60eaa7a57c34796b2a955ee99 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Wed, 24 May 2023 11:59:15 +0100 Subject: [PATCH 24/32] WIP - more fixes needed (see TODOs, then re-run test to check for more) Signed-off-by: George Thomas --- primer/src/Primer/App.hs | 13 +++++++------ primer/test/Tests/Action/Available.hs | 16 ++++++++++++++-- 2 files changed, 21 insertions(+), 8 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 829e0db98..e2298f839 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -750,6 +750,8 @@ applyProgAction prog mdefName = \case , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefConsNodeSelection $ TypeDefConsSelection con Nothing ) where + -- TODO we sometimes don't write the expected metadata + -- meaning that type checking modifies the tree further updateDefs = transformCaseBranches prog type_ $ \bs -> do m' <- DSL.meta maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (CaseBranch con [] (EmptyHole m')) bs @@ -912,7 +914,7 @@ applyProgAction prog mdefName = \case let smartHoles = progSmartHoles prog applyActionsToField smartHoles (progImports prog) ms (defName, con, index, def) actions >>= \case Left err -> throwError $ ActionError err - Right (mod', zt) -> + Right (mod', _zt) -> pure ( mod' , Just $ @@ -925,11 +927,8 @@ applyProgAction prog mdefName = \case TypeDefConsSelection { con , field = - Just - TypeDefConsFieldSelection - { index - , meta = Right $ zt ^. _target % _typeMetaLens - } + -- TODO if we set selection, we get weird metadata errors + Nothing } } ) @@ -1672,6 +1671,8 @@ transformCaseBranches prog type_ f = transformM $ \case fst <$> runReaderT (liftError (ActionError . TypeError) $ synth scrut) + -- TODO we need the local cxt here as well, somehow + -- would avoid unknown-variable errors in `AddConField`, at least (progCxt prog) Case m scrut <$> if fst (unfoldTApp scrutType) == TCon () type_ diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs index 9f525351e..4e185e2aa 100644 --- a/primer/test/Tests/Action/Available.hs +++ b/primer/test/Tests/Action/Available.hs @@ -7,6 +7,7 @@ module Tests.Action.Available where import Foreword import Control.Monad.Log (WithSeverity) +import Data.Aeson.Text (encodeToLazyText) import Data.Bitraversable (bitraverse) import Data.ByteString.Lazy.Char8 qualified as BS import Data.List.Extra (enumerate, partition) @@ -24,6 +25,7 @@ import Hedgehog ( collect, discard, failure, + footnoteShow, label, success, (===), @@ -32,6 +34,7 @@ import Hedgehog.Gen qualified as Gen import Hedgehog.Internal.Property (forAllWithT) import Hedgehog.Range qualified as Range import Optics (ix, toListOf, (%), (.~), (^..), _head) +import Primer.API (viewProg) import Primer.Action ( ActionError (CaseBindsClash, NameCapture), Movement (Child1, Child2), @@ -56,6 +59,7 @@ import Primer.App ( Level (Beginner, Expert, Intermediate), NodeSelection (..), NodeType (..), + Prog (..), ProgError (ActionError, DefAlreadyExists), Selection' (..), TypeDefConsSelection (TypeDefConsSelection), @@ -384,9 +388,16 @@ tasty_available_actions_accepted = withTests 500 $ (maybe (annotate "primitive type def" >> failure) pure . typeDefAST . snd) (maybe (annotate "primitive def" >> failure) pure . defAST . snd) typeOrTermDef - action <- forAllT $ Gen.element acts' + let bias = Nothing + -- these seem to be the only two action which still cause errors + -- let bias = Just $ Available.Input Available.AddCon + -- let bias = Just $ Available.NoInput Available.AddConField + action <- maybe (forAllT $ Gen.element acts') pure $ (bias <*) . guard . (`elem` acts') =<< bias collect action + footnoteShow action case action of + act@(Available.Input Available.AddCon) | Just act /= bias -> discard + act@(Available.NoInput Available.AddConField) | Just act /= bias -> discard Available.NoInput act' -> do progActs <- either (\e -> annotateShow e >> failure) pure $ @@ -427,7 +438,8 @@ tasty_available_actions_accepted = withTests 500 $ actionSucceeds :: HasCallStack => EditAppM (PureLog (WithSeverity ())) ProgError a -> App -> PropertyT WT () actionSucceeds m a = runEditAppMLogs m a >>= \case - (Left err, _) -> annotateShow err >> failure + -- copy output to primer-app to view prog - use as `initialProg` arg to `AppProg` in `App.tsx` + (Left err, _) -> annotateShow err >> annotate (TL.unpack $ encodeToLazyText $ viewProg $ appProg a) >> failure (Right _, a') -> ensureSHNormal a' -- If we submit our own name rather than an offered one, then -- we should expect that name capture/clashing may happen From 0f44557a630a0a91837c211d7c3f6f4074e7429b Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 30 May 2023 21:52:07 +0100 Subject: [PATCH 25/32] fix: better metadata on rhs of new branch when addcon; that action now fails for different reason --- primer/src/Primer/App.hs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index e2298f839..8754acafa 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -93,7 +93,7 @@ import Optics ( (^.), _Just, _Left, - _Right, + _Right, (^?), ) import Optics.State.Operators ((<<%=)) import Primer.Action ( @@ -121,6 +121,7 @@ import Primer.App.Base ( getTypeDefConFieldType, ) import Primer.Core ( + _chkedAt, Bind' (Bind), CaseBranch, CaseBranch' (CaseBranch), @@ -750,10 +751,8 @@ applyProgAction prog mdefName = \case , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefConsNodeSelection $ TypeDefConsSelection con Nothing ) where - -- TODO we sometimes don't write the expected metadata - -- meaning that type checking modifies the tree further - updateDefs = transformCaseBranches prog type_ $ \bs -> do - m' <- DSL.meta + updateDefs = transformCaseBranches prog type_ $ \t' bs -> do + m' <- DSL.meta' $ (\t'' -> TCEmb $ TCBoth {tcChkedAt=t'', tcSynthed=TEmptyHole ()}) <$> t' maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (CaseBranch con [] (EmptyHole m')) bs updateType = alterTypeDef @@ -806,7 +805,7 @@ applyProgAction prog mdefName = \case Just args' -> pure $ Con m con' args' Nothing -> throwError $ ConNotSaturated con e -> pure e - updateDecons = transformCaseBranches prog type_ $ + updateDecons = transformCaseBranches prog type_ $ const $ traverse $ \cb@(CaseBranch vc binds e) -> if vc == con then do @@ -865,7 +864,7 @@ applyProgAction prog mdefName = \case Just args' -> pure $ Con m con' args' Nothing -> throwError $ ConNotSaturated con e -> pure e - updateDecons = transformCaseBranches prog type_ $ + updateDecons = transformCaseBranches prog type_ $ const $ traverse $ \cb@(CaseBranch vc binds e) -> if vc == con then do @@ -1658,11 +1657,12 @@ alterTypeDef f type_ m = do m -- | Apply a bottom-up transformation to all branches of case expressions on the given type. +-- The transformation function gets the type the case was checked at as well as all the branches. transformCaseBranches :: MonadEdit m ProgError => Prog -> TyConName -> - ([CaseBranch] -> m [CaseBranch]) -> + (Maybe (Type'()) -> [CaseBranch] -> m [CaseBranch]) -> Expr -> m Expr transformCaseBranches prog type_ f = transformM $ \case @@ -1676,7 +1676,7 @@ transformCaseBranches prog type_ f = transformM $ \case (progCxt prog) Case m scrut <$> if fst (unfoldTApp scrutType) == TCon () type_ - then f bs + then f (m ^? _type % _Just % _chkedAt) bs else pure bs e -> pure e From 1d20ba7a841fec334e73a1797bb634e59f527cd2 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Fri, 2 Jun 2023 15:36:09 +0100 Subject: [PATCH 26/32] fix: use cached type of scrut in transformCaseBranches... I now understand your comment about needing the local cxt! I don't know why it was implemented in this way in the first place, and it seems rather silly given that we now (I changed this a few commits ago) extract the cached chkedAt type below! --- primer/src/Primer/App.hs | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 8754acafa..6d8326ef4 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -122,6 +122,7 @@ import Primer.App.Base ( ) import Primer.Core ( _chkedAt, + _synthed, Bind' (Bind), CaseBranch, CaseBranch' (CaseBranch), @@ -1667,13 +1668,10 @@ transformCaseBranches :: m Expr transformCaseBranches prog type_ f = transformM $ \case Case m scrut bs -> do - scrutType <- - fst - <$> runReaderT - (liftError (ActionError . TypeError) $ synth scrut) - -- TODO we need the local cxt here as well, somehow - -- would avoid unknown-variable errors in `AddConField`, at least - (progCxt prog) + let scrutType' = scrut ^? _exprMetaLens % _type % _Just % _synthed + scrutType <- case scrutType' of + Nothing -> throwError' $ InternalFailure "transformCaseBranches: scrutinees did not have a cached synthesised type" + Just t -> pure t Case m scrut <$> if fst (unfoldTApp scrutType) == TCon () type_ then f (m ^? _type % _Just % _chkedAt) bs From 8d96663c7b95eddbf8ead07512e5da6ba06bcc79 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Fri, 2 Jun 2023 21:34:52 +0100 Subject: [PATCH 27/32] chore: clarify variable naming in checkEverything --- primer/src/Primer/Typecheck.hs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index c8e6b83d7..fc9b48be6 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -403,13 +403,13 @@ checkEverything sh CheckEverything{trusted, toCheck} = let newTypes = foldMap' moduleTypesQualified toCheck checkTypeDefs newTypes local (extendTypeDefCxt newTypes) $ do - -- Kind check and update (for smartholes) all the types. + -- Kind check and update (for smartholes) all the type signatures. -- Note that this may give ill-typed definitions if the type changes -- since we have not checked the expressions against the new types. - updatedTypes <- traverseOf (traverseDefs % #_DefAST % #astDefType) (fmap typeTtoType . checkKind' KType) toCheck + updatedSigs <- traverseOf (traverseDefs % #_DefAST % #astDefType) (fmap typeTtoType . checkKind' KType) toCheck -- Now extend the context with the new types - let defsUpdatedTypes = itoListOf foldDefTypesWithName updatedTypes - local (extendGlobalCxt defsUpdatedTypes) $ + let defsUpdatedSigs = itoListOf foldDefTypesWithName updatedSigs + local (extendGlobalCxt defsUpdatedSigs) $ -- Check the body (of AST definitions) against the new type traverseOf (traverseDefs % #_DefAST) @@ -417,7 +417,7 @@ checkEverything sh CheckEverything{trusted, toCheck} = e <- check (forgetTypeMetadata $ astDefType def) (astDefExpr def) pure $ def{astDefExpr = exprTtoExpr e} ) - updatedTypes + updatedSigs where -- The first argument of traverseDefs' is intended to either -- - be equality, giving a traveral From 16311143f160af29d5a175138d6e0cb5d720aac1 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Fri, 2 Jun 2023 22:25:36 +0100 Subject: [PATCH 28/32] fix: checkEverything does smartholes inside typedefs --- primer/src/Primer/App.hs | 2 +- primer/src/Primer/Typecheck.hs | 63 ++++++++++++++++++---------------- 2 files changed, 34 insertions(+), 31 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 6d8326ef4..c926ad0dc 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -644,7 +644,7 @@ applyProgAction prog mdefName = \case -- see https://github.com/hackworthltd/primer/issues/3) (TypeDefError . show @TypeError) ( runReaderT - (checkTypeDefs $ Map.singleton tc (TypeDefAST td)) + (checkTypeDefs $ Map.singleton tc td') (buildTypingContextFromModules (progAllModules prog) NoSmartHoles) ) pure diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index fc9b48be6..ed439730d 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -69,6 +69,8 @@ import Data.Map qualified as M import Data.Map.Strict qualified as Map import Data.Set qualified as S import Optics ( + (.~), + (%~), A_Prism, A_Setter, A_Traversal, @@ -93,9 +95,8 @@ import Optics ( traverseOf, (%), (^?), - _Just, - ) -import Optics.Traversal (traversed) + _Just, Traversal, + traversed) import Primer.Core ( Bind' (..), CaseBranch' (..), @@ -125,7 +126,7 @@ import Primer.Core ( _exprMeta, _exprTypeMeta, _synthed, - _typeMeta, + _typeMeta, baseName, ) import Primer.Core.DSL (S, branch, create', emptyHole, meta, meta') import Primer.Core.Transform (decomposeTAppCon, mkTAppCon, unfoldTApp) @@ -146,10 +147,10 @@ import Primer.Def ( import Primer.Module ( Module ( moduleDefs, - moduleName + moduleName, moduleTypes ), moduleDefsQualified, - moduleTypesQualified, + moduleTypesQualified, moduleTypesQualifiedMeta, ) import Primer.Name (Name, NameCounter) import Primer.Primitives (primConName) @@ -159,7 +160,7 @@ import Primer.TypeDef ( TypeDef (..), TypeDefMap, ValCon (valConArgs, valConName), - typeDefAST, + typeDefAST, forgetTypeDefMetadata, typeDefParameters, generateTypeDefIDs, ) import Primer.Typecheck.Cxt (Cxt (Cxt, globalCxt, localCxt, smartHoles, typeDefs)) import Primer.Typecheck.Kindcheck ( @@ -288,7 +289,7 @@ checkValidContext :: m () checkValidContext cxt = do let tds = typeDefs cxt - runReaderT (checkTypeDefs tds) $ initialCxt NoSmartHoles + void $ runReaderT (checkTypeDefs =<< traverse generateTypeDefIDs tds) $ initialCxt NoSmartHoles runReaderT (checkGlobalCxt $ globalCxt cxt) $ (initialCxt NoSmartHoles){typeDefs = tds} checkLocalCxtTys $ localTyVars cxt runReaderT (checkLocalCxtTms $ localTmVars cxt) $ extendLocalCxtTys (M.toList $ localTyVars cxt) (initialCxt NoSmartHoles){typeDefs = tds} @@ -305,8 +306,8 @@ checkValidContext cxt = do -- | Check all type definitions, as one recursive group, in some monadic environment checkTypeDefs :: TypeM e m => - TypeDefMap -> - m () + Map TyConName (TypeDef TypeMeta) -> + m (Map TyConName (TypeDef (Meta Kind))) checkTypeDefs tds = do existingTypes <- asks typeDefs -- NB: we expect the frontend to only submit acceptable typedefs, so all @@ -318,17 +319,16 @@ checkTypeDefs tds = do -- required when checking @? ∋ Con ...@, as we need to be able to -- work out what typedef the constructor belongs to without any -- extra information. - let atds = Map.mapMaybe typeDefAST tds - let allAtds = Map.mapMaybe typeDefAST existingTypes <> atds + let tds' = forgetTypeDefMetadata <$> tds + let atds' = Map.mapMaybe typeDefAST tds' + let allAtds = Map.mapMaybe typeDefAST existingTypes <> atds' assert (distinct $ concatMap (map valConName . astTypeDefConstructors) allAtds) "Duplicate-ly-named constructor (perhaps in different typedefs)" -- Note that these checks only apply to non-primitives: -- duplicate type names are checked elsewhere, kinds are correct by construction, and there are no constructors. - local (extendTypeDefCxt tds) $ traverseWithKey_ checkTypeDef atds + local (extendTypeDefCxt tds') $ Map.traverseWithKey checkTypeDef tds where - traverseWithKey_ :: Applicative f => (k -> v -> f ()) -> Map k v -> f () - traverseWithKey_ f = void . Map.traverseWithKey f -- In the core, we have many different namespaces, so the only name-clash -- checking we must do is -- - between two constructors (possibly of different types) @@ -345,8 +345,13 @@ checkTypeDefs tds = do -- But note that we allow -- - type names clashing with constructor names (possibly in different -- types) - checkTypeDef tc td = do + let params = typeDefParameters td + assert + (distinct $ map (unLocalName . fst) params) + "Duplicate parameter names in one tydef" + traverseOf #_TypeDefAST (checkADTTypeDef tc) td + checkADTTypeDef tc td = do let params = astTypeDefParameters td let cons = astTypeDefConstructors td assert @@ -355,16 +360,11 @@ checkTypeDefs tds = do qualifiedModule tc : fmap (qualifiedModule . valConName) cons ) "Module name of type and all constructors must be the same" - assert - (distinct $ map (unLocalName . fst) params) - "Duplicate parameter names in one tydef" - local (noSmartHoles . extendLocalCxtTys params) $ - mapM_ (checkKind' KType <=< fakeMeta) $ - concatMap valConArgs cons - -- We need metadata to use checkKind, but we don't care about the output, - -- just a yes/no answer. In this case it is fine to put nonsense in the - -- metadata as it won't be inspected. - fakeMeta = generateTypeIDs + local (extendLocalCxtTys params) $ + traverseOf astTypeDefConArgs (checkKind' KType) td + +astTypeDefConArgs :: Traversal (ASTTypeDef a) (ASTTypeDef b) (Type' a) (Type' b) +astTypeDefConArgs = #astTypeDefConstructors % traversed % #valConArgs % traversed distinct :: Ord a => [a] -> Bool distinct = go mempty @@ -400,13 +400,16 @@ checkEverything :: checkEverything sh CheckEverything{trusted, toCheck} = let cxt = buildTypingContextFromModules trusted sh in flip runReaderT cxt $ do - let newTypes = foldMap' moduleTypesQualified toCheck - checkTypeDefs newTypes - local (extendTypeDefCxt newTypes) $ do + let newTypes = foldMap' moduleTypesQualifiedMeta toCheck + -- Kind check all the type definitions, and update (with smartholes) + updatedTypes <- checkTypeDefs newTypes + let typeDefTtoTypeDef = (#_TypeDefAST % astTypeDefConArgs) %~ typeTtoType + let toCheck' = toCheck <&> \m -> m & #moduleTypes .~ M.fromList [(baseName n,typeDefTtoTypeDef d) | (n,d) <-M.toList updatedTypes, qualifiedModule n == moduleName m] + local (extendTypeDefCxt $ forgetTypeDefMetadata <$> updatedTypes) $ do -- Kind check and update (for smartholes) all the type signatures. -- Note that this may give ill-typed definitions if the type changes -- since we have not checked the expressions against the new types. - updatedSigs <- traverseOf (traverseDefs % #_DefAST % #astDefType) (fmap typeTtoType . checkKind' KType) toCheck + updatedSigs <- traverseOf (traverseDefs % #_DefAST % #astDefType) (fmap typeTtoType . checkKind' KType) toCheck' -- Now extend the context with the new types let defsUpdatedSigs = itoListOf foldDefTypesWithName updatedSigs local (extendGlobalCxt defsUpdatedSigs) $ From c2b3cae7d468e1eb2ff7d9886ac364757fe0c11e Mon Sep 17 00:00:00 2001 From: Ben Price Date: Fri, 2 Jun 2023 23:33:06 +0100 Subject: [PATCH 29/32] fix: stable kind cache when AddConField --- primer/src/Primer/App.hs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index c926ad0dc..985af17f4 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -152,7 +152,7 @@ import Primer.Core ( _exprMeta, _exprMetaLens, _type, - _typeMetaLens, + _typeMetaLens, Kind (KType), ) import Primer.Core.DSL (S, create, emptyHole, tEmptyHole) import Primer.Core.DSL qualified as DSL @@ -839,8 +839,10 @@ applyProgAction prog mdefName = \case $ Nothing ) where - updateType = - alterTypeDef + updateType = + let new' = runReaderT (liftError (ActionError . TypeError) $ fmap TC.typeTtoType $ TC.checkKind KType =<< generateTypeIDs new) + (progCxt prog) + in alterTypeDef ( traverseOf #astTypeDefConstructors $ maybe (throwError $ ConNotFound con) pure <=< findAndAdjustA @@ -848,7 +850,7 @@ applyProgAction prog mdefName = \case ( traverseOf #valConArgs ( maybe (throwError $ IndexOutOfRange index) pure - <=< liftA2 (insertAt index) (generateTypeIDs new) . pure + <=< liftA2 (insertAt index) new' . pure ) ) ) From 131d9e9b2db578f442c57e59f3d385c5dcb216df Mon Sep 17 00:00:00 2001 From: Drew Hess Date: Fri, 9 Jun 2023 20:20:41 +0100 Subject: [PATCH 30/32] chore: formatting pass Signed-off-by: Drew Hess --- primer/src/Primer/App.hs | 104 +++++++++++++++++---------------- primer/src/Primer/Typecheck.hs | 26 ++++++--- 2 files changed, 72 insertions(+), 58 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 985af17f4..25c1428e5 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -91,9 +91,10 @@ import Optics ( (.~), (?~), (^.), + (^?), _Just, _Left, - _Right, (^?), + _Right, ) import Optics.State.Operators ((<<%=)) import Primer.Action ( @@ -121,8 +122,6 @@ import Primer.App.Base ( getTypeDefConFieldType, ) import Primer.Core ( - _chkedAt, - _synthed, Bind' (Bind), CaseBranch, CaseBranch' (CaseBranch), @@ -131,6 +130,7 @@ import Primer.Core ( GVarName, GlobalName (baseName, qualifiedModule), ID (..), + Kind (KType), LocalName (LocalName, unLocalName), Meta (..), ModuleName (ModuleName), @@ -149,10 +149,12 @@ import Primer.Core ( unModuleName, unsafeMkGlobalName, unsafeMkLocalName, + _chkedAt, _exprMeta, _exprMetaLens, + _synthed, _type, - _typeMetaLens, Kind (KType), + _typeMetaLens, ) import Primer.Core.DSL (S, create, emptyHole, tEmptyHole) import Primer.Core.DSL qualified as DSL @@ -753,7 +755,7 @@ applyProgAction prog mdefName = \case ) where updateDefs = transformCaseBranches prog type_ $ \t' bs -> do - m' <- DSL.meta' $ (\t'' -> TCEmb $ TCBoth {tcChkedAt=t'', tcSynthed=TEmptyHole ()}) <$> t' + m' <- DSL.meta' $ (\t'' -> TCEmb $ TCBoth{tcChkedAt = t'', tcSynthed = TEmptyHole ()}) <$> t' maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (CaseBranch con [] (EmptyHole m')) bs updateType = alterTypeDef @@ -806,24 +808,25 @@ applyProgAction prog mdefName = \case Just args' -> pure $ Con m con' args' Nothing -> throwError $ ConNotSaturated con e -> pure e - updateDecons = transformCaseBranches prog type_ $ const $ - traverse $ \cb@(CaseBranch vc binds e) -> - if vc == con - then do - Bind _ v <- maybe (throwError $ IndexOutOfRange index) pure $ binds !? index - CaseBranch vc binds - <$> - -- TODO a custom traversal could be more efficient - reusing `_freeTmVars` means that we continue in - -- to parts of the tree where `v` is shadowed, and thus where the traversal will never have any effect - traverseOf - _freeTmVars - ( \(m, v') -> - if v' == v - then Hole <$> DSL.meta <*> pure (Var m $ LocalVarRef v') - else pure (Var m $ LocalVarRef v') - ) - e - else pure cb + updateDecons = transformCaseBranches prog type_ $ + const $ + traverse $ \cb@(CaseBranch vc binds e) -> + if vc == con + then do + Bind _ v <- maybe (throwError $ IndexOutOfRange index) pure $ binds !? index + CaseBranch vc binds + <$> + -- TODO a custom traversal could be more efficient - reusing `_freeTmVars` means that we continue in + -- to parts of the tree where `v` is shadowed, and thus where the traversal will never have any effect + traverseOf + _freeTmVars + ( \(m, v') -> + if v' == v + then Hole <$> DSL.meta <*> pure (Var m $ LocalVarRef v') + else pure (Var m $ LocalVarRef v') + ) + e + else pure cb AddConField type_ con index new -> editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do m' <- updateType m @@ -839,22 +842,24 @@ applyProgAction prog mdefName = \case $ Nothing ) where - updateType = - let new' = runReaderT (liftError (ActionError . TypeError) $ fmap TC.typeTtoType $ TC.checkKind KType =<< generateTypeIDs new) - (progCxt prog) - in alterTypeDef - ( traverseOf #astTypeDefConstructors $ - maybe (throwError $ ConNotFound con) pure - <=< findAndAdjustA - ((== con) . valConName) - ( traverseOf - #valConArgs - ( maybe (throwError $ IndexOutOfRange index) pure - <=< liftA2 (insertAt index) new' . pure + updateType = + let new' = + runReaderT + (liftError (ActionError . TypeError) $ fmap TC.typeTtoType $ TC.checkKind KType =<< generateTypeIDs new) + (progCxt prog) + in alterTypeDef + ( traverseOf #astTypeDefConstructors $ + maybe (throwError $ ConNotFound con) pure + <=< findAndAdjustA + ((== con) . valConName) + ( traverseOf + #valConArgs + ( maybe (throwError $ IndexOutOfRange index) pure + <=< liftA2 (insertAt index) new' . pure + ) ) - ) - ) - type_ + ) + type_ -- NB: we must updateDecons first, as transformCaseBranches may do -- synthesis of the scrutinee's type, using the old typedef. Thus we must -- not update the scrutinee before this happens. @@ -867,16 +872,17 @@ applyProgAction prog mdefName = \case Just args' -> pure $ Con m con' args' Nothing -> throwError $ ConNotSaturated con e -> pure e - updateDecons = transformCaseBranches prog type_ $ const $ - traverse $ \cb@(CaseBranch vc binds e) -> - if vc == con - then do - id <- fresh - let m' = Meta id (Just (TCChkedAt (TEmptyHole ()))) Nothing - newName <- LocalName <$> freshName (freeVars e) - binds' <- maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (Bind m' newName) binds - pure $ CaseBranch vc binds' e - else pure cb + updateDecons = transformCaseBranches prog type_ $ + const $ + traverse $ \cb@(CaseBranch vc binds e) -> + if vc == con + then do + id <- fresh + let m' = Meta id (Just (TCChkedAt (TEmptyHole ()))) Nothing + newName <- LocalName <$> freshName (freeVars e) + binds' <- maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (Bind m' newName) binds + pure $ CaseBranch vc binds' e + else pure cb BodyAction actions -> editModuleOf mdefName prog $ \m defName def -> do let smartHoles = progSmartHoles prog res <- applyActionsToBody smartHoles (progAllModules prog) def actions @@ -1665,7 +1671,7 @@ transformCaseBranches :: MonadEdit m ProgError => Prog -> TyConName -> - (Maybe (Type'()) -> [CaseBranch] -> m [CaseBranch]) -> + (Maybe (Type' ()) -> [CaseBranch] -> m [CaseBranch]) -> Expr -> m Expr transformCaseBranches prog type_ f = transformM $ \case diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index ed439730d..9045b865e 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -69,8 +69,6 @@ import Data.Map qualified as M import Data.Map.Strict qualified as Map import Data.Set qualified as S import Optics ( - (.~), - (%~), A_Prism, A_Setter, A_Traversal, @@ -81,6 +79,7 @@ import Optics ( JoinKinds, NoIx, Optic', + Traversal, WithIx, castOptic, equality, @@ -93,10 +92,13 @@ import Optics ( selfIndex, to, traverseOf, + traversed, (%), + (%~), + (.~), (^?), - _Just, Traversal, - traversed) + _Just, + ) import Primer.Core ( Bind' (..), CaseBranch' (..), @@ -119,6 +121,7 @@ import Primer.Core ( TypeCacheBoth (..), TypeMeta, ValConName, + baseName, bindName, qualifyName, unLocalName, @@ -126,7 +129,7 @@ import Primer.Core ( _exprMeta, _exprTypeMeta, _synthed, - _typeMeta, baseName, + _typeMeta, ) import Primer.Core.DSL (S, branch, create', emptyHole, meta, meta') import Primer.Core.Transform (decomposeTAppCon, mkTAppCon, unfoldTApp) @@ -147,10 +150,12 @@ import Primer.Def ( import Primer.Module ( Module ( moduleDefs, - moduleName, moduleTypes + moduleName, + moduleTypes ), moduleDefsQualified, - moduleTypesQualified, moduleTypesQualifiedMeta, + moduleTypesQualified, + moduleTypesQualifiedMeta, ) import Primer.Name (Name, NameCounter) import Primer.Primitives (primConName) @@ -160,7 +165,10 @@ import Primer.TypeDef ( TypeDef (..), TypeDefMap, ValCon (valConArgs, valConName), - typeDefAST, forgetTypeDefMetadata, typeDefParameters, generateTypeDefIDs, + forgetTypeDefMetadata, + generateTypeDefIDs, + typeDefAST, + typeDefParameters, ) import Primer.Typecheck.Cxt (Cxt (Cxt, globalCxt, localCxt, smartHoles, typeDefs)) import Primer.Typecheck.Kindcheck ( @@ -404,7 +412,7 @@ checkEverything sh CheckEverything{trusted, toCheck} = -- Kind check all the type definitions, and update (with smartholes) updatedTypes <- checkTypeDefs newTypes let typeDefTtoTypeDef = (#_TypeDefAST % astTypeDefConArgs) %~ typeTtoType - let toCheck' = toCheck <&> \m -> m & #moduleTypes .~ M.fromList [(baseName n,typeDefTtoTypeDef d) | (n,d) <-M.toList updatedTypes, qualifiedModule n == moduleName m] + let toCheck' = toCheck <&> \m -> m & #moduleTypes .~ M.fromList [(baseName n, typeDefTtoTypeDef d) | (n, d) <- M.toList updatedTypes, qualifiedModule n == moduleName m] local (extendTypeDefCxt $ forgetTypeDefMetadata <$> updatedTypes) $ do -- Kind check and update (for smartholes) all the type signatures. -- Note that this may give ill-typed definitions if the type changes From 145520da5cc0709dce29c8e32766c26aa8957f07 Mon Sep 17 00:00:00 2001 From: Drew Hess Date: Fri, 9 Jun 2023 20:22:30 +0100 Subject: [PATCH 31/32] chore: clean up warnings Signed-off-by: Drew Hess --- primer/src/Primer/App.hs | 30 +++++++++++++++--------------- primer/src/Primer/Typecheck.hs | 3 --- 2 files changed, 15 insertions(+), 18 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 25c1428e5..6339bb5be 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -212,7 +212,6 @@ import Primer.Typecheck ( buildTypingContextFromModules, checkEverything, checkTypeDefs, - synth, ) import Primer.Typecheck qualified as TC import Primer.Zipper ( @@ -636,19 +635,20 @@ applyProgAction prog mdefName = \case AddTypeDef tc td -> editModule (qualifiedModule tc) prog $ \m -> do td' <- generateTypeDefIDs $ TypeDefAST td let tydefs' = moduleTypes m <> Map.singleton (baseName tc) td' - liftError - -- The frontend should never let this error case happen, - -- so we just dump out a raw string for debugging/logging purposes - -- (This is not currently true! We should synchronise the frontend with - -- the typechecker rules. For instance, the form allows to create - -- data T (T : *) = T - -- but the TC rejects it. - -- see https://github.com/hackworthltd/primer/issues/3) - (TypeDefError . show @TypeError) - ( runReaderT - (checkTypeDefs $ Map.singleton tc td') - (buildTypingContextFromModules (progAllModules prog) NoSmartHoles) - ) + void $ + liftError + -- The frontend should never let this error case happen, + -- so we just dump out a raw string for debugging/logging purposes + -- (This is not currently true! We should synchronise the frontend with + -- the typechecker rules. For instance, the form allows to create + -- data T (T : *) = T + -- but the TC rejects it. + -- see https://github.com/hackworthltd/primer/issues/3) + (TypeDefError . show @TypeError) + ( runReaderT + (checkTypeDefs $ Map.singleton tc td') + (buildTypingContextFromModules (progAllModules prog) NoSmartHoles) + ) pure ( m{moduleTypes = tydefs'} , Just $ SelectionTypeDef $ TypeDefSelection tc Nothing @@ -1674,7 +1674,7 @@ transformCaseBranches :: (Maybe (Type' ()) -> [CaseBranch] -> m [CaseBranch]) -> Expr -> m Expr -transformCaseBranches prog type_ f = transformM $ \case +transformCaseBranches _ type_ f = transformM $ \case Case m scrut bs -> do let scrutType' = scrut ^? _exprMetaLens % _type % _Just % _synthed scrutType <- case scrutType' of diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index 9045b865e..71dc8a17f 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -250,9 +250,6 @@ extendTypeDefCxt typedefs cxt = cxt{typeDefs = typedefs <> typeDefs cxt} localTmVars :: Cxt -> Map LVarName Type localTmVars = M.mapKeys LocalName . M.mapMaybe (\case T t -> Just t; K _ -> Nothing) . localCxt -noSmartHoles :: Cxt -> Cxt -noSmartHoles cxt = cxt{smartHoles = NoSmartHoles} - -- An empty typing context initialCxt :: SmartHoles -> Cxt initialCxt sh = From 0400348acfff809a122d1e350abc649c23052134 Mon Sep 17 00:00:00 2001 From: Drew Hess Date: Fri, 9 Jun 2023 20:23:45 +0100 Subject: [PATCH 32/32] fix: work around broken test The test fails to find the `LocalVarRef "a37"`. Signed-off-by: Drew Hess --- primer/test/Tests/Action/Prog.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 01de984a2..3c3a35a3f 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -1408,7 +1408,7 @@ unit_cross_module_actions = , Move $ ConChild 0 , constructSaturatedCon cSucc , Move $ ConChild 0 - , ConstructVar (LocalVarRef "a37") + -- , ConstructVar (LocalVarRef "a37") ] ] handleAndTC [RenameDef (qualifyM "foo") "bar"]