From 92b9d5d8e1ef403082261ee6575c93e81c0a7235 Mon Sep 17 00:00:00 2001
From: Alexander Bandukwala <7h3kk1d@gmail.com>
Date: Mon, 16 Dec 2024 08:29:50 -0500
Subject: [PATCH] Make AST sum type closer to Haz3lcore

---
 src/haz3lmenhir/AST.re        |  9 +++--
 src/haz3lmenhir/Conversion.re | 68 +++++++----------------------------
 2 files changed, 18 insertions(+), 59 deletions(-)

diff --git a/src/haz3lmenhir/AST.re b/src/haz3lmenhir/AST.re
index aff75b41a..5657f37fb 100644
--- a/src/haz3lmenhir/AST.re
+++ b/src/haz3lmenhir/AST.re
@@ -89,8 +89,7 @@ type typ =
   | FloatType
   | BoolType
   | UnitType
-  | SumTyp(typ, option(typ))
-  | SumTerm(string, option(typ))
+  | SumTyp(sumtype)
   | UnknownType(typ_provenance)
   | TupleType(list(typ))
   | ArrayType(typ)
@@ -98,7 +97,11 @@ type typ =
   | TypVar(string)
   | InvalidTyp(string)
   | ForallType(tpat, typ)
-  | RecType(tpat, typ);
+  | RecType(tpat, typ)
+and sumterm =
+  | Variant(string, option(typ))
+  | BadEntry(typ)
+and sumtype = list(sumterm);
 
 [@deriving (show({with_path: false}), sexp, qcheck)]
 type pat =
diff --git a/src/haz3lmenhir/Conversion.re b/src/haz3lmenhir/Conversion.re
index 0d0399189..7c4613062 100644
--- a/src/haz3lmenhir/Conversion.re
+++ b/src/haz3lmenhir/Conversion.re
@@ -357,11 +357,7 @@ module rec Exp: {
 }
 and Typ: {
   let of_menhir_ast: AST.typ => Haz3lcore.Typ.t;
-  let constructormap_of_sumterm_list:
-    list(AST.typ) => Haz3lcore.ConstructorMap.t(Haz3lcore.Typ.t);
 
-  let constructormap_variant_of_sumterm:
-    AST.typ => Haz3lcore.ConstructorMap.variant(Haz3lcore.Typ.t);
   let of_core: Haz3lcore.Typ.t => AST.typ;
 } = {
   let rec of_menhir_ast = (typ: AST.typ): Haz3lcore.Typ.t => {
@@ -385,62 +381,22 @@ and Typ: {
     | TupleType(ts) => Prod(List.map(of_menhir_ast, ts))
     | ArrayType(t) => List(of_menhir_ast(t))
     | ArrowType(t1, t2) => Arrow(of_menhir_ast(t1), of_menhir_ast(t2))
-    | SumTyp(term, next) =>
-      let terms = ref([term]);
-      let rec go = (next: option(AST.typ)): list(AST.typ) => {
-        switch (next) {
-        | Some(t) =>
-          switch (t) {
-          | SumTyp(term, next) =>
-            terms := [term, ...terms^];
-            go(next);
-          | _ => raise(Failure("SumTyp conversion failure"))
-          }
-        | None => terms^
-        };
-      };
-      let _ = go(next);
-      let converted_terms = constructormap_of_sumterm_list(terms^);
+    | SumTyp(sumterms) =>
+      open Haz3lcore;
+      let converted_terms: list(ConstructorMap.variant(TermBase.typ_t)) =
+        List.map(
+          (sumterm: AST.sumterm): ConstructorMap.variant(TermBase.typ_t) =>
+            switch (sumterm) {
+            | Variant(name, typ) =>
+              Variant(name, [], Option.map(of_menhir_ast, typ))
+            | BadEntry(typ) => BadEntry(of_menhir_ast(typ))
+            },
+          sumterms,
+        );
       Sum(converted_terms);
-    | SumTerm(_) => raise(Failure("SumTerm conversion not possible"))
     | ForallType(tp, t) => Forall(TPat.of_menhir_ast(tp), of_menhir_ast(t))
     | RecType(tp, t) => Rec(TPat.of_menhir_ast(tp), of_menhir_ast(t))
     };
-  }
-  and constructormap_of_sumterm_list =
-      (terms: list(AST.typ)): Haz3lcore.ConstructorMap.t(Haz3lcore.Typ.t) => {
-    List.map(constructormap_variant_of_sumterm, terms) |> List.rev;
-  }
-  and constructormap_variant_of_sumterm =
-      (term: AST.typ): Haz3lcore.ConstructorMap.variant(Haz3lcore.Typ.t) => {
-    switch (term) {
-    | SumTerm(name, typs) =>
-      switch (typs) {
-      | Some(typs) =>
-        switch (typs) {
-        | TupleType(ts) =>
-          switch (List.length(ts)) {
-          | 1 => Variant(name, [], Some(of_menhir_ast(List.hd(ts))))
-          | _ => Variant(name, [], Some(of_menhir_ast(typs)))
-          }
-        | _ =>
-          raise(
-            Failure(
-              "TupleType expected in constructormap_variant_of_sumterm but not found",
-            ),
-          )
-        }
-      | None => Variant(name, [], None)
-      }
-    | UnknownType(EmptyHole) =>
-      BadEntry(Unknown(Hole(EmptyHole)) |> Haz3lcore.Typ.fresh) // TODO Figure out if this is correct
-    | _ =>
-      raise(
-        Failure(
-          "SumTerm expected in constructormap_variant_of_sumterm but not found",
-        ),
-      )
-    };
   };
   let of_core_type_provenance =
       (p: Haz3lcore.TermBase.type_provenance): AST.typ_provenance => {