simplify

Author: MaximilianAlgehed

src/Constrained/Generation.hs

@@ -836,17 +836,7 @@ mergeSolverStage (SolverStage x ps spec relevant) plan =
         normalizeSolverStage $ SolverStage
             y
             (ps ++ ps')
-            ( addToErrorSpec
-                ( NE.fromList
-                    ( [ "Solving var " ++ show x ++ " fails."
-                      , "Merging the Specs"
-                      , "   1. " ++ show spec
-                      , "   2. " ++ show spec'
-                      ]
-                    )
-                )
-                (spec <> spec')
-            )
+            (spec <> spec')
             (relevant <> relevant')
       Nothing -> stage
   | stage@(SolverStage y ps' spec' relevant') <- plan
@@ -900,27 +890,21 @@ backPropagation relevant (SolverPlan initplan) = SolverPlan (go [] (reverse init
     go acc [] = acc
     go acc (s@(SolverStage (x :: Var a) ps spec _) : plan) = go (s : acc) plan'
       where
-        newStages = concatMap (newStage spec) ps
+        newStages = concatMap newStage ps
         plan' = foldr mergeSolverStage plan newStages
+
         -- Note use of the Term Pattern Equal
-        newStage specl (Assert (Equal (V x') t)) =
-          termVarEqCases specl x' t
-        newStage specr (Assert (Equal t (V x'))) =
-          termVarEqCases specr x' t
-        newStage _ _ = []
-
-        termVarEqCases :: HasSpec b => Specification a -> Var b -> Term b -> [SolverStage]
-        termVarEqCases specx x' t
-          | Set.singleton (Name x) == freeVarSet t
-          , Result ctx <- toCtx x t =
-            [SolverStage x' [] (forwardPropagateSpec specx ctx) (Set.insert (Name x) relevant)]
-        termVarEqCases specx x' t
-          | Just Refl <- eqVar x x'
-          , [Name y] <- Set.toList $ freeVarSet t
-          , Result ctx <- toCtx y t =
-              [SolverStage y [] (propagateSpec specx ctx)
-               (Set.insert (Name x') relevant)]
-        termVarEqCases _ _ _ = []
+        newStage (Assert (Equal tl tr))
+          | [Name xl] <- Set.toList $ freeVarSet tl
+          , [Name xr] <- Set.toList $ freeVarSet tr
+          , Name x `elem` [Name xl, Name xr]
+          , Result ctxL <- toCtx xl tl
+          , Result ctxR <- toCtx xr tr
+          = case (eqVar x xl, eqVar x xr) of
+              (Just Refl, _) -> [SolverStage xr [] (propagateSpec (forwardPropagateSpec spec ctxL) ctxR) (Set.insert (Name x) relevant)]
+              (_, Just Refl) -> [SolverStage xl [] (propagateSpec (forwardPropagateSpec spec ctxR) ctxL) (Set.insert (Name x) relevant)]
+              _ -> error "The impossible happened"
+        newStage _ = []
 
 -- | Function symbols for `(==.)`
 data EqW :: [Type] -> Type -> Type where