Remove sequential code again

3 files changed, 29 insertions, 175 deletions

diff --git a/mips/mips_extras_sequential.lem b/mips/mips_extras_sequential.lem
deleted file mode 100644
index 8de5aec3..00000000
--- a/mips/mips_extras_sequential.lem
+++ /dev/null
@@ -1,126 +0,0 @@
-open import Pervasives
-open import Pervasives_extra
-open import Sail_instr_kinds
-open import Sail_values
-open import Sail_operators
-open import State_monad
-open import State
-
-val MEMr             : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monadS 'regval 'b 'e
-val MEMr_reserve     : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monadS 'regval 'b 'e
-val MEMr_tag         : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monadS 'regval (bool * 'b) 'e
-val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monadS 'regval (bool * 'b) 'e
-
-let MEMr addr size             = read_memS Read_plain addr size
-let MEMr_reserve addr size     = read_memS Read_reserve addr size
-
-val read_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> monadS 'regval bool 'e
-let read_tag_bool addr =
-  read_tagS addr >>$= fun t ->
-  maybe_failS "read_tag_bool" (bool_of_bitU t)
-
-val write_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> bool -> monadS 'regval unit 'e
-let write_tag_bool addr t = write_tagS addr (bitU_of_bool t) >>$= fun _ -> returnS ()
-
-let MEMr_tag addr size =
-  read_memS Read_plain addr size >>$= fun v ->
-  read_tag_bool addr >>$= fun t ->
-  returnS (t, v)
-
-let MEMr_tag_reserve addr size =
-  read_memS Read_plain addr size >>$= fun v ->
-  read_tag_bool addr >>$= fun t ->
-  returnS (t, v)
-
-
-val MEMea                 : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monadS 'regval unit 'e
-val MEMea_conditional     : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monadS 'regval unit 'e
-val MEMea_tag             : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monadS 'regval unit 'e
-val MEMea_tag_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monadS 'regval unit 'e
-
-let MEMea addr size                 = write_mem_eaS Write_plain addr (nat_of_int size)
-let MEMea_conditional addr size     = write_mem_eaS Write_conditional addr (nat_of_int size)
-
-let MEMea_tag addr size             = write_mem_eaS Write_plain addr (nat_of_int size)
-let MEMea_tag_conditional addr size = write_mem_eaS Write_conditional addr (nat_of_int size)
-
-
-val MEMval                 : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monadS 'regval unit 'e
-val MEMval_conditional     : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monadS 'regval bool 'e
-val MEMval_tag             : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monadS 'regval unit 'e
-val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monadS 'regval bool 'e
-
-let MEMval _ size v                      = write_mem_valS v >>$= fun _ -> returnS ()
-let MEMval_conditional _ size v          = write_mem_valS v >>$= fun b -> returnS (if b then true else false)
-let MEMval_tag addr size t v             = write_mem_valS v >>$= fun _ -> write_tag_bool addr t >>$= fun _ -> returnS ()
-let MEMval_tag_conditional addr size t v = write_mem_valS v >>$= fun b -> write_tag_bool addr t >>$= fun _ -> returnS (if b then true else false)
-
-val MEM_sync  : forall 'regval 'e. unit -> monadS 'regval unit 'e
-
-let MEM_sync () = returnS ()  (*barrier Barrier_MIPS_SYNC*)
-
-(* Some wrappers copied from aarch64_extras *)
-(* TODO: Harmonise into a common library *)
-
-let get_slice_int_bl len n lo =
-  (* TODO: Is this the intended behaviour? *)
-  let hi = lo + len - 1 in
-  let bs = bools_of_int (hi + 1) n in
-  subrange_list false bs hi lo
-
-val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
-let get_slice_int len n lo = of_bools (get_slice_int_bl len n lo)
-
-let write_ram _ size _ addr data =
-  MEMea addr size >>$
-  MEMval addr size data
-
-let read_ram _ size _ addr = MEMr addr size
-
-let inline reg_deref = read_regS
-
-let string_of_bits bs = string_of_bv (bits_of bs)
-let string_of_int = show
-
-let _sign_extend bits len = maybe_failwith (of_bits (exts_bv len bits))
-let _zero_extend bits len = maybe_failwith (of_bits (extz_bv len bits))
-
-let shift_bits_left v n =
-  let r = Maybe.bind (unsigned n) (fun n -> of_bits (shiftl_bv v n)) in
-  maybe_failS "shift_bits_left" r
-let shift_bits_right v n =
-  let r = Maybe.bind (unsigned n) (fun n -> of_bits (shiftr_bv v n)) in
-  maybe_failS "shift_bits_right" r
-let shift_bits_right_arith v n =
-  let r = Maybe.bind (unsigned n) (fun n -> of_bits (arith_shiftr_bv v n)) in
-  maybe_failS "shift_bits_right_arith" r
-
-(* Use constants for undefined values for now *)
-let internal_pick vs = returnS (head vs)
-let undefined_bool = undefined_boolS
-let undefined_string () = returnS ""
-let undefined_unit () = returnS ()
-let undefined_int () = returnS (0:ii)
-val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monadS 'rv (list 'a) 'e
-let undefined_vector len u = returnS (repeat [u] len)
-val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monadS 'rv 'a 'e
-let undefined_bitvector len = returnS (of_bools (repeat [false] len))
-val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monadS 'rv 'a 'e
-let undefined_bits = undefined_bitvector
-let undefined_bit () = returnS B0
-let undefined_real () = returnS (realFromFrac 0 1)
-let undefined_range i j = returnS i
-let undefined_atom i = returnS i
-let undefined_nat () = returnS (0:ii)
-
-let skip () = returnS ()
-
-val elf_entry : unit -> integer
-let elf_entry () = 0
-declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry`
-
-let print_bits msg bs = prerr_endline (msg ^ (string_of_bits bs))
-
-val get_time_ns : unit -> integer
-let get_time_ns () = 0
-declare ocaml target_rep function get_time_ns = `(fun () -> Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())))`
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 36794348..c872d420 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -62,8 +62,6 @@ open Pretty_print_common
 let opt_sequential = ref false
 let opt_mwords = ref false
 
-let appendS str = if !opt_sequential then str ^ "S" else str
-
 type context = {
   early_ret : bool;
   bound_nexps : NexpSet.t;
@@ -551,7 +549,7 @@ let doc_exp_lem, doc_let_lem =
     let wrap_parens doc = if aexp_needed then parens (doc) else doc in
     let liftR doc =
       if ctxt.early_ret && effectful (effect_of full_exp)
-      then wrap_parens (separate space [string (appendS "liftR"); parens (doc)])
+      then wrap_parens (separate space [string "liftR"; parens (doc)])
       else wrap_parens doc in
     match e with
     | E_assign((LEXP_aux(le_act,tannot) as le), e) ->
@@ -569,13 +567,13 @@ let doc_exp_lem, doc_let_lem =
                    underscore ^^
                    doc_id_lem id in
                  liftR ((prefix 2 1)
-                   (string (appendS "write_reg_field_range"))
+                   (string "write_reg_field_range")
                    (align (doc_lexp_deref_lem ctxt le ^/^
                       field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e)))
             | _ ->
                let deref = doc_lexp_deref_lem ctxt le in
                liftR ((prefix 2 1)
-                 (string (appendS "write_reg_range"))
+                 (string "write_reg_range")
                  (align (deref ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
         | LEXP_vector (le,e2) ->
            (match le with
@@ -606,13 +604,13 @@ let doc_exp_lem, doc_let_lem =
             dot ^^
             string "set_field"*) in
            liftR ((prefix 2 1)
-             (string (appendS "write_reg_field"))
+             (string "write_reg_field")
              (doc_lexp_deref_lem ctxt le ^^ space ^^
                 field_ref ^/^ expY e))
         | LEXP_deref re ->
-           liftR ((prefix 2 1) (string (appendS "write_reg")) (expY re ^/^ expY e))
+           liftR ((prefix 2 1) (string "write_reg") (expY re ^/^ expY e))
         | _ ->
-           liftR ((prefix 2 1) (string (appendS "write_reg")) (doc_lexp_deref_lem ctxt le ^/^ expY e)))
+           liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem ctxt le ^/^ expY e)))
     | E_vector_append(le,re) ->
       raise (Reporting_basic.err_unreachable l
         "E_vector_append should have been rewritten before pretty-printing")
@@ -629,8 +627,7 @@ let doc_exp_lem, doc_let_lem =
        | Id_aux (Id "None", _) as none -> doc_id_lem_ctor none
        | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _)
          when effectful (effect_of full_exp) ->
-          let suffix = if !opt_sequential then "S" else "M" in
-          let call = doc_id_lem (append_id f suffix) in
+          let call = doc_id_lem (append_id f "M") in
           wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args)))
        (* temporary hack to make the loop body a function of the temporary variables *)
        | Id_aux (Id "foreach", _) ->
@@ -652,11 +649,7 @@ let doc_exp_lem, doc_let_lem =
                     parens (separate space [string "integerNegate"; expY exp3])
                  | _ -> expY exp3
                in
-               let combinator =
-                 if effectful (effect_of body)
-                 then if !opt_sequential then "foreachS" else "foreachM"
-                 else "foreach"
-               in
+               let combinator = if effectful (effect_of body) then "foreachM" else "foreach" in
                let indices_pp = parens (separate space [string "index_list"; expY exp1; expY exp2; step]) in
                let used_vars_body = find_e_ids body in
                let body_lambda =
@@ -689,13 +682,12 @@ let doc_exp_lem, doc_let_lem =
             match args with
             | [cond; varstuple; body] ->
                let return (E_aux (e, a)) = E_aux (E_internal_return (E_aux (e, a)), a) in
-               let monad_suffix = if !opt_sequential then "S" else "M" in
                let csuffix, cond, body =
                  match effectful (effect_of cond), effectful (effect_of body) with
                    | false, false -> "", cond, body
-                   | false, true  -> monad_suffix, return cond, body
-                   | true,  false -> monad_suffix, cond, return body
-                   | true,  true  -> monad_suffix, cond, body
+                   | false, true  -> "M", return cond, body
+                   | true,  false -> "M", cond, return body
+                   | true,  true  -> "M", cond, body
                in
                let used_vars_body = find_e_ids body in
                let lambda =
@@ -726,7 +718,7 @@ let doc_exp_lem, doc_let_lem =
           begin
             match args with
             | [exp] ->
-               let epp = separate space [string (appendS "early_return"); expY exp] in
+               let epp = separate space [string "early_return"; expY exp] in
                let aexp_needed, tepp =
                  if contains_t_pp_var ctxt (typ_of exp) ||
                     contains_t_pp_var ctxt (typ_of full_exp) then
@@ -795,7 +787,7 @@ let doc_exp_lem, doc_let_lem =
        let eff = effect_of full_exp in
        let base_typ = Env.base_typ_of env typ in
        if has_effect eff BE_rreg then
-         let epp = separate space [string (appendS "read_reg");doc_id_lem (append_id id "_ref")] in
+         let epp = separate space [string "read_reg";doc_id_lem (append_id id "_ref")] in
          if is_bitvector_typ base_typ
          then liftR (parens (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env true base_typ)))))
          else liftR epp
@@ -870,7 +862,7 @@ let doc_exp_lem, doc_let_lem =
                  (string "end")))
     | E_try (e, pexps) ->
        if effectful (effect_of e) then
-         let try_catch = if ctxt.early_ret then appendS "try_catchR" else "try_catch" in
+         let try_catch = if ctxt.early_ret then "try_catchR" else "try_catch" in
          wrap_parens
            (group ((separate space [string try_catch; expY e; string "(function "]) ^/^
                    (separate_map (break 1) (doc_case ctxt) pexps) ^/^
@@ -878,10 +870,10 @@ let doc_exp_lem, doc_let_lem =
        else
          raise (Reporting_basic.err_todo l "Warning: try-block around pure expression")
     | E_throw e ->
-       align (liftR (separate space [string (appendS "throw"); expY e]))
-    | E_exit e -> liftR (separate space [string (appendS "exit"); expY e])
+       align (liftR (separate space [string "throw"; expY e]))
+    | E_exit e -> liftR (separate space [string "exit"; expY e])
     | E_assert (e1,e2) ->
-       align (liftR (separate space [string (appendS "assert_exp"); expY e1; expY e2]))
+       align (liftR (separate space [string "assert_exp"; expY e1; expY e2]))
     | E_app_infix (e1,id,e2) ->
        expV aexp_needed (E_aux (E_app (deinfix id, [e1; e2]), (l, annot)))
     | E_var(lexp, eq_exp, in_exp) ->
@@ -889,28 +881,26 @@ let doc_exp_lem, doc_let_lem =
     | E_internal_plet (pat,e1,e2) ->
        let epp =
          let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in
-         let bind_pp = string (if !opt_sequential then ">>$=" else ">>=") in
-         let seq_pp = string (if !opt_sequential then ">>$" else ">>") in
          let middle =
            match fst (untyp_pat pat) with
-           | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> seq_pp
+           | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ">>"
            | P_aux (P_tup _, _)
              when not (IdSet.mem (mk_id "varstup") (find_e_ids e2)) ->
               (* Work around indentation issues in Lem when translating
                  tuple patterns to Isabelle *)
               separate space
-                [bind_pp; string "fun varstup -> let";
+                [string ">>= fun varstup -> let";
                  doc_pat_lem ctxt true pat;
                  string "= varstup in"]
            | _ ->
-              separate space [bind_pp; string "fun";
+              separate space [string ">>= fun";
                               doc_pat_lem ctxt true pat; arrow]
          in
          infix 0 1 middle (expV b e1) (expN e2)
        in
        wrap_parens (align epp)
     | E_internal_return (e1) ->
-       wrap_parens (align (separate space [string (appendS "return"); expY e1]))
+       wrap_parens (align (separate space [string "return"; expY e1]))
     | E_sizeof nexp ->
       (match nexp_simp nexp with
         | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem (L_aux (L_num i, l))
@@ -918,7 +908,6 @@ let doc_exp_lem, doc_let_lem =
           raise (Reporting_basic.err_unreachable l
             "pretty-printing non-constant sizeof expressions to Lem not supported"))
     | E_return r ->
-      (* let ret_monad = if !opt_sequential then " : MR regstate" else " : MR" in *)
       let ta =
         if contains_t_pp_var ctxt (typ_of full_exp) || contains_t_pp_var ctxt (typ_of r)
         then empty
@@ -926,7 +915,7 @@ let doc_exp_lem, doc_let_lem =
           [string ": MR";
           parens (doc_typ_lem (typ_of full_exp));
           parens (doc_typ_lem (typ_of r))] in
-      align (parens (string (appendS "early_return") ^//^ expV true r ^//^ ta))
+      align (parens (string "early_return" ^//^ expV true r ^//^ ta))
     | E_constraint _ -> string "true"
     | E_comment _ | E_comment_struc _ -> empty
     | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _
@@ -1253,7 +1242,7 @@ let doc_tannot_opt_lem (Typ_annot_opt_aux(t,_)) = match t with
 let doc_fun_body_lem ctxt exp =
   let doc_exp = doc_exp_lem ctxt false exp in
   if ctxt.early_ret
-  then align (string (appendS "catch_early_return") ^//^ parens (doc_exp))
+  then align (string "catch_early_return" ^//^ parens (doc_exp))
   else doc_exp
 
 let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) =
@@ -1448,17 +1437,11 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) (Defs defs)
         separate empty (List.map doc_def_lem statedefs); hardline;
         hardline;
         register_refs; hardline;
-        if !opt_sequential then
-          concat [
-            string ("type MR 'a 'r = monadRS regstate 'a 'r " ^ exc_typ); hardline;
-            string ("type M 'a = monadS regstate 'a " ^ exc_typ); hardline;
-          ]
-        else
-          concat [
-            string ("type MR 'a 'r = base_monadR register_value regstate 'a 'r " ^ exc_typ); hardline;
-            string ("type M 'a = base_monad register_value regstate 'a " ^ exc_typ); hardline
-          ]
-        ]);
+        concat [
+          string ("type MR 'a 'r = base_monadR register_value regstate 'a 'r " ^ exc_typ); hardline;
+          string ("type M 'a = base_monad register_value regstate 'a " ^ exc_typ); hardline
+        ]
+       ]);
   (print defs_file)
     (concat
        [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
diff --git a/src/process_file.ml b/src/process_file.ml
index 1d4c5f03..34c1a255 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -243,10 +243,7 @@ let output_lem filename libs defs =
   let generated_line = generated_line filename in
   (* let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in *)
   let types_module = (filename ^ "_types") in
-  let monad_modules = (*["Prompt_monad"; "Prompt"; "State"] in*)
-    if !Pretty_print_lem.opt_sequential
-    then ["State_monad"; "State"]
-    else ["Prompt_monad"; "Prompt"] in
+  let monad_modules = ["Prompt_monad"; "Prompt"] in
   let operators_module =
     if !Pretty_print_lem.opt_mwords
     then "Sail_operators_mwords"