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

-- | Generate Ada.
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"