Adalog: add a N_Predicate atomc relation kind

TN: SB20-024
For libadalang/langkit#618

Author: pmderodat

support/langkit_support-adalog-generic_main_support.ads

@@ -82,6 +82,13 @@ package Langkit_Support.Adalog.Generic_Main_Support is
    is
      (+Create_Propagate (L, R, Conv, -Dbg_String));
 
+   function N_Propagate
+     (To   : Refs.Logic_Var;
+      Comb : Combiner_Type'Class;
+      Vars : Logic_Var_Array;
+      Dbg_String : String := "") return Relation
+   is (+Create_N_Propagate (To, Comb, Vars, -Dbg_String));
+
    function Unify
      (L, R : Refs.Logic_Var; Dbg_String : String := "") return Relation
    is (+Create_Unify (L, R, -Dbg_String));

support/langkit_support-adalog-solver.adb

@@ -753,6 +753,7 @@ package body Langkit_Support.Adalog.Solver is
                   when Assign | True | False => True,
 
                   when Propagate   => Append_Definition (Atom.From),
+                  when N_Propagate => Append_Definitions (Atom.Comb_Vars),
                   when Predicate   => Append_Definition (Atom.Target),
                   when N_Predicate => Append_Definitions (Atom.Vars),
 
@@ -972,10 +973,15 @@ package body Langkit_Support.Adalog.Solver is
    is
       --  We handle Unify here, even though it is not strictly treated in the
       --  dependency graph, so that the Unify_From variable is registered in
-      --  the list of variables of the equation. TODO??? Might be cleaner to
-      --  have a separate function to return all variables a relation uses?
+      --  the list of variables of the equation.
+      --
+      --  We also pretend that N_Propagate has no dependency here because it
+      --  depends on multiple variables. Callers should handle it separately.
+      --
+      --  TODO??? Might be cleaner to have a separate function to return all
+      --  variables a relation uses?
      (case Self.Kind is
-         when Assign | True | False | N_Predicate => null,
+         when Assign | N_Propagate | True | False | N_Predicate => null,
          when Propagate => Self.From,
          when Predicate => Self.Target,
          when Unify     => Self.Unify_From);
@@ -991,8 +997,8 @@ package body Langkit_Support.Adalog.Solver is
       --  the list of variables of the equation. TODO??? Might be cleaner to
       --  have a separate function to return all variables a relation defines?
      (case Self.Kind is
-         when Assign | Propagate | Unify             => Self.Target,
-         when Predicate | True | False | N_Predicate => null);
+         when Assign | Propagate | N_Propagate | Unify => Self.Target,
+         when Predicate | True | False | N_Predicate   => null);
 
    -----------------
    -- To_Relation --
@@ -1683,6 +1689,27 @@ package body Langkit_Support.Adalog.Solver is
                           Debug_String => Debug_String);
    end Create_Propagate;
 
+   ------------------------
+   -- Create_N_Propagate --
+   ------------------------
+
+   function Create_N_Propagate
+     (To           : Logic_Var;
+      Comb         : Combiner_Type'Class;
+      Logic_Vars   : Logic_Var_Array;
+      Debug_String : String_Access := null) return Relation
+   is
+      Vars_Vec : Logic_Var_Vector := Logic_Var_Vectors.Empty_Vector;
+   begin
+      Vars_Vec.Concat (Logic_Var_Vectors.Elements_Array (Logic_Vars));
+      return To_Relation
+        (Atomic_Relation_Type'(Kind      => N_Propagate,
+                               Comb_Vars => Vars_Vec,
+                               Comb      => new Combiner_Type'Class'(Comb),
+                               Target    => To),
+         Debug_String => Debug_String);
+   end Create_N_Propagate;
+
    ----------------------
    -- Create_Propagate --
    ----------------------
@@ -1803,6 +1830,10 @@ package body Langkit_Support.Adalog.Solver is
             end if;
             Free (Self.Conv);
 
+         when N_Propagate =>
+            Destroy (Self.Comb.all);
+            Free (Self.Comb);
+
          when Predicate =>
             Destroy (Self.Pred.all);
             Free (Self.Pred);
@@ -1852,6 +1883,14 @@ package body Langkit_Support.Adalog.Solver is
    function Solve_Atomic (Self : Atomic_Relation) return Boolean is
       Atom : Atomic_Relation_Type renames Self.Atomic_Rel;
 
+      function Converted_Val (Val : Value_Type) return Value_Type
+      is
+        (if Atom.Conv /= null
+         then Atom.Conv.Convert_Wrapper (Val)
+         else Val);
+      --  Assuming ``Atom`` is an Assign or Propagate atom, return ``Val``
+      --  transformed by its converter.
+
       function Assign_Val (Val : Value_Type) return Boolean;
       --  Tries to assign ``Val`` to ``Atom.Target`` and return True either if
       --  ``Atom.Target`` already has a value compatible with ``Val``, or if
@@ -1860,33 +1899,56 @@ package body Langkit_Support.Adalog.Solver is
       --  This assumes that ``Self`` is either an ``Assign`` or a `Propagate``
       --  relation.
 
+      procedure Get_Values (Vars : Logic_Var_Vector; Vals : out Value_Array);
+      --  Assign to ``Vals`` the value of the variables in ``Vars``.
+      --
+      --  This assumes that ``Vars`` and ``Vals`` have the same bounds. Note
+      --  that we could turn this into a function that returns the array, but
+      --  this would require secondary stack support and its overhead, whereas
+      --  this is performance critical code.
+
       ----------------
       -- Assign_Val --
       ----------------
 
       function Assign_Val (Val : Value_Type) return Boolean is
-         Conv_Val : constant Value_Type :=
-           (if Atom.Conv /= null
-            then Atom.Conv.Convert_Wrapper (Val)
-            else Val);
       begin
          if Is_Defined (Atom.Target) then
-            return Conv_Val = Get_Value (Atom.Target);
+            return Val = Get_Value (Atom.Target);
          else
-            Set_Value (Atom.Target, Conv_Val);
+            Set_Value (Atom.Target, Val);
             return True;
          end if;
       end Assign_Val;
 
+      ----------------
+      -- Get_Values --
+      ----------------
+
+      procedure Get_Values (Vars : Logic_Var_Vector; Vals : out Value_Array) is
+      begin
+         for I in Vals'Range loop
+            Vals (I) := Get_Value (Vars.Get (I));
+         end loop;
+      end Get_Values;
+
       Ret : Boolean;
    begin
       case Atom.Kind is
          when Assign =>
-            Ret := Assign_Val (Atom.Val);
+            Ret := Assign_Val (Converted_Val (Atom.Val));
 
          when Propagate =>
             pragma Assert (Is_Defined (Atom.From));
-            Ret := Assign_Val (Get_Value (Atom.From));
+            Ret := Assign_Val (Converted_Val (Get_Value (Atom.From)));
+
+         when N_Propagate =>
+            declare
+               Vals : Value_Array (1 .. Atom.Comb_Vars.Length);
+            begin
+               Get_Values (Atom.Comb_Vars, Vals);
+               Ret := Assign_Val (Atom.Comb.Combine_Wrapper (Vals));
+            end;
 
          when Predicate =>
             pragma Assert (Is_Defined (Atom.Target));
@@ -1896,10 +1958,7 @@ package body Langkit_Support.Adalog.Solver is
             declare
                Vals : Value_Array (1 .. Atom.Vars.Length);
             begin
-               for I in Atom.Vars.First_Index .. Atom.Vars.Last_Index loop
-                  Vals (I) := Get_Value (Atom.Vars.Get (I));
-               end loop;
-
+               Get_Values (Atom.Vars, Vals);
                Ret := Atom.N_Pred.Call_Wrapper (Vals);
             end;
 
@@ -1931,6 +1990,22 @@ package body Langkit_Support.Adalog.Solver is
       function Prop_Image (Left, Right : String) return String
       is
         (Left & " <- " & Right_Image (Right));
+
+      function Var_Args_Image (Vars : Logic_Var_Vector) return String;
+
+      --------------------
+      -- Var_Args_Image --
+      --------------------
+
+      function Var_Args_Image (Vars : Logic_Var_Vector) return String is
+         Vars_Image : XString_Array (1 .. Vars.Length);
+      begin
+         for I in Vars_Image'Range loop
+            Vars_Image (I) := To_XString (Image (Vars.Get (I)));
+         end loop;
+         return "(" & To_XString (", ").Join (Vars_Image).To_String & ")";
+      end Var_Args_Image;
+
    begin
       case Self.Kind is
          when Propagate =>
@@ -1940,6 +2015,10 @@ package body Langkit_Support.Adalog.Solver is
             return Prop_Image
               (Image (Self.Target), Logic_Vars.Value_Image (Self.Val));
 
+         when N_Propagate =>
+            return Image (Self.Target) & " <- " & Self.Comb.Image
+                   & Var_Args_Image (Self.Comb_Vars);
+
          when Predicate =>
             declare
                Full_Img : constant String :=
@@ -1954,16 +2033,11 @@ package body Langkit_Support.Adalog.Solver is
             declare
                Full_Img : constant String :=
                  Self.N_Pred.Full_Image (Logic_Var_Array (Self.Vars.To_Array));
-               Vars_Image : XString_Array (1 .. Self.Vars.Length);
             begin
-               if Full_Img /= "" then
-                  return Full_Img;
-               end if;
-               for I in Vars_Image'Range loop
-                  Vars_Image (I) := To_XString (Image (Self.Vars.Get (I)));
-               end loop;
-               return Self.N_Pred.Image
-                 & "?(" & To_XString (", ").Join (Vars_Image).To_String & ")";
+               return
+                 (if Full_Img /= ""
+                  then Full_Img
+                  else Self.N_Pred.Image & "?" & Var_Args_Image (Self.Vars));
             end;
 
          when True =>

support/langkit_support-adalog-solver.ads

@@ -140,6 +140,15 @@ package Langkit_Support.Adalog.Solver is
    --  If ``Conv`` is provided, the actually assigned value is the result of
    --  ``Conv`` when called on ``From``'s value.
 
+   function Create_N_Propagate
+     (To           : Logic_Var;
+      Comb         : Combiner_Type'Class;
+      Logic_Vars   : Logic_Var_Array;
+      Debug_String : String_Access := null) return Relation;
+   --  Create a relation that will solve successfully if it is possible to
+   --  assign to ``To`` the value computed by calling ``Comb`` on the given
+   --  ``Logic_Vars``.
+
    function Create_Domain
      (Logic_Var    : Logic_Vars.Logic_Var;
       Domain       : Value_Array;
@@ -182,11 +191,14 @@ package Langkit_Support.Adalog.Solver is
 private
 
    type Converter_Access is access all Converter_Type'Class;
+   type Combiner_Access is access all Combiner_Type'Class;
    type Predicate_Access is access all Predicate_Type'Class;
    type N_Predicate_Access is access all N_Predicate_Type'Class;
 
    procedure Free is new Ada.Unchecked_Deallocation
      (Converter_Type'Class, Converter_Access);
+   procedure Free is new Ada.Unchecked_Deallocation
+     (Combiner_Type'Class, Combiner_Access);
    procedure Free is new Ada.Unchecked_Deallocation
      (Predicate_Type'Class, Predicate_Access);
    procedure Free is new Ada.Unchecked_Deallocation
@@ -200,7 +212,7 @@ private
    -- Atomic_Relation --
    ---------------------
 
-   type Atomic_Kind is (Propagate, Unify, Assign, Predicate,
+   type Atomic_Kind is (Propagate, N_Propagate, Unify, Assign, Predicate,
                         N_Predicate, True, False);
 
    type Atomic_Relation_Type (Kind : Atomic_Kind := Propagate) is record
@@ -228,6 +240,14 @@ private
                when others => null;
             end case;
 
+         when N_Propagate =>
+            Comb_Vars : Logic_Var_Vector;
+            --  List of logic variables used by the converter
+
+            Comb : Combiner_Access;
+            --  Combiner function to assign a value to Target that is computed
+            --  from the value of N_Propagate_Vars.
+
          when Predicate =>
             Pred : Predicate_Access;
             --  The predicate that will be applied as part of this relation

support/langkit_support-adalog-solver_interface.adb

@@ -36,6 +36,7 @@ package body Langkit_Support.Adalog.Solver_Interface is
    type Predicate_Fn is access function (V : Value_Type) return Boolean;
    type Converter_Fn is access function (V : Value_Type) return Value_Type;
    type N_Predicate_Fn is access function (Vs : Value_Array) return Boolean;
+   type Combiner_Fn is access function (Vs : Value_Array) return Value_Type;
 
    type Predicate_Fn_Wrapper is new Predicate_Type with record
       Callback : Predicate_Fn;
@@ -73,6 +74,18 @@ package body Langkit_Support.Adalog.Solver_Interface is
    overriding function Image (Self : Converter_Wrapper) return String
    is (Self.Name.To_String);
 
+   type Combiner_Wrapper is new Combiner_Type with record
+      Callback : Combiner_Fn;
+      Name     : XString;
+   end record;
+
+   overriding function Combine
+     (Self : Combiner_Wrapper; Vs : Value_Array) return Value_Type
+   is (Self.Callback (Vs));
+
+   overriding function Image (Self : Combiner_Wrapper) return String
+   is (Self.Name.To_String);
+
    ------------------
    -- Call_Wrapper --
    ------------------
@@ -120,6 +133,23 @@ package body Langkit_Support.Adalog.Solver_Interface is
       return Self.Cache_Value;
    end Convert_Wrapper;
 
+   ---------------------
+   -- Combine_Wrapper --
+   ---------------------
+
+   function Combine_Wrapper
+     (Self : in out Combiner_Type'Class;
+      Vals : Logic_Vars.Value_Array) return Value_Type
+   is
+   begin
+      if not Self.Cache_Set or else Self.Cache_Key /= Vals then
+         Self.Cache_Value := Self.Combine (Vals);
+         Self.Cache_Set := True;
+         Self.Cache_Key := Vals;
+      end if;
+      return Self.Cache_Value;
+   end Combine_Wrapper;
+
    ---------------
    -- Converter --
    ---------------
@@ -194,4 +224,24 @@ package body Langkit_Support.Adalog.Solver_Interface is
          Name        => To_XString (Pred_Name));
    end N_Predicate;
 
+   --------------
+   -- Combiner --
+   --------------
+
+   function Combiner
+     (Comb      : access function (V : Value_Array) return Value_Type;
+      Arity     : Positive;
+      Comb_Name : String := "Combiner") return Combiner_Type'Class
+   is
+   begin
+      return Combiner_Wrapper'
+        (N           => Arity,
+         Cache_Set   => False,
+         Cache_Key   => <>,
+         Cache_Value => <>,
+         Ref_Count   => 1,
+         Callback    => Comb'Unrestricted_Access.all,
+         Name        => To_XString (Comb_Name));
+   end Combiner;
+
 end Langkit_Support.Adalog.Solver_Interface;