Make AST sum type closer to Haz3lcore

hazelgrove · Dec 16, 2024 · 92b9d5d · 92b9d5d
1 parent d13e07c
commit 92b9d5d
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 59 deletions.
diff --git a/src/haz3lmenhir/AST.re b/src/haz3lmenhir/AST.re
@@ -89,16 +89,19 @@ type typ =
   | FloatType
   | BoolType
   | UnitType
-  | SumTyp(typ, option(typ))
-  | SumTerm(string, option(typ))
+  | SumTyp(sumtype)
   | UnknownType(typ_provenance)
   | TupleType(list(typ))
   | ArrayType(typ)
   | ArrowType(typ, 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
@@ -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 => {