5 files changed, 168 insertions, 39 deletions

diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
index a4095ae2e7..8b123eb7b0 100644
--- a/tuto3/src/g_tuto3.ml4
+++ b/tuto3/src/g_tuto3.ml4
@@ -1,7 +1,6 @@
 DECLARE PLUGIN "tuto3_plugin"
 
 open Ltac_plugin
-open Pp
 
 open Construction_game
 
@@ -24,15 +23,20 @@ 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
 
-TACTIC EXTEND collapse_hyps
-| [ "hide" "hypothesis" ident(i) ] ->
-  [ Tuto_tactic.hide_tactic i ]
-END
\ No newline at end of file
diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml
index a0ac967731..fbb6863f7e 100644
--- a/tuto3/src/tuto_tactic.ml
+++ b/tuto3/src/tuto_tactic.ml
@@ -2,15 +2,21 @@ 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 Universes in
-    let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "hide" in
-    let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "hide_marker" 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_global x))
-      [gr_H; gr_M];
+      [gr_H; gr_M; gr_R; gr_P; gr_U];
     !constants
   else
     !constants
@@ -18,35 +24,109 @@ let collect_constants () =
 let c_H () =
   match collect_constants () with
     it :: _ -> it
-  | _ -> failwith "could not obtain an internal representation of hide"
+  | _ -> 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 hide_marker"
+  | _ -> 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
-   [None, (CAst.make (c_M (), Misctypes.NoBindings))] None
+   [(* 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. *)
+           Misctypes.NoBindings))]
+     (* we don't destruct the result according to any intro_pattern *)
+    None
   end
-(*
-let package i = Goal.enter begin fun gl ->
-    let h_hyps_id = (Names.Id.of_string "hidden_hyps") in
+
+(* 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 store = Goal.extra gl in
-    let concl = Tacmach.New.pf_concl in
-    
-    let ty_i = ... in
-    let ev = Evarutil.new_evar in
-    mkApp (mkLambda(h_hyps_id, mkApp(c_h, [|ty_i|] , ev),
-           [| mkApp (c_hm, [| ty_ev; EConstr.mkVar i |]) |])
-end
- *)
-
-let repackage _ = failwith "todo"
-
-let hide_tactic i =
-  let h_hyps_id = (Names.Id.of_string "hidden_hyps") 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 ~store
+          (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
@@ -54,9 +134,11 @@ let hide_tactic i =
           (Pp.str ("no hypothesis named" ^ (Names.Id.to_string i))))
     else
       if Termops.mem_named_context_val h_hyps_id hyps then
-          tclTHEN (Tactics.revert [i; h_hyps_id]) (repackage ())
+          tclTHEN (repackage i h_hyps_id)
+            (tclTHEN (Tactics.clear [h_hyps_id; i])
+               (Tactics.introduction h_hyps_id))
       else
-        package i
+        tclTHEN (package i)
+          (tclTHEN (Tactics.rename_hyp [i, h_hyps_id])
+             (Tactics.move_hyp h_hyps_id Misctypes.MoveLast))
     end
-      
-      
diff --git a/tuto3/src/tuto_tactic.mli b/tuto3/src/tuto_tactic.mli
index 13f905ed8a..dbf6cf48e2 100644
--- a/tuto3/src/tuto_tactic.mli
+++ b/tuto3/src/tuto_tactic.mli
@@ -1 +1,3 @@
-val hide_tactic : Names.Id.t -> unit Proofview.tactic
+val two_lambda_pattern :
+    Evd.evar_map -> EConstr.t -> EConstr.t * EConstr.t * EConstr.t
+val pack_tactic : Names.Id.t -> unit Proofview.tactic
diff --git a/tuto3/theories/Data.v b/tuto3/theories/Data.v
index 4de0a9a0f9..0b07fee4f2 100644
--- a/tuto3/theories/Data.v
+++ b/tuto3/theories/Data.v
@@ -1,5 +1,18 @@
 Require Import ArithRing.
 
+Inductive pack (A: Type) : Type :=
+  packer : A -> pack A.
+
+Arguments packer {A}.
+
+Definition uncover (A : Type) (packed : pack A) : A :=
+  match packed with packer v => v end.
+
+Notation "!!!" := (pack _) (at level 0, only printing).
+
+(* The following data is used as material for automatic proofs
+  based on type classes. *)
+
 Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}.
 
 Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}.
@@ -12,6 +25,18 @@ Instance EvenNat_rec n (p : EvenNat n) : EvenNat (S (S n)) :=
 
 Definition tuto_div2 n (p : EvenNat n) := @half _ p.
 
+(* to be used in the following examples
+Compute (@half 8 _).
+
+Check (@half_prop 8 _).
+
+Check (@half_prop 7 _).
+
+and in command Tuto3_3 8. *)
+
+(* The following data is used as material for automatic proofs
+  based on canonical structures. *)
+
 Record S_ev n := Build_S_ev {double_of : nat; _ : 2 * n = double_of}.
 
 Definition s_half_proof n (r : S_ev n) : 2 * n = double_of n r :=
@@ -41,10 +66,3 @@ Check (C _ _ _ eq_refl : cmp 6 _).
 Check (C _ _ _ eq_refl : cmp 7 _).
 
 *)
-
-Inductive hide (A: Type) : Type :=
-  hide_marker : A -> hide A.
-
-Arguments hide_marker {A}.
-
-Notation "!!!" := (hide _) (at level 0, only printing).
\ No newline at end of file
diff --git a/tuto3/theories/test.v b/tuto3/theories/test.v
new file mode 100644
index 0000000000..43204ddf34
--- /dev/null
+++ b/tuto3/theories/test.v
@@ -0,0 +1,23 @@
+(* to be used e.g. in : coqtop -I src -R theories Tuto3 < theories/test.v *)
+
+Require Import Tuto3.Loader.
+
+(* This should print Type. *)
+Tuto3_1.
+
+(* This should print a term that contains an existential variable. *)
+(* And then print the same term, where the variable has been correctly
+   instantiated. *)
+Tuto3_2.
+
+Lemma tutu x y (A : 0 < x) (B : 10 < y) : True.
+Proof.
+pack hypothesis A.
+(* Hypothesis A should have disappeared and a "packed_hyps" hypothesis
+  should have appeared, with unreadable content. *)
+pack hypothesis B.
+(* Hypothesis B should have disappeared *)
+destruct packed_hyps as [unpacked_hyps].
+(* Hypothesis unpacked_hyps should contain the previous contents of A and B. *)
+exact I.
+Qed.