- don't return the set of bound variables in open_branch,

  as it is most often ignored
- check for empty map in t_subst/f_subst
- bugfix: don't forget nested match statements in Decl and Compile_match

src/core/decl.ml

@@ -514,18 +514,18 @@ exception NonExhaustiveExpr of (pattern list * expr)
 
 let rec check_matchT kn () t = match t.t_node with
   | Tcase (tl,bl) ->
-      let mk_b (pl,_,t) = (pl,t) in
-      let bl = List.map (fun b -> mk_b (t_open_branch b)) bl in
+      let bl = List.map t_open_branch bl in
       ignore (try Pattern.CompileTerm.compile (find_constructors kn) tl bl
-      with Pattern.NonExhaustive pl -> raise (NonExhaustiveExpr (pl, Term t)))
+      with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,Term t)));
+      t_fold (check_matchT kn) (check_matchF kn) () t
   | _ -> t_fold (check_matchT kn) (check_matchF kn) () t
 
 and check_matchF kn () f = match f.f_node with
   | Fcase (tl,bl) ->
-      let mk_b (pl,_,f) = (pl,f) in
-      let bl = List.map (fun b -> mk_b (f_open_branch b)) bl in
+      let bl = List.map f_open_branch bl in
       ignore (try Pattern.CompileFmla.compile (find_constructors kn) tl bl
-      with Pattern.NonExhaustive pl -> raise (NonExhaustiveExpr (pl, Fmla f)))
+      with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,Fmla f)));
+      f_fold (check_matchT kn) (check_matchF kn) () f
   | _ -> f_fold (check_matchT kn) (check_matchF kn) () f
 
 let check_match kn d = decl_fold (check_matchT kn) (check_matchF kn) () d

src/core/pretty.ml

@@ -237,16 +237,16 @@ and print_fnode opl opr fmt f = match f.f_node with
         print_fmla f1 print_fmla f2 print_opl_fmla f3
 
 and print_tbranch fmt br =
-  let pl,svs,t = t_open_branch br in
+  let pl,t = t_open_branch br in
   fprintf fmt "@[<hov 4>| %a ->@ %a@]"
     (print_list comma print_pat) pl print_term t;
-  Svs.iter forget_var svs
+  Svs.iter forget_var (List.fold_left pat_freevars Svs.empty pl)
 
 and print_fbranch fmt br =
-  let pl,svs,f = f_open_branch br in
+  let pl,f = f_open_branch br in
   fprintf fmt "@[<hov 4>| %a ->@ %a@]"
     (print_list comma print_pat) pl print_fmla f;
-  Svs.iter forget_var svs
+  Svs.iter forget_var (List.fold_left pat_freevars Svs.empty pl)
 
 and print_tl fmt tl =
   if tl = [] then () else fprintf fmt "@ [%a]"

src/core/term.ml

@@ -152,6 +152,12 @@ let pat_all pr pat =
 let pat_any pr pat =
   try pat_fold (any_fn pr) false pat with FoldSkip -> true
 
+let rec pat_freevars s pat = match pat.pat_node with
+  | Pwild -> s
+  | Pvar v -> Svs.add v s
+  | Pas (p, v) -> pat_freevars (Svs.add v s) p
+  | Papp (_,pl) -> List.fold_left pat_freevars s pl
+
 (* smart constructors for patterns *)
 
 exception BadArity of int * int
@@ -850,19 +856,19 @@ let rec pat_rename ns p = match p.pat_node with
 let pat_substs pl =
   let m, _ = pat_varmap pl in
   Mvs.fold
-    (fun x i (vars, s, ns) ->
+    (fun x i (s, ns) ->
        let x' = fresh_vsymbol x in
-       Svs.add x' vars, Im.add i (t_var x') s, Mvs.add x x' ns)
+       Im.add i (t_var x') s, Mvs.add x x' ns)
     m
-    (Svs.empty, Im.empty, Mvs.empty)
+    (Im.empty, Mvs.empty)
 
 let t_open_branch (pl, _, t) =
-  let vars, s, ns = pat_substs pl in
-  (List.map (pat_rename ns) pl, vars, t_inst s 0 t)
+  let s, ns = pat_substs pl in
+  (List.map (pat_rename ns) pl, t_inst s 0 t)
 
 let f_open_branch (pl, _, f) =
-  let vars, s, ns = pat_substs pl in
-  (List.map (pat_rename ns) pl, vars, f_inst s 0 f)
+  let s, ns = pat_substs pl in
+  (List.map (pat_rename ns) pl, f_inst s 0 f)
 
 (** Term library *)
 
@@ -888,10 +894,10 @@ let e_equal e1 e2 = match e1, e2 with
 let tr_equal = List.for_all2 (List.for_all2 e_equal)
 
 let t_branch fn acc b =
-  let pl,_,t = t_open_branch b in let t' = fn t in acc && t' == t, (pl, t')
+  let pl,t = t_open_branch b in let t' = fn t in acc && t' == t, (pl, t')
 
 let f_branch fn acc b =
-  let pl,_,f = f_open_branch b in let f' = fn f in acc && f' == f, (pl, f')
+  let pl,f = f_open_branch b in let f' = fn f in acc && f' == f, (pl, f')
 
 let t_map fnT fnF t = t_label_copy t (match t.t_node with
   | Tbvar _ -> raise UnboundIndex
@@ -934,8 +940,8 @@ let t_map fnT = t_map (protect fnT)
 
 (* safe opening fold *)
 
-let t_branch fn acc b = let _,_,t = t_open_branch b in fn acc t
-let f_branch fn acc b = let _,_,f = f_open_branch b in fn acc f
+let t_branch fn acc b = let _,t = t_open_branch b in fn acc t
+let f_branch fn acc b = let _,f = f_open_branch b in fn acc f
 
 let t_fold fnT fnF acc t = match t.t_node with
   | Tbvar _ -> raise UnboundIndex
@@ -998,8 +1004,8 @@ let f_v_fold fn = f_v_fold fn 0
 
 (* looks for occurrence of a variable from set [s] in a term [t] *)
 
-let t_occurs s t = t_v_any (fun u -> Svs.mem u s) t
-let f_occurs s f = f_v_any (fun u -> Svs.mem u s) f
+let t_occurs s t = not (Svs.is_empty s) && t_v_any (fun u -> Svs.mem u s) t
+let f_occurs s f = not (Svs.is_empty s) && f_v_any (fun u -> Svs.mem u s) f
 
 let t_occurs_single v t = t_v_any (fun u -> u == v) t
 let f_occurs_single v f = f_v_any (fun u -> u == v) f
@@ -1008,8 +1014,8 @@ let f_occurs_single v f = f_v_any (fun u -> u == v) f
 
 let find_vs m u = try Mvs.find u m with Not_found -> t_var u
 
-let t_subst m t = t_v_map (find_vs m) t
-let f_subst m f = f_v_map (find_vs m) f
+let t_subst m t = if Mvs.is_empty m then t else t_v_map (find_vs m) t
+let f_subst m f = if Mvs.is_empty m then f else f_v_map (find_vs m) f
 
 let eq_vs v t u = if u == v then t else t_var u
 

src/core/term.mli

@@ -84,6 +84,8 @@ val pat_fold : ('a -> pattern -> 'a) -> 'a -> pattern -> 'a
 val pat_all : (pattern -> bool) -> pattern -> bool
 val pat_any : (pattern -> bool) -> pattern -> bool
 
+val pat_freevars : Svs.t -> pattern -> Svs.t
+
 (** Terms and formulas *)
 
 type label = string
@@ -216,8 +218,8 @@ val f_let_simp : vsymbol -> term -> fmla -> fmla
 val t_open_bound : term_bound -> vsymbol * term
 val f_open_bound : fmla_bound -> vsymbol * fmla
 
-val t_open_branch : term_branch -> pattern list * Svs.t * term
-val f_open_branch : fmla_branch -> pattern list * Svs.t * fmla
+val t_open_branch : term_branch -> pattern list * term
+val f_open_branch : fmla_branch -> pattern list * fmla
 
 val f_open_quant : fmla_quant -> vsymbol list * trigger list * fmla
 

src/printer/coq.ml

@@ -229,16 +229,16 @@ and print_fnode opl opr drv fmt f = match f.f_node with
     end
 
 and print_tbranch drv fmt br =
-  let pl,svs,t = t_open_branch br in
+  let pl,t = t_open_branch br in
   fprintf fmt "@[<hov 4>| %a =>@ %a@]"
     (print_list comma (print_pat drv)) pl (print_term drv) t;
-  Svs.iter forget_var svs
+  Svs.iter forget_var (List.fold_left pat_freevars Svs.empty pl)
 
 and print_fbranch drv fmt br =
-  let pl,svs,f = f_open_branch br in
+  let pl,f = f_open_branch br in
   fprintf fmt "@[<hov 4>| %a =>@ %a@]"
     (print_list comma (print_pat drv)) pl (print_fmla drv) f;
-  Svs.iter forget_var svs
+  Svs.iter forget_var (List.fold_left pat_freevars Svs.empty pl)
 
 and print_tl drv fmt tl =
   if tl = [] then () else fprintf fmt "@ [%a]"

src/printer/why3.ml

@@ -230,16 +230,16 @@ and print_fnode opl opr drv fmt f = match f.f_node with
     end
 
 and print_tbranch drv fmt br =
-  let pl,svs,t = t_open_branch br in
+  let pl,t = t_open_branch br in
   fprintf fmt "@[<hov 4>| %a ->@ %a@]"
     (print_list comma (print_pat drv)) pl (print_term drv) t;
-  Svs.iter forget_var svs
+  Svs.iter forget_var (List.fold_left pat_freevars Svs.empty pl)
 
 and print_fbranch drv fmt br =
-  let pl,svs,f = f_open_branch br in
+  let pl,f = f_open_branch br in
   fprintf fmt "@[<hov 4>| %a ->@ %a@]"
     (print_list comma (print_pat drv)) pl (print_fmla drv) f;
-  Svs.iter forget_var svs
+  Svs.iter forget_var (List.fold_left pat_freevars Svs.empty pl)
 
 and print_tl drv fmt tl =
   if tl = [] then () else fprintf fmt "@ [%a]"

src/transform/compile_match.ml

@@ -23,14 +23,16 @@ open Task
 
 let rec rewriteT kn t = match t.t_node with
   | Tcase (tl,bl) ->
-      let mk_b (pl,_,t) = (pl,t) in
+      let tl = List.map (rewriteT kn) tl in
+      let mk_b (pl,t) = (pl, rewriteT kn t) in
       let bl = List.map (fun b -> mk_b (t_open_branch b)) bl in
       Pattern.CompileTerm.compile (find_constructors kn) tl bl
   | _ -> t_map (rewriteT kn) (rewriteF kn) t
 
 and rewriteF kn f = match f.f_node with
   | Fcase (tl,bl) ->
-      let mk_b (pl,_,f) = (pl,f) in
+      let tl = List.map (rewriteT kn) tl in
+      let mk_b (pl,f) = (pl, rewriteF kn f) in
       let bl = List.map (fun b -> mk_b (f_open_branch b)) bl in
       Pattern.CompileFmla.compile (find_constructors kn) tl bl
   | _ -> f_map (rewriteT kn) (rewriteF kn) f

src/transform/eliminate_algebraic.ml

@@ -39,7 +39,7 @@ let uncompiled = "eliminate_algebraic: compile_match required"
 let rec rewriteT kn state t = match t.t_node with
   | Tcase ([t1],bl) ->
       let mk_br (w,m) br =
-        let (pl,_,e) = t_open_branch br in
+        let (pl,e) = t_open_branch br in
         match pl with
         | [{ pat_node = Papp (cs,pl) }] ->
             let add_var e p pj = match p.pat_node with
@@ -67,7 +67,7 @@ let rec rewriteT kn state t = match t.t_node with
 and rewriteF kn state f = match f.f_node with
   | Fcase ([t1],bl) ->
       let mk_br (w,m) br =
-        let (pl,_,e) = f_open_branch br in
+        let (pl,e) = f_open_branch br in
         match pl with
         | [{ pat_node = Papp (cs,pl) }] ->
             let add_var e p pj = match p.pat_node with