Reimplement conversion modulo AC

.github/workflows/main.yml

@@ -4,6 +4,8 @@ on:
   push:
     paths-ignore:
       - '**/*.md'
+      - '**/*.bnf'
+      - '**/*.rst'
   workflow_dispatch:
 jobs:
   lambdapi:

CHANGES.md

@@ -16,6 +16,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 ### Changed
 
 - Replaced Bindlib by de Bruijn (Frédéric) and closures (Bruno). The performances are slightly better than with Bindlib, especially on rewriting intensive files (the new version is 3.7 times faster on `tests/OK/perf_rw_engine.lp`). Lambdapi is now 2 times faster than dkcheck on matita, and only 2 times slower than dkcheck on holide.
+- Terms are not kept in AC-canonical form any more. This allows to handle AC symbols more efficiently.
+- When declaring a symbol as associative commutative, the side left or right is now mandatory.
+- The ordering used to compare terms now compare arguments from left to right. This may require to permute some arguments for every thing to work again.
 - Several improvements to use the search engine:
   * normalize queries in websearch/search
   * pre-load a file in websearch (e.g. to declare implicit args)

doc/commands.rst

@@ -116,26 +116,36 @@ the system with additional information on its properties and behavior.
 
   - ``constant``: No rule or definition can be given to the symbol
   - ``injective``: The symbol can be considered as injective, that is, if ``f t1 .. tn`` ≡ ``f u1 .. un``, then ``t1``\ ≡\ ``u1``, …, ``tn``\ ≡\ ``un``. For the moment, the verification is left to the user.
-  - ``commutative``: Adds in the conversion the equation ``f t u ≡ f u t``.
-  - ``associative``: Adds in the conversion the equation ``f (f t u) v ≡ f t (f u v)`` (in conjonction with ``commutative`` only).
-
-    For handling commutative and associative-commutative symbols,
-    terms are systemically put in some canonical form following a
-    technique described `here
-    <http://dx.doi.org/10.1007/978-3-540-71316-6_8>`__.
-
-    If a symbol ``f`` is ``commutative`` and not ``associative`` then,
-    for every canonical term of the form ``f t u``, we have ``t ≤ u``,
-    where ``≤`` is a total ordering on terms left unspecified.
-
-    If a symbol ``f`` is ``commutative`` and ``associative left`` then
-    there is no canonical term of the form ``f t (f u v)`` and thus
-    every canonical term headed by ``f`` is of the form ``f … (f (f t₁
-    t₂) t₃) …  tₙ``. If a symbol ``f`` is ``commutative`` and
-    ``associative`` or ``associative right`` then there is no
-    canonical term of the form ``f (f t u) v`` and thus every
-    canonical term headed by ``f`` is of the form ``f t₁ (f t₂ (f t₃ …
-    tₙ) … )``. Moreover, in both cases, we have ``t₁ ≤ t₂ ≤ … ≤ tₙ``.
+
+  - ``commutative``: If a symbol ``f`` is ``commutative`` but not
+    ``associative`` then the reduction relation is enriched with the
+    following conditional rewriting rule:
+
+    * ``f t u ↪ f u t`` if ``t > u``
+
+    where ``≤`` is a total ordering on terms such that:
+    * ``f t₁ t₂ < g u`` iff ``f <ᶠ g``, where ``≤ᶠ`` is a total ordering on function symbols and term constructors left unspecified;
+    * ``f t₁ t₂ < f u₁ u₂`` iff ``t₁ < u₁`` or else ``t₁ = u₁`` and ``t₂ < u₂`` (arguments are compare lexicographically from left to right).
+
+  - ``left associative commutative``: In this case, the reduction
+    relation is enriched with the following conditional rewriting
+    rules:
+
+    * ``f t (f u v) ↪ f (f t u) v``
+    * ``f t u ↪ f u t`` if ``t > u``
+    * ``f (f t u) v ↪ f (f u t) v`` if ``t > u``
+
+  - ``right associative commutative``: In this case, the reduction
+    relation is enriched with the following conditional rewriting
+    rules:
+
+    * ``f (f t u) v ↪ f t (f u v)``
+    * ``f t u ↪ f u t`` if ``t > u``
+    * ``f t (f u v) ↪ f u (f t v)`` if ``t > u``
+
+  This can be used to identify terms modulo the following theories:
+  - ACI = AC + Idempotence: `max-suc algebra <https://github.com/Deducteam/lambdapi/blob/master/tests/OK/max-suc-alg.lp>` in the representation of type universe levels
+  - AG = AC + Inverse + Neutral: `linear arithmetic <https://github.com/Deducteam/lambdapi/blob/master/tests/OK/lia.lp>`
 
 - **Exposition modifiers** define how a symbol can be used outside the
   module where it is defined. By default, the symbol can be used

doc/lambdapi.bnf

@@ -57,7 +57,7 @@ QID ::= [UID "."]+ UID
 <path> ::= UID
          | QID
 
-<modifier> ::= [<side>] "associative"
+<modifier> ::= <side> "associative" "commutative"
              | "commutative"
              | "constant"
              | "injective"

libraries/matita.sh

@@ -74,5 +74,6 @@ fi
 
 # Checking the files.
 cd ${DIR}
+rm -f *.lpo
 \time -f "Finished in %E at %P with %MKb of RAM" \
   lambdapi check --lib-root . --no-warnings -c matita.dk

src/common/logger.ml

@@ -95,7 +95,6 @@ let get_activated_loggers () =
    Without the optional argument, use [!default_loggers] *)
 let reset_loggers ?(default=Stdlib.(! default_loggers)) () =
   let default_value = String.contains default in
-
   let fn { logger_key; logger_enabled; _ } =
     logger_enabled := default_value logger_key
   in
@@ -106,10 +105,17 @@ let reset_loggers ?(default=Stdlib.(! default_loggers)) () =
 let log_summary () =
   List.map (fun d -> (d.logger_key, d.logger_desc)) Stdlib.(!loggers)
 
-(** [set_debug_in b c f x] sets [c] logger to [b] for evaluating [f x]. *)
-let set_debug_in : bool -> char -> ('a -> 'b) -> 'a -> 'b = fun b c f x ->
+(** [set_debug_in c b f] sets [c] logger to [b] for evaluating [f()]. *)
+let set_debug_in : char -> bool -> (unit -> 'a) -> 'a = fun c b f ->
   let is_activated = String.contains (get_activated_loggers()) in
   let v = is_activated c in
   let s = String.make 1 c in
   set_debug b s;
-  try let r = f x in set_debug v s; r with e -> set_debug v s; raise e
+  try let r = f() in set_debug v s; r with e -> set_debug v s; raise e
+
+(** [set_debug_in c b f] sets the loggers in [c] to [b] to evaluate [f()]. *)
+let set_debug_in : string -> bool -> (unit -> 'a) -> 'a = fun s b f ->
+  let default = get_activated_loggers() in
+  set_debug b s;
+  try let r = f() in reset_loggers ~default (); r
+  with e -> reset_loggers ~default (); raise e

src/common/logger.mli

@@ -32,5 +32,5 @@ val reset_loggers : ?default:string -> unit -> unit
 (** [log_summary ()] gives the keys and descriptions for logging options. *)
 val log_summary : unit -> (char * string) list
 
-(** [set_debug_in b c f x] sets [c] logger to [b] for evaluating [f x]. *)
-val set_debug_in : bool -> char -> ('a -> 'b) -> 'a -> 'b
+(** [set_debug_in s b f] sets the loggers in [s] to [b] to evaluate [f()]. *)
+val set_debug_in : string -> bool -> (unit -> 'a) -> 'a

src/core/coercion.ml

@@ -3,16 +3,16 @@ open Term
 
 let coerce : sym =
   let id = Pos.none "coerce" in
-  Sign.add_symbol Ghost.sign Public Defin Eager false id None mk_Kind []
+  Sign.add_symbol Ghost.sign Public Defin Eager false id None Kind []
 
-let apply a b t : term = add_args (mk_Symb coerce) [a; b; t]
+let apply a b t : term = add_args (Symb coerce) [a; b; t]
 
 let _ =
   (* Add the rule [coerce $A $A $t ↪ $t] (but we don't have access to
      the parser here) *)
   let rule =
-    let a = mk_Patt (Some 0, "A", [||])
-    and t = mk_Patt (Some 1, "t", [||]) in
+    let a = Patt (Some 0, "A", [||])
+    and t = Patt (Some 1, "t", [||]) in
     let lhs = [a;a;t] and arities = [|0;0|] and names = [|"A";"t"|] in
     { lhs; names; rhs=t; arity=3; arities; vars_nb=2; xvars_nb = 0;
       rule_pos = None }

src/core/ctxt.ml

@@ -28,8 +28,8 @@ let to_prod : ctxt -> term -> term * int = fun ctx t ->
     let b = bind_var x t in
     let u =
       match d with
-      | None -> mk_Prod (a,b)
-      | Some d -> mk_LLet (a,d,b)
+      | None -> Prod (a,b)
+      | Some d -> LLet (a,d,b)
     in
     u, k+1
   in
@@ -38,14 +38,14 @@ let to_prod : ctxt -> term -> term * int = fun ctx t ->
 (** [to_abst ctx t] builds a sequence of abstractions over the context [ctx],
     in the term [t]. *)
 let to_abst : ctxt -> term -> term = fun ctx t ->
-  let f t (x, a, _) = mk_Abst (a, bind_var x t) in
+  let f t (x, a, _) = Abst (a, bind_var x t) in
   List.fold_left f t ctx
 
 (** [to_let ctx t] adds the defined variables of [ctx] on top of [t]. *)
 let to_let : ctxt -> term -> term = fun ctx t ->
   let f t = function
     | _, _, None -> t
-    | x, a, Some u -> mk_LLet (a, u, bind_var x t)
+    | x, a, Some u -> LLet (a, u, bind_var x t)
   in
   List.fold_left f t ctx
 

src/core/env.ml

@@ -46,8 +46,8 @@ let to_prod : env -> term -> term = fun env t ->
   let add_prod t (_,(x,a,d)) =
     let b = bind_var x t in
     match d with
-    | None -> mk_Prod (a, b)
-    | Some d -> mk_LLet (a, d, b)
+    | None -> Prod (a, b)
+    | Some d -> LLet (a, d, b)
   in
   List.fold_left add_prod t env
 
@@ -60,8 +60,8 @@ let to_abst : env -> term -> term = fun env t ->
   let add_abst t (_,(x,a,d)) =
     let b = bind_var x t in
     match d with
-    | None -> mk_Abst (a, b)
-    | Some d -> mk_LLet (a, d, b)
+    | None -> Abst (a, b)
+    | Some d -> LLet (a, d, b)
   in
   List.fold_left add_abst t env
 
@@ -72,14 +72,14 @@ let vars : env -> var array = fun env ->
 
 (** [appl t env] applies [t] to the variables of [env]. *)
 let appl : term -> env -> term = fun t env ->
-  List.fold_right (fun (_,(x,_,_)) t -> mk_Appl (t, mk_Vari x)) env t
+  List.fold_right (fun (_,(x,_,_)) t -> Appl (t, Vari x)) env t
 
 (** [to_terms env] extracts the array of the variables in [env] and injects
     them in [tbox]. This is the same as [Array.map _Vari (vars env)]. Note
     that the order is reversed: [to_tbox [(xn,an);..;(x1,a1)] =
     [|x1;..;xn|]]. *)
 let to_terms : env -> term array = fun env ->
-  Array.of_list (List.rev_map (fun (_,(x,_,_)) -> mk_Vari x) env)
+  Array.of_list (List.rev_map (fun (_,(x,_,_)) -> Vari x) env)
 
 (** [to_ctxt e] converts an environment into a context. *)
 let to_ctxt : env -> ctxt = List.map snd
@@ -142,5 +142,5 @@ let of_prod_using : ctxt -> var array -> term -> env * term = fun c xs t ->
              let xi = xs.(i) in
              let name = base_name xi in
              let env = add name xi a d env in
-             build_env (i+1) env (subst b (mk_Vari xi)))
+             build_env (i+1) env (subst b (Vari xi)))
   in build_env 0 [] t