Ltac2 version of Especialize

LibHyps/LibHyps.v

@@ -9,6 +9,34 @@ Require Export LibHyps.LibHypsTactics.
 (* We export ; { } etc. ";;" also. *)
 
 
+Ltac rename_or_revert H := autorename_strict H + revert dependent H.
+
+(* Some usual tactics one may want to use on new hyps. *)
+
+(* This is similar to subst x, but ensures that H and only H is used.
+   Even if there is another hyp with the same variable *)
+Ltac substHyp H :=
+  match type of H with
+  (* | Depl => fail 1 (* fail immediately, we are applying on a list of hyps. *) *)
+  | ?x = ?y =>
+    (* subst would maybe subst using another hyp, so use replace to be sure *)
+    once ((is_var(x); replace x with y in *; [try clear x ; try clear H] )
+          + (is_var(y); replace y with x in * ; [try clear y; try clear H]))
+  | _ => idtac
+  end.
+
+(* revert, fails if impossible, should not fail if hyps are ordered in the right order *)
+Ltac revertHyp H := revert H. (* revert is a tactic notation, so we need to define this *)
+
+(* revert if subst fails. Never fail, be careful not to use this tactic in the
+   left member of a "+" tactical: *)
+Ltac subst_or_revert H := try first [progress substHyp H | generalize dependent H].
+
+(* try subst. Never fail, be careful to not use this tactic in the
+   left member of a "+" tactical: *)
+Ltac subst_or_idtac H := substHyp H.
+
+
 Export TacNewHyps.Notations.
 
 (* There are three variants of the autorename tatic, depending on what
@@ -27,11 +55,16 @@ Tactic Notation (at level 4) "/" "n?" := (onAllHyps rename_or_revert).
 Tactic Notation (at level 4) tactic4(Tac) "/" "r" := Tac ; {< revertHyp }.
 Tactic Notation (at level 4) "/" "r" := (onAllHypsRev revertHyp).
 
+Tactic Notation (at level 4) tactic4(Tac) "/" "g" := Tac ; { move_up_types }.
+(* Tactic Notation (at level 4) tactic4(Tac) "/" "g" := Tac ; {! group_up_list }. *)
+(*
 (* WARNING group_up_list applies to the whole list of hyps directly. *)
 (* Tactic Notation (at level 4) tactic4(Tac) "/" "g" := (then_allnh Tac group_up_list). *)
-Tactic Notation (at level 4) tactic4(Tac) "/" "g" := Tac ; {! group_up_list }.
-Tactic Notation (at level 4) "/" "g" := (group_up_list all_hyps).
+(* Tactic Notation (at level 4) tactic4(Tac) "/" "g" := Tac ; {! group_up_list }. *)
 
+(* Not yet reimplemented in ltac2 *)
+Tactic Notation (at level 4) "/" "g" := (group_up_list all_hyps).
+*)
 (* Tactic Notation (at level 4) tactic4(Tac) "/" "s" := (then_eachnh Tac subst_or_idtac). *)
 Tactic Notation (at level 4) tactic4(Tac) "/" "s" := Tac ; { subst_or_idtac }.
 Tactic Notation (at level 4) "/" "s" := (onAllHyps subst_or_idtac).
@@ -46,11 +79,11 @@ Tactic Notation (at level 4) tactic4(Tac) "/" "sg" := (Tac /s/g).
 Tactic Notation (at level 4) tactic4(Tac) "/" "ng" := (Tac /n/g).
 Tactic Notation (at level 4) tactic4(Tac) "/" "gn" := (Tac /g/n).
 
-Tactic Notation (at level 4) "/" "sng" :=
-  (onAllHyps subst_or_idtac); (onAllHyps autorename); group_up_list all_hyps.
+(* Tactic Notation (at level 4) "/" "sng" := *)
+  (* (onAllHyps subst_or_idtac); (onAllHyps autorename); group_up_list all_hyps. *)
 Tactic Notation (at level 4) "/" "sn" := (onAllHyps subst_or_idtac); (onAllHyps autorename).
 Tactic Notation (at level 4) "/" "sr" := (onAllHyps subst_or_idtac); (onAllHyps revertHyp).
-Tactic Notation (at level 4) "/" "ng" := ((onAllHyps autorename) ; group_up_list all_hyps).
+Tactic Notation (at level 4) "/" "ng" := ((onAllHyps autorename) ; (onAllHyps move_up_types) ).
 
 Module LegacyNotations.
   Import Notations.
@@ -85,49 +118,50 @@ Goal forall x1 x3:bool, forall a z e : nat,
 Proof.
   (* Set Ltac Debug. *)
   (* then_nh_rev ltac:(intros) ltac:(subst_or_idtac).   *)
-  intros ; {! group_up_list }.
+  (* intros ; {! group_up_list }. *)
 
   (* intros ? ? ? ? ? ? ? ? ? ?. *)
   (* group_up_list (DCons bool b1 DNil). *)
-  Undo.
-  intros ; { move_up_types }.
-  Undo.
+  (* Undo. *)
+  (* intros ; { move_up_types }. *)
+  (* Undo. *)
   intros /n.
   Undo.
   intros /s/n.
   Undo.
   intros /n.
-  match goal with
-  | h: bool => assert 
-  end
-  Undo.
-  intros/n.
   Undo.
-  intros ; { autorename }; {! group_up_list }.
+  intros ; { autorename }. (*; {! group_up_list }.*)
   Undo.
-  intros/ng.
+  (* intros/ng. *)
+  (* Undo. *)
+  intros ; {subst_or_idtac} ; { autorename }. (* ; {! group_up_list }.*)
   Undo.
-  intros ; {subst_or_idtac} ; { autorename } ; {! group_up_list }.
-  Undo.
-  intros/sng.
-  Fail progress intros ; { revertHyp }.
+  (* intros/sng. *)
+  (* Fail progress intros ; { revertHyp }. *)
 
-  subst_or_idtac (DCons (z0 + r = a) H DNil).
+  (* subst_or_idtac (DCons (z0 + r = a) H DNil). *)
 
 
-  let hyps := all_hyps in
-  idtac hyps.
-  subst_or_idtac hyps.
+  (* let hyps := all_hyps in *)
+  (* idtac hyps. *)
+  (* subst_or_idtac hyps. *)
 
-  intros  ;!;  ltac:(subst_or_idtac_l).
+  (* intros  ;!;  ltac:(subst_or_idtac_l). *)
 
-  then_nh_one_by_one ltac:(intros) ltac:(subst_or_idtac).  
-; {< subst_or_idtac }. ; { group_up_list } ; { autorename_l }.
-  subst_or_idtac h_eq_a_add_z0_t.
-  intros ; { fun h => autorename_strict h }.
+  (* then_nh_one_by_one ltac:(intros) ltac:(subst_or_idtac).   *)
+(* ; {< subst_or_idtac }. ; { group_up_list } ; { autorename_l }. *)
+  (* subst_or_idtac h_eq_a_add_z0_t. *)
+  Fail (intros ; { fun h => autorename_strict h }).
+  intros ; { fun h => autorename_orelse_revert h }.
+  match goal with
+  | |- (fun _ : bool => z = e) true -> True => idtac
+  end.
+  Undo 2.
   intros ; { fun h => idtac h }.
+  Undo.
   intros ; { ltac:(fun h => idtac h) }.
-   intros ; [H: sng H].
+
 *)   
 (*
 Goal forall x1 x3:bool, True -> forall a z e r t z e r t z e r t z e r t y: nat, False -> forall u i o p q s d f g:nat, forall x2:bool,  True -> True.

LibHyps/LibHypsDebug.v

@@ -0,0 +1,58 @@
+Require Import Ltac2.Ltac2.
+From Ltac2 Require Import Option Constr Printf.
+
+(* debug *)
+(*
+Require LibHyps.LibHypsTactics.
+Module Prgoal_Notation.
+  Ltac pr_goal :=
+    match goal with
+      |- ?g =>
+        let allh := LibHyps.TacNewHyps.harvest_hyps LibHyps.TacNewHyps.revert_clearbody_all in
+        (* let allh := all_hyps in *)
+        idtac "GOAL: " allh " ⊢ " g
+    end.
+End Prgoal_Notation.
+*)
+
+Ltac2 tag_info s := (String.concat "" [ "<infomsg>"; s; "</infomsg>" ]).
+Ltac2 tag_msg m := Message.concat
+                     (Message.concat (Message.of_string "<infomsg>") m)
+                     (Message.of_string "</infomsg>").
+Ltac2 str_to_msg s := tag_msg (Message.of_string s).
+Ltac2 int_to_msg i := tag_msg (Message.of_int i).
+Ltac2 id_to_msg id := tag_msg (Message.of_ident id).
+Ltac2 constr_to_msg c := tag_msg (Message.of_constr c).
+
+Ltac2 msgm m := Message.print (tag_msg m).
+Ltac2 msgs s := Message.print (str_to_msg s).
+Ltac2 msgi i := Message.print (int_to_msg i).
+Ltac2 msgc c := Message.print (constr_to_msg c).
+Ltac2 msgid id := Message.print (id_to_msg id).
+
+Ltac2 pr_list (pr: unit -> 'a -> message) () (l: 'a list) : message :=
+  let rec pr_list_  () (l: 'a list) :=
+    match l with
+    | [] => fprintf ""
+    | [e] => fprintf "%a" pr e
+    | e::l' => fprintf "%a , %a" pr e pr_list_ l'
+    end in
+  fprintf "[ %a ]" pr_list_ l.
+
+
+Ltac2 pr_binder () (b:binder):message :=
+  let nme:ident option := Binder.name b in
+  let typ:constr := Binder.type b in
+  fprintf "(%I:%t)" (Option.get nme) typ.
+
+Ltac2 pr_string () (s:string): message := fprintf "%s" s.
+
+Ltac2 pr_goal() :=
+  let l := Control.hyps() in
+  printf "<infomsg> Goal:";
+  List.iter (fun (nme,_,typ) => printf "%I : %t" nme typ) l;
+  printf "⊢ %t" (Control.goal());
+  printf "</infomsg>".
+
+Ltac2 pr_acc () (acc:string list) :=
+  fprintf "[%a]" (pr_list pr_string) acc.