- remove ls_constr field from lsymbol

- check pattern well-formedness in Pattern
- add arguments to exceptions in Ty and Term

src/core/decl.ml

@@ -38,14 +38,12 @@ type ls_defn = lsymbol * fmla
 type logic_decl = lsymbol * ls_defn option
 
 exception UnboundVars of Svs.t
-exception IllegalConstructor of lsymbol
 
 let check_fvs f =
   let fvs = f_freevars Svs.empty f in
   if Svs.is_empty fvs then f else raise (UnboundVars fvs)
 
 let make_fs_defn fs vl t =
-  if fs.ls_constr then raise (IllegalConstructor fs);
   let hd = t_app fs (List.map t_var vl) t.t_ty in
   let fd = f_forall vl [] (f_equ hd t) in
   fs, Some (fs, check_fvs fd)
@@ -197,8 +195,6 @@ let create_logic_decl ldl = Hsdecl.hashcons (mk_decl (Dlogic ldl))
 let create_ind_decl idl = Hsdecl.hashcons (mk_decl (Dind idl))
 let create_prop_decl k p f = Hsdecl.hashcons (mk_decl (Dprop (k,p,f)))
 
-exception ConstructorExpected of lsymbol
-exception UnboundTypeVar of tvsymbol
 exception IllegalTypeAlias of tysymbol
 exception ClashIdent of ident
 exception BadLogicDecl of ident
@@ -211,7 +207,6 @@ let add_id s id =
 let create_ty_decl tdl =
   if tdl = [] then raise EmptyDecl;
   let check_constr ty acc fs =
-    if not fs.ls_constr then raise (ConstructorExpected fs);
     let vty = of_option fs.ls_value in
     ignore (ty_match Mtv.empty vty ty);
     let add s ty = match ty.ty_node with
@@ -219,11 +214,12 @@ let create_ty_decl tdl =
       | _ -> assert false
     in
     let vs = ty_fold add Stv.empty vty in
-    let rec check () ty = match ty.ty_node with
-      | Tyvar v -> if not (Stv.mem v vs) then raise (UnboundTypeVar v)
-      | _ -> ty_fold check () ty
+    let rec check s ty = match ty.ty_node with
+      | Tyvar v when not (Stv.mem v vs) -> Stv.add v s
+      | _ -> ty_fold check s ty
     in
-    List.iter (check ()) fs.ls_args;
+    let ts = List.fold_left check Stv.empty fs.ls_args in
+    if not (Stv.is_empty ts) then raise (UnboundTypeVars ts);
     add_id acc fs.ls_name
   in
   let check_decl acc (ts,td) = match td with

src/core/decl.mli

@@ -102,15 +102,12 @@ val create_ind_decls : ind_decl list -> decl list
 
 (* exceptions *)
 
-exception ConstructorExpected of lsymbol
 exception IllegalTypeAlias of tysymbol
-exception UnboundTypeVar of tvsymbol
 
 exception InvalidIndDecl of lsymbol * prsymbol
 exception TooSpecificIndDecl of lsymbol * prsymbol * term
 exception NonPositiveIndDecl of lsymbol * prsymbol * lsymbol
 
-exception IllegalConstructor of lsymbol
 exception BadLogicDecl of ident
 exception UnboundVars of Svs.t
 exception ClashIdent of ident

src/core/pattern.ml

@@ -28,23 +28,34 @@ module type Action = sig
   val mk_case : term -> (pattern * action) list -> action
 end
 
+exception ConstructorExpected of lsymbol
 exception NonExhaustive of pattern list
 
 module Compile (X : Action) = struct
   open X
 
-  let rec compile css tl rl = match tl,rl with
+  let rec compile constructors tl rl = match tl,rl with
     | _, [] -> (* no actions *)
         let pl = List.map (fun t -> pat_wild t.t_ty) tl in
         raise (NonExhaustive pl)
     | [], (_,a) :: _ -> (* no terms, at least one action *)
         a
     | t :: tl, _ -> (* process the leftmost column *)
+        (* extract the set of constructors *)
+        let ty = t.t_ty in
+        let css = match ty.ty_node with
+          | Tyapp (ts,_) ->
+              let s_add s cs = Sls.add cs s in
+              List.fold_left s_add Sls.empty (constructors ts)
+          | Tyvar _ -> Sls.empty
+        in
         (* map constructors to argument types *)
         let rec populate types p = match p.pat_node with
           | Pwild | Pvar _ -> types
           | Pas (p,_) -> populate types p
-          | Papp (fs,pl) -> Mls.add fs pl types
+          | Papp (fs,pl) ->
+              if Sls.mem fs css then Mls.add fs pl types
+              else raise (ConstructorExpected fs)
         in
         let populate types (pl,_) = populate types (List.hd pl) in
         let types = List.fold_left populate Mls.empty rl in
@@ -72,27 +83,21 @@ module Compile (X : Action) = struct
         in
         let cases,wilds = List.fold_right dispatch rl (Mls.empty,[]) in
         (* assemble the primitive case statement *)
-        let ty = t.t_ty in
         let pw = pat_wild ty in
-        let exhaustive, nopat = match ty.ty_node with
-          | Tyapp (ts,_) ->
-              begin match css ts with
-              | [] -> false, pw
-              | cl ->
-                  let test cs = not (Mls.mem cs types) in
-                  begin match List.filter test cl with
-                  | cs :: _ ->
-                      (* FIXME? specialize types to t.t_ty *)
-                      let pl = List.map pat_wild cs.ls_args in
-                      false, pat_app cs pl (of_option cs.ls_value)
-                  | _ -> true, pw
-                  end
-              end
-          | Tyvar _ -> false, pw
+        let nopat =
+          if Sls.is_empty css then Some pw else
+          let test cs = not (Mls.mem cs types) in
+          let unused = Sls.filter test css in
+          if Sls.is_empty unused then None else
+          let cs = Sls.choose unused in
+          let pl = List.map pat_wild cs.ls_args in
+          Some (pat_app cs pl (of_option cs.ls_value))
         in
-        let base = if exhaustive then [] else
-          try [pw, compile css tl wilds]
-          with NonExhaustive pl -> raise (NonExhaustive (nopat::pl))
+        let base = match nopat with
+          | None -> []
+          | Some pat ->
+              (try [pw, compile constructors tl wilds]
+              with NonExhaustive pl -> raise (NonExhaustive (pat::pl)))
         in
         let add fs ql acc =
           let id = id_fresh "x" in
@@ -104,7 +109,7 @@ module Compile (X : Action) = struct
             | [], pl -> pat_app fs acc ty :: pl
             | _, _ -> assert false
           in
-          try (pat, compile css tl (Mls.find fs cases)) :: acc
+          try (pat, compile constructors tl (Mls.find fs cases)) :: acc
           with NonExhaustive pl -> raise (NonExhaustive (pat_cont [] vl pl))
         in
         match Mls.fold add types base with

src/core/pattern.mli

@@ -28,6 +28,7 @@ module type Action = sig
   val mk_case : term -> (pattern * action) list -> action
 end
 
+exception ConstructorExpected of lsymbol
 exception NonExhaustive of pattern list
 
 module Compile (X : Action) : sig

src/core/pretty.ml

@@ -40,7 +40,7 @@ let iprinter,tprinter,lprinter,pprinter =
   let usanitize = sanitizer char_to_ualpha char_to_alnumus in
   create_ident_printer bl ~sanitizer:isanitize,
   create_ident_printer bl ~sanitizer:lsanitize,
-  create_ident_printer bl ~sanitizer:lsanitize,
+  create_ident_printer bl ~sanitizer:isanitize,
   create_ident_printer bl ~sanitizer:usanitize
 
 let thash = Hid.create 63
@@ -61,9 +61,8 @@ let tv_set = ref Sid.empty
 (* type variables always start with a quote *)
 let print_tv fmt tv =
   tv_set := Sid.add tv.tv_name !tv_set;
-  let sanitize n = "'" ^ n in
-  let n = id_unique iprinter ~sanitizer:sanitize tv.tv_name in
-  fprintf fmt "%s" n
+  let sanitizer n = "'" ^ n in
+  fprintf fmt "%s" (id_unique iprinter ~sanitizer tv.tv_name)
 
 let forget_tvs () =
   Sid.iter (forget_id iprinter) !tv_set;
@@ -71,17 +70,15 @@ let forget_tvs () =
 
 (* logic variables always start with a lower case letter *)
 let print_vs fmt vs =
-  let sanitize = String.uncapitalize in
-  let n = id_unique iprinter ~sanitizer:sanitize vs.vs_name in
-  fprintf fmt "%s" n
+  let sanitizer = String.uncapitalize in
+  fprintf fmt "%s" (id_unique iprinter ~sanitizer vs.vs_name)
 
 let forget_var vs = forget_id iprinter vs.vs_name
 
 (* theory names always start with an upper case letter *)
 let print_th fmt th =
-  let sanitize = String.capitalize in
-  let n = id_unique iprinter ~sanitizer:sanitize th.th_name in
-  fprintf fmt "%s" n
+  let sanitizer = String.capitalize in
+  fprintf fmt "%s" (id_unique iprinter ~sanitizer th.th_name)
 
 let print_ts fmt ts =
   Hid.replace thash ts.ts_name ts;
@@ -89,11 +86,12 @@ let print_ts fmt ts =
 
 let print_ls fmt ls =
   Hid.replace lhash ls.ls_name ls;
-  let n = if ls.ls_constr
-    then id_unique lprinter ~sanitizer:String.capitalize ls.ls_name
-    else id_unique lprinter ls.ls_name
-  in
-  fprintf fmt "%s" n
+  fprintf fmt "%s" (id_unique lprinter ls.ls_name)
+
+let print_cs fmt ls =
+  Hid.replace lhash ls.ls_name ls;
+  let sanitizer = String.capitalize in
+  fprintf fmt "%s" (id_unique lprinter ~sanitizer ls.ls_name)
 
 let print_pr fmt pr =
   Hid.replace phash pr.pr_name pr;
@@ -141,7 +139,7 @@ let rec print_pat fmt p = match p.pat_node with
   | Pvar v -> print_vs fmt v
   | Pas (p,v) -> fprintf fmt "%a as %a" print_pat p print_vs v
   | Papp (cs,pl) -> fprintf fmt "%a%a"
-      print_ls cs (print_paren_r print_pat) pl
+      print_cs cs (print_paren_r print_pat) pl
 
 let print_vsty fmt v =
   fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
@@ -259,7 +257,7 @@ and print_expr fmt = e_apply (print_term fmt) (print_fmla fmt)
 (** Declarations *)
 
 let print_constr fmt cs =
-  fprintf fmt "@[<hov 4>| %a%a@]" print_ls cs
+  fprintf fmt "@[<hov 4>| %a%a@]" print_cs cs
     (print_paren_l print_ty) cs.ls_args
 
 let print_ty_args fmt = function

src/core/pretty.mli

@@ -34,6 +34,7 @@ val print_vs : formatter -> vsymbol -> unit       (* variable *)
 
 val print_ts : formatter -> tysymbol -> unit      (* type symbol *)
 val print_ls : formatter -> lsymbol -> unit       (* logic symbol *)
+val print_cs : formatter -> lsymbol -> unit       (* constructor symbol *)
 val print_pr : formatter -> prsymbol -> unit      (* proposition name *)
 
 val print_ty : formatter -> ty -> unit            (* type *)

src/core/term.ml

@@ -50,7 +50,6 @@ type lsymbol = {
   ls_name   : ident;
   ls_args   : ty list;
   ls_value  : ty option;
-  ls_constr : bool;
 }
 
 module Lsym = StructMake (struct
@@ -62,16 +61,14 @@ module Sls = Lsym.S
 module Mls = Lsym.M
 module Hls = Lsym.H
 
-let create_lsymbol name args value constr = {
+let create_lsymbol name args value = {
   ls_name   = id_register name;
   ls_args   = args;
   ls_value  = value;
-  ls_constr = constr;
 }
 
-let create_fsymbol nm al vl = create_lsymbol nm al (Some vl) false
-let create_fconstr nm al vl = create_lsymbol nm al (Some vl) true
-let create_psymbol nm al    = create_lsymbol nm al None false
+let create_fsymbol nm al vl = create_lsymbol nm al (Some vl)
+let create_psymbol nm al    = create_lsymbol nm al (None)
 
 (** Patterns *)
 
@@ -157,20 +154,19 @@ let pat_any pr pat =
 
 (* smart constructors for patterns *)
 
-exception BadArity
-exception ConstructorExpected of lsymbol
+exception BadArity of int * int
 exception FunctionSymbolExpected of lsymbol
 exception PredicateSymbolExpected of lsymbol
 
 let pat_app fs pl ty =
-  if not fs.ls_constr then raise (ConstructorExpected fs);
   let s = match fs.ls_value with
     | Some vty -> ty_match Mtv.empty vty ty
     | None -> raise (FunctionSymbolExpected fs)
   in
   let mtch s ty p = ty_match s ty p.pat_ty in
   ignore (try List.fold_left2 mtch s fs.ls_args pl
-          with Invalid_argument _ -> raise BadArity);
+    with Invalid_argument _ -> raise (BadArity
+      (List.length fs.ls_args, List.length pl)));
   pat_app fs pl ty
 
 let pat_as p v =
@@ -572,14 +568,16 @@ let t_app fs tl ty =
   in
   let mtch s ty t = ty_match s ty t.t_ty in
   ignore (try List.fold_left2 mtch s fs.ls_args tl
-          with Invalid_argument _ -> raise BadArity);
+    with Invalid_argument _ -> raise (BadArity
+      (List.length fs.ls_args, List.length tl)));
   t_app fs tl ty
 
 let t_app_infer fs tl =
   let mtch s ty t = ty_match s ty t.t_ty in
   let s =
     try List.fold_left2 mtch Mtv.empty fs.ls_args tl
-    with Invalid_argument _ -> raise BadArity
+    with Invalid_argument _ -> raise (BadArity
+      (List.length fs.ls_args, List.length tl))
   in
   let ty = match fs.ls_value with
     | Some ty -> ty_inst s ty
@@ -594,7 +592,8 @@ let f_app ps tl =
   in
   let mtch s ty t = ty_match s ty t.t_ty in
   ignore (try List.fold_left2 mtch s ps.ls_args tl
-          with Invalid_argument _ -> raise BadArity);
+    with Invalid_argument _ -> raise (BadArity
+      (List.length ps.ls_args, List.length tl)));
   f_app ps tl
 
 let p_check t p =
@@ -767,12 +766,12 @@ let f_inst_single v f = f_inst (Im.add 0 v Im.empty) 0 f
 
 (* safe smart constructors *)
 
-exception NonLinear of vsymbol
+exception DuplicateVar of vsymbol
 
 let f_quant q vl tl f = if vl = [] then f else
   let i = ref (-1) in
   let add m v =
-    if Mvs.mem v m then raise (NonLinear v);
+    if Mvs.mem v m then raise (DuplicateVar v);
     incr i; Mvs.add v !i m
   in
   let m = List.fold_left add Mvs.empty vl in
@@ -786,10 +785,10 @@ let pat_varmap pl =
   let i = ref (-1) in
   let rec mk_map acc p = match p.pat_node with
     | Pvar n ->
-        if Mvs.mem n acc then raise (NonLinear n);
+        if Mvs.mem n acc then raise (DuplicateVar n);
         incr i; Mvs.add n !i acc
     | Pas (p, n) ->
-        if Mvs.mem n acc then raise (NonLinear n);
+        if Mvs.mem n acc then raise (DuplicateVar n);
         incr i; mk_map (Mvs.add n !i acc) p
     | _ -> pat_fold mk_map acc p
   in

src/core/term.mli

@@ -39,13 +39,10 @@ type lsymbol = private {
   ls_name   : ident;
   ls_args   : ty list;
   ls_value  : ty option;
-  ls_constr : bool;
 }
 
-val create_lsymbol : preid -> ty list -> ty option -> bool -> lsymbol
-
+val create_lsymbol : preid -> ty list -> ty option -> lsymbol
 val create_fsymbol : preid -> ty list -> ty -> lsymbol
-val create_fconstr : preid -> ty list -> ty -> lsymbol
 val create_psymbol : preid -> ty list -> lsymbol
 
 module Sls : Set.S with type elt = lsymbol
@@ -54,9 +51,8 @@ module Hls : Hashtbl.S with type key = lsymbol
 
 (** Exceptions *)
 
-exception BadArity
-exception NonLinear of vsymbol
-exception ConstructorExpected of lsymbol
+exception BadArity of int * int
+exception DuplicateVar of vsymbol
 exception FunctionSymbolExpected of lsymbol
 exception PredicateSymbolExpected of lsymbol
 

src/core/theory.ml

@@ -336,7 +336,7 @@ let cl_find_ls cl ls =
   with Not_found ->
     let ta' = List.map (cl_trans_ty cl) ls.ls_args in
     let vt' = option_map (cl_trans_ty cl) ls.ls_value in
-    let ls' = create_lsymbol (id_dup ls.ls_name) ta' vt' ls.ls_constr in
+    let ls' = create_lsymbol (id_dup ls.ls_name) ta' vt' in
     cl_add_ls cl ls ls';
     ls'
 

src/core/ty.ml

@@ -119,33 +119,36 @@ let ty_any pr ty =
 
 (* smart constructors *)
 
-exception NonLinear
-exception UnboundTypeVariable
+exception BadTypeArity of int * int
+exception DuplicateTypeVar of tvsymbol
+exception UnboundTypeVars of Stv.t
 
-let rec tv_known vs ty = match ty.ty_node with
-  | Tyvar n -> Stv.mem n vs
-  | _ -> ty_all (tv_known vs) ty
+let rec tv_known s acc ty = match ty.ty_node with
+  | Tyvar n when not (Stv.mem n s) -> Stv.add n acc
+  | _ -> ty_fold (tv_known s) acc ty
 
 let create_tysymbol name args def =
   let add s v =
-    if Stv.mem v s then raise NonLinear;
+    if Stv.mem v s then raise (DuplicateTypeVar v);
     Stv.add v s
   in
   let s = List.fold_left add Stv.empty args in
-  let _ = match def with
-    | Some ty -> tv_known s ty || raise UnboundTypeVariable
-    | _ -> true
-  in
+  begin match def with
+    | Some ty ->
+        let ts = tv_known s Stv.empty ty in
+        if not (Stv.is_empty ts) then raise (UnboundTypeVars ts)
+    | _ -> ()
+  end;
   create_tysymbol name args def
 
-exception BadTypeArity
-
 let rec tv_inst m ty = match ty.ty_node with
   | Tyvar n -> Mtv.find n m
   | _ -> ty_map (tv_inst m) ty
 
 let ty_app s tl =
-  if List.length tl != List.length s.ts_args then raise BadTypeArity;
+  let tll = List.length tl in
+  let stl = List.length s.ts_args in
+  if tll != stl then raise (BadTypeArity (stl,tll));
   match s.ts_def with
     | Some ty ->
         let add m v t = Mtv.add v t m in

src/core/ty.mli

@@ -56,9 +56,9 @@ module Sty : Set.S with type elt = ty
 module Mty : Map.S with type key = ty
 module Hty : Hashtbl.S with type key = ty
 
-exception BadTypeArity
-exception NonLinear
-exception UnboundTypeVariable
+exception BadTypeArity of int * int
+exception DuplicateTypeVar of tvsymbol
+exception UnboundTypeVars of Stv.t
 
 val create_tysymbol : preid -> tvsymbol list -> ty option -> tysymbol
 

src/parser/typing.ml

@@ -673,9 +673,8 @@ let add_types dl th =
 		  in
 		  try
 		    ty_app ts (List.map apply tyl)
-		  with Ty.BadTypeArity ->
-		    error ~loc:(qloc q) (TypeArity (q, List.length ts.ts_args,
-						    List.length tyl))
+		  with Ty.BadTypeArity (tsal, tyll) ->
+		    error ~loc:(qloc q) (TypeArity (q, tsal, tyll))
 	    in
 	    create_tysymbol id vl (Some (apply ty))
 	| TDabstract | TDalgebraic _ ->
@@ -712,7 +711,7 @@ let add_types dl th =
 	    let param (_, t) = ty_of_dty (dty th' t) in
 	    let tyl = List.map param pl in
 	    Hashtbl.replace csymbols id.id loc;
-	    create_fconstr (id_user id.id loc) tyl ty
+	    create_fsymbol (id_user id.id loc) tyl ty
 	  in
 	  Talgebraic (List.map constructor cl)
     in

src/printer/why3.ml

@@ -53,9 +53,8 @@ let tv_set = ref Sid.empty
 (* type variables always start with a quote *)
 let print_tv fmt tv =
   tv_set := Sid.add tv.tv_name !tv_set;
-  let sanitize n = "'" ^ n in
-  let n = id_unique iprinter ~sanitizer:sanitize tv.tv_name in
-  fprintf fmt "%s" n
+  let sanitizer n = "'" ^ n in
+  fprintf fmt "%s" (id_unique iprinter ~sanitizer tv.tv_name)
 
 let forget_tvs () =
   Sid.iter (forget_id iprinter) !tv_set;
@@ -63,9 +62,8 @@ let forget_tvs () =
 
 (* logic variables always start with a lower case letter *)
 let print_vs fmt vs =
-  let sanitize = String.uncapitalize in
-  let n = id_unique iprinter ~sanitizer:sanitize vs.vs_name in
-  fprintf fmt "%s" n
+  let sanitizer = String.uncapitalize in
+  fprintf fmt "%s" (id_unique iprinter ~sanitizer vs.vs_name)
 
 let forget_var vs = forget_id iprinter vs.vs_name
 
@@ -73,11 +71,11 @@ let print_ts fmt ts =
   fprintf fmt "%s" (id_unique tprinter ts.ts_name)
 
 let print_ls fmt ls =
-  let n = if ls.ls_constr
-    then id_unique lprinter ~sanitizer:String.capitalize ls.ls_name
-    else id_unique lprinter ls.ls_name
-  in
-  fprintf fmt "%s" n
+  fprintf fmt "%s" (id_unique lprinter ls.ls_name)
+
+let print_cs fmt ls =
+  let sanitizer = String.capitalize in
+  fprintf fmt "%s" (id_unique lprinter ~sanitizer ls.ls_name)
 
 let print_pr fmt pr =
   fprintf fmt "%s" (id_unique pprinter pr.pr_name)
@@ -128,7 +126,7 @@ let rec print_pat drv fmt p = match p.pat_node with
     begin match query_ident drv cs.ls_name with
       | Syntax s -> syntax_arguments s (print_pat drv) fmt pl
       | _ -> fprintf fmt "%a%a"
-          print_ls cs (print_paren_r (print_pat drv)) pl
+          print_cs cs (print_paren_r (print_pat drv)) pl
     end
 
 let print_vsty drv fmt v =
@@ -252,7 +250,7 @@ and print_expr drv fmt = e_apply (print_term drv fmt) (print_fmla drv fmt)
 (** Declarations *)
 
 let print_constr drv fmt cs =
-  fprintf fmt "@[<hov 4>| %a%a@]" print_ls cs
+  fprintf fmt "@[<hov 4>| %a%a@]" print_cs cs
     (print_paren_l (print_ty drv)) cs.ls_args
 
 let print_ty_args fmt = function

src/transform/encoding_decorate.ml

@@ -153,12 +153,8 @@ let conv_ls tenv ls =
   else
     let preid = id_clone ls.ls_name in
     let tyl = List.map (conv_ty_neg tenv) ls.ls_args in
-    let ty_res = 
-      match ls.ls_value with
-        | None -> None
-        | Some ty ->
-            Some (conv_ty_pos tenv ty) in
-    create_lsymbol preid tyl ty_res false
+    let ty_res = Util.option_map (conv_ty_pos tenv) ls.ls_value in
+    create_lsymbol preid tyl ty_res
 
 
 let conv_ts tenv ts =