Adalog: remove comparers

The symbolic solver does not handle comparers, so it makes no sense to
keep them in Langkit.

TN: SB20-024

Author: pmderodat

langkit/compile_context.py

@@ -665,11 +665,6 @@ def __init__(self,
         Set of properties used as converters in logic equations.
         """
 
-        self.logic_comparer_props: Set[PropertyDef] = set()
-        """
-        Set of properties used as comparers in logic equations.
-        """
-
         self.default_unit_provider = default_unit_provider
         self.case_insensitive = case_insensitive
         self.symbol_canonicalizer = symbol_canonicalizer
@@ -977,11 +972,6 @@ def sorted_logic_converters(self):
         return sorted(self.logic_converter_props,
                       key=lambda x: x.name.camel)
 
-    @property
-    def sorted_logic_comparers(self):
-        return sorted(self.logic_comparer_props,
-                      key=lambda x: x.name.camel)
-
     def sorted_types(self, type_set):
         """
         Turn "type_set" into a list of types sorted by name.
@@ -1005,21 +995,17 @@ def sorted_exception_types(self) -> List[GeneratedException]:
         return sorted(self.exception_types.values(),
                       key=lambda e: e.doc_entity)
 
-    def do_generate_logic_functors(self, convert_property=None,
-                                   eq_property=None):
+    def do_generate_logic_functors(self, convert_property=None):
         """
         Generate a logic binder with the given conversion property.
 
         If you call this function several times for the same property, only one
         binder will be generaed.
 
         :param PropertyDef convert_property: The conversion property.
-        :param PropertyDef eq_property: The equality property.
         """
         if convert_property:
             self.logic_converter_props.add(convert_property)
-        if eq_property:
-            self.logic_comparer_props.add(eq_property)
 
     @staticmethod
     def grammar_rule_api_name(rule):

langkit/dsl_unparse.py

@@ -1221,7 +1221,6 @@ def handle_designated_env_macro():
     elif isinstance(expr, Bind):
         return "%eq({})".format(", ".join(keep([
             ee(expr.from_expr), ee(expr.to_expr),
-            "eq_prop={}".format(fqn(expr.eq_prop)) if expr.eq_prop else ""
             "conv_prop={}".format(fqn(expr.conv_prop)) if expr.conv_prop else ""
         ])))
 

langkit/expressions/logic.py

@@ -43,12 +43,6 @@ class Bind(AbstractExpression):
     return any ``ASTNode`` subclass. It is used to convert `from_expr` into a
     value to which `to_expr` is compared.
 
-    If provided, `eq_prop` must be a property that takes one ``ASTNode``
-    subclass argument and that compares it to ``Self``. In this case, the
-    argument must be of the same type that the node that owns the property. It
-    is used to compare the two logic variables (after `conv_prop` call, if
-    applicable).
-
     For instance, in order to express the following logical equation::
 
         B = A.some_property()
@@ -61,12 +55,10 @@ class Bind(AbstractExpression):
     class Expr(CallExpr):
         def __init__(self,
                      conv_prop: PropertyDef,
-                     eq_prop: PropertyDef,
                      lhs: ResolvedExpression,
                      rhs: ResolvedExpression,
                      abstract_expr: Optional[AbstractExpression] = None):
             self.conv_prop = conv_prop
-            self.eq_prop = eq_prop
             self.lhs = lhs
             self.rhs = rhs
 
@@ -81,19 +73,14 @@ def __init__(self,
                     ("Cache_Value", LiteralExpr("<>", None)),
                 ))
 
-            if eq_prop:
-                constructor_args.append(self.functor_expr(
-                    eq_prop, f"Eq => Comparer_{self.eq_prop.uid}"
-                ))
-
             if abstract_expr:
                 constructor_args.append(
                     f"Debug_String => {sloc_info_arg(abstract_expr.location)}"
                 )
 
             if rhs.type.matches(T.root_node.entity):
                 fn_name = 'Solver.Create_Assign'
-            elif conv_prop or eq_prop:
+            elif conv_prop:
                 fn_name = 'Solver.Create_Propagate'
             else:
                 fn_name = 'Solver.Create_Unify'
@@ -129,14 +116,13 @@ def functor_expr(prop: PropertyDef,
         @property
         def subexprs(self):
             return {'conv_prop': self.conv_prop,
-                    'eq_prop':   self.eq_prop,
                     'lhs':       self.lhs,
                     'rhs':       self.rhs}
 
         def __repr__(self):
             return '<Bind.Expr>'
 
-    def __init__(self, from_expr, to_expr, conv_prop=None, eq_prop=None):
+    def __init__(self, from_expr, to_expr, conv_prop=None):
         """
         :param AbstractExpression from_expr: An expression resolving to a
             logical variable that is the source of the bind.
@@ -147,20 +133,11 @@ def __init__(self, from_expr, to_expr, conv_prop=None, eq_prop=None):
             For convenience, it can be a property on any subclass of the root
             AST node class, and can return any subclass of the root AST node
             class.
-        :param PropertyDef|None eq_prop: The property to use to test for
-            equality between the value of the two expressions. For convenience,
-            it can be a property on a subclass of the root AST node class,
-            however:
-
-            1. It needs to take exactly two parameters, the self parameter and
-               another parameter.
-            2. The two parameters must be of exactly the same type.
         """
         super().__init__()
         self.from_expr = from_expr
         self.to_expr = to_expr
         self.conv_prop = conv_prop
-        self.eq_prop = eq_prop
 
     def resolve_props(self):
         from langkit.expressions import FieldAccess
@@ -181,10 +158,6 @@ def resolve(name, prop):
 
             return prop
 
-        self.eq_prop = resolve('eq_prop', self.eq_prop)
-        if self.eq_prop:
-            self.eq_prop.root_property
-
         self.conv_prop = resolve('conv_prop', self.conv_prop)
         if self.conv_prop:
             self.conv_prop = self.conv_prop.root_property
@@ -193,7 +166,7 @@ def construct(self):
         from langkit.compile_context import get_context
         self.resolve_props()
 
-        get_context().do_generate_logic_functors(self.conv_prop, self.eq_prop)
+        get_context().do_generate_logic_functors(self.conv_prop)
 
         # We have to wait for the construct pass for the following checks
         # because they rely on type information, which is not supposed to be
@@ -209,45 +182,14 @@ def construct(self):
                  'Bind property must belong to a subtype of {}'.format(
                      T.root_node.dsl_name
                 )),
-            ])
 
-            DynamicVariable.check_call_bindings(
-                self.conv_prop, "In Bind's conv_prop {prop}"
-            )
-
-        # Those checks are run in construct, because we need the eq_prop to be
-        # prepared already, which is not certain in do_prepare (order
-        # dependent).
-
-        if self.eq_prop:
-            args = self.eq_prop.natural_arguments
-            check_multiple([
-                (self.eq_prop.type == T.Bool,
-                 'Equality property must return boolean'),
-
-                (self.eq_prop.struct.matches(T.root_node),
-                 'Equality property must belong to a subtype of {}'.format(
-                     T.root_node.dsl_name
-                )),
-
-                (len(args) == 1,
-                 'Equality property: expected 1 argument, got {}'.format(
-                     len(args)
-                )),
+                (all(arg.default_value is not None
+                     for arg in self.conv_prop.natural_arguments),
+                 'Bind property can take only optional arguments'),
             ])
 
-            other_type = args[0].type
-            check_source_language(
-                other_type.is_entity_type,
-                "First arg of equality property should be an entity type"
-            )
-            check_source_language(
-                other_type.element_type == self.eq_prop.struct,
-                "Self and first argument should be of the same type"
-            )
-
             DynamicVariable.check_call_bindings(
-                self.eq_prop, "In Bind's eq_prop {prop}"
+                self.conv_prop, "In Bind's conv_prop {prop}"
             )
 
         # Left operand must be a logic variable. Make sure the resulting
@@ -282,8 +224,7 @@ def construct(self):
             from langkit.expressions import Cast
             rhs = Cast.Expr(rhs, T.root_node.entity)
 
-        return Bind.Expr(self.conv_prop, self.eq_prop,
-                         lhs, rhs, abstract_expr=self)
+        return Bind.Expr(self.conv_prop, lhs, rhs, abstract_expr=self)
 
 
 class DomainExpr(ComputingExpr):

langkit/templates/astnode_types_ada.mako

@@ -5,8 +5,8 @@
 
 
 <%def name="logic_helpers()">
-   ## Generate predicate, converter and comparer functors, which wrap
-   ## properties to be used in logic equations.
+   ## Generate predicate and converter functors, which wrap properties to be
+   ## used in logic equations.
    ##
    ## Note that we need to generate them before the properties bodies, because
    ## they'll be used in the bodies.
@@ -18,9 +18,6 @@
    % for conv_prop in ctx.sorted_logic_converters:
       ${prop_helpers.logic_converter(conv_prop)}
    % endfor
-   % for eq_prop in ctx.sorted_logic_comparers:
-      ${prop_helpers.logic_equal(eq_prop)}
-   % endfor
 </%def>
 
 

langkit/templates/parsers/pkg_main_body_ada.mako

@@ -92,8 +92,7 @@ package body ${ada_lib_name}.Parsers is
 
    type Dontskip_Parser_Function is access function
      (Parser : in out Parser_Type;
-      Pos    : Token_Index)
-      return ${ctx.root_grammar_class.storage_type_name};
+      Pos    : Token_Index) return ${ctx.root_grammar_class.storage_type_name};
 
    package Dont_Skip_Fn_Vectors
    is new Ada.Containers.Vectors (Natural, Dontskip_Parser_Function);

langkit/templates/properties/helpers.mako

@@ -96,72 +96,6 @@
    end Image;
 </%def>
 
-<%def name="logic_equal(eq_prop)">
-   <%
-      struct = eq_prop.struct
-      type_name = 'Comparer_{}'.format(eq_prop.uid)
-   %>
-
-   ${dynamic_vars_holder_decl(
-         type_name, "Solver_Ifc.Comparer_Type", eq_prop.dynamic_vars
-     )}
-
-   overriding function Image (Self : ${type_name}) return String;
-   overriding function Compare
-     (Self : ${type_name}; L, R : ${T.entity.name}) return Boolean;
-
-   -----------
-   -- Image --
-   -----------
-
-   overriding function Image (Self : ${type_name}) return String is
-   begin
-      return ("${eq_prop.qualname}");
-   end Image;
-
-   -------------
-   -- Compare --
-   -------------
-
-   overriding function Compare
-     (Self : ${type_name}; L, R : ${T.entity.name}) return Boolean
-   is
-     % if not eq_prop.dynamic_vars:
-        pragma Unreferenced (Self);
-     % endif
-   begin
-      --  If any node pointer is null, then use that for equality
-      if L.Node = null or else R.Node = null then
-         return L.Node = R.Node;
-      end if;
-
-      --  Check that both arguments have appropriate types for the property
-      --  call.
-      if L.Node.Kind not in ${struct.ada_kind_range_name} then
-         raise Property_Error with
-            "Wrong type for ${eq_prop.qualname}'s ""self"" argument";
-      elsif R.Node.Kind not in ${struct.ada_kind_range_name} then
-         raise Property_Error with
-            "Wrong type for ${eq_prop.qualname}'s"
-            & " ""${eq_prop.natural_arguments[0].dsl_name}"" argument";
-      end if;
-
-      --  All is good: do the call
-      declare
-         R_Entity : constant ${struct.entity.name} := (R.Node, R.Info);
-      begin
-         return ${eq_prop.name}
-          (${eq_prop.self_arg_name}             => L.Node,
-           ${eq_prop.natural_arguments[0].name} => R_Entity,
-           % for dynvar in eq_prop.dynamic_vars:
-              ${dynvar.argument_name} => Self.${dynvar.argument_name},
-           % endfor
-           ${eq_prop.entity_info_name}          => L.Info);
-       end;
-   end Compare;
-
-</%def>
-
 <%def name="logic_predicates(prop)">
    % for (args_types, default_passed_args, pred_id) in prop.logic_predicates:
 

support/langkit_support-adalog-generic_main_support.adb

@@ -274,15 +274,7 @@ package body Langkit_Support.Adalog.Generic_Main_Support is
    procedure Run_Main (Main : access procedure) is
    begin
       Setup_Traces;
-
-      begin
-         Main.all;
-      exception
-         when Exc : Unsupported_Error =>
-            Put_Line
-              (Exception_Name (Exc) & ": " & Exception_Message (Exc));
-      end;
-
+      Main.all;
       Finalize;
    end Run_Main;
 

support/langkit_support-adalog-generic_main_support.ads

@@ -78,10 +78,9 @@ package Langkit_Support.Adalog.Generic_Main_Support is
    function Propagate
      (L, R       : Refs.Logic_Var;
       Conv       : Converter_Type'Class := No_Converter;
-      Eq         : Comparer_Type'Class := No_Comparer;
       Dbg_String : String := "") return Relation
    is
-     (+Create_Propagate (L, R, Conv, Eq, -Dbg_String));
+     (+Create_Propagate (L, R, Conv, -Dbg_String));
 
    function Unify
      (L, R : Refs.Logic_Var; Dbg_String : String := "") return Relation
@@ -91,10 +90,9 @@ package Langkit_Support.Adalog.Generic_Main_Support is
      (L          : Refs.Logic_Var;
       R          : T;
       Conv       : Converter_Type'Class := No_Converter;
-      Eq         : Comparer_Type'Class := No_Comparer;
       Dbg_String : String := "") return Relation
    is
-     (+Create_Assign (L, R, Conv, Eq, -Dbg_String));
+     (+Create_Assign (L, R, Conv, -Dbg_String));
 
    function Predicate
      (L          : Refs.Logic_Var;

support/langkit_support-adalog-solver.adb

@@ -1650,16 +1650,10 @@ package body Langkit_Support.Adalog.Solver is
      (Logic_Var    : Logic_Vars.Logic_Var;
       Value        : Value_Type;
       Conv         : Converter_Type'Class := No_Converter;
-      Eq           : Comparer_Type'Class := No_Comparer;
       Debug_String : String_Access := null) return Relation
    is
       Conv_Ptr : Converter_Access := null;
    begin
-      if not Is_No_Comparer (Eq) then
-         raise Unsupported_Error with
-           "Comparer_Type not supported with the symbolic solver";
-      end if;
-
       if not Is_No_Converter (Conv) then
          Conv_Ptr := new Converter_Type'Class'(Conv);
       end if;
@@ -1711,16 +1705,10 @@ package body Langkit_Support.Adalog.Solver is
    function Create_Propagate
      (From, To     : Logic_Var;
       Conv         : Converter_Type'Class := No_Converter;
-      Eq           : Comparer_Type'Class := No_Comparer;
       Debug_String : String_Access := null) return Relation
    is
       Conv_Ptr : Converter_Access := null;
    begin
-      if not Is_No_Comparer (Eq) then
-         raise Unsupported_Error with
-           "Comparer_Type not supported with the symbolic solver";
-      end if;
-
       if not Is_No_Converter (Conv) then
          Conv_Ptr := new Converter_Type'Class'(Conv);
       end if;