Skip to content

Monadic translator lib fixes #1346

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

Closed
talsewell wants to merge 2 commits into from
Closed

Monadic translator lib fixes #1346

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
21255a1
monadic translator: less dependent on const naming
talsewell Mar 3, 2026
b5d7bde
monadic translator: less use of parsing in libs
talsewell Mar 3, 2026
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
49 changes: 27 additions & 22 deletions translator/monadic/ml_monadStoreLib.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,32 +50,38 @@ local
end
open Parse
(* Information about the subscript exceptions *)
val Conv_Subscript = EVAL ``sub_exn_v`` |> concl |> rand
val Conv_Subscript = EVAL semanticPrimitivesSyntax.sub_exn_v |> concl |> rand
(* val Stamp_Subscript = Conv_Subscript |> rator |> rand |> rand *)
in

(* Sidestep setting up "syntax" libraries, fetch const from def. *)
fun left_const thm = concl thm
|> strip_conj |> hd |> strip_forall |> snd |> lhs
|> strip_comb |> fst

(* Constants *)
val hprop_ty = “:hprop”
val v_ty = “:v”
val ffi_state_ty = “:'ffi semanticPrimitives$state”
val ffi_ffi_proj_ty = “:'ffi ffi_proj”
val lookup_ret_ty = “:num # stamp”
val hprop_ty = cfHeapsBaseSyntax.hprop_ty
val v_ty = semanticPrimitivesSyntax.v_ty
val ffi_var = mk_vartype "'ffi"
val ffi_state_ty = semanticPrimitivesSyntax.state_ty |> type_subst [alpha |-> ffi_var]
val ffi_ffi_proj_ty = cfHeapsBaseSyntax.mk_ffi_proj_ty ffi_var
val lookup_ret_ty = pairSyntax.mk_prod(numSyntax.num, semanticPrimitivesSyntax.stamp_ty)

val TRUE = boolSyntax.T
val emp_const = “emp : hprop”
val APPEND_const = “APPEND : α list -> α list -> α list”
val CONS_const = “CONS : α -> α list -> α list”
val REF_const = “REF”
val RARRAY_const = “RARRAY”
val ARRAY_const = “ARRAY”
val SOME_const = “SOME”
val one_const = “1 : num”
val cond_const = “set_sep$cond”
val emp_const = cfHeapsBaseSyntax.emp_tm
val APPEND_const = listSyntax.append_tm
val CONS_const = listSyntax.cons_tm
val REF_const = cfHeapsBaseTheory.REF_def |> left_const
val RARRAY_const = ml_monad_translatorBaseTheory.RARRAY_def |> left_const
val ARRAY_const = cfHeapsBaseTheory.ARRAY_def |> left_const
val one_const = numSyntax.term_of_int 1
val cond_const = set_sepTheory.cond_def |> left_const
val get_refs_const = “λ(state : 'a semanticPrimitives$state). state.refs”
val opref_expr = “λname. (App Opref [Var (Short name)])”
val empty_v_list = “[] : v list”
val empty_v_store = “[] : v store”
val empty_alpha_list = “[] : α list”
val empty_v_list = listSyntax.mk_list ([], v_ty)
val empty_v_store = listSyntax.mk_list ([],
semanticPrimitivesSyntax.store_v_ty |> type_subst [alpha |-> v_ty])
val empty_alpha_list = listSyntax.mk_list ([], alpha)
val nsLookup_env_short_term = “λ(env : v sem_env) name. nsLookup env.v (Short name)”
val Conv_Subscript = Conv_Subscript
end (* local *)
Expand Down Expand Up @@ -105,7 +111,7 @@ fun mk_VALID_REFS_PRED H =

fun mk_lookup_eq name env type_tm = let
val lookup_tm = ISPECL [name, env] lookup_cons_def |> concl |> dest_eq |> fst
val some_tm = mk_comb (inst [alpha |-> lookup_ret_ty] SOME_const, mk_pair(one_const, type_tm))
val some_tm = optionSyntax.mk_some(mk_pair(one_const, type_tm))
in mk_eq(lookup_tm, some_tm) end

(******* COPY/PASTE from ml_monadProgScript.sml *****************************************)
Expand Down Expand Up @@ -418,8 +424,7 @@ fun create_store_X_hprop refs_manip_list
val get_term = mk_comb (get_f, Term.inst ty_subst state_var) |>
BETA_CONV |> concl |> dest_eq |> snd

val hprop =
list_mk_ucomb(``RARRAY_REL``, [ref_inv, rarray_ref_loc, get_term])
val hprop = mk_RARRAY_REL ref_inv rarray_ref_loc get_term
in
hprop
end
Expand All @@ -441,7 +446,7 @@ fun create_store_X_hprop refs_manip_list
val get_term = mk_comb (get_f, Term.inst ty_subst state_var) |>
BETA_CONV |> concl |> dest_eq |> snd

val hprop = list_mk_ucomb(``ARRAY_REL``, [ref_inv, farray_loc, get_term])
val hprop = mk_ARRAY_REL ref_inv farray_loc get_term
in
hprop
end
Expand Down
3 changes: 3 additions & 0 deletions translator/monadic/ml_monad_translator_interfaceLib.sig
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,9 @@
signature ml_monad_translator_interfaceLib =
sig

(* Sets up monadic syntax, Less invasive than the full version. *)
val minimal_set_up_monadic_translator : unit -> unit

val set_up_monadic_translator : unit -> unit

type term = Term.term
Expand Down
69 changes: 36 additions & 33 deletions translator/monadic/ml_monad_translator_interfaceLib.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,16 +15,29 @@ open preamble ml_monadBaseLib ml_monadStoreLib ml_monad_translatorLib

******************************************************************************)

fun set_up_monadic_translator () = let
(* Sidestep setting up "syntax" libraries, fetch const from def. *)
fun left_const thm = concl thm
|> strip_conj |> hd |> strip_forall |> snd |> lhs
|> strip_comb |> fst

fun minimal_set_up_monadic_translator () = let
(* Add monadic syntax: do x <- f y; ... od *)
val _ = ParseExtras.temp_loose_equality();
val _ = monadsyntax.temp_add_monadsyntax()

(* Parser overloadings *)
val _ = Parse.temp_overload_on("monad_bind",``st_ex_bind``);
val _ = Parse.temp_overload_on("monad_unitbind",``st_ex_ignore_bind``);
val _ = Parse.temp_overload_on("monad_ignore_bind",``st_ex_ignore_bind``);
val _ = Parse.temp_overload_on("return",``st_ex_return``);
open ml_monadBaseTheory
val _ = Parse.temp_overload_on("monad_bind", left_const st_ex_bind_def);
val ign_c = left_const st_ex_ignore_bind_def;
val _ = Parse.temp_overload_on("monad_unitbind", ign_c);
val _ = Parse.temp_overload_on("monad_ignore_bind", ign_c);
val _ = Parse.temp_overload_on("return", left_const st_ex_return_def);
in () end

fun set_up_monadic_translator () = let
(* Take all steps taken by a previous version. *)
val _ = ParseExtras.temp_loose_equality();

val _ = minimal_set_up_monadic_translator();

(* Hide "state" due to semanticPrimitives *)
val _ = hide "state";
Expand All @@ -39,8 +52,7 @@ in () end

******************************************************************************)

fun toUppers(str) = String.implode (map Char.toUpper (String.explode str));
val unit_ty = type_of ``()``;
val unit_ty = type_of (left_const oneTheory.one_DEF);


datatype translator_mode = GLOBAL | LOCAL;
Expand All @@ -56,8 +68,6 @@ datatype translator_mode = GLOBAL | LOCAL;
type state = {
state_access_funs : (string * thm * thm) list ref,
(* (name, get, set) *)
store_invariant_name : string ref,
store_exn_invariant_name : string ref,
exn_type_def : thm ref,
additional_type_theories : string list ref,
hprop_field_names : (term * string) list ref,
Expand All @@ -71,8 +81,6 @@ type state = {
(* Initial internal state *)
val internal_state : state = {
state_access_funs = ref [],
store_invariant_name = ref "STATE_STORE",
store_exn_invariant_name = ref "STATE_EXN",
exn_type_def = ref ml_translatorTheory.UNIT_TYPE_def,
additional_type_theories = ref [],
hprop_field_names = ref [],
Expand Down Expand Up @@ -139,27 +147,27 @@ fun with_state state_type (translator_config : config) =
let val accessors = define_monad_access_funs state_type
in
#state_type internal_state := state_type;
#store_invariant_name internal_state :=
(state_type |> dest_type |> fst |> toUppers);
#state_access_funs internal_state := accessors;
translator_config
end;

(* This hack also used in ml_translatorLib. *)
fun guess_const_def tm = let
val stuff = dest_thy_const tm
in DB.fetch (#Thy stuff) (#Name stuff ^ "_def") end

(*
* Register the exception type and return the type definition
*)
fun register_exception_type exn_type =
let val exn_name = (exn_type |> dest_type |> fst |> toUppers)
val exn_type_def_name = exn_name ^ "_TYPE_def"
in (
(
register_type ``:unit``;
register_type ``:'a # 'b``;
register_type ``:'a list``;
register_type ``:'a option``;
register_exn_type exn_type;
#store_exn_invariant_name internal_state := exn_name;
theorem exn_type_def_name
) end;
guess_const_def (get_type_inv exn_type)
);

(*
* Set the exception type, and get monadic exception functions
Expand Down Expand Up @@ -344,7 +352,7 @@ fun extract_farrays_manip_funs (name, init, get, set, len, sub, upd) =
local

val IMP_STAR_GC = Q.prove(
`(STAR a x) s ∧ (y = GC) ⇒ (STAR a y) s`,
`(STAR a x) s ∧ (y = cfHeapsBase$GC) ⇒ (STAR a y) s`,
fs [set_sepTheory.STAR_def] >>
rw [] >> asm_exists_tac >> fs [] >>
EVAL_TAC >>
Expand All @@ -356,11 +364,9 @@ local
in

fun add_field_access_patterns (hprop_comb, field_name) = let
val store_inv_name = ( !(#store_invariant_name internal_state) )
val state_ty = ( !(#state_type internal_state) )
val state_predicate =
if state_ty = unit_ty then ``UNIT_TYPE``
else Term [QUOTE store_inv_name]
val state_predicate = get_type_inv state_ty
val state_predicate_def = guess_const_def state_predicate
val field = Term [QUOTE field_name]
val st_field = Term [QUOTE "st.", QUOTE field_name]

Expand All @@ -382,7 +388,7 @@ in
impl_tac
>- (
fs [ml_monad_translatorBaseTheory.REFS_PRED_def] >>
fs [fetch "-" (store_inv_name ^ "_def")] >>
fs [state_predicate_def] >>
qabbrev_tac `a = ^hprop_comb ^st_field` >>
qabbrev_tac `b = GC` >>
fs [AC set_sepTheory.STAR_ASSOC set_sepTheory.STAR_COMM] >>
Expand All @@ -397,18 +403,15 @@ in
Cases_on `f ^st_field` >> fs [] >>
EVERY_CASE_TAC >>
rveq >> fs [] >>
fs [fetch "-" (store_inv_name ^ "_def")] >>
fs [state_predicate_def] >>
fs [ml_monadBaseTheory.liftM_def] >>
rw [] >>
rfs[] >>
fs[HPROP_COMB_STAR_COMM, set_sepTheory.STAR_ASSOC] >>
metis_tac[set_sepTheory.STAR_ASSOC]
)
val state_exn_name = ( !(#store_exn_invariant_name internal_state) )
val state_exn_ty = ( !(#exn_type internal_state) )
val state_exn_predicate =
if state_exn_ty = unit_ty then ``UNIT_TYPE``
else Term [QUOTE state_exn_name, QUOTE "_TYPE"]
val state_exn_predicate = get_type_inv state_exn_ty

val access_thm_list = mapfilter
(fn ((_, name), (thm, Thm, _)) => (name^"_"^field_name, thm)
Expand Down Expand Up @@ -464,7 +467,7 @@ fun start_translation (translator_config : config) =
((!(#refs c) ) |> map from_named_tuple_refs)
((!(#resizeable_arrays c) ) |> map from_named_tuple_rarray)
((!(#fixed_arrays c) ) |> map from_named_tuple_farray)
( !(#store_invariant_name s) )
((!(#state_type c) ) |> dest_type |> fst |> (fn s => s^"_STORE_INV"))
( !(#state_type c) )
( !(#exn_type_def s) )
((!(#exn_access_funs c) ) |> map from_named_tuple_exn)
Expand All @@ -485,7 +488,7 @@ fun start_translation (translator_config : config) =
map extract_rarrays_manip_funs)
((!(#fixed_arrays c) ) |> map from_named_tuple_farray |>
map extract_farrays_manip_funs)
( !(#store_invariant_name s) )
((!(#state_type c) ) |> dest_type |> fst |> (fn s => s^"_STORE_INV"))
( !(#state_type c) )
( !(#exn_type_def s) )
((!(#exn_access_funs c) ) |> map from_named_tuple_exn)
Expand Down