summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml11
-rw-r--r--src/c_backend.ml2
-rw-r--r--src/elf_loader.ml8
-rw-r--r--src/gen_lib/prompt.lem6
-rw-r--r--src/gen_lib/sail_operators.lem12
-rw-r--r--src/gen_lib/sail_operators_bitlists.lem17
-rw-r--r--src/gen_lib/sail_operators_mwords.lem17
-rw-r--r--src/gen_lib/sail_values.lem1
-rw-r--r--src/gen_lib/state_monad.lem13
-rw-r--r--src/initial_check.ml60
-rw-r--r--src/interpreter.ml9
-rw-r--r--src/latex.ml2
-rw-r--r--src/monomorphise.ml22
-rw-r--r--src/parse_ast.ml1
-rw-r--r--src/parser.mly12
-rw-r--r--src/pretty_print_coq.ml1410
-rw-r--r--src/pretty_print_lem.ml77
-rw-r--r--src/pretty_print_sail.ml1
-rw-r--r--src/process_file.ml26
-rw-r--r--src/process_file.mli2
-rw-r--r--src/rewriter.ml102
-rw-r--r--src/rewriter.mli16
-rw-r--r--src/rewrites.ml140
-rw-r--r--src/sail.ml17
-rw-r--r--src/state.ml210
-rw-r--r--src/type_check.ml282
-rw-r--r--src/type_check.mli21
-rw-r--r--src/value.ml4
28 files changed, 2217 insertions, 284 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 98fc6bde..7af1b006 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -477,6 +477,7 @@ and map_lexp_annot_aux f = function
| LEXP_memory (id, exps) -> LEXP_memory (id, List.map (map_exp_annot f) exps)
| LEXP_cast (typ, id) -> LEXP_cast (typ, id)
| LEXP_tup lexps -> LEXP_tup (List.map (map_lexp_annot f) lexps)
+ | LEXP_vector_concat lexps -> LEXP_vector_concat (List.map (map_lexp_annot f) lexps)
| LEXP_vector (lexp, exp) -> LEXP_vector (map_lexp_annot f lexp, map_exp_annot f exp)
| LEXP_vector_range (lexp, exp1, exp2) -> LEXP_vector_range (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2)
| LEXP_field (lexp, id) -> LEXP_field (map_lexp_annot f lexp, id)
@@ -675,8 +676,8 @@ let rec string_of_exp (E_aux (exp, _)) =
| E_try (exp, cases) ->
"try " ^ string_of_exp exp ^ " catch { case " ^ string_of_list " case " string_of_pexp cases ^ "}"
| E_let (letbind, exp) -> "let " ^ string_of_letbind letbind ^ " in " ^ string_of_exp exp
- | E_assign (lexp, bind) -> string_of_lexp lexp ^ " := " ^ string_of_exp bind
- | E_cast (typ, exp) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_exp exp
+ | E_assign (lexp, bind) -> string_of_lexp lexp ^ " = " ^ string_of_exp bind
+ | E_cast (typ, exp) -> string_of_exp exp ^ " : " ^ string_of_typ typ
| E_vector vec -> "[" ^ string_of_list ", " string_of_exp vec ^ "]"
| E_vector_access (v, n) -> string_of_exp v ^ "[" ^ string_of_exp n ^ "]"
| E_vector_update (v, n, exp) -> "[" ^ string_of_exp v ^ " with " ^ string_of_exp n ^ " = " ^ string_of_exp exp ^ "]"
@@ -732,7 +733,7 @@ and string_of_pat (P_aux (pat, l)) =
| P_wild -> "_"
| P_id v -> string_of_id v
| P_var (pat, tpat) -> string_of_pat pat ^ " as " ^ string_of_typ_pat tpat
- | P_typ (typ, pat) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_pat pat
+ | P_typ (typ, pat) -> string_of_pat pat ^ " : " ^ string_of_typ typ
| P_tup pats -> "(" ^ string_of_list ", " string_of_pat pats ^ ")"
| P_app (f, pats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_pat pats ^ ")"
| P_cons (pat1, pat2) -> string_of_pat pat1 ^ " :: " ^ string_of_pat pat2
@@ -765,7 +766,9 @@ and string_of_lexp (LEXP_aux (lexp, _)) =
| LEXP_tup lexps -> "(" ^ string_of_list ", " string_of_lexp lexps ^ ")"
| LEXP_vector (lexp, exp) -> string_of_lexp lexp ^ "[" ^ string_of_exp exp ^ "]"
| LEXP_vector_range (lexp, exp1, exp2) ->
- string_of_lexp lexp ^ "[" ^ string_of_exp exp1 ^ ".." ^ string_of_exp exp2 ^ "]"
+ string_of_lexp lexp ^ "[" ^ string_of_exp exp1 ^ " .. " ^ string_of_exp exp2 ^ "]"
+ | LEXP_vector_concat lexps ->
+ string_of_list " @ " string_of_lexp lexps
| LEXP_field (lexp, id) -> string_of_lexp lexp ^ "." ^ string_of_id id
| LEXP_memory (f, xs) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"
and string_of_letbind (LB_aux (lb, l)) =
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 5cf282f9..23a8c92e 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1927,7 +1927,7 @@ and compile_block ctx = function
let setup, _, call, cleanup = compile_aexp ctx exp in
let rest = compile_block ctx exps in
let gs = gensym () in
- setup @ [idecl CT_unit gs; call (CL_id gs)] @ cleanup @ rest
+ iblock (setup @ [idecl CT_unit gs; call (CL_id gs)] @ cleanup) :: rest
(** Compile a sail type definition into a IR one. Most of the
actual work of translating the typedefs into C is done by the code
diff --git a/src/elf_loader.ml b/src/elf_loader.ml
index 89987647..02ff072b 100644
--- a/src/elf_loader.ml
+++ b/src/elf_loader.ml
@@ -65,9 +65,9 @@ let rec break n = function
| (_ :: _ as xs) -> [Lem_list.take n xs] @ break n (Lem_list.drop n xs)
let print_segment seg =
- let (Byte_sequence.Sequence bs) = seg.Elf_interpreted_segment.elf64_segment_body in
+ let bs = seg.Elf_interpreted_segment.elf64_segment_body in
prerr_endline "0011 2233 4455 6677 8899 aabb ccdd eeff 0123456789abcdef";
- List.iter (fun bs -> prerr_endline (hex_line bs)) (break 16 bs)
+ List.iter (fun bs -> prerr_endline (hex_line bs)) (break 16 (Byte_sequence.char_list_of_byte_sequence bs))
let read name =
let info = Sail_interface.populate_and_obtain_global_symbol_init_info name in
@@ -112,7 +112,7 @@ let write_file chan paddr i byte =
let load_segment ?writer:(writer=write_sail_lib) seg =
let open Elf_interpreted_segment in
- let (Byte_sequence.Sequence bs) = seg.elf64_segment_body in
+ let bs = seg.elf64_segment_body in
let paddr = seg.elf64_segment_paddr in
let base = seg.elf64_segment_base in
let offset = seg.elf64_segment_offset in
@@ -121,7 +121,7 @@ let load_segment ?writer:(writer=write_sail_lib) seg =
prerr_endline ("Segment base address: " ^ Big_int.to_string base);
prerr_endline ("Segment physical address: " ^ Big_int.to_string paddr);
print_segment seg;
- List.iteri (writer paddr) (List.map int_of_char bs)
+ List.iteri (writer paddr) (List.map int_of_char (Byte_sequence.char_list_of_byte_sequence bs))
let load_elf ?writer:(writer=write_sail_lib) name =
let segments, e_entry, symbol_map = read name in
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index de683047..830f2350 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -38,6 +38,12 @@ end
declare {isabelle} termination_argument foreachM = automatic
+val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
+let and_boolM l r = l >>= (fun l -> if l then r else return false)
+
+val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
+let or_boolM l r = l >>= (fun l -> if l then return true else r)
+
val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e
let bool_of_bitU_fail = function
| B0 -> return false
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index d4275c87..78aab65e 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -223,3 +223,15 @@ let inline ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedInteger
val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool
let inline scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r)
+
+val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
+let get_slice_int_bv len n lo =
+ let hi = lo + len - 1 in
+ let bs = bools_of_int (hi + 1) n in
+ of_bools (subrange_list false bs hi lo)
+
+val set_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -> integer
+let set_slice_int_bv len n lo v =
+ let hi = lo + len - 1 in
+ let bs = bits_of_int (hi + 1) n in
+ maybe_failwith (signed_of_bits (update_subrange_list false bs hi lo (bits_of v)))
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem
index b0a29b5e..fed293b4 100644
--- a/src/gen_lib/sail_operators_bitlists.lem
+++ b/src/gen_lib/sail_operators_bitlists.lem
@@ -35,6 +35,9 @@ let zero_extend bits len = extz_bits len bits
val sign_extend : list bitU -> integer -> list bitU
let sign_extend bits len = exts_bits len bits
+val zeros : integer -> list bitU
+let zeros len = repeat [B0] len
+
val vector_truncate : list bitU -> integer -> list bitU
let vector_truncate bs len = extz_bv len bs
@@ -289,6 +292,20 @@ let duplicate_oracle b n =
val reverse_endianness : list bitU -> list bitU
let reverse_endianness v = reverse_endianness_list v
+val get_slice_int : integer -> integer -> integer -> list bitU
+let get_slice_int = get_slice_int_bv
+
+val set_slice_int : integer -> integer -> integer -> list bitU -> integer
+let set_slice_int = set_slice_int_bv
+
+val slice : list bitU -> integer -> integer -> list bitU
+let slice v lo len =
+ subrange_vec_dec v (lo + len - 1) lo
+
+val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU
+let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
+ update_subrange_vec_dec out (n + slice_len - 1) n v
+
val eq_vec : list bitU -> list bitU -> bool
val neq_vec : list bitU -> list bitU -> bool
val ult_vec : list bitU -> list bitU -> bool
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 8bcc0319..077dfb02 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -76,6 +76,9 @@ let zero_extend w _ = Machine_word.zeroExtend w
val sign_extend : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
let sign_extend w _ = Machine_word.signExtend w
+val zeros : forall 'a. Size 'a => integer -> mword 'a
+let zeros _ = Machine_word.wordFromNatural 0
+
val vector_truncate : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
let vector_truncate w _ = Machine_word.zeroExtend w
@@ -310,6 +313,20 @@ let duplicate b n = maybe_failwith (duplicate_maybe b n)
val reverse_endianness : forall 'a. Size 'a => mword 'a -> mword 'a
let reverse_endianness v = wordFromBitlist (reverse_endianness_list (bitlistFromWord v))
+val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a
+let get_slice_int = get_slice_int_bv
+
+val set_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a -> integer
+let set_slice_int = set_slice_int_bv
+
+val slice : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
+let slice v lo len =
+ subrange_vec_dec v (lo + len - 1) lo
+
+val set_slice : forall 'a 'b. Size 'a, Size 'b => integer -> integer -> mword 'a -> integer -> mword 'b -> mword 'a
+let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
+ update_subrange_vec_dec out (n + slice_len - 1) n v
+
val eq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val neq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
val ult_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 2d9eda9c..5c6dc593 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -414,6 +414,7 @@ let rec hexstring_of_bits bs = match bs with
| (Just n, Just s) -> Just (n :: s)
| _ -> Nothing
end
+ | [] -> Just []
| _ -> Nothing
end
declare {isabelle} termination_argument hexstring_of_bits = automatic
diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
index 8253b800..a2919762 100644
--- a/src/gen_lib/state_monad.lem
+++ b/src/gen_lib/state_monad.lem
@@ -265,3 +265,16 @@ let update_reg_field_bit regfield i reg_val bit =
let new_field_value = set_bit (regfield.field_is_inc) current_field_value i (to_bitU bit) in
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)*)
+
+(* TODO Add Show typeclass for value and exception type *)
+val show_result : forall 'a 'e. result 'a 'e -> string
+let show_result = function
+ | Value _ -> "Value ()"
+ | Ex (Failure msg) -> "Failure " ^ msg
+ | Ex (Throw _) -> "Throw"
+end
+
+val prerr_results : forall 'a 'e 's. SetType 's => set (result 'a 'e * 's) -> unit
+let prerr_results rs =
+ let _ = Set.map (fun (r, _) -> let _ = prerr_endline (show_result r) in ()) rs in
+ ()
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 51820b29..e1dd906b 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -542,35 +542,45 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
), (l,()))
and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit lexp =
- LEXP_aux(
- (match exp with
- | Parse_ast.E_id(id) -> LEXP_id(to_ast_id id)
- | Parse_ast.E_deref(exp) -> LEXP_deref(to_ast_exp k_env def_ord exp)
- | Parse_ast.E_cast(typ,Parse_ast.E_aux(Parse_ast.E_id(id),l')) ->
- LEXP_cast(to_ast_typ k_env def_ord typ, to_ast_id id)
- | Parse_ast.E_tuple(tups) ->
+ let lexp = match exp with
+ | Parse_ast.E_id id -> LEXP_id (to_ast_id id)
+ | Parse_ast.E_deref exp -> LEXP_deref (to_ast_exp k_env def_ord exp)
+ | Parse_ast.E_cast (typ, Parse_ast.E_aux (Parse_ast.E_id id, l')) ->
+ LEXP_cast (to_ast_typ k_env def_ord typ, to_ast_id id)
+ | Parse_ast.E_tuple tups ->
let ltups = List.map (to_ast_lexp k_env def_ord) tups in
- let is_ok_in_tup (LEXP_aux (le,(l,_))) =
+ let is_ok_in_tup (LEXP_aux (le, (l, _))) =
match le with
- | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> ()
+ | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_vector_concat _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> ()
| LEXP_memory _ | LEXP_deref _ ->
- typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None in
+ typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None
+ in
List.iter is_ok_in_tup ltups;
- LEXP_tup(ltups)
- | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),args) ->
- (match f with
- | Parse_ast.Id(id) ->
- (match List.map (to_ast_exp k_env def_ord) args with
- | [E_aux(E_lit (L_aux (L_unit, _)), _)] -> LEXP_memory(to_ast_id f',[])
- | [E_aux(E_tuple exps,_)] -> LEXP_memory(to_ast_id f',exps)
- | args -> LEXP_memory(to_ast_id f', args))
- | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None)
- | Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp)
- | Parse_ast.E_vector_subrange(vexp,exp1,exp2) ->
- LEXP_vector_range(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2)
- | Parse_ast.E_field(fexp,id) -> LEXP_field(to_ast_lexp k_env def_ord fexp, to_ast_id id)
- | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None)
- , (l,()))
+ LEXP_tup ltups
+ | Parse_ast.E_app ((Parse_ast.Id_aux (f, l') as f'), args) ->
+ begin match f with
+ | Parse_ast.Id(id) ->
+ (match List.map (to_ast_exp k_env def_ord) args with
+ | [E_aux (E_lit (L_aux (L_unit, _)), _)] -> LEXP_memory (to_ast_id f', [])
+ | [E_aux (E_tuple exps,_)] -> LEXP_memory (to_ast_id f', exps)
+ | args -> LEXP_memory(to_ast_id f', args))
+ | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None
+ end
+ | Parse_ast.E_vector_append (exp1, exp2) ->
+ LEXP_vector_concat (to_ast_lexp k_env def_ord exp1 :: to_ast_lexp_vector_concat k_env def_ord exp2)
+ | Parse_ast.E_vector_access (vexp, exp) -> LEXP_vector (to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp)
+ | Parse_ast.E_vector_subrange (vexp, exp1, exp2) ->
+ LEXP_vector_range (to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2)
+ | Parse_ast.E_field (fexp, id) -> LEXP_field (to_ast_lexp k_env def_ord fexp, to_ast_id id)
+ | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None
+ in
+ LEXP_aux (lexp, (l, ()))
+
+and to_ast_lexp_vector_concat k_env def_ord (Parse_ast.E_aux (exp_aux, l) as exp) =
+ match exp_aux with
+ | Parse_ast.E_vector_append (exp1, exp2) ->
+ to_ast_lexp k_env def_ord exp1 :: to_ast_lexp_vector_concat k_env def_ord exp2
+ | _ -> [to_ast_lexp k_env def_ord exp]
and to_ast_case (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : unit pexp =
match pex with
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 2b24d66c..e62fcfc3 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -257,7 +257,10 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| E_loop (Until, exp, body) -> wrap (E_block [body; E_aux (E_if (exp, orig_exp, exp_of_value V_unit), annot)])
| E_assert (exp, msg) when is_true exp -> wrap unit_exp
- | E_assert (exp, msg) when is_false exp -> assertion_failed "FIXME"
+ | E_assert (exp, msg) when is_false exp && is_value msg ->
+ failwith (coerce_string (value_of_exp msg))
+ | E_assert (exp, msg) when is_false exp ->
+ step msg >>= fun msg' -> wrap (E_assert (exp, msg'))
| E_assert (exp, msg) ->
step exp >>= fun exp' -> wrap (E_assert (exp', msg))
@@ -502,6 +505,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
else
puts (lstate, { gstate with boxes = StringMap.add name (value_of_exp exp) gstate.boxes }) >> wrap unit_exp
| E_assign (LEXP_aux (LEXP_tup lexps, annot), exp) -> failwith "Tuple assignment"
+ | E_assign (LEXP_aux (LEXP_vector_concat lexps, annot), exp) -> failwith "Vector concat assignment"
(*
let values = coerce_tuple (value_of_exp exp) in
wrap (E_block (List.map2 (fun lexp v -> E_aux (E_assign (lexp, exp_of_value v), (Parse_ast.Unknown, None))) lexps values))
@@ -553,6 +557,9 @@ and exp_of_lexp (LEXP_aux (lexp_aux, _) as lexp) =
| LEXP_tup lexps -> mk_exp (E_tuple (List.map exp_of_lexp lexps))
| LEXP_vector (lexp, exp) -> mk_exp (E_vector_access (exp_of_lexp lexp, exp))
| LEXP_vector_range (lexp, exp1, exp2) -> mk_exp (E_vector_subrange (exp_of_lexp lexp, exp1, exp2))
+ | LEXP_vector_concat [] -> failwith "Empty LEXP_vector_concat node in exp_of_lexp"
+ | LEXP_vector_concat [lexp] -> exp_of_lexp lexp
+ | LEXP_vector_concat (lexp :: lexps) -> mk_exp (E_vector_append (exp_of_lexp lexp, exp_of_lexp (mk_lexp (LEXP_vector_concat lexps))))
| LEXP_field (lexp, id) -> mk_exp (E_field (exp_of_lexp lexp, id))
and pattern_match env (P_aux (p_aux, _) as pat) value =
diff --git a/src/latex.ml b/src/latex.ml
index 01cf55b2..f16dddd8 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -134,7 +134,7 @@ let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l
let oc = open_out (Filename.concat dir (cmd ^ "_sail.tex")) in
output_string oc (Pretty_print_sail.to_string (latex_loc no_loc l));
close_out oc;
- string (Printf.sprintf "\\newcommand{\\%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting{%s/%s_sail.tex}}" dir cmd)
+ string (Printf.sprintf "\\newcommand{\\%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting[language=sail]{%s/%s_sail.tex}}" dir cmd)
end
let latex_command_id ?prefix:(prefix="") dir id no_loc annot =
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 75b82da2..0585d9fa 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -636,6 +636,7 @@ let nexp_subst_fns substs =
| LEXP_tup les -> re (LEXP_tup (List.map s_lexp les))
| LEXP_vector (le,e) -> re (LEXP_vector (s_lexp le, s_exp e))
| LEXP_vector_range (le,e1,e2) -> re (LEXP_vector_range (s_lexp le, s_exp e1, s_exp e2))
+ | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map s_lexp les))
| LEXP_field (le,id) -> re (LEXP_field (s_lexp le, id))
| LEXP_deref e -> re (LEXP_deref (s_exp e))
in (s_pat,s_exp)
@@ -955,7 +956,9 @@ let rec assigned_vars_in_lexp (LEXP_aux (le,_)) =
match le with
| LEXP_id id
| LEXP_cast (_,id) -> IdSet.singleton id
- | LEXP_tup lexps -> List.fold_left (fun vs le -> IdSet.union vs (assigned_vars_in_lexp le)) IdSet.empty lexps
+ | LEXP_tup lexps
+ | LEXP_vector_concat lexps ->
+ List.fold_left (fun vs le -> IdSet.union vs (assigned_vars_in_lexp le)) IdSet.empty lexps
| LEXP_memory (_,es) -> List.fold_left (fun vs e -> IdSet.union vs (assigned_vars e)) IdSet.empty es
| LEXP_vector (le,e) -> IdSet.union (assigned_vars_in_lexp le) (assigned_vars e)
| LEXP_vector_range (le,e1,e2) ->
@@ -1468,6 +1471,7 @@ let split_defs all_errors splits defs =
re (LEXP_vector_range (fst (const_prop_lexp ref_vars substs assigns le),
fst (const_prop_exp ref_vars substs assigns e1),
fst (const_prop_exp ref_vars substs assigns e2)))
+ | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map (fun le -> fst (const_prop_lexp ref_vars substs assigns le)) les))
| LEXP_field (le,id) -> re (LEXP_field (fst (const_prop_lexp ref_vars substs assigns le), id))
| LEXP_deref e ->
re (LEXP_deref (fst (const_prop_exp ref_vars substs assigns e)))
@@ -2014,6 +2018,7 @@ let split_defs all_errors splits defs =
| LEXP_tup les -> re (LEXP_tup (List.map map_lexp les))
| LEXP_vector (le,e) -> re (LEXP_vector (map_lexp le, map_exp e))
| LEXP_vector_range (le,e1,e2) -> re (LEXP_vector_range (map_lexp le, map_exp e1, map_exp e2))
+ | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map map_lexp les))
| LEXP_field (le,id) -> re (LEXP_field (map_lexp le, id))
| LEXP_deref e -> re (LEXP_deref (map_exp e))
in map_pexp, map_letbind
@@ -2354,10 +2359,20 @@ let rewrite_size_parameters env (Defs defs) =
| Some exp -> Some (fold_exp { id_exp_alg with e_app = rewrite_e_app } exp) in
FCL_aux (FCL_Funcl (id,construct_pexp (pat,guard,body,(pl,None))),(l,None))
in
+ let rewrite_letbind lb =
+ let rewrite_e_app (id,args) =
+ match Bindings.find id fn_sizes with
+ | to_change,_ ->
+ let args' = mapat (replace_with_the_value []) to_change args in
+ E_app (id,args')
+ | exception Not_found -> E_app (id,args)
+ in fold_letbind { id_exp_alg with e_app = rewrite_e_app } lb
+ in
let rewrite_def = function
| DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,funcls),(l,_))) ->
(* TODO rewrite tannopt? *)
DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,List.map rewrite_funcl funcls),(l,None)))
+ | DEF_val lb -> DEF_val (rewrite_letbind lb)
| DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,annot))) as spec ->
begin
match Bindings.find id fn_sizes with
@@ -3120,7 +3135,8 @@ and analyse_lexp fn_id env assigns deps (LEXP_aux (lexp,(l,_))) =
| LEXP_memory (id,es) ->
let _, assigns, r = analyse_exp fn_id env assigns (E_aux (E_tuple es,(Unknown,None))) in
assigns, r
- | LEXP_tup lexps ->
+ | LEXP_tup lexps
+ | LEXP_vector_concat lexps ->
List.fold_left (fun (assigns,r) lexp ->
let assigns,r' = analyse_lexp fn_id env assigns deps lexp
in assigns,merge r r') (assigns,empty) lexps
@@ -3775,7 +3791,7 @@ let make_bitvector_cast_fns env src_typ target_typ =
match src_t, tar_t with
| Typ_tup typs, Typ_tup typs' ->
let ps,es = List.split (List.map2 aux typs typs') in
- P_aux (P_tup ps,(Generated src_l, src_ann)),
+ P_aux (P_typ (src_typ, P_aux (P_tup ps,(Generated src_l, src_ann))),(Generated src_l, src_ann)),
E_aux (E_tuple es,(Generated tar_l, tar_ann))
| Typ_app (Id_aux (Id "vector",_),
[Typ_arg_aux (Typ_arg_nexp size,_); _;
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index a6b519e5..607285c7 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -564,6 +564,7 @@ lexp_aux = (* lvalue expression, can't occur out of the parser *)
| LEXP_mem of id * (exp) list
| LEXP_vector of lexp * exp (* vector element *)
| LEXP_vector_range of lexp * exp * exp (* subvector *)
+ | LEXP_vector_concat of lexp list
| LEXP_field of lexp * id (* struct field *)
and lexp =
diff --git a/src/parser.mly b/src/parser.mly
index cccd4a4a..a46defd6 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -61,9 +61,11 @@ let default_opt x = function
| None -> x
| Some y -> y
-let assoc_opt key assocs =
+let assoc_opt key (assocs, default) =
try Some (List.assoc key assocs) with
- | Not_found -> None
+ | Not_found -> default
+
+let cons_fst h (t,x) = (h::t,x)
let string_of_id = function
| Id_aux (Id str, _) -> str
@@ -1288,9 +1290,11 @@ let_def:
externs:
| id Colon String
- { [(string_of_id $1, $3)] }
+ { ([(string_of_id $1, $3)], None) }
+ | Under Colon String
+ { ([], Some $3) }
| id Colon String Comma externs
- { (string_of_id $1, $3) :: $5 }
+ { cons_fst (string_of_id $1, $3) $5 }
val_spec_def:
| Doc val_spec_def
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
new file mode 100644
index 00000000..a1133e09
--- /dev/null
+++ b/src/pretty_print_coq.ml
@@ -0,0 +1,1410 @@
+(**************************************************************************)
+(* Sail *)
+(* *)
+(* Copyright (c) 2013-2017 *)
+(* Kathyrn Gray *)
+(* Shaked Flur *)
+(* Stephen Kell *)
+(* Gabriel Kerneis *)
+(* Robert Norton-Wright *)
+(* Christopher Pulte *)
+(* Peter Sewell *)
+(* Alasdair Armstrong *)
+(* Brian Campbell *)
+(* Thomas Bauereiss *)
+(* Anthony Fox *)
+(* Jon French *)
+(* Dominic Mulligan *)
+(* Stephen Kell *)
+(* Mark Wassell *)
+(* *)
+(* All rights reserved. *)
+(* *)
+(* This software was developed by the University of Cambridge Computer *)
+(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
+(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
+(* *)
+(* Redistribution and use in source and binary forms, with or without *)
+(* modification, are permitted provided that the following conditions *)
+(* are met: *)
+(* 1. Redistributions of source code must retain the above copyright *)
+(* notice, this list of conditions and the following disclaimer. *)
+(* 2. Redistributions in binary form must reproduce the above copyright *)
+(* notice, this list of conditions and the following disclaimer in *)
+(* the documentation and/or other materials provided with the *)
+(* distribution. *)
+(* *)
+(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
+(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
+(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
+(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
+(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
+(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
+(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
+(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
+(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
+(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
+(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
+(* SUCH DAMAGE. *)
+(**************************************************************************)
+
+(* TODO:
+ | DEF_reg_dec dec -> group (doc_dec_lem dec)
+ | DEF_fundef fdef -> group (doc_fundef_lem fdef) ^/^ hardline
+ | DEF_internal_mutrec fundefs -> doc_mutrec_lem fundefs ^/^ hardline
+
+ doc_id / doc_id_type with a DeIid ...*
+ fix_id
+ doc_quant_item on constraints
+ type quantifiers in records, unions
+ update notation for records
+ register_refs?
+ should I control the nexps somewhat?
+ L_real
+ should P_var produce an "as"?
+ does doc_pat detuple too much?
+ Import ListNotations
+ P_record?
+ type quantifiers and constraints in definitions
+ should atom types be specially treated? (probably not in doc_typ, but elsewhere)
+ ordering of kids in existential types is fragile!
+ doc_nexp needs precedence fixed (i.e., parens inserted)
+ doc_exp_lem assignments, foreach (etc), early_return (supress type when it's not ASTable?),
+ application (do we need to bother printing types so much?), casts (probably ought to print type),
+ record update
+ lem/isabelle formatting hacks
+ move List imports
+ renaming kids bound in fn bodies as well as top-level funcl pattern
+*)
+
+open Type_check
+open Ast
+open Ast_util
+open Rewriter
+open PPrint
+open Pretty_print_common
+
+module StringSet = Set.Make(String)
+
+(****************************************************************************
+ * PPrint-based sail-to-coq pprinter
+****************************************************************************)
+
+type context = {
+ early_ret : bool;
+ kid_renames : kid KBindings.t;
+ bound_nexps : NexpSet.t;
+}
+let empty_ctxt = {
+ early_ret = false;
+ kid_renames = KBindings.empty;
+ bound_nexps = NexpSet.empty
+}
+
+let langlebar = string "<|"
+let ranglebar = string "|>"
+let anglebars = enclose langlebar ranglebar
+let enclose_record = enclose (string "{| ") (string " |}")
+let bigarrow = string "=>"
+
+let separate_opt s f l = separate s (Util.map_filter f l)
+
+let is_number_char c =
+ c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' ||
+ c = '6' || c = '7' || c = '8' || c = '9'
+
+let rec fix_id remove_tick name = match name with
+ | "assert"
+ | "lsl"
+ | "lsr"
+ | "asr"
+ | "type"
+ | "fun"
+ | "function"
+ | "raise"
+ | "try"
+ | "match"
+ | "with"
+ | "check"
+ | "field"
+ | "LT"
+ | "GT"
+ | "EQ"
+ | "integer"
+ -> name ^ "'"
+ | _ ->
+ if String.contains name '#' then
+ fix_id remove_tick (String.concat "_" (Util.split_on_char '#' name))
+ else if String.contains name '?' then
+ fix_id remove_tick (String.concat "_pat_" (Util.split_on_char '?' name))
+ else if name.[0] = '\'' then
+ let var = String.sub name 1 (String.length name - 1) in
+ if remove_tick then var else (var ^ "'")
+ else if is_number_char(name.[0]) then
+ ("v" ^ name ^ "'")
+ else name
+
+let doc_id (Id_aux(i,_)) =
+ match i with
+ | Id i -> string (fix_id false i)
+ | DeIid x ->
+ (* add an extra space through empty to avoid a closing-comment
+ * token in case of x ending with star. *)
+ parens (separate space [colon; string x; empty])
+
+let doc_id_type (Id_aux(i,_)) =
+ match i with
+ | Id("int") -> string "Z"
+ | Id("nat") -> string "Z"
+ | Id i -> string (fix_id false i)
+ | DeIid x ->
+ (* add an extra space through empty to avoid a closing-comment
+ * token in case of x ending with star. *)
+ parens (separate space [colon; string x; empty])
+
+let doc_id_ctor (Id_aux(i,_)) =
+ match i with
+ | Id i -> string (fix_id false i)
+ | DeIid x ->
+ (* add an extra space through empty to avoid a closing-comment
+ * token in case of x ending with star. *)
+ separate space [colon; string x; empty]
+
+let doc_var_lem ctx kid = string (fix_id true (string_of_kid (try KBindings.find kid ctx.kid_renames with Not_found -> kid)))
+
+let doc_docstring_lem (l, _) = match l with
+ | Parse_ast.Documented (str, _) -> string ("(*" ^ str ^ "*)") ^^ hardline
+ | _ -> empty
+
+let simple_annot l typ = (Parse_ast.Generated l, Some (Env.empty, typ, no_effect))
+let simple_num l n = E_aux (
+ E_lit (L_aux (L_num n, Parse_ast.Generated l)),
+ simple_annot (Parse_ast.Generated l)
+ (atom_typ (Nexp_aux (Nexp_constant n, Parse_ast.Generated l))))
+
+let effectful_set = function
+ | [] -> false
+ | _ -> true
+ (*List.exists
+ (fun (BE_aux (eff,_)) ->
+ match eff with
+ | BE_rreg | BE_wreg | BE_rmem | BE_rmemt | BE_wmem | BE_eamem
+ | BE_exmem | BE_wmv | BE_wmvt | BE_barr | BE_depend | BE_nondet
+ | BE_escape -> true
+ | _ -> false)*)
+
+let effectful (Effect_aux (Effect_set effs, _)) = effectful_set effs
+
+let is_regtyp (Typ_aux (typ, _)) env = match typ with
+ | Typ_app(id, _) when string_of_id id = "register" -> true
+ | _ -> false
+
+let doc_nexp ctx nexp =
+ let (Nexp_aux (nexp, l) as full_nexp) = nexp_simp nexp in
+ match nexp with
+ | Nexp_constant i -> string (Big_int.to_string i)
+ | Nexp_var v -> doc_var_lem ctx v
+ | Nexp_id id -> doc_id id
+ | Nexp_times (n1, n2) -> separate space [doc_nexp n1; star; doc_nexp n2]
+ | Nexp_sum (n1, n2) -> separate space [doc_nexp n1; plus; doc_nexp n2]
+ | Nexp_minus (n1, n2) -> separate space [doc_nexp n1; minus; doc_nexp n2]
+ | Nexp_exp n -> separate space [string "2"; caret; doc_nexp n]
+ | Nexp_neg n -> separate space [minus; doc_nexp n]
+ | _ ->
+ raise (Reporting_basic.err_unreachable l
+ ("cannot pretty-print nexp \"" ^ string_of_nexp full_nexp ^ "\""))
+
+(* Rewrite mangled names of type variables to the original names *)
+let rec orig_nexp (Nexp_aux (nexp, l)) =
+ let rewrap nexp = Nexp_aux (nexp, l) in
+ match nexp with
+ | Nexp_var kid -> rewrap (Nexp_var (orig_kid kid))
+ | Nexp_times (n1, n2) -> rewrap (Nexp_times (orig_nexp n1, orig_nexp n2))
+ | Nexp_sum (n1, n2) -> rewrap (Nexp_sum (orig_nexp n1, orig_nexp n2))
+ | Nexp_minus (n1, n2) -> rewrap (Nexp_minus (orig_nexp n1, orig_nexp n2))
+ | Nexp_exp n -> rewrap (Nexp_exp (orig_nexp n))
+ | Nexp_neg n -> rewrap (Nexp_neg (orig_nexp n))
+ | _ -> rewrap nexp
+
+(* 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 (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))
+ | Typ_fn (t1,t2,_) -> NexpSet.union (trec t1) (trec t2)
+ | Typ_tup ts ->
+ List.fold_left (fun s t -> NexpSet.union s (trec t))
+ NexpSet.empty ts
+ | Typ_app(Id_aux (Id "vector", _), [
+ Typ_arg_aux (Typ_arg_nexp m, _);
+ Typ_arg_aux (Typ_arg_order ord, _);
+ Typ_arg_aux (Typ_arg_typ elem_typ, _)]) ->
+ let m = nexp_simp m in
+ if is_bit_typ elem_typ && not (is_nexp_constant m) then
+ NexpSet.singleton (orig_nexp m)
+ else trec elem_typ
+ | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
+ trec etyp
+ | 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 ta))
+ NexpSet.empty tas
+ | Typ_exist (kids,_,t) -> trec t
+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 typ
+ | Typ_arg_order _ -> NexpSet.empty
+
+let lem_tyvars_of_typ typ =
+ NexpSet.fold (fun nexp ks -> KidSet.union ks (tyvars_of_nexp nexp))
+ (lem_nexps_of_typ typ) KidSet.empty
+
+(* When making changes here, check whether they affect lem_tyvars_of_typ *)
+let doc_typ, doc_atomic_typ =
+ let fns ctx =
+ (* following the structure of parser for precedence *)
+ 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 ret_typ =
+ if effectful efct
+ 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 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 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 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",_)),_) ->
+ string "mword " ^^ doc_nexp ctx (nexp_simp m)
+ | _ -> string "list" ^^ 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, _)]) ->
+ let tpp = string "register_ref regstate register_value " ^^ typ etyp in
+ if atyp_needed then parens tpp else tpp
+ | Typ_app(Id_aux (Id "range", _),_) ->
+ (string "Z")
+ | Typ_app(Id_aux (Id "implicit", _),_) ->
+ (string "Z")
+ | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
+ (string "Z")
+ | Typ_app(id,args) ->
+ let tpp = (doc_id_type id) ^^ space ^^ (separate_map space doc_typ_arg args) in
+ if atyp_needed then parens tpp else tpp
+ | _ -> 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) ->
+ (*if List.exists ((=) (string_of_id id)) regtypes
+ then string "register"
+ else*) doc_id_type id
+ | Typ_var v -> doc_var_lem ctx v
+ | Typ_app _ | Typ_tup _ | Typ_fn _ ->
+ (* exhaustiveness matters here to avoid infinite loops
+ * if we add a new Typ constructor *)
+ let tpp = typ ty in
+ if atyp_needed then parens tpp else tpp
+ | Typ_exist (kids,_,ty) ->
+ let tpp = typ ty in
+tpp (* List.fold_left
+ (fun tpp kid -> braces (separate space [doc_var_lem kid; colon; string "Z"; ampersand; tpp]))
+ tpp kids*)
+ and doc_typ_arg (Typ_arg_aux(t,_)) = match t with
+ | Typ_arg_typ t -> app_typ true t
+ | Typ_arg_nexp n -> doc_nexp ctx n
+ | Typ_arg_order o -> empty
+ in typ', atomic_typ
+ in (fun ctx -> (fst (fns ctx))), (fun ctx -> (snd (fns ctx)))
+
+(* Check for variables in types that would be pretty-printed and are not
+ bound in the val spec of the function. *)
+let contains_t_pp_var ctxt (Typ_aux (t,a) as typ) =
+ NexpSet.diff (lem_nexps_of_typ typ) ctxt.bound_nexps
+ |> NexpSet.exists (fun nexp -> not (is_nexp_constant nexp))
+
+let replace_typ_size ctxt env (Typ_aux (t,a)) =
+ match t with
+ | Typ_app (Id_aux (Id "vector",_) as id, [Typ_arg_aux (Typ_arg_nexp size,_);ord;typ']) ->
+ begin
+ let mk_typ nexp =
+ Some (Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
+ in
+ match Type_check.solve env size with
+ | Some n -> mk_typ (nconstant n)
+ | None ->
+ let is_equal nexp =
+ prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
+ in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
+ | nexp -> mk_typ nexp
+ | exception Not_found -> None
+ end
+ | _ -> None
+
+let doc_tannot_lem ctxt env eff typ =
+ let of_typ typ =
+ let ta = doc_typ ctxt typ in
+ if eff then string " : M " ^^ parens ta
+ else string " : " ^^ ta
+ in
+ if contains_t_pp_var ctxt typ
+ then
+ match replace_typ_size ctxt env typ with
+ | None -> empty
+ | Some typ -> of_typ typ
+ else of_typ typ
+
+let doc_lit (L_aux(lit,l)) =
+ match lit with
+ | L_unit -> utf8string "tt"
+ | L_zero -> utf8string "B0"
+ | L_one -> utf8string "B1"
+ | L_false -> utf8string "false"
+ | L_true -> utf8string "true"
+ | L_num i ->
+ let ipp = Big_int.to_string i in
+ utf8string ipp
+ | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*)
+ | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*)
+ | L_undef ->
+ utf8string "(return (failwith \"undefined value of unsupported type\"))"
+ | L_string s -> utf8string ("\"" ^ s ^ "\"")
+ | L_real s ->
+ (* Lem does not support decimal syntax, so we translate a string
+ of the form "x.y" into the ratio (x * 10^len(y) + y) / 10^len(y).
+ The OCaml library has a conversion function from strings to floats, but
+ not from floats to ratios. ZArith's Q library does have the latter, but
+ 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;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)
+ | _ ->
+ raise (Reporting_basic.Fatal_error
+ (Reporting_basic.Err_syntax_locn (l, "could not parse real literal"))) in
+ parens (separate space (List.map string [
+ "realFromFrac"; Big_int.to_string num; Big_int.to_string denom]))
+
+(* TODO: parens *)
+let rec doc_nc ctx (NC_aux (nc,_)) =
+ match nc with
+ | NC_equal (ne1, ne2) -> doc_op equals (doc_nexp ctx ne1) (doc_nexp ctx ne2)
+ | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
+ | NC_bounded_le (ne1, ne2) -> doc_op (string "<=") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
+ | NC_not_equal (ne1, ne2) -> doc_op (string "<>") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
+ | NC_set (kid, is) -> (* TODO: is this a good translation? *)
+ separate space [string "In"; doc_var_lem ctx kid;
+ brackets (separate (string "; ")
+ (List.map (fun i -> string (Nat_big_num.to_string i)) is))]
+ | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc ctx nc1) (doc_nc ctx nc2)
+ | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc ctx nc1) (doc_nc ctx nc2)
+ | NC_true -> string "True"
+ | NC_false -> string "False"
+
+let doc_quant_item ctx delimit (QI_aux (qi,_)) =
+ match qi with
+ | QI_id (KOpt_aux (KOpt_none kid,_)) ->
+ Some (delimit (separate space [doc_var_lem ctx kid; colon; string "Z"]))
+ | QI_id (KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (kind,_)],_),kid),_)) -> begin
+ match kind with
+ | BK_type -> Some (delimit (separate space [doc_var_lem ctx kid; colon; string "Type"]))
+ | BK_int -> Some (delimit (separate space [doc_var_lem ctx kid; colon; string "Z"]))
+ | BK_order -> None
+ end
+ | QI_id _ -> failwith "Quantifier with multiple kinds"
+ | QI_const nc -> Some (bquote ^^ braces (string "ArithFact" ^^ parens (doc_nc ctx nc)))
+
+let doc_typquant_items ctx delimit (TypQ_aux (tq,_)) =
+ match tq with
+ | TypQ_tq qis -> separate_opt space (doc_quant_item ctx delimit) qis
+ | TypQ_no_forall -> empty
+
+let doc_typquant ctx (TypQ_aux(tq,_)) typ = match tq with
+| TypQ_tq ((_ :: _) as qs) ->
+ string "forall " ^^ separate_opt space (doc_quant_item ctx parens) qs ^^ string ". " ^^ typ
+| _ -> typ
+
+(* Produce Size type constraints for bitvector sizes when using
+ machine words. Often these will be unnecessary, but this simple
+ approach will do for now. *)
+
+let rec typeclass_nexps (Typ_aux(t,_)) =
+ match t with
+ | Typ_id _
+ | Typ_var _
+ -> NexpSet.empty
+ | Typ_fn (t1,t2,_) -> NexpSet.union (typeclass_nexps t1) (typeclass_nexps t2)
+ | Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts)
+ | Typ_app (Id_aux (Id "vector",_),
+ [Typ_arg_aux (Typ_arg_nexp size_nexp,_);
+ _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)])
+ | Typ_app (Id_aux (Id "itself",_),
+ [Typ_arg_aux (Typ_arg_nexp size_nexp,_)]) ->
+ let size_nexp = nexp_simp size_nexp in
+ if is_nexp_constant size_nexp then NexpSet.empty else
+ NexpSet.singleton (orig_nexp size_nexp)
+ | Typ_app _ -> NexpSet.empty
+ | Typ_exist (kids,_,t) -> NexpSet.empty (* todo *)
+
+let doc_typschm ctx quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
+ let pt = doc_typ ctx t in
+ if quants then doc_typquant ctx tq pt else pt
+
+let is_ctor env id = match Env.lookup_id id env with
+| Enum _ -> true
+| _ -> false
+
+(*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 ctxt apat_needed (P_aux (p,(l,annot))) = match p with
+ | P_app(id, ((_ :: _) as pats)) ->
+ let ppp = doc_unop (doc_id_ctor id)
+ (parens (separate_map comma (doc_pat ctxt true) pats)) in
+ if apat_needed then parens ppp else ppp
+ | P_app(id, []) -> doc_id_ctor id
+ | P_lit lit -> doc_lit lit
+ | P_wild -> underscore
+ | P_id id -> doc_id id
+ | P_var(p,_) -> doc_pat ctxt true p
+ | P_as(p,id) -> parens (separate space [doc_pat ctxt true p; string "as"; doc_id id])
+ | P_typ(typ,p) ->
+ let doc_p = doc_pat ctxt true p in
+ doc_p
+ (* Type annotations aren't allowed everywhere in patterns in Coq *)
+ (*parens (doc_op colon doc_p (doc_typ typ))*)
+ | P_vector pats ->
+ let ppp = brackets (separate_map semi (doc_pat ctxt true) pats) 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 ctxt apat_needed p
+ | _ -> parens (separate_map comma_sp (doc_pat ctxt false) pats))
+ | P_list pats -> brackets (separate_map semi (doc_pat ctxt false) pats)
+ | P_cons (p,p') -> doc_op (string "::") (doc_pat ctxt true p) (doc_pat ctxt true p')
+ | P_record (_,_) -> empty (* TODO *)
+
+let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with
+ | Typ_tup ts -> List.exists typ_needs_printed ts
+ | Typ_app (Id_aux (Id "itself",_),_) -> true
+ | Typ_app (_, targs) -> is_bitvector_typ typ || List.exists typ_needs_printed_arg targs
+ | Typ_fn (t1,t2,_) -> typ_needs_printed t1 || typ_needs_printed t2
+ | Typ_exist (kids,_,t) ->
+ let visible_kids = KidSet.inter (KidSet.of_list kids) (lem_tyvars_of_typ t) in
+ typ_needs_printed t && KidSet.is_empty visible_kids
+ | _ -> false
+and typ_needs_printed_arg (Typ_arg_aux (targ, _)) = match targ with
+ | Typ_arg_typ t -> typ_needs_printed t
+ | _ -> false
+
+let contains_early_return exp =
+ let e_app (f, args) =
+ let rets, args = List.split args in
+ (List.fold_left (||) (string_of_id f = "early_return") rets,
+ E_app (f, args)) in
+ fst (fold_exp
+ { (Rewriter.compute_exp_alg false (||))
+ with e_return = (fun (_, r) -> (true, E_return r)); e_app = e_app } exp)
+
+let find_e_ids exp =
+ let e_id id = IdSet.singleton id, E_id id in
+ fst (fold_exp
+ { (compute_exp_alg IdSet.empty IdSet.union) with e_id = e_id } exp)
+
+let typ_id_of (Typ_aux (typ, l)) = match typ with
+ | Typ_id id -> id
+ | Typ_app (register, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)])
+ when string_of_id register = "register" -> id
+ | Typ_app (id, _) -> id
+ | _ -> raise (Reporting_basic.err_unreachable l "failed to get type id")
+
+let prefix_recordtype = true
+let report = Reporting_basic.err_unreachable
+let doc_exp_lem, doc_let_lem =
+ let rec top_exp (ctxt : context) (aexp_needed : bool)
+ (E_aux (e, (l,annot)) as full_exp) =
+ let expY = top_exp ctxt true in
+ let expN = top_exp ctxt false in
+ let expV = top_exp ctxt in
+ let liftR doc =
+ if ctxt.early_ret && effectful (effect_of full_exp)
+ then separate space [string "liftR"; parens (doc)]
+ else doc in
+ match e with
+ | E_assign((LEXP_aux(le_act,tannot) as le), e) ->
+ (* can only be register writes *)
+ (match le_act (*, t, tag*) with
+ | LEXP_vector_range (le,e2,e3) ->
+ (match le with
+ | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) ->
+ if is_bit_typ (typ_of_annot fannot) then
+ raise (report l "indexing a register's (single bit) bitfield not supported")
+ else
+ let field_ref =
+ doc_id (typ_id_of (typ_of_annot lannot)) ^^
+ underscore ^^
+ doc_id id in
+ liftR ((prefix 2 1)
+ (string "write_reg_field_range")
+ (align (doc_lexp_deref_lem ctxt le ^/^
+ field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e)))
+ | _ ->
+ let deref = doc_lexp_deref_lem ctxt le in
+ liftR ((prefix 2 1)
+ (string "write_reg_range")
+ (align (deref ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
+ | LEXP_vector (le,e2) ->
+ (match le with
+ | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) ->
+ if is_bit_typ (typ_of_annot fannot) then
+ raise (report l "indexing a register's (single bit) bitfield not supported")
+ else
+ let field_ref =
+ doc_id (typ_id_of (typ_of_annot lannot)) ^^
+ underscore ^^
+ doc_id id in
+ 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 ctxt le ^/^
+ field_ref ^/^ expY e2 ^/^ expY e)))
+ | LEXP_aux (_, lannot) ->
+ let deref = doc_lexp_deref_lem ctxt 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))
+ )
+ | LEXP_field ((LEXP_aux (_, lannot) as le),id) ->
+ let field_ref =
+ doc_id (typ_id_of (typ_of_annot lannot)) ^^
+ underscore ^^
+ doc_id id (*^^
+ dot ^^
+ string "set_field"*) in
+ liftR ((prefix 2 1)
+ (string "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 "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")
+ | E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re)
+ | E_if(c,t,e) ->
+ let epp = if_exp ctxt false c t e in
+ if aexp_needed then parens (align epp) else epp
+ | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) ->
+ raise (report l "E_for should have been rewritten before pretty-printing")
+ | E_loop _ ->
+ raise (report l "E_loop should have been rewritten before pretty-printing")
+ | E_let(leb,e) ->
+ let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
+ if aexp_needed then parens epp else epp
+ | E_app(f,args) ->
+ begin match f with
+ (* temporary hack to make the loop body a function of the temporary variables *)
+ | Id_aux (Id "None", _) as none -> doc_id_ctor none
+ | Id_aux (Id "foreach", _) ->
+ begin
+ match args with
+ | [exp1; exp2; exp3; ord_exp; vartuple; body] ->
+ let loopvar, body = match body with
+ | E_aux (E_let (LB_aux (LB_val (
+ P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _), _), _), body), _) -> id, body
+ | E_aux (E_let (LB_aux (LB_val (
+ P_aux (P_var (P_aux (P_id id, _), _), _), _), _), body), _) -> id, body
+ | E_aux (E_let (LB_aux (LB_val (
+ P_aux (P_id id, _), _), _), body), _) -> id, body
+ | _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in
+ let step = match ord_exp with
+ | E_aux (E_lit (L_aux (L_false, _)), _) ->
+ parens (separate space [string "integerNegate"; expY exp3])
+ | _ -> expY exp3
+ in
+ let combinator = if effectful (effect_of body) then "foreachM" else "foreach" in
+ let indices_pp = parens (separate space [string "index_list"; expY exp1; expY exp2; step]) in
+ let used_vars_body = find_e_ids body in
+ let body_lambda =
+ (* Work around indentation issues in Lem when translating
+ tuple or literal unit patterns to Isabelle *)
+ match fst (uncast_exp vartuple) with
+ | E_aux (E_tuple _, _)
+ when not (IdSet.mem (mk_id "varstup") used_vars_body)->
+ separate space [string "fun"; doc_id loopvar; string "varstup"; bigarrow]
+ ^^ break 1 ^^
+ separate space [string "let"; expY vartuple; string ":= varstup in"]
+ | E_aux (E_lit (L_aux (L_unit, _)), _)
+ when not (IdSet.mem (mk_id "unit_var") used_vars_body) ->
+ separate space [string "fun"; doc_id loopvar; string "unit_var"; bigarrow]
+ | _ ->
+ separate space [string "fun"; doc_id loopvar; expY vartuple; bigarrow]
+ in
+ parens (
+ (prefix 2 1)
+ ((separate space) [string combinator; indices_pp; expY vartuple])
+ (parens
+ (prefix 2 1 (group body_lambda) (expN body))
+ )
+ )
+ | _ -> raise (Reporting_basic.err_unreachable l
+ "Unexpected number of arguments for loop combinator")
+ end
+ | Id_aux (Id (("while" | "until") as combinator), _) ->
+ begin
+ match args with
+ | [cond; varstuple; body] ->
+ let return (E_aux (e, a)) = E_aux (E_internal_return (E_aux (e, a)), a) 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
+ in
+ let used_vars_body = find_e_ids body in
+ let lambda =
+ (* Work around indentation issues in Lem when translating
+ tuple or literal unit patterns to Isabelle *)
+ match fst (uncast_exp varstuple) with
+ | E_aux (E_tuple _, _)
+ when not (IdSet.mem (mk_id "varstup") used_vars_body)->
+ separate space [string "fun varstup"; bigarrow] ^^ break 1 ^^
+ separate space [string "let"; expY varstuple; string ":= varstup in"]
+ | E_aux (E_lit (L_aux (L_unit, _)), _)
+ when not (IdSet.mem (mk_id "unit_var") used_vars_body) ->
+ separate space [string "fun unit_var"; bigarrow]
+ | _ ->
+ separate space [string "fun"; expY varstuple; bigarrow]
+ in
+ parens (
+ (prefix 2 1)
+ ((separate space) [string (combinator ^ csuffix); expY varstuple])
+ ((prefix 0 1)
+ (parens (prefix 2 1 (group lambda) (expN cond)))
+ (parens (prefix 2 1 (group lambda) (expN body))))
+ )
+ | _ -> raise (Reporting_basic.err_unreachable l
+ "Unexpected number of arguments for loop combinator")
+ end
+ | Id_aux (Id "early_return", _) ->
+ begin
+ match args with
+ | [exp] ->
+ let epp = separate space [string "early_return"; expY exp] in
+ let aexp_needed, tepp =
+ if contains_t_pp_var ctxt (typ_of exp) ||
+ contains_t_pp_var ctxt (typ_of full_exp) then
+ aexp_needed, epp
+ else
+ let tannot = separate space [string "MR";
+ doc_atomic_typ ctxt false (typ_of full_exp);
+ doc_atomic_typ ctxt 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
+ "Unexpected number of arguments for early_return builtin")
+ end
+ | _ ->
+ begin match annot with
+ | Some (env, _, _) when Env.is_union_constructor f env ->
+ let epp =
+ match args with
+ | [] -> doc_id_ctor f
+ | [arg] -> doc_id_ctor f ^^ space ^^ expV true arg
+ | _ ->
+ doc_id_ctor f ^^ space ^^
+ parens (separate_map comma (expV false) args) in
+ if aexp_needed then parens (align epp) else epp
+ | _ ->
+ let call, is_extern = match annot with
+ | Some (env, _, _) when Env.is_extern f env "coq" ->
+ string (Env.get_extern f env "coq"), true
+ | _ -> doc_id f, false in
+ let epp = hang 2 (flow (break 1) (call :: List.map expY args)) in
+ let (taepp,aexp_needed) =
+ let env = env_of full_exp in
+ let t = Env.expand_synonyms env (typ_of full_exp) in
+ let eff = effect_of full_exp in
+ if typ_needs_printed t
+ then (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env (effectful eff) t))), true)
+ else (epp, aexp_needed) in
+ liftR (if aexp_needed then parens (align taepp) else taepp)
+ end
+ end
+ | E_vector_access (v,e) ->
+ raise (Reporting_basic.err_unreachable l
+ "E_vector_access should have been rewritten before pretty-printing")
+ | E_vector_subrange (v,e1,e2) ->
+ raise (Reporting_basic.err_unreachable l
+ "E_vector_subrange should have been rewritten before pretty-printing")
+ | E_field((E_aux(_,(l,fannot)) as fexp),id) ->
+ (match fannot with
+ | Some(env, (Typ_aux (Typ_id tid, _)), _)
+ | Some(env, (Typ_aux (Typ_app (tid, _), _)), _)
+ when Env.is_record tid env ->
+ let fname =
+ if prefix_recordtype && string_of_id tid <> "regstate"
+ then (string (string_of_id tid ^ "_")) ^^ doc_id id
+ else doc_id id in
+ expY fexp ^^ dot ^^ fname
+ | _ ->
+ raise (report l "E_field expression with no register or record type"))
+ | E_block [] -> string "tt"
+ | E_block exps -> raise (report l "Blocks should have been removed till now.")
+ | E_nondet exps -> raise (report l "Nondet blocks not supported.")
+ | E_id id | E_ref id ->
+ let env = env_of full_exp in
+ let typ = typ_of full_exp in
+ 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 (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
+ else if Env.is_register id env then doc_id (append_id id "_ref")
+ else if is_ctor env id then doc_id_ctor id
+ else doc_id id
+ | E_lit lit -> doc_lit lit
+ | E_cast(typ,e) ->
+ expV aexp_needed e
+ | E_tuple exps ->
+ parens (align (group (separate_map (comma ^^ break 1) expN exps)))
+ | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
+ let recordtyp = match annot with
+ | Some (env, Typ_aux (Typ_id tid,_), _)
+ | Some (env, Typ_aux (Typ_app (tid, _), _), _) ->
+ (* 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
+ let epp = enclose_record (align (separate_map
+ (semi_sp ^^ break 1)
+ (doc_fexp ctxt recordtyp) fexps)) in
+ if aexp_needed then parens epp else epp
+ | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
+ let recordtyp = match annot with
+ | Some (env, Typ_aux (Typ_id tid,_), _)
+ | Some (env, Typ_aux (Typ_app (tid, _), _), _)
+ 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 ctxt 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) =
+ if is_vector_typ t then vector_start_index t, vector_typ_args_of t
+ else raise (Reporting_basic.err_unreachable l
+ "E_vector of non-vector type") in
+ let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
+ let expspp =
+ match exps with
+ | [] -> empty
+ | e :: es ->
+ let (expspp,_) =
+ List.fold_left
+ (fun (pp,count) e ->
+ (pp ^^ semi ^^ (if count = 20 then break 0 else empty) ^^
+ expN e),
+ if count = 20 then 0 else count + 1)
+ (expN e,0) es in
+ align (group expspp) in
+ let epp = brackets expspp in
+ let (epp,aexp_needed) =
+ if is_bit_typ etyp then
+ let bepp = string "vec_of_bits" ^^ space ^^ align epp in
+ (align (group (prefix 0 1 bepp (doc_tannot_lem ctxt (env_of full_exp) false t))), true)
+ else (epp,aexp_needed) in
+ if aexp_needed then parens (align epp) else epp
+ | E_vector_update(v,e1,e2) ->
+ raise (Reporting_basic.err_unreachable l
+ "E_vector_update should have been rewritten before pretty-printing")
+ | E_vector_update_subrange(v,e1,e2,e3) ->
+ raise (Reporting_basic.err_unreachable l
+ "E_vector_update should have been rewritten before pretty-printing")
+ | E_list exps ->
+ brackets (separate_map semi (expN) exps)
+ | E_case(e,pexps) ->
+ let only_integers e = expY e in
+ let epp =
+ group ((separate space [string "match"; only_integers e; string "with"]) ^/^
+ (separate_map (break 1) (doc_case ctxt) pexps) ^/^
+ (string "end")) in
+ if aexp_needed then parens (align epp) else align epp
+ | E_try (e, pexps) ->
+ if effectful (effect_of e) then
+ let try_catch = if ctxt.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 ctxt) 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
+ | E_app_infix (e1,id,e2) ->
+ raise (Reporting_basic.err_unreachable l
+ "E_app_infix should have been rewritten before pretty-printing")
+ | E_var(lexp, eq_exp, in_exp) ->
+ raise (report l "E_vars should have been removed before pretty-printing")
+ | E_internal_plet (pat,e1,e2) ->
+ let epp =
+ let b = match e1 with E_aux (E_if _,_) -> true | _ -> false 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_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";
+ doc_pat ctxt true pat;
+ string "= varstup in"]
+ | _ ->
+ separate space [string ">>= fun"; doc_pat ctxt true pat; bigarrow]
+ 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 "returnm"; expY e1]
+ | E_sizeof nexp ->
+ (match nexp_simp nexp with
+ | Nexp_aux (Nexp_constant i, _) -> doc_lit (L_aux (L_num i, l))
+ | _ ->
+ raise (Reporting_basic.err_unreachable l
+ "pretty-printing non-constant sizeof expressions to Lem not supported"))
+ | E_return r ->
+ let ret_monad = " : 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;
+ parens (doc_typ ctxt (typ_of full_exp));
+ parens (doc_typ ctxt (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 _ | E_internal_value _ ->
+ raise (Reporting_basic.err_unreachable l
+ "unsupported internal expression encountered while pretty-printing")
+ and if_exp ctxt (elseif : bool) c t e =
+ let if_pp = string (if elseif then "else if" else "if") in
+ let else_pp = match e with
+ | E_aux (E_if (c', t', e'), _)
+ | E_aux (E_cast (_, E_aux (E_if (c', t', e'), _)), _) ->
+ if_exp ctxt true c' t' e'
+ | _ -> prefix 2 1 (string "else") (top_exp ctxt false e)
+ in
+ (prefix 2 1
+ (soft_surround 2 1 if_pp (top_exp ctxt true c) (string "then"))
+ (top_exp ctxt false t)) ^^
+ break 1 ^^
+ else_pp
+ and let_exp ctxt (LB_aux(lb,_)) = match lb with
+ | LB_val(pat,e) ->
+ prefix 2 1
+ (separate space [string "let"; squote ^^ doc_pat ctxt true pat; coloneq])
+ (top_exp ctxt false e)
+
+ and doc_fexp ctxt recordtyp (FE_aux(FE_Fexp(id,e),_)) =
+ let fname =
+ if prefix_recordtype && string_of_id recordtyp <> "regstate"
+ then (string (string_of_id recordtyp ^ "_")) ^^ doc_id id
+ else doc_id id in
+ group (doc_op coloneq fname (top_exp ctxt true e))
+
+ and doc_case ctxt = function
+ | Pat_aux(Pat_exp(pat,e),_) ->
+ group (prefix 3 1 (separate space [pipe; doc_pat ctxt false pat;bigarrow])
+ (group (top_exp ctxt 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 ctxt ((LEXP_aux(lexp,(l,annot)))) = match lexp with
+ | LEXP_field (le,id) ->
+ parens (separate empty [doc_lexp_deref_lem ctxt le;dot;doc_id id])
+ | LEXP_id id -> doc_id (append_id id "_ref")
+ | LEXP_cast (typ,id) -> doc_id (append_id id "_ref")
+ | LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem ctxt) 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
+
+let doc_type_union ctxt typ_name (Tu_aux(Tu_ty_id(typ,id),_)) =
+ separate space [doc_id_ctor id; colon;
+ doc_typ ctxt typ; arrow; typ_name]
+
+let rec doc_range_lem (BF_aux(r,_)) = match r with
+ | BF_single i -> parens (doc_op comma (doc_int i) (doc_int i))
+ | 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 (TD_aux(td, (l, annot))) = match td with
+ | TD_abbrev(id,nm,(TypSchm_aux (TypSchm_ts (typq, _), _) as typschm)) ->
+ doc_op coloneq
+ (separate space [string "Definition"; doc_id_type id; doc_typquant_items empty_ctxt parens typq])
+ (doc_typschm empty_ctxt false typschm) ^^ dot
+ | TD_record(id,nm,typq,fs,_) ->
+ let fname fid = if prefix_recordtype && string_of_id id <> "regstate"
+ then concat [doc_id id;string "_";doc_id_type fid;]
+ else doc_id_type fid in
+ let f_pp (typ,fid) =
+ concat [fname fid;space;colon;space;doc_typ empty_ctxt typ; semi] in
+ let rectyp = match typq with
+ | TypQ_aux (TypQ_tq qs, _) ->
+ let quant_item = function
+ | QI_aux (QI_id (KOpt_aux (KOpt_none kid, _)), l)
+ | QI_aux (QI_id (KOpt_aux (KOpt_kind (_, kid), _)), l) ->
+ [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid, l)), l)]
+ | _ -> [] in
+ let targs = List.concat (List.map quant_item qs) in
+ mk_typ (Typ_app (id, targs))
+ | TypQ_aux (TypQ_no_forall, _) -> mk_id_typ id in
+ let fs_doc = group (separate_map (break 1) f_pp fs) in
+ let doc_update_field (_,fid) =
+ let idpp = fname fid in
+ let otherfield (_,fid') =
+ if Id.compare fid fid' == 0 then empty else
+ let idpp = fname fid' in
+ separate space [semi; idpp; string ":="; idpp; string "r"]
+ in
+ string "Notation \"{[ r 'with' '" ^^ idpp ^^ string "' := e ]}\" := ({| " ^^
+ idpp ^^ string " := e" ^^ concat (List.map otherfield fs) ^^
+ space ^^ string "|})."
+ in
+ let updates_pp = separate hardline (List.map doc_update_field fs) in
+ (* let doc_field (ftyp, fid) =
+ let reftyp =
+ 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 empty_ctxt env false reftyp in
+ let get, set =
+ string "rec_val" ^^ dot ^^ fname fid,
+ anglebars (space ^^ string "rec_val with " ^^
+ (doc_op equals (fname fid) (string "v")) ^^ space) in
+ let base_ftyp = match annot with
+ | Some (env, _, _) -> Env.base_typ_of env ftyp
+ | _ -> ftyp in
+ let (start, is_inc) =
+ try
+ let start, (_, ord, _) = vector_start_index base_ftyp, vector_typ_args_of base_ftyp in
+ match nexp_simp start with
+ | Nexp_aux (Nexp_constant i, _) -> (i, is_order_inc ord)
+ | _ ->
+ raise (Reporting_basic.err_unreachable Parse_ast.Unknown
+ ("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start))
+ with
+ | _ -> (Big_int.zero, true) in
+ doc_op equals
+ (concat [string "let "; parens (concat [doc_id id; underscore; doc_id fid; rfannot])])
+ (anglebars (concat [space;
+ doc_op equals (string "field_name") (string_lit (doc_id fid)); semi_sp;
+ doc_op equals (string "field_start") (string (Big_int.to_string start)); semi_sp;
+ doc_op equals (string "field_is_inc") (string (if is_inc then "true" else "false")); semi_sp;
+ doc_op equals (string "get_field") (parens (doc_op arrow (string "fun rec_val") get)); semi_sp;
+ doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in *)
+ doc_op coloneq
+ (separate space [string "Record"; doc_id_type id; doc_typquant_items empty_ctxt parens typq])
+ ((*doc_typquant_lem typq*) (braces (space ^^ align fs_doc ^^ space))) ^^
+ dot ^^ hardline ^^ updates_pp
+ | TD_variant(id,nm,typq,ar,_) ->
+ (match id with
+ | Id_aux ((Id "read_kind"),_) -> empty
+ | Id_aux ((Id "write_kind"),_) -> empty
+ | Id_aux ((Id "barrier_kind"),_) -> empty
+ | Id_aux ((Id "trans_kind"),_) -> empty
+ | Id_aux ((Id "instruction_kind"),_) -> empty
+ (* | Id_aux ((Id "regfp"),_) -> empty
+ | Id_aux ((Id "niafp"),_) -> empty
+ | Id_aux ((Id "diafp"),_) -> empty *)
+ | Id_aux ((Id "option"),_) -> empty
+ | _ ->
+ let typ_nm = separate space [doc_id_type id; doc_typquant_items empty_ctxt parens typq] in
+ let ar_doc = group (separate_map (break 1 ^^ pipe ^^ space) (doc_type_union empty_ctxt typ_nm) ar) in
+ let typ_pp =
+ (doc_op coloneq)
+ (concat [string "Inductive"; space; typ_nm])
+ ((*doc_typquant_lem typq*) ar_doc) in
+ typ_pp ^^ dot ^^ hardline ^^ hardline)
+ | TD_enum(id,nm,enums,_) ->
+ (match id with
+ | Id_aux ((Id "read_kind"),_) -> empty
+ | Id_aux ((Id "write_kind"),_) -> empty
+ | Id_aux ((Id "barrier_kind"),_) -> empty
+ | Id_aux ((Id "trans_kind"),_) -> empty
+ | Id_aux ((Id "instruction_kind"),_) -> empty
+ | Id_aux ((Id "regfp"),_) -> empty
+ | Id_aux ((Id "niafp"),_) -> empty
+ | Id_aux ((Id "diafp"),_) -> empty
+ | _ ->
+ let enums_doc = group (separate_map (break 1 ^^ pipe ^^ space) doc_id_ctor enums) in
+ let typ_pp = (doc_op coloneq)
+ (concat [string "Inductive"; space; doc_id_type id;])
+ (enums_doc) in
+ typ_pp ^^ dot ^^ hardline ^^ hardline)
+ | _ -> raise (Reporting_basic.err_unreachable l "register with non-constant indices")
+
+let args_of_typ l env typs =
+ 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))), typ),
+ E_aux (E_id id, (l, Some (env, typ, no_effect))) in
+ List.split (List.mapi arg typs)
+
+let rec untuple_args_pat typ (P_aux (paux, ((l, _) as annot)) as pat) =
+ let env = env_of_annot annot in
+ let tup_typs = match typ with
+ | Typ_aux (Typ_tup typs, _) -> Some typs
+ | _ -> match Env.expand_synonyms env typ with
+ | Typ_aux (Typ_tup typs, _) -> Some typs
+ | _ -> None
+ in
+ let identity = (fun body -> body) in
+ match paux, tup_typs with
+ | P_tup [], _ ->
+ let annot = (l, Some (Env.empty, unit_typ, no_effect)) in
+ [P_aux (P_lit (mk_lit L_unit), annot), unit_typ], identity
+ | P_tup pats, Some typs -> List.combine pats typs, identity
+ | P_tup pats, _ -> failwith "Tuple pattern against non-tuple type"
+ | P_wild, Some typs ->
+ let wild typ = P_aux (P_wild, (l, Some (env, typ, no_effect))), typ in
+ List.map wild typs, identity
+ | P_typ (_, pat), _ -> untuple_args_pat typ pat
+ | P_as _, Some typs | P_id _, Some typs ->
+ let argpats, argexps = args_of_typ l env typs 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,typ], identity
+
+let doc_rec (Rec_aux(r,_)) = match r with
+ | Rec_nonrec -> string "Definition"
+ | Rec_rec -> string "Fixpoint"
+
+let doc_fun_body 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))
+ else doc_exp
+
+(* Coq doesn't support "as" patterns well in Definition binders, so we push
+ them over to the r.h.s. of the := *)
+let demote_as_pattern i (P_aux (_,p_annot) as pat,typ) =
+ let open Rewriter in
+ if fst (fold_pat ({ (compute_pat_alg false (||)) with p_as = (fun ((_,p),id) -> true, P_as (p,id)) }) pat)
+ then
+ let id = mk_id ("arg" ^ string_of_int i) in (* TODO: name conflicts *)
+ (P_aux (P_id id, p_annot),typ),
+ fun (E_aux (_,e_ann) as e) ->
+ E_aux (E_let (LB_aux (LB_val (pat, E_aux (E_id id, p_annot)),p_annot),e),e_ann)
+ else (pat,typ), fun e -> e
+
+(* Ideally we'd remove the duplication between type variables and atom
+ arguments, but for now we just add an equality constraint. *)
+
+let atom_constraint ctxt (pat, typ) =
+ let typ = Env.base_typ_of (pat_env_of pat) typ in
+ match pat, typ with
+ | P_aux (P_id id, _),
+ Typ_aux (Typ_app (Id_aux (Id "atom",_),
+ [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_) ->
+ Some (bquote ^^ braces (string "ArithFact" ^^ space ^^
+ parens (doc_op equals (doc_id id) (doc_var_lem ctxt kid))))
+ | _ -> None
+
+let all_ids pexp =
+ let open Rewriter in
+ fold_pexp (
+ { (pure_exp_alg IdSet.empty IdSet.union) with
+ e_id = (fun id -> IdSet.singleton id);
+ e_ref = (fun id -> IdSet.singleton id);
+ e_app = (fun (id,ids) ->
+ List.fold_left IdSet.union (IdSet.singleton id) ids);
+ e_app_infix = (fun (ids1,id,ids2) ->
+ IdSet.add id (IdSet.union ids1 ids2));
+ e_for = (fun (id,ids1,ids2,ids3,_,ids4) ->
+ IdSet.add id (IdSet.union ids1 (IdSet.union ids2 (IdSet.union ids3 ids4))));
+ lEXP_id = IdSet.singleton;
+ lEXP_memory = (fun (id,ids) ->
+ List.fold_left IdSet.union (IdSet.singleton id) ids);
+ lEXP_cast = (fun (_,id) -> IdSet.singleton id);
+ pat_alg = { (pure_pat_alg IdSet.empty IdSet.union) with
+ p_as = (fun (ids,id) -> IdSet.add id ids);
+ p_id = IdSet.singleton;
+ p_app = (fun (id,ids) ->
+ List.fold_left IdSet.union (IdSet.singleton id) ids);
+ }
+ }) pexp
+
+let tyvars_of_typquant (TypQ_aux (tq,_)) =
+ match tq with
+ | TypQ_no_forall -> KidSet.empty
+ | TypQ_tq qs -> List.fold_left KidSet.union KidSet.empty
+ (List.map tyvars_of_quant_item qs)
+
+let mk_kid_renames ids_to_avoid kids =
+ let map_id = function
+ | Id_aux (Id i, _) -> Some (fix_id false i)
+ | Id_aux (DeIid _, _) -> None
+ in
+ let ids = StringSet.of_list (Util.map_filter map_id (IdSet.elements ids_to_avoid)) in
+ let rec check_kid kid (newkids,rebindings) =
+ let rec check kid1 =
+ let kid_string = fix_id true (string_of_kid kid1) in
+ if StringSet.mem kid_string ids
+ then let kid2 = match kid1 with Kid_aux (Var x,l) -> Kid_aux (Var (x ^ "0"),l) in
+ check kid2
+ else
+ KidSet.add kid1 newkids, KBindings.add kid kid1 rebindings
+ in check kid
+ in snd (KidSet.fold check_kid kids (kids, KBindings.empty))
+
+let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
+ let (tq,typ) = Env.get_val_spec_orig id (env_of_annot annot) in
+ let (arg_typ, ret_typ, eff) = match typ with
+ | Typ_aux (Typ_fn (arg_typ, ret_typ, eff),_) -> arg_typ, ret_typ, eff
+ | _ -> failwith ("Function " ^ string_of_id id ^ " does not have function type")
+ in
+ let ids_to_avoid = all_ids pexp in
+ let kids_used = tyvars_of_typquant tq in
+ let pat,guard,exp,(l,_) = destruct_pexp pexp in
+ let ctxt =
+ { early_ret = contains_early_return exp;
+ kid_renames = mk_kid_renames ids_to_avoid kids_used;
+ bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ) } in
+ let quantspp = doc_typquant_items ctxt braces tq in
+ let pats, bind = untuple_args_pat arg_typ pat in
+ let pats, binds = List.split (Util.list_mapi demote_as_pattern pats) in
+ let exp = List.fold_left (fun body f -> f body) (bind exp) binds in
+ let patspp = separate_map space (fun (pat,typ) ->
+ squote ^^ parens (separate space [doc_pat ctxt true pat; colon; doc_typ ctxt typ])) pats in
+ let atom_constr_pp = separate_opt space (atom_constraint ctxt) pats in
+ let retpp =
+ if effectful eff
+ then string "M" ^^ space ^^ parens (doc_typ ctxt ret_typ)
+ else doc_typ ctxt ret_typ
+ 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
+ (separate space [doc_id id; quantspp; patspp; atom_constr_pp; colon; retpp; coloneq])
+ (doc_fun_body ctxt exp ^^ dot))
+
+let get_id = function
+ | [] -> failwith "FD_function with empty list"
+ | (FCL_aux (FCL_Funcl (id,_),_))::_ -> id
+
+(* Strictly speaking, Lem doesn't support multiple clauses for a single function
+ joined by "and", although it has worked for Isabelle before. However, all
+ the funcls should have been merged by the merge_funcls rewrite now. *)
+let doc_fundef_rhs_lem (FD_aux(FD_function(r, typa, efa, funcls),fannot)) =
+ separate_map (hardline ^^ string "and ") doc_funcl funcls
+
+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 fundefs
+
+let rec doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),fannot)) =
+ match fcls with
+ | [] -> failwith "FD_function with empty function list"
+ | [FCL_aux (FCL_Funcl(id,_),annot) as funcl]
+ when not (Env.is_extern id (env_of_annot annot) "coq") ->
+ (doc_rec r) ^^ space ^^ (doc_funcl funcl)
+ | [_] -> empty (* extern *)
+ | _ -> failwith "FD_function with more than one clause"
+
+
+
+let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
+ match reg with
+ | DEC_reg(typ,id) -> empty
+ (*
+ let env = env_of_annot annot in
+ let rt = Env.base_typ_of env typ in
+ if is_vector_typ rt then
+ let start, (size, order, etyp) = vector_start_index rt, 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 id)
+ (string "Register" ^^ space ^^
+ align (separate space [string_lit(doc_id 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 is_field_accessor regtypes fdef =
+ let is_field_of regtyp field =
+ List.exists (fun (tname, (_, _, fields)) -> tname = regtyp &&
+ List.exists (fun (_, fid) -> string_of_id fid = field) fields) regtypes in
+ match Util.split_on_char '_' (string_of_id (id_of_fundef fdef)) with
+ | [access; regtyp; field] ->
+ (access = "get" || access = "set") && is_field_of regtyp field
+ | _ -> false
+
+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
+ ("Non-constant indices in register type " ^ tname)) in
+ let dir_b = i1 < i2 in
+ let dir = (if dir_b then "true" else "false") in
+ let doc_field (fr, fid) =
+ let i, j = match fr with
+ | BF_aux (BF_single i, _) -> (i, i)
+ | BF_aux (BF_range (i, j), _) -> (i, j)
+ | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown
+ ("Unsupported type in field " ^ string_of_id fid ^ " of " ^ tname)) in
+ let fsize = Big_int.succ (Big_int.abs (Big_int.sub i j)) in
+ (* TODO Assumes normalised, decreasing bitvector slices; however, since
+ start indices or indexing order do not appear in Lem type annotations,
+ this does not matter. *)
+ let ftyp = vector_typ (nconstant fsize) dec_ord bit_typ in
+ let reftyp =
+ 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 empty_ctxt Env.empty false reftyp in
+ doc_op equals
+ (concat [string "let "; parens (concat [string tname; underscore; doc_id fid; rfannot])])
+ (concat [
+ space; langlebar; string " field_name = \"" ^^ doc_id 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 = 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 def =
+ (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *)
+ match def with
+ | DEF_spec v_spec -> empty (* Types appear in definitions *)
+ | DEF_fixity _ -> empty
+ | DEF_overload _ -> empty
+ | DEF_type t_def -> group (doc_typdef t_def) ^/^ hardline
+ | DEF_reg_dec dec -> group (doc_dec_lem dec)
+
+ | DEF_default df -> empty
+ | DEF_fundef fdef -> group (doc_fundef fdef) ^/^ hardline
+ | DEF_internal_mutrec fundefs -> doc_mutrec_lem fundefs ^/^ hardline
+ | DEF_val (LB_aux (LB_val (pat, exp), _)) ->
+ let (id,typpp) = match pat with
+ | P_aux (P_typ (typ, P_aux (P_id id,_)),_) -> id, space ^^ colon ^^ space ^^ doc_typ empty_ctxt typ
+ | P_aux (P_id id, _) -> id, empty
+ | _ -> failwith "Top-level value definition with complex pattern not supported for Coq yet"
+ in
+ group (string "Definition" ^^ space ^^ doc_id id ^^ typpp ^^ space ^^ coloneq ^^
+ doc_exp_lem empty_ctxt false exp ^^ dot) ^/^ hardline
+ | DEF_scattered sdef -> failwith "doc_def: shoulnd't have DEF_scattered at this point"
+
+ | DEF_kind _ -> empty
+
+ | DEF_comm (DC_comm s) -> comment (string s)
+ | DEF_comm (DC_comm_struct d) -> comment (doc_def d)
+
+
+let find_exc_typ 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 pp_defs_coq (types_file,types_modules) (defs_file,defs_modules) (Defs defs) top_line =
+ (* let regtypes = find_regtypes d in *)
+ let state_ids =
+ State.generate_regstate_defs true defs
+ |> Initial_check.val_spec_ids
+ in
+ let is_state_def = function
+ | DEF_spec vs -> IdSet.mem (id_of_val_spec vs) state_ids
+ | DEF_fundef fd -> IdSet.mem (id_of_fundef fd) state_ids
+ | _ -> false
+ in
+ let is_typ_def = function
+ | DEF_type _ -> true
+ | _ -> false
+ in
+ let exc_typ = find_exc_typ defs in
+ let typdefs, defs = List.partition is_typ_def defs in
+ let statedefs, defs = List.partition is_state_def defs in
+ let register_refs = State.register_refs_coq (State.find_registers defs) in
+ (print types_file)
+ (concat
+ [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
+ (separate_map hardline)
+ (fun lib -> separate space [string "Require Import";string lib] ^^ dot) types_modules;hardline;
+string "Require Import String."; hardline;
+ separate empty (List.map doc_def typdefs); hardline;
+ hardline;
+ separate empty (List.map doc_def statedefs); hardline;
+ hardline;
+ register_refs; hardline;
+ concat [
+ string ("Definition MR a r := monadR register_value a r " ^ exc_typ ^ "."); hardline;
+ string ("Definition M a := monad register_value a " ^ exc_typ ^ "."); hardline
+ ]
+ ]);
+ (print defs_file)
+ (concat
+ [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
+ (separate_map hardline)
+ (fun lib -> separate space [string "Require Import";string lib] ^^ dot) defs_modules;hardline;
+string "Require Import List. Import ListNotations.";
+ hardline;
+ separate empty (List.map doc_def defs);
+ hardline]);
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index f58c3fa6..c181249d 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -551,10 +551,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 "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 *)
@@ -619,31 +620,34 @@ let doc_exp_lem, doc_let_lem =
raise (Reporting_basic.err_unreachable l
"E_vector_append should have been rewritten before pretty-printing")
| E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re)
- | E_if(c,t,e) ->
- let epp = if_exp ctxt false c t e in
- if aexp_needed then parens (align epp) else epp
+ | E_if(c,t,e) -> wrap_parens (align (if_exp ctxt false c t e))
| E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) ->
raise (report l "E_for should have been rewritten before pretty-printing")
| E_loop _ ->
raise (report l "E_loop should have been rewritten before pretty-printing")
| E_let(leb,e) ->
- let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
- if aexp_needed then parens epp else epp
+ wrap_parens (let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e)
| E_app(f,args) ->
begin match f with
- (* temporary hack to make the loop body a function of the temporary variables *)
| Id_aux (Id "None", _) as none -> doc_id_lem_ctor none
+ | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _)
+ when effectful (effect_of full_exp) ->
+ let call = doc_id_lem (append_id f "M") in
+ wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args)))
+ (* temporary hack to make the loop body a function of the temporary variables *)
| Id_aux (Id "foreach", _) ->
begin
match args with
| [exp1; exp2; exp3; ord_exp; vartuple; body] ->
let loopvar, body = match body with
- | E_aux (E_let (LB_aux (LB_val (
- P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _), _), _), body), _) -> id, body
- | E_aux (E_let (LB_aux (LB_val (
- P_aux (P_var (P_aux (P_id id, _), _), _), _), _), body), _) -> id, body
- | E_aux (E_let (LB_aux (LB_val (
- P_aux (P_id id, _), _), _), body), _) -> id, body
+ | E_aux (E_let (LB_aux (LB_val (_, _), _),
+ E_aux (E_let (LB_aux (LB_val (_, _), _),
+ E_aux (E_if (_,
+ E_aux (E_let (LB_aux (LB_val (
+ ((P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _))
+ | (P_aux (P_var (P_aux (P_id id, _), _), _))
+ | (P_aux (P_id id, _))), _), _),
+ body), _), _), _)), _)), _) -> id, body
| _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in
let step = match ord_exp with
| E_aux (E_lit (L_aux (L_false, _)), _) ->
@@ -743,7 +747,7 @@ let doc_exp_lem, doc_let_lem =
| _ ->
doc_id_lem_ctor f ^^ space ^^
parens (separate_map comma (expV false) args) in
- if aexp_needed then parens (align epp) else epp
+ wrap_parens (align epp)
| _ ->
let call, is_extern = match annot with
| Some (env, _, _) when Env.is_extern f env "lem" ->
@@ -796,8 +800,7 @@ let doc_exp_lem, doc_let_lem =
else if is_ctor env id then doc_id_lem_ctor id
else doc_id_lem id
| E_lit lit -> doc_lit_lem lit
- | E_cast(typ,e) ->
- expV aexp_needed e
+ | E_cast(typ,e) -> expV aexp_needed e
| E_tuple exps ->
parens (align (group (separate_map (comma ^^ break 1) expN exps)))
| E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
@@ -807,10 +810,9 @@ 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
- let epp = anglebars (space ^^ (align (separate_map
- (semi_sp ^^ break 1)
- (doc_fexp ctxt recordtyp) fexps)) ^^ space) in
- if aexp_needed then parens epp else epp
+ wrap_parens (anglebars (space ^^ (align (separate_map
+ (semi_sp ^^ break 1)
+ (doc_fexp ctxt recordtyp) fexps)) ^^ space))
| E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
let recordtyp = match annot with
| Some (env, Typ_aux (Typ_id tid,_), _)
@@ -829,7 +831,7 @@ let doc_exp_lem, doc_let_lem =
let start = match nexp_simp start with
| Nexp_aux (Nexp_constant i, _) -> Big_int.to_string i
| _ -> if dir then "0" else string_of_int (List.length exps) in
- let expspp =
+ (* let expspp =
match exps with
| [] -> empty
| e :: es ->
@@ -840,7 +842,8 @@ let doc_exp_lem, doc_let_lem =
expN e),
if count = 20 then 0 else count + 1)
(expN e,0) es in
- align (group expspp) in
+ align (group expspp) in *)
+ let expspp = align (group (flow_map (semi ^^ break 0) expN exps)) in
let epp = brackets expspp in
let (epp,aexp_needed) =
if is_bit_typ etyp && !opt_mwords then
@@ -858,28 +861,24 @@ let doc_exp_lem, doc_let_lem =
brackets (separate_map semi (expN) exps)
| E_case(e,pexps) ->
let only_integers e = expY e in
- let epp =
- group ((separate space [string "match"; only_integers e; string "with"]) ^/^
- (separate_map (break 1) (doc_case ctxt) pexps) ^/^
- (string "end")) in
- if aexp_needed then parens (align epp) else align epp
+ wrap_parens
+ (group ((separate space [string "match"; only_integers e; string "with"]) ^/^
+ (separate_map (break 1) (doc_case ctxt) pexps) ^/^
+ (string "end")))
| E_try (e, pexps) ->
if effectful (effect_of e) then
let try_catch = if ctxt.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 ctxt) pexps) ^/^
- (string "end)")) in
- if aexp_needed then parens (align epp) else align epp
+ wrap_parens
+ (group ((separate space [string try_catch; expY e; string "(function "]) ^/^
+ (separate_map (break 1) (doc_case ctxt) pexps) ^/^
+ (string "end)")))
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
+ align (liftR (separate space [string "throw"; expY e]))
| 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
+ align (liftR (separate space [string "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")
@@ -905,9 +904,9 @@ let doc_exp_lem, doc_let_lem =
in
infix 0 1 middle (expV b e1) (expN e2)
in
- if aexp_needed then parens (align epp) else epp
+ wrap_parens (align epp)
| E_internal_return (e1) ->
- separate space [string "return"; expY e1]
+ wrap_parens (align (separate space [string "return"; expY e1]))
| E_sizeof nexp ->
(match nexp_simp nexp with
| Nexp_aux (Nexp_constant i, _) -> doc_lit_lem (L_aux (L_num i, l))
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index a59db812..6ea669f9 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -420,6 +420,7 @@ and doc_atomic_lexp (LEXP_aux (l_aux, _) as lexp) =
| LEXP_field (lexp, id) -> doc_atomic_lexp lexp ^^ dot ^^ doc_id id
| LEXP_vector (lexp, exp) -> doc_atomic_lexp lexp ^^ brackets (doc_exp exp)
| LEXP_vector_range (lexp, exp1, exp2) -> doc_atomic_lexp lexp ^^ brackets (separate space [doc_exp exp1; string ".."; doc_exp exp2])
+ | LEXP_vector_concat lexps -> parens (separate_map (string " @ ") doc_lexp lexps)
| LEXP_memory (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
| _ -> parens (doc_lexp lexp)
and doc_pexps pexps = surround 2 0 lbrace (separate_map (comma ^^ hardline) doc_pexp pexps) rbrace
diff --git a/src/process_file.ml b/src/process_file.ml
index 7f9ef069..1bf8eee9 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -57,6 +57,7 @@ let opt_lem_mwords = ref false
type out_type =
| Lem_ast_out
| Lem_out of string list
+ | Coq_out of string list
let get_lexbuf f =
let in_chan = open_in f in
@@ -327,6 +328,28 @@ let output_lem filename libs defs =
print ol isa_lemmas;
close_output_with_check ext_ol
+let output_coq filename libs defs =
+ let generated_line = generated_line filename in
+ let types_module = (filename ^ "_types") in
+ let monad_modules = ["Prompt_monad"; "Prompt"; "State"] in
+ let operators_module = "Sail_operators_mwords" in
+ let base_imports = [
+ "Sail_instr_kinds";
+ "Sail_values";
+ operators_module
+ ] @ monad_modules
+ in
+ let ((ot,_, _) as ext_ot) =
+ open_output_with_check_unformatted (filename ^ "_types" ^ ".v") in
+ let ((o,_, _) as ext_o) =
+ open_output_with_check_unformatted (filename ^ ".v") in
+ (Pretty_print_coq.pp_defs_coq
+ (ot, base_imports)
+ (o, base_imports @ (types_module :: libs))
+ defs generated_line);
+ close_output_with_check ext_ot;
+ close_output_with_check ext_o
+
let rec iterate (f : int -> unit) (n : int) : unit =
if n = 0 then ()
else (f n; iterate f (n - 1))
@@ -348,6 +371,8 @@ let output1 libpath out_arg filename defs =
end
| Lem_out libs ->
output_lem f' libs defs
+ | Coq_out libs ->
+ output_coq f' libs defs
let output libpath out_arg files =
List.iter
@@ -378,6 +403,7 @@ let rewrite rewriters defs =
let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
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_coq = rewrite Rewrites.rewrite_defs_lem
let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml
let rewrite_ast_c = rewrite Rewrites.rewrite_defs_c
let rewrite_ast_interpreter = rewrite Rewrites.rewrite_defs_interpreter
diff --git a/src/process_file.mli b/src/process_file.mli
index 2f418ff9..b38b4259 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -56,6 +56,7 @@ val monomorphise_ast : ((string * int) * string) list -> Type_check.Env.t -> Typ
val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_undefined: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_coq : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_c : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_interpreter : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
@@ -81,6 +82,7 @@ val opt_dall_split_errors : bool ref
type out_type =
| Lem_ast_out
| Lem_out of string list (* If present, the strings are files to open in the lem backend*)
+ | Coq_out of string list (* If present, the strings are files to open in the coq backend*)
val output :
string -> (* The path to the library *)
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 08c90803..6212e0da 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -197,6 +197,8 @@ let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match snd annot with
| LEXP_memory (_,es) -> union_eff_exps es
| LEXP_tup les ->
List.fold_left (fun eff le -> union_effects eff (effect_of_lexp le)) no_effect les
+ | LEXP_vector_concat les ->
+ List.fold_left (fun eff le -> union_effects eff (effect_of_lexp le)) no_effect les
| LEXP_vector (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e)
| LEXP_vector_range (lexp,e1,e2) ->
union_effects (effect_of_lexp lexp)
@@ -385,6 +387,7 @@ let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) =
rewrap (LEXP_vector_range (rewriters.rewrite_lexp rewriters lexp,
rewriters.rewrite_exp rewriters exp1,
rewriters.rewrite_exp rewriters exp2))
+ | LEXP_vector_concat lexps -> rewrap (LEXP_vector_concat (List.map (rewriters.rewrite_lexp rewriters) lexps))
| LEXP_field (lexp,id) -> rewrap (LEXP_field (rewriters.rewrite_lexp rewriters lexp,id))
let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) =
@@ -560,6 +563,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
; lEXP_tup : 'lexp list -> 'lexp_aux
; lEXP_vector : 'lexp * 'exp -> 'lexp_aux
; lEXP_vector_range : 'lexp * 'exp * 'exp -> 'lexp_aux
+ ; lEXP_vector_concat : 'lexp list -> 'lexp_aux
; lEXP_field : 'lexp * id -> 'lexp_aux
; lEXP_aux : 'lexp_aux * 'a annot -> 'lexp
; fE_Fexp : id * 'exp -> 'fexp_aux
@@ -639,7 +643,8 @@ and fold_lexp_aux alg = function
| LEXP_vector (lexp,e) -> alg.lEXP_vector (fold_lexp alg lexp, fold_exp alg e)
| LEXP_vector_range (lexp,e1,e2) ->
alg.lEXP_vector_range (fold_lexp alg lexp, fold_exp alg e1, fold_exp alg e2)
- | LEXP_field (lexp,id) -> alg.lEXP_field (fold_lexp alg lexp, id)
+ | LEXP_vector_concat les -> alg.lEXP_vector_concat (List.map (fold_lexp alg) les)
+ | LEXP_field (lexp,id) -> alg.lEXP_field (fold_lexp alg lexp, id)
and fold_lexp alg (LEXP_aux (lexp_aux,annot)) =
alg.lEXP_aux (fold_lexp_aux alg lexp_aux, annot)
and fold_fexp_aux alg (FE_Fexp (id,e)) = alg.fE_Fexp (id, fold_exp alg e)
@@ -710,6 +715,7 @@ let id_exp_alg =
; lEXP_tup = (fun tups -> LEXP_tup tups)
; lEXP_vector = (fun (lexp,e2) -> LEXP_vector (lexp,e2))
; lEXP_vector_range = (fun (lexp,e2,e3) -> LEXP_vector_range (lexp,e2,e3))
+ ; lEXP_vector_concat = (fun lexps -> LEXP_vector_concat lexps)
; lEXP_field = (fun (lexp,id) -> LEXP_field (lexp,id))
; lEXP_aux = (fun (lexp,annot) -> LEXP_aux (lexp,annot))
; fE_Fexp = (fun (id,e) -> FE_Fexp (id,e))
@@ -818,6 +824,9 @@ let compute_exp_alg bot join =
; lEXP_vector = (fun ((vl,lexp),(v2,e2)) -> (join vl v2, LEXP_vector (lexp,e2)))
; lEXP_vector_range = (fun ((vl,lexp),(v2,e2),(v3,e3)) ->
(join_list [vl;v2;v3], LEXP_vector_range (lexp,e2,e3)))
+ ; lEXP_vector_concat = (fun ls ->
+ let (vs,ls) = List.split ls in
+ (join_list vs, LEXP_vector_concat ls))
; lEXP_field = (fun ((vl,lexp),id) -> (vl, LEXP_field (lexp,id)))
; lEXP_aux = (fun ((vl,lexp),annot) -> (vl, LEXP_aux (lexp,annot)))
; fE_Fexp = (fun (id,(v,e)) -> (v, FE_Fexp (id,e)))
@@ -836,3 +845,94 @@ let compute_exp_alg bot join =
; lB_aux = (fun ((vl,lb),annot) -> (vl,LB_aux (lb,annot)))
; pat_alg = compute_pat_alg bot join
}
+
+let pure_pat_alg bot join =
+ let join_list vs = List.fold_left join bot vs in
+ { p_lit = (fun lit -> bot)
+ ; p_wild = bot
+ ; p_as = (fun (v,id) -> v)
+ ; p_typ = (fun (typ,v) -> v)
+ ; p_id = (fun id -> bot)
+ ; p_var = (fun (v,kid) -> v)
+ ; p_app = (fun (id,ps) -> join_list ps)
+ ; p_record = (fun (ps,b) -> join_list ps)
+ ; p_vector = join_list
+ ; p_vector_concat = join_list
+ ; p_tup = join_list
+ ; p_list = join_list
+ ; p_string_append = join_list
+ ; p_cons = (fun (vh,vt) -> join vh vt)
+ ; p_aux = (fun (v,annot) -> v)
+ ; fP_aux = (fun (v,annot) -> v)
+ ; fP_Fpat = (fun (id,v) -> v)
+ }
+
+let pure_exp_alg bot join =
+ let join_list vs = List.fold_left join bot vs in
+ { e_block = join_list
+ ; e_nondet = join_list
+ ; e_id = (fun id -> bot)
+ ; e_ref = (fun id -> bot)
+ ; e_lit = (fun lit -> bot)
+ ; e_cast = (fun (typ,v) -> v)
+ ; e_app = (fun (id,es) -> join_list es)
+ ; e_app_infix = (fun (v1,id,v2) -> join v1 v2)
+ ; e_tuple = join_list
+ ; e_if = (fun (v1,v2,v3) -> join_list [v1;v2;v3])
+ ; e_for = (fun (id,v1,v2,v3,order,v4) -> join_list [v1;v2;v3;v4])
+ ; e_loop = (fun (lt, v1, v2) -> join v1 v2)
+ ; e_vector = join_list
+ ; e_vector_access = (fun (v1,v2) -> join v1 v2)
+ ; e_vector_subrange = (fun (v1,v2,v3) -> join_list [v1;v2;v3])
+ ; e_vector_update = (fun (v1,v2,v3) -> join_list [v1;v2;v3])
+ ; e_vector_update_subrange = (fun (v1,v2,v3,v4) -> join_list [v1;v2;v3;v4])
+ ; e_vector_append = (fun (v1,v2) -> join v1 v2)
+ ; e_list = join_list
+ ; e_cons = (fun (v1,v2) -> join v1 v2)
+ ; e_record = (fun vs -> vs)
+ ; e_record_update = (fun (v1,vf) -> join v1 vf)
+ ; e_field = (fun (v1,id) -> v1)
+ ; e_case = (fun (v1,vps) -> join_list (v1::vps))
+ ; e_try = (fun (v1,vps) -> join_list (v1::vps))
+ ; e_let = (fun (vl,v2) -> join vl v2)
+ ; e_assign = (fun (vl,v2) -> join vl v2)
+ ; e_sizeof = (fun nexp -> bot)
+ ; e_constraint = (fun nc -> bot)
+ ; e_exit = (fun v1 -> v1)
+ ; e_throw = (fun v1 -> v1)
+ ; e_return = (fun v1 -> v1)
+ ; e_assert = (fun (v1,v2) -> join v1 v2)
+ ; e_internal_cast = (fun (a,v1) -> v1)
+ ; e_internal_exp = (fun a -> bot)
+ ; e_internal_exp_user = (fun (a1,a2) -> bot)
+ ; e_comment = (fun c -> bot)
+ ; e_comment_struc = (fun v -> bot)
+ ; e_internal_let = (fun (vl, v2, v3) -> join_list [vl;v2;v3])
+ ; e_internal_plet = (fun (vp, v1, v2) -> join_list [vp;v1;v2])
+ ; e_internal_return = (fun v -> v)
+ ; e_internal_value = (fun v -> bot)
+ ; e_aux = (fun (v,annot) -> v)
+ ; lEXP_id = (fun id -> bot)
+ ; lEXP_deref = (fun v -> v)
+ ; lEXP_memory = (fun (id,es) -> join_list es)
+ ; lEXP_cast = (fun (typ,id) -> bot)
+ ; lEXP_tup = join_list
+ ; lEXP_vector = (fun (vl,v2) -> join vl v2)
+ ; lEXP_vector_range = (fun (vl,v2,v3) -> join_list [vl;v2;v3])
+ ; lEXP_vector_concat = join_list
+ ; lEXP_field = (fun (vl,id) -> vl)
+ ; lEXP_aux = (fun (vl,annot) -> vl)
+ ; fE_Fexp = (fun (id,v) -> v)
+ ; fE_aux = (fun (vf,annot) -> vf)
+ ; fES_Fexps = (fun (vs,b) -> join_list vs)
+ ; fES_aux = (fun (vf,annot) -> vf)
+ ; def_val_empty = bot
+ ; def_val_dec = (fun v -> v)
+ ; def_val_aux = (fun (v,aux) -> v)
+ ; pat_exp = (fun (vp,v) -> join vp v)
+ ; pat_when = (fun (vp,v,v') -> join_list [vp;v;v'])
+ ; pat_aux = (fun (v,a) -> v)
+ ; lB_val = (fun (vp,v) -> join vp v)
+ ; lB_aux = (fun (vl,annot) -> vl)
+ ; pat_alg = pure_pat_alg bot join
+ }
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 90c15b16..edc93e5d 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -156,6 +156,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
; lEXP_tup : 'lexp list -> 'lexp_aux
; lEXP_vector : 'lexp * 'exp -> 'lexp_aux
; lEXP_vector_range : 'lexp * 'exp * 'exp -> 'lexp_aux
+ ; lEXP_vector_concat : 'lexp list -> 'lexp_aux
; lEXP_field : 'lexp * id -> 'lexp_aux
; lEXP_aux : 'lexp_aux * 'a annot -> 'lexp
; fE_Fexp : id * 'exp -> 'fexp_aux
@@ -168,7 +169,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
; pat_exp : 'pat * 'exp -> 'pexp_aux
; pat_when : 'pat * 'exp * 'exp -> 'pexp_aux
; pat_aux : 'pexp_aux * 'a annot -> 'pexp
- ; lB_val : 'pat * 'exp -> 'letbind_aux
+ ; lB_val : 'pat * 'exp -> 'letbind_aux
; lB_aux : 'letbind_aux * 'a annot -> 'letbind
; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg
}
@@ -181,6 +182,10 @@ val fold_exp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_a
'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a exp -> 'exp
+val fold_letbind : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
+ 'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
+ 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a letbind -> 'letbind
+
val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a pexp -> 'pexp
@@ -203,6 +208,15 @@ val compute_exp_alg : 'b -> ('b -> 'b -> 'b) ->
('b * 'a letbind_aux),('b * 'a letbind),
('b * 'a pat),('b * 'a pat_aux),('b * 'a fpat),('b * 'a fpat_aux)) exp_alg
+val pure_pat_alg : 'b -> ('b -> 'b -> 'b) -> ('a,'b,'b,'b,'b) pat_alg
+
+val pure_exp_alg : 'b -> ('b -> 'b -> 'b) ->
+ ('a,'b,'b,'b,'b,'b,
+ 'b,'b,'b,
+ 'b,'b,'b,'b,
+ 'b,'b,
+ 'b,'b,'b,'b) exp_alg
+
val simple_annot : Parse_ast.l -> typ -> Parse_ast.l * tannot
val add_p_typ : typ -> tannot pat -> tannot pat
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 3f6f95f4..b7ebd073 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -127,7 +127,7 @@ let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with
| LEXP_memory _ | LEXP_deref _ -> false
| LEXP_id id
| LEXP_cast (_, id) -> id_is_local_var id env
- | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps
+ | LEXP_tup lexps | LEXP_vector_concat lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps
| LEXP_vector (lexp,_)
| LEXP_vector_range (lexp,_,_)
| LEXP_field (lexp,_) -> lexp_is_local lexp env
@@ -136,7 +136,7 @@ let rec lexp_is_local_intro (LEXP_aux (lexp, _)) env = match lexp with
| LEXP_memory _ | LEXP_deref _ -> false
| LEXP_id id
| LEXP_cast (_, id) -> id_is_unbound id env
- | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local_intro lexp env) lexps
+ | LEXP_tup lexps | LEXP_vector_concat lexps -> List.for_all (fun lexp -> lexp_is_local_intro lexp env) lexps
| LEXP_vector (lexp,_)
| LEXP_vector_range (lexp,_,_)
| LEXP_field (lexp,_) -> lexp_is_local_intro lexp env
@@ -190,16 +190,18 @@ let lookup_equal_kids env =
List.fold_left add_nc KBindings.empty (Env.get_constraints env)
let lookup_constant_kid env kid =
- try
- let kids = KBindings.find kid (lookup_equal_kids env) in
- let check_nc const nc = match const, nc with
- | None, NC_aux (NC_equal (Nexp_aux (Nexp_var kid, _), Nexp_aux (Nexp_constant i, _)), _)
- when KidSet.mem kid kids ->
- Some i
- | _, _ -> const
- in
- List.fold_left check_nc None (Env.get_constraints env)
- with Not_found -> None
+ let kids =
+ match KBindings.find kid (lookup_equal_kids env) with
+ | kids -> kids
+ | exception Not_found -> KidSet.singleton kid
+ in
+ let check_nc const nc = match const, nc with
+ | None, NC_aux (NC_equal (Nexp_aux (Nexp_var kid, _), Nexp_aux (Nexp_constant i, _)), _)
+ when KidSet.mem kid kids ->
+ Some i
+ | _, _ -> const
+ in
+ List.fold_left check_nc None (Env.get_constraints env)
let rec rewrite_nexp_ids env (Nexp_aux (nexp, l) as nexp_aux) = match nexp with
| Nexp_id id -> rewrite_nexp_ids env (Env.get_num_def id env)
@@ -241,8 +243,19 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids =
| (l, None) -> (l, None)
in
- rewrite_defs_base {
- rewriters_base with rewrite_exp = (fun _ -> map_exp_annot rewrite_annot)
+ let rewrite_def rewriters = function
+ | DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), (l, Some (env, typ, eff)))) ->
+ let typschm = match typschm with
+ | TypSchm_aux (TypSchm_ts (tq, typ), l) ->
+ TypSchm_aux (TypSchm_ts (tq, rewrite_typ env typ), l)
+ in
+ let a = rewrite_annot (l, Some (env, typ, eff)) in
+ DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), a))
+ | d -> Rewriter.rewrite_def rewriters d
+ in
+
+ rewrite_defs_base { rewriters_base with
+ rewrite_exp = (fun _ -> map_exp_annot rewrite_annot); rewrite_def = rewrite_def
},
rewrite_typ
@@ -281,7 +294,7 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
scope. *)
| Some size when prove env (nc_eq (nsum size (nint 1)) nexp) ->
let one_exp = infer_exp env (mk_lit_exp (L_num (Big_int.of_int 1))) in
- Some (E_aux (E_app (mk_id "add_range", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect))))
+ Some (E_aux (E_app (mk_id "add_atom", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect))))
| _ ->
begin
match destruct_vector env typ with
@@ -293,12 +306,12 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
let rec split_nexp (Nexp_aux (nexp_aux, l) as nexp) =
match nexp_aux with
| Nexp_sum (n1, n2) ->
- mk_exp (E_app (mk_id "add_range", [split_nexp n1; split_nexp n2]))
+ mk_exp (E_app (mk_id "add_atom", [split_nexp n1; split_nexp n2]))
| Nexp_minus (n1, n2) ->
- mk_exp (E_app (mk_id "sub_range", [split_nexp n1; split_nexp n2]))
+ mk_exp (E_app (mk_id "sub_atom", [split_nexp n1; split_nexp n2]))
| Nexp_times (n1, n2) ->
- mk_exp (E_app (mk_id "mult_range", [split_nexp n1; split_nexp n2]))
- | Nexp_neg nexp -> mk_exp (E_app (mk_id "negate_range", [split_nexp nexp]))
+ mk_exp (E_app (mk_id "mult_atom", [split_nexp n1; split_nexp n2]))
+ | Nexp_neg nexp -> mk_exp (E_app (mk_id "negate_atom", [split_nexp nexp]))
| _ -> mk_exp (E_sizeof nexp)
in
let rec rewrite_e_aux split_sizeof (E_aux (e_aux, (l, _)) as orig_exp) =
@@ -487,6 +500,7 @@ let rewrite_sizeof (Defs defs) =
; lEXP_tup = (fun tups -> let (tups,tups') = List.split tups in (LEXP_tup tups, LEXP_tup tups'))
; lEXP_vector = (fun ((lexp,lexp'),(e2,e2')) -> (LEXP_vector (lexp,e2), LEXP_vector (lexp',e2')))
; lEXP_vector_range = (fun ((lexp,lexp'),(e2,e2'),(e3,e3')) -> (LEXP_vector_range (lexp,e2,e3), LEXP_vector_range (lexp',e2',e3')))
+ ; lEXP_vector_concat = (fun lexps -> let (lexps,lexps') = List.split lexps in (LEXP_vector_concat lexps, LEXP_vector_concat lexps'))
; lEXP_field = (fun ((lexp,lexp'),id) -> (LEXP_field (lexp,id), LEXP_field (lexp',id)))
; lEXP_aux = (fun ((lexp,lexp'),annot) -> (LEXP_aux (lexp,annot), LEXP_aux (lexp',annot)))
; fE_Fexp = (fun (id,(e,e')) -> (FE_Fexp (id,e), FE_Fexp (id,e')))
@@ -1909,6 +1923,16 @@ let is_funcl_rec (FCL_aux (FCL_Funcl (id, pexp), _)) =
E_app_infix (e1, f, e2))) }
exp)
+
+let pat_var (P_aux (paux, a)) =
+ let env = env_of_annot a in
+ let is_var id =
+ not (Env.is_union_constructor id env) &&
+ match Env.lookup_id id env with Enum _ -> false | _ -> true
+ in match paux with
+ | (P_as (_, id) | P_id id) when is_var id -> Some id
+ | _ -> None
+
(* Split out function clauses for individual union constructor patterns
(e.g. AST nodes) into auxiliary functions. Used for the execute function. *)
let rewrite_split_fun_constr_pats fun_name (Defs defs) =
@@ -1933,10 +1957,10 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
Bindings.add aux_fun_id (aux_clauses @ [aux_funcl]) aux_funs
with Not_found ->
let argpats, argexps = List.split (List.mapi
- (fun idx (P_aux (paux, a)) ->
- let id = match paux with
- | P_as (_, id) | P_id id -> id
- | _ -> mk_id ("arg" ^ string_of_int idx)
+ (fun idx (P_aux (_,a) as pat) ->
+ let id = match pat_var pat with
+ | Some id -> id
+ | None -> mk_id ("arg" ^ string_of_int idx)
in
P_aux (P_id id, a), E_aux (E_id id, a))
args)
@@ -2290,11 +2314,11 @@ let rewrite_simple_types (Defs defs) =
let defs = Defs (List.map simple_def defs) in
rewrite_defs_base simple_defs defs
-let rewrite_tuple_vector_assignments defs =
+let rewrite_vector_concat_assignments defs =
let assign_tuple e_aux annot =
let env = env_of_annot annot in
match e_aux with
- | E_assign (LEXP_aux (LEXP_tup lexps, lannot), exp) ->
+ | E_assign (LEXP_aux (LEXP_vector_concat lexps, lannot), exp) ->
let typ = Env.base_typ_of env (typ_of exp) in
if is_vector_typ typ then
(* let _ = Pretty_print_common.print stderr (Pretty_print_sail.doc_exp (E_aux (e_aux, annot))) in *)
@@ -2527,8 +2551,11 @@ let rewrite_defs_letbind_effects =
| LEXP_vector_range (lexp,e1,e2) ->
n_lexp lexp (fun lexp ->
n_exp_name e1 (fun e1 ->
- n_exp_name e2 (fun e2 ->
+ n_exp_name e2 (fun e2 ->
k (fix_eff_lexp (LEXP_aux (LEXP_vector_range (lexp,e1,e2),annot))))))
+ | LEXP_vector_concat es ->
+ n_lexpL es (fun es ->
+ k (fix_eff_lexp (LEXP_aux (LEXP_vector_concat es,annot))))
| LEXP_field (lexp,id) ->
n_lexp lexp (fun lexp ->
k (fix_eff_lexp (LEXP_aux (LEXP_field (lexp,id),annot))))
@@ -2563,6 +2590,14 @@ let rewrite_defs_letbind_effects =
| E_cast (typ,exp') ->
n_exp_name exp' (fun exp' ->
k (rewrap (E_cast (typ,exp'))))
+ | E_app (op_bool, [l; r])
+ when string_of_id op_bool = "and_bool" || string_of_id op_bool = "or_bool" ->
+ (* Leave effectful operands of Boolean "and"/"or" in place to allow
+ short-circuiting. *)
+ let newreturn = effectful l || effectful r in
+ let l = n_exp_term newreturn l in
+ let r = n_exp_term newreturn r in
+ k (rewrap (E_app (op_bool, [l; r])))
| E_app (id,exps) ->
n_exp_nameL exps (fun exps ->
k (rewrap (E_app (id,exps))))
@@ -3203,20 +3238,21 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
|> mk_var_exps_pats pl env
in
let exp4 = rewrite_var_updates (add_vars overwrite exp4 vars) in
- let ord_exp, kids, constr, lower, upper =
- match destruct_range env (typ_of exp1), destruct_range env (typ_of exp2) with
+ let ord_exp, kids, constr, lower, upper, lower_exp, upper_exp =
+ match destruct_numeric env (typ_of exp1), destruct_numeric env (typ_of exp2) with
| None, _ | _, None ->
raise (Reporting_basic.err_unreachable el "Could not determine loop bounds")
- | Some (kids1, constr1, l1, u1), Some (kids2, constr2, l2, u2) ->
+ | Some (kids1, constr1, n1), Some (kids2, constr2, n2) ->
let kids = kids1 @ kids2 in
let constr = nc_and constr1 constr2 in
- let ord_exp, lower, upper =
+ let ord_exp, lower, upper, lower_exp, upper_exp =
if is_order_inc order
- then (annot_exp (E_lit (mk_lit L_true)) el env bool_typ, l1, u2)
- else (annot_exp (E_lit (mk_lit L_false)) el env bool_typ, l2, u1)
+ then (annot_exp (E_lit (mk_lit L_true)) el env bool_typ, n1, n2, exp1, exp2)
+ else (annot_exp (E_lit (mk_lit L_false)) el env bool_typ, n2, n1, exp2, exp1)
in
- ord_exp, kids, constr, lower, upper
+ ord_exp, kids, constr, lower, upper, lower_exp, upper_exp
in
+ (* Bind the loop variable in the body, annotated with constraints *)
let lvar_kid = mk_kid ("loop_" ^ string_of_id id) in
let lvar_nc = nc_and constr (nc_and (nc_lteq lower (nvar lvar_kid)) (nc_lteq (nvar lvar_kid) upper)) in
let lvar_typ = mk_typ (Typ_exist (lvar_kid :: kids, lvar_nc, atom_typ (nvar lvar_kid))) in
@@ -3225,7 +3261,33 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
TP_aux (TP_var lvar_kid, gen_loc el))) el env lvar_typ)) in
let lb = fix_eff_lb (annot_letbind (lvar_pat, exp1) el env lvar_typ) in
let body = fix_eff_exp (annot_exp (E_let (lb, exp4)) el env (typ_of exp4)) in
- let v = fix_eff_exp (annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; body])) el env (typ_of body)) in
+ (* If lower > upper, the loop body never gets executed, and the type
+ checker might not be able to prove that the initial value exp1
+ satisfies the constraints on the loop variable.
+
+ Make this explicit by guarding the loop body with lower <= upper.
+ (for type-checking; the guard is later removed again by the Lem
+ pretty-printer). This could be implemented with an assertion, but
+ that would force the loop to be effectful, so we use an if-expression
+ instead. This code assumes that the loop bounds have (possibly
+ existential) atom types, and the loop body has type unit. *)
+ let lower_kid = mk_kid ("loop_" ^ string_of_id id ^ "_lower") in
+ let lower_pat = P_var (annot_pat P_wild el env (typ_of lower_exp), mk_typ_pat (TP_app (mk_id "atom", [mk_typ_pat (TP_var lower_kid)]))) in
+ let lb_lower = annot_letbind (lower_pat, lower_exp) el env (typ_of lower_exp) in
+ let upper_kid = mk_kid ("loop_" ^ string_of_id id ^ "_upper") in
+ let upper_pat = P_var (annot_pat P_wild el env (typ_of upper_exp), mk_typ_pat (TP_app (mk_id "atom", [mk_typ_pat (TP_var upper_kid)]))) in
+ let lb_upper = annot_letbind (upper_pat, upper_exp) el env (typ_of upper_exp) in
+ let guard = annot_exp (E_constraint (nc_lteq (nvar lower_kid) (nvar upper_kid))) el env bool_typ in
+ let unit_exp = annot_exp (E_lit (mk_lit L_unit)) el env unit_typ in
+ let skip_val = tuple_exp (if overwrite then vars else unit_exp :: vars) in
+ let guarded_body =
+ fix_eff_exp (annot_exp (E_let (lb_lower,
+ fix_eff_exp (annot_exp (E_let (lb_upper,
+ fix_eff_exp (annot_exp (E_if (guard, body, skip_val))
+ el env (typ_of exp4))))
+ el env (typ_of exp4))))
+ el env (typ_of exp4)) in
+ let v = fix_eff_exp (annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; guarded_body])) el env (typ_of body)) in
Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats))
| E_loop(loop,cond,body) ->
let vars, varpats =
@@ -3254,7 +3316,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
(* after rewrite_defs_letbind_effects c has no variable updates *)
let env = env_of_annot annot in
let typ = typ_of e1 in
- let eff = union_eff_exps [e1;e2] in
+ let eff = union_eff_exps [c;e1;e2] in
let v = E_aux (E_if (c,e1,e2), (gen_loc el, Some (env, typ, eff))) in
Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats))
| E_case (e1,ps) ->
@@ -3712,7 +3774,7 @@ let recheck_defs defs = fst (check initial_env defs)
let rewrite_defs_lem = [
("realise_mappings", rewrite_defs_realise_mappings);
- ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
+ ("vector_concat_assignments", rewrite_vector_concat_assignments);
("tuple_assignments", rewrite_tuple_assignments);
("simple_assignments", rewrite_simple_assignments);
("remove_vector_concat", rewrite_defs_remove_vector_concat);
@@ -3752,7 +3814,7 @@ let rewrite_defs_ocaml = [
("pat_string_append", rewrite_defs_pat_string_append);
("mapping_builtins", rewrite_defs_mapping_builtins);
("pat_lits", rewrite_defs_pat_lits);
- ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
+ ("vector_concat_assignments", rewrite_vector_concat_assignments);
("tuple_assignments", rewrite_tuple_assignments);
("simple_assignments", rewrite_simple_assignments);
("remove_vector_concat", rewrite_defs_remove_vector_concat);
@@ -3774,7 +3836,7 @@ let rewrite_defs_c = [
("pat_string_append", rewrite_defs_pat_string_append);
("mapping_builtins", rewrite_defs_mapping_builtins);
("pat_lits", rewrite_defs_pat_lits);
- ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
+ ("vector_concat_assignments", rewrite_vector_concat_assignments);
("tuple_assignments", rewrite_tuple_assignments);
("simple_assignments", rewrite_simple_assignments);
("remove_vector_concat", rewrite_defs_remove_vector_concat);
@@ -3793,7 +3855,7 @@ let rewrite_defs_interpreter = [
("realise_mappings", rewrite_defs_realise_mappings);
("pat_string_append", rewrite_defs_pat_string_append);
("mapping_builtins", rewrite_defs_mapping_builtins);
- ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
+ ("vector_concat_assignments", rewrite_vector_concat_assignments);
("tuple_assignments", rewrite_tuple_assignments);
("simple_assignments", rewrite_simple_assignments);
("remove_vector_concat", rewrite_defs_remove_vector_concat);
diff --git a/src/sail.ml b/src/sail.ml
index 85719f4d..f459d774 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -62,9 +62,11 @@ let opt_print_lem = ref false
let opt_print_ocaml = ref false
let opt_print_c = ref false
let opt_print_latex = ref false
+let opt_print_coq = ref false
let opt_memo_z3 = ref false
let opt_sanity = ref false
let opt_libs_lem = ref ([]:string list)
+let opt_libs_coq = ref ([]:string list)
let opt_file_arguments = ref ([]:string list)
let opt_mono_split = ref ([]:((string * int) * string) list)
let opt_process_elf : string option ref = ref None
@@ -120,6 +122,12 @@ let options = Arg.align ([
( "-lem_mwords",
Arg.Set Pretty_print_lem.opt_mwords,
" use native machine word library for Lem output");
+ ( "-coq",
+ Arg.Set opt_print_coq,
+ " output a Coq translated version of the input");
+ ( "-coq_lib",
+ Arg.String (fun l -> opt_libs_coq := l::!opt_libs_coq),
+ "<filename> provide additional library to open in Coq output");
( "-latex_prefix",
Arg.String (fun prefix -> Latex.opt_prefix_latex := prefix),
" set a custom prefix for generated latex command (default sail)");
@@ -149,6 +157,9 @@ let options = Arg.align ([
( "-enum_casts",
Arg.Set Initial_check.opt_enum_casts,
" allow enumerations to be automatically casted to numeric range types");
+ ( "-no_lexp_bounds_check",
+ Arg.Set Type_check.opt_no_lexp_bounds_check,
+ " turn off bounds checking for vector assignments in l-expressions");
( "-no_effects",
Arg.Set Type_check.opt_no_effects,
" (experimental) turn off effect checking");
@@ -310,6 +321,12 @@ let main() =
let ast_lem = rewrite_ast_lem ast_lem in
output "" (Lem_out (!opt_libs_lem)) [out_name,ast_lem]
else ());
+ (if !(opt_print_coq)
+ then
+ let type_envs, ast_coq = State.add_regstate_defs true type_envs ast in
+ let ast_coq = rewrite_ast_coq ast_coq in
+ output "" (Coq_out (!opt_libs_coq)) [out_name,ast_coq]
+ else ());
(if !(opt_print_latex)
then
begin
diff --git a/src/state.ml b/src/state.ml
index 59fb9995..5a360456 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -60,6 +60,11 @@ open Pretty_print_sail
let defs_of_string = ast_of_def_string Ast_util.inc_ord
+let is_defined defs name = IdSet.mem (mk_id name) (ids_of_defs (Defs defs))
+
+let has_default_order defs =
+ List.exists (function DEF_default (DT_aux (DT_order _, _)) -> true | _ -> false) defs
+
let find_registers defs =
List.fold_left
(fun acc def ->
@@ -77,18 +82,100 @@ let generate_regstate = function
| [] -> ["type regstate = unit"]
| registers ->
let reg (typ, id) = Printf.sprintf "%s : %s" (string_of_id id) (to_string (doc_typ typ)) in
- let initreg (_, id) = Printf.sprintf "%s = undefined" (string_of_id id) in
- let regstate =
- "struct regstate = { " ^
- (String.concat ", " (List.map reg registers)) ^
- " }"
- in
- let initstate =
- "let initial_regstate : regstate = struct { " ^
- (String.concat ", " (List.map initreg registers)) ^
- " }"
- in
- regstate :: (if !Initial_check.opt_undefined_gen then [initstate] else [])
+ ["struct regstate = { " ^ (String.concat ", " (List.map reg registers)) ^ " }"]
+
+let generate_initial_regstate defs =
+ let registers = find_registers defs in
+ if registers = [] then [] else
+ try
+ (* Recursively choose a default value for every type in the spec.
+ vals, constructed below, maps user-defined types to default values. *)
+ let rec lookup_init_val vals (Typ_aux (typ_aux, _) as typ) =
+ match typ_aux with
+ | Typ_id id ->
+ if string_of_id id = "bool" then "false" else
+ if string_of_id id = "bit" then "bitzero" else
+ if string_of_id id = "int" then "0" else
+ if string_of_id id = "nat" then "0" else
+ if string_of_id id = "real" then "0" else
+ if string_of_id id = "string" then "\"\"" else
+ if string_of_id id = "unit" then "()" else
+ Bindings.find id vals []
+ | Typ_app (id, _) when string_of_id id = "list" -> "[||]"
+ | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]) when string_of_id id = "atom" ->
+ string_of_nexp nexp
+ | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _); _]) when string_of_id id = "range" ->
+ string_of_nexp nexp
+ | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant len, _)), _); _ ;
+ Typ_arg_aux (Typ_arg_typ etyp, _)])
+ when string_of_id id = "vector" ->
+ (* Output a list of initial values of the vector elements, or a
+ literal binary zero value if this is a bitvector and the
+ environment has a default indexing order (required by the
+ typechecker for binary and hex literals) *)
+ let literal_bitvec = is_bit_typ etyp && has_default_order defs in
+ let init_elem = if literal_bitvec then "0" else lookup_init_val vals etyp in
+ let rec elems len =
+ if (Nat_big_num.less_equal len Nat_big_num.zero) then [] else
+ init_elem :: elems (Nat_big_num.pred len)
+ in
+ if literal_bitvec then "0b" ^ (String.concat "" (elems len)) else
+ "[" ^ (String.concat ", " (elems len)) ^ "]"
+ | Typ_app (id, args) -> Bindings.find id vals args
+ | Typ_tup typs ->
+ "(" ^ (String.concat ", " (List.map (lookup_init_val vals) typs)) ^ ")"
+ | Typ_exist (_, _, typ) -> lookup_init_val vals typ
+ | _ -> raise Not_found
+ in
+ (* Helper functions to instantiate type arguments *)
+ let typ_subst_targ kid (Typ_arg_aux (arg, _)) typ = match arg with
+ | Typ_arg_nexp (Nexp_aux (nexp, _)) -> typ_subst_nexp kid nexp typ
+ | Typ_arg_typ (Typ_aux (typ', _)) -> typ_subst_typ kid typ' typ
+ | Typ_arg_order (Ord_aux (ord, _)) -> typ_subst_order kid ord typ
+ in
+ let typ_subst_quant_item typ (QI_aux (qi, _)) arg = match qi with
+ | QI_id (KOpt_aux ((KOpt_none kid | KOpt_kind (_, kid)), _)) ->
+ typ_subst_targ kid arg typ
+ | _ -> typ
+ in
+ let typ_subst_typquant tq args typ =
+ List.fold_left2 typ_subst_quant_item typ (quant_items tq) args
+ in
+ let add_typ_init_val vals = function
+ | TD_enum (id, _, id1 :: _, _) ->
+ (* Choose the first value of an enumeration type as default *)
+ Bindings.add id (fun _ -> string_of_id id1) vals
+ | TD_variant (id, _, tq, (Tu_aux (Tu_ty_id (typ1, id1), _)) :: _, _) ->
+ (* Choose the first variant of a union type as default *)
+ let init_val args =
+ let typ1 = typ_subst_typquant tq args typ1 in
+ string_of_id id1 ^ " (" ^ lookup_init_val vals typ1 ^ ")"
+ in
+ Bindings.add id init_val vals
+ | TD_abbrev (id, _, TypSchm_aux (TypSchm_ts (tq, typ), _)) ->
+ let init_val args = lookup_init_val vals (typ_subst_typquant tq args typ) in
+ Bindings.add id init_val vals
+ | TD_record (id, _, tq, fields, _) ->
+ let init_val args =
+ let init_field (typ, id) =
+ let typ = typ_subst_typquant tq args typ in
+ string_of_id id ^ " = " ^ lookup_init_val vals typ
+ in
+ "struct { " ^ (String.concat ", " (List.map init_field fields)) ^ " }"
+ in
+ Bindings.add id init_val vals
+ | TD_bitfield (id, typ, _) ->
+ Bindings.add id (fun _ -> lookup_init_val vals typ) vals
+ | _ -> vals
+ in
+ let init_vals = List.fold_left (fun vals def -> match def with
+ | DEF_type (TD_aux (td, _)) -> add_typ_init_val vals td
+ | _ -> vals) Bindings.empty defs
+ in
+ let init_reg (typ, id) = string_of_id id ^ " = " ^ lookup_init_val init_vals typ in
+ ["let initial_regstate : regstate = struct { " ^ (String.concat ", " (List.map init_reg registers)) ^ " }"]
+ with
+ | _ -> [] (* Do not generate an initial register state if anything goes wrong *)
let rec regval_constr_id mwords (Typ_aux (t, l) as typ) = match t with
| Typ_id id -> id
@@ -135,9 +222,8 @@ let generate_regval_typ typs =
(String.concat ", " (builtins :: List.map constr (Bindings.bindings typs))) ^
" }"]
-let add_regval_conv id typ defs =
+let add_regval_conv id typ (Defs defs) =
let id = string_of_id id in
- let is_defined name = IdSet.mem (mk_id name) (ids_of_defs defs) in
let typ_str = to_string (doc_typ typ) in
(* Create a function that converts from regval to the target type. *)
let from_name = id ^ "_of_regval" in
@@ -146,14 +232,14 @@ let add_regval_conv id typ defs =
Printf.sprintf "function %s Regval_%s(v) = Some(v)" from_name id;
Printf.sprintf "and %s _ = None()" from_name
] in
- let from_defs = if is_defined from_name then [] else [from_val; from_function] in
+ let from_defs = if is_defined defs from_name then [] else [from_val; from_function] in
(* Create a function that converts from target type to regval. *)
let to_name = "regval_of_" ^ id in
let to_val = Printf.sprintf "val %s : %s -> register_value" to_name typ_str in
let to_function = Printf.sprintf "function %s v = Regval_%s(v)" to_name id in
- let to_defs = if is_defined to_name then [] else [to_val; to_function] in
+ let to_defs = if is_defined defs to_name then [] else [to_val; to_function] in
let cdefs = concat_ast (List.map defs_of_string (from_defs @ to_defs)) in
- append_ast defs cdefs
+ append_ast (Defs defs) cdefs
let rec regval_convs_lem mwords (Typ_aux (t, _) as typ) = match t with
| Typ_app _ when is_vector_typ typ && not (mwords && is_bitvector_typ typ) ->
@@ -306,6 +392,85 @@ let generate_isa_lemmas mwords (Defs defs : tannot defs) =
hardline ^^ hardline ^^
separate_map (hardline ^^ hardline) register_lemmas registers
+let rec regval_convs_coq (Typ_aux (t, _) as typ) = match t with
+ | Typ_app _ when is_vector_typ typ && not (is_bitvector_typ typ) ->
+ let size, ord, etyp = vector_typ_args_of typ in
+ let size = string_of_nexp (nexp_simp size) in
+ let is_inc = if is_order_inc ord then "true" else "false" in
+ let etyp_of, of_etyp = regval_convs_coq etyp in
+ "(fun v => vector_of_regval " ^ etyp_of ^ " v)",
+ "(fun v => regval_of_vector " ^ of_etyp ^ " " ^ size ^ " " ^ is_inc ^ " v)"
+ | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)])
+ when string_of_id id = "list" ->
+ let etyp_of, of_etyp = regval_convs_coq etyp in
+ "(fun v => list_of_regval " ^ etyp_of ^ " v)",
+ "(fun v => regval_of_list " ^ of_etyp ^ " v)"
+ | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)])
+ when string_of_id id = "option" ->
+ let etyp_of, of_etyp = regval_convs_coq etyp in
+ "(fun v => option_of_regval " ^ etyp_of ^ " v)",
+ "(fun v => regval_of_option " ^ of_etyp ^ " v)"
+ | _ ->
+ let id = string_of_id (regval_constr_id true typ) in
+ "(fun v => " ^ id ^ "_of_regval v)", "(fun v => regval_of_" ^ id ^ " v)"
+
+let register_refs_coq registers =
+ let generic_convs =
+ separate_map hardline string [
+ "Definition vector_of_regval {a} (of_regval : register_value -> option a) (rv : register_value) : option (list a) := match rv with";
+ " | Regval_vector (_, _, v) => just_list (List.map of_regval v)";
+ " | _ => None";
+ "end.";
+ "";
+ "Definition regval_of_vector {a} (regval_of : a -> register_value) (size : Z) (is_inc : bool) (xs : list a) : register_value := Regval_vector (size, is_inc, List.map regval_of xs).";
+ "";
+ "Definition list_of_regval {a} (of_regval : register_value -> option a) (rv : register_value) : option (list a) := match rv with";
+ " | Regval_list v => just_list (List.map of_regval v)";
+ " | _ => None";
+ "end.";
+ "";
+ "Definition regval_of_list {a} (regval_of : a -> register_value) (xs : list a) : register_value := Regval_list (List.map regval_of xs).";
+ "";
+ "Definition option_of_regval {a} (of_regval : register_value -> option a) (rv : register_value) : option (option a) := match rv with";
+ " | Regval_option v => option_map of_regval v";
+ " | _ => None";
+ "end.";
+ "";
+ "Definition regval_of_option {a} (regval_of : a -> register_value) (v : option a) := Regval_option (option_map regval_of v).";
+ "";
+ ""
+ ]
+ in
+ let register_ref (typ, id) =
+ let idd = string (string_of_id id) in
+ (* let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in *)
+ let of_regval, regval_of = regval_convs_coq typ in
+ concat [string "Definition "; idd; string "_ref := {|"; hardline;
+ string " name := \""; idd; string "\";"; hardline;
+ string " read_from := (fun s => s.("; idd; string "));"; hardline;
+ string " write_to := (fun v s => ({[ s with "; idd; string " := v ]}));"; hardline;
+ string " of_regval := "; string of_regval; string ";"; hardline;
+ string " regval_of := "; string regval_of; string " |}."; hardline]
+ in
+ let refs = separate_map hardline register_ref registers in
+ let get_set_reg (_, id) =
+ let idd = string_of_id id in
+ string (" if string_dec reg_name \"" ^ idd ^ "\" then Some (" ^ idd ^ "_ref.(regval_of) (" ^ idd ^ "_ref.(read_from) s)) else"),
+ string (" if string_dec reg_name \"" ^ idd ^ "\" then option_map (fun v => " ^ idd ^ "_ref.(write_to) v s) (" ^ idd ^ "_ref.(of_regval) v) else")
+ in
+ let getters_setters =
+ let getters, setters = List.split (List.map get_set_reg registers) in
+ string "Local Open Scope string." ^^ hardline ^^
+ string "Definition get_regval (reg_name : string) (s : regstate) : option register_value :=" ^^ hardline ^^
+ separate hardline getters ^^ hardline ^^
+ string " None." ^^ hardline ^^ hardline ^^
+ string "Definition set_regval (reg_name : string) (v : register_value) (s : regstate) : option regstate :=" ^^ hardline ^^
+ separate hardline setters ^^ hardline ^^
+ string " None." ^^ hardline ^^ hardline ^^
+ string "Definition register_accessors := (get_regval, set_regval)." ^^ hardline ^^ hardline
+ in
+ separate hardline [generic_convs; refs; getters_setters]
+
let generate_regstate_defs mwords defs =
(* FIXME We currently don't want to generate undefined_type functions
for register state and values. For the Lem backend, this would require
@@ -314,17 +479,16 @@ let generate_regstate_defs mwords defs =
let gen_undef = !Initial_check.opt_undefined_gen in
Initial_check.opt_undefined_gen := false;
let registers = find_registers defs in
- let def_ids = ids_of_defs (Defs defs) in
- let has_def name = IdSet.mem (mk_id name) def_ids in
let regtyps = register_base_types mwords (List.map fst registers) in
let option_typ =
- if has_def "option" then [] else
+ if is_defined defs "option" then [] else
["union option ('a : Type) = {None : unit, Some : 'a}"]
in
- let regval_typ = if has_def "register_value" then [] else generate_regval_typ regtyps in
- let regstate_typ = if has_def "regstate" then [] else generate_regstate registers in
+ let regval_typ = if is_defined defs "register_value" then [] else generate_regval_typ regtyps in
+ let regstate_typ = if is_defined defs "regstate" then [] else generate_regstate registers in
+ let initregstate = if is_defined defs "initial_regstate" then [] else generate_initial_regstate defs in
let defs =
- option_typ @ regval_typ @ regstate_typ
+ option_typ @ regval_typ @ regstate_typ @ initregstate
|> List.map defs_of_string
|> concat_ast
|> Bindings.fold add_regval_conv regtyps
diff --git a/src/type_check.ml b/src/type_check.ml
index b204b30b..268183fe 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -63,6 +63,10 @@ let opt_tc_debug = ref 0
re-writer passes, so it should only be used for debugging. *)
let opt_no_effects = ref false
+(* opt_no_lexp_bounds_check turns of the bounds checking in vector
+ assignments in l-expressions *)
+let opt_no_lexp_bounds_check = ref false
+
let depth = ref 0
let rec indent n = match n with
@@ -385,6 +389,7 @@ module Env : sig
val update_val_spec : id -> typquant * typ -> t -> t
val define_val_spec : id -> t -> t
val get_val_spec : id -> t -> typquant * typ
+ val get_val_spec_orig : id -> t -> typquant * typ
val is_union_constructor : id -> t -> bool
val is_mapping : id -> t -> bool
val add_record : id -> typquant -> (typ * id) list -> t -> t
@@ -398,6 +403,7 @@ module Env : sig
val add_union_id : id -> typquant * typ -> t -> t
val add_flow : id -> (typ -> typ) -> t -> t
val get_flow : id -> t -> typ -> typ
+ val remove_flow : id -> t -> t
val is_register : id -> t -> bool
val get_register : id -> t -> typ
val add_register : id -> typ -> t -> t
@@ -430,7 +436,7 @@ module Env : sig
val add_cast : id -> t -> t
val allow_polymorphic_undefineds : t -> t
val polymorphic_undefineds : t -> bool
- val lookup_id : id -> t -> lvar
+ val lookup_id : ?raw:bool -> id -> t -> lvar
val fresh_kid : ?kid:kid -> t -> kid
val expand_synonyms : t -> typ -> typ
val canonicalize : t -> typ -> typ
@@ -815,6 +821,12 @@ end = struct
let freshen_bind env bind =
List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars)
+ let get_val_spec_orig id env =
+ try
+ Bindings.find id env.top_val_specs
+ with
+ | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id)
+
let get_val_spec id env =
try
let bind = Bindings.find id env.top_val_specs in
@@ -988,10 +1000,12 @@ end = struct
| Not_found -> fun typ -> typ
let add_flow id f env =
- begin
- typ_print (lazy ("Adding flow constraints for " ^ string_of_id id));
- { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow }
- end
+ typ_print (lazy ("Adding flow constraints for " ^ string_of_id id));
+ { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow }
+
+ let remove_flow id env =
+ typ_print (lazy ("Removing flow constraints for " ^ string_of_id id));
+ { env with flow = Bindings.remove id env.flow }
let is_register id env =
Bindings.mem id env.registers
@@ -1030,11 +1044,11 @@ end = struct
let get_locals env = env.locals
- let lookup_id id env =
+ let lookup_id ?raw:(raw=false) id env =
try
let (mut, typ) = Bindings.find id env.locals in
let flow = get_flow id env in
- Local (mut, flow typ)
+ Local (mut, if raw then typ else flow typ)
with
| Not_found ->
begin
@@ -1075,12 +1089,11 @@ end = struct
let add_constraint (NC_aux (nc_aux, l) as constr) env =
wf_constraint env constr;
- begin
- typ_print (lazy ("Adding constraint " ^ string_of_n_constraint constr));
- match nc_aux with
- | NC_true -> env
- | _ -> { env with constraints = constr :: env.constraints }
- end
+ match nc_aux with
+ | NC_true -> env
+ | _ ->
+ typ_print (lazy ("Adding constraint " ^ string_of_n_constraint constr));
+ { env with constraints = constr :: env.constraints }
let get_ret_typ env = env.ret_typ
@@ -1227,6 +1240,12 @@ let destruct_numeric env typ =
Some ([kid], nc_true, nvar kid)
| _, _ -> None
+let bind_numeric l typ env =
+ match destruct_numeric env typ with
+ | Some (kids, nc, nexp) ->
+ nexp, add_existential kids nc env
+ | None -> typ_error l ("Expected " ^ string_of_typ typ ^ " to be numeric")
+
(** Pull an (potentially)-existentially qualified type into the global
typing environment **)
let bind_existential typ env =
@@ -1357,7 +1376,7 @@ let prove_z3' env constr =
| Constraint.Unknown -> typ_debug (lazy "unknown"); false
let prove_z3 env nc =
- typ_print (lazy ("Prove " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc));
+ typ_print (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc));
prove_z3' env (fun var_of -> Constraint.negate (nc_constraint env var_of nc))
let solve env nexp =
@@ -1880,7 +1899,10 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t
match destruct_exist env typ1, unwrap_exist env (Env.canonicalize env typ2) with
| Some (kids, nc, typ1), _ ->
let env = add_existential kids nc env in subtyp l env typ1 typ2
+ (* | None, ([], _, typ2) ->
+ typ_error l (string_of_typ typ1 ^ " < " ^ string_of_typ typ2) *)
| None, (kids, nc, typ2) ->
+ typ_debug (lazy "Subtype check with unification");
let env = add_typ_vars kids env in
let kids' = KidSet.elements (KidSet.diff (KidSet.of_list kids) (typ_frees typ2)) in
let unifiers, existential_kids, existential_nc =
@@ -2062,6 +2084,9 @@ let typ_of_mpexp (MPat_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
let env_of_mpexp (MPat_aux (_, (l, tannot))) = env_of_annot (l, tannot)
+let lexp_typ_of (LEXP_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
+
+let lexp_env_of (LEXP_aux (_, (l, tannot))) = env_of_annot (l, tannot)
(* Flow typing *)
@@ -2246,7 +2271,7 @@ let rec filter_casts env from_typ to_typ casts =
let crule r env exp typ =
incr depth;
- typ_print (lazy ("Check " ^ string_of_exp exp ^ " <= " ^ string_of_typ typ));
+ typ_print (lazy (Util.("Check " |> cyan |> clear) ^ string_of_exp exp ^ " <= " ^ string_of_typ typ));
try
let checked_exp = r env exp typ in
decr depth; checked_exp
@@ -2257,7 +2282,7 @@ let irule r env exp =
incr depth;
try
let inferred_exp = r env exp in
- typ_print (lazy ("Infer " ^ string_of_exp exp ^ " => " ^ string_of_typ (typ_of inferred_exp)));
+ typ_print (lazy (Util.("Infer " |> blue |> clear) ^ string_of_exp exp ^ " => " ^ string_of_typ (typ_of inferred_exp)));
decr depth;
inferred_exp
with
@@ -2430,6 +2455,9 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
| None -> typ_error l "Cannot use return outside a function"
in
annot_exp (E_return checked_exp) typ
+ | E_tuple exps, Typ_tup typs when List.length exps = List.length typs ->
+ let checked_exps = List.map2 (fun exp typ -> crule check_exp env exp typ) exps typs in
+ annot_exp (E_tuple checked_exps) typ
| E_app (f, xs), _ ->
let inferred_exp = infer_funapp l env f xs (Some typ) in
type_coercion env inferred_exp typ
@@ -2646,9 +2674,9 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
(Reporting_basic.loc_to_string l))
else ();
match Env.lookup_id v env with
- | Local (Immutable, _) | Unbound -> annot_pat (P_id v) typ, Env.add_local v (Immutable, typ) env, []
- | Local (Mutable, _) | Register _ ->
- typ_error l ("Cannot shadow mutable local or register in switch statement pattern " ^ string_of_pat pat)
+ | Local _ | Unbound -> annot_pat (P_id v) typ, Env.add_local v (Immutable, typ) env, []
+ | Register _ ->
+ typ_error l ("Cannot shadow register in pattern " ^ string_of_pat pat)
| Enum enum -> subtyp l env enum typ; annot_pat (P_id v) typ, env, []
end
| P_var (pat, typ_pat) ->
@@ -2959,7 +2987,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in
annot_assign tlexp checked_exp, env'
| LEXP_id v when has_typ v env ->
- begin match Env.lookup_id v env with
+ begin match Env.lookup_id ~raw:true v env with
| Local (Mutable, vtyp) | Register vtyp ->
let checked_exp = crule check_exp env exp vtyp in
let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in
@@ -2972,9 +3000,26 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
annot_assign tlexp inferred_exp, env'
and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
+ typ_print (lazy ("Binding mutable " ^ string_of_lexp lexp ^ " to " ^ string_of_typ typ));
let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some (env, typ, eff))) in
let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in
match lexp_aux with
+ | LEXP_cast (typ_annot, v) ->
+ begin match Env.lookup_id ~raw:true v env with
+ | Local (Immutable, _) | Enum _ ->
+ typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
+ | Local (Mutable, vtyp) ->
+ subtyp l env typ typ_annot;
+ subtyp l env typ_annot vtyp;
+ annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env
+ | Register vtyp ->
+ subtyp l env typ typ_annot;
+ subtyp l env typ_annot vtyp;
+ annot_lexp_effect (LEXP_cast (typ_annot, v)) typ (mk_effect [BE_wreg]), env
+ | Unbound ->
+ subtyp l env typ typ_annot;
+ annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env
+ end
| LEXP_deref exp ->
let inferred_exp = infer_exp env exp in
begin match typ_of inferred_exp with
@@ -2983,39 +3028,16 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
| Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _) when string_of_id r = "register" ->
subtyp l env typ vtyp; annot_lexp_effect (LEXP_deref inferred_exp) typ (mk_effect [BE_wreg]), env
| _ ->
- typ_error l (string_of_typ typ ^ " must be a ref or register type in (*" ^ string_of_exp exp ^ ")")
+ typ_error l (string_of_typ typ ^ " must be a ref or register type in " ^ string_of_exp exp ^ ")")
end
| LEXP_id v ->
- begin match Env.lookup_id v env with
+ begin match Env.lookup_id ~raw:true v env with
| Local (Immutable, _) | Enum _ ->
typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
- | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env
+ | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, Env.remove_flow v env
| Register vtyp -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]), env
| Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env
end
- | LEXP_cast (typ_annot, v) ->
- begin
- match Env.lookup_id v env with
- | Local (Immutable, _) | Enum _ ->
- typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
- | Local (Mutable, vtyp) ->
- begin
- subtyp l env typ typ_annot;
- subtyp l env typ_annot vtyp;
- annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env
- end
- | Register vtyp ->
- begin
- subtyp l env typ typ_annot;
- subtyp l env typ_annot vtyp;
- annot_lexp_effect (LEXP_cast (typ_annot, v)) typ (mk_effect [BE_wreg]), env
- end
- | Unbound ->
- begin
- subtyp l env typ typ_annot;
- annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env
- end
- end
| LEXP_tup lexps ->
begin
let typ = Env.expand_synonyms env typ in
@@ -3030,99 +3052,85 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
| Invalid_argument _ -> typ_error l "Tuple l-expression and tuple type have different length"
in
annot_lexp (LEXP_tup tlexps) typ, env
- (* This case is pretty much just for the PSTATE.<N,Z,C,V> := vector pattern which is really common in ASL. *)
- (* Maybe this code can be made not horrible? *)
- | Typ_app (id, _) when Id.compare id (mk_id "vector") == 0 ->
- begin
- match destruct_vector env typ with
- | Some (vec_len, _, _) ->
- let bind_bits_tuple lexp (tlexps, env, llen) =
- match lexp with
- | LEXP_aux (LEXP_id v, _) ->
- begin
- match Env.lookup_id v env with
- | Local (Immutable, _) | Enum _ ->
- typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
- | Unbound ->
- typ_error l "Unbound variable in vector tuple assignment"
- | Local (Mutable, vtyp) | Register vtyp ->
- let llen' = match destruct_vector env vtyp with
- | Some (llen', _, _) -> llen'
- | None -> typ_error l "Variables in vector tuple assignment must be vectors"
- in
- let tlexp, env = bind_lexp env lexp vtyp in
- tlexp :: tlexps, env, nsum llen llen'
- end
- | LEXP_aux (LEXP_field (LEXP_aux (LEXP_id v, _), fid), _) ->
- (* FIXME: will only work for ASL *)
- let rec_id =
- match Env.lookup_id v env with
- | Register (Typ_aux (Typ_id rec_id, _)) -> rec_id
- | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here")
- in
- let typq, _, vtyp, _ = Env.get_accessor rec_id fid env in
- let llen' = match destruct_vector env vtyp with
- | Some (llen', _, _) -> llen'
- | None -> typ_error l "Variables in vector tuple assignment must be vectors"
- in
- let tlexp, env = bind_lexp env lexp vtyp in
- tlexp :: tlexps, env, nsum llen llen'
- | _ -> typ_error l "bit vector assignment must only contain identifiers"
- in
- let tlexps, env, lexp_len = List.fold_right bind_bits_tuple lexps ([], env, nint 0) in
- if prove env (nc_eq vec_len lexp_len)
- then annot_lexp (LEXP_tup tlexps) typ, env
- else typ_error l "Vector and tuple length must be the same in assignment"
- | None -> typ_error l ("Malformed vector type " ^ string_of_typ typ)
+ | _ -> typ_error l ("Cannot bind tuple l-expression against non tuple type " ^ string_of_typ typ)
+ end
+ | _ ->
+ let inferred_lexp = infer_lexp env lexp in
+ subtyp l env typ (lexp_typ_of inferred_lexp);
+ inferred_lexp, env
+
+and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
+ let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some (env, typ, eff))) in
+ let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in
+ match lexp_aux with
+ | LEXP_id v ->
+ begin match Env.lookup_id v env with
+ | Local (Mutable, typ) -> annot_lexp (LEXP_id v) typ
+ (* Probably need to remove flows here *)
+ | Register typ -> annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg])
+ | Local (Immutable, _) | Enum _ ->
+ typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
+ | Unbound ->
+ typ_error l ("Cannot create a new identifier in this l-expression " ^ string_of_lexp lexp)
+ end
+ | LEXP_vector_range (v_lexp, exp1, exp2) ->
+ begin
+ let inferred_v_lexp = infer_lexp env v_lexp in
+ let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in
+ match v_typ_aux with
+ | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)])
+ when Id.compare id (mk_id "vector") = 0 ->
+ let inferred_exp1 = infer_exp env exp1 in
+ let inferred_exp2 = infer_exp env exp2 in
+ let nexp1, env = bind_numeric l (typ_of inferred_exp1) env in
+ let nexp2, env = bind_numeric l (typ_of inferred_exp2) env in
+ begin match ord with
+ | Ord_aux (Ord_inc, _) when !opt_no_lexp_bounds_check || prove env (nc_lteq nexp1 nexp2) ->
+ let len = nexp_simp (nsum (nminus nexp2 nexp1) (nint 1)) in
+ annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (vector_typ len ord elem_typ)
+ | Ord_aux (Ord_dec, _) when !opt_no_lexp_bounds_check || prove env (nc_gteq nexp1 nexp2) ->
+ let len = nexp_simp (nsum (nminus nexp1 nexp2) (nint 1)) in
+ annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (vector_typ len ord elem_typ)
+ | _ -> typ_error l ("Could not infer length of vector slice assignment " ^ string_of_lexp lexp)
end
- | _ -> typ_error l ("Cannot bind tuple l-expression against non tuple or vector type " ^ string_of_typ typ)
+ | _ -> typ_error l "Cannot assign slice of non vector type"
end
- | LEXP_vector_range (LEXP_aux (LEXP_id v, _), exp1, exp2) ->
+ | LEXP_vector (v_lexp, exp) ->
begin
- let is_immutable, is_register, vtyp = match Env.lookup_id v env with
- | Unbound -> typ_error l "Cannot assign to element of unbound vector"
- | Enum _ -> typ_error l "Cannot vector assign to enumeration element"
- | Local (Immutable, vtyp) -> true, false, vtyp
- | Local (Mutable, vtyp) -> false, false, vtyp
- | Register vtyp -> false, true, vtyp
- in
- let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_subrange", [E_aux (E_id v, (l, ())); exp1; exp2]), (l, ()))) in
- let inferred_exp1, inferred_exp2 = match access with
- | E_aux (E_app (_, [_; inferred_exp1; inferred_exp2]), _) -> inferred_exp1, inferred_exp2
- | _ -> assert false
- in
- match typ_of access with
- | _ when not is_immutable && is_register ->
- subtyp l env typ (typ_of access);
- annot_lexp (LEXP_vector_range (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp1, inferred_exp2)) typ, env
- | _ when not is_immutable ->
- subtyp l env typ (typ_of access);
- annot_lexp (LEXP_vector_range (annot_lexp (LEXP_id v) vtyp, inferred_exp1, inferred_exp2)) typ, env
- | _ -> typ_error l ("Bad vector assignment: " ^ string_of_lexp lexp)
+ let inferred_v_lexp = infer_lexp env v_lexp in
+ let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in
+ match v_typ_aux with
+ | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)])
+ when Id.compare id (mk_id "vector") = 0 ->
+ let inferred_exp = infer_exp env exp in
+ let nexp, env = bind_numeric l (typ_of inferred_exp) env in
+ if !opt_no_lexp_bounds_check || prove env (nc_and (nc_lteq (nint 0) nexp) (nc_lteq nexp (nexp_simp (nminus len (nint 1))))) then
+ annot_lexp (LEXP_vector (inferred_v_lexp, inferred_exp)) elem_typ
+ else
+ typ_error l ("Vector assignment not provably in bounds " ^ string_of_lexp lexp)
+ | _ -> typ_error l "Cannot assign vector element of non vector type"
end
- (* Not sure about this case... can the left lexp be anything other than an identifier? *)
- | LEXP_vector (LEXP_aux (LEXP_id v, _), exp) ->
+ | LEXP_vector_concat [] -> typ_error l "Cannot have empty vector concatenation l-expression"
+ | LEXP_vector_concat (v_lexp :: v_lexps) ->
begin
- let is_immutable, is_register, vtyp = match Env.lookup_id v env with
- | Unbound -> typ_error l "Cannot assign to element of unbound vector"
- | Enum _ -> typ_error l "Cannot vector assign to enumeration element"
- | Local (Immutable, vtyp) -> true, false, vtyp
- | Local (Mutable, vtyp) -> false, false, vtyp
- | Register vtyp -> false, true, vtyp
- in
- let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in
- let inferred_exp = match access with
- | E_aux (E_app (_, [_; inferred_exp]), _) -> inferred_exp
- | _ -> assert false
+ let sum_lengths first_ord first_elem_typ acc (Typ_aux (v_typ_aux, _) as v_typ) =
+ match v_typ_aux with
+ | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)])
+ when Id.compare id (mk_id "vector") = 0 && ord_identical ord first_ord ->
+ typ_equality l env elem_typ first_elem_typ;
+ nsum acc len
+ | _ -> typ_error l "Vector concatentation l-expression must only contain vector types of the same order"
in
- match typ_of access with
- | _ when not is_immutable && is_register ->
- subtyp l env typ (typ_of access);
- annot_lexp (LEXP_vector (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp)) typ, env
- | _ when not is_immutable ->
- subtyp l env typ (typ_of access);
- annot_lexp (LEXP_vector (annot_lexp (LEXP_id v) vtyp, inferred_exp)) typ, env
- | _ -> typ_error l ("Bad vector assignment: " ^ string_of_lexp lexp)
+ let inferred_v_lexp = infer_lexp env v_lexp in
+ let inferred_v_lexps = List.map (infer_lexp env) v_lexps in
+ let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in
+ let v_typs = List.map (fun lexp -> Env.expand_synonyms env (lexp_typ_of lexp)) inferred_v_lexps in
+ match v_typ_aux with
+ | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)])
+ when Id.compare id (mk_id "vector") = 0 ->
+ let len = List.fold_left (sum_lengths ord elem_typ) len v_typs in
+ annot_lexp (LEXP_vector_concat (inferred_v_lexp :: inferred_v_lexps)) (vector_typ (nexp_simp len) ord elem_typ)
+ | _ -> typ_error l ("Vector concatentation l-expression must only contain vector types, found " ^ string_of_typ v_typ)
end
| LEXP_field (LEXP_aux (LEXP_id v, _), fid) ->
(* FIXME: will only work for ASL *)
@@ -3132,7 +3140,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
| _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here")
in
let typq, _, ret_typ, _ = Env.get_accessor rec_id fid env in
- annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ (mk_effect [BE_wreg]), env
+ annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ (mk_effect [BE_wreg])
| _ -> typ_error l ("Unhandled l-expression " ^ string_of_lexp lexp)
and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
@@ -3229,7 +3237,8 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
| E_app (f, xs) -> infer_funapp l env f xs None
| E_loop (loop_type, cond, body) ->
let checked_cond = crule check_exp env cond bool_typ in
- let checked_body = crule check_exp env body unit_typ in
+ let flows, constrs = infer_flow env checked_cond in
+ let checked_body = crule check_exp (add_flows true flows env) body unit_typ in
annot_exp (E_loop (loop_type, checked_cond, checked_body)) unit_typ
| E_for (v, f, t, step, ord, body) ->
begin
@@ -4049,6 +4058,9 @@ and propagate_lexp_effect_aux = function
let p_exp2 = propagate_exp_effect exp2 in
LEXP_vector_range (p_lexp, p_exp1, p_exp2),
union_effects (collect_effects [p_exp1; p_exp2]) (effect_of_lexp p_lexp)
+ | LEXP_vector_concat lexps ->
+ let p_lexps = List.map propagate_lexp_effect lexps in
+ LEXP_vector_concat p_lexps, collect_effects_lexp p_lexps
| LEXP_field (lexp, id) ->
let p_lexp = propagate_lexp_effect lexp in
LEXP_field (p_lexp, id),effect_of_lexp p_lexp
diff --git a/src/type_check.mli b/src/type_check.mli
index 39594b7d..7251f50c 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -63,6 +63,10 @@ val opt_tc_debug : int ref
re-writer passes, so it should only be used for debugging. *)
val opt_no_effects : bool ref
+(** [opt_no_lexp_bounds_check] turns of the bounds checking in vector
+ assignments in l-expressions. *)
+val opt_no_lexp_bounds_check : bool ref
+
(** {2 Type errors} *)
type type_error =
@@ -88,9 +92,14 @@ module Env : sig
(** Note: Most get_ functions assume the identifiers exist, and throw
type errors if it doesn't. *)
- (** get the quantifier and type for a function identifier. *)
+ (** Get the quantifier and type for a function identifier, freshening
+ type variables. *)
val get_val_spec : id -> t -> typquant * typ
+ (** Like get_val_spec, except that the original type variables are used.
+ Useful when processing the body of the function. *)
+ val get_val_spec_orig : id -> t -> typquant * typ
+
val update_val_spec : id -> typquant * typ -> t -> t
val get_register : id -> t -> typ
@@ -143,8 +152,9 @@ module Env : sig
(** Lookup id searchs for a specified id in the environment, and
returns it's type and what kind of identifier it is, using the
lvar type. Returns Unbound if the identifier is unbound, and
- won't throw any exceptions. *)
- val lookup_id : id -> t -> lvar
+ won't throw any exceptions. If the raw option is true, then look
+ up the type without any flow typing modifiers. *)
+ val lookup_id : ?raw:bool -> id -> t -> lvar
val is_union_constructor : id -> t -> bool
@@ -300,6 +310,8 @@ val destruct_exist : Env.t -> typ -> (kid list * n_constraint * typ) option
val destruct_range : Env.t -> typ -> (kid list * n_constraint * nexp * nexp) option
+val destruct_numeric : Env.t -> typ -> (kid list * n_constraint * nexp) option
+
val destruct_vector : Env.t -> typ -> (nexp * order * typ) option
type uvar =
@@ -312,6 +324,9 @@ val string_of_uvar : uvar -> string
val subst_unifiers : uvar KBindings.t -> typ -> typ
+val typ_subst_nexp : kid -> nexp_aux -> typ -> typ
+val typ_subst_typ : kid -> typ_aux -> typ -> typ
+val typ_subst_order : kid -> order_aux -> typ -> typ
val typ_subst_kid : kid -> kid -> typ -> typ
val unify : l -> Env.t -> typ -> typ -> uvar KBindings.t * kid list * n_constraint option
diff --git a/src/value.ml b/src/value.ml
index 1365b835..858a17d9 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -194,6 +194,9 @@ let value_string_drop = function
let value_string_length = function
| [v] -> V_int (coerce_string v |> Sail_lib.string_length)
| _ -> failwith "value string_length"
+let value_eq_bit = function
+ | [v1; v2] -> V_bool (Sail_lib.eq_bit (coerce_bit v1, coerce_bit v2))
+ | _ -> failwith "value eq_bit"
let value_length = function
| [v] -> V_int (coerce_gv v |> List.length |> Big_int.of_int)
@@ -432,6 +435,7 @@ let primops =
("string_startswith", value_string_startswith);
("string_drop", value_string_drop);
("string_length", value_string_length);
+ ("eq_bit", value_eq_bit);
("eq_anything", value_eq_anything);
("length", value_length);
("subrange", value_subrange);
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 21:01:11 +0000