nick8325 / equinox

Paradox model finder and equinox theorem prover for first-order logic.
MIT License
19 stars 4 forks source link

Error build `FolSat.hs` #16

Closed Average-user closed 4 years ago

Average-user commented 4 years ago
[17 of 18] Compiling Equinox.FolSat   ( Equinox/FolSat.hs, Equinox/FolSat.o )

Equinox/FolSat.hs:317:22: error:
    • Could not deduce (Control.Monad.Fail.MonadFail Sat.S)
        arising from a do statement
        with the failable pattern ‘Left subs’
      from the context: (Ord a, Num a, Show a)
        bound by the inferred type of
                   findAllSubs :: (Ord a, Num a, Show a) =>
                                  a -> Sat.S (Either [Map Symbol Con] (Bool, Set Symbol))
        at Equinox/FolSat.hs:(305,12)-(327,42)
    • In a stmt of a 'do' block: Left subs <- findAllSubs (i + 1)
      In the expression:
        do Sat.lift (showOne send (i + 1))
           cs <- sequence [getModelValueValue v | v <- vs]
           let sub = M.fromList (xs `zip` cs)
           Sat.addClause [Sat.neg (v =? c) | (v, c) <- vs `zip` cs, c /= st]
           ....
      In a stmt of a 'do' block:
        if b then
            do Sat.lift (showOne send (i + 1))
               cs <- sequence [getModelValueValue v | v <- vs]
               let sub = ...
               ....
        else
            do if i == 0 then do ... else do ...
    |
317 |                      Left subs <- findAllSubs (i+1)
    |                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
make[1]: *** [Makefile:42: ../equinox] Error 1

Not sure what to do

nick8325 commented 4 years ago

Should be fixed now!