Skip to content

Commit

Permalink
Clarify counter_agent_info fetched from signatures with record and names
Browse files Browse the repository at this point in the history
  • Loading branch information
antoinepouille committed Nov 30, 2023
1 parent fc70bf0 commit 06ddb9d
Show file tree
Hide file tree
Showing 7 changed files with 125 additions and 101 deletions.
76 changes: 47 additions & 29 deletions core/grammar/counters_compiler.ml
Original file line number Diff line number Diff line change
Expand Up @@ -428,8 +428,15 @@ let compile ~warning ~debug_mode compil =

let make_counter_agent sigs (first, (dst, ra_erased)) (last, equal) i j pos
created =
let ra_type, arity, incr_b, incr_a = Signature.incr_agent sigs in
let ra_ports = Array.make arity ((LKappa.LNK_FREE, pos), LKappa.Maintained) in
let counter_agent_info = Signature.get_counter_agent_info sigs in
let port_b = fst counter_agent_info.ports in
let port_a = snd counter_agent_info.ports in
let ra_type = counter_agent_info.id in

let ra_ports =
Array.make counter_agent_info.arity
((LKappa.LNK_FREE, pos), LKappa.Maintained)
in
let before_switch =
if first && created then
LKappa.Linked i
Expand All @@ -440,19 +447,19 @@ let make_counter_agent sigs (first, (dst, ra_erased)) (last, equal) i j pos
if first then
LKappa.LNK_VALUE (i, dst), pos
else
LKappa.LNK_VALUE (i, (ra_type, incr_a)), pos
LKappa.LNK_VALUE (i, (ra_type, port_a)), pos
in
let () = ra_ports.(incr_b) <- before, before_switch in
let () = ra_ports.(port_b) <- before, before_switch in
let after =
if last && equal then
LKappa.LNK_FREE, pos
else if last then
LKappa.LNK_ANY, pos
else
LKappa.LNK_VALUE (j, (ra_type, incr_b)), pos
LKappa.LNK_VALUE (j, (ra_type, port_b)), pos
in
let () = ra_ports.(incr_a) <- after, LKappa.Maintained in
let ra_ints = Array.make arity LKappa.I_ANY in
let () = ra_ports.(port_a) <- after, LKappa.Maintained in
let ra_ints = Array.make counter_agent_info.arity LKappa.I_ANY in
{
LKappa.ra_type;
ra_erased;
Expand All @@ -462,19 +469,21 @@ let make_counter_agent sigs (first, (dst, ra_erased)) (last, equal) i j pos
}

let raw_counter_agent (first, first_link) (last, last_link) i j sigs equal =
let incr_type, arity, incr_b, incr_a = Signature.incr_agent sigs in
let ports = Array.make arity Raw_mixture.FREE in
let counter_agent_info = Signature.get_counter_agent_info sigs in
let port_b = fst counter_agent_info.ports in
let port_a = snd counter_agent_info.ports in
let ports = Array.make counter_agent_info.arity Raw_mixture.FREE in
let internals =
Array.init arity (fun i ->
Signature.default_internal_state incr_type i sigs)
Array.init counter_agent_info.arity (fun i ->
Signature.default_internal_state counter_agent_info.id i sigs)
in
let before =
if first then
Raw_mixture.VAL first_link
else
Raw_mixture.VAL i
in
let () = ports.(incr_b) <- before in
let () = ports.(port_b) <- before in
let after =
if last && equal then
Raw_mixture.FREE
Expand All @@ -483,9 +492,9 @@ let raw_counter_agent (first, first_link) (last, last_link) i j sigs equal =
else
Raw_mixture.VAL j
in
let () = ports.(incr_a) <- after in
let () = ports.(port_a) <- after in
{
Raw_mixture.a_type = incr_type;
Raw_mixture.a_type = counter_agent_info.id;
Raw_mixture.a_ports = ports;
Raw_mixture.a_ints = internals;
}
Expand Down Expand Up @@ -519,12 +528,13 @@ let rec link_incr sigs i nb ag_info equal lnk pos delta =
)

let rec erase_incr sigs i incrs delta lnk =
let _, _, incr_b, _ = Signature.incr_agent sigs in
let counter_agent_info = Signature.get_counter_agent_info sigs in
let port_b = fst counter_agent_info.ports in
match incrs with
| hd :: tl ->
if i = abs delta then (
let before, _ = hd.LKappa.ra_ports.(incr_b) in
let () = hd.LKappa.ra_ports.(incr_b) <- before, LKappa.Linked lnk in
let before, _ = hd.LKappa.ra_ports.(port_b) in
let () = hd.LKappa.ra_ports.(port_b) <- before, LKappa.Linked lnk in
hd :: tl
) else (
let () =
Expand All @@ -539,7 +549,6 @@ let rec erase_incr sigs i incrs delta lnk =

let counter_becomes_port sigs ra p_id (delta, pos') pos equal test start_link_nb
=
let incr_type, _, incr_b, _ = Signature.incr_agent sigs in
let start_link_for_created = start_link_nb + test + 1 in
let lnk_for_erased = start_link_nb + abs delta in
let ag_info = (p_id, ra.LKappa.ra_type), ra.LKappa.ra_erased in
Expand Down Expand Up @@ -574,8 +583,11 @@ let counter_becomes_port sigs ra p_id (delta, pos') pos equal test start_link_nb
else
LKappa.Linked lnk_for_erased
in
let counter_agent_info = Signature.get_counter_agent_info sigs in
let port_b = fst counter_agent_info.ports in
let p =
(LKappa.LNK_VALUE (start_link_nb, (incr_b, incr_type)), pos), switch
( (LKappa.LNK_VALUE (start_link_nb, (port_b, counter_agent_info.id)), pos),
switch )
in
let () = ra.LKappa.ra_ports.(p_id) <- p in
adjust_delta, created
Expand Down Expand Up @@ -710,7 +722,6 @@ let remove_counter_rule sigs mix created =
List.rev_map (fun ag -> ag.ra) (List.rev created) )

let agent_with_max_counter sigs c ((agent_name, _) as ag_ty) =
let incr_type, _, incr_b, _ = Signature.incr_agent sigs in
let ag_id = Signature.num_of_agent ag_ty sigs in
let sign = Signature.get sigs ag_id in
let arity = Signature.arity sigs ag_id in
Expand All @@ -726,7 +737,9 @@ let agent_with_max_counter sigs c ((agent_name, _) as ag_ty) =
let incrs =
link_incr sigs 0 (max_val' + 1) ((c_id, ag_id), false) false 1 pos (-1)
in
let p = LKappa.LNK_VALUE (1, (incr_b, incr_type)), pos in
let counter_agent_info = Signature.get_counter_agent_info sigs in
let port_b = fst counter_agent_info.ports in
let p = LKappa.LNK_VALUE (1, (port_b, counter_agent_info.id)), pos in
let () = ports.(c_id) <- p, LKappa.Maintained in
let ra =
{
Expand Down Expand Up @@ -791,8 +804,10 @@ let make_counter i name =
}

let add_counter_to_contact_map sigs add_link_contact_map =
let incr_id, _, incr_b, incr_a = Signature.incr_agent sigs in
add_link_contact_map incr_id incr_a incr_id incr_b
let counter_agent_info = Signature.get_counter_agent_info sigs in
let port_b = fst counter_agent_info.ports in
let port_a = snd counter_agent_info.ports in
add_link_contact_map counter_agent_info.id port_a counter_agent_info.id port_b

let forbid_modification (delta, pos) =
if delta != 0 then LKappa.forbid_modification pos (Some delta)
Expand Down Expand Up @@ -833,8 +848,9 @@ let annotate_edit_counters sigs ((agent_name, _) as ag_ty) counters ra
let arity = Signature.arity sigs ag_id in
let ra_counters = Array.make arity None in
let register_counter_modif c_id =
let incr_id, _, incr_b, _ = Signature.incr_agent sigs in
add_link_contact_map ag_id c_id incr_id incr_b
let counter_agent_info = Signature.get_counter_agent_info sigs in
let port_b = fst counter_agent_info.ports in
add_link_contact_map ag_id c_id counter_agent_info.id port_b
in
let _ =
List.fold_left
Expand Down Expand Up @@ -864,8 +880,9 @@ let annotate_counters_with_diff sigs ((agent_name, pos) as ag_ty) lc rc ra
let sign = Signature.get sigs ag_id in
let arity = Signature.arity sigs ag_id in
let register_counter_modif c c_id =
let incr_id, _, incr_b, _ = Signature.incr_agent sigs in
let () = add_link_contact_map ag_id c_id incr_id incr_b in
let counter_agent_info = Signature.get_counter_agent_info sigs in
let port_b = fst counter_agent_info.ports in
let () = add_link_contact_map ag_id c_id counter_agent_info.id port_b in
c, LKappa.Maintained
in
let ra_counters = Array.make arity None in
Expand Down Expand Up @@ -949,8 +966,9 @@ let annotate_created_counters sigs ((agent_name, _) as ag_ty) counters
in

let register_counter_modif c_id =
let incr_id, _, incr_b, _ = Signature.incr_agent sigs in
add_link_contact_map ag_id c_id incr_id incr_b
let counter_agent_info = Signature.get_counter_agent_info sigs in
let port_b = fst counter_agent_info.ports in
add_link_contact_map ag_id c_id counter_agent_info.id port_b
in
let _ =
List.fold_left
Expand Down
6 changes: 3 additions & 3 deletions core/grammar/lKappa_compiler.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1668,12 +1668,12 @@ let prepare_agent_sig ~(sites : Ast.site list) :
( ( c.counter_name,
{
internal_state = NamedDecls.create [||];
(* Agent with counter can link to port [b] on counter agent [__incr] *)
(* Agent with counter can link to port [b] on counter agent [__counter_agent] *)
links =
Some
[
( Locality.annotate_with_dummy "b",
Locality.annotate_with_dummy "__incr" );
Locality.annotate_with_dummy "__counter_agent" );
];
counters_info = Some (j, Locality.v c.counter_delta);
} )
Expand All @@ -1693,7 +1693,7 @@ let make_counter_agent_site_sigs
(string * Locality.t)
* ((string * Locality.t) * (string * Locality.t)) list Signature.site_sig
NamedDecls.t =
let counter_agent_name = "__incr", Locality.dummy in
let counter_agent_name = "__counter_agent", Locality.dummy in
let a_port_name = "a", Locality.dummy in
(* after port *)
let b_port_name = "b", Locality.dummy in
Expand Down
91 changes: 46 additions & 45 deletions core/siteGraphs/signature.ml
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ let one_to_json =
signature.counters_info );
])

let one_of_json =
let one_of_json : Yojson.Basic.t -> bool array array site_sig NamedDecls.t =
NamedDecls.of_json (function
| `Assoc [ ("internal_state", a); ("links", b); ("counters_info", c) ] ->
{
Expand Down Expand Up @@ -141,18 +141,24 @@ let one_of_json =
| x ->
raise (Yojson.Basic.Util.Type_error ("Problematic agent signature", x)))

(* TODO rework this type: rename t, merge incr and incr_sites *)
type s = { t: t NamedDecls.t; incr: int option; incr_sites: (int * int) option }
type counter_agent_info = { id: int; arity: int; ports: int * int }

let size sigs = NamedDecls.size sigs.t
let get sigs agent_id = NamedDecls.elt_val sigs.t agent_id
type s = {
agent_sigs: t NamedDecls.t;
counter_agent_info: counter_agent_info option;
}

let size sigs = NamedDecls.size sigs.agent_sigs
let get sigs agent_id = NamedDecls.elt_val sigs.agent_sigs agent_id
let arity sigs agent_id = NamedDecls.size (get sigs agent_id)

let max_arity sigs =
NamedDecls.fold (fun _ _ x a -> max x (NamedDecls.size a)) 0 sigs.t
NamedDecls.fold (fun _ _ x a -> max x (NamedDecls.size a)) 0 sigs.agent_sigs

let agent_of_num i sigs = NamedDecls.elt_name sigs.agent_sigs i

let agent_of_num i sigs = NamedDecls.elt_name sigs.t i
let num_of_agent name sigs = NamedDecls.elt_id ~kind:"agent" sigs.t name
let num_of_agent name sigs =
NamedDecls.elt_id ~kind:"agent" sigs.agent_sigs name

let id_of_site ((agent_name, _) as agent_ty) site_name sigs =
let n = num_of_agent agent_ty sigs in
Expand Down Expand Up @@ -199,44 +205,36 @@ let rec allowed_link ag1 s1 ag2 s2 sigs =

let create ~counters_per_agent agent_sigs =
{
t = agent_sigs;
incr =
(if counters_per_agent = [] then
None
else
Some 0);
incr_sites =
agent_sigs;
counter_agent_info =
(if counters_per_agent = [] then
None
else
Some (0, 1));
(* If there is a counter agent, we choose 0 for its agent id and 0 and 1 as its port ids *)
Some { id = 0; arity = 2; ports = 0, 1 });
}

let is_counter_agent sigs n_id =
match sigs.incr with
match sigs.counter_agent_info with
| None -> false
| Some incr_id -> n_id = incr_id
| Some agent_info -> n_id = agent_info.id

let ports_if_counter_agent sigs n_id =
if
match sigs.incr with
| None -> false
| Some incr_id -> n_id = incr_id
then
sigs.incr_sites
else
None
match sigs.counter_agent_info with
| None -> None
| Some agent_info ->
if n_id = agent_info.id then
Some agent_info.ports
else
None

let site_is_counter sigs ag_ty id =
counter_of_site_id id (get sigs ag_ty) <> None

let incr_agent sigs =
match sigs.incr with
| None -> failwith "No incr agent"
| Some id ->
(match sigs.incr_sites with
| None -> failwith "Signature of counter inconsistent"
| Some (before, after) -> id, 2, before, after)
let get_counter_agent_info sigs =
match sigs.counter_agent_info with
| None -> failwith "No counter agent"
| Some counter_agent_info -> counter_agent_info

let print_agent sigs f ag_ty =
Format.pp_print_string f @@ agent_of_num ag_ty sigs
Expand Down Expand Up @@ -299,19 +297,22 @@ let print f sigs =
Format.fprintf f "@[<v>%a@]"
(NamedDecls.print ~sep:Pp.space (fun i n f si ->
Format.fprintf f "@[<h>%%agent: %s(%a)@]" n (print_one ~sigs i) si))
sigs.t
sigs.agent_sigs

let to_json sigs = NamedDecls.to_json one_to_json sigs.t
let to_json sigs = NamedDecls.to_json one_to_json sigs.agent_sigs

let of_json v =
let t = NamedDecls.of_json one_of_json v in
let incr, incr_sites =
match Mods.StringMap.find_option "__incr" t.NamedDecls.finder with
| Some incr_id ->
let incr = NamedDecls.elt_val t incr_id in
let after = num_of_site ("a", Locality.dummy) incr in
let before = num_of_site ("b", Locality.dummy) incr in
Some incr_id, Some (before, after)
| None -> None, None
let agent_sigs : 'a site_sig NamedDecls.t NamedDecls.t =
NamedDecls.of_json one_of_json v
in
{ t; incr; incr_sites }
match
Mods.StringMap.find_option "__counter_agent" agent_sigs.NamedDecls.finder
with
| Some id ->
let agent_signature = NamedDecls.elt_val agent_sigs id in
let ports =
( num_of_site ("a", Locality.dummy) agent_signature,
num_of_site ("b", Locality.dummy) agent_signature )
in
{ agent_sigs; counter_agent_info = Some { id; arity = 2; ports } }
| None -> { agent_sigs; counter_agent_info = None }
9 changes: 7 additions & 2 deletions core/siteGraphs/signature.mli
Original file line number Diff line number Diff line change
Expand Up @@ -81,12 +81,17 @@ val allowed_link : int -> int -> int -> int -> s -> bool

(** {2 Counter specific} *)

(** If there are counters in the signature, we define a single agent as the
* counter agent, which will be used as _dummies_ to keep track of the value *)

val is_counter_agent : s -> int -> bool
val ports_if_counter_agent : s -> int -> (int * int) option
val site_is_counter : s -> int -> int -> bool

val incr_agent : s -> int * int * int * int
(** id, arity, before, after *)
type counter_agent_info = { id: int; arity: int; ports: int * int }

val get_counter_agent_info : s -> counter_agent_info
(** [counter_agent agent_sigs] *)

(** {2 I/O} *)

Expand Down
Loading

0 comments on commit 06ddb9d

Please sign in to comment.