1		% (c) 2015-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		% CONTENTS OF FILE GENERATED BY prob_rule_compiler.pl
6
7		:- module(rewrite_rules_db,[rewrite_rule_mandatory/8, rewrite_rule_normalize/8]).
8
9		:- use_module(probsrc(module_information),[module_info/2]).
10		:- module_info(group,typechecker).
11		:- module_info(description,'Rewrite rules for transformations/simplifications on the AST.').
12
13		% rewrite_rule_mandatory(_, _, _, _, _, _, _, _) :- !,fail. % comment in to disable rewriting
14
15
16		% tree(S) = {tr|[]:dom(tr) & !(tt).(tt : dom(tr) => tt : seq(NATURAL1) & (tt /= [] => front(tt) : dom(tr) & (last(tt) > 1 => front(tt) <- last(tt) - 1 : dom(tr)))) & ran(tr) <: S}
17		rewrite_rule_mandatory(tree(A), set(set(couple(seq(integer),B))), C, [set(B)], comprehension_set([b(identifier(tr),set(couple(seq(integer),B)),[])],b(conjunct(b(conjunct(b(member(b(empty_sequence,seq(integer),[]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[]),b(forall([b(identifier(tt),seq(integer),[introduced_by(forall)])],b(member(b(identifier(tt),seq(integer),[introduced_by(forall)]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[]),b(conjunct(b(member(b(identifier(tt),seq(integer),[introduced_by(forall)]),b(seq(b(integer_set('NATURAL1'),set(integer),[])),set(seq(integer)),[])),pred,[]),b(implication(b(not_equal(b(identifier(tt),seq(integer),[introduced_by(forall)]),b(empty_sequence,seq(integer),[])),pred,[]),b(conjunct(b(member(b(front(b(identifier(tt),seq(integer),[introduced_by(forall)])),seq(integer),[contains_wd_condition]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[contains_wd_condition]),b(implication(b(greater(b(last(b(identifier(tt),seq(integer),[introduced_by(forall)])),integer,[contains_wd_condition]),b(integer(1),integer,[])),pred,[contains_wd_condition]),b(member(b(insert_tail(b(front(b(identifier(tt),seq(integer),[introduced_by(forall)])),seq(integer),[contains_wd_condition]),b(minus(b(last(b(identifier(tt),seq(integer),[introduced_by(forall)])),integer,[contains_wd_condition]),b(integer(1),integer,[])),integer,[contains_wd_condition])),seq(integer),[contains_wd_condition]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[used_ids([tr]),contains_wd_condition])),pred,[contains_wd_condition]),b(subset(b(range(b(identifier(tr),set(couple(seq(integer),B)),[])),set(B),[]),A),pred,[])),pred,[contains_wd_condition])), set(set(couple(seq(integer),B))), [was(tree),prob_annotation('SYMBOLIC')|C], tree).
18
19		% btree(S) = {tr|[]:dom(tr) & !(tt).(tt : dom(tr) => tt : seq(NATURAL1) & (tt /= [] => (front(tt) : dom(tr) & last(tt) : 1..2 & front(tt) <- (3-last(tt)) : dom(tr)))) & ran(tr) <: S}
20		rewrite_rule_mandatory(btree(A), set(set(couple(seq(integer),B))), C, [set(B)], comprehension_set([b(identifier(tr),set(couple(seq(integer),B)),[])],b(conjunct(b(conjunct(b(member(b(empty_sequence,seq(integer),[]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[]),b(forall([b(identifier(tt),seq(integer),[introduced_by(forall)])],b(member(b(identifier(tt),seq(integer),[introduced_by(forall)]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[]),b(conjunct(b(member(b(identifier(tt),seq(integer),[introduced_by(forall)]),b(seq(b(integer_set('NATURAL1'),set(integer),[])),set(seq(integer)),[])),pred,[]),b(implication(b(not_equal(b(identifier(tt),seq(integer),[introduced_by(forall)]),b(empty_sequence,seq(integer),[])),pred,[]),b(conjunct(b(conjunct(b(member(b(front(b(identifier(tt),seq(integer),[introduced_by(forall)])),seq(integer),[contains_wd_condition]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[contains_wd_condition]),b(member(b(last(b(identifier(tt),seq(integer),[introduced_by(forall)])),integer,[contains_wd_condition]),b(interval(b(integer(1),integer,[]),b(integer(2),integer,[])),set(integer),[])),pred,[contains_wd_condition])),pred,[contains_wd_condition]),b(member(b(insert_tail(b(front(b(identifier(tt),seq(integer),[introduced_by(forall)])),seq(integer),[contains_wd_condition]),b(minus(b(integer(3),integer,[]),b(last(b(identifier(tt),seq(integer),[introduced_by(forall)])),integer,[contains_wd_condition])),integer,[contains_wd_condition])),seq(integer),[contains_wd_condition]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[used_ids([tr]),contains_wd_condition])),pred,[contains_wd_condition]),b(subset(b(range(b(identifier(tr),set(couple(seq(integer),B)),[])),set(B),[]),A),pred,[])),pred,[contains_wd_condition])), set(set(couple(seq(integer),B))), [was(btree),prob_annotation('SYMBOLIC')|C], btree).
21
22		% top(S) = S([])
23		% Instantiated type of S to POW(seq(INTEGER)*__DEFERREDSET____19)
24		rewrite_rule_mandatory(top(A), B, C, [set(couple(seq(integer),B))], function(A,b(empty_sequence,seq(integer),[])), B, [was(top)|C], top).
25
26		% N:dom(T) => rank(T,N) = last(N)
27		% Instantiated type of T to POW(seq(INTEGER)*__DEFERREDSET____20)
28		rewrite_rule_mandatory(rank(A,B), integer, C, [set(couple(seq(integer),_)),seq(integer)], assertion_expression(b(member(B,b(domain(A),set(seq(integer)),[])),pred,[]),'WD Error for: rank',b(last(B),integer,[contains_wd_condition])), integer, [was(rank)|C], rank).
29
30		% N:dom(T) => father(T,N) = front(N)
31		% Instantiated type of T to POW(seq(INTEGER)*__DEFERREDSET____21)
32		rewrite_rule_mandatory(father(A,B), seq(integer), C, [set(couple(seq(integer),_)),seq(integer)], assertion_expression(b(member(B,b(domain(A),set(seq(integer)),[])),pred,[]),'WD Error for: father',b(front(B),seq(integer),[contains_wd_condition])), seq(integer), [was(father)|C], father).
33
34		% (N:dom(T) & N <- I:dom(T)) => son(T,N,I) = N <- I
35		% Instantiated type of T to POW(seq(INTEGER)*__DEFERREDSET____22)
36		rewrite_rule_mandatory(son(A,B,C), seq(integer), D, [set(couple(seq(integer),_)),seq(integer),integer], assertion_expression(b(conjunct(b(member(B,b(domain(A),set(seq(integer)),[])),pred,[]),b(member(b(insert_tail(B,C),seq(integer),[contains_wd_condition]),b(domain(A),set(seq(integer)),[])),pred,[contains_wd_condition])),pred,[contains_wd_condition]),'WD Error for: son',b(insert_tail(B,C),seq(integer),[contains_wd_condition])), seq(integer), [was(son)|D], son).
37
38		% const(X,Q) = { [] |-> X} \/ UNION(const_i).(const_i:dom(Q)| dom({pi,a,p| (p,a):Q(const_i) & pi=const_i->p}))
39		% Instantiated type of a to __DEFERREDSET____23
40		rewrite_rule_mandatory(const(A,B), set(couple(seq(integer),C)), D, [C,seq(set(couple(seq(integer),C)))], union(b(general_union(b(range(b(comprehension_set([b(identifier(const_i),integer,[]),b(identifier('_lambda_result_'),set(couple(seq(integer),C)),[lambda_result])],b(conjunct(b(member(b(identifier(const_i),integer,[]),b(domain(B),set(integer),[])),pred,[]),b(equal(b(identifier('_lambda_result_'),set(couple(seq(integer),C)),[lambda_result]),b(domain(b(comprehension_set([b(identifier(pi),seq(integer),[]),b(identifier(a),C,[]),b(identifier(p),seq(integer),[])],b(conjunct(b(member(b(couple(b(identifier(p),seq(integer),[]),b(identifier(a),C,[])),couple(seq(integer),C),[]),b(function(B,b(identifier(const_i),integer,[])),set(couple(seq(integer),C)),[contains_wd_condition])),pred,[contains_wd_condition]),b(equal(b(identifier(pi),seq(integer),[]),b(insert_front(b(identifier(const_i),integer,[]),b(identifier(p),seq(integer),[])),seq(integer),[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),set(couple(couple(seq(integer),C),seq(integer))),[contains_wd_condition])),set(couple(seq(integer),C)),[contains_wd_condition])),pred,[lambda_result,contains_wd_condition])),pred,[prob_annotation('LAMBDA'),contains_wd_condition])),set(couple(integer,set(couple(seq(integer),C)))),[contains_wd_condition,generated(quantified_union)])),set(set(couple(seq(integer),C))),[contains_wd_condition,generated(quantified_union)])),set(couple(seq(integer),C)),[contains_wd_condition]),b(set_extension([b(couple(b(empty_sequence,seq(integer),[]),A),couple(seq(integer),C),[])]),set(couple(seq(integer),C)),[])), set(couple(seq(integer),C)), [was(const)|D], const).
41
42		% [] : dom(T) => sons(T) = dom({son_x,r,si|si:dom(T) & si/=[] & son_x=first(si) & r= {p,a|(son_x->p,a):T}})
43		% Instantiated type of r to POW(seq(INTEGER)*__DEFERREDSET____24)
44		rewrite_rule_mandatory(sons(A), seq(set(couple(seq(integer),B))), C, [set(couple(seq(integer),B))], assertion_expression(b(member(b(empty_sequence,seq(integer),[]),b(domain(A),set(seq(integer)),[])),pred,[]),'WD Error for: sons',b(domain(b(comprehension_set([b(identifier(son_x),integer,[]),b(identifier(r),set(couple(seq(integer),B)),[]),b(identifier(si),seq(integer),[])],b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(si),seq(integer),[]),b(domain(A),set(seq(integer)),[])),pred,[]),b(not_equal(b(identifier(si),seq(integer),[]),b(empty_sequence,seq(integer),[])),pred,[])),pred,[]),b(equal(b(identifier(son_x),integer,[]),b(first(b(identifier(si),seq(integer),[])),integer,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition]),b(equal(b(identifier(r),set(couple(seq(integer),B)),[]),b(comprehension_set([b(identifier(p),seq(integer),[]),b(identifier(a),B,[])],b(member(b(couple(b(insert_front(b(identifier(son_x),integer,[]),b(identifier(p),seq(integer),[])),seq(integer),[contains_wd_condition]),b(identifier(a),B,[])),couple(seq(integer),B),[contains_wd_condition]),A),pred,[contains_wd_condition])),set(couple(seq(integer),B)),[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),set(couple(couple(integer,set(couple(seq(integer),B))),seq(integer))),[contains_wd_condition])),seq(set(couple(seq(integer),B))),[contains_wd_condition])), seq(set(couple(seq(integer),B))), [was(sons)|C], sons).
45
46		% bin(X) = const(X,[])
47		% Instantiated type of X to __DEFERREDSET____25
48		rewrite_rule_mandatory(bin(A), set(couple(seq(integer),B)), C, [B], const(A,b(empty_sequence,seq(set(couple(seq(integer),B))),[])), set(couple(seq(integer),B)), [was(bin)|C], bin).
49
50		% bin(L,X,R) = const(X,[L,R])
51		% Instantiated type of L to POW(seq(INTEGER)*__DEFERREDSET____26)
52		rewrite_rule_mandatory(bin(A,B,C), set(couple(seq(integer),D)), E, [set(couple(seq(integer),D)),D,set(couple(seq(integer),D))], const(B,b(sequence_extension([A,C]),seq(set(couple(seq(integer),D))),[])), set(couple(seq(integer),D)), [was(bin)|E], bin).
53
54		% left(X) = first(sons(X))
55		% Instantiated type of X to POW(seq(INTEGER)*__DEFERREDSET____27)
56		rewrite_rule_mandatory(left(A), set(couple(seq(integer),B)), C, [set(couple(seq(integer),B))], first(b(sons(A),seq(set(couple(seq(integer),B))),[])), set(couple(seq(integer),B)), [was(left)|C], left).
57
58		% right(X) = last(sons(X))
59		% Instantiated type of X to POW(seq(INTEGER)*__DEFERREDSET____28)
60		rewrite_rule_mandatory(right(A), set(couple(seq(integer),B)), C, [set(couple(seq(integer),B))], last(b(sons(A),seq(set(couple(seq(integer),B))),[])), set(couple(seq(integer),B)), [was(right)|C], right).
61
62		% subtree(T,N) = (%u.(u:seq(INTEGER)|N^u) ; T)
63		% Instantiated type of T to POW(seq(INTEGER)*__DEFERREDSET____29)
64		%rewrite_rule_mandatory(subtree(A,B), set(couple(seq(integer),C)), D, [set(couple(seq(integer),C)),seq(integer)], composition(b(comprehension_set([b(identifier(u),seq(integer),[]),b(identifier('_lambda_result_'),seq(integer),[lambda_result])],b(conjunct(b(member(b(identifier(u),seq(integer),[]),b(seq(b(integer_set('INTEGER'),set(integer),[])),set(seq(integer)),[])),pred,[]),b(equal(b(identifier('_lambda_result_'),seq(integer),[lambda_result]),b(concat(B,b(identifier(u),seq(integer),[])),seq(integer),[contains_wd_condition])),pred,[lambda_result,contains_wd_condition])),pred,[prob_annotation('LAMBDA'),contains_wd_condition])),set(couple(seq(integer),seq(integer))),[contains_wd_condition]),A), set(couple(seq(integer),C)), [was(subtree)|D], subtree).
65		% subtree(T,N) = (%u.(u:(INTEGER<->INTEGER)|N^u) ; T)
66		rewrite_rule_mandatory(subtree(A,B), set(couple(seq(integer),C)), D, [set(couple(seq(integer),C)),seq(integer)], composition(b(comprehension_set([b(identifier(u),set(couple(integer,integer)),[]),b(identifier('_lambda_result_'),seq(integer),[lambda_result])],b(equal(b(identifier('_lambda_result_'),seq(integer),[lambda_result]),b(concat(B,b(identifier(u),seq(integer),[])),seq(integer),[contains_wd_condition])),pred,[prob_annotation('LAMBDA'),lambda_result,contains_wd_condition])),set(couple(set(couple(integer,integer)),seq(integer))),[contains_wd_condition]),A), set(couple(seq(integer),C)), [was(subtree)|D], subtree).
67
68
69		% arity(T,N) = size(sons(subtree(T,N)))
70		% Instantiated type of T to POW(seq(INTEGER)*__DEFERREDSET____30)
71		rewrite_rule_mandatory(arity(A,B), integer, C, [set(couple(seq(integer),D)),seq(integer)], size(b(sons(b(subtree(A,B),set(couple(seq(integer),D)),[])),seq(set(couple(seq(integer),D))),[])), integer, [was(arity)|C], arity).
72
73		% []:dom(T) => sizet(T) = card(T)
74		rewrite_rule_mandatory(sizet(A), integer, B, [set(couple(seq(integer),_))], assertion_expression(b(member(b(empty_sequence,seq(integer),[]),b(domain(A),set(seq(integer)),[])),pred,[]),'WD Error for: sizet',b(card(A),integer,[contains_wd_condition])), integer, [was(sizet)|B], sizet).
75
76		% prefix(T)=closure1(%(st,sn).(sn:seq(ran(T)) & st:seq1(tree(ran(T))) | ((sons(first(st))^tail(st)) , sn <- top(first(st)) )))[{([T],[])}]([])
77		%rewrite_rule_mandatory(prefix(A), seq(B), C, [set(couple(seq(integer),B))], function(b(image(b(closure(b(comprehension_set([b(identifier(st),seq(set(couple(seq(integer),B))),[]),b(identifier(sn),seq(B),[]),b(identifier('_lambda_result_'),couple(seq(set(couple(seq(integer),B))),seq(B)),[lambda_result])],b(conjunct(b(conjunct(b(member(b(identifier(sn),seq(B),[]),b(seq(b(range(A),set(B),[])),set(seq(B)),[])),pred,[]),b(member(b(identifier(st),seq(set(couple(seq(integer),B))),[]),b(seq1(b(tree(b(range(A),set(B),[])),set(set(couple(seq(integer),B))),[])),set(seq(set(couple(seq(integer),B)))),[])),pred,[])),pred,[]),b(equal(b(identifier('_lambda_result_'),couple(seq(set(couple(seq(integer),B))),seq(B)),[lambda_result]),b(couple(b(concat(b(sons(b(first(b(identifier(st),seq(set(couple(seq(integer),B))),[])),set(couple(seq(integer),B)),[contains_wd_condition])),seq(set(couple(seq(integer),B))),[contains_wd_condition]),b(tail(b(identifier(st),seq(set(couple(seq(integer),B))),[])),seq(set(couple(seq(integer),B))),[contains_wd_condition])),seq(set(couple(seq(integer),B))),[contains_wd_condition]),b(insert_tail(b(identifier(sn),seq(B),[]),b(top(b(first(b(identifier(st),seq(set(couple(seq(integer),B))),[])),set(couple(seq(integer),B)),[contains_wd_condition])),B,[contains_wd_condition])),seq(B),[contains_wd_condition])),couple(seq(set(couple(seq(integer),B))),seq(B)),[contains_wd_condition])),pred,[lambda_result,contains_wd_condition])),pred,[prob_annotation('LAMBDA'),contains_wd_condition])),set(couple(couple(seq(set(couple(seq(integer),B))),seq(B)),couple(seq(set(couple(seq(integer),B))),seq(B)))),[contains_wd_condition])),set(couple(couple(seq(set(couple(seq(integer),B))),seq(B)),couple(seq(set(couple(seq(integer),B))),seq(B)))),[contains_wd_condition]),b(set_extension([b(couple(b(sequence_extension([A]),seq(set(couple(seq(integer),B))),[]),b(empty_sequence,seq(B),[])),couple(seq(set(couple(seq(integer),B))),seq(B)),[])]),set(couple(seq(set(couple(seq(integer),B))),seq(B))),[])),set(couple(seq(set(couple(seq(integer),B))),seq(B))),[contains_wd_condition]),b(empty_sequence,seq(set(couple(seq(integer),B))),[])), seq(B), [was(prefix)|C], prefix).
78		% prefix(T) = closure1(/*@ symbolic */ %(st,sn).(sn:(INTEGER<->ran(T)) & st /= [] & st:(INTEGER<->POW((INTEGER<->INTEGER)*ran(T))) | ((sons(first(st))^tail(st)) , sn <- top(first(st)) )))[{([T],[])}]([])
79		rewrite_rule_mandatory(prefix(A), seq(B), C, [set(couple(seq(integer),B))], function(b(image(
80		b(closure(
81		b(comprehension_set(
82		[b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[]),b(identifier(sn),set(couple(integer,B)),[]),b(identifier('_lambda_result_'),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),[lambda_result])],
83		b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(sn),set(couple(integer,B)),[]),b(relations(b(integer_set('INTEGER'),set(integer),[]),b(range(A),set(B),[])),set(set(couple(integer,B))),[])),pred,[]),b(not_equal(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[]),b(empty_sequence,seq(set(couple(set(couple(integer,integer)),B))),[])),pred,[])),pred,[]),b(member(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[]),b(relations(b(integer_set('INTEGER'),set(integer),[]),b(pow_subset(b(cartesian_product(b(relations(b(integer_set('INTEGER'),set(integer),[]),b(integer_set('INTEGER'),set(integer),[])),set(set(couple(integer,integer))),[]),b(range(A),set(B),[])),set(couple(set(couple(integer,integer)),B)),[])),set(set(couple(set(couple(integer,integer)),B))),[])),set(seq(set(couple(set(couple(integer,integer)),B)))),[])),pred,[])),pred,[]),b(equal(b(identifier('_lambda_result_'),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),[lambda_result]),b(couple(b(concat(b(sons(b(first(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[])),set(couple(seq(integer),B)),[contains_wd_condition])),seq(set(couple(seq(integer),B))),[contains_wd_condition]),b(tail(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[])),seq(set(couple(seq(integer),B))),[contains_wd_condition])),seq(set(couple(seq(integer),B))),[contains_wd_condition]),b(insert_tail(b(identifier(sn),seq(B),[]),b(top(b(first(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[])),set(couple(seq(integer),B)),[contains_wd_condition])),B,[contains_wd_condition])),seq(B),[contains_wd_condition])),couple(seq(set(couple(seq(integer),B))),seq(B)),[contains_wd_condition])),pred,[lambda_result,contains_wd_condition])),pred,[prob_annotation('LAMBDA'),contains_wd_condition])),
84		set(couple(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))))),
85		[contains_wd_condition,prob_annotation('SYMBOLIC')])),set(couple(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))))),[contains_wd_condition]),b(set_extension([b(couple(b(sequence_extension([A]),seq(set(couple(seq(integer),B))),[]),b(empty_sequence,seq(B),[])),couple(seq(set(couple(seq(integer),B))),seq(B)),[])]),set(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B)))),[])),set(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B)))),[contains_wd_condition]),b(empty_sequence,seq(set(couple(set(couple(integer,integer)),B))),[])), seq(B), [was(prefix)|C], prefix).
86
87		% postfix(T) = rev(closure1(/*@ symbolic */ %(st,sn).(sn:(INTEGER<->ran(T)) & st /= [] & st:(INTEGER<->POW((INTEGER<->INTEGER)*ran(T))) | ((rev(sons(first(st)))^tail(st)) , sn <- top(first(st)) )))[{([T],[])}]([]))
88		rewrite_rule_mandatory(postfix(A), seq(B), C, [set(couple(seq(integer),B))], rev(b(function(b(image(b(closure(b(comprehension_set([b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[]),b(identifier(sn),set(couple(integer,B)),[]),b(identifier('_lambda_result_'),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),[lambda_result])],b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(sn),set(couple(integer,B)),[]),b(relations(b(integer_set('INTEGER'),set(integer),[]),b(range(A),set(B),[])),set(set(couple(integer,B))),[])),pred,[]),b(not_equal(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[]),b(empty_sequence,seq(set(couple(set(couple(integer,integer)),B))),[])),pred,[])),pred,[]),b(member(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[]),b(relations(b(integer_set('INTEGER'),set(integer),[]),b(pow_subset(b(cartesian_product(b(relations(b(integer_set('INTEGER'),set(integer),[]),b(integer_set('INTEGER'),set(integer),[])),set(set(couple(integer,integer))),[]),b(range(A),set(B),[])),set(couple(set(couple(integer,integer)),B)),[])),set(set(couple(set(couple(integer,integer)),B))),[])),set(seq(set(couple(set(couple(integer,integer)),B)))),[])),pred,[])),pred,[]),b(equal(b(identifier('_lambda_result_'),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),[lambda_result]),b(couple(b(concat(b(rev(b(sons(b(first(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[])),set(couple(seq(integer),B)),[contains_wd_condition])),seq(set(couple(seq(integer),B))),[contains_wd_condition])),seq(set(couple(seq(integer),B))),[contains_wd_condition]),b(tail(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[])),seq(set(couple(seq(integer),B))),[contains_wd_condition])),seq(set(couple(seq(integer),B))),[contains_wd_condition]),b(insert_tail(b(identifier(sn),seq(B),[]),b(top(b(first(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[])),set(couple(seq(integer),B)),[contains_wd_condition])),B,[contains_wd_condition])),seq(B),[contains_wd_condition])),couple(seq(set(couple(seq(integer),B))),seq(B)),[contains_wd_condition])),pred,[lambda_result,contains_wd_condition])),pred,[prob_annotation('LAMBDA'),contains_wd_condition])),set(couple(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))))),[contains_wd_condition,prob_annotation('SYMBOLIC')])),set(couple(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))))),[contains_wd_condition]),b(set_extension([b(couple(b(sequence_extension([A]),seq(set(couple(seq(integer),B))),[]),b(empty_sequence,seq(B),[])),couple(seq(set(couple(seq(integer),B))),seq(B)),[])]),set(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B)))),[])),set(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B)))),[contains_wd_condition]),b(empty_sequence,seq(set(couple(set(couple(integer,integer)),B))),[])),seq(B),[contains_wd_condition])), seq(B), [was(postfix)|C], postfix).
89
90		% --------------------------------
91
92
93		% fnc(r) = %fnc_x.(fnc_x:dom(r)|r[{fnc_x}])
94		rewrite_rule_mandatory(trans_function(A), set(couple(B,set(C))), D, [set(couple(B,C))], comprehension_set([b(identifier(fnc_x),B,[]),b(identifier('_lambda_result_'),set(C),[lambda_result])],b(conjunct(b(member(b(identifier(fnc_x),B,[]),b(domain(A),set(B),[])),pred,[]),b(equal(b(identifier('_lambda_result_'),set(C),[lambda_result]),b(image(A,b(set_extension([b(identifier(fnc_x),B,[])]),set(B),[])),set(C),[])),pred,[lambda_result])),pred,[prob_annotation('LAMBDA')])), set(couple(B,set(C))), [was(trans_function)|D], trans_function).
95
96		% rel(r) = {rel_x,rel_y| rel_x:dom(r) & rel_y: union(r[{rel_x}])}
97		rewrite_rule_mandatory(trans_relation(A), set(couple(B,C)), D, [set(couple(B,set(C)))], comprehension_set([b(identifier(rel_x),B,[]),b(identifier(rel_y),C,[])],b(conjunct(b(member(b(identifier(rel_x),B,[]),b(domain(A),set(B),[])),pred,[]),b(member(b(identifier(rel_y),C,[]),b(general_union(b(image(A,b(set_extension([b(identifier(rel_x),B,[])]),set(B),[])),set(set(C)),[])),set(C),[])),pred,[])),pred,[])), set(couple(B,C)), [was(trans_relation)|D], trans_relation).
98
99
100		% DOES REQUIRE BETTER PATTERN MATCH to be implemented
101		% have now been added to cleanup_post in b_ast_cleanup
102		% [] ^ S = S
103		%rewrite_rule_mandatory(concat(b(empty_sequence,seq(A),_),b(B,C,_)), seq(A), D, [seq(A),seq(A)], B, C, [was(concat)|D], concat).
104		% S ^ [] = S
105		%rewrite_rule_mandatory(concat(b(A,B,_),b(empty_sequence,seq(C),_)), seq(C), D, [seq(C),seq(C)], A, B, [was(concat)|D], concat).
106
107		% D-->{R} = {%xtf.(xtf:D|R)}
108		%rewrite_rule_mandatory(total_function(A,b(set_extension([B]),set(C),_)), set(set(couple(D,C))), E, [set(D),set(C)], set_extension([b(comprehension_set([b(identifier(xtf),D,[]),b(identifier('_lambda_result_'),C,[lambda_result])],b(conjunct(b(member(b(identifier(xtf),D,[]),A),pred,[]),b(equal(b(identifier('_lambda_result_'),C,[lambda_result]),B),pred,[lambda_result])),pred,[prob_annotation('LAMBDA')])),set(couple(D,C)),[])]), set(set(couple(D,C))), [was(total_function)|E], total_function).
109
110		% ---------------------------------------
111
112		% POW(X) = {pow_x|pow_x<:X}
113		rewrite_rule_normalize(pow_subset(A), set(set(B)), C, [set(B)], comprehension_set([b(identifier(pow_x),set(B),[])],b(subset(b(identifier(pow_x),set(B),[]),A),pred,[])), set(set(B)), [was(pow_subset)|C], pow_subset).
114
115		% POW1(X) = {pow1_x|pow1_x /= {} & pow1_x<:X}
116		rewrite_rule_normalize(pow1_subset(A), set(set(B)), C, [set(B)], comprehension_set([b(identifier(pow1_x),set(B),[])],b(conjunct(b(not_equal(b(identifier(pow1_x),set(B),[]),b(empty_set,set(B),[])),pred,[]),b(subset(b(identifier(pow1_x),set(B),[]),A),pred,[])),pred,[])), set(set(B)), [was(pow1_subset)|C], pow1_subset).
117
118		% NAT = 0..MAXINT
119		rewrite_rule_normalize(integer_set('NAT'), set(integer), A, [integer,integer], interval(b(integer(0),integer,[]),b(max_int,integer,[])), set(integer), [was(integer_set)|A], integer_set).
120
121		% NAT1 = 1..MAXINT
122		rewrite_rule_normalize(integer_set('NAT1'), set(integer), A, [integer,integer], interval(b(integer(1),integer,[]),b(max_int,integer,[])), set(integer), [was(integer_set)|A], integer_set).
123
124		% INT = MININT..MAXINT
125		rewrite_rule_normalize(integer_set('INT'), set(integer), A, [integer,integer], interval(b(min_int,integer,[]),b(max_int,integer,[])), set(integer), [was(integer_set)|A], integer_set).
126
127		% NATURAL = {nat|nat>=0}
128		rewrite_rule_normalize(integer_set('NATURAL'), set(integer), A, [integer], comprehension_set([b(identifier(nat),integer,[])],b(greater_equal(b(identifier(nat),integer,[]),b(integer(0),integer,[])),pred,[])), set(integer), [was(integer_set)|A], integer_set).
129
130		% NATURAL1 = {nat1|nat1>=1}
131		rewrite_rule_normalize(integer_set('NATURAL1'), set(integer), A, [integer], comprehension_set([b(identifier(nat1),integer,[])],b(greater_equal(b(identifier(nat1),integer,[]),b(integer(1),integer,[])),pred,[])), set(integer), [was(integer_set)|A], integer_set).
132
133		% id(S) = %id_x.(id_x:S|id_x) % TO DO: should identifier S really appear below ?
134		rewrite_rule_normalize(identity(b(identifier('S'),set(A),_)), set(couple(A,A)), B, [A,A], comprehension_set([b(identifier(id_x),A,[]),b(identifier('_lambda_result_'),A,[lambda_result])],b(conjunct(b(member(b(identifier(id_x),A,[]),b(identifier('S'),set(A),[])),pred,[]),b(equal(b(identifier('_lambda_result_'),A,[lambda_result]),b(identifier(id_x),A,[])),pred,[lambda_result])),pred,[prob_annotation('LAMBDA')])), set(couple(A,A)), [was(identity)|B], identity).
135