From e1636b4ff2d5add8c1db0ff338eaf514059937df Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Fri, 3 May 2024 12:01:23 +0200 Subject: [PATCH] Refactor: make funAbstr a FunctionFlag --- src/full/Agda/Syntax/Common.hs | 9 +++ src/full/Agda/Syntax/Internal/Names.hs | 2 +- src/full/Agda/TypeChecking/Monad/Base.hs | 68 ++++++++++++------- src/full/Agda/TypeChecking/ProjectionLike.hs | 6 +- src/full/Agda/TypeChecking/Rules/Decl.hs | 3 +- src/full/Agda/TypeChecking/Rules/Def.hs | 16 ++--- .../Serialise/Instances/Internal.hs | 6 +- src/full/Agda/Utils/Lens.hs | 3 + 8 files changed, 74 insertions(+), 39 deletions(-) diff --git a/src/full/Agda/Syntax/Common.hs b/src/full/Agda/Syntax/Common.hs index 7f00eab8160..d1cb7872473 100644 --- a/src/full/Agda/Syntax/Common.hs +++ b/src/full/Agda/Syntax/Common.hs @@ -37,6 +37,7 @@ import Agda.Syntax.Common.Pretty import Agda.Syntax.Position import Agda.Utils.BiMap (HasTag(..)) +import Agda.Utils.Boolean (Boolean(fromBool), IsBool(toBool)) import Agda.Utils.Functor import Agda.Utils.Lens import Agda.Utils.List1 ( List1, pattern (:|), (<|) ) @@ -2383,6 +2384,14 @@ instance Monoid IsAbstract where mempty = ConcreteDef mappend = (<>) +instance Boolean IsAbstract where + fromBool True = AbstractDef + fromBool False = ConcreteDef + +instance IsBool IsAbstract where + toBool AbstractDef = True + toBool ConcreteDef = False + instance KillRange IsAbstract where killRange = id diff --git a/src/full/Agda/Syntax/Internal/Names.hs b/src/full/Agda/Syntax/Internal/Names.hs index 937d0e565c0..90df32a2803 100644 --- a/src/full/Agda/Syntax/Internal/Names.hs +++ b/src/full/Agda/Syntax/Internal/Names.hs @@ -161,7 +161,7 @@ instance NamesIn Defn where PrimitiveSort _ s -> namesAndMetasIn' sg s AbstractDefn{} -> __IMPOSSIBLE__ -- Andreas 2017-07-27, Q: which names can be in @cc@ which are not already in @cl@? - Function cl cc _ _ _ _ _ _ _ _ _ el _ _ _ + Function cl cc _ _ _ _ _ _ _ _ el _ _ _ -> namesAndMetasIn' sg (cl, cc, el) Datatype _ _ cl cs s _ _ _ trX trD -> namesAndMetasIn' sg (cl, cs, s, trX, trD) diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs index 54eba543ba5..6ced89833f0 100644 --- a/src/full/Agda/TypeChecking/Monad/Base.hs +++ b/src/full/Agda/TypeChecking/Monad/Base.hs @@ -111,6 +111,7 @@ import Agda.Interaction.Library import Agda.Utils.Benchmark (MonadBench(..)) import Agda.Utils.BiMap (BiMap, HasTag(..)) import qualified Agda.Utils.BiMap as BiMap +import Agda.Utils.Boolean ( fromBool, toBool ) import Agda.Utils.CallStack ( CallStack, HasCallStack, withCallerCallStack ) import Agda.Utils.FileName import Agda.Utils.Functor @@ -2328,6 +2329,8 @@ data FunctionFlag | FunErasure -- ^ Was @--erasure@ in effect when the function was defined? -- (This can affect the type of a projection.) + | FunAbstract + -- ^ Is the function abstract? deriving (Eq, Ord, Enum, Show, Generic, Ix, Bounded) instance SmallSetElement FunctionFlag @@ -2420,7 +2423,6 @@ data FunctionData = FunctionData -- Does include this function. -- Empty list if not recursive. -- @Nothing@ if not yet computed (by positivity checker). - , _funAbstr :: IsAbstract , _funProjection :: Either ProjectionLikenessMissing Projection -- ^ Is it a record projection? -- If yes, then return the name of the record type and index of @@ -2429,6 +2431,7 @@ data FunctionData = FunctionData -- instantiation.) This information is used in the termination -- checker. , _funFlags :: SmallSet FunctionFlag + -- ^ Various boolean flags pertaining to the function definition, see 'FunctionFlag'. , _funTerminates :: Maybe Bool -- ^ Has this function been termination checked? Did it pass? , _funExtLam :: Maybe ExtLamInfo @@ -2454,7 +2457,6 @@ pattern Function -> [Clause] -> FunctionInverse -> Maybe [QName] - -> IsAbstract -> Either ProjectionLikenessMissing Projection -> SmallSet FunctionFlag -> Maybe Bool @@ -2471,7 +2473,6 @@ pattern Function , funCovering , funInv , funMutual - , funAbstr , funProjection , funFlags , funTerminates @@ -2487,7 +2488,6 @@ pattern Function funCovering funInv funMutual - funAbstr funProjection funFlags funTerminates @@ -2843,7 +2843,6 @@ instance Pretty FunctionData where _funCovering funInv funMutual - funAbstr funProjection funFlags funTerminates @@ -2859,7 +2858,6 @@ instance Pretty FunctionData where , "funTreeless =" pretty funTreeless , "funInv =" pretty funInv , "funMutual =" pshow funMutual - , "funAbstr =" pshow funAbstr , "funProjection =" pretty funProjection , "funFlags =" pshow funFlags , "funTerminates =" pshow funTerminates @@ -3009,7 +3007,6 @@ emptyFunctionData_ erasure = FunctionData , _funTreeless = Nothing , _funInv = NotInjective , _funMutual = Nothing - , _funAbstr = ConcreteDef , _funProjection = Left MaybeProjection , _funFlags = SmallSet.fromList [ FunErasure | erasure ] , _funTerminates = Nothing @@ -3026,17 +3023,24 @@ emptyFunction = FunctionDefn <$> emptyFunctionData emptyFunction_ :: Bool -> Defn emptyFunction_ = FunctionDefn . emptyFunctionData_ -funFlag :: FunctionFlag -> Lens' Defn Bool -funFlag flag f def@Function{ funFlags = flags } = +funFlag_ :: FunctionFlag -> Lens' FunctionData Bool +funFlag_ flag f def@FunctionData{ _funFlags = flags } = f (SmallSet.member flag flags) <&> - \ b -> def{ funFlags = (if b then SmallSet.insert else SmallSet.delete) flag flags } -funFlag _ f def = f False $> def + \ b -> def{ _funFlags = (if b then SmallSet.insert else SmallSet.delete) flag flags } + +funFlag :: FunctionFlag -> Lens' Defn Bool +funFlag flag f = \case + FunctionDefn d -> FunctionDefn <$> funFlag_ flag f d + def -> f False $> def funStatic, funInline, funMacro :: Lens' Defn Bool funStatic = funFlag FunStatic funInline = funFlag FunInline funMacro = funFlag FunMacro +funMacro_ :: Lens' FunctionData Bool +funMacro_ = funFlag_ FunMacro + -- | Toggle the 'FunFirstOrder' flag. funFirstOrder :: Lens' Defn Bool funFirstOrder = funFlag FunFirstOrder @@ -3045,6 +3049,22 @@ funFirstOrder = funFlag FunFirstOrder funErasure :: Lens' Defn Bool funErasure = funFlag FunErasure +-- | Toggle the 'FunAbstract' flag. +funAbstract :: Lens' Defn Bool +funAbstract = funFlag FunAbstract + +-- | Toggle the 'FunAbstract' flag. +funAbstr :: Lens' Defn IsAbstract +funAbstr = funAbstract . iso fromBool toBool + +-- | Toggle the 'FunAbstract' flag. +funAbstract_ :: Lens' FunctionData Bool +funAbstract_ = funFlag_ FunAbstract + +-- | Toggle the 'FunAbstract' flag. +funAbstr_ :: Lens' FunctionData IsAbstract +funAbstr_ = funAbstract_ . iso fromBool toBool + isMacro :: Defn -> Bool isMacro = (^. funMacro) @@ -3255,17 +3275,17 @@ defTerminationUnconfirmed Defn{theDef = Function{funTerminates = _ }} = T defTerminationUnconfirmed _ = False defAbstract :: Definition -> IsAbstract -defAbstract d = case theDef d of - Axiom{} -> ConcreteDef - DataOrRecSig{} -> ConcreteDef - GeneralizableVar{} -> ConcreteDef - AbstractDefn{} -> AbstractDef - Function{funAbstr = a} -> a - Datatype{dataAbstr = a} -> a - Record{recAbstr = a} -> a - Constructor{conAbstr = a} -> a - Primitive{primAbstr = a} -> a - PrimitiveSort{} -> ConcreteDef +defAbstract def = case theDef def of + AxiomDefn _ -> ConcreteDef + DataOrRecSigDefn _ -> ConcreteDef + GeneralizableVar -> ConcreteDef + AbstractDefn _ -> AbstractDef + FunctionDefn d -> d ^. funAbstr_ + DatatypeDefn d -> _dataAbstr d + RecordDefn d -> _recAbstr d + ConstructorDefn d -> _conAbstr d + PrimitiveDefn d -> _primAbstr d + PrimitiveSortDefn _ -> ConcreteDef defOpaque :: Definition -> IsOpaque defOpaque d = case theDef d of @@ -5823,8 +5843,8 @@ instance KillRange Defn where DataOrRecSig n -> DataOrRecSig n GeneralizableVar -> GeneralizableVar AbstractDefn{} -> __IMPOSSIBLE__ -- only returned by 'getConstInfo'! - Function a b c d e f g h i j k l m n o -> - killRangeN Function a b c d e f g h i j k l m n o + Function a b c d e f g h i j k l m n -> + killRangeN Function a b c d e f g h i j k l m n Datatype a b c d e f g h i j -> killRangeN Datatype a b c d e f g h i j Record a b c d e f g h i j k l m -> killRangeN Record a b c d e f g h i j k l m Constructor a b c d e f g h i j k -> killRangeN Constructor a b c d e f g h i j k diff --git a/src/full/Agda/TypeChecking/ProjectionLike.hs b/src/full/Agda/TypeChecking/ProjectionLike.hs index d14e56cfeae..303385b62c5 100644 --- a/src/full/Agda/TypeChecking/ProjectionLike.hs +++ b/src/full/Agda/TypeChecking/ProjectionLike.hs @@ -81,6 +81,7 @@ import Agda.TypeChecking.Telescope import Agda.TypeChecking.DropArgs +import Agda.Utils.Lens import Agda.Utils.List import Agda.Utils.Maybe import Agda.Utils.Monad @@ -271,7 +272,7 @@ makeProjection x = whenM (optProjectionLike <$> pragmaOptions) $ do def@Function{funProjection = Left MaybeProjection, funClauses = cls, funSplitTree = st0, funCompiled = cc0, funInv = NotInjective, funMutual = Just [], -- Andreas, 2012-09-28: only consider non-mutual funs - funAbstr = ConcreteDef, funOpaque = TransparentDef} -> do + funOpaque = TransparentDef} | not (def ^. funAbstract) -> do ps0 <- filterM validProj $ candidateArgs [] t reportSLn "tc.proj.like" 30 $ if null ps0 then " no candidates found" else " candidates: " ++ prettyShow ps0 @@ -326,7 +327,7 @@ makeProjection x = whenM (optProjectionLike <$> pragmaOptions) $ do } Function{funInv = Inverse{}} -> reportSLn "tc.proj.like" 30 $ " injective functions can't be projections" - Function{funAbstr = AbstractDef} -> + d@Function{} | d ^. funAbstract -> reportSLn "tc.proj.like" 30 $ " abstract functions can't be projections" Function{funOpaque = OpaqueDef _} -> reportSLn "tc.proj.like" 30 $ " opaque functions can't be projections" @@ -338,6 +339,7 @@ makeProjection x = whenM (optProjectionLike <$> pragmaOptions) $ do reportSLn "tc.proj.like" 30 $ " mutual functions can't be projections" Function{funMutual = Nothing} -> reportSLn "tc.proj.like" 30 $ " mutuality check has not run yet" + Function{} -> __IMPOSSIBLE__ -- match is complete, but GHC does not see this (because of d^.funAbstract) Axiom{} -> reportSLn "tc.proj.like" 30 $ " not a function, but Axiom" DataOrRecSig{} -> reportSLn "tc.proj.like" 30 $ " not a function, but DataOrRecSig" GeneralizableVar{} -> reportSLn "tc.proj.like" 30 $ " not a function, but GeneralizableVar" diff --git a/src/full/Agda/TypeChecking/Rules/Decl.hs b/src/full/Agda/TypeChecking/Rules/Decl.hs index 74450414d89..8e3f8fe8de3 100644 --- a/src/full/Agda/TypeChecking/Rules/Decl.hs +++ b/src/full/Agda/TypeChecking/Rules/Decl.hs @@ -676,7 +676,8 @@ checkAxiom' gentel kind i info0 mp x e = whenAbstractFreezeMetasAfter i $ defaul RecName -> DataOrRecSig npars AxiomName -> defaultAxiom -- Old comment: NB: used also for data and record type sigs _ -> __IMPOSSIBLE__ - where fun = FunctionDefn funD{ _funAbstr = Info.defAbstract i, _funOpaque = Info.defOpaque i } + where + fun = FunctionDefn $ set funAbstr_ (Info.defAbstract i) funD{ _funOpaque = Info.defOpaque i } addConstant x =<< do useTerPragma $ defn diff --git a/src/full/Agda/TypeChecking/Rules/Def.hs b/src/full/Agda/TypeChecking/Rules/Def.hs index b420790a0a7..e0e32925a6f 100644 --- a/src/full/Agda/TypeChecking/Rules/Def.hs +++ b/src/full/Agda/TypeChecking/Rules/Def.hs @@ -192,9 +192,10 @@ checkAlias t ai i name e mc = -- Add the definition fun <- emptyFunctionData - addConstant' name ai name t $ set funMacro (Info.defMacro i == MacroDef) $ - FunctionDefn fun - { _funClauses = [ Clause -- trivial clause @name = v@ + addConstant' name ai name t $ FunctionDefn $ + set funMacro_ (Info.defMacro i == MacroDef) $ + set funAbstr_ (Info.defAbstract i) $ + fun { _funClauses = [ Clause -- trivial clause @name = v@ { clauseLHSRange = getRange i , clauseFullRange = getRange i , clauseTel = EmptyTel @@ -210,7 +211,6 @@ checkAlias t ai i name e mc = } ] , _funCompiled = Just $ Done [] $ bodyMod v , _funSplitTree = Just $ SplittingDone 0 - , _funAbstr = Info.defAbstract i , _funOpaque = Info.defOpaque i } @@ -435,14 +435,14 @@ checkFunDefS t ai extlam with i name withSubAndLets cs = do -- If there was a pragma for this definition, we can set the -- funTerminates field directly. fun <- emptyFunctionData - defn <- autoInline $ - set funMacro (ismacro || Info.defMacro i == MacroDef) $ - FunctionDefn fun + defn <- autoInline $ FunctionDefn $ + set funMacro_ (ismacro || Info.defMacro i == MacroDef) $ + set funAbstr_ (Info.defAbstract i) $ + fun { _funClauses = cs , _funCompiled = Just cc , _funSplitTree = mst , _funInv = inv - , _funAbstr = Info.defAbstract i , _funOpaque = Info.defOpaque i , _funExtLam = (\ e -> e { extLamSys = sys }) <$> extlam , _funWith = with diff --git a/src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs b/src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs index 87f8f367dc2..73b003d7dd9 100644 --- a/src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs +++ b/src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs @@ -421,7 +421,7 @@ instance EmbPrj BuiltinSort where instance EmbPrj Defn where icod_ (Axiom a) = icodeN 0 Axiom a - icod_ (Function a b s t u c d e f g h i j k l) = icodeN 1 (\ a b s -> Function a b s t) a b s u c d e f g h i j k l + icod_ (Function a b s t u c d e f g h i j k) = icodeN 1 (\ a b s -> Function a b s t) a b s u c d e f g h i j k icod_ (Datatype a b c d e f g h i j) = icodeN 2 Datatype a b c d e f g h i j icod_ (Record a b c d e f g h i j k l m) = icodeN 3 Record a b c d e f g h i j k l m icod_ (Constructor a b c d e f g h i j k) = icodeN 4 Constructor a b c d e f g h i j k @@ -433,8 +433,8 @@ instance EmbPrj Defn where value = vcase valu where valu [0, a] = valuN Axiom a - valu [1, a, b, s, u, c, d, e, f, g, h, i, j, k, l] - = valuN (\ a b s -> Function a b s Nothing) a b s u c d e f g h i j k l + valu [1, a, b, s, u, c, d, e, f, g, h, i, j, k] + = valuN (\ a b s -> Function a b s Nothing) a b s u c d e f g h i j k valu [2, a, b, c, d, e, f, g, h, i, j] = valuN Datatype a b c d e f g h i j valu [3, a, b, c, d, e, f, g, h, i, j, k, l, m] = valuN Record a b c d e f g h i j k l m valu [4, a, b, c, d, e, f, g, h, i, j, k] = valuN Constructor a b c d e f g h i j k diff --git a/src/full/Agda/Utils/Lens.hs b/src/full/Agda/Utils/Lens.hs index 233c4e2bc49..146af1f80d7 100644 --- a/src/full/Agda/Utils/Lens.hs +++ b/src/full/Agda/Utils/Lens.hs @@ -55,6 +55,9 @@ set l = over l . const over :: Lens' o i -> LensMap o i over l f o = runIdentity $ l (Identity . f) o +-- | Build a lens out of an isomorphism. +iso :: (o -> i) -> (i -> o) -> Lens' o i +iso get set f = fmap set . f . get -- * State accessors and modifiers using 'StateT'.