summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-01-12 17:27:37 +0000
committerAlasdair Armstrong2018-01-12 17:27:37 +0000
commite56eafdb87f3f4e362cca7d0a6ca3d8a0e849b44 (patch)
tree4b19d06dd6a234c5524c88e8aeceefce41ca8864 /src
parentebc33211b0a3a6c14bbe4106b9a618b8ac594f52 (diff)
parentffcf8a814cdd23eaff9286835478afb66fbb0029 (diff)
Merge remote-tracking branch 'origin/experiments' into sail2
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml8
-rw-r--r--src/ast_util.mli1
-rw-r--r--src/gen_lib/prompt.lem149
-rw-r--r--src/gen_lib/state.lem174
-rw-r--r--src/lem_interp/sail_impl_base.lem27
-rw-r--r--src/monomorphise.ml7
-rw-r--r--src/pretty_print.mli2
-rw-r--r--src/pretty_print_lem.ml504
-rw-r--r--src/process_file.ml20
-rw-r--r--src/process_file.mli2
-rw-r--r--src/rewriter.ml3
-rw-r--r--src/rewrites.ml53
-rw-r--r--src/sail.ml8
-rw-r--r--src/type_check.ml37
14 files changed, 567 insertions, 428 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index e502f86f..206515c5 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -692,6 +692,14 @@ let id_of_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) =
| Some id -> id
| None -> raise (Reporting_basic.err_typ l "funcl list is empty")
+let id_of_type_def_aux = function
+ | TD_abbrev (id, _, _)
+ | TD_record (id, _, _, _, _)
+ | TD_variant (id, _, _, _, _)
+ | TD_enum (id, _, _, _)
+ | TD_bitfield (id, _, _) -> id
+let id_of_type_def (TD_aux (td_aux, _)) = id_of_type_def_aux td_aux
+
module BE = struct
type t = base_effect
let compare be1 be2 = String.compare (string_of_base_effect be1) (string_of_base_effect be2)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index a4ad92fb..69bd5a52 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -194,6 +194,7 @@ val string_of_letbind : 'a letbind -> string
val string_of_index_range : index_range -> string
val id_of_fundef : 'a fundef -> id
+val id_of_type_def : 'a type_def -> id
val id_of_kid : kid -> id
val kid_of_id : id -> kid
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index e9684414..744b6f7f 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -2,13 +2,12 @@ open import Pervasives_extra
open import Sail_impl_base
open import Sail_values
-type MR 'a 'r = outcome_r 'a 'r
-type M 'a = outcome 'a
+type M 'a 'e = outcome 'a 'e
-val return : forall 'a 'r. 'a -> MR 'a 'r
+val return : forall 'a 'e. 'a -> M 'a 'e
let return a = Done a
-val bind : forall 'a 'b 'r. MR 'a 'r -> ('a -> MR 'b 'r) -> MR 'b 'r
+val bind : forall 'a 'b 'e. M 'a 'e -> ('a -> M 'b 'e) -> M 'b 'e
let rec bind m f = match m with
| Done a -> f a
| Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (bind o f,opt))
@@ -22,60 +21,72 @@ let rec bind m f = match m with
| Escape descr -> Escape descr
| Fail descr -> Fail descr
| Error descr -> Error descr
- | Return a -> Return a
+ | Exception e -> Exception e
| Internal descr o_s -> Internal descr (let (o,opt) = o_s in (bind o f ,opt))
end
let inline (>>=) = bind
-val (>>) : forall 'b 'r. MR unit 'r -> MR 'b 'r -> MR 'b 'r
-let inline (>>) m n = m >>= fun _ -> n
+val (>>) : forall 'b 'e. M unit 'e -> M 'b 'e -> M 'b 'e
+let inline (>>) m n = m >>= fun (_ : unit) -> n
-val exit : forall 'a 'b. 'b -> M 'a
-let exit s = Fail Nothing
+val exit : forall 'a 'e. unit -> M 'a 'e
+let exit () = Fail Nothing
-val assert_exp : bool -> string -> M unit
+val assert_exp : forall 'e. bool -> string -> M unit 'e
let assert_exp exp msg = if exp then Done () else Fail (Just msg)
-val early_return : forall 'r. 'r -> MR unit 'r
-let early_return r = Return r
+val throw : forall 'a 'e. 'e -> M 'a 'e
+let throw e = Exception e
-val liftR : forall 'a 'r. M 'a -> MR 'a 'r
-let rec liftR m = match m with
+val try_catch : forall 'a 'e1 'e2. M 'a 'e1 -> ('e1 -> M 'a 'e2) -> M 'a 'e2
+let rec try_catch m h = match m with
| Done a -> Done a
- | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (liftR o,opt))
- | Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (liftR o,opt))
- | Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (liftR o,opt))
- | Excl_res k -> Excl_res (fun v -> let (o,opt) = k v in (liftR o,opt))
- | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (liftR o,opt))
- | Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (liftR o,opt))
- | Footprint o_s -> Footprint (let (o,opt) = o_s in (liftR o,opt))
- | Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (liftR o,opt))
- | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (liftR o,opt))
+ | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (try_catch o h,opt))
+ | Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (try_catch o h,opt))
+ | Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (try_catch o h,opt))
+ | Excl_res k -> Excl_res (fun v -> let (o,opt) = k v in (try_catch o h,opt))
+ | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (try_catch o h,opt))
+ | Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (try_catch o h,opt))
+ | Footprint o_s -> Footprint (let (o,opt) = o_s in (try_catch o h,opt))
+ | Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (try_catch o h,opt))
| Escape descr -> Escape descr
| Fail descr -> Fail descr
| Error descr -> Error descr
- | Return _ -> Error "uncaught early return"
+ | Exception e -> h e
+ | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (try_catch o h ,opt))
end
-val catch_early_return : forall 'a 'r. MR 'a 'a -> M 'a
-let rec catch_early_return m = match m with
- | Done a -> Done a
- | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
- | Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
- | Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
- | Excl_res k -> Excl_res (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
- | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (catch_early_return o,opt))
- | Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (catch_early_return o,opt))
- | Footprint o_s -> Footprint (let (o,opt) = o_s in (catch_early_return o,opt))
- | Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (catch_early_return o,opt))
- | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (catch_early_return o,opt))
- | Escape descr -> Escape descr
- | Fail descr -> Fail descr
- | Error descr -> Error descr
- | Return a -> Done a
-end
-
-val read_mem : forall 'a 'b. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'b
+(* 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 MR 'a 'r 'e = M 'a (either 'r 'e)
+
+val early_return : forall 'a 'r 'e. 'r -> MR 'a 'r 'e
+let early_return r = throw (Left r)
+
+val catch_early_return : forall 'a 'e. MR 'a 'a 'e -> M 'a 'e
+let catch_early_return m =
+ try_catch m
+ (function
+ | Left a -> return a
+ | Right e -> throw e
+ end)
+
+(* Lift to monad with early return by wrapping exceptions *)
+val liftR : forall 'a 'r 'e. M 'a 'e -> MR 'a 'r 'e
+let liftR m = try_catch m (fun e -> throw (Right e))
+
+(* Catch exceptions in the presence of early returns *)
+val try_catchR : forall 'a 'r 'e1 'e2. MR 'a 'r 'e1 -> ('e1 -> MR 'a 'r 'e2) -> MR 'a 'r 'e2
+let try_catchR m h =
+ try_catch m
+ (function
+ | Left r -> throw (Left r)
+ | Right e -> h e
+ end)
+
+
+val read_mem : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'b 'e
let read_mem dir rk addr sz =
let addr = address_lifted_of_bitv (bits_of addr) in
let sz = natFromInteger sz in
@@ -84,24 +95,24 @@ let read_mem dir rk addr sz =
(Done bitv,Nothing) in
Read_mem (rk,addr,sz) k
-val excl_result : unit -> M bool
+val excl_result : forall 'e. unit -> M bool 'e
let excl_result () =
let k successful = (return successful,Nothing) in
Excl_res k
-val write_mem_ea : forall 'a. Bitvector 'a => write_kind -> 'a -> integer -> M unit
+val write_mem_ea : forall 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> M unit 'e
let write_mem_ea wk addr sz =
let addr = address_lifted_of_bitv (bits_of addr) in
let sz = natFromInteger sz in
Write_ea (wk,addr,sz) (Done (),Nothing)
-val write_mem_val : forall 'a. Bitvector 'a => 'a -> M bool
+val write_mem_val : forall 'a 'e. Bitvector 'a => 'a -> M bool 'e
let write_mem_val v =
let v = external_mem_value (bits_of v) in
let k successful = (return successful,Nothing) in
Write_memv v k
-val read_reg_aux : forall 'a. Bitvector 'a => reg_name -> M 'a
+val read_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> M 'a 'e
let read_reg_aux reg =
let k reg_value =
let v = of_bits (internal_reg_value reg_value) in
@@ -123,7 +134,7 @@ let read_reg_bitfield reg regfield =
let reg_deref = read_reg
-val write_reg_aux : forall 'a. Bitvector 'a => reg_name -> 'a -> M unit
+val write_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> 'a -> M unit 'e
let write_reg_aux reg_name v =
let regval = external_reg_value reg_name (bits_of v) in
Write_reg (reg_name,regval) (Done (), Nothing)
@@ -149,29 +160,29 @@ let write_reg_field_bit = write_reg_field_pos
let write_reg_ref (reg, v) = write_reg reg v
-val barrier : barrier_kind -> M unit
+val barrier : forall 'e. barrier_kind -> M unit 'e
let barrier bk = Barrier bk (Done (), Nothing)
-val footprint : M unit
+val footprint : forall 'e. M unit 'e
let footprint = Footprint (Done (),Nothing)
-val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> MR unit 'e) -> list 'a -> MR unit 'e
+val iter_aux : forall 'a 'e. integer -> (integer -> 'a -> M unit 'e) -> list 'a -> M unit 'e
let rec iter_aux i f xs = match xs with
| x :: xs -> f i x >> iter_aux (i + 1) f xs
| [] -> return ()
end
-val iteri : forall 'regs 'e 'a. (integer -> 'a -> MR unit 'e) -> list 'a -> MR unit 'e
+val iteri : forall 'a 'e. (integer -> 'a -> M unit 'e) -> list 'a -> M unit 'e
let iteri f xs = iter_aux 0 f xs
-val iter : forall 'regs 'e 'a. ('a -> MR unit 'e) -> list 'a -> MR unit 'e
+val iter : forall 'a 'e. ('a -> M unit 'e) -> list 'a -> M unit 'e
let iter f xs = iteri (fun _ x -> f x) xs
-val foreachM_inc : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
- (integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
+val foreachM_inc : forall 'vars 'e. (integer * integer * integer) -> 'vars ->
+ (integer -> 'vars -> M 'vars 'e) -> M 'vars 'e
let rec foreachM_inc (i,stop,by) vars body =
if (by > 0 && i <= stop) || (by < 0 && stop <= i)
then
@@ -180,8 +191,8 @@ let rec foreachM_inc (i,stop,by) vars body =
else return vars
-val foreachM_dec : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
- (integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
+val foreachM_dec : forall 'vars 'e. (integer * integer * integer) -> 'vars ->
+ (integer -> 'vars -> M 'vars 'e) -> M 'vars 'e
let rec foreachM_dec (i,stop,by) vars body =
if (by > 0 && i >= stop) || (by < 0 && stop >= i)
then
@@ -193,21 +204,21 @@ val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'va
let rec while_PP vars cond body =
if cond vars then while_PP (body vars) cond body else vars
-val while_PM : forall 'vars 'r. 'vars -> ('vars -> bool) ->
- ('vars -> MR 'vars 'r) -> MR 'vars 'r
+val while_PM : forall 'vars 'e. 'vars -> ('vars -> bool) ->
+ ('vars -> M 'vars 'e) -> M 'vars 'e
let rec while_PM vars cond body =
if cond vars then
body vars >>= fun vars -> while_PM vars cond body
else return vars
-val while_MP : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
- ('vars -> 'vars) -> MR 'vars 'r
+val while_MP : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) ->
+ ('vars -> 'vars) -> M 'vars 'e
let rec while_MP vars cond body =
cond vars >>= fun cond_val ->
if cond_val then while_MP (body vars) cond body else return vars
-val while_MM : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
- ('vars -> MR 'vars 'r) -> MR 'vars 'r
+val while_MM : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) ->
+ ('vars -> M 'vars 'e) -> M 'vars 'e
let rec while_MM vars cond body =
cond vars >>= fun cond_val ->
if cond_val then
@@ -219,21 +230,21 @@ let rec until_PP vars cond body =
let vars = body vars in
if (cond vars) then vars else until_PP (body vars) cond body
-val until_PM : forall 'vars 'r. 'vars -> ('vars -> bool) ->
- ('vars -> MR 'vars 'r) -> MR 'vars 'r
+val until_PM : forall 'vars 'e. 'vars -> ('vars -> bool) ->
+ ('vars -> M 'vars 'e) -> M 'vars 'e
let rec until_PM vars cond body =
body vars >>= fun vars ->
if (cond vars) then return vars else until_PM vars cond body
-val until_MP : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
- ('vars -> 'vars) -> MR 'vars 'r
+val until_MP : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) ->
+ ('vars -> 'vars) -> M 'vars 'e
let rec until_MP vars cond body =
let vars = body vars in
cond vars >>= fun cond_val ->
if cond_val then return vars else until_MP vars cond body
-val until_MM : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
- ('vars -> MR 'vars 'r) -> MR 'vars 'r
+val until_MM : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) ->
+ ('vars -> M 'vars 'e) -> M 'vars 'e
let rec until_MM vars cond body =
body vars >>= fun vars ->
cond vars >>= fun cond_val ->
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index fa0fcd24..f9011323 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -23,55 +23,79 @@ let init_state regs =
write_ea = Nothing;
last_exclusive_operation_was_load = false |>
-(* State, nondeterminism and exception monad with result type 'a
- and exception type 'e. *)
-type ME 'regs 'a 'e = sequential_state 'regs -> list ((either 'a 'e) * sequential_state 'regs)
-
-(* By default, we use strings to distinguish between different types of exceptions *)
-type M 'regs 'a = ME 'regs 'a string
+type ex 'e =
+ | Exit
+ | Assert of string
+ | Throw of 'e
-(* For early return, we abuse exceptions by throwing and catching
- the return value. The exception type is "either 'r string", where "Right e"
- represents a proper exception and "Left r" an early return of value "r". *)
-type MR 'regs 'a 'r = ME 'regs 'a (either 'r string)
+type result 'a 'e =
+ | Value of 'a
+ | Exception of (ex 'e)
-val liftR : forall 'a 'r 'regs. M 'regs 'a -> MR 'regs 'a 'r
-let liftR m s = List.map (function
- | (Left a, s') -> (Left a, s')
- | (Right e, s') -> (Right (Right e), s')
- end) (m s)
+(* State, nondeterminism and exception monad with result value type 'a
+ and exception type 'e. *)
+type M 'regs 'a 'e = sequential_state 'regs -> list (result 'a 'e * sequential_state 'regs)
-val return : forall 'regs 'a 'e. 'a -> ME 'regs 'a 'e
-let return a s = [(Left a,s)]
+val return : forall 'regs 'a 'e. 'a -> M 'regs 'a 'e
+let return a s = [(Value a,s)]
-val bind : forall 'regs 'a 'b 'e. ME 'regs 'a 'e -> ('a -> ME 'regs 'b 'e) -> ME 'regs 'b 'e
+val bind : forall 'regs 'a 'b 'e. M 'regs 'a 'e -> ('a -> M 'regs 'b 'e) -> M 'regs 'b 'e
let bind m f (s : sequential_state 'regs) =
List.concatMap (function
- | (Left a, s') -> f a s'
- | (Right e, s') -> [(Right e, s')]
+ | (Value a, s') -> f a s'
+ | (Exception e, s') -> [(Exception e, s')]
end) (m s)
let inline (>>=) = bind
-val (>>): forall 'regs 'b 'e. ME 'regs unit 'e -> ME 'regs 'b 'e -> ME 'regs 'b 'e
-let inline (>>) m n = m >>= fun _ -> n
+val (>>): forall 'regs 'b 'e. M 'regs unit 'e -> M 'regs 'b 'e -> M 'regs 'b 'e
+let inline (>>) m n = m >>= fun (_ : unit) -> n
-val exit : forall 'regs 'e 'a. 'e -> M 'regs 'a
-let exit _ s = [(Right "exit", s)]
+val throw : forall 'regs 'a 'e. 'e -> M 'regs 'a 'e
+let throw e s = [(Exception (Throw e), s)]
-val assert_exp : forall 'regs. bool -> string -> M 'regs unit
-let assert_exp exp msg s = if exp then [(Left (), s)] else [(Right msg, s)]
+val try_catch : forall 'regs 'a 'e1 'e2. M 'regs 'a 'e1 -> ('e1 -> M 'regs 'a 'e2) -> M 'regs 'a 'e2
+let try_catch m h s =
+ List.concatMap (function
+ | (Value a, s') -> return a s'
+ | (Exception (Throw e), s') -> h e s'
+ | (Exception Exit, s') -> [(Exception Exit, s')]
+ | (Exception (Assert msg), s') -> [(Exception (Assert msg), s')]
+ end) (m s)
-val early_return : forall 'regs 'a 'r. 'r -> MR 'regs 'a 'r
-let early_return r s = [(Right (Left r), s)]
+val exit : forall 'regs 'e 'a. unit -> M 'regs 'a 'e
+let exit () s = [(Exception Exit, s)]
-val catch_early_return : forall 'regs 'a. MR 'regs 'a 'a -> M 'regs 'a
-let catch_early_return m s =
- List.map
+val assert_exp : forall 'regs 'e. bool -> string -> M 'regs unit 'e
+let assert_exp exp msg s = if exp then [(Value (), s)] else [(Exception (Assert msg), s)]
+
+(* 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 MR 'regs 'a 'r 'e = M 'regs 'a (either 'r 'e)
+
+val early_return : forall 'regs 'a 'r 'e. 'r -> MR 'regs 'a 'r 'e
+let early_return r = throw (Left r)
+
+val catch_early_return : forall 'regs 'a 'e. MR 'regs 'a 'a 'e -> M 'regs 'a 'e
+let catch_early_return m =
+ try_catch m
+ (function
+ | Left a -> return a
+ | Right e -> throw e
+ end)
+
+(* Lift to monad with early return by wrapping exceptions *)
+val liftR : forall 'a 'r 'regs 'e. M 'regs 'a 'e -> MR 'regs 'a 'r 'e
+let liftR m = try_catch m (fun e -> throw (Right e))
+
+(* Catch exceptions in the presence of early returns *)
+val try_catchR : forall 'regs 'a 'r 'e1 'e2. MR 'regs 'a 'r 'e1 -> ('e1 -> MR 'regs 'a 'r 'e2) -> MR 'regs 'a 'r 'e2
+let try_catchR m h =
+ try_catch m
(function
- | (Right (Left a), s') -> (Left a, s')
- | (Right (Right e), s') -> (Right e, s')
- | (Left a, s') -> (Left a, s')
- end) (m s)
+ | Left r -> throw (Left r)
+ | Right e -> h e
+ end)
val range : integer -> integer -> list integer
let rec range i j =
@@ -103,20 +127,20 @@ let is_exclusive = function
end
-val read_mem : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'regs 'b
+val read_mem : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'regs 'b 'e
let read_mem dir read_kind addr sz state =
let addr = unsigned addr in
let addrs = range addr (addr+sz-1) in
let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in
let value = of_bits (Sail_values.internal_mem_value dir memory_value) in
if is_exclusive read_kind
- then [(Left value, <| state with last_exclusive_operation_was_load = true |>)]
- else [(Left value, state)]
+ then [(Value value, <| state with last_exclusive_operation_was_load = true |>)]
+ else [(Value value, state)]
(* caps are aligned at 32 bytes *)
let cap_alignment = (32 : integer)
-val read_tag : forall 'regs 'a. Bitvector 'a => bool -> read_kind -> 'a -> M 'regs bitU
+val read_tag : forall 'regs 'a 'e. Bitvector 'a => bool -> read_kind -> 'a -> M 'regs bitU 'e
let read_tag dir read_kind addr state =
let addr = (unsigned addr) / cap_alignment in
let tag = match (Map.lookup addr state.tagstate) with
@@ -124,20 +148,20 @@ let read_tag dir read_kind addr state =
| Nothing -> B0
end in
if is_exclusive read_kind
- then [(Left tag, <| state with last_exclusive_operation_was_load = true |>)]
- else [(Left tag, state)]
+ then [(Value tag, <| state with last_exclusive_operation_was_load = true |>)]
+ else [(Value tag, state)]
-val excl_result : forall 'regs. unit -> M 'regs bool
+val excl_result : forall 'regs 'e. unit -> M 'regs bool 'e
let excl_result () state =
let success =
- (Left true, <| state with last_exclusive_operation_was_load = false |>) in
- (Left false, state) :: if state.last_exclusive_operation_was_load then [success] else []
+ (Value true, <| state with last_exclusive_operation_was_load = false |>) in
+ (Value false, state) :: if state.last_exclusive_operation_was_load then [success] else []
-val write_mem_ea : forall 'regs 'a. Bitvector 'a => write_kind -> 'a -> integer -> M 'regs unit
+val write_mem_ea : forall 'regs 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> M 'regs unit 'e
let write_mem_ea write_kind addr sz state =
- [(Left (), <| state with write_ea = Just (write_kind,unsigned addr,sz) |>)]
+ [(Value (), <| state with write_ea = Just (write_kind,unsigned addr,sz) |>)]
-val write_mem_val : forall 'a 'regs 'b. Bitvector 'a => 'a -> M 'regs bool
+val write_mem_val : forall 'a 'regs 'b 'e. Bitvector 'a => 'a -> M 'regs bool 'e
let write_mem_val v state =
let (write_kind,addr,sz) = match state.write_ea with
| Nothing -> failwith "write ea has not been announced yet"
@@ -147,27 +171,27 @@ let write_mem_val v state =
let addresses_with_value = List.zip addrs v in
let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem)
state.memstate addresses_with_value in
- [(Left true, <| state with memstate = memstate |>)]
+ [(Value true, <| state with memstate = memstate |>)]
-val write_tag : forall 'regs. bitU -> M 'regs bool
+val write_tag : forall 'regs 'e. bitU -> M 'regs bool 'e
let write_tag t state =
let (write_kind,addr,sz) = match state.write_ea with
| Nothing -> failwith "write ea has not been announced yet"
| Just write_ea -> write_ea end in
let taddr = addr / cap_alignment in
let tagstate = Map.insert taddr t state.tagstate in
- [(Left true, <| state with tagstate = tagstate |>)]
+ [(Value true, <| state with tagstate = tagstate |>)]
-val read_reg : forall 'regs 'a. register_ref 'regs 'a -> M 'regs 'a
+val read_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> M 'regs 'a 'e
let read_reg reg state =
let v = reg.read_from state.regstate in
- [(Left v,state)]
+ [(Value v,state)]
(*let read_reg_range reg i j state =
let v = slice (get_reg state (name_of_reg reg)) i j in
- [(Left (vec_to_bvec v),state)]
+ [(Value (vec_to_bvec v),state)]
let read_reg_bit reg i state =
let v = access (get_reg state (name_of_reg reg)) i in
- [(Left v,state)]
+ [(Value v,state)]
let read_reg_field reg regfield =
let (i,j) = register_field_indices reg regfield in
read_reg_range reg i j
@@ -177,17 +201,17 @@ let read_reg_bitfield reg regfield =
let reg_deref = read_reg
-val write_reg : forall 'regs 'a. register_ref 'regs 'a -> 'a -> M 'regs unit
+val write_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> 'a -> M 'regs unit 'e
let write_reg reg v state =
- [(Left (), <| state with regstate = reg.write_to state.regstate v |>)]
+ [(Value (), <| state with regstate = reg.write_to state.regstate v |>)]
let write_reg_ref (reg, v) = write_reg reg v
-val update_reg : forall 'regs 'a 'b. register_ref 'regs 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit
+val update_reg : forall 'regs 'a 'b 'e. register_ref 'regs 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit 'e
let update_reg reg f v state =
let current_value = get_reg state reg in
let new_value = f current_value v in
- [(Left (), set_reg state reg new_value)]
+ [(Value (), set_reg state reg new_value)]
let write_reg_field reg regfield = update_reg reg regfield.set_field
@@ -219,26 +243,26 @@ let update_reg_field_bit regfield i reg_val bit =
regfield.set_field reg_val new_field_value
let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i)
-val barrier : forall 'regs. barrier_kind -> M 'regs unit
+val barrier : forall 'regs 'e. barrier_kind -> M 'regs unit 'e
let barrier _ = return ()
-val footprint : forall 'regs. M 'regs unit
+val footprint : forall 'regs 'e. M 'regs unit 'e
let footprint s = return () s
-val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> ME 'regs unit 'e) -> list 'a -> ME 'regs unit 'e
+val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e
let rec iter_aux i f xs = match xs with
| x :: xs -> f i x >> iter_aux (i + 1) f xs
| [] -> return ()
end
-val iteri : forall 'regs 'e 'a. (integer -> 'a -> ME 'regs unit 'e) -> list 'a -> ME 'regs unit 'e
+val iteri : forall 'regs 'e 'a. (integer -> 'a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e
let iteri f xs = iter_aux 0 f xs
-val iter : forall 'regs 'e 'a. ('a -> ME 'regs unit 'e) -> list 'a -> ME 'regs unit 'e
+val iter : forall 'regs 'e 'a. ('a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e
let iter f xs = iteri (fun _ x -> f x) xs
val foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
- (integer -> 'vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e
+ (integer -> 'vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec foreachM_inc (i,stop,by) vars body =
if (by > 0 && i <= stop) || (by < 0 && stop <= i)
then
@@ -248,7 +272,7 @@ let rec foreachM_inc (i,stop,by) vars body =
val foreachM_dec : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
- (integer -> 'vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e
+ (integer -> 'vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec foreachM_dec (i,stop,by) vars body =
if (by > 0 && i >= stop) || (by < 0 && stop >= i)
then
@@ -261,20 +285,20 @@ let rec while_PP vars cond body =
if cond vars then while_PP (body vars) cond body else vars
val while_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) ->
- ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e
+ ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec while_PM vars cond body =
if cond vars then
body vars >>= fun vars -> while_PM vars cond body
else return vars
-val while_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) ->
- ('vars -> 'vars) -> ME 'regs 'vars 'e
+val while_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
+ ('vars -> 'vars) -> M 'regs 'vars 'e
let rec while_MP vars cond body =
cond vars >>= fun cond_val ->
if cond_val then while_MP (body vars) cond body else return vars
-val while_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) ->
- ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e
+val while_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
+ ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec while_MM vars cond body =
cond vars >>= fun cond_val ->
if cond_val then
@@ -287,20 +311,20 @@ let rec until_PP vars cond body =
if (cond vars) then vars else until_PP (body vars) cond body
val until_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) ->
- ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e
+ ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec until_PM vars cond body =
body vars >>= fun vars ->
if (cond vars) then return vars else until_PM vars cond body
-val until_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) ->
- ('vars -> 'vars) -> ME 'regs 'vars 'e
+val until_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
+ ('vars -> 'vars) -> M 'regs 'vars 'e
let rec until_MP vars cond body =
let vars = body vars in
cond vars >>= fun cond_val ->
if cond_val then return vars else until_MP vars cond body
-val until_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) ->
- ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e
+val until_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
+ ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec until_MM vars cond body =
body vars >>= fun vars ->
cond vars >>= fun cond_val ->
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 421219da..368f7505 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -905,36 +905,35 @@ end
(* the address_lifted types should go away here and be replaced by address *)
type with_aux 'o = 'o * maybe ((unit -> (string * string)) * ((list (reg_name * register_value)) -> list event))
-type outcome_r 'a 'r =
+type outcome 'a 'e =
(* Request to read memory, value is location to read, integer is size to read,
followed by registers that were used in computing that size *)
- | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome_r 'a 'r))
+ | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome 'a 'e))
(* Tell the system a write is imminent, at address lifted, of size nat *)
- | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome_r 'a 'r))
+ | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome 'a 'e))
(* Request the result of store-exclusive *)
- | Excl_res of (bool -> with_aux (outcome_r 'a 'r))
+ | Excl_res of (bool -> with_aux (outcome 'a 'e))
(* Request to write memory at last signalled address. Memory value should be 8
times the size given in ea signal *)
- | Write_memv of memory_value * (bool -> with_aux (outcome_r 'a 'r))
+ | Write_memv of memory_value * (bool -> with_aux (outcome 'a 'e))
(* Request a memory barrier *)
- | Barrier of barrier_kind * with_aux (outcome_r 'a 'r)
+ | Barrier of barrier_kind * with_aux (outcome 'a 'e)
(* Tell the system to dynamically recalculate dependency footprint *)
- | Footprint of with_aux (outcome_r 'a 'r)
+ | Footprint of with_aux (outcome 'a 'e)
(* Request to read register, will track dependency when mode.track_values *)
- | Read_reg of reg_name * (register_value -> with_aux (outcome_r 'a 'r))
+ | Read_reg of reg_name * (register_value -> with_aux (outcome 'a 'e))
(* Request to write register *)
- | Write_reg of (reg_name * register_value) * with_aux (outcome_r 'a 'r)
+ | Write_reg of (reg_name * register_value) * with_aux (outcome 'a 'e)
| Escape of maybe string
(*Result of a failed assert with possible error message to report*)
| Fail of maybe string
- (* Early return with value of type 'r *)
- | Return of 'r
- | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome_r 'a 'r)
+ (* Exception of type 'e *)
+ | Exception of 'e
+ | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome 'a 'e)
| Done of 'a
| Error of string
-type outcome 'a = outcome_r 'a unit
-type outcome_s 'a = with_aux (outcome 'a)
+type outcome_s 'a 'e = with_aux (outcome 'a 'e)
(* first string : output of instruction_stack_to_string
second string: output of local_variables_to_string *)
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index af3484ec..06f0683a 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -102,7 +102,7 @@ let rec subst_nc substs (NC_aux (nc,l) as n_constraint) =
begin
match KBindings.find kid substs with
| Nexp_aux (Nexp_constant i,_) ->
- if List.mem i is then re NC_true else re NC_false
+ if List.exists (fun j -> Big_int.equal i j) is then re NC_true else re NC_false
| nexp ->
raise (Reporting_basic.err_general l
("Unable to substitute " ^ string_of_nexp nexp ^
@@ -1691,11 +1691,10 @@ let rewrite_size_parameters env (Defs defs) =
let sizes_funcl fsizes (FCL_aux (FCL_Funcl (id,pexp),(l,_))) =
let sizes = size_vars pexp in
let pat,guard,exp,pannot = destruct_pexp pexp in
- (* TODO: what, if anything, should sequential be? *)
let visible_tyvars =
KidSet.union
- (Pretty_print_lem.lem_tyvars_of_typ false true (pat_typ_of pat))
- (Pretty_print_lem.lem_tyvars_of_typ false true (typ_of exp))
+ (Pretty_print_lem.lem_tyvars_of_typ (pat_typ_of pat))
+ (Pretty_print_lem.lem_tyvars_of_typ (typ_of exp))
in
let expose_tyvars = KidSet.diff sizes visible_tyvars in
let parameters = match pat with
diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index c685e0a4..b459926b 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -53,4 +53,4 @@ open Type_check
(* Prints on formatter the defs as Lem Ast nodes *)
val pp_lem_defs : Format.formatter -> tannot defs -> unit
-val pp_defs_lem : bool -> bool -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit
+val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index a79ae0eb..0002f8cc 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -59,6 +59,9 @@ open Pretty_print_common
* PPrint-based sail-to-lem pprinter
****************************************************************************)
+let opt_sequential = ref false
+let opt_mwords = ref false
+
let print_to_from_interp_value = ref false
let langlebar = string "<|"
let ranglebar = string "|>"
@@ -190,8 +193,8 @@ let rec orig_nexp (Nexp_aux (nexp, l)) =
(* Returns the set of type variables that will appear in the Lem output,
which may be smaller than those in the Sail type. May need to be
updated with doc_typ_lem *)
-let rec lem_nexps_of_typ sequential mwords (Typ_aux (t,_)) =
- let trec = lem_nexps_of_typ sequential mwords in
+let rec lem_nexps_of_typ (Typ_aux (t,_)) =
+ let trec = lem_nexps_of_typ in
match t with
| Typ_id _ -> NexpSet.empty
| Typ_var kid -> NexpSet.singleton (orig_nexp (nvar kid))
@@ -205,75 +208,78 @@ let rec lem_nexps_of_typ sequential mwords (Typ_aux (t,_)) =
Typ_arg_aux (Typ_arg_order ord, _);
Typ_arg_aux (Typ_arg_typ elem_typ, _)]) ->
let m = nexp_simp m in
- if mwords && is_bit_typ elem_typ && not (is_nexp_constant m) then
+ if !opt_mwords && is_bit_typ elem_typ && not (is_nexp_constant m) then
NexpSet.singleton (orig_nexp m)
else trec elem_typ
(* NexpSet.union
- (if mwords then tyvars_of_nexp (nexp_simp m) else NexpSet.empty)
+ (if !opt_mwords then tyvars_of_nexp (nexp_simp m) else NexpSet.empty)
(trec elem_typ) *)
| Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
- if sequential then trec etyp else NexpSet.empty
+ if !opt_sequential then trec etyp else NexpSet.empty
| Typ_app(Id_aux (Id "range", _),_)
| Typ_app(Id_aux (Id "implicit", _),_)
| Typ_app(Id_aux (Id "atom", _), _) -> NexpSet.empty
| Typ_app (_,tas) ->
- List.fold_left (fun s ta -> NexpSet.union s (lem_nexps_of_typ_arg sequential mwords ta))
+ List.fold_left (fun s ta -> NexpSet.union s (lem_nexps_of_typ_arg ta))
NexpSet.empty tas
| Typ_exist (kids,_,t) ->
let s = trec t in
List.fold_left (fun s k -> NexpSet.remove k s) s (List.map nvar kids)
-and lem_nexps_of_typ_arg sequential mwords (Typ_arg_aux (ta,_)) =
+and lem_nexps_of_typ_arg (Typ_arg_aux (ta,_)) =
match ta with
| Typ_arg_nexp nexp -> NexpSet.singleton (nexp_simp (orig_nexp nexp))
- | Typ_arg_typ typ -> lem_nexps_of_typ sequential mwords typ
+ | Typ_arg_typ typ -> lem_nexps_of_typ typ
| Typ_arg_order _ -> NexpSet.empty
-let lem_tyvars_of_typ sequential mwords typ =
+let lem_tyvars_of_typ typ =
NexpSet.fold (fun nexp ks -> KidSet.union ks (tyvars_of_nexp nexp))
- (lem_nexps_of_typ sequential mwords typ) KidSet.empty
+ (lem_nexps_of_typ typ) KidSet.empty
(* When making changes here, check whether they affect lem_tyvars_of_typ *)
let doc_typ_lem, doc_atomic_typ_lem =
(* following the structure of parser for precedence *)
- let rec typ sequential mwords ty = fn_typ sequential mwords true ty
- and typ' sequential mwords ty = fn_typ sequential mwords false ty
- and fn_typ (sequential : bool) (mwords : bool) atyp_needed ((Typ_aux (t, _)) as ty) = match t with
+ let rec typ ty = fn_typ true ty
+ and typ' ty = fn_typ false ty
+ and fn_typ atyp_needed ((Typ_aux (t, _)) as ty) = match t with
| Typ_fn(arg,ret,efct) ->
- (*let exc_typ = string "string" in*)
let ret_typ =
if effectful efct
- then separate space [string "_M";(*parens exc_typ;*) fn_typ sequential mwords true ret]
- else separate space [fn_typ sequential mwords false ret] in
- let tpp = separate space [tup_typ sequential mwords true arg; arrow;ret_typ] in
+ then separate space [string "M"; fn_typ true ret]
+ else separate space [fn_typ false ret] in
+ let arg_typs = match arg with
+ | Typ_aux (Typ_tup typs, _) ->
+ List.map (app_typ false) typs
+ | _ -> [tup_typ false arg] in
+ let tpp = separate (space ^^ arrow ^^ space) (arg_typs @ [ret_typ]) in
(* once we have proper excetions we need to know what the exceptions type is *)
if atyp_needed then parens tpp else tpp
- | _ -> tup_typ sequential mwords atyp_needed ty
- and tup_typ sequential mwords atyp_needed ((Typ_aux (t, _)) as ty) = match t with
+ | _ -> tup_typ atyp_needed ty
+ and tup_typ atyp_needed ((Typ_aux (t, _)) as ty) = match t with
| Typ_tup typs ->
- parens (separate_map (space ^^ star ^^ space) (app_typ sequential mwords false) typs)
- | _ -> app_typ sequential mwords atyp_needed ty
- and app_typ sequential mwords atyp_needed ((Typ_aux (t, l)) as ty) = match t with
+ parens (separate_map (space ^^ star ^^ space) (app_typ false) typs)
+ | _ -> app_typ atyp_needed ty
+ and app_typ atyp_needed ((Typ_aux (t, l)) as ty) = match t with
| Typ_app(Id_aux (Id "vector", _), [
Typ_arg_aux (Typ_arg_nexp n, _);
Typ_arg_aux (Typ_arg_nexp m, _);
Typ_arg_aux (Typ_arg_order ord, _);
Typ_arg_aux (Typ_arg_typ elem_typ, _)]) ->
let tpp = match elem_typ with
- | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) when mwords ->
+ | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) when !opt_mwords ->
string "bitvector " ^^ doc_nexp_lem (nexp_simp m)
(* (match nexp_simp m with
| (Nexp_aux(Nexp_constant i,_)) -> string "bitvector ty" ^^ doc_int i
| (Nexp_aux(Nexp_var _, _)) -> separate space [string "bitvector"; doc_nexp m]
| _ -> raise (Reporting_basic.err_unreachable l
"cannot pretty-print bitvector type with non-constant length")) *)
- | _ -> string "vector" ^^ space ^^ typ sequential mwords elem_typ in
+ | _ -> string "vector" ^^ space ^^ typ elem_typ in
if atyp_needed then parens tpp else tpp
| Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
(* TODO: Better distinguish register names and contents? *)
(* fn_typ regtypes atyp_needed etyp *)
let tpp =
- if sequential
- then string "register_ref regstate " ^^ typ sequential mwords etyp
+ if !opt_sequential
+ then string "register_ref regstate " ^^ typ etyp
else string "register" in
if atyp_needed then parens tpp else tpp
| Typ_app(Id_aux (Id "range", _),_) ->
@@ -283,10 +289,10 @@ let doc_typ_lem, doc_atomic_typ_lem =
| Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
(string "integer")
| Typ_app(id,args) ->
- let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space (doc_typ_arg_lem sequential mwords) args) in
+ let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space doc_typ_arg_lem args) in
if atyp_needed then parens tpp else tpp
- | _ -> atomic_typ sequential mwords atyp_needed ty
- and atomic_typ sequential mwords atyp_needed ((Typ_aux (t, l)) as ty) = match t with
+ | _ -> atomic_typ atyp_needed ty
+ and atomic_typ atyp_needed ((Typ_aux (t, l)) as ty) = match t with
| Typ_id (Id_aux (Id "bool",_)) -> string "bool"
| Typ_id (Id_aux (Id "bit",_)) -> string "bitU"
| Typ_id (id) ->
@@ -297,11 +303,11 @@ let doc_typ_lem, doc_atomic_typ_lem =
| Typ_app _ | Typ_tup _ | Typ_fn _ ->
(* exhaustiveness matters here to avoid infinite loops
* if we add a new Typ constructor *)
- let tpp = typ sequential mwords ty in
+ let tpp = typ ty in
if atyp_needed then parens tpp else tpp
| Typ_exist (kids,_,ty) -> begin
- let tpp = typ sequential mwords ty in
- let visible_vars = lem_tyvars_of_typ sequential mwords ty in
+ let tpp = typ ty in
+ let visible_vars = lem_tyvars_of_typ ty in
match List.filter (fun kid -> KidSet.mem kid visible_vars) kids with
| [] -> if atyp_needed then parens tpp else tpp
| bad -> raise (Reporting_basic.err_general l
@@ -309,8 +315,8 @@ let doc_typ_lem, doc_atomic_typ_lem =
String.concat ", " (List.map string_of_kid bad) ^
" escape into Lem"))
end
- and doc_typ_arg_lem sequential mwords (Typ_arg_aux(t,_)) = match t with
- | Typ_arg_typ t -> app_typ sequential mwords true t
+ and doc_typ_arg_lem (Typ_arg_aux(t,_)) = match t with
+ | Typ_arg_typ t -> app_typ true t
| Typ_arg_nexp n -> doc_nexp_lem (nexp_simp n)
| Typ_arg_order o -> empty
in typ', atomic_typ
@@ -320,36 +326,37 @@ let doc_typ_lem, doc_atomic_typ_lem =
length argument are checked for variables, and the latter only if it is
a bitvector; for other types of vectors, the length is not pretty-printed
in the type, and the start index is never pretty-printed in vector types. *)
-let rec contains_t_pp_var mwords (Typ_aux (t,a) as typ) = match t with
+let rec contains_t_pp_var (Typ_aux (t,a) as typ) = match t with
| Typ_id _ -> false
| Typ_var _ -> true
| Typ_exist _ -> true
- | Typ_fn (t1,t2,_) -> contains_t_pp_var mwords t1 || contains_t_pp_var mwords t2
- | Typ_tup ts -> List.exists (contains_t_pp_var mwords) ts
+ | Typ_fn (t1,t2,_) -> contains_t_pp_var t1 || contains_t_pp_var t2
+ | Typ_tup ts -> List.exists contains_t_pp_var ts
| Typ_app (c,targs) ->
if Ast_util.is_number typ then false
else if is_bitvector_typ typ then
let (_,length,_,_) = vector_typ_args_of typ in
let length = nexp_simp length in
not (is_nexp_constant length ||
- (mwords && match length with Nexp_aux (Nexp_var _,_) -> true | _ -> false))
- else List.exists (contains_t_arg_pp_var mwords) targs
-and contains_t_arg_pp_var mwords (Typ_arg_aux (targ, _)) = match targ with
- | Typ_arg_typ t -> contains_t_pp_var mwords t
+ (!opt_mwords &&
+ match length with Nexp_aux (Nexp_var _,_) -> true | _ -> false))
+ else List.exists contains_t_arg_pp_var targs
+and contains_t_arg_pp_var (Typ_arg_aux (targ, _)) = match targ with
+ | Typ_arg_typ t -> contains_t_pp_var t
| Typ_arg_nexp nexp -> not (is_nexp_constant (nexp_simp nexp))
| _ -> false
-let doc_tannot_lem sequential mwords eff typ =
- if contains_t_pp_var mwords typ then empty
+let doc_tannot_lem eff typ =
+ if contains_t_pp_var typ then empty
else
- let ta = doc_typ_lem sequential mwords typ in
- if eff then string " : _M " ^^ parens ta
+ let ta = doc_typ_lem typ in
+ if eff then string " : M " ^^ parens ta
else string " : " ^^ ta
(* doc_lit_lem gets as an additional parameter the type information from the
* expression around it: that's a hack, but how else can we distinguish between
* undefined values of different types ? *)
-let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a =
+let doc_lit_lem in_pat (L_aux(lit,l)) a =
match lit with
| L_unit -> utf8string "()"
| L_zero -> utf8string "B0"
@@ -372,8 +379,8 @@ let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a =
| Typ_app (Id_aux (Id "register", _),_) -> utf8string "UndefinedRegister 0"
| Typ_id (Id_aux (Id "string", _)) -> utf8string "\"\""
| _ ->
- let ta = if contains_t_pp_var mwords typ then empty
- else doc_tannot_lem sequential mwords false typ in
+ let ta = if contains_t_pp_var typ then empty
+ else doc_tannot_lem false typ in
parens
((utf8string "(failwith \"undefined value of unsupported type\")") ^^ ta))
| _ -> utf8string "(failwith \"undefined value of unsupported type\")")
@@ -386,7 +393,7 @@ let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a =
using this would require adding a dependency on ZArith to Sail. *)
let parts = Util.split_on_char '.' s in
let (num, denom) = match parts with
- | [i] -> (Big_int.of_string i, (Big_int.of_int 1))
+ | [i] -> (Big_int.of_string i, Big_int.of_int 1)
| [i;f] ->
let denom = Big_int.pow_int_positive 10 (String.length f) in
(Big_int.add (Big_int.mul (Big_int.of_string i) denom) (Big_int.of_string f), denom)
@@ -437,19 +444,19 @@ let rec typeclass_nexps (Typ_aux(t,_)) = match t with
| Typ_app _ -> NexpSet.empty
| Typ_exist (kids,_,t) -> NexpSet.empty (* todo *)
-let doc_typclasses_lem mwords t =
- if mwords then
+let doc_typclasses_lem t =
+ if !opt_mwords then
let nexps = typeclass_nexps t in
if NexpSet.is_empty nexps then (empty, NexpSet.empty) else
(separate_map comma_sp (fun nexp -> string "Size " ^^ doc_nexp_lem nexp) (NexpSet.elements nexps) ^^ string " => ", nexps)
else (empty, NexpSet.empty)
-let doc_typschm_lem sequential mwords quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
- let pt = doc_typ_lem sequential mwords t in
+let doc_typschm_lem quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
+ let pt = doc_typ_lem t in
if quants
then
- let nexps_used = lem_nexps_of_typ sequential mwords t in
- let ptyc, nexps_sizes = doc_typclasses_lem mwords t in
+ let nexps_used = lem_nexps_of_typ t in
+ let ptyc, nexps_sizes = doc_typclasses_lem t in
let nexps_to_include = NexpSet.union nexps_used nexps_sizes in
if NexpSet.is_empty nexps_to_include
then pt
@@ -463,44 +470,44 @@ let is_ctor env id = match Env.lookup_id id env with
(*Note: vector concatenation, literal vectors, indexed vectors, and record should
be removed prior to pp. The latter two have never yet been seen
*)
-let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) = match p with
+let rec doc_pat_lem apat_needed (P_aux (p,(l,annot)) as pa) = match p with
| P_app(id, ((_ :: _) as pats)) ->
let ppp = doc_unop (doc_id_lem_ctor id)
- (parens (separate_map comma (doc_pat_lem sequential mwords true) pats)) in
+ (parens (separate_map comma (doc_pat_lem true) pats)) in
if apat_needed then parens ppp else ppp
| P_app(id,[]) -> doc_id_lem_ctor id
- | P_lit lit -> doc_lit_lem sequential mwords true lit annot
+ | P_lit lit -> doc_lit_lem true lit annot
| P_wild -> underscore
| P_id id ->
begin match id with
| Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
| _ -> doc_id_lem id end
- | P_var(p,kid) -> doc_pat_lem sequential mwords true p
- | P_as(p,id) -> parens (separate space [doc_pat_lem sequential mwords true p; string "as"; doc_id_lem id])
+ | P_var(p,kid) -> doc_pat_lem true p
+ | P_as(p,id) -> parens (separate space [doc_pat_lem true p; string "as"; doc_id_lem id])
| P_typ(Typ_aux (Typ_tup typs, _), P_aux (P_tup pats, _)) ->
(* Isabelle does not seem to like type-annotated tuple patterns;
it gives a syntax error. Avoid this by annotating the tuple elements instead *)
let doc_elem typ (P_aux (_, annot) as pat) =
- doc_pat_lem sequential mwords true (P_aux (P_typ (typ, pat), annot)) in
+ doc_pat_lem true (P_aux (P_typ (typ, pat), annot)) in
parens (separate comma_sp (List.map2 doc_elem typs pats))
| P_typ(typ,p) ->
- let doc_p = doc_pat_lem sequential mwords true p in
- if contains_t_pp_var mwords typ then doc_p
- else parens (doc_op colon doc_p (doc_typ_lem sequential mwords typ))
+ let doc_p = doc_pat_lem true p in
+ if contains_t_pp_var typ then doc_p
+ else parens (doc_op colon doc_p (doc_typ_lem typ))
| P_vector pats ->
let ppp =
(separate space)
- [string "Vector";brackets (separate_map semi (doc_pat_lem sequential mwords true) pats);underscore;underscore] in
+ [string "Vector";brackets (separate_map semi (doc_pat_lem true) pats);underscore;underscore] in
if apat_needed then parens ppp else ppp
| P_vector_concat pats ->
raise (Reporting_basic.err_unreachable l
"vector concatenation patterns should have been removed before pretty-printing")
| P_tup pats ->
(match pats with
- | [p] -> doc_pat_lem sequential mwords apat_needed p
- | _ -> parens (separate_map comma_sp (doc_pat_lem sequential mwords false) pats))
- | P_list pats -> brackets (separate_map semi (doc_pat_lem sequential mwords false) pats) (*Never seen but easy in lem*)
- | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem sequential mwords true p) (doc_pat_lem sequential mwords true p')
+ | [p] -> doc_pat_lem apat_needed p
+ | _ -> parens (separate_map comma_sp (doc_pat_lem false) pats))
+ | P_list pats -> brackets (separate_map semi (doc_pat_lem false) pats) (*Never seen but easy in lem*)
+ | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem true p) (doc_pat_lem true p')
| P_record (_,_) -> empty (* TODO *)
let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with
@@ -532,11 +539,11 @@ let typ_id_of (Typ_aux (typ, l)) = match typ with
let prefix_recordtype = true
let report = Reporting_basic.err_unreachable
let doc_exp_lem, doc_let_lem =
- let rec top_exp sequential mwords (early_ret : bool) (aexp_needed : bool)
+ let rec top_exp (early_ret : bool) (aexp_needed : bool)
(E_aux (e, (l,annot)) as full_exp) =
- let expY = top_exp sequential mwords early_ret true in
- let expN = top_exp sequential mwords early_ret false in
- let expV = top_exp sequential mwords early_ret in
+ let expY = top_exp early_ret true in
+ let expN = top_exp early_ret false in
+ let expV = top_exp early_ret in
let liftR doc =
if early_ret && effectful (effect_of full_exp)
then separate space [string "liftR"; parens (doc)]
@@ -558,10 +565,10 @@ let doc_exp_lem, doc_let_lem =
doc_id_lem id in
liftR ((prefix 2 1)
(string "write_reg_field_range")
- (align (doc_lexp_deref_lem sequential mwords early_ret le ^/^
+ (align (doc_lexp_deref_lem early_ret le ^/^
field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e)))
| _ ->
- let deref = doc_lexp_deref_lem sequential mwords early_ret le in
+ let deref = doc_lexp_deref_lem early_ret le in
liftR ((prefix 2 1)
(string "write_reg_range")
(align (deref ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
@@ -578,10 +585,10 @@ let doc_exp_lem, doc_let_lem =
let call = if is_bitvector_typ (Env.base_typ_of (env_of full_exp) (typ_of_annot fannot)) then "write_reg_field_bit" else "write_reg_field_pos" in
liftR ((prefix 2 1)
(string call)
- (align (doc_lexp_deref_lem sequential mwords early_ret le ^/^
+ (align (doc_lexp_deref_lem early_ret le ^/^
field_ref ^/^ expY e2 ^/^ expY e)))
| LEXP_aux (_, lannot) ->
- let deref = doc_lexp_deref_lem sequential mwords early_ret le in
+ let deref = doc_lexp_deref_lem early_ret le in
let call = if is_bitvector_typ (Env.base_typ_of (env_of full_exp) (typ_of_annot lannot)) then "write_reg_bit" else "write_reg_pos" in
liftR ((prefix 2 1) (string call)
(deref ^/^ expY e2 ^/^ expY e))
@@ -595,10 +602,10 @@ let doc_exp_lem, doc_let_lem =
string "set_field"*) in
liftR ((prefix 2 1)
(string "write_reg_field")
- (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
+ (doc_lexp_deref_lem early_ret le ^^ space ^^
field_ref ^/^ expY e))
| _ ->
- liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem sequential mwords early_ret le ^/^ expY e)))
+ liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem early_ret le ^/^ expY e)))
| E_vector_append(le,re) ->
raise (Reporting_basic.err_unreachable l
"E_vector_append should have been rewritten before pretty-printing")
@@ -614,7 +621,7 @@ let doc_exp_lem, doc_let_lem =
| E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) ->
raise (report l "E_for should have been removed till now")
| E_let(leb,e) ->
- let epp = let_exp sequential mwords early_ret leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
+ let epp = let_exp early_ret leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
if aexp_needed then parens epp else epp
| E_app(f,args) ->
begin match f with
@@ -669,13 +676,13 @@ let doc_exp_lem, doc_let_lem =
| [exp] ->
let epp = separate space [string "early_return"; expY exp] in
let aexp_needed, tepp =
- if contains_t_pp_var mwords (typ_of exp) ||
- contains_t_pp_var mwords (typ_of full_exp) then
+ if contains_t_pp_var (typ_of exp) ||
+ contains_t_pp_var (typ_of full_exp) then
aexp_needed, epp
else
- let tannot = separate space [string "_MR";
- doc_atomic_typ_lem sequential mwords false (typ_of full_exp);
- doc_atomic_typ_lem sequential mwords false (typ_of exp)] in
+ let tannot = separate space [string "MR";
+ doc_atomic_typ_lem false (typ_of full_exp);
+ doc_atomic_typ_lem false (typ_of exp)] in
true, doc_op colon epp tannot in
if aexp_needed then parens tepp else tepp
| _ -> raise (Reporting_basic.err_unreachable l
@@ -693,19 +700,23 @@ let doc_exp_lem, doc_let_lem =
parens (separate_map comma (expV false) args) in
if aexp_needed then parens (align epp) else epp
| _ ->
- let call = match annot with
+ let call, is_extern = match annot with
| Some (env, _, _) when Env.is_extern f env "lem" ->
- string (Env.get_extern f env "lem")
- | _ -> doc_id_lem f in
- let argspp = match args with
- | [arg] -> expV true arg
- | args -> parens (align (separate_map (comma ^^ break 0) (expV false) args)) in
+ string (Env.get_extern f env "lem"), true
+ | _ -> doc_id_lem f, false in
+ let argspp =
+ (* TODO Update Sail library functions to not use tupled arguments,
+ then remove the special case here *)
+ if is_extern then
+ parens (align (separate_map (comma ^^ break 0) (expV true) args))
+ else
+ align (separate_map (break 1) (expV true) args) in
let epp = align (call ^//^ argspp) in
let (taepp,aexp_needed) =
let t = (*Env.base_typ_of (env_of full_exp)*) (typ_of full_exp) in
let eff = effect_of full_exp in
if typ_needs_printed (Env.base_typ_of (env_of full_exp) t)
- then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true)
+ then (align epp ^^ (doc_tannot_lem (effectful eff) t), true)
else (epp, aexp_needed) in
liftR (if aexp_needed then parens (align taepp) else taepp)
end
@@ -738,11 +749,11 @@ let doc_exp_lem, doc_let_lem =
if has_effect eff BE_rreg then
let epp = separate space [string "read_reg";doc_id_lem id] in
if is_bitvector_typ base_typ
- then liftR (parens (epp ^^ doc_tannot_lem sequential mwords true base_typ))
+ then liftR (parens (epp ^^ doc_tannot_lem true base_typ))
else liftR epp
else if is_ctor env id then doc_id_lem_ctor id
else doc_id_lem id
- | E_lit lit -> doc_lit_lem sequential mwords false lit annot
+ | E_lit lit -> doc_lit_lem false lit annot
| E_cast(typ,e) ->
expV aexp_needed e
| E_tuple exps ->
@@ -756,7 +767,7 @@ let doc_exp_lem, doc_let_lem =
| _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
let epp = anglebars (space ^^ (align (separate_map
(semi_sp ^^ break 1)
- (doc_fexp sequential mwords early_ret recordtyp) fexps)) ^^ space) in
+ (doc_fexp early_ret recordtyp) fexps)) ^^ space) in
if aexp_needed then parens epp else epp
| E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
let recordtyp = match annot with
@@ -765,7 +776,7 @@ let doc_exp_lem, doc_let_lem =
when Env.is_record tid env ->
tid
| _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
- anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp sequential mwords early_ret recordtyp) fexps))
+ anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp early_ret recordtyp) fexps))
| E_vector exps ->
let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
let (start, len, order, etyp) =
@@ -791,9 +802,9 @@ let doc_exp_lem, doc_let_lem =
let epp =
group (separate space [string "Vector"; brackets expspp;string start;string dir_out]) in
let (epp,aexp_needed) =
- if is_bit_typ etyp && mwords then
+ if is_bit_typ etyp && !opt_mwords then
let bepp = string "vec_to_bvec" ^^ space ^^ parens (align epp) in
- (bepp ^^ doc_tannot_lem sequential mwords false t, true)
+ (bepp ^^ doc_tannot_lem false t, true)
else (epp,aexp_needed) in
if aexp_needed then parens (align epp) else epp
| E_vector_update(v,e1,e2) ->
@@ -824,10 +835,23 @@ let doc_exp_lem, doc_let_lem =
let epp =
group ((separate space [string "match"; only_integers e; string "with"]) ^/^
- (separate_map (break 1) (doc_case sequential mwords early_ret) pexps) ^/^
+ (separate_map (break 1) (doc_case early_ret) pexps) ^/^
(string "end")) in
if aexp_needed then parens (align epp) else align epp
- | E_exit e -> liftR (separate space [string "exit"; expY e;])
+ | E_try (e, pexps) ->
+ if effectful (effect_of e) then
+ let try_catch = if early_ret then "try_catchR" else "try_catch" in
+ let epp =
+ group ((separate space [string try_catch; expY e; string "(function "]) ^/^
+ (separate_map (break 1) (doc_case early_ret) pexps) ^/^
+ (string "end)")) in
+ if aexp_needed then parens (align epp) else align epp
+ 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])
| 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
@@ -844,67 +868,67 @@ let doc_exp_lem, doc_let_lem =
(separate space [expV b e1; string ">>"]) ^^ hardline ^^ expN e2
| _ ->
(separate space [expV b e1; string ">>= fun";
- doc_pat_lem sequential mwords true pat;arrow]) ^^ hardline ^^ expN e2 in
+ doc_pat_lem true pat;arrow]) ^^ hardline ^^ expN e2 in
if aexp_needed then parens (align epp) else epp
| E_internal_return (e1) ->
separate space [string "return"; expY e1]
| E_sizeof nexp ->
(match nexp_simp nexp with
- | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem sequential mwords false (L_aux (L_num i, l)) annot
+ | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem false (L_aux (L_num i, l)) annot
| _ ->
raise (Reporting_basic.err_unreachable l
"pretty-printing non-constant sizeof expressions to Lem not supported"))
| E_return r ->
- let ret_monad = if 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 mwords (typ_of full_exp) || contains_t_pp_var mwords (typ_of r)
+ if contains_t_pp_var (typ_of full_exp) || contains_t_pp_var (typ_of r)
then empty
else separate space
[string ret_monad;
- parens (doc_typ_lem sequential mwords (typ_of full_exp));
- parens (doc_typ_lem sequential mwords (typ_of r))] in
+ 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))
| E_constraint _ -> string "true"
| E_comment _ | E_comment_struc _ -> empty
| E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _ | E_internal_exp_user _ ->
raise (Reporting_basic.err_unreachable l
"unsupported internal expression encountered while pretty-printing")
- and let_exp sequential mwords early_ret (LB_aux(lb,_)) = match lb with
+ and let_exp early_ret (LB_aux(lb,_)) = match lb with
| LB_val(pat,e) ->
prefix 2 1
- (separate space [string "let"; doc_pat_lem sequential mwords true pat; equals])
- (top_exp sequential mwords early_ret false e)
+ (separate space [string "let"; doc_pat_lem true pat; equals])
+ (top_exp early_ret false e)
- and doc_fexp sequential mwords early_ret recordtyp (FE_aux(FE_Fexp(id,e),_)) =
+ and doc_fexp early_ret recordtyp (FE_aux(FE_Fexp(id,e),_)) =
let fname =
if prefix_recordtype
then (string (string_of_id recordtyp ^ "_")) ^^ doc_id_lem id
else doc_id_lem id in
- group (doc_op equals fname (top_exp sequential mwords early_ret true e))
+ group (doc_op equals fname (top_exp early_ret true e))
- and doc_case sequential mwords early_ret = function
+ and doc_case early_ret = function
| Pat_aux(Pat_exp(pat,e),_) ->
- group (prefix 3 1 (separate space [pipe; doc_pat_lem sequential mwords false pat;arrow])
- (group (top_exp sequential mwords early_ret false e)))
+ group (prefix 3 1 (separate space [pipe; doc_pat_lem false pat;arrow])
+ (group (top_exp early_ret false e)))
| Pat_aux(Pat_when(_,_,_),(l,_)) ->
raise (Reporting_basic.err_unreachable l
"guarded pattern expression should have been rewritten before pretty-printing")
- and doc_lexp_deref_lem sequential mwords early_ret ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
+ and doc_lexp_deref_lem early_ret ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
| LEXP_field (le,id) ->
- parens (separate empty [doc_lexp_deref_lem sequential mwords early_ret le;dot;doc_id_lem id])
+ parens (separate empty [doc_lexp_deref_lem early_ret le;dot;doc_id_lem id])
| LEXP_id id -> doc_id_lem id
| LEXP_cast (typ,id) -> doc_id_lem id
- | LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem sequential mwords early_ret) lexps)
+ | LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem early_ret) lexps)
| _ ->
raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Unsupported lexp"))
(* expose doc_exp_lem and doc_let *)
in top_exp, let_exp
(*TODO Upcase and downcase type and constructors as needed*)
-let doc_type_union_lem sequential mwords (Tu_aux(typ_u,_)) = match typ_u with
+let doc_type_union_lem (Tu_aux(typ_u,_)) = match typ_u with
| Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor id; string "of";
- parens (doc_typ_lem sequential mwords typ)]
+ parens (doc_typ_lem typ)]
| Tu_id id -> separate space [pipe; doc_id_lem_ctor id]
let rec doc_range_lem (BF_aux(r,_)) = match r with
@@ -912,17 +936,17 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with
| BF_range(i1,i2) -> parens (doc_op comma (doc_int i1) (doc_int i2))
| BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2)
-let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
+let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
| TD_abbrev(id,nm,(TypSchm_aux (TypSchm_ts (typq, _), _) as typschm)) ->
doc_op equals
(separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem None typq])
- (doc_typschm_lem sequential mwords false typschm)
+ (doc_typschm_lem false typschm)
| TD_record(id,nm,typq,fs,_) ->
let fname fid = if prefix_recordtype
then concat [doc_id_lem id;string "_";doc_id_lem_type fid;]
else doc_id_lem_type fid in
let f_pp (typ,fid) =
- concat [fname fid;space;colon;space;doc_typ_lem sequential mwords typ; semi] in
+ concat [fname fid;space;colon;space;doc_typ_lem typ; semi] in
let rectyp = match typq with
| TypQ_aux (TypQ_tq qs, _) ->
let quant_item = function
@@ -939,7 +963,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown),
[mk_typ_arg (Typ_arg_typ rectyp);
mk_typ_arg (Typ_arg_typ ftyp)])) in
- let rfannot = doc_tannot_lem sequential mwords false reftyp in
+ let rfannot = doc_tannot_lem false reftyp in
let get, set =
string "rec_val" ^^ dot ^^ fname fid,
anglebars (space ^^ string "rec_val with " ^^
@@ -968,7 +992,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
doc_op equals
(separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem None typq])
((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space))) ^^ hardline ^^
- if sequential && string_of_id id = "regstate" then empty
+ if !opt_sequential && string_of_id id = "regstate" then empty
else separate_map hardline doc_field fs
| TD_variant(id,nm,typq,ar,_) ->
(match id with
@@ -982,7 +1006,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
| Id_aux ((Id "diafp"),_) -> empty *)
| Id_aux ((Id "option"),_) -> empty
| _ ->
- let ar_doc = group (separate_map (break 1) (doc_type_union_lem sequential mwords) ar) in
+ let ar_doc = group (separate_map (break 1) doc_type_union_lem ar) in
let typ_pp =
(doc_op equals)
(concat [string "type"; space; doc_id_lem_type id; space; doc_typquant_items_lem None typq])
@@ -1152,30 +1176,64 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
else empty)
| _ -> raise (Reporting_basic.err_unreachable l "register with non-constant indices")
+let args_of_typ l env typ =
+ let typs = match typ with
+ | Typ_aux (Typ_tup typs, _) -> typs
+ | typ -> [typ] in
+ let arg i typ =
+ let id = mk_id ("arg" ^ string_of_int i) in
+ P_aux (P_id id, (l, Some (env, typ, no_effect))),
+ E_aux (E_id id, (l, Some (env, typ, no_effect))) in
+ List.split (List.mapi arg typs)
+
+let rec untuple_args_pat (P_aux (paux, ((l, _) as annot)) as pat) =
+ let env = env_of_annot annot in
+ let (Typ_aux (taux, _)) = typ_of_annot annot in
+ let identity = (fun body -> body) in
+ match paux, taux with
+ | P_tup [], _ ->
+ let annot = (l, Some (Env.empty, unit_typ, no_effect)) in
+ [P_aux (P_lit (mk_lit L_unit), annot)], identity
+ | P_tup pats, _ -> pats, identity
+ | P_wild, Typ_tup typs ->
+ let wild typ = P_aux (P_wild, (l, Some (env, typ, no_effect))) in
+ List.map wild typs, identity
+ | P_typ (_, pat), _ -> untuple_args_pat pat
+ | P_as _, Typ_tup _ | P_id _, Typ_tup _ ->
+ let argpats, argexps = args_of_typ l env (pat_typ_of pat) in
+ let argexp = E_aux (E_tuple argexps, annot) in
+ let bindargs (E_aux (_, bannot) as body) =
+ E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in
+ argpats, bindargs
+ | _, _ ->
+ [pat], identity
+
let doc_rec_lem (Rec_aux(r,_)) = match r with
| Rec_nonrec -> space
| Rec_rec -> space ^^ string "rec" ^^ space
-let doc_tannot_opt_lem sequential mwords (Typ_annot_opt_aux(t,_)) = match t with
- | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem sequential mwords typ)
+let doc_tannot_opt_lem (Typ_annot_opt_aux(t,_)) = match t with
+ | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem typ)
-let doc_fun_body_lem sequential mwords exp =
+let doc_fun_body_lem exp =
let early_ret =contains_early_return exp in
- let doc_exp = doc_exp_lem sequential mwords early_ret false exp in
+ let doc_exp = doc_exp_lem early_ret false exp in
if early_ret
then align (string "catch_early_return" ^//^ parens (doc_exp))
else doc_exp
-let doc_funcl_lem sequential mwords (FCL_aux(FCL_Funcl(id,pexp),_)) =
+let doc_funcl_lem (FCL_aux(FCL_Funcl(id,pexp),_)) =
let pat,guard,exp,(l,_) = destruct_pexp pexp in
+ let pats, bind = untuple_args_pat pat in
+ let patspp = separate_map space (doc_pat_lem true) pats in
let _ = match guard with
| None -> ()
| _ ->
raise (Reporting_basic.err_unreachable l
- "guarded pattern expression should have been rewritten before pretty-printing")
- in
- group (prefix 3 1 ((doc_pat_lem sequential mwords false pat) ^^ space ^^ arrow)
- (doc_fun_body_lem sequential mwords exp))
+ "guarded pattern expression should have been rewritten before pretty-printing") in
+ group (prefix 3 1
+ (separate space [doc_id_lem id; patspp; equals])
+ (doc_fun_body_lem (bind exp)))
let get_id = function
| [] -> failwith "FD_function with empty list"
@@ -1183,39 +1241,16 @@ let get_id = function
module StringSet = Set.Make(String)
-let doc_fundef_rhs_lem sequential mwords (FD_aux(FD_function(r, typa, efa, funcls),fannot) as fd) =
- match funcls with
- | [] -> failwith "FD_function with empty function list"
- | [FCL_aux(FCL_Funcl(id,pexp),_)] ->
- let pat,guard,exp,(l,_) = destruct_pexp pexp in
- let _ = match guard with
- | None -> ()
- | _ ->
- raise (Reporting_basic.err_unreachable l
- "guarded pattern expression should have been rewritten before pretty-printing")
- in
- (prefix 2 1)
- ((separate space)
- [doc_id_lem id;
- (doc_pat_lem sequential mwords true pat);
- equals])
- (doc_fun_body_lem sequential mwords exp)
- | _ ->
- let clauses =
- (separate_map (break 1))
- (fun fcl -> separate space [pipe;doc_funcl_lem sequential mwords fcl]) funcls in
- (prefix 2 1)
- ((separate space) [doc_id_lem (id_of_fundef fd);equals;string "function"])
- (clauses ^/^ string "end")
+let doc_fundef_rhs_lem (FD_aux(FD_function(r, typa, efa, funcls),fannot) as fd) =
+ separate_map (hardline ^^ string "and ") doc_funcl_lem funcls
-let doc_mutrec_lem sequential mwords = function
+let doc_mutrec_lem = function
| [] -> failwith "DEF_internal_mutrec with empty function list"
| fundefs ->
string "let rec " ^^
- separate_map (hardline ^^ string "and ")
- (doc_fundef_rhs_lem sequential mwords) fundefs
+ separate_map (hardline ^^ string "and ") doc_fundef_rhs_lem fundefs
-let rec doc_fundef_lem sequential mwords (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) =
+let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) =
match fcls with
| [] -> failwith "FD_function with empty function list"
| FCL_aux (FCL_Funcl(id,_),_) :: _
@@ -1244,14 +1279,16 @@ let rec doc_fundef_lem sequential mwords (FD_aux(FD_function(r, typa, efa, fcls)
if StringSet.mem candidate already_used then
pick_name_not_clashing_with already_used (candidate ^ "'")
else candidate in
+ let unit_pat = P_aux (P_lit (mk_lit L_unit), (l, Some (Env.empty, unit_typ, no_effect))) in
let aux_fname = pick_name_not_clashing_with already_used_fnames (string_of_id id ^ "_" ^ ctor) in
+ let aux_args = if argspat = [] then unit_pat else P_aux (P_tup argspat,pannot) in
let already_used_fnames = StringSet.add aux_fname already_used_fnames in
let fcl = FCL_aux (FCL_Funcl (Id_aux (Id aux_fname,l),
- Pat_aux (Pat_exp (P_aux (P_tup argspat,pannot),exp),(pexp_l,None)))
+ Pat_aux (Pat_exp (aux_args,exp),(pexp_l,None)))
,annot) in
let auxiliary_functions =
auxiliary_functions ^^ hardline ^^ hardline ^^
- doc_fundef_lem sequential mwords (FD_aux (FD_function(r,typa,efa,[fcl]),fannot)) in
+ doc_fundef_lem (FD_aux (FD_function(r,typa,efa,[fcl]),fannot)) in
(* Bind complex patterns to names so that we can pass them to the
auxiliary function *)
let name_pat idx (P_aux (p,a)) = match p with
@@ -1261,17 +1298,18 @@ let rec doc_fundef_lem sequential mwords (FD_aux(FD_function(r, typa, efa, fcls)
| _ -> P_aux (P_as (P_aux (p,a), Id_aux (Id ("arg" ^ string_of_int idx),l)),a) in
let named_argspat = List.mapi name_pat argspat in
let named_pat = P_aux (P_app (Id_aux (Id ctor,l),named_argspat),pannot) in
+ let named_args = if argspat = [] then [unit_pat] else named_argspat in
let doc_arg idx (P_aux (p,(l,a))) = match p with
| P_as (pat,id) -> doc_id_lem id
- | P_lit lit -> doc_lit_lem sequential mwords false lit a
+ | P_lit lit -> doc_lit_lem false lit a
| P_id id -> doc_id_lem id
| _ -> string ("arg" ^ string_of_int idx) in
let clauses =
clauses ^^ (break 1) ^^
(separate space
- [pipe;doc_pat_lem sequential mwords false named_pat;arrow;
+ [pipe;doc_pat_lem false named_pat;arrow;
string aux_fname;
- parens (separate comma (List.mapi doc_arg named_argspat))]) in
+ separate space (List.mapi doc_arg named_args)]) in
(already_used_fnames,auxiliary_functions,clauses)
) (StringSet.empty,empty,empty) fcls in
@@ -1281,60 +1319,45 @@ let rec doc_fundef_lem sequential mwords (FD_aux(FD_function(r, typa, efa, fcls)
(clauses ^/^ string "end")
| FCL_aux (FCL_Funcl(id,_),annot) :: _
when not (Env.is_extern id (env_of_annot annot) "lem") ->
- string "let" ^^ (doc_rec_lem r) ^^ (doc_fundef_rhs_lem sequential mwords fd)
+ string "let" ^^ (doc_rec_lem r) ^^ (doc_fundef_rhs_lem fd)
| _ -> empty
-let doc_dec_lem sequential (DEC_aux (reg, ((l, _) as annot))) =
+let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
match reg with
| DEC_reg(typ,id) ->
- if sequential then empty
+ if !opt_sequential then empty
else
let env = env_of_annot annot in
- (match typ with
- | _ ->
- let rt = Env.base_typ_of env typ in
- if is_vector_typ rt then
- let (start, size, order, etyp) = vector_typ_args_of rt in
- if is_bit_typ etyp && is_nexp_constant start && is_nexp_constant size then
- let o = if is_order_inc order then "true" else "false" in
- (doc_op equals)
- (string "let" ^^ space ^^ doc_id_lem id)
- (string "Register" ^^ space ^^
- align (separate space [string_lit(doc_id_lem id);
- doc_nexp (size);
- doc_nexp (start);
- string o;
- string "[]"]))
- ^/^ hardline
- else raise (Reporting_basic.err_unreachable l
- ("can't deal with register type " ^ string_of_typ typ))
- else raise (Reporting_basic.err_unreachable l
- ("can't deal with register type " ^ string_of_typ typ)))
+ let rt = Env.base_typ_of env typ in
+ if is_vector_typ rt then
+ let (start, size, order, etyp) = vector_typ_args_of rt in
+ if is_bit_typ etyp && is_nexp_constant start && is_nexp_constant size then
+ let o = if is_order_inc order then "true" else "false" in
+ (doc_op equals)
+ (string "let" ^^ space ^^ doc_id_lem id)
+ (string "Register" ^^ space ^^
+ align (separate space [string_lit(doc_id_lem id);
+ doc_nexp (size);
+ doc_nexp (start);
+ string o;
+ string "[]"]))
+ ^/^ hardline
+ else raise (Reporting_basic.err_unreachable l ("can't deal with register type " ^ string_of_typ typ))
+ else raise (Reporting_basic.err_unreachable l ("can't deal with register type " ^ string_of_typ typ))
| DEC_alias(id,alspec) -> empty
| DEC_typ_alias(typ,id,alspec) -> empty
-let doc_spec_lem sequential mwords (VS_aux (valspec,annot)) =
+let doc_spec_lem (VS_aux (valspec,annot)) =
match valspec with
| VS_val_spec (typschm,id,ext,_) when ext "lem" = None ->
(* let (TypSchm_aux (TypSchm_ts (tq, typ), _)) = typschm in
- if contains_t_pp_var mwords typ then empty else *)
- separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem sequential mwords true typschm] ^/^ hardline
+ if contains_t_pp_var typ then empty else *)
+ separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem true typschm] ^/^ hardline
(* | VS_val_spec (_,_,Some _,_) -> empty *)
| _ -> empty
-let find_regtypes defs = []
- (*
- List.fold_left
- (fun acc def ->
- match def with
- | DEF_type (TD_aux(TD_register (Id_aux (Id tname, _), n1, n2, fields),_)) ->
- (tname, (n1, n2, fields)) :: acc
- | _ -> acc
- ) [] defs
- *)
-
let is_field_accessor regtypes fdef =
let is_field_of regtyp field =
List.exists (fun (tname, (_, _, fields)) -> tname = regtyp &&
@@ -1344,7 +1367,7 @@ let is_field_accessor regtypes fdef =
(access = "get" || access = "set") && is_field_of regtyp field
| _ -> false
-let doc_regtype_fields sequential mwords (tname, (n1, n2, fields)) =
+let doc_regtype_fields (tname, (n1, n2, fields)) =
let i1, i2 = match n1, n2 with
| Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> i1, i2
| _ -> raise (Reporting_basic.err_typ Parse_ast.Unknown
@@ -1366,48 +1389,48 @@ let doc_regtype_fields sequential mwords (tname, (n1, n2, fields)) =
mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown),
[mk_typ_arg (Typ_arg_typ (mk_id_typ (mk_id tname)));
mk_typ_arg (Typ_arg_typ ftyp)])) in
- let rfannot = doc_tannot_lem sequential mwords false reftyp in
+ let rfannot = doc_tannot_lem false reftyp in
doc_op equals
(concat [string "let "; parens (concat [string tname; underscore; doc_id_lem fid; rfannot])])
(concat [
space; langlebar; string " field_name = \"" ^^ doc_id_lem fid ^^ string "\";"; hardline;
space; space; space; string (" field_start = " ^ Big_int.to_string i ^ ";"); hardline;
space; space; space; string (" field_is_inc = " ^ dir ^ ";"); hardline;
- space; space; space; string (" get_field = (fun reg -> get_" ^ tname ^ "_" ^ string_of_id fid ^ "(reg));"); hardline;
- space; space; space; string (" set_field = (fun reg v -> set_" ^ tname ^ "_" ^ string_of_id fid ^ "(reg, v)) "); ranglebar])
+ space; space; space; string (" get_field = get_" ^ tname ^ "_" ^ string_of_id fid ^ ";"); hardline;
+ space; space; space; string (" set_field = set_" ^ tname ^ "_" ^ string_of_id fid ^ " "); ranglebar])
in
separate_map hardline doc_field fields
-let rec doc_def_lem sequential mwords regtypes def =
+let rec doc_def_lem regtypes def =
(* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *)
match def with
- | DEF_spec v_spec -> (empty,doc_spec_lem sequential mwords v_spec)
+ | DEF_spec v_spec -> (empty,doc_spec_lem v_spec)
| DEF_fixity _ -> (empty,empty)
| DEF_overload _ -> (empty,empty)
- | DEF_type t_def -> (group (doc_typdef_lem sequential mwords t_def) ^/^ hardline,empty)
- | DEF_reg_dec dec -> (group (doc_dec_lem sequential dec),empty)
+ | DEF_type t_def -> (group (doc_typdef_lem t_def) ^/^ hardline,empty)
+ | DEF_reg_dec dec -> (group (doc_dec_lem dec),empty)
| DEF_default df -> (empty,empty)
| DEF_fundef fdef ->
- let doc_fdef = group (doc_fundef_lem sequential mwords fdef) ^/^ hardline in
+ let doc_fdef = group (doc_fundef_lem fdef) ^/^ hardline in
if is_field_accessor regtypes fdef then (doc_fdef, empty) else (empty, doc_fdef)
| DEF_internal_mutrec fundefs ->
- (empty, doc_mutrec_lem sequential mwords fundefs ^/^ hardline)
- | DEF_val lbind -> (empty,group (doc_let_lem sequential mwords false lbind) ^/^ hardline)
+ (empty, doc_mutrec_lem fundefs ^/^ hardline)
+ | DEF_val lbind -> (empty,group (doc_let_lem false lbind) ^/^ hardline)
| DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point"
| DEF_kind _ -> (empty,empty)
| DEF_comm (DC_comm s) -> (empty,comment (string s))
| DEF_comm (DC_comm_struct d) ->
- let (typdefs,vdefs) = doc_def_lem sequential mwords regtypes d in
+ let (typdefs,vdefs) = doc_def_lem regtypes d in
(empty,comment (typdefs ^^ hardline ^^ vdefs))
-let doc_defs_lem sequential mwords (Defs defs) =
- let regtypes = find_regtypes defs in
- let field_refs = separate_map hardline (doc_regtype_fields sequential mwords) regtypes in
- let (typdefs,valdefs) = List.split (List.map (doc_def_lem sequential mwords regtypes) defs) in
+let doc_defs_lem (Defs defs) =
+ let regtypes = [] in
+ let field_refs = separate_map hardline doc_regtype_fields regtypes in
+ let (typdefs,valdefs) = List.split (List.map (doc_def_lem regtypes) defs) in
(separate empty typdefs ^^ field_refs, separate empty valdefs)
let find_registers (Defs defs) =
@@ -1422,7 +1445,13 @@ let find_registers (Defs defs) =
| _ -> acc
) [] defs
-let doc_regstate_lem mwords registers =
+let find_exc_typ (Defs defs) =
+ let is_exc_typ_def = function
+ | DEF_type td -> string_of_id (id_of_type_def td) = "exception"
+ | _ -> false in
+ if List.exists is_exc_typ_def defs then "exception" else "unit"
+
+let doc_regstate_lem registers =
let l = Parse_ast.Unknown in
let annot = (l, None) in
let regstate = match registers with
@@ -1446,21 +1475,16 @@ let doc_regstate_lem mwords registers =
| _ ->
let initreg (typ, id, env) =
let annot typ = Some (env, typ, no_effect) in
- let initval = undefined_of_typ mwords l annot typ in
+ let initval = undefined_of_typ !opt_mwords l annot typ in
FE_aux (FE_Fexp (id, initval), (l, annot typ)) in
E_aux (
E_record (FES_aux (FES_Fexps (List.map initreg registers, false), annot)),
(l, Some (Env.empty, mk_id_typ (mk_id "regstate"), no_effect)))
in
- doc_op equals (string "let initial_regstate") (doc_exp_lem true mwords false false exp)
+ doc_op equals (string "let initial_regstate") (doc_exp_lem false false exp)
else empty
in
- concat [
- doc_typdef_lem true mwords (TD_aux (regstate, annot)); hardline;
- hardline;
- string "type _MR 'a 'r = MR regstate 'a 'r"; hardline;
- string "type _M 'a = M regstate 'a"
- ],
+ doc_typdef_lem (TD_aux (regstate, annot)),
initregstate
let doc_register_refs_lem registers =
@@ -1486,11 +1510,12 @@ let doc_register_refs_lem registers =
string " write_to = (fun s v -> (<| s with "; field; string " = v |>)) |>"] in
separate_map hardline doc_register_ref registers
-let pp_defs_lem sequential mwords (types_file,types_modules) (defs_file,defs_modules) d top_line =
+let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) d top_line =
(* let regtypes = find_regtypes d in *)
- let (typdefs,valdefs) = doc_defs_lem sequential mwords d in
- let regstate_def, initregstate_def = doc_regstate_lem mwords (find_registers d) in
+ let (typdefs,valdefs) = doc_defs_lem d in
+ let regstate_def, initregstate_def = doc_regstate_lem (find_registers d) in
let register_refs = doc_register_refs_lem (find_registers d) in
+ let exc_typ = find_exc_typ d in
(print types_file)
(concat
[string "(*" ^^ (string top_line) ^^ string "*)";hardline;
@@ -1510,12 +1535,19 @@ let pp_defs_lem sequential mwords (types_file,types_modules) (defs_file,defs_mod
else empty;
typdefs; hardline;
hardline;
- if sequential then
+ if !opt_sequential then
concat [regstate_def; hardline;
- hardline;
- register_refs]
+ hardline;
+ string ("type MR 'a 'r = State.MR regstate 'a 'r " ^ exc_typ); hardline;
+ string ("type M 'a = State.M regstate 'a " ^ exc_typ); hardline;
+ hardline;
+ register_refs
+ ]
else
- concat [string "type _MR 'a 'r = MR 'a 'r"; hardline; string "type _M 'a = M 'a"; hardline]
+ concat [
+ string ("type MR 'a 'r = Prompt.MR 'a 'r " ^ exc_typ); hardline;
+ string ("type M 'a = Prompt.M 'a " ^ exc_typ); hardline
+ ]
]);
(print defs_file)
(concat
diff --git a/src/process_file.ml b/src/process_file.ml
index 7a4f71e3..ca23d876 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -53,7 +53,7 @@ let opt_lem_mwords = ref false
type out_type =
| Lem_ast_out
- | Lem_out of string option
+ | Lem_out of string list
let get_lexbuf f =
let in_chan = open_in f in
@@ -101,7 +101,7 @@ let opt_dmono_analysis = ref 0
let opt_auto_mono = ref false
let monomorphise_ast locs type_env ast =
- let ast = Monomorphise.monomorphise (!opt_lem_mwords) (!opt_auto_mono) (!opt_dmono_analysis)
+ let ast = Monomorphise.monomorphise (!Pretty_print_lem.opt_mwords) (!opt_auto_mono) (!opt_dmono_analysis)
locs type_env ast in
let () = if !opt_ddump_raw_mono_ast then Pretty_print_sail.pp_defs stdout ast else () in
let ienv = Type_check.Env.no_casts Type_check.initial_env in
@@ -130,10 +130,10 @@ let generated_line f =
let output_lem filename libs defs =
let generated_line = generated_line filename in
- let seq_suffix = if !opt_lem_sequential then "_sequential" else "" in
+ let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in
let types_module = (filename ^ "_embed_types" ^ seq_suffix) in
- let monad_module = if !opt_lem_sequential then "State" else "Prompt" in
- let operators_module = if !opt_lem_mwords then "Sail_operators_mwords" else "Sail_operators" in
+ let monad_module = if !Pretty_print_lem.opt_sequential then "State" else "Prompt" in
+ let operators_module = if !Pretty_print_lem.opt_mwords then "Sail_operators_mwords" else "Sail_operators" in
let libs = List.map (fun lib -> lib ^ seq_suffix) libs in
let base_imports = [
"Pervasives_extra";
@@ -146,7 +146,7 @@ let output_lem filename libs defs =
open_output_with_check_unformatted (filename ^ "_embed_types" ^ seq_suffix ^ ".lem") in
let ((o,_, _) as ext_o) =
open_output_with_check_unformatted (filename ^ "_embed" ^ seq_suffix ^ ".lem") in
- (Pretty_print.pp_defs_lem !opt_lem_sequential !opt_lem_mwords
+ (Pretty_print.pp_defs_lem
(ot, base_imports)
(o, base_imports @ (String.capitalize types_module :: libs))
defs generated_line);
@@ -172,10 +172,8 @@ let output1 libpath out_arg filename defs =
Pretty_print.pp_lem_defs o defs;
close_output_with_check ext_o
end
- | Lem_out None ->
- output_lem f' [] defs
- | Lem_out (Some lib) ->
- output_lem f' [lib] defs
+ | Lem_out libs ->
+ output_lem f' libs defs
let output libpath out_arg files =
List.iter
@@ -204,7 +202,7 @@ let rewrite rewriters defs =
raise (Reporting_basic.err_typ l (Type_check.string_of_type_error err))
let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
-let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !opt_lem_mwords x)]
+let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !Pretty_print_lem.opt_mwords x)]
let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem
let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml
let rewrite_ast_interpreter = rewrite Rewrites.rewrite_defs_interpreter
diff --git a/src/process_file.mli b/src/process_file.mli
index ee021e61..1d98afc6 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -75,7 +75,7 @@ val opt_auto_mono : bool ref
type out_type =
| Lem_ast_out
- | Lem_out of string option (* If present, the string is a file to open in the lem backend*)
+ | Lem_out of string list (* If present, the strings are files to open in the lem backend*)
val output :
string -> (* The path to the library *)
diff --git a/src/rewriter.ml b/src/rewriter.ml
index e0297ae0..9e9409ec 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -134,8 +134,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
List.fold_left union_effects (effect_of e) (List.map effect_of_pexp pexps)
| E_let (lb,e) -> union_effects (effect_of_lb lb) (effect_of e)
| E_assign (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e)
- | E_exit e | E_throw e -> union_effects eff (effect_of e)
- | E_return e -> union_effects eff (effect_of e)
+ | E_exit e | E_return e | E_throw e -> union_effects eff (effect_of e)
| E_sizeof _ | E_sizeof_internal _ | E_constraint _ -> no_effect
| E_assert (c,m) -> union_effects eff (union_eff_exps [c; m])
| E_comment _ | E_comment_struc _ -> no_effect
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 3b74d38a..e14ced08 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1031,6 +1031,12 @@ let bitwise_and_exp exp1 exp2 =
let andid = Id_aux (Id "and_bool", gen_loc l) in
annot_exp (E_app(andid,[exp1;exp2])) l (env_of exp1) bool_typ
+let compose_guard_opt g1 g2 = match g1, g2 with
+ | Some g1, Some g2 -> Some (bitwise_and_exp g1 g2)
+ | Some g1, None -> Some g1
+ | None, Some g2 -> Some g2
+ | None, None -> None
+
let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with
| P_lit _ | P_wild | P_id _ -> false
| P_as (pat,_) | P_typ (_,pat) | P_var (pat,_) -> contains_bitvector_pat pat
@@ -1125,13 +1131,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
annot_exp (E_let (letbind,body)) l env (typ_of body)) in
(letexp, letbind) in
- let compose_guards guards =
- let conj g1 g2 = match g1, g2 with
- | Some g1, Some g2 -> Some (bitwise_and_exp g1 g2)
- | Some g1, None -> Some g1
- | None, Some g2 -> Some g2
- | None, None -> None in
- List.fold_right conj guards None in
+ let compose_guards guards = List.fold_right compose_guard_opt guards None in
let flatten_guards_decls gd =
let (guards,decls,letbinds) = Util.split3 gd in
@@ -1297,6 +1297,38 @@ let rewrite_defs_remove_bitvector_pats (Defs defs) =
Defs (List.flatten (List.map rewrite_def defs))
(* )) *)
+(* Rewrite literal number patterns to guarded patterns
+ Those numeral patterns are not handled very well by Lem (or Isabelle)
+ *)
+let rewrite_defs_remove_numeral_pats =
+ let p_lit = function
+ | L_aux (L_num n, l) ->
+ let id = fresh_id "l__" Parse_ast.Unknown in
+ let annot_exp e_aux typ = E_aux (e_aux, simple_annot l typ) in
+ let guard =
+ annot_exp (E_app_infix (
+ annot_exp (E_id id) (atom_typ (nconstant n)),
+ mk_id "==",
+ simple_num l n
+ )) bool_typ in
+ (Some guard, P_id id)
+ | lit -> (None, P_lit lit) in
+ let guard_pat =
+ fold_pat { (compute_pat_alg None compose_guard_opt) with p_lit = p_lit } in
+ let pat_aux (pexp_aux, a) =
+ let pat,guard,exp,a = destruct_pexp (Pat_aux (pexp_aux, a)) in
+ let guard',pat = guard_pat pat in
+ match compose_guard_opt guard guard' with
+ | Some g -> Pat_aux (Pat_when (pat, g, exp), a)
+ | None -> Pat_aux (Pat_exp (pat, exp), a) in
+ let exp_alg = { id_exp_alg with pat_aux = pat_aux } in
+ let rewrite_exp _ = fold_exp exp_alg in
+ let rewrite_funcl (FCL_aux (FCL_Funcl (id, pexp), annot)) =
+ FCL_aux (FCL_Funcl (id, fold_pexp exp_alg pexp), annot) in
+ let rewrite_fun _ (FD_aux (FD_function (r_o, t_o, e_o, funcls), a)) =
+ FD_aux (FD_function (r_o, t_o, e_o, List.map rewrite_funcl funcls), a) in
+ rewrite_defs_base
+ { rewriters_base with rewrite_exp = rewrite_exp; rewrite_fun = rewrite_fun }
(* Remove pattern guards by rewriting them to if-expressions within the
pattern expression. *)
@@ -2302,7 +2334,7 @@ let rewrite_defs_letbind_effects =
n_pexpL newreturn pexps (fun pexps ->
k (rewrap (E_case (exp1,pexps)))))
| E_try (exp1,pexps) ->
- let newreturn = List.exists effectful_pexp pexps in
+ let newreturn = effectful exp1 || List.exists effectful_pexp pexps in
n_exp_name exp1 (fun exp1 ->
n_pexpL newreturn pexps (fun pexps ->
k (rewrap (E_try (exp1,pexps)))))
@@ -2320,7 +2352,6 @@ let rewrite_defs_letbind_effects =
n_exp_name exp1 (fun exp1 ->
k (rewrap (E_assign (lexp,exp1)))))
| E_exit exp' -> k (E_aux (E_exit (n_exp_term (effectful exp') exp'),annot))
- | E_throw exp' -> k (E_aux (E_throw (n_exp_term (effectful exp') exp'),annot))
| E_assert (exp1,exp2) ->
n_exp_name exp1 (fun exp1 ->
n_exp_name exp2 (fun exp2 ->
@@ -2347,6 +2378,9 @@ let rewrite_defs_letbind_effects =
| E_return exp' ->
n_exp_name exp' (fun exp' ->
k (rewrap (E_return exp')))
+ | E_throw exp' ->
+ n_exp_name exp' (fun exp' ->
+ k (rewrap (E_throw exp')))
| E_internal_plet _ -> failwith "E_internal_plet should not be here yet" in
let rewrite_fun _ (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),fdannot)) =
@@ -2884,6 +2918,7 @@ let rewrite_defs_lem = [
(* ("simple_assignments", rewrite_simple_assignments); *)
("remove_vector_concat", rewrite_defs_remove_vector_concat);
("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats);
+ ("remove_numeral_pats", rewrite_defs_remove_numeral_pats);
("guarded_pats", rewrite_defs_guarded_pats);
("exp_lift_assign", rewrite_defs_exp_lift_assign);
("register_ref_writes", rewrite_register_ref_writes);
diff --git a/src/sail.ml b/src/sail.ml
index e9e55487..41ca792c 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -96,10 +96,10 @@ let options = Arg.align ([
Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem),
"<filename> provide additional library to open in Lem output");
( "-lem_sequential",
- Arg.Set Process_file.opt_lem_sequential,
+ Arg.Set Pretty_print_lem.opt_sequential,
" use sequential state monad for Lem output");
( "-lem_mwords",
- Arg.Set Process_file.opt_lem_mwords,
+ Arg.Set Pretty_print_lem.opt_mwords,
" use native machine word library for Lem output");
( "-mono-split",
Arg.String (fun s ->
@@ -231,9 +231,7 @@ let main() =
else ());
(if !(opt_print_lem)
then let ast_lem = rewrite_ast_lem ast in
- if !(opt_libs_lem) = []
- then output "" (Lem_out None) [out_name,ast_lem]
- else output "" (Lem_out (Some (List.hd !opt_libs_lem))) [out_name,ast_lem]
+ output "" (Lem_out (!opt_libs_lem)) [out_name,ast_lem]
else ());
end
diff --git a/src/type_check.ml b/src/type_check.ml
index 66805ba5..30845727 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1528,6 +1528,39 @@ let uv_nexp_constraint env (kid, uvar) =
| U_nexp nexp -> Env.add_constraint (nc_eq (nvar kid) nexp) env
| _ -> env
+(* The kid_order function takes a set of Int-kinded kids, and returns
+ a list of those kids in the order they appear in a type, as well as
+ a set containing all the kids that did not occur in the type. We
+ only care about Int-kinded kids because those are the only type
+ that can appear in an existential. *)
+
+let rec kid_order_nexp kids (Nexp_aux (aux, l) as nexp) =
+ match aux with
+ | Nexp_var kid when KidSet.mem kid kids -> ([kid], KidSet.remove kid kids)
+ | Nexp_var _ | Nexp_id _ | Nexp_constant _ -> ([], kids)
+ | Nexp_exp nexp | Nexp_neg nexp -> kid_order_nexp kids nexp
+ | Nexp_times (nexp1, nexp2) | Nexp_sum (nexp1, nexp2) | Nexp_minus (nexp1, nexp2) ->
+ let (ord, kids) = kid_order_nexp kids nexp1 in
+ let (ord', kids) = kid_order_nexp kids nexp2 in
+ (ord @ ord', kids)
+ | Nexp_app (id, nexps) ->
+ List.fold_left (fun (ord, kids) nexp -> let (ord', kids) = kid_order_nexp kids nexp in (ord @ ord', kids)) ([], kids) nexps
+
+let rec kid_order kids (Typ_aux (aux, l) as typ) =
+ match aux with
+ | Typ_var kid when KidSet.mem kid kids -> ([kid], KidSet.remove kid kids)
+ | Typ_id _ | Typ_var _ -> ([], kids)
+ | Typ_tup typs ->
+ List.fold_left (fun (ord, kids) typ -> let (ord', kids) = kid_order kids typ in (ord @ ord', kids)) ([], kids) typs
+ | Typ_app (_, args) ->
+ List.fold_left (fun (ord, kids) arg -> let (ord', kids) = kid_order_arg kids arg in (ord @ ord', kids)) ([], kids) args
+ | Typ_fn _ | Typ_exist _ -> typ_error l ("Existential or function type cannot appear within existential type: " ^ string_of_typ typ)
+and kid_order_arg kids (Typ_arg_aux (aux, l) as arg) =
+ match aux with
+ | Typ_arg_typ typ -> kid_order kids typ
+ | Typ_arg_nexp nexp -> kid_order_nexp kids nexp
+ | Typ_arg_order _ -> ([], kids)
+
let rec alpha_equivalent env typ1 typ2 =
let counter = ref 0 in
let new_kid () = let kid = mk_kid ("alpha#" ^ string_of_int !counter) in (incr counter; kid) in
@@ -1542,7 +1575,9 @@ let rec alpha_equivalent env typ1 typ2 =
let kids = List.map (fun kid -> (kid, new_kid ())) kids in
let nc = List.fold_left (fun nc (kid, nk) -> nc_subst_nexp kid (Nexp_var nk) nc) nc kids in
let typ = List.fold_left (fun nc (kid, nk) -> typ_subst_nexp kid (Nexp_var nk) nc) typ kids in
- Typ_exist (List.map snd kids, nc, typ)
+ let kids = List.map snd kids in
+ let (kids, _) = kid_order (KidSet.of_list kids) typ in
+ Typ_exist (kids, nc, typ)
| Typ_app (id, args) ->
Typ_app (id, List.map relabel_arg args)
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:39:07 +0000