Mercurial > hg > Applications > Lite
view itlstd.pl @ 22:29cf617f49db default tip
newer CVS version
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 22 Apr 2016 16:47:13 +0900 |
parents | 07d6c4c5654b |
children |
line wrap: on
line source
/* Copyright (C) 1991, Shinji Kono, Sony Computer Science Laboratory, Inc. The University, Newcastle upton Tyne Everyone is permitted to copy and distribute verbatim copies of this license, but changing it is not allowed. You can also use this wording to make the terms for other programs. send your comments to kono@csl.sony.co.jp $Header: /Users/kono/src/CVS/Lite/itlstd.pl,v 1.3 2007/08/30 05:16:36 kono Exp $ */ % ITL standarization % % Wed Jun 19 12:11:29 BST 1991 % % a standard form of ITL, based on subterm classification % % P = \Sum Pn & Px % Q = \Sum Qn & Qx % P & Q = empty,Pn,Qn ; ( Px = Qx = true) % more,Pn,Qn & Qx; ( Px = true ) % more,Pn,(Px & Q) % subterm_init :- r_abolish(sb,3), asserta((sb(-1,[],[]))), r_abolish(sbn,1), asserta(sbn(0)), r_abolish(itl_state,2), assertz(itl_state((['->'([],false)]),false)), assertz(itl_state((['->'([],true)]),0)),!. std_check(I,J,N) :- sb(N,I,J),!. std_check(I,J,N1) :- retract(sbn(N)),N1 is N+1,asserta(sbn(N1)), assertz(sb(N1,I,J)),!. itlstd(P,List) :- setof(N,subterm(P,N),List),!. subterm(P,'->'(C,T)) :- subterm(P,T,[],C0), sortC(C0,C). % bubble sort sortC([],[]). sortC([H|T],[Min|Y]):- min(T,H,Min,Rest), sortC(Rest,Y). min([],X,X,[]). min([H|T],X,Y,[H|S]) :- ord(H,X),!,min(T,X,Y,S). min([H|T],X,Y,[X|S]) :- min(T,H,Y,S). ord(not(X),not(Y)) :- !,X @> Y. ord(X,not(Y)) :- !,X @> Y. ord(not(X),Y) :- !,X @> Y. ord(X,Y) :- !,X @> Y. subterm(true,true,C,C):-!. subterm(false,false,C,C):-!. subterm(P,V,C,C1) :- atomic(P),!, local(V,P,C,C1). subterm(up(P),V,C,C1) :- !, local(V,up(P),C,C1). subterm(down(P),V,C,C1) :- !, local(V,down(P),C,C1). subterm((false&_),false,C,C) :-!. subterm((_&false),false,C,C) :-!. subterm((P&Q),V,C,C1) :-!, std_check(P,Q,N),local(V,N,C,C1). subterm(@(Q),V,C,C1) :-!, std_check(@(Q),'$$$',N),local(V,N,C,C1). subterm(^(Q),V,C,C1) :-!, std_check(^(Q),'$$$',N),local(V,N,C,C1). subterm((P,Q),V,C,C1) :-!, subterm(P,PV,C,C0),subterm(Q,QV,C0,C1), and(PV,QV,V). subterm((P;Q),V,C,C1) :-!, subterm(P,PV,C,C0),subterm(Q,QV,C0,C1), or(PV,QV,V). subterm(not(P),V,C,C1) :-!, subterm(P,PV,C,C1),negate(PV,V). % end %