add missing checks in create_tysymbol

src/term.ml

@@ -105,13 +105,22 @@ module Ty = struct
   let ty_exists pr ty =
     try ty_fold (exists_fn pr) false ty with FoldSkip -> true
 
-  (* set of free type variables *)
+  (* smart constructors *)
 
-  let rec ty_vars acc ty = match ty.ty_node with
-    | Tyvar u -> Name.S.add u acc
-    | _ -> ty_fold ty_vars acc ty
+  let tv_add_unique vs tv = if Name.S.mem tv vs
+    then raise NonLinearPattern else Name.S.add tv vs
 
-  (* smart constructors *)
+  let rec tv_known vs ty = match ty.ty_node with
+    | Tyvar n -> Name.S.mem n vs
+    | _ -> ty_forall (tv_known vs) ty
+
+  let create_tysymbol name args def =
+    let tvs = List.fold_left tv_add_unique Name.S.empty args in
+    let _ = match def with
+      | Some ty -> tv_known tvs ty || raise UnboundVariable
+      | _ -> true
+    in
+    create_tysymbol name args def
 
   exception BadTypeArity
 
@@ -119,6 +128,8 @@ module Ty = struct
     if List.length tl == List.length s.ts_args
       then ty_app s tl else raise BadTypeArity
 
+  (* type matching *)
+
   exception TypeMismatch
 
   let rec matching s ty1 ty2 =
@@ -672,8 +683,8 @@ let rec t_vars lvl acc t = match t.t_node with
 
 and f_vars lvl acc t = f_fold_unsafe t_vars f_vars lvl acc t
 
-let t_vars s t = t_vars 0 s t
-let f_vars s f = f_vars 0 s f
+let t_freevars s t = t_vars 0 s t
+let f_freevars s f = f_vars 0 s f
 
 (* USE PHYSICAL EQUALITY *)
 (*

src/term.mli

@@ -49,7 +49,6 @@ module Ty : sig
   val ty_fold : ('a -> ty -> 'a) -> 'a -> ty -> 'a
   val ty_forall : (ty -> bool) -> ty -> bool
   val ty_exists : (ty -> bool) -> ty -> bool
-  val ty_vars : Name.S.t -> ty -> Name.S.t
 
   val ty_match : ty -> ty -> ty Name.M.t -> ty Name.M.t option
 
@@ -268,8 +267,8 @@ val f_subst_single : vsymbol -> term -> fmla -> fmla
 
 (* set of free variables *)
 
-val t_vars : Svs.t -> term -> Svs.t
-val f_vars : Svs.t -> fmla -> Svs.t
+val t_freevars : Svs.t -> term -> Svs.t
+val f_freevars : Svs.t -> fmla -> Svs.t
 
 (* USE PHYSICAL EQUALITY *)
 (*