Merge pull request herd#1703 from herd/aslspec-importing-rules

Importing inference rules from LaTeX to aslspec

Author: Roman-Manevich

asllib/StaticOperations.ml

@@ -141,6 +141,11 @@ let filter_reduce_constraint_div =
         | _ -> None)
     | _ -> None
   in
+  let make_constraint_range_opt z1 z2 =
+    if Z.equal z1 z2 then Some (exact (expr_of_z z1))
+    else if Z.leq z1 z2 then Some (range (expr_of_z z1) (expr_of_z z2))
+    else None
+  in
   function
   | Constraint_Exact e as c -> (
       match get_literal_div_opt e with
@@ -167,9 +172,7 @@ let filter_reduce_constraint_div =
               Format.eprintf "Reducing %a DIV %a@ got z1=%a and z2=%a@."
                 PP.pp_expr e1 PP.pp_expr e2 Z.pp_print z1 Z.pp_print z2
           in
-          if Z.equal z1 z2 then Some (exact (expr_of_z z1))
-          else if Z.leq z1 z2 then Some (range (expr_of_z z1) (expr_of_z z2))
-          else None
+          make_constraint_range_opt z1 z2
       | Some z1, None -> Some (range (expr_of_z z1) e2)
       | None, Some z2 -> Some (range e1 (expr_of_z z2))
       | None, None -> Some c)

asllib/aslspec/AST.ml

@@ -40,6 +40,7 @@ module AttributeKey = struct
     | Custom
         (** Whether an operator over a list of arguments should be rendered by a
             custom multi-argument macro. *)
+    | Typecast  (** Whether an operator serves only to perform a typecast. *)
     | Short_Circuit_Macro
         (** A LaTeX macro name to succinctly denote any value of a type [T].
             This is used to denote the short-circuit result of a relation
@@ -60,6 +61,7 @@ module AttributeKey = struct
       | LHS_Hypertargets -> 5
       | Associative -> 6
       | Custom -> 7
+      | Typecast -> 8
     in
     let a_int = key_to_int a in
     let b_int = key_to_int b in
@@ -76,6 +78,7 @@ module AttributeKey = struct
     | LHS_Hypertargets -> "lhs_hypertargets"
     | Associative -> "associative"
     | Custom -> "custom"
+    | Typecast -> "typecast"
 end
 
 (** A value associated with an attribute key. *)
@@ -582,6 +585,10 @@ module Relation : sig
   (** [is_custom_operator t] tests whether the operator represented by [t] has
       the [custom] attributes set to [true]. *)
 
+  val is_typecast_operator : t -> bool
+  (** [is_typecast_operator t] tests whether the operator represented by [t] has
+      the [typecast] attributes set to [true]. *)
+
   val math_layout : t -> layout option
   (** The layout used when rendered as a stand-alone relation definition. *)
 end = struct
@@ -655,6 +662,9 @@ end = struct
 
   let is_custom_operator self =
     Attributes.get_bool AttributeKey.Custom ~default:false self.att
+
+  let is_typecast_operator self =
+    Attributes.get_bool AttributeKey.Typecast ~default:false self.att
 end
 
 (** A datatype for grouping (subsets of) type definitions. *)

asllib/aslspec/SpecLexer.mll

@@ -63,6 +63,7 @@ rule token = parse
     | "semantics"           { SEMANTICS }
     | "short_circuit_macro" { SHORT_CIRCUIT_MACRO }
     | "then"                { THEN }
+    | "typecast"            { TYPECAST }
     | "typedef"             { TYPEDEF }
     | "typing"              { TYPING }
     | "variadic"            { VARIADIC }

asllib/aslspec/SpecParser.mly

@@ -59,6 +59,7 @@ let bool_of_string s =
 %token RULE
 %token SEMANTICS
 %token SHORT_CIRCUIT_MACRO
+%token TYPECAST
 %token TYPEDEF
 %token TYPING
 %token VARIADIC
@@ -294,6 +295,7 @@ let operator_attribute :=
 let operator_style_attribute ==
     | ASSOCIATIVE; EQ; value=IDENTIFIER; { (Associative, BoolAttribute (bool_of_string value)) }
     | CUSTOM; EQ; value=IDENTIFIER; { (Custom, BoolAttribute (bool_of_string value)) }
+    | TYPECAST; EQ; value=IDENTIFIER; { (Typecast, BoolAttribute (bool_of_string value)) }
 
 let prose_application_attribute ==
     PROSE_APPLICATION; EQ; template=STRING; { (Prose_Application, StringAttribute template) }

asllib/aslspec/builtins.spec

@@ -1,3 +1,20 @@
+operator cond_case[T](Bool, T) -> T
+{
+  math_macro = \condcase,
+  custom = true,
+};
+
+// TODO: add a custom rendering where all conditions
+// and all values are properly aligned.
+// Perhaps this can be achieved by adding a raw attribute to macros, which doesn't wrap them with braces.
+// TODO: add custom syntac for cases.
+variadic operator cond_op[T](list1(T)) -> T
+{
+  math_macro = \condop,
+  custom = true,
+};
+
+// This constant is for internal use only.
 constant bot { "bottom", math_macro = \bot };
 
 constant None { "the empty \optionalterm{}" };
@@ -34,6 +51,18 @@ typedef Z
     math_macro = \Z,
 };
 
+operator is_integer(q: Q) -> Bool
+{
+  "{q} is an integer",
+  math_macro = \isintegerop,
+};
+
+operator is_not_integer(q: Q) -> Bool
+{
+  "{q} is not an integer",
+  math_macro = \isnotintegerop,
+};
+
 typedef Q
 { "rational",
    math_macro = \Q,
@@ -56,7 +85,7 @@ operator assign[T](lhs: T, rhs: T) -> Bool
 
 operator reverse_assign[T](lhs: T, rhs: T) -> Bool
 {
-  math_macro = \eqname,
+  math_macro = \reverseeqdef,
 };
 
 operator equal[T](a: T, b: T) -> (c: Bool)
@@ -75,21 +104,6 @@ operator if_then_else[T](Bool, T, T) -> T
   math_macro = \ifthenelseop,
 };
 
-// TODO: add a custom rendering where all conditions
-// and all values are properly aligned.
-// Perhaps this can be achieved by adding a "raw" attribute to macros, which doesn't wrap them with braces.
-// TODO: add custom syntax for cases.
-variadic operator cond_op[T](list1(T)) -> T
-{
-  math_macro = \condop,
-  custom = true,
-};
-operator cond_case[T](Bool, T) -> T
-{
-  math_macro = \condcase,
-  custom = true,
-};
-
 variadic operator and(list1(Bool)) -> Bool
 {
   associative = true,
@@ -102,21 +116,28 @@ variadic operator or(list1(Bool)) -> Bool
   math_macro = \lor,
 };
 
-operator list_and(list1(Bool)) -> Bool
+operator list_and(list0(Bool)) -> Bool
 {
-  math_macro = \land,
+  math_macro = \listand,
 };
 
-operator list_or(list1(Bool)) -> Bool
+operator list_or(list0(Bool)) -> Bool
 {
-  math_macro = \lor,
+  math_macro = \listor,
 };
 
 operator not(Bool) -> Bool
 {
   math_macro = \opnot,
 };
 
+// This is negation, specialized to a single variable to allow
+// the macro to drop the parenthesis around the variable.
+operator not_single(Bool) -> Bool
+{
+  math_macro = \opnotvar,
+};
+
 operator iff(Bool, Bool) -> Bool
 {
   math_macro = \IFF,
@@ -138,6 +159,11 @@ operator num_minus[NumType](NumType, NumType) -> NumType
   math_macro = \numminus,
 };
 
+operator num_negate[NumType](NumType) -> NumType
+{
+  math_macro = \numnegate,
+};
+
 // Negation for number types.
 operator negate[NumType](NumType) -> NumType
 {
@@ -147,6 +173,7 @@ operator negate[NumType](NumType) -> NumType
 variadic operator num_times[NumType](list1(NumType)) -> NumType
 {
   math_macro = \numtimes,
+  associative = true,
 };
 
 operator num_divide[NumType](NumType, NumType) -> NumType
@@ -157,6 +184,7 @@ operator num_divide[NumType](NumType, NumType) -> NumType
 operator num_exponent[NumType](NumType, NumType) -> NumType
 {
   math_macro = \numexponent,
+  custom = true,
 };
 
 operator less_than[NumType](NumType, NumType) -> Bool

asllib/aslspec/render.ml

@@ -516,7 +516,7 @@ module Make (S : SPEC_VALUE) = struct
       let op_macro = get_or_gen_math_macro op_name in
       let layout =
         if Spec.is_cond_operator_name S.spec op_name then
-          (* Special case for the match_cases operator, which is always vertical. *)
+          (* Special case for the 'cond' operator, which is always vertical. *)
           vertical_if_unspecified layout args
         else horizontal_if_unspecified layout args
       in
@@ -623,7 +623,7 @@ module Make (S : SPEC_VALUE) = struct
         pp_case_name_opt name_opt
         (pp_print_list
          (* The quadruple backslash means the next premise definitely starts on a new line. *)
-           ~pp_sep:(fun fmt () -> fprintf fmt {|\hva\\\\@.|})
+           ~pp_sep:(fun fmt () -> fprintf fmt {|\hva\\@.|})
            pp_premise)
         premises pp_conclusion conclusion
 

asllib/aslspec/spec.ml

@@ -1840,6 +1840,17 @@ module Check = struct
         use_def_mode * Term.t list ->
         context_expr:Expr.t ->
         Term.t list * Term.t
+      (** [instantiate_operator_types_from_inferred_types spec relation_name
+           num_actual_args (mode, inferred_types) ~context_expr] instantiates
+          the types of the arguments and output of the operator [relation_name]
+          given the number of actual arguments [num_actual_args] and the
+          [inferred_types] for either its arguments or its output depending on
+          [mode]. The [context_expr] is used for error reporting. When mode is
+          [Use], the [inferred_types] correspond to the argument types. When
+          mode is [Def], the [inferred_types] correspond to the output type. By
+          instantiating we mean substituting type parameters in the operator
+          definition with concrete types inferred for a given operator
+          invocation expression. *)
     end = struct
       (** [unify_parameter_type spec ~relation_name parameter_name
            parameter_type type_env] attempts to unify [parameter_type] with any
@@ -2076,17 +2087,6 @@ module Check = struct
           in
           (instantiated_arg_types, instantiated_output_type)
 
-      (** [instantiate_operator_types_from_inferred_types spec relation_name
-           num_actual_args (mode, inferred_types) ~context_expr] instantiates
-          the types of the arguments and output of the operator [relation_name]
-          given the number of actual arguments [num_actual_args] and the
-          [inferred_types] for either its arguments or its output depending on
-          [mode]. The [context_expr] is used for error reporting. When mode is
-          [Use], the [inferred_types] correspond to the argument types. When
-          mode is [Def], the [inferred_types] correspond to the output type. By
-          instantiating we mean substituting type parameters in the operator
-          definition with concrete types inferred for a given operator
-          invocation expression. *)
       let instantiate_operator_types_from_inferred_types spec relation_name
           num_actual_args (mode, inferred_types) ~context_expr =
         let formal_arg_types =
@@ -2509,7 +2509,7 @@ module Check = struct
                and return the function's output type. *)
             let lhs_type, type_env = infer_type_in_env spec type_env lhs in
             let from_term, to_term =
-              match lhs_type with
+              match CheckTypeInstantiations.reduce_term spec lhs_type with
               | Function { from_type = _, from_term; to_type = _, to_term } ->
                   (from_term, to_term)
               | _ -> Error.invalid_map_lhs_type lhs_type ~context_expr:expr
@@ -3111,25 +3111,34 @@ module ExtendNames = struct
   open Expr
   open Rule
 
-  (** [opt_extend] Wraps [expr] with a name if [opt_name] is [Some]. Avoids
-      naming a variable expression with its own name, as an optimization. *)
-  let opt_extend expr opt_name =
-    match (expr, opt_name) with
+  (** [opt_extend] Wraps [expr] with a name if [opt_param_name] is [Some].
+      Avoids naming a variable expression with its own name. *)
+  let opt_extend spec expr opt_param_name =
+    match (expr, opt_param_name) with
     | _, None -> expr
     | Var v, Some name when String.equal v name ->
         expr (* Avoid naming a variable with its own name. *)
+    | ( Expr.Relation
+          { name = operator_name; is_operator = true; args = [ Var v ] },
+        Some name ) ->
+        let relation = relation_for_id spec operator_name in
+        if Relation.is_typecast_operator relation && String.equal v name then
+          (* Typecasts render the input variable. If the input variable has the same name
+             as the parameter, avoid naming it. *)
+          expr
+        else NamedExpr (expr, name)
     | _, Some name -> NamedExpr (expr, name)
 
   (** [extend_with_names type_term expr ] recursively transforms [expr] by
       adding names from [type_term] to sub-expressions of [expr]. Currently,
       only tuples (labelled or unlabelled) are supported, which is sufficient
       for most output configurations. *)
-  let rec extend_with_names type_term expr =
+  let rec extend_with_names spec type_term expr =
     match (type_term, expr) with
     | Term.Tuple { label_opt = None; args = [ (opt_name, _) ] }, _ ->
         (* An unlabelled tuple with a single component serves as a named reference
            to any type.*)
-        opt_extend expr opt_name
+        opt_extend spec expr opt_name
     | ( Term.Tuple { label_opt = term_label_opt; args = term_components },
         Expr.Tuple { label_opt = expr_label_opt; args = expr_components } )
       when Option.equal String.equal term_label_opt expr_label_opt ->
@@ -3147,7 +3156,7 @@ module ExtendNames = struct
         let extended_args =
           List.map2
             (fun (opt_name, arg_type) arg ->
-              opt_extend (extend_with_names arg_type arg) opt_name)
+              opt_extend spec (extend_with_names spec arg_type arg) opt_name)
             term_components expr_components
         in
         Expr.Tuple { label_opt = expr_label_opt; args = extended_args }
@@ -3167,7 +3176,7 @@ module ExtendNames = struct
               (* Fallback to the main output type. *)
               List.hd output_types
         in
-        let extended_rhs = extend_with_names output_type rhs in
+        let extended_rhs = extend_with_names spec output_type rhs in
         let extended_expr =
           Transition { lhs; rhs = extended_rhs; short_circuit }
         in

asllib/aslspec/tests.t/operators.expected

@@ -41,7 +41,7 @@ The relation
 } % EndDefineRelation
 
 \DefineRule{f}{\begin{mathpar}
-\inferrule{ { { { \texttt{a}\intplus\texttt{b} } \equal \texttt{c} } } \\\\
+\inferrule{ { { { \texttt{a}\intplus\texttt{b} } \equal \texttt{c} } } \hva\\
  { { \texttt{d} \eqdef { \ifthenelseop[H]{{ \texttt{a} \member \texttt{S} }}{\texttt{b}}{\texttt{c}} } } } }{
  { \f(\texttt{a}, \texttt{b}, \texttt{c}, \texttt{S}) \typearrow \texttt{d} } 
 }

asllib/aslspec/tests.t/rule.expected

@@ -61,8 +61,8 @@ The relation
                                               { \condcase[H]{{ \texttt{a} \equal \texttt{b} }}{\texttt{a}} }, \\
                                               { \condcase[H]{{ \texttt{a} \greaterthan \texttt{b} }}{{ \texttt{a}\numplus\texttt{b} }} }, \\
                                               { \condcase[H]{{ \texttt{a} \lessthan \texttt{b} }}{\texttt{b}} }
-                                              \end{array}} } } } \\\\
- { { \texttt{r\_f} \eqdef { \texttt{r}.\FIELDf\numplus\texttt{r}.\FIELDg } } } \\\\
+                                              \end{array}} } } } \hva\\
+ { { \texttt{r\_f} \eqdef { \texttt{r}.\FIELDf\numplus\texttt{r}.\FIELDg } } } \hva\\
  { { \texttt{r'} \eqdef \texttt{r}\left\{\begin{array}{lcl}
                                          \FIELDf & : & \texttt{res}
                                          \end{array}\right\} } } }{

asllib/aslspec/tests.t/run.t

@@ -7,18 +7,8 @@
   Generated LaTeX macros into generated_macros.tex
   $ aslspec rule.spec --render; diff -w generated_macros.tex rule.expected; rm -f generated_macros.tex
   Generated LaTeX macros into generated_macros.tex
-  64,65c64,65
-  <                                               \end{array}} } } } \hva\\\\
-  <  { { \texttt{r\_f} \eqdef { \texttt{r}.\FIELDf\numplus\texttt{r}.\FIELDg } } } \hva\\\\
-  ---
-  >                                               \end{array}} } } } \\\\
-  >  { { \texttt{r\_f} \eqdef { \texttt{r}.\FIELDf\numplus\texttt{r}.\FIELDg } } } \\\\
   $ aslspec operators.spec --render; diff -w generated_macros.tex operators.expected; rm -f generated_macros.tex
   Generated LaTeX macros into generated_macros.tex
-  44c44
-  < \inferrule{ { { { \texttt{a}\intplus\texttt{b} } \equal \texttt{c} } } \hva\\\\
-  ---
-  > \inferrule{ { { { \texttt{a}\intplus\texttt{b} } \equal \texttt{c} } } \\\\
 
   $ aslspec type_name.bad
   Syntax Error: illegal element-defining identifier: t2 around type_name.bad line 1 column 41