summaryrefslogtreecommitdiff
path: root/src/TermNetTest.hs
blob: 57eb06f65bfc4db32e430f26bbcc65008cbb4cf3 (plain)
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
import Library.Theorem
import Library.Term
import qualified Library.TermNet as Net
import Test.DataTypes
import qualified Data.Set as Set
import Data.List



main = do
    let thm1 = Theorem (Set.empty) stdConstTerm
        thm2 = Theorem (Set.empty) (stdVarTerm "b")
        thm3 = Theorem (Set.empty) (stdVarTerm "c")
        thm4 = Theorem (Set.empty) (stdAbsTerm "h")

        net1 = Net.addThm Net.empty thm1 0
        net2 = Net.addThm net1 thm2 1
        net3 = Net.addThm net2 thm3 2
        net4 = Net.addThm net3 thm4 3

        match = Net.matchThm net4 thm4
 

    putStrLn (show net4)
    putStrLn ""
    putStrLn (show match)