Mercurial > hg > Applications > Lite

comparison bdtstd.pl @ 2:1c57a78f1d98

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial revision
author kono
date Thu, 18 Jan 2001 23:27:24 +0900
parents
children 07d6c4c5654b
comparison
equal deleted inserted replaced
1:683efd6f9a81 2:1c57a78f1d98
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 %