| 1 | % (c) 2020-2023 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(member(A,B),Subst,member(SA,SB)) :- !, | |
| 65 | rename_norm_term(A,Subst,SA), rename_norm_term(B,Subst,SB). | |
| 66 | rename_norm_term(rec(F),Subst,rec(SF)) :- !, | |
| 67 | l_rename_norm_terms(F,Subst,SF). | |
| 68 | rename_norm_term(Nr,_,Res) :- simple_norm_term(Nr),!,Res=Nr. | |
| 69 | rename_norm_term(QOP,Subst,RQOP) :- | |
| 70 | quantified_op(QOP,Functor,Ids,Exprs,Bodies),!, | |
| 71 | l_rename_norm_terms(Exprs,Subst,RExprs), | |
| 72 | sort(Ids,SIds), | |
| 73 | % TO DO: also ensure Subst is sorted and use linear algo | |
| 74 | exclude(clash_with_new(SIds),Subst,NSubst), | |
| 75 | %print(clashing(SIds,Subst,NSubst,Bodies)),nl, | |
| 76 | l_rename_norm_terms(Bodies,NSubst,RBodies), | |
| 77 | quantified_op(RQOP,Functor,Ids,RExprs,RBodies). | |
| 78 | rename_norm_term(Term,Subst,RenTerm) :- functor(Term,BOP,2), bin_op(BOP),!, | |
| 79 | functor(RenTerm,BOP,2), | |
| 80 | arg(1,Term,A), arg(1,RenTerm,RA), rename_norm_term(A,Subst,RA), | |
| 81 | arg(2,Term,B), arg(2,RenTerm,RB), rename_norm_term(B,Subst,RB). | |
| 82 | rename_norm_term(Term,Subst,RenTerm) :- functor(Term,UOP,1), un_op(UOP),!, | |
| 83 | functor(RenTerm,UOP,1), | |
| 84 | arg(1,Term,A), arg(1,RenTerm,RA), rename_norm_term(A,Subst,RA). | |
| 85 | rename_norm_term(Term,Subst,RenTerm) :- list_op(Term,Kind,List),!, | |
| 86 | list_op(RenTerm,Kind,RList), | |
| 87 | l_rename_norm_terms(List,Subst,RList). | |
| 88 | rename_norm_term(A,_,_) :- print(uncovered_renaming(A)),nl,fail. | |
| 89 | ||
| 90 | % uncovered_renaming(external_function_call(STRING_CODES,[$(s)])) | |
| 91 | ||
| 92 | :- use_module(library(ordsets),[ord_member/2]). | |
| 93 | clash_with_new(SortedIDs,rename(ID,_)) :- ord_member($(ID),SortedIDs). | |
| 94 | ||
| 95 | l_rename_norm_terms([],_,[]). | |
| 96 | l_rename_norm_terms([H|T],Subst,[RH|RT]) :- | |
| 97 | rename_norm_term(H,Subst,RH),!, | |
| 98 | l_rename_norm_terms(T,Subst,RT). | |
| 99 | ||
| 100 | ||
| 101 | list_op(set_extension(L),set_extension,L). | |
| 102 | list_op(sequence_extension(L),sequence_extension,L). | |
| 103 | list_op(external_function_call(Name,Args),external_function_call(Name),Args). | |
| 104 | ||
| 105 | % quantified_op(Term, ListOfDollarIDs, ListOfExprsOutsideOfScope, ListExpressionInNewScope) | |
| 106 | quantified_op(comprehension_set(IDS,Body),comprehension_set,IDS,[],[Body]). | |
| 107 | quantified_op(exists(IDS,Body),exists,IDS,[],[Body]). | |
| 108 | quantified_op(forall(IDS,LHS,RHS),forall,IDS,[],[LHS,RHS]). | |
| 109 | quantified_op(let_expression(IDS,Exprs,Body),let_expression,IDS,Exprs,[Body]). | |
| 110 | quantified_op(let_predicate(IDS,Exprs,Body),let_predicate,IDS,Exprs,[Body]). | |
| 111 | ||
| 112 | ||
| 113 | % TO DO: add more bin and unary ops; records, quantified operators | |
| 114 | bin_op(add). | |
| 115 | bin_op(add_real). | |
| 116 | bin_op(card). | |
| 117 | bin_op(cartesian_product). | |
| 118 | bin_op(composition). | |
| 119 | bin_op(concat). | |
| 120 | bin_op(couple). | |
| 121 | bin_op(div). | |
| 122 | bin_op(div_real). | |
| 123 | bin_op(disjunct). | |
| 124 | bin_op(domain_restriction). | |
| 125 | bin_op(domain_subtraction). | |
| 126 | bin_op(equivalence). | |
| 127 | bin_op(greater). | |
| 128 | bin_op(greater_equal). | |
| 129 | bin_op(floored_div). | |
| 130 | bin_op(function). | |
| 131 | bin_op(image). | |
| 132 | bin_op(implication). | |
| 133 | bin_op(insert_front). | |
| 134 | bin_op(insert_tail). | |
| 135 | bin_op(intersection). | |
| 136 | bin_op(interval). | |
| 137 | bin_op(iteration). | |
| 138 | bin_op(less). | |
| 139 | bin_op(less_equal). | |
| 140 | bin_op(less_real). | |
| 141 | bin_op(less_equal_real). | |
| 142 | bin_op(minus). | |
| 143 | bin_op(minus_real). | |
| 144 | bin_op(modulo). | |
| 145 | bin_op(multiplication). | |
| 146 | bin_op(multiplication_real). | |
| 147 | bin_op(overwrite). | |
| 148 | bin_op(not_equal). | |
| 149 | bin_op(not_member). | |
| 150 | bin_op(partial_bijection). | |
| 151 | bin_op(partial_function). | |
| 152 | bin_op(partial_injection). | |
| 153 | bin_op(partial_surjection). | |
| 154 | bin_op(power_of). | |
| 155 | bin_op(power_of_real). | |
| 156 | bin_op(range_restriction). | |
| 157 | bin_op(range_subtraction). | |
| 158 | bin_op(relations). | |
| 159 | bin_op(restrict_front). | |
| 160 | bin_op(restrict_tail). | |
| 161 | bin_op(set_subtraction). | |
| 162 | bin_op(size). | |
| 163 | bin_op(subset). | |
| 164 | bin_op(subset_strict). | |
| 165 | bin_op(surjection_relation). | |
| 166 | bin_op(total_function). | |
| 167 | bin_op(total_injection). | |
| 168 | bin_op(total_surjection). | |
| 169 | bin_op(total_relation). | |
| 170 | bin_op(total_surjection_relation). | |
| 171 | bin_op(union). | |
| 172 | ||
| 173 | un_op(bag_items). | |
| 174 | un_op(card). | |
| 175 | un_op(closure). % closure1 | |
| 176 | un_op(compaction). | |
| 177 | un_op(convert_bool). | |
| 178 | un_op(convert_real). | |
| 179 | un_op(convert_int_floor). | |
| 180 | un_op(convert_int_ceiling). | |
| 181 | un_op(domain). | |
| 182 | un_op(finite). | |
| 183 | un_op(fin_subset). | |
| 184 | un_op(fin1_subset). | |
| 185 | un_op(first_of_pair). | |
| 186 | un_op(front). | |
| 187 | un_op(identity). | |
| 188 | un_op(iseq). | |
| 189 | un_op(iseq1). | |
| 190 | un_op(negation). | |
| 191 | un_op(max). | |
| 192 | un_op(max_real). | |
| 193 | un_op(min). | |
| 194 | un_op(min_real). | |
| 195 | un_op(mu). | |
| 196 | un_op(perm). | |
| 197 | un_op(pow_subset). | |
| 198 | un_op(pow1_subset). | |
| 199 | un_op(range). | |
| 200 | un_op(rev). | |
| 201 | un_op(reverse). | |
| 202 | un_op(reflexive_closure). | |
| 203 | un_op(second_of_pair). | |
| 204 | un_op(seq). | |
| 205 | un_op(seq1). | |
| 206 | un_op(size). | |
| 207 | un_op(tail). | |
| 208 | un_op(unary_minus). | |
| 209 | un_op(unary_minus_real). | |
| 210 | ||
| 211 | % do not require renaming: | |
| 212 | simple_norm_term(truth). | |
| 213 | simple_norm_term(boolean_true). | |
| 214 | simple_norm_term(boolean_false). | |
| 215 | simple_norm_term(bool_set). | |
| 216 | simple_norm_term(float_set). | |
| 217 | simple_norm_term(real_set). | |
| 218 | simple_norm_term(string_set). | |
| 219 | simple_norm_term(typeset). | |
| 220 | simple_norm_term(value(_)). | |
| 221 | simple_norm_term(string(_)). | |
| 222 | simple_norm_term(empty_set). | |
| 223 | simple_norm_term(empty_sequence). | |
| 224 | simple_norm_term(max_int). | |
| 225 | simple_norm_term(min_int). | |
| 226 | simple_norm_term('NATURAL'). | |
| 227 | simple_norm_term('NATURAL1'). | |
| 228 | simple_norm_term(lazy_lookup_pred(_)). | |
| 229 | simple_norm_term(lazy_lookup_expr(_)). | |
| 230 | simple_norm_term(Nr) :- number(Nr). |