GillianPlatform / Gillian

The Gillian Platform main repository
https://GillianPlatform.github.io
BSD 3-Clause "New" or "Revised" License
73 stars 11 forks source link

Rethink ExecMap #280

Closed NatKarmios closed 1 month ago

NatKarmios commented 5 months ago

ExecMap as a data structure is becoming somewhat of a burden.

This should be restructured to

  1. Not be recursive; use a map of IDs to nodes instead
  2. Be more consistent; the Cmd, BranchCmd, FinalCmd variants aren't necessary (at least at the top level of nodes)

An idea of a new structure could be:

(* An id of None means it hasn't been executed yet *)
type 'case 'data exec_map_next =
| Single of id option * 'data
| Branch of ('case * id option * 'data)

(* Should this be mutable? *)
type 'data 'case 'next exec_map_node = {
  data : 'data;
  next : 'next; (* e.g. exec_map_next option, where None means a final command *)
}

type 'node exec_map_entry =
| Node of 'node
| Alias of id

type 'node exec_map = {
  root : 'node;
  map : (id, 'node exec_map_entry) HashMap.t;
}

Given how much polymorphism is being juggled here, I'm thinking this should be a module type instantiated by each lifter.