| 1 | | % (c) 2009-2026 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 | | :- use_module(bsyntaxtree,[is_set_type/2]). |
| 145 | | |
| 146 | | % is_constructor_axiom(+TAxiom,+Sets,-GType,-TConstructor,-Cons,-TDom) |
| 147 | | % TAxiom: A typed predicate |
| 148 | | % Sets: A list of typed identifiers, the deferred sets |
| 149 | | % GType: The (untyped) ID of the set that represents the record |
| 150 | | % TConstructor: The constructor function (a bijection from a domain to the record type) |
| 151 | | % Cons: a term of the form constructor(Domain,DomainType,Kind) where Kind is either constructor or destructor |
| 152 | | % TDom: The domain of the constructor |
| 153 | | % The constructor can actually be a destructor, i.e. a bijection from the record to the domain. |
| 154 | | % The third argument in the Cons term indicates which case has been encountered |
| 155 | | is_constructor_axiom(TAxiom,Sets,GType,TConstructor,Cons,TDom) :- |
| 156 | | % The axiom has the form c : Dom >->> Set, where |
| 157 | | % c and Set are identifiers |
| 158 | | get_texpr_expr(TAxiom,member(TConstructor,TBijection)), |
| 159 | | get_texpr_type(TConstructor,SetType), |
| 160 | | is_set_type(SetType,couple(FromType,ToType)), |
| 161 | | get_texpr_id(TConstructor,_), % just make sure that TConstructor is an identifer |
| 162 | | FromType \= ToType, % otherwise bijection maps to itself |
| 163 | | (get_texpr_expr(TBijection,total_bijection(TDom,TSet)), |
| 164 | | Cons=constructor(TDom,FromType,constructor) |
| 165 | | ; get_texpr_expr(TBijection,total_bijection(TSet,TDom)), |
| 166 | | % we have the bijection the other way; does not really matter for a bijection anyway |
| 167 | | Cons = constructor(TSet,ToType,destructor)), |
| 168 | | get_texpr_type(TSet,set(global(GType))), |
| 169 | | get_texpr_id(TSet,GType), |
| 170 | | % check if the set is a deferred set, not an enumerated set |
| 171 | | get_texpr_id(SetTest,GType), |
| 172 | | memberchk(SetTest,Sets), |
| 173 | | % in Dom, there should be no reference to Set |
| 174 | | no_reference(TDom,GType). |
| 175 | | |
| 176 | | |
| 177 | | no_reference(TExpr,Type) :- |
| 178 | | syntaxtraversion(TExpr,Expr,_,_,Subs,_), |
| 179 | | no_reference2(Expr,Type), |
| 180 | | no_reference_l(Subs,Type). |
| 181 | | no_reference2(identifier(Type),Type) :- !,fail. |
| 182 | | no_reference2(_,_). |
| 183 | | no_reference_l([],_). |
| 184 | | no_reference_l([Expr|Rest],Type) :- |
| 185 | | no_reference(Expr,Type), |
| 186 | | no_reference_l(Rest,Type). |
| 187 | | |
| 188 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 189 | | create_optional_field_access(SetName,Domain,Constructor,UpAc,Properties,RestList) :- |
| 190 | | get_texpr_id(Set,SetName), |
| 191 | | find_and_remove_field_declaration(Set,Domain,Constructor,Fields,Properties,P4), |
| 192 | | !, |
| 193 | | replace_update_definitions(Fields,Set,Constructor,Updates,P4,P5), |
| 194 | | maplist(create_field_definition(Domain),Fields,Accessors,FieldDefs), |
| 195 | | append(FieldDefs,P5,RestList), |
| 196 | | % A list of identifiers that are used at update and accessor functions: |
| 197 | | append(Updates,Accessors,UpAc). |
| 198 | | create_optional_field_access(_Set,_Domain,_Constructor,[],Properties,Properties). |
| 199 | | |
| 200 | | find_and_remove_field_declaration(Set,Domain,Constructor,Fields,Pin,Pout) :- |
| 201 | | % F1 >< ... >< Fn : Set -->> Domain |
| 202 | | bsyntax_pattern(member(FieldProduct,total_surjection(-Set,-Domain)), SurjMemb), |
| 203 | | selectchk(SurjMemb,Pin,P1), |
| 204 | | % the injection is only defined for closed records |
| 205 | | % (F1 >< ...) >< Fn : Set >-> Domain |
| 206 | | bsyntax_pattern(member(-FieldProduct,total_injection(-Set,-Domain)), InjMemb), |
| 207 | | selectchk(InjMemb,P1,P2), |
| 208 | | access_locations(FieldProduct,Domain,Fields), |
| 209 | | % for each field accessor fx, there should be a declaration |
| 210 | | % fx : Record --> Domain, remove them |
| 211 | | remove_field_declarations(Fields,Set,P2,P3), |
| 212 | | % for each field accessor fx, there should be a predicate |
| 213 | | % !(v1,...,...), remove it |
| 214 | | remove_field_quantifiers(Fields,Constructor,P3,Pout). |
| 215 | | |
| 216 | | % find the field accessor functions |
| 217 | | access_locations(TExpr,TDomain,Fields) :- |
| 218 | | access_locations1(TExpr,TDomain,[],Fields). |
| 219 | | access_locations1(TExpr,TDomain,Path,Fields) :- |
| 220 | | get_texpr_expr(TExpr,Expr), |
| 221 | | access_locations2(Expr,TExpr,TDomain,Path,Fields). |
| 222 | | access_locations2(identifier(_Id),TExpr,TDomain,Path,[fieldloc(TExpr,TDomain,RPath)]) :- reverse(Path,RPath). |
| 223 | | access_locations2(direct_product(F1,F2),_TExpr,TCart,Path,Fields) :- |
| 224 | | get_texpr_expr(TCart,cartesian_product(D1,D2)), |
| 225 | | access_locations1(F1,D1,[left |Path],Fields1), |
| 226 | | access_locations1(F2,D2,[right|Path],Fields2), |
| 227 | | append(Fields1,Fields2,Fields). |
| 228 | | |
| 229 | | create_field_definition(RecordDomain,fieldloc(AccessorId1,Domain,Path),AccessorId,Equal) :- |
| 230 | | add_texpr_infos(AccessorId1,[record_detection(accessor)],AccessorId), |
| 231 | | create_texpr(equal(AccessorId,AccessorDef),pred,[],Equal), |
| 232 | | % the accessor function maps a record to the domain |
| 233 | | get_texpr_type(RecordDomain,RType), |
| 234 | | is_set_type(RType,RecordTupleType), |
| 235 | | create_accessor_function(Domain,Path,RecordTupleType,AccessorDef). |
| 236 | | |
| 237 | | create_accessor_function(Domain,Path,RecordTupleType,AccessDefinition) :- |
| 238 | | % fieldAccess = {r,v | v = prj...(r)} |
| 239 | | create_texpr(identifier(r),RecordTupleType,[],RecordVar), |
| 240 | | get_texpr_type(Domain,FType), |
| 241 | | is_set_type(FType,FieldType), |
| 242 | | create_texpr(identifier(v),FieldType,[],ValueVar), |
| 243 | | create_texpr(equal(ValueVar,Projection),pred,[],Equals), |
| 244 | | create_projection(Path,RecordVar,Projection), |
| 245 | | %translate:print_bexpr(Projection),nl, |
| 246 | | create_symbolic_comprehension_set([RecordVar,ValueVar],Equals, |
| 247 | | [record_detection(accessor)],AccessDefinition). |
| 248 | | |
| 249 | | create_symbolic_comprehension_set(Ids,Pred,Info,Result) :- |
| 250 | | create_comprehension_set(Ids,Pred,Info,CompSet), |
| 251 | | mark_bexpr_as_symbolic(CompSet,Result). |
| 252 | | |
| 253 | | create_projection(Path,RecordVar,ProjectionResult) :- |
| 254 | | get_texpr_type(RecordVar,InnerType), |
| 255 | | create_projection_aux(Path,InnerType,RecordVar,ProjectionResult). |
| 256 | | |
| 257 | | create_projection_aux([],_InnerType,SubExpression,SubExpression). % return record as is |
| 258 | | create_projection_aux([Loc|Path],couple(A,B),SubExpression,ProjectionResult) :- |
| 259 | | ( Loc==left -> Expr=first_of_pair(SubExpression), InnerType=A |
| 260 | | ; Loc==right -> Expr=second_of_pair(SubExpression),InnerType=B), |
| 261 | | create_texpr(Expr,InnerType,[],NewSubExpression), |
| 262 | | create_projection_aux(Path,InnerType,NewSubExpression,ProjectionResult). |
| 263 | | |
| 264 | | |
| 265 | | % remove fieldx : RecSet --> Domx |
| 266 | | remove_field_declarations([],_RecSet,Predicates,Predicates). |
| 267 | | remove_field_declarations([fieldloc(AccessorId,Domain,_Path)|Frest],RecSet,Pin,Pout) :- |
| 268 | | remove_field_declaration(AccessorId,Domain,RecSet,Pin,Pinter), |
| 269 | | remove_field_declarations(Frest,RecSet,Pinter,Pout). |
| 270 | | remove_field_declaration(AccessorId,Domain,RecSet,Pin,Pout) :- |
| 271 | | bsyntax_pattern(member(-AccessorId,total_function(-RecSet,-Domain)),Pattern), |
| 272 | | selectchk(Pattern,Pin,Pout). |
| 273 | | |
| 274 | | % remove !(f1,...,fn). ( f1:T1 & ... & fn:Tn => fieldx(make_rec(f1|->f2|->f3)) = fx) |
| 275 | | remove_field_quantifiers(Fields,Constructor,Pin,Pout) :- |
| 276 | | remove_field_quantifiers2(Fields,0,Constructor,Pin,Pout). |
| 277 | | |
| 278 | | remove_field_quantifiers2(Fields,N,Constructor,Pin,Pout) :- |
| 279 | | ( nth0(N,Fields,fieldloc(Field,_Dom,_Path)) -> |
| 280 | | remove_field_quantifier(Field,N,Fields,Constructor,Pin,Pinter), |
| 281 | | N2 is N+1, |
| 282 | | remove_field_quantifiers2(Fields,N2,Constructor,Pinter,Pout) |
| 283 | | ; |
| 284 | | Pin=Pout). |
| 285 | | remove_field_quantifier(Field,N,Fields,Constructor,Pin,Pout) :- |
| 286 | | make_field_identifiers(Fields,FSkels), |
| 287 | | get_texpr_ids(FSkels,Ids), |
| 288 | | nth0(N,FSkels,Ref), |
| 289 | | bsyntax_pattern(forall(FSkels,_,equal(function(-Field,function(-Constructor,ConstArg)),-Ref)),ForAll), |
| 290 | ? | select(ForAll,Pin,Pout), |
| 291 | | are_mappings(ConstArg,Ids),!. |
| 292 | | are_mappings(TExpr,Ids) :- |
| 293 | | are_mappings2(TExpr,Ids,[]). |
| 294 | | are_mappings2(TExpr) --> |
| 295 | | {get_texpr_expr(TExpr,Expr)}, |
| 296 | | are_mappings3(Expr). |
| 297 | | are_mappings3(identifier(Id)) --> [Id]. |
| 298 | | are_mappings3(couple(A,B)) --> |
| 299 | | are_mappings2(A), |
| 300 | | are_mappings2(B). |
| 301 | | |
| 302 | | make_field_identifiers([],[]). |
| 303 | | make_field_identifiers([FieldAcc|FRest],[Id|Irest]) :- |
| 304 | | make_field_identifier(FieldAcc,Id), |
| 305 | | make_field_identifiers(FRest,Irest). |
| 306 | | make_field_identifier(fieldloc(FieldAcc,_,_),Id) :- |
| 307 | | get_texpr_type(FieldAcc,SType), |
| 308 | | is_set_type(SType,couple(_,FType)), |
| 309 | | create_texpr(identifier(_),FType,_,Id). |
| 310 | | |
| 311 | | replace_update_definitions(Fields,RecSet,Constructor,Updates,Pin,Pout) :- |
| 312 | | replace_update_definitions2(Fields,Fields,RecSet,Constructor,Updates,Pin,Pout). |
| 313 | | replace_update_definitions2([],_Fields,_RecSet,_Constructor,[],Predicates,Predicates). |
| 314 | | replace_update_definitions2([fieldloc(AccessorId,FDomain,Path)|Frest],Fields,RecSet, |
| 315 | | Constructor,[UpdateId|URest],Pin,Pout) :- |
| 316 | | replace_update_definition(AccessorId,FDomain,Path,Fields,RecSet,Constructor,UpdateId,Pin,Pinter), |
| 317 | | replace_update_definitions2(Frest,Fields,RecSet,Constructor,URest,Pinter,Pout). |
| 318 | | |
| 319 | | % Identify two predicates of the form |
| 320 | | % updatex : Record ** Domain --> Record |
| 321 | | % !(Rec,New).(_ => updatex(Rec,New) = Constructor(..)) |
| 322 | | % and replace them by |
| 323 | | % updatex = {i,o | #(n,f1,...,fn).(i=(f1,...,fn)|->n & o=(f1,...,n,..,fn))} |
| 324 | | replace_update_definition(FieldAccessorId,FieldDomain,Path,Fields, |
| 325 | | RecSet,Constructor,Update,Pin,[Equal|Pout]) :- |
| 326 | | % Updatex : Record ** Domain --> Record |
| 327 | | bsyntax_pattern(member(Update1,total_function(cartesian_product(-RecSet,-FieldDomain),-RecSet)),Memb), |
| 328 | ? | select(Memb,Pin,P1), |
| 329 | | % !(Rec,New).(_ => Updatex(Rec,New) = Constructor(..)) |
| 330 | | % TODO: Implication and constructor arguments are missing |
| 331 | | bsyntax_pattern(forall([Rec,New],_,equal(function(-Update1,couple(-Rec,-New)), |
| 332 | | function(-Constructor,_))), ForAll), |
| 333 | ? | select(ForAll,P1,Pout), |
| 334 | | !, |
| 335 | | add_texpr_infos(Update1,[record_detection(update)],Update), |
| 336 | | % Updatex = {i,o | #(i,r,f1,...,fn).(i=r|->n & ) } |
| 337 | | create_texpr(equal(Update,Function),pred,[],Equal), |
| 338 | | create_update_function(FieldAccessorId,FieldDomain,Path,Fields,Function). |
| 339 | | |
| 340 | | create_update_function(FieldAccessorId,FieldDomain,Path,Fields,Function) :- |
| 341 | | % {i,o | #n,f1,...,fn. ( i=( (f1,...,fn) |-> n ) ) & o=(f1,...,n,...,fn) } |
| 342 | | get_texpr_type(FieldAccessorId,SType), |
| 343 | | is_set_type(SType,couple(RecType,FieldType)), |
| 344 | | InType = couple(RecType,FieldType), |
| 345 | | create_texpr(identifier(update__in),InType,[],In), |
| 346 | | create_texpr(identifier(update__out),RecType,[],Out), |
| 347 | | create_symbolic_comprehension_set([In,Out],Pred,[record_detection(update)],CompSet), |
| 348 | | |
| 349 | | % #(n,f1,...,fn).(...&...) |
| 350 | | %create_exists([NewValue|FieldVars],ExistsPred,Pred), % moved below; see comment |
| 351 | | create_var_for_field(FieldAccessorId,FieldDomain,'f$n__',NewValue), |
| 352 | | maplist(create_field_var,Fields,FieldVars), |
| 353 | | create_texpr(conjunct(InEqual,OutEqual),pred,[],ExistsPred), |
| 354 | | |
| 355 | | % i = ( (f1,...,fn) |-> n ) |
| 356 | | create_texpr(equal(In,InPair),pred,[],InEqual), |
| 357 | | create_texpr(couple(OldFields,NewValue),InType,[],InPair), |
| 358 | | create_record_tuple(Fields,FieldVars,OldFields), |
| 359 | | |
| 360 | | % o = (f1,...,n,...,fn) |
| 361 | | create_texpr(equal(Out,NewFields),pred,[],OutEqual), |
| 362 | | update_record_tuple(Path,NewValue,OldFields,NewFields), |
| 363 | | |
| 364 | | % the creation of the exists has to be deferred until here as used identifiers are computed: |
| 365 | | create_exists([NewValue|FieldVars],ExistsPred,Pred), |
| 366 | | %translate:print_bexpr(CompSet),nl, |
| 367 | | |
| 368 | | % we need to call the clean-up functions because exists(...) needs more |
| 369 | | % information about which identifier are used and that information |
| 370 | | % is added by clean_up/3. |
| 371 | | clean_up(CompSet,[],Function). |
| 372 | | |
| 373 | | % for a fields, create an identifier with the corresponding type |
| 374 | | create_field_var(fieldloc(AccessorId,Domain,_Path),TId) :- |
| 375 | | create_var_for_field(AccessorId,Domain,'f$__',TId). |
| 376 | | create_var_for_field(AccessorId,Domain,Prefix,TId) :- |
| 377 | | get_texpr_id(AccessorId,FId), |
| 378 | | get_texpr_type(Domain,DType), |
| 379 | | is_set_type(DType,Type), |
| 380 | | atom_concat(Prefix,FId,VId), |
| 381 | | create_texpr(identifier(VId),Type,[],TId). |
| 382 | | |
| 383 | | % for a list of fields and identifiers f1,...,fn, create a tuple (f1,...,fn) |
| 384 | | create_record_tuple([],[],_). |
| 385 | | create_record_tuple([fieldloc(_,_,Path)|Frest],[FieldVar|Vrest],Tuple) :- |
| 386 | | create_record_tuple2(Path,FieldVar,Tuple), |
| 387 | | create_record_tuple(Frest,Vrest,Tuple). |
| 388 | | create_record_tuple2([],Expr,Expr). |
| 389 | | create_record_tuple2([Loc|Path],Expr,Tuple) :- |
| 390 | | ( Loc==left -> create_texpr(couple(Sub,_),couple(SubType,_),[],Tuple) |
| 391 | | ; Loc==right -> create_texpr(couple(_,Sub),couple(_,SubType),[],Tuple)), |
| 392 | | get_texpr_type(Sub,SubType), |
| 393 | | create_record_tuple2(Path,Expr,Sub). |
| 394 | | |
| 395 | | % in a tuple representing a record, replace one field |
| 396 | | update_record_tuple([],NewValue,_OldFields,NewValue). |
| 397 | | update_record_tuple([Loc|Path],NewValue,OldFields,NewFields) :- |
| 398 | | get_texpr_expr(OldFields,couple(A,B)), |
| 399 | | get_texpr_type(OldFields,Type), |
| 400 | | create_texpr(couple(X,Y),Type,[],NewFields), |
| 401 | | ( Loc==left -> X=NewSub,A=OldSub,Y=B |
| 402 | | ; Loc==right -> Y=NewSub,B=OldSub,X=A), |
| 403 | | update_record_tuple(Path,NewValue,OldSub,NewSub). |
| 404 | | |
| 405 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 406 | | % replace_type_in_machine(+T1,+T2,+Domain,+OldMachine,-NewMachine): |
| 407 | | % T1: The name of the global set that refers to the old type |
| 408 | | % T2: The new type that should replace global(T1) |
| 409 | | % Domain: A B expression that describes the domain of the record, used to |
| 410 | | % constrain introduced identifiers |
| 411 | | % OldMachine: The B machine before replacement |
| 412 | | % NewMachine: The resulting B machine |
| 413 | | replace_type_in_machine(T1,T2,Domain,OldMachine,NewMachine) :- |
| 414 | | extract_constants_that_are_types(OldMachine,RTT), |
| 415 | | (is_just_type(Domain,RTT) -> Domain2 = simple ; Domain2 = Domain), |
| 416 | | % add predicates to constrain variables or constants, if needed |
| 417 | | foldl(add_type_constraint_to_section(T1,Domain2), |
| 418 | | [decl([abstract_constants,concrete_constants],properties), |
| 419 | | decl([abstract_variables,concrete_variables],invariant)], |
| 420 | | OldMachine,Machine1), |
| 421 | | % replace the type in the expressions of the machine (identifier declarations |
| 422 | | % can be treated as expressions, too) |
| 423 | | foldl(replace_type_in_machine2(T1,T2,Domain2), |
| 424 | | [abstract_constants,concrete_constants, |
| 425 | | abstract_variables,concrete_variables, |
| 426 | | promoted, unpromoted, |
| 427 | | constraints, properties, invariant, assertions, |
| 428 | | initialisation, operation_bodies], |
| 429 | | Machine1,NewMachine). |
| 430 | | replace_type_in_machine2(T1,T2,Domain,Sec,In,Out) :- |
| 431 | | select_section_texprs(Sec,Old,New,In,Out), |
| 432 | | replace_type_in_exprs(Old,T1,T2,Domain,New). |
| 433 | | replace_type_in_expr(TExpr,T1,T2,Domain,New) :- |
| 434 | | % if identifiers (e.g. i) are declared in an expression (like in forall), we may have |
| 435 | | % to add an predicate (e.g. i:1..4) |
| 436 | | ( Domain=simple -> % the domain is a whole type, no additional constraint needed |
| 437 | | TExpr2 = TExpr |
| 438 | ? | ; has_declared_identifier(TExpr,Ids),contains_identifier_with_type(Ids,T1) -> |
| 439 | | % identifiers are introduced and one of them contains the record type |
| 440 | | add_type_declarations(TExpr,global(T1),Domain,Ids,TExpr2) |
| 441 | | ; % no identifiers introduced that use the record type |
| 442 | | TExpr = TExpr2 |
| 443 | | ), |
| 444 | | create_texpr(Expr,EType,Info,TExpr2), % de-assemble old expression |
| 445 | | replace_type(EType,T1,T2,NType), % replace type global(T1) by T2 in Type |
| 446 | | create_texpr(NExpr2,NType,Info,New), % assemble new expression with new type |
| 447 | | syntaxtransformation(Expr,Subs,_Names,NSubs,NExpr1), % continue with sub-expressions |
| 448 | | replace_type_in_exprs(Subs,T1,T2,Domain,NSubs), |
| 449 | | replace_hidden_type_paras(NExpr1,T1,T2,NExpr2). |
| 450 | | replace_type_in_exprs([],_T1,_T2,_Domain,[]). |
| 451 | | replace_type_in_exprs([Sub|Irest],T1,T2,Domain,[NSub|Orest]) :- |
| 452 | | replace_type_in_expr(Sub,T1,T2,Domain,NSub), |
| 453 | | replace_type_in_exprs(Irest,T1,T2,Domain,Orest). |
| 454 | | |
| 455 | | |
| 456 | | replace_hidden_type_paras(freetype_constructor(A,Case,Expr),T1,T2,freetype_constructor(RA,Case,Expr)) :- !, |
| 457 | | replace_freetype_paras(A,T1,T2,RA). |
| 458 | | replace_hidden_type_paras(freetype_destructor(A,Case,Expr),T1,T2,freetype_destructor(RA,Case,Expr)) :- !, |
| 459 | | replace_freetype_paras(A,T1,T2,RA). |
| 460 | | replace_hidden_type_paras(E,_,_,E). |
| 461 | | |
| 462 | | |
| 463 | | contains_identifier_with_type(Ids,T1) :- |
| 464 | | get_texpr_type(TId,Type), |
| 465 | ? | member(TId,Ids), |
| 466 | ? | contains_type(global(T1),Type). |
| 467 | | |
| 468 | | add_type_constraint_to_section(_ToReplace,simple,_Decl,In,Out) :- |
| 469 | | !,In=Out. |
| 470 | | add_type_constraint_to_section(ToReplace,Domain,decl(IdSecs,PredSec),In,Out) :- |
| 471 | | maplist(aux_get_section(In),IdSecs,IdsL),append(IdsL,Ids1), |
| 472 | | % do not add constraints for accessor and update functions for records: |
| 473 | | exclude(is_record_detection_expr,Ids1,Ids), |
| 474 | ? | ( contains_identifier_with_type(Ids,ToReplace) -> |
| 475 | | create_type_predicate(global(ToReplace),Domain,Ids,P), |
| 476 | | ( is_truth(P) -> In=Out % Trivial, nothing to do |
| 477 | | ; % Add the type constraint to the relevant predicate section |
| 478 | | select_section(PredSec,OldPred,NewPred,In,Out), |
| 479 | | conjunct_predicates([P,OldPred],NewPred) |
| 480 | | ) |
| 481 | | ; % Not applicable, nothing to do |
| 482 | | In=Out). |
| 483 | | aux_get_section(Machine,Sec,Content) :- % just to rearrange the parameters |
| 484 | | get_section(Sec,Machine,Content). |
| 485 | | |
| 486 | | is_record_detection_expr(Expr) :- |
| 487 | | get_texpr_info(Expr,Info),memberchk(record_detection(_),Info). |
| 488 | | |
| 489 | | replace_type(global(Type),Type,NewType,Result) :- !, NewType=Result. |
| 490 | | replace_type(couple(A,B),T1,T2,couple(RA,RB)) :- |
| 491 | | !, replace_type(A,T1,T2,RA), replace_type(B,T1,T2,RB). |
| 492 | | replace_type(set(A),T1,T2,set(RA)) :- |
| 493 | | !, replace_type(A,T1,T2,RA). |
| 494 | | replace_type(seq(A),T1,T2,seq(RA)) :- |
| 495 | | !, replace_type(A,T1,T2,RA). |
| 496 | | replace_type(freetype(A),T1,T2,freetype(RA)) :- |
| 497 | | !, replace_freetype_paras(A,T1,T2,RA). |
| 498 | | replace_type(T,_,_,T). % just skip types like integer, string, etc. |
| 499 | | |
| 500 | | % replace type inside freetype type parameters (relevant for Event-B polymorphic theories) |
| 501 | | replace_freetype_paras(A,T1,T2,RA) :- |
| 502 | | get_freetype_type_parameters(A,Func,TypeParas), |
| 503 | | maplist(mreplace(T1,T2),TypeParas,NewTypeParas), |
| 504 | | get_freetype_type_parameters(RA,Func,NewTypeParas). |
| 505 | | |
| 506 | | mreplace(T1,T2,Type,ReplacedType) :- replace_type(Type,T1,T2,ReplacedType). |
| 507 | | |
| 508 | | contains_type(Type,couple(A,_)) :- contains_type(Type,A). |
| 509 | | contains_type(Type,couple(_,B)) :- contains_type(Type,B). |
| 510 | ? | contains_type(Type,set(A)) :- contains_type(Type,A). |
| 511 | | contains_type(Type,seq(A)) :- contains_type(Type,A). |
| 512 | | contains_type(Type,freetype(A)) :- get_freetype_type_parameters(A,_,TypeParas), |
| 513 | | member(TP,TypeParas), contains_type(Type,TP). |
| 514 | | contains_type(Type,Type). |
| 515 | | |
| 516 | | add_type_declarations(TExpr,ToReplace,Set,Ids,Result) :- |
| 517 | | create_type_predicate(ToReplace,Set,Ids,P), |
| 518 | | ( is_truth(P) -> Result = TExpr % Nothing to do |
| 519 | | ; add_declaration_for_identifier(TExpr,P,Result)). |
| 520 | | |
| 521 | | create_type_predicate(ToReplace,Set,Ids,P) :- |
| 522 | | include(expr_contains_type(ToReplace),Ids,RelevantIds), |
| 523 | | maplist(create_type_membership(ToReplace,Set),RelevantIds,Preds), |
| 524 | | conjunct_predicates(Preds,P1), |
| 525 | | clean_up(P1,[],P). |
| 526 | | |
| 527 | | expr_contains_type(ToReplace,TExpr) :- |
| 528 | | get_texpr_type(TExpr,Type), |
| 529 | ? | contains_type(ToReplace,Type). |
| 530 | | |
| 531 | | create_type_membership(ToReplace,Set,TId,Membership) :- |
| 532 | | get_texpr_type(TId,Type), |
| 533 | | create_set_for_type(Type,ToReplace,Set,GenSet), |
| 534 | | create_texpr(member(TId,GenSet),pred,[],Membership). |
| 535 | | |
| 536 | | create_set_for_type(T,ToReplace,Set,R) :- |
| 537 | | T=ToReplace,!,R=Set. |
| 538 | | create_set_for_type(couple(A,B),ToReplace,Set,R) :- !, |
| 539 | | create_set_for_type(A,ToReplace,Set,SA), |
| 540 | | create_set_for_type(B,ToReplace,Set,SB), |
| 541 | | ( is_typeset(SA),is_typeset(SB) -> create_typeset(couple(A,B),R) |
| 542 | | ; create_texpr(cartesian_product(SA,SB),set(couple(A,B)),[],R)). |
| 543 | | create_set_for_type(set(A),ToReplace,Set,R) :- !, |
| 544 | | create_set_for_type(A,ToReplace,Set,SA), |
| 545 | | ( is_typeset(SA) -> create_typeset(set(A),R) |
| 546 | | ; create_texpr(pow_subset(SA),set(set(A)),[],R)). |
| 547 | | create_set_for_type(seq(A),ToReplace,Set,R) :- !, |
| 548 | | % for our purpose, we can ignore other constraints on sequences |
| 549 | | create_set_for_type(set(couple(integer,A)),ToReplace,Set,R). |
| 550 | | create_set_for_type(Type,_ToReplace,_Set,R) :- create_typeset(Type,R). |
| 551 | | is_typeset(Expr) :- get_texpr_expr(Expr,typeset). |
| 552 | | |
| 553 | | create_typeset(Type,Set) :- |
| 554 | | create_texpr(typeset,set(Type),[],Set). |
| 555 | | |
| 556 | | % extract_constants_that_are_types(+Machine,-RTT): |
| 557 | | % gives a list of identifiers of those constants that are defined to be the whole type. |
| 558 | | % This works only for constants that are defined with an equality, e.g. |
| 559 | | % c = BOOL**BOOL |
| 560 | | extract_constants_that_are_types(Machine,RTT) :- |
| 561 | | get_all_equalities_from_machine(Machine,Equalities), |
| 562 | | extract_type_references(Equalities,[],RTT). |
| 563 | | % get_all_equalities_from_properties(+Machine,-Equalities): |
| 564 | | % extract all equalities from the properties. |
| 565 | | % Equalities is a list of terms equal(Id,Expr) where Id denotes a |
| 566 | | % constant and Expr the expr on the other side of the equation. |
| 567 | | get_all_equalities_from_machine(Machine,Equalities) :- |
| 568 | | get_all_constants_from_machine(Machine,Constants), |
| 569 | | get_section(properties,Machine,Properties), |
| 570 | | conjunction_to_list(Properties,PList), |
| 571 | | convlist(is_equality_left(Constants), PList,LEqualities), |
| 572 | | convlist(is_equality_right(Constants),PList,REqualities), |
| 573 | | append(LEqualities,REqualities,Equalities). |
| 574 | | get_all_constants_from_machine(Machine,Constants) :- |
| 575 | | get_section(abstract_constants,Machine,AC), |
| 576 | | get_section(concrete_constants,Machine,CC), |
| 577 | | append(AC,CC,Constants). |
| 578 | | % extract_type_references(+Equalities,+RTT,-Result): |
| 579 | | % Equalities: A list of term of the form equal(Id,Expr), see get_all_equalities_from_properties/2 |
| 580 | | % RTT: An ordered list of already known constants that refer to types |
| 581 | | % Result: A ordered list of constants (their id, no types) that refer to types |
| 582 | | % The predicate works recursively because a definition like a = B**INTEGER can denote a |
| 583 | | % type if B also denotes a type which must be detected first. |
| 584 | | extract_type_references(Equalities,RTT,Result) :- |
| 585 | | convlist(equality_is_typedef(RTT),Equalities,ReferencesToTypes), |
| 586 | | list_to_ord_set(ReferencesToTypes,Sorted), |
| 587 | | ord_subtract(Sorted,RTT,Unique), |
| 588 | | ( Unique = [] -> Result=RTT % no new definitions found |
| 589 | | ; % new definitions found, continue recursively |
| 590 | | ord_union(Unique,RTT,NewRTT), |
| 591 | | extract_type_references(Equalities,NewRTT,Result) |
| 592 | | ). |
| 593 | | % Pred is of form Id=Expr where Id is a constant |
| 594 | | is_equality_left(Constants,Pred,equal(Id,Expr)) :- |
| 595 | | get_texpr_expr(Pred,equal(TId,Expr)), is_equality_aux(TId,Constants,Id). |
| 596 | | % Pred is of form Expr=Id where Id is a constant |
| 597 | | is_equality_right(Constants,Pred,equal(Id,Expr)) :- |
| 598 | | get_texpr_expr(Pred,equal(Expr,TId)), is_equality_aux(TId,Constants,Id). |
| 599 | | is_equality_aux(TId,Constants,Id) :- |
| 600 | | get_texpr_id(TId,Id),get_texpr_id(Constant,Id),memberchk(Constant,Constants). |
| 601 | | equality_is_typedef(RTT,equal(Id,Expr),Id) :- |
| 602 | | is_just_type(Expr,RTT). |