add_new for maps and sets + some minor changes

src/core/decl.ml

@@ -236,7 +236,8 @@ let check_termination ldl =
   Mls.iter (build_call_graph cgr syms) syms;
   let check ls _ =
     let cl = build_call_list cgr ls in
-    check_call_list ls cl in
+    check_call_list ls cl
+  in
   Mls.mapi check syms
 
 (** Inductive predicate declaration *)
@@ -372,8 +373,7 @@ exception EmptyDecl
 exception EmptyAlgDecl of tysymbol
 exception EmptyIndDecl of lsymbol
 
-let news_id s id = Sid.change id (fun there ->
-  if there then raise (ClashIdent id) else true) s
+let news_id s id = Sid.add_new id (ClashIdent id) s
 
 let syms_ts s ts = Sid.add ts.ts_name s
 let syms_ls s ls = Sid.add ls.ls_name s

src/core/pattern.ml

@@ -67,23 +67,22 @@ module Compile (X : Action) = struct
         in
         (* dispatch every case to a primitive constructor/wild case *)
         let cases,wilds =
-          let change_case fs pl a cases =
+          let add_case fs pl a cases =
             Mls.change fs (function
               | None -> Some [pl,a]
-              | Some rl -> Some ((pl,a)::rl)) cases in
+              | Some rl -> Some ((pl,a)::rl)) cases
+          in
           let union_cases pl a types cases =
-            let make_wild pl a ql =
-              let add pl q = pat_wild q.pat_ty :: pl in
-              [List.fold_left add pl ql,a]
-            in
-            let types = Mls.map (make_wild pl a) types in
-            Mls.union (fun _ pla rl -> Some (List.append pla rl))
-              types cases in
+            let add pl q = pat_wild q.pat_ty :: pl in
+            let wild ql = [List.fold_left add pl ql, a] in
+            let join _ wl rl = Some (List.append wl rl) in
+            Mls.union join (Mls.map wild types) cases
+          in
           let rec dispatch (pl,a) (cases,wilds) =
             let p = List.hd pl in let pl = List.tl pl in
             match p.pat_node with
               | Papp (fs,pl') ->
-                  change_case fs (List.rev_append pl' pl) a cases, wilds
+                  add_case fs (List.rev_append pl' pl) a cases, wilds
               | Por (p,q) ->
                   dispatch (p::pl, a) (dispatch (q::pl, a) (cases,wilds))
               | Pas (p,x) ->
@@ -129,8 +128,8 @@ module Compile (X : Action) = struct
             if Mls.mem cs types then comp_cases cs al else comp_wilds ()
         | _ ->
             let base =
-              if Mls.submap (fun _ () _ -> true) css types
-              then [] else [mk_branch (pat_wild ty) (comp_wilds ())]
+              if Mls.submap (const3 true) css types then []
+              else [mk_branch (pat_wild ty) (comp_wilds ())]
             in
             let add cs ql acc =
               let get_vs q = create_vsymbol (id_fresh "x") q.pat_ty in

src/core/printer.ml

@@ -142,16 +142,12 @@ let remove_prop pr =
 let get_syntax_map task =
   let add_ts td m = match td.td_node with
     | Meta (_,[MAts ts; MAstr s]) ->
-      Mid.change ts.ts_name (function
-        | None -> Some s
-        | Some _ -> raise (KnownTypeSyntax ts)) m
+        Mid.add_new ts.ts_name s (KnownTypeSyntax ts) m
     | _ -> assert false
   in
   let add_ls td m = match td.td_node with
     | Meta (_,[MAls ls; MAstr s]) ->
-      Mid.change ls.ls_name (function
-        | None -> Some s
-        | Some _ -> raise (KnownLogicSyntax ls)) m
+        Mid.add_new ls.ls_name s (KnownLogicSyntax ls) m
     | _ -> assert false
   in
   let m = Mid.empty in

src/core/ty.ml

@@ -139,9 +139,7 @@ exception DuplicateTypeVar of tvsymbol
 exception UnboundTypeVar of tvsymbol
 
 let create_tysymbol name args def =
-  let add s v = Stv.change v (fun there ->
-    if there then raise (DuplicateTypeVar v) else true) s
-  in
+  let add s v = Stv.add_new v (DuplicateTypeVar v) s in
   let s = List.fold_left add Stv.empty args in
   let rec vars () ty = match ty.ty_node with
     | Tyvar v when not (Stv.mem v s) -> raise (UnboundTypeVar v)

src/util/stdlib.ml

@@ -62,6 +62,7 @@ module type S =
     val mapi_fold:
       (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
     val translate : (key -> key) -> 'a t -> 'a t
+    val add_new : key -> 'a -> exn -> 'a t -> 'a t
 
     module type Set =
     sig
@@ -95,6 +96,7 @@ module type S =
       val inter : t -> t -> t
       val diff : t -> t -> t
       val translate : (elt -> elt) -> t -> t
+      val add_new : elt -> exn -> t -> t
     end
 
     module Set : Set
@@ -496,6 +498,10 @@ module Make(Ord: OrderedType) = struct
           Node(l,v,d,r,h),last in
       let m,_ = aux None m in m
 
+    let add_new x v e m = change x (function
+      | Some _ -> raise e
+      | None -> Some v) m
+
     module type Set =
     sig
       type elt = key
@@ -528,6 +534,7 @@ module Make(Ord: OrderedType) = struct
       val inter : t -> t -> t
       val diff : t -> t -> t
       val translate : (elt -> elt) -> t -> t
+      val add_new : elt -> exn -> t -> t
     end
 
     module Set =
@@ -568,6 +575,7 @@ module Make(Ord: OrderedType) = struct
         let inter = inter (fun _ _ _ -> Some ())
         let diff = diff (fun _ _ _ -> None)
         let translate = translate
+        let add_new x = add_new x ()
       end
 
 end

src/util/stdlib.mli

@@ -225,6 +225,10 @@ module type S =
         function [f]. [f] must be strictly monotone on the key of [m].
         Otherwise it raises invalid_arg *)
 
+    val add_new : key -> 'a -> exn -> 'a t -> 'a t
+    (** [add_new x v e m] binds [x] to [v] in [m] if [x] is not bound,
+        and raises [exn] otherwise. *)
+
     module type Set =
     sig
       type elt = key
@@ -340,6 +344,10 @@ module type S =
       (** [translate f s] translates the elements in the set [s] by the
           function [f]. [f] must be strictly monotone on the elements of [s].
           Otherwise it raises invalid_arg *)
+
+      val add_new : elt -> exn -> t -> t
+      (** [add_new x e s] adds [x] to [s] if [s] does not contain [x],
+          and raises [exn] otherwise. *)
     end
 
     module Set : Set

src/util/util.ml

@@ -16,13 +16,19 @@
 (*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
 (*                                                                        *)
 (**************************************************************************)
+
 open Stdlib
+
 (* useful combinators *)
 
 let ($) f x = f x
 
 let const f _ = f
 
+let const2 f _ _ = f
+
+let const3 f _ _ _ = f
+
 let flip f x y = f y x
 
 let cons f acc x = (f x)::acc

src/util/util.mli

@@ -16,13 +16,19 @@
 (*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
 (*                                                                        *)
 (**************************************************************************)
+
 open Stdlib
+
 (** Useful functions *)
 
 val ($) : ('a -> 'b) -> 'a -> 'b
 
 val const : 'a -> 'b -> 'a
 
+val const2 : 'a -> 'b -> 'c -> 'a
+
+val const3 : 'a -> 'b -> 'c -> 'd -> 'a
+
 val flip : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
 
 val cons : ('a -> 'b) -> 'b list -> 'a -> 'b list
@@ -85,6 +91,7 @@ val any_fn : ('a -> bool) -> 'b -> 'a -> bool
 
 val ffalse : 'a -> bool
 (** [ffalse] constant function [false] *)
+
 val ttrue : 'a -> bool
 (** [ttrue] constant function [true] *)
 
@@ -120,7 +127,7 @@ module OrderedHashList (X : Tagged) : OrderedHash with type t = X.t list
 module StructMake (X : Tagged) :
 sig
   module M : Map.S with type key = X.t
-  module S : M.Set  with type elt = X.t
+  module S : M.Set
   module H : Hashtbl.S with type key = X.t
 end