Formulas (#19)

* Formulas

* Memoization

* Fix anyOf

openapi-diff.cabal

@@ -86,6 +86,7 @@ library
   import:              common-options
   hs-source-dirs:      src
   exposed-modules:  OpenAPI.Checker.Aux
+                  , OpenAPI.Checker.Formula
                   , OpenAPI.Checker.Memo
                   , OpenAPI.Checker.Report
                   , OpenAPI.Checker.Run

src/OpenAPI/Checker/Formula.hs

@@ -0,0 +1,75 @@
+module OpenAPI.Checker.Formula
+  ( FormulaF
+  , VarRef
+  , anyOf
+  , anError
+  , calculate
+  ) where
+
+import Data.Kind
+import Data.Monoid
+import qualified Data.List.NonEmpty as NE
+import OpenAPI.Checker.Trace
+import qualified OpenAPI.Checker.TracePrefixTree as T
+
+type VarRef = Int
+
+-- | The type @FormulaF f r ()@ describes (modulo contents of errors) boolean
+-- formulas involving variables, conjunctions, and disjunctions. These
+-- operations (and the generated algebra) are monotonous. This ensures that
+-- there always exist fixpoints, i.e. that @x = f x@ has at least one solution.
+data FormulaF (f :: k -> Type) (r :: k) (a :: Type) where
+  Result :: a -> FormulaF f r a
+  Errors :: !(T.TracePrefixTree f r) -> FormulaF f r a
+    -- ^ invariant: never empty
+  Apply :: FormulaF f r (b -> c) -> FormulaF f r b -> (c -> a) -> FormulaF f r a
+    -- ^ invariant: LHS and RHS are never 'Result' nor 'Errors'
+  SelectFirst :: NE.NonEmpty (FormulaF f r b)
+    -> !(AnItem f r) -> (b -> a) -> FormulaF f r a
+    -- ^ invariant: the list doesn't contain any 'Result's or 'Errors'.
+  Variable :: !VarRef -> FormulaF f r a
+
+anError :: AnItem f r -> FormulaF f r a
+anError e = Errors $ T.singleton e
+
+instance Functor (FormulaF f r) where
+  fmap f (Result x) = Result (f x)
+  fmap _ (Errors e) = Errors e
+  fmap f (Apply g x h) = Apply g x (f . h)
+  fmap f (SelectFirst xs e h) = SelectFirst xs e (f . h)
+  fmap _ (Variable r) = Variable r
+
+instance Applicative (FormulaF f r) where
+  pure = Result
+  Result f <*> x = f <$> x
+  Errors e <*> Result _ = Errors e
+  Errors e1 <*> Errors e2 = Errors (e1 <> e2)
+  f <*> x = Apply f x id
+
+anyOf :: [FormulaF f r a] -> AnItem f r -> FormulaF f r a
+anyOf fs allE = case foldMap check fs of
+  (First (Just x), _) -> Result x
+  (First Nothing, (x:xs)) -> SelectFirst (x NE.:| xs) allE id
+  (First Nothing, []) -> Errors $ T.singleton allE
+  where
+    check (Result x) = (First (Just x), mempty)
+    check (Errors _) = (mempty, mempty)
+    check (SelectFirst xs _ h) = (mempty, NE.toList (fmap (fmap h) xs))
+    check x = (mempty, [x])
+
+calculate :: FormulaF f r a -> Either (T.TracePrefixTree f r) a
+calculate (Result x) = Right x
+calculate (Errors e) = Left e
+calculate (Apply f x h) = case calculate f of
+  Left e1 -> case calculate x of
+    Left e2 -> Left (e1 <> e2)
+    Right _ -> Left e1
+  Right f' -> case calculate x of
+    Left e2 -> Left e2
+    Right x' -> Right (h (f' x'))
+calculate (SelectFirst xs e h) = go (calculate <$> NE.toList xs)
+  where
+    go (Left _ : rs) = go rs
+    go (Right x : _) = Right (h x)
+    go [] = Left $ T.singleton e
+calculate (Variable i) = error $ "Unknown variable " <> show i

src/OpenAPI/Checker/Memo.hs

@@ -1,70 +1,125 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 -- | Utilities for effectfully memoizing other, more effectful functions.
 module OpenAPI.Checker.Memo
-  ( Progress(..)
-  , MonadMemo
+  ( MonadMemo
   , MemoState
   , runMemo
-  , tryMemo
-  , tryMemoWithTag
+  , modifyMemoNonce
+  , KnotTier(..)
+  , unknot
+  , memoWithKnot
+  , memoTaggedWithKnot
   ) where
 
 import Control.Monad.State
+import Data.Dynamic
 import qualified Data.Map as M
 import Data.Tagged
+import Data.Void
 import qualified Data.TypeRepMap as T
 import Type.Reflection
 
--- | A computation has either 'Finished', or it is 'InProgress'.
-data Progress a = Finished a | InProgress
-  deriving (Eq, Ord, Show)
+data Progress a = Finished a | Started | TyingKnot Dynamic
 
 data MemoMap a where
   MemoMap :: !(M.Map k (Progress v)) -> MemoMap (k, v)
 
-newtype MemoState = MemoState (T.TypeRepMap MemoMap)
+data MemoState s = MemoState s (T.TypeRepMap MemoMap)
 
 -- | An effectful memoization monad.
-type MonadMemo m = MonadState MemoState m
+type MonadMemo s m = MonadState (MemoState s) m
 
 memoStateLookup
-  :: forall k v. (Typeable k, Typeable v, Ord k)
-  => k -> MemoState -> Maybe (Progress v)
-memoStateLookup k (MemoState t) = case T.lookup @(k, v) t of
+  :: forall k v s. (Typeable k, Typeable v, Ord k)
+  => k -> MemoState s -> Maybe (Progress v)
+memoStateLookup k (MemoState _ t) = case T.lookup @(k, v) t of
   Just (MemoMap m) -> M.lookup k m
   Nothing -> Nothing
 
 memoStateInsert
-  :: forall k v. (Typeable k, Typeable v, Ord k)
-  => k -> Progress v -> MemoState -> MemoState
-memoStateInsert k x (MemoState t) = MemoState $ T.insert (MemoMap m'') t
+  :: forall k v s. (Typeable k, Typeable v, Ord k)
+  => k -> Progress v -> MemoState s -> MemoState s
+memoStateInsert k x (MemoState s t) = MemoState s $ T.insert (MemoMap m'') t
   where
     m'' = M.insert k x m'
     m' = case T.lookup @(k, v) t of
       Just (MemoMap m) -> m
       Nothing -> M.empty
 
--- | Run a memoized computation.
-runMemo :: Monad m => StateT MemoState m a -> m a
-runMemo = (`evalStateT` MemoState T.empty)
+modifyMemoNonce :: MonadMemo s m => (s -> s) -> m s
+modifyMemoNonce f = do
+  MemoState s t <- get
+  put $ MemoState (f s) t
+  pure s
 
--- | Try to call a function whilst memoizing its result. If we are already
--- inside an evaluation of some function with these arguments, this returns
--- @InProgress@. Beware of different functions that have the same type.
-tryMemo
-  :: forall k v m. (Typeable k, Typeable v, Ord k, MonadMemo m)
-  => (k -> m v) -> k -> m (Progress v)
-tryMemo f k = memoStateLookup k <$> get >>= \case
-  Just x -> pure x
+-- | Run a memoized computation.
+runMemo :: Monad m => s -> StateT (MemoState s) m a -> m a
+runMemo s = (`evalStateT` MemoState s T.empty)
+
+-- | A description of how to effectfully tie knots in type @v@, using the @m@
+-- monad, and by sharing some @d@ data among the recursive instances.
+data KnotTier v d m = KnotTier
+  { onKnotFound :: m d -- ^ Create some data that will be connected to this knot
+  , onKnotUsed :: d -> m v -- ^ This is what the knot will look like as a value
+    -- to the inner computations
+  , tieKnot :: d -> v -> m v -- ^ Once we're done and we're outside, tie the
+    -- knot using the datum
+  }
+
+unknot :: KnotTier v Void m
+unknot = KnotTier
+  { onKnotFound = error "Recursion detected"
+  , onKnotUsed = absurd
+  , tieKnot = absurd
+  }
+
+-- | Run a potentially recursive computation. The provided key will be used to
+-- refer to the result of this computation. If during the computation, another
+-- attempt to run the computation with the same key is made, we run a
+-- tying-the-knot procedure.
+--
+-- If another attempt to run the computation with the same key is made
+-- *after we're done*, we will return the memoized value.
+memoWithKnot
+  :: forall k v d m s.
+    (Typeable k, Typeable v, Typeable d, Ord k, MonadMemo s m)
+  => KnotTier v d m
+  -> m v -- ^ the computation to memoize
+  -> k -- ^ key for memoization
+  -> m v
+memoWithKnot tier f k = memoStateLookup @k @v k <$> get >>= \case
+  Just (Finished v) -> pure v
+  Just Started -> do
+    d <- onKnotFound tier
+    modify $ memoStateInsert @k @v k (TyingKnot $ toDyn d)
+    onKnotUsed tier d
+  Just (TyingKnot dyn) -> case fromDynamic dyn of
+    Just d -> onKnotUsed tier d
+    Nothing -> error $ "Type mismatch when examining the knot of "
+      <> show (typeRep @(k -> v)) <> ": expected " <> show (typeRep @d)
+      <> ", got " <> show (dynTypeRep dyn)
   Nothing -> do
-    modify $ memoStateInsert k (InProgress @v)
-    result <- Finished <$> f k
-    modify $ memoStateInsert k result
-    pure result
+    modify $ memoStateInsert @k @v k Started
+    v <- f
+    v' <- memoStateLookup @k @v k <$> get >>= \case
+      Just Started -> pure v
+      Just (TyingKnot dyn) -> case fromDynamic dyn of
+        Just d -> tieKnot tier d v
+        Nothing -> error $ "Type mismatch when tying the knot of "
+          <> show (typeRep @(k -> v)) <> ": expected " <> show (typeRep @d)
+          <> ", got " <> show (dynTypeRep dyn)
+      Just (Finished _) -> error $ "Unexpected Finished when memoizing "
+          <> show (typeRep @(k -> v))
+      Nothing -> error $ "No key found when memoizing "
+          <> show (typeRep @(k -> v))
+    modify $ memoStateInsert @k @v k (Finished v')
+    pure v'
 
 -- | Disambiguate memoized computations with an arbitrary tag.
-tryMemoWithTag
-  :: forall t k v m. (Typeable t, Typeable k, Typeable v, Ord k, MonadMemo m)
-  => (k -> m v) -> k -> m (Progress v)
-tryMemoWithTag f k = withTypeable (typeRepKind $ typeRep @t) $
-  tryMemo (f . unTagged) (Tagged @t k)
+memoTaggedWithKnot
+  :: forall t k v d m s.
+    ( Typeable t, Typeable k, Typeable v, Typeable d
+    , Ord k, MonadMemo s m )
+  => KnotTier v d m -> m v -> k -> m v
+memoTaggedWithKnot tier f k = withTypeable (typeRepKind $ typeRep @t) $
+  memoWithKnot tier f (Tagged @t k)

src/OpenAPI/Checker/Subtree.hs

@@ -2,27 +2,24 @@ module OpenAPI.Checker.Subtree
   ( APIStep(..)
   , Subtree(..)
   , CompatM(..)
-  , runCompatM
+  , CompatFormula
+  , runCompatFormula
+  , localM
   , local'
-  , warnIssue
-  , throwIssue
-  , warnIssueAt
-  , throwIssueAt
-  , throwWarnings
-  , warnIssues
+  , issueAtTrace
+  , issueAt
+  , memo
   ) where
 
-import Control.Monad.Error.Class
 import Control.Monad.Identity
-import Control.Monad.Reader.Class
-import Control.Monad.Trans.Except (ExceptT, runExceptT)
-import Control.Monad.Trans.Reader (ReaderT(..))
-import Control.Monad.Trans.State (StateT)
-import Control.Monad.Trans.Writer.Strict (WriterT, runWriterT)
-import Control.Monad.Writer.Class
+import Control.Monad.Reader
+import Control.Monad.State
+import Data.Functor.Compose
 import Data.Kind
 import Data.OpenApi
 import Data.Text
+import Data.Typeable
+import OpenAPI.Checker.Formula
 import OpenAPI.Checker.Memo
 import OpenAPI.Checker.Trace
 import qualified OpenAPI.Checker.TracePrefixTree as T
@@ -48,64 +45,60 @@ data TracedEnv t = TracedEnv
 newtype CompatM t a = CompatM
   { unCompatM ::
     ReaderT (ProdCons (TracedEnv t))
-      (ExceptT (T.TracePrefixTree CheckIssue OpenApi)
-        (WriterT (T.TracePrefixTree CheckIssue OpenApi)
-          (StateT MemoState Identity))) a
+      (StateT (MemoState VarRef) Identity) a
   } deriving newtype
     ( Functor, Applicative, Monad
     , MonadReader (ProdCons (TracedEnv t))
-    , MonadError (T.TracePrefixTree CheckIssue OpenApi)
-    , MonadWriter (T.TracePrefixTree CheckIssue OpenApi)
+    , MonadState (MemoState VarRef)
     )
 
-class (Ord t, Ord (CheckIssue t)) => Subtree (t :: Type) where
+type CompatFormula t = Compose (CompatM t) (FormulaF CheckIssue OpenApi)
+
+class (Typeable t, Ord t, Ord (CheckIssue t)) => Subtree (t :: Type) where
   type family CheckEnv t :: Type
   data family CheckIssue t :: Type
-  checkCompatibility :: ProdCons t -> CompatM t a
+  -- | If we ever followed a reference, reroute the path through "components"
+  normalizeTrace :: Trace OpenApi t -> Trace OpenApi t
+  checkCompatibility :: ProdCons t -> CompatFormula t ()
 
-runCompatM :: ProdCons (TracedEnv t) -> CompatM t a ->
-  ( Either (T.TracePrefixTree CheckIssue OpenApi) a -- unrecovarable errors
-  , T.TracePrefixTree CheckIssue OpenApi ) -- warnings
-runCompatM env = runIdentity . runMemo . runWriterT
-  . runExceptT . (`runReaderT` env) . unCompatM
+runCompatFormula
+  :: ProdCons (TracedEnv t)
+  -> Compose (CompatM t) (FormulaF f r) a
+  -> Either (T.TracePrefixTree f r) a
+runCompatFormula env (Compose f)
+  = calculate . runIdentity . runMemo 0 . (`runReaderT` env) . unCompatM $ f
 
-local'
+localM
   :: ProdCons (Trace a b)
   -> (ProdCons (CheckEnv a) -> ProdCons (CheckEnv b))
   -> CompatM b x
   -> CompatM a x
-local' xs wrapEnv (CompatM k) = CompatM $ ReaderT $ \env ->
+localM xs wrapEnv (CompatM k) = CompatM $ ReaderT $ \env ->
   runReaderT k $ TracedEnv
     <$> (catTrace <$> (getTrace <$> env) <*> xs)
     <*> wrapEnv (getEnv <$> env)
 
-warnIssue :: Subtree t => Trace OpenApi t -> CheckIssue t -> CompatM t ()
-warnIssue xs issue = tell $ T.singleton $ AnItem xs issue
+local'
+  :: ProdCons (Trace a b)
+  -> (ProdCons (CheckEnv a) -> ProdCons (CheckEnv b))
+  -> Compose (CompatM b) (FormulaF f r) x
+  -> Compose (CompatM a) (FormulaF f r) x
+local' xs wrapEnv (Compose h) = Compose (localM xs wrapEnv h)
 
-throwIssue :: Subtree t => Trace OpenApi t -> CheckIssue t -> CompatM t a
-throwIssue xs issue = throwError $ T.singleton $ AnItem xs issue
+issueAtTrace
+  :: Subtree t => Trace OpenApi t -> CheckIssue t -> CompatFormula t a
+issueAtTrace xs issue = Compose $ pure $ anError $ AnItem xs issue
 
-warnIssueAt
+issueAt
   :: Subtree t
   => (forall x. ProdCons x -> x)
   -> CheckIssue t
-  -> CompatM t ()
-warnIssueAt f issue = do
+  -> CompatFormula t a
+issueAt f issue = Compose $ do
   xs <- asks $ getTrace . f
-  warnIssue xs issue
+  pure $ anError $ AnItem xs issue
 
-throwIssueAt
-  :: Subtree t
-  => (forall x. ProdCons x -> x)
-  -> CheckIssue t
-  -> CompatM t a
-throwIssueAt f issue = do
-  xs <- asks $ getTrace . f
-  throwIssue xs issue
-
-throwWarnings :: CompatM t a -> CompatM t a
-throwWarnings k = listen k >>= \case
-  (x, issues) -> if T.null issues then pure x else throwError issues
-
-warnIssues :: CompatM t a -> CompatM t (Maybe a)
-warnIssues k = catchError (Just <$> k) (\issues -> Nothing <$ tell issues)
+memo :: (Subtree t, Typeable a) => CompatFormula t a -> CompatFormula t a
+memo (Compose f) = Compose $ do
+  pxs <- asks (normalizeTrace . getTrace <$>)
+  memoWithKnot unknot f pxs

src/OpenAPI/Checker/TracePrefixTree.hs

@@ -24,9 +24,9 @@ import Data.Type.Equality
 
 -- | A list of @AnItem r f@, but optimized into a prefix tree.
 data TracePrefixTree (f :: k -> Type) (r :: k) = TracePrefixTree
-    { rootItems :: !(ASet (f r))
-    , snocItems :: !(T.TypeRepMap (AStep f r))
-    }
+  { rootItems :: !(ASet (f r))
+  , snocItems :: !(T.TypeRepMap (AStep f r))
+  }
 
 deriving instance Eq (TracePrefixTree f a)