Skip to content

Commit

Permalink
Start support for counters with negative values
Browse files Browse the repository at this point in the history
  • Loading branch information
Jérôme FERET committed Apr 3, 2024
1 parent 43af760 commit 63d8e86
Show file tree
Hide file tree
Showing 20 changed files with 325 additions and 221 deletions.
2 changes: 1 addition & 1 deletion core/KaSa_rep/frontend/ckappa_sig.ml
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ and counter_sig = {
counter_sig_default: int;
counter_sig_min: int option option;
counter_sig_max: int option option;
counter_visible: Ast.origine;
counter_visible: Counters_info.origine;
}

and counter_test = CEQ of int | CGTE of int | CVAR of string | UNKNOWN
Expand Down
2 changes: 1 addition & 1 deletion core/KaSa_rep/frontend/ckappa_sig.mli
Original file line number Diff line number Diff line change
Expand Up @@ -151,7 +151,7 @@ and counter_sig = {
counter_sig_default: int;
counter_sig_min: int option option;
counter_sig_max: int option option;
counter_visible: Ast.origine;
counter_visible: Counters_info.origine;
}

and counter_test = CEQ of int | CGTE of int | CVAR of string | UNKNOWN
Expand Down
16 changes: 8 additions & 8 deletions core/KaSa_rep/frontend/prepreprocess.ml
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,7 @@ let pop_entry parameters error id (map, set) =
)

let get_counter_name counter = fst counter.Ast.counter_name
let get_counter_name_sig counter = fst counter.Ast.counter_sig_name
let get_counter_name_sig counter = fst counter.Counters_info.counter_sig_name

let rec scan_interface ~get_counter_name parameters k agent interface
(((error, a), (set_sites, set_counters)) as remanent) =
Expand Down Expand Up @@ -287,10 +287,10 @@ let translate_counter parameters error int_set counter =
Some a);
} )

let translate_counter_sig parameters error int_set (counter : Ast.counter_sig) =
let translate_counter_sig parameters error int_set (counter : Counters_info.counter_sig) =
let error, _ =
check_freshness parameters error "Counters"
(fst counter.Ast.counter_sig_name)
(fst counter.Counters_info.counter_sig_name)
int_set
in
let fetch x =
Expand All @@ -300,11 +300,11 @@ let translate_counter_sig parameters error int_set (counter : Ast.counter_sig) =
in
( error,
{
Ckappa_sig.counter_sig_name = fst counter.Ast.counter_sig_name;
Ckappa_sig.counter_sig_max = fetch counter.Ast.counter_sig_max;
Ckappa_sig.counter_sig_min = fetch counter.Ast.counter_sig_min;
Ckappa_sig.counter_sig_default = counter.Ast.counter_sig_default;
Ckappa_sig.counter_visible = counter.Ast.counter_sig_visible;
Ckappa_sig.counter_sig_name = fst counter.Counters_info.counter_sig_name;
Ckappa_sig.counter_sig_max = fetch counter.Counters_info.counter_sig_max;
Ckappa_sig.counter_sig_min = fetch counter.Counters_info.counter_sig_min;
Ckappa_sig.counter_sig_default = counter.Counters_info.counter_sig_default;
Ckappa_sig.counter_visible = counter.Counters_info.counter_sig_visible;
} )

let rec translate_interface ~translate_counter parameters is_signature
Expand Down
4 changes: 3 additions & 1 deletion core/api/kappa_facade.ml
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,9 @@ let parse ~patternSharing (ast : Ast.parsing_compil) var_overwrite
~pause:(fun f -> Lwt.bind (yield ()) f)
~return:Lwt.return ?rescale_init:None ?overwrite_t0:None
~compile_mode_on:false ~outputs ~sharing:patternSharing
ast_compiled_data.agents_sig ast_compiled_data.token_names
ast_compiled_data.agents_sig
ast_compiled_data.counters_info
ast_compiled_data.token_names
ast_compiled_data.contact_map ast_compiled_data.result
>>= fun (env, with_trace, init_l) ->
let counter =
Expand Down
8 changes: 7 additions & 1 deletion core/cli/cli_init.ml
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ type preprocessed_ast = {

type compilation_result = {
conf: Configuration.t;
counters_info: Counters_info.t;
env: Model.t;
contact_map: Contact_map.t;
updated_alg_vars: int list;
Expand Down Expand Up @@ -60,7 +61,9 @@ let preprocess_ast ~warning ~debug_mode ?kasim_args cli_args
let conf, _, _, _ = Configuration.parse compil.Ast.configurations in
( Some
(LKappa_compiler.init_of_ast ~warning ~syntax_version
ast_compiled_data.agents_sig ast_compiled_data.contact_map
ast_compiled_data.agents_sig
ast_compiled_data.counters_info
ast_compiled_data.contact_map
ast_compiled_data.token_names.NamedDecls.finder
ast_compiled_data.alg_vars_finder compil.Ast.init),
conf.Configuration.initial )
Expand Down Expand Up @@ -121,6 +124,7 @@ let get_pack_from_preprocessed_ast kasim_args ~(compile_mode_on : bool)
?overwrite_init:preprocessed_ast.overwrite_init
?overwrite_t0:preprocessed_ast.overwrite_t0 ~compile_mode_on
preprocessed_ast.ast_compiled_data.agents_sig
preprocessed_ast.ast_compiled_data.counters_info
preprocessed_ast.ast_compiled_data.token_names
preprocessed_ast.ast_compiled_data.contact_map
preprocessed_ast.ast_compiled_data.result
Expand All @@ -136,6 +140,7 @@ let get_pack_from_preprocessed_ast kasim_args ~(compile_mode_on : bool)
{
conf = preprocessed_ast.conf;
env;
counters_info = preprocessed_ast.ast_compiled_data.counters_info;
contact_map = preprocessed_ast.ast_compiled_data.contact_map;
updated_alg_vars = preprocessed_ast.ast_compiled_data.updated_alg_vars;
story_compression;
Expand Down Expand Up @@ -186,6 +191,7 @@ let get_pack_from_marshalizedfile ~warning kasim_args cli_args marshalized_file
LKappa_compiler.init_of_ast ~warning
~syntax_version:cli_args.Run_cli_args.syntaxVersion
(Model.signatures compilation_result.env)
compilation_result.counters_info
compilation_result.contact_map
(Model.tokens_finder compilation_result.env)
(Model.algs_finder compilation_result.env)
Expand Down
1 change: 1 addition & 0 deletions core/cli/cli_init.mli
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ type preprocessed_ast = {
(* TODO contact map is also in env *)
type compilation_result = {
conf: Configuration.t;
counters_info: Counters_info.t;
env: Model.t;
contact_map: Contact_map.t;
updated_alg_vars: int list;
Expand Down
57 changes: 19 additions & 38 deletions core/grammar/ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -37,35 +37,16 @@ type counter = {
(** In a rule: change in counter value, in an agent declaration: max value of the counter, 0 if absent *)
}

type translate_int = BASIS_MINUS_INPUT of int

let apply_int t i =
match t with
| BASIS_MINUS_INPUT d -> d - i
| Counters_info.BASIS_MINUS_INPUT d -> d - i

let reorder_bounds t (i,j) =
match t with
| BASIS_MINUS_INPUT _ -> j,i

type conversion_info =
{
from_sig_name: string Loc.annoted;
convert_value: translate_int;
convert_delta: translate_int;
}
(** Counter syntax from AST, present in 3 contexts with different meanings: agent definition, species init declaration, rule *)

type origine = From_original_ast | From_clte_elimination of conversion_info
| Counters_info.BASIS_MINUS_INPUT _ -> j,i

type counter_sig = {
counter_sig_name: string Loc.annoted;
counter_sig_min: int option Loc.annoted option;
counter_sig_max: int option Loc.annoted option;
counter_sig_visible: origine;
counter_sig_default: int;
}

let counter_sig_of_counter (c : counter) : counter_sig =
let counter_sig_of_counter (c : counter) : Counters_info.counter_sig =
let (counter_sig_min, counter_sig_default) : (int option * Loc.t) option * int
=
match c.counter_test with
Expand All @@ -77,23 +58,23 @@ let counter_sig_of_counter (c : counter) : counter_sig =
| i, loc -> Some (Some i, loc)
in
{
counter_sig_name = c.counter_name;
Counters_info.counter_sig_name = c.counter_name;
counter_sig_min;
counter_sig_max;
counter_sig_default;
counter_sig_visible = From_original_ast;
}

let make_inverted_counter_sig (counter : counter_sig)
(counter_sig_name : string Loc.annoted) : counter_sig =
let make_inverted_counter_sig (counter : Counters_info.counter_sig)
(counter_sig_name : string Loc.annoted) : Counters_info.counter_sig =
let f_int =
match counter.counter_sig_max, counter.counter_sig_min with
| Some (Some max, _), Some (Some min, _) ->
BASIS_MINUS_INPUT (max+min)
Counters_info.BASIS_MINUS_INPUT (max+min)
| (None | Some (None, _)), _ | _, (None | Some (None, _)) ->
failwith "unbounded counters not implemented yet"
in
let f_op = BASIS_MINUS_INPUT 0 in
let f_op = Counters_info.BASIS_MINUS_INPUT 0 in
{
counter with
counter_sig_name;
Expand Down Expand Up @@ -123,7 +104,7 @@ type 'counter parametric_agent =
| Absent of Loc.t

type agent = counter parametric_agent
type agent_sig = counter_sig parametric_agent
type agent_sig = Counters_info.counter_sig parametric_agent

(* TODO: document why list list *)
type mixture = agent list list
Expand Down Expand Up @@ -363,13 +344,13 @@ let print_counter f c =
c.counter_delta

let print_counter_sig f c =
Format.fprintf f "%s{%a%a}%a" (fst c.counter_sig_name)
Format.fprintf f "%s{%a%a}%a" (fst c.Counters_info.counter_sig_name)
(Pp.option ~with_space:false print_counter_min)
c.counter_sig_min
c.Counters_info.counter_sig_min
(Pp.option ~with_space:false print_counter_max)
c.counter_sig_max
c.Counters_info.counter_sig_max
(print_counter_default c.counter_sig_min)
c.counter_sig_default
c.Counters_info.counter_sig_default

let print_ast_site ~print_counter f = function
| Port p -> print_ast_port f p
Expand Down Expand Up @@ -673,7 +654,7 @@ let site_sig_of_json filenames = function
] ->
Counter
{
counter_sig_name =
Counters_info.counter_sig_name =
Loc.annoted_of_yojson ~filenames Yojson.Basic.Util.to_string n;
counter_sig_min =
Yojson.Basic.Util.to_option
Expand Down Expand Up @@ -755,18 +736,18 @@ let counter_sig_to_json ~filenames c =
`Assoc
[
( "counter_sig_name",
Loc.yojson_of_annoted ~filenames JsonUtil.of_string c.counter_sig_name );
Loc.yojson_of_annoted ~filenames JsonUtil.of_string c.Counters_info.counter_sig_name );
( "counter_min",
JsonUtil.of_option
(Loc.yojson_of_annoted ~filenames
(JsonUtil.of_option JsonUtil.of_int))
c.counter_sig_min );
c.Counters_info.counter_sig_min );
( "counter_max",
JsonUtil.of_option
(Loc.yojson_of_annoted ~filenames
(JsonUtil.of_option JsonUtil.of_int))
c.counter_sig_max );
"counter_default", JsonUtil.of_int c.counter_sig_default;
c.Counters_info.counter_sig_max );
"counter_default", JsonUtil.of_int c.Counters_info.counter_sig_default;
]

let site_to_json ~counter_to_json filenames = function
Expand Down Expand Up @@ -1527,7 +1508,7 @@ let merge_internals =

let rec merge_sites_counter c = function
| [] -> [ Counter c ]
| Counter c' :: _ as l when fst c.counter_sig_name = fst c'.counter_sig_name
| Counter c' :: _ as l when fst c.Counters_info.counter_sig_name = fst c'.Counters_info.counter_sig_name
->
l
| ((Port _ | Counter _) as h) :: t -> h :: merge_sites_counter c t
Expand Down
18 changes: 9 additions & 9 deletions core/grammar/ast.mli
Original file line number Diff line number Diff line change
Expand Up @@ -35,29 +35,29 @@ type counter = {
counter_delta: int Loc.annoted;
}

type translate_int = BASIS_MINUS_INPUT of int
(*type translate_int = BASIS_MINUS_INPUT of int*)

val apply_int: translate_int -> int -> int
val reorder_bounds: translate_int -> ('a * 'a ) -> ('a * 'a)
val apply_int: Counters_info.translate_int -> int -> int
val reorder_bounds: Counters_info.translate_int -> ('a * 'a ) -> ('a * 'a)

type conversion_info =
(*type conversion_info =
{
from_sig_name: string Loc.annoted;
convert_value: translate_int;
convert_delta: translate_int;
}
}*)

type origine = From_original_ast | From_clte_elimination of conversion_info
(*type origine = From_original_ast | From_clte_elimination of conversion_info
type counter_sig = {
counter_sig_name: string Loc.annoted;
counter_sig_min: int option Loc.annoted option;
counter_sig_max: int option Loc.annoted option;
counter_sig_visible: origine;
counter_sig_default: int;
}
}*)

val make_inverted_counter_sig : counter_sig -> string Loc.annoted -> counter_sig
val make_inverted_counter_sig : Counters_info.counter_sig -> string Loc.annoted -> Counters_info.counter_sig

(* Site type, with custom definition of counter type: used with `counter` and `counter_sig` *)
type 'counter site = Port of port | Counter of 'counter
Expand All @@ -68,7 +68,7 @@ type 'counter parametric_agent =
| Absent of Loc.t

type agent = counter parametric_agent
type agent_sig = counter_sig parametric_agent
type agent_sig = Counters_info.counter_sig parametric_agent
type mixture = agent list list

val mixture_to_user_graph : mixture -> User_graph.connected_component
Expand Down
Loading

0 comments on commit 63d8e86

Please sign in to comment.