Refactor: make funAbstr a FunctionFlag

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
 

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)

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

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"

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

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

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

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'.