summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/jib/jib_compile.ml41
-rw-r--r--src/jib/jib_optimize.ml1
-rw-r--r--src/jib/jib_ssa.ml1
-rw-r--r--src/jib/jib_util.ml8
-rw-r--r--src/sail.ml2
-rw-r--r--src/specialize.ml2
-rw-r--r--src/specialize.mli2
-rw-r--r--src/value2.lem20
8 files changed, 34 insertions, 43 deletions
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index d74d3c0b..219e0855 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -422,7 +422,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
let ctx = { ctx with local_env = env } in
match apat_aux, cval with
| AP_id (pid, _), (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env ->
- [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind (string_of_id pid))), CT_bool) case_label],
+ [ijump (F_op (F_field (frag, "kind"), "!=", F_ctor_kind (pid, [], ctyp)), CT_bool) case_label],
[],
ctx
@@ -465,25 +465,25 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
| AP_app (ctor, apat, variant_typ), (frag, ctyp) ->
begin match ctyp with
| CT_variant (_, ctors) ->
- let ctor_c_id = string_of_id ctor in
let ctor_ctyp = Bindings.find ctor (ctor_bindings ctors) in
+ let pat_ctyp = apat_ctyp ctx apat in
(* These should really be the same, something has gone wrong if they are not. *)
if ctyp_equal ctor_ctyp (ctyp_of_typ ctx variant_typ) then
raise (Reporting.err_general l (Printf.sprintf "%s is not the same type as %s" (string_of_ctyp ctor_ctyp) (string_of_ctyp (ctyp_of_typ ctx variant_typ))))
else ();
- let ctor_c_id, ctor_ctyp =
+ let unifiers, ctor_ctyp =
if is_polymorphic ctor_ctyp then
- let unification = List.map ctyp_suprema (ctyp_unify ctor_ctyp (apat_ctyp ctx apat)) in
- (if List.length unification > 0 then
- ctor_c_id ^ "_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification
- else
- ctor_c_id),
- ctyp_suprema (apat_ctyp ctx apat)
+ let unifiers = List.map ctyp_suprema (ctyp_unify ctor_ctyp pat_ctyp) in
+ unifiers, ctyp_suprema (apat_ctyp ctx apat)
else
- ctor_c_id, ctor_ctyp
+ [], ctor_ctyp
in
- let instrs, cleanup, ctx = compile_match ctx apat ((F_field (frag, Util.zencode_string ctor_c_id), ctor_ctyp)) case_label in
- [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind ctor_c_id)), CT_bool) case_label]
+ let ctor_field = match unifiers with
+ | [] -> Util.zencode_string (string_of_id ctor)
+ | _ -> Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
+ in
+ let instrs, cleanup, ctx = compile_match ctx apat ((F_field (frag, ctor_field), ctor_ctyp)) case_label in
+ [ijump (F_op (F_field (frag, "kind"), "!=", F_ctor_kind (ctor, unifiers, pat_ctyp)), CT_bool) case_label]
@ instrs,
cleanup,
ctx
@@ -549,11 +549,10 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
let body_setup, body_call, body_cleanup = compile_aexp ctx body in
let gs = ngensym () in
let case_instrs =
- destructure @ [icomment "end destructuring"]
+ destructure
@ (if not trivial_guard then
guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup
@ [iif (F_unary ("!", F_id gs), CT_bool) (destructure_cleanup @ [igoto case_label]) [] CT_unit]
- @ [icomment "end guard"]
else [])
@ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup
@ [igoto finish_match_label]
@@ -563,15 +562,13 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
else
[iblock case_instrs; ilabel case_label]
in
- [icomment "begin match"]
- @ aval_setup @ [idecl ctyp case_return_id]
+ aval_setup @ [idecl ctyp case_return_id]
@ List.concat (List.map compile_case cases)
@ [imatch_failure ()]
@ [ilabel finish_match_label],
(fun clexp -> icopy l clexp (F_id case_return_id, ctyp)),
[iclear ctyp case_return_id]
@ aval_cleanup
- @ [icomment "end match"]
(* Compile try statement *)
| AE_try (aexp, cases, typ) ->
@@ -1280,8 +1277,8 @@ let rec specialize_variants ctx prior =
function
| I_aux (I_funcall (clexp, extern, id, [cval]), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 ->
(* Work out how each call to a constructor in instantiated and add that to unifications *)
- let unification = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in
- let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification) in
+ let unifiers = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in
+ let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> string_of_ctyp ctyp) unifiers) in
unifications := Bindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications;
(* We need to cast each cval to it's ctyp_suprema in order to put it in the most general constructor *)
@@ -1315,6 +1312,12 @@ let rec specialize_variants ctx prior =
| I_aux (I_funcall (clexp, extern, id, cvals), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 ->
Reporting.unreachable l __POS__ "Multiple argument constructor found"
+ (* We have to be careful this is the only place where an F_ctor_kind can appear before calling specialize variants *)
+ | I_aux (I_jump ((F_op (_, "!=", F_ctor_kind (id, unifiers, pat_ctyp)), CT_bool), _), _) as instr when Id.compare id ctor_id = 0 ->
+ let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> string_of_ctyp ctyp) unifiers) in
+ unifications := Bindings.add mono_id (ctyp_suprema pat_ctyp) !unifications;
+ instr
+
| instr -> instr
in
diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
index e4891970..cda3924a 100644
--- a/src/jib/jib_optimize.ml
+++ b/src/jib/jib_optimize.ml
@@ -161,6 +161,7 @@ let rec frag_subst id subst = function
| F_call (op, frags) -> F_call (op, List.map (frag_subst id subst) frags)
| F_field (frag, field) -> F_field (frag_subst id subst frag, field)
| F_raw str -> F_raw str
+ | F_ctor_kind (ctor, unifiers, ctyp) -> F_ctor_kind (ctor, unifiers, ctyp)
| F_poly frag -> F_poly (frag_subst id subst frag)
let cval_subst id subst (frag, ctyp) = frag_subst id subst frag, ctyp
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index e0ff4849..852f1bbd 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -456,6 +456,7 @@ let rename_variables graph root children =
| F_call (id, fs) -> F_call (id, List.map fold_frag fs)
| F_field (f, field) -> F_field (fold_frag f, field)
| F_raw str -> F_raw str
+ | F_ctor_kind (ctor, unifiers, ctyp) -> F_ctor_kind (ctor, unifiers, ctyp)
| F_poly f -> F_poly (fold_frag f)
in
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 76d7b5d2..0a1afbef 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -165,6 +165,7 @@ let rec frag_rename from_id to_id = function
| F_unary (op, f) -> F_unary (op, frag_rename from_id to_id f)
| F_field (f, field) -> F_field (frag_rename from_id to_id f, field)
| F_raw raw -> F_raw raw
+ | F_ctor_kind (ctor, unifiers, ctyp) -> F_ctor_kind (ctor, unifiers, ctyp)
| F_poly f -> F_poly (frag_rename from_id to_id f)
let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ctyp)
@@ -253,9 +254,8 @@ let string_of_value = function
| V_unit -> "UNIT"
| V_bit Sail2_values.B0 -> "UINT64_C(0)"
| V_bit Sail2_values.B1 -> "UINT64_C(1)"
+ | V_bit Sail2_values.BU -> failwith "Undefined bit found in value"
| V_string str -> "\"" ^ str ^ "\""
- | V_ctor_kind str -> "Kind_" ^ Util.zencode_string str
- | _ -> failwith "Cannot convert value to string"
let string_of_name ?zencode:(zencode=true) =
let ssa_num n = if n < 0 then "" else ("/" ^ string_of_int n) in
@@ -282,6 +282,9 @@ let rec string_of_fragment ?zencode:(zencode=true) = function
| F_unary (op, f) ->
op ^ string_of_fragment' ~zencode:zencode f
| F_raw raw -> raw
+ | F_ctor_kind (ctor, [], _) -> "Kind_" ^ Util.zencode_string (string_of_id ctor)
+ | F_ctor_kind (ctor, unifiers, _) ->
+ "Kind_" ^ Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
| F_poly f -> string_of_fragment ~zencode:zencode f
and string_of_fragment' ?zencode:(zencode=true) f =
match f with
@@ -619,6 +622,7 @@ let rec fragment_deps = function
| F_field (frag, _) | F_unary (_, frag) | F_poly frag -> fragment_deps frag
| F_call (_, frags) -> List.fold_left NameSet.union NameSet.empty (List.map fragment_deps frags)
| F_op (frag1, _, frag2) -> NameSet.union (fragment_deps frag1) (fragment_deps frag2)
+ | F_ctor_kind _ -> NameSet.empty
| F_raw _ -> NameSet.empty
let cval_deps = function (frag, _) -> fragment_deps frag
diff --git a/src/sail.ml b/src/sail.ml
index b016e574..9c3a3d5c 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -273,7 +273,7 @@ let options = Arg.align ([
Arg.Set opt_ddump_tc_ast,
" (debug) dump the typechecked ast to stdout");
( "-ddump_rewrite_ast",
- Arg.String (fun l -> opt_ddump_rewrite_ast := Some (l, 0)),
+ Arg.String (fun l -> opt_ddump_rewrite_ast := Some (l, 0); Specialize.opt_ddump_spec_ast := Some (l, 0)),
"<prefix> (debug) dump the ast after each rewriting step to <prefix>_<i>.lem");
( "-ddump_flow_graphs",
Arg.Set Jib_compile.opt_debug_flow_graphs,
diff --git a/src/specialize.ml b/src/specialize.ml
index 5a7624bc..ca33ee85 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -53,7 +53,7 @@ open Ast_util
open Rewriter
let opt_ddump_spec_ast = ref None
-
+
let is_typ_ord_arg = function
| A_aux (A_typ _, _) -> true
| A_aux (A_order _, _) -> true
diff --git a/src/specialize.mli b/src/specialize.mli
index 28d118ca..0a64112c 100644
--- a/src/specialize.mli
+++ b/src/specialize.mli
@@ -54,6 +54,8 @@ open Ast
open Ast_util
open Type_check
+val opt_ddump_spec_ast : (string * int) option ref
+
type specialization
(** Only specialize Type- and Ord- kinded polymorphism. *)
diff --git a/src/value2.lem b/src/value2.lem
index e8a8262a..caf355b7 100644
--- a/src/value2.lem
+++ b/src/value2.lem
@@ -49,34 +49,14 @@
(*========================================================================*)
open import Pervasives
-open import Assert_extra
-open Map
open import Sail2_values
type vl =
- | V_vector of list vl
- | V_list of list vl
| V_bits of list bitU
| V_bit of bitU
- | V_tuple of list vl
| V_bool of bool
- | V_nondet (* Special nondeterministic boolean *)
| V_unit
| V_int of integer
| V_string of string
- | V_ctor of string * list vl
- | V_ctor_kind of string
- | V_record of list (string * vl)
| V_null (* Used for unitialized values and null pointers in C compilation *)
-
-
-let value_int_op_int op = function
- | [V_int v1; V_int v2] -> V_int (op v1 v2)
- | _ -> V_null
-end
-
-let value_bool_op_int op = function
- | [V_int v1; V_int v2] -> V_bool (op v1 v2)
- | _ -> V_null
-end
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 00:28:14 +0000