Julin S (Jan 07 2022 at 07:54): 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.
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
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
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
Yannick Forster (Jan 07 2022 at 07:58):My guess here would be that it is the rs <- map
Yannick Forster (Jan 07 2022 at 07:59):map returns a list, whereas the <- notation strictly expects a monadic value
Yannick Forster (Jan 07 2022 at 07:59):So you need to replace this part by a plain let
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)
Yannick Forster (Jan 07 2022 at 08:56):Yes, I think it is trying to infer Monad list
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
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?
Yannick Forster (Jan 07 2022 at 09:10):Still the same error message?
Yannick Forster (Jan 07 2022 at 09:10):Did you try finding the problem by replacing parts of the program with tmFail "test"?
Yannick Forster (Jan 07 2022 at 09:12):Ah: You're mapping on oibs, but you want to map on oibs.(ind_bodies)
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.
Yannick Forster said:
Ah: You're mapping on
oibs, but you want to map onoibs.(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.
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 |}))
Yes, it really isn't evaluated :) You need res <- tmEval cbn rs ;; tmPrint res
Yannick Forster (Jan 07 2022 at 09:48):You have a lot of control over evaluation in the TemplateMonad
Julin S (Jan 07 2022 at 09:59):Got it working now. Thanks a lot!
Notification Bot (Jan 07 2022 at 10:00):Julin S has marked this topic as resolved.
Last updated: May 31 2023 at 09:01 UTC