view kiss.pl @ 19:e1d3145cff7a lite-verifier

*** empty log message ***
author kono
date Thu, 30 Aug 2007 12:44:35 +0900
parents 1c57a78f1d98
children 07d6c4c5654b
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
 $Id$
*/

% :- dynamic st_variables/2.

set_input_var(L) :- abolish(input_variable_list,1),
	asserta(input_variable_list(L)).

kiss :-
	(variable_list(L);L=[]),
	(st_variables(In,_);In=[]),
	delete(L,In,Out),
	write('# '),write_kiss_var_list(In),write((->)),
		write_kiss_var_list(Out),nl,
%	write('.v '),length(L,Ll),write(Ll),nl,
	write('.p '),itl_transition(X),write(X),nl,
	write('.s '),itl_state_number(Y),write(Y),nl,
	write('.i '),length(In,Inl),write(Inl),nl,
	write('.o '),length(Out,Outl),write(Outl),nl,
	kiss(In,Out).

kiss(In,Out) :-
	state(S,Cond,D),
	write_kiss(S,Cond,D,In,Out),fail.
kiss(_,_) :- write('.e'),nl.

write_kiss_var_list([]):-!.
write_kiss_var_list([H|L]):-!,write(H),put(32),   % " "
	write_kiss_var_list(L).

write_kiss(S,Cond,D,In,Out) :-
       write_kiss_var(In,Cond),put(32),   % " "
       write_kiss_state(S),
       write_kiss_state(D),
       write_kiss_var(Out,Cond),nl,!.

write_kiss_state(0) :-	!,
       write(se),put(9).
write_kiss_state(true) :-!,
       write(st),put(9).
write_kiss_state(false) :-	!,
       write(sf),put(9).   
write_kiss_state(S) :-	!,
       write(s),write(S),put(9).

delete([],_,[]) :-!.
delete([H|X],L,Y) :- member(H,L),!,delete(X,L,Y).
delete([H|X],L,[H|Y]) :- delete(X,L,Y).

write_kiss_var([],_):-!.
write_kiss_var([H|L],Cond) :- member(H,Cond),!,write(1),
	write_kiss_var(L,Cond).
write_kiss_var([H|L],Cond) :- member(not(H),Cond),!,write(0),
	write_kiss_var(L,Cond).
write_kiss_var([_|L],Cond) :- write(-),
	write_kiss_var(L,Cond).

tgen :-
	(variable_list(L);L=[]),
	(st_variables(In,_);In=[]),
	delete(L,In,Out),
	write(('?-'(static(L)))),put(46),nl,  % "."
	make_print_state(L,L1,LL),
	write((print_state :- L1,write(LL))),put(46),nl,
	tgen(In,Out).
tgen(In,Out) :-
	state(S,Cond,D),
	write_tclause(S,Cond,D,In,Out),fail.
tgen(_,_).

make_print_state([H],(H1= *(H)),((H) = H1)):-!.
make_print_state([H|L],((H1= *(H)),L1),(((H) = H1),LL1)):-
	make_print_state(L,L1,LL1).

write_tclause(S,[empty|Cond],true,In,Out) :-!,
	write_tstate(S), write(' :- '), % write(empty),put(44), % ","
	write_tcondition(In,Out,Cond),
	write(true), put(46),nl.  % true, empty or false  "."
write_tclause(_S,[empty|_Cond],false,_In,_Out) :-!.
%write_tclause(S,[empty|Cond],false,In,_Out) :-!,
%	write_tstate(S), write(' :- '),write(empty),put(44),
%	write_tcondition(In,[],Cond), % don't touch output
%	write(fail),put(46),nl.  % true, empty or false
write_tclause(S,[empty|Cond],D,In,Out) :-!,
	write_tstate(S), write(' :- '), % write(empty),put(44), % ","
	write_tcondition(In,Out,Cond),
	write_tstate(D),put(46),nl.  % true, empty or false  "."
write_tclause(_S,[more|_Cond],false,_In,_Out) :-!.
%write_tclause(S,[more|Cond],false,In,_Out) :-!,
%	write_tstate(S), write(' :- '),write(more),put(44),  % ","
%	write_tcondition(In,[],Cond),  % don't touch output
%	write(fail), put(46),nl.
write_tclause(S,[more|Cond],true,In,Out) :-!,
	write_tstate(S), write(' :- '),write(more),put(44),
	write_tcondition(In,Out,Cond),
	write(true), put(46),nl.
write_tclause(S,[more|Cond],D,In,Out) :-!,
	write_tstate(S), write(' :- '),write(more),put(44),
	write_tcondition(In,Out,Cond),
	write((@)),write_tstate(D),
	put(46),nl.

write_tcondition(In,Out,Cond) :-
	write_tvar(In,Cond,'= '),
	write_tvar(Out,Cond,':= ').
write_tvar([],_,_):-!.
write_tvar([H|L],Cond,Eq) :- member(H,Cond),!,
	write(*(H)),write(Eq),write(1),put(44),
	write_tvar(L,Cond,Eq).
write_tvar([H|L],Cond,Eq) :- member(not(H),Cond),!,
	write(*(H)),write(Eq),write(0),put(44),
	write_tvar(L,Cond,Eq).
write_tvar([_|L],Cond,Eq) :- 
	write_tvar(L,Cond,Eq).

write_tstate(0) :-	!,
       write(empty).
write_tstate(true) :-!,
       write(true).
write_tstate(false) :-	!,
       write(fail).
write_tstate(S) :-	!,
       write(s),write(S).

/*

KISS2 format

.i 4 
.o 2 
.p 60 
.s 10
--01 st0 st0 00

*/

read_kiss(File) :-
	read_kiss(File,empty).

read_kiss(File,Emode) :-
	see(File),
	get0(C), read_kiss_header(C,C1,IL,OL),
	nonvar(IL),nonvar(OL),
	make_vars(IL,"i",0,In),
	make_vars(OL,"o",0,Out),
	init_read_kiss(In,Out,IL,OL),
	read_kiss_body(C1,In,Out,Emode),
	seen.
read_kiss(_,_) :- write('Error'),nl,seen.

make_vars(N,_,_,[]) :- N =< 0,!.
make_vars(N,V,M,[H|L]) :-!,
	name(M,LM),append(V,LM,LH), name(H,LH),
	N1 is N-1,M1 is M+1,
	make_vars(N1,V,M1,L).

read_kiss(File,In,Out,Emode) :-
	see(File),
	read_kiss(In,Out,Emode),!,
	seen.
read_kiss(_,_,_,_) :- write('Error'),nl,seen.

read_kiss(In,Out,Emode) :-
	get0(C), read_kiss_header(C,C1,IL1,OL1),
	((var(In),make_vars(IL1,"i",0,In));true),
	((var(Out),make_vars(OL1,"o",0,Out));true),
	init_read_kiss(In,Out,IL,OL),
	check_vars(IL,OL,IL1,OL1),
	read_kiss_body(C1,In,Out,Emode).

init_read_kiss(In,Out,IL,OL) :-
	abolish(st_variables,2),
	abolish(st,3),
	assert(st_variables(In,Out)),
	assert(st(true,true,true)),
	length(In,IL),length(Out,OL).

check_vars(IL,0,IL,_) :-!.  % ignore output
check_vars(IL,OL,IL,OL) :-!.
check_vars(IL,_OL,IL1,_OL1) :-IL=\=IL1,
	write('Input variable number is wrong'),nl,fail.
check_vars(_IL,OL,_IL1,OL1) :-OL=\=OL1,
	write('Output variable number is wrong'),nl,fail.

read_kiss_header(C,C2,IL,OL) :-[C]=".",!, get(C0),
	read_kiss_header1(C0,C1,IL,OL),
	read_kiss_header(C1,C2,IL,OL).
read_kiss_header(C,C,_,_) :-([C]="0";[C]="1";[C]="-"),!.
read_kiss_header(C,C1,IL,OL) :- 
	skip_line(C,C0),
	read_kiss_header(C0,C1,IL,OL).

read_kiss_header1(C,C2,IL,_OL):-[C]="i",!,get(C0),
    read_number(C0,C1,IL),skip_line(C1,C2).
read_kiss_header1(C,C2,_IL,OL):-[C]="o",!,get(C0),
    read_number(C0,C1,OL),skip_line(C1,C2).
read_kiss_header1(C,C1,_,_):-[C]="p",!,
    skip_line(C,C1).
read_kiss_header1(C,C1,_,_):-[C]="s",!,
    skip_line(C,C1).
read_kiss_header1(C,C1,_,_):-
    skip_line(C,C1).

read_kiss_body(-1,_,_,_) :-!.
read_kiss_body(C,In,Out,Emode) :-
	([C]="0";[C]="1";[C]="-"),!,
	read_kiss_var(In ,C, _, In1),get(C1),
	read_kiss_state(C1,C2,S),
	read_kiss_state(C2,C3,D),
	read_kiss_var(Out,C3,C4,Out1),
	assert_state(Emode,S,In1,Out1,D),
	skip_line(C4,C5),
	read_kiss_body(C5,In,Out,Emode).
read_kiss_body(C,In,Out,Emode) :-
	skip_line(C,C1),
	read_kiss_body(C1,In,Out,Emode).

assert_state(_,S,In1,Out1,D) :-
	st(S,_,_),!,
	assertz(st(S,(In1,Out1),D)).
assert_state(empty,S,In1,Out1,D) :-!,
	assertz(st(S,empty,empty)),
	assertz(st(S,(In1,Out1),D)).
assert_state(_,S,In1,Out1,D) :-
	assertz(st(S,(In1,Out1),D)).

read_kiss_var([],C, C, true):-!.
read_kiss_var([_],C, C1, true):- [C]="-",!,get0(C1).
read_kiss_var([H],C, C1, not(H)):- [C]="0",!,get0(C1).
read_kiss_var([H],C, C1, H):- [C]="1",!,get0(C1).
read_kiss_var([H|L],C, C1, O):-
	kiss_var([C],H,O,O1),!,get0(C0),
	read_kiss_var(L,C0,C1,O1).
read_kiss_var(L,_, C1, O):- get0(C),
	read_kiss_var(L,C, C1, O).

kiss_var("-",_,O,O).
kiss_var("0",H,(not(H),O),O).
kiss_var("1",H,(H,O),O).

read_number(C,C1,N) :- read_number1(C,C1,NL),name(N,NL).
read_number(_,_,0) :- write('A number is expected.'),nl.
read_number1(C,C1,[C|L]) :- 
	([C]="0"; [C]="1"; [C]="2"; [C]="3"; [C]="4"; [C]="5";
	 [C]="6"; [C]="7"; [C]="8"; [C]="9"),!,get0(C2),
	 read_number1(C2,C1,L).
read_number1(C,C,[]).

read_kiss_state(C,C1,N) :- read_kiss_state1(C,C1,NL),name(N,NL).
read_kiss_state(_,_,0) :- write('A kiss_state is expected.'),nl.
read_kiss_state1(C,C1,[C|L]) :- 
	 [Z]="0",C>=Z, !,
	 get0(C2),
	 read_kiss_state1(C2,C1,L).
read_kiss_state1(C,C1,[]) :-
	skip_space(C,C1),!.

skip_space(C,C1):- ([C]=" ";[C]="	"),!,
	get(C0),skip_space(C0,C1).
skip_space(C,C).

skip_line(10,C) :- !,get0(C).
skip_line(-1,C) :- !,C= -1.
skip_line(_,C) :- get0(C0),skip_line(C0,C).

/* end */