acl2 (empty) → 0.0.0

raw patch · 4 files changed

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

Dependencies added: base, process

Files

LICENSE +25/−0
Language/ACL2.hs +261/−0
Setup.hs +6/−0
acl2.cabal +29/−0

+ LICENSE view

@@ -0,0 +1,25 @@+Copyright (c) Tom Hawkins 2014++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. For non-commercial use only.++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/ACL2.hs view

@@ -0,0 +1,261 @@+-- | 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'' :: Bool -> [Expr] -> IO Bool+check'' debug a = do+  exe <- savedACL2+  (_, result, _) <- readProcessWithExitCode exe [] code+  let pass = not $ any (isPrefixOf "ACL2 Error") $ lines result+  if debug+    then do+      putStrLn code+      putStrLn result+    else return ()+  return pass+  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 = check'' False++check' :: [Expr] -> IO Bool+check' = check'' True++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"+

+ Setup.hs view

@@ -0,0 +1,6 @@+module Main (main) where++import Distribution.Simple (defaultMain)++main :: IO ()+main = defaultMain

+ acl2.cabal view

@@ -0,0 +1,29 @@+name:    acl2+version: 0.0.0++category: Language, Formal Methods++synopsis:    Writing and calling ACL2 from Haskell.+description: Writing and calling ACL2 from Haskell.++author:     Tom Hawkins  <tomahawkins@gmail.com>+maintainer: Tom Hawkins  <tomahawkins@gmail.com>++license: BSD3+license-file: LICENSE++build-type:    Simple+cabal-version: >= 1.9.2++library+  build-depends:+    base     >= 4.0 && < 6.0,+    process  >= 1.0 && < 2.0+  exposed-modules:+    Language.ACL2+  ghc-options: -W++source-repository head+  type:     git+  location: git://github.com/tomahawkins/acl2.git+