@@ -1,9 +1,11 @@
11module OpenAPI.Checker.Formula
22 ( FormulaF
33 , VarRef
4− , anyOf
4+ , variable
5+ , eitherOf
56 , anError
67 , calculate
8+ , maxFixpoint
79 ) where
810
911import Data.Kind
@@ -17,45 +19,63 @@ type VarRef = Int
1719-- | The type @FormulaF f r ()@ describes (modulo contents of errors) boolean
1820-- formulas involving variables, conjunctions, and disjunctions. These
1921-- 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.
22+-- fixpoints always exist, i.e. that @x = f x@ has at least one solution.
2123data FormulaF (f :: k -> Type) (r :: k) (a :: Type) where
2224 Result :: a -> FormulaF f r a
2325 Errors :: !(T.TracePrefixTree f r) -> FormulaF f r a
2426 -- ^ invariant: never empty
2527 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+ -- ^ invariant: at least one of LHS and RHS is not 'Errors', and they are
29+ -- both not 'Result'
30+ SelectFirst :: NE.NonEmpty (SomeFormulaF b)
2831 -> !(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
32+ -- ^ invariant: the list doesn't contain any 'Result's, 'Errors' or
33+ -- 'SelectFirst'
34+ Variable :: !VarRef -> a -> FormulaF f r a
35+
36+mkApply :: FormulaF f r (b -> c) -> FormulaF f r b -> (c -> a) -> FormulaF f r a
37+mkApply (Result f) x h = h . f <$> x
38+mkApply f (Result x) h = h . ($ x) <$> f
39+mkApply (Errors e1) (Errors e2) _ = Errors (e1 <> e2)
40+mkApply f x h = Apply f x h
41+
42+mkSelectFirst :: [SomeFormulaF b] -> AnItem f r -> (b -> a) -> FormulaF f r a
43+mkSelectFirst fs allE h = case foldMap check fs of
44+ (First (Just x), _) -> Result (h x)
45+ (First Nothing, (x:xs)) -> SelectFirst (x NE.:| xs) allE h
46+ (First Nothing, []) -> Errors $ T.singleton allE
47+ where
48+ check (SomeFormulaF (Result x)) = (First (Just x), mempty)
49+ check (SomeFormulaF (Errors _)) = (mempty, mempty)
50+ check (SomeFormulaF (SelectFirst xs _ h'))
51+ = (mempty, NE.toList (fmap (fmap h') xs))
52+ check x = (mempty, [x])
53+
54+data SomeFormulaF (a :: Type) where
55+ SomeFormulaF :: FormulaF f r a -> SomeFormulaF a
3156
3257anError :: AnItem f r -> FormulaF f r a
3358anError e = Errors $ T.singleton e
3459
60+variable :: VarRef -> FormulaF f r ()
61+variable v = Variable v ()
62+
3563instance Functor (FormulaF f r) where
3664 fmap f (Result x) = Result (f x)
3765 fmap _ (Errors e) = Errors e
3866 fmap f (Apply g x h) = Apply g x (f . h)
3967 fmap f (SelectFirst xs e h) = SelectFirst xs e (f . h)
40− fmap _ (Variable r) = Variable r
68+ fmap f (Variable r x) = Variable r (f x)
69+
70+instance Functor SomeFormulaF where
71+ fmap f (SomeFormulaF x) = SomeFormulaF (fmap f x)
4172
4273instance Applicative (FormulaF f r) where
4374 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
75+ f <*> x = mkApply f x id
4876
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])
77+eitherOf :: [FormulaF f' r' a] -> AnItem f r -> FormulaF f r a
78+eitherOf fs allE = mkSelectFirst (map SomeFormulaF fs) allE id
5979
6080calculate :: FormulaF f r a -> Either (T.TracePrefixTree f r) a
6181calculate (Result x) = Right x
@@ -67,9 +87,25 @@ calculate (Apply f x h) = case calculate f of
6787 Right f' -> case calculate x of
6888 Left e2 -> Left e2
6989 Right x' -> Right (h (f' x'))
70−calculate (SelectFirst xs e h) = go (calculate <$> NE.toList xs)
90+calculate (SelectFirst xs e h) = go (NE.toList xs)
7191 where
72− go (Left _ : rs) = go rs
73− go (Right x : _) = Right (h x)
92+ go (SomeFormulaF r:rs) = case calculate r of
93+ Left _ -> go rs
94+ Right x -> Right (h x)
7495 go [] = Left $ T.singleton e
75−calculate (Variable i) = error $ "Unknown variable " <> show i
96+calculate (Variable i _) = error $ "Unknown variable " <> show i
97+
98+-- Approximate for now. Answers yes/no correctly, but the error lists aren't
99+-- super accurate. TODO: improve
100+maxFixpoint :: VarRef -> FormulaF f r () -> FormulaF f r ()
101+maxFixpoint i = go
102+ where
103+ go :: FormulaF f r a -> FormulaF f r a
104+ go (Result x) = Result x
105+ go (Errors e) = Errors e
106+ go (Apply f x h) = mkApply (go f) (go x) h
107+ go (SelectFirst fs e h) = mkSelectFirst (NE.toList (fmap goSF fs)) e h
108+ go (Variable j x) | i == j = Result x
109+ go v@(Variable _ _) = v
110+ goSF :: SomeFormulaF a -> SomeFormulaF a
111+ goSF (SomeFormulaF x) = SomeFormulaF (go x)