Commit 10f6693e authored by Alexander Weigl's avatar Alexander Weigl

grammar restructured

 * if/while/strict/relax added
 * no rt adaptions
parent 3d79d1fe
...@@ -28,12 +28,11 @@ stmtList ...@@ -28,12 +28,11 @@ stmtList
statement statement
: //scriptDecl : //scriptDecl
assignment assignment
| repeatStmt | casesStmt
| casesStmt | scriptCommand
| forEachStmt | unconditionalBlock
| theOnlyStmt | conditionalBlock
| scriptCommand
// | callStmt // | callStmt
; ;
...@@ -102,10 +101,6 @@ scriptVar ...@@ -102,10 +101,6 @@ scriptVar
; ;
repeatStmt
: REPEAT INDENT stmtList DEDENT
;
casesStmt casesStmt
: CASES INDENT : CASES INDENT
casesList* casesList*
...@@ -126,12 +121,12 @@ casesList ...@@ -126,12 +121,12 @@ casesList
: CLOSES INDENT closesGuard=stmtList DEDENT : CLOSES INDENT closesGuard=stmtList DEDENT
;*/ ;*/
forEachStmt unconditionalBlock
: FOREACH INDENT stmtList DEDENT : (kind+=(FOREACH|THEONLY|STRICT|RELAX|REPEAT))+ IDENT stmtList DEDENT
; ;
theOnlyStmt conditionalBlock
: THEONLY INDENT stmtList DEDENT : kind=(IF|WHILE) LPAREN expression RPAREN IDENT stmtList DEDENT
; ;
...@@ -176,14 +171,16 @@ BOOL: 'bool' ; ...@@ -176,14 +171,16 @@ BOOL: 'bool' ;
TERMTYPE : 'term' ;*/ TERMTYPE : 'term' ;*/
FOREACH : 'foreach' ; FOREACH : 'foreach' ;
THEONLY : 'theonly' ; THEONLY : 'theonly' ;
STRICT : 'strict' ;
RELAX : 'relax';
IF:'if';
WHILE:'while';
INDENT : '{' ; INDENT : '{' ;
DEDENT : '}' ; DEDENT : '}' ;
SEMICOLON : ';' ; SEMICOLON : ';' ;
COLON : ':' ; COLON : ':' ;
HEAPSIMP:'heap-simp';
SUBST_TO: '\\'; SUBST_TO: '\\';
STRING_LITERAL STRING_LITERAL
: '\'' ('\'\'' | ~ ('\''))* '\'' : '\'' ('\'\'' | ~ ('\''))* '\''
; ;
......
package edu.kit.iti.formal.psdbg.parser; package edu.kit.iti.formal.psdbg.parser;
/*- /*-
* #%L * #%L
* ProofScriptParser * ProofScriptParser
* %% * %%
* Copyright (C) 2017 Application-oriented Formal Verification * Copyright (C) 2017 Application-oriented Formal Verification
* %% * %%
* This program is free software: you can redistribute it and/or modify * This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General default License as * it under the terms of the GNU General default License as
* published by the Free Software Foundation, either version 3 of the * published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version. * License, or (at your option) any later version.
* *
* This program is distributed in the hope that it will be useful, * This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of * but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General default License for more details. * GNU General default License for more details.
* *
* You should have received a copy of the GNU General default * You should have received a copy of the GNU General default
* License along with this program. If not, see * License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>. * <http://www.gnu.org/licenses/gpl-3.0.html>.
* #L% * #L%
*/ */
import edu.kit.iti.formal.psdbg.parser.ast.*; import edu.kit.iti.formal.psdbg.parser.ast.*;
...@@ -200,4 +200,30 @@ public interface ASTTraversal<T> extends Visitor<T> { ...@@ -200,4 +200,30 @@ public interface ASTTraversal<T> extends Visitor<T> {
func.getArguments().forEach(a -> a.accept(this)); func.getArguments().forEach(a -> a.accept(this));
return null; return null;
} }
@Override
default T visit(WhileStatement ws) {
ws.getCondition().accept(this);
ws.getBody().accept(this);
return null;
}
@Override
default T visit(IfStatement is) {
is.getCondition().accept(this);
is.getBody().accept(this);
return null;
}
@Override
default T visit(StrictBlock strictBlock) {
strictBlock.getBody().accept(this);
return null;
}
@Override
default T visit(RelaxBlock relaxBlock) {
relaxBlock.getBody().accept(this);
return null;
}
} }
...@@ -156,5 +156,25 @@ public class DefaultASTVisitor<T> implements Visitor<T> { ...@@ -156,5 +156,25 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
public T visit(FunctionCall func) { public T visit(FunctionCall func) {
return defaultVisit(func); return defaultVisit(func);
} }
@Override
public T visit(WhileStatement ws) {
return defaultVisit(ws);
}
@Override
public T visit(IfStatement is) {
return defaultVisit(is);
}
@Override
public T visit(StrictBlock strictBlock) {
return defaultVisit(strictBlock);
}
@Override
public T visit(RelaxBlock relaxBlock) {
return defaultVisit(relaxBlock);
}
} }
...@@ -318,6 +318,51 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> { ...@@ -318,6 +318,51 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
return null; return null;
} }
@Override
public Void visit(DefaultCaseStatement defCase) {
return super.visit(defCase);
}
@Override
public Void visit(CaseStatement caseStatement) {
return super.visit(caseStatement);
}
@Override
public Void visit(SubstituteExpression subst) {
return super.visit(subst);
}
@Override
public Void visit(TryCase TryCase) {
return super.visit(TryCase);
}
@Override
public Void visit(ClosesCase closesCase) {
return super.visit(closesCase);
}
@Override
public Void visit(WhileStatement ws) {
return super.visit(ws);
}
@Override
public Void visit(IfStatement is) {
return super.visit(is);
}
@Override
public Void visit(StrictBlock strictBlock) {
return super.visit(strictBlock);
}
@Override
public Void visit(RelaxBlock relaxBlock) {
return super.visit(relaxBlock);
}
//region Printers little helper //region Printers little helper
private int getLastNewline() { private int getLastNewline() {
......
package edu.kit.iti.formal.psdbg.parser; package edu.kit.iti.formal.psdbg.parser;
/*- /*-
* #%L * #%L
* ProofScriptParser * ProofScriptParser
* %% * %%
* Copyright (C) 2017 Application-oriented Formal Verification * Copyright (C) 2017 Application-oriented Formal Verification
* %% * %%
* This program is free software: you can redistribute it and/or modify * This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as * it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the * published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version. * License, or (at your option) any later version.
* *
* This program is distributed in the hope that it will be useful, * This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of * but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details. * GNU General Public License for more details.
* *
* You should have received a copy of the GNU General Public * You should have received a copy of the GNU General Public
* License along with this program. If not, see * License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>. * <http://www.gnu.org/licenses/gpl-3.0.html>.
* #L% * #L%
*/ */
import edu.kit.iti.formal.psdbg.parser.ast.*; import edu.kit.iti.formal.psdbg.parser.ast.*;
...@@ -39,26 +39,61 @@ import java.util.ArrayList; ...@@ -39,26 +39,61 @@ import java.util.ArrayList;
import java.util.LinkedHashMap; import java.util.LinkedHashMap;
import java.util.List; import java.util.List;
import java.util.Map; import java.util.Map;
import java.util.function.Function;
import java.util.stream.Collectors; import java.util.stream.Collectors;
/** /**
* @author Alexander Weigl * @author Alexander Weigl
* @version 2 (29.10.17), introduction of parent * @version 2 (29.10.17), introduction of parent
* version 1 (27.04.17) * version 1 (27.04.17)
*/ */
public class TransformAst implements ScriptLanguageVisitor<Object> { public class TransformAst implements ScriptLanguageVisitor<Object> {
/** /**
* Start index for positional arguments for command calls * Start index for positional arguments for command calls
*/ */
public static final int KEY_START_INDEX_PARAMETER = 2; public static final int KEY_START_INDEX_PARAMETER = 2;
@Getter @Getter
private final List<ProofScript> scripts = new ArrayList<>(10); private final List<ProofScript> scripts = new ArrayList<>(10);
@Getter @Getter
@Setter @Setter
private FunctionRegister functionRegister = new FunctionRegister(); private FunctionRegister functionRegister = new FunctionRegister();
private Function<String, UnconditionalBlock> ubFactory;
private Function<String, ConditionalBlock> cbFactory;
public TransformAst() { public TransformAst() {
functionRegister.loadDefault(); functionRegister.loadDefault();
ubFactory = (id -> {
switch (id) {
case "foreach":
return new ForeachStatement();
case "theonly":
return new TheOnlyStatement();
case "repeat":
return new RepeatStatement();
case "relax":
return new RelaxBlock();
case "strict":
return new StrictBlock();
default:
throw new RuntimeException("Block " + id + " is not known.");
}
});
cbFactory = (id -> {
switch (id) {
case "if":
return new IfStatement();
case "while":
return new WhileStatement();
default:
throw new RuntimeException("Block " + id + " is not known.");
}
});
} }
@Override @Override
...@@ -268,11 +303,11 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -268,11 +303,11 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
} }
@Override @Override
public Map<String, Expression> visitSubstExpressionList(ScriptLanguageParser.SubstExpressionListContext ctx) { public Map<String, Expression<ParserRuleContext>> visitSubstExpressionList(ScriptLanguageParser.SubstExpressionListContext ctx) {
Map<String, Expression> map = new LinkedHashMap<>(); Map<String, Expression<ParserRuleContext>> map = new LinkedHashMap<>();
for (int i = 0; i < ctx.scriptVar().size(); i++) { for (int i = 0; i < ctx.scriptVar().size(); i++) {
map.put(ctx.scriptVar(i).getText(), map.put(ctx.scriptVar(i).getText(),
(Expression) ctx.expression(i).accept(this)); (Expression<ParserRuleContext>) ctx.expression(i).accept(this));
} }
return map; return map;
} }
...@@ -335,16 +370,6 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -335,16 +370,6 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
throw new IllegalStateException("not implemented"); throw new IllegalStateException("not implemented");
} }
@Override
public Object visitRepeatStmt(ScriptLanguageParser.RepeatStmtContext ctx) {
RepeatStatement rs = new RepeatStatement();
rs.setRuleContext(ctx);
Statements body = (Statements) ctx.stmtList().accept(this);
rs.setBody(body);
body.setParent(rs);
return rs;
}
@Override @Override
public Object visitCasesStmt(ScriptLanguageParser.CasesStmtContext ctx) { public Object visitCasesStmt(ScriptLanguageParser.CasesStmtContext ctx) {
CasesStatement cases = new CasesStatement(); CasesStatement cases = new CasesStatement();
...@@ -388,25 +413,32 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -388,25 +413,32 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
@Override @Override
public Object visitForEachStmt(ScriptLanguageParser.ForEachStmtContext ctx) { public UnconditionalBlock visitUnconditionalBlock(ScriptLanguageParser.UnconditionalBlockContext ctx) {
ForeachStatement f = new ForeachStatement(); List<UnconditionalBlock> list = ctx.kind.stream().map(token -> ubFactory.apply(token.getText())).collect(Collectors.toList());
f.setRuleContext(ctx); UnconditionalBlock first = list.get(0);
UnconditionalBlock last = list.stream().reduce((a, b) -> {
b.setParent(a);
a.getBody().add(b);
return b;
}).orElse(first);
list.forEach(a -> a.setRuleContext(ctx));
Statements body = (Statements) ctx.stmtList().accept(this); Statements body = (Statements) ctx.stmtList().accept(this);
f.setBody(body); last.setBody(body);
body.setParent(f); body.setParent(last);
return f; return first;
} }
@Override @Override
public Object visitTheOnlyStmt(ScriptLanguageParser.TheOnlyStmtContext ctx) { public ConditionalBlock visitConditionalBlock(ScriptLanguageParser.ConditionalBlockContext ctx) {
TheOnlyStatement f = new TheOnlyStatement(); ConditionalBlock cb = cbFactory.apply(ctx.kind.getText());
f.setRuleContext(ctx); cb.setRuleContext(ctx);
Statements body = (Statements) ctx.stmtList().accept(this); Statements body = (Statements) ctx.stmtList().accept(this);
f.setBody(body); cb.setBody(body);
body.setParent(f); body.setParent(cb);
return f; return cb;
} }
@Override @Override
public Object visitScriptCommand(ScriptLanguageParser.ScriptCommandContext ctx) { public Object visitScriptCommand(ScriptLanguageParser.ScriptCommandContext ctx) {
CallStatement scs = new CallStatement(); CallStatement scs = new CallStatement();
......
package edu.kit.iti.formal.psdbg.parser; package edu.kit.iti.formal.psdbg.parser;
/*- /*-
* #%L * #%L
* ProofScriptParser * ProofScriptParser
* %% * %%
* Copyright (C) 2017 Application-oriented Formal Verification * Copyright (C) 2017 Application-oriented Formal Verification
* %% * %%
* This program is free software: you can redistribute it and/or modify * This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as * it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the * published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version. * License, or (at your option) any later version.
* *
* This program is distributed in the hope that it will be useful, * This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of * but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details. * GNU General Public License for more details.
* *
* You should have received a copy of the GNU General Public * You should have received a copy of the GNU General Public
* License along with this program. If not, see * License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>. * <http://www.gnu.org/licenses/gpl-3.0.html>.
* #L% * #L%
*/ */
import edu.kit.iti.formal.psdbg.parser.ast.*; import edu.kit.iti.formal.psdbg.parser.ast.*;
...@@ -81,4 +81,13 @@ public interface Visitor<T> { ...@@ -81,4 +81,13 @@ public interface Visitor<T> {
T visit(ClosesCase closesCase); T visit(ClosesCase closesCase);
T visit(FunctionCall func); T visit(FunctionCall func);
T visit(WhileStatement ws);
T visit(IfStatement is);
T visit(StrictBlock strictBlock);
T visit(RelaxBlock relaxBlock);
} }
package edu.kit.iti.formal.psdbg.parser.ast;
/*-
* #%L
* ProofScriptParser
* %%
* Copyright (C) 2017 Application-oriented Formal Verification
* %%
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
* #L%
*/
import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
import lombok.*;
import org.antlr.v4.runtime.ParserRuleContext;
/**
* @author Alexander Weigl
* @version 1 (29.04.17)
*/
@Getter
@Setter
@AllArgsConstructor
@NoArgsConstructor
public abstract class ConditionalBlock
extends Statement<ScriptLanguageParser.ConditionalBlockContext> {
@Getter
@Setter
@NonNull protected Statements body = new Statements();
@Getter
@Setter
@NonNull protected Expression condition = BooleanLiteral.TRUE;
@Override
public boolean eq(ASTNode o) {
if (this == o) return true;
if (o == null || getClass() != o.getClass()) return false;
if (!super.equals(o)) return false;
ConditionalBlock that = (ConditionalBlock) o;
return getBody() != null ? getBody().eq(that.getBody()) : that.getBody() == null;
}
}
...@@ -34,7 +34,7 @@ import lombok.Setter; ...@@ -34,7 +34,7 @@ import lombok.Setter;
*/ */
@Getter @Getter
@Setter @Setter
public class ForeachStatement extends GoalSelector<ScriptLanguageParser.ForEachStmtContext> { public class ForeachStatement extends UnconditionalBlock {
public ForeachStatement() { public ForeachStatement() {
} }
......
package edu.kit.iti.formal.psdbg.parser.ast;
/*-
* #%L
* ProofScriptParser
* %%
* Copyright (C) 2017 Application-oriented Formal Verification
* %%
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
* #L%
*/
import lombok.*;
import org.antlr.v4.runtime.ParserRuleContext;
/**
* @author Alexander Weigl
* @version 1 (29.04.17)
*/
@Getter
@Setter
@AllArgsConstructor
@NoArgsConstructor
public abstract class GoalSelector<T extends ParserRuleContext>
extends Statement<T> {
@Getter
@Setter
@NonNull private Statements body = new Statements();
@Override
public boolean eq(ASTNode o) {
if (this == o) return true;
if (o == null || getClass() != o.getClass()) return false;
if (!super.equals(o)) return false;
GoalSelector<?> that = (GoalSelector<?>) o;
return getBody() != null ? getBody().eq(that.getBody()) : that.getBody() == null;
}
}
package edu.kit.iti.formal.psdbg.parser.ast;
import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
import edu.kit.iti.formal.psdbg.parser.Visitor;
public class IfStatement extends ConditionalBlock {
@Override
public <T> T accept(Visitor<T> visitor) {
return visitor.visit(this);
}
@Override
public Statement<ScriptLanguageParser.ConditionalBlockContext> copy() {
IfStatement is = new IfStatement();
is.ruleContext = ruleContext;
is.body = body.copy();
is.condition = condition.copy();
return is;
}
}