1		% (c) 2009-2019 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(kernel_z, [compaction/3,bag_items/3]).
6		% The module for Z specific kernel operations
7
8		:- use_module(library(avl)).
9
10		%:- use_module(debug).
11		:- use_module(self_check).
12		%:- use_module(tools).
13		%:- use_module(error_manager).
14		:- use_module(kernel_objects).
15		:- use_module(kernel_waitflags,[add_wd_error/3,assert_must_abort_wf/2]).
16		:- use_module(custom_explicit_sets,[try_expand_custom_set/2]).
17
18		:- use_module(module_information,[module_info/2]).
19		:- module_info(group,proz).
20		:- module_info(description,'This module provides operations that are special to the Z notation (sequence compaction, items of a bag).').
21
22
23		/* The compaction of a set integer -> X is the sequence where the "gaps are filled up".
24		E.g. compaction of {(1,a),(4,b),(8,c)} is {(1,a),(2,b),(3,c)}. */
25
26		:- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_z:compaction([(int(1),int(11)), (int(4),int(44))],[(int(1),int(11)), (int(2),int(44))],WF),WF)).
27		:- assert_must_succeed(kernel_z:compaction([(int(1),int(11)), (int(4),int(44))],[(int(2),int(44)), (int(1),int(11))],_)).
28		:- assert_must_succeed((kernel_z:compaction(S,R,_),
29		S=[(int(5),int(55)),(int(1),int(11)), (int(4),int(44))], kernel_objects:equal_object(R,[(int(3),int(55)),(int(1),int(11)), (int(2),int(44))]))).
30		:- assert_must_abort_wf(kernel_z:compaction([(int(1),int(11)), (int(4),int(44)), (int(1),int(22))],_,WF),WF).
31
32		:- block compaction(-,?,?).
33		compaction(Sequence,Value,WF) :-
34		try_expand_custom_set(Sequence,ESeq),
35		try_expand_custom_set(Value,EValue),
36		compaction2(ESeq,EValue,WF).
37
38		compaction2(Relation,Sequence,WF) :-
39		empty_avl(Empty),
40		collect_sorted_values(Relation,Empty,SortedValues,WF),
41		create_sequence(SortedValues,Sequence1),
42		equal_object(Sequence1,Sequence).
43
44		:- block collect_sorted_values(-,?,?,?).
45		collect_sorted_values([],Avl,Avl,_WF).
46		collect_sorted_values([(int(Pos),Element)|Rest],In,Out,WF) :-
47		add_value(Pos,Element,Rest,In,Out,WF).
48
49		:- block add_value(-,?,?,?,?,?).
50		add_value(Pos,Element,Rest,In,Out,WF) :-
51		( avl_fetch(Pos,In,Old) ->
52		not_equal_object_wf(Old,Element,WF),
53		add_wd_error('Input for squash is not a function',
54		b(value([(int(Pos),Old),(int(Pos),Element)]),seq(any),[]),WF),
55		Out=failure
56		; otherwise ->
57		avl_store(Pos,In,Element,Inter),
58		collect_sorted_values(Rest,Inter,Out,WF)).
59
60		:- block create_sequence(-,?).
61		create_sequence(failure,_Sequence) :- !.
62		create_sequence(SortedValues,Sequence) :-
63		create_sequence2(SortedValues,1,Sequence1),
64		equal_object(Sequence1,Sequence).
65		create_sequence2(SortedValues,Pos,Sequence) :-
66		( avl_del_min(SortedValues, _Min, Element, Rest) ->
67		Sequence = [(int(Pos),Element)|RestSequence],
68		NextPos is Pos+1,
69		create_sequence2(Rest,NextPos,RestSequence)
70		; otherwise ->
71		Sequence = []).
72
73		:- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_z:bag_items([(int(1),int(11)), (int(2),int(22)), (int(3),int(11))],[(int(11),int(2)), (int(22),int(1))],WF),WF)).
74		:- assert_must_abort_wf(bag_items([(int(1),int(11)), (int(2),int(22)), (int(4),int(11))],_,WF),WF).
75		:- assert_must_abort_wf(bag_items([(int(1),int(11)), (int(2),int(22)), (int(1),int(11))],_,WF),WF).
76
77		% This predicate computes the effect of the items function in Z.
78		% It is written for basic bag support without performance in mind.
79		:- block bag_items(-,?,?).
80		bag_items(Sequence,Bag,WF) :-
81		try_expand_custom_set(Sequence,ESequence),
82		empty_avl(Empty),
83		bag_items2(ESequence,[],Bag,Empty,WF).
84
85		:- block bag_items2(-,?,?,?,?).
86		bag_items2([],InBag,OutBag,Cnt,WF) :-
87		( check_count(Cnt) ->
88		equal_object_wf(InBag,OutBag,WF)
89		; otherwise ->
90		add_wd_error('Input for bag_times is not a sequence',[],WF)).
91		bag_items2([(int(Pos),Elem)|Rest],InBag,OutBag,InCnt,WF) :-
92		bag_items3(Pos,Elem,InBag,InterBag,InCnt,OutCnt,WF),
93		bag_items2(Rest,InterBag,OutBag,OutCnt,WF).
94		:- block bag_items3(-,?,?,?,?,?,?).
95		bag_items3(Pos,Elem,InBag,OutBag,InCnt,OutCnt,WF) :-
96		( avl_fetch(Pos,InCnt) ->
97		add_wd_error('Input for bag_times is not a function',[],WF)
98		; otherwise ->
99		avl_store(Pos,InCnt,true,OutCnt),
100		OldEntry = (Elem,int(OldCount)),
101		( exact_element_of(OldEntry, InBag) ->
102		remove_element_wf( OldEntry, InBag, InterBag,WF),!,
103		NewCount is OldCount+1
104		; otherwise ->
105		InterBag = InBag,
106		NewCount = 1),
107		add_element_wf( (Elem,int(NewCount)), InterBag, OutBag,WF)).
108
109		check_count(Cnt) :-
110		avl_domain(Cnt,Domain),
111		check_count2(Domain,1).
112		check_count2([],_).
113		check_count2([H|T],H) :- I is H+1,check_count2(T,I).