From ecd1489ae3c8e15949c3badde93e87fe50424af1 Mon Sep 17 00:00:00 2001 From: Drew Hess Date: Thu, 13 Jan 2022 12:18:49 +0000 Subject: [PATCH] style: Fourmolu 0.5.0 formatting changes. No functional changes here, this is pure formatting. Note that we exclude `primer/test/outputs` as those are formatting-sensitive. --- primer-selda/src/Primer/Database/Selda.hs | 34 +-- primer-service/src/Primer/Pagination.hs | 8 +- primer/src/Primer/API.hs | 12 +- primer/src/Primer/Action.hs | 48 ++-- primer/src/Primer/Action/Available.hs | 66 ++--- primer/src/Primer/App.hs | 24 +- primer/src/Primer/Core.hs | 2 +- primer/src/Primer/Database.hs | 16 +- primer/src/Primer/Eval.hs | 332 +++++++++++----------- primer/src/Primer/EvalFull.hs | 60 ++-- primer/src/Primer/Questions.hs | 4 +- primer/src/Primer/Typecheck.hs | 16 +- primer/src/Primer/Zipper.hs | 34 +-- primer/test/Tests/Action/Prog.hs | 4 +- primer/test/Tests/EvalFull.hs | 2 +- primer/test/Tests/Typecheck.hs | 6 +- primer/test/Tests/Unification.hs | 6 +- 17 files changed, 337 insertions(+), 337 deletions(-) diff --git a/primer-selda/src/Primer/Database/Selda.hs b/primer-selda/src/Primer/Database/Selda.hs index a1e5c29c3..36c1e5c82 100644 --- a/primer-selda/src/Primer/Database/Selda.hs +++ b/primer-selda/src/Primer/Database/Selda.hs @@ -60,23 +60,23 @@ import Primer.Database ( -- consisting of the session's 'App', the git version of Primer that -- last updated it, and the session's name. data SessionRow = SessionRow - { -- | The session's UUID. - uuid :: UUID - , -- | Primer's git version. We would prefer that this were a git - -- rev, but for technical reasons, it may also be a last-modified - -- date. - gitversion :: Version - , -- | The session's 'App'. Note that the 'App' is serialized to - -- JSON before being stored as a bytestring in the database. - app :: BL.ByteString - , -- | The session's name. - -- - -- This should be of type 'SessionName', but Selda doesn't make it - -- particularly easy to derive @SqlType@ from a newtype wrapper - -- around 'Text', so rather than copy-pasting the 'Text' instance, - -- we just convert back to 'Text' before serializing to the - -- database. - name :: Text + { uuid :: UUID + -- ^ The session's UUID. + , gitversion :: Version + -- ^ Primer's git version. We would prefer that this were a git + -- rev, but for technical reasons, it may also be a last-modified + -- date. + , app :: BL.ByteString + -- ^ The session's 'App'. Note that the 'App' is serialized to + -- JSON before being stored as a bytestring in the database. + , name :: Text + -- ^ The session's name. + -- + -- This should be of type 'SessionName', but Selda doesn't make it + -- particularly easy to derive @SqlType@ from a newtype wrapper + -- around 'Text', so rather than copy-pasting the 'Text' instance, + -- we just convert back to 'Text' before serializing to the + -- database. } deriving (Generic) diff --git a/primer-service/src/Primer/Pagination.hs b/primer-service/src/Primer/Pagination.hs index 249666ef7..deed62996 100644 --- a/primer-service/src/Primer/Pagination.hs +++ b/primer-service/src/Primer/Pagination.hs @@ -81,10 +81,10 @@ type PP api = :> api data Pagination = Pagination - { -- | Defaults to @1@ if not given in the query parameters - page :: Positive - , -- | Does not default, since there is no default that would work for all cases - size :: Maybe Positive + { page :: Positive + -- ^ Defaults to @1@ if not given in the query parameters + , size :: Maybe Positive + -- ^ Does not default, since there is no default that would work for all cases } instance diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index f22866767..7b1d0ab13 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -297,12 +297,12 @@ instance ToJSON Tree data Prog = Prog { types :: [Name] , -- 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] + -- 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/Action.hs b/primer/src/Primer/Action.hs index 0f61ca880..42e9e6e4c 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -135,8 +135,8 @@ data OfferedAction a = OfferedAction , description :: Text , input :: ActionInput a , priority :: Int - , -- | Used primarily for display purposes. - actionType :: ActionType + , actionType :: ActionType + -- ^ Used primarily for display purposes. } deriving (Functor) @@ -599,7 +599,7 @@ moveExpr m@(Branch c) z | Case _ _ brs <- target z = moveExpr m@(Branch _) _ = throwError $ CustomFailure (Move m) "Move-to-branch failed: this is not a case expression" moveExpr Child2 z | Case{} <- target z = - throwError $ CustomFailure (Move Child2) "cannot move to 'Child2' of a case: use Branch instead" + throwError $ CustomFailure (Move Child2) "cannot move to 'Child2' of a case: use Branch instead" moveExpr m z = move m z -- | Apply a movement to a zipper @@ -914,11 +914,11 @@ renameLam y ze = case target ze of Lam m x e | unName x == y -> pure ze | otherwise -> do - let y' = unsafeMkName y - case renameVar x y' e of - Just e' -> pure $ replace (Lam m y' e') ze - Nothing -> - throwError NameCapture + let y' = unsafeMkName y + case renameVar x y' e of + Just e' -> pure $ replace (Lam m y' e') ze + Nothing -> + throwError NameCapture _ -> throwError $ CustomFailure (RenameLam y) "the focused expression is not a lambda" @@ -928,11 +928,11 @@ renameLAM b ze = case target ze of LAM m a e | unName a == b -> pure ze | otherwise -> do - let b' = unsafeMkName b - case renameTyVarExpr a b' e of - Just e' -> pure $ replace (LAM m b' e') ze - Nothing -> - throwError NameCapture + let b' = unsafeMkName b + case renameTyVarExpr a b' e of + Just e' -> pure $ replace (LAM m b' e') ze + Nothing -> + throwError NameCapture _ -> throwError $ CustomFailure (RenameLAM b) "the focused expression is not a type abstraction" @@ -942,15 +942,15 @@ renameLet y ze = case target ze of Let m x e1 e2 | unName x == y -> pure ze | otherwise -> do - let y' = unsafeMkName y - (e1', e2') <- doRename x y' e1 e2 - pure $ replace (Let m y' e1' e2') ze + let y' = unsafeMkName y + (e1', e2') <- doRename x y' e1 e2 + pure $ replace (Let m y' e1' e2') ze Letrec m x e1 t1 e2 | unName x == y -> pure ze | otherwise -> do - let y' = unsafeMkName y - (e1', e2') <- doRename x y' e1 e2 - pure $ replace (Letrec m y' e1' t1 e2') ze + let y' = unsafeMkName y + (e1', e2') <- doRename x y' e1 e2 + pure $ replace (Letrec m y' e1' t1 e2') ze _ -> throwError $ CustomFailure (RenameLet y) "the focused expression is not a let" where @@ -1028,10 +1028,10 @@ renameForall b zt = case target zt of TForall m a k t | unName a == b -> pure zt | otherwise -> do - let b' = unsafeMkName b - case renameTyVar a b' t of - Just t' -> pure $ replace (TForall m b' k t') zt - Nothing -> - throwError NameCapture + let b' = unsafeMkName b + case renameTyVar a b' t of + Just t' -> pure $ replace (TForall m b' k t') zt + Nothing -> + throwError NameCapture _ -> throwError $ CustomFailure (RenameForall b) "the focused expression is not a forall type" diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs index d32f95ce6..cd37e688d 100644 --- a/primer/src/Primer/Action/Available.hs +++ b/primer/src/Primer/Action/Available.hs @@ -209,25 +209,25 @@ findNodeWithParent id x = go x Nothing go expr parent | expr ^. _exprMetaLens % _id == id = Just (ExprNode expr, parent) | otherwise = case expr of - Hole _ e -> go e (Just (ExprNode expr)) - EmptyHole _ -> Nothing - Ann _ e t -> go e (Just (ExprNode expr)) <|> goTy t expr - App _ a b -> go a (Just (ExprNode expr)) <|> go b (Just (ExprNode expr)) - APP _ a b -> go a (Just (ExprNode expr)) <|> goTy b expr - Con _ _ -> Nothing - Lam _ _ e -> go e (Just (ExprNode expr)) - LAM _ _ e -> go e (Just (ExprNode expr)) - Var _ _ -> Nothing - GlobalVar _ _ -> Nothing - Let _ _ a b -> go a (Just (ExprNode expr)) <|> go b (Just (ExprNode expr)) - Letrec _ _ a ta b -> go a (Just (ExprNode expr)) <|> goTy ta expr <|> go b (Just (ExprNode expr)) - LetType _ _ t e -> goTy t expr <|> go e (Just (ExprNode expr)) - Case _ e branches -> - let (Alt inBranches) = flip foldMap branches $ - \(CaseBranch _ binds rhs) -> - Alt (go rhs (Just (ExprNode expr))) - <> foldMap (Alt . map (\b -> (CaseBindNode b, Just (ExprNode expr))) . findBind id) binds - in go e (Just (ExprNode expr)) <|> inBranches + Hole _ e -> go e (Just (ExprNode expr)) + EmptyHole _ -> Nothing + Ann _ e t -> go e (Just (ExprNode expr)) <|> goTy t expr + App _ a b -> go a (Just (ExprNode expr)) <|> go b (Just (ExprNode expr)) + APP _ a b -> go a (Just (ExprNode expr)) <|> goTy b expr + Con _ _ -> Nothing + Lam _ _ e -> go e (Just (ExprNode expr)) + LAM _ _ e -> go e (Just (ExprNode expr)) + Var _ _ -> Nothing + GlobalVar _ _ -> Nothing + Let _ _ a b -> go a (Just (ExprNode expr)) <|> go b (Just (ExprNode expr)) + Letrec _ _ a ta b -> go a (Just (ExprNode expr)) <|> goTy ta expr <|> go b (Just (ExprNode expr)) + LetType _ _ t e -> goTy t expr <|> go e (Just (ExprNode expr)) + Case _ e branches -> + let (Alt inBranches) = flip foldMap branches $ + \(CaseBranch _ binds rhs) -> + Alt (go rhs (Just (ExprNode expr))) + <> foldMap (Alt . map (\b -> (CaseBindNode b, Just (ExprNode expr))) . findBind id) binds + in go e (Just (ExprNode expr)) <|> inBranches goTy t p = case findTypeWithParent id t of Nothing -> Nothing @@ -239,13 +239,13 @@ findType :: forall b. ID -> Type' (Meta b) -> Maybe (Type' (Meta b)) findType id ty | ty ^. _typeMetaLens % _id == id = Just ty | otherwise = case ty of - TEmptyHole _ -> Nothing - THole _ t -> findType id t - TCon _ _ -> Nothing - TVar _ _ -> Nothing - TFun _ a b -> findType id a <|> findType id b - TApp _ a b -> findType id a <|> findType id b - TForall _ _ _ t -> findType id t + TEmptyHole _ -> Nothing + THole _ t -> findType id t + TCon _ _ -> Nothing + TVar _ _ -> Nothing + TFun _ a b -> findType id a <|> findType id b + TApp _ a b -> findType id a <|> findType id b + TForall _ _ _ t -> findType id t -- | Find a sub-type in a larger type by its ID. Also returning its parent findTypeWithParent :: forall b. ID -> Type' (Meta b) -> Maybe (Type' (Meta b), Maybe (Type' (Meta b))) @@ -254,13 +254,13 @@ findTypeWithParent id x = go x Nothing go ty parent | ty ^. _typeMetaLens % _id == id = Just (ty, parent) | otherwise = case ty of - TEmptyHole _ -> Nothing - THole _ t -> go t (Just ty) - TCon _ _ -> Nothing - TVar _ _ -> Nothing - TFun _ a b -> go a (Just ty) <|> go b (Just ty) - TApp _ a b -> go a (Just ty) <|> go b (Just ty) - TForall _ _ _ t -> go t (Just ty) + TEmptyHole _ -> Nothing + THole _ t -> go t (Just ty) + TCon _ _ -> Nothing + TVar _ _ -> Nothing + TFun _ a b -> go a (Just ty) <|> go b (Just ty) + TApp _ a b -> go a (Just ty) <|> go b (Just ty) + TForall _ _ _ t -> go t (Just ty) -- | If the given binding has the given ID, return Just that binding, otherwise return nothing. -- This is just a helper for 'findNode'. diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 238668195..2245153cd 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -333,15 +333,15 @@ applyProgAction prog mdefID = \case Just _ -> pure (prog, Just id_) DeleteDef id_ | Map.member id_ (progDefs prog) -> do - let defs = Map.delete id_ (progDefs prog) - prog' = prog{progDefs = defs, progSelection = Nothing} - -- Run a full TC solely to ensure that no references to the removed id - -- remain. This is rather inefficient and could be improved in the - -- future. - runExceptT (checkEverything @TypeError NoSmartHoles (progTypes prog) (progDefs prog')) >>= \case - Left _ -> throwError $ DefInUse id_ - Right _ -> pure () - pure (prog', Nothing) + let defs = Map.delete id_ (progDefs prog) + prog' = prog{progDefs = defs, progSelection = Nothing} + -- Run a full TC solely to ensure that no references to the removed id + -- remain. This is rather inefficient and could be improved in the + -- future. + runExceptT (checkEverything @TypeError NoSmartHoles (progTypes prog) (progDefs prog')) >>= \case + Left _ -> throwError $ DefInUse id_ + Right _ -> pure () + pure (prog', Nothing) DeleteDef id_ -> throwError $ DefNotFound id_ RenameDef id_ nameStr -> case Map.lookup id_ (progDefs prog) of Nothing -> throwError $ DefNotFound id_ @@ -634,7 +634,7 @@ copyPasteSig p (fromDefId, fromTyId) toDefId setup = do Left err -> throwError $ ActionError err Right (_, _, tgt) -> pure $ focusOnlyType tgt let sharedScope = - if fromDefId == toDefId --optimization only + if fromDefId == toDefId -- optimization only then getSharedScopeTy c $ Right tgt else mempty -- Delete unbound vars @@ -762,7 +762,7 @@ copyPasteBody p (fromDefId, fromId) toDefId setup = do (Right _, InExpr _) -> throwError $ CopyPasteError "tried to paste a type into an expression" (Right srcT, InType tgtT) -> do let sharedScope = - if fromDefId == toDefId --optimization only + if fromDefId == toDefId -- optimization only then getSharedScopeTy srcT $ Left tgtT else mempty -- Delete unbound vars. TODO: we may want to let-bind them? @@ -781,7 +781,7 @@ copyPasteBody p (fromDefId, fromId) toDefId setup = do tcWholeProg finalProg (Left srcE, InExpr tgtE) -> do let sharedScope = - if fromDefId == toDefId --optimization only + if fromDefId == toDefId -- optimization only then getSharedScope srcE tgtE else mempty -- Delete unbound vars. TODO: we may want to let-bind them? diff --git a/primer/src/Primer/Core.hs b/primer/src/Primer/Core.hs index 5fc695056..375b29834 100644 --- a/primer/src/Primer/Core.hs +++ b/primer/src/Primer/Core.hs @@ -100,7 +100,7 @@ data TypeCacheBoth = TCBoth {tcChkedAt :: Type' (), tcSynthed :: Type' ()} deriving (Eq, Show, Generic, Data) deriving (FromJSON, ToJSON) via VJSON TypeCacheBoth ---TODO `_chkedAt` and `_synthed` should be `AffineTraversal`s, +-- TODO `_chkedAt` and `_synthed` should be `AffineTraversal`s, -- but there is currently no `failing` for AffineTraversals, only for AffineFolds (`afailing`). -- See https://github.com/well-typed/optics/pull/393 diff --git a/primer/src/Primer/Database.hs b/primer/src/Primer/Database.hs index b68e303f8..a4af76dfd 100644 --- a/primer/src/Primer/Database.hs +++ b/primer/src/Primer/Database.hs @@ -132,10 +132,10 @@ data Session = Session {id :: SessionId, name :: SessionName} -- | Per-session information. data SessionData = SessionData - { -- | The session's 'App'. - sessionApp :: App - , -- | The session's name. - sessionName :: SessionName + { sessionApp :: App + -- ^ The session's 'App'. + , sessionName :: SessionName + -- ^ The session's name. } deriving (Generic) @@ -176,10 +176,10 @@ data Op -- | A config for the 'serve' computation. data ServiceCfg = ServiceCfg - { -- | The database operation queue. - opQueue :: TBQueue Op - , -- | The running version of Primer. - version :: Version + { opQueue :: TBQueue Op + -- ^ The database operation queue. + , version :: Version + -- ^ The running version of Primer. } -- | A 'Page' is a portion of the results of some DB query, along with the diff --git a/primer/src/Primer/Eval.hs b/primer/src/Primer/Eval.hs index 9e6534a56..0613f49e1 100644 --- a/primer/src/Primer/Eval.hs +++ b/primer/src/Primer/Eval.hs @@ -144,88 +144,88 @@ data BetaReductionDetail domain codomain = BetaReductionDetail deriving (FromJSON, ToJSON) via VJSONPrefix "beta" (BetaReductionDetail domain codomain) data LocalVarInlineDetail = LocalVarInlineDetail - { -- | ID of the let expression that binds this variable - localVarInlineLetID :: ID - , -- | ID of the variable being replaced - localVarInlineVarID :: ID - , -- | Name of the variable - localVarInlineBindingName :: Name - , -- | ID of the expression or type that the variable is bound to - localVarInlineValueID :: ID - , -- | ID of the expression or type that has replaced the variable in the result - localVarInlineReplacementID :: ID - , -- | If 'True', the variable being inlined is a type variable. - -- Otherwise it is a term variable. - localVarInlineIsTypeVar :: Bool + { localVarInlineLetID :: ID + -- ^ ID of the let expression that binds this variable + , localVarInlineVarID :: ID + -- ^ ID of the variable being replaced + , localVarInlineBindingName :: Name + -- ^ Name of the variable + , localVarInlineValueID :: ID + -- ^ ID of the expression or type that the variable is bound to + , localVarInlineReplacementID :: ID + -- ^ ID of the expression or type that has replaced the variable in the result + , localVarInlineIsTypeVar :: Bool + -- ^ If 'True', the variable being inlined is a type variable. + -- Otherwise it is a term variable. } deriving (Eq, Show, Generic) deriving (FromJSON, ToJSON) via VJSONPrefix "localVarInline" LocalVarInlineDetail data GlobalVarInlineDetail = GlobalVarInlineDetail - { -- | The definition that the variable refers to - globalVarInlineDef :: Def - , -- | The variable being replaced - globalVarInlineVar :: Expr - , -- | The result of the reduction - globalVarInlineAfter :: Expr + { globalVarInlineDef :: Def + -- ^ The definition that the variable refers to + , globalVarInlineVar :: Expr + -- ^ The variable being replaced + , globalVarInlineAfter :: Expr + -- ^ The result of the reduction } deriving (Eq, Show, Generic) deriving (FromJSON, ToJSON) via VJSONPrefix "globalVarInline" GlobalVarInlineDetail data CaseReductionDetail = CaseReductionDetail - { -- | the case expression before reduction - caseBefore :: Expr - , -- | the resulting expression after reduction - caseAfter :: Expr - , -- | the ID of the target (scrutinee) - caseTargetID :: ID - , -- | the ID of the constructor node in the target - caseTargetCtorID :: ID - , -- | the name of the matching constructor - caseCtorName :: Name - , -- | the arguments to the constructor in the target - caseTargetArgIDs :: [ID] - , -- | the bindings in the case branch (one for each arg above) - caseBranchBindingIDs :: [ID] - , -- | the right hand side of the selected case branch - caseBranchRhsID :: ID - , -- | the let expressions binding each argument in the result - caseLetIDs :: [ID] + { caseBefore :: Expr + -- ^ the case expression before reduction + , caseAfter :: Expr + -- ^ the resulting expression after reduction + , caseTargetID :: ID + -- ^ the ID of the target (scrutinee) + , caseTargetCtorID :: ID + -- ^ the ID of the constructor node in the target + , caseCtorName :: Name + -- ^ the name of the matching constructor + , caseTargetArgIDs :: [ID] + -- ^ the arguments to the constructor in the target + , caseBranchBindingIDs :: [ID] + -- ^ the bindings in the case branch (one for each arg above) + , caseBranchRhsID :: ID + -- ^ the right hand side of the selected case branch + , caseLetIDs :: [ID] + -- ^ the let expressions binding each argument in the result } deriving (Eq, Show, Generic) deriving (FromJSON, ToJSON) via VJSONPrefix "case" CaseReductionDetail data LetRemovalDetail = LetRemovalDetail - { -- | the let expression before reduction - letRemovalBefore :: Expr - , -- | the resulting expression after reduction - letRemovalAfter :: Expr - , -- | the name of the unused bound variable - letRemovalBindingName :: Name - , -- | the full let expression - letRemovalLetID :: ID - , -- | the right hand side of the let - letRemovalBodyID :: ID + { letRemovalBefore :: Expr + -- ^ the let expression before reduction + , letRemovalAfter :: Expr + -- ^ the resulting expression after reduction + , letRemovalBindingName :: Name + -- ^ the name of the unused bound variable + , letRemovalLetID :: ID + -- ^ the full let expression + , letRemovalBodyID :: ID + -- ^ the right hand side of the let } deriving (Eq, Show, Generic) deriving (FromJSON, ToJSON) via VJSONPrefix "letRemoval" LetRemovalDetail data PushAppIntoLetrecDetail = PushAppIntoLetrecDetail - { -- | the expression before reduction - pushAppIntoLetrecBefore :: Expr - , -- | the expression after reduction - pushAppIntoLetrecAfter :: Expr - , -- | the ID of the argument to the application - pushAppIntoLetrecArgID :: ID - , -- | the ID of the letrec - pushAppIntoLetrecLetrecID :: ID - , -- | the ID of the lambda - pushAppIntoLetrecLamID :: ID - , -- | The name of the variable bound by the letrec - pushAppIntoLetrecLetBindingName :: Name - , -- | If 'True', the application is of a big lambda to a type. - -- Otherwise it is of a small lambda to a term. - pushAppIntoLetrecIsTypeApplication :: Bool + { pushAppIntoLetrecBefore :: Expr + -- ^ the expression before reduction + , pushAppIntoLetrecAfter :: Expr + -- ^ the expression after reduction + , pushAppIntoLetrecArgID :: ID + -- ^ the ID of the argument to the application + , pushAppIntoLetrecLetrecID :: ID + -- ^ the ID of the letrec + , pushAppIntoLetrecLamID :: ID + -- ^ the ID of the lambda + , pushAppIntoLetrecLetBindingName :: Name + -- ^ The name of the variable bound by the letrec + , pushAppIntoLetrecIsTypeApplication :: Bool + -- ^ If 'True', the application is of a big lambda to a type. + -- Otherwise it is of a small lambda to a term. } deriving (Eq, Show, Generic) deriving (FromJSON, ToJSON) via VJSONPrefix "pushAppIntoLetrec" PushAppIntoLetrecDetail @@ -410,16 +410,16 @@ tryReduceExpr globals locals = \case pure ( expr , BetaReduction - BetaReductionDetail - { betaBefore = App mApp lam arg - , betaAfter = expr - , betaBindingName = x - , betaLambdaID = lam ^. _id - , betaLetID = expr ^. _id - , betaArgID = arg ^. _id - , betaBodyID = body ^. _id - , betaTypes = Nothing - } + BetaReductionDetail + { betaBefore = App mApp lam arg + , betaAfter = expr + , betaBindingName = x + , betaLambdaID = lam ^. _id + , betaLetID = expr ^. _id + , betaArgID = arg ^. _id + , betaBodyID = body ^. _id + , betaTypes = Nothing + } ) -- Beta reduction (with annotation) -- (\x. e1 : A -> B) e2 ==> let x = e2 : A in e1 : B @@ -450,16 +450,16 @@ tryReduceExpr globals locals = \case pure ( expr , BetaReduction - BetaReductionDetail - { betaBefore = App mApp annotation arg - , betaAfter = expr - , betaBindingName = x - , betaLambdaID = lam ^. _id - , betaLetID = letexpr ^. _id - , betaArgID = arg ^. _id - , betaBodyID = body ^. _id - , betaTypes = types - } + BetaReductionDetail + { betaBefore = App mApp annotation arg + , betaAfter = expr + , betaBindingName = x + , betaLambdaID = lam ^. _id + , betaLetID = letexpr ^. _id + , betaArgID = arg ^. _id + , betaBodyID = body ^. _id + , betaTypes = types + } ) -- (letrec x : T = λ ...) e before@(App mApp (Letrec mLet x e1 t lam@Lam{}) e2) | Set.notMember x (freeVars e2) -> do @@ -469,15 +469,15 @@ tryReduceExpr globals locals = \case pure ( expr , PushAppIntoLetrec - PushAppIntoLetrecDetail - { pushAppIntoLetrecBefore = before - , pushAppIntoLetrecAfter = expr - , pushAppIntoLetrecArgID = e2 ^. _id - , pushAppIntoLetrecLetrecID = mLet ^. _id - , pushAppIntoLetrecLamID = lam ^. _id - , pushAppIntoLetrecLetBindingName = x - , pushAppIntoLetrecIsTypeApplication = False - } + PushAppIntoLetrecDetail + { pushAppIntoLetrecBefore = before + , pushAppIntoLetrecAfter = expr + , pushAppIntoLetrecArgID = e2 ^. _id + , pushAppIntoLetrecLetrecID = mLet ^. _id + , pushAppIntoLetrecLamID = lam ^. _id + , pushAppIntoLetrecLetBindingName = x + , pushAppIntoLetrecIsTypeApplication = False + } ) -- Beta reduction of an inner application -- This rule is theoretically redundant but because we render nested applications with just one @@ -499,16 +499,16 @@ tryReduceExpr globals locals = \case pure ( expr , BETAReduction - BetaReductionDetail - { betaBefore = APP mAPP lam arg - , betaAfter = expr - , betaBindingName = x - , betaLambdaID = lam ^. _id - , betaLetID = expr ^. _id - , betaArgID = arg ^. _id - , betaBodyID = body ^. _id - , betaTypes = Nothing - } + BetaReductionDetail + { betaBefore = APP mAPP lam arg + , betaAfter = expr + , betaBindingName = x + , betaLambdaID = lam ^. _id + , betaLetID = expr ^. _id + , betaArgID = arg ^. _id + , betaBodyID = body ^. _id + , betaTypes = Nothing + } ) -- Beta reduction of big lambda (with annotation) -- With the current editor K is always KType, so the annotation is a @@ -528,16 +528,16 @@ tryReduceExpr globals locals = \case pure ( expr , BETAReduction - BetaReductionDetail - { betaBefore = APP mAPP annotation t - , betaAfter = expr - , betaBindingName = x - , betaLambdaID = lam ^. _id - , betaLetID = expr ^. _id - , betaArgID = t ^. _id - , betaBodyID = body ^. _id - , betaTypes = Just (k, b) - } + BetaReductionDetail + { betaBefore = APP mAPP annotation t + , betaAfter = expr + , betaBindingName = x + , betaLambdaID = lam ^. _id + , betaLetID = expr ^. _id + , betaArgID = t ^. _id + , betaBodyID = body ^. _id + , betaTypes = Just (k, b) + } ) _ -> throwError $ BadBigLambdaAnnotation annotation -- (letrec x : T = Λ ...) e @@ -548,15 +548,15 @@ tryReduceExpr globals locals = \case pure ( expr , PushAppIntoLetrec - PushAppIntoLetrecDetail - { pushAppIntoLetrecBefore = before - , pushAppIntoLetrecAfter = expr - , pushAppIntoLetrecArgID = e2 ^. _id - , pushAppIntoLetrecLetrecID = mLet ^. _id - , pushAppIntoLetrecLamID = lam ^. _id - , pushAppIntoLetrecLetBindingName = x - , pushAppIntoLetrecIsTypeApplication = True - } + PushAppIntoLetrecDetail + { pushAppIntoLetrecBefore = before + , pushAppIntoLetrecAfter = expr + , pushAppIntoLetrecArgID = e2 ^. _id + , pushAppIntoLetrecLetrecID = mLet ^. _id + , pushAppIntoLetrecLamID = lam ^. _id + , pushAppIntoLetrecLetBindingName = x + , pushAppIntoLetrecIsTypeApplication = True + } ) -- Beta reduction of an inner big lambda application -- This rule is theoretically redundant but because we render nested applications with just one @@ -576,11 +576,11 @@ tryReduceExpr globals locals = \case -- that hasn't yet been reduced. Var mVar x | Just (i, Left e) <- Map.lookup x locals -> do - -- Since we're duplicating @e@, we must regenerate all its IDs. - e' <- regenerateExprIDs e - pure - ( e' - , LocalVarInline + -- Since we're duplicating @e@, we must regenerate all its IDs. + e' <- regenerateExprIDs e + pure + ( e' + , LocalVarInline LocalVarInlineDetail { localVarInlineLetID = i , localVarInlineVarID = mVar ^. _id @@ -589,7 +589,7 @@ tryReduceExpr globals locals = \case , localVarInlineReplacementID = e' ^. _id , localVarInlineIsTypeVar = False } - ) + ) -- Inline global variable -- (f = e : t) |- f ==> e : t GlobalVar mVar i | Just def <- Map.lookup i globals -> do @@ -600,11 +600,11 @@ tryReduceExpr globals locals = \case pure ( expr , GlobalVarInline - GlobalVarInlineDetail - { globalVarInlineVar = GlobalVar mVar i - , globalVarInlineDef = def - , globalVarInlineAfter = expr - } + GlobalVarInlineDetail + { globalVarInlineVar = GlobalVar mVar i + , globalVarInlineDef = def + , globalVarInlineAfter = expr + } ) -- Redundant let removal -- let x = e1 in e2 ==> e2 if x not free in e2 @@ -625,26 +625,26 @@ tryReduceExpr globals locals = \case -- corresponding argument in the scrutinee. Case m scrut branches | (expr, termArgs) <- unfoldApp (removeAnn scrut) - , (Con mCon c, _typeArgs) <- unfoldAPP expr -> - do - -- Find the branch with the same constructor - case find (\(CaseBranch n _ _) -> n == c) branches of - Just (CaseBranch _ binds rhs) -> do - -- Check that we have as many term args as bindings - when (length binds /= length termArgs) $ throwError CaseBranchBindingLengthMismatch - -- Construct a let for each bind - let makeLet (Bind _ x, e) rest = let_ x (pure e) (pure rest) - (expr', letIDs) <- - foldrM - ( \a (e, lets) -> do - l <- makeLet a e - pure (l, l ^. _id : lets) - ) - (rhs, []) - (zip binds termArgs) - pure - ( expr' - , CaseReduction + , (Con mCon c, _typeArgs) <- unfoldAPP expr -> + do + -- Find the branch with the same constructor + case find (\(CaseBranch n _ _) -> n == c) branches of + Just (CaseBranch _ binds rhs) -> do + -- Check that we have as many term args as bindings + when (length binds /= length termArgs) $ throwError CaseBranchBindingLengthMismatch + -- Construct a let for each bind + let makeLet (Bind _ x, e) rest = let_ x (pure e) (pure rest) + (expr', letIDs) <- + foldrM + ( \a (e, lets) -> do + l <- makeLet a e + pure (l, l ^. _id : lets) + ) + (rhs, []) + (zip binds termArgs) + pure + ( expr' + , CaseReduction CaseReductionDetail { caseBefore = Case m scrut branches , caseAfter = expr' @@ -656,21 +656,21 @@ tryReduceExpr globals locals = \case , caseBranchRhsID = rhs ^. _id , caseLetIDs = letIDs } - ) - Nothing -> throwError NoMatchingCaseBranch + ) + Nothing -> throwError NoMatchingCaseBranch _ -> throwError NotRedex where mkLetRemovalDetail expr body x meta = pure ( body , LetRemoval - LetRemovalDetail - { letRemovalBefore = expr - , letRemovalAfter = body - , letRemovalBindingName = x - , letRemovalLetID = meta ^. _id - , letRemovalBodyID = body ^. _id - } + LetRemovalDetail + { letRemovalBefore = expr + , letRemovalAfter = body + , letRemovalBindingName = x + , letRemovalLetID = meta ^. _id + , letRemovalBodyID = body ^. _id + } ) tryReduceType :: @@ -686,11 +686,11 @@ tryReduceType _globals locals = \case -- lambda that hasn't yet been reduced. TVar mTVar x | Just (i, Right t) <- Map.lookup x locals -> do - -- Since we're duplicating @t@, we must regenerate all its IDs. - t' <- regenerateTypeIDs t - pure - ( t' - , LocalTypeVarInline + -- Since we're duplicating @t@, we must regenerate all its IDs. + t' <- regenerateTypeIDs t + pure + ( t' + , LocalTypeVarInline LocalVarInlineDetail { localVarInlineLetID = i , localVarInlineVarID = mTVar ^. _id @@ -699,7 +699,7 @@ tryReduceType _globals locals = \case , localVarInlineReplacementID = t' ^. _id , localVarInlineIsTypeVar = True } - ) + ) _ -> throwError NotRedex -- Traverse a type, regenerating all its IDs diff --git a/primer/src/Primer/EvalFull.hs b/primer/src/Primer/EvalFull.hs index 21ea64cbf..75ffa7751 100644 --- a/primer/src/Primer/EvalFull.hs +++ b/primer/src/Primer/EvalFull.hs @@ -165,8 +165,8 @@ evalFullStepCount tydefs env n d = go 0 go s expr | s >= n = pure (s, Left $ TimedOut expr) | otherwise = case step tydefs env d expr of - Nothing -> pure (s, Right expr) -- this is a normal form - Just me -> me >>= go (s + 1) + Nothing -> pure (s, Right expr) -- this is a normal form + Just me -> me >>= go (s + 1) -- The 'Dir' argument only affects what happens if the root is an annotation: -- do we keep it (Syn) or remove it (Chk). I.e. is an upsilon reduction allowed @@ -236,17 +236,17 @@ viewCaseRedex tydefs = \case -- do a BETA reduction)! Case _ (Ann _ expr ty) brs | Just (c, _, as, xs, e) <- extract expr brs - , Just argTys <- instantiateCon ty c -> - formCaseRedex (Left ty) c argTys as xs e + , Just argTys <- instantiateCon ty c -> + formCaseRedex (Left ty) c argTys as xs e -- In the constructors-are-synthesisable case, we don't have the benefit of -- an explicit annotation, and have to work out the type based off the name -- of the constructor. Case _ expr brs | Just (c, tyargs, args, patterns, br) <- extract expr brs - , Just (_, tydef) <- lookupConstructor tydefs c - , ty <- foldl (\t a -> TApp () t $ set _typeMeta () a) (TCon () (typeDefName tydef)) (take (length $ typeDefParameters tydef) tyargs) - , Just argTys <- instantiateCon ty c -> - formCaseRedex (Right ty) c argTys args patterns br + , Just (_, tydef) <- lookupConstructor tydefs c + , ty <- foldl (\t a -> TApp () t $ set _typeMeta () a) (TCon () (typeDefName tydef)) (take (length $ typeDefParameters tydef) tyargs) + , Just argTys <- instantiateCon ty c -> + formCaseRedex (Right ty) c argTys args patterns br _ -> Nothing where extract expr brs = @@ -261,8 +261,8 @@ viewCaseRedex tydefs = \case _ -> Nothing instantiateCon ty c | Right (_, instVCs) <- instantiateValCons' tydefs $ set _typeMeta () ty - , Just (_, argTys) <- find ((== c) . fst) instVCs = - Just argTys + , Just (_, argTys) <- find ((== c) . fst) instVCs = + Just argTys | otherwise = Nothing formCaseRedex ty c argTys args patterns br = pure $ do argTys' <- sequence argTys @@ -365,14 +365,14 @@ findRedex tydefs globals dir = go . focus -- If we are substituting x->y in e.g. λy.x, we rename the y to avoid capture -- This may recompute the FV set of l quite a lot. We could be more efficient here! | fvs <- setOf _freeVarsLocal l - , not $ S.null $ fvs `S.intersection` bs = - up z <&> \z' -> case target z' of - Lam m x e -> RExpr z' $ RenameBindingsLam m x e fvs - LAM m x e -> RExpr z' $ RenameBindingsLAM m x e fvs - Case m s brs -> RExpr z' $ RenameBindingsCase m s brs fvs - -- We should replace this with a proper exception. See: - -- https://github.com/hackworthltd/primer/issues/148 - e -> error $ "Internal Error: something other than Lam/LAM/Case was a binding: " ++ show e + , not $ S.null $ fvs `S.intersection` bs = + up z <&> \z' -> case target z' of + Lam m x e -> RExpr z' $ RenameBindingsLam m x e fvs + LAM m x e -> RExpr z' $ RenameBindingsLAM m x e fvs + Case m s brs -> RExpr z' $ RenameBindingsCase m s brs fvs + -- We should replace this with a proper exception. See: + -- https://github.com/hackworthltd/primer/issues/148 + e -> error $ "Internal Error: something other than Lam/LAM/Case was a binding: " ++ show e | otherwise = goSubst n l z goSubstTy :: Name -> Type -> TypeZ -> Maybe RedexWithContext goSubstTy n t tz = case target tz of @@ -385,8 +385,8 @@ findRedex tydefs globals dir = go . focus -- If we are substituting x->y in forall y.s, we rename the y to avoid capture -- As we don't have 'let's in types, this is a big step | fvs <- freeVarsTy t - , m `S.member` fvs -> - pure $ RType tz $ RenameForall i m k s fvs + , m `S.member` fvs -> + pure $ RType tz $ RenameForall i m k s fvs _ -> eachChild tz (goSubstTy n t) -- TODO: deal with metadata. https://github.com/hackworthltd/primer/issues/6 @@ -417,14 +417,14 @@ runRedex = \case LAM m y <$> let_ x (var y) (pure e) RenameBindingsCase m s brs avoid | (brs0, CaseBranch ctor binds rhs : brs1) <- break (\(CaseBranch _ bs _) -> any ((`S.member` avoid) . bindName) bs) brs -> - let bns = map bindName binds - avoid' = avoid <> freeVars rhs <> S.fromList bns - in do - rn <- traverse (\b -> if b `S.member` avoid then Right . (b,) <$> freshName avoid' else pure $ Left b) bns - let f b@(Bind i _) = \case Left _ -> b; Right (_, w) -> Bind i w - let binds' = zipWith f binds rn - rhs' <- foldrM (\(v, w) -> let_ v (var w) . pure) rhs $ rights rn - pure $ Case m s $ brs0 ++ CaseBranch ctor binds' rhs' : brs1 + let bns = map bindName binds + avoid' = avoid <> freeVars rhs <> S.fromList bns + in do + rn <- traverse (\b -> if b `S.member` avoid then Right . (b,) <$> freshName avoid' else pure $ Left b) bns + let f b@(Bind i _) = \case Left _ -> b; Right (_, w) -> Bind i w + let binds' = zipWith f binds rn + rhs' <- foldrM (\(v, w) -> let_ v (var w) . pure) rhs $ rights rn + pure $ Case m s $ brs0 ++ CaseBranch ctor binds' rhs' : brs1 -- We should replace this with a proper exception. See: -- https://github.com/hackworthltd/primer/issues/148 | otherwise -> error "Internal Error: RenameBindingsCase found no applicable branches" @@ -453,6 +453,6 @@ renameTy a b = go t@(TForall m c k s) | c == a -> pure t | c == b -> - freshName (S.singleton a <> S.singleton b <> freeVarsTy s) >>= \c' -> - renameTy c c' s >>= fmap (TForall m c' k) . go + freshName (S.singleton a <> S.singleton b <> freeVarsTy s) >>= \c' -> + renameTy c c' s >>= fmap (TForall m c' k) . go | otherwise -> TForall m c k <$> go s diff --git a/primer/src/Primer/Questions.hs b/primer/src/Primer/Questions.hs index 77ff0d8d2..b64011ec9 100644 --- a/primer/src/Primer/Questions.hs +++ b/primer/src/Primer/Questions.hs @@ -100,8 +100,8 @@ baseNames tk = do pure $ case tk of Left (Just ty) | Just c <- headCon ty - , Just hints@(_ : _) <- typeDefNameHints <$> Map.lookup c tys -> - hints + , Just hints@(_ : _) <- typeDefNameHints <$> Map.lookup c tys -> + hints Left (Just TFun{}) -> ["f", "g", "h"] Left _ -> ["x", "y", "z"] Right (Just KType) -> ["α", "β", "γ"] diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index 8d6899552..af6bf257e 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -145,14 +145,14 @@ data KindOrType = K Kind | T Type data Cxt = Cxt { smartHoles :: SmartHoles - , -- | invariant: the key matches the 'typeDefName' inside the 'TypeDef' - typeDefs :: M.Map Name TypeDef - , -- | local variables - localCxt :: Map Name KindOrType - , -- | global variables (i.e. IDs of top-level definitions) - -- [We don't care about the name for TC purposes, but is nice to have - -- around when we generate names so we don't shadow top-level defs] - globalCxt :: Map ID (Name, Type) + , typeDefs :: M.Map Name TypeDef + -- ^ invariant: the key matches the 'typeDefName' inside the 'TypeDef' + , localCxt :: Map Name KindOrType + -- ^ local variables + , globalCxt :: Map ID (Name, Type) + -- ^ global variables (i.e. IDs of top-level definitions) + -- [We don't care about the name for TC purposes, but is nice to have + -- around when we generate names so we don't shadow top-level defs] } deriving (Show) diff --git a/primer/src/Primer/Zipper.hs b/primer/src/Primer/Zipper.hs index ff4e8e67e..e12b99368 100644 --- a/primer/src/Primer/Zipper.hs +++ b/primer/src/Primer/Zipper.hs @@ -117,16 +117,16 @@ instance HasID TypeZ where -- These fields are chosen to be convenient for renaming, and they may not be that useful for future -- actions we want to perform. data CaseBindZ = CaseBindZ - { -- | a zipper focused on the case expression - caseBindZExpr :: ExprZ - , -- | the focused binding - caseBindZFocus :: Bind' ExprMeta - , -- | the rhs of the branch - caseBindZRhs :: Expr - , -- | all other bindings in the case branch, i.e. all except the focused one - caseBindAllBindings :: [Bind' ExprMeta] - , -- | a function to update the focused binding and rhs simultaneously - caseBindZUpdate :: Bind' ExprMeta -> Expr -> ExprZ -> ExprZ + { caseBindZExpr :: ExprZ + -- ^ a zipper focused on the case expression + , caseBindZFocus :: Bind' ExprMeta + -- ^ the focused binding + , caseBindZRhs :: Expr + -- ^ the rhs of the branch + , caseBindAllBindings :: [Bind' ExprMeta] + -- ^ all other bindings in the case branch, i.e. all except the focused one + , caseBindZUpdate :: Bind' ExprMeta -> Expr -> ExprZ -> ExprZ + -- ^ a function to update the focused binding and rhs simultaneously } deriving (Generic) @@ -317,9 +317,9 @@ focusOn i = fmap snd . search matchesID -- If the target has an embedded type, search the type for a match. -- If the target is a case expression with bindings, search each binding for a match. | otherwise = - let inType = focusType z >>= search (guarded (== i) . getID . target) <&> fst <&> InType - inCaseBinds = findInCaseBinds i z - in inType <|> inCaseBinds + let inType = focusType z >>= search (guarded (== i) . getID . target) <&> fst <&> InType + inCaseBinds = findInCaseBinds i z + in inType <|> inCaseBinds -- | Focus on the node with the given 'ID', if it exists in the type focusOnTy :: ID -> Zipper Type Type -> Maybe (Zipper Type Type) @@ -336,10 +336,10 @@ search :: (IsZipper za a) => (za -> Maybe b) -> za -> Maybe (za, b) search f z | Just x <- f z = Just (z, x) | otherwise = - -- if the node has children, recurse on the leftmost child - (down z >>= search f . farthest left) - -- then recurse on the sibling to the right - <|> (right z >>= search f) + -- if the node has children, recurse on the leftmost child + (down z >>= search f . farthest left) + -- then recurse on the sibling to the right + <|> (right z >>= search f) -- | Move the zipper focus as far in one direction as possible farthest :: (a -> Maybe a) -> a -> a diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 823afa069..5a7753906 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -403,7 +403,7 @@ unit_copy_paste_type_scoping = do -- use the typechecked input p, as the result will have had a typecheck run, so -- we need the cached kinds to match up let clearIDs = set (traversed % _defIDs) 0 - in --clearIDs (set (_Just % #defName) "blank" src ) @?= clearIDs (Map.lookup toDef (progDefs r)) + in -- clearIDs (set (_Just % #defName) "blank" src ) @?= clearIDs (Map.lookup toDef (progDefs r)) clearIDs (progDefs r) @?= clearIDs (progDefs tcpExpected) -- ∀a b.a ~> ∀a.a @@ -453,7 +453,7 @@ unit_copy_paste_expr_1 = do expectPasted <- con "MakePair" `aPP` tvar "a" `aPP` tEmptyHole `app` emptyHole `app` emptyHole -- TODO: in the future we may want to insert let bindings for variables -- which are out of scope in the target, and produce something like - --expectPasted <- letType "b" tEmptyHole $ let_ "y" (emptyHole `ann` tvar "a") $ let_ "z" (emptyHole `ann` tvar "b") toCopy' + -- expectPasted <- letType "b" tEmptyHole $ let_ "y" (emptyHole `ann` tvar "a") $ let_ "z" (emptyHole `ann` tvar "b") toCopy' defInitial <- Def defID' "main" <$> skel emptyHole <*> pure ty expected <- Def defID' "main" <$> skel (pure expectPasted) <*> pure ty pure diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs index b3c69d03a..61f0e9af6 100644 --- a/primer/test/Tests/EvalFull.hs +++ b/primer/test/Tests/EvalFull.hs @@ -114,7 +114,7 @@ unit_7 = let (e, maxID) = create $ do let l = lam "x" $ var "x" `app` var "x" (l `ann` tEmptyHole) `app` l - in --in evalFullTest maxID mempty mempty 100 Syn e <~==> Left (TimedOut e) + in -- in evalFullTest maxID mempty mempty 100 Syn e <~==> Left (TimedOut e) evalFullTest maxID mempty mempty 100 Syn e <~==> Right e unit_8 :: Assertion diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs index 55471c385..d9666b601 100644 --- a/primer/test/Tests/Typecheck.hs +++ b/primer/test/Tests/Typecheck.hs @@ -195,8 +195,8 @@ hprop_decomposeTAppCon = property $ do ty <- forAll $ evalExprGen 0 $ set _typeMeta () <$> genType let dec = decomposeTAppCon ty -- See Note [cover] - --cover 30 "decomposable" $ isJust dec - --cover 30 "non-decomposable" $ isNothing dec + -- cover 30 "decomposable" $ isJust dec + -- cover 30 "non-decomposable" $ isNothing dec case dec of Nothing -> success Just (n, args) -> ty === mkTAppCon n args @@ -302,7 +302,7 @@ unit_remove_hole_not_perfect :: Assertion unit_remove_hole_not_perfect = app (hole (con "Succ")) (con "Zero") `smartSynthGives` app (hole (con "Succ")) (con "Zero") -- We currently give this as output - --app (con "Succ") (con "Zero") -- We would prefer to see the hole removed + -- app (con "Succ") (con "Zero") -- We would prefer to see the hole removed -- When not using "smart" TC which automatically inserts holes etc, -- one would have to do a bit of dance to build a case expression, and diff --git a/primer/test/Tests/Unification.hs b/primer/test/Tests/Unification.hs index 1309b3ea5..c57c6298c 100644 --- a/primer/test/Tests/Unification.hs +++ b/primer/test/Tests/Unification.hs @@ -399,7 +399,7 @@ hprop_refl = propertyWTInExtendedUVCxt defaultCxt $ \uvs -> do u <- unify' cxt uvs t t u === Just mempty ---unify _ [] S T is Nothing or Just [], exactly when S = T up to holes +-- unify _ [] S T is Nothing or Just [], exactly when S = T up to holes hprop_eq :: Property hprop_eq = propertyWTInExtendedLocalGlobalCxt defaultCxt $ do cxt <- ask @@ -428,7 +428,7 @@ hprop_only_sub_uvs = propertyWTInExtendedUVCxt defaultCxt $ \uvs -> do Nothing -> discard Just sub -> assert $ M.keysSet sub `S.isSubsetOf` uvs ---unify ga uvs S T = Maybe sub => S[sub] = T[sub] +-- unify ga uvs S T = Maybe sub => S[sub] = T[sub] hprop_sub_unifies :: Property hprop_sub_unifies = propertyWTInExtendedUVCxt defaultCxt $ \uvs -> do cxt <- ask @@ -443,7 +443,7 @@ hprop_sub_unifies = propertyWTInExtendedUVCxt defaultCxt $ \uvs -> do t' <- substTys (M.toList sub) t diff s' consistentTypes t' ---unify ga uvs S T = Maybe sub => for t/a in sub, have checkKind uvs(a) t +-- unify ga uvs S T = Maybe sub => for t/a in sub, have checkKind uvs(a) t hprop_sub_checks :: Property hprop_sub_checks = propertyWTInExtendedUVCxt' defaultCxt $ \uvs -> do cxt <- ask