From b02dc674d6ad57c6a411d8591191aa66dcec49a6 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 5 Jun 2024 19:26:21 +0100 Subject: [PATCH] Coq: switch to suppressing regfp types in the library Avoids suppressing alternative definitions, e.g. in the current RISC-V spec --- lib/regfp.sail | 9 + src/sail_coq_backend/pretty_print_coq.ml | 247 +++++++++-------------- 2 files changed, 108 insertions(+), 148 deletions(-) diff --git a/lib/regfp.sail b/lib/regfp.sail index f1d9be4cd..2acc284f5 100644 --- a/lib/regfp.sail +++ b/lib/regfp.sail @@ -92,12 +92,14 @@ union niafp = { type niafps = list(niafp) /* only for MIPS */ +$option --coq-extern-type diafp union diafp = { DIAFP_none : unit, DIAFP_concrete : bits(64), DIAFP_reg : regfp } +$option --coq-extern-type read_kind enum read_kind = { Read_plain, Read_reserve, @@ -114,6 +116,7 @@ enum read_kind = { Read_X86_locked } +$option --coq-extern-type write_kind enum write_kind = { Write_plain, Write_conditional, @@ -128,6 +131,7 @@ enum write_kind = { Write_X86_locked } +$option --coq-extern-type barrier_kind $ifdef ARM_SPEC enum barrier_kind = { Barrier_DMB_SY, @@ -157,6 +161,7 @@ enum barrier_kind = { Barrier_ISB } $else +$option --coq-extern-type a64_barrier_domain enum a64_barrier_domain = { A64_FullShare, A64_InnerShare, @@ -164,6 +169,7 @@ enum a64_barrier_domain = { A64_NonShare } +$option --coq-extern-type a64_barrier_type enum a64_barrier_type = { A64_barrier_all, A64_barrier_LD, @@ -194,6 +200,7 @@ union barrier_kind = { } $endif +$option --coq-extern-type trans_kind enum trans_kind = { Transaction_start, Transaction_commit, @@ -201,6 +208,7 @@ enum trans_kind = { } /* cache maintenance instructions */ +$option --coq-extern-type cache_op_kind enum cache_op_kind = { /* AArch64 DC */ Cache_op_D_IVAC, Cache_op_D_ISW, Cache_op_D_CSW, Cache_op_D_CISW, @@ -210,6 +218,7 @@ enum cache_op_kind = { } +$option --coq-extern-type instruction_kind union instruction_kind = { IK_barrier : barrier_kind, IK_mem_read : read_kind, diff --git a/src/sail_coq_backend/pretty_print_coq.ml b/src/sail_coq_backend/pretty_print_coq.ml index 48ddc2e18..0ec47ae94 100644 --- a/src/sail_coq_backend/pretty_print_coq.ml +++ b/src/sail_coq_backend/pretty_print_coq.ml @@ -2538,16 +2538,6 @@ let doc_typdef types_mod avoid_target_names generic_eq_types enum_number_defs (T ^^ inhabited_pp ^^ twice hardline | TD_variant (id, typq, ar, _) -> ( match id with - | Id_aux (Id "read_kind", _) -> empty - | Id_aux (Id "write_kind", _) -> empty - | Id_aux (Id "a64_barrier_domain", _) -> empty - | Id_aux (Id "a64_barrier_type", _) -> 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 id_pp = doc_id_type types_mod avoid_target_names None id in @@ -2617,113 +2607,98 @@ let doc_typdef types_mod avoid_target_names generic_eq_types enum_number_defs (T in typ_pp ^^ dot ^^ hardline ^^ reset_implicits_pp ^^ hardline ^^ eq_pp ^^ hardline ^^ inhabited_pp ^^ hardline ) - | TD_enum (id, enums, _) -> ( - match id with - | Id_aux (Id "read_kind", _) -> empty - | Id_aux (Id "write_kind", _) -> empty - | Id_aux (Id "a64_barrier_domain", _) -> empty - | Id_aux (Id "a64_barrier_type", _) -> empty - | Id_aux (Id "barrier_kind", _) -> empty - | Id_aux (Id "trans_kind", _) -> empty - | Id_aux (Id "instruction_kind", _) -> empty - | Id_aux (Id "cache_op_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 bare_ctxt) enums) in - let id_pp = doc_id_type types_mod avoid_target_names None id in - let typ_pp = - (doc_op coloneq) (concat [string "Inductive"; space; id_pp]) (ifflat empty (pipe ^^ space) ^^ enums_doc) - in - (* If we have conversion functions to Z, put them here and - derive a decision procedure that's efficient even for - large enums. *) - let eq1_pp = - let fallback = string "Scheme Equality for" ^^ space ^^ id_pp ^^ dot in - match (Bindings.find_opt id (fst enum_number_defs), Bindings.find_opt id (snd enum_number_defs)) with - | Some (num_of_id, num_of_pp), Some (of_num_id, of_num_pp) -> - let num_of_id_pp = doc_id bare_ctxt num_of_id in - let of_num_id_pp = doc_id bare_ctxt of_num_id in - let lemma1 = - separate hardline - [ - string "Lemma " ^^ id_pp ^^ string "_num_of_roundtrip " - ^^ parens (string "x : " ^^ id_pp) - ^^ string " : " ^^ of_num_id_pp ^^ space - ^^ parens (num_of_id_pp ^^ string " x") - ^^ string " = x."; - string "destruct x; reflexivity."; - string "Qed."; - ] - in - let lemma2 = - separate hardline - [ - string "Lemma " ^^ num_of_id_pp ^^ string "_injective " - ^^ parens (string "x y : " ^^ id_pp) - ^^ string " : " ^^ num_of_id_pp ^^ string " x = " ^^ num_of_id_pp ^^ string " y -> x = y."; - string "intro."; - string "rewrite <- (" ^^ id_pp ^^ string "_num_of_roundtrip x)."; - string "rewrite <- (" ^^ id_pp ^^ string "_num_of_roundtrip y)."; - string "congruence."; - string "Qed."; - ] - in - let eq_pp = - separate hardline - [ - string "Definition " ^^ id_pp ^^ string "_eq_dec (x y : " ^^ id_pp - ^^ string ") : {x = y} + {x <> y}."; - string "refine (match Z.eq_dec (" ^^ num_of_id_pp ^^ string " x) (" ^^ num_of_id_pp - ^^ string " y) with"; - string "| left e => left (" ^^ num_of_id_pp ^^ string "_injective x y e)"; - string "| right ne => right _"; - string "end)."; - string "congruence."; - string "Defined."; - ] - in - num_of_pp ^^ of_num_pp ^^ separate hardline [lemma1; lemma2; eq_pp] - | Some (_, pp), None | None, Some (_, pp) -> pp ^^ fallback - | None, None -> fallback - in - let eq2_pp = + | TD_enum (id, enums, _) -> + let enums_doc = group (separate_map (break 1 ^^ pipe ^^ space) (doc_id_ctor bare_ctxt) enums) in + let id_pp = doc_id_type types_mod avoid_target_names None id in + let typ_pp = + (doc_op coloneq) (concat [string "Inductive"; space; id_pp]) (ifflat empty (pipe ^^ space) ^^ enums_doc) + in + (* If we have conversion functions to Z, put them here and + derive a decision procedure that's efficient even for + large enums. *) + let eq1_pp = + let fallback = string "Scheme Equality for" ^^ space ^^ id_pp ^^ dot in + match (Bindings.find_opt id (fst enum_number_defs), Bindings.find_opt id (snd enum_number_defs)) with + | Some (num_of_id, num_of_pp), Some (of_num_id, of_num_pp) -> + let num_of_id_pp = doc_id bare_ctxt num_of_id in + let of_num_id_pp = doc_id bare_ctxt of_num_id in + let lemma1 = + separate hardline + [ + string "Lemma " ^^ id_pp ^^ string "_num_of_roundtrip " + ^^ parens (string "x : " ^^ id_pp) + ^^ string " : " ^^ of_num_id_pp ^^ space + ^^ parens (num_of_id_pp ^^ string " x") + ^^ string " = x."; + string "destruct x; reflexivity."; + string "Qed."; + ] + in + let lemma2 = + separate hardline + [ + string "Lemma " ^^ num_of_id_pp ^^ string "_injective " + ^^ parens (string "x y : " ^^ id_pp) + ^^ string " : " ^^ num_of_id_pp ^^ string " x = " ^^ num_of_id_pp ^^ string " y -> x = y."; + string "intro."; + string "rewrite <- (" ^^ id_pp ^^ string "_num_of_roundtrip x)."; + string "rewrite <- (" ^^ id_pp ^^ string "_num_of_roundtrip y)."; + string "congruence."; + string "Qed."; + ] + in + let eq_pp = + separate hardline + [ + string "Definition " ^^ id_pp ^^ string "_eq_dec (x y : " ^^ id_pp ^^ string ") : {x = y} + {x <> y}."; + string "refine (match Z.eq_dec (" ^^ num_of_id_pp ^^ string " x) (" ^^ num_of_id_pp + ^^ string " y) with"; + string "| left e => left (" ^^ num_of_id_pp ^^ string "_injective x y e)"; + string "| right ne => right _"; + string "end)."; + string "congruence."; + string "Defined."; + ] + in + num_of_pp ^^ of_num_pp ^^ separate hardline [lemma1; lemma2; eq_pp] + | Some (_, pp), None | None, Some (_, pp) -> pp ^^ fallback + | None, None -> fallback + in + let eq2_pp = + string "#[export]" ^^ hardline + ^^ group + (nest 2 + (flow (break 1) + [ + string "Instance Decidable_eq_" ^^ id_pp ^^ space ^^ colon; + string "forall (x y : " ^^ id_pp ^^ string "), Decidable (x = y) :="; + string "Decidable_eq_from_dec " ^^ id_pp ^^ string "_eq_dec."; + ] + ) + ) + in + let inhabited_pp = + match enums with + | example_id :: _ -> string "#[export]" ^^ hardline ^^ group (nest 2 (flow (break 1) [ - string "Instance Decidable_eq_" ^^ id_pp ^^ space ^^ colon; - string "forall (x y : " ^^ id_pp ^^ string "), Decidable (x = y) :="; - string "Decidable_eq_from_dec " ^^ id_pp ^^ string "_eq_dec."; + string "Instance dummy_" ^^ id_pp ^^ space ^^ colon; + string "Inhabited " ^^ id_pp ^^ string " := {"; ] + ^/^ string "inhabitant :=" + ^^ nest 2 (break 1 ^^ doc_id_ctor bare_ctxt example_id) ) + ^/^ string "}." ) - in - let inhabited_pp = - match enums with - | example_id :: _ -> - string "#[export]" ^^ hardline - ^^ group - (nest 2 - (flow (break 1) - [ - string "Instance dummy_" ^^ id_pp ^^ space ^^ colon; - string "Inhabited " ^^ id_pp ^^ string " := {"; - ] - ^/^ string "inhabitant :=" - ^^ nest 2 (break 1 ^^ doc_id_ctor bare_ctxt example_id) - ) - ^/^ string "}." - ) - ^^ hardline - | [] -> - Reporting.print_err l "Warning" ("Empty type: " ^ string_of_id id); - empty - in - typ_pp ^^ dot ^^ hardline ^^ eq1_pp ^^ hardline ^^ eq2_pp ^^ hardline ^^ inhabited_pp ^^ twice hardline - ) + ^^ hardline + | [] -> + Reporting.print_err l "Warning" ("Empty type: " ^ string_of_id id); + empty + in + typ_pp ^^ dot ^^ hardline ^^ eq1_pp ^^ hardline ^^ eq2_pp ^^ hardline ^^ inhabited_pp ^^ twice hardline let args_of_typ l env typs = let arg i typ = @@ -3472,47 +3447,23 @@ let doc_isla_typ types_mod avoid_target_names (TD_aux (td, _)) = empty; empty; ] - | TD_enum (id, enums, _) -> ( - match id with - | Id_aux (Id "read_kind", _) -> empty - | Id_aux (Id "write_kind", _) -> empty - | Id_aux (Id "a64_barrier_domain", _) -> empty - | Id_aux (Id "a64_barrier_type", _) -> empty - | Id_aux (Id "barrier_kind", _) -> empty - | Id_aux (Id "trans_kind", _) -> empty - | Id_aux (Id "instruction_kind", _) -> empty - | Id_aux (Id "cache_op_kind", _) -> empty - | Id_aux (Id "regfp", _) -> empty - | Id_aux (Id "niafp", _) -> empty - | Id_aux (Id "diafp", _) -> empty - | _ -> - hang 2 - (string "#[export] Instance get_isla_" ^^ type_id_pp id ^^ string " : IslaEnum " ^^ type_id_pp id - ^^ string " :=" ^^ hardline - ^^ surround_separate_map 2 1 (brackets empty) lbracket - (string ";" ^^ break 1) - rbracket - (fun id -> - let idpp = doc_id_ctor bare_ctxt id in - parens (dquotes idpp ^^ string ", " ^^ idpp) - ) - enums - ^^ dot - ) - ^^ hardline ^^ hardline - ) + | TD_enum (id, enums, _) -> + hang 2 + (string "#[export] Instance get_isla_" ^^ type_id_pp id ^^ string " : IslaEnum " ^^ type_id_pp id + ^^ string " :=" ^^ hardline + ^^ surround_separate_map 2 1 (brackets empty) lbracket + (string ";" ^^ break 1) + rbracket + (fun id -> + let idpp = doc_id_ctor bare_ctxt id in + parens (dquotes idpp ^^ string ", " ^^ idpp) + ) + enums + ^^ dot + ) + ^^ hardline ^^ hardline | TD_variant (id, typq, ar, _) -> ( match id with - | Id_aux (Id "read_kind", _) -> empty - | Id_aux (Id "write_kind", _) -> empty - | Id_aux (Id "a64_barrier_domain", _) -> empty - | Id_aux (Id "a64_barrier_type", _) -> 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 | Id_aux (Id "register_value", _) -> empty | _ ->