I was trying to figure out why it seems that in a Coq generic argument there seems to be 3 arguments to the constructor GenArg when according to me there should only be 2 (plus one of the argument seems to skip to other constructors I was expecting based on the OCaml algebraic data type code e.g. OptArg).
I see from coq-serapi:
((GenArg raw (OptArg (ExtraArg ltac_selector)) ())
(GenArg raw (OptArg (ExtraArg ltac_info)) ())
(GenArg raw (ExtraArg tactic)
(TacArg
((v
(TacCall
((v
(((v (Ser_Qualid (DirPath ()) (Id ___hole)))
(loc
(((fname ToplevelInput) (line_nb 1) (bol_pos 0)
(line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 8)))))
( (ConstrMayEval
(ConstrTerm
((v
(CPrim (Numeral SPlus ((int 0) (frac "") (exp "")))))
(loc
(((fname ToplevelInput) (line_nb 1) (bol_pos 0)
(line_nb_last 1) (bol_pos_last 0) (bp 9) (ep 10))))))) )))
(loc
(((fname ToplevelInput) (line_nb 1) (bol_pos 0)
(line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 10)))))))
(loc
(((fname ToplevelInput) (line_nb 1) (bol_pos 0)
(line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 10)))))))
(GenArg raw (ExtraArg ltac_use_default) false)) ))))
focusing on the first one in the raw_generic_argument list:
(GenArg raw (OptArg (ExtraArg ltac_selector)) ()
we see we have this weird word raw that according to me should NOT be there because look at the type definition for raw_generic_argument:
type 'l generic_argument =
| GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument
A inhabitant of 'level generic_argument is a inhabitant of some type at level 'level, together with the representation of this type.
type raw_generic_argument = rlevel generic_argument
the constructor GenArg should only take 2 things. But the argument I showed takes 3 things -- the last one being unit, perhaps?
Can someone explain we what's going on?
In addition, the second argument (OptArg (ExtraArg ltac_selector)) seems completely off too. We know 'l is rlevel. We should have ('a rlevel) abstract_argument_type as the first argument (which seems to be the second one according to the s-expression I pasted. The abstract_argument_type has constructors:
type (_, _) abstract_argument_type =
| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type
but none appear...which is super puzzling to me. There are 3 options and nothing else. So why does it randomly skip to the constructor OptArg corresponding to gen_arg_type?
