| 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(record_detection,[replace_sets_by_records/2]). | |
| 6 | ||
| 7 | ||
| 8 | :- use_module(tools). | |
| 9 | :- use_module(self_check). | |
| 10 | ||
| 11 | :- use_module(module_information,[module_info/2]). | |
| 12 | :- module_info(group,typechecker). | |
| 13 | :- module_info(description,'This module detects bijections between deferred sets and cartesian products, and compiles them away.'). | |
| 14 | ||
| 15 | ||
| 16 | :- use_module(library(lists)). | |
| 17 | :- use_module(library(ordsets)). | |
| 18 | ||
| 19 | :- use_module(bmachine_structure). | |
| 20 | :- use_module(bsyntaxtree). | |
| 21 | :- use_module(preferences,[get_preference/2]). | |
| 22 | :- use_module(b_ast_cleanup,[clean_up/3]). | |
| 23 | :- use_module(kernel_freetypes,[get_freetype_type_parameters/3]). | |
| 24 | :- use_module(b_global_sets,[register_replaced_global_set/2]). | |
| 25 | ||
| 26 | replace_sets_by_records(Machine,ResultMachine) :- | |
| 27 | % replace until a fixpoint is reached | |
| 28 | ? | replace_sets_by_records2(Machine,RMachine),!, |
| 29 | replace_sets_by_records(RMachine,ResultMachine). | |
| 30 | /* we could do something like this for the values clause for deferred sets mapped to integer intervals: | |
| 31 | it would have to be done for all deferred sets + the problem is that the type checker runs before this code ! | |
| 32 | replace_sets_by_records(Machine,ResultMachine) :- | |
| 33 | bmachine:get_section(values,Machine,Values), | |
| 34 | member(b(values_entry(TID,TVal),_,Info),Values), | |
| 35 | get_texpr_id(TID,Set), | |
| 36 | bmachine:get_section(deferred_sets,Machine,Sets), | |
| 37 | get_texpr_id(TExpr,Set),member(TExpr,Sets), | |
| 38 | get_texpr_type(TVal,Type), | |
| 39 | !, | |
| 40 | Domain = TVal, | |
| 41 | replace_type_in_machine(GlobalSet,Type,Domain,Machine,ResultMachine). | |
| 42 | */ | |
| 43 | replace_sets_by_records(Machine,Machine). | |
| 44 | ||
| 45 | replace_sets_by_records2(Machine,ResultMachine) :- | |
| 46 | get_preference(use_record_construction,true), | |
| 47 | has_deferred_sets(Machine), | |
| 48 | get_section(deferred_sets,Machine,DeferredSets), | |
| 49 | select_section(properties,Properties,NewProperties,Machine,ConsMachine), | |
| 50 | ? | select_constructor_axiom(Properties,DeferredSets,Set,Constructor,Cons,Domain,RestList1), |
| 51 | (debug:debug_mode(on) -> format('Record detected for deferred set ~w~n',[Set]) ; true), | |
| 52 | check_record_construction_ok(Set,Domain), | |
| 53 | replace_sets_by_records3(NewProperties,ConsMachine,Set,Constructor,Cons,Domain,RestList1,ResultMachine). | |
| 54 | ||
| 55 | ||
| 56 | :- use_module(typing_tools,[is_infinite_type/1]). | |
| 57 | :- use_module(specfile,[classical_b_mode/0]). | |
| 58 | :- use_module(error_manager,[add_message/4]). | |
| 59 | check_record_construction_ok(Set,Domain) :- | |
| 60 | ? | classical_b_mode, % classical B |
| 61 | get_texpr_type(Domain,Type), | |
| 62 | is_infinite_type(Type), | |
| 63 | % now we know that we have detected a record | |
| 64 | % Section 5.2.6 of \cite{Abrial:BBook} (page 281) and Section 7.13 of \atelierb{} handbook says that given sets are finite | |
| 65 | !, | |
| 66 | get_preference(disprover_mode,false), % fail in disprover mode for classical B | |
| 67 | ajoin(['Translating deferred set ',Set,' to possibly infinite set (set USE_RECORD_CONSTRUCTION to FALSE to prevent this) : '],Msg), | |
| 68 | add_message(record_detection,Msg,Domain,Domain). | |
| 69 | check_record_construction_ok(_,_). | |
| 70 | ||
| 71 | :- use_module(error_manager,[add_internal_error/2, add_error/4]). | |
| 72 | :- use_module(translate,[print_bexpr/1]). | |
| 73 | replace_sets_by_records3(NewProperties,ConsMachine,Set,Constructor1,Cons,Domain,RestList1,ResultMachine) :- | |
| 74 | Cons = constructor(ConstructorDomain,RecDomainType,_), | |
| 75 | add_texpr_infos(Constructor1,[record_detection(constructor)],Constructor), | |
| 76 | create_constructor_definition(Constructor,ConstructorDomain,ConsDef), | |
| 77 | (debug:debug_mode(on) -> format(' Constructor for ~w: ',[Set]),print_bexpr(ConsDef),nl ; true), %% | |
| 78 | create_recordset_definition(Set,Domain,SetDef), | |
| 79 | (debug:debug_mode(on) -> format(' New definition for ~w: ',[Set]),print_bexpr(SetDef),nl ; true), %% | |
| 80 | create_optional_field_access(Set,Domain,Constructor,RecordFunIds,RestList1,RestList), | |
| 81 | conjunct_predicates([ConsDef,SetDef|RestList],NewProperties), | |
| 82 | move_deferred_set(Set,ConsMachine,SetMachine), | |
| 83 | % replace the constants (constructor,accessors,update functions) by versions that | |
| 84 | % have an info field that indicate their function (needed later to exclude them when | |
| 85 | % adding additional constraints): | |
| 86 | foldl(replace_constant,[Constructor|RecordFunIds],SetMachine,M2), | |
| 87 | %% print(replacing(Set,RecDomainType)),nl, %% | |
| 88 | replace_type_in_machine(Set,RecDomainType,Domain,M2,ResultMachine), | |
| 89 | !, | |
| 90 | register_replaced_global_set(Set,Domain). | |
| 91 | replace_sets_by_records3(NewProperties,ConsMachine,Set,Constructor,Cons,Domain,RestList1,ResultMachine) :- | |
| 92 | add_internal_error('Replacing record failed ',replace_sets_by_records3(NewProperties,ConsMachine,Set,Constructor,Cons,Domain,RestList1,ResultMachine)),fail. | |
| 93 | ||
| 94 | has_deferred_sets(Machine) :- | |
| 95 | get_section(deferred_sets,Machine,DefSets), | |
| 96 | DefSets = [_|_]. | |
| 97 | ||
| 98 | % replace_constant(+NewConstant,+In,-Out): | |
| 99 | % replace a constant by a new one of the same name | |
| 100 | replace_constant(NewConstant,In,Out) :- | |
| 101 | % try the replacement in abstract and concrete constants: | |
| 102 | ( replace_id_in_section(NewConstant,abstract_constants,In,Out) -> true | |
| 103 | ; replace_id_in_section(NewConstant,concrete_constants,In,Out) -> true | |
| 104 | ; add_error(record_detection,'Could not replace constant: ',NewConstant,NewConstant), | |
| 105 | fail | |
| 106 | ). | |
| 107 | replace_id_in_section(NewId,Section,In,Out) :- | |
| 108 | get_texpr_id(NewId,Id), get_texpr_id(OldId,Id), | |
| 109 | select_section(Section,OldIds,NewIds,In,Out), | |
| 110 | selectchk(OldId,OldIds,NewId,NewIds). | |
| 111 | ||
| 112 | % select_constructor_axiom(+Properties,+Sets,-Set,-Constructor,-Cons,-Domain,-RestList) | |
| 113 | % Chooses a constructor axiom if any exists | |
| 114 | % Properties: The properties (a typed predicate) of the machine | |
| 115 | % Sets: The list of deferred sets (a list of typed identifiers) | |
| 116 | % Set,Constructor,Cons,Domain: see is_constructor_axiom/6 below | |
| 117 | % RestList: A list of remaining predicates after removing the constructor axiom | |
| 118 | select_constructor_axiom(Properties,Sets,Set,Constructor,Cons,Domain,RestList) :- | |
| 119 | conjunction_to_list(Properties,PList), | |
| 120 | ? | select(Prop,PList,RestList), |
| 121 | ? | is_constructor_axiom(Prop,Sets,Set,Constructor,Cons,Domain). |
| 122 | ||
| 123 | create_constructor_definition(Constructor,Domain,ConsDef) :- | |
| 124 | create_texpr(equal(Constructor,Identity),pred,[],ConsDef), | |
| 125 | get_texpr_type(Constructor,Type), | |
| 126 | create_texpr(identity(Domain),Type,[],Identity). | |
| 127 | ||
| 128 | create_recordset_definition(SetName,Domain,SetDef) :- | |
| 129 | create_texpr(equal(Set,Domain),pred,[],SetDef), | |
| 130 | get_texpr_type(Domain,Type), | |
| 131 | create_texpr(identifier(SetName),Type,[],Set). | |
| 132 | ||
| 133 | % move_deferred_set(Set+,OldMachine+,NewMachine-) :- | |
| 134 | % Moves a deferred set to the concrete_constants section | |
| 135 | % Set: The (untyped) id of the set | |
| 136 | % OldMachine: The complete B machine where the set is a deferred set | |
| 137 | % NewMachine: The same B machine, but the deferred set is now a constant | |
| 138 | move_deferred_set(Set,OldMachine,NewMachine) :- | |
| 139 | select_section(deferred_sets,Sets,NewSets,OldMachine,Machine1), | |
| 140 | get_texpr_id(TSet,Set), | |
| 141 | selectchk(TSet,Sets,NewSets), | |
| 142 | select_section(concrete_constants,Constants,[TSet|Constants],Machine1,NewMachine). | |
| 143 | ||
| 144 | % is_constructor_axiom(+TAxiom,+Sets,-GType,-TConstructor,-Cons,-TDom) | |
| 145 | % TAxiom: A typed predicate | |
| 146 | % Sets: A list of typed identifiers, the deferred sets | |
| 147 | % GType: The (untyped) ID of the set that represents the record | |
| 148 | % TConstructor: The constructor function (a bijection from a domain to the record type) | |
| 149 | % Cons: a term of the form constructor(Domain,DomainType,Kind) where Kind is either constructor or destructor | |
| 150 | % TDom: The domain of the constructor | |
| 151 | % The constructor can actually be a destructor, i.e. a bijection from the record to the domain. | |
| 152 | % The third argument in the Cons term indicates which case has been encountered | |
| 153 | is_constructor_axiom(TAxiom,Sets,GType,TConstructor,Cons,TDom) :- | |
| 154 | % The axiom has the form c : Dom >->> Set, where | |
| 155 | % c and Set are identifiers | |
| 156 | get_texpr_expr(TAxiom,member(TConstructor,TBijection)), | |
| 157 | get_texpr_type(TConstructor,set(couple(FromType,ToType))), | |
| 158 | get_texpr_id(TConstructor,_), % just make sure that TConstructor is an identifer | |
| 159 | FromType \= ToType, % otherwise bijection maps to itself | |
| 160 | (get_texpr_expr(TBijection,total_bijection(TDom,TSet)), | |
| 161 | Cons=constructor(TDom,FromType,constructor) | |
| 162 | ; get_texpr_expr(TBijection,total_bijection(TSet,TDom)), | |
| 163 | % we have the bijection the other way; does not really matter for a bijection anyway | |
| 164 | Cons = constructor(TSet,ToType,destructor)), | |
| 165 | get_texpr_type(TSet,set(global(GType))), | |
| 166 | get_texpr_id(TSet,GType), | |
| 167 | % check if the set is a deferred set, not an enumerated set | |
| 168 | get_texpr_id(SetTest,GType), | |
| 169 | memberchk(SetTest,Sets), | |
| 170 | % in Dom, there should be no reference to Set | |
| 171 | no_reference(TDom,GType). | |
| 172 | ||
| 173 | ||
| 174 | no_reference(TExpr,Type) :- | |
| 175 | syntaxtraversion(TExpr,Expr,_,_,Subs,_), | |
| 176 | no_reference2(Expr,Type), | |
| 177 | no_reference_l(Subs,Type). | |
| 178 | no_reference2(identifier(Type),Type) :- !,fail. | |
| 179 | no_reference2(_,_). | |
| 180 | no_reference_l([],_). | |
| 181 | no_reference_l([Expr|Rest],Type) :- | |
| 182 | no_reference(Expr,Type), | |
| 183 | no_reference_l(Rest,Type). | |
| 184 | ||
| 185 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 186 | create_optional_field_access(SetName,Domain,Constructor,UpAc,Properties,RestList) :- | |
| 187 | get_texpr_id(Set,SetName), | |
| 188 | find_and_remove_field_declaration(Set,Domain,Constructor,Fields,Properties,P4), | |
| 189 | !, | |
| 190 | replace_update_definitions(Fields,Set,Constructor,Updates,P4,P5), | |
| 191 | maplist(create_field_definition(Domain),Fields,Accessors,FieldDefs), | |
| 192 | append(FieldDefs,P5,RestList), | |
| 193 | % A list of identifiers that are used at update and accessor functions: | |
| 194 | append(Updates,Accessors,UpAc). | |
| 195 | create_optional_field_access(_Set,_Domain,_Constructor,[],Properties,Properties). | |
| 196 | ||
| 197 | find_and_remove_field_declaration(Set,Domain,Constructor,Fields,Pin,Pout) :- | |
| 198 | % F1 >< ... >< Fn : Set -->> Domain | |
| 199 | bsyntax_pattern(member(FieldProduct,total_surjection(-Set,-Domain)), SurjMemb), | |
| 200 | selectchk(SurjMemb,Pin,P1), | |
| 201 | % the injection is only defined for closed records | |
| 202 | % (F1 >< ...) >< Fn : Set >-> Domain | |
| 203 | bsyntax_pattern(member(-FieldProduct,total_injection(-Set,-Domain)), InjMemb), | |
| 204 | selectchk(InjMemb,P1,P2), | |
| 205 | access_locations(FieldProduct,Domain,Fields), | |
| 206 | % for each field accessor fx, there should be a declaration | |
| 207 | % fx : Record --> Domain, remove them | |
| 208 | remove_field_declarations(Fields,Set,P2,P3), | |
| 209 | % for each field accessor fx, there should be a predicate | |
| 210 | % !(v1,...,...), remove it | |
| 211 | remove_field_quantifiers(Fields,Constructor,P3,Pout). | |
| 212 | ||
| 213 | % find the field accessor functions | |
| 214 | access_locations(TExpr,TDomain,Fields) :- | |
| 215 | access_locations1(TExpr,TDomain,[],Fields). | |
| 216 | access_locations1(TExpr,TDomain,Path,Fields) :- | |
| 217 | get_texpr_expr(TExpr,Expr), | |
| 218 | access_locations2(Expr,TExpr,TDomain,Path,Fields). | |
| 219 | access_locations2(identifier(_Id),TExpr,TDomain,Path,[fieldloc(TExpr,TDomain,RPath)]) :- reverse(Path,RPath). | |
| 220 | access_locations2(direct_product(F1,F2),_TExpr,TCart,Path,Fields) :- | |
| 221 | get_texpr_expr(TCart,cartesian_product(D1,D2)), | |
| 222 | access_locations1(F1,D1,[left |Path],Fields1), | |
| 223 | access_locations1(F2,D2,[right|Path],Fields2), | |
| 224 | append(Fields1,Fields2,Fields). | |
| 225 | ||
| 226 | create_field_definition(RecordDomain,fieldloc(AccessorId1,Domain,Path),AccessorId,Equal) :- | |
| 227 | add_texpr_infos(AccessorId1,[record_detection(accessor)],AccessorId), | |
| 228 | create_texpr(equal(AccessorId,AccessorDef),pred,[],Equal), | |
| 229 | % the accessor function maps a record to the domain | |
| 230 | get_texpr_type(RecordDomain,set(RecordTupleType)), | |
| 231 | create_accessor_function(Domain,Path,RecordTupleType,AccessorDef). | |
| 232 | ||
| 233 | create_accessor_function(Domain,Path,RecordTupleType,AccessDefinition) :- | |
| 234 | % fieldAccess = {r,v | v = prj...(r)} | |
| 235 | create_texpr(identifier(r),RecordTupleType,[],RecordVar), | |
| 236 | get_texpr_type(Domain,set(FieldType)), | |
| 237 | create_texpr(identifier(v),FieldType,[],ValueVar), | |
| 238 | create_texpr(equal(ValueVar,Projection),pred,[],Equals), | |
| 239 | create_projection(Path,RecordVar,Projection), | |
| 240 | %translate:print_bexpr(Projection),nl, | |
| 241 | create_symbolic_comprehension_set([RecordVar,ValueVar],Equals, | |
| 242 | [record_detection(accessor)],AccessDefinition). | |
| 243 | ||
| 244 | create_symbolic_comprehension_set(Ids,Pred,Info,Result) :- | |
| 245 | create_comprehension_set(Ids,Pred,Info,CompSet), | |
| 246 | mark_bexpr_as_symbolic(CompSet,Result). | |
| 247 | ||
| 248 | create_projection(Path,RecordVar,ProjectionResult) :- | |
| 249 | get_texpr_type(RecordVar,InnerType), | |
| 250 | create_projection_aux(Path,InnerType,RecordVar,ProjectionResult). | |
| 251 | ||
| 252 | create_projection_aux([],_InnerType,SubExpression,SubExpression). % return record as is | |
| 253 | create_projection_aux([Loc|Path],couple(A,B),SubExpression,ProjectionResult) :- | |
| 254 | ( Loc==left -> Expr=first_of_pair(SubExpression), InnerType=A | |
| 255 | ; Loc==right -> Expr=second_of_pair(SubExpression),InnerType=B), | |
| 256 | create_texpr(Expr,InnerType,[],NewSubExpression), | |
| 257 | create_projection_aux(Path,InnerType,NewSubExpression,ProjectionResult). | |
| 258 | ||
| 259 | ||
| 260 | % remove fieldx : RecSet --> Domx | |
| 261 | remove_field_declarations([],_RecSet,Predicates,Predicates). | |
| 262 | remove_field_declarations([fieldloc(AccessorId,Domain,_Path)|Frest],RecSet,Pin,Pout) :- | |
| 263 | remove_field_declaration(AccessorId,Domain,RecSet,Pin,Pinter), | |
| 264 | remove_field_declarations(Frest,RecSet,Pinter,Pout). | |
| 265 | remove_field_declaration(AccessorId,Domain,RecSet,Pin,Pout) :- | |
| 266 | bsyntax_pattern(member(-AccessorId,total_function(-RecSet,-Domain)),Pattern), | |
| 267 | selectchk(Pattern,Pin,Pout). | |
| 268 | ||
| 269 | % remove !(f1,...,fn). ( f1:T1 & ... & fn:Tn => fieldx(make_rec(f1|->f2|->f3)) = fx) | |
| 270 | remove_field_quantifiers(Fields,Constructor,Pin,Pout) :- | |
| 271 | remove_field_quantifiers2(Fields,0,Constructor,Pin,Pout). | |
| 272 | ||
| 273 | remove_field_quantifiers2(Fields,N,Constructor,Pin,Pout) :- | |
| 274 | ( nth0(N,Fields,fieldloc(Field,_Dom,_Path)) -> | |
| 275 | remove_field_quantifier(Field,N,Fields,Constructor,Pin,Pinter), | |
| 276 | N2 is N+1, | |
| 277 | remove_field_quantifiers2(Fields,N2,Constructor,Pinter,Pout) | |
| 278 | ; | |
| 279 | Pin=Pout). | |
| 280 | remove_field_quantifier(Field,N,Fields,Constructor,Pin,Pout) :- | |
| 281 | make_field_identifiers(Fields,FSkels), | |
| 282 | get_texpr_ids(FSkels,Ids), | |
| 283 | nth0(N,FSkels,Ref), | |
| 284 | bsyntax_pattern(forall(FSkels,_,equal(function(-Field,function(-Constructor,ConstArg)),-Ref)),ForAll), | |
| 285 | select(ForAll,Pin,Pout), | |
| 286 | are_mappings(ConstArg,Ids),!. | |
| 287 | are_mappings(TExpr,Ids) :- | |
| 288 | are_mappings2(TExpr,Ids,[]). | |
| 289 | are_mappings2(TExpr) --> | |
| 290 | {get_texpr_expr(TExpr,Expr)}, | |
| 291 | are_mappings3(Expr). | |
| 292 | are_mappings3(identifier(Id)) --> [Id]. | |
| 293 | are_mappings3(couple(A,B)) --> | |
| 294 | are_mappings2(A), | |
| 295 | are_mappings2(B). | |
| 296 | ||
| 297 | make_field_identifiers([],[]). | |
| 298 | make_field_identifiers([FieldAcc|FRest],[Id|Irest]) :- | |
| 299 | make_field_identifier(FieldAcc,Id), | |
| 300 | make_field_identifiers(FRest,Irest). | |
| 301 | make_field_identifier(fieldloc(FieldAcc,_,_),Id) :- | |
| 302 | get_texpr_type(FieldAcc,set(couple(_,FType))), | |
| 303 | create_texpr(identifier(_),FType,_,Id). | |
| 304 | ||
| 305 | replace_update_definitions(Fields,RecSet,Constructor,Updates,Pin,Pout) :- | |
| 306 | replace_update_definitions2(Fields,Fields,RecSet,Constructor,Updates,Pin,Pout). | |
| 307 | replace_update_definitions2([],_Fields,_RecSet,_Constructor,[],Predicates,Predicates). | |
| 308 | replace_update_definitions2([fieldloc(AccessorId,FDomain,Path)|Frest],Fields,RecSet, | |
| 309 | Constructor,[UpdateId|URest],Pin,Pout) :- | |
| 310 | replace_update_definition(AccessorId,FDomain,Path,Fields,RecSet,Constructor,UpdateId,Pin,Pinter), | |
| 311 | replace_update_definitions2(Frest,Fields,RecSet,Constructor,URest,Pinter,Pout). | |
| 312 | ||
| 313 | % Identify two predicates of the form | |
| 314 | % updatex : Record ** Domain --> Record | |
| 315 | % !(Rec,New).(_ => updatex(Rec,New) = Constructor(..)) | |
| 316 | % and replace them by | |
| 317 | % updatex = {i,o | #(n,f1,...,fn).(i=(f1,...,fn)|->n & o=(f1,...,n,..,fn))} | |
| 318 | replace_update_definition(FieldAccessorId,FieldDomain,Path,Fields, | |
| 319 | RecSet,Constructor,Update,Pin,[Equal|Pout]) :- | |
| 320 | % Updatex : Record ** Domain --> Record | |
| 321 | bsyntax_pattern(member(Update1,total_function(cartesian_product(-RecSet,-FieldDomain),-RecSet)),Memb), | |
| 322 | select(Memb,Pin,P1), | |
| 323 | % !(Rec,New).(_ => Updatex(Rec,New) = Constructor(..)) | |
| 324 | % TODO: Implication and constructor arguments are missing | |
| 325 | bsyntax_pattern(forall([Rec,New],_,equal(function(-Update1,couple(-Rec,-New)), | |
| 326 | function(-Constructor,_))), ForAll), | |
| 327 | select(ForAll,P1,Pout), | |
| 328 | !, | |
| 329 | add_texpr_infos(Update1,[record_detection(update)],Update), | |
| 330 | % Updatex = {i,o | #(i,r,f1,...,fn).(i=r|->n & ) } | |
| 331 | create_texpr(equal(Update,Function),pred,[],Equal), | |
| 332 | create_update_function(FieldAccessorId,FieldDomain,Path,Fields,Function). | |
| 333 | ||
| 334 | create_update_function(FieldAccessorId,FieldDomain,Path,Fields,Function) :- | |
| 335 | % {i,o | #n,f1,...,fn. ( i=( (f1,...,fn) |-> n ) ) & o=(f1,...,n,...,fn) } | |
| 336 | get_texpr_type(FieldAccessorId,set(couple(RecType,FieldType))), | |
| 337 | InType = couple(RecType,FieldType), | |
| 338 | create_texpr(identifier(update__in),InType,[],In), | |
| 339 | create_texpr(identifier(update__out),RecType,[],Out), | |
| 340 | create_symbolic_comprehension_set([In,Out],Pred,[record_detection(update)],CompSet), | |
| 341 | ||
| 342 | % #(n,f1,...,fn).(...&...) | |
| 343 | %create_exists([NewValue|FieldVars],ExistsPred,Pred), % moved below; see comment | |
| 344 | create_var_for_field(FieldAccessorId,FieldDomain,'f$n__',NewValue), | |
| 345 | maplist(create_field_var,Fields,FieldVars), | |
| 346 | create_texpr(conjunct(InEqual,OutEqual),pred,[],ExistsPred), | |
| 347 | ||
| 348 | % i = ( (f1,...,fn) |-> n ) | |
| 349 | create_texpr(equal(In,InPair),pred,[],InEqual), | |
| 350 | create_texpr(couple(OldFields,NewValue),InType,[],InPair), | |
| 351 | create_record_tuple(Fields,FieldVars,OldFields), | |
| 352 | ||
| 353 | % o = (f1,...,n,...,fn) | |
| 354 | create_texpr(equal(Out,NewFields),pred,[],OutEqual), | |
| 355 | update_record_tuple(Path,NewValue,OldFields,NewFields), | |
| 356 | ||
| 357 | % the creation of the exists has to be deferred until here as used identifiers are computed: | |
| 358 | create_exists([NewValue|FieldVars],ExistsPred,Pred), | |
| 359 | %translate:print_bexpr(CompSet),nl, | |
| 360 | ||
| 361 | % we need to call the clean-up functions because exists(...) needs more | |
| 362 | % information about which identifier are used and that information | |
| 363 | % is added by clean_up/3. | |
| 364 | clean_up(CompSet,[],Function). | |
| 365 | ||
| 366 | % for a fields, create an identifier with the corresponding type | |
| 367 | create_field_var(fieldloc(AccessorId,Domain,_Path),TId) :- | |
| 368 | create_var_for_field(AccessorId,Domain,'f$__',TId). | |
| 369 | create_var_for_field(AccessorId,Domain,Prefix,TId) :- | |
| 370 | get_texpr_id(AccessorId,FId), | |
| 371 | get_texpr_type(Domain,set(Type)), | |
| 372 | atom_concat(Prefix,FId,VId), | |
| 373 | create_texpr(identifier(VId),Type,[],TId). | |
| 374 | ||
| 375 | % for a list of fields and identifiers f1,...,fn, create a tuple (f1,...,fn) | |
| 376 | create_record_tuple([],[],_). | |
| 377 | create_record_tuple([fieldloc(_,_,Path)|Frest],[FieldVar|Vrest],Tuple) :- | |
| 378 | create_record_tuple2(Path,FieldVar,Tuple), | |
| 379 | create_record_tuple(Frest,Vrest,Tuple). | |
| 380 | create_record_tuple2([],Expr,Expr). | |
| 381 | create_record_tuple2([Loc|Path],Expr,Tuple) :- | |
| 382 | ( Loc==left -> create_texpr(couple(Sub,_),couple(SubType,_),[],Tuple) | |
| 383 | ; Loc==right -> create_texpr(couple(_,Sub),couple(_,SubType),[],Tuple)), | |
| 384 | get_texpr_type(Sub,SubType), | |
| 385 | create_record_tuple2(Path,Expr,Sub). | |
| 386 | ||
| 387 | % in a tuple representing a record, replace one field | |
| 388 | update_record_tuple([],NewValue,_OldFields,NewValue). | |
| 389 | update_record_tuple([Loc|Path],NewValue,OldFields,NewFields) :- | |
| 390 | get_texpr_expr(OldFields,couple(A,B)), | |
| 391 | get_texpr_type(OldFields,Type), | |
| 392 | create_texpr(couple(X,Y),Type,[],NewFields), | |
| 393 | ( Loc==left -> X=NewSub,A=OldSub,Y=B | |
| 394 | ; Loc==right -> Y=NewSub,B=OldSub,X=A), | |
| 395 | update_record_tuple(Path,NewValue,OldSub,NewSub). | |
| 396 | ||
| 397 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 398 | % replace_type_in_machine(+T1,+T2,+Domain,+OldMachine,-NewMachine): | |
| 399 | % T1: The name of the global set that refers to the old type | |
| 400 | % T2: The new type that should replace global(T1) | |
| 401 | % Domain: A B expression that describes the domain of the record, used to | |
| 402 | % constrain introduced identifiers | |
| 403 | % OldMachine: The B machine before replacement | |
| 404 | % NewMachine: The resulting B machine | |
| 405 | replace_type_in_machine(T1,T2,Domain,OldMachine,NewMachine) :- | |
| 406 | extract_constants_that_are_types(OldMachine,RTT), | |
| 407 | (is_just_type(Domain,RTT) -> Domain2 = simple ; Domain2 = Domain), | |
| 408 | % add predicates to constrain variables or constants, if needed | |
| 409 | foldl(add_type_constraint_to_section(T1,Domain2), | |
| 410 | [decl([abstract_constants,concrete_constants],properties), | |
| 411 | decl([abstract_variables,concrete_variables],invariant)], | |
| 412 | OldMachine,Machine1), | |
| 413 | % replace the type in the expressions of the machine (identifier declarations | |
| 414 | % can be treated as expressions, too) | |
| 415 | foldl(replace_type_in_machine2(T1,T2,Domain2), | |
| 416 | [abstract_constants,concrete_constants, | |
| 417 | abstract_variables,concrete_variables, | |
| 418 | promoted, unpromoted, | |
| 419 | constraints, properties, invariant, assertions, | |
| 420 | initialisation, operation_bodies], | |
| 421 | Machine1,NewMachine). | |
| 422 | replace_type_in_machine2(T1,T2,Domain,Sec,In,Out) :- | |
| 423 | select_section_texprs(Sec,Old,New,In,Out), | |
| 424 | replace_type_in_exprs(Old,T1,T2,Domain,New). | |
| 425 | replace_type_in_expr(TExpr,T1,T2,Domain,New) :- | |
| 426 | % if identifiers (e.g. i) are declared in an expression (like in forall), we may have | |
| 427 | % to add an predicate (e.g. i:1..4) | |
| 428 | ( Domain=simple -> % the domain is a whole type, no additional constraint needed | |
| 429 | TExpr2 = TExpr | |
| 430 | ; has_declared_identifier(TExpr,Ids),contains_identifier_with_type(Ids,T1) -> | |
| 431 | % identifiers are introduced and one of them contains the record type | |
| 432 | add_type_declarations(TExpr,global(T1),Domain,Ids,TExpr2) | |
| 433 | ; % no identifiers introduced that use the record type | |
| 434 | TExpr = TExpr2 | |
| 435 | ), | |
| 436 | create_texpr(Expr,EType,Info,TExpr2), % de-assemble old expression | |
| 437 | replace_type(EType,T1,T2,NType), % replace type global(T1) by T2 in Type | |
| 438 | create_texpr(NExpr2,NType,Info,New), % assemble new expression with new type | |
| 439 | syntaxtransformation(Expr,Subs,_Names,NSubs,NExpr1), % continue with sub-expressions | |
| 440 | replace_type_in_exprs(Subs,T1,T2,Domain,NSubs), | |
| 441 | replace_hidden_type_paras(NExpr1,T1,T2,NExpr2). | |
| 442 | replace_type_in_exprs([],_T1,_T2,_Domain,[]). | |
| 443 | replace_type_in_exprs([Sub|Irest],T1,T2,Domain,[NSub|Orest]) :- | |
| 444 | replace_type_in_expr(Sub,T1,T2,Domain,NSub), | |
| 445 | replace_type_in_exprs(Irest,T1,T2,Domain,Orest). | |
| 446 | ||
| 447 | ||
| 448 | replace_hidden_type_paras(freetype_constructor(A,Case,Expr),T1,T2,freetype_constructor(RA,Case,Expr)) :- !, | |
| 449 | replace_freetype_paras(A,T1,T2,RA). | |
| 450 | replace_hidden_type_paras(freetype_destructor(A,Case,Expr),T1,T2,freetype_destructor(RA,Case,Expr)) :- !, | |
| 451 | replace_freetype_paras(A,T1,T2,RA). | |
| 452 | replace_hidden_type_paras(E,_,_,E). | |
| 453 | ||
| 454 | ||
| 455 | contains_identifier_with_type(Ids,T1) :- | |
| 456 | get_texpr_type(TId,Type), | |
| 457 | member(TId,Ids), | |
| 458 | contains_type(global(T1),Type). | |
| 459 | ||
| 460 | add_type_constraint_to_section(_ToReplace,simple,_Decl,In,Out) :- | |
| 461 | !,In=Out. | |
| 462 | add_type_constraint_to_section(ToReplace,Domain,decl(IdSecs,PredSec),In,Out) :- | |
| 463 | maplist(aux_get_section(In),IdSecs,IdsL),append(IdsL,Ids1), | |
| 464 | % do not add constraints for accessor and update functions for records: | |
| 465 | exclude(is_record_detection_expr,Ids1,Ids), | |
| 466 | ( contains_identifier_with_type(Ids,ToReplace) -> | |
| 467 | create_type_predicate(global(ToReplace),Domain,Ids,P), | |
| 468 | ( is_truth(P) -> In=Out % Trivial, nothing to do | |
| 469 | ; % Add the type constraint to the relevant predicate section | |
| 470 | select_section(PredSec,OldPred,NewPred,In,Out), | |
| 471 | conjunct_predicates([P,OldPred],NewPred) | |
| 472 | ) | |
| 473 | ; % Not applicable, nothing to do | |
| 474 | In=Out). | |
| 475 | aux_get_section(Machine,Sec,Content) :- % just to rearrange the parameters | |
| 476 | get_section(Sec,Machine,Content). | |
| 477 | ||
| 478 | is_record_detection_expr(Expr) :- | |
| 479 | get_texpr_info(Expr,Info),memberchk(record_detection(_),Info). | |
| 480 | ||
| 481 | replace_type(global(Type),Type,NewType,Result) :- !, NewType=Result. | |
| 482 | replace_type(couple(A,B),T1,T2,couple(RA,RB)) :- | |
| 483 | !, replace_type(A,T1,T2,RA), replace_type(B,T1,T2,RB). | |
| 484 | replace_type(set(A),T1,T2,set(RA)) :- | |
| 485 | !, replace_type(A,T1,T2,RA). | |
| 486 | replace_type(seq(A),T1,T2,seq(RA)) :- | |
| 487 | !, replace_type(A,T1,T2,RA). | |
| 488 | replace_type(freetype(A),T1,T2,freetype(RA)) :- | |
| 489 | !, replace_freetype_paras(A,T1,T2,RA). | |
| 490 | replace_type(T,_,_,T). % just skip types like integer, string, etc. | |
| 491 | ||
| 492 | % replace type inside freetype type parameters (relevant for Event-B polymorphic theories) | |
| 493 | replace_freetype_paras(A,T1,T2,RA) :- | |
| 494 | get_freetype_type_parameters(A,Func,TypeParas), | |
| 495 | maplist(mreplace(T1,T2),TypeParas,NewTypeParas), | |
| 496 | get_freetype_type_parameters(RA,Func,NewTypeParas). | |
| 497 | ||
| 498 | mreplace(T1,T2,Type,ReplacedType) :- replace_type(Type,T1,T2,ReplacedType). | |
| 499 | ||
| 500 | contains_type(Type,couple(A,_)) :- contains_type(Type,A). | |
| 501 | contains_type(Type,couple(_,B)) :- contains_type(Type,B). | |
| 502 | contains_type(Type,set(A)) :- contains_type(Type,A). | |
| 503 | contains_type(Type,seq(A)) :- contains_type(Type,A). | |
| 504 | contains_type(Type,freetype(A)) :- get_freetype_type_parameters(A,_,TypeParas), | |
| 505 | member(TP,TypeParas), contains_type(Type,TP). | |
| 506 | contains_type(Type,Type). | |
| 507 | ||
| 508 | add_type_declarations(TExpr,ToReplace,Set,Ids,Result) :- | |
| 509 | create_type_predicate(ToReplace,Set,Ids,P), | |
| 510 | ( is_truth(P) -> Result = TExpr % Nothing to do | |
| 511 | ; add_declaration_for_identifier(TExpr,P,Result)). | |
| 512 | ||
| 513 | create_type_predicate(ToReplace,Set,Ids,P) :- | |
| 514 | include(expr_contains_type(ToReplace),Ids,RelevantIds), | |
| 515 | maplist(create_type_membership(ToReplace,Set),RelevantIds,Preds), | |
| 516 | conjunct_predicates(Preds,P1), | |
| 517 | clean_up(P1,[],P). | |
| 518 | ||
| 519 | expr_contains_type(ToReplace,TExpr) :- | |
| 520 | get_texpr_type(TExpr,Type), | |
| 521 | contains_type(ToReplace,Type). | |
| 522 | ||
| 523 | create_type_membership(ToReplace,Set,TId,Membership) :- | |
| 524 | get_texpr_type(TId,Type), | |
| 525 | create_set_for_type(Type,ToReplace,Set,GenSet), | |
| 526 | create_texpr(member(TId,GenSet),pred,[],Membership). | |
| 527 | ||
| 528 | create_set_for_type(T,ToReplace,Set,R) :- | |
| 529 | T=ToReplace,!,R=Set. | |
| 530 | create_set_for_type(couple(A,B),ToReplace,Set,R) :- !, | |
| 531 | create_set_for_type(A,ToReplace,Set,SA), | |
| 532 | create_set_for_type(B,ToReplace,Set,SB), | |
| 533 | ( is_typeset(SA),is_typeset(SB) -> create_typeset(couple(A,B),R) | |
| 534 | ; create_texpr(cartesian_product(SA,SB),set(couple(A,B)),[],R)). | |
| 535 | create_set_for_type(set(A),ToReplace,Set,R) :- !, | |
| 536 | create_set_for_type(A,ToReplace,Set,SA), | |
| 537 | ( is_typeset(SA) -> create_typeset(set(A),R) | |
| 538 | ; create_texpr(pow_subset(SA),set(set(A)),[],R)). | |
| 539 | create_set_for_type(seq(A),ToReplace,Set,R) :- !, | |
| 540 | % for our purpose, we can ignore other constraints on sequences | |
| 541 | create_set_for_type(set(couple(integer,A)),ToReplace,Set,R). | |
| 542 | create_set_for_type(Type,_ToReplace,_Set,R) :- create_typeset(Type,R). | |
| 543 | is_typeset(Expr) :- get_texpr_expr(Expr,typeset). | |
| 544 | ||
| 545 | create_typeset(Type,Set) :- | |
| 546 | create_texpr(typeset,set(Type),[],Set). | |
| 547 | ||
| 548 | % extract_constants_that_are_types(+Machine,-RTT): | |
| 549 | % gives a list of identifiers of those constants that are defined to be the whole type. | |
| 550 | % This works only for constants that are defined with an equality, e.g. | |
| 551 | % c = BOOL**BOOL | |
| 552 | extract_constants_that_are_types(Machine,RTT) :- | |
| 553 | get_all_equalities_from_machine(Machine,Equalities), | |
| 554 | extract_type_references(Equalities,[],RTT). | |
| 555 | % get_all_equalities_from_properties(+Machine,-Equalities): | |
| 556 | % extract all equalities from the properties. | |
| 557 | % Equalities is a list of terms equal(Id,Expr) where Id denotes a | |
| 558 | % constant and Expr the expr on the other side of the equation. | |
| 559 | get_all_equalities_from_machine(Machine,Equalities) :- | |
| 560 | get_all_constants_from_machine(Machine,Constants), | |
| 561 | get_section(properties,Machine,Properties), | |
| 562 | conjunction_to_list(Properties,PList), | |
| 563 | convlist(is_equality_left(Constants), PList,LEqualities), | |
| 564 | convlist(is_equality_right(Constants),PList,REqualities), | |
| 565 | append(LEqualities,REqualities,Equalities). | |
| 566 | get_all_constants_from_machine(Machine,Constants) :- | |
| 567 | get_section(abstract_constants,Machine,AC), | |
| 568 | get_section(concrete_constants,Machine,CC), | |
| 569 | append(AC,CC,Constants). | |
| 570 | % extract_type_references(+Equalities,+RTT,-Result): | |
| 571 | % Equalities: A list of term of the form equal(Id,Expr), see get_all_equalities_from_properties/2 | |
| 572 | % RTT: An ordered list of already known constants that refer to types | |
| 573 | % Result: A ordered list of constants (their id, no types) that refer to types | |
| 574 | % The predicate works recursively because a definition like a = B**INTEGER can denote a | |
| 575 | % type if B also denotes a type which must be detected first. | |
| 576 | extract_type_references(Equalities,RTT,Result) :- | |
| 577 | convlist(equality_is_typedef(RTT),Equalities,ReferencesToTypes), | |
| 578 | list_to_ord_set(ReferencesToTypes,Sorted), | |
| 579 | ord_subtract(Sorted,RTT,Unique), | |
| 580 | ( Unique = [] -> Result=RTT % no new definitions found | |
| 581 | ; % new definitions found, continue recursively | |
| 582 | ord_union(Unique,RTT,NewRTT), | |
| 583 | extract_type_references(Equalities,NewRTT,Result) | |
| 584 | ). | |
| 585 | % Pred is of form Id=Expr where Id is a constant | |
| 586 | is_equality_left(Constants,Pred,equal(Id,Expr)) :- | |
| 587 | get_texpr_expr(Pred,equal(TId,Expr)), is_equality_aux(TId,Constants,Id). | |
| 588 | % Pred is of form Expr=Id where Id is a constant | |
| 589 | is_equality_right(Constants,Pred,equal(Id,Expr)) :- | |
| 590 | get_texpr_expr(Pred,equal(Expr,TId)), is_equality_aux(TId,Constants,Id). | |
| 591 | is_equality_aux(TId,Constants,Id) :- | |
| 592 | get_texpr_id(TId,Id),get_texpr_id(Constant,Id),memberchk(Constant,Constants). | |
| 593 | equality_is_typedef(RTT,equal(Id,Expr),Id) :- | |
| 594 | is_just_type(Expr,RTT). |