Adds a tactic that hides the contents of an hypothesis from view

6 files changed, 77 insertions, 0 deletions

diff --git a/tuto3/_CoqProject b/tuto3/_CoqProject
index 23ba975de4..6a3c1978a7 100644
--- a/tuto3/_CoqProject
+++ b/tuto3/_CoqProject
@@ -4,6 +4,8 @@
 theories/Data.v
 theories/Loader.v
 
+src/tuto_tactic.ml
+src/tuto_tactic.mli
 src/construction_game.ml
 src/construction_game.mli
 src/g_tuto3.ml4
diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
index f028880087..a4095ae2e7 100644
--- a/tuto3/src/g_tuto3.ml4
+++ b/tuto3/src/g_tuto3.ml4
@@ -32,3 +32,7 @@ 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/tuto3_plugin.mlpack b/tuto3/src/tuto3_plugin.mlpack
index 3b6ce58e45..d6fc1d509a 100644
--- a/tuto3/src/tuto3_plugin.mlpack
+++ b/tuto3/src/tuto3_plugin.mlpack
@@ -1,2 +1,3 @@
 Construction_game
+Tuto_tactic
 G_tuto3
\ No newline at end of file
diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml
new file mode 100644
index 0000000000..a0ac967731
--- /dev/null
+++ b/tuto3/src/tuto_tactic.ml
@@ -0,0 +1,62 @@
+open Proofview
+
+let constants = ref ([] : EConstr.t list)
+
+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
+    constants := List.map (fun x -> of_constr (constr_of_global x))
+      [gr_H; gr_M];
+    !constants
+  else
+    !constants
+
+let c_H () =
+  match collect_constants () with
+    it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of hide"
+
+let c_M () =
+  match collect_constants () with
+    _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of hide_marker"
+
+let package i = Goal.enter begin fun gl ->
+  Tactics.apply_in true false i
+   [None, (CAst.make (c_M (), Misctypes.NoBindings))] None
+  end
+(*
+let package i = Goal.enter begin fun gl ->
+    let h_hyps_id = (Names.Id.of_string "hidden_hyps") in
+    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
+  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 (Tactics.revert [i; h_hyps_id]) (repackage ())
+      else
+        package i
+    end
+      
+      
diff --git a/tuto3/src/tuto_tactic.mli b/tuto3/src/tuto_tactic.mli
new file mode 100644
index 0000000000..13f905ed8a
--- /dev/null
+++ b/tuto3/src/tuto_tactic.mli
@@ -0,0 +1 @@
+val hide_tactic : Names.Id.t -> unit Proofview.tactic
diff --git a/tuto3/theories/Data.v b/tuto3/theories/Data.v
index b2afffed68..4de0a9a0f9 100644
--- a/tuto3/theories/Data.v
+++ b/tuto3/theories/Data.v
@@ -41,3 +41,10 @@ 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