Make some functions on terms more robust w.r.t new term constructs.

Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.

2 files changed, 34 insertions, 13 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 737e86848..8b78a91b5 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -159,11 +159,8 @@ let rec constr_expr_eq e1 e2 =
       Id.equal id1 id2 && List.equal instance_eq c1 c2
     | CSort s1, CSort s2 ->
       Miscops.glob_sort_eq s1 s2
-    | CCast(a1,(CastConv b1|CastVM b1)), CCast(a2,(CastConv b2|CastVM b2)) ->
-      constr_expr_eq a1 a2 &&
-      constr_expr_eq b1 b2
-    | CCast(a1,CastCoerce), CCast(a2, CastCoerce) ->
-      constr_expr_eq a1 a2
+  | CCast(t1,c1), CCast(t2,c2) ->
+    constr_expr_eq t1 t2 && cast_expr_eq c1 c2
     | CNotation(n1, s1), CNotation(n2, s2) ->
       String.equal n1 n2 &&
       constr_notation_substitution_eq s1 s2
@@ -176,7 +173,10 @@ let rec constr_expr_eq e1 e2 =
     | CDelimiters(s1,e1), CDelimiters(s2,e2) ->
       String.equal s1 s2 &&
       constr_expr_eq e1 e2
-    | _ -> false
+  | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
+     | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
+     | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
+     | CGeneralization _ | CDelimiters _), _ -> false
 
 and args_eq (a1,e1) (a2,e2) =
   Option.equal (eq_located explicitation_eq) e1 e2 &&
@@ -232,6 +232,16 @@ and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) =
 and instance_eq (x1,c1) (x2,c2) =
   Id.equal x1 x2 && constr_expr_eq c1 c2
 
+and cast_expr_eq c1 c2 = match c1, c2 with
+| CastConv t1, CastConv t2
+| CastVM t1, CastVM t2
+| CastNative t1, CastNative t2 -> constr_expr_eq t1 t2
+| CastCoerce, CastCoerce -> true
+| CastConv _, _
+| CastVM _, _
+| CastNative _, _
+| CastCoerce, _ -> false
+
 let constr_loc c = CAst.(c.loc)
 let cases_pattern_expr_loc cp = CAst.(cp.loc)
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 0344dda97..20492e38c 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -980,6 +980,19 @@ let match_termlist match_fun alp metas sigma rest x y iter termin lassoc =
   else
     bind_termlist_env alp sigma x l
 
+let match_cast match_fun sigma c1 c2 =
+  match c1, c2 with
+  | CastConv t1, CastConv t2
+  | CastVM t1, CastVM t2
+  | CastNative t1, CastNative t2 ->
+    match_fun sigma t1 t2
+  | CastCoerce, CastCoerce ->
+    sigma
+  | CastConv _, _
+  | CastVM _, _
+  | CastNative _, _
+  | CastCoerce, _ -> raise No_match
+
 let does_not_come_from_already_eta_expanded_var glob =
   (* This is hack to avoid looping on a rule with rhs of the form *)
   (* "?f (fun ?x => ?g)" since otherwise, matching "F H" expands in *)
@@ -1125,11 +1138,8 @@ let rec match_ inner u alp metas sigma a1 a2 =
       let alp,sigma = Array.fold_right2 (fun id1 id2 alsig ->
 	match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in
       Array.fold_left2 (match_in u alp metas) sigma bl1 bl2
-  | GCast(c1,CastConv t1), NCast (c2,CastConv t2)
-  | GCast(c1,CastVM t1), NCast (c2,CastVM t2) ->
-      match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2
-  | GCast(c1, CastCoerce), NCast(c2, CastCoerce) ->
-      match_in u alp metas sigma c1 c2
+  | GCast(t1, c1), NCast(t2, c2) ->
+    match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2
   | GSort (GType _), NSort (GType _) when not u -> sigma
   | GSort s1, NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma
   | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
@@ -1157,8 +1167,9 @@ let rec match_ inner u alp metas sigma a1 a2 =
           match_names metas (alp,sigma) (Name id') na in
       match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2
 
-  | (GRec _ | GEvar _), _
-  | _,_ -> raise No_match
+  | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
+     | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
+     | GCast _), _ -> raise No_match
 
 and match_in u = match_ true u