|
2
|
1 %
|
|
|
2 /*
|
|
|
3 Copyright (C) 1991, Shinji Kono, Sony Computer Science Laboratory, Inc.
|
|
|
4 The University, Newcastle upton Tyne
|
|
|
5
|
|
|
6 Everyone is permitted to copy and distribute verbatim copies
|
|
|
7 of this license, but changing it is not allowed. You can also
|
|
|
8 use this wording to make the terms for other programs.
|
|
|
9
|
|
|
10 send your comments to kono@csl.sony.co.jp
|
|
|
11 $Id$
|
|
|
12 */
|
|
|
13 % ITL subterm standarization with BDT
|
|
|
14 %
|
|
|
15 % Fri Jun 21 10:32:58 BST 1991
|
|
|
16 %
|
|
|
17 % a standard form of ITL, based on subterm classification
|
|
|
18 %
|
|
|
19 %
|
|
|
20 subterm_init :-
|
|
|
21 abolish(sb,2),
|
|
|
22 asserta((sb([],-1))),
|
|
|
23 abolish(sbn,1),
|
|
|
24 asserta(sbn(0)).
|
|
|
25
|
|
|
26 std_check(I,J) :-
|
|
|
27 sb(I,J),!.
|
|
|
28 std_check(I,N1) :-
|
|
|
29 retract(sbn(N)),N1 is N+1,asserta(sbn(N1)),
|
|
|
30 assertz(sb(I,N1)),!.
|
|
|
31
|
|
|
32 itlstd(P,List) :-
|
|
|
33 sbdt(P,List).
|
|
|
34
|
|
|
35 % BDT classification of subterm
|
|
|
36
|
|
|
37 sbdt(true,true):-!.
|
|
|
38 sbdt(false,false):-!.
|
|
|
39 sbdt(P,F) :- atomic(P),!,F= ?(P,true,false).
|
|
|
40 sbdt(?(C,T,F),?(C,T,F)) :- !.
|
|
|
41 sbdt(not(P),F) :- !,sbdt(P,F0),sbdt_not(F0,F),!.
|
|
|
42 sbdt_not(true,false).
|
|
|
43 sbdt_not(false,true).
|
|
|
44 sbdt_not(F,?(H,A1,B1)):-
|
|
|
45 arg(1,F,H),arg(2,F,A),arg(3,F,B),
|
|
|
46 sbdt_not(A,A1),sbdt_not(B,B1).
|
|
|
47 sbdt((P,Q),F) :- !,
|
|
|
48 sbdt(P,P0),sbdt(Q,Q0),
|
|
|
49 sbdt_and(P0,Q0,F),!.
|
|
|
50 sbdt_and(false,_,false):-!.
|
|
|
51 sbdt_and(_,false,false):-!.
|
|
|
52 sbdt_and(true,T,T):-!.
|
|
|
53 sbdt_and(T,true,T):-!.
|
|
|
54 sbdt_and(P,Q,R) :-!,
|
|
|
55 arg(1,P,PF),arg(1,Q,QF),
|
|
|
56 sbdt_and(PF,QF,P,Q,R).
|
|
|
57 sbdt_and(PF,QF,P,Q,R):-PF @< QF,!,
|
|
|
58 sbdt_and(QF,PF,Q,P,R).
|
|
|
59 sbdt_and(PF,QF,P,Q,?(QF,R0,R1)):-PF @> QF,!,
|
|
|
60 arg(2,Q,Q0),arg(3,Q,Q1),
|
|
|
61 sbdt_and(Q0,P,R0),
|
|
|
62 sbdt_and(Q1,P,R1).
|
|
|
63 sbdt_and(PF,PF,P,Q,?(PF,R0,R1)):-
|
|
|
64 arg(2,P,P0),arg(3,P,P1),
|
|
|
65 arg(2,Q,Q0),arg(3,Q,Q1),
|
|
|
66 sbdt_and(P0,Q0,R0),
|
|
|
67 sbdt_and(P1,Q1,R1).
|
|
|
68 sbdt((P;Q),F) :- !,
|
|
|
69 sbdt(P,P0),sbdt(Q,Q0),
|
|
|
70 sbdt_or(P0,Q0,F),!.
|
|
|
71 sbdt_or(true,_,true):-!.
|
|
|
72 sbdt_or(_,true,true):-!.
|
|
|
73 sbdt_or(false,T,T):-!.
|
|
|
74 sbdt_or(T,false,T):-!.
|
|
|
75 sbdt_or(P,Q,R) :-!,
|
|
|
76 arg(1,P,PF),arg(1,Q,QF),
|
|
|
77 sbdt_or(PF,QF,P,Q,R).
|
|
|
78 sbdt_or(PF,QF,P,Q,R):-PF @< QF,!,
|
|
|
79 sbdt_or(QF,PF,Q,P,R).
|
|
|
80 sbdt_or(PF,QF,P,Q,?(QF,R0,R1)):-PF @> QF,!,
|
|
|
81 arg(2,Q,Q0),arg(3,Q,Q1),
|
|
|
82 sbdt_or(Q0,P,R0),
|
|
|
83 sbdt_or(Q1,P,R1).
|
|
|
84 sbdt_or(PF,PF,P,Q,?(PF,R0,R1)):-
|
|
|
85 arg(2,P,P0),arg(3,P,P1),
|
|
|
86 arg(2,Q,Q0),arg(3,Q,Q1),
|
|
|
87 sbdt_or(P0,Q0,R0),
|
|
|
88 sbdt_or(P1,Q1,R1).
|
|
|
89 sbdt((P&Q), ?(N,true,false)) :-!,
|
|
|
90 sbdt(P,P1),sbdt(Q,Q1), % projection touch later part of chop
|
|
|
91 std_check((P1&Q1),N).
|
|
|
92 %sbdt(@(Q), ?(N,true,false)) :-!, % Don't check next part now
|
|
|
93 % std_check(@(Q),N). % this makes everything very slow
|
|
|
94 %sbdt(*(Q), ?(N,true,false)) :-!, % Don't check next part now
|
|
|
95 % std_check(*(Q),N). % this makes everything very slow
|
|
|
96 %sbdt(free_fin(Q), ?(N,true,false)) :-!,
|
|
|
97 % std_check(free_fin(Q),N).
|
|
|
98 % bottom up development is effective for quantifier
|
|
|
99 sbdt(exists(P,Q), ?(N,true,false)) :-!,
|
|
|
100 sbdt(Q,QF),
|
|
|
101 std_check(exists(P,QF),N).
|
|
|
102 sbdt(proj(P,Q), ?(N,true,false)) :-!,
|
|
|
103 sbdt(Q,QF), % P part is fixed
|
|
|
104 std_check(proj(P,QF),N).
|
|
|
105 sbdt(prefix(P), ?(N,true,false)) :-!,
|
|
|
106 sbdt(P,PF), % P part is fixed
|
|
|
107 std_check(prefix(PF),N).
|
|
|
108 % Simple Functor including Regular variable and state
|
|
|
109 sbdt(Func,F) :- functor(Func,_,1),!,F= ?(N,true,false),
|
|
|
110 std_check(Func,N).
|
|
|
111 sbdt(Func,F) :- functor(Func,_,2),!,F= ?(N,true,false),
|
|
|
112 std_check(Func,N).
|
|
|
113 sbdt(Def,true) :-
|
|
|
114 write('bdtstd error: '),write(Def),nl.
|
|
|
115
|
|
|
116 sbterm :-
|
|
|
117 listing(sb/2),listing(itl_state/2).
|
|
|
118
|
|
|
119
|
|
|
120 bdt2itl(B,F) :- number(B),!,sb(F0,B),
|
|
|
121 bdt2itl(F0,F).
|
|
|
122 bdt2itl(?(IF,THEN,ELSE),F) :-
|
|
|
123 bdt2itl(IF,IF0),bdt2itl(THEN,THEN0),bdt2itl(ELSE,ELSE0),
|
|
|
124 bdt2itl_opt(IF0,THEN0,ELSE0,F).
|
|
|
125 % little more readable representation
|
|
|
126 bdt2itl_opt(IF,true,false,IF) :- !.
|
|
|
127 bdt2itl_opt(IF,false,true,not(IF)) :- !.
|
|
|
128 bdt2itl_opt(IF,true,ELSE,(IF;ELSE)) :- !.
|
|
|
129 bdt2itl_opt(IF,THEN,false,(IF,THEN)) :- !.
|
|
|
130 bdt2itl_opt(IF,false,ELSE,(not(IF);ELSE)) :- !.
|
|
|
131 bdt2itl_opt(IF,THEN,true,(not(IF),THEN)) :- !.
|
|
|
132 bdt2itl_opt(IF,THEN,ELSE,?(IF,THEN,ELSE)) :- !.
|
|
|
133 bdt2itl(B,F) :- atom(B),!,F=B.
|
|
|
134 bdt2itl(B,F) :-
|
|
|
135 functor(B,H,N),functor(F,H,N),bdt2itl_subterm(N,N,B,F).
|
|
|
136 bdt2itl_subterm(0,_,_,_) :- !.
|
|
|
137 bdt2itl_subterm(N,N1,F,F0) :-
|
|
|
138 N0 is N-1,
|
|
|
139 arg(N,F,A),arg(N,F0,A0),
|
|
|
140 bdt2itl(A,A0),bdt2itl_subterm(N0,N1,F,F0).
|
|
|
141
|
|
|
142 % BDT end %
|
