propagate information to translate counters

core/KaSa_rep/frontend/ckappa_sig.ml

@@ -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.visible;
+  counter_visible: Ast.origine;
 }
 
 and counter_test = CEQ of int | CGTE of int | CVAR of string | UNKNOWN

core/KaSa_rep/frontend/ckappa_sig.mli

@@ -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.visible;
+  counter_visible: Ast.origine;
 }
 
 and counter_test = CEQ of int | CGTE of int | CVAR of string | UNKNOWN

core/grammar/ast.ml

@@ -37,26 +37,27 @@ 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
 
-type hidden_info =
-  {
-    from_sig_name: string Loc.annoted;
-    convert_value: (int -> int);
-    convert_delta: (int -> int);
-    convert_test: (counter_test option -> counter_test option);
-    convert_back_value: (int -> int);
-    convert_back_delta: (int -> int);
-    convert_back_test: (counter_test option -> counter_test option)
-  }
+let apply_int t i =
+  match t with
+    | BASIS_MINUS_INPUT d -> d - 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 visible = Visible | Hidden of hidden_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: visible;
+  counter_sig_visible: origine;
   counter_sig_default: int;
 }
 
@@ -76,47 +77,32 @@ let counter_sig_of_counter (c : counter) : counter_sig =
     counter_sig_min;
     counter_sig_max;
     counter_sig_default;
-    counter_sig_visible = Visible;
+    counter_sig_visible = From_original_ast;
   }
 
 let make_inverted_counter_sig (counter : counter_sig)
     (counter_sig_name : string Loc.annoted) : counter_sig =
   let f_int =
-  (match counter.counter_sig_max, counter.counter_sig_min with
-  | Some (Some max, _), Some (Some min, _) ->
-    fun i -> max - i + min
-  | (None | Some (None, _)), _ | _, (None | Some (None, _)) ->
-    failwith "unbounded counters not implemented yet");
+    match counter.counter_sig_max, counter.counter_sig_min with
+    | Some (Some max, _), Some (Some min, _) ->
+      BASIS_MINUS_INPUT (max+min)
+    | (None | Some (None, _)), _ | _, (None | Some (None, _)) ->
+      failwith "unbounded counters not implemented yet"
   in
-  let f_op i = -i in
+  let f_op = BASIS_MINUS_INPUT 0 in
   {
     counter with
     counter_sig_name;
     counter_sig_visible =
-      Hidden
+      From_clte_elimination
       {
         from_sig_name=counter.counter_sig_name;
         convert_value=f_int;
         convert_delta=f_op;
-        convert_test=(fun x ->
-                        match x with
-                        | None | Some (CVAR _) -> None
-                        | Some (CEQ i) -> Some (CEQ (f_int i))
-                        | Some (CGTE i) -> Some (CLTE (f_int i))
-                        | Some (CLTE i) -> Some (CGTE (f_int i)));
-        convert_back_value=f_int;
-        convert_back_delta=f_op;
-        convert_back_test=(fun x ->
-                        match x with
-                        | None -> None
-                        | Some (CVAR _) -> failwith "there should be no variable in inverted counters"
-                        | Some (CEQ i) -> Some (CEQ (f_int i))
-                        | Some (CGTE i) -> Some (CLTE (f_int i))
-                        | Some (CLTE i) -> Some (CGTE (f_int i)));
       }
     ;
     counter_sig_default =
-      f_int counter.counter_sig_default
+      apply_int f_int counter.counter_sig_default
 
   }
 
@@ -696,7 +682,7 @@ let site_sig_of_json filenames = function
                (Yojson.Basic.Util.to_option Yojson.Basic.Util.to_int))
             max;
         counter_sig_default = Yojson.Basic.Util.to_int default;
-        counter_sig_visible = Visible;
+        counter_sig_visible = From_original_ast;
       }
   | `Assoc [ ("port_name", n); ("port_int", i); ("port_link", l) ]
   | `Assoc [ ("port_name", n); ("port_link", l); ("port_int", i) ]
@@ -855,7 +841,7 @@ let agent_sig_of_json = agent_of_json ~site_of_json:site_sig_of_json
 let agent_sig_to_json =
   agent_to_json ~counter_to_json:counter_sig_to_json ~filter:(fun c ->
       match c with
-      | Counter c -> c.counter_sig_visible=Visible
+      | Counter c -> c.counter_sig_visible=From_original_ast
       | Port _ -> true)
 
 let agent_of_json = agent_of_json ~site_of_json

core/grammar/ast.mli

@@ -35,24 +35,24 @@ type counter = {
   counter_delta: int Loc.annoted;
 }
 
-type hidden_info =
+type translate_int = BASIS_MINUS_INPUT of int
+
+val apply_int: translate_int -> int -> int
+
+type conversion_info =
   {
     from_sig_name: string Loc.annoted;
-    convert_value: (int -> int);
-    convert_delta: (int -> int);
-    convert_test: (counter_test option -> counter_test option);
-    convert_back_value: (int -> int);
-    convert_back_delta: (int -> int);
-    convert_back_test: (counter_test option -> counter_test option)
+    convert_value: translate_int;
+    convert_delta: translate_int;
   }
 
-type visible = Visible | Hidden of hidden_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: visible;
+  counter_sig_visible: origine;
   counter_sig_default: int;
 }
 

core/grammar/kappaParser.mly

@@ -529,14 +529,14 @@ port_expression_sig:
            Ast.counter_sig_min = None;
            Ast.counter_sig_max = Some (Some $4, rhs_pos 4);
            Ast.counter_sig_default = $4;
-           Ast.counter_sig_visible = Ast.Visible}}
+           Ast.counter_sig_visible = Ast.From_original_ast}}
   | ID PLUS EQUAL MINUS INT
         {Ast.Counter
   { Ast.counter_sig_name = ($1,rhs_pos 1);
     Ast.counter_sig_min = None;
     Ast.counter_sig_max = Some (Some (-$5), rhs_pos 5);
     Ast.counter_sig_default = -$5;
-    Ast.counter_sig_visible = Ast.Visible}}
+    Ast.counter_sig_visible = Ast.From_original_ast}}
   | ID counter_test PLUS EQUAL INT
        { let min =
             match $2 with
@@ -548,7 +548,7 @@ port_expression_sig:
            Ast.counter_sig_min = Some (Some min, rhs_pos 2);
            Ast.counter_sig_max = Some (Some $5, rhs_pos 5);
            Ast.counter_sig_default = min;
-           Ast.counter_sig_visible = Ast.Visible}}
+           Ast.counter_sig_visible = Ast.From_original_ast}}
   | ID counter_test PLUS EQUAL MINUS INT
       { let min =
            match $2 with
@@ -561,7 +561,7 @@ port_expression_sig:
           Ast.counter_sig_min = Some (Some min, rhs_pos 2);
           Ast.counter_sig_max = Some (Some (-$6), rhs_pos 6);
           Ast.counter_sig_default = min ;
-          Ast.counter_sig_visible = Ast.Visible}}
+          Ast.counter_sig_visible = Ast.From_original_ast}}
   | ID counter_test
       { let min =
            match $2 with
@@ -574,7 +574,7 @@ port_expression_sig:
     Ast.counter_sig_min = Some (Some min, rhs_pos 2);
     Ast.counter_sig_max = None;
     Ast.counter_sig_default = min;
-    Ast.counter_sig_visible = Ast.Visible}}
+    Ast.counter_sig_visible = Ast.From_original_ast}}
 
 
 internal_state:

core/grammar/kparser4.mly

@@ -180,7 +180,7 @@ site_counter_sig:
                 (match counter_sig_min with
                   | None | Some (None, _)-> 0
                   | Some (Some i,_) -> i );
-            Ast.counter_sig_visible=Ast.Visible;
+            Ast.counter_sig_visible=Ast.From_original_ast;
             } }
     | ID annoted
       { Ast.Port

core/grammar/lKappa_compiler.ml

@@ -2065,12 +2065,20 @@ let translate_clte_into_cgte (ast_compil : Ast.parsing_compil) =
         | Some (Ast.CEQ _) | Some (Ast.CGTE _) | Some (Ast.CVAR _) | None -> acc)
   in
 
+  let add (x,y) data map =
+         Mods.StringMap.add
+           x
+           (Mods.StringMap.add y data
+                 (Mods.StringMap.find_default Mods.StringMap.empty x map))
+           map
+  in
   (* Create opposite counters that have the same tests *)
-  let signatures : Ast.agent_sig list =
-    List.map
-      (fun agent ->
+  let (signatures : Ast.agent_sig list),
+      (map : Ast.conversion_info Mods.StringMap.t Mods.StringMap.t)=
+    List.fold_left
+      (fun (acc,map) agent ->
         match agent with
-        | Ast.Absent _ -> agent
+        | Ast.Absent _ -> agent::acc, map
         | Present (agent_name_, site_list, agent_mod) ->
           let agent_name = Loc.v agent_name_ in
           let counters_with_clte_tests_from_agent :
@@ -2080,9 +2088,11 @@ let translate_clte_into_cgte (ast_compil : Ast.parsing_compil) =
                 agent_name = agent_name_counter)
               counters_with_clte_tests
           in
-          let new_counter_sites : Ast.counter_sig Ast.site list =
+          let (new_counter_sites : Ast.counter_sig Ast.site list),
+              map
+            =
             List.fold_left
-              (fun acc (_, counter_name, sum_bounds_ref) ->
+              (fun (acc,map) (_, counter_name, sum_bounds_ref) ->
                 (* Find counter to invert *)
                 let counter_orig : Ast.counter_sig =
                   List.find_map
@@ -2117,26 +2127,36 @@ let translate_clte_into_cgte (ast_compil : Ast.parsing_compil) =
                          ( "Cannot take the opposite of an unbounded counters  ",
                            Loc.get_annot counter_orig.counter_sig_name ))
                 in
-
-                let counter_sig_visible = Ast.Visible in
+                let convert_info =
+                  {
+                    Ast.from_sig_name = counter_orig.counter_sig_name;
+                    convert_value = BASIS_MINUS_INPUT (inf_bound + sup_bound);
+                    convert_delta = BASIS_MINUS_INPUT (inf_bound + sup_bound)
+                  }
+                in
+                let counter_sig_visible =
+                      Ast.From_clte_elimination convert_info
+                in
                 (* Write in sum_bounds_ref the sum of the counter bounds above *)
                 sum_bounds_ref := inf_bound + sup_bound;
-
-                Ast.Counter
+                let counter =
                   {
                     Ast.counter_sig_name;
                     Ast.counter_sig_min;
                     Ast.counter_sig_max;
                     Ast.counter_sig_default;
                     Ast.counter_sig_visible;
                   }
-                :: acc)
-              [] counters_with_clte_tests_from_agent
+                in
+                (Ast.Counter counter)::acc,
+                add (agent_name,Loc.v counter_orig.counter_sig_name) convert_info map)
+              ([],map) (List.rev counters_with_clte_tests_from_agent)
           in
-
-          Ast.Present (agent_name_, site_list @ new_counter_sites, agent_mod))
-      ast_compil.signatures
+          (Ast.Present (agent_name_, site_list @ new_counter_sites, agent_mod))::acc,
+           map)
+      ([], Mods.StringMap.empty) (List.rev ast_compil.signatures)
   in
+  let _ = map in
 
   (* In rules, we need to replace the counter tests and the counter modifications *)
   let replace_counter_by_invert (mix : Ast.mixture) : Ast.mixture =