de.uka.ilkd.key.macros.scripts.meta

Class ValueInjector

java.lang.Object

de.uka.ilkd.key.macros.scripts.meta.ValueInjector

public class ValueInjector
extends java.lang.Object

Version:

1 (29.03.17)

Author:

Alexander Weigl

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Map<java.lang.Class,StringConverter>	converters A mapping between desired types and suitable @StringConverter.
private static ValueInjector	instance A default instance

Constructor Summary

Constructors

Constructor and Description
ValueInjector()

Method Summary

Modifier and Type	Method and Description
<T> void	addConverter(java.lang.Class<T> clazz, StringConverter<T> conv) Registers the given converter for the specified class.
private java.lang.Object	convert(ProofScriptArgument<?> meta, java.lang.String val)
static ValueInjector	createDefault() Returns a fresh instance of a ValueInjector with the support for basic primitive data types.
<T> StringConverter<T>	getConverter(java.lang.Class<T> clazz) Finds a converter for the given class.
static ValueInjector	getInstance() Returns the default instance of a ValueInjector Use with care.
private java.util.Map<java.lang.String,java.lang.Object>	getStringMap(java.lang.Object obj, ProofScriptArgument<?> vararg)
<T> T	inject(ProofScriptCommand<?> command, T obj, java.util.Map<java.lang.String,java.lang.String> arguments) Injects the converted version of the given arguments in the given obj.
private void	injectIntoField(ProofScriptArgument<?> meta, java.util.Map<java.lang.String,java.lang.String> args, java.lang.Object obj)
static <T> T	injection(ProofScriptCommand<?> command, T obj, java.util.Map<java.lang.String,java.lang.String> arguments) Injects the given arguments in the obj.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

instance

private static ValueInjector instance

A default instance

See Also:

getInstance()

converters

private java.util.Map<java.lang.Class,StringConverter> converters

A mapping between desired types and suitable @StringConverter.

Should be

T --> StringConverter

Constructor Detail

ValueInjector

public ValueInjector()

Method Detail

injection

public static <T> T injection(ProofScriptCommand<?> command,
                              T obj,
                              java.util.Map<java.lang.String,java.lang.String> arguments)
                       throws ArgumentRequiredException,
                              InjectionReflectionException,
                              NoSpecifiedConverterException,
                              ConversionException

Injects the given arguments in the obj. For more details see inject(ProofScriptCommand, Object, Map)

Type Parameters:

T - an arbitrary type

Parameters:

command - a proof script command

obj - a parameter class with annotation

arguments - a non-null map of string pairs

Returns:

the same object as obj

Throws:

ArgumentRequiredException - a required argument was not given in arguments

InjectionReflectionException - an access on some reflection methods occurred

NoSpecifiedConverterException - unknown type for the current converter map

ConversionException - an converter could not translate the given value in

getInstance

public static ValueInjector getInstance()

Returns the default instance of a ValueInjector Use with care. No multi-threading.

Returns:

a static reference to the default converter.

See Also:

createDefault()

createDefault

public static ValueInjector createDefault()

Returns a fresh instance of a ValueInjector with the support for basic primitive data types.

Returns:

a fresh instance

inject

public <T> T inject(ProofScriptCommand<?> command,
                    T obj,
                    java.util.Map<java.lang.String,java.lang.String> arguments)
             throws ConversionException,
                    InjectionReflectionException,
                    NoSpecifiedConverterException,
                    ArgumentRequiredException

Injects the converted version of the given arguments in the given obj.

Type Parameters:

T - type safety

Parameters:

command - a proof script command

obj - a non-null instance of a parameter class (with annotation)

arguments - a non-null string map

Returns:

the same object as obj

Throws:

ArgumentRequiredException - a required argument was not given in arguments

InjectionReflectionException - an access on some reflection methods occurred

NoSpecifiedConverterException - unknown type for the current converter map

ConversionException - an converter could not translate the given value in

See Also:

Option, Flag

getStringMap

private java.util.Map<java.lang.String,java.lang.Object> getStringMap(java.lang.Object obj,
                                                                      ProofScriptArgument<?> vararg)
                                                               throws InjectionReflectionException

Throws:

InjectionReflectionException

injectIntoField

private void injectIntoField(ProofScriptArgument<?> meta,
                             java.util.Map<java.lang.String,java.lang.String> args,
                             java.lang.Object obj)
                      throws InjectionReflectionException,
                             ArgumentRequiredException,
                             ConversionException,
                             NoSpecifiedConverterException

Throws:

InjectionReflectionException

ArgumentRequiredException

ConversionException

NoSpecifiedConverterException

convert

private java.lang.Object convert(ProofScriptArgument<?> meta,
                                 java.lang.String val)
                          throws NoSpecifiedConverterException,
                                 ConversionException

Throws:

NoSpecifiedConverterException

ConversionException

addConverter

public <T> void addConverter(java.lang.Class<T> clazz,
                             StringConverter<T> conv)

Registers the given converter for the specified class.

Type Parameters:

T - an arbitrary type

Parameters:

clazz - a class

conv - a converter for the given class

getConverter

public <T> StringConverter<T> getConverter(java.lang.Class<T> clazz)

Finds a converter for the given class.

Type Parameters:

T - an arbitrary type

Parameters:

clazz - a non-null class

Returns:

null or a suitable converter (registered) converter for the requested class.