summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--cheri/Makefile5
-rw-r--r--lib/isabelle/Makefile5
-rw-r--r--lib/isabelle/State_lemmas.thy10
-rw-r--r--lib/isabelle/manual/Manual.thy2
-rw-r--r--mips/mips_extras_sequential.lem116
-rw-r--r--src/gen_lib/state.lem59
-rw-r--r--src/gen_lib/state_lifting.lem27
-rw-r--r--src/gen_lib/state_monad.lem14
-rw-r--r--src/pretty_print_lem.ml70
-rw-r--r--src/process_file.ml9
-rw-r--r--src/process_file.mli2
11 files changed, 241 insertions, 78 deletions
diff --git a/cheri/Makefile b/cheri/Makefile
index 01583280..d053fc67 100644
--- a/cheri/Makefile
+++ b/cheri/Makefile
@@ -54,6 +54,11 @@ cheri.lem: $(CHERI_SAILS)
$(SAIL) -lem -o cheri -auto_mono -mono_rewrites -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^
cheri_types.lem: cheri.lem
+cheri_sequential.lem: $(CHERI_SAILS)
+ $(SAIL) -lem -o cheri_sequential -auto_mono -mono_rewrites -lem_mwords -lem_sequential -lem_lib Mips_extras_sequential -undefined_gen -memo_z3 $^
+cheri_sequential_types.lem: cheri_sequential.lem
+Cheri_sequential.thy: $(MIPS_SAIL_DIR)/mips_extras_sequential.lem
+
cheri128_no_tlb.lem: $(CHERI128_NO_TLB_SAILS)
$(SAIL) -lem -o cheri128_no_tlb -lem_lib Mips_extras -undefined_gen -memo_z3 $^
cheri128_no_tlb_types.lem: cheri128_no_tlb.lem
diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index f8786321..b10dde78 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -1,6 +1,6 @@
THYS = Sail_instr_kinds.thy Sail_values.thy Sail_operators.thy \
Sail_operators_mwords.thy Sail_operators_bitlists.thy \
- State_monad.thy State.thy Prompt_monad.thy Prompt.thy
+ State_monad.thy State.thy State_lifting.thy Prompt_monad.thy Prompt.thy
EXTRA_THYS = State_monad_lemmas.thy State_lemmas.thy Prompt_monad_lemmas.thy \
Sail_operators_mwords_lemmas.thy Hoare.thy
@@ -51,5 +51,8 @@ State_monad.thy: ../../src/gen_lib/state_monad.lem Sail_values.thy
State.thy: ../../src/gen_lib/state.lem Prompt.thy State_monad.thy State_monad_lemmas.thy
lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
+State_lifting.thy: ../../src/gen_lib/state_lifting.lem Prompt.thy State.thy
+ lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
+
clean:
-rm $(THYS)
diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy
index 84b08e6c..253c21b9 100644
--- a/lib/isabelle/State_lemmas.thy
+++ b/lib/isabelle/State_lemmas.thy
@@ -1,5 +1,5 @@
theory State_lemmas
- imports State
+ imports State State_lifting
begin
lemma All_liftState_dom: "liftState_dom (r, m)"
@@ -44,12 +44,12 @@ lemma liftState_catch_early_return[simp]:
by (auto simp: catch_early_return_def catch_early_returnS_def sum.case_distrib cong: sum.case_cong)
lemma liftState_liftR[simp]:
- "liftState r (liftR m) = liftSR (liftState r m)"
- by (auto simp: liftR_def liftSR_def)
+ "liftState r (liftR m) = liftRS (liftState r m)"
+ by (auto simp: liftR_def liftRS_def)
lemma liftState_try_catchR[simp]:
- "liftState r (try_catchR m h) = try_catchSR (liftState r m) (liftState r \<circ> h)"
- by (auto simp: try_catchR_def try_catchSR_def sum.case_distrib cong: sum.case_cong)
+ "liftState r (try_catchR m h) = try_catchRS (liftState r m) (liftState r \<circ> h)"
+ by (auto simp: try_catchR_def try_catchRS_def sum.case_distrib cong: sum.case_cong)
lemma liftState_read_mem_BC:
assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a"
diff --git a/lib/isabelle/manual/Manual.thy b/lib/isabelle/manual/Manual.thy
index 53175ec9..90d65320 100644
--- a/lib/isabelle/manual/Manual.thy
+++ b/lib/isabelle/manual/Manual.thy
@@ -288,7 +288,7 @@ exception handler as arguments.
The exception mechanism is also used to implement early returns by throwing and catching return
values: A function body with one or more early returns of type @{typ 'a} (and exception type
@{typ 'e}) is lifted to a monadic expression with exception type @{typ "('a + 'e)"} using
-@{term liftSR}, such that an early return of the value @{term a} throws @{term "Inl a"}, and a
+@{term liftRS}, such that an early return of the value @{term a} throws @{term "Inl a"}, and a
regular exception @{term e} is thrown as @{term "Inr e"}. The function body is then wrapped in
@{term catch_early_returnS} to lower it back to the default monad and exception type. These
liftings and lowerings are automatically inserted by Sail for functions with early returns.\<^footnote>\<open>To be
diff --git a/mips/mips_extras_sequential.lem b/mips/mips_extras_sequential.lem
new file mode 100644
index 00000000..c3651500
--- /dev/null
+++ b/mips/mips_extras_sequential.lem
@@ -0,0 +1,116 @@
+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 ()
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 61477258..6bc304a8 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,33 +1,8 @@
open import Pervasives_extra
-(*open import Sail_impl_base*)
open import Sail_values
-open import Prompt_monad
-open import Prompt
open import State_monad
open import {isabelle} `State_monad_lemmas`
-(* State monad wrapper around prompt monad *)
-
-val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
-let rec liftState ra s = match s with
- | (Done a) -> returnS a
- | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
- | (Read_tag t k) -> bindS (read_tagS t) (fun v -> liftState ra (k v))
- | (Write_memv a k) -> bindS (write_mem_bytesS a) (fun v -> liftState ra (k v))
- | (Write_tag a t k) -> bindS (write_tagS a t) (fun v -> liftState ra (k v))
- | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v))
- | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v))
- | (Undefined k) -> bindS (undefined_boolS ()) (fun v -> liftState ra (k v))
- | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz) (liftState ra k)
- | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k)
- | (Footprint k) -> liftState ra k
- | (Barrier _ k) -> liftState ra k
- | (Print _ k) -> liftState ra k (* TODO *)
- | (Fail descr) -> failS descr
- | (Exception e) -> throwS e
-end
-
-
val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
let rec iterS_aux i f xs = match xs with
| x :: xs -> f i x >>$ iterS_aux (i + 1) f xs
@@ -53,6 +28,40 @@ end
declare {isabelle} termination_argument foreachS = automatic
+val bool_of_bitU_fail : forall 'rv 'e. bitU -> monadS 'rv bool 'e
+let bool_of_bitU_fail = function
+ | B0 -> returnS false
+ | B1 -> returnS true
+ | BU -> failS "bool_of_bitU"
+end
+
+val bool_of_bitU_oracleS : forall 'rv 'e. bitU -> monadS 'rv bool 'e
+let bool_of_bitU_oracleS = function
+ | B0 -> returnS false
+ | B1 -> returnS true
+ | BU -> undefined_boolS ()
+end
+
+val bools_of_bits_oracleS : forall 'rv 'e. list bitU -> monadS 'rv (list bool) 'e
+let bools_of_bits_oracleS bits =
+ foreachS bits []
+ (fun b bools ->
+ bool_of_bitU_oracleS b >>$= (fun b ->
+ returnS (bools ++ [b])))
+
+val of_bits_oracleS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
+let of_bits_oracleS bits =
+ bools_of_bits_oracleS bits >>$= (fun bs ->
+ returnS (of_bools bs))
+
+val of_bits_failS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
+let of_bits_failS bits = maybe_failS "of_bits" (of_bits bits)
+
+val mword_oracleS : forall 'rv 'a 'e. Size 'a => unit -> monadS 'rv (mword 'a) 'e
+let mword_oracleS () =
+ bools_of_bits_oracleS (repeat [BU] (integerFromNat size)) >>$= (fun bs ->
+ returnS (wordFromBitlist bs))
+
val whileS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) ->
('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
diff --git a/src/gen_lib/state_lifting.lem b/src/gen_lib/state_lifting.lem
new file mode 100644
index 00000000..7e569a7e
--- /dev/null
+++ b/src/gen_lib/state_lifting.lem
@@ -0,0 +1,27 @@
+open import Pervasives_extra
+open import Sail_values
+open import Prompt_monad
+open import Prompt
+open import State_monad
+open import {isabelle} `State_monad_lemmas`
+
+(* State monad wrapper around prompt monad *)
+
+val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
+let rec liftState ra s = match s with
+ | (Done a) -> returnS a
+ | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
+ | (Read_tag t k) -> bindS (read_tagS t) (fun v -> liftState ra (k v))
+ | (Write_memv a k) -> bindS (write_mem_bytesS a) (fun v -> liftState ra (k v))
+ | (Write_tag a t k) -> bindS (write_tagS a t) (fun v -> liftState ra (k v))
+ | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v))
+ | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v))
+ | (Undefined k) -> bindS (undefined_boolS ()) (fun v -> liftState ra (k v))
+ | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz) (liftState ra k)
+ | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k)
+ | (Footprint k) -> liftState ra k
+ | (Barrier _ k) -> liftState ra k
+ | (Print _ k) -> liftState ra k (* TODO *)
+ | (Fail descr) -> failS descr
+ | (Exception e) -> throwS e
+end
diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
index 8253b800..781bc129 100644
--- a/src/gen_lib/state_monad.lem
+++ b/src/gen_lib/state_monad.lem
@@ -94,12 +94,12 @@ let assert_expS exp msg = if exp then returnS () else failS msg
(* For early return, we abuse exceptions by throwing and catching
the return value. The exception type is "either 'r 'e", where "Right e"
represents a proper exception and "Left r" an early return of value "r". *)
-type monadSR 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e)
+type monadRS 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e)
-val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadSR 'regs 'a 'r 'e
+val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadRS 'regs 'a 'r 'e
let early_returnS r = throwS (Left r)
-val catch_early_returnS : forall 'regs 'a 'e. monadSR 'regs 'a 'a 'e -> monadS 'regs 'a 'e
+val catch_early_returnS : forall 'regs 'a 'e. monadRS 'regs 'a 'a 'e -> monadS 'regs 'a 'e
let catch_early_returnS m =
try_catchS m
(function
@@ -108,12 +108,12 @@ let catch_early_returnS m =
end)
(* Lift to monad with early return by wrapping exceptions *)
-val liftSR : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadSR 'regs 'a 'r 'e
-let liftSR m = try_catchS m (fun e -> throwS (Right e))
+val liftRS : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadRS 'regs 'a 'r 'e
+let liftRS m = try_catchS m (fun e -> throwS (Right e))
(* Catch exceptions in the presence of early returns *)
-val try_catchSR : forall 'regs 'a 'r 'e1 'e2. monadSR 'regs 'a 'r 'e1 -> ('e1 -> monadSR 'regs 'a 'r 'e2) -> monadSR 'regs 'a 'r 'e2
-let try_catchSR m h =
+val try_catchRS : forall 'regs 'a 'r 'e1 'e2. monadRS 'regs 'a 'r 'e1 -> ('e1 -> monadRS 'regs 'a 'r 'e2) -> monadRS 'regs 'a 'r 'e2
+let try_catchRS m h =
try_catchS m
(function
| Left r -> throwS (Left r)
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index f58c3fa6..a7da28bc 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -62,6 +62,8 @@ 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,10 +553,11 @@ let doc_exp_lem, doc_let_lem =
let expY = top_exp ctxt true in
let expN = top_exp ctxt false in
let expV = top_exp ctxt in
+ 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 separate space [string "liftR"; parens (doc)]
- else doc in
+ then wrap_parens (separate space [string (appendS "liftR"); parens (doc)])
+ else wrap_parens doc in
match e with
| E_assign((LEXP_aux(le_act,tannot) as le), e) ->
(* can only be register writes *)
@@ -571,13 +574,13 @@ let doc_exp_lem, doc_let_lem =
underscore ^^
doc_id_lem id in
liftR ((prefix 2 1)
- (string "write_reg_field_range")
+ (string (appendS "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 "write_reg_range")
+ (string (appendS "write_reg_range"))
(align (deref ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
| LEXP_vector (le,e2) ->
(match le with
@@ -608,13 +611,13 @@ let doc_exp_lem, doc_let_lem =
dot ^^
string "set_field"*) in
liftR ((prefix 2 1)
- (string "write_reg_field")
+ (string (appendS "write_reg_field"))
(doc_lexp_deref_lem ctxt le ^^ space ^^
field_ref ^/^ expY e))
| LEXP_deref re ->
- liftR ((prefix 2 1) (string "write_reg") (expY re ^/^ expY e))
+ liftR ((prefix 2 1) (string (appendS "write_reg")) (expY re ^/^ expY e))
| _ ->
- liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem ctxt le ^/^ expY e)))
+ liftR ((prefix 2 1) (string (appendS "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")
@@ -650,7 +653,11 @@ 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 "foreachM" else "foreach" in
+ let combinator =
+ if effectful (effect_of body)
+ then if !opt_sequential then "foreachS" else "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 =
@@ -683,12 +690,13 @@ 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 -> "M", return cond, body
- | true, false -> "M", cond, return body
- | true, true -> "M", cond, body
+ | false, true -> monad_suffix, return cond, body
+ | true, false -> monad_suffix, cond, return body
+ | true, true -> monad_suffix, cond, body
in
let used_vars_body = find_e_ids body in
let lambda =
@@ -719,7 +727,7 @@ let doc_exp_lem, doc_let_lem =
begin
match args with
| [exp] ->
- let epp = separate space [string "early_return"; expY exp] in
+ let epp = separate space [string (appendS "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
@@ -788,7 +796,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 "read_reg";doc_id_lem (append_id id "_ref")] in
+ let epp = separate space [string (appendS "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
@@ -874,12 +882,10 @@ let doc_exp_lem, doc_let_lem =
else
raise (Reporting_basic.err_todo l "Warning: try-block around pure expression")
| E_throw e ->
- let epp = liftR (separate space [string "throw"; expY e]) in
- if aexp_needed then parens (align epp) else align epp
- | E_exit e -> liftR (separate space [string "exit"; expY e])
+ align (liftR (separate space [string (appendS "throw"); expY e]))
+ | E_exit e -> liftR (separate space [string (appendS "exit"); expY e])
| E_assert (e1,e2) ->
- let epp = liftR (separate space [string "assert_exp"; expY e1; expY e2]) in
- if aexp_needed then parens (align epp) else align epp
+ align (liftR (separate space [string (appendS "assert_exp"); expY e1; expY e2]))
| E_app_infix (e1,id,e2) ->
raise (Reporting_basic.err_unreachable l
"E_app_infix should have been rewritten before pretty-printing")
@@ -888,26 +894,28 @@ 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, _)), _) ->
- string ">>"
+ | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> seq_pp
| 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
- [string ">>= fun varstup -> let";
+ [bind_pp; string "fun varstup -> let";
doc_pat_lem ctxt true pat;
string "= varstup in"]
| _ ->
- separate space [string ">>= fun"; doc_pat_lem ctxt true pat; arrow]
+ separate space [bind_pp; string "fun";
+ doc_pat_lem ctxt true pat; arrow]
in
infix 0 1 middle (expV b e1) (expN e2)
in
if aexp_needed then parens (align epp) else epp
| E_internal_return (e1) ->
- separate space [string "return"; expY e1]
+ wrap_parens (align (separate space [string (appendS "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))
@@ -915,15 +923,15 @@ 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 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
else separate space
- [string ret_monad;
+ [string ": MR";
parens (doc_typ_lem (typ_of full_exp));
parens (doc_typ_lem (typ_of r))] in
- align (parens (string "early_return" ^//^ expV true r ^//^ ta))
+ align (parens (string (appendS "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 _
@@ -1250,7 +1258,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 "catch_early_return" ^//^ parens (doc_exp))
+ then align (string (appendS "catch_early_return") ^//^ parens (doc_exp))
else doc_exp
let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) =
@@ -1445,12 +1453,12 @@ 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
+ if !opt_sequential then
concat [
- string ("type MR 'a 'r = State_monad.MR regstate 'a 'r " ^ exc_typ); hardline;
- string ("type M 'a = State_monad.M regstate 'a " ^ exc_typ); hardline;
+ string ("type MR 'a 'r = monadRS regstate 'a 'r " ^ exc_typ); hardline;
+ string ("type M 'a = monadS regstate 'a " ^ exc_typ); hardline;
]
- else *)
+ else
concat [
string ("type MR 'a 'r = monadR register_value 'a 'r " ^ exc_typ); hardline;
string ("type M 'a = monad register_value 'a " ^ exc_typ); hardline
diff --git a/src/process_file.ml b/src/process_file.ml
index 4856c20a..1d4c5f03 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -51,9 +51,6 @@
open PPrint
open Pretty_print_common
-let opt_lem_sequential = ref false
-let opt_lem_mwords = ref false
-
type out_type =
| Lem_ast_out
| Lem_out of string list
@@ -246,10 +243,10 @@ 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
+ let monad_modules = (*["Prompt_monad"; "Prompt"; "State"] in*)
+ if !Pretty_print_lem.opt_sequential
then ["State_monad"; "State"]
- else ["Prompt_monad"; "Prompt"] in *)
+ else ["Prompt_monad"; "Prompt"] in
let operators_module =
if !Pretty_print_lem.opt_mwords
then "Sail_operators_mwords"
diff --git a/src/process_file.mli b/src/process_file.mli
index b38b4259..cc94888e 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -65,8 +65,6 @@ val rewrite_ast_check : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val load_file_no_check : Ast.order -> string -> unit Ast.defs
val load_file : Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t
-val opt_lem_sequential : bool ref
-val opt_lem_mwords : bool ref
val opt_just_check : bool ref
val opt_ddump_tc_ast : bool ref
val opt_ddump_rewrite_ast : ((string * int) option) ref
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:57:19 +0000