1		% (c) 2009-2024 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(bsyntaxtree_quantifiers,[ create_z_let/6 ]).
6
7
8		:- use_module(module_information,[module_info/2]).
9		:- module_info(group,typechecker).
10		:- module_info(description,'This module provides operations on the type-checked AST.').
11
12
13
14		:- use_module(bsyntaxtree,[find_identifier_uses/3,get_texpr_id/2, get_texpr_ids/2, get_texpr_type/2,
15		find_identifier_uses_l/3, rename_bt/3,
16		create_texpr/4]).
17
18
19		% ****************************************************
20
21		:- use_module(error_manager,[add_warning/3]).
22
23		% create Z-style let; see page 59 of Spivey, identifiers are not in scope for Value expressions
24		% ExPr is either expr or pred or a variable
25		create_z_let(ExPr,Ids,Values,Inner1,Infos,Result) :-
26		remove_unused_identifiers(Ids,Values,Inner1,RIds0,RValues0),
27		remove_unnecessary_lets(RIds0,RValues0,RIds1,RValues),
28		( RIds1=[] -> Result = Inner1
29		;
30		find_identifier_uses_l(RValues,[],RVars),
31		gen_fresh_typed_params(RIds1,Inner1,RVars,RIds,Inner),
32		(var(ExPr), get_texpr_type(Inner,Pred), Pred==pred -> ExPr=pred ; true), % if ExPr not set: infer it from Inner
33		(ExPr=expr ->
34		get_texpr_type(Inner,Type),
35		create_texpr(let_expression(RIds,RValues,Inner),Type,Infos,Result)
36		; ExPr=pred ->
37		create_texpr(let_predicate(RIds,RValues,Inner),pred,Infos,Result)
38		),
39		% extra check: but gen_fresh_typed_params should ensure everything ok
40		get_texpr_ids(RIds,S1), sort(S1,SortedIDs),
41		(ord_intersection(SortedIDs,RVars,Clash), Clash \= []
42		-> add_warning(create_let,'Variable clash in generated let:',Clash)
43		% can cause problems if we use let_predicate/let_expression which allows introducing multiple, dependent ids
44		; true)
45		).
46
47		:- use_module(library(lists)).
48		:- use_module(library(ordsets)).
49
50		%% rename parameters and direct definition body to use fresh ids
51		%% reason is that otherwise we repeatedly introduce the same variable and obtain nested lets with variable clashes
52		%% i.e., we may get lets of the form LET a ... LET a,b BE a=(a) & b=(a) ... where (a) is the outer value of a
53		%% Note: however, performance of test 1657 suffers if we systematically rename (hence we only rename VarsToAvoid)
54		gen_fresh_typed_params(TParams,TBody,VarsToAvoid,NewTParams,NewTBody) :-
55		maplist(alpha_typed_id_rename(VarsToAvoid),TParams,NewTParams,RenameList),
56		rename_bt(TBody,RenameList,NewTBody).
57
58		:- use_module(probsrc(gensym),[gensym/2]).
59		alpha_typed_id_rename(VarsToAvoid,b(identifier(OldID),T,I),b(identifier(FreshID),T,I),rename(OldID,FreshID)) :-
60		(ord_member(OldID,VarsToAvoid) -> gensym(OldID,FreshID) ; FreshID=OldID).
61
62		remove_unused_identifiers(TLetIds1,TLetValues1,TDef,TLetIds,TLetValues) :-
63		find_identifier_uses(TDef,[],UsedIds),
64		maplist(combine_with_minus,TLetIds1,TLetValues1,IdValuePairs),
65		include(id_is_used(UsedIds),IdValuePairs,NewIdValuePairs),
66		maplist(combine_with_minus,TLetIds,TLetValues,NewIdValuePairs).
67
68		% remove let a=a, ...
69		remove_unnecessary_lets([],[],[],[]).
70		remove_unnecessary_lets([TID|T1],[TRHS|T2],IDS,RHSS) :-
71		(unnecessary_let(TID,TRHS)
72		-> remove_unnecessary_lets(T1,T2,IDS,RHSS)
73		; IDS=[TID|TIDS], RHSS = [TRHS|TRHSS], remove_unnecessary_lets(T1,T2,TIDS,TRHSS)
74		).
75		unnecessary_let(b(identifier(ID),T,_),b(identifier(ID),T,_)).
76		combine_with_minus(A,B,A-B).
77		id_is_used(UsedIds,TId-_Value) :-
78		get_texpr_id(TId,Id),memberchk(Id,UsedIds).
79