Fixed the menhir sum type parsing & conversion to match hazel sum typ…

…e parsing
hazelgrove · Dec 2, 2024 · b5ed4c3 · b5ed4c3
1 parent 115d4e2
commit b5ed4c3
Show file tree

Hide file tree

Showing 5 changed files with 7,708 additions and 4 deletions.
diff --git a/src/haz3lmenhir/AST.re b/src/haz3lmenhir/AST.re
@@ -82,7 +82,7 @@ type typ =
   | BoolType
   | UnitType
   | SumTyp(typ, option(typ))
-  | SumTerm(string, typ)
+  | SumTerm(string, option(typ))
   | UnknownType(typ_provenance)
   | TupleType(list(typ))
   | ArrayType(typ)

diff --git a/src/haz3lmenhir/Conversion.re b/src/haz3lmenhir/Conversion.re
@@ -265,12 +265,29 @@ and Typ: {
   }
   and constructormap_of_sumterm_list =
       (terms: list(AST.typ)): Haz3lcore.ConstructorMap.t(Haz3lcore.Typ.t) => {
-    List.map(constructormap_variant_of_sumterm, terms);
+    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) => Variant(name, [], Some(of_menhir_ast(typs)))
+    | 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)
+      }
     | _ =>
       raise(
         Failure(