Slow pattern matching elaboration

[ErrWare]

Description of the problem

Rocq takes 17-35 seconds to accept the Nify_fn definition below, and 8 seconds to accept the same definition minus one match case. First reported on a zulip thread), the workaround was to use an equality decision procedure instead of a match. Pierre-Marie Pédrot profiled the example and suggests there is "algorithmic slowdown due to unification constraints [from] a huge list of Evd.unification_pb".

Require Import NArith ZArith.
Open Scope N.
From MetaRocq.Template Require Export All Checker Reduction.
Export MonadNotation.
From MetaRocq.Utils Require Export bytestring.
Export String.
Open Scope bs.
Open Scope list.

Definition zxbits z i j := ((Z.shiftr z i) mod (Z.shiftl 1%Z (Z.max 0 (j - i))))%Z.
Definition xbits n i j :=  (N.shiftr n i) mod (N.shiftl 1 (j - i)).

Notation "'_zxbits_'" := (tConst (MPfile ["mvp"; "Project"], "zxbits") []).
Notation "'_xbits_'" := (tConst (MPfile ["mvp"; "Project"], "xbits") []).
Notation "'_Z.of_N_'" := (tConst (MPdot (MPfile ["IntDef"; "BinNums"; "Corelib"]) "Z", "of_N") []).
Notation "'_N.eqb_'" := (tConst (MPdot (MPfile ["BinNatDef"; "NArith"; "Stdlib"]) "N", "eqb") []).
Notation "'_Z.eqb_'" := (tConst (MPdot (MPfile ["IntDef"; "BinNums"; "Corelib"]) "Z", "eqb") []).

Fixpoint monadmap {A B:Type} (f:A->TemplateMonad B) (l:list A) : TemplateMonad (list B) :=
  match l with
  | h::t => fh <- f h;; ft <- monadmap f t;; tmReturn (fh::ft)
  | nil => tmReturn nil
  end.

(* Takes 17s in mvp, 35s in project. *)
Time Definition Nify_fn (Nify:term -> TemplateMonad term) (fn:term) (ts:list term): TemplateMonad term :=
  Nts <- monadmap Nify ts ;;
  match fn with
  | _zxbits_ => tmReturn (tApp _xbits_ Nts)
  | _Z.of_N_ => match ts with h::nil => Nify h | _ => tmFail "Z.of_N had more than one argument." end
  | _Z.eqb_ => tmReturn (tApp _N.eqb_ Nts)
  | _ => tmReturn (tApp fn Nts)
  end.

(* Takes 8s in mvp and project. *)
Time Definition Nify_fn' (Nify:term -> TemplateMonad term) (fn:term) (ts:list term): TemplateMonad term :=
  Nts <- monadmap Nify ts ;;
  match fn with
  (* removed zxbits case *)
  | _Z.of_N_ => match ts with h::nil => Nify h | _ => tmFail "Z.of_N had more than one argument." end
  | _Z.eqb_ => tmReturn (tApp _N.eqb_ Nts)
  | _ => tmReturn (tApp fn Nts)
  end.

Version of Rocq / Coq where this bug occurs

9.1.1

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response

[SkySkimmer]

reduced

Declare Scope bs_scope.

Module BS.
  Inductive t : Set :=
  | EmptyString
  | String (_ : Byte.byte) (_ : t).
  Bind Scope bs_scope with t.

  Fixpoint print (b : t) : list Byte.byte :=
    match b with
    | EmptyString => nil
    | String b bs => b :: print bs
    end.

  Fixpoint parse (b : list Byte.byte) : t :=
    match b with
    | nil => EmptyString
    | cons b bs => String b (parse bs)
    end.
End BS.
String Notation BS.t BS.parse BS.print : bs_scope.

Open Scope bs_scope.

Set Universe Polymorphism.
Cumulative Inductive Monad : Type -> Type :=
| ret : forall {A}, A -> Monad A
| bind : forall {A B}, Monad A -> (A -> Monad B) -> Monad B.

Time Definition bli x :=
  bind (ret tt) (fun _ =>
    match x with
    | "mvp.Project.zxbits" => ret 1
    | "IntDef.BinNums.Corelib.Z.of_N" => ret 2
    | "IntDef.BinNums.Corelib.Z.eqb" => ret 3
    | _ => ret 4
    end).
(* 10s *)

[SkySkimmer]

This isn't a kernel problem BTW

[ppedrot]

@SkySkimmer your reduced problem does not exhibit the same profile. Half of time of the original issue was passed in evar manipulation in unification constraints, which are lacking from your example.

[ppedrot]

Slightly minimized but still depending on a bit of metarocq.

From MetaRocq.Utils Require Export bytestring.
Export String.
Open Scope bs.

(*
Weirdly enough, with only the Require below Nify_fn is basically instantaneous.

From Stdlib Require Import String.
Open Scope string_scope.
*)

Definition ident := string.

Definition dirpath := list ident.

Inductive modpath : Set :=
| MPfile : dirpath -> modpath
| MPdot : modpath -> ident -> modpath.

Definition kername := prod modpath ident.

Axiom level : Set.

Definition instance := list level.

Inductive term : Type :=
| tRel : term
| tApp : term -> list term -> term
| tConst : kername -> instance -> term.

Notation "'_zxbits_'" := (tConst (MPfile (cons "mvp" (cons "Project" nil)), "zxbits") nil).
Notation "'_xbits_'" := (tConst (MPfile (cons "mvp" (cons "Project" nil)), "xbits") nil).
Notation "'_Z.of_N_'" := (tConst (MPdot (MPfile (cons "IntDef" (cons "BinNums" (cons "CoreLib" nil)))) "Z", "of_N") nil).
Notation "'_N.eqb_'" := (tConst (MPdot (MPfile (cons "BinNatDef" (cons "NArith" (cons "Stdlib" nil)))) "N", "eqb") nil).
Notation "'_Z.eqb_'" := (tConst (MPdot (MPfile (cons "IntDef" (cons "BinNums" (cons "CoreLib" nil)))) "Z", "eqb") nil).

#[universes(polymorphic)]
Inductive TemplateMonad@{t u} : Type@{t} -> Prop :=
| tmReturn : forall (A : Type@{t}), A -> TemplateMonad A
| tmBind : forall (A B : Type@{t}), TemplateMonad A -> (A -> TemplateMonad B) -> TemplateMonad B
| tmFail : forall (A : Type@{t}), string -> TemplateMonad A.

Arguments tmReturn {A}.
Arguments tmBind {A B}.
Arguments tmFail {A}.

#[universes(polymorphic)]
Class Monad@{d c} (m : forall _ : Type@{d}, Type@{c}) : Type@{max(d+1,c)} := Build_Monad
  { ret : forall (t : Type@{d}) (_ : t), m t;
    bind : forall (t u : Type@{d}) (_ : m t) (_ : forall _ : t, m u), m u }.

Arguments ret {m Monad t}.
Arguments bind {m Monad t u}.

#[universes(polymorphic)]
Instance TemplateMonad_Monad@{t u} : Monad@{t u} TemplateMonad :=
{| ret := @tmReturn@{t u}; bind := @tmBind@{t u} |}
     : Monad@{t u} TemplateMonad@{t u}.

Fixpoint monadmap {A B:Type} (f:A->TemplateMonad B) (l:list A) : TemplateMonad (list B) :=
  match l with
  | cons h t =>
    bind (f h) (fun fh : B => bind (monadmap f t) (fun ft : list B => tmReturn (cons fh ft)))
  | nil => tmReturn nil
  end.

(* Takes 17s in mvp, 35s in project. *)
Time Definition Nify_fn (Nify:term -> TemplateMonad term) (fn:term) (ts:list term): TemplateMonad term :=
  bind (monadmap Nify ts) (fun Nts =>
  match fn with
  | _zxbits_ => tmReturn (tApp _xbits_ Nts)
  | _Z.of_N_ => match ts with cons h nil => Nify h | _ => tmFail "Z.of_N had more than one argument." end
  | _Z.eqb_ => tmReturn (tApp _N.eqb_ Nts)
  | _ => tmReturn (tApp fn Nts)
  end).

[Janno]

Without dependencies:

Set Implicit Arguments.
Notation cons := cons (only parsing).
Delimit Scope bs_scope with bs.

Module Export String.
  Inductive t : Set :=
  | EmptyString
  | String (_ : Byte.byte) (_ : t).
Fixpoint print (b : t) : list Byte.byte.
Admitted.
Fixpoint parse (b : list Byte.byte) : t.
exact (match b with
    | nil => EmptyString
    | cons b bs => String b (parse bs)
    end).
Defined.
Notation string := String.t.

String Notation String.t String.parse String.print : bs_scope.
Open Scope bs.

Definition ident := string.

Definition dirpath := list ident.

Inductive modpath : Set :=
| MPfile : dirpath -> modpath
| MPdot : modpath -> ident -> modpath.

Definition kername := prod modpath ident.

Axiom level : Set.

Definition instance := list level.

Inductive term : Type :=
| tRel : term
| tApp : term -> list term -> term
| tConst : kername -> instance -> term.

Notation "'_zxbits_'" := (tConst (MPfile (cons "mvp" (cons "Project" nil)), "zxbits") nil).
Notation "'_xbits_'" := (tConst (MPfile (cons "mvp" (cons "Project" nil)), "xbits") nil).
Notation "'_Z.of_N_'" := (tConst (MPdot (MPfile (cons "IntDef" (cons "BinNums" (cons "CoreLib" nil)))) "Z", "of_N") nil).
Notation "'_N.eqb_'" := (tConst (MPdot (MPfile (cons "BinNatDef" (cons "NArith" (cons "Stdlib" nil)))) "N", "eqb") nil).
Notation "'_Z.eqb_'" := (tConst (MPdot (MPfile (cons "IntDef" (cons "BinNums" (cons "CoreLib" nil)))) "Z", "eqb") nil).

Inductive TemplateMonad : Type -> Prop :=
| tmReturn : forall (A : Type), A -> TemplateMonad A
| tmBind : forall (A B : Type), TemplateMonad A -> (A -> TemplateMonad B) -> TemplateMonad B
| tmFail : forall (A : Type), string -> TemplateMonad A.

Class Monad (m : forall _ : Type, Type) : Type := Build_Monad
  { ret : forall (t : Type) (_ : t), m t;
    bind : forall (t u : Type) (_ : m t) (_ : forall _ : t, m u), m u }.
Arguments bind {m Monad t u}.
Instance TemplateMonad_Monad : Monad TemplateMonad.
exact ({| ret := @tmReturn; bind := @tmBind |}
     : Monad TemplateMonad).
Defined.

Fixpoint monadmap {A B:Type} (f:A->TemplateMonad B) (l:list A) : TemplateMonad (list B) :=
  match l with
  | cons h t =>
    bind (f h) (fun fh : B => bind (monadmap f t) (fun ft : list B => tmReturn (cons fh ft)))
  | nil => tmReturn nil
  end.

Timeout 5 Definition Nify_fn (Nify:term -> TemplateMonad term) (fn:term) (ts:list term): TemplateMonad term :=
  bind (monadmap Nify ts) (fun Nts =>
  match fn with
  | _zxbits_ => tmReturn (tApp _xbits_ Nts)
  | _Z.of_N_ => match ts with cons h nil => Nify h | _ => tmFail "Z.of_N had more than one argument." end
  | _Z.eqb_ => tmReturn (tApp _N.eqb_ Nts)
  | _ => tmReturn (tApp fn Nts)
  end).

[ppedrot]

What's the difference between custom strings and the ones from the stdlib? They look the same to me...

[SkySkimmer]

Metarocq uses byte list, stdlib uses (bool * bool * ... * bool) list