Remove unused AST constructor

Clean up ott grammar a bit

15 files changed, 2 insertions, 49 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index df657fcd..7a42950c 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -510,7 +510,6 @@ let unaux_constraint (NC_aux (nc, _)) = nc
 let rec map_exp_annot f (E_aux (exp, annot)) = E_aux (map_exp_annot_aux f exp, f annot)
 and map_exp_annot_aux f = function
   | E_block xs -> E_block (List.map (map_exp_annot f) xs)
-  | E_nondet xs -> E_nondet (List.map (map_exp_annot f) xs)
   | E_id id -> E_id id
   | E_ref id -> E_ref id
   | E_lit lit -> E_lit lit
@@ -937,7 +936,6 @@ let rec string_of_exp (E_aux (exp, _)) =
   | E_var (lexp, binding, exp) -> "var " ^ string_of_lexp lexp ^ " = " ^ string_of_exp binding ^ " in " ^ string_of_exp exp
   | E_internal_return exp -> "internal_return (" ^ string_of_exp exp ^ ")"
   | E_internal_plet (pat, exp, body) -> "internal_plet " ^ string_of_pat pat ^ " = " ^ string_of_exp exp ^ " in " ^ string_of_exp body
-  | E_nondet _ -> "NONDET"
   | E_internal_value v -> "INTERNAL_VALUE(" ^ Value.string_of_value v ^ ")"
 
 and string_of_measure (Measure_aux (m,_)) =
@@ -1530,7 +1528,6 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
   let wrap e_aux = E_aux (e_aux, annot) in
   let e_aux = match e_aux with
     | E_block exps -> E_block (List.map (subst id value) exps)
-    | E_nondet exps -> E_nondet (List.map (subst id value) exps)
     | E_id id' -> if Id.compare id id' = 0 then unaux_exp value else E_id id'
     | E_lit lit -> E_lit lit
     | E_cast (typ, exp) -> E_cast (typ, subst id value exp)
@@ -1752,7 +1749,6 @@ and locate_fpat : 'a. (l -> l) -> 'a fpat -> 'a fpat = fun f (FP_aux (FP_Fpat (i
 let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp = fun f (E_aux (e_aux, (l, annot))) ->
   let e_aux = match e_aux with
     | E_block exps -> E_block (List.map (locate f) exps)
-    | E_nondet exps -> E_nondet (List.map (locate f) exps)
     | E_id id -> E_id (locate_id f id)
     | E_lit lit -> E_lit (locate_lit f lit)
     | E_cast (typ, exp) -> E_cast (locate_typ f typ, locate f exp)
diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml
index 89a4ba82..201e43e7 100644
--- a/src/constant_propagation.ml
+++ b/src/constant_propagation.ml
@@ -387,9 +387,6 @@ let const_props defs ref_vars =
     | E_block es ->
        let es',assigns = threaded_map (const_prop_exp substs) assigns es in
        re (E_block es') assigns
-    | E_nondet es ->
-       let es',assigns = non_det_exp_list es in
-       re (E_nondet es') assigns
     | E_id id ->
        let env = Type_check.env_of_annot (l, annot) in
        (try
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 522faab7..8a61134c 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -365,7 +365,6 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) =
       (match to_ast_fexps false ctx exps with
       | Some(fexps) -> E_record(fexps)
       | None -> E_block(List.map (to_ast_exp ctx) exps))
-    | P.E_nondet(exps) -> E_nondet(List.map (to_ast_exp ctx) exps)
     | P.E_id(id) -> E_id(to_ast_id id)
     | P.E_ref(id) -> E_ref(to_ast_id id)
     | P.E_lit(lit) -> E_lit(to_ast_lit lit)
diff --git a/src/jib/anf.ml b/src/jib/anf.ml
index fdb4f941..5165904d 100644
--- a/src/jib/anf.ml
+++ b/src/jib/anf.ml
@@ -752,9 +752,5 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
      (* Sizeof nodes removed by sizeof rewriting pass *)
      raise (Reporting.err_unreachable l __POS__ "encountered E_constraint node when converting to ANF")
 
-  | E_nondet _ ->
-     (* We don't compile E_nondet nodes *)
-     raise (Reporting.err_unreachable l __POS__ "encountered E_nondet node when converting to ANF")
-
   | E_internal_return _ | E_internal_plet _ ->
      raise (Reporting.err_unreachable l __POS__ "encountered unexpected internal node when converting to ANF")
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 145d9046..93579420 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -545,11 +545,6 @@ let stop_at_false_assertions e =
              then E_aux (E_block es,ann), stop
              else E_aux (E_block (es@[dummy_value_of_typ typ']),ann), Some typ'
        end
-    | E_nondet es ->
-       let es,stops = List.split (List.map exp es) in
-       let stop = List.exists (function Some _ -> true | _ -> false) stops in
-       let stop = if stop then Some (typ_of_annot ann) else None in
-       E_aux (E_nondet es,ann), stop
     | E_cast (typ,e) -> let e,stop = exp e in
                         let stop = match stop with Some _ -> Some typ | None -> None in
                         E_aux (E_cast (typ,e),ann),stop
@@ -980,7 +975,6 @@ let split_defs all_errors splits env defs =
         let re e = E_aux (e,annot) in
         match e with
         | E_block es -> re (E_block (List.map map_exp es))
-        | E_nondet es -> re (E_nondet (List.map map_exp es))
         | E_id _
         | E_lit _
         | E_sizeof _
@@ -2048,9 +2042,6 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
             d, assigns, merge r r'
        in
        aux env assigns es
-    | E_nondet es ->
-       let _, assigns, r = non_det es in
-       (dempty, assigns, r)
     | E_id id ->
        begin 
          match Bindings.find id env.var_deps with
@@ -2536,8 +2527,7 @@ let rec sets_from_assert e =
    above. *)
 let rec find_set_assertions (E_aux (e,_)) =
   match e with
-  | E_block es
-  | E_nondet es ->
+  | E_block es ->
      List.fold_left merge_set_asserts_by_kid KBindings.empty (List.map find_set_assertions es)
   | E_cast (_,e) -> find_set_assertions e
   | E_let (LB_aux (LB_val (p,e1),_),e2) ->
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 5c3a5382..1d2c3534 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -247,7 +247,6 @@ and measure =
 and
 exp_aux =  (* Expression *)
    E_block of (exp) list (* block (parsing conflict with structs?) *)
- | E_nondet of (exp) list (* block that can evaluate the contained expressions in any ordering *)
  | E_id of id (* identifier *)
  | E_ref of id
  | E_deref of exp
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index f1128d7a..f0947315 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1825,7 +1825,6 @@ let doc_exp, doc_let =
            raise (report l __POS__ "E_field expression with no register or record type"))
     | E_block [] -> string "tt"
     | E_block exps -> raise (report l __POS__ "Blocks should have been removed till now.")
-    | E_nondet exps -> raise (report l __POS__ "Nondet blocks not supported.")
     | E_id id | E_ref id ->
        let env = env_of full_exp in
        let typ = typ_of full_exp in
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index fdb263e4..cf083eb5 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -815,7 +815,6 @@ let doc_exp_lem, doc_let_lem =
            raise (report l __POS__ "E_field expression with no register or record type"))
     | E_block [] -> string "()"
     | E_block exps -> raise (report l __POS__ "Blocks should have been removed till now.")
-    | E_nondet exps -> raise (report l __POS__ "Nondet blocks not supported.")
     | E_id id | E_ref id ->
        let env = env_of full_exp in
        let typ = typ_of full_exp in
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index da44645c..ae1f467c 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -387,7 +387,6 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
   | E_block [] -> string "()"
   | E_block exps ->
      group (lbrace ^^ nest 4 (hardline ^^ doc_block exps) ^^ hardline ^^ rbrace)
-  | E_nondet exps -> assert false
   (* This is mostly for the -convert option *)
   | E_app_infix (x, id, y) when Id.compare (mk_id "quot") id == 0 ->
      separate space [doc_atomic_exp x; string "/"; doc_atomic_exp y]
diff --git a/src/return_analysis.ml b/src/return_analysis.ml
index 256f97cf..789df2c5 100644
--- a/src/return_analysis.ml
+++ b/src/return_analysis.ml
@@ -69,8 +69,6 @@ let analyze_exp_returns exp =
           analyze last exp
        end
 
-    | E_nondet exps -> List.iter (analyze last) exps
-
     | E_id id ->
        if last then
          add_return annot
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 2573a135..24261861 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -140,7 +140,6 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match destruct_tannot (snd annot)
 | Some (env, typ, eff) ->
   let effsum = match e with
     | E_block es -> union_eff_exps es
-    | E_nondet es -> union_eff_exps es
     | E_id _ | E_ref _
     | E_lit _ -> eff
     | E_cast (_,e) -> effect_of e
@@ -271,7 +270,6 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) =
   let rewrite = rewriters.rewrite_exp rewriters in
   match exp with
   | E_block exps -> rewrap (E_block (List.map rewrite exps))
-  | E_nondet exps -> rewrap (E_nondet (List.map rewrite exps))
   | E_id _ | E_lit _  -> rewrap exp
   | E_cast (typ, exp) -> rewrap (E_cast (typ, rewrite exp))
   | E_app (id,exps) -> rewrap (E_app (id,List.map rewrite exps))
@@ -534,7 +532,6 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg =
   { e_block                  : 'exp list -> 'exp_aux
-  ; e_nondet                 : 'exp list -> 'exp_aux
   ; e_id                     : id -> 'exp_aux
   ; e_ref                    : id -> 'exp_aux
   ; e_lit                    : lit -> 'exp_aux
@@ -596,7 +593,6 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
 
 let rec fold_exp_aux alg = function
   | E_block es -> alg.e_block (List.map (fold_exp alg) es)
-  | E_nondet es -> alg.e_nondet (List.map (fold_exp alg) es)
   | E_id id -> alg.e_id id
   | E_ref id -> alg.e_ref id
   | E_lit lit -> alg.e_lit lit
@@ -680,7 +676,6 @@ let fold_function alg (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, fun
 
 let id_exp_alg =
   { e_block = (fun es -> E_block es)
-  ; e_nondet = (fun es -> E_nondet es)
   ; e_id = (fun id -> E_id id)
   ; e_ref = (fun id -> E_ref id)
   ; e_lit = (fun lit -> (E_lit lit))
@@ -776,7 +771,6 @@ let compute_exp_alg bot join =
   let join_list vs = List.fold_left join bot vs in
   let split_join f es = let (vs,es) = List.split es in (join_list vs, f es) in
   { e_block = split_join (fun es -> E_block es)
-  ; e_nondet = split_join (fun es -> E_nondet es)
   ; e_id = (fun id -> (bot, E_id id))
   ; e_ref = (fun id -> (bot, E_ref id))
   ; e_lit = (fun lit -> (bot, E_lit lit))
@@ -883,7 +877,6 @@ let pure_pat_alg bot join =
 let pure_exp_alg bot join =
   let join_list vs = List.fold_left join bot vs in
   { e_block = join_list
-  ; e_nondet = join_list
   ; e_id = (fun id -> bot)
   ; e_ref = (fun id -> bot)
   ; e_lit = (fun lit -> bot)
@@ -1004,10 +997,6 @@ let default_fold_exp f x (E_aux (e,ann) as exp) =
      let x,es = List.fold_left (fun (x,es) e ->
                     let x,e' = f x e in x,e'::es) (x,[]) es in
      x, re (E_block (List.rev es))
-  | E_nondet es ->
-     let x,es = List.fold_left (fun (x,es) e ->
-                    let x,e' = f x e in x,e'::es) (x,[]) es in
-     x, re (E_nondet (List.rev es))
   | E_id _
   | E_ref _
   | E_lit _ -> x, exp
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 878e0d15..77974f86 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -118,7 +118,6 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg = 
  { e_block                  : 'exp list -> 'exp_aux
- ; e_nondet                 : 'exp list -> 'exp_aux
  ; e_id                     : id -> 'exp_aux
  ; e_ref                    : id -> 'exp_aux
  ; e_lit                    : lit -> 'exp_aux
diff --git a/src/rewrites.ml b/src/rewrites.ml
index cbbd72d4..c94e2f57 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2333,7 +2333,6 @@ let rewrite_defs_letbind_effects env =
 
     match exp_aux with
     | E_block es -> failwith "E_block should have been removed till now"
-    | E_nondet _ -> failwith "E_nondet not supported"
     | E_id id -> k exp
     | E_ref id -> k exp
     | E_lit _ -> k exp
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 8afc985d..907c62a5 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -184,7 +184,7 @@ let rec pat_bindings consider_var bound used (P_aux(p,(_,tannot))) =
 let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.t * Nameset.t * Nameset.t) =
   let list_fv b n s es = List.fold_right (fun e (b,n,s) -> fv_of_exp consider_var b n s e) es (b,n,s) in
   match e with
-  | E_block es | Ast.E_nondet es | Ast.E_tuple es | Ast.E_vector es | Ast.E_list es ->
+  | E_block es | Ast.E_tuple es | Ast.E_vector es | Ast.E_list es ->
     list_fv bound used set es
   | E_id id ->
      let used = conditional_add_exp bound used id in
@@ -808,7 +808,6 @@ let nexp_subst_fns substs =
     let re e = E_aux (e,(l,s_tannot annot)) in
       match e with
       | E_block es -> re (E_block (List.map s_exp es))
-      | E_nondet es -> re (E_nondet (List.map s_exp es))
       | E_id _
       | E_ref _
       | E_lit _
diff --git a/src/type_check.ml b/src/type_check.ml
index 77263b4a..9c37f5c9 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -3629,8 +3629,6 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
      let rec last_typ = function [exp] -> typ_of exp | _ :: exps -> last_typ exps | [] -> unit_typ in
      let inferred_block = check_block l env exps None in
      annot_exp (E_block inferred_block) (last_typ inferred_block)
-  | E_nondet exps ->
-     annot_exp (E_nondet (List.map (fun exp -> crule check_exp env exp unit_typ) exps)) unit_typ
   | E_id v ->
      begin
        match Env.lookup_id v env with
@@ -4329,9 +4327,6 @@ and propagate_exp_effect_aux = function
   | E_block xs ->
      let p_xs = List.map propagate_exp_effect xs in
      E_block p_xs, collect_effects p_xs
-  | E_nondet xs ->
-     let p_xs = List.map propagate_exp_effect xs in
-     E_nondet p_xs, collect_effects p_xs
   | E_id id -> E_id id, no_effect
   | E_ref id -> E_ref id, no_effect
   | E_lit lit -> E_lit lit, no_effect