-- | A DSL for ACL2.
module Language.ACL2
  ( Expr (..)
  , check
  , check'
  , mutualRecursion
  , defun
  , defun'
  , defconst
  , defthm
  , thm
  , call
  , obj
  , quote
  , consp
  , cons
  , car
  , cdr
  , nth
  , len
  , take'
  , nthcdr
  , updateNth
  , append
  , let'
  , if'
  , case'
  , assoc
  , var
  , list
  , lit
  , string
  , nil
  , t
  , zp
  , zip'
  , undefined'
  , equal
  , not'
  , and'
  , or'
  , implies
  , goodbye
  , integerp
  , mod'
  , (<.)
  , (>.)
  , (<=.)
  , (>=.)
  ) where

import Data.List
import System.Environment
import System.Process

data SExpr
  = SV String
  | SA [SExpr]

instance Show SExpr where
  show a = case a of
    SV a -> a ++ "\n"
    SA args -> "( " ++ indent (concatMap show args) ++ ")\n"
      where
      indent = drop 2 . unlines . map ("  " ++) . lines

data Expr
  = Obj [Expr]
  | Lit String
  deriving (Eq, Ord)

instance Show Expr where show = show . sExpr

instance Num Expr where
  a + b = call "+" [a, b]
  a - b = call "-" [a, b]
  a * b = call "*" [a, b]
  negate a = 0 - a
  abs = undefined
  signum = undefined
  fromInteger = Lit . show

sExpr :: Expr -> SExpr
sExpr a = case a of
  Obj     a   -> SA $ map sExpr a
  Lit     a   -> SV a

check' :: [Expr] -> IO (Bool, String)
check' a = do
  exe <- savedACL2
  (_, result, _) <- readProcessWithExitCode exe [] code
  let pass = not $ any (isPrefixOf "ACL2 Error") $ lines result
  return (pass, result)
  where
  code = unlines $ map show a
  savedACL2 :: IO FilePath
  savedACL2 = do
    env <- getEnvironment
    case lookup "ACL2_SOURCES" env of
      Nothing -> error "Environment variable ACL2_SOURCES not set."
      Just a -> return $ a ++ "/saved_acl2"

check :: [Expr] -> IO Bool
check a = check' a >>= return . fst

uni :: String -> Expr -> Expr
uni f a = call f [a]

bin :: String -> Expr -> Expr -> Expr
bin f a b = call f [a, b]

tri :: String -> Expr -> Expr -> Expr -> Expr
tri f a b c = call f [a, b, c]

mutualRecursion :: [Expr] -> Expr
mutualRecursion = call "mutual-recursion"

defun :: String -> [String] -> Expr -> Expr
defun name args body = call "defun" [var name, obj $ map var args, body]

defun' :: String -> [String] -> Expr -> Expr -> Expr
defun' name args measure body = call "defun"
  [ var name
  , obj $ map var args
  , call "declare" [call "xargs" [var ":measure", call "nfix" [measure]]]
  , body
  ]

defconst :: String -> Expr -> Expr
defconst name const = call "defconst" [var name, const]

defthm :: String -> Expr -> Expr
defthm name a = call "defthm" [var name, a]

thm :: Expr -> Expr
thm = uni "thm"
 
call :: String -> [Expr] -> Expr
call a b = Obj $ var a : b

obj :: [Expr] -> Expr
obj = Obj

quote :: Expr -> Expr
quote = uni "quote"

list :: [Expr] -> Expr
list a = call "list" a

consp :: Expr -> Expr
consp = uni "consp"

cons :: Expr -> Expr -> Expr
cons = bin "cons"

car :: Expr -> Expr
car = uni "car"

cdr :: Expr -> Expr
cdr = uni "cdr"

nth :: Expr -> Expr -> Expr
nth = bin "nth"

len :: Expr -> Expr
len = uni "len"

take' :: Expr -> Expr -> Expr
take' = bin "take"

nthcdr :: Expr -> Expr -> Expr
nthcdr = bin "nthcdr"

updateNth :: Expr -> Expr -> Expr -> Expr
updateNth = tri "update-nth"

append :: Expr -> Expr -> Expr
append = bin "append"

let' :: [(String, Expr)] -> Expr -> Expr
let' a b = case b of
  Obj [Lit "let*", Obj lets, expr] -> call "let*" [obj $ [ obj [var n, e] | (n, e) <- a ] ++ lets, expr]
  _ -> call "let*" [obj [ obj [var n, e] | (n, e) <- a ], b]

var :: String -> Expr
var = Lit

lit :: String -> Expr
lit = Lit

string :: String -> Expr
string = Lit . show

nil :: Expr
nil = Lit "nil"

t :: Expr
t = Lit "t"

if' :: Expr -> Expr -> Expr -> Expr
if' = tri "if"

case' :: Expr -> [(Expr, Expr)] -> Expr -> Expr
case' a b c = call "case" $ a : [ obj [a, b] | (a, b) <- b ] ++ [call "otherwise" [c]]

zp :: Expr -> Expr
zp = uni "zp"

zip' :: Expr -> Expr
zip' = uni "zip"

integerp :: Expr -> Expr
integerp = uni "integerp"

undefined' :: Expr
undefined' = Lit "undefined"

equal :: Expr -> Expr -> Expr
equal = bin "equal"

not' :: Expr -> Expr
not' = uni "not"

and' :: Expr -> Expr -> Expr
and' = bin "and"

or' :: Expr -> Expr -> Expr
or' = bin "or"

implies :: Expr -> Expr -> Expr
implies = bin "implies"

goodbye :: Expr
goodbye = call "good-bye" []

mod' :: Expr -> Expr -> Expr
mod' = bin "mod"

(<.) :: Expr -> Expr -> Expr
(<.) = bin "<"

(<=.) :: Expr -> Expr -> Expr
(<=.) = bin "<="

(>.) :: Expr -> Expr -> Expr
(>.) = bin ">"

(>=.) :: Expr -> Expr -> Expr
(>=.) = bin ">="

assoc :: Expr -> Expr -> Expr
assoc = bin "assoc"