[injector] Unfold rules at the recursive end of the rule

src/injector/call_graph.ml

@@ -10,7 +10,9 @@ let get_dependencies (rule : Rule.t) : StringSet.t =
     | Terminal _ | Range _ -> acc
     | Star atom | Plus atom | Opt atom -> atom_deps acc atom
     | Group body ->
-      List.fold_left (fun acc case -> List.fold_left atom_deps acc case) acc body
+      List.fold_left
+        (fun acc case -> List.fold_left atom_deps acc case)
+        acc body
   in
   List.fold_left
     (fun acc case -> List.fold_left atom_deps acc case)
@@ -24,17 +26,19 @@ let build (rules : Rule.t list) : t =
 let dependencies name cg =
   StringMap.find_opt name cg |> Option.value ~default:StringSet.empty
 
-let recursive_nonterminals cg =
-  let nodes = StringMap.bindings cg |> List.map fst in
-  let rec can_reach start target visited =
+let can_reach cg start target =
+  let rec loop start target visited =
     if StringSet.mem start visited then false
     else
       let deps = dependencies start cg in
       if StringSet.mem target deps then true
       else
         StringSet.exists
-          (fun next -> can_reach next target (StringSet.add start visited))
+          (fun next -> loop next target (StringSet.add start visited))
           deps
   in
-  List.filter (fun node -> can_reach node node StringSet.empty) nodes
-  |> StringSet.of_list
+  loop start target StringSet.empty
+
+let recursive_nonterminals cg =
+  let nodes = StringMap.bindings cg |> List.map fst in
+  List.filter (fun node -> can_reach cg node node) nodes |> StringSet.of_list

src/injector/transform.ml

@@ -5,39 +5,57 @@ let unfold (rules : Rule.t list) (k : int) : Rule.t list =
   let cg = Call_graph.build rules in
   let recursive = Call_graph.recursive_nonterminals cg in
 
-  let make_name name i = Printf.sprintf "%s_%d" name i in
-
-  let rec is_recursive_atom = function
-    | Non_terminal id -> StringSet.mem id recursive
-    | Terminal _ | Range _ -> false
-    | Star atom | Plus atom -> is_recursive_atom atom
-    | Group body -> List.exists is_recursive_case body
+  (* Create an ordering of non-terminals to break cycles exactly once *)
+  let order =
+    List.mapi (fun i (r : Rule.t) -> (r.name, i)) rules
+    |> List.to_seq |> StringMap.of_seq
+  in
+  let get_order name =
+    StringMap.find_opt name order |> Option.value ~default:0
+  in
 
-  and is_recursive_case case = List.exists is_recursive_atom case in
+  let make_name name i = Printf.sprintf "%s_%d" name i in
 
-  let rec transform_atom i atom =
+  let rec transform_atom current_name i atom =
     match atom with
-    | Terminal _ | Range _ -> atom
-    | Star atom -> Star (transform_atom i atom)
-    | Plus atom -> Plus (transform_atom i atom)
-    | Group body -> Group (List.map (transform_case i) body)
+    | Terminal _ | Range _ -> Some atom
+    | Star atom ->
+      Option.map (fun a -> Star a) (transform_atom current_name i atom)
+    | Plus atom ->
+      Option.map (fun a -> Plus a) (transform_atom current_name i atom)
+    | Opt atom ->
+      Option.map (fun a -> Opt a) (transform_atom current_name i atom)
+    | Group body ->
+      let new_body = List.filter_map (transform_case current_name i) body in
+      if List.is_empty new_body then None else Some (Group new_body)
     | Non_terminal id ->
-      if StringSet.mem id recursive then Non_terminal (make_name id i)
-      else Non_terminal id
-
-  and transform_case i case = List.map (transform_atom i) case in
+      if StringSet.mem id recursive then
+        let next_i =
+          if
+            Call_graph.can_reach cg id current_name
+            && get_order id <= get_order current_name
+          then i - 1
+          else i
+        in
+        if next_i < 0 then None else Some (Non_terminal (make_name id next_i))
+      else Some (Non_terminal id)
+  and transform_case current_name i case =
+    let rec loop acc = function
+      | [] -> Some (List.rev acc)
+      | hd :: tl -> (
+        match transform_atom current_name i hd with
+        | None -> None
+        | Some a -> loop (a :: acc) tl )
+    in
+    loop [] case
+  in
 
   let build_new_rules rule =
     let rec loop acc i =
       if i < 0 then acc
       else
         let new_name = make_name rule.name i in
-        let new_body =
-          if i = 0 then
-            (* Filter out cases that contain recursive calls *)
-            List.filter (fun case -> not (is_recursive_case case)) rule.body
-          else List.map (transform_case (i - 1)) rule.body
-        in
+        let new_body = List.filter_map (transform_case rule.name i) rule.body in
         let new_rule = { name = new_name; body = new_body } in
         loop (new_rule :: acc) (i - 1)
     in
@@ -49,10 +67,10 @@ let unfold (rules : Rule.t list) (k : int) : Rule.t list =
       (fun acc rule ->
         if StringSet.mem rule.name recursive then build_new_rules rule @ acc
         else
-          (* Not recursive one might call recursive ones *)
-          let new_rule =
-            { name = rule.name; body = List.map (transform_case k) rule.body }
+          let new_body =
+            List.filter_map (transform_case rule.name k) rule.body
           in
+          let new_rule = { name = rule.name; body = new_body } in
           new_rule :: acc )
       [] rules
   in

test/injector/complete/test_basic.t

@@ -9,10 +9,10 @@ Basic completion:
   <B> ::= <A> "b" | "d";
   Unfolding level:
   Unfolded grammar (k = 3):
-  <A_3> ::= <B_2> "a" | "c";
-  <A_2> ::= <B_1> "a" | "c";
-  <A_1> ::= <B_0> "a" | "c";
-  <A_0> ::= "c";
+  <A_3> ::= <B_3> "a" | "c";
+  <A_2> ::= <B_2> "a" | "c";
+  <A_1> ::= <B_1> "a" | "c";
+  <A_0> ::= <B_0> "a" | "c";
   <B_3> ::= <A_2> "b" | "d";
   <B_2> ::= <A_1> "b" | "d";
   <B_1> ::= <A_0> "b" | "d";
@@ -22,8 +22,16 @@ Basic completion:
   SMT Expr: (str.in_re x
              (regexp.union
               (regexp.++
-               (regexp.union (regexp.++ (str.to_re "c") (str.to_re "b"))
+               (regexp.union
+                (regexp.++
+                 (regexp.union
+                  (regexp.++
+                   (regexp.union
+                    (regexp.++
+                     (regexp.union (regexp.++ (str.to_re "d") (str.to_re "a"))
+                      (str.to_re "c")) (str.to_re "b")) (str.to_re "d"))
+                   (str.to_re "a")) (str.to_re "c")) (str.to_re "b"))
                 (str.to_re "d")) (str.to_re "a")) (str.to_re "c")))
   Satisfying model:
   (model
-    (x str "cba"))
+    (x str "daba"))

test/injector/unit/test_features.ml

@@ -1,6 +1,7 @@
 open Injector
 
-let test_grammar_features = {|
+let test_grammar_features =
+  {|
 <Range> ::= [a-z] [A-Z] [0-9];
 <Star> ::= "a"* <Range>*;
 <Plus> ::= "b"+ [0-9]+;

test/injector/verify/test_basic.t

@@ -9,10 +9,10 @@ Basic verification:
   <B> ::= <A> "b" | "d";
   Unfolding level:
   Unfolded grammar (k = 3):
-  <A_3> ::= <B_2> "a" | "c";
-  <A_2> ::= <B_1> "a" | "c";
-  <A_1> ::= <B_0> "a" | "c";
-  <A_0> ::= "c";
+  <A_3> ::= <B_3> "a" | "c";
+  <A_2> ::= <B_2> "a" | "c";
+  <A_1> ::= <B_1> "a" | "c";
+  <A_0> ::= <B_0> "a" | "c";
   <B_3> ::= <A_2> "b" | "d";
   <B_2> ::= <A_1> "b" | "d";
   <B_1> ::= <A_0> "b" | "d";
@@ -22,6 +22,14 @@ Basic verification:
   SMT Expr: (str.in_re "cba"
              (regexp.union
               (regexp.++
-               (regexp.union (regexp.++ (str.to_re "c") (str.to_re "b"))
+               (regexp.union
+                (regexp.++
+                 (regexp.union
+                  (regexp.++
+                   (regexp.union
+                    (regexp.++
+                     (regexp.union (regexp.++ (str.to_re "d") (str.to_re "a"))
+                      (str.to_re "c")) (str.to_re "b")) (str.to_re "d"))
+                   (str.to_re "a")) (str.to_re "c")) (str.to_re "b"))
                 (str.to_re "d")) (str.to_re "a")) (str.to_re "c")))
   Candiate 'cba' is a valid sentence of A_2