|
2
|
1 /*
|
|
|
2 Copyright (C) 1991, Shinji Kono, Sony Computer Science Laboratory, Inc.
|
|
|
3 The University, Newcastle upton Tyne
|
|
|
4
|
|
|
5 Everyone is permitted to copy and distribute verbatim copies
|
|
|
6 of this license, but changing it is not allowed. You can also
|
|
|
7 use this wording to make the terms for other programs.
|
|
|
8
|
|
|
9 send your comments to kono@csl.sony.co.jp
|
|
|
10 $Header$
|
|
|
11 */
|
|
|
12
|
|
|
13 % ITL standarization
|
|
|
14 %
|
|
|
15 % Wed Jun 19 12:11:29 BST 1991
|
|
|
16 %
|
|
|
17 % a standard form of ITL, based on subterm classification
|
|
|
18 %
|
|
|
19 % P = \Sum Pn & Px
|
|
|
20 % Q = \Sum Qn & Qx
|
|
|
21 % P & Q = empty,Pn,Qn ; ( Px = Qx = true)
|
|
|
22 % more,Pn,Qn & Qx; ( Px = true )
|
|
|
23 % more,Pn,(Px & Q)
|
|
|
24 %
|
|
|
25 subterm_init :-
|
|
20
|
26 r_abolish(sb,3),
|
|
2
|
27 asserta((sb(-1,[],[]))),
|
|
20
|
28 r_abolish(sbn,1),
|
|
2
|
29 asserta(sbn(0)),
|
|
20
|
30 r_abolish(itl_state,2),
|
|
|
31 assertz(itl_state((['->'([],false)]),false)),
|
|
|
32 assertz(itl_state((['->'([],true)]),0)),!.
|
|
2
|
33
|
|
|
34
|
|
|
35 std_check(I,J,N) :-
|
|
|
36 sb(N,I,J),!.
|
|
|
37 std_check(I,J,N1) :-
|
|
|
38 retract(sbn(N)),N1 is N+1,asserta(sbn(N1)),
|
|
|
39 assertz(sb(N1,I,J)),!.
|
|
|
40
|
|
|
41 itlstd(P,List) :-
|
|
|
42 setof(N,subterm(P,N),List),!.
|
|
|
43
|
|
20
|
44 subterm(P,'->'(C,T)) :-
|
|
2
|
45 subterm(P,T,[],C0),
|
|
|
46 sortC(C0,C).
|
|
|
47
|
|
|
48 % bubble sort
|
|
|
49 sortC([],[]).
|
|
|
50 sortC([H|T],[Min|Y]):-
|
|
|
51 min(T,H,Min,Rest),
|
|
|
52 sortC(Rest,Y).
|
|
|
53
|
|
|
54 min([],X,X,[]).
|
|
|
55 min([H|T],X,Y,[H|S]) :- ord(H,X),!,min(T,X,Y,S).
|
|
|
56 min([H|T],X,Y,[X|S]) :- min(T,H,Y,S).
|
|
|
57
|
|
|
58 ord(not(X),not(Y)) :- !,X @> Y.
|
|
|
59 ord(X,not(Y)) :- !,X @> Y.
|
|
|
60 ord(not(X),Y) :- !,X @> Y.
|
|
|
61 ord(X,Y) :- !,X @> Y.
|
|
|
62
|
|
|
63 subterm(true,true,C,C):-!.
|
|
|
64 subterm(false,false,C,C):-!.
|
|
|
65 subterm(P,V,C,C1) :- atomic(P),!, local(V,P,C,C1).
|
|
|
66 subterm(up(P),V,C,C1) :- !, local(V,up(P),C,C1).
|
|
|
67 subterm(down(P),V,C,C1) :- !, local(V,down(P),C,C1).
|
|
|
68 subterm((false&_),false,C,C) :-!.
|
|
|
69 subterm((_&false),false,C,C) :-!.
|
|
|
70 subterm((P&Q),V,C,C1) :-!,
|
|
|
71 std_check(P,Q,N),local(V,N,C,C1).
|
|
|
72 subterm(@(Q),V,C,C1) :-!,
|
|
|
73 std_check(@(Q),'$$$',N),local(V,N,C,C1).
|
|
|
74 subterm(^(Q),V,C,C1) :-!,
|
|
|
75 std_check(^(Q),'$$$',N),local(V,N,C,C1).
|
|
|
76 subterm((P,Q),V,C,C1) :-!,
|
|
|
77 subterm(P,PV,C,C0),subterm(Q,QV,C0,C1), and(PV,QV,V).
|
|
|
78 subterm((P;Q),V,C,C1) :-!,
|
|
|
79 subterm(P,PV,C,C0),subterm(Q,QV,C0,C1), or(PV,QV,V).
|
|
|
80 subterm(not(P),V,C,C1) :-!,
|
|
|
81 subterm(P,PV,C,C1),negate(PV,V).
|
|
|
82 % end %
|
