danr / emna Goto Github PK

There seems to be an issue when translating functions which uses data structures containing abstract sorts.

Input: https://gist.github.com/chip2n/05b3f584c73b3a25bcd0
Output:

emna: src/Tip/QuickSpec/Translate.hs, line 124: tree: cannot match types
[]
(=> (Tree Dummy) (Tree Dummy) Bool)
(=> (Tree Int) (Tree Int) Bool)

We'd love to fix it (and the other issues as well), but I can't guarantee we have time to do so before our thesis is due (April 13).

emna doesn't build with the latest version of https://github.com/tip-org/tools/
More specifically, Waldmeister.hs causes problems.
This is because of the new real number support

For isaplanner/prop_06.smt2 (and others): the property cannot be proven, but summary of proof is still printed, and exit code is 0.

Some debugging info:
loop returns Right when it shouldn't, from line 135.
The reason for this is that there is no UserAsserted property left in the list. All the remaining properties have fm_info = Unknown (which I think means "conjectured by QuickSpec").
This means that the original UserAsserted property disappears along the way somehow.

OSX 10.10.5
Z3 version 4.4.0

When I invoke for example

dist/build/emna/emna --prover=z examples/Reverse.hs

emna proves the property properly and exits, but z3 continues running in the background eating up CPU until killed.

Running emna on the following Haskell code:

data List a = Empty | Cons a (List a)

listMap :: (a -> b) -> List a -> List b
listMap f Empty       = Empty
listMap f (Cons a as) = Cons (f a) (listMap f as)

prop :: List a -> Equality (List a)
prop a = listMap id a === a

causes the following error:

emna: src/QuickSpec/Pruning.hs, line 100: No instances in
  [a, List a]
for
  listMap x Empty = Empty :: List a
under
  [x :: c -> a, Empty :: List a, Empty :: List c,
   listMap x Empty :: List a]

However, running it manually on the generated TIP code (from tip-ghc) works fine:

(declare-datatypes (a)
  ((List2 (Empty) (Cons (Cons_0 a) (Cons_1 (List2 a))))))
(define-fun-rec
  (par (a b)
    (listMap
       ((x (=> a b)) (y (List2 a))) (List2 b)
       (match y
         (case Empty (as Empty (List2 b)))
         (case (Cons a2 bs) (Cons (@ x a2) (listMap x bs)))))))
(assert-not
  (par (a)
    (forall ((b (List2 a))) (= (listMap (lambda ((x a)) x) b) b))))
(check-sat)