improve (empty) → 0.0.0

raw patch · 4 files changed

+521/−0 lines, 4 filesdep +basedep +mtldep +processsetup-changed

Dependencies added: base, mtl, process

Files

LICENSE +27/−0
Language/ImProve.hs +450/−0
Setup.hs +6/−0
improve.cabal +38/−0

+ LICENSE view

@@ -0,0 +1,27 @@+Copyright (c) Tom Hawkins 2010++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.+3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE+ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF+SUCH DAMAGE.

+ Language/ImProve.hs view

@@ -0,0 +1,450 @@+module Language.ImProve+  (+  -- * Types+    E+  , V+  , AllE+  , NumE+  , Name+  -- * Expressions+  -- ** Constants+  , true+  , false+  , constant+  -- ** Variable Reference+  , ref+  -- ** Logical Operations+  , not_+  , (&&.)+  , (||.)+  , and_+  , or_+  , any_+  , all_+  , imply+  -- ** Equality and Comparison+  , (==.)+  , (/=.)+  , (<.)+  , (<=.)+  , (>.)+  , (>=.)+  -- ** Min, max, and limiting.+  , min_+  , minimum_+  , max_+  , maximum_+  , limit+  -- ** Arithmetic Operations+  , (*.)+  , (/.)+  , mod_+  -- ** Conditional Operator+  , mux+  -- ** Lookups+  , linear+  -- * Hierarchical Scope+  , scope+  -- * Variable Declarations+  , bool+  , bool'+  , int+  , int'+  , float+  , float'+  , input+  -- * Statements+  , Stmt+  -- ** Variable Assignment+  , (<==)+  -- ** Conditional Execution+  , ifelse+  , if_+  -- ** Incrementing and decrementing.+  , incr+  , decr+  -- ** Assertions and  Assumptions+  , assert+  , assume+  -- * Compilation+  , compile+  ) where++import Control.Monad+import Data.List+import Data.Ratio++infixl 7 *., /., `mod_`+infix  4 ==., /=., <., <=., >., >=.+infixl 3 &&.+infixl 2 ||.+infixr 1 <==++type Name = String++-- | Variables.+data V a+  = V   [Name] a+  | VIn [Name]++-- | All types.+class AllE a where+  showConst :: a -> String+  showType  :: a -> String++instance AllE Bool where+  showConst a = case a of+    True  -> "1"+    False -> "0"++  showType _ = "int"++instance AllE Int where+  showConst = show+  showType _ = "int"+  +instance AllE Float where+  showConst = show+  showType _ = "float"++-- | Number types.+class    AllE a => NumE a+instance NumE Int+instance NumE Float++-- | Core expressions.+data E a where+  Ref   :: V a -> E a+  Const :: AllE a => a -> E a+  Add   :: NumE a => E a -> E a -> E a+  Sub   :: NumE a => E a -> E a -> E a+  Mul   :: NumE a => E a -> a -> E a+  Div   :: NumE a => E a -> a -> E a+  Mod   :: E Int -> Int -> E Int+  Not   :: E Bool -> E Bool+  And   :: E Bool -> E Bool -> E Bool+  Or    :: E Bool -> E Bool -> E Bool+  Eq    :: AllE a => E a -> E a -> E Bool+  Lt    :: NumE a => E a -> E a -> E Bool+  Gt    :: NumE a => E a -> E a -> E Bool+  Le    :: NumE a => E a -> E a -> E Bool+  Ge    :: NumE a => E a -> E a -> E Bool+  Mux   :: E Bool -> E a -> E a -> E a++instance Show (E a) where show = undefined +instance Eq   (E a) where (==) = undefined++instance (Num a, AllE a, NumE a) => Num (E a) where+  (+) = Add+  (-) = Sub+  (*) = error "general multiplication not supported, use (*.)"+  negate a = 0 - a+  abs a = mux (a <. 0) (negate a) a+  signum a = mux (a ==. 0) 0 $ mux (a <. 0) (-1) 1+  fromInteger = Const . fromInteger++instance Fractional (E Float) where+  (/) = error "general division not supported, use (/.)"+  recip a = 1 / a+  fromRational r = Const $ fromInteger (numerator r) / fromInteger (denominator r)++-- | True term.+true :: E Bool+true = Const True++-- | False term.+false :: E Bool+false = Const False++-- | Arbitrary constants.+constant :: AllE a => a -> E a+constant = Const++-- | Logical negation.+not_ :: E Bool -> E Bool+not_ = Not++-- | Logical AND.+(&&.) :: E Bool -> E Bool -> E Bool+(&&.) = And++-- | Logical OR.+(||.) :: E Bool -> E Bool -> E Bool+(||.) = Or++-- | The conjunction of a E Bool list.+and_ :: [E Bool] -> E Bool+and_ = foldl (&&.) true++-- | The disjunction of a E Bool list.+or_ :: [E Bool] -> E Bool+or_ = foldl (||.) false++-- | True iff the predicate is true for all elements.+all_ :: (a -> E Bool) -> [a] -> E Bool+all_ f a = and_ $ map f a++-- | True iff the predicate is true for any element.+any_ :: (a -> E Bool) -> [a] -> E Bool+any_ f a = or_ $ map f a++-- Logical implication (if a then b).+imply :: E Bool -> E Bool -> E Bool +imply a b = not_ a ||. b++-- | Equal.+(==.) :: AllE a => E a -> E a -> E Bool+(==.) = Eq++-- | Not equal.+(/=.) :: AllE a => E a -> E a -> E Bool+a /=. b = not_ (a ==. b)++-- | Less than.+(<.) :: NumE a => E a -> E a -> E Bool+(<.) = Lt++-- | Greater than.+(>.) :: NumE a => E a -> E a -> E Bool+(>.) = Gt++-- | Less than or equal.+(<=.) :: NumE a => E a -> E a -> E Bool+(<=.) = Le++-- | Greater than or equal.+(>=.) :: NumE a => E a -> E a -> E Bool+(>=.) = Ge++-- | Returns the minimum of two numbers.+min_ :: NumE a => E a -> E a -> E a+min_ a b = mux (a <=. b) a b++-- | Returns the minimum of a list of numbers.+minimum_ :: NumE a => [E a] -> E a+minimum_ = foldl1 min_++-- | Returns the maximum of two numbers.+max_ :: NumE a => E a -> E a -> E a+max_ a b = mux (a >=. b) a b++-- | Returns the maximum of a list of numbers.+maximum_ :: NumE a => [E a] -> E a+maximum_ = foldl1 max_++-- | Limits between min and max.+limit :: NumE a => E a -> E a -> E a -> E a+limit a b i = max_ min $ min_ max i+  where+  min = min_ a b+  max = max_ a b++-- | Multiplication.+(*.) :: NumE a => E a -> a -> E a+(*.) = Mul++-- | Division.+(/.) :: NumE a => E a -> a -> E a+(/.) = Div++-- | Modulo.+mod_ :: E Int -> Int -> E Int+mod_ = Mod++-- | Linear interpolation and extrapolation between two points.+linear :: (Float, Float) -> (Float, Float) -> E Float -> E Float+linear (x1, y1) (x2, y2) a = a *. slope + constant inter+  where+  slope = (y2 - y1) / (x2 - x1)+  inter = y1 - slope * x1++-- | References a variable.+ref :: V a -> E a+ref = Ref++-- | Conditional expression.+--+-- > mux test onTrue onFalse+mux :: E Bool -> E a -> E a -> E a+mux = Mux++-- | Creates a hierarchical scope.+scope :: Name -> Stmt a -> Stmt a+scope name (Stmt f0) = Stmt f1+  where+  f1 (scope, statement) = (a, (scope, statement1))+    where+    (a, (_, statement1)) = f0 (scope ++ [name], statement)+  +getScope :: Stmt [Name]+getScope = Stmt $ \ (scope, statement) -> (scope, (scope, statement))++var :: AllE a => Name -> a -> Stmt (V a)+var name init = do+  scope <- getScope+  return $ V (scope ++ [name]) init++-- | Input variable declaration.  Input variables are initialized to 0.+input  :: (Name -> a -> Stmt (V a)) -> Name -> Stmt (E a)+input _ name = do+  scope <- getScope+  return $ ref $ VIn (scope ++ [name])++-- | Boolean variable declaration.+bool :: Name -> Bool -> Stmt (V Bool)+bool = var++-- | Boolean variable declaration and immediate assignment.+bool' :: Name -> E Bool -> Stmt (E Bool)+bool' name value = do+  a <- bool name False+  a <== value+  return $ ref a++-- | Int variable declaration.+int :: Name -> Int -> Stmt (V Int)+int = var++-- | Int variable declaration and immediate assignment.+int' :: Name -> E Int -> Stmt (E Int)+int' name value = do+  a <- int name 0+  a <== value+  return $ ref a++-- | Float variable declaration.+float :: Name -> Float -> Stmt (V Float)+float = var++-- | Float variable declaration and immediate assignment.+float' :: Name -> E Float -> Stmt (E Float)+float' name value = do+  a <- float name 0+  a <== value+  return $ ref a++-- | Increments an E Int.+incr :: V Int -> Stmt ()+incr a = a <== ref a + 1++-- | Decrements an E Int.+decr :: V Int -> Stmt ()+decr a = a <== ref a - 1++data Statement+  = AssignBool  (V Bool ) (E Bool )+  | AssignInt   (V Int  ) (E Int  )+  | AssignFloat (V Float) (E Float)+  | Branch (E Bool) Statement Statement+  | Sequence Statement Statement+  | Assert [Name] (E Bool)+  | Assume [Name] (E Bool)+  | Null++-- | The Stmt monad holds variable declarations and statements.+data Stmt a = Stmt (([Name], Statement) -> (a, ([Name], Statement)))++instance Monad Stmt where+  return a = Stmt $ \ s -> (a, s)+  (Stmt f1) >>= f2 = Stmt f3+    where+    f3 s1 = f4 s2+      where+      (a, s2) = f1 s1+      Stmt f4 = f2 a++statement :: Statement -> Stmt ()+statement a = Stmt $ \ (scope, statement) -> ((), (scope, Sequence statement a))++evalStmt :: [Name] -> Stmt () -> Statement+evalStmt scope (Stmt f) = snd $ snd $ f (scope, Null)++class    Assign a     where (<==) :: V a -> E a -> Stmt ()+instance Assign Bool  where a <== b = statement $ AssignBool  a b+instance Assign Int   where a <== b = statement $ AssignInt   a b+instance Assign Float where a <== b = statement $ AssignFloat a b++-- | Assert that a condition is true.+assert :: Name -> E Bool -> Stmt ()+assert a b = do+  scope <- getScope+  statement $ Assert (scope ++ [a]) b++-- | Declare an assumption condition is true.+assume :: Name -> E Bool -> Stmt ()+assume a b = do+  scope <- getScope+  statement $ Assume (scope ++ [a]) b++-- | Conditional if-else.+ifelse :: E Bool -> Stmt () -> Stmt () -> Stmt ()+ifelse cond onTrue onFalse = do+  scope <- getScope+  statement $ Branch cond (evalStmt scope onTrue) (evalStmt scope onFalse)++-- | Conditional without the else.+if_ :: E Bool -> Stmt () -> Stmt()+if_ cond stmt = ifelse cond stmt $ return ()++-- | Generate C code.+compile :: Name -> Stmt () -> IO ()+compile name program = do+  writeFile (name ++ ".c") $+       "// Generated by ImProve.\n\n"+    ++ "#include <assert.h>\n\n"+    ++ "// XXX Need to build state struct.\n\n"+    ++ "void " ++ name ++ "() {\n"+    ++ indent (codeStmt stmt)+    ++ "}\n\n"+  writeFile (name ++ ".h") $+       "// Generated by ImProve.\n\n"+    ++ "// XXX Need to build state struct.\n\n"+    ++ "void " ++ name ++ "(void);\n\n"+  where+  stmt = evalStmt [] program++  varName :: V a -> String+  varName a = intercalate "." $ (name ++ "Variables") : names+    where+    names = case a of+      V names _ -> names+      VIn names -> names+  +  codeStmt :: Statement -> String+  codeStmt a = case a of+    AssignBool  a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"+    AssignInt   a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"+    AssignFloat a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"+    Branch a b Null -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\n"+    Branch a b c    -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\nelse {\n" ++ indent (codeStmt c) ++ "}\n"+    Sequence a b -> codeStmt a ++ codeStmt b+    Assert names a -> "// assert " ++ intercalate "." names ++ "\nassert(" ++ codeExpr a ++ ");\n"+    Assume names a -> "// assume " ++ intercalate "." names ++ "\nassert(" ++ codeExpr a ++ ");\n"+    Null -> ""+  +  codeExpr :: E a -> String+  codeExpr a = case a of+    Ref a -> varName a+    Const a -> showConst a+    Add a b -> group [codeExpr a, "+", codeExpr b]+    Sub a b -> group [codeExpr a, "-", codeExpr b]+    Mul a b -> group [codeExpr a, "*", showConst b]+    Div a b -> group [codeExpr a, "/", showConst b]+    Mod a b -> group [codeExpr a, "%", showConst b]+    Not a   -> group ["!", codeExpr a]+    And a b -> group [codeExpr a, "&&",  codeExpr b]+    Or  a b -> group [codeExpr a, "||",  codeExpr b]+    Eq  a b -> group [codeExpr a, "==",  codeExpr b]+    Lt  a b -> group [codeExpr a, "<",   codeExpr b]+    Gt  a b -> group [codeExpr a, ">",   codeExpr b]+    Le  a b -> group [codeExpr a, "<=",  codeExpr b]+    Ge  a b -> group [codeExpr a, ">=",  codeExpr b]+    Mux a b c -> group [codeExpr a, "?", codeExpr b, ":", codeExpr c] +    where+    group :: [String] -> String+    group a = "(" ++ intercalate " " a ++ ")"+++indent :: String -> String+indent = unlines . map ("  " ++) . lines+

+ Setup.hs view

@@ -0,0 +1,6 @@+#! /usr/bin/env runhaskell++import Distribution.Simple (defaultMain)++main :: IO ()+main = defaultMain

+ improve.cabal view

@@ -0,0 +1,38 @@+name:    improve+version: 0.0.0++category: Language++synopsis: A simple imperative, provable programming language for embedded applications.++description:+    TODO++author:     Tom Hawkins <tomahawkins@gmail.com>+maintainer: Tom Hawkins <tomahawkins@gmail.com>++license:      BSD3+license-file: LICENSE++homepage: http://tomahawkins.org++build-type:    Simple+cabal-version: >= 1.6++library+    build-depends:+        base       >= 4.2     && < 5,+        mtl        >= 1.1.0.1 && < 1.2,+        process    >= 1.0.1.1 && < 1.2++    exposed-modules:+        Language.ImProve++    extensions: GADTs, FlexibleInstances++    ghc-options: -W++source-repository head+    type:     git+    location: git://github.com/tomahawkins/atom.git+