Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Reducing the amount of information read from the table file for variant types #379

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Reducing the amount of information read from the table file for variant types #379

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 10 additions & 2 deletions c-refinement/Read_Table.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,13 +61,21 @@ fun read_table (file_name:string) thy =
| decode_sigil _ ((Const (@{const_name Boxed}, _)) $ (Const (@{const_name ReadOnly}, _)) $ _) = ReadOnly
| decode_sigil _ (Const (@{const_name Unboxed}, _)) = Unboxed
| decode_sigil pos t = raise TERM (report pos ^ "bad sigil", [t]);


fun decode_variant_state _ @{term Checked} = Checked
| decode_variant_state _ @{term Unchecked} = Unchecked
| decode_variant_state pos t = raise TERM (report pos ^ "failed to parse variant state:", [t])

fun decode_type (_, Const (@{const_name TCon}, _) $ _ $ _ $ _, cT) =
UAbstract cT
| decode_type (pos, Const (@{const_name TRecord}, _) $ _ $ sigil, cT) =
URecord (cT, decode_sigil pos sigil)
| decode_type (_, Const (@{const_name TSum}, _) $ variants, cT) =
USum (cT, variants)
| decode_type (pos, Const (@{const_name TSum}, _) $ variants, cT) =
USum (cT, variants |> HOLogic.dest_list
|> map (fn x => x |> HOLogic.dest_prod |> snd |> HOLogic.dest_prod |> snd
|> decode_variant_state pos
))
| decode_type (_, Const (@{const_name TProduct}, _) $ _ $ _, cT) =
UProduct cT
| decode_type (pos, t, _) =
Expand Down
20 changes: 9 additions & 11 deletions c-refinement/Specialised_Lemma_USum.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,16 +21,14 @@ begin

ML \<open>

fun bool_of_variant_state @{term Checked} = true
| bool_of_variant_state @{term Unchecked} = false
| bool_of_variant_state x = raise ERROR ("bool_of_variant_state: not a variant_state: " ^ @{make_string} x)
fun bool_of_variant_state Checked = true
| bool_of_variant_state Unchecked = false

fun variant_state_of_bool true = @{term Checked}
| variant_state_of_bool false = @{term Unchecked}

fun get_checkeds_of_usum_uval ctxt uval =
usum_list_of_types ctxt uval |>
map (fn x => x |> HOLogic.dest_prod |> snd |> HOLogic.dest_prod |> snd |> bool_of_variant_state)
fun get_checkeds_of_usum_uval uval =
usum_list_of_checked uval |> map bool_of_variant_state

\<close>

Expand All @@ -56,7 +54,7 @@ fun (uval1 can_be_casted_to uval2) ctxt heap_info =
filter (fn (_,(a,b)) => a <> b)
in
if (field_names1 = field_names2) andalso (field_types1 = field_types2)
then case check_diff (get_checkeds_of_usum_uval ctxt uval1) (get_checkeds_of_usum_uval ctxt uval2) of
then case check_diff (get_checkeds_of_usum_uval uval1) (get_checkeds_of_usum_uval uval2) of
(* Only if going from unchecked to checked *)
[(ix,(false,true))] => SOME ix
(* If multiple differences, or no differences, we don't need to worry about case *)
Expand Down Expand Up @@ -103,8 +101,8 @@ ML\<open> fun mk_case_prop from_uval to_uval variant_ctor_num file_nm ctxt =
val nth_field_tag_name = nth_field_ml_tag_name |> Utils.encode_isa_string;
val get_tag_names = fn uval => heap_info_uval_to_field_names heap uval |> tl |> map (unsuffix "_C");
val from_tag_nms = get_tag_names from_uval;
val from_tag_checks = get_checkeds_of_usum_uval ctxt from_uval
val to_tag_checks = get_checkeds_of_usum_uval ctxt to_uval
val from_tag_checks = get_checkeds_of_usum_uval from_uval
val to_tag_checks = get_checkeds_of_usum_uval to_uval

val alternative_tys = map (fn n => Free ("alt_ty" ^ string_of_int n, @{typ "Cogent.type"}))
(1 upto length from_tag_nms)
Expand Down Expand Up @@ -171,7 +169,7 @@ local

fun mk_case_lem_name (from:uval) field_num ctxt =
let
val cs = get_checkeds_of_usum_uval ctxt from
val cs = get_checkeds_of_usum_uval from
val cs_str = cs |> map (fn b => if b then "C" else "U") |> String.concat
in
"corres_case_" ^ get_uval_name from ^ "_" ^ Int.toString field_num ^ "th_field_" ^ cs_str
Expand Down Expand Up @@ -221,7 +219,7 @@ fun mk_specialised_esac_lemma file_nm ctxt from_usum =
val _ = tracing (" mk_specialised_esac_lemma for " ^ from_C_nm)
val thy = Proof_Context.theory_of ctxt;
val is_usum = get_usums [from_usum] |> null |> not;
val with_checks = map_index I (get_checkeds_of_usum_uval ctxt from_usum)
val with_checks = map_index I (get_checkeds_of_usum_uval from_usum)
val uncheckeds = List.filter (fn (_,x) => not x) with_checks
in
case uncheckeds of
Expand Down
15 changes: 9 additions & 6 deletions c-refinement/Specialised_Lemma_Utils.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -177,8 +177,11 @@ declare [[ cheat_specialised_lemmas = false ]]

ML\<open> (* type definition on the ML-level.*)
datatype sigil = ReadOnly | Writable | Unboxed

datatype variant_state = Checked | Unchecked

datatype uval = UProduct of string
| USum of string * term (* term contains argument to TSum (excluding TSum itself) *)
| USum of string * variant_state list (* for each constructor, whether it is checked or not *)
| URecord of string * sigil
| UAbstract of string;
;
Expand All @@ -193,7 +196,7 @@ fun unify_sigils (URecord (ty_name,_)) = URecord (ty_name,Writable)
\<close>

ML\<open> (* unify_usum_tys *)
fun unify_usum_tys (USum (ty_name,_)) = USum (ty_name, Term.dummy)
fun unify_usum_tys (USum (ty_name,_)) = USum (ty_name, [])
| unify_usum_tys uval = uval
\<close>

Expand Down Expand Up @@ -234,13 +237,13 @@ ML\<open> val get_uval_readonly_records =
filter (fn uval => case uval of (URecord (_, ReadOnly)) => true | _ => false);
\<close>

ML\<open> fun usum_list_of_types _ uval = case uval of
USum (_, variants) => HOLogic.dest_list variants
| _ => error ("usum_list_of_types: not USum")
ML\<open> fun usum_list_of_checked uval = case uval of
USum (_, checked) => checked
| _ => error ("usum_list_of_checked: not USum")
\<close>

ML\<open> fun is_UAbstract (UAbstract _) = true
| is_UAbstract _ = false;
| is_UAbstract _ = false;
\<close>

ML\<open> fun get_ty_nm_C uval = uval |> get_uval_name |> (fn nm => nm ^ "_C"); \<close>
Expand Down