| 1 | %% AST Node types for fuzzing. | |
| 2 | % This is a subset of the types specified in probsrc(btypechecker) | |
| 3 | % and might be altered. | |
| 4 | ||
| 5 | :- module(fuzztypes, [has_type/2, | |
| 6 | primary_type/1, | |
| 7 | primitive_type/1, | |
| 8 | higher_order_type/1, | |
| 9 | higher_order_sub_types/2, | |
| 10 | child_types/2, | |
| 11 | node_by_name/2, | |
| 12 | node_info/3, | |
| 13 | is_leaf_node/1 | |
| 14 | ]). | |
| 15 | ||
| 16 | :- op(600, xfy, (<:>)). | |
| 17 | ||
| 18 | :- use_module(library(lists), [maplist/2]). | |
| 19 | ||
| 20 | ||
| 21 | has_type(nat_set, set(integer)). % Special case for integer_set('NAT'). | |
| 22 | has_type(natural_set, set(integer)). % Special case for integer_set('NATURAL'). | |
| 23 | has_type(nat1_set, set(integer)). % Special case for integer_set('NAT1'). | |
| 24 | has_type(natural1_set, set(integer)). % Special case for integer_set('NATURAL1'). | |
| 25 | has_type(int_set, set(integer)). % Special case for integer_set('INT'). | |
| 26 | has_type(integer_set, set(integer)). % Special case for integer_set('INTEGER'). | |
| 27 | has_type(Term, Type) :- | |
| 28 | Term <:> Type. | |
| 29 | ||
| 30 | ||
| 31 | primitive_type(integer). | |
| 32 | primitive_type(real). | |
| 33 | % primitive_type(pred). % Note: Never generate a random pred type expression. | |
| 34 | primitive_type(boolean). | |
| 35 | primitive_type(string). | |
| 36 | ||
| 37 | higher_order_type(set(_)). | |
| 38 | higher_order_type(seq(_)). | |
| 39 | higher_order_type(couple(_, _)). | |
| 40 | ||
| 41 | higher_order_sub_types(set(A), [A]). | |
| 42 | higher_order_sub_types(seq(A), [A]). | |
| 43 | higher_order_sub_types(couple(A, B), [A, B]). | |
| 44 | ||
| 45 | primary_type(T) :- primitive_type(T), !. | |
| 46 | primary_type(T) :- | |
| 47 | higher_order_type(T), | |
| 48 | higher_order_sub_types(T, SubTypes), | |
| 49 | maplist(primary_type, SubTypes). | |
| 50 | ||
| 51 | ||
| 52 | ||
| 53 | node_info(Name, Type, Children) :- | |
| 54 | has_type(Node, Type), % TODO: Maybe find version that doesn't traverse all has_type/2 rules. | |
| 55 | Node =.. [Name|Children]. | |
| 56 | ||
| 57 | ||
| 58 | node_by_name(Name, Node) :- | |
| 59 | node_info(Name, _, Children), | |
| 60 | Node =.. [Name|Children]. | |
| 61 | ||
| 62 | ||
| 63 | is_leaf_node(Name) :- | |
| 64 | node_info(Name, _, []). | |
| 65 | ||
| 66 | ||
| 67 | % predicates | |
| 68 | truth <:> pred. | |
| 69 | falsity <:> pred. | |
| 70 | conjunct(pred,pred) <:> pred. | |
| 71 | %conjunct([pred]) <:> pred. | |
| 72 | negation(pred) <:> pred. | |
| 73 | disjunct(pred,pred) <:> pred. | |
| 74 | %disjunct([pred]) <:> pred. | |
| 75 | implication(pred,pred) <:> pred. | |
| 76 | equivalence(pred,pred) <:> pred. | |
| 77 | equal(A,A) <:> pred. | |
| 78 | not_equal(A,A) <:> pred. | |
| 79 | member(A,set(A)) <:> pred. | |
| 80 | not_member(A,set(A)) <:> pred. | |
| 81 | subset(set(A),set(A)) <:> pred. | |
| 82 | subset_strict(set(A),set(A)) <:> pred. | |
| 83 | not_subset(set(A),set(A)) <:> pred. | |
| 84 | not_subset_strict(set(A),set(A)) <:> pred. | |
| 85 | less_equal(integer,integer) <:> pred. | |
| 86 | less(integer,integer) <:> pred. | |
| 87 | less_equal_real(real,real) <:> pred. | |
| 88 | less_real(real,real) <:> pred. | |
| 89 | greater_equal(integer,integer) <:> pred. | |
| 90 | greater(integer,integer) <:> pred. | |
| 91 | finite(set(_)) <:> pred. | |
| 92 | exists(ids,pred) <:> pred. | |
| 93 | forall(ids,pred,pred) <:> pred. % Added by hand | |
| 94 | partition(set(T),[set(T)]) <:> pred. | |
| 95 | ||
| 96 | % expressions | |
| 97 | boolean_true <:> boolean. | |
| 98 | boolean_false <:> boolean. | |
| 99 | max_int <:> integer. | |
| 100 | min_int <:> integer. | |
| 101 | empty_set <:> set(_). | |
| 102 | bool_set <:> set(boolean). | |
| 103 | float_set <:> set(real). | |
| 104 | real_set <:> set(real). | |
| 105 | string_set <:> set(string). | |
| 106 | convert_bool(pred) <:> boolean. | |
| 107 | convert_real(integer) <:> real. | |
| 108 | convert_int_floor(real) <:> integer. | |
| 109 | convert_int_ceiling(real) <:> integer. | |
| 110 | add(integer,integer) <:> integer. | |
| 111 | add_real(real,real) <:> real. | |
| 112 | minus(integer,integer) <:> integer. | |
| 113 | minus_real(real,real) <:> real. | |
| 114 | unary_minus(integer) <:> integer. | |
| 115 | unary_minus_real(real) <:> real. | |
| 116 | multiplication(integer,integer) <:> integer. | |
| 117 | multiplication_real(real,real) <:> real. | |
| 118 | cartesian_product(set(A),set(B)) <:> set(couple(A,B)). | |
| 119 | div(integer,integer) <:> integer. | |
| 120 | div_real(real,real) <:> real. | |
| 121 | floored_div(integer,integer) <:> integer. | |
| 122 | modulo(integer,integer) <:> integer. | |
| 123 | power_of(integer,integer) <:> integer. | |
| 124 | power_of_real(real,real) <:> real. | |
| 125 | successor <:> set(couple(integer,integer)). | |
| 126 | predecessor <:> set(couple(integer,integer)). | |
| 127 | max(set(integer)) <:> integer. | |
| 128 | min(set(integer)) <:> integer. | |
| 129 | max_real(set(real)) <:> real. | |
| 130 | min_real(set(real)) <:> real. | |
| 131 | card(set(_)) <:> integer. | |
| 132 | couple(A,B) <:> couple(A,B). | |
| 133 | pow_subset(set(A)) <:> set(set(A)). | |
| 134 | pow1_subset(set(A)) <:> set(set(A)). | |
| 135 | fin_subset(set(A)) <:> set(set(A)). | |
| 136 | fin1_subset(set(A)) <:> set(set(A)). | |
| 137 | interval(integer,integer) <:> set(integer). | |
| 138 | union(set(A),set(A)) <:> set(A). | |
| 139 | intersection(set(A),set(A)) <:> set(A). | |
| 140 | set_subtraction(set(A),set(A)) <:> set(A). /* ?? */ | |
| 141 | general_union(set(set(A))) <:> set(A). | |
| 142 | general_intersection(set(set(A))) <:> set(A). | |
| 143 | relations(set(A),set(B)) <:> set(set(couple(A,B))). | |
| 144 | identity(set(A)) <:> set(couple(A,A)). | |
| 145 | reverse(set(couple(A,B))) <:> set(couple(B,A)). % function inverse ~ | |
| 146 | first_projection(set(A),set(B)) <:> set(couple(couple(A,B),A)). | |
| 147 | % event_b_first_projection(set(couple(A,B))) <:> set(couple(couple(A,B),A)). % should no longer appear after Rodin 1.0 | |
| 148 | second_projection(set(A),set(B)) <:> set(couple(couple(A,B),B)). | |
| 149 | % event_b_second_projection(set(couple(A,B))) <:> set(couple(couple(A,B),B)). % should no longer appear after Rodin 1.0 | |
| 150 | first_of_pair(couple(A,_)) <:> A. % new | |
| 151 | second_of_pair(couple(_,B)) <:> B. % new | |
| 152 | composition(set(couple(A,B)),set(couple(B,C))) <:> set(couple(A,C)). | |
| 153 | ring(set(couple(B,C)),set(couple(A,B))) <:> set(couple(A,C)). | |
| 154 | direct_product(set(couple(E,F)),set(couple(E,G))) <:> set(couple(E,couple(F,G))). | |
| 155 | parallel_product(set(couple(E,F)),set(couple(G,H))) <:> set(couple(couple(E,G),couple(F,H))). | |
| 156 | trans_function(set(couple(A,B))) <:> set(couple(A,set(B))). | |
| 157 | trans_relation(set(couple(A,set(B)))) <:> set(couple(A,B)). | |
| 158 | iteration(set(couple(A,A)),integer) <:> set(couple(A,A)). | |
| 159 | reflexive_closure(set(couple(A,A))) <:> set(couple(A,A)). | |
| 160 | closure(set(couple(A,A))) <:> set(couple(A,A)). | |
| 161 | domain(set(couple(A,_))) <:> set(A). | |
| 162 | range(set(couple(_,B))) <:> set(B). | |
| 163 | image(set(couple(A,B)),set(A)) <:> set(B). | |
| 164 | domain_restriction(set(A),set(couple(A,B))) <:> set(couple(A,B)). | |
| 165 | domain_subtraction(set(A),set(couple(A,B))) <:> set(couple(A,B)). | |
| 166 | range_restriction(set(couple(A,B)),set(B)) <:> set(couple(A,B)). | |
| 167 | range_subtraction(set(couple(A,B)),set(B)) <:> set(couple(A,B)). | |
| 168 | overwrite(set(couple(A,B)),set(couple(A,B))) <:> set(couple(A,B)). | |
| 169 | partial_function(A,B)<:>T :- relations(A,B)<:>T. | |
| 170 | total_function(A,B)<:>T :- relations(A,B)<:>T. | |
| 171 | partial_injection(A,B)<:>T :- relations(A,B)<:>T. | |
| 172 | total_injection(A,B)<:>T :- relations(A,B)<:>T. | |
| 173 | partial_surjection(A,B)<:>T :- relations(A,B)<:>T. | |
| 174 | total_surjection(A,B)<:>T :- relations(A,B)<:>T. | |
| 175 | total_bijection(A,B)<:>T :- relations(A,B)<:>T. | |
| 176 | partial_bijection(A,B)<:>T :- relations(A,B)<:>T. | |
| 177 | total_relation(A,B)<:>T :- relations(A,B)<:>T. | |
| 178 | surjection_relation(A,B)<:>T :- relations(A,B)<:>T. | |
| 179 | total_surjection_relation(A,B)<:>T :- relations(A,B)<:>T. | |
| 180 | seq(set(A)) <:> set(seq(A)). | |
| 181 | seq1(X)<:>T :- seq(X)<:>T. | |
| 182 | iseq(X)<:>T :- seq(X)<:>T. | |
| 183 | iseq1(X)<:>T :- seq(X)<:>T. | |
| 184 | perm(set(A)) <:> set(seq(A)). | |
| 185 | empty_sequence <:> seq(_). | |
| 186 | size(seq(_)) <:> integer. | |
| 187 | first(seq(A)) <:> A. | |
| 188 | last(seq(A)) <:> A. | |
| 189 | front(seq(A)) <:> seq(A). | |
| 190 | tail(seq(A)) <:> seq(A). | |
| 191 | rev(seq(A)) <:> seq(A). | |
| 192 | concat(seq(A),seq(A)) <:> seq(A). | |
| 193 | insert_front(A,seq(A)) <:> seq(A). | |
| 194 | insert_tail(seq(A),A) <:> seq(A). | |
| 195 | restrict_front(seq(A),integer) <:> seq(A). | |
| 196 | restrict_tail(seq(A),integer) <:> seq(A). | |
| 197 | general_concat(seq(seq(A))) <:> seq(A). | |
| 198 | function(set(couple(A,B)),A) <:> B. | |
| 199 | set_extension([T]) <:> set(T). | |
| 200 | sequence_extension([T]) <:> seq(T). | |
| 201 | comprehension_set(ids(T),pred) <:> set(T). % ids(T) means T is the cross product of all types in the ID list. | |
| 202 | event_b_comprehension_set(ids,T,pred) <:> set(T). | |
| 203 | lambda(ids(A),pred,R) <:> set(couple(A,R)). % ids(A) means A is the cross product of all types in the ID list. | |
| 204 | general_sum(ids,pred,T) <:> T :- member(T, [integer,real]). | |
| 205 | general_product(ids,pred,T) <:> T :- member(T, [integer,real]). | |
| 206 | quantified_union(ids,pred,set(T)) <:> set(T). | |
| 207 | quantified_intersection(ids,pred,set(T)) <:> set(T). | |
| 208 | mu(set(T)) <:> T. | |
| 209 | if_then_else(pred,T,T) <:> T. | |
| 210 | % tree(set(A)) <:> set(set(couple(seq(integer),A))). % Section 5.20 of Atelier-B manrefb.pdf | |
| 211 | % btree(A) <:> T :- tree(A) <:> T. | |
| 212 | % tree_over(A) <:> set(couple(seq(integer),A)). % dummy function to ease writing of rules below | |
| 213 | % const(A,seq(TreeA)) <:> TreeA :- tree_over(A) <:> TreeA. | |
| 214 | % top(TreeA) <:> A :- tree_over(A) <:> TreeA. | |
| 215 | % prefix(TreeA) <:> seq(A) :- tree_over(A) <:> TreeA. | |
| 216 | % postfix(TreeA) <:> seq(A) :- tree_over(A) <:> TreeA. | |
| 217 | % sizet(TreeA) <:> integer :- tree_over(_) <:> TreeA. | |
| 218 | % mirror(TreeA) <:> TreeA :- tree_over(_) <:> TreeA. | |
| 219 | % rank(TreeA,seq(integer)) <:> integer :- tree_over(_) <:> TreeA. % seq(integer) is the type of paths | |
| 220 | % father(TreeA,seq(integer)) <:> seq(integer) :- tree_over(_) <:> TreeA. | |
| 221 | % son(TreeA,seq(integer),integer) <:> seq(integer) :- tree_over(_) <:> TreeA. | |
| 222 | % subtree(TreeA,seq(integer)) <:> TreeA :- tree_over(_) <:> TreeA. | |
| 223 | % arity(TreeA,seq(integer)) <:> integer :- tree_over(_) <:> TreeA. | |
| 224 | % sons(TreeA) <:> seq(TreeA) :- tree_over(_) <:> TreeA. | |
| 225 | % bin(A) <:> TreeA :- tree_over(A) <:> TreeA. | |
| 226 | % bin(TreeA,A,TreeA) <:> TreeA :- tree_over(A) <:> TreeA. | |
| 227 | % infix(TreeA) <:> seq(A) :- tree_over(A) <:> TreeA. | |
| 228 | % left(TreeA) <:> TreeA :- tree_over(_) <:> TreeA. | |
| 229 | % right(TreeA) <:> TreeA :- tree_over(_) <:> TreeA. | |
| 230 | ||
| 231 | child_types(NodeName, Children) :- | |
| 232 | has_type(Node, _), | |
| 233 | Node =.. [NodeName|Children], | |
| 234 | !. |