|
9
|
1 module example1 where
|
|
|
2 open import Data.List hiding (all ; and ; or )
|
|
|
3 open import Data.Maybe
|
|
15
|
4 open import Data.Bool hiding ( not ; _∧_ ; _∨_ )
|
|
9
|
5
|
|
10
|
6 data Const : Set where
|
|
|
7 a : Const
|
|
|
8 b : Const
|
|
|
9 c : Const
|
|
9
|
10
|
|
10
|
11 data Var : Set where
|
|
|
12 X : Var
|
|
|
13 Y : Var
|
|
|
14 Z : Var
|
|
9
|
15
|
|
10
|
16 data Func : Set where
|
|
|
17 f : Func
|
|
|
18 g : Func
|
|
|
19 h : Func
|
|
9
|
20
|
|
10
|
21 data Pred : Set where
|
|
|
22 p : Pred
|
|
|
23 q : Pred
|
|
|
24 r : Pred
|
|
9
|
25
|
|
10
|
26 open import Logic Const Func Var Pred
|
|
|
27
|
|
|
28 ex1 : Statement
|
|
15
|
29 ex1 = ¬ ( pred q ∧ ( All X => predx p ( func f (var X) ) ))
|
|
9
|
30
|
|
10
|
31 subst-expr : Expr → Var → Expr → Expr
|
|
|
32 subst-expr (var X) X v = v
|
|
|
33 subst-expr (var Y) Y v = v
|
|
|
34 subst-expr (var Z) Z v = v
|
|
9
|
35 subst-expr (func f₁ e) xv v = func f₁ ( subst-expr e xv v )
|
|
10
|
36 subst-expr (e , e1) xv v = ( subst-expr e xv v ) , ( subst-expr e1 xv v )
|
|
|
37 subst-expr x _ v = x
|
|
9
|
38
|
|
10
|
39 amap : (px : Pred ) → Bool
|
|
|
40 amap q = true
|
|
9
|
41 amap px = false
|
|
10
|
42 pmap : (px : Pred ) → Expr → Bool
|
|
|
43 pmap p (const c) = true
|
|
|
44 pmap p (func d (const a) , const b ) = true
|
|
9
|
45 pmap px _ = false
|
|
|
46
|
|
|
47 -- we only try simple constant, it may contains arbitrary complex functional value
|
|
|
48 all0 : List Expr
|
|
10
|
49 all0 = const a ∷ const b ∷ const c ∷ []
|
|
9
|
50
|
|
18
|
51 test3 : Bool
|
|
|
52 test3 = M amap pmap all0 subst-expr ( Exist X => predx p (var X) )
|
|
9
|
53
|
|
15
|
54 open import clausal Const Func Var Pred
|
|
|
55
|
|
18
|
56 test4 : List Clause
|
|
|
57 test4 = translate ( Exist X => predx p (var X) ) (c ∷ []) (h ∷ []) subst-expr
|
|
15
|
58
|
