Skip to content

Commit

Permalink
fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
MaximilianAlgehed committed May 3, 2024
1 parent 33f0085 commit 9d6b0a5
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 8 deletions.
11 changes: 8 additions & 3 deletions libs/constrained-generators/src/Constrained/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1097,7 +1097,7 @@ simplifySpec spec = case spec of
let optP = optimisePred p
in fromGESpec
$ explain
[ show $ "Simplifying" /> pretty spec
[ show $ "Simplifying: " /> pretty spec
, show $ "optimisePred =>" /> pretty optP
]
$ computeSpecSimplified x optP
Expand All @@ -1109,7 +1109,7 @@ simplifySpec spec = case spec of
-- | Precondition: the `Pred fn` defines the `Var a`
computeSpecSimplified ::
forall fn a. (HasSpec fn a, HasCallStack) => Var a -> Pred fn -> GE (Specification fn a)
computeSpecSimplified x p = case p of
computeSpecSimplified x p = localGESpec $ case p of
Monitor {} -> pure mempty
GenHint h t -> propagateSpec (giveHint h) <$> toCtx x t -- NOTE: this implies you do need to actually propagate hints, e.g. propagate depth control in a `tail` or `cdr` like function
Subst x' t p' -> computeSpec x (substitutePred x' t p') -- NOTE: this is impossible as it should have gone away already
Expand All @@ -1136,7 +1136,8 @@ computeSpecSimplified x p = case p of
fatalError ["Dependency error in computeSpec: IfElse", " " ++ show x, show $ indent 2 (pretty p)]
Reifies (Lit a) (Lit val) f
| f val == a -> pure TrueSpec
| otherwise -> genError ["Value does not reify to literal: " ++ show val ++ " -/> " ++ show a]
| otherwise ->
pure $ ErrorSpec ["Value does not reify to literal: " ++ show val ++ " -/> " ++ show a]
Reifies t' (Lit val) f ->
propagateSpec (equalSpec (f val)) <$> toCtx x t'
Reifies Lit {} _ _ ->
Expand All @@ -1148,6 +1149,10 @@ computeSpecSimplified x p = case p of
Reifies {} ->
fatalError
["The impossible happened in computeSpec: Reifies", " " ++ show x, show $ indent 2 (pretty p)]
where
-- We want `genError` to turn into `ErrorSpec` and we want `FatalError` to turn into `FatalError`
localGESpec ge@FatalError {} = ge
localGESpec ge = pure $ fromGESpec ge

-- | Precondition: the `Pred fn` defines the `Var a`
computeSpec ::
Expand Down
5 changes: 0 additions & 5 deletions libs/constrained-generators/test/Constrained/Test.hs
Original file line number Diff line number Diff line change
Expand Up @@ -148,11 +148,6 @@ negativeTests =
prop_complete @BaseFn @Int $
constrained $ \x ->
reify x id $ \y -> y ==. 10
prop "reify overconstrained" $
expectFailure $
prop_complete @BaseFn @Int $
constrained $ \x ->
reify x id $ \y -> y ==. 10

numberyTests :: Spec
numberyTests =
Expand Down

0 comments on commit 9d6b0a5

Please sign in to comment.