camfort-0.901: tests/Camfort/Specification/UnitsSpec.hs
{-# LANGUAGE ImplicitParams #-}
module Camfort.Specification.UnitsSpec (spec) where
import qualified Data.ByteString.Char8 as B
import Language.Fortran.Parser.Any
import qualified Language.Fortran.Analysis as FA
import qualified Language.Fortran.Analysis.Renaming as FAR
import Camfort.Input
import Camfort.Functionality
import Camfort.Output
import Camfort.Analysis.Annotations
import Camfort.Specification.Units
import Camfort.Specification.Units.Monad
import Camfort.Specification.Units.InferenceFrontend
import Camfort.Specification.Units.InferenceBackend
import Camfort.Specification.Units.Environment
import Data.List
import Data.Maybe
import Data.Either
import qualified Data.Array as A
import qualified Numeric.LinearAlgebra as H
import qualified Data.Map.Strict as M
import GHC.Real
import Numeric.LinearAlgebra (
atIndex, (<>), (><), rank, (?), toLists, toList, fromLists, fromList, rows, cols,
takeRows, takeColumns, dropRows, dropColumns, subMatrix, diag, build, fromBlocks,
ident, flatten, lu, dispf, Matrix
)
import Test.Hspec
import Test.QuickCheck
import Test.Hspec.QuickCheck
runFrontendInit litMode pf = usConstraints state
where
pf' = FA.initAnalysis . fmap mkUnitAnnotation . fmap (const unitAnnotation) $ pf
uOpts = unitOpts0 { uoNameMap = M.empty, uoDebug = False, uoLiterals = litMode }
(_, state, logs) = runUnitSolver uOpts pf' initInference
runUnits litMode pf m = (r, usConstraints state)
where
pf' = FA.initAnalysis . fmap mkUnitAnnotation . fmap (const unitAnnotation) $ pf
uOpts = unitOpts0 { uoNameMap = M.empty, uoDebug = False, uoLiterals = litMode }
(r, state, logs) = runUnitSolver uOpts pf' $ initInference >> m
runUnits' litMode pf m = (state, logs)
where
pf' = FA.initAnalysis . fmap mkUnitAnnotation . fmap (const unitAnnotation) $ pf
uOpts = unitOpts0 { uoNameMap = M.empty, uoDebug = True, uoLiterals = litMode }
(r, state, logs) = runUnitSolver uOpts pf' $ initInference >> m
runUnitsRenamed' litMode pf m = (state, logs)
where
pf' = FAR.analyseRenames . FA.initAnalysis . fmap mkUnitAnnotation . fmap (const unitAnnotation) $ pf
uOpts = unitOpts0 { uoNameMap = FAR.extractNameMap pf', uoDebug = True, uoLiterals = litMode }
(r, state, logs) = runUnitSolver uOpts pf' $ initInference >> m
spec :: Spec
spec = do
describe "Unit Inference Frontend" $ do
describe "Literal Mode" $ do
it "litTest1 Mixed" $ do
head (fromJust (head (rights [fst (runUnits LitMixed litTest1 runInconsistentConstraints)]))) `shouldSatisfy`
conParamEq (ConEq (UnitName "a") (UnitMul (UnitName "a") (UnitVar ("j", "j"))))
it "litTest1 Poly" $ do
head (fromJust (head (rights [fst (runUnits LitPoly litTest1 runInconsistentConstraints)]))) `shouldSatisfy`
conParamEq (ConEq (UnitName "a") (UnitMul (UnitName "a") (UnitVar ("j", "j"))))
it "litTest1 Unitless" $ do
head (fromJust (head (rights [fst (runUnits LitUnitless litTest1 runInconsistentConstraints)]))) `shouldSatisfy`
conParamEq (ConEq (UnitName "a") (UnitVar ("k", "k")))
describe "Polymorphic functions" $ do
it "squarePoly1" $ do
show (sort (head (rights [fst (runUnits LitMixed squarePoly1 runInferVariables)]))) `shouldBe`
show (sort [(("a", "a"),UnitName "m"),(("b", "b"), UnitName "s"),(("x", "x"),UnitPow (UnitName "m") 2.0),(("y", "y"),UnitPow (UnitName "s") 2.0)])
describe "Recursive functions" $ do
it "Recursive Addition is OK" $ do
show (sort (head (rights [fst (runUnits LitMixed recursive1 runInferVariables)]))) `shouldBe`
show (sort [(("y", "y"),UnitName "m"),(("z", "z"), UnitName "m")])
describe "Recursive functions" $ do
it "Recursive Multiplication is not OK" $ do
head (fromJust (head (rights [fst (runUnits LitMixed recursive2 runInconsistentConstraints)]))) `shouldSatisfy`
conParamEq (ConEq (UnitParamPosAbs ("recur", 0)) (UnitParamPosAbs ("recur", 2)))
describe "Unit Inference Backend" $ do
describe "Flatten constraints" $ do
it "testCons1" $ do
flattenConstraints testCons1 `shouldBe` testCons1_flattened
describe "Shift terms" $ do
it "testCons1" $ do
map shiftTerms (flattenConstraints testCons1) `shouldBe` testCons1_shifted
it "testCons2" $ do
map shiftTerms (flattenConstraints testCons2) `shouldBe` testCons2_shifted
it "testCons3" $ do
map shiftTerms (flattenConstraints testCons3) `shouldBe` testCons3_shifted
describe "Consistency" $ do
it "testCons1" $ do
inconsistentConstraints testCons1 `shouldBe` Just [ConEq (UnitName "kg") (UnitName "m")]
it "testCons2" $ do
inconsistentConstraints testCons2 `shouldBe` Nothing
it "testCons3" $ do
inconsistentConstraints testCons3 `shouldBe` Nothing
describe "Critical Variables" $ do
it "testCons2" $ do
criticalVariables testCons2 `shouldSatisfy` null
it "testCons3" $ do
criticalVariables testCons3 `shouldBe` [UnitVar ("c", "c"), UnitVar ("e", "e")]
it "testCons4" $ do
criticalVariables testCons4 `shouldBe` [UnitVar ("simple2_a22", "simple2_a22")]
it "testCons5" $ do
criticalVariables testCons5 `shouldSatisfy` null
describe "Infer Variables" $ do
it "testCons5" $ do
inferVariables testCons5 `shouldBe` testCons5_infer
describe "Check that (restricted) double to ratios is consistent" $ do
it "test all in -10/-10 ... 10/10, apart from /0" $
do and [testDoubleToRationalSubset x y | x <- [-10..10], y <- [-10..10]]
--------------------------------------------------
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",0,0)) (-1.0)))
,ConEq (UnitName "s") (UnitParamPosUse ("simple1_sqr6",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",0,0)) (UnitParamPosUse ("simple1_mul7",0,1))
,ConEq (UnitParamPosUse ("simple1_sqr6",1,0)) (UnitParamPosUse ("simple1_mul7",1,1))
,ConEq (UnitParamPosUse ("simple1_sqr6",1,0)) (UnitParamPosUse ("simple1_mul7",2,1))
,ConEq (UnitParamPosUse ("simple1_mul7",0,1)) (UnitMul (UnitParamPosUse ("simple1_mul7",1,1)) (UnitParamPosUse ("simple1_mul7",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",0,0)) 1.0],[UnitPow (UnitName "m") 1.0])
,([UnitPow (UnitParamPosUse ("simple1_sqr6",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",0,0)) 1.0,UnitPow (UnitParamPosUse ("simple1_mul7",0,1)) (-1.0)],[])
,([UnitPow (UnitParamPosUse ("simple1_sqr6",1,0)) 1.0,UnitPow (UnitParamPosUse ("simple1_mul7",1,1)) (-1.0)],[])
,([UnitPow (UnitParamPosUse ("simple1_sqr6",1,0)) 1.0,UnitPow (UnitParamPosUse ("simple1_mul7",2,1)) (-1.0)],[])
,([UnitPow (UnitParamPosUse ("simple1_mul7",0,1)) 1.0,UnitPow (UnitParamPosUse ("simple1_mul7",1,1)) (-1.0),UnitPow (UnitParamPosUse ("simple1_mul7",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",0,0))
,ConEq (UnitVar ("simple2_a22", "simple2_a22")) (UnitParamPosUse ("simple2_sqr3",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",0,0)) (UnitMul (UnitParamPosUse ("simple2_sqr3",1,0)) (UnitParamPosUse ("simple2_sqr3",1,0)))]
testCons5 = [ConEq (UnitVar ("simple2_a11", "simple2_a11")) (UnitParamPosUse ("simple2_sqr3",0,0))
,ConEq (UnitAlias "accel") (UnitParamPosUse ("simple2_sqr3",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",0,0)) (UnitMul (UnitParamPosUse ("simple2_sqr3",1,0)) (UnitParamPosUse ("simple2_sqr3",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 =
if x <= 10 && y <= 10 && x >= -10 && y >= -10 && y /= 0
then doubleToRationalSubset (fromIntegral x / fromIntegral y) == Just (x % y)
else True
--------------------------------------------------
litTest1 = flip fortranParser "litTest1.f90" . B.pack $ unlines
[ "program main"
, " != unit(a) :: x"
, " real :: x, j, k"
, ""
, " j = 1 + 1"
, " k = j * j"
, " x = x + k"
, " x = x * j ! inconsistent"
, "end program main" ]
squarePoly1 = flip fortranParser "squarePoly1.f90" . B.pack $ unlines
[ "! Demonstrates parametric polymorphism through functions-calling-functions."
, "program squarePoly"
, " implicit none"
, " real :: x"
, " real :: y"
, " != unit(m) :: a"
, " real :: a"
, " != unit(s) :: b"
, " real :: b"
, " x = squareP(a)"
, " y = squareP(b)"
, " contains"
, " real function square(n)"
, " real :: n"
, " square = n * n"
, " end function"
, " real function squareP(m)"
, " real :: m"
, " squareP = square(m)"
, " end function"
, "end program" ]
recursive1 = flip fortranParser "recursive1.f90" . B.pack $ unlines
[ "program main"
, " != unit(m) :: y"
, " integer :: x = 5, y = 2, z"
, " z = recur(x,y)"
, " print *, y"
, "contains"
, " real recursive function recur(n, b) result(r)"
, " integer :: n, b"
, " if (n .EQ. 0) then"
, " r = b"
, " else"
, " r = b + recur(n - 1, b)"
, " end if"
, " end function recur"
, "end program main" ]
recursive2 = flip fortranParser "recursive2.f90" . B.pack $ unlines
[ "program main"
, " != unit(m) :: y"
, " integer :: x = 5, y = 2, z"
, " z = recur(x,y)"
, " print *, y"
, "contains"
, " real recursive function recur(n, b) result(r)"
, " integer :: n, b"
, " if (n .EQ. 0) then"
, " r = b"
, " else"
, " r = b * recur(n - 1, b) ! inconsistent"
, " end if"
, " end function recur"
, "end program main" ]