1		% (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(schemavars,[schema_vars/3,schema_vars_decl/3]).
6
7		:- use_module(library(lists)).
8
9		:- use_module(probsrc(tools)).
10
11		:- use_module(z_tools).
12		:- use_module(zenvironment).
13
14		:- use_module(probsrc(module_information)).
15		:- module_info(group,proz).
16		:- module_info(description,'This module contains code to extract the variables declared and visible in a schema declaration').
17
18		%********************************************************************************
19		% extract vars from declaration
20
21		schema_vars(sref(Name,Deco,_,Renamings),Env,Vars) :-
22		zlookup_schema(Env,Name,_,Expr),
23		schema_vars(Expr,Env,Vars1),
24		decorate_vars(Vars1,Deco,DVars),
25		rename(DVars,Renamings,Vars).
26
27		schema_vars(sand(A,B),Env,Vars) :- schema_vars_logbin(A,B,Env,Vars).
28		schema_vars(sor(A,B),Env,Vars) :- schema_vars_logbin(A,B,Env,Vars).
29		schema_vars(simplies(A,B),Env,Vars) :- schema_vars_logbin(A,B,Env,Vars).
30		schema_vars(sequiv(A,B),Env,Vars) :- schema_vars_logbin(A,B,Env,Vars).
31		schema_vars(snot(A),Env,Vars) :- schema_vars(A,Env,Vars).
32		schema_vars(sforall(B,S),Env,Vars) :- schema_vars_quantifier(B,S,Env,Vars).
33		schema_vars(sexists(B,S),Env,Vars) :- schema_vars_quantifier(B,S,Env,Vars).
34		schema_vars(sexists1(B,S),Env,Vars) :- schema_vars_quantifier(B,S,Env,Vars).
35		schema_vars(hide(S,Hide),Env,Vars) :-
36		schema_vars(S,Env,All),remove_all(All,Hide,Vars).
37
38		schema_vars(fatsemi(A,B),Env,Vars) :-
39		schema_vars(A,Env,AVars),
40		findall(name(Name,'\''),member(name(Name,'\''),AVars),InterA),
41		remove_all(AVars,InterA,Aall),
42
43		schema_vars(B,Env,BVars),
44		findall(name(Name,''),member(name(Name,''),BVars),InterB),
45		remove_all(BVars,InterB,Ball),
46
47		append_not_duplicate(Aall,Ball,Vars).
48		schema_vars(project(_,B),Env,Vars) :- schema_vars(B,Env,Vars).
49		schema_vars(pre(Schema),Env,Vars) :-
50		schema_vars(Schema,Env,AllVars),
51		findall(name(Name,Deco),
52		(member(name(Name,Deco),AllVars), \+ member(Deco,['\'','!'])),
53		Vars).
54		schema_vars(pipe(A,B),Env,Vars) :-
55		schema_vars(A,Env,AVars),
56		schema_vars(B,Env,BVars),
57		findall(name(Name,'!'),
58		(member(name(Name,'!'),AVars),member(name(Name,'?'),BVars)),
59		Out),
60		findall(name(Name,'?'),member(name(Name,'!'),Out),In),
61		remove_all(AVars,Out,AwoO),
62		remove_all(BVars,In,BwoI),
63		append_not_duplicate(AwoO,BwoI,Vars).
64
65		schema_vars(text(Body),Env,Vars) :- schema_vars(Body,Env,Vars).
66		schema_vars(body(Decl,_),Env,Vars) :- schema_vars_decl(Decl,Env,Vars).
67
68		% Helper predicates
69
70		% vars of a schema binary logical expression
71		schema_vars_logbin(A,B,Env,Vars) :-
72		schema_vars(A,Env,AVars),
73		schema_vars(B,Env,BVars),
74		append_not_duplicate(AVars,BVars,Vars).
75
76		% vars of a schema quantifier expression
77		schema_vars_quantifier(Schema,Body,Env,Vars) :-
78		schema_vars(Body,Env,Hide),
79		schema_vars(hide(Schema,Hide),Env,Vars).
80
81		% vars of the declaration part of a body
82		schema_vars_decl(Decls,Env,Vars) :-
83		maplist(schema_vars_decl2(Env),Decls,LVars),
84		append(LVars,Vars).
85		schema_vars_decl2(_,decl(Vars,_),Vars).
86		schema_vars_decl2(Env,sdecl(Sexpr),Vars) :- schema_vars(Sexpr,Env,Vars).
87
88		% renames variables
89		rename([],_,[]).
90		rename([NameA|Rest],Renamings,[NameB|RenamedRest]) :-
91		(member(rename(NameB,NameA),Renamings) ->
92		true;
93		NameA = NameB),
94		rename(Rest,Renamings,RenamedRest).