Skip to content

Commit

Permalink
Merge branch 'master' into highprecision
Browse files Browse the repository at this point in the history
  • Loading branch information
@nickbattle
nickbattle committed Nov 26, 2023
2 parents c4c6122 + 5dc8d6e commit c170d0f
Show file tree
Hide file tree
Showing 18 changed files with 372 additions and 401 deletions.
38 changes: 16 additions & 22 deletions vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitFunctionDefinition.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -122,35 +122,34 @@ public NameValuePairList getNamedValues(Context ctxt)
{
NameValuePairList nvl = new NameValuePairList();

FunctionValue prefunc =
(predef == null) ? null : new FunctionValue(predef, null, null, null);

FunctionValue postfunc =
(postdef == null) ? null : new FunctionValue(postdef, null, null, null);

FunctionValue func = new FunctionValue(this, prefunc, postfunc, null);
func.isStatic = accessSpecifier.isStatic;;
func.uninstantiated = (typeParams != null);
nvl.add(new NameValuePair(name, func));
FunctionValue prefunc = null;
FunctionValue postfunc = null;
FunctionValue measurefunc = null;

if (predef != null)
{
nvl.add(new NameValuePair(predef.name, prefunc));
prefunc.uninstantiated = (typeParams != null);
NameValuePairList names = predef.getNamedValues(ctxt);
prefunc = names.getNamedValue(predef.name);
nvl.addAll(names);
}

if (postdef != null)
{
nvl.add(new NameValuePair(postdef.name, postfunc));
postfunc.uninstantiated = (typeParams != null);
NameValuePairList names = postdef.getNamedValues(ctxt);
postfunc = names.getNamedValue(postdef.name);
nvl.addAll(names);
}

if (measureDef != null && measureDef.name.isMeasureName())
{
// Add implicit measure_* functions and any pre_measure_*s too.
nvl.addAll(measureDef.getNamedValues(ctxt));
NameValuePairList names = measureDef.getNamedValues(ctxt);
measurefunc = names.getNamedValue(measureDef.name);
nvl.addAll(names);
}

FunctionValue func = new FunctionValue(this, prefunc, postfunc, measurefunc, null);
nvl.add(new NameValuePair(name, func));

return nvl;
}

Expand Down Expand Up @@ -195,13 +194,8 @@ public FunctionValue getPolymorphicValue(TCTypeList argTypes, Context params, Co
}

TCFunctionType ftype = (TCFunctionType)INInstantiate.instantiate(getType(), params, ctxt);
FunctionValue rv = new FunctionValue(this, ftype, params, prefv, postfv, null);
FunctionValue rv = new FunctionValue(this, ftype, params, prefv, postfv, measurefv, null);

if (measurefv != null)
{
rv.setMeasure(measurefv);
}

polyfuncs.put(argTypes, rv);
return rv;
}
Expand Down
8 changes: 2 additions & 6 deletions vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitOperationDefinition.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -102,25 +102,21 @@ public NameValuePairList getNamedValues(Context ctxt)
NameValuePairList nvl = new NameValuePairList();

FunctionValue prefunc =
(predef == null) ? null : new FunctionValue(predef, null, null, null);
(predef == null) ? null : new FunctionValue(predef, null, null, null, null);

FunctionValue postfunc =
(postdef == null) ? null : new FunctionValue(postdef, null, null, null);
(postdef == null) ? null : new FunctionValue(postdef, null, null, null, null);

OperationValue op = new OperationValue(this, prefunc, postfunc, statedef);
op.isConstructor = isConstructor;
op.isStatic = accessSpecifier.isStatic;
nvl.add(new NameValuePair(name, op));

if (predef != null)
{
prefunc.isStatic = accessSpecifier.isStatic;
nvl.add(new NameValuePair(predef.name, prefunc));
}

if (postdef != null)
{
postfunc.isStatic = accessSpecifier.isStatic;
nvl.add(new NameValuePair(postdef.name, postfunc));
}

Expand Down
44 changes: 17 additions & 27 deletions vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitFunctionDefinition.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -130,39 +130,34 @@ public NameValuePairList getNamedValues(Context ctxt)
{
NameValuePairList nvl = new NameValuePairList();

FunctionValue prefunc =
(predef == null) ? null : new FunctionValue(predef, null, null, null);

FunctionValue postfunc =
(postdef == null) ? null : new FunctionValue(postdef, null, null, null);

// Note, body may be null if it is really implicit. This is caught
// when the function is invoked. The value is needed to implement
// the pre_() expression for implicit functions.

FunctionValue func = new FunctionValue(this, prefunc, postfunc, null);
func.isStatic = accessSpecifier.isStatic;
func.uninstantiated = (typeParams != null);
nvl.add(new NameValuePair(name, func));
FunctionValue prefunc = null;
FunctionValue postfunc = null;
FunctionValue measurefunc = null;

if (predef != null)
{
nvl.add(new NameValuePair(predef.name, prefunc));
prefunc.uninstantiated = (typeParams != null);
NameValuePairList names = predef.getNamedValues(ctxt);
prefunc = names.getNamedValue(predef.name);
nvl.addAll(names);
}

if (postdef != null)
{
nvl.add(new NameValuePair(postdef.name, postfunc));
postfunc.uninstantiated = (typeParams != null);
NameValuePairList names = postdef.getNamedValues(ctxt);
postfunc = names.getNamedValue(postdef.name);
nvl.addAll(names);
}

if (measureDef != null && measureDef.name.isMeasureName())
{
// Add implicit measure_* functions and any pre_measure_*s too.
nvl.addAll(measureDef.getNamedValues(ctxt));
NameValuePairList names = measureDef.getNamedValues(ctxt);
measurefunc = names.getNamedValue(measureDef.name);
nvl.addAll(names);
}

FunctionValue func = new FunctionValue(this, prefunc, postfunc, measurefunc, null);
nvl.add(new NameValuePair(name, func));

return nvl;
}

Expand Down Expand Up @@ -207,12 +202,7 @@ public FunctionValue getPolymorphicValue(TCTypeList actualTypes, Context params,
}

TCFunctionType ftype = (TCFunctionType)INInstantiate.instantiate(getType(), params, ctxt);
FunctionValue rv = new FunctionValue(this, ftype, params, prefv, postfv, null);

if (measurefv != null)
{
rv.setMeasure(measurefv);
}
FunctionValue rv = new FunctionValue(this, ftype, params, prefv, postfv, measurefv, null);

polyfuncs.put(actualTypes, rv);
return rv;
Expand Down
8 changes: 2 additions & 6 deletions vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitOperationDefinition.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -123,29 +123,25 @@ public NameValuePairList getNamedValues(Context ctxt)
NameValuePairList nvl = new NameValuePairList();

FunctionValue prefunc =
(predef == null) ? null : new FunctionValue(predef, null, null, null);
(predef == null) ? null : new FunctionValue(predef, null, null, null, null);

FunctionValue postfunc =
(postdef == null) ? null : new FunctionValue(postdef, null, null, null);
(postdef == null) ? null : new FunctionValue(postdef, null, null, null, null);

// Note, body may be null if it is really implicit. This is caught
// when the function is invoked. The value is needed to implement
// the pre_() expression for implicit functions.

OperationValue op = new OperationValue(this, prefunc, postfunc, statedef);
op.isConstructor = isConstructor;
op.isStatic = accessSpecifier.isStatic;
nvl.add(new NameValuePair(name, op));

if (predef != null)
{
prefunc.isStatic = accessSpecifier.isStatic;
nvl.add(new NameValuePair(predef.name, prefunc));
}

if (postdef != null)
{
postfunc.isStatic = accessSpecifier.isStatic;
nvl.add(new NameValuePair(postdef.name, postfunc));
}

Expand Down
4 changes: 2 additions & 2 deletions vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INStateDefinition.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -115,13 +115,13 @@ public void initState(StateContext initialContext)
{
if (invdef != null)
{
invfunc = new FunctionValue(invdef, null, null, initialContext);
invfunc = new FunctionValue(invdef, null, null, null, initialContext);
initialContext.put(name.getInvName(location), invfunc);
}

if (initdef != null)
{
initfunc = new FunctionValue(initdef, null, null, initialContext);
initfunc = new FunctionValue(initdef, null, null, null, initialContext);
initialContext.put(name.getInitName(location), initfunc);
}

Expand Down
10 changes: 5 additions & 5 deletions vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INTypeDefinition.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -90,31 +90,31 @@ public NameValuePairList getNamedValues(Context ctxt)

if (invdef != null)
{
FunctionValue invfunc = new FunctionValue(invdef, null, null, null);
FunctionValue invfunc = new FunctionValue(invdef, null, null, null, null);
nvl.add(new NameValuePair(invdef.name, invfunc));
}

if (eqdef != null)
{
FunctionValue eqfunc = new FunctionValue(eqdef, null, null, null);
FunctionValue eqfunc = new FunctionValue(eqdef, null, null, null, null);
nvl.add(new NameValuePair(eqdef.name, eqfunc));
}

if (orddef != null)
{
FunctionValue ordfunc = new FunctionValue(orddef, null, null, null);
FunctionValue ordfunc = new FunctionValue(orddef, null, null, null, null);
nvl.add(new NameValuePair(orddef.name, ordfunc));
}

if (mindef != null)
{
FunctionValue minfunc = new FunctionValue(mindef, null, null, null);
FunctionValue minfunc = new FunctionValue(mindef, null, null, null, null);
nvl.add(new NameValuePair(mindef.name, minfunc));
}

if (maxdef != null)
{
FunctionValue maxfunc = new FunctionValue(maxdef, null, null, null);
FunctionValue maxfunc = new FunctionValue(maxdef, null, null, null, null);
nvl.add(new NameValuePair(maxdef.name, maxfunc));
}

Expand Down
2 changes: 1 addition & 1 deletion vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INFuncInstantiationExpression.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -121,7 +121,7 @@ public Value eval(Context ctxt)
rv = impdef.getPolymorphicValue(argtypes, params, ctxt);
}

rv.setSelf(fv.self);
rv.setSelf(fv);
rv.uninstantiated = false;
return rv;
}
Expand Down
39 changes: 26 additions & 13 deletions vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,6 @@
import com.fujitsu.vdmj.pog.SubTypeObligation;
import com.fujitsu.vdmj.tc.definitions.TCDefinition;
import com.fujitsu.vdmj.tc.definitions.TCExplicitFunctionDefinition;
import com.fujitsu.vdmj.tc.lex.TCNameToken;
import com.fujitsu.vdmj.tc.types.TCMapType;
import com.fujitsu.vdmj.tc.types.TCType;
import com.fujitsu.vdmj.tc.types.TCTypeList;
Expand Down Expand Up @@ -103,17 +102,15 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
}
}

boolean polymorphic = type.isFunction(location) && type.getFunction().instantiated != null;

if (!type.isUnknown(location) && !polymorphic &&
if (!type.isUnknown(location) &&
(type.isFunction(location) || type.isOperation(location)))
{
TCTypeList paramTypes = type.isFunction(location) ?
type.getFunction().parameters : type.getOperation().parameters;

String prename = root.getPreName();

if (type.isFunction(location) && (prename == null || !prename.equals("")))
if (type.isFunction(location) && prename != null && !prename.equals(""))
{
boolean needed = true;

Expand Down Expand Up @@ -154,10 +151,14 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
}
}

if (!type.isUnknown(location) && type.isFunction(location) && !polymorphic)
if (!type.isUnknown(location) && type.isFunction(location))
{
if (recursive != null) // name is a function in a recursive loop
{
/**
* All of the functions in the loop will generate similar obligations,
* so the "add" method eliminates any duplicates.
*/
for (PODefinitionList loop: recursive)
{
obligations.add(new RecursiveObligation(location, loop, this, ctxt));
Expand All @@ -180,16 +181,16 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
return obligations;
}

public String getMeasureApply(TCNameToken measure)
public String getMeasureApply(String measure)
{
return getMeasureApply(measure, true);
}

/**
* Create a measure application string from this apply, turning the root function
* name into the measure name passed, and collapsing curried argument sets into one.
* name into the measure name passed.
*/
private String getMeasureApply(TCNameToken measure, boolean close)
private String getMeasureApply(String measure, boolean close)
{
String start = null;

Expand All @@ -200,19 +201,31 @@ private String getMeasureApply(TCNameToken measure, boolean close)
}
else if (root instanceof POVariableExpression)
{
start = measure.getName() + "(";
start = measure;
}
else if (root instanceof POFuncInstantiationExpression)
{
POFuncInstantiationExpression fie = (POFuncInstantiationExpression)root;
start = measure.getName() + "[" + Utils.listToString(fie.actualTypes) + "](";
start = measure + "[" + Utils.listToString(fie.actualTypes) + "]";
}
else
{
start = root.toString() + "(";
start = root.toString();
}

StringBuilder sb = new StringBuilder(start);
sb.append("(");
String separator = "";

return start + Utils.listToString(args) + (close ? ")" : ", ");
for (POExpression arg: args)
{
sb.append(separator);
sb.append(Utils.deBracketed(arg));
separator = ", ";
}

sb.append(")");
return sb.toString();
}

@Override
Expand Down
8 changes: 4 additions & 4 deletions vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POExpression.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -116,13 +116,13 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
* This is used during proof obligation generation. It is implemented in
* the VariableExpression class.
*
* null => expression is not a function.
* "" => expression is a function without a precondition.
* "pre_<name>" => expression is a function with a precondition.
* null => expression is not a function or operation.
* "" => expression is a fn/op without a precondition.
* "pre_<name>" => expression is a fn/op with a precondition.
*/
public String getPreName()
{
return null; // Not a function, by default
return null; // Not a fn/op, by default
}

/**
Expand Down
Loading

0 comments on commit c170d0f

Please sign in to comment.