parmatch.ml: refactor matrix_stable_vars to easily handle inconsistent matrices

gasche · gasche · commit 63ed2cc031a4 · 2017-12-31T12:48:54.000+01:00
diff --git a/typing/parmatch.ml b/typing/parmatch.ml
@@ -2135,23 +2135,22 @@ and simplify_head_pat head_bound_variables p ps varsets k =
   | _ ->
     (p, { row = ps; varsets = head_bound_variables :: varsets; }) :: k
 
+(* Compute stable bindings *)
 
-let split_rows rows =
-  let extend_row columns r =
-    { r with row = columns @ r.row } in
-  let q0 = discr_pat omega rows in
-  match build_specialized_submatrices ~extend_row q0 rows with
-  | { default; constrs = [] } -> [default]
-  | { default = _; constrs } -> List.map snd constrs
+type stable_vars =
+  | All
+  | Vars of IdSet.t
 
-(* Compute stable bindings *)
+let stable_inter sv1 sv2 = match sv1, sv2 with
+  | All, sv | sv, All -> sv
+  | Vars s1, Vars s2 -> Vars (IdSet.inter s1 s2)
 
 let reduce f = function
 | [] -> invalid_arg "reduce"
 | x::xs -> List.fold_left f x xs
 
 let rec matrix_stable_vars rs = match rs with
-| [] -> assert false (* No empty matrix *)
+| [] -> All
 | { row = []; _ } :: _ ->
     (* All rows have the same number of columns;
        if the first row is empty, they all are. *)
@@ -2165,13 +2164,27 @@ let rec matrix_stable_vars rs = match rs with
     let stables_in_varsets = reduce (List.map2 IdSet.inter) rows_varsets in
 
     (* The stable variables are those stable at any position *)
-    List.fold_left IdSet.union IdSet.empty stables_in_varsets
-| rs ->
-   let submatrices = split_rows (simplify_first_col rs) in
-   let submat_stable = List.map matrix_stable_vars submatrices in
-   (* a stable variable must be stable in each submatrix;
-      if the matrix has at least one row, there is at least one submatrix *)
-   reduce IdSet.inter submat_stable
+    Vars (List.fold_left IdSet.union IdSet.empty stables_in_varsets)
+| rows ->
+    let rows = simplify_first_col rows in
+    let extend_row columns r =
+      { r with row = columns @ r.row } in
+    let q0 = discr_pat omega rows in
+    match build_specialized_submatrices ~extend_row q0 rows with
+    | { default; constrs = [] } ->
+        (* the first column contains no head constructor;
+           they are all _ after simplification, so it can be dropped *)
+        matrix_stable_vars default
+    | { default = _; constrs } ->
+        (* A stable variable must be stable in each submatrix.
+
+           If the first column contains some head constructors, there
+           is no need to look at stability for the default matrix: all
+           other submatrices contain the default matrix, so they have
+           less stable variables. *)
+        let submatrices = List.map snd constrs in
+        let submat_stable = List.map matrix_stable_vars submatrices in
+        List.fold_left stable_inter All submat_stable
 
 let pattern_stable_vars p = matrix_stable_vars [{varsets = []; row = [p]}]
 
@@ -2239,12 +2252,14 @@ let check_ambiguous_bindings =
             let all =
               IdSet.inter (pattern_vars p) (all_rhs_idents g) in
             if not (IdSet.is_empty all) then begin
-              let stable = pattern_stable_vars p in
-              let ambiguous = IdSet.diff all stable in
-              if not (IdSet.is_empty ambiguous) then begin
-                let pps = IdSet.elements ambiguous |> List.map Ident.name in
-                let warn = Ambiguous_pattern pps in
-                Location.prerr_warning p.pat_loc warn
-              end
+              match pattern_stable_vars p with
+              | All -> ()
+              | Vars stable ->
+                  let ambiguous = IdSet.diff all stable in
+                  if not (IdSet.is_empty ambiguous) then begin
+                    let pps = IdSet.elements ambiguous |> List.map Ident.name in
+                    let warn = Ambiguous_pattern pps in
+                    Location.prerr_warning p.pat_loc warn
+                  end
             end)
         cases
