Skip to content

Commit 566ee7b

Browse files
DavePearceDavePearce
committed
Merge branch 'feature/14-requires' into develop
2 parents d0c5c43 + 69c8b10 commit 566ee7b

File tree

9 files changed

+116
-80
lines changed

9 files changed

+116
-80
lines changed

‎config.xml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
<project name="BuildConfig">
2-
<property name="version" value="0.4.1"/>
2+
<property name="version" value="0.4.2"/>
33
<property name="WYBS_JAR" value="lib/wybs-v0.3.34.jar"/>
44
</project>

‎examples/types/Types.wyrl

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -38,17 +38,19 @@ reduce Intersect{Type x}:
3838
reduce Intersect{Not(Any), Type... xs}:
3939
=> Not(Any)
4040

41-
reduce Intersect{Any, Type... xs}:
42-
=> Intersect (xs), if |xs| > 0
41+
reduce Intersect{Any, Type... xs}
42+
requires |xs| > 0:
43+
=> Intersect (xs)
4344

4445
reduce Intersect{Int, Pair y, Type... ys}:
4546
=> Not(Any)
4647

4748
reduce Intersect{Intersect{Type... xs}, Type... ys}:
4849
=> Intersect (xs ++ ys)
4950

50-
reduce Intersect{Not(Type x), Type y, Type... ys}:
51-
=> Not(Any), if x == y
51+
reduce Intersect{Not(Type x), Type y, Type... ys}
52+
requires x == y:
53+
=> Not(Any)
5254

5355
reduce Intersect{Union{Type... xs}, Type... ys}:
5456
=> let ys = { Intersect(x ++ ys) | x in xs }
@@ -76,8 +78,9 @@ reduce Union{Not(Any), Type... xs}:
7678
=> Union (xs), if |xs| > 0
7779
=> Not(Any)
7880

79-
reduce Union{Not(Type x), Type y, Type... ys}:
80-
=> Any, if x == y
81+
reduce Union{Not(Type x), Type y, Type... ys}
82+
requires x == y:
83+
=> Any
8184

8285
reduce Union{Union{Type... xs}, Type... ys}:
8386
=> Union (xs ++ ys)

‎src/wyrl/core/SpecFile.java

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -89,27 +89,29 @@ public TypeDecl(String n, Type type, boolean isOpen, Map<String,Object> annotati
8989

9090
public static abstract class RewriteDecl extends AnnotableDecl {
9191
public Pattern.Term pattern;
92+
public Expr requires;
9293
public final ArrayList<RuleDecl> rules;
9394

94-
public RewriteDecl(Pattern.Term pattern, Collection<RuleDecl> rules,
95+
public RewriteDecl(Pattern.Term pattern, Expr requires, Collection<RuleDecl> rules,
9596
Map<String,Object> annotations, Attribute... attributes) {
9697
super(annotations, attributes);
9798
this.pattern = pattern;
99+
this.requires = requires;
98100
this.rules = new ArrayList<RuleDecl>(rules);
99101
}
100102
}
101103

102104
public static class ReduceDecl extends RewriteDecl {
103-
public ReduceDecl(Pattern.Term pattern, Collection<RuleDecl> rules,
105+
public ReduceDecl(Pattern.Term pattern, Expr requires, Collection<RuleDecl> rules,
104106
Map<String,Object> annotations, Attribute... attributes) {
105-
super(pattern,rules,annotations,attributes);
107+
super(pattern,requires,rules,annotations,attributes);
106108
}
107109
}
108110

109111
public static class InferDecl extends RewriteDecl {
110-
public InferDecl(Pattern.Term pattern, Collection<RuleDecl> rules, Map<String, Object> annotations,
112+
public InferDecl(Pattern.Term pattern, Expr requires, Collection<RuleDecl> rules, Map<String, Object> annotations,
111113
Attribute... attributes) {
112-
super(pattern,rules,annotations,attributes);
114+
super(pattern,requires,rules,annotations,attributes);
113115
}
114116
}
115117

‎src/wyrl/core/TypeExpansion.java

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -83,6 +83,9 @@ protected void expandTypeTests(SpecFile spec,
8383
expandTypeTests(id.file, terms, macros);
8484
} else if (d instanceof SpecFile.RewriteDecl) {
8585
SpecFile.RewriteDecl td = (SpecFile.RewriteDecl) d;
86+
if(td.requires != null) {
87+
expandTypeTests(td.requires,spec,macros);
88+
}
8689
for(SpecFile.RuleDecl rd : td.rules) {
8790
expandTypeTests(rd,spec,terms,macros);
8891
}

‎src/wyrl/core/TypeInference.java

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,13 @@ public void infer(SpecFile.RewriteDecl rd) {
9595
Type.Ref thisType = infer(rd.pattern,environment);
9696
// The "this" variable can be used to access the outermost rule.
9797
environment.put("this",thisType);
98-
98+
// Infer types for the requires clause (if present)
99+
if(rd.requires != null) {
100+
Pair<Expr,Type> p = resolve(rd.requires,environment);
101+
rd.requires = p.first();
102+
checkSubtype(Type.T_BOOL(),p.second(),rd.requires);
103+
}
104+
// Now, infer types for the individual rule declarations
99105
for(SpecFile.RuleDecl rule : rd.rules) {
100106
infer(rule,environment);
101107
}

‎src/wyrl/io/JavaFileWriter.java

Lines changed: 75 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -282,7 +282,14 @@ public void translate(RewriteDecl decl, SpecFile file) {
282282
myOut(3, "int r" + thus + " = target;");
283283
int level = translatePatternMatch(3, decl.pattern, null, thus,
284284
environment);
285-
285+
if (decl.requires != null) {
286+
// FIXME: this is not necessarily always required
287+
Environment reqEnvironment = new Environment();
288+
reqEnvironment.allocate(param, "this");
289+
translateStateUnpack(level,decl.pattern,thus,false,reqEnvironment);
290+
int requires = translate(level, decl.requires, reqEnvironment, file);
291+
myOut(level++, "if(r" + requires + ") { // REQUIRES");
292+
}
286293
// Add the appropriate activation
287294
indent(level);
288295
out.print("int[] state = {");
@@ -329,7 +336,7 @@ public void translate(RewriteDecl decl, SpecFile file) {
329336
environment = new Environment();
330337
thus = environment.allocate(param, "this");
331338
myOut(3, "int r" + thus + " = state[0];");
332-
translateStateUnpack(3, decl.pattern, thus, environment);
339+
translateStateUnpack(3, decl.pattern, thus, true, environment);
333340

334341
// second, translate the individual rules
335342
for (RuleDecl rd : decl.rules) {
@@ -876,40 +883,40 @@ protected boolean willSkip(Pattern pattern, Type declared) {
876883
* @param environment
877884
*/
878885
protected void translateStateUnpack(int level, Pattern pattern, int source,
879-
Environment environment) {
886+
boolean unpack, Environment environment) {
880887
if (pattern instanceof Pattern.Leaf) {
881888
translateStateUnpack(level, (Pattern.Leaf) pattern, source,
882-
environment);
889+
unpack, environment);
883890
} else if (pattern instanceof Pattern.Term) {
884891
translateStateUnpack(level, (Pattern.Term) pattern, source,
885-
environment);
892+
unpack, environment);
886893
} else if (pattern instanceof Pattern.BagOrSet) {
887894
translateStateUnpack(level, (Pattern.BagOrSet) pattern, source,
888-
environment);
895+
unpack, environment);
889896
} else {
890897
translateStateUnpack(level, (Pattern.List) pattern, source,
891-
environment);
898+
unpack, environment);
892899
}
893900
}
894901

895902
protected void translateStateUnpack(int level, Pattern.Leaf pattern,
896-
int source, Environment environment) {
903+
int source, boolean unpack, Environment environment) {
897904
// Don't need to do anything!!
898905
}
899906

900907
protected void translateStateUnpack(int level, Pattern.Term pattern,
901-
int source, Environment environment) {
908+
int source, boolean unpack, Environment environment) {
902909
if (pattern.data != null) {
903910
int target = environment.allocate(Type.T_ANY(), pattern.variable);
904-
if (pattern.variable != null) {
911+
if (pattern.variable != null && unpack) {
905912
myOut(level, "int r" + target + " = state[" + target + "]; // " + pattern.variable);
906913
}
907-
translateStateUnpack(level, pattern.data, target, environment);
914+
translateStateUnpack(level, pattern.data, target, unpack, environment);
908915
}
909916
}
910917

911918
protected void translateStateUnpack(int level, Pattern.BagOrSet pattern,
912-
int source, Environment environment) {
919+
int source, boolean unpack, Environment environment) {
913920

914921
Pair<Pattern, String>[] elements = pattern.elements;
915922
int[] indices = new int[elements.length];
@@ -919,31 +926,7 @@ protected void translateStateUnpack(int level, Pattern.BagOrSet pattern,
919926
int item = environment.allocate(Type.T_ANY(), p_name);
920927
if (pattern.unbounded && (i + 1) == elements.length) {
921928
if (p_name != null) {
922-
String src = "s" + source;
923-
myOut(level, "Automaton.Collection " + src
924-
+ " = (Automaton.Collection) automaton.get(state["
925-
+ source + "]);");
926-
String array = src + "children";
927-
myOut(level, "int[] " + array + " = new int[" + src
928-
+ ".size() - " + i + "];");
929-
String idx = "s" + source + "i";
930-
String jdx = "s" + source + "j";
931-
myOut(level, "for(int " + idx + "=0, " + jdx + "=0; " + idx
932-
+ " != " + src + ".size();++" + idx + ") {");
933-
if (i != 0) {
934-
indent(level + 1);
935-
out.print("if(");
936-
for (int j = 0; j < i; ++j) {
937-
if (j != 0) {
938-
out.print(" || ");
939-
}
940-
out.print(idx + " == r" + indices[j]);
941-
}
942-
out.println(") { continue; }");
943-
}
944-
myOut(level + 1, array + "[" + jdx + "++] = " + src + ".get(" + idx
945-
+ ");");
946-
myOut(level, "}");
929+
String array = extractUnboundedTail(i, level, source, indices, unpack);
947930
if (pattern instanceof Pattern.Set) {
948931
myOut(level, "Automaton.Set r" + item
949932
+ " = new Automaton.Set(" + array + ");");
@@ -960,17 +943,59 @@ protected void translateStateUnpack(int level, Pattern.BagOrSet pattern,
960943
} else {
961944
int index = environment.allocate(Type.T_VOID());
962945
indices[i] = index;
963-
if (p_name != null) {
946+
if (p_name != null && unpack) {
964947
myOut(level, "int r" + item + " = state[" + item + "]; // " + p_name);
965948
}
966-
myOut(level, "int r" + index + " = state[" + index + "];");
967-
translateStateUnpack(level, p.first(), item, environment);
949+
if(unpack) {
950+
myOut(level, "int r" + index + " = state[" + index + "];");
951+
}
952+
translateStateUnpack(level, p.first(), item, unpack, environment);
953+
}
954+
}
955+
}
956+
957+
/**
958+
* Extract all elements of an array which don't match any of the supplied
959+
* indices.
960+
*
961+
* @param i
962+
* @param level
963+
* @param source
964+
* @param indices
965+
* @return
966+
*/
967+
private String extractUnboundedTail(int i, int level, int source, int[] indices, boolean unpack) {
968+
String src = "c" + source;
969+
if (unpack) {
970+
myOut(level,
971+
"Automaton.Collection " + src + " = (Automaton.Collection) automaton.get(state[" + source + "]);");
972+
}
973+
String array = src + "children";
974+
myOut(level, "int[] " + array + " = new int[" + src
975+
+ ".size() - " + i + "];");
976+
String idx = "s" + source + "i";
977+
String jdx = "s" + source + "j";
978+
myOut(level, "for(int " + idx + "=0, " + jdx + "=0; " + idx
979+
+ " != " + src + ".size();++" + idx + ") {");
980+
if (i != 0) {
981+
indent(level + 1);
982+
out.print("if(");
983+
for (int j = 0; j < i; ++j) {
984+
if (j != 0) {
985+
out.print(" || ");
986+
}
987+
out.print(idx + " == r" + indices[j]);
968988
}
989+
out.println(") { continue; }");
969990
}
991+
myOut(level + 1, array + "[" + jdx + "++] = " + src + ".get(" + idx
992+
+ ");");
993+
myOut(level, "}");
994+
return array;
970995
}
971996

972997
protected void translateStateUnpack(int level, Pattern.List pattern,
973-
int source, Environment environment) {
998+
int source, boolean unpack, Environment environment) {
974999

9751000
Pair<Pattern, String>[] elements = pattern.elements;
9761001
for (int i = 0; i != elements.length; ++i) {
@@ -979,9 +1004,13 @@ protected void translateStateUnpack(int level, Pattern.List pattern,
9791004
if (pattern.unbounded && (i + 1) == elements.length) {
9801005
int target = environment.allocate(Type.T_VOID(), p_name);
9811006
if (p_name != null) {
982-
myOut(level, "Automaton.List r" + target
983-
+ " = ((Automaton.List) automaton.get(state["
984-
+ source + "])).sublist(" + i + ");");
1007+
if (unpack) {
1008+
myOut(level, "Automaton.List r" + target
1009+
+ " = ((Automaton.List) automaton.get(state["
1010+
+ source + "])).sublist(" + i + ");");
1011+
} else {
1012+
myOut(level, "Automaton.List r" + target + " = l" + source + ";");
1013+
}
9851014
}
9861015

9871016
// NOTE: calling translate unpack here is strictly unnecessary
@@ -990,10 +1019,10 @@ protected void translateStateUnpack(int level, Pattern.List pattern,
9901019

9911020
} else {
9921021
int target = environment.allocate(Type.T_ANY(), p_name);
993-
if (p_name != null) {
1022+
if (p_name != null && unpack) {
9941023
myOut(level, "int r" + target + " = state[" + target + "]; // " + p_name);
9951024
}
996-
translateStateUnpack(level, p.first(), target, environment);
1025+
translateStateUnpack(level, p.first(), target, unpack, environment);
9971026
}
9981027
}
9991028
}

‎src/wyrl/io/SpecLexer.java

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -468,6 +468,7 @@ public boolean isIdentifierStart(char c) {
468468
"define",
469469
"reduce",
470470
"infer",
471+
"requires",
471472
"function",
472473
"let",
473474
"num",

‎src/wyrl/io/SpecParser.java

Lines changed: 12 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -244,38 +244,30 @@ private Decl parseRewriteDecl(Map<String,Object> annotations) {
244244
reduce = false;
245245
}
246246
Pattern.Term pattern = (Pattern.Term) parsePatternTerm();
247+
Expr requires = parseRequiresClause();
247248
match(Colon.class);
248249
matchEndLine();
249250
List<RuleDecl> rules = parseRuleBlock(1);
250251

251252
if(reduce) {
252-
return new ReduceDecl(pattern,rules,annotations,sourceAttr(start,index-1));
253+
return new ReduceDecl(pattern,requires,rules,annotations,sourceAttr(start,index-1));
253254
} else {
254-
return new InferDecl(pattern,rules,annotations,sourceAttr(start,index-1));
255+
return new InferDecl(pattern,requires,rules,annotations,sourceAttr(start,index-1));
255256
}
256257
}
257258

258-
private Pair<String,Integer> parseNameAndRank() {
259-
String name = "";
260-
int rank = 0;
259+
private Expr parseRequiresClause() {
261260
skipWhiteSpace(true);
262-
Token lookahead = tokens.get(index);
263-
if(lookahead.text.equals("name")) {
264-
matchKeyword("name");
265-
Strung s = match(Strung.class);
266-
name = s.text.substring(1,s.text.length()-1);
267-
}
268-
skipWhiteSpace(true);
269-
lookahead = tokens.get(index);
270-
if(lookahead.text.equals("rank")) {
271-
matchKeyword("rank");
272-
Int i = match(Int.class);
273-
rank = i.value.intValue();
261+
if (index < tokens.size() && tokens.get(index).text.equals("requires")) {
262+
matchKeyword("requires");
263+
Expr result = parseCondition();
264+
skipWhiteSpace(true);
265+
return result;
266+
} else {
267+
return null;
274268
}
275-
276-
return new Pair<String,Integer>(name,rank);
277269
}
278-
270+
279271
private Decl parseFunctionDecl(Map<String,Object> annotations) {
280272
int start = index;
281273
matchKeyword("function");

‎src/wyrw/core/Inference.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ public class Inference extends AbstractRewrite {
2424
* performance and it remains unclear whether or not isomorphic automata are
2525
* actually a problem in practice.
2626
*/
27-
public static final boolean USE_SUBSTITUTION = false;
27+
public static final boolean USE_SUBSTITUTION = true;
2828

2929
private final int MAX_REDUCTIONS = 10000;
3030

0 commit comments

Comments
 (0)