1 files changed, 279 insertions, 0 deletions
diff --git a/hol-light/TacticRecording/hiproofs.ml b/hol-light/TacticRecording/hiproofs.ml
new file mode 100644
index 00000000..b48dd2da
--- /dev/null
+++ b/hol-light/TacticRecording/hiproofs.ml
@@ -0,0 +1,279 @@
+(* ========================================================================== *)
+(* HIPROOFS (HOL LIGHT)                                                       *)
+(* - Hiproofs and refactoring operations                                      *)
+(*                                                                            *)
+(* By Mark Adams                                                              *)
+(* Copyright (c) Univeristy of Edinburgh, 2012                                *)
+(* ========================================================================== *)
+
+
+(* This file defines a hiproof [1] datatype and various operations on it.     *)
+(* The datatype closely resembles that proposed in [2], with the notable      *)
+(* difference that atomic steps carry their arity.                            *)
+
+(* [1] "Hiproofs: A Hierarchical Notion of Proof Tree", Denney, Power &       *)
+(*    Tourlas, 2006.                                                          *)
+(* [2] "A Tactic Language for Hiproofs", Aspinall, Denney & Luth, 2008.       *)
+
+
+
+(* ** DATATYPE ** *)
+
+
+(* Hiproof datatype *)
+
+(* Note that atomic tactics are labelled with their arity, corresponding to   *)
+(* how many subgoals they result in.  An arity of -1 indicates unknown, and 0 *)
+(* indicates a tactic that completes its goal.                                *)
+
+type hiproof =
+    Hactive                             (* Active subgoal *)
+  | Hatomic of (finfo * int)            (* Atomic tactic + arity *)
+  | Hidentity                           (* Null, for wiring *)
+  | Hlabelled of (finfo * hiproof)      (* Box *)
+  | Hsequence of (hiproof * hiproof)    (* Serial application *)
+  | Htensor of hiproof list             (* Parallel application *)
+  | Hempty;;                            (* Completed goal *)
+
+
+(* Constructors and destructors *)
+
+let hsequence (h1,h2) = Hsequence (h1,h2);;
+
+let dest_hsequence h =
+  match h with
+    Hsequence hh -> hh
+  | _   -> failwith "Not a sequence hiproof";;
+
+let is_hsequence h = can dest_hsequence h;;
+
+let dest_atomic_hiproof h =
+  match h with
+    Hatomic (info,n) -> (info,n)
+  | _ -> failwith "dest_atomic_hiproof: Not an atomic hiproof";;
+
+
+(* Arity *)
+
+let rec hiproof_arity h =
+  match h with
+    Hactive           -> 1
+  | Hatomic (_,n)     -> n
+  | Hidentity         -> 1
+  | Hlabelled (_,h0)  -> hiproof_arity h0
+  | Hsequence (h1,h2) -> hiproof_arity h2
+  | Htensor hs        -> sum (map hiproof_arity hs)
+  | Hempty            -> 0;;
+
+
+(* Hitrace *)
+
+type hitrace =
+   Hicomment of int list
+ | Hiproof of hiproof;;
+
+
+
+(* ** REFACTORING OPERATIONS ** *)
+
+
+(* Generic refactoring operation *)
+
+(* Applies a refactoring function 'foo' at every level of hiproof 'h', from   *)
+(* bottom up.  If the 'r' flag is set then refactoring is repeated bottom up  *)
+(* whenever 'foo' makes a change.  Note that if 'foo' makes no change then it *)
+(* should just return its input hiproof (rather than raise an exception).     *)
+
+let rec refactor_hiproof r foo h =
+  let h' =
+     match h with
+       Hlabelled (info,h0)
+          -> let h0' = refactor_hiproof r foo h0 in
+             Hlabelled (info,h0')
+     | Hsequence (h1,h2)
+          -> let h1' = refactor_hiproof r foo h1 in
+             let h2' = refactor_hiproof r foo h2 in
+             Hsequence (h1',h2')
+     | Htensor hs
+          -> let hs' = map (refactor_hiproof r foo) hs in 
+             Htensor hs'
+     | _  -> h in
+  let h'' = if (h' = h) then h else h' in
+  let h''' = foo h'' in
+  if r & not (h''' = h'')
+    then refactor_hiproof r foo h'''
+    else h''';;
+
+
+(* Trivial simplification *)
+
+(* Removes basic algebraic identities/zeros.                                  *)
+
+let collapse_tensor h hs =
+  match h with
+    Hempty      -> hs
+  | Htensor hs0 -> hs0 @ hs
+  | _           -> h :: hs;;
+
+let trivsimp_hiproof h =
+  let trivsimp h =
+     match h with
+       Hatomic ((Some"ALL_TAC",[]), _) -> Hidentity
+     | Hsequence (h1, Hempty)    -> h1
+     | Hsequence (h1, Hidentity) -> h1
+     | Hsequence (Hidentity, h2) -> h2
+     | Htensor []    -> Hempty
+     | Htensor [h0]  -> h0
+     | Htensor hs0   -> if (forall (fun h0 -> h0 = Hidentity) hs0)
+                          then Hidentity
+                          else Htensor (foldr collapse_tensor hs0 [])
+     | _   -> h in
+  refactor_hiproof true trivsimp h;;
+
+
+(* Matching up lists of hiproofs *)
+
+let rec matchup_hiproofs hs1 hs2 =
+  match hs1 with
+    [] -> []
+  | h1::hs01
+       -> let n1 = hiproof_arity h1 in
+          let (hs2a,hs2b) = try chop_list n1 hs2
+                with Failure _ ->
+                     if (n1 = -1)
+                       then failwith "matchup_hiproofs: unknown arity"
+                       else failwith "matchup_hiproofs: Internal error - \
+                                                      inconsistent arities" in
+          Hsequence (h1, Htensor hs2a) :: (matchup_hiproofs hs01 hs2b);;
+
+
+(* Separating out lists of hiproofs *)
+
+let separate_hiproofs0 h (hs01,hs02) =
+  match h with
+    Hsequence (h1,h2)
+       -> (h1::hs01, h2::hs02)
+  | _  -> let n = hiproof_arity h in
+          let h2 = Htensor (copy n Hidentity) in
+          (h::hs01, h2::hs02);;
+
+let separate_hiproofs hs = foldr separate_hiproofs0 hs ([],[]);;
+
+
+(* Delabelling *)
+
+(* Strips out any boxes from the proof.  Note that some boxes, such as        *)
+(* 'SUBGOAL_THEN', cannot be stripped out without spoiling the proof, and so  *)
+(* are left alone.                                                            *)
+
+let delabel_hiproof h =
+  let delabel h =
+     match h with
+       Hlabelled ((Some "SUBGOAL_THEN",_),h0)
+          -> h
+     | Hlabelled (_,h0)
+          -> h0
+     | _  -> h in
+  refactor_hiproof true delabel h;;
+
+
+(* Right-grouping *)
+
+(* Expands the proof into a right-associative sequence, with tensor           *)
+(* compounding on the right.  Leaves all boxes unchanged.                     *)
+
+let rightgroup_hiproof h =
+  let rightgroup h =
+     match h with
+       Hsequence (Hsequence (h1, Htensor hs2), Htensor hs3)
+          -> Hsequence (h1, Htensor (matchup_hiproofs hs2 hs3))
+     | Hsequence (Hsequence (h1, Htensor hs2), h3)
+          -> Hsequence (h1, Htensor (matchup_hiproofs hs2 [h3]))
+     | _  -> h in
+  refactor_hiproof true rightgroup h;;
+
+
+(* Left-grouping *)
+
+(* Expands the proof into a left-associative sequence.                        *)
+
+let leftgroup_hiproof h =
+  let leftgroup h =
+     match h with
+       Hsequence (h1, Hsequence (h2, h3))
+          -> Hsequence (Hsequence (h1,h2), h3)
+(*     | Hsequence (h1, Htensor hs2)
+          -> if (exists is_hsequence hs2)
+               then let (hs2a,hs2b) = separate_hiproofs hs2 in
+                    Hsequence (Hsequence (h1, Htensor hs2a), Htensor hs2b)
+               else h  *)
+     | _  -> h in
+  refactor_hiproof true leftgroup h;;
+
+
+(* THEN insertion *)
+
+(* Looks for opportunities to use 'THEN' tacticals.  Note that this disrupts  *)
+(* arity consistency.                                                         *)
+
+let thenise_hiproof h =
+  let thenise h =
+     match h with
+       Hsequence (h1, Htensor (h2::h2s))
+          -> if (forall (fun h0 -> h0 = h2) h2s)
+               then Hlabelled ((Some "THEN", []), h)
+               else h
+     | Hsequence (h1, Hsequence (Htensor (h2::h2s), h3))
+          -> if (forall (fun h0 -> h0 = h2) h2s)
+               then Hsequence
+                     (Hlabelled ((Some "THEN", []),
+                                 Hsequence (h1, Htensor (h2::h2s))), h3)
+               else h
+     | _  -> h in
+  refactor_hiproof false thenise h;;
+
+
+
+(* ** OTHER OPERATIONS ** *)
+
+
+(* Tactic trace *)
+
+(* Gives a trace of the basic tactics used in the proof, ignoring how they    *)
+(* were combined by tacticals.                                                *)
+
+let rec hiproof_tactic_trace0 h =
+  match h with
+    Hactive
+       -> [active_info]
+  | Hatomic (info, _)
+       -> [info]
+  | Hidentity
+       -> []
+  | Hlabelled (info,h0)
+       -> hiproof_tactic_trace0 h0
+  | Hsequence (h1,h2)
+       -> (hiproof_tactic_trace0 h1) @ (hiproof_tactic_trace0 h2)
+  | Htensor hs
+       -> flat (map hiproof_tactic_trace0 hs)
+  | Hempty
+       -> [];;
+
+let hiproof_tactic_trace h = (hiproof_tactic_trace0 o delabel_hiproof) h;;
+
+
+(* Block trace *)
+
+(* Gives a trace of the hiproofs used in the proof, stopping at boxes.        *)
+
+let rec hiproof_block_trace0 ns0 h =
+  match h with
+  | Hsequence (h1,h2)
+       -> (hiproof_block_trace0 ns0 h1) @ (hiproof_block_trace0 ns0 h2)
+  | Htensor hs
+       -> let nss = map (fun n -> ns0 @ [n]) (1 -- length hs) in
+          flat (map (fun (ns,h) -> (Hicomment ns) :: hiproof_block_trace0 ns h)
+                    (zip nss hs))
+  | _  -> [Hiproof h];;
+
+let hiproof_block_trace h = hiproof_block_trace0 [] h;;