Add 'doc/plugin_tutorial/' from commit '168a13dab1c9987f592994150997e692d4d7e40b'

git-subtree-dir: doc/plugin_tutorial
git-subtree-mainline: 8c040974facb733682d24c488dc89941671f4ab7
git-subtree-split: 168a13dab1c9987f592994150997e692d4d7e40b

7 files changed, 393 insertions, 0 deletions

diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.ml b/doc/plugin_tutorial/tuto3/src/construction_game.ml
new file mode 100644
index 0000000000..22b02f6893
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/src/construction_game.ml
@@ -0,0 +1,184 @@
+open Pp
+
+let example_sort evd =
+(* creating a new sort requires that universes should be recorded
+  in the evd datastructure, so this datastructure also needs to be
+  passed around. *)
+  let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
+  let new_type = EConstr.mkSort s in
+  evd, new_type
+
+let c_one evd =
+(* In the general case, global references may refer to universe polymorphic
+   objects, and their universe has to be made afresh when creating an instance. *)
+  let gr_S =
+    Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
+(* the long name of "S" was found with the command "About S." *)
+  let gr_O =
+    Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
+  let evd, c_O = Evarutil.new_global evd gr_O in
+  let evd, c_S = Evarutil.new_global evd gr_S in
+(* Here is the construction of a new term by applying functions to argument. *)
+  evd, EConstr.mkApp (c_S, [| c_O |])
+
+let dangling_identity env evd =
+(* I call this a dangling identity, because it is not polymorph, but
+   the type on which it applies is left unspecified, as it is
+   represented by an existential variable.  The declaration for this
+   existential variable needs to be added in the evd datastructure. *)
+  let evd, type_type = example_sort evd in
+  let evd, arg_type = Evarutil.new_evar env evd type_type in
+(* Notice the use of a De Bruijn index for the inner occurrence of the
+  bound variable. *)
+  evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
+          EConstr.mkRel 1)
+
+let dangling_identity2 env evd =
+(* This example uses directly a function that produces an evar that
+  is meant to be a type. *)
+  let evd, (arg_type, type_type) =
+    Evarutil.new_type_evar env evd Evd.univ_rigid in
+  evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
+          EConstr.mkRel 1)
+
+let example_sort_app_lambda () =
+    let env = Global.env () in
+    let evd = Evd.from_env env in
+    let evd, c_v = c_one evd in
+(* dangling_identity and dangling_identity2 can be used interchangeably here *)
+    let evd, c_f = dangling_identity2 env evd in
+    let c_1 = EConstr.mkApp (c_f, [| c_v |]) in
+    let _ = Feedback.msg_notice
+       (Printer.pr_econstr_env env evd c_1) in
+    (* type verification happens here.  Type verification will update
+       existential variable information in the evd part. *)
+    let evd, the_type = Typing.type_of env evd c_1 in
+(* At display time, you will notice that the system knows about the
+  existential variable being instantiated to the "nat" type, even
+  though c_1 still contains the meta-variable. *)
+    Feedback.msg_notice
+      ((Printer.pr_econstr_env env evd c_1) ++
+       str " has type " ++
+       (Printer.pr_econstr_env env evd the_type))
+
+
+let c_S evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
+  Evarutil.new_global evd gr
+
+let c_O evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
+  Evarutil.new_global evd gr
+
+let c_E evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in
+  Evarutil.new_global evd gr
+
+let c_D evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in
+  Evarutil.new_global evd gr
+
+let c_Q evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in
+  Evarutil.new_global evd gr
+
+let c_R evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in
+  Evarutil.new_global evd gr
+
+let c_N evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in
+  Evarutil.new_global evd gr
+
+let c_C evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "C" in
+  Evarutil.new_global evd gr
+
+let c_F evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in
+  Evarutil.new_global evd gr
+
+let c_P evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in
+  Evarutil.new_global evd gr
+
+(* If c_S was universe polymorphic, we should have created a new constant
+   at each iteration of buildup. *)
+let mk_nat evd n =
+  let evd, c_S = c_S evd in
+  let evd, c_O = c_O evd in
+  let rec buildup = function
+    | 0 -> c_O
+    | n -> EConstr.mkApp (c_S, [| buildup (n - 1) |]) in
+  if n <= 0 then evd, c_O else evd, buildup n
+
+let example_classes n =
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let evd, c_n = mk_nat evd n in
+  let evd, n_half = mk_nat evd (n / 2) in
+  let evd, c_N = c_N evd in
+  let evd, c_div = c_D evd in
+  let evd, c_even = c_E evd in
+  let evd, c_Q = c_Q evd in
+  let evd, c_R = c_R evd in
+  let arg_type = EConstr.mkApp (c_even, [| c_n |]) in
+  let evd0 = evd in
+  let evd, instance = Evarutil.new_evar env evd arg_type in
+  let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in
+  let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in
+  let evd, the_type = Typing.type_of env evd c_half in
+  let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in
+  let proved_equality =
+    EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), Constr.DEFAULTcast,
+      EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in
+(* This is where we force the system to compute with type classes. *)
+(* Question to coq developers: why do we pass two evd arguments to
+   solve_remaining_evars? Is the choice of evd0 relevant here? *)
+  let evd = Pretyping.solve_remaining_evars
+    (Pretyping.default_inference_flags true) env evd ~initial:evd0 in
+  let evd, final_type = Typing.type_of env evd proved_equality in
+  Feedback.msg_notice (Printer.pr_econstr_env env evd proved_equality)
+
+(* This function, together with definitions in Data.v, shows how to
+   trigger automatic proofs at the time of typechecking, based on
+   canonical structures.
+
+   n is a number for which we want to find the half (and a proof that
+   this half is indeed the half)
+*)
+let example_canonical n =
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+(* Construct a natural representation of this integer. *)
+  let evd, c_n = mk_nat evd n in
+(* terms for "nat", "eq", "S_ev", "eq_refl", "C" *)
+  let evd, c_N = c_N evd in
+  let evd, c_F = c_F evd in
+  let evd, c_R = c_R evd in
+  let evd, c_C = c_C evd in
+  let evd, c_P = c_P evd in
+(* the last argument of C *)
+  let refl_term = EConstr.mkApp (c_R, [|c_N; c_n |]) in
+(* Now we build two existential variables, for the value of the half and for
+   the "S_ev" structure that triggers the proof search. *)
+  let evd, ev1 = Evarutil.new_evar env evd c_N in
+(* This is the type for the second existential variable *)
+  let csev = EConstr.mkApp (c_F, [| ev1 |]) in
+  let evd, ev2 = Evarutil.new_evar env evd csev in
+(* Now we build the C structure. *)
+  let test_term = EConstr.mkApp (c_C, [| c_n; ev1; ev2; refl_term |]) in
+(* Type-checking this term will compute values for the existential variables *)
+  let evd, final_type = Typing.type_of env evd test_term in
+(* The computed type has two parameters, the second one is the proof. *)
+  let value = match EConstr.kind evd final_type with
+      | Constr.App(_, [| _; the_half |]) -> the_half
+      | _ -> failwith "expecting the whole type to be \"cmp _ the_half\"" in
+  let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd value) in
+(* I wish for a nicer way to get the value of ev2 in the evar_map *)
+  let prf_struct = EConstr.of_constr (EConstr.to_constr evd ev2) in
+  let the_prf = EConstr.mkApp (c_P, [| ev1; prf_struct |]) in
+  let evd, the_statement = Typing.type_of env evd the_prf in
+  Feedback.msg_notice
+    (Printer.pr_econstr_env env evd the_prf ++ str " has type " ++
+     Printer.pr_econstr_env env evd the_statement)
diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.mli b/doc/plugin_tutorial/tuto3/src/construction_game.mli
new file mode 100644
index 0000000000..1832ed6630
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/src/construction_game.mli
@@ -0,0 +1,4 @@
+val dangling_identity : Environ.env -> Evd.evar_map -> Evd.evar_map * EConstr.t
+val example_sort_app_lambda : unit -> unit
+val example_classes : int -> unit
+val example_canonical : int -> unit
diff --git a/doc/plugin_tutorial/tuto3/src/dune b/doc/plugin_tutorial/tuto3/src/dune
new file mode 100644
index 0000000000..ba6d8b288f
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/src/dune
@@ -0,0 +1,10 @@
+(library
+ (name tuto3_plugin)
+ (public_name coq.plugins.tutorial.p3)
+ (flags :standard -warn-error -3)
+ (libraries coq.plugins.ltac))
+
+(rule
+ (targets g_tuto3.ml)
+ (deps (:pp-file g_tuto3.mlg))
+ (action (run coqpp %{pp-file})))
diff --git a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
new file mode 100644
index 0000000000..82ba45726e
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
@@ -0,0 +1,46 @@
+DECLARE PLUGIN "tuto3_plugin"
+
+{
+
+open Ltac_plugin
+
+open Construction_game
+
+(* This one is necessary, to avoid message about missing wit_string *)
+open Stdarg
+
+}
+
+VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
+| [ "Tuto3_1" ] ->
+  { let env = Global.env () in
+    let evd = Evd.from_env env in
+    let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
+    let new_type_2 = EConstr.mkSort s in
+    let evd, _ =
+      Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in
+    Feedback.msg_notice
+      (Printer.pr_econstr_env env evd new_type_2) }
+END
+
+VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
+| [ "Tuto3_2" ] -> { example_sort_app_lambda () }
+END
+
+TACTIC EXTEND collapse_hyps
+| [ "pack" "hypothesis" ident(i) ] ->
+  { Tuto_tactic.pack_tactic i }
+END
+
+(* More advanced examples, where automatic proof happens but
+   no tactic is being called explicitely.  The first one uses
+   type classes. *)
+VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
+| [ "Tuto3_3" int(n) ] -> { example_classes n }
+END
+
+(* The second one uses canonical structures. *)
+VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY
+| [ "Tuto3_4" int(n) ] -> { example_canonical n }
+END
+
diff --git a/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack b/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack
new file mode 100644
index 0000000000..f4645ad7ed
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack
@@ -0,0 +1,3 @@
+Construction_game
+Tuto_tactic
+G_tuto3
diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
new file mode 100644
index 0000000000..9818867621
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
@@ -0,0 +1,143 @@
+open Proofview
+
+let constants = ref ([] : EConstr.t list)
+
+(* This is a pattern to collect terms from the Coq memory of valid terms
+  and proofs.  This pattern extends all the way to the definition of function
+ c_U *)
+let collect_constants () =
+  if (!constants = []) then
+    let open Coqlib in
+    let open EConstr in
+    let open UnivGen in
+    let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "pack" in
+    let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "packer" in
+    let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in
+    let gr_P = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "prod" in
+    let gr_U = find_reference "Tuto3" ["Tuto3"; "Data"] "uncover" in
+    constants := List.map (fun x -> of_constr (constr_of_monomorphic_global x))
+      [gr_H; gr_M; gr_R; gr_P; gr_U];
+    !constants
+  else
+    !constants
+
+let c_H () =
+  match collect_constants () with
+    it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of pack"
+
+let c_M () =
+  match collect_constants () with
+    _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of pack_marker"
+
+let c_R () =
+  match collect_constants () with
+    _ :: _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of pair"
+
+let c_P () =
+  match collect_constants () with
+    _ :: _ :: _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of prod"
+
+let c_U () =
+  match collect_constants () with
+    _ :: _ :: _ :: _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of prod"
+
+(* The following tactic is meant to pack an hypothesis when no other
+   data is already packed.
+
+   The main difficulty in defining this tactic is to understand how to
+   construct the input expected by apply_in. *)
+let package i = Goal.enter begin fun gl ->
+  Tactics.apply_in true false i
+   [(* this means that the applied theorem is not to be cleared. *)
+    None, (CAst.make (c_M (),
+           (* we don't specialize the theorem with extra values. *)
+           Tactypes.NoBindings))]
+     (* we don't destruct the result according to any intro_pattern *)
+    None
+  end
+
+(* This function is meant to observe a type of shape (f a)
+   and return the value a.  *)
+
+(* Remark by Maxime: look for destApp combinator. *)
+let unpack_type evd term =
+  let report () =
+    CErrors.user_err (Pp.str "expecting a packed type") in
+  match EConstr.kind evd term with
+  | Constr.App (_, [| ty |]) -> ty
+  | _ -> report ()
+
+(* This function is meant to observe a type of shape
+   A -> pack B -> C and return A, B, C
+  but it is not used in the current version of our tactic.
+  It is kept as an example. *)
+let two_lambda_pattern evd term =
+  let report () =
+    CErrors.user_err (Pp.str "expecting two nested implications") in
+(* Note that pattern-matching is always done through the EConstr.kind function,
+   which only provides one-level deep patterns. *)
+  match EConstr.kind evd term with
+  (* Here we recognize the outer implication *)
+  | Constr.Prod (_, ty1, l1) ->
+      (* Here we recognize the inner implication *)
+      (match EConstr.kind evd l1 with
+      | Constr.Prod (n2, packed_ty2, deep_conclusion) ->
+        (* Here we recognized that the second type is an application *)
+        ty1, unpack_type evd packed_ty2, deep_conclusion
+      | _ -> report ())
+  | _ -> report ()
+
+(* In the environment of the goal, we can get the type of an assumption
+  directly by a lookup.  The other solution is to call a low-cost retyping
+  function like *)
+let get_type_of_hyp env id =
+  match EConstr.lookup_named id env with
+  | Context.Named.Declaration.LocalAssum (_, ty) -> ty
+  | _ -> CErrors.user_err (let open Pp in
+                             str (Names.Id.to_string id) ++
+                             str " is not a plain hypothesis")
+
+let repackage i h_hyps_id = Goal.enter begin fun gl ->
+    let env = Goal.env gl in
+    let evd = Tacmach.New.project gl in
+    let concl = Tacmach.New.pf_concl gl in
+    let (ty1 : EConstr.t) = get_type_of_hyp env i in
+    let (packed_ty2 : EConstr.t) = get_type_of_hyp env h_hyps_id in
+    let ty2 = unpack_type evd packed_ty2 in
+    let new_packed_type = EConstr.mkApp (c_P (), [| ty1; ty2 |]) in
+    let open EConstr in
+    let new_packed_value =
+        mkApp (c_R (), [| ty1; ty2; mkVar i;
+          mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in
+    Refine.refine ~typecheck:true begin fun evd ->
+      let evd, new_goal = Evarutil.new_evar env evd
+          (mkProd (Names.Name.Anonymous,
+                     mkApp(c_H (), [| new_packed_type |]),
+                       Vars.lift 1 concl)) in
+        evd, mkApp (new_goal,
+                 [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |])
+      end
+    end
+
+let pack_tactic i =
+  let h_hyps_id = (Names.Id.of_string "packed_hyps") in
+  Proofview.Goal.enter begin fun gl ->
+    let hyps = Environ.named_context_val (Proofview.Goal.env gl) in
+    if not (Termops.mem_named_context_val i hyps) then
+      (CErrors.user_err
+          (Pp.str ("no hypothesis named" ^ (Names.Id.to_string i))))
+    else
+      if Termops.mem_named_context_val h_hyps_id hyps then
+          tclTHEN (repackage i h_hyps_id)
+            (tclTHEN (Tactics.clear [h_hyps_id; i])
+               (Tactics.introduction h_hyps_id))
+      else
+        tclTHEN (package i)
+          (tclTHEN (Tactics.rename_hyp [i, h_hyps_id])
+             (Tactics.move_hyp h_hyps_id Logic.MoveLast))
+    end
diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli b/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli
new file mode 100644
index 0000000000..dbf6cf48e2
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli
@@ -0,0 +1,3 @@
+val two_lambda_pattern :
+    Evd.evar_map -> EConstr.t -> EConstr.t * EConstr.t * EConstr.t
+val pack_tactic : Names.Id.t -> unit Proofview.tactic