Remove constraint synonyms

They weren't needed for ASL parser like I thought they would be, and
they increase the complexity of dealing with constraints throughout
Sail, so just remove them.

Also fix some compiler warnings

15 files changed, 10 insertions, 86 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index d61c96ed..14638b88 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -387,8 +387,6 @@ let rec nc_negate (NC_aux (nc, l)) =
   | NC_set (kid, [int]) -> nc_neq (nvar kid) (nconstant int)
   | NC_set (kid, int :: ints) ->
      mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_set (kid, ints)))))
-  | NC_app _ ->
-     raise (Reporting.err_unreachable l __POS__ "tried to negate constraint with unexpanded synonym")
 
 let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown)
 
@@ -581,8 +579,8 @@ let def_loc = function
   | DEF_reg_dec (DEC_aux (_, (l, _)))
   | DEF_fixity (_, _, Id_aux (_, l))
   | DEF_overload (Id_aux (_, l), _) -> l
-  | DEF_constraint (Id_aux (_, l), _, _) -> l
   | DEF_internal_mutrec _ -> Parse_ast.Unknown
+  | DEF_pragma (_, _, l) -> l
 
 let string_of_id = function
   | Id_aux (Id v, _) -> v
@@ -696,8 +694,6 @@ and string_of_n_constraint = function
      "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")"
   | NC_aux (NC_set (kid, ns), _) ->
      string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}"
-  | NC_aux (NC_app (id, nexps), _) ->
-     "where " ^ string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_nexp nexps ^ ")"
   | NC_aux (NC_true, _) -> "true"
   | NC_aux (NC_false, _) -> "false"
 
@@ -954,8 +950,6 @@ module NC = struct
     | NC_or (nc1,nc2), NC_or (nc3,nc4)
     | NC_and (nc1,nc2), NC_and (nc3,nc4)
       -> lex_ord compare compare nc1 nc3 nc2 nc4
-    | NC_app (id1, nexps1), NC_app (id2, nexps2)
-      -> lex_ord (Id.compare) (Util.compare_list Nexp.compare) id1 id2 nexps1 nexps2
     | NC_true, NC_true
     | NC_false, NC_false
       -> 0
@@ -966,7 +960,6 @@ module NC = struct
     | NC_set _, _ -> -1        | _, NC_set _ -> 1
     | NC_or _, _ -> -1         | _, NC_or _ -> 1
     | NC_and _, _ -> -1        | _, NC_and _ -> 1
-    | NC_app _, _ -> -1        | _, NC_app _ -> 1
     | NC_true, _ -> -1         | _, NC_true -> 1
 end
 
@@ -1152,8 +1145,6 @@ let rec tyvars_of_constraint (NC_aux (nc, _)) =
   | NC_or (nc1, nc2)
   | NC_and (nc1, nc2) ->
      KidSet.union (tyvars_of_constraint nc1) (tyvars_of_constraint nc2)
-  | NC_app (id, nexps) ->
-     List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_nexp nexps)
   | NC_true
   | NC_false -> KidSet.empty
 
@@ -1421,7 +1412,6 @@ let rec locate_nc f (NC_aux (nc_aux, l)) =
     | NC_set (kid, nums) -> NC_set (locate_kid f kid, nums)
     | NC_or (nc1, nc2) -> NC_or (locate_nc f nc1, locate_nc f nc2)
     | NC_and (nc1, nc2) -> NC_and (locate_nc f nc1, locate_nc f nc2)
-    | NC_app (id, nexps) -> NC_app (id, List.map (locate_nexp f) nexps)
     | NC_true -> NC_true
     | NC_false -> NC_false
   in
@@ -1596,7 +1586,6 @@ and nc_subst_nexp_aux l sv subst = function
      else set_nc
   | NC_or (nc1, nc2) -> NC_or (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
   | NC_and (nc1, nc2) -> NC_and (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
-  | NC_app (id, nexps) -> NC_app (id, List.map (nexp_subst sv subst) nexps)
   | NC_false -> NC_false
   | NC_true -> NC_true
 
diff --git a/src/initial_check.ml b/src/initial_check.ml
index bd32a8e3..b442ae97 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -375,9 +375,6 @@ and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint)
                 NC_or (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2)
              | Parse_ast.NC_and (nc1, nc2) ->
                 NC_and (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2)
-             | Parse_ast.NC_app (id, typs) ->
-                let nexps = List.map (to_ast_nexp k_env) typs in
-                NC_app (to_ast_id id, nexps)
              | Parse_ast.NC_true -> NC_true
              | Parse_ast.NC_false -> NC_false
     ), l)
@@ -901,11 +898,6 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out
   | Parse_ast.DEF_reg_dec(dec) ->
      let d = to_ast_dec envs dec in
      ((Finished(DEF_reg_dec(d))),envs),partial_defs
-  | Parse_ast.DEF_constraint (id, kids, nc) ->
-     let id = to_ast_id id in
-     let kids = List.map to_ast_var kids in
-     let nc = to_ast_nexp_constraint k_env nc in
-     ((Finished (DEF_constraint (id, kids, nc))), envs), partial_defs
   | Parse_ast.DEF_pragma (pragma, arg, l) ->
      ((Finished(DEF_pragma (pragma, arg, l))), envs), partial_defs
   | Parse_ast.DEF_internal_mutrec _ ->
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 975e8017..0d7fd6e5 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -2113,6 +2113,7 @@ let split_defs all_errors splits defs =
       | DEF_reg_dec _
       | DEF_overload _
       | DEF_fixity _
+      | DEF_pragma _
       | DEF_internal_mutrec _
         -> [d]
       | DEF_fundef fd -> [DEF_fundef (map_fundef fd)]
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index ddff51ea..c50977ed 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -177,7 +177,6 @@ n_constraint_aux =  (* constraint over kind $_$ *)
  | NC_set of kid * (Big_int.num) list
  | NC_or of n_constraint * n_constraint
  | NC_and of n_constraint * n_constraint
- | NC_app of id * atyp list
  | NC_true
  | NC_false
 
@@ -568,7 +567,6 @@ def =  (* Top-level definition *)
  | DEF_scattered of scattered_def (* scattered definition *)
  | DEF_reg_dec of dec_spec (* register declaration *)
  | DEF_pragma of string * string * l
- | DEF_constraint of id * kid list * n_constraint
  | DEF_internal_mutrec of fundef list
 
 
diff --git a/src/parser.mly b/src/parser.mly
index 8287060c..cd655217 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -337,8 +337,6 @@ nc_and:
     { $1 }
 
 atomic_nc:
-  | Where id Lparen typ_list Rparen
-    { mk_nc (NC_app ($2, $4)) $startpos $endpos }
   | True
     { mk_nc NC_true $startpos $endpos }
   | False
@@ -1454,8 +1452,6 @@ def:
     { DEF_kind (KD_aux (KD_nabbrev (K_aux (K_kind [BK_aux (BK_int, loc $startpos($1) $endpos($1))],
 					   loc $startpos($1) $endpos($1)), $2, mk_namesectn, $4),
 			loc $startpos $endpos)) }
-  | Constraint id Lparen kid_list Rparen Eq nc
-    { DEF_constraint ($2, $4, $7) }
   | Mutual Lcurly fun_def_list Rcurly
     { DEF_internal_mutrec $3 }
   | Pragma
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 6825259c..1fb35158 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -207,7 +207,6 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
        separate space [nexp_constraint nc1; string "&"; nexp_constraint nc2]
     | NC_true -> string "true"
     | NC_false -> string "false"
-    | NC_app (id, args) -> doc_id id ^^ parens (separate_map (comma ^^ space) nexp args)
 
   (* expose doc_typ, doc_atomic_typ, doc_nexp and doc_nexp_constraint *)
   in typ, atomic_typ, nexp, nexp_constraint
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index cfffb8c9..630d5b1e 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1686,7 +1686,6 @@ let types_used_with_generic_eq defs =
     | DEF_fixity _
     | DEF_overload _
     | DEF_default _
-    | DEF_constraint _
     | DEF_pragma _
     | DEF_reg_dec _
       -> IdSet.empty
@@ -2284,6 +2283,7 @@ let rec doc_def unimplemented generic_eq_types def =
   | DEF_scattered sdef -> failwith "doc_def: shoulnd't have DEF_scattered at this point"
   | DEF_mapdef (MD_aux (_, (l,_))) -> unreachable l __POS__ "Coq doesn't support mappings"
   | DEF_kind _ -> empty
+  | DEF_pragma _ -> empty
 
 let find_exc_typ defs =
   let is_exc_typ_def = function
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 779d81f8..53b703bf 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1420,6 +1420,7 @@ let rec doc_def_lem def =
 
   | DEF_kind _ -> empty
   | DEF_mapdef (MD_aux (_, (l, _))) -> unreachable l __POS__ "Lem doesn't support mappings"
+  | DEF_pragma _ -> empty
 
 let find_exc_typ defs =
   let is_exc_typ_def = function
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 53e77df2..fe533f00 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -125,7 +125,6 @@ let doc_nc nc =
     | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2
     | NC_set (kid, ints) ->
        separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)]
-    | NC_app (id, nexps) -> string "where" ^^ space ^^ doc_id id ^^ parens (separate_map (comma ^^ space) doc_nexp nexps)
     | _ -> nc0 ~parenthesize:true nc
   and nc0 ?parenthesize:(parenthesize=false) (NC_aux (nc_aux, _) as nc) =
     (* Rather than parens (nc0 x) we use nc0 ~parenthesize:true x, because if
@@ -640,8 +639,6 @@ let rec doc_def def = group (match def with
   | DEF_fixity (prec, n, id) ->
      fixities := Bindings.add id (prec, Big_int.to_int n) !fixities;
      separate space [doc_prec prec; doc_int n; doc_id id]
-  | DEF_constraint (id, kids, nc) ->
-     separate space [string "constraint"; doc_id id; parens (separate_map (comma ^^ space) doc_kid kids); equals; doc_nc nc]
   | DEF_overload (id, ids) ->
      separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
   ) ^^ hardline
diff --git a/src/rewriter.ml b/src/rewriter.ml
index cf547307..082d9850 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -359,7 +359,6 @@ let rewrite_def rewriters d = match d with
   | DEF_internal_mutrec fdefs -> DEF_internal_mutrec (List.map (rewriters.rewrite_fun rewriters) fdefs)
   | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind)
   | DEF_pragma (pragma, arg, l) -> DEF_pragma (pragma, arg, l)
-  | DEF_constraint _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_constraint survived to rewritter")
   | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewritter")
 
 let rewrite_defs_base rewriters (Defs defs) =
diff --git a/src/sail.ml b/src/sail.ml
index 417d3ef4..b9a18417 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -247,9 +247,6 @@ let options = Arg.align ([
   ( "-dprofile",
     Arg.Set Profile.opt_profile,
     " (debug) provides basic profiling information for rewriting passes within Sail");
-  ( "-Xconstraint_synonyms",
-    Arg.Set Type_check.opt_constraint_synonyms,
-    " (extension) allow constraint synonyms");
   ( "-v",
     Arg.Set opt_print_version,
     " print version");
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index c858754e..fa68c6f2 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -282,6 +282,10 @@ and fv_of_lexp consider_var bound used set (LEXP_aux(lexp,(_,tannot))) =
         (fun e (b,u,s) ->
           fv_of_exp consider_var b u s e) args (bound,used,set) in
     bound,Nameset.add (string_of_id id) used,set
+  | LEXP_vector_concat(args) ->
+     List.fold_right
+       (fun e (b,u,s) ->
+         fv_of_lexp consider_var b u s e) args (bound,used,set)
   | LEXP_field(lexp,_) -> fv_of_lexp consider_var bound used set lexp
   | LEXP_vector(lexp,exp) ->
     let bound_l,used,set = fv_of_lexp consider_var bound used set lexp in
@@ -486,8 +490,7 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function
      List.fold_left Nameset.union Nameset.empty (List.map snd fvs)
   | DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef
   | DEF_reg_dec rdec -> fv_of_rd consider_var rdec
-  | DEF_constraint (id, _, _) ->
-     raise (Reporting.err_unreachable (id_loc id) __POS__ "Constraint should be re-written")
+  | DEF_pragma _ -> mt,mt
 
 let group_defs consider_scatter_as_one (Ast.Defs defs) =
   List.map (fun d -> (fv_of_def false consider_scatter_as_one defs d,d)) defs
diff --git a/src/type_check.ml b/src/type_check.ml
index 81f5fe6d..866aa071 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -69,10 +69,6 @@ let opt_no_effects = ref false
    assignments in l-expressions *)
 let opt_no_lexp_bounds_check = ref false
 
-(* opt_constraint_synonyms allows constraint synonyms as toplevel
-   definitions *)
-let opt_constraint_synonyms = ref false
-
 (* opt_expand_valspec expands typedefs in valspecs during type check.
    We prefer not to do it for latex output but it is otherwise a good idea. *)
 let opt_expand_valspec = ref true
@@ -171,7 +167,6 @@ and strip_n_constraint_aux = function
   | NC_set (kid, nums) -> NC_set (strip_kid kid, nums)
   | NC_or (nc1, nc2) -> NC_or (strip_n_constraint nc1, strip_n_constraint nc2)
   | NC_and (nc1, nc2) -> NC_and (strip_n_constraint nc1, strip_n_constraint nc2)
-  | NC_app (id, nexps) -> NC_app (strip_id id, List.map strip_nexp nexps)
   | NC_true -> NC_true
   | NC_false -> NC_false
 and strip_n_constraint = function
@@ -287,11 +282,7 @@ module Env : sig
   val polymorphic_undefineds : t -> bool
   val lookup_id : ?raw:bool -> id -> t -> typ lvar
   val fresh_kid : ?kid:kid -> t -> kid
-
   val expand_synonyms : t -> typ -> typ
-  val expand_constraint_synonyms : t -> n_constraint -> n_constraint
-  val expand_typquant_synonyms : t -> typquant -> typquant
-
   val canonicalize : t -> typ -> typ
   val base_typ_of : t -> typ -> typ
   val add_smt_op : id -> string -> t -> t
@@ -490,27 +481,6 @@ end = struct
     then ()
     else typ_error (id_loc id) ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id)
 
-  let rec expand_constraint_synonyms env (NC_aux (nc_aux, l) as nc) =
-    let expand = expand_constraint_synonyms env in
-    match nc_aux with
-    | NC_app (id, nexps) ->
-       begin
-         try
-           let kids, nc = Bindings.find id env.constraint_synonyms in
-           let nc = List.fold_left2 (fun nc kid nexp -> nc_subst_nexp kid (unaux_nexp nexp) nc) nc kids nexps in
-           expand nc
-         with Not_found -> typ_error l ("Could not expand constraint synonym in " ^ string_of_n_constraint nc)
-       end
-    | NC_and (nc1, nc2) -> NC_aux (NC_and (expand nc1, expand nc2), l)
-    | NC_or (nc1, nc2) -> NC_aux (NC_or (expand nc1, expand nc2), l)
-    | NC_true | NC_false | NC_set _ | NC_equal _ | NC_not_equal _ | NC_bounded_le _ | NC_bounded_ge _  -> nc
-
-  let expand_quant_item_synonyms env = function
-    | QI_aux (QI_id kopt, l) -> QI_aux (QI_id kopt, l)
-    | QI_aux (QI_const nc, l) -> QI_aux (QI_const (expand_constraint_synonyms env nc), l)
-
-  let expand_typquant_synonyms env = quant_map_items (expand_quant_item_synonyms env)
-
   let rec expand_synonyms env (Typ_aux (typ, l) as t) =
     match typ with
     | Typ_internal_unknown -> Typ_aux (Typ_internal_unknown, l)
@@ -718,11 +688,6 @@ end = struct
       end
     | NC_or (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2
     | NC_and (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2
-    | NC_app (id, nexps) ->
-       if not (Bindings.mem id env.constraint_synonyms) then
-         typ_error l ("Constraint synonym " ^ string_of_id id ^ " is not defined")
-       else ();
-       List.iter (wf_nexp ~exs:exs env) nexps
     | NC_true | NC_false -> ()
 
   let counter = ref 0
@@ -783,7 +748,6 @@ end = struct
           forall 'n, 'n >= 2. (int('n), foo) -> bar
           this enforces the invariant that all things on the left of functions are 'base types' (i.e. without existentials)
         *)
-       let typq = expand_typquant_synonyms env typq in
        let base_args = List.map (destruct_exist env) arg_typs in
        let existential_arg typq = function
          | None -> typq
@@ -1063,7 +1027,6 @@ end = struct
     match nc_aux with
     | NC_true -> env
     | _ ->
-       let constr = expand_constraint_synonyms env constr in
        typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint constr));
        { env with constraints = constr :: env.constraints }
 
@@ -1162,8 +1125,7 @@ let add_typquant l (quant : typquant) (env : Env.t) : Env.t =
   | TypQ_aux (TypQ_tq quants, _) -> List.fold_left add_quant_item env quants
 
 let expand_bind_synonyms l env (typq, typ) =
-  Env.expand_typquant_synonyms env typq, Env.expand_synonyms (add_typquant l typq env) typ
-
+  typq, Env.expand_synonyms (add_typquant l typq env) typ
 
 (* Create vectors with the default order from the environment *)
 
@@ -1335,7 +1297,6 @@ let rec nc_constraint env var_of (NC_aux (nc, l)) =
                     (List.map (fun i -> Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant i)) ints)
   | NC_or (nc1, nc2) -> Constraint.disj (nc_constraint env var_of nc1) (nc_constraint env var_of nc2)
   | NC_and (nc1, nc2) -> Constraint.conj (nc_constraint env var_of nc1) (nc_constraint env var_of nc2)
-  | NC_app (id, nexps) -> raise (Reporting.err_unreachable l __POS__ "constraint synonym reached smt generation")
   | NC_false -> Constraint.literal false
   | NC_true -> Constraint.literal true
 
@@ -4527,10 +4488,6 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
   | DEF_fixity (prec, n, op) -> [DEF_fixity (prec, n, op)], env
   | DEF_fundef fdef -> check_fundef env fdef
   | DEF_mapdef mdef -> check_mapdef env mdef
-  | DEF_constraint (id, kids, nc) when !opt_constraint_synonyms ->
-     [], Env.add_constraint_synonym id kids nc env
-  | DEF_constraint (id, _, _) ->
-     typ_error (id_loc id) "Use -Xconstraint_synonyms to enable constraint synonyms"
   | DEF_internal_mutrec fdefs ->
      let defs = List.concat (List.map (fun fdef -> fst (check_fundef env fdef)) fdefs) in
      let split_fundef (defs, fdefs) def = match def with
diff --git a/src/type_check.mli b/src/type_check.mli
index dc1cfe97..1081af08 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -67,10 +67,6 @@ val opt_no_effects : bool ref
    assignments in l-expressions. *)
 val opt_no_lexp_bounds_check : bool ref
 
-(** [opt_constraint_synonyms] allows constraint synonyms as toplevel
-   definitions *)
-val opt_constraint_synonyms : bool ref
-
 (** opt_expand_valspec expands typedefs in valspecs during type check.
    We prefer not to do it for latex output but it is otherwise a good idea. *)
 val opt_expand_valspec : bool ref
diff --git a/src/type_error.ml b/src/type_error.ml
index a49334ac..7551970f 100644
--- a/src/type_error.ml
+++ b/src/type_error.ml
@@ -96,7 +96,6 @@ and nc_subst_nexp_aux l sv subst = function
      else set_nc
   | NC_or (nc1, nc2) -> NC_or (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
   | NC_and (nc1, nc2) -> NC_and (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
-  | NC_app (id, nexps) -> NC_app (id, List.map (nexp_subst sv subst) nexps)
   | NC_false -> NC_false
   | NC_true -> NC_true