Add experimental support for units of measurement, only in constraint…

…s for now.

src/Redfin/Examples/Energy.hs

@@ -8,14 +8,15 @@ module Redfin.Examples.Energy (
 
 import Prelude hiding (read)
 import Text.Pretty.Simple (pPrint)
-import Data.SBV
+import Data.SBV hiding ((%), (#))
 import Redfin
 import Redfin.Assembly hiding (div, abs)
 import Redfin.Listing
 import qualified Redfin.Assembly as Assembly
 import Redfin.Verify
 import Redfin.Data.Fixed
 import Redfin.Language.Expression
+import Redfin.Language.Units
 import Redfin.Examples.Common
 
 energyEstimate :: Integral a => a -> a -> a -> a -> a
@@ -57,19 +58,21 @@ energyEstimateLowLevel = do
     st r1 p2
     mul r0 p2
     sra_i r0 1
-    div_si r0 2
     halt
 
+-- t :: Fixed
+-- t = (30 % Year) # Second
+
 equivalence :: Symbolic SBool
 equivalence = do
     t1 <- forall "t1"
     t2 <- forall "t2"
     p1 <- forall "p1"
     p2 <- forall "p2"
-    constrain $ t1 .>= 0 &&& t1 .<= 948672000000
-    constrain $ t2 .>= 0 &&& t2 .<= 948672000000
-    constrain $ p1 .>= 0 &&& p1 .<= 1000
-    constrain $ p2 .>= 0 &&& p2 .<= 1000
+    constrain $ t1 .>= 0 &&& t1 .<= getFixed ((30 % Year :: Time) # Second)
+    constrain $ t2 .>= 0 &&& t2 .<= getFixed ((30 % Year :: Time) # Second)
+    constrain $ p1 .>= 0 &&& p1 .<= getFixed ((1 % Watt :: Power) # milli Watt)
+    constrain $ p2 .>= 0 &&& p2 .<= getFixed ((1 % Watt :: Power) # milli Watt)
     let mem = initialiseMemory [(0, t1), (1, t2), (2, p1), (3, p2), (5, 100)]
         steps = 100
         finalStateLL = verify steps $ templateState energyEstimateLowLevel mem
@@ -101,10 +104,10 @@ highLevelCorrect = do
     t2 <- forall "t2"
     p1 <- forall "p1"
     p2 <- forall "p2"
-    constrain $ t1 .>= 0 &&& t1 .<= 948672000000
-    constrain $ t2 .>= 0 &&& t2 .<= 948672000000
-    constrain $ p1 .>= 0 &&& p1 .<= 1000
-    constrain $ p2 .>= 0 &&& p2 .<= 1000
+    constrain $ t1 .>= 0 &&& t1 .<= getFixed ((30 % Year :: Time) # Second)
+    constrain $ t2 .>= 0 &&& t2 .<= getFixed ((30 % Year :: Time) # Second)
+    constrain $ p1 .>= 0 &&& p1 .<= getFixed ((1 % Watt :: Power) # milli Watt)
+    constrain $ p2 .>= 0 &&& p2 .<= getFixed ((1 % Watt :: Power) # milli Watt)
     let mem = initialiseMemory [(0, t1), (1, t2), (2, p1), (3, p2), (5, 100)]
         steps = 100
         finalState = verify steps $ templateState energyEstimateHighLevel mem
@@ -113,6 +116,26 @@ highLevelCorrect = do
     pure $   bnot overflow
          &&& result .>= 0
 
+
+highLevelCorrectFP :: Symbolic SBool
+highLevelCorrectFP = do
+    t1 <- forall "t1"
+    t2 <- forall "t2"
+    p1 <- forall "p1"
+    p2 <- forall "p2"
+    constrain $ t1 .>= 0 &&& t1 .<= getFixed ((30 % Year :: Time) # Second)
+    constrain $ t2 .>= 0 &&& t2 .<= getFixed ((30 % Year :: Time) # Second)
+    constrain $ p1 .>= 0 &&& p1 .<= getFixed ((1 % Watt :: Power) # milli Watt)
+    constrain $ p2 .>= 0 &&& p2 .<= getFixed ((1 % Watt :: Power) # milli Watt)
+    let mem = initialiseMemory [(0, t1), (1, t2), (2, p1), (3, p2), (5, 100)]
+        steps = 100
+        finalState = verify steps $ templateState energyEstimateHighLevel mem
+        result = readArray (registers finalState) 0
+        overflow = readArray (flags finalState) (flagId Overflow)
+    pure $
+        -- bnot overflow &&&
+        (Fixed $ result) .>= 0
+
 simulateHighLevel :: IO ()
 simulateHighLevel = do
     let mem = initialiseMemory [ (0, 10)

src/Redfin/Language/Units.hs

@@ -0,0 +1,32 @@
+{-# LANGUAGE DataKinds, StandaloneDeriving, TypeOperators #-}
+
+module Redfin.Language.Units (Year (..), Time, Power, Energy
+                             , module Data.Units.SI
+                             , module Data.Units.SI.Prefixes
+                             , module Data.Metrology.Poly ) where
+
+import Data.Metrology.Poly
+import Data.Metrology.SI   ()  -- DefaultLCSU instances
+import qualified Data.Metrology.SI.PolyTypes as SI
+import Data.Units.SI
+import Data.Units.SI.Prefixes
+import Data.Metrology.Show
+import Data.Metrology.Unsafe
+import Redfin.Data.Fixed
+
+data Year = Year
+instance Unit Year where
+  type BaseUnit Year = Second
+  conversionRatio _ = 60 * 60 * 24 * 365.242
+
+type Time = SI.Time 'DefaultLCSU Fixed
+
+type Power = SI.Power 'DefaultLCSU Fixed
+
+type Energy = Time %* Power
+
+t :: Time
+t = 30 % Year
+
+t' :: Fixed
+t' = ((1 % Watt :: Power) # milli Watt)

stack.yaml

@@ -1,3 +1,6 @@
 packages:
 - '.'
-resolver: lts-10.3
+resolver: lts-10.3
+extra-deps:
+- units-2.4.1
+- units-defs-2.0.1.1