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). |