g_tuto1.mlg

DECLARE PLUGIN "tuto1_plugin"

{

(*
 * In this exercise, we will implement a Coq plugin!
 * Our plugin will manipulate terms from Coq and define new terms.
 * As always, this will be discussion-based, with the usual format.
 *)
open Pp
open Stdarg
open Termutils
open Exercise

}

(*** Defining terms ***)

(*
 * The cool thing about this exercise is showing you how you can
 * define terms inside of a Coq plugin. Coq plugins are implemented
 * inside of OCaml, with a special syntax to interface with Coq.
 * We can take Coq terms as input, and we can also define new Coq terms.
 * All Coq terms that we define are checked by Coq's type checker in the end,
 * so we don't have to worry about accidentally breaking Coq.
 *
 * Below is a custom version of the Definition command in Coq,
 * called MyDefine. MyDefine works like Definition---you can check out Demo.v
 * to see it in action. It calls some functions from Termutils, which I've
 * written for you to simplify your job a tiny bit.
 *
 * EXERCISE 1: Look at the functions I've defined for you in termutils.mli,
 * and the comments I've writen explaining them. From those functions,
 * add a comment explaining each function call in MyDefine below.
 *)
VERNAC COMMAND EXTEND MyDefine CLASSIFIED AS SIDEFF
| [ "MyDefine" ident(i) ":=" constr(e) ] ->
   {
     let sigma, env = global_env () in
     let sigma, trm = internalize env e sigma in
     define i trm sigma
   }
END

(*** Reasoning about terms in a plugin ***)

(*
 * It isn't just that we can define our own terms in plugins.
 * We can also reason about existing terms!
 *
 * Below I've implemented a command that counts all occurrences of terms
 * that are definitionally equal to src_e inside of e, with a few assumptions.
 * You can again check out Demo.v to see this command in action.
 * 
 * EXERCISE 2: Look once more the functions I've defined for you in
 * termutils.mli, and the comments I've writen explaining them.
 * Look also at the signature of the count function I've written for you
 * in exercise.mli. From those functions, add a comment explaining each
 * function call in Count below.
 *
 * EXERCISE 3: Look at the implementation of count in exercise.ml.
 * Look also at the definition of the AST in the Coq kernel:
 * https://github.com/coq/coq/blob/v8.14/kernel/constr.mli#L237
 * What is each case of the implementation of count in exercise.ml doing?
 * Add comments explaining each case.
 *
 * EXERCISE 4: Look again at the implementation of count in exercise.ml.
 * Look again also at the definition of the AST in the Coq kernel:
 * https://github.com/coq/coq/blob/v8.14/kernel/constr.mli#L237
 * Are there any cases that are not handled well right now?
 * (It's OK if you do not know what some of the cases are---though feel free
 * to ask. This is to get you thinking about the Coq AST, mostly.)
 *)
VERNAC COMMAND EXTEND Count CLASSIFIED AS SIDEFF
| [ "Count" constr(src_e) "in" constr(e) ] ->
   {
     let sigma, env = global_env () in
     let sigma, src = internalize env src_e sigma in
     let sigma, trm = internalize env e sigma in
     let sigma, count = count env src trm sigma in
     Feedback.msg_notice (strbrk (string_of_int count))
   }
END

(*** Both together ***)

(*
 * OK, now finally time to have some fun. You're going to implement
 * the Sub command, which substitutes all subterms of e that are
 * definitionally equal to the terms in the source list src_es
 * with the corresponding terms in the destination list dst_es.
 * In other words, this behaves like count, but instead of counting,
 * it substitutes, and it does this over an ordered list of substitutions.
 *
 * Please check out Demo.v before starting this so that you can get a better
 * idea of what this is supposed to do.
 *
 * EXERCISE 5: Implement sub in exercise.ml. When you are done, the Sub
 * command should behave as expected in Demo.v.
 *)
VERNAC COMMAND EXTEND Sub CLASSIFIED AS SIDEFF
| [ "Sub" constr_list(src_es) "with" constr_list(dst_es) "in"
      constr(e) "as" ident(i) ] ->
   {
     let sigma, env = global_env () in
     let sigma, srcs = map_state (internalize env) src_es sigma in
     let sigma, dsts = map_state (internalize env) dst_es sigma in
     let sigma, trm = internalize env e sigma in
     let sigma, subbed =
       fold_left_state
         (fun subbed (src, dst) -> sub env (src, dst) subbed)
         trm
         (List.combine srcs dsts)
         sigma
     in Termutils.define i subbed sigma
   }
END

(*** DISCUSSION ***)

(*
 * Same format as usual---please post in the forum as a group!
 * And you need to answer _just one_ of these questions to get credit
 * (though you can answer both if you are feeling adventurous).
 *
 * QUESTION 1: Based on your experiences so far, what do you think the
 * tradeoffs are of writing automation inside of a Coq plugin versus inside
 * of Ltac? Can you think of any use cases for which you'd prefer Ltac
 * over a plugin? And can you think of any use cases for which you'd prefer
 * a plugin over Ltac? In each case, why?
 *
 * QUESTION 2: Think back to all of the Coq tactics you've written or used
 * so far, like "rewrite" or "induction" or "autoinduct". Are there any you
 * think you could improve by implementing them inside of a plugin? How so? 
 *)

(*** BONUS ***)

(*
 * There are so, so many ways you can extend this. Some ideas below.
 *
 * BONUS 1: Extend your command to handle let expressions.
 * The function push_let_in from here may help:
 * https://github.com/uwplse/coq-plugin-lib/blob/master/src/coq/logicutils/contexts/envutils.ml
 *
 * BONUS 2: Extend your command to unfold constants.
 * The function lookup_definition from the same file linked to above may
 * help, though it is a bit out of date.
 *
 * BONUS 3: Notice how both "count" and "sub" have similar structure.
 * Factor that structure out into a fold over the structure of the AST,
 * and use it inside of both "count" and "sub". This will be useful for
 * other commands and tactics you might want to implement in the future!
 *)