search

Twigonometry / IsabelleDSL

IsabelleDSL (iDSL) is a framework for generating Domain-Specific Languages from specifications written in Isabelle
0 stars 0 forks source link

Calculator Haskell file produces incorrect results #4

Closed Twigonometry closed 2 years ago

Twigonometry commented 2 years ago 
*Calculator> eval (St (Int_of_integer 0)) (Add (Int_of_integer 5) (Sub (Int_of_integer 4) (Div (Int_of_integer 4) (GetResult))))
St (Int_of_integer (-4))
*Calculator> eval (St (Int_of_integer 0)) (Add (Int_of_integer 5) (Sub (Int_of_integer 4) (GetResult)))
St (Int_of_integer (-1))

However, equivalent Isabelle statements are correct. Exported Python is also correct:

=== Results of Exported File ===

0
0.25
Twigonometry commented 2 years ago

Note: this is separate to the issue with current calculator model not being able to process float values.

Twigonometry commented 2 years ago

Issue mentioned above is #19

Twigonometry commented 2 years ago

This seems to have fixed itself - strange behaviour I couldn't reproduce after working on other things for a while, perhaps it was an artifact of some caching on Isabelle's part? Either way, closed by f15a3c1c