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_has_next`

and `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

```
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

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