module Language.ImProve.Code.Ada (codeAda) where
import Control.Monad.State
import Data.List
import Text.Printf
import Language.ImProve.Core
import Language.ImProve.Tree hiding (Branch)
import qualified Language.ImProve.Tree as T
codeAda :: Name -> Statement -> IO ()
codeAda name stmt = do
writeFile (name ++ ".ads") $ unlines
[ "-- Generated by ImProve."
, ""
, "package " ++ name ++ " is"
, ""
, indent $ unlines
[ codeVariables name scope
, name ++ "_Variables : " ++ name ++ "_Record0;"
, ""
, "procedure " ++ name ++ ";"
]
, "end " ++ name ++ ";"
, ""
]
writeFile (name ++ ".adb") $ unlines
[ "-- Generated by ImProve."
, ""
, "with Ada.Assertions;"
, ""
, "package body " ++ name ++ " is"
, ""
, indent $ unlines
[ "procedure " ++ name ++ " is"
, " use Ada.Assertions;"
, "begin"
, indent $ codeStmt name [] stmt
, "end " ++ name ++ ";"
, ""
]
, "end " ++ name ++ ";"
, ""
]
where
scope = case tree (\ (_, path, _) -> path) $ stmtVars stmt of
[] -> error "program contains no useful statements"
a -> T.Branch (name ++ "_variables") a
instance Show Statement where show = codeStmt "none" []
codeStmt :: Name -> [Name] -> Statement -> String
codeStmt name path a = case a of
Assign a b -> name ++ "_Variables." ++ pathName a ++ " := " ++ codeExpr b ++ ";\n"
Branch a b Null -> "if " ++ codeExpr a ++ " then\n" ++ indent (codeStmt name path b) ++ "end if;\n"
Branch a b c -> "if " ++ codeExpr a ++ " then\n" ++ indent (codeStmt name path b) ++ "\nelse\n" ++ indent (codeStmt name path c) ++ "end if;\n"
Sequence a b -> codeStmt name path a ++ codeStmt name path b
Theorem _ _ _ a -> "Assert(" ++ codeExpr a ++ ", " ++ show (pathName path) ++ ");\n"
Assume _ a -> "Assert(" ++ codeExpr a ++ ", " ++ show (pathName path) ++ ");\n"
Label name' a -> "-- " ++ name' ++ "\n" ++ indent (codeStmt name (path ++ [name']) a)
Null -> ""
where
codeExpr :: E a -> String
codeExpr a = case a of
Ref a -> name ++ "_Variables." ++ pathName a
Const a -> showConst $ const' a
Add a b -> group [codeExpr a, "+", codeExpr b]
Sub a b -> group [codeExpr a, "-", codeExpr b]
Mul a b -> group [codeExpr a, "*", showConst (const' b)]
Div a b -> group [codeExpr a, "/", showConst (const' b)]
Mod a b -> group [codeExpr a, "mod", showConst (const' b)]
Not a -> group ["not", codeExpr a]
And a b -> group [codeExpr a, "and", codeExpr b]
Or a b -> group [codeExpr a, "or", 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 ["if", codeExpr a, "then", codeExpr b, "else", codeExpr c]
where
group :: [String] -> String
group a = "(" ++ intercalate " " a ++ ")"
indent :: String -> String
indent = unlines . map (" " ++) . lines
type Rec = State (Int, String)
codeVariables :: Name -> Tree Name (Bool, Path, Const) -> String
codeVariables name a = indent s
where
(_, s) = execState (typ a) (0, "")
typ :: Tree Name (Bool, Path, Const) -> Rec String
typ a = case a of
T.Branch _ items -> do
i <- nextId
fields <- mapM field items
let typeName = printf "%s_Record%d" name i
appendCode $ unlines
[ printf "type %s is" typeName
, indent $ unlines
[ "record"
, indent $ unlines $ fields
, "end record;"
]
]
return typeName
Leaf _ (_, _, init) -> return $ printf "%s := %s" (showConstType init) (showConst init)
field :: Tree Name (Bool, Path, Const) -> Rec String
field a = do
t <- typ a
case a of
T.Branch name _ -> return $ printf "%-30s : %s;" name t
Leaf name (input, _, _) -> return $ printf "%-30s : %s;%s" name t (if input then " -- input" else "")
nextId :: Rec Int
nextId = do
(i, s) <- get
put (i + 1, s)
return i
appendCode :: String -> Rec ()
appendCode s = modify $ \ (i, s') -> (i, s' ++ s)
showConst :: Const -> String
showConst a = case a of
Bool a -> show a
Int a -> show a
Float a -> show a
showConstType :: Const -> String
showConstType a = case a of
Bool _ -> "Boolean"
Int _ -> "Integer range -2147483648 .. 2147483647"
Float _ -> "Float"