1		:- module(welldef, [ensure_wd/2,
2		po_on_lhs/1,
3		po_on_lhs/2,
4		strip_pos/2,
5		wd_pos/2]).
6
7		:- use_module(library(lists), [maplist/3, maplist/4, append/2]).
8
9		:- use_module(wdsrc(well_def_hyps), [empty_hyps/1, push_hyp/4, negate_hyp/2]).
10		:- use_module(wdsrc(well_def_analyser), [transform_wd/4, compute_wd/4,
11		toplevel_wd_pos/3]).
12		:- use_module(probsrc(bsyntaxtree), [repair_used_ids/3]).
13
14
15		:- use_module(fuzztypes).
16
17
18		%% wd_pos(Predicate, ProofObligations).
19		%
20		% Returns a list of proof obligations for the given predicate.
21		wd_pos(Pred, WDPOs) :-
22		empty_hyps(Hyps),
23		findall(WDPO, compute_wd(Pred, Hyps, [discharge_po], WDPO), WDPOs).
24
25
26		%% ensure_wd(+Predicate, -PredicateWithProofObligations).
27		%
28		% Ensures that the given predicate is well-defined by adding open
29		% proof obligations for all well-definedness conditions as additional conjuncts.
30		ensure_wd(Pred, WDPred) :-
31		empty_hyps(Hyps),
32		% push_hyp(Hyps, Pred, [create_full_po], FullHyps),
33		% transform_bexpr(b_ast_cleanup:compute_wd_info, Pred, InterPred),
34		transform_wd(Pred, Hyps, [discharge_po], AnnotatedPred),
35		ensure_wd_node(AnnotatedPred, Hyps, _, PrelimWD),
36		repair_used_ids('Welldef Enforcer', PrelimWD, WDPred).
37
38		%% ensure_wd_node(+Ast, +Hyps, -RemainingGoals, -WdAst).
39		%
40		% Implements any WD conditions into the closest predicate nodes.
41		% When not possible the remaining conditions are returned via `RemainingGoals`.
42		ensure_wd_node([N | Ns], H, RemainingPOs, [Wd|Wds]) :-
43		!, % Special case: List.
44		ensure_wd_node_list([N | Ns], H, NestedRemainingPOs, [Wd|Wds]),
45		append(NestedRemainingPOs, RemainingPOs).
46		ensure_wd_node(b(Node, Type, Info), H, RemainingPOs, NewAst) :-
47		% Special cases: POs to LHS (middle child)
48		Cases = [general_sum, general_product, quantified_intersection, quantified_union, lambda, forall],
49		node_split(Node, Name, [Ids, Pred, Expr]),
50		member(Name, Cases),
51		!,
52		wd_to_lhs(Pred, Expr, H, WdPred, WdExpr),
53		node_split(WdNode, Name, [Ids, WdPred, WdExpr]),
54		WdAst = b(WdNode, Type, Info),
55		toplevel_wd_pos(WdAst, H, RootPOs),
56		conjunct_or_propagate_pos(WdAst, RootPOs, NewAst, RemainingPOs).
57		ensure_wd_node(b(Node, Type, Info), H, RemainingPOs, NewAst) :-
58		% Special cases: POs to RHS (last child)
59		Cases = [event_b_comprehension_set],
60		node_split(Node, Name, [Ids, Expr, Pred]),
61		member(Name, Cases),
62		!,
63		wd_to_rhs(Expr, Pred, H, WdExpr, WdPred),
64		node_split(WdNode, Name, [Ids, WdExpr, WdPred]),
65		WdAst = b(WdNode, Type, Info),
66		toplevel_wd_pos(WdAst, H, RootPOs),
67		conjunct_or_propagate_pos(WdAst, RootPOs, NewAst, RemainingPOs).
68		ensure_wd_node(b(assertion_expression(Test, ErrText, Value), Type, Info), H, POs, Result) :-
69		Result = b(assertion_expression(Test, ErrText, WdValue), Type, Info),
70		ensure_wd_node(Value, H, POs, WdValue).
71		ensure_wd_node(b(if_then_else(If, Then, Else), Type, Info), H, POs, WdIfThenElse) :-
72		Type \= pred, !, % Special case for If-Expressions.
73		ensure_wd_node(If, H, [], WdIf),
74		push_hyp(H, If, [create_full_po], ThenH),
75		transform_wd(Then, H, [discharge_po], TThen),
76		ensure_wd_node(TThen, ThenH, ThenPOs, WdThen),
77		negate_hyp(If, NotIf),
78		push_hyp(H, NotIf, [create_full_po], ElseH),
79		ensure_wd_node(Else, ElseH, ElsePOs, WdElse),
80		if_then_else_po(WdIf, ThenPOs, IfThen),
81		ensure_wd_node(NotIf, H, [], WdNotIf),
82		if_then_else_po(WdNotIf, ElsePOs, NotIfElse),
83		WdIfThenElse = b(if_then_else(WdIf, WdThen, WdElse), Type, Info),
84		append(IfThen, NotIfElse, POs).
85		ensure_wd_node(b(Node, Type, Info), H, RemainingPOs, NewAst) :-
86		% Special cases: WD constraints from LHS chain into RHS
87		Cases = [conjunct,implication],
88		node_split(Node, Name, [Lhs, Rhs]),
89		member(Name, Cases),
90		!,
91		ensure_wd_node(Lhs, H, [], WdLhs),
92		push_hyp(H, WdLhs, [create_full_po], RhsH),
93		ensure_wd_node(Rhs, RhsH, [], WdRhs),
94		node_split(WdNode, Name, [WdLhs, WdRhs]),
95		WdAst = b(WdNode, Type, Info),
96		toplevel_wd_pos(WdAst, H, RootPOs),
97		conjunct_or_propagate_pos(WdAst, RootPOs, NewAst, RemainingPOs).
98		ensure_wd_node(Node, H, RemainderPOs, WdPred) :-
99		wd_children_and_pos(Node, H, POs, InterNode),
100		conjunct_or_propagate_pos(InterNode, POs, WdPred, RemainderPOs).
101
102
103		ensure_wd_node_list([], _, [], []) :- !.
104		ensure_wd_node_list([N | Ns], H, [R | Rs], [Wd | Wds]) :-
105		ensure_wd_node(N, H, R, Wd),
106		ensure_wd_node_list(Ns, H, Rs, Wds).
107
108
109
110		% Helper for repetitive code.
111		wd_children_and_pos(b(Node, Type, Info), H, POs, UpdatedNode) :-
112		node_split(Node, Name, Children),
113		ensure_wd_node_list(Children, H, Remainders, WdChildren),
114		append(Remainders, ChildPOs),
115		node_split(NewNode, Name, WdChildren),
116		UpdatedNode = b(NewNode, Type, Info),
117		toplevel_wd_pos(UpdatedNode, H, RootPOs),
118		append(ChildPOs, RootPOs, POs).
119
120
121		% Helps dispatching whether the POs need to be included into a predicate or
122		% an expression needs to propagate them upwards.
123		conjunct_or_propagate_pos(b(Node, pred, Info), POs, WdPred, []) :-
124		!, % predicates conjunct the POs into themselves.
125		filter_discharged_pos(POs, UndischargedPOs),
126		include_pos(UndischargedPOs, b(Node, pred, Info), WdPred).
127		conjunct_or_propagate_pos(Node, POs, Node, POs). % Expressions remain unchanged.
128
129
130
131
132
133		% Assumes Lhs is predicate and Rhs is expression.
134		wd_to_lhs(Lhs, Rhs, H, WdLhs, Rhs2) :-
135		ensure_wd_node(Lhs, H, [], Lhs2),
136		push_hyp(H, Lhs2, [create_full_po], NewH),
137		wd_children_and_pos(Rhs, NewH, POs, Rhs2),
138		filter_discharged_pos(POs, UndischargedPOs),
139		include_pos(UndischargedPOs, Lhs2, WdLhs).
140		% Assumes Lhs is expression and Rhs is predicate.
141		wd_to_rhs(Lhs, Rhs, H, WdLhs, WdRhs) :-
142		wd_to_lhs(Rhs, Lhs, H, WdRhs, WdLhs).
143
144
145		if_then_else_po(Condition, BranchPOs, Res) :-
146		filter_discharged_pos(BranchPOs, Filtered),
147		if_then_else_implication(Filtered, Condition, Res).
148
149		if_then_else_implication([], _, []) :- !.
150		if_then_else_implication(POs, Condition, [Res]) :-
151		po_conjunct(POs, BranchConjunct),
152		Res = b(implication(Condition, BranchConjunct), pred, [contains_wd_condition]).
153
154
155
156
157		%% include_pos(ProofObligations, Predicate, PredicateWithPOs).
158		%
159		% Returns a predicate with the given proof obligations included via `conjunct` nodes.
160		include_pos([], Pred, Pred) :- !.
161		include_pos(POs, Pred, b(conjunct(POsConj, Pred), pred, [contains_wd_condition,fuzzed_with_wd_po_included])) :-
162		po_conjunct(POs, POsConj).
163
164		filter_discharged_pos([], []).
165		filter_discharged_pos([PO | POs], [PO | NonDischarged]) :-
166		PO = b(_, _, Info),
167		\+ member(discharged(true, _), Info), !,
168		filter_discharged_pos(POs, NonDischarged).
169		filter_discharged_pos([_|POs], NonDischarged) :-
170		filter_discharged_pos(POs, NonDischarged).
171
172		po_conjunct([PO], PO) :- !.
173		po_conjunct([PO | POs], b(conjunct(PO, POsConj), pred, [contains_wd_condition])) :-
174		po_conjunct(POs, POsConj).
175
176
177		%% po_on_lhs(+AST).
178		%
179		% Succeeds if the left side of the AST is marked as POs.
180		% This will be the case, if the b/3 structure contains the
181		% `fuzzed_with_wd_po_included` flag.
182		%
183		% AST: The AST to check.
184		po_on_lhs(b(conjunct(_, _), _, Info)) :-
185		member(fuzzed_with_wd_po_included, Info).
186
187		%% po_on_lhs(+AST, -RHS).
188		%
189		% Succeeds if the left side of the AST is marked as POs.
190		% This will be the case, if the b/3 structure contains the
191		% `fuzzed_with_wd_po_included` flag.
192		%
193		% AST: The AST to check.
194		% RHS: The non-PO part of the AST.
195		po_on_lhs(b(conjunct(_, RHS), _, Info), RHS) :-
196		member(fuzzed_with_wd_po_included, Info).
197
198
199		%% strip_pos(+Ast, -AstWithoutPOs).
200		%
201		% Removes any subtrees which are generated by `ensure_wd` from the predicate.
202		strip_pos([A|As], Raws) :-
203		!,
204		maplist(strip_pos, [A|As], Raws).
205		strip_pos(Ast, RawAst) :-
206		po_on_lhs(Ast, InterAst),
207		!,
208		strip_pos(InterAst, RawAst).
209		strip_pos(b(assertion_expression(_, _, SecuredPred), _, _), Result) :-
210		!, % assertion expressions are discarded.
211		strip_pos(SecuredPred, Result).
212		strip_pos(b(Node, Type, Info), b(NewNode, Type, Info)) :-
213		node_split(Node, Name, Children),
214		maplist(strip_pos, Children, NewChildren),
215		node_split(NewNode, Name, NewChildren).
216
217
218		node_split(Node, Name, [b(Child1, T1, I1) | OtherChildren]) :-
219		Node =.. [Name, b(Child1, T1, I1) | OtherChildren], !.
220		node_split(Node, Name, [[A|As] | OtherChildren]) :-
221		Node =.. [Name, [A|As] | OtherChildren], !.
222		node_split(Node, Node, []). % Catches things like integer(42) or integer_set('NAT').