| 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(kodkod2, | |
| 6 | [ extract_used_types/4 | |
| 7 | , create_atoms_for_types/6 | |
| 8 | , create_identifier_relations/5 | |
| 9 | ]). | |
| 10 | ||
| 11 | :- use_module(library(lists)). | |
| 12 | :- use_module(library(avl)). | |
| 13 | :- use_module(library(ordsets)). | |
| 14 | ||
| 15 | :- use_module(kodkodsrc(kodkod_tools)). | |
| 16 | :- use_module(kodkodsrc(kodkod_integer_recalc)). | |
| 17 | ||
| 18 | :- use_module(probsrc(module_information),[module_info/2]). | |
| 19 | :- use_module(probsrc(tools),[foldl/4,foldl/5]). | |
| 20 | :- use_module(probsrc(error_manager)). | |
| 21 | :- use_module(probsrc(bsyntaxtree)). | |
| 22 | :- use_module(probsrc(bmachine)). | |
| 23 | :- use_module(probsrc(b_interpreter),[b_compute_expression_nowf/6]). | |
| 24 | :- use_module(probsrc(b_global_sets),[all_elements_of_type/2,is_b_global_constant/3]). | |
| 25 | :- use_module(probsrc(store),[empty_state/1]). | |
| 26 | ||
| 27 | :- module_info(group,kodkod). | |
| 28 | :- module_info(description,'This module contains the several phases of a translation process to Kodkod.'). | |
| 29 | ||
| 30 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 31 | % Phase 2 | |
| 32 | % extract all used types | |
| 33 | % for integers, check if bitstrings are necessary and store | |
| 34 | % the needed intervals | |
| 35 | ||
| 36 | % extract_used_types(+TExpr,-UsedTypes,-IntegerRange,-BitstringRange): | |
| 37 | % extracts from a syntax tree the list of used types, the | |
| 38 | % ranges of integers and the ranges of integers that occur in sets | |
| 39 | extract_used_types(TExpr,UsedTypes,IntegerRange,BitstringRange) :- | |
| 40 | % first adapt the output of the interval analysis to our needs | |
| 41 | % (see the comments in kodkod_integer_recalc for details) | |
| 42 | integer_recalc(TExpr,unknown_atoms(NeedsAtoms),RExpr), | |
| 43 | % now extract the used types | |
| 44 | extract_used_types1(RExpr,UsedTypes1,IntegerRange1,BitstringRange1), | |
| 45 | ( NeedsAtoms == true -> | |
| 46 | % the cardinality and the sum of a set of integers are bounded by the integer atoms, | |
| 47 | % which are only known now | |
| 48 | integer_recalc(TExpr,atoms(BitstringRange1),RExpr2), | |
| 49 | extract_used_types1(RExpr2,UsedTypes,IntegerRange,BitstringRange), | |
| 50 | ( BitstringRange == BitstringRange1 -> true | |
| 51 | ; % the cardinality itself is used as a set element, requiring more atoms | |
| 52 | throw(kodkod(unsupported_int('cardinality or sum of integer set requires additional integer atoms')))) | |
| 53 | ; | |
| 54 | UsedTypes=UsedTypes1, IntegerRange=IntegerRange1, BitstringRange=BitstringRange1). | |
| 55 | ||
| 56 | extract_used_types1(TExpr,UsedTypes,IntegerRange,BitstringRange) :- | |
| 57 | syntaxtraversion(TExpr,Expr,Type,_,Subs1,Names), | |
| 58 | ( higher_order_exception(Expr,Subs) -> | |
| 59 | UsedTypesA=[],IntRangeA=none,BitRangeA=none | |
| 60 | ; extract_type_information(Type,TExpr,Names,UsedTypesA,IntRangeA,BitRangeA) -> | |
| 61 | Subs1 = Subs | |
| 62 | ; | |
| 63 | throw(kodkod(unsupported_type(Type)))), | |
| 64 | add_atom_ranges_of_elements(Expr,BitRangeA,BitRangeB), | |
| 65 | extract_used_types_l(Subs,UsedTypesA,IntRangeA,BitRangeB, | |
| 66 | UsedTypes,IntegerRange,BitstringRange). | |
| 67 | ||
| 68 | % Integer expressions used as elements of a set (or as argument of a function) | |
| 69 | % are cast to integer atoms (int2intset). Kodkod's cast yields the empty set if | |
| 70 | % there is no atom for the value, e.g. 3:{0,1} would be translated to {} <: {0,1} | |
| 71 | % and be true. Hence the range of these expressions must be covered by the atoms. | |
| 72 | add_atom_ranges_of_elements(Expr,BitRangeIn,BitRangeOut) :- | |
| 73 | integer_element_positions(Expr,Elems),!, | |
| 74 | include(is_integer_expr,Elems,IntElems), | |
| 75 | foldl(extract_integer_as_set,IntElems,BitRangeIn,BitRangeOut). | |
| 76 | add_atom_ranges_of_elements(_,BitRange,BitRange). | |
| 77 | ||
| 78 | integer_element_positions(member(E,_),[E]). | |
| 79 | integer_element_positions(not_member(E,_),[E]). | |
| 80 | integer_element_positions(set_extension(Elems),Elems). | |
| 81 | integer_element_positions(function(_,Arg),[Arg]). | |
| 82 | integer_element_positions(couple(A,B),[A,B]). | |
| 83 | ||
| 84 | extract_used_types_l([],Types,IntRange,BitRange,Types,IntRange,BitRange). | |
| 85 | extract_used_types_l([Expr|Erest],TypesI,IntRangeI,BitRangeI,Types,IntRange,BitRange) :- | |
| 86 | extract_used_types1(Expr,TypesA,IntRangeA,BitRangeA), | |
| 87 | merge_integer_info(IntRangeI,IntRangeA,IntRangeB), | |
| 88 | merge_integer_info(BitRangeI,BitRangeA,BitRangeB), | |
| 89 | ord_union(TypesI,TypesA,TypesB), | |
| 90 | extract_used_types_l(Erest,TypesB,IntRangeB,BitRangeB,Types,IntRange,BitRange). | |
| 91 | ||
| 92 | extract_type_information(Type,TExpr,Names,UsedTypesA,IntRangeA,BitRangeA) :- | |
| 93 | extract_type_information2(Type,TExpr,Names,[],UsedTypesA,IntRangeA,BitRangeA). | |
| 94 | extract_type_information2(T,_,_,_,[T],none,none) :- | |
| 95 | basic_type(T). | |
| 96 | extract_type_information2(integer,TExpr,_,Scope,[],IntRange,none) :- | |
| 97 | extract_finite_integer_range(TExpr,Scope,IntRange). | |
| 98 | extract_type_information2(set(Type),TExpr,_,Scope,UsedTypes,IntRange,BitRange) :- | |
| 99 | extract_type_information_set(Type,TExpr,[elem|Scope],UsedTypes,IntRange,BitRange). | |
| 100 | extract_type_information2(seq(Type),TExpr,_,Scope,UsedTypes,IntRange,BitRange) :- | |
| 101 | extract_type_information2(set(couple(integer,Type)),TExpr,[],Scope,UsedTypes,IntRange,BitRange). | |
| 102 | extract_type_information2(couple(A,B),TExpr,_,Scope,UsedTypes,IntRange,BitRange) :- | |
| 103 | extract_type_information_couple(A,TExpr,[left|Scope],TypesA,IntRangeA,BitRangeA), | |
| 104 | extract_type_information_couple(B,TExpr,[right|Scope],TypesB,IntRangeB,BitRangeB), | |
| 105 | merge_integer_info(IntRangeA,IntRangeB,IntRange), | |
| 106 | merge_integer_info(BitRangeA,BitRangeB,BitRange), | |
| 107 | ord_union(TypesA,TypesB,UsedTypes). | |
| 108 | extract_type_information2(pred,_Expr,Names,_Scope,Types,IntRange,BitRange) :- | |
| 109 | treat_quantified_integers_as_sets(Names,Types,IntRange,BitRange). | |
| 110 | ||
| 111 | % integers in a pair are represented by integer atoms (the pair is a product of relations) | |
| 112 | extract_type_information_couple(integer,TExpr,Scope,[],Range,Range) :- !, | |
| 113 | extract_finite_integer_range(TExpr,Scope,Range). | |
| 114 | extract_type_information_couple(Type,TExpr,Scope,UsedTypes,IntRange,BitRange) :- | |
| 115 | extract_type_information2(Type,TExpr,[],Scope,UsedTypes,IntRange,BitRange). | |
| 116 | ||
| 117 | treat_quantified_integers_as_sets(Names,[],none,Range) :- | |
| 118 | include(is_integer_expr,Names,Integers), | |
| 119 | foldl(extract_integer_as_set,Integers,none,Range). | |
| 120 | ||
| 121 | is_integer_expr(TExpr) :- get_texpr_type(TExpr,integer). | |
| 122 | ||
| 123 | % Basic idea: extract_finite_integer_range/3 returns the bitrange (used for simple | |
| 124 | % integers), but we treat as if it was the intRange (used for integer sets) | |
| 125 | extract_integer_as_set(TExpr,IntRangeI,IntRangeO) :- | |
| 126 | extract_finite_integer_range(TExpr,[],IntRange), | |
| 127 | merge_integer_info(IntRangeI,IntRange,IntRangeO). | |
| 128 | ||
| 129 | extract_type_information_set(T,_,_,[T],none,none) :- | |
| 130 | basic_type(T). | |
| 131 | extract_type_information_set(integer,TExpr,Scope,[],BitRange,BitRange) :- | |
| 132 | extract_finite_integer_range(TExpr,Scope,BitRange). | |
| 133 | extract_type_information_set(couple(A,B),TExpr,Scope,UsedTypes,IntRange,BitRange) :- | |
| 134 | extract_type_information_set(A,TExpr,[left|Scope],TypesA,IntRangeA,BitRangeA), | |
| 135 | extract_type_information_set(B,TExpr,[right|Scope],TypesB,IntRangeB,BitRangeB), | |
| 136 | merge_integer_info(IntRangeA,IntRangeB,IntRange), | |
| 137 | merge_integer_info(BitRangeA,BitRangeB,BitRange), | |
| 138 | ord_union(TypesA,TypesB,UsedTypes). | |
| 139 | ||
| 140 | basic_type(boolean). | |
| 141 | basic_type(global(_)). | |
| 142 | ||
| 143 | higher_order_exception(member(Elem,THOSet),[Elem|Subsets]) :- | |
| 144 | get_texpr_expr(THOSet,HOSet), | |
| 145 | higher_order_exception2(HOSet,Subsets). | |
| 146 | higher_order_exception2(total_function(Dom,Ran),[Dom,Ran]). | |
| 147 | higher_order_exception2(total_injection(Dom,Ran),[Dom,Ran]). | |
| 148 | higher_order_exception2(total_surjection(Dom,Ran),[Dom,Ran]). | |
| 149 | higher_order_exception2(total_bijection(Dom,Ran),[Dom,Ran]). | |
| 150 | higher_order_exception2(partial_function(Dom,Ran),[Dom,Ran]). | |
| 151 | higher_order_exception2(partial_injection(Dom,Ran),[Dom,Ran]). | |
| 152 | higher_order_exception2(partial_surjection(Dom,Ran),[Dom,Ran]). | |
| 153 | higher_order_exception2(partial_bijection(Dom,Ran),[Dom,Ran]). | |
| 154 | higher_order_exception2(total_relation(Dom,Ran),[Dom,Ran]). | |
| 155 | higher_order_exception2(surjection_relation(Dom,Ran),[Dom,Ran]). | |
| 156 | ||
| 157 | ||
| 158 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 159 | % Phase 3 | |
| 160 | % create the relations for the used types | |
| 161 | ||
| 162 | % create_atoms_for_types(+Types,+IntegerRange,+BitstringRange, | |
| 163 | % -Size,-Typemap,-Idmap,-Valuemap): | |
| 164 | % Types is a list of used types | |
| 165 | % IntegerRange is the range of used integers | |
| 166 | % IntsetRange is the range of used integers that occur in a set and | |
| 167 | % have each to be modelled as an atom. | |
| 168 | % Typemap is an AVL map from used types to relations | |
| 169 | % Idmap is an AVL map from some constants (including __true and __false | |
| 170 | % for true and false) to a relation | |
| 171 | % Valuemap in an AVL mapping from B values to Kodkod tuples | |
| 172 | create_atoms_for_types(Types,IntegerRange,IntsetRange,Typemap,Idmap,Valuemap) :- | |
| 173 | empty_avl(EmptyMap), | |
| 174 | create_atoms_for_intsets(IntsetRange,EmptyMap,TM1), | |
| 175 | create_atoms_for_integers(IntegerRange,TM1,TM2), | |
| 176 | create_atoms_for_types2(Types,TM2,EmptyMap,EmptyMap,Typemap,Idmap,Valuemap). | |
| 177 | ||
| 178 | create_atoms_for_intsets(none,Map,Map). | |
| 179 | create_atoms_for_intsets(irange(A,B),MapIn,MapOut) :- | |
| 180 | Size is B-A+1, | |
| 181 | intset_relation_kodkod_name(Relname), | |
| 182 | add_type_relation(integer,Relname,Size,intsetrel(Relname,A,B),MapIn,MapOut). | |
| 183 | ||
| 184 | create_atoms_for_integers(none,Map,Map). | |
| 185 | create_atoms_for_integers(irange(A,B),MapIn,MapOut) :- | |
| 186 | pow2integer_relation_kodkod_name(Relname), | |
| 187 | add_type_relation('__pow2integer',Relname,unknown,pow2rel(Relname,A,B),MapIn,MapOut). | |
| 188 | ||
| 189 | add_type_relation(Type,RelationName,Size,Relspec,In,Out) :- | |
| 190 | avl_store(Type,In,relation(RelationName,Size,Relspec),Out). | |
| 191 | add_standard_relation(BType,KType,Id,Size,In,Out) :- | |
| 192 | create_relation_for_type(Id,KType,Relspec), | |
| 193 | avl_store(BType,In,relation(Id,Size,Relspec),Out). | |
| 194 | add_global_type_relation(GType,RelationPrefix,Size,Id,In,Out) :- | |
| 195 | unique_identifier(RelationPrefix,GType,Id), | |
| 196 | add_standard_relation(global(GType),Id,Id,Size,In,Out). | |
| 197 | ||
| 198 | create_atoms_for_types2([],TypeMap,IdMap,ValueMap,TypeMap,IdMap,ValueMap). | |
| 199 | create_atoms_for_types2([Type|Trest],TMin,IDMin,VMin,TMout,IDMout,VMout) :- | |
| 200 | create_atoms_for_type(Type,TMin,IDMin,VMin,TM,IDM,VM), | |
| 201 | create_atoms_for_types2(Trest,TM,IDM,VM,TMout,IDMout,VMout). | |
| 202 | ||
| 203 | create_atoms_for_type(boolean,TMIn,IdIn,VMIn,TMOut,IdOut,VMOut) :- | |
| 204 | add_standard_relation(boolean,bool,bool,2,TMIn,TMOut), | |
| 205 | lookup_constant_value(boolean_true,boolean,VTrue), | |
| 206 | lookup_constant_value(boolean_false,boolean,VFalse), | |
| 207 | assign_values_to_atoms([VTrue,VFalse],boolean,VMIn,VMOut), | |
| 208 | assign_elements_to_atoms(['__kodkod__true','__kodkod__false'],bool,IdIn,IdOut). | |
| 209 | create_atoms_for_type(global(G),TMIn,IdIn,VMIn,TMOut,IdOut,VMOut) :- | |
| 210 | all_elements_of_type(G,ABValues), | |
| 211 | sort(ABValues,BValues), % in case of random enumeration there are problems; see test 1666 | |
| 212 | % Note: all_elements_of_type now provides elements in sorted order; so sort/2 call is in principle not necessary anymore | |
| 213 | length(BValues,Size), | |
| 214 | add_global_type_relation(G,g,Size,RelId,TMIn,TMOut), | |
| 215 | assign_values_to_atoms(BValues,global(G),VMIn,VMOut), | |
| 216 | findall(E, is_b_global_constant(G,_,E), Elements), | |
| 217 | assign_elements_to_atoms(Elements,RelId,IdIn,IdOut). | |
| 218 | ||
| 219 | lookup_constant_value(Expr,Type,Value) :- | |
| 220 | create_texpr(Expr,Type,[],TExpr), | |
| 221 | empty_state(Empty), | |
| 222 | b_compute_expression_nowf(TExpr,Empty,Empty,Value,'KODKOD constant',0). | |
| 223 | ||
| 224 | assign_values_to_atoms(BValues,Type,VMin,VMout) :- | |
| 225 | assign_values_to_atoms2(BValues,Type,0,VMin,VMout). | |
| 226 | assign_values_to_atoms2([],_Type,_Index,ValueMap,ValueMap). | |
| 227 | assign_values_to_atoms2([BValue|BVrest],Type,Index,VMin,VMout) :- | |
| 228 | assign_value_to_atom(BValue,Type,Index,VMin,VM), | |
| 229 | Index2 is Index+1, | |
| 230 | assign_values_to_atoms2(BVrest,Type,Index2,VM,VMout). | |
| 231 | assign_value_to_atom(BValue,Type,Index,VMin,VMout) :- | |
| 232 | avl_store(Type:BValue,VMin,Index,VMout). | |
| 233 | ||
| 234 | assign_elements_to_atoms(Elements,Type,IdMapIn,IdMapOut) :- | |
| 235 | assign_elements_to_atoms2(Elements,Type,0,IdMapIn,IdMapOut). | |
| 236 | assign_elements_to_atoms2([],_Type,_Index,IdMap,IdMap). | |
| 237 | assign_elements_to_atoms2([Elem|Erest],Type,Index,IdMapIn,IdMapOut) :- | |
| 238 | assign_element_to_atom(Elem,Type,Index,IdMapIn,IdMap), | |
| 239 | Index2 is Index+1, | |
| 240 | assign_elements_to_atoms2(Erest,Type,Index2,IdMap,IdMapOut). | |
| 241 | assign_element_to_atom(Elem,Type,Index,In,Out) :- | |
| 242 | unique_identifier(e,Elem,Id), | |
| 243 | create_element_relation(Id,Type,Index,Rel), | |
| 244 | avl_store(Elem,In,Rel,Out). | |
| 245 | ||
| 246 | create_relation_for_type(Id,Type,Rel) :- | |
| 247 | create_generic_relation(Id,[Type],set,exact,full,Rel). | |
| 248 | create_element_relation(Id,Type,Index,Rel) :- | |
| 249 | create_generic_relation(Id,[Type],set,exact,[tuple([Index])],Rel). | |
| 250 | create_generic_relation(Id,Types,SetOrSingle,ExactOrSubset,TupleSet,reldef(Id,Types,SetOrSingle,ExactOrSubset,TupleSet)). | |
| 251 | ||
| 252 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 253 | % Phase 4 | |
| 254 | % create the relations for global constants or variables (i.e. those identifiers | |
| 255 | % which are not introduced by quantifiers) | |
| 256 | ||
| 257 | create_identifier_relations(TIds,Typemap,Bits,IdMapIn,IdMapOut) :- | |
| 258 | maplist(create_identifier_relation(Typemap,Bits),TIds,Ids,Rels), | |
| 259 | foldl(store_in_avl,Ids,Rels,IdMapIn,IdMapOut). | |
| 260 | store_in_avl(Id,Rel,In,Out) :- | |
| 261 | avl_store(Id,In,Rel,Out). | |
| 262 | ||
| 263 | create_identifier_relation(Typemap,Bits,TId,Id,Rel) :- | |
| 264 | get_texpr_id(TId,Id), | |
| 265 | get_texpr_type(TId,Type), | |
| 266 | get_texpr_info(TId,Info), | |
| 267 | unique_identifier(id,Id,RelId), | |
| 268 | is_set_or_single(Type,SetOrSingle,RestType), | |
| 269 | create_identifier_relation2(RestType,SetOrSingle,RelId,Info,Bits,Typemap,Rel). | |
| 270 | create_identifier_relation2(integer,set,RelId,_Info,_Bits,_Typemap,Rel) :- | |
| 271 | !,intset_relation_kodkod_name(Type), | |
| 272 | create_generic_relation(RelId,[Type],set,subset,full,Rel). | |
| 273 | create_identifier_relation2(integer,single,RelId,Info,Bits,_Typemap,Rel) :- | |
| 274 | !, | |
| 275 | % if the type does not fit into the bitset range, the choice is clear: | |
| 276 | % we have to use the pow2 representation | |
| 277 | (in_bitrange(Info,Bits) -> intset_relation_kodkod_name(Type) ; pow2integer_relation_kodkod_name(Type)), | |
| 278 | create_generic_relation(RelId,[Type],single,subset,full,Rel). | |
| 279 | create_identifier_relation2(RestType,SetOrSingle,RelId,_Info,_Bits,Typemap,Rel) :- | |
| 280 | extract_ktypes(RestType,Typemap,Types), | |
| 281 | create_generic_relation(RelId,Types,SetOrSingle,subset,full,Rel). | |
| 282 | ||
| 283 | in_bitrange(Info,irange(BLow,BUp)) :- | |
| 284 | integer_range(Info,Low,Up), | |
| 285 | BLow =< Low, | |
| 286 | Up =< BUp. | |
| 287 | integer_range(Info,Lower,Upper) :- | |
| 288 | memberchk(analysis(A),Info), | |
| 289 | memberchk(interval:irange(Lower,Upper),A). | |
| 290 | ||
| 291 | ||
| 292 | is_set_or_single(seq(T),set,couple(integer,T)) :- !. | |
| 293 | is_set_or_single(set(T),set,T) :- !. | |
| 294 | is_set_or_single(T,single,T). | |
| 295 | ||
| 296 | extract_ktypes(couple(A,B),Typemap,Types) :- !, | |
| 297 | extract_ktypes(A,Typemap,ATypes), | |
| 298 | append(ATypes,BTypes,Types), | |
| 299 | extract_ktypes(B,Typemap,BTypes). | |
| 300 | extract_ktypes(Type,Typemap,[Name]) :- | |
| 301 | avl_fetch(Type,Typemap,Relation), | |
| 302 | Relation = relation(Name,_Size,_Relspec). | |
| 303 | ||
| 304 | ||
| 305 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 306 | % Get all referenced relations in the Kodkod formula | |
| 307 | /* currently not used: | |
| 308 | ||
| 309 | remove_unused_relations(Typemap,Idmap,Valuemap,Formula,NTypemap,NIdmap,Valuemap) :- | |
| 310 | get_used_relations(Formula,UsedRels), | |
| 311 | remove_unused_idrelations(UsedRels,Idmap,NIdmap), | |
| 312 | get_used_types_in_rels(NIdmap,UsedRels,UsedRels2), | |
| 313 | remove_unused_types(Typemap,UsedRels2,NTypemap). | |
| 314 | ||
| 315 | remove_unused_idrelations(UsedRels,Idmap,NIdmap) :- | |
| 316 | avl_to_list(Idmap,IdList), | |
| 317 | include(is_used_idrelation(UsedRels),IdList,NIdList), | |
| 318 | list_to_avl(NIdList,NIdmap). | |
| 319 | is_used_idrelation(UsedRels,_-reldef(Id,_,_,_,_)) :- memberchk(Id,UsedRels). | |
| 320 | ||
| 321 | get_used_types_in_rels(Idmap,UsedRels,NewUsed) :- | |
| 322 | avl_to_list(Idmap,IdList), | |
| 323 | findall(T, (member(_-reldef(_,Ts,_,_,_),IdList),member(T,Ts)), Types), | |
| 324 | append(UsedRels,Types,U2), | |
| 325 | sort(U2,NewUsed). | |
| 326 | ||
| 327 | remove_unused_types(Typemap,UsedRels,NTypemap) :- | |
| 328 | avl_to_list(Typemap,TypeList), | |
| 329 | include(is_used_type(UsedRels),TypeList,NTypeList), | |
| 330 | list_to_avl(NTypeList,NTypemap). | |
| 331 | is_used_type(UsedRels,_-relation(Id,_,_)) :- memberchk(Id,UsedRels). | |
| 332 | ||
| 333 | get_used_relations(K,UsedRels) :- | |
| 334 | get_used_relations2(K,U,[]), | |
| 335 | sort(U,UsedRels). | |
| 336 | get_used_relations2(relref(Id)) --> !,[Id]. | |
| 337 | get_used_relations2(K) --> | |
| 338 | {compound(K),!,K =.. Args},get_used_relations_l(Args). | |
| 339 | get_used_relations2(_K) --> []. | |
| 340 | get_used_relations_l([]) --> []. | |
| 341 | get_used_relations_l([K|Krest]) --> | |
| 342 | get_used_relations2(K), | |
| 343 | get_used_relations_l(Krest). | |
| 344 | */ |