Get list of constructors of Inductive

[samuelgruetter]

Is it possible to write the following function in Ltac2 in a generic way, without having to write one line for each type?

Ltac2 constructors_of_type t :=
  match! t with
  | prod _ _ => [ constr:(@pair) ]
  | Z => [ constr:(Z0); constr:(Zpos); constr:(Zneg) ]
  | nat => [ constr:(O); constr:(S) ]
  | _ => Control.throw (Tactic_failure None)
  end.

[JasonGross]

I tried this, but it does not work because of #10094:

Require Import Ltac2.Ltac2.

Module Import Ltac2.
  Module List.
    Ltac2 rec map (f : 'a -> 'b) (ls : 'a list) :=
      match ls with
      | [] => []
      | l :: ls => f l :: map f ls
      end.
    Ltac2 rec fold_right (f : 'a -> 'b -> 'b) (a : 'b) (ls : 'a list) :=
      match ls with
      | [] => a
      | l :: ls => f l (fold_right f a ls)
      end.
  End List.
End Ltac2.

Ltac2 rec head v :=
  match! v with
  | ?f ?x => head f
  | ?x => x
  end.

Ltac2 rec get_constructors_from (i : int) (ind : inductive) :=
  Control.plus
    (fun () => let c := Constr.Unsafe.constructor ind i in
               c :: get_constructors_from (Int.add i 1) ind)
    (fun e
     => match e with
        | Not_found => []
        | _ => Control.throw e
        end).

Ltac2 constructors_of_type t :=
  let t := head t in
  match Constr.Unsafe.kind t with
  | Constr.Unsafe.Ind ind inst
    => let ls := get_constructors_from 0 ind in
         List.map (fun c => Constr.Unsafe.make (Constr.Unsafe.Constructor c inst)) ls
  | _ => Control.throw (Tactic_failure (Some (Message.of_constr t)))
  end.

[JasonGross]

Here is a thing that works. Due to #10090, I decided to use Ltac1's tactics in terms rather than inserting an extra call to hnf. This is very kludgy, and @ppedrot should probably include a primitive that does this, or at least a primitive to count the number of constructors of an inductive. Anyway, here's the code:

Require Import Ltac2.Ltac2.

Module Import Ltac2.
  Module List.
    Ltac2 rec iter (f : 'a -> unit) (ls : 'a list) :=
      match ls with
      | [] => ()
      | l :: ls => f l; iter f ls
      end.
    Ltac2 rec map (f : 'a -> 'b) (ls : 'a list) :=
      match ls with
      | [] => []
      | l :: ls => f l :: map f ls
      end.
    Ltac2 rec fold_right (f : 'a -> 'b -> 'b) (a : 'b) (ls : 'a list) :=
      match ls with
      | [] => a
      | l :: ls => f l (fold_right f a ls)
      end.
    Ltac2 rec seq (start : int) (step : int) (last : int) :=
      match Int.equal (Int.compare (Int.sub last start) step) -1 with
      | true
        => []
      | false
        => start :: seq (Int.add start step) step last
      end.
  End List.
End Ltac2.

Ltac2 get_n_constructors (n : int) (ind : inductive) :=
  List.map (Constr.Unsafe.constructor ind) (List.seq 0 1 n).

Ltac2 count_constructors (ty : constr) :=
  let c := '(fun n : $ty => ltac:(lazymatch goal with n : _ |- _ => destruct n end; exact tt)) in
  match Constr.Unsafe.kind c with
  | Constr.Unsafe.Lambda _ _ c
    => match Constr.Unsafe.kind c with
       | Constr.Unsafe.Case _ _ _ cases
         => Array.length cases
       | _ => Control.throw (Tactic_failure (Some (Message.of_constr c)))
       end
  | _ => Control.throw (Tactic_failure (Some (Message.of_constr c)))
  end.

Ltac2 rec head v :=
  match! v with
  | ?f ?x => head f
  | ?x => x
  end.

Ltac2 constructors_of_type ty :=
  let t := head ty in
  match Constr.Unsafe.kind t with
  | Constr.Unsafe.Ind ind inst
    => let n := count_constructors ty in
       let ls := get_n_constructors n ind in
       List.map (fun c => Constr.Unsafe.make (Constr.Unsafe.Constructor c inst)) ls
  | _ => Control.throw (Tactic_failure (Some (Message.of_constr t)))
  end.

Goal True.
  let ls := List.map constructors_of_type [
                       '(prod nat nat);
                       'nat;
                       '(sum nat nat)
                     ] in
  List.iter (fun v => Message.print (List.fold_right Message.concat (Message.of_string "") (List.map (fun m => Message.concat (Message.of_constr m) (Message.of_string "; ")) v))) ls.
  (* @pair;
0; S;
@inl; @inr;
 *)

[JasonGross]

See also #10940