From 058b266eccba0a539f8956da15f4f877e4f3754b Mon Sep 17 00:00:00 2001 From: Ben Price Date: Wed, 20 Oct 2021 15:12:45 +0100 Subject: [PATCH 1/4] [primer] api: remove error wrapper on 'getProgram' This never fails. Let's expose that fact in the API. --- primer-service/src/Primer/Server.hs | 2 +- primer/src/Primer/API.hs | 4 ++-- primer/src/Primer/App.hs | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/primer-service/src/Primer/Server.hs b/primer-service/src/Primer/Server.hs index 019159f56..1074235c4 100644 --- a/primer-service/src/Primer/Server.hs +++ b/primer-service/src/Primer/Server.hs @@ -197,7 +197,7 @@ type SAPI = ( -- GET /api/program -- Get the current program state - "program" :> Get '[JSON] (Result ProgError Prog) + "program" :> Get '[JSON] Prog -- GET /api/session-name -- Get the current session name. diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index c92618ed9..b81459682 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -256,8 +256,8 @@ liftEditAppM h sid = withSession' sid (EditApp $ runEditAppM h) liftQueryAppM :: (MonadIO m, MonadThrow m) => QueryAppM a -> SessionId -> PrimerM m (Result ProgError a) liftQueryAppM h sid = withSession' sid (QueryApp $ runQueryAppM h) -getProgram :: (MonadIO m, MonadThrow m) => SessionId -> PrimerM m (Result ProgError Prog) -getProgram = liftQueryAppM handleGetProgramRequest +getProgram :: (MonadIO m, MonadThrow m) => SessionId -> PrimerM m Prog +getProgram sid = withSession' sid $ QueryApp handleGetProgramRequest edit :: (MonadIO m, MonadThrow m) => SessionId -> MutationRequest -> PrimerM m (Result ProgError Prog) edit sid req = liftEditAppM (handleMutationRequest req) sid diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 8055f8729..15afd124a 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -292,7 +292,7 @@ focusNode prog defid nodeid = Just x -> pure x -- | Handle a request to retrieve the current program -handleGetProgramRequest :: MonadQueryApp m => m Prog +handleGetProgramRequest :: MonadReader App m => m Prog handleGetProgramRequest = asks appProg -- | Handle a request to mutate the app state From a4f6e74e0cddcde671e39ec88b2b344948a0e58e Mon Sep 17 00:00:00 2001 From: Ben Price Date: Mon, 18 Oct 2021 17:09:00 +0100 Subject: [PATCH 2/4] First iteration of tree api --- primer-service/src/Primer/OpenAPI.hs | 8 ++ primer-service/src/Primer/Server.hs | 25 ++++-- primer/primer.cabal | 1 + primer/src/Primer/API.hs | 117 +++++++++++++++++++++++++-- primer/test/Tests/API.hs | 21 +++++ 5 files changed, 159 insertions(+), 13 deletions(-) create mode 100644 primer/test/Tests/API.hs diff --git a/primer-service/src/Primer/OpenAPI.hs b/primer-service/src/Primer/OpenAPI.hs index 1e0b13119..0a5ec9b92 100644 --- a/primer-service/src/Primer/OpenAPI.hs +++ b/primer-service/src/Primer/OpenAPI.hs @@ -6,8 +6,11 @@ module Primer.OpenAPI ( ) where import Data.OpenApi (ToSchema) +import Primer.API (Def, Prog, Tree) import Primer.App (InitialApp) +import Primer.Core (ID) import Primer.Database (Session, SessionName) +import Primer.Name (Name) -- $orphanInstances -- @@ -19,3 +22,8 @@ import Primer.Database (Session, SessionName) instance ToSchema SessionName instance ToSchema Session instance ToSchema InitialApp +instance ToSchema ID +instance ToSchema Name +instance ToSchema Tree +instance ToSchema Def +instance ToSchema Prog diff --git a/primer-service/src/Primer/Server.hs b/primer-service/src/Primer/Server.hs index 1074235c4..86ab21546 100644 --- a/primer-service/src/Primer/Server.hs +++ b/primer-service/src/Primer/Server.hs @@ -47,6 +47,7 @@ import Primer.API ( renameSession, variablesInScope, ) +import qualified Primer.API as API import Primer.Action ( Action (Move), ActionError (TypeError), @@ -162,7 +163,11 @@ type PrimerOpenAPI = :<|> QueryFlag "inMemory" :> "sessions" :> PaginationParams :> Summary "List sessions" :> - OpId "getSessionList" Get '[JSON] (Paginated Session)) + OpId "getSessionList" Get '[JSON] (Paginated Session) + + -- The rest of the API is scoped to a particular session + :<|> QueryParam' '[Required, Strict] "session" SessionId :> SOpenAPI + ) type PrimerLegacyAPI = "api" :> ( @@ -193,15 +198,19 @@ type PrimerLegacyAPI = :<|> Raw -- | The session-specific bits of the api -type SAPI = ( - +type SOpenAPI = ( -- GET /api/program -- Get the current program state - "program" :> Get '[JSON] Prog + "program" :> Get '[JSON] API.Prog + ) + +-- | The session-specific bits of the api +-- (legacy version) +type SAPI = ( -- GET /api/session-name -- Get the current session name. - :<|> "session-name" :> Get '[JSON] Text + "session-name" :> Get '[JSON] Text -- PUT /api/session-name -- Attempt to set the current session name. Returns the new @@ -370,13 +379,13 @@ primerServer = openAPIServer :<|> legacyServer where openAPIServer = newSession - :<|> \b p -> pagedDefaultClamp 100 p $ listSessions b + :<|> (\b p -> pagedDefaultClamp 100 p $ listSessions b) + :<|> getProgram legacyServer = ( copySession :<|> getVersion :<|> ( \sid -> - getProgram sid - :<|> getSessionName sid + getSessionName sid :<|> renameSession sid :<|> edit sid :<|> (variablesInScope sid :<|> generateNames sid) diff --git a/primer/primer.cabal b/primer/primer.cabal index bb6111696..9474db303 100644 --- a/primer/primer.cabal +++ b/primer/primer.cabal @@ -96,6 +96,7 @@ test-suite primer-test Tests.Action.Capture Tests.Action.Prog Tests.AlphaEquality + Tests.API Tests.Database Tests.Eval Tests.EvalFull diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index b81459682..93846ed85 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -19,6 +19,9 @@ module Primer.API ( copySession, listSessions, getVersion, + Tree, + Prog, + Def, getProgram, getSessionName, renameSession, @@ -28,6 +31,9 @@ module Primer.API ( evalStep, evalFull, flushSessions, + -- viewTree*: only exported for testing + viewTreeType, + viewTreeExpr, ) where import Foreword @@ -41,6 +47,10 @@ import Control.Concurrent.STM ( writeTBQueue, ) import Control.Monad.Catch (MonadThrow, throwM) +import Data.Aeson (ToJSON) +import Data.Data (showConstr, toConstr) +import qualified Data.Generics.Uniplate.Data as U +import qualified Data.Map as Map import qualified ListT (toList) import Primer.App ( App, @@ -51,7 +61,6 @@ import Primer.App ( EvalResp (..), InitialApp, MutationRequest, - Prog, ProgError, QueryAppM, Question (..), @@ -62,13 +71,25 @@ import Primer.App ( handleMutationRequest, handleQuestion, initialApp, + progDefs, + progTypes, runEditAppM, runQueryAppM, ) +import qualified Primer.App as App import Primer.Core ( + Expr, + Expr' (APP, Ann, Con, LetType, Letrec, Var), ID, Kind, - Type', + Type, + Type' (TCon, TVar), + defExpr, + defID, + defName, + defType, + getID, + typeDefName, ) import Primer.Database ( OffsetLimit, @@ -97,7 +118,7 @@ import qualified Primer.Database as Database ( Success ), ) -import Primer.Name (Name) +import Primer.Name (Name, unName) import qualified StmContainers.Map as StmMap data Env = Env @@ -257,9 +278,95 @@ liftQueryAppM :: (MonadIO m, MonadThrow m) => QueryAppM a -> SessionId -> Primer liftQueryAppM h sid = withSession' sid (QueryApp $ runQueryAppM h) getProgram :: (MonadIO m, MonadThrow m) => SessionId -> PrimerM m Prog -getProgram sid = withSession' sid $ QueryApp handleGetProgramRequest +getProgram sid = withSession' sid $ QueryApp $ viewProg . handleGetProgramRequest + +-- | A frontend will be mostly concerned with rendering, and does not need the +-- full complexity of our AST for that task. 'Tree' is a simplified view with +-- just enough information to render nicely. +-- (NB: currently this is just a first draft, and is expected to evolve.) +data Tree = Tree + { nodeId :: ID + , label :: Text + , childTrees :: [Tree] + } + deriving (Show, Eq, Generic) + +instance ToJSON Tree + +-- | This type is the API's view of a 'App.Prog' +-- (this is expected to evolve as we flesh out the API) +data Prog = Prog + { types :: [Name] + , -- We don't use Map ID Def, as the openapi instance of map is broken (goes + -- via list of pairs, and openapi3 cannot represent hetrogenous tuples!) + -- See https://github.com/biocad/openapi3/issues/31 + defs :: [Def] + } + deriving (Generic) + +instance ToJSON Prog + +-- | 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 + { id :: ID + , name :: Name + , type_ :: Tree + , term :: Tree + } + deriving (Generic) + +instance ToJSON Def + +viewProg :: App.Prog -> Prog +viewProg p = + Prog + { types = typeDefName <$> progTypes p + , defs = + ( \d -> + Def + { id = defID d + , name = defName d + , type_ = viewTreeType $ defType d + , term = viewTreeExpr $ defExpr d + } + ) + <$> Map.elems (progDefs p) + } + +-- | A simple method to extract 'Tree's from 'Expr's. This is injective. +-- Currently it is designed to be simple and just enough to enable +-- experimenting with rendering on the frontend. +-- +-- It is expected to evolve in the future. +viewTreeExpr :: Expr -> Tree +viewTreeExpr = U.para $ \e exprChildren -> + let c = toS $ showConstr $ toConstr e + n = case e of + Con _ n' -> c <> " " <> unName n' + Var _ n' -> c <> " " <> unName n' + _ -> c + -- add info about type children + allChildren = case e of + Ann _ _ ty -> exprChildren ++ [viewTreeType ty] + APP _ _ ty -> exprChildren ++ [viewTreeType ty] + LetType _ _ ty _ -> viewTreeType ty : exprChildren + Letrec _ _ _ ty _ -> let (h, t) = splitAt 1 exprChildren in h ++ viewTreeType ty : t + -- otherwise, no type children + _ -> exprChildren + in Tree (getID e) n allChildren + +-- | Similar to 'viewTreeExpr', but for 'Type's +viewTreeType :: Type -> Tree +viewTreeType = U.para $ \e allChildren -> + let c = toS $ showConstr $ toConstr e + n = case e of + TCon _ n' -> c <> " " <> unName n' + TVar _ n' -> c <> " " <> unName n' + _ -> c + in Tree (getID e) n allChildren -edit :: (MonadIO m, MonadThrow m) => SessionId -> MutationRequest -> PrimerM m (Result ProgError Prog) +edit :: (MonadIO m, MonadThrow m) => SessionId -> MutationRequest -> PrimerM m (Result ProgError App.Prog) edit sid req = liftEditAppM (handleMutationRequest req) sid variablesInScope :: (MonadIO m, MonadThrow m) => SessionId -> (ID, ID) -> PrimerM m (Result ProgError (([(Name, Kind)], [(Name, Type' ())]), [(ID, Name, Type' ())])) diff --git a/primer/test/Tests/API.hs b/primer/test/Tests/API.hs new file mode 100644 index 000000000..4b5a59f5c --- /dev/null +++ b/primer/test/Tests/API.hs @@ -0,0 +1,21 @@ +module Tests.API where + +import Foreword + +import Gen.Core.Raw (evalExprGen, genExpr, genType) +import Hedgehog +import Primer.API (viewTreeExpr, viewTreeType) + +hprop_viewTreeExpr_injective :: Property +hprop_viewTreeExpr_injective = property $ do + e1 <- forAll $ evalExprGen 0 genExpr + e2 <- forAll $ evalExprGen 0 genExpr + when (e1 == e2) discard + viewTreeExpr e1 /== viewTreeExpr e2 + +hprop_viewTreeType_injective :: Property +hprop_viewTreeType_injective = property $ do + t1 <- forAll $ evalExprGen 0 genType + t2 <- forAll $ evalExprGen 0 genType + when (t1 == t2) discard + viewTreeType t1 /== viewTreeType t2 From af584b09708f559ce36d720a00432e47e952a47e Mon Sep 17 00:00:00 2001 From: Ben Price Date: Wed, 20 Oct 2021 14:43:27 +0100 Subject: [PATCH 3/4] Change API to serialize IDs and Names plainly i.e. we now have '1' and '"foo"' instead of '{unID:1}' and '{unName:"foo"}' Almost all of this commit is testcase churn because of this change.` The change to ToJSONKey enables us to output 'Map ID _' from our API (whilst having correct OpenAPI3 documentation), since the map will be serialized as an object, where the keys are 'show' of the IDs. However, we decide to keep our list-based representation, as documented in a comment. Note that this only applies to the "new api", and not to the serialization test fixtures. --- primer-service/src/Primer/OpenAPI.hs | 14 +- primer/src/Primer/API.hs | 9 +- primer/src/Primer/Core.hs | 7 +- primer/src/Primer/Name.hs | 2 +- primer/test/outputs/serialization/action.json | 4 +- .../outputs/serialization/actionerror.json | 4 +- primer/test/outputs/serialization/def.json | 16 +-- .../serialization/edit_response_1.json | 4 +- .../serialization/edit_response_2.json | 121 ++++++------------ primer/test/outputs/serialization/expr.json | 4 +- primer/test/outputs/serialization/id.json | 4 +- primer/test/outputs/serialization/name.json | 4 +- primer/test/outputs/serialization/prog.json | 121 ++++++------------ .../outputs/serialization/progaction.json | 4 +- .../test/outputs/serialization/selection.json | 24 +--- primer/test/outputs/serialization/type.json | 4 +- .../test/outputs/serialization/typeDef.json | 28 +--- 17 files changed, 127 insertions(+), 247 deletions(-) diff --git a/primer-service/src/Primer/OpenAPI.hs b/primer-service/src/Primer/OpenAPI.hs index 0a5ec9b92..0ce92959b 100644 --- a/primer-service/src/Primer/OpenAPI.hs +++ b/primer-service/src/Primer/OpenAPI.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE StandaloneDeriving #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Primer.OpenAPI ( @@ -6,9 +7,10 @@ module Primer.OpenAPI ( ) where import Data.OpenApi (ToSchema) +import Data.Text (Text) import Primer.API (Def, Prog, Tree) import Primer.App (InitialApp) -import Primer.Core (ID) +import Primer.Core (ID (..)) import Primer.Database (Session, SessionName) import Primer.Name (Name) @@ -22,8 +24,14 @@ import Primer.Name (Name) instance ToSchema SessionName instance ToSchema Session instance ToSchema InitialApp -instance ToSchema ID -instance ToSchema Name + +-- We need to GND the ID instance to match its To/FromJSON instances +deriving newtype instance ToSchema ID + +-- We can't GND derive for Name as it is an opaque type +-- But the JSON instance is done by GND, so we must match here... +-- This instance works because the parameter has a phantom role! +deriving via Text instance (ToSchema Name) instance ToSchema Tree instance ToSchema Def instance ToSchema Prog diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index 93846ed85..266366eea 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -297,9 +297,12 @@ instance ToJSON Tree -- (this is expected to evolve as we flesh out the API) data Prog = Prog { types :: [Name] - , -- We don't use Map ID Def, as the openapi instance of map is broken (goes - -- via list of pairs, and openapi3 cannot represent hetrogenous tuples!) - -- See https://github.com/biocad/openapi3/issues/31 + , -- We don't use Map ID Def, as the JSON encoding would be as an object, + -- where keys are IDs converted to strings and we have no nice way of + -- saying "all the keys of this object should parse as numbers". Similarly, + -- it is rather redundant as each Def carries a defID field (which is + -- encoded as a number), and it is difficult to enforce that "the keys of + -- this object match the defID field of the corresponding value". defs :: [Def] } deriving (Generic) diff --git a/primer/src/Primer/Core.hs b/primer/src/Primer/Core.hs index 644a208ab..5fc695056 100644 --- a/primer/src/Primer/Core.hs +++ b/primer/src/Primer/Core.hs @@ -64,11 +64,8 @@ newtype ID = ID {unID :: Int} -- The Ord and Enum instances are useful for tests but we may remove them in -- future, so don't use them in app code. deriving newtype (Show, Num, Ord, Enum) - deriving (FromJSON, ToJSON) via VJSON ID - -instance ToJSONKey ID - -instance FromJSONKey ID + deriving newtype (FromJSON, ToJSON) + deriving newtype (ToJSONKey, FromJSONKey) data Meta a = Meta ID a (Maybe Value) deriving (Generic, Eq, Show, Data, Functor) diff --git a/primer/src/Primer/Name.hs b/primer/src/Primer/Name.hs index 1c2ec2804..654a73af5 100644 --- a/primer/src/Primer/Name.hs +++ b/primer/src/Primer/Name.hs @@ -23,7 +23,7 @@ import Primer.JSON newtype Name = Name {unName :: Text} deriving (Eq, Ord, Generic, Data) deriving newtype (Show, IsString) - deriving (FromJSON, ToJSON) via VJSON Name + deriving newtype (FromJSON, ToJSON) -- | Construct a name from a Text. This is called unsafe because there are no -- guarantees about whether the name refers to anything that is in scope. diff --git a/primer/test/outputs/serialization/action.json b/primer/test/outputs/serialization/action.json index 0b8adf0e5..834c280fd 100644 --- a/primer/test/outputs/serialization/action.json +++ b/primer/test/outputs/serialization/action.json @@ -1,6 +1,4 @@ { - "contents": { - "unID": 0 - }, + "contents": 0, "tag": "SetCursor" } \ No newline at end of file diff --git a/primer/test/outputs/serialization/actionerror.json b/primer/test/outputs/serialization/actionerror.json index 610d019f0..26e8a96a3 100644 --- a/primer/test/outputs/serialization/actionerror.json +++ b/primer/test/outputs/serialization/actionerror.json @@ -1,6 +1,4 @@ { - "contents": { - "unID": 0 - }, + "contents": 0, "tag": "IDNotFound" } \ No newline at end of file diff --git a/primer/test/outputs/serialization/def.json b/primer/test/outputs/serialization/def.json index 26497389a..19c3eb0e4 100644 --- a/primer/test/outputs/serialization/def.json +++ b/primer/test/outputs/serialization/def.json @@ -1,9 +1,7 @@ { "defExpr": { "contents": [ - { - "unID": 0 - }, + 0, { "contents": { "contents": [], @@ -15,17 +13,11 @@ ], "tag": "EmptyHole" }, - "defID": { - "unID": 1 - }, - "defName": { - "unName": "main" - }, + "defID": 1, + "defName": "main", "defType": { "contents": [ - { - "unID": 0 - }, + 0, { "tag": "KType" }, diff --git a/primer/test/outputs/serialization/edit_response_1.json b/primer/test/outputs/serialization/edit_response_1.json index 8d5bee8ca..fc4a18aa6 100644 --- a/primer/test/outputs/serialization/edit_response_1.json +++ b/primer/test/outputs/serialization/edit_response_1.json @@ -1,8 +1,6 @@ { "contents": { - "contents": { - "unID": 0 - }, + "contents": 0, "tag": "IDNotFound" }, "tag": "Error" diff --git a/primer/test/outputs/serialization/edit_response_2.json b/primer/test/outputs/serialization/edit_response_2.json index 7b6fbdea0..88076147a 100644 --- a/primer/test/outputs/serialization/edit_response_2.json +++ b/primer/test/outputs/serialization/edit_response_2.json @@ -1,48 +1,35 @@ { "contents": { - "progDefs": [ - [ - { - "unID": 1 - }, - { - "defExpr": { - "contents": [ - { - "unID": 0 - }, - { - "contents": { - "contents": [], - "tag": "TEmptyHole" - }, - "tag": "TCSynthed" - }, - null - ], - "tag": "EmptyHole" - }, - "defID": { - "unID": 1 - }, - "defName": { - "unName": "main" - }, - "defType": { - "contents": [ - { - "unID": 0 - }, - { - "tag": "KType" + "progDefs": { + "1": { + "defExpr": { + "contents": [ + 0, + { + "contents": { + "contents": [], + "tag": "TEmptyHole" }, - null - ], - "tag": "TEmptyHole" - } + "tag": "TCSynthed" + }, + null + ], + "tag": "EmptyHole" + }, + "defID": 1, + "defName": "main", + "defType": { + "contents": [ + 0, + { + "tag": "KType" + }, + null + ], + "tag": "TEmptyHole" } - ] - ], + } + }, "progLog": { "unlog": [ [ @@ -64,9 +51,7 @@ "selectedDef": { "defExpr": { "contents": [ - { - "unID": 0 - }, + 0, { "contents": { "contents": [], @@ -78,17 +63,11 @@ ], "tag": "EmptyHole" }, - "defID": { - "unID": 1 - }, - "defName": { - "unName": "main" - }, + "defID": 1, + "defName": "main", "defType": { "contents": [ - { - "unID": 0 - }, + 0, { "tag": "KType" }, @@ -100,9 +79,7 @@ "selectedNode": { "meta": { "Left": [ - { - "unID": 0 - }, + 0, { "contents": { "contents": [], @@ -113,9 +90,7 @@ null ] }, - "nodeId": { - "unID": 0 - }, + "nodeId": 0, "nodeType": { "tag": "BodyNode" } @@ -135,18 +110,14 @@ { "contents": [ [], - { - "unName": "b" - } + "b" ], "tag": "TCon" }, { "contents": [ [], - { - "unName": "a" - } + "a" ], "tag": "TCon" } @@ -156,35 +127,25 @@ { "contents": [ [], - { - "unName": "Nat" - } + "Nat" ], "tag": "TCon" } ], - "valConName": { - "unName": "C" - } + "valConName": "C" } ], - "typeDefName": { - "unName": "T" - }, + "typeDefName": "T", "typeDefNameHints": [], "typeDefParameters": [ [ - { - "unName": "a" - }, + "a", { "tag": "KType" } ], [ - { - "unName": "b" - }, + "b", { "contents": [ { diff --git a/primer/test/outputs/serialization/expr.json b/primer/test/outputs/serialization/expr.json index 19374dacb..69fa63969 100644 --- a/primer/test/outputs/serialization/expr.json +++ b/primer/test/outputs/serialization/expr.json @@ -1,8 +1,6 @@ { "contents": [ - { - "unID": 0 - }, + 0, { "contents": { "contents": [], diff --git a/primer/test/outputs/serialization/id.json b/primer/test/outputs/serialization/id.json index 8e5d1b35f..c22708346 100644 --- a/primer/test/outputs/serialization/id.json +++ b/primer/test/outputs/serialization/id.json @@ -1,3 +1 @@ -{ - "unID": 0 -} \ No newline at end of file +0 \ No newline at end of file diff --git a/primer/test/outputs/serialization/name.json b/primer/test/outputs/serialization/name.json index a6d6abbbd..3403a0c7f 100644 --- a/primer/test/outputs/serialization/name.json +++ b/primer/test/outputs/serialization/name.json @@ -1,3 +1 @@ -{ - "unName": "x" -} \ No newline at end of file +"x" \ No newline at end of file diff --git a/primer/test/outputs/serialization/prog.json b/primer/test/outputs/serialization/prog.json index 8a0d08f57..3d8d32b9a 100644 --- a/primer/test/outputs/serialization/prog.json +++ b/primer/test/outputs/serialization/prog.json @@ -1,47 +1,34 @@ { - "progDefs": [ - [ - { - "unID": 1 - }, - { - "defExpr": { - "contents": [ - { - "unID": 0 - }, - { - "contents": { - "contents": [], - "tag": "TEmptyHole" - }, - "tag": "TCSynthed" - }, - null - ], - "tag": "EmptyHole" - }, - "defID": { - "unID": 1 - }, - "defName": { - "unName": "main" - }, - "defType": { - "contents": [ - { - "unID": 0 - }, - { - "tag": "KType" + "progDefs": { + "1": { + "defExpr": { + "contents": [ + 0, + { + "contents": { + "contents": [], + "tag": "TEmptyHole" }, - null - ], - "tag": "TEmptyHole" - } + "tag": "TCSynthed" + }, + null + ], + "tag": "EmptyHole" + }, + "defID": 1, + "defName": "main", + "defType": { + "contents": [ + 0, + { + "tag": "KType" + }, + null + ], + "tag": "TEmptyHole" } - ] - ], + } + }, "progLog": { "unlog": [ [ @@ -63,9 +50,7 @@ "selectedDef": { "defExpr": { "contents": [ - { - "unID": 0 - }, + 0, { "contents": { "contents": [], @@ -77,17 +62,11 @@ ], "tag": "EmptyHole" }, - "defID": { - "unID": 1 - }, - "defName": { - "unName": "main" - }, + "defID": 1, + "defName": "main", "defType": { "contents": [ - { - "unID": 0 - }, + 0, { "tag": "KType" }, @@ -99,9 +78,7 @@ "selectedNode": { "meta": { "Left": [ - { - "unID": 0 - }, + 0, { "contents": { "contents": [], @@ -112,9 +89,7 @@ null ] }, - "nodeId": { - "unID": 0 - }, + "nodeId": 0, "nodeType": { "tag": "BodyNode" } @@ -134,18 +109,14 @@ { "contents": [ [], - { - "unName": "b" - } + "b" ], "tag": "TCon" }, { "contents": [ [], - { - "unName": "a" - } + "a" ], "tag": "TCon" } @@ -155,35 +126,25 @@ { "contents": [ [], - { - "unName": "Nat" - } + "Nat" ], "tag": "TCon" } ], - "valConName": { - "unName": "C" - } + "valConName": "C" } ], - "typeDefName": { - "unName": "T" - }, + "typeDefName": "T", "typeDefNameHints": [], "typeDefParameters": [ [ - { - "unName": "a" - }, + "a", { "tag": "KType" } ], [ - { - "unName": "b" - }, + "b", { "contents": [ { diff --git a/primer/test/outputs/serialization/progaction.json b/primer/test/outputs/serialization/progaction.json index 2e0e4dec5..6303f85fb 100644 --- a/primer/test/outputs/serialization/progaction.json +++ b/primer/test/outputs/serialization/progaction.json @@ -1,6 +1,4 @@ { - "contents": { - "unID": 0 - }, + "contents": 0, "tag": "MoveToDef" } \ No newline at end of file diff --git a/primer/test/outputs/serialization/selection.json b/primer/test/outputs/serialization/selection.json index 92480f322..798af6aef 100644 --- a/primer/test/outputs/serialization/selection.json +++ b/primer/test/outputs/serialization/selection.json @@ -2,9 +2,7 @@ "selectedDef": { "defExpr": { "contents": [ - { - "unID": 0 - }, + 0, { "contents": { "contents": [], @@ -16,17 +14,11 @@ ], "tag": "EmptyHole" }, - "defID": { - "unID": 1 - }, - "defName": { - "unName": "main" - }, + "defID": 1, + "defName": "main", "defType": { "contents": [ - { - "unID": 0 - }, + 0, { "tag": "KType" }, @@ -38,9 +30,7 @@ "selectedNode": { "meta": { "Left": [ - { - "unID": 0 - }, + 0, { "contents": { "contents": [], @@ -51,9 +41,7 @@ null ] }, - "nodeId": { - "unID": 0 - }, + "nodeId": 0, "nodeType": { "tag": "BodyNode" } diff --git a/primer/test/outputs/serialization/type.json b/primer/test/outputs/serialization/type.json index de8c0b92f..2596b3c9c 100644 --- a/primer/test/outputs/serialization/type.json +++ b/primer/test/outputs/serialization/type.json @@ -1,8 +1,6 @@ { "contents": [ - { - "unID": 0 - }, + 0, { "tag": "KType" }, diff --git a/primer/test/outputs/serialization/typeDef.json b/primer/test/outputs/serialization/typeDef.json index fbe1f3764..6b0fbd173 100644 --- a/primer/test/outputs/serialization/typeDef.json +++ b/primer/test/outputs/serialization/typeDef.json @@ -8,18 +8,14 @@ { "contents": [ [], - { - "unName": "b" - } + "b" ], "tag": "TCon" }, { "contents": [ [], - { - "unName": "a" - } + "a" ], "tag": "TCon" } @@ -29,35 +25,25 @@ { "contents": [ [], - { - "unName": "Nat" - } + "Nat" ], "tag": "TCon" } ], - "valConName": { - "unName": "C" - } + "valConName": "C" } ], - "typeDefName": { - "unName": "T" - }, + "typeDefName": "T", "typeDefNameHints": [], "typeDefParameters": [ [ - { - "unName": "a" - }, + "a", { "tag": "KType" } ], [ - { - "unName": "b" - }, + "b", { "contents": [ { From 837f037acf6aefc677d72cdaf8331004765be90c Mon Sep 17 00:00:00 2001 From: Ben Price Date: Thu, 4 Nov 2021 17:22:26 +0000 Subject: [PATCH 4/4] fix: make viewTree* injective We also add regression tests. [Historical note: this patch series was authored before Gen.Core.Raw obtained better coverage. This is the reason the non-injectivity was not discovered earlier, and the reason for the reliance on unit tests here.] --- primer/src/Primer/API.hs | 14 ++++---- primer/test/Tests/API.hs | 74 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 80 insertions(+), 8 deletions(-) diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index 266366eea..50d723100 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -79,11 +79,11 @@ import Primer.App ( import qualified Primer.App as App import Primer.Core ( Expr, - Expr' (APP, Ann, Con, LetType, Letrec, Var), + Expr' (APP, Ann, GlobalVar, LetType, Letrec), ID, Kind, Type, - Type' (TCon, TVar), + Type' (TForall), defExpr, defID, defName, @@ -346,9 +346,8 @@ viewTreeExpr :: Expr -> Tree viewTreeExpr = U.para $ \e exprChildren -> let c = toS $ showConstr $ toConstr e n = case e of - Con _ n' -> c <> " " <> unName n' - Var _ n' -> c <> " " <> unName n' - _ -> c + GlobalVar _ i -> c <> " " <> show i + _ -> unwords $ c : map unName (U.childrenBi e) -- add info about type children allChildren = case e of Ann _ _ ty -> exprChildren ++ [viewTreeType ty] @@ -364,9 +363,8 @@ viewTreeType :: Type -> Tree viewTreeType = U.para $ \e allChildren -> let c = toS $ showConstr $ toConstr e n = case e of - TCon _ n' -> c <> " " <> unName n' - TVar _ n' -> c <> " " <> unName n' - _ -> c + TForall _ m k _ -> c <> " " <> unName m <> ":" <> show k + _ -> unwords $ c : map unName (U.childrenBi e) in Tree (getID e) n allChildren edit :: (MonadIO m, MonadThrow m) => SessionId -> MutationRequest -> PrimerM m (Result ProgError App.Prog) diff --git a/primer/test/Tests/API.hs b/primer/test/Tests/API.hs index 4b5a59f5c..a98d76183 100644 --- a/primer/test/Tests/API.hs +++ b/primer/test/Tests/API.hs @@ -5,6 +5,10 @@ import Foreword import Gen.Core.Raw (evalExprGen, genExpr, genType) import Hedgehog import Primer.API (viewTreeExpr, viewTreeType) +import Primer.Core.DSL +import Test.Tasty.HUnit + +import Primer.Core hprop_viewTreeExpr_injective :: Property hprop_viewTreeExpr_injective = property $ do @@ -19,3 +23,73 @@ hprop_viewTreeType_injective = property $ do t2 <- forAll $ evalExprGen 0 genType when (t1 == t2) discard viewTreeType t1 /== viewTreeType t2 + +-- regression tests to check we encode names into the tree + +unit_viewTreeExpr_injective_con :: Assertion +unit_viewTreeExpr_injective_con = + distinctTreeExpr (con "C") (con "D") + +unit_viewTreeExpr_injective_lam :: Assertion +unit_viewTreeExpr_injective_lam = + distinctTreeExpr (lam "x" emptyHole) (lam "y" emptyHole) + +unit_viewTreeExpr_injective_LAM :: Assertion +unit_viewTreeExpr_injective_LAM = + distinctTreeExpr (lAM "x" emptyHole) (lAM "y" emptyHole) + +unit_viewTreeExpr_injective_var :: Assertion +unit_viewTreeExpr_injective_var = + distinctTreeExpr (var "x") (var "y") + +unit_viewTreeExpr_injective_globalvar :: Assertion +unit_viewTreeExpr_injective_globalvar = + distinctTreeExpr (global 0) (global 1) + +unit_viewTreeExpr_injective_let :: Assertion +unit_viewTreeExpr_injective_let = + distinctTreeExpr (let_ "x" emptyHole emptyHole) (let_ "y" emptyHole emptyHole) + +unit_viewTreeExpr_injective_lettype :: Assertion +unit_viewTreeExpr_injective_lettype = + distinctTreeExpr (letType "x" tEmptyHole emptyHole) (letType "y" tEmptyHole emptyHole) + +unit_viewTreeExpr_injective_letrec :: Assertion +unit_viewTreeExpr_injective_letrec = + distinctTreeExpr (letrec "x" emptyHole tEmptyHole emptyHole) (letrec "y" emptyHole tEmptyHole emptyHole) + +unit_viewTreeExpr_injective_case_conName :: Assertion +unit_viewTreeExpr_injective_case_conName = + distinctTreeExpr (case_ emptyHole [branch "C" [("x", Nothing)] emptyHole]) (case_ emptyHole [branch "D" [("x", Nothing)] emptyHole]) + +unit_viewTreeExpr_injective_case_paramName :: Assertion +unit_viewTreeExpr_injective_case_paramName = + distinctTreeExpr (case_ emptyHole [branch "C" [("x", Nothing)] emptyHole]) (case_ emptyHole [branch "C" [("y", Nothing)] emptyHole]) + +unit_viewTreeType_injective_con :: Assertion +unit_viewTreeType_injective_con = + distinctTreeType (tcon "T") (tcon "S") + +unit_viewTreeType_injective_var :: Assertion +unit_viewTreeType_injective_var = + distinctTreeType (tvar "a") (tvar "b") + +unit_viewTreeType_injective_forall_param :: Assertion +unit_viewTreeType_injective_forall_param = + distinctTreeType (tforall "a" KType tEmptyHole) (tforall "b" KType tEmptyHole) + +unit_viewTreeType_injective_forall_kind :: Assertion +unit_viewTreeType_injective_forall_kind = + distinctTreeType (tforall "a" KType tEmptyHole) (tforall "a" KHole tEmptyHole) + +distinctTreeExpr :: S Expr -> S Expr -> Assertion +distinctTreeExpr e1 e2 = + let t1 = viewTreeExpr $ fst $ create e1 + t2 = viewTreeExpr $ fst $ create e2 + in assertBool ("non-injective viewTreeExpr: " ++ show t1) (t1 /= t2) + +distinctTreeType :: S Type -> S Type -> Assertion +distinctTreeType e1 e2 = + let t1 = viewTreeType $ fst $ create e1 + t2 = viewTreeType $ fst $ create e2 + in assertBool ("non-injective viewTreeType: " ++ show t1) (t1 /= t2)