git.iko.soy/typeable/compaREST
on master help sign in
Formulas (#19)
84e87f6mniip
openapi-diff.cabal+1
compare with master
unifiedsplit
@@ -86,6 +86,7 @@ library
86 import: common-options
86 import: common-options
87 hs-source-dirs: src
87 hs-source-dirs: src
88 exposed-modules: OpenAPI.Checker.Aux
88 exposed-modules: OpenAPI.Checker.Aux
89+ , OpenAPI.Checker.Formula
89 , OpenAPI.Checker.Memo
90 , OpenAPI.Checker.Memo
90 , OpenAPI.Checker.Report
91 , OpenAPI.Checker.Report
91 , OpenAPI.Checker.Run
92 , OpenAPI.Checker.Run
src/OpenAPI/Checker/Formula.hsnew file+75
@@ -0,0 +1,75 @@
1+module OpenAPI.Checker.Formula
2+ ( FormulaF
3+ , VarRef
4+ , anyOf
5+ , anError
6+ , calculate
7+ ) where
8+
9+import Data.Kind
10+import Data.Monoid
11+import qualified Data.List.NonEmpty as NE
12+import OpenAPI.Checker.Trace
13+import qualified OpenAPI.Checker.TracePrefixTree as T
14+
15+type VarRef = Int
16+
17+-- | The type @FormulaF f r ()@ describes (modulo contents of errors) boolean
18+-- formulas involving variables, conjunctions, and disjunctions. These
19+-- operations (and the generated algebra) are monotonous. This ensures that
20+-- there always exist fixpoints, i.e. that @x = f x@ has at least one solution.
21+data FormulaF (f :: k -> Type) (r :: k) (a :: Type) where
22+ Result :: a -> FormulaF f r a
23+ Errors :: !(T.TracePrefixTree f r) -> FormulaF f r a
24+ -- ^ invariant: never empty
25+ Apply :: FormulaF f r (b -> c) -> FormulaF f r b -> (c -> a) -> FormulaF f r a
26+ -- ^ invariant: LHS and RHS are never 'Result' nor 'Errors'
27+ SelectFirst :: NE.NonEmpty (FormulaF f r b)
28+ -> !(AnItem f r) -> (b -> a) -> FormulaF f r a
29+ -- ^ invariant: the list doesn't contain any 'Result's or 'Errors'.
30+ Variable :: !VarRef -> FormulaF f r a
31+
32+anError :: AnItem f r -> FormulaF f r a
33+anError e = Errors $ T.singleton e
34+
35+instance Functor (FormulaF f r) where
36+ fmap f (Result x) = Result (f x)
37+ fmap _ (Errors e) = Errors e
38+ fmap f (Apply g x h) = Apply g x (f . h)
39+ fmap f (SelectFirst xs e h) = SelectFirst xs e (f . h)
40+ fmap _ (Variable r) = Variable r
41+
42+instance Applicative (FormulaF f r) where
43+ pure = Result
44+ Result f <*> x = f <$> x
45+ Errors e <*> Result _ = Errors e
46+ Errors e1 <*> Errors e2 = Errors (e1 <> e2)
47+ f <*> x = Apply f x id
48+
49+anyOf :: [FormulaF f r a] -> AnItem f r -> FormulaF f r a
50+anyOf fs allE = case foldMap check fs of
51+ (First (Just x), _) -> Result x
52+ (First Nothing, (x:xs)) -> SelectFirst (x NE.:| xs) allE id
53+ (First Nothing, []) -> Errors $ T.singleton allE
54+ where
55+ check (Result x) = (First (Just x), mempty)
56+ check (Errors _) = (mempty, mempty)
57+ check (SelectFirst xs _ h) = (mempty, NE.toList (fmap (fmap h) xs))
58+ check x = (mempty, [x])
59+
60+calculate :: FormulaF f r a -> Either (T.TracePrefixTree f r) a
61+calculate (Result x) = Right x
62+calculate (Errors e) = Left e
63+calculate (Apply f x h) = case calculate f of
64+ Left e1 -> case calculate x of
65+ Left e2 -> Left (e1 <> e2)
66+ Right _ -> Left e1
67+ Right f' -> case calculate x of
68+ Left e2 -> Left e2
69+ Right x' -> Right (h (f' x'))
70+calculate (SelectFirst xs e h) = go (calculate <$> NE.toList xs)
71+ where
72+ go (Left _ : rs) = go rs
73+ go (Right x : _) = Right (h x)
74+ go [] = Left $ T.singleton e
75+calculate (Variable i) = error $ "Unknown variable " <> show i
src/OpenAPI/Checker/Memo.hs+89−34
@@ -1,70 +1,125 @@
1{-# LANGUAGE AllowAmbiguousTypes #-}
1{-# LANGUAGE AllowAmbiguousTypes #-}
2-- | Utilities for effectfully memoizing other, more effectful functions.
2-- | Utilities for effectfully memoizing other, more effectful functions.
3module OpenAPI.Checker.Memo
3module OpenAPI.Checker.Memo
4− ( Progress(..)
5− , MonadMemo
4+ ( MonadMemo
6 , MemoState
5 , MemoState
7 , runMemo
6 , runMemo
8− , tryMemo
7+ , modifyMemoNonce
9− , tryMemoWithTag
8+ , KnotTier(..)
9+ , unknot
10+ , memoWithKnot
11+ , memoTaggedWithKnot
10 ) where
12 ) where
11
13
12import Control.Monad.State
14import Control.Monad.State
15+import Data.Dynamic
13import qualified Data.Map as M
16import qualified Data.Map as M
14import Data.Tagged
17import Data.Tagged
18+import Data.Void
15import qualified Data.TypeRepMap as T
19import qualified Data.TypeRepMap as T
16import Type.Reflection
20import Type.Reflection
17
21
18−-- | A computation has either 'Finished', or it is 'InProgress'.
19−data Progress a = Finished a | InProgress
22+data Progress a = Finished a | Started | TyingKnot Dynamic
20− deriving (Eq, Ord, Show)
21
23
22data MemoMap a where
24data MemoMap a where
23 MemoMap :: !(M.Map k (Progress v)) -> MemoMap (k, v)
25 MemoMap :: !(M.Map k (Progress v)) -> MemoMap (k, v)
24
26
25−newtype MemoState = MemoState (T.TypeRepMap MemoMap)
27+data MemoState s = MemoState s (T.TypeRepMap MemoMap)
26
28
27-- | An effectful memoization monad.
29-- | An effectful memoization monad.
28−type MonadMemo m = MonadState MemoState m
30+type MonadMemo s m = MonadState (MemoState s) m
29
31
30memoStateLookup
32memoStateLookup
31− :: forall k v. (Typeable k, Typeable v, Ord k)
33+ :: forall k v s. (Typeable k, Typeable v, Ord k)
32− => k -> MemoState -> Maybe (Progress v)
34+ => k -> MemoState s -> Maybe (Progress v)
33−memoStateLookup k (MemoState t) = case T.lookup @(k, v) t of
35+memoStateLookup k (MemoState _ t) = case T.lookup @(k, v) t of
34 Just (MemoMap m) -> M.lookup k m
36 Just (MemoMap m) -> M.lookup k m
35 Nothing -> Nothing
37 Nothing -> Nothing
36
38
37memoStateInsert
39memoStateInsert
38− :: forall k v. (Typeable k, Typeable v, Ord k)
40+ :: forall k v s. (Typeable k, Typeable v, Ord k)
39− => k -> Progress v -> MemoState -> MemoState
41+ => k -> Progress v -> MemoState s -> MemoState s
40−memoStateInsert k x (MemoState t) = MemoState $ T.insert (MemoMap m'') t
42+memoStateInsert k x (MemoState s t) = MemoState s $ T.insert (MemoMap m'') t
41 where
43 where
42 m'' = M.insert k x m'
44 m'' = M.insert k x m'
43 m' = case T.lookup @(k, v) t of
45 m' = case T.lookup @(k, v) t of
44 Just (MemoMap m) -> m
46 Just (MemoMap m) -> m
45 Nothing -> M.empty
47 Nothing -> M.empty
46
48
49+modifyMemoNonce :: MonadMemo s m => (s -> s) -> m s
50+modifyMemoNonce f = do
51+ MemoState s t <- get
52+ put $ MemoState (f s) t
53+ pure s
54+
47-- | Run a memoized computation.
55-- | Run a memoized computation.
48−runMemo :: Monad m => StateT MemoState m a -> m a
56+runMemo :: Monad m => s -> StateT (MemoState s) m a -> m a
49−runMemo = (`evalStateT` MemoState T.empty)
57+runMemo s = (`evalStateT` MemoState s T.empty)
58+
59+-- | A description of how to effectfully tie knots in type @v@, using the @m@
60+-- monad, and by sharing some @d@ data among the recursive instances.
61+data KnotTier v d m = KnotTier
62+ { onKnotFound :: m d -- ^ Create some data that will be connected to this knot
63+ , onKnotUsed :: d -> m v -- ^ This is what the knot will look like as a value
64+ -- to the inner computations
65+ , tieKnot :: d -> v -> m v -- ^ Once we're done and we're outside, tie the
66+ -- knot using the datum
67+ }
68+
69+unknot :: KnotTier v Void m
70+unknot = KnotTier
71+ { onKnotFound = error "Recursion detected"
72+ , onKnotUsed = absurd
73+ , tieKnot = absurd
74+ }
50
75
51−-- | Try to call a function whilst memoizing its result. If we are already
76+-- | Run a potentially recursive computation. The provided key will be used to
52−-- inside an evaluation of some function with these arguments, this returns
77+-- refer to the result of this computation. If during the computation, another
53−-- @InProgress@. Beware of different functions that have the same type.
78+-- attempt to run the computation with the same key is made, we run a
54−tryMemo
79+-- tying-the-knot procedure.
80+--
81+-- If another attempt to run the computation with the same key is made
82+-- *after we're done*, we will return the memoized value.
83+memoWithKnot
84+ :: forall k v d m s.
55− :: forall k v m. (Typeable k, Typeable v, Ord k, MonadMemo m)
85+ (Typeable k, Typeable v, Typeable d, Ord k, MonadMemo s m)
56− => (k -> m v) -> k -> m (Progress v)
86+ => KnotTier v d m
87+ -> m v -- ^ the computation to memoize
88+ -> k -- ^ key for memoization
89+ -> m v
57−tryMemo f k = memoStateLookup k <$> get >>= \case
90+memoWithKnot tier f k = memoStateLookup @k @v k <$> get >>= \case
58− Just x -> pure x
91+ Just (Finished v) -> pure v
92+ Just Started -> do
93+ d <- onKnotFound tier
94+ modify $ memoStateInsert @k @v k (TyingKnot $ toDyn d)
95+ onKnotUsed tier d
96+ Just (TyingKnot dyn) -> case fromDynamic dyn of
97+ Just d -> onKnotUsed tier d
98+ Nothing -> error $ "Type mismatch when examining the knot of "
99+ <> show (typeRep @(k -> v)) <> ": expected " <> show (typeRep @d)
100+ <> ", got " <> show (dynTypeRep dyn)
59 Nothing -> do
101 Nothing -> do
60− modify $ memoStateInsert k (InProgress @v)
102+ modify $ memoStateInsert @k @v k Started
61− result <- Finished <$> f k
103+ v <- f
104+ v' <- memoStateLookup @k @v k <$> get >>= \case
105+ Just Started -> pure v
106+ Just (TyingKnot dyn) -> case fromDynamic dyn of
107+ Just d -> tieKnot tier d v
108+ Nothing -> error $ "Type mismatch when tying the knot of "
109+ <> show (typeRep @(k -> v)) <> ": expected " <> show (typeRep @d)
110+ <> ", got " <> show (dynTypeRep dyn)
111+ Just (Finished _) -> error $ "Unexpected Finished when memoizing "
112+ <> show (typeRep @(k -> v))
113+ Nothing -> error $ "No key found when memoizing "
114+ <> show (typeRep @(k -> v))
62− modify $ memoStateInsert k result
115+ modify $ memoStateInsert @k @v k (Finished v')
63− pure result
116+ pure v'
64
117
65-- | Disambiguate memoized computations with an arbitrary tag.
118-- | Disambiguate memoized computations with an arbitrary tag.
66−tryMemoWithTag
119+memoTaggedWithKnot
120+ :: forall t k v d m s.
67− :: forall t k v m. (Typeable t, Typeable k, Typeable v, Ord k, MonadMemo m)
121+ ( Typeable t, Typeable k, Typeable v, Typeable d
68− => (k -> m v) -> k -> m (Progress v)
122+ , Ord k, MonadMemo s m )
123+ => KnotTier v d m -> m v -> k -> m v
69−tryMemoWithTag f k = withTypeable (typeRepKind $ typeRep @t) $
124+memoTaggedWithKnot tier f k = withTypeable (typeRepKind $ typeRep @t) $
70− tryMemo (f . unTagged) (Tagged @t k)
125+ memoWithKnot tier f (Tagged @t k)
src/OpenAPI/Checker/Subtree.hs+44−51
@@ -2,27 +2,24 @@ module OpenAPI.Checker.Subtree
2 ( APIStep(..)
2 ( APIStep(..)
3 , Subtree(..)
3 , Subtree(..)
4 , CompatM(..)
4 , CompatM(..)
5− , runCompatM
5+ , CompatFormula
6+ , runCompatFormula
7+ , localM
6 , local'
8 , local'
7− , warnIssue
9+ , issueAtTrace
8− , throwIssue
10+ , issueAt
9− , warnIssueAt
11+ , memo
10− , throwIssueAt
11− , throwWarnings
12− , warnIssues
13 ) where
12 ) where
14
13
15−import Control.Monad.Error.Class
16import Control.Monad.Identity
14import Control.Monad.Identity
17−import Control.Monad.Reader.Class
15+import Control.Monad.Reader
18−import Control.Monad.Trans.Except (ExceptT, runExceptT)
19−import Control.Monad.Trans.Reader (ReaderT(..))
16+import Control.Monad.State
20−import Control.Monad.Trans.State (StateT)
17+import Data.Functor.Compose
21−import Control.Monad.Trans.Writer.Strict (WriterT, runWriterT)
22−import Control.Monad.Writer.Class
23import Data.Kind
18import Data.Kind
24import Data.OpenApi
19import Data.OpenApi
25import Data.Text
20import Data.Text
21+import Data.Typeable
22+import OpenAPI.Checker.Formula
26import OpenAPI.Checker.Memo
23import OpenAPI.Checker.Memo
27import OpenAPI.Checker.Trace
24import OpenAPI.Checker.Trace
28import qualified OpenAPI.Checker.TracePrefixTree as T
25import qualified OpenAPI.Checker.TracePrefixTree as T
@@ -48,64 +45,60 @@ data TracedEnv t = TracedEnv
48newtype CompatM t a = CompatM
45newtype CompatM t a = CompatM
49 { unCompatM ::
46 { unCompatM ::
50 ReaderT (ProdCons (TracedEnv t))
47 ReaderT (ProdCons (TracedEnv t))
51− (ExceptT (T.TracePrefixTree CheckIssue OpenApi)
52− (WriterT (T.TracePrefixTree CheckIssue OpenApi)
53− (StateT MemoState Identity))) a
48+ (StateT (MemoState VarRef) Identity) a
54 } deriving newtype
49 } deriving newtype
55 ( Functor, Applicative, Monad
50 ( Functor, Applicative, Monad
56 , MonadReader (ProdCons (TracedEnv t))
51 , MonadReader (ProdCons (TracedEnv t))
57− , MonadError (T.TracePrefixTree CheckIssue OpenApi)
52+ , MonadState (MemoState VarRef)
58− , MonadWriter (T.TracePrefixTree CheckIssue OpenApi)
59 )
53 )
60
54
55+type CompatFormula t = Compose (CompatM t) (FormulaF CheckIssue OpenApi)
56+
61−class (Ord t, Ord (CheckIssue t)) => Subtree (t :: Type) where
57+class (Typeable t, Ord t, Ord (CheckIssue t)) => Subtree (t :: Type) where
62 type family CheckEnv t :: Type
58 type family CheckEnv t :: Type
63 data family CheckIssue t :: Type
59 data family CheckIssue t :: Type
60+ -- | If we ever followed a reference, reroute the path through "components"
61+ normalizeTrace :: Trace OpenApi t -> Trace OpenApi t
64− checkCompatibility :: ProdCons t -> CompatM t a
62+ checkCompatibility :: ProdCons t -> CompatFormula t ()
65
63
64+runCompatFormula
66−runCompatM :: ProdCons (TracedEnv t) -> CompatM t a ->
65+ :: ProdCons (TracedEnv t)
66+ -> Compose (CompatM t) (FormulaF f r) a
67− ( Either (T.TracePrefixTree CheckIssue OpenApi) a -- unrecovarable errors
67+ -> Either (T.TracePrefixTree f r) a
68− , T.TracePrefixTree CheckIssue OpenApi ) -- warnings
68+runCompatFormula env (Compose f)
69−runCompatM env = runIdentity . runMemo . runWriterT
70− . runExceptT . (`runReaderT` env) . unCompatM
69+ = calculate . runIdentity . runMemo 0 . (`runReaderT` env) . unCompatM $ f
71
70
72−local'
71+localM
73 :: ProdCons (Trace a b)
72 :: ProdCons (Trace a b)
74 -> (ProdCons (CheckEnv a) -> ProdCons (CheckEnv b))
73 -> (ProdCons (CheckEnv a) -> ProdCons (CheckEnv b))
75 -> CompatM b x
74 -> CompatM b x
76 -> CompatM a x
75 -> CompatM a x
77−local' xs wrapEnv (CompatM k) = CompatM $ ReaderT $ \env ->
76+localM xs wrapEnv (CompatM k) = CompatM $ ReaderT $ \env ->
78 runReaderT k $ TracedEnv
77 runReaderT k $ TracedEnv
79 <$> (catTrace <$> (getTrace <$> env) <*> xs)
78 <$> (catTrace <$> (getTrace <$> env) <*> xs)
80 <*> wrapEnv (getEnv <$> env)
79 <*> wrapEnv (getEnv <$> env)
81
80
82−warnIssue :: Subtree t => Trace OpenApi t -> CheckIssue t -> CompatM t ()
81+local'
83−warnIssue xs issue = tell $ T.singleton $ AnItem xs issue
82+ :: ProdCons (Trace a b)
83+ -> (ProdCons (CheckEnv a) -> ProdCons (CheckEnv b))
84+ -> Compose (CompatM b) (FormulaF f r) x
85+ -> Compose (CompatM a) (FormulaF f r) x
86+local' xs wrapEnv (Compose h) = Compose (localM xs wrapEnv h)
84
87
88+issueAtTrace
85−throwIssue :: Subtree t => Trace OpenApi t -> CheckIssue t -> CompatM t a
89+ :: Subtree t => Trace OpenApi t -> CheckIssue t -> CompatFormula t a
86−throwIssue xs issue = throwError $ T.singleton $ AnItem xs issue
90+issueAtTrace xs issue = Compose $ pure $ anError $ AnItem xs issue
87
91
88−warnIssueAt
92+issueAt
89 :: Subtree t
93 :: Subtree t
90 => (forall x. ProdCons x -> x)
94 => (forall x. ProdCons x -> x)
91 -> CheckIssue t
95 -> CheckIssue t
92− -> CompatM t ()
96+ -> CompatFormula t a
93−warnIssueAt f issue = do
97+issueAt f issue = Compose $ do
94 xs <- asks $ getTrace . f
98 xs <- asks $ getTrace . f
95− warnIssue xs issue
99+ pure $ anError $ AnItem xs issue
96−
97−throwIssueAt
98− :: Subtree t
99− => (forall x. ProdCons x -> x)
100− -> CheckIssue t
101− -> CompatM t a
102−throwIssueAt f issue = do
103− xs <- asks $ getTrace . f
104− throwIssue xs issue
105−
106−throwWarnings :: CompatM t a -> CompatM t a
107−throwWarnings k = listen k >>= \case
108− (x, issues) -> if T.null issues then pure x else throwError issues
109
100
110−warnIssues :: CompatM t a -> CompatM t (Maybe a)
101+memo :: (Subtree t, Typeable a) => CompatFormula t a -> CompatFormula t a
111−warnIssues k = catchError (Just <$> k) (\issues -> Nothing <$ tell issues)
102+memo (Compose f) = Compose $ do
103+ pxs <- asks (normalizeTrace . getTrace <$>)
104+ memoWithKnot unknot f pxs
src/OpenAPI/Checker/TracePrefixTree.hs+3−3
@@ -24,9 +24,9 @@ import Data.Type.Equality
24
24
25-- | A list of @AnItem r f@, but optimized into a prefix tree.
25-- | A list of @AnItem r f@, but optimized into a prefix tree.
26data TracePrefixTree (f :: k -> Type) (r :: k) = TracePrefixTree
26data TracePrefixTree (f :: k -> Type) (r :: k) = TracePrefixTree
27− { rootItems :: !(ASet (f r))
27+ { rootItems :: !(ASet (f r))
28− , snocItems :: !(T.TypeRepMap (AStep f r))
28+ , snocItems :: !(T.TypeRepMap (AStep f r))
29− }
29+ }
30
30
31deriving instance Eq (TracePrefixTree f a)
31deriving instance Eq (TracePrefixTree f a)
32
32