1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
/*
* SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
*
* SPDX-License-Identifier: EPL-2.0
*/
package tools.refinery.language.web.semantics.metadata;
import com.google.inject.Inject;
import tools.refinery.language.ide.syntaxcoloring.TypeHashProvider;
import tools.refinery.language.semantics.NodeNameProvider;
import tools.refinery.language.semantics.ProblemTrace;
import tools.refinery.store.model.Interpretation;
import tools.refinery.store.model.Model;
import tools.refinery.store.reasoning.ReasoningAdapter;
import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
import tools.refinery.store.reasoning.literal.Concreteness;
import tools.refinery.store.reasoning.representation.PartialRelation;
import tools.refinery.store.reasoning.translator.typehierarchy.InferredType;
import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator;
import tools.refinery.store.representation.TruthValue;
import tools.refinery.store.tuple.Tuple;
public class NodeMetadataFactory {
@Inject
private NodeNameProvider nodeNameProvider;
@Inject
private TypeHashProvider typeHashProvider;
private ProblemTrace problemTrace;
private Concreteness concreteness;
private Interpretation<InferredType> typeInterpretation;
private PartialInterpretation<TruthValue, Boolean> existsInterpretation;
public void initialize(ProblemTrace problemTrace, Concreteness concreteness, Model model) {
this.problemTrace = problemTrace;
this.concreteness = concreteness;
typeInterpretation = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL);
existsInterpretation = model.getAdapter(ReasoningAdapter.class).getPartialInterpretation(concreteness,
ReasoningAdapter.EXISTS_SYMBOL);
nodeNameProvider.setProblem(problemTrace.getProblem());
}
public NodeMetadata doCreateMetadata(int nodeId, String name, String simpleName, NodeKind kind) {
var type = getType(nodeId);
return doCreateMetadata(name, simpleName, type, kind);
}
public NodeMetadata createFreshlyNamedMetadata(int nodeId) {
var type = getType(nodeId);
var name = getName(type, nodeId);
return doCreateMetadata(name, name, type, NodeKind.IMPLICIT);
}
private PartialRelation getType(int nodeId) {
var inferredType = typeInterpretation.get(Tuple.of(nodeId));
if (inferredType == null) {
return null;
}
return inferredType.candidateType();
}
private String getName(PartialRelation type, int nodeId) {
if (concreteness == Concreteness.CANDIDATE && !existsInterpretation.get(Tuple.of(nodeId)).may()) {
// Do not increment the node name counter for non-existent nodes in the candidate interpretation.
// While non-existent nodes may appear in the partial interpretation, they are never displayed in the
// candidate interpretation.
return "::" + nodeId;
}
if (type == null) {
return nodeNameProvider.getNextName(null);
}
var relation = problemTrace.getRelation(type);
return nodeNameProvider.getNextName(relation.getName());
}
private NodeMetadata doCreateMetadata(String name, String simpleName, PartialRelation type, NodeKind kind) {
var typeHash = getTypeHash(type);
return new NodeMetadata(name, simpleName, typeHash, kind);
}
private String getTypeHash(PartialRelation type) {
if (type == null) {
return null;
}
var relation = problemTrace.getRelation(type);
return typeHashProvider.getTypeHash(relation);
}
}
|
