| 1 | | % (c) 2020-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(well_def_tools, [rename_norm_term/3, member_in_norm_conjunction/2, not_occurs/2, occurs/2]). |
| 6 | | |
| 7 | | :- use_module(probsrc(module_information),[module_info/2]). |
| 8 | | :- module_info(group,well_def_prover). |
| 9 | | :- module_info(description,'This module provides utilities for the WD prover.'). |
| 10 | | |
| 11 | | |
| 12 | | :- use_module(probsrc(debug)). |
| 13 | | % -------------------- |
| 14 | | % tools for normalized expressions: |
| 15 | | |
| 16 | | % check if a known/bound ID occurs in a normalized expression |
| 17 | ? | not_occurs(Expr,ID) :- (occurs(Expr,ID) -> debug_println(19,occurs_in(ID,Expr)),fail ; true). |
| 18 | | occurs('$'(ID1),ID2) :- !, ID1 = ID2. |
| 19 | | occurs(conjunct(A,B),ID) :- !, (occurs(A,ID) ; occurs(B,ID)). |
| 20 | | occurs(couple(A,B),ID) :- !, (occurs(A,ID) ; occurs(B,ID)). |
| 21 | | occurs(equal(A,B),ID) :- !, (occurs(A,ID) ; occurs(B,ID)). |
| 22 | | occurs(field(_,A),ID) :- !, occurs(A,ID). |
| 23 | | occurs(function(A,B),ID) :- !, (occurs(A,ID) ; occurs(B,ID)). |
| 24 | | occurs(interval(A,B),ID) :- !, (occurs(A,ID) ; occurs(B,ID)). |
| 25 | | occurs(member(A,B),ID) :- !, (occurs(A,ID) ; occurs(B,ID)). |
| 26 | | occurs(record_field(A,B),ID) :- !, (occurs(A,ID) ; occurs(B,ID)). |
| 27 | | occurs(value(_),_ID) :- !, fail. |
| 28 | | occurs(string(_),_ID) :- !, fail. |
| 29 | | occurs(reverse(A),ID) :- !, occurs(A,ID). |
| 30 | | occurs(domain(A),ID) :- !, occurs(A,ID). |
| 31 | | occurs(range(A),ID) :- !, occurs(A,ID). |
| 32 | | occurs(comprehension_set(Paras,Body),ID) :- !, |
| 33 | | (member('$'(ID),Paras) -> fail % ID becomes invisible |
| 34 | ? | ; occurs(Body,ID)). |
| 35 | | % TO DO: treat other bound IDs exists,... [but not crucial, as we err on the safe side here] |
| 36 | ? | occurs([H|T],ID) :- !, (occurs(H,ID) -> true ; occurs(T,ID)). |
| 37 | | occurs(boolean_true,_) :- !,fail. |
| 38 | | occurs(boolean_false,_) :- !,fail. |
| 39 | | occurs(empty_set,_) :- !,fail. |
| 40 | ? | occurs(Expr,ID) :- Expr =.. [_|Args], member(A,Args), occurs(A,ID). |
| 41 | | |
| 42 | | member_in_norm_conjunction(Pred,Pred). |
| 43 | | member_in_norm_conjunction(conjunct(A,B),Pred) :- |
| 44 | ? | member_in_norm_conjunction(A,Pred) ; member_in_norm_conjunction(B,Pred). |
| 45 | | |
| 46 | | |
| 47 | | :- use_module(library(lists),[exclude/3]). |
| 48 | | |
| 49 | | % apply a substitution to a normalised term: |
| 50 | | rename_norm_term('$'(X),Subst,Res) :- !, |
| 51 | ? | (member(rename(X,NewTerm),Subst) % TODO : use ord_member |
| 52 | | -> Res=NewTerm |
| 53 | | ; Res='$'(X)). |
| 54 | | rename_norm_term(conjunct(A,B),Subst,conjunct(SA,SB)) :- !, |
| 55 | | rename_norm_term(A,Subst,SA), rename_norm_term(B,Subst,SB). |
| 56 | | rename_norm_term(if_then_else(A,B,C),Subst,if_then_else(SA,SB,SC)) :- !, |
| 57 | | rename_norm_term(A,Subst,SA), rename_norm_term(B,Subst,SB), rename_norm_term(C,Subst,SC). |
| 58 | | rename_norm_term(equal(A,B),Subst,equal(SA,SB)) :- !, |
| 59 | | rename_norm_term(A,Subst,SA), rename_norm_term(B,Subst,SB). |
| 60 | | rename_norm_term(function(A,B),Subst,function(SA,SB)) :- !, |
| 61 | | rename_norm_term(A,Subst,SA), rename_norm_term(B,Subst,SB). |
| 62 | | rename_norm_term(field(F,B),Subst,field(F,SB)) :- !, |
| 63 | | rename_norm_term(B,Subst,SB). |
| 64 | | rename_norm_term(record_field(Rec,FieldName),Subst,record_field(Rec,FieldName)) :- !, |
| 65 | | rename_norm_term(Rec,Subst,Rec). |
| 66 | | rename_norm_term(member(A,B),Subst,member(SA,SB)) :- !, |
| 67 | | rename_norm_term(A,Subst,SA), rename_norm_term(B,Subst,SB). |
| 68 | | rename_norm_term(rec(F),Subst,rec(SF)) :- !, |
| 69 | | l_rename_norm_terms(F,Subst,SF). |
| 70 | ? | rename_norm_term(Nr,_,Res) :- simple_norm_term(Nr),!,Res=Nr. |
| 71 | | rename_norm_term(QOP,Subst,RQOP) :- |
| 72 | | quantified_op(QOP,Functor,Ids,Exprs,Bodies),!, |
| 73 | | l_rename_norm_terms(Exprs,Subst,RExprs), |
| 74 | | sort(Ids,SIds), |
| 75 | | % TO DO: also ensure Subst is sorted and use linear algo |
| 76 | | exclude(clash_with_new(SIds),Subst,NSubst), |
| 77 | | %print(clashing(SIds,Subst,NSubst,Bodies)),nl, |
| 78 | | l_rename_norm_terms(Bodies,NSubst,RBodies), |
| 79 | | quantified_op(RQOP,Functor,Ids,RExprs,RBodies). |
| 80 | | rename_norm_term(Term,Subst,RenTerm) :- functor(Term,BOP,2), bin_op(BOP),!, |
| 81 | | functor(RenTerm,BOP,2), |
| 82 | | arg(1,Term,A), arg(1,RenTerm,RA), rename_norm_term(A,Subst,RA), |
| 83 | | arg(2,Term,B), arg(2,RenTerm,RB), rename_norm_term(B,Subst,RB). |
| 84 | | rename_norm_term(Term,Subst,RenTerm) :- functor(Term,UOP,1), un_op(UOP),!, |
| 85 | | functor(RenTerm,UOP,1), |
| 86 | ? | arg(1,Term,A), arg(1,RenTerm,RA), rename_norm_term(A,Subst,RA). |
| 87 | | rename_norm_term(Term,Subst,RenTerm) :- list_op(Term,Kind,List),!, |
| 88 | ? | list_op(RenTerm,Kind,RList), |
| 89 | | l_rename_norm_terms(List,Subst,RList). |
| 90 | | rename_norm_term(A,_,_) :- print(uncovered_renaming(A)),nl,fail. |
| 91 | | |
| 92 | | % uncovered_renaming(external_function_call(STRING_CODES,[$(s)])) |
| 93 | | |
| 94 | | :- use_module(library(ordsets),[ord_member/2]). |
| 95 | | clash_with_new(SortedIDs,rename(ID,_)) :- ord_member($(ID),SortedIDs). |
| 96 | | |
| 97 | | l_rename_norm_terms([],_,[]). |
| 98 | | l_rename_norm_terms([H|T],Subst,[RH|RT]) :- |
| 99 | | rename_norm_term(H,Subst,RH),!, |
| 100 | | l_rename_norm_terms(T,Subst,RT). |
| 101 | | |
| 102 | | |
| 103 | | list_op(set_extension(L),set_extension,L). |
| 104 | | list_op(sequence_extension(L),sequence_extension,L). |
| 105 | | list_op(external_function_call(Name,Args),external_function_call(Name),Args). |
| 106 | | |
| 107 | | % quantified_op(Term, ListOfDollarIDs, ListOfExprsOutsideOfScope, ListExpressionInNewScope) |
| 108 | | quantified_op(comprehension_set(IDS,Body),comprehension_set,IDS,[],[Body]). |
| 109 | | quantified_op(exists(IDS,Body),exists,IDS,[],[Body]). |
| 110 | | quantified_op(forall(IDS,LHS,RHS),forall,IDS,[],[LHS,RHS]). |
| 111 | | quantified_op(let_expression(IDS,Exprs,Body),let_expression,IDS,Exprs,[Body]). |
| 112 | | quantified_op(let_predicate(IDS,Exprs,Body),let_predicate,IDS,Exprs,[Body]). |
| 113 | | quantified_op(general_product(IDS,P,E),general_product,IDS,[],[P,E]). |
| 114 | | quantified_op(general_sum(IDS,P,E),general_sum,IDS,[],[P,E]). |
| 115 | | % lazy_let_pred, ... |
| 116 | | |
| 117 | | |
| 118 | | % TO DO: add more bin and unary ops; records, quantified operators |
| 119 | | bin_op(add). |
| 120 | | bin_op(add_real). |
| 121 | | bin_op(card). |
| 122 | | bin_op(cartesian_product). |
| 123 | | bin_op(composition). |
| 124 | | bin_op(concat). |
| 125 | | bin_op(couple). |
| 126 | | bin_op(div). |
| 127 | | bin_op(div_real). |
| 128 | | bin_op(disjunct). |
| 129 | | bin_op(domain_restriction). |
| 130 | | bin_op(domain_subtraction). |
| 131 | | bin_op(equivalence). |
| 132 | | bin_op(greater). |
| 133 | | bin_op(greater_equal). |
| 134 | | bin_op(floored_div). |
| 135 | | bin_op(function). |
| 136 | | bin_op(image). |
| 137 | | bin_op(implication). |
| 138 | | bin_op(insert_front). |
| 139 | | bin_op(insert_tail). |
| 140 | | bin_op(intersection). |
| 141 | | bin_op(interval). |
| 142 | | bin_op(iteration). |
| 143 | | bin_op(less). |
| 144 | | bin_op(less_equal). |
| 145 | | bin_op(less_real). |
| 146 | | bin_op(less_equal_real). |
| 147 | | bin_op(minus). |
| 148 | | bin_op(minus_real). |
| 149 | | bin_op(modulo). |
| 150 | | bin_op(multiplication). |
| 151 | | bin_op(multiplication_real). |
| 152 | | bin_op(overwrite). |
| 153 | | bin_op(not_equal). |
| 154 | | bin_op(not_member). |
| 155 | | bin_op(partial_bijection). |
| 156 | | bin_op(partial_function). |
| 157 | | bin_op(partial_injection). |
| 158 | | bin_op(partial_surjection). |
| 159 | | bin_op(power_of). |
| 160 | | bin_op(power_of_real). |
| 161 | | bin_op(range_restriction). |
| 162 | | bin_op(range_subtraction). |
| 163 | | bin_op(relations). |
| 164 | | bin_op(restrict_front). |
| 165 | | bin_op(restrict_tail). |
| 166 | | bin_op(set_subtraction). |
| 167 | | bin_op(size). |
| 168 | | bin_op(subset). |
| 169 | | bin_op(subset_strict). |
| 170 | | bin_op(surjection_relation). |
| 171 | | bin_op(total_function). |
| 172 | | bin_op(total_injection). |
| 173 | | bin_op(total_surjection). |
| 174 | | bin_op(total_relation). |
| 175 | | bin_op(total_surjection_relation). |
| 176 | | bin_op(union). |
| 177 | | |
| 178 | | un_op(bag_items). |
| 179 | | un_op(card). |
| 180 | | un_op(closure). % closure1 |
| 181 | | un_op(compaction). |
| 182 | | un_op(convert_bool). |
| 183 | | un_op(convert_real). |
| 184 | | un_op(convert_int_floor). |
| 185 | | un_op(convert_int_ceiling). |
| 186 | | un_op(domain). |
| 187 | | un_op(finite). |
| 188 | | un_op(fin_subset). |
| 189 | | un_op(fin1_subset). |
| 190 | | un_op(first_of_pair). |
| 191 | | un_op(front). |
| 192 | | un_op(identity). |
| 193 | | un_op(iseq). |
| 194 | | un_op(iseq1). |
| 195 | | un_op(last). |
| 196 | | un_op(negation). |
| 197 | | un_op(max). |
| 198 | | un_op(max_real). |
| 199 | | un_op(min). |
| 200 | | un_op(min_real). |
| 201 | | un_op(mu). |
| 202 | | un_op(perm). |
| 203 | | un_op(pow_subset). |
| 204 | | un_op(pow1_subset). |
| 205 | | un_op(range). |
| 206 | | un_op(rev). |
| 207 | | un_op(reverse). |
| 208 | | un_op(reflexive_closure). |
| 209 | | un_op(second_of_pair). |
| 210 | | un_op(seq). |
| 211 | | un_op(seq1). |
| 212 | | un_op(size). |
| 213 | | un_op(tail). |
| 214 | | un_op(unary_minus). |
| 215 | | un_op(unary_minus_real). |
| 216 | | |
| 217 | | % do not require renaming: |
| 218 | | simple_norm_term(truth). |
| 219 | | simple_norm_term(boolean_true). |
| 220 | | simple_norm_term(boolean_false). |
| 221 | | simple_norm_term(bool_set). |
| 222 | | simple_norm_term(float_set). |
| 223 | | simple_norm_term(real_set). |
| 224 | | simple_norm_term(string_set). |
| 225 | | simple_norm_term(typeset). |
| 226 | | simple_norm_term(value(_)). |
| 227 | | simple_norm_term(string(_)). |
| 228 | | simple_norm_term(empty_set). |
| 229 | | simple_norm_term(empty_sequence). |
| 230 | | simple_norm_term(max_int). |
| 231 | | simple_norm_term(min_int). |
| 232 | | simple_norm_term('NATURAL'). |
| 233 | | simple_norm_term('NATURAL1'). |
| 234 | | simple_norm_term(lazy_lookup_pred(_)). |
| 235 | | simple_norm_term(lazy_lookup_expr(_)). |
| 236 | | simple_norm_term(Nr) :- number(Nr). |