Automatically generating gallina quotation functions?

[JasonGross]

Is there any way to script this process? It might make a nice addition to this plugin:

Class Quotable (T : Type) := quote : T -> Ast.term.

Local Notation "( x ; y )" := (existT _ x y).

Definition map_quote : list { T : Type & Quotable T * T }%type -> list Ast.term
  := List.map (fun TvH : { T : Type & Quotable T * T }%type
               => @quote (projT1 TvH) (fst (projT2 TvH)) (snd (projT2 TvH))).

Local Notation " [[ x ;; .. ;; y ]] " := (cons (_; (_, x)) .. (cons (_; (_, y)) nil) ..) : list_scope.
Local Notation " [[ x ]] " := (cons (_; (_, x)) nil) : list_scope.

Quote Definition qO := O.
Quote Definition qS := S.

Fixpoint quote_nat (n : nat) : Ast.term
  := match n with
       | O => qO
       | S n' => Ast.tApp qS [quote_nat n']
     end.

Instance nat_quotable : Quotable nat := quote_nat.

Quote Definition qtrue := true.
Quote Definition qfalse := false.

Definition quote_bool (b : bool) : Ast.term
  := if b then qtrue else qfalse.

Instance bool_quotable : Quotable bool := quote_bool.

Quote Definition qAscii := Ascii.Ascii.

Fixpoint quote_ascii (a : Ascii.ascii) : Ast.term
  := match a with
       | Ascii.Ascii b0 b1 b2 b3 b4 b5 b6 b7
         => Ast.tApp qAscii (map_quote [[b0 ;; b1 ;; b2 ;; b3 ;; b4 ;; b5 ;; b6 ;; b7]])
     end.

Instance ascii_quotable : Quotable Ascii.ascii := quote_ascii.

Quote Definition qEmptyString := EmptyString.
Quote Definition qString := String.

Fixpoint quote_string (s : string) : Ast.term
  := match s with
       | EmptyString => qEmptyString
       | String a s' => Ast.tApp qString [quote a; quote_string s']
     end.

Instance string_quotable : Quotable string := quote_string.

[gmalecha]

This is not meant to be the purpose of this plugin. The idea is to produce something as close as possible to the kernel's representation. For example,

quote ("a" ++ "b")

should produce

App (App (append) (quoting of "a")) (quoting of "b")

Your implementation of quote_string does not do this. It will reduce and quote the result.

[gmalecha]

The actual idea of this plugin is to use Ast.term to be able to write programs that generate programs like this. I.e. can you write a function generate_to_string : Ast.inductive_body -> Ast.term that will take a description of an inductive data type and produce an Ast.term that when internalized will run like to_string.

[JasonGross]

The actual thing I need (for mathematical reasons) is a function quote : Ast.term -> Ast.term which takes any syntactic program and adds an extra layer of syntax on top of it. That is, if we have the sequence Gallina; term of type Ast.term; term of type Ast.term which, when denoted, gives a term of type Ast.term; ..., quote should add one level of indirection in this sequence. This is, again, for quining and Löb's theorem.

In case anyone else comes looking, here's some python code that does, basically, this:

def make_quote_definition(q_i_idents):
    for qi, i in q_i_idents:
        print('Quote Definition %s := %s.' % (qi, i))

def make_quote_for_type_match(q_i_n_idents):
    for qi, i, n in q_i_n_idents:
        ls1 = ' '.join('x%d' % idx for idx in range(n))
        ls2 = '[' + '; '.join('quote x%d' % idx for idx in range(n)) + ']'
        yield '          | %s %s => Ast.tApp %s %s' % (i, ls1, qi, ls2)

def make_quote_for_type(q_i_n_idents, qtype_name, type_name, rec=True):
    q_i_n_idents = list(q_i_n_idents)
    make_quote_definition([(q, i) for q, i, n in q_i_n_idents])
    print('')
    print('''%s quote_%s (x : %s) : Preterm
  := %smatch x with
%s
     end.
''' % (('Fixpoint' if rec else 'Definition'), qtype_name, type_name,
       ("""let x' := (quote_%s : Quotable %s) in
     """ % (qtype_name, type_name) if rec else ''),
       '\n'.join(make_quote_for_type_match(q_i_n_idents))))
    print('Instance %s_quotable : Quotable %s := quote_%s.' % (qtype_name, type_name, qtype_name))
    print('')

ls_inductive = (('mkInd', 2), )
make_quote_for_type((('q' + i, 'Ast.' + i, n) for i, n in ls_inductive), 'inductive', 'Ast.inductive', rec=False)
#ls_sort = (('sProp', 0), ('sSet', 0), ('sType', 1))
#make_quote_for_type((('q' + i, 'Ast.' + i, n) for i, n in ls_sort), 'sort', 'Ast.sort', rec=False)
#ls_name = (('nAnon', 0), ('nNamed', 1))
#make_quote_for_type((('q' + i, 'Ast.' + i, n) for i, n in ls_name), 'name', 'Ast.name', rec=False)
#ls_cast_kind = (('VmCast', 0), ('NativeCast', 0), ('Cast', 0), ('RevertCast', 0))
#make_quote_for_type((('q' + i, 'Ast.' + i, n) for i, n in ls_cast_kind), 'cast_kind', 'Ast.cast_kind', rec=False)
#qds = (('Rel', 1), ('Var', 1), ('Meta', 1), ('Evar', 1), ('Sort', 1), ('Cast', 3), ('Prod', 3), ('Lambda', 3), ('LetIn', 4), ('App', 2), ('Const', 1), ('Ind', 1), ('Construct', 2), ('Case', 4), ('Fix', 2), ('Unknown', 1))
#make_quote_for_type((('qt' + i, 'Ast.t' + i, n) for i, n in qds), 'term', 'Ast.term')

[JasonGross]

For example,

quote ("a" ++ "b")

should produce

App (App (append) (quoting of "a")) (quoting of "b")

This is impossible if quote is a gallina function. I agree that there should be an Ltac function that does just this, but I also need a gallina function, primarily to be used on terms already in normal form.

[gmalecha]

If you are just quoting constants (i.e. everything is a constructor) then it should be pretty easy to implement this as a Coq function.