Merge branch 'mappings' into sail2

1 files changed, 6 insertions, 0 deletions

diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml
index c13452ff..2372ea82 100644
--- a/src/pattern_completeness.ml
+++ b/src/pattern_completeness.ml
@@ -68,6 +68,7 @@ type gpat =
   | GP_cons of gpat * gpat
   | GP_app of (gpat Bindings.t)
   | GP_record of (gpat Bindings.t)
+  | GP_string_append of gpat list
 
 let rec string_of_gpat = function
   | GP_lit lit -> string_of_lit lit
@@ -80,12 +81,14 @@ let rec string_of_gpat = function
   | GP_app app ->
      Util.string_of_list "|" (fun (id, gpat) -> string_of_id id ^ string_of_gpat gpat) (Bindings.bindings app)
   | GP_record _ -> "GP RECORD"
+  | GP_string_append gpats -> Util.string_of_list " ^^ " string_of_gpat gpats
 
 let is_wild = function
   | GP_wild -> true
   | _ -> false
 
 let rec generalize ctx (P_aux (p_aux, _) as pat) =
+
   match p_aux with
   | P_lit lit -> GP_lit lit
   | P_wild -> GP_wild
@@ -116,6 +119,9 @@ let rec generalize ctx (P_aux (p_aux, _) as pat) =
      let ghd_pat = generalize ctx hd_pat in
      let gtl_pat = generalize ctx tl_pat in
      if is_wild ghd_pat && is_wild gtl_pat then GP_wild else GP_cons (ghd_pat, gtl_pat)
+  | P_string_append pats ->
+     let gpats = List.map (generalize ctx) pats in
+     if List.for_all is_wild gpats then GP_wild else GP_string_append gpats
   | P_app (f, pats) ->
      let gpats = List.map (generalize ctx) pats in
      if List.for_all is_wild gpats then