Work for pi and sigma (#147)

JetBrains · Apr 6, 2020 · 7c74a28 · 7c74a28
1 parent 1b49d03
commit 7c74a28
Showing 1 changed file with 41 additions and 0 deletions.
diff --git a/base/src/main/java/org/arend/naming/resolving/visitor/ExpressionResolveNameVisitor.java b/base/src/main/java/org/arend/naming/resolving/visitor/ExpressionResolveNameVisitor.java
@@ -165,6 +165,10 @@ public Concrete.Expression visitLam(Concrete.LamExpression expr, Void params) {
 
   @Override
   public Concrete.Expression visitPi(Concrete.PiExpression expr, Void params) {
+    List<Concrete.Parameter> parameters = new ArrayList<>();
+    convertPiAppHoles(expr, parameters);
+    if (!parameters.isEmpty())
+      return new Concrete.LamExpression(expr.getData(), parameters, expr).accept(this, null);
     try (Utils.ContextSaver ignored = new Utils.ContextSaver(myContext)) {
       visitParameters(expr.getParameters(), null);
       expr.codomain = expr.codomain.accept(this, null);
@@ -174,6 +178,10 @@ public Concrete.Expression visitPi(Concrete.PiExpression expr, Void params) {
 
   @Override
   public Concrete.Expression visitSigma(Concrete.SigmaExpression expr, Void params) {
+    List<Concrete.Parameter> parameters = new ArrayList<>();
+    convertSigmaAppHoles(expr, parameters);
+    if (!parameters.isEmpty())
+      return new Concrete.LamExpression(expr.getData(), parameters, expr).accept(this, null);
     try (Utils.ContextSaver ignored = new Utils.ContextSaver(myContext)) {
       visitParameters(expr.getParameters(), null);
       for (Concrete.TypeParameter parameter : expr.getParameters()) {
@@ -525,6 +533,10 @@ else if (elem.expression instanceof Concrete.ProjExpression)
         elem.expression = visitProj((Concrete.ProjExpression) elem.expression, null);
       else if (elem.expression instanceof Concrete.CaseExpression)
         elem.expression = visitCase((Concrete.CaseExpression) elem.expression, null);
+      else if (elem.expression instanceof Concrete.PiExpression)
+        elem.expression = visitPi((Concrete.PiExpression) elem.expression, null);
+      else if (elem.expression instanceof Concrete.SigmaExpression)
+        elem.expression = visitSigma((Concrete.SigmaExpression) elem.expression, null);
       else if (elem.expression instanceof Concrete.BinOpSequenceExpression)
         elem.expression = visitBinOpSequence((Concrete.BinOpSequenceExpression) elem.expression, null);
       else if (elem.expression instanceof Concrete.ReferenceExpression)
@@ -542,6 +554,10 @@ else if (expression instanceof Concrete.BinOpSequenceExpression)
       convertBinOpAppHoles((Concrete.BinOpSequenceExpression) expression, parameters);
     else if (expression instanceof Concrete.CaseExpression)
       convertCaseAppHoles((Concrete.CaseExpression) expression, parameters);
+    else if (expression instanceof Concrete.PiExpression)
+      convertPiAppHoles((Concrete.PiExpression) expression, parameters);
+    else if (expression instanceof Concrete.SigmaExpression)
+      convertSigmaAppHoles((Concrete.SigmaExpression) expression, parameters);
   }
 
   private static void convertAppHoles(Concrete.AppExpression expr, List<Concrete.Parameter> parameters) {
@@ -578,4 +594,29 @@ private void convertCaseAppHoles(Concrete.CaseExpression expr, List<Concrete.Par
         argument.expression = new Concrete.ReferenceExpression(data, ref);
       } else convertRecursively(argument.expression, parameters);
   }
+
+  private void convertPiAppHoles(Concrete.PiExpression expr, List<Concrete.Parameter> parameters) {
+    for (Concrete.TypeParameter parameter : expr.getParameters())
+      convertParameterAppHoles(parameters, parameter);
+    if (expr.codomain instanceof Concrete.ApplyHoleExpression) {
+      Object data = expr.codomain.getData();
+      LocalReferable ref = new LocalReferable("p" + parameters.size());
+      parameters.add(new Concrete.NameParameter(data, true, ref));
+      expr.codomain = new Concrete.ReferenceExpression(data, ref);
+    } else convertRecursively(expr.codomain, parameters);
+  }
+
+  private void convertSigmaAppHoles(Concrete.SigmaExpression expr, List<Concrete.Parameter> parameters) {
+    for (Concrete.TypeParameter parameter : expr.getParameters())
+      convertParameterAppHoles(parameters, parameter);
+  }
+
+  private void convertParameterAppHoles(List<Concrete.Parameter> parameters, Concrete.TypeParameter parameter) {
+    if (parameter.type instanceof Concrete.ApplyHoleExpression) {
+      Object data = parameter.type.getData();
+      LocalReferable ref = new LocalReferable("p" + parameters.size());
+      parameters.add(new Concrete.NameParameter(data, true, ref));
+      parameter.type = new Concrete.ReferenceExpression(data, ref);
+    } else convertRecursively(parameter.type, parameters);
+  }
 }