Merge pull request #3391 from mtzguido/mlfix

extraction: fix missing cases in mlpattern_to_string
FStarLang · Aug 21, 2024 · 6106046 · 6106046
2 parents 9096467 + a1b94a8
commit 6106046
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 0 deletions.
diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml
diff --git a/src/extraction/FStar.Extraction.ML.Syntax.fst b/src/extraction/FStar.Extraction.ML.Syntax.fst
@@ -205,6 +205,10 @@ and mlpattern_to_string mlp =
   | MLP_Const c -> BU.format1 "(MLP_Const %s)" (mlconstant_to_string c)
   | MLP_Var x -> BU.format1 "(MLP_Var %s)" x
   | MLP_CTor (p, ps) -> BU.format2 "(MLP_CTor (%s, [%s]))" (string_of_mlpath p) (String.concat "; " (List.map mlpattern_to_string ps))
+  | MLP_Branch ps -> BU.format1 "(MLP_Branch [%s])" (String.concat "; " (List.map mlpattern_to_string ps))
+
+  | MLP_Record (path, fields) ->
+    BU.format2 "(MLP_Record (%s, [%s]))" (String.concat "." path) (String.concat "; " (List.map (fun (x, p) -> BU.format2 "(%s, %s)" x (mlpattern_to_string p)) fields))
   | MLP_Tuple ps -> BU.format1 "(MLP_Tuple [%s])" (String.concat "; " (List.map mlpattern_to_string ps))
 
 let mltybody_to_string (d:mltybody) : string =