Various small improvements to capability

Whole of examples3 now processes
Facility for adding manual labels to atomic/composite tactics

1 files changed, 12 insertions, 158 deletions

diff --git a/hol-light/TacticRecording/tacticrec.ml b/hol-light/TacticRecording/tacticrec.ml
index 0836f87c..7df77fad 100644
--- a/hol-light/TacticRecording/tacticrec.ml
+++ b/hol-light/TacticRecording/tacticrec.ml
@@ -61,7 +61,7 @@ type ginfo =
 
 type gstep =
    Gatom of finfo                    (* Atomic tactic *)
- | Gbox of (finfo * gtree * bool)    (* Box for a tactical; flag for special *)
+ | Gbox of (label * gtree * bool)    (* Box for a tactical; flag for special *)
 
 and gtree0 =
    Gactive                                                (* Active goal *)
@@ -80,7 +80,7 @@ and gtree =
 (*                                                                            *)
 (*  (_, ref                                                                   *)
 (*   Gexecuted                                                                *)
-(*     (Gbox (Some "T1")                                                      *)
+(*     (Gbox (Tactical (Some "T1"))                                           *)
 (*        (_, ref                                                             *)
 (*         Gexecuted                                                          *)
 (*           (Gatom (Some "T2"),                                              *)
@@ -88,7 +88,7 @@ and gtree =
 (*              (_, ref Gexit _) ])),                                         *)
 (*      [ (_, ref                                                             *)
 (*         Gexecuted                                                          *)
-(*           (Gbox (Some "DP")                                                *)
+(*           (Gbox (Tactical (Some "DP"))                                     *)
 (*              (_, ref                                                       *)
 (*               Gexecuted                                                    *)
 (*                 (Gatom (Some "Normalise"),                                 *)
@@ -125,7 +125,8 @@ let gtree_fproof ((info,_):gtree) = ginfo_fproof info;;
 
 let gstep_tactic (gstp:gstep) =
   match gstp with
-    Gatom info | Gbox (info,_,_) -> info;;
+    Gatom info | Gbox (Tactical info, _, true) -> info
+  | Gbox _ -> failwith "gstep_tactic: Not an atomic tactic";;
 
 let gtree_proof ((_,gtrm):gtree) =
   match (!gtrm) with
@@ -206,8 +207,8 @@ let rec gtree_all_children gtr =
 
 and gstep_all_children gstp =
   match gstp with
-    Gbox (_,gtr,false) -> gtr::(gtree_all_children gtr)
-  | Gatom _ | Gbox _   -> [];;
+    Gatom _ | Gbox (_,_,true) -> []
+  | Gbox (_,gtr,false)        -> gtr::(gtree_all_children gtr);;
 
 
 
@@ -243,9 +244,9 @@ let extend_gtree (pid:goalid) (gstp:gstep) (gs':goal list) : xgoal list =
            with Assert_failure _ ->
                    failwith "extend_gtree: Internal error - Not active" in
   let (ids',gtrs) = unzip (map (new_active_subgtree pid) gs') in
-  let gxs' = zip gs' ids' in
+  let xgs' = zip gs' ids' in
   (gtrm := Gexecuted (gstp,gtrs);
-   gxs');;
+   xgs');;
 
 
 (* Deletion *)
@@ -276,153 +277,6 @@ let externalise_gtree ((id0,id):goalid*goalid) : unit =
 
 
 
-(* ** WRAPPER FUNCTIONS ** *)
-
-(* These functions are for promoting existing tactics and tacticals.          *)
-
-
-(* Tactic wrapper *)
-
-(* This is for wrapping around a tactic, to promote it to work on xgoals and  *)
-(* incorporate the results into an existing gtree.                            *)
-
-let tactic_wrap0 finfo (tac:tactic) (gx:xgoal) : xgoalstate =
-  let (g,id) = dest_xgoal gx in
-  let (meta,gs',just) = tac g in
-  let gxs' = extend_gtree id (Gatom finfo) gs' in
-  (meta,gxs',just);;
-
-let tactic_wrap x tac =
-  tactic_wrap0 (Some x, []) tac;;
-
-let string_tactic_wrap x (tac:string->tactic) (s:string) : xtactic =
-  tactic_wrap0 (Some x, [Fstring s]) (tac s);;
-
-let term_tactic_wrap x (tac:term->tactic) (tm:term) : xtactic =
-  tactic_wrap0 (Some x, [Fterm tm]) (tac tm);;
-
-let termpair_tactic_wrap x (tac:term*term->tactic) (tm1,tm2) : xtactic =
-  tactic_wrap0 (Some x, [Fpair (Fterm tm1, Fterm tm2)]) (tac (tm1,tm2));;
-
-let termlist_tactic_wrap x (tac:term list->tactic) tms : xtactic =
-  tactic_wrap0 (Some x, [Flist (map (fun tm -> Fterm tm) tms)]) (tac tms);;
-
-let thm_tactic_wrap x (tac:thm->tactic) (xth:xthm) : xtactic =
-  let (th,prf) = dest_xthm xth in
-  tactic_wrap0 (Some x, [Fthm prf]) (tac th);;
-
-let thmlist_tactic_wrap x (tac:thm list->tactic) (xths:xthm list) : xtactic =
-  let (ths,prfs) = unzip (map dest_xthm xths) in
-  tactic_wrap0 (Some x, [Flist (map (fun prf -> Fthm prf) prfs)]) (tac ths);;
-
-let stringthm_tactic_wrap x (tac:string->thm->tactic) s (xth:xthm) : xtactic =
-  let (th,prf) = dest_xthm xth in
-  tactic_wrap0 (Some x, [Fstring s; Fthm prf]) (tac s th);;
-
-
-(* xCONV_TAC - a special case I think; not a tactical *)
-
-let t_tm = `T`;;
-
-let xCONV_TAC (cx:xconv) (gx:xgoal) : xgoalstate =
-  let (g,id) = dest_xgoal gx in
-
-  let (asl,w) = g in
-  let thx = cx w in
-  let (th,proof) = dest_xthm thx in
-  let tm = concl th in
-  let finfo = (Some "CONV_TAC", [finfo_as_meta_arg proof]) in
-
-  let tac g =
-     if (aconv tm w)
-       then (null_meta, [], fun i [] -> INSTANTIATE_ALL i th)
-     else let l,r = dest_eq tm in
-       if not (aconv l w)
-       then failwith "CONV_TAC: bad equation"
-     else if (r = t_tm)
-       then (null_meta, [], fun i [] -> INSTANTIATE_ALL i (EQT_ELIM th))
-       else (null_meta, [(asl,r)],
-             fun i [th0] -> EQ_MP (INSTANTIATE_ALL i (SYM th)) th0) in
-
-  let (meta,gs,just) = tac g in
-  let gxs = extend_gtree id (Gatom finfo) gs in
-  (meta,gxs,just);;
-
-
-(* Tactical wrapper *)
-
-(* This is for wrapping around a tactical, to incorporate the results into a  *)
-(* box in an existing gtree, where the execution of the tactical's tactics is *)
-(* captured inside the box, so that they can be stepped through and/or        *)
-(* refactored.  Thus we cannot take the tactical as a black box; it must      *)
-(* already be promoted to work with xtactics and xgoals.  This must done by   *)
-(* hand for each tactical by trivially adjusting its original source code.    *)
-
-let tactical_wrap0 finfo (xttcl:'a->xtactic) (arg:'a) (gx:xgoal) : xgoalstate =
-  let (g,id) = dest_xgoal gx in
-  let (id0,gtr0) = new_active_subgtree id g in
-  let gx0 = mk_xgoal (g,id0) in
-  let (meta,gxs0,just) = xttcl arg gx0 in
-  let (gs0,ids0) = unzip (map dest_xgoal gxs0) in
-  let gxs = extend_gtree id (Gbox (finfo,gtr0,false)) gs0 in
-  let ids = map xgoal_id gxs in
-  (do_list externalise_gtree (zip ids0 ids);
-   (meta,gxs,just));;
-
-let tactical_wrap x (xttcl:'a->xtactic) (xtac:'a) : xtactic =
-  tactical_wrap0 (Some x, []) xttcl xtac;;
-
-let btactical_wrap x (xttcl:'a->'b->xtactic) (xtac1:'a) (xtac2:'b) : xtactic =
-  tactical_wrap0 (Some x, []) (xttcl xtac1) xtac2;;
-
-let int_tactical_wrap x (xttcl:int->'a->xtactic) (n:int) (xtac:'a) : xtactic =
-  tactical_wrap0 (Some x, [Fint n]) (xttcl n) xtac;;
-
-let list_tactical_wrap x (xttcl:('a->xtactic)->'a list->xtactic)
-                         (xtac:'a->xtactic) (l:'a list) : xtactic =
-  tactical_wrap0 (Some x, []) (xttcl xtac) l;;
-
-
-(* xSUBGOAL_THEN - seems to be another special case *)
-
-let xASSUME = conv_wrap "ASSUME" ASSUME;;
-
-let xSUBGOAL_THEN (tm:term) (ttac:xthm_tactic) (gx:xgoal) : xgoalstate =
-  let arg = xASSUME tm in
-
-  let (g,id) = dest_xgoal gx in
-  let (id0,gtr0) = new_active_subgtree id g in
-  let gx0 = mk_xgoal (g,id0) in
-  let (meta,gxs0,just) = ttac arg gx0 in
-  let (gs0,ids0) = unzip (map dest_xgoal gxs0) in
-
-  let (asl,_) = g in
-  let g2 = (asl,tm) in
-  let finfo = (Some "SUBGOAL_THEN",
-               [Fterm tm; (finfo_as_meta_arg o gtree_tactic) gtr0]) in
-
-  let gxs = extend_gtree id (Gbox (finfo,gtr0,true)) (g2::gs0) in
-  let ids1 = map xgoal_id (tl gxs) in
-  let just' = fun i l -> PROVE_HYP (hd l) (just i (tl l)) in
-  (do_list externalise_gtree (zip ids0 ids1);
-   (meta,gxs,just'));;
-
-
-(*
-let SUBGOAL_TAC s tm prfs =
-  match prfs with
-   p::ps -> (warn (ps <> []) "SUBGOAL_TAC: additional subproofs ignored";
-             SUBGOAL_THEN tm (LABEL_TAC s) THENL [p; ALL_TAC])
-  | [] -> failwith "SUBGOAL_TAC: no subproof given";;
-
-let (FREEZE_THEN :thm_tactical) =
-  fun ttac th (asl,w) ->
-    let meta,gl,just = ttac (ASSUME(concl th)) (asl,w) in
-    meta,gl,fun i l -> PROVE_HYP th (just i l);;
-*)
-
-
-
 (* ** SUBGOAL PACKAGE OPERATIONS FOR XGOALS ** *)
 
 (* A few of the xtactic subgoal package commands are adjusted here.           *)
@@ -470,12 +324,12 @@ let xg t =
 
 (* Undoing a tactic proof step *)
 
-(* 'xb' needs to be adjusted to deleted the undone step in the goal tree.     *)
+(* 'xb' needs to be adjusted to delete the undone step in the goal tree.      *)
 
 let xb () =
   let result = xb () in
-  let (_,gxs,_) = hd result in
-  let (_,id) = hd gxs in
+  let (_,xgs,_) = hd result in
+  let (_,id) = hd xgs in
   (delete_step id;
    result);;