From 06ddb9d233fb83d7ffbc4fa5866c5e4069ff0495 Mon Sep 17 00:00:00 2001 From: Antoine Pouille Date: Mon, 27 Nov 2023 16:56:24 +0100 Subject: [PATCH] Clarify counter_agent_info fetched from signatures with record and names --- core/grammar/counters_compiler.ml | 76 ++++++++++++++++---------- core/grammar/lKappa_compiler.ml | 6 +- core/siteGraphs/signature.ml | 91 ++++++++++++++++--------------- core/siteGraphs/signature.mli | 9 ++- core/symmetries/kade_backend.ml | 20 +++---- core/term/lKappa.ml | 6 +- core/term/raw_mixture.ml | 18 +++--- 7 files changed, 125 insertions(+), 101 deletions(-) diff --git a/core/grammar/counters_compiler.ml b/core/grammar/counters_compiler.ml index dfdcb717d..54b4a991c 100644 --- a/core/grammar/counters_compiler.ml +++ b/core/grammar/counters_compiler.ml @@ -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 @@ -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; @@ -462,11 +469,13 @@ 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 @@ -474,7 +483,7 @@ let raw_counter_agent (first, first_link) (last, last_link) i j sigs equal = 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 @@ -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; } @@ -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 () = @@ -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 @@ -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 @@ -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 @@ -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 = { @@ -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) @@ -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 @@ -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 @@ -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 diff --git a/core/grammar/lKappa_compiler.ml b/core/grammar/lKappa_compiler.ml index 892e22c43..e98fb52fb 100644 --- a/core/grammar/lKappa_compiler.ml +++ b/core/grammar/lKappa_compiler.ml @@ -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); } ) @@ -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 diff --git a/core/siteGraphs/signature.ml b/core/siteGraphs/signature.ml index 66ea31622..38e9fd548 100644 --- a/core/siteGraphs/signature.ml +++ b/core/siteGraphs/signature.ml @@ -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) ] -> { @@ -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 @@ -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 @@ -299,19 +297,22 @@ let print f sigs = Format.fprintf f "@[%a@]" (NamedDecls.print ~sep:Pp.space (fun i n f si -> Format.fprintf f "@[%%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 } diff --git a/core/siteGraphs/signature.mli b/core/siteGraphs/signature.mli index 10fb3f604..57fffa013 100644 --- a/core/siteGraphs/signature.mli +++ b/core/siteGraphs/signature.mli @@ -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} *) diff --git a/core/symmetries/kade_backend.ml b/core/symmetries/kade_backend.ml index c1ebcffe8..e3b75f788 100644 --- a/core/symmetries/kade_backend.ml +++ b/core/symmetries/kade_backend.ml @@ -232,13 +232,13 @@ end module Raw_mixture = struct include Raw_mixture - let print_link ~noCounters symbol_table incr_agents f = function + let print_link ~noCounters symbol_table counter_agents f = function | Raw_mixture.FREE -> Utils.print_free_site f symbol_table | Raw_mixture.VAL i -> (try - let root = Raw_mixture.find incr_agents i in + let root = Raw_mixture.find counter_agents i in let counter, (_, is_counter) = - Mods.DynArray.get incr_agents.Raw_mixture.rank root + Mods.DynArray.get counter_agents.Raw_mixture.rank root in if is_counter && not noCounters then Format.fprintf f "{=%d}" counter @@ -271,7 +271,7 @@ module Raw_mixture = struct | None -> Format.pp_print_int f s) let print_intf ~noCounters with_link ?sigs - ?(symbol_table = Symbol_table.symbol_table_V4) incr_agents (ag_ty : int) f + ?(symbol_table = Symbol_table.symbol_table_V4) counter_agents (ag_ty : int) f (ports, ints) = let rec aux empty i = if i < Array.length ports then ( @@ -284,7 +284,7 @@ module Raw_mixture = struct (aux_pp_si sigs symbol_table ag_ty i) ints.(i) (if with_link then - print_link ~noCounters symbol_table incr_agents + print_link ~noCounters symbol_table counter_agents else fun _ _ -> ()) @@ -301,10 +301,10 @@ module Raw_mixture = struct | None -> Format.pp_print_int f a let print_agent ~noCounters created link ?sigs - ?(symbol_table = Symbol_table.symbol_table_V4) incr_agents f ag = + ?(symbol_table = Symbol_table.symbol_table_V4) counter_agents f ag = Format.fprintf f "%a%s@[%a@]%s%t" (aux_pp_ag sigs) ag.Raw_mixture.a_type symbol_table.Symbol_table.agent_open - (print_intf ~noCounters link ?sigs ~symbol_table incr_agents + (print_intf ~noCounters link ?sigs ~symbol_table counter_agents ag.Raw_mixture.a_type) (ag.Raw_mixture.a_ports, ag.Raw_mixture.a_ints) symbol_table.Symbol_table.agent_close (fun f -> if created then Format.pp_print_string f "+") @@ -312,7 +312,7 @@ module Raw_mixture = struct let print ~noCounters ~created ?sigs ?(symbol_table = Symbol_table.symbol_table_V4) f mix = - let incr_agents = Raw_mixture.union_find_counters sigs mix in + let counter_agents = Raw_mixture.union_find_counters sigs mix in let rec aux_print some = function | [] -> () | h :: t -> @@ -327,7 +327,7 @@ module Raw_mixture = struct else ( let () = if some then Utils.print_agent_sep_comma symbol_table f in let () = - print_agent ~noCounters created true ?sigs ~symbol_table incr_agents + print_agent ~noCounters created true ?sigs ~symbol_table counter_agents f h in aux_print true t @@ -522,7 +522,7 @@ module LKappa = struct raise (ExceptionDefn.Internal_Error (Locality.annotate_with_dummy - "Port a of __incr agent not well specified"))))) + "Port a of __counter_agent agent not well specified"))))) mix in t diff --git a/core/term/lKappa.ml b/core/term/lKappa.ml index c58bd96ae..733b8d947 100644 --- a/core/term/lKappa.ml +++ b/core/term/lKappa.ml @@ -261,7 +261,7 @@ let union_find_counters sigs mix = raise (ExceptionDefn.Internal_Error (Locality.annotate_with_dummy - "Port a of __incr agent not well specified"))))) + "Port a of __counter_agent agent not well specified"))))) mix in t @@ -273,7 +273,7 @@ let print_rule_agent ~noCounters sigs ~ltypes counters created_counters f ag = if ag.ra_erased then Format.pp_print_string f "-") let print_rule_mixture ~noCounters sigs ~ltypes created f mix = - let incr_agents = union_find_counters (Some sigs) mix in + let counter_agents = union_find_counters (Some sigs) mix in let created_incr = Raw_mixture.union_find_counters (Some sigs) created in let rec aux_print some = function | [] -> () @@ -283,7 +283,7 @@ let print_rule_mixture ~noCounters sigs ~ltypes created f mix = else ( let () = if some then Pp.comma f in let () = - print_rule_agent ~noCounters sigs ~ltypes incr_agents created_incr f h + print_rule_agent ~noCounters sigs ~ltypes counter_agents created_incr f h in aux_print true t ) diff --git a/core/term/raw_mixture.ml b/core/term/raw_mixture.ml index 8cc857fc6..a695fc782 100644 --- a/core/term/raw_mixture.ml +++ b/core/term/raw_mixture.ml @@ -95,12 +95,12 @@ let union_find_counters sigs mix = in t -let print_link ~noCounters incr_agents f = function +let print_link ~noCounters counter_agents f = function | FREE -> Format.pp_print_string f "[.]" | VAL i -> (try - let root = find incr_agents i in - let counter, (_, is_counter) = Mods.DynArray.get incr_agents.rank root in + let root = find counter_agents i in + let counter, (_, is_counter) = Mods.DynArray.get counter_agents.rank root in if is_counter && not noCounters then Format.fprintf f "{=%d}" counter else @@ -115,7 +115,7 @@ let aux_pp_si sigs a s f i = | Some i -> Format.fprintf f "%i{%i}" s i | None -> Format.pp_print_int f s) -let print_intf ~noCounters with_link ?sigs incr_agents ag_ty f (ports, ints) = +let print_intf ~noCounters with_link ?sigs counter_agents ag_ty f (ports, ints) = let rec aux empty i = if i < Array.length ports then ( let () = @@ -126,7 +126,7 @@ let print_intf ~noCounters with_link ?sigs incr_agents ag_ty f (ports, ints) = Pp.space) (aux_pp_si sigs ag_ty i) ints.(i) (if with_link then - print_link ~noCounters incr_agents + print_link ~noCounters counter_agents else fun _ _ -> ()) @@ -142,14 +142,14 @@ let aux_pp_ag sigs f a = | Some sigs -> Signature.print_agent sigs f a | None -> Format.pp_print_int f a -let print_agent ~noCounters created link ?sigs incr_agents f ag = +let print_agent ~noCounters created link ?sigs counter_agents f ag = Format.fprintf f "%a(@[%a@])%t" (aux_pp_ag sigs) ag.a_type - (print_intf ~noCounters link ?sigs incr_agents ag.a_type) + (print_intf ~noCounters link ?sigs counter_agents ag.a_type) (ag.a_ports, ag.a_ints) (fun f -> if created then Format.pp_print_string f "+") let print ~noCounters ~created ~initial_comma ?sigs f mix = - let incr_agents = union_find_counters sigs mix in + let counter_agents = union_find_counters sigs mix in let rec aux_print some = function | [] -> () | h :: t -> @@ -162,7 +162,7 @@ let print ~noCounters ~created ~initial_comma ?sigs f mix = aux_print some t else ( let () = if some then Pp.comma f in - let () = print_agent ~noCounters created true ?sigs incr_agents f h in + let () = print_agent ~noCounters created true ?sigs counter_agents f h in aux_print true t ) in