module Camfort.Specification.Units.InferenceBackendSpec (spec) where import GHC.Real ((%)) import Test.Hspec hiding (Spec) import qualified Test.Hspec as Test import Camfort.Specification.Units.Environment import Camfort.Specification.Units.InferenceBackendSBV ( criticalVariables, inconsistentConstraints, inferVariables ) import Camfort.Specification.Units.InferenceBackend ( flattenConstraints, shiftTerms ) import Camfort.Specification.Units.BackendTypes (constraintToDim, dimParamEq, Dim, dimFromList, prop_composition) import Data.Maybe (fromJust) import Test.QuickCheck spec :: Test.Spec spec = do describe "Backend Types" $ it "Substitution composition" $ property $ prop_composition describe "Flatten constraints" $ it "testCons1" $ flattenConstraints testCons1 `shouldBe` testCons1_flattened describe "Shift terms" $ do it "testCons1" $ map shiftTerms (flattenConstraints testCons1) `shouldBe` testCons1_shifted it "testCons2" $ map shiftTerms (flattenConstraints testCons2) `shouldBe` testCons2_shifted it "testCons3" $ map shiftTerms (flattenConstraints testCons3) `shouldBe` testCons3_shifted describe "Consistency" $ do it "testCons1" $ (constraintToDim . head . fromJust $ inconsistentConstraints testCons1) `shouldSatisfy` dimParamEq (dimFromList [(UnitName "kg", -1), (UnitName "m", 1)]) it "testCons2" $ inconsistentConstraints testCons2 `shouldBe` Nothing it "testCons3" $ inconsistentConstraints testCons3 `shouldBe` Nothing describe "Critical Variables" $ do it "testCons2" $ criticalVariables testCons2 `shouldSatisfy` null it "testCons3" $ criticalVariables testCons3 `shouldBe` [UnitVar ("c", "c"), UnitVar ("e", "e")] it "testCons4" $ criticalVariables testCons4 `shouldBe` [UnitVar ("simple2_a22", "simple2_a22")] it "testCons5" $ criticalVariables testCons5 `shouldSatisfy` null describe "Infer Variables" $ it "testCons4" $ show (inferVariables testCons5) `shouldBe` show testCons5_infer describe "Check that (restricted) double to ratios is consistent" $ it "test all in -10/-10 ... 10/10, apart from /0" $ and [testDoubleToRationalSubset x y | x <- [-10..10], y <- [-10..10]] instance Arbitrary UnitInfo where arbitrary = do name <- arbitrary return $ UnitVar (name, name) testCons1 = [ ConEq (UnitName "kg") (UnitName "m") , ConEq (UnitVar ("x", "x")) (UnitName "m") , ConEq (UnitVar ("y", "y")) (UnitName "kg")] testCons1_flattened = [([UnitPow (UnitName "kg") 1.0],[UnitPow (UnitName "m") 1.0]) ,([UnitPow (UnitVar ("x", "x")) 1.0],[UnitPow (UnitName "m") 1.0]) ,([UnitPow (UnitVar ("y", "y")) 1.0],[UnitPow (UnitName "kg") 1.0])] testCons1_shifted = [([],[UnitPow (UnitName "m") 1.0,UnitPow (UnitName "kg") (-1.0)]) ,([UnitPow (UnitVar ("x", "x")) 1.0],[UnitPow (UnitName "m") 1.0]) ,([UnitPow (UnitVar ("y", "y")) 1.0],[UnitPow (UnitName "kg") 1.0])] -------------------------------------------------- testCons2 = [ConEq (UnitMul (UnitName "m") (UnitPow (UnitName "s") (-1.0))) (UnitMul (UnitName "m") (UnitPow (UnitName "s") (-1.0))) ,ConEq (UnitName "m") (UnitMul (UnitMul (UnitName "m") (UnitPow (UnitName "s") (-1.0))) (UnitName "s")) ,ConEq (UnitAlias "accel") (UnitMul (UnitName "m") (UnitPow (UnitParamPosUse (("simple1_sqr6", "sqr"),0,0)) (-1.0))) ,ConEq (UnitName "s") (UnitParamPosUse (("simple1_sqr6", "sqr"),1,0)) ,ConEq (UnitVar ("simple1_a5", "simple1_a5")) (UnitAlias "accel") ,ConEq (UnitVar ("simple1_t4", "simple1_t4")) (UnitName "s") ,ConEq (UnitVar ("simple1_v3", "simple1_v3")) (UnitMul (UnitName "m") (UnitPow (UnitName "s") (-1.0))) ,ConEq (UnitVar ("simple1_x1", "simple1_x1")) (UnitName "m") ,ConEq (UnitVar ("simple1_y2", "simple1_y2")) (UnitName "m") ,ConEq (UnitParamPosUse (("simple1_sqr6","sqr"),0,0)) (UnitParamPosUse (("simple1_mul7","mul"),0,1)) ,ConEq (UnitParamPosUse (("simple1_sqr6","sqr"),1,0)) (UnitParamPosUse (("simple1_mul7","mul"),1,1)) ,ConEq (UnitParamPosUse (("simple1_sqr6","sqr"),1,0)) (UnitParamPosUse (("simple1_mul7","mul"),2,1)) ,ConEq (UnitParamPosUse (("simple1_mul7","mul"),0,1)) (UnitMul (UnitParamPosUse (("simple1_mul7","mul"),1,1)) (UnitParamPosUse (("simple1_mul7","mul"),2,1))) ,ConEq (UnitAlias "accel") (UnitMul (UnitName "m") (UnitPow (UnitName "s") (-2.0)))] testCons2_shifted = [([],[UnitPow (UnitName "m") 1.0,UnitPow (UnitName "s") (-1.0),UnitPow (UnitName "m") (-1.0),UnitPow (UnitName "s") 1.0]) ,([],[UnitPow (UnitName "m") 1.0,UnitPow (UnitName "m") (-1.0)]) ,([UnitPow (UnitAlias "accel") 1.0,UnitPow (UnitParamPosUse (("simple1_sqr6","sqr"),0,0)) 1.0],[UnitPow (UnitName "m") 1.0]) ,([UnitPow (UnitParamPosUse (("simple1_sqr6","sqr"),1,0)) (-1.0)],[UnitPow (UnitName "s") (-1.0)]) ,([UnitPow (UnitVar ("simple1_a5", "simple1_a5")) 1.0,UnitPow (UnitAlias "accel") (-1.0)],[]) ,([UnitPow (UnitVar ("simple1_t4", "simple1_t4")) 1.0],[UnitPow (UnitName "s") 1.0]) ,([UnitPow (UnitVar ("simple1_v3", "simple1_v3")) 1.0],[UnitPow (UnitName "m") 1.0,UnitPow (UnitName "s") (-1.0)]) ,([UnitPow (UnitVar ("simple1_x1", "simple1_x1")) 1.0],[UnitPow (UnitName "m") 1.0]) ,([UnitPow (UnitVar ("simple1_y2", "simple1_y2")) 1.0],[UnitPow (UnitName "m") 1.0]) ,([UnitPow (UnitParamPosUse (("simple1_sqr6","sqr"),0,0)) 1.0,UnitPow (UnitParamPosUse (("simple1_mul7","mul"),0,1)) (-1.0)],[]) ,([UnitPow (UnitParamPosUse (("simple1_sqr6","sqr"),1,0)) 1.0,UnitPow (UnitParamPosUse (("simple1_mul7","mul"),1,1)) (-1.0)],[]) ,([UnitPow (UnitParamPosUse (("simple1_sqr6","sqr"),1,0)) 1.0,UnitPow (UnitParamPosUse (("simple1_mul7","mul"),2,1)) (-1.0)],[]) ,([UnitPow (UnitParamPosUse (("simple1_mul7","mul"),0,1)) 1.0,UnitPow (UnitParamPosUse (("simple1_mul7","mul"),1,1)) (-1.0),UnitPow (UnitParamPosUse (("simple1_mul7","mul"),2,1)) (-1.0)],[]) ,([UnitPow (UnitAlias "accel") 1.0],[UnitPow (UnitName "m") 1.0,UnitPow (UnitName "s") (-2.0)])] testCons3 = [ ConEq (UnitVar ("a", "a")) (UnitVar ("e", "e")) , ConEq (UnitVar ("a", "a")) (UnitMul (UnitVar ("b", "b")) (UnitMul (UnitVar ("c", "c")) (UnitVar ("d", "d")))) , ConEq (UnitVar ("d", "d")) (UnitName "m") ] testCons3_shifted = [([UnitPow (UnitVar ("a", "a")) 1.0,UnitPow (UnitVar ("e", "e")) (-1.0)],[]) ,([UnitPow (UnitVar ("a", "a")) 1.0,UnitPow (UnitVar ("b", "b")) (-1.0),UnitPow (UnitVar ("c", "c")) (-1.0),UnitPow (UnitVar ("d", "d")) (-1.0)],[]) ,([UnitPow (UnitVar ("d", "d")) 1.0],[UnitPow (UnitName "m") 1.0])] testCons4 = [ConEq (UnitVar ("simple2_a11", "simple2_a11")) (UnitParamPosUse (("simple2_sqr3","sqr"),0,0)) ,ConEq (UnitVar ("simple2_a22", "simple2_a22")) (UnitParamPosUse (("simple2_sqr3","sqr"),1,0)) -- ,ConEq (UnitVar ("simple2_a11", "simple2_a11")) (UnitVar ("simple2_a11", "simple2_a11")) -- ,ConEq (UnitVar ("simple2_a22", "simple2_a22")) (UnitVar ("simple2_a22", "simple2_a22")) ,ConEq (UnitParamPosUse (("simple2_sqr3","sqr"),0,0)) (UnitMul (UnitParamPosUse (("simple2_sqr3","sqr"),1,0)) (UnitParamPosUse (("simple2_sqr3","sqr"),1,0)))] testCons5 = [ConEq (UnitVar ("simple2_a11", "simple2_a11")) (UnitParamPosUse (("simple2_sqr3","sqr"),0,0)) ,ConEq (UnitAlias "accel") (UnitParamPosUse (("simple2_sqr3","sqr"),1,0)) ,ConEq (UnitVar ("simple2_a11", "simple2_a11")) (UnitVar ("simple2_a11", "simple2_a11")) ,ConEq (UnitVar ("simple2_a22", "simple2_a22")) (UnitAlias "accel") ,ConEq (UnitParamPosUse (("simple2_sqr3","sqr"),0,0)) (UnitMul (UnitParamPosUse (("simple2_sqr3","sqr"),1,0)) (UnitParamPosUse (("simple2_sqr3","sqr"),1,0))) ,ConEq (UnitAlias "accel") (UnitMul (UnitName "m") (UnitPow (UnitName "s") (-2.0)))] testCons5_infer = [(("simple2_a11", "simple2_a11"),UnitMul (UnitPow (UnitName "m") 2.0) (UnitPow (UnitName "s") (-4.0))) ,(("simple2_a22", "simple2_a22"),UnitMul (UnitPow (UnitName "m") 1.0) (UnitPow (UnitName "s") (-2.0)))] testDoubleToRationalSubset :: Integer -> Integer -> Bool testDoubleToRationalSubset x y = not (x <= 10 && y <= 10 && x >= -10 && y >= -10 && y /= 0) || doubleToRationalSubset (fromIntegral x / fromIntegral y) == Just (x % y)