Tags: /
coq
/
Quite a crude way. There got to be better and elegant ways. This post is sort of a note to my future self.
TemplateMonad seems to be the right way to do this, but in this post it is not used. Maybe it'll help appreciate the utility of TemplateMonad.
Versions of software used:
I had an example inductive type:
Inductive C :=
| r : C
| g : nat -> C
| b : bool -> nat -> C.
And I needed to find a way to extract the constructors of this type as an AST (abstract syntax tree).
Template-Coq, which is part of the MetaCoq project, allows us to do this.
So the aim is to get a result like
[("r", astof(C));
("g", astof(nat -> C));
("b", astof(nat -> C))]
Template-Coq can do:
We're gonna need the quoting part.
Let's start. First, we 'quote' C recursively (the non-recursive quoting doesn't give as much level of detail) and store its AST form in qC:
From MetaCoq.Template Require Import utils All.
Require Import List String.
Import ListNotations MonadNotation.
MetaCoq Quote Recursively Definition qC := C.
qC looks like
([(MPfile ["myfilename"], "C",
InductiveDecl
{|
ind_finite := Finite; (* Recursivity kind: Inductive. Not co-inductive *)
ind_npars := 0; (* No parameters *)
ind_params := []; (* No parameters *)
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 |});
(MPfile ["Datatypes"; "Init"; "Coq"], "bool",
InductiveDecl
{|
ind_finite := Finite;
ind_npars := 0;
ind_params := [];
ind_bodies := [{|
ind_name := "bool";
ind_type := tSort
(Universe.from_kernel_repr
(Level.lSet, false) []);
ind_kelim := InType;
ind_ctors := [("true", tRel 0, 0); ("false", tRel 0, 0)];
ind_projs := [] |}];
ind_universes := Monomorphic_ctx
(LevelSetProp.of_list [], ConstraintSet.empty);
ind_variance := None |});
(MPfile ["Datatypes"; "Init"; "Coq"], "nat",
InductiveDecl
{|
ind_finite := Finite;
ind_npars := 0;
ind_params := [];
ind_bodies := [{|
ind_name := "nat";
ind_type := tSort
(Universe.from_kernel_repr
(Level.lSet, false) []);
ind_kelim := InType;
ind_ctors := [("O", tRel 0, 0);
("S", tProd nAnon (tRel 0) (tRel 1), 1)];
ind_projs := [] |}];
ind_universes := Monomorphic_ctx
(LevelSetProp.of_list [], ConstraintSet.empty);
ind_variance := None |})],
tInd {| inductive_mind := (MPfile ["myfilename"], "C"); inductive_ind := 0 |} [])
: program
where "myfilename" is the name of the source file.
Quite verbose, yes, but it's the AST of the Coq source, after all.
This quoted term that we got is of type program which is defined like
(* metacoq/template-coq/theories/Environment.v *)
Definition program : Type := global_env * term.
So here, the global_env term is (skipping most parts of as it has already been mentioned):
[(MPfile ["myfilename"], "C",
InductiveDecl
{|
ind_finite := Finite;
ind_npars := 0;
ind_params := [];
ind_bodies := [{|
...
...
ind_projs := [] |}];
ind_universes := Monomorphic_ctx
(LevelSetProp.of_list [], ConstraintSet.empty);
ind_variance := None |});
(MPfile ["Datatypes"; "Init"; "Coq"], "bool",
InductiveDecl
{|
ind_finite := Finite;
ind_npars := 0;
ind_params := [];
ind_bodies := [{|
ind_name := "bool";
ind_type := tSort
(Universe.from_kernel_repr
(Level.lSet, false) []);
ind_kelim := InType;
ind_ctors := [("true", tRel 0, 0); ("false", tRel 0, 0)];
ind_projs := [] |}];
ind_universes := Monomorphic_ctx
(LevelSetProp.of_list [], ConstraintSet.empty);
ind_variance := None |});
(MPfile ["Datatypes"; "Init"; "Coq"], "nat",
InductiveDecl
...
...
ind_variance := None |})].
and the term term is:
= tInd
{|
inductive_mind := (MPfile ["myfilename"], "C");
inductive_ind := 0 |} []
: term
The constructors seem to be in the global_env term.
Let's get the global_env term from the program value:
Definition aux1 (p : program) : global_env := fst p.
Compute aux1 qC.
Within the global_env term, the constructors appears to be in the ind_bodies field of the inductiveDecl record.
global_env is defined like:
(* metacoq/template-coq/theories/Environment.v *)
Definition global_env : Type := list (kername * global_decl).
We need the first value in this list.
Could use List.hd for that, but since List.hd is defined like
(* theories/Lists/List.v *)
Definition hd (A : Type) (default:A) (l:list A) :=
match l with
| [] => default
| x :: _ => x
end.
in a way that requires a default value, we need a default (kername * global_decl) value (the 'quest' to find default values is included at the end of this post as an addendum).
Definition default_global_decl : 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).
Okay, now that we have got a default (kername * global_decl) as default_kg, let's get the first (kername * global_decl).
Definition aux2 (g : global_env) : (kername * global_decl) :=
List.hd default_kg g.
Compute aux2 (aux1 qC).
(*
= (MPfile ["myfilename"], "C",
InductiveDecl
{|
ind_finite := Finite;
ind_npars := 0;
ind_params := [];
ind_bodies := [{|
ind_name := "C";
ind_type := tSort
{|
Universe.t_set := {|
UnivExprSet.this := [UnivExpr.npe
(NoPropLevel.lSet, false)];
UnivExprSet.is_ok := UnivExprSet.Raw.singleton_ok
(UnivExpr.npe
(NoPropLevel.lSet, false)) |};
Universe.t_ne := eq_refl |};
ind_kelim := InType;
ind_ctors := [("r", tRel 0, 0);
...
...
];
ind_projs := [] |}];
ind_universes := Monomorphic_ctx
({|
LevelSet.this := [];
LevelSet.is_ok := LevelSet.Raw.empty_ok |},
{|
ConstraintSet.this := [];
ConstraintSet.is_ok := ConstraintSet.Raw.empty_ok |});
ind_variance := None |})
: kername × global_decl
*)
kername is defined like
(* template-coq/theories/BasicAst.v *)
Definition kername : Set := modpath × ident.
So the (kername * global_decl) is actually (modpath * ident) * global_decl which may also be written like modpath * ident * global_decl as coq tuples associate to the left such that (1, 2, 3) and ((1, 2), 3) are same.
Check (1,2,3).
(* (1, 2, 3) : (nat × nat) × nat *)
Check ((1,2),3).
(* (1, 2, 3) : (nat × nat) × nat *)
In the output of aux2 (aux1 qC),
MPfile ["three"] is the modpath"C" is the identInductiveDecl is the global_decl~The constructors are in the global_decl part.
Making a function aux3 to get the global_decl,
Definition aux3 (kg : kername * global_decl) : global_decl := snd kg.
Compute aux3 (aux2 (aux1 qC)).
(*
= InductiveDecl
{|
ind_finite := Finite;
ind_npars := 0;
ind_params := [];
ind_bodies := [{|
ind_name := "C";
ind_type := tSort
{|
Universe.t_set := {|
UnivExprSet.this := [UnivExpr.npe
(NoPropLevel.lSet, false)];
UnivExprSet.is_ok := UnivExprSet.Raw.singleton_ok
(UnivExpr.npe
(NoPropLevel.lSet, false)) |};
Universe.t_ne := eq_refl |};
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
({|
LevelSet.this := [];
LevelSet.is_ok := LevelSet.Raw.empty_ok |},
{|
ConstraintSet.this := [];
ConstraintSet.is_ok := ConstraintSet.Raw.empty_ok |});
ind_variance := None |}
: global_decl
*)
The constructors are inside the ind_bodies field of the mutual_inductive_body argument to InductiveDecl. ind_bodies has a list one_inductive_body.
Definition aux4 (g : global_decl) : list one_inductive_body :=
match g with
| ConstantDecl _ => []%list
| InductiveDecl mib => mib.(ind_bodies) (* TODO Map *)
end.
Compute aux4 (aux3 (aux2 (aux1 qC))).
(*
= [{|
ind_name := "C";
ind_type := tSort
{|
Universe.t_set := {|
UnivExprSet.this := [UnivExpr.npe
(NoPropLevel.lSet, false)];
UnivExprSet.is_ok := UnivExprSet.Raw.singleton_ok
(UnivExpr.npe
(NoPropLevel.lSet, false)) |};
Universe.t_ne := eq_refl |};
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 := [] |}]
: list one_inductive_body
*)
Now we are quite close to constructors, which are inside the ind_ctors field of the one_inductive_body values.
Definition aux5 (oibs : list one_inductive_body)
: list (list (ident * term * nat)) :=
map (fun o:one_inductive_body => o.(ind_ctors)) oibs.
Compute aux5 (aux4 (aux3 (aux2 (aux1 qC)))). (* CONSTRUCTORS! *)
(*
= [[("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))
*)
Piecing all the 'aux' functions together:
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))
*)
Which is what we were after.
(Just for fun's sake, let me try this notation here.
Notation "f $ x" := (f x)
(at level 60, right associativity, only parsing).
Definition aux' (p : program) : list (list (ident * term * nat)) :=
let gd := snd $ List.hd default_kg $ (fst p) in
map (fun o:one_inductive_body => o.(ind_ctors))
match gd with
| ConstantDecl _ => []%list
| InductiveDecl mib => mib.(ind_bodies)
end.
Compute aux' qC.
But I had been warned that this can cause scope inference to break.
Okay, side-mission over.)
For use with List.hd which requires a default value.
Being unfamiliar with the Template-Coq types when I used it for the first time, I found it helpful to write them down.
Still not sure if this was necessary, but as of writing this post, I don't know of any other way.
identident is same as string and represents an identifier.
(* template-coq/theories/BasicAst.v *)
Definition ident : Set := string.
modpathDefinition:
(* template-coq/theories/BasicAst.v *)
Inductive modpath : Set :=
| MPfile (dp : dirpath)
| MPbound (dp : dirpath) (id : ident) (i : nat)
| MPdot (mp : modpath) (id : ident).
Let's go with the simplest constructor, MPfile.
Using a dummy dirpath value,
Check MPfile []%list : modpath.
(*
MPfile [] : modpath
: modpath
*)
kernameDefinition:
(* template-coq/theories/BasicAst.v *)
Definition kername : Set := modpath × ident.
Using dummy modpath and ident values (where ident is same as string),
Check (MPfile []%list, ""%string) : kername.
(*
(MPfile [], "") : kername
: kername
*)
dirpathDefinition:
(* template-coq/theories/BasicAst.v *)
Definition dirpath : Set := list ident.
which means it is basically list string.
A list! Easy. An empty list would do.
Check []%list : dirpath.
(*
[] : dirpath
: dirpath
*)
global_declDefinition:
Inductive global_decl : Type :=
(* Represents declaration of constants, I guess *)
| ConstantDecl : constant_body -> global_decl
(* Represents declaration of inductive types, probably *)
| InductiveDecl : mutual_inductive_body -> global_decl.
Simplest constructor is ConstantDecl, let's go with that.
Using a dummy constant_body value,
Check ConstantDecl (Build_constant_body (tVar ""%string) None
(Monomorphic_ctx ((LevelSet.Mkt []%list), (ConstraintSet.Mkt []%list)) : universes_decl)) : global_decl.
(*
ConstantDecl
{|
cst_type := tVar "";
cst_body := None;
cst_universes := Monomorphic_ctx
({|
LevelSet.this := [];
LevelSet.is_ok := LevelSet.Raw.empty_ok |},
{|
ConstraintSet.this := [];
ConstraintSet.is_ok := ConstraintSet.Raw.empty_ok |})
:
universes_decl |}
:
global_decl
: global_decl
*)
constant_bodyDefinition:
Record constant_body : Type := Build_constant_body {
cst_type : term;
cst_body : option term;
cst_universes : universes_decl
}.
Simplest option value is, of course, None.
Using dummy universe_decl and terms values with this,
Check Build_constant_body (tVar ""%string) None
(Monomorphic_ctx ((LevelSet.Mkt []%list), (ConstraintSet.Mkt []%list)) : universes_decl) : constant_body.
(*
{|
cst_type := tVar "";
cst_body := None;
cst_universes := Monomorphic_ctx
({|
LevelSet.this := [];
LevelSet.is_ok := LevelSet.Raw.empty_ok |},
{|
ConstraintSet.this := [];
ConstraintSet.is_ok := ConstraintSet.Raw.empty_ok |})
:
universes_decl |}
:
constant_body
: constant_body
*)
termDefinition:
Inductive term : Type :=
tRel : nat -> term
| tVar : ident -> term
| tEvar : nat -> list term -> term
| tSort : Universe.t -> term
| tCast : term -> cast_kind -> term -> term
| tProd : name -> term -> term -> term
| tLambda : name -> term -> term -> term
| tLetIn : name -> term -> term -> term -> term
| tApp : term -> list term -> term
| tConst : kername -> Instance.t -> term
| tInd : inductive -> Instance.t -> term
| tConstruct : inductive -> nat -> Instance.t -> term
| tCase : inductive × nat -> term -> term -> list (nat × term) -> term
| tProj : projection -> term -> term
| tFix : mfixpoint term -> nat -> term
| tCoFix : mfixpoint term -> nat -> term
Arguments tRel _%nat_scope
Arguments tEvar _%nat_scope _%list_scope
Arguments tApp _ _%list_scope
Arguments tConstruct _ _%nat_scope
Arguments tCase _ _ _ _%list_scope
Arguments tFix _ _%nat_scope
Arguments tCoFix _ _%nat_scope
tVar seems simple enough.
Check (tVar ""%string) : term.
(*
tVar "" : term
: term
*)
universes_declDefinition:
Inductive universes_decl : Type :=
Monomorphic_ctx : ContextSet.t -> universes_decl
| Polymorphic_ctx : AUContext.t -> universes_decl
Let's go with Monomorphic_ctx (because monomorphic got to be simpler than polymorphic, right?). Using a dummy ContextSet.t value,
Check Monomorphic_ctx ((LevelSet.Mkt []%list), (ConstraintSet.Mkt []%list)) : universes_decl.
(*
Monomorphic_ctx
({| LevelSet.this := []; LevelSet.is_ok := LevelSet.Raw.empty_ok |},
{|
ConstraintSet.this := [];
ConstraintSet.is_ok := ConstraintSet.Raw.empty_ok |})
:
universes_decl
: universes_decl
*)
ContextSet.tDefinition:
ContextSet.t = LevelSet.t × ConstraintSet.t
: Type
Using dummy LevelSet.t and ConstraintSet.t values,
Check ((LevelSet.Mkt []%list), (ConstraintSet.Mkt []%list)) : ContextSet.t.
(*
({| LevelSet.this := []; LevelSet.is_ok := LevelSet.Raw.empty_ok |},
{|
ConstraintSet.this := [];
ConstraintSet.is_ok := ConstraintSet.Raw.empty_ok |})
:
ContextSet.t
: ContextSet.t
*)
LevelSet.tDefinition:
LevelSet.t = LevelSet.t_
: Type
Using a dummy LevelSet.t_ value,
Check LevelSet.Mkt []%list : LevelSet.t.
(*
{| LevelSet.this := []; LevelSet.is_ok := LevelSet.Raw.empty_ok |}
:
LevelSet.t
: LevelSet.t
*)
LevelSet.t_Definition:
Record t_ : Type := Mkt {
this : LevelSet.Raw.t;
is_ok : LevelSet.Raw.Ok this
}.
Arguments LevelSet.Mkt _ {is_ok}.
is_ok is implicit. Using a random LevelSet.Raw.t,
Check LevelSet.Mkt []%list : LevelSet.t_.
(*
{| LevelSet.this := []; LevelSet.is_ok := LevelSet.Raw.empty_ok |}
:
LevelSet.t_
: LevelSet.t_
*)
LevelSet.Raw.tLevelSet.Raw.t = list LevelSet.Raw.elt
: Type
A list. So we can stop here with a simple []%list.
Check []%list : LevelSet.Raw.t.
(*
[] : LevelSet.Raw.t
: LevelSet.Raw.t
*)
ConstraintSet.tDefinition:
ConstraintSet.t = ConstraintSet.t_
: Type
Using dummy ConstraintSet.t_ value,
Check ConstraintSet.Mkt []%list : ConstraintSet.t.
(*
{|
ConstraintSet.this := [];
ConstraintSet.is_ok := ConstraintSet.Raw.empty_ok |}
:
ConstraintSet.t
: ConstraintSet.t
*)
ConstraintSet.t_Record t_ : Type := Mkt {
this : ConstraintSet.Raw.t;
is_ok : ConstraintSet.Raw.Ok this
}.
Arguments ConstraintSet.Mkt _ {is_ok}
is_ok is implicit. Using a dummy ConstraintSet.Raw.t,
Check ConstraintSet.Mkt []%list : ConstraintSet.t_.
(*
{|
ConstraintSet.this := [];
ConstraintSet.is_ok := ConstraintSet.Raw.empty_ok |}
:
ConstraintSet.t_
: ConstraintSet.t_
*)
ConstraintSet.Raw.tConstraintSet.Raw.t = list ConstraintSet.Raw.elt
: Type
A list!
Check []%list : ConstraintSet.Raw.t.
(*
[] : ConstraintSet.Raw.t
: ConstraintSet.Raw.t
*)
recursivity_kindDefinition:
Inductive recursivity_kind : Set :=
Finite : recursivity_kind
| CoFinite : recursivity_kind
| BiFinite : recursivity_kind
Going with Finite.
Check Finite : recursivity_kind.
(*
Finite : recursivity_kind
: recursivity_kind
*)
mutual_inductive_bodyRecord mutual_inductive_body : Type := Build_mutual_inductive_body
{ ind_finite : recursivity_kind;
ind_npars : nat;
ind_params : context;
ind_bodies : list one_inductive_body;
ind_universes : universes_decl;
ind_variance : option (list Variance.t) }
Arguments Build_mutual_inductive_body _ _%nat_scope _ _%list_scope
Using dummy values,
Compute Build_mutual_inductive_body Finite 0 []%list []%list
(Monomorphic_ctx (LevelSet.Mkt []%list, ConstraintSet.Mkt []%list)) None.
(*
= {|
ind_finite := Finite;
ind_npars := 0;
ind_params := [];
ind_bodies := [];
ind_universes := Monomorphic_ctx
({|
LevelSet.this := [];
LevelSet.is_ok := LevelSet.Raw.empty_ok |},
{|
ConstraintSet.this := [];
ConstraintSet.is_ok := ConstraintSet.Raw.empty_ok |});
ind_variance := None |}
: mutual_inductive_body
*)
contextDefinition:
context = list context_decl
: Type
List. Empty list would do.
Check []%list : context.
(*
[] : context
: context
*)
sort_familyDefinition:
Inductive sort_family : Set :=
InProp : sort_family | InSet : sort_family | InType : sort_family
Any of the three would do. Let's go with InProp.
Check InProp : sort_family.
(*
InProp : sort_family
: sort_family
*)
one_inductive_bodyDefinition:
Record one_inductive_body : Type := Build_one_inductive_body
{ ind_name : ident;
ind_type : term;
ind_kelim : sort_family;
ind_ctors : list ((ident × term) × nat);
ind_projs : list (ident × term) }
Arguments Build_one_inductive_body _ _ _ (_ _)%list_scope
Using dummy ident, term and sort_family values,
Check Build_one_inductive_body "None"%string (tVar "None"%string) InProp []%list []%list.
(*
{|
ind_name := "None";
ind_type := tVar "None";
ind_kelim := InProp;
ind_ctors := [];
ind_projs := [] |}
: one_inductive_body
*)
(This blog post was originally completed by 07 January 2022.)