Stream: MetaCoq

Topic: ✔ TemplateMonad: get constructors of inductive type


view this post on Zulip Julin S (Jan 07 2022 at 07:54):

I was trying to obtain all the constructors of the following inductive type:

Inductive C :=
| r : C
| g : nat -> C
| b : bool -> nat -> C.

I was able to do something like that with

MetaCoq Quote Recursively Definition qC := C.


Definition default_global_decl :=
  ConstantDecl (Build_constant_body
    (tVar ""%string)
    None
    (Monomorphic_ctx
      (LevelSet.Mkt []%list, ConstraintSet.Mkt []%list))).

Definition default_kername : kername :=
  (MPfile []%list, ""%string).

Definition default_kg : (kername * global_decl) :=
  (default_kername, default_global_decl).


Definition aux (p : program) : list (list (ident * term * nat)) :=
  let genv := fst p in
  let kgd := List.hd default_kg genv in
  let gd := snd kgd in
  let oibs :=
    match gd with
    | ConstantDecl _ => []%list
    | InductiveDecl mib => mib.(ind_bodies)
    end in
  map (fun o:one_inductive_body => o.(ind_ctors)) oibs.

Compute aux qC.
(*
= [[("r", tRel 0, 0);
        ("g",
        tProd nAnon
          (tInd
             {|
             inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "nat");
             inductive_ind := 0 |} []) (tRel 1), 1);
        ("b",
        tProd nAnon
          (tInd
             {|
             inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "bool");
             inductive_ind := 0 |} [])
          (tProd nAnon
             (tInd
                {|
                inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"],
                                  "nat");
                inductive_ind := 0 |} []) (tRel 2)), 2)]]
     : list (list ((ident × term) × nat))
*)

How can something similar be done with TemplateMonad? I tried

Definition aux'2 (qname : qualid) : TemplateMonad unit :=
  x <- tmLocate1 qname ;;
  (*x2 <- tmQuoteInductive x;;*)
  match x with
  | IndRef ind =>
      oibs <- tmQuoteInductive ind.(inductive_mind) ;;
      (* list one_inductive_body *)

      rs <- map (fun o:one_inductive_body => o.(ind_ctors)) oibs ;;
     tmPrint rs
  | _ => tmFail "not an inductive"
  end.

But that didn't work out. Got quite a long error.

view this post on Zulip Julin S (Jan 07 2022 at 07:54):


The error was:

The following term contains unresolved implicit arguments:
  (fun qname : qualid =>
   x <- tmLocate1 qname;;
   match x with
   | VarRef i => tmFail "not an inductive"
   | ConstRef k => tmFail "not an inductive"
   | IndRef ind =>
       oibs <- tmQuoteInductive (inductive_mind ind);;
       rs <- map (fun o : one_inductive_body => ind_ctors o) oibs;;
       tmPrint rs
   | ConstructRef i n => tmFail "not an inductive"
   end)
More precisely:
- ?Monad: Cannot infer this placeholder of type "Monad ?T" (no type class
  instance found) in environment:
  qname : qualid
- ?T: Cannot infer a subterm of type "Type -> Type" in the type of this
  pattern-matching problem in environment:
  qname : qualid
- ?T0: Cannot infer a subterm of type "Type" in the type of this
  pattern-matching problem in environment:
  qname : qualid
- ?A: Cannot infer the implicit parameter A of tmFail whose type is
  "Type" in environment:
  qname : qualid
  x : global_reference
  i : ident
- ?A0: Cannot infer the implicit parameter A of tmFail whose type is
  "Type" in environment:
  qname : qualid
  x : global_reference
  k : kername
- ?Monad0: Cannot infer this placeholder of type "Monad ?m" (no type class
  instance found) in
  environment:
  qname : qualid
  x : global_reference
  ind : inductive
- ?Monad1: Cannot infer this placeholder of type "Monad ?m0" (no type class
  instance found) in
  environment:
  qname : qualid
  x : global_reference
  ind : inductive
  oibs : list one_inductive_body
- ?t: Cannot infer this placeholder of type "Type" in
  environment:
  qname : qualid
  x : global_reference
  ind : inductive
  oibs : list one_inductive_body
- ?A1: Cannot infer the implicit parameter A of tmPrint whose type is
  "Type" in
  environment:
  qname : qualid
  x : global_reference
  ind : inductive
  oibs : list one_inductive_body
- ?m: Cannot infer this placeholder of type "Type -> Type" in
  environment:
  qname : qualid
- ?m0: Cannot infer this placeholder of type "Type -> Type" in
  environment:
  qname : qualid
- ?A2: Cannot infer the implicit parameter A of tmFail whose type is
  "Type" in
  environment:
  qname : qualid
  x : global_reference
  i : inductive
  n : nat

view this post on Zulip Yannick Forster (Jan 07 2022 at 07:57):

Unfortunately, type errors in template programs show up as these big ugly unreadable things. Whenever something like this happens you can read it as "type error" - don't try to read the message

view this post on Zulip Yannick Forster (Jan 07 2022 at 07:58):

I debug them by commenting out chunks of the program and replacing them by tmFail to see where the error is

view this post on Zulip Yannick Forster (Jan 07 2022 at 07:58):

My guess here would be that it is the rs <- map

view this post on Zulip Yannick Forster (Jan 07 2022 at 07:59):

map returns a list, whereas the <- notation strictly expects a monadic value

view this post on Zulip Yannick Forster (Jan 07 2022 at 07:59):

So you need to replace this part by a plain let

view this post on Zulip Paolo Giarrusso (Jan 07 2022 at 08:19):

ah, this is the problem where _all_ implicits are logged if _one_ of them fails to infer? Luckily Matthieu merged a fix for this error reporting in Coq 8.15 to be released soon (https://github.com/coq/coq/pull/13952)

view this post on Zulip Yannick Forster (Jan 07 2022 at 08:56):

Yes, I think it is trying to infer Monad list

view this post on Zulip Yannick Forster (Jan 07 2022 at 08:56):

If this is fixed now I'll move to 8.15 on all projects and never look back

view this post on Zulip Julin S (Jan 07 2022 at 09:09):

Yannick Forster said:

So you need to replace this part by a plain let

Tried using a let, but couldn't get it right.

Definition aux'2 (qname : qualid) : TemplateMonad unit :=
  x <- tmLocate1 qname ;;
  (*x2 <- tmQuoteInductive x;;*)
  match x with
  | IndRef ind =>
      oibs <- tmQuoteInductive ind.(inductive_mind) ;;
      (* list one_inductive_body *)

      let rs := (map (fun o:one_inductive_body => o.(ind_ctors)) oibs) in
      tmPrint rs
  | _ => tmFail "not an inductive"
  end.

Is it wrong? What else could I be missing?

view this post on Zulip Yannick Forster (Jan 07 2022 at 09:10):

Still the same error message?

view this post on Zulip Yannick Forster (Jan 07 2022 at 09:10):

Did you try finding the problem by replacing parts of the program with tmFail "test"?

view this post on Zulip Yannick Forster (Jan 07 2022 at 09:12):

Ah: You're mapping on oibs, but you want to map on oibs.(ind_bodies)

view this post on Zulip Julin S (Jan 07 2022 at 09:39):

Yannick Forster said:

Did you try finding the problem by replacing parts of the program with tmFail "test"?

When we use tmFail to debug, we got to remove the code following it, right?

As in

Definition aux'2_1 (qname : qualid) : TemplateMonad unit :=
  x <- tmLocate1 qname ;;
  (*x2 <- tmQuoteInductive x;;*)
  match x with
  | IndRef ind =>
      oibs <- tmQuoteInductive ind.(inductive_mind) ;;
      (* list one_inductive_body *)

      tmFail "test"
      (* Nothing should come after this, right? *)

      (*
      rs <- map (fun o:one_inductive_body => o.(ind_ctors)) oibs ;;
         tmPrint rs *)
  | _ => tmFail "not an inductive"
  end.

view this post on Zulip Julin S (Jan 07 2022 at 09:39):

Yannick Forster said:

Ah: You're mapping on oibs, but you want to map on oibs.(ind_bodies)

I don't know why I thought what I had named oibs was a list one_inductive_body when it was actually a mutual_inductive_body.. :grimacing:

I modified it to

Definition aux'2 (qname : qualid) : TemplateMonad unit :=
  x <- tmLocate1 qname ;;
  (*x2 <- tmQuoteInductive x;;*)
  match x with
  | IndRef ind =>
      mib <- tmQuoteInductive ind.(inductive_mind) ;;
      (* mib : mutual_inductive_body *)

      (* o.(ind_ctors) : list one_inductive_body *)
      let rs := map (fun o:one_inductive_body => o.(ind_ctors))
                    mib.(ind_bodies) in
      tmPrint rs
      (* rs : list (list ((ident * term) * nat) ) *)

  | _ => tmFail "not an inductive"
  end.

and it got defined without error.

But upon running it, it looks like it's not being evaluated.

view this post on Zulip Julin S (Jan 07 2022 at 09:40):


MetaCoq Run (aux'2 "C").

Output was:

(map (fun o : one_inductive_body => ind_ctors o)
   (ind_bodies
      {|
      ind_finite := Finite;
      ind_npars := 0;
      ind_params := [];
      ind_bodies := [{|
                     ind_name := "C";
                     ind_type := tSort
                                   (Universe.from_kernel_repr
                                      (Level.lSet, false) []);
                     ind_kelim := InType;
                     ind_ctors := [("r", tRel 0, 0);
                                  ("g",
                                  tProd nAnon
                                    (tInd
                                       {|
                                       inductive_mind := (
                                                 MPfile
                                                 ["Datatypes"; "Init"; "Coq"],
                                                 "nat");
                                       inductive_ind := 0 |} [])
                                    (tRel 1), 1);
                                  ("b",
                                  tProd nAnon
                                    (tInd
                                       {|
                                       inductive_mind := (
                                                 MPfile
                                                 ["Datatypes"; "Init"; "Coq"],
                                                 "bool");
                                       inductive_ind := 0 |} [])
                                    (tProd nAnon
                                       (tInd
                                          {|
                                          inductive_mind := (
                                                 MPfile
                                                 ["Datatypes"; "Init"; "Coq"],
                                                 "nat");
                                          inductive_ind := 0 |} [])
                                       (tRel 2)), 2)];
                     ind_projs := [] |}];
      ind_universes := Monomorphic_ctx
                         (LevelSetProp.of_list [], ConstraintSet.empty);
      ind_variance := None |}))

view this post on Zulip Yannick Forster (Jan 07 2022 at 09:48):

Yes, it really isn't evaluated :) You need res <- tmEval cbn rs ;; tmPrint res

view this post on Zulip Yannick Forster (Jan 07 2022 at 09:48):

You have a lot of control over evaluation in the TemplateMonad

view this post on Zulip Julin S (Jan 07 2022 at 09:59):

Got it working now. Thanks a lot!

view this post on Zulip Notification Bot (Jan 07 2022 at 10:00):

Julin S has marked this topic as resolved.


Last updated: Aug 11 2022 at 02:03 UTC