From 8c9f2ab67c70b3b7d65ec5090ccbc492e7c9cd63 Mon Sep 17 00:00:00 2001
From: Arne Keller <arne.keller@student.kit.edu>
Date: Tue, 20 Jul 2021 15:02:29 +0200
Subject: [PATCH] Instantiate abs step

see #18
---
 .../edu/kit/typicalc/model/step/StepAnnotator.java | 14 ++++++++++++--
 .../latexcreator/LatexCreatorConstants.java        |  3 ++-
 .../latexcreator/LatexCreatorType.java             |  4 ++--
 3 files changed, 16 insertions(+), 5 deletions(-)

diff --git a/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java b/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java
index a522ec5..6113352 100644
--- a/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java
+++ b/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java
@@ -1,7 +1,10 @@
 package edu.kit.typicalc.model.step;
 
+import edu.kit.typicalc.model.type.FunctionType;
+import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstants;
 import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorConstraints;
 import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorMode;
+import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorType;
 
 import java.util.ArrayList;
 import java.util.List;
@@ -15,8 +18,15 @@ public class StepAnnotator implements StepVisitor {
 
     @Override
     public void visit(AbsStepDefault absD) {
-        annotations.add("$"
-                + LatexCreatorConstraints.createSingleConstraint(absD.getConstraint(), LatexCreatorMode.NORMAL) + "$");
+        var t1 = ((FunctionType) absD.getConstraint().getSecondType()).getParameter();
+        var t2 = ((FunctionType) absD.getConstraint().getSecondType()).getOutput();
+        annotations.add("$$\\begin{align}"
+                + "&" + LatexCreatorConstants.RULE_VARIABLE + "_1 := "
+                + new LatexCreatorType(t1, LatexCreatorMode.NORMAL).getLatex() + LatexCreatorConstants.LATEX_NEW_LINE + "\n"
+                + "&" + LatexCreatorConstants.RULE_VARIABLE + "_2 := "
+                + new LatexCreatorType(t2, LatexCreatorMode.NORMAL).getLatex() + LatexCreatorConstants.LATEX_NEW_LINE + "\n"
+                + "&" + LatexCreatorConstraints.createSingleConstraint(absD.getConstraint(), LatexCreatorMode.NORMAL)
+                + "\\end{align}$$");
         absD.getPremise().accept(this);
     }
 
diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java
index dd1bfbf..9d16f40 100644
--- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java
+++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorConstants.java
@@ -55,10 +55,11 @@ public final class LatexCreatorConstants {
     protected static final String TREE_VARIABLE = "\\alpha";
     protected static final String GENERATED_ASSUMPTION_VARIABLE = "\\beta";
     protected static final String USER_VARIABLE = "\\tau";
+    public static final String RULE_VARIABLE = "\\tau";
     protected static final String SIGMA = "\\sigma";
     protected static final String GAMMA = "\\Gamma";
 
-    protected static final String LATEX_NEW_LINE = "\\\\";
+    public static final String LATEX_NEW_LINE = "\\\\";
     protected static final String CIRC = "\\circ";
     protected static final String COLOR_RED = "\\color{Red}";
     protected static final String COLOR_HIGHLIGHTED = "\\color{RoyalBlue}";
diff --git a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorType.java b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorType.java
index 46ce3f9..26b53e3 100644
--- a/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorType.java
+++ b/src/main/java/edu/kit/typicalc/view/content/typeinferencecontent/latexcreator/LatexCreatorType.java
@@ -27,7 +27,7 @@ public class LatexCreatorType implements TypeVisitor {
      *
      * @param type the type
      */
-    protected LatexCreatorType(Type type, LatexCreatorMode mode) {
+    public LatexCreatorType(Type type, LatexCreatorMode mode) {
         this.type = type;
         this.mode = mode;
         type.accept(this);
@@ -36,7 +36,7 @@ public class LatexCreatorType implements TypeVisitor {
     /**
      * @return the generated LaTeX code
      */
-    protected String getLatex() {
+    public String getLatex() {
         return latex.toString();
     }