Hello. I am using the imperative refinement framework and sepref. I have a question regarding the use of the map type
'a ⇒ 'b option and the use of hashmaps in imperative HOL code. I defined a monadic function that maps a natural number to each member of a specified set,
definition compute_scores :: "'a set ⇒ 'a Profile_List ⇒ ('a ⇀ nat) nres" . The function is can be refined to imperative HOL with sepref using the hashmap implmentation from the imperative collections framework. I now want to define a separate function that takes a map and returns the maximum of all values. My algorithmic Idea is something like this: Bildschirmfoto_2022-11-30_14-56-50.png
I can't synthesize imperative HOL code using sepref. I think, I cannot use the dom function, neither the Option.the operator. How can I access the values in the map, especially with sepref in mind?
Valentin Springsklee has marked this topic as resolved.
Valentin Springsklee has marked this topic as unresolved.
in which step does sepref fail?
To test if there is some missing precondition or some missing function:
apply sepref_dbg_keep apply sepref_dbg_trans_keep apply sepref_dbg_trans_step_keep apply sepref_dbg_side_unfold
To test if some identification fails:
apply sepref_dbg_preproc apply sepref_dbg_cons_init apply sepref_dbg_id apply sepref_dbg_monadify apply sepref_dbg_opt_init apply sepref_dbg_trans apply sepref_dbg_opt apply sepref_dbg_cons_solve apply sepref_dbg_cons_solve apply sepref_dbg_cons_solve_cp apply sepref_dbg_constraints
hm_it_init seem to exist for the purpose of iterating
but I don't know if there is a proper setup
Hello, thanks for the quick reply! So, we have
is " scoremax" :: "((hm.assn (nat_assn) (nat_assn))⇧k →⇩a (nat_assn))"
Sepref fails in the trans phase.
sepref_dbg_trans_keep promts "Phase Translation steps
*** Wrong number of produced goals" . And after applying
sepref_dbg_trans_step_keep, Phase Apply rule
*** Phase tactic failed is promted. Can it be, that dom and ran
Then you have to look at the first goal (I suggest using
subgoal premises p): If the goal contains a precondition, then the proof of the precondition failed. If it contains a function to synthesize, then some rule is missing
Ok thank you! after applying
subgoal premise p, i get
hn_refine (hn_ctxt (hm.assn nat_assn nat_assn) x_ xi_) (m' x_ xi_) (Γ'' x_ xi_)
(Rh x_ xi_) (RETURN (dom x_)). I have had that error before using the dom function in a command (not assertion). Do you have a general tip how to iterate over any (finite) map?
That indicate that sepref does not know what to do with dom
I have never tried to iterate over finite maps (in my use case, I can just iterate over all values up to the maximum)
I would search for all theorems involving hm_it_has_next (find_theorems!) to see if it used anywhere else
Thank you! That is a great tip. I have wondered about iterators.
Last updated: Dec 07 2023 at 08:19 UTC