From 73787bf7ea9a2e5dd1df197ceec0854eb69d0c70 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Thu, 18 May 2023 16:11:44 +0100 Subject: [PATCH] WIP - undo Signed-off-by: George Thomas --- primer-service/primer-service.cabal | 4 +- primer/primer.cabal | 4 +- primer/src/Primer/App.hs | 71 ++++++++++++++++++++------- primer/src/Primer/Typecheck.hs | 36 +++++++------- primer/test/Tests/Action/Available.hs | 21 +++++++- 5 files changed, 95 insertions(+), 41 deletions(-) diff --git a/primer-service/primer-service.cabal b/primer-service/primer-service.cabal index 3eaaa7519..dceebf6a6 100644 --- a/primer-service/primer-service.cabal +++ b/primer-service/primer-service.cabal @@ -194,7 +194,7 @@ test-suite service-test , aeson-pretty , base , bytestring - , hedgehog ^>=1.2 + , hedgehog ^>=1.1 , hedgehog-quickcheck ^>=0.1.1 , hspec ^>=2.10 , openapi3 @@ -209,7 +209,7 @@ test-suite service-test , tasty ^>=1.4.1 , tasty-discover ^>=5.0 , tasty-golden ^>=2.3.5 - , tasty-hedgehog ^>=1.4 + , tasty-hedgehog ^>=1.3 , tasty-hspec ^>=1.2.0.1 , tasty-hunit ^>=0.10.0 , text diff --git a/primer/primer.cabal b/primer/primer.cabal index 8038d3fb9..0e59fc756 100644 --- a/primer/primer.cabal +++ b/primer/primer.cabal @@ -163,13 +163,13 @@ library primer-hedgehog build-depends: , base , containers - , hedgehog ^>=1.2 + , hedgehog ^>=1.1 , mmorph ^>=1.2.0 , mtl , primer , primer-testlib , tasty-discover ^>=5.0 - , tasty-hedgehog ^>=1.4 + , tasty-hedgehog ^>=1.3 library primer-testlib visibility: public diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 5e07f9480..e9f6489fc 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, @@ -135,7 +136,8 @@ import Primer.Core ( TyConName, Type, Type' (..), - TypeCache (TCSynthed), + TypeCache (TCChkedAt, TCEmb, TCSynthed), + TypeCacheBoth (TCBoth), TypeMeta, ValConName, getID, @@ -146,8 +148,10 @@ import Primer.Core ( unsafeMkGlobalName, unsafeMkLocalName, _chkedAt, + _exprMeta, _exprMetaLens, _synthed, + _type, _typeMetaLens, ) import Primer.Core.DSL (S, ann, create, emptyHole, hole, tEmptyHole, tvar) @@ -667,21 +671,26 @@ 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' + . over + (_exprMeta % _type % _Just) + ( \case + -- TODO is there a better way to do this? maybe I should define a getter + 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 + -- TODO rename `updateType` to `updateTypeDef` and this to `updateType`? in all branches? + 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 @@ -706,6 +715,7 @@ applyProgAction prog mdefName = \case over (#_Con % _2) updateName . over (#_Case % _3 % traversed % #_CaseBranch % _1) updateName updateName n = if n == old then new else n + -- RenameTypeParam type_ old (unsafeMkLocalName -> new) -> editModule (qualifiedModule type_) prog $ \m -> do m' <- updateType m @@ -721,6 +731,8 @@ applyProgAction prog mdefName = \case updateParam def = do when (new `elem` map fst (astTypeDefParameters def)) $ throwError $ ParamAlreadyExists new let nameRaw = unLocalName new + -- TODO we may as welll remove these, since we don't consistently check this sort of thing + -- as evidenced by code I've just commented out elsewhere when (nameRaw == baseName type_) $ throwError $ TyConParamClash nameRaw when (nameRaw `elem` map (baseName . valConName) (astTypeDefConstructors def)) $ throwError $ ValConParamClash nameRaw def @@ -737,6 +749,7 @@ applyProgAction prog mdefName = \case % traversed ) $ traverseOf _freeVarsTy + -- TODO respect scope i.e. avoid capture by not going under forall $ \(_, v) -> tvar $ updateName v updateName n = if n == old then new else n AddCon type_ index (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> con) -> @@ -753,6 +766,27 @@ applyProgAction prog mdefName = \case , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefConsNodeSelection $ TypeDefConsSelection con Nothing ) where + -- transformCaseBranches' :: + -- MonadEdit m ProgError => + -- Prog -> + -- TyConName -> + -- Maybe TypeCache -> + -- ([CaseBranch] -> m [CaseBranch]) -> + -- Expr -> + -- m Expr + -- transformCaseBranches' prog type_ t f = transformM $ \case + -- Case m scrut bs -> do + -- scrutType <- + -- fst + -- <$> runReaderT + -- (liftError (ActionError . TypeError) $ synth scrut) + -- (progCxt prog) + -- Case (m & _type .~ t) scrut + -- <$> if fst (unfoldTApp scrutType) == TCon () type_ + -- then f bs + -- else pure bs + -- e -> pure e + -- updateDefs = transformCaseBranches' prog type_ (Just (TCChkedAt $ TApp () (TEmptyHole ()) (TEmptyHole ()))) $ \bs -> do updateDefs = transformCaseBranches prog type_ $ \bs -> do m' <- DSL.meta maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (CaseBranch con [] (EmptyHole m')) bs @@ -923,7 +957,8 @@ 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) -> + -- Right (mod', zt) -> pure ( mod' , Just $ @@ -936,11 +971,13 @@ 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 + -- Just + -- TypeDefConsFieldSelection + -- { index + -- , meta = Right $ zt ^. _target % _typeMetaLens + -- } } } ) diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index 5526355c4..ee057e85b 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -95,7 +95,7 @@ import Primer.Core ( Expr' (..), ExprMeta, GVarName, - GlobalName (baseName, qualifiedModule), + GlobalName (qualifiedModule), ID, Kind (..), LVarName, @@ -310,10 +310,10 @@ checkTypeDefs tds = do -- 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 - assert - (distinct $ concatMap (map valConName . astTypeDefConstructors) allAtds) - "Duplicate-ly-named constructor (perhaps in different typedefs)" + -- 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 @@ -346,12 +346,12 @@ 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 <> 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" + -- 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" local (noSmartHoles . extendLocalCxtTys params) $ mapM_ (checkKind' KType <=< fakeMeta) $ concatMap valConArgs cons @@ -360,13 +360,13 @@ checkTypeDefs tds = do -- metadata as it won't be inspected. fakeMeta = generateTypeIDs -distinct :: Ord a => [a] -> Bool -distinct = go mempty - where - go _ [] = True - go seen (x : xs) - | x `S.member` seen = False - | otherwise = go (S.insert x seen) xs +-- distinct :: Ord a => [a] -> Bool +-- distinct = go mempty +-- where +-- go _ [] = True +-- go seen (x : xs) +-- | x `S.member` seen = False +-- | otherwise = go (S.insert x seen) xs data CheckEverythingRequest = CheckEverything { trusted :: [Module] diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs index ce2f41df3..b7d671387 100644 --- a/primer/test/Tests/Action/Available.hs +++ b/primer/test/Tests/Action/Available.hs @@ -23,6 +23,7 @@ import Hedgehog ( collect, discard, failure, + footnoteShow, label, success, (===), @@ -74,6 +75,7 @@ import Primer.Core ( HasID (_id), ID, ModuleName (ModuleName, unModuleName), + TypeMeta, getID, mkSimpleModuleName, moduleNamePretty, @@ -361,9 +363,24 @@ 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' + -- TODO handle these (everything else seems to work) + -- let ifPoss = Available.Input Available.RenameTypeParam + -- let ifPoss = Available.Input Available.AddCon + -- let ifPoss = Available.NoInput Available.AddConField -- TODO I think I fixed the issue here, but I still see an unrelated-looking unknown-var error + action <- do + forAllT $ Gen.element acts' + -- if ifPoss `elem` acts' + -- then pure ifPoss + -- else forAllT $ Gen.element acts' collect action + footnoteShow action -- TODO remove case action of + Available.Input Available.AddCon -> discard + Available.Input Available.RenameTypeParam -> discard + Available.NoInput Available.AddConField -> discard + -- act@(Available.Input Available.AddCon) | act /= ifPoss -> discard + -- act@(Available.Input Available.RenameTypeParam) | act /= ifPoss -> discard + -- act@(Available.NoInput Available.AddConField) | act /= ifPoss -> discard Available.NoInput act' -> do progActs <- either (\e -> annotateShow e >> failure) pure $ @@ -517,7 +534,7 @@ offeredActionTest sh l inputExpr position action expectedOutput = do action' <- case action of Left a -> do assertOffered $ Available.NoInput a - pure $ toProgActionNoInput (foldMap' moduleDefsQualified $ progModules prog) (Right exprDef) (SelectionDef $ DefSelection exprDefName $ Just $ NodeSelection BodyNode id) a + pure $ toProgActionNoInput @TypeMeta (foldMap' moduleDefsQualified $ progModules prog) (Right exprDef) (SelectionDef $ DefSelection exprDefName $ Just $ NodeSelection BodyNode id) a Right (a, o) -> do assertOffered $ Available.Input a case options a of