-
Notifications
You must be signed in to change notification settings - Fork 0
/
axiom.hs
31 lines (24 loc) · 852 Bytes
/
axiom.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
module Axiom (Axiom(..), buildAxiom) where
import Formula
import Assignment
data Axiom = Axiom {
constructor :: (Int -> Formula),
airity :: Int
}
instance Show Axiom where
show (Axiom construct _) = show $ construct 0
combineLists :: (Ord a) => [a] -> [a] -> [a]
combineLists [] x = x
combineLists x [] = x
combineLists (a:ax) (b:bx)
| a < b = a : combineLists ax (b:bx)
| a == b = a : combineLists ax bx
| otherwise = b : combineLists (a:ax) bx
vSet :: Formula -> [Int]
vSet (Atom _) = []
vSet (Neg form) = vSet form
vSet (Variable n) = [n]
vSet (If form1 form2) = combineLists (vSet form1) (vSet form2)
buildAxiom :: Formula -> Axiom
buildAxiom form = Axiom (\x -> apply [ SubAssignment var (Variable $ x + index) | (index, var) <- zip [0..] variables ] form) (length variables)
where variables = vSet form