FirstOrderTheory (empty) → 0.1.0.4

raw patch · 6 files changed

+175/−0 lines, 6 filesdep +basedep +containerssetup-changed

Dependencies added: base, containers

Files

• FirstOrderTheory.cabal +21/−0
• LICENSE +30/−0
• Setup.hs +2/−0
• src/FirstOrderTheory/Syntax.hs +79/−0
• src/FirstOrderTheory/Theory.hs +31/−0
• src/FirstOrderTheory/Utils.hs +12/−0

@@ -0,0 +1,21 @@+-- Initial FirstOrderTheory.cabal generated by cabal init.  For further+-- documentation, see http://haskell.org/cabal/users-guide/++name:                FirstOrderTheory+version:             0.1.0.4+synopsis:            Grammar and typeclass for first order theories+description:         Grammar and typeclass for first order theories+license:             BSD3+license-file:        LICENSE+author:              Dillon Huff+maintainer:          dillonhuff@gmail.com+-- copyright:           +category:            Math+build-type:          Simple+cabal-version:       >=1.8++library+  exposed-modules:     FirstOrderTheory.Theory, FirstOrderTheory.Utils, FirstOrderTheory.Syntax+  -- other-modules:       +  build-depends:       base ==4.6.*, containers+  hs-source-dirs:      src

@@ -0,0 +1,30 @@+Copyright (c) 2014, Dillon Huff++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * 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.++    * Neither the name of Dillon Huff nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"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 COPYRIGHT+OWNER 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.

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,79 @@+module FirstOrderTheory.Syntax(+  Literal, Atom, Term,+  atomArgs, predicateName, isFunctionWithName,+  isNeg, getAtom, varName, intVal, funcArgs,+  lit, nLit, atom, func, var, intConst) where++import Data.List as L++import FirstOrderTheory.Utils++data Literal+  = Lit Atom+  | Neg Atom+    deriving (Eq, Ord)++lit = Lit+nLit = Neg++-- |Returns false if the literal is an atomic formula and true if the+-- literal is the negation of an atomic formula+isNeg :: Literal -> Bool+isNeg (Neg _) = True+isNeg _ = False++-- |Returns the atomic formula of the given literal+getAtom :: Literal -> Atom+getAtom (Neg a) = a+getAtom (Lit a) = a++instance Show Literal where+  show (Lit p) = show p+  show (Neg p) = "~" ++ show p++data Atom = Atom Name [Term]+                 deriving (Eq, Ord)++-- |Returns a new atom+atom = Atom++-- |Return the terms that are arguments to the predicate of the input atom+atomArgs (Atom _ args) = args++-- |Return the name of the predicate of the input atom+predicateName (Atom n _) = n++instance Show Atom where+  show (Atom name args) = name ++ "[" ++ (L.intercalate ", " $ L.map show args) ++ "]"++data Term+  = Function Name [Term]+  | Variable Name+  | Integer Int+    deriving (Eq, Ord)++func = Function+var = Variable+intConst = Integer++-- |Returns True if the input term is a function with the give name,+-- and false otherwise+isFunctionWithName n (Function m _) = n == m+isFunctionWithName _ _ = False++-- |Return the name of the input variable,+-- throws error if input term is not a variable+varName (Variable n) = n++-- |Returns the input function's argument list,+-- throws error if input term is not a function+funcArgs (Function _ args) = args++-- |Returns the integer value of an Integer constant or an error+-- if the input is not an integer+intVal (Integer i) = i++instance Show Term where+  show (Integer val) = show val+  show (Variable name) = name+  show (Function name args) = name ++ "(" ++ (L.intercalate ", " $ L.map show args) ++ ")"

@@ -0,0 +1,31 @@+module FirstOrderTheory.Theory(+  FirstOrderTheory(..),+  PredicateDecl,+  FunctionDecl,+  predicateDecl,+  functionDecl) where++import Data.Set as S++import FirstOrderTheory.Syntax+import FirstOrderTheory.Utils++data PredicateDecl = PredicateDecl Name Arity [Sort]+                     deriving (Eq, Ord)++-- |Specify a new predicate declaration+predicateDecl = PredicateDecl++data FunctionDecl = FunctionDecl Name Arity [Sort] Sort+                    deriving (Eq, Ord)++-- |Specify a new function declaration+functionDecl = FunctionDecl++-- |Description of a decidable first order theory+class FirstOrderTheory t where+  theoryName :: t -> String+  sorts :: t -> Set Sort+  predicates :: t -> Set PredicateDecl+  functions :: t -> Set FunctionDecl+  decideSat :: t -> Set Literal -> (Bool, Set Literal)

@@ -0,0 +1,12 @@+module FirstOrderTheory.Utils(+  Name, Arity, Sort,+  sort) where++type Name = String+type Arity = Int++type Sort = String++-- |Make a new sort with the input name+sort :: String -> Sort+sort str = str