From 35bb54da8ef435b90459e76bf6708e83ee4dd0c2 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Mon, 4 Nov 2024 15:02:27 +0000 Subject: [PATCH] Add POLaunchFactory for creating launches --- .../quickcheck/commands/QCRunCommand.java | 2 +- .../quickcheck/commands/QCRunLSPCommand.java | 2 +- .../com/fujitsu/vdmj/pog/POLaunchFactory.java | 285 ++++++++++++++++++ .../com/fujitsu/vdmj/pog/ProofObligation.java | 178 +---------- 4 files changed, 295 insertions(+), 172 deletions(-) create mode 100644 vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java diff --git a/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java b/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java index 4a342934b..45a170354 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java +++ b/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java @@ -116,7 +116,7 @@ else if (obligation.witness != null) } else if (obligation.kind.isStandAlone()) { - launch = obligation.getLaunch(null); + launch = obligation.getLaunch(); } else { diff --git a/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java b/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java index 37716ec4f..0e0d9f2f7 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java +++ b/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java @@ -119,7 +119,7 @@ else if (obligation.witness != null) } else if (obligation.kind.isStandAlone()) { - launch = obligation.getLaunch(null); + launch = obligation.getLaunch(); } else { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java new file mode 100644 index 000000000..1ba0245e5 --- /dev/null +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java @@ -0,0 +1,285 @@ +/******************************************************************************* + * + * Copyright (c) 2024 Nick Battle. + * + * Author: Nick Battle + * + * This file is part of VDMJ. + * + * VDMJ 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. + * + * VDMJ 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 VDMJ. If not, see . + * SPDX-License-Identifier: GPL-3.0-or-later + * + ******************************************************************************/ +package com.fujitsu.vdmj.pog; + +import java.util.List; +import java.util.Vector; + +import com.fujitsu.vdmj.po.definitions.POExplicitFunctionDefinition; +import com.fujitsu.vdmj.po.definitions.POExplicitOperationDefinition; +import com.fujitsu.vdmj.po.definitions.POImplicitFunctionDefinition; +import com.fujitsu.vdmj.po.definitions.POImplicitOperationDefinition; +import com.fujitsu.vdmj.po.patterns.POPattern; +import com.fujitsu.vdmj.po.patterns.POPatternList; +import com.fujitsu.vdmj.po.patterns.POPatternListList; +import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingConstantVisitor; +import com.fujitsu.vdmj.po.patterns.visitors.PORemoveIgnoresVisitor; +import com.fujitsu.vdmj.po.types.POPatternListTypePair; +import com.fujitsu.vdmj.po.types.POPatternListTypePairList; +import com.fujitsu.vdmj.runtime.Context; +import com.fujitsu.vdmj.runtime.Interpreter; +import com.fujitsu.vdmj.tc.lex.TCNameToken; +import com.fujitsu.vdmj.tc.types.TCFunctionType; +import com.fujitsu.vdmj.tc.types.TCParameterType; +import com.fujitsu.vdmj.tc.types.TCType; +import com.fujitsu.vdmj.tc.types.TCTypeList; +import com.fujitsu.vdmj.values.ParameterValue; + +/** + * A class to help with the construction of launch invocations for POs. + */ +public class POLaunchFactory +{ + private static class ApplyCall + { + public String applyName = null; + public List applyTypes = new Vector(); + public List applyArgs = new Vector(); + } + + private static class ApplyArg + { + public String name; + public String type; + public String value; + + public ApplyArg(String name, String type, String value) + { + this.name = name; + this.type = type; + this.value = value; + } + } + + private final ProofObligation po; + private ApplyCall applyCall = null; + + public POLaunchFactory(ProofObligation po) + { + this.po = po; + init(); + } + + private void init() + { + applyCall = null; // Also used on exceptions + } + + /** + * Generate a string invocation or ApplyCall for the PO context. + */ + public String getCexLaunch() + { + if (po.counterexample == null) + { + return getLaunch(Interpreter.getInstance().getInitialContext()); + } + + return getLaunch(po.counterexample); + } + + public String getWitnessLaunch() + { + if (po.witness == null) + { + return getLaunch(Interpreter.getInstance().getInitialContext()); + } + + return getLaunch(po.witness); + } + + public ApplyCall getCexApply() + { + getCexLaunch(); + return applyCall; + } + + public ApplyCall getWitnessApply() + { + getWitnessLaunch(); + return applyCall; + } + + public String getLaunch(Context ctxt) + { + try + { + applyCall = new ApplyCall(); + + if (po.definition instanceof POExplicitFunctionDefinition) + { + POExplicitFunctionDefinition efd = (POExplicitFunctionDefinition)po.definition; + return + launchNameTypes(efd.name, efd.typeParams, ctxt) + + launchArguments(efd.paramPatternList, efd.type, ctxt); + } + else if (po.definition instanceof POImplicitFunctionDefinition) + { + POImplicitFunctionDefinition ifd = (POImplicitFunctionDefinition)po.definition; + return + launchNameTypes(ifd.name, ifd.typeParams, ctxt) + + launchArguments(ifd.parameterPatterns, ctxt); + } + else if (po.definition instanceof POExplicitOperationDefinition) + { + POExplicitOperationDefinition eop = (POExplicitOperationDefinition)po.definition; + return + launchNameTypes(eop.name, null, ctxt) + + launchArguments(eop.parameterPatterns, eop.type.parameters, ctxt); + } + else if (po.definition instanceof POImplicitOperationDefinition) + { + POImplicitOperationDefinition iop = (POImplicitOperationDefinition)po.definition; + return + launchNameTypes(iop.name, null, ctxt) + + launchArguments(iop.parameterPatterns, ctxt); + } + else if (po.kind.isStandAlone()) + { + // PO is a stand alone expression, so just execute that + return po.source.trim(); + } + } + catch (Exception e) + { + // Cannot match all parameters from context + init(); + } + + return null; + } + + private String launchNameTypes(TCNameToken name, TCTypeList typeParams, Context ctxt) throws Exception + { + StringBuilder callString = new StringBuilder(name.getName()); + PORemoveIgnoresVisitor.init(); + applyCall.applyName = name.getName(); + + if (typeParams != null) + { + String inst = addTypeParams(typeParams, ctxt); + callString.append(inst); + } + + return callString.toString(); + } + + private String launchArguments(POPatternListList paramPatternList, TCFunctionType type, Context ctxt) throws Exception + { + StringBuilder callString = new StringBuilder(); + TCType _type = type; + + for (POPatternList pl: paramPatternList) + { + TCFunctionType ftype = (TCFunctionType)_type; + callString.append(launchArguments(pl, ftype.parameters, ctxt)); + _type = ftype.result; + } + + return callString.toString(); + } + + private String launchArguments(POPatternList paramPatternList, TCTypeList types, Context ctxt) throws Exception + { + StringBuilder callString = new StringBuilder(); + callString.append("("); + String sep = ""; + int i = 0; + + for (POPattern p: paramPatternList) + { + String match = paramMatch(p.removeIgnorePatterns(), types.get(i++), ctxt); + callString.append(sep); + callString.append(match); + sep = ", "; + } + + callString.append(")"); + return callString.toString(); + } + + private String launchArguments(POPatternListTypePairList parameterPatterns, Context ctxt) throws Exception + { + StringBuilder callString = new StringBuilder(); + String sep = ""; + callString.append("("); + + for (POPatternListTypePair pl: parameterPatterns) + { + for (POPattern p: pl.patterns) + { + String match = paramMatch(p.removeIgnorePatterns(), pl.type, ctxt); + callString.append(sep); + callString.append(match); + sep = ", "; + } + } + + callString.append(")"); + + return callString.toString(); + } + + private String addTypeParams(TCTypeList params, Context ctxt) throws Exception + { + StringBuilder callString = new StringBuilder(); + String sep = ""; + callString.append("["); + + for (TCType p: params) + { + TCParameterType param = (TCParameterType)p; + ParameterValue inst = (ParameterValue) ctxt.get(param.name); + + if (inst == null) + { + throw new Exception("Can't match type param " + param); + } + + callString.append(sep); + callString.append(inst.type); + applyCall.applyTypes.add(inst.type.toString()); + sep = ", "; + } + + callString.append("]"); + return callString.toString(); + } + + private String paramMatch(POPattern p, TCType type, Context ctxt) throws Exception + { + POGetMatchingConstantVisitor visitor = new POGetMatchingConstantVisitor(); + String result = p.apply(visitor, ctxt); + + if (visitor.hasFailed()) + { + throw new Exception("Can't match param " + p); + } + else + { + applyCall.applyArgs.add(new ApplyArg(p.toString(), type.toString(), result)); + return result; + } + } +} diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java index 3f41e9c0c..273ff1cfc 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -27,27 +27,12 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.annotations.POAnnotationList; import com.fujitsu.vdmj.po.definitions.PODefinition; -import com.fujitsu.vdmj.po.definitions.POExplicitFunctionDefinition; -import com.fujitsu.vdmj.po.definitions.POExplicitOperationDefinition; -import com.fujitsu.vdmj.po.definitions.POImplicitFunctionDefinition; -import com.fujitsu.vdmj.po.definitions.POImplicitOperationDefinition; -import com.fujitsu.vdmj.po.patterns.POPattern; -import com.fujitsu.vdmj.po.patterns.POPatternList; -import com.fujitsu.vdmj.po.patterns.POPatternListList; -import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingConstantVisitor; import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingExpressionVisitor; -import com.fujitsu.vdmj.po.patterns.visitors.PORemoveIgnoresVisitor; -import com.fujitsu.vdmj.po.types.POPatternListTypePair; -import com.fujitsu.vdmj.po.types.POPatternListTypePairList; import com.fujitsu.vdmj.runtime.Context; -import com.fujitsu.vdmj.runtime.Interpreter; import com.fujitsu.vdmj.tc.expressions.TCExistsExpression; import com.fujitsu.vdmj.tc.expressions.TCExpression; -import com.fujitsu.vdmj.tc.lex.TCNameToken; -import com.fujitsu.vdmj.tc.types.TCParameterType; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeList; -import com.fujitsu.vdmj.values.ParameterValue; abstract public class ProofObligation implements Comparable { @@ -248,171 +233,24 @@ protected String explicitType(TCType type, LexLocation poLoc) } /** - * Generate a string invocation for the context passed. + * Generate a string invocation for the PO context. */ public String getCexLaunch() { - if (counterexample == null) - { - return getLaunch(Interpreter.getInstance().getInitialContext()); - } - - return getLaunch(counterexample); + POLaunchFactory factory = new POLaunchFactory(this); + return factory.getCexLaunch(); } public String getWitnessLaunch() { - if (witness == null) - { - return getLaunch(Interpreter.getInstance().getInitialContext()); - } - - return getLaunch(witness); - } - - public String getLaunch(Context ctxt) - { - try - { - if (definition instanceof POExplicitFunctionDefinition) - { - POExplicitFunctionDefinition efd = (POExplicitFunctionDefinition)definition; - return - launchNameTypes(efd.name, efd.typeParams, ctxt) + - launchArguments(efd.paramPatternList, ctxt); - } - else if (definition instanceof POImplicitFunctionDefinition) - { - POImplicitFunctionDefinition ifd = (POImplicitFunctionDefinition)definition; - return - launchNameTypes(ifd.name, ifd.typeParams, ctxt) + - launchArguments(ifd.parameterPatterns, ctxt); - } - else if (definition instanceof POExplicitOperationDefinition) - { - POExplicitOperationDefinition eop = (POExplicitOperationDefinition)definition; - return - launchNameTypes(eop.name, null, ctxt) + - launchArguments(eop.getParamPatternList(), ctxt); - } - else if (definition instanceof POImplicitOperationDefinition) - { - POImplicitOperationDefinition iop = (POImplicitOperationDefinition)definition; - return - launchNameTypes(iop.name, null, ctxt) + - launchArguments(iop.parameterPatterns, ctxt); - } - else if (kind.isStandAlone()) - { - // PO is a stand alone expression, so just execute that - return source.trim(); - } - } - catch (Exception e) - { - // Cannot match all parameters from context - } - - return null; - } - - private String launchNameTypes(TCNameToken name, TCTypeList typeParams, Context ctxt) throws Exception - { - StringBuilder callString = new StringBuilder(name.getName()); - PORemoveIgnoresVisitor.init(); - - if (typeParams != null) - { - String inst = addTypeParams(typeParams, ctxt); - callString.append(inst); - } - - return callString.toString(); - } - - private String launchArguments(POPatternListList paramPatternList, Context ctxt) throws Exception - { - StringBuilder callString = new StringBuilder(); - - for (POPatternList pl: paramPatternList) - { - String sep = ""; - callString.append("("); - - for (POPattern p: pl) - { - String match = paramMatch(p.removeIgnorePatterns(), ctxt); - callString.append(sep); - callString.append(match); - sep = ", "; - } - - callString.append(")"); - } - - return callString.toString(); + POLaunchFactory factory = new POLaunchFactory(this); + return factory.getWitnessLaunch(); } - private String launchArguments(POPatternListTypePairList parameterPatterns, Context ctxt) throws Exception - { - StringBuilder callString = new StringBuilder(); - String sep = ""; - callString.append("("); - - for (POPatternListTypePair pl: parameterPatterns) - { - for (POPattern p: pl.patterns) - { - String match = paramMatch(p.removeIgnorePatterns(), ctxt); - callString.append(sep); - callString.append(match); - sep = ", "; - } - } - - callString.append(")"); - - return callString.toString(); - } - - private String addTypeParams(TCTypeList params, Context ctxt) throws Exception + public String getLaunch() { - StringBuilder callString = new StringBuilder(); - String sep = ""; - callString.append("["); - - for (TCType p: params) - { - TCParameterType param = (TCParameterType)p; - ParameterValue inst = (ParameterValue) ctxt.get(param.name); - - if (inst == null) - { - throw new Exception("Can't match type param " + param); - } - - callString.append(sep); - callString.append(inst.type); - sep = ", "; - } - - callString.append("]"); - return callString.toString(); - } - - private String paramMatch(POPattern p, Context ctxt) throws Exception - { - POGetMatchingConstantVisitor visitor = new POGetMatchingConstantVisitor(); - String result = p.apply(visitor, ctxt); - - if (visitor.hasFailed()) - { - throw new Exception("Can't match param " + p); - } - else - { - return result; - } + POLaunchFactory factory = new POLaunchFactory(this); + return factory.getLaunch(null); } /**