Stream: General

Topic: Map type, hashmap with sepref

Valentin Springsklee (Nov 30 2022 at 13:59):

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?

Notification Bot (Nov 30 2022 at 14:03):

Valentin Springsklee has marked this topic as resolved.

Notification Bot (Nov 30 2022 at 14:03):

Valentin Springsklee has marked this topic as unresolved.

Mathias Fleury (Nov 30 2022 at 14:11):

in which step does sepref fail?

Mathias Fleury (Nov 30 2022 at 14:12):

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

Mathias Fleury (Nov 30 2022 at 14:13):

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

Mathias Fleury (Nov 30 2022 at 14:22):

hm_it_has_next and hm_it_init seem to exist for the purpose of iterating

Mathias Fleury (Nov 30 2022 at 14:23):

but I don't know if there is a proper setup

Valentin Springsklee (Nov 30 2022 at 14:24):

Hello, thanks for the quick reply! So, we have

sepref_definition tryitmap is " scoremax" :: "((hm.assn (nat_assn) (nat_assn))⇧k →⇩a (nat_assn))" unfolding scoremax_def[abs_def]

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

Mathias Fleury (Nov 30 2022 at 14:32):

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

Valentin Springsklee (Nov 30 2022 at 14:36):

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?

Mathias Fleury (Nov 30 2022 at 14:42):

That indicate that sepref does not know what to do with dom

Mathias Fleury (Nov 30 2022 at 14:45):

I have never tried to iterate over finite maps (in my use case, I can just iterate over all values up to the maximum)

Mathias Fleury (Nov 30 2022 at 14:45):

I would search for all theorems involving hm_it_has_next (find_theorems!) to see if it used anywhere else

Valentin Springsklee (Nov 30 2022 at 14:48):

Thank you! That is a great tip. I have wondered about iterators.

Last updated: Apr 20 2024 at 12:26 UTC