Added translation from CLTE to CGTE

core/KaSa_rep/frontend/prepreprocess.ml

@@ -257,6 +257,7 @@ let translate_counter_test test =
   | Ast.CEQ i -> Ckappa_sig.CEQ i
   | Ast.CGTE i -> Ckappa_sig.CGTE i
   | Ast.CVAR x -> Ckappa_sig.CVAR x
+  | Ast.CLTE _i -> failwith "not_implemented" (* TODO NOW *)
 
 let fst_opt a_opt =
   match a_opt with

core/dataStructures/loc.ml

@@ -12,6 +12,8 @@ type 'a annoted = 'a * t
 
 let v (v, _) = v
 let get_annot (_, annot) = annot
+let copy_annot (_, loc) a = a, loc
+let map_annot f (a, loc) = f a, loc
 
 let of_pos start_location end_location =
   let () =

core/dataStructures/loc.mli

@@ -19,6 +19,12 @@ val v : 'a annoted -> 'a
 val get_annot : 'a annoted -> t
 (** Extract annotation from Loc.annoted *)
 
+val copy_annot : 'b annoted -> 'a -> 'a annoted
+(** Create annoted variable with same annotation as existing variable *)
+
+val map_annot : ('a -> 'b) -> 'a annoted -> 'b annoted
+(** Apply operation on variable and keep annotation *)
+
 val of_pos : Lexing.position -> Lexing.position -> t
 val dummy : t
 val annot_with_dummy : 'a -> 'a annoted

core/grammar/ast.ml

@@ -24,20 +24,19 @@ type port = {
 }
 
 (* TODO change name, CVAR is not a test? *)
+(* TODO discriminate between counter definition and counter test ? *)
+(* TODO: change this to CTYPE = CTEST (CTESTTYPE * int) | CVAR string? *)
 
-(** What test is done by the counter expression
- * - CEQ: If counter value is equal to the specified value
- * - CGTE: If counter value is greater or equal to the specified value
- * - CVAR: Not a test, but defines a variable to be used in the rule rates *)
-type counter_test = CEQ of int | CGTE of int | CVAR of string
+type counter_test = CEQ of int | CGTE of int | CLTE of int | CVAR of string
 
 type counter = {
   counter_name: string Loc.annoted;
   counter_test: counter_test Loc.annoted option;
-      (** In a rule: what test is done, in an agent declaration: the initial value *)
+      (** In a rule: what test is done, in an agent declaration: the min value, in an init declaration: the init value, None if absent *)
   counter_delta: int Loc.annoted;
-      (** In a rule: change in counter value, in an agent declaration: max value of the counter *)
+      (** In a rule: change in counter value, in an agent declaration: max value of the counter, 0 if absent *)
 }
+(** Counter syntax from AST, present in 3 contexts with different meanings: agent definition, species init declaration, rule *)
 
 type site = Port of port | Counter of counter
 type agent_mod = NoMod | Erase | Create
@@ -46,6 +45,7 @@ type agent =
   | Present of string Loc.annoted * site list * agent_mod
   | Absent of Loc.t
 
+(* TODO: document why list list *)
 type mixture = agent list list
 
 type edit_notation = {
@@ -249,6 +249,7 @@ let print_ast_port f p =
 let print_counter_test f = function
   | CEQ x, _ -> Format.fprintf f "=%i" x
   | CGTE x, _ -> Format.fprintf f ">=%i" x
+  | CLTE x, _ -> Format.fprintf f "<=%i" x
   | CVAR x, _ -> Format.fprintf f "=%s" x
 
 let print_counter_delta test f (delta, _) =
@@ -284,6 +285,7 @@ let string_option_annoted_of_json filenames =
 let counter_test_to_json = function
   | CEQ x -> `Assoc [ "test", `String "eq"; "val", `Int x ]
   | CGTE x -> `Assoc [ "test", `String "gte"; "val", `Int x ]
+  | CLTE x -> `Assoc [ "test", `String "lte"; "val", `Int x ]
   | CVAR x -> `Assoc [ "test", `String "eq"; "val", `String x ]
 
 let counter_test_of_json = function
@@ -293,6 +295,9 @@ let counter_test_of_json = function
   | `Assoc [ ("val", `Int x); ("test", `String "gte") ]
   | `Assoc [ ("test", `String "gte"); ("val", `Int x) ] ->
     CGTE x
+  | `Assoc [ ("val", `Int x); ("test", `String "gle") ]
+  | `Assoc [ ("test", `String "gle"); ("val", `Int x) ] ->
+    CLTE x
   | `Assoc [ ("test", `String "eq"); ("val", `String x) ]
   | `Assoc [ ("val", `String x); ("test", `String "eq") ] ->
     CVAR x

core/grammar/ast.mli

@@ -22,7 +22,12 @@ type port = {
 }
 (** Describe a port from an agent. [_int] references the internal state of the port, [_link], the possible links that can be made to this port, [_mod] to the changes in a rule that would be made to the state, used only in edit_notation  *)
 
-type counter_test = CEQ of int | CGTE of int | CVAR of string
+(** What test is done by the counter expression
+ * - CEQ: If counter value is equal to the specified value
+ * - CGTE: If counter value is greater or equal to the specified value
+ * - CLTE: If counter value is less or equal to the specified value
+ * - CVAR: Not a test, but defines a variable to be used in the rule rates *)
+type counter_test = CEQ of int | CGTE of int | CLTE of int | CVAR of string
 
 type counter = {
   counter_name: string Loc.annoted;

core/grammar/counters_compiler.ml

@@ -218,7 +218,8 @@ let split_cvar_counter_in_rules_per_value (var_name : string) (annot : Loc.t)
   let max_value : int = Loc.v counter_def.counter_delta in
   let min_value : int =
     match counter_def.counter_test with
-    | None | Some (Ast.CGTE _, _) | Some (Ast.CVAR _, _) ->
+    | None | Some (Ast.CGTE _, _) | Some (Ast.CLTE _, _) | Some (Ast.CVAR _, _)
+      ->
       raise
         (ExceptionDefn.Malformed_Decl
            ( "Invalid counter signature - have to specify min bound",
@@ -275,6 +276,8 @@ let split_counter_variables_into_separate_rules ~warning rules signatures =
             (ExceptionDefn.Malformed_Decl
                ( "Counter " ^ Loc.v c.counter_name ^ " becomes negative",
                  Loc.get_annot c.counter_name ))
+      | Some (Ast.CLTE _value, _annot) ->
+        failwith "not implemented" (* TODO NOW *)
       | Some (Ast.CGTE value, annot) ->
         if value + delta < 0 then
           raise
@@ -591,7 +594,7 @@ let rec erase_incr (sigs : Signature.s) (i : int) (incrs : LKappa.rule_mixture)
     )
   | [] -> []
 
-(** Returns mixtures for agnet with site changed from counter to port, as well as new [link_nb] after previous additions
+(** Returns mixtures for agent with site changed from counter to port, as well as new [link_nb] after previous additions
  * Used by [compile_counter_in_rule_agent]*)
 let counter_becomes_port (sigs : Signature.s) (ra : LKappa.rule_agent)
     (p_id : int) (counter : Ast.counter) (start_link_nb : int) :
@@ -628,6 +631,7 @@ let counter_becomes_port (sigs : Signature.s) (ra : LKappa.rule_agent)
              Loc.get_annot counter_test ))
     | Ast.CEQ j -> j, true
     | Ast.CGTE j -> j, false
+    | Ast.CLTE _j -> failwith "not implemented" (* TODO now *)
   in
   let start_link_for_created : int = start_link_nb + test + 1 in
   let link_for_erased : int = start_link_nb + abs delta in
@@ -720,7 +724,7 @@ let compile_counter_in_raw_agent (sigs : Signature.s)
             agent_name c.Ast.counter_name
         | Some (test, _) ->
           (match test with
-          | Ast.CGTE _ | Ast.CVAR _ ->
+          | Ast.CGTE _ | Ast.CLTE _ | Ast.CVAR _ ->
             let agent_name =
               Format.asprintf "@[%a@]"
                 (Signature.print_agent sigs)

core/grammar/kappaParser.mly

@@ -448,6 +448,7 @@ interface_expression:
 counter_test:
    | TYPE INT { Some (Ast.CEQ $2,rhs_pos 2)}
    | TYPE GREATER INT { Some (Ast.CGTE $3,rhs_pos 3)}
+   | TYPE SMALLER INT { Some (Ast.CLTE $3,rhs_pos 3)}
    | TYPE ID { Some (Ast.CVAR $2,rhs_pos 2)}
 
 port_expression:

core/grammar/kparser4.mly

@@ -129,6 +129,7 @@ counter_modif:
 counter_test:
   | EQUAL annoted INT { (Ast.CEQ $3,rhs_pos 3) }
   | GREATER annoted EQUAL annoted INT { (Ast.CGTE $5,rhs_pos 5) }
+  | SMALLER annoted EQUAL annoted INT { (Ast.CLTE $5,rhs_pos 5) }
   | EQUAL annoted ID { (Ast.CVAR $3,rhs_pos 3) }
   ;