Helper function for tCase

[Lysxia]

While playing around with MetaCoq, I found getting tCase right to be quite a hurdle, because of all the required annotations.

So I wrote a little wrapper that seems fairly general-purpose. Did I miss some existing utility, or does this tMatch function below seem to have a place in the library? It's very much in draft state, but if you have any comments to simplify this, I would welcome that too!

Roughly, given x, y, z : term and a function branches, tMatch x y z branches constructs the expression match x : y return z where ... end, assuming y is some inductive type, using the function branches to fill every branch given the name, type, and arity of the corresponding constructor.

https://gist.github.com/Lysxia/6a9025aeec5f89f36728da1426a3c9dd

[gmalecha]

Code like this seems great! I'm not sure where is best to put something like this.

[TheoWinterhalter]

Thank you. I'm wondering what would be the use cases though. In the example you provide, it would also have been possible to directly quote the match, right?

[Lysxia]

My use case right now is to derive serialization functions (roughly Haskell's Show or Rust's Debug), so the context and types are not known statically to allow me to quote a match, but on the other hand it seems that ensuring the well-formedness of tCase could partly be automated.

[Lysxia]

The fruit of my labor is here, hopefully that gives you a more concrete idea of where I'm coming from:

• Some generic defintions (inncluding tMatch): https://github.com/Lysxia/coq-ceres/blob/a9cd1d750f9fd3ce67e2d98b92a7355baa88d091/theories/TemplateLib.v

• Deriving a serialization function for inductive types: https://github.com/Lysxia/coq-ceres/blob/a9cd1d750f9fd3ce67e2d98b92a7355baa88d091/theories/Derive.v

• Some example usage: https://github.com/Lysxia/coq-ceres/blob/metacoq/test/DeriveTest.v

As a short overview, I'm generating functions looking like this from their type:

(* deriveSerialize (forall A B, Serialize A -> Serialize B -> Serialize (A + B)) *)
Fixpoint to_sexp_sum {A B} (to_sexpA : A -> sexp) (to_sexpB : B -> sexp) (x : A + B) : sexp :=
  match x with
  | inl a => List ["inl" ; to_sexpA a]
  | inr b => List ["inr" ; to_sexpB b]
  end.

I feel like I'm not quite making good use of the (un)quoting facilities of the TemplateMonad. A prime example is this: https://github.com/Lysxia/coq-ceres/blob/a9cd1d750f9fd3ce67e2d98b92a7355baa88d091/theories/Derive.v#L63-L67

  ...
  q_cname <- tmQuote (ARaw cname) ;;
  tmReturn
    match sfields with
    ...
    | _ :: _ => mkApp q_List (q_list_of_list_q q_sexp (q_cname :: sfields))
    end

Is there a more direct way to construct the term for List (ARaw cname :: $(f)) : sexp with some pseudo-syntax for unquoting a f : term (f := q_list_of_list_q q_sexp sfields). As far as I can tell, I can't do tmUnquoteTyped f since f is actually an open term that's going to go under a lambda.

To mention another issue of a similar kind, type class inference needs to be invoked explicitly. But again, that seems restricted to closed terms, so I can't just call inference whenever I need it. I have to push the context back into a term like forall A, Serialize A -> Serialize (option A), call type class inference to get a closed function of that type, and then apply it to the parameters from my original context.

[mattam82]

I don't think we have the infrastructure to do things like this yet. The issues with quoting/unquoting/calling tc inference under context are quite interesting! With the current reorganization of the code, all of this shall really go in the template-coq/ folder, maybe in a specific folder. Now the typing stuff that was in template-coq is in checker/. Alternatively, we could also reorganize translations into plugins and have an infrastructure or something similar there.