Menu
▾
▴
[Hol-checkins] SF.net SVN: hol:[6467] HOL/examples/separationLogic/src
|
From: <th...@us...> - 2009-01-08 14:02:47
|
Revision: 6467
http://hol.svn.sourceforge.net/hol/?rev=6467&view=rev
Author: thtuerk
Date: 2009-01-08 14:02:20 +0000 (Thu, 08 Jan 2009)
Log Message:
-----------
general cleanup with lots of minor changes
Modified Paths:
--------------
HOL/examples/separationLogic/src/generalHelpersScript.sml
HOL/examples/separationLogic/src/smallfoot/examples.txt
HOL/examples/separationLogic/src/smallfoot/smallfootLib.sml
HOL/examples/separationLogic/src/smallfoot/smallfootScript.sml
HOL/examples/separationLogic/src/smallfoot/smallfootSyntax.sml
Modified: HOL/examples/separationLogic/src/generalHelpersScript.sml
===================================================================
--- HOL/examples/separationLogic/src/generalHelpersScript.sml 2009-01-08 13:56:56 UTC (rev 6466)
+++ HOL/examples/separationLogic/src/generalHelpersScript.sml 2009-01-08 14:02:20 UTC (rev 6467)
@@ -1500,6 +1500,19 @@
(LENGTH l1 = LENGTH l2)
`;
+
+val LIST_UNROLL_GIVEN_ELEMENT_NAMES_REWRITE = store_thm ("LIST_UNROLL_GIVEN_ELEMENT_NAMES_REWRITE",
+``(LIST_UNROLL_GIVEN_ELEMENT_NAMES [] []) /\
+ (LIST_UNROLL_GIVEN_ELEMENT_NAMES (x::xs) (y::ys) =
+ LIST_UNROLL_GIVEN_ELEMENT_NAMES xs ys) /\
+ ~(LIST_UNROLL_GIVEN_ELEMENT_NAMES [] (y::ys)) /\
+ ~(LIST_UNROLL_GIVEN_ELEMENT_NAMES (x::xs) [])``,
+
+SIMP_TAC list_ss [LIST_UNROLL_GIVEN_ELEMENT_NAMES_def]);
+
+
+
+
val LIST_UNROLL_GIVEN_ELEMENT_NAMES___UNROLL = store_thm ("LIST_UNROLL_GIVEN_ELEMENT_NAMES___UNROLL",
``(LIST_UNROLL_GIVEN_ELEMENT_NAMES x [] = (x = [])) /\
(LIST_UNROLL_GIVEN_ELEMENT_NAMES x (h::L) =
Modified: HOL/examples/separationLogic/src/smallfoot/examples.txt
===================================================================
--- HOL/examples/separationLogic/src/smallfoot/examples.txt 2009-01-08 13:56:56 UTC (rev 6466)
+++ HOL/examples/separationLogic/src/smallfoot/examples.txt 2009-01-08 14:02:20 UTC (rev 6467)
@@ -14,7 +14,7 @@
smallfootSyntax BoolExtractShared
ConseqConv smallfootTheory
smallfootParser
- smallfootLib
+ smallfootLib quantHeuristicsLib
@@ -292,33 +292,51 @@
temp_add_smallfoot_pp();
use_smallfoot_pretty_printer := true;
-val examplesDir = concat [Globals.HOLDIR, "/examples/separationLogic/src/smallfoot/EXAMPLES/"]
+val examplesDir = concat [Globals.HOLDIR, "/examples/separationLogic/src/smallfoot/EXAMPLES/"];
(* 16.0 s *) val file = concat [examplesDir, "mergesort.sf"];
val thm = smallfoot_verbose_auto_prove file;
+
(* 2.0 s *) val file = concat [examplesDir, "parallel_tree_deallocate.sf"];
val thm = smallfoot_verbose_auto_prove file;
+
(* 14.5 s *) val file = concat [examplesDir, "parallel_mergesort.sf"];
val thm = smallfoot_verbose_auto_prove file;
+
+
(* 43.5 s *) val file = concat [examplesDir, "list.sf"];
val thm = smallfoot_verbose_auto_prove file;
+
(* 9.5 s *) val file = concat [examplesDir, "tree.sf"];
val thm = smallfoot_verbose_auto_prove file;
+
+
(* 0.7 s *) val file = concat [examplesDir, "passive_stack_race.sf"]; (*semantics differs from smallfoot!*)
val thm = smallfoot_verbose_auto_prove file;
+
+
(* 2.3 s *) val file = concat [examplesDir, "business1.sf"];
val thm = smallfoot_verbose_auto_prove file;
+
+
(* 2.7 s *) val file = concat [examplesDir, "pointer_transferring_buffer.sf"];
val thm = smallfoot_verbose_auto_prove file;
+
(* 2.0 s *) val file = concat [examplesDir, "pointer_non_transferring_buffer.sf"];
val thm = smallfoot_verbose_auto_prove file;
+
(* 6.2 s *) val file = concat [examplesDir, "mm_buf.sf"];
val thm = smallfoot_verbose_auto_prove file;
+
(* 3.7 s *) val file = concat [examplesDir, "memory_manager.sf"];
val thm = smallfoot_verbose_auto_prove file;
+
+
(* 27.5 s *) val file = concat [examplesDir, "split_binary_semaphore.sf"];
val thm = smallfoot_verbose_auto_prove file;
+
+
(* 53.5 s *) val file = concat [examplesDir, "mm_non_blocking.sf"];
val thm = smallfoot_verbose_auto_prove file;
@@ -338,6 +356,7 @@
(*automatic proof just fails*)
val thm = smallfoot_auto_prove file;
+val _ = smallfoot_auto_prove file;
use_smallfoot_pretty_printer := false
@@ -346,21 +365,29 @@
set_goal([],parse_smallfoot_file file);
-
+use_smallfoot_pretty_printer := true
SMALLFOOT_SPECIFICATION_TAC THEN
REPEAT STRIP_TAC THEN
REPEAT SMALLFOOT_STEP_TAC
+SIMP_TAC std_ss [FORALL_AND_THM]
SMALLFOOT_MINI_STEP_TAC
-ESMALLFOOT_SOLVE_TAC
+SMALLFOOT_SOLVE_TAC
+
+SIMP_TAC std_ss [bagTheory.BAG_MERGE_EQNS]
+SIMP_TAC std_ss [asl_true_def, UNIV_DEF]
+asl_true_def
+REWRITE_TAC[]
+
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC
SMALLFOOT_NO_CASE_SPLIT_STEP_TAC
SMALLFOOT_NO_CASE_SPLIT_MINI_STEP_TAC
SMALLFOOT_PROP_IMPLIES___EQ_CASE_SPLIT_TAC
SMALLFOOT_STEP_TAC
-....
+....
+SMALLFOOT_CLEAN_TAC
REPEAT STRIP_TAC THEN
SMALLFOOT_STEP_TAC
@@ -392,8 +419,7 @@
(*enqueue need as little help*)
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
- SMALLFOOT_CLEAN_TAC THEN
- Q.EXISTS_TAC `r_const` THEN
+ QUANT_TAC [("b'", `r_const`,[])] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC,
(*works fine*)
@@ -401,6 +427,7 @@
(*works as well, but needs a case split*)
SMALLFOOT_SOLVE_TAC
+
]);
@@ -421,13 +448,11 @@
(*Handle procedures separately*)
REPEAT STRIP_TAC THENL [
- (*push works fine*)
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC,
(*enqueue need as little help*)
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
- SMALLFOOT_CLEAN_TAC THEN
- Q.EXISTS_TAC `r_const` THEN
+ QUANT_TAC [("b'", `r_const`, [])] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC,
(*works fine*)
@@ -438,10 +463,12 @@
]);
+
+
val examplesDir = concat [Globals.HOLDIR, "/examples/separationLogic/src/smallfoot/EXAMPLES/"]
val file = concat [examplesDir, "reverse_data.sf"];
@@ -449,7 +476,7 @@
val t = parse_smallfoot_file file
smallfoot_set_goal file;
-set_goal ([], t)
+set_goal ([], t);
SMALLFOOT_SPECIFICATION_TAC
(*or*)
@@ -457,27 +484,23 @@
(*Handle procedures separately*)
REPEAT STRIP_TAC THENL [
- (*push works fine*)
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
- REPEAT STRIP_TAC THEN
- Q.EXISTS_TAC `idata_hd::pdata` THEN
- Q.EXISTS_TAC `idata_tl` THEN
- ASM_SIMP_TAC list_ss [APPEND_ASSOC_CONS] THEN
+ QUANT_TAC [("pdata'", `idata_h::pdata`, []),
+ ("idata'", `idata_t`, [])] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC,
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
- REPEAT STRIP_TAC THEN
- Q.EXISTS_TAC `data` THEN
- REPEAT STRIP_TAC THEN
- Q.EXISTS_TAC `[]` THEN
- Q.EXISTS_TAC `data` THEN
+ QUANT_TAC [("data'", `data`, []),
+ ("pdata", `[]`, []),
+ ("idata", `data`, [])] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC
]);
+
open sortingTheory relationTheory
val examplesDir = concat [Globals.HOLDIR, "/examples/separationLogic/src/smallfoot/EXAMPLES/"]
@@ -487,6 +510,7 @@
parse_smallfoot_file file
smallfoot_set_goal file;
+SMALLFOOT_SPECIFICATION_TAC
@@ -500,18 +524,16 @@
CONJ_TAC THEN1 (
(*case q = NULL*)
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
- REPEAT STRIP_TAC THEN
- Q.EXISTS_TAC `pdata` THEN
- ASM_SIMP_TAC list_ss [PERM_REFL] THEN
+ QUANT_TAC [("rdata", `pdata`, [])] THEN
+ SIMP_TAC list_ss [PERM_REFL] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC
) THEN
SMALLFOOT_STEP_TAC THEN
CONJ_TAC THEN1 (
(*case p = NULL*)
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
- REPEAT STRIP_TAC THEN
- Q.EXISTS_TAC `qdata` THEN
- ASM_SIMP_TAC list_ss [PERM_REFL] THEN
+ QUANT_TAC [("rdata", `qdata`, [])] THEN
+ SIMP_TAC list_ss [PERM_REFL] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC
) THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
@@ -523,10 +545,10 @@
qdata' := tl qdata
To prove the precondition of merge,
one needs to infer that qdata' is sorted*)
- Q.EXISTS_TAC `pdata` THEN
- Q.EXISTS_TAC `qdata_tl` THEN
- `SORTED $<= (qdata_tl:num list)` by ALL_TAC THEN1 (
- Cases_on `qdata_tl` THEN
+ QUANT_TAC [("pdata'", `pdata_h::pdata_t`, []),
+ ("qdata'", `qdata_t`, [])] THEN
+ `SORTED $<= (qdata_t:num list)` by ALL_TAC THEN1 (
+ Cases_on `qdata_t` THEN
FULL_SIMP_TAC std_ss [SORTED_DEF]
) THEN
ASM_SIMP_TAC list_ss [] THEN
@@ -540,11 +562,11 @@
data is the sorted content of pdata and qdata_tl.
We then need to show that qdata_hd :: rdata is
sorted and contains the same elements as pdata, qdata.*)
- Q.EXISTS_TAC `qdata_hd::rdata` THEN
+ Q.EXISTS_TAC `qdata_h::rdata` THEN
ASM_SIMP_TAC list_ss [] THEN
- Tactical.REVERSE (`SORTED $<= (qdata_hd::rdata) /\
- PERM (pdata_hd::(pdata_tl ++ qdata_hd::qdata_tl))
- (qdata_hd::rdata)` by ALL_TAC) THEN1 (
+ Tactical.REVERSE (`SORTED $<= (qdata_h::rdata) /\
+ PERM (pdata_h::(pdata_t ++ qdata_h::qdata_t))
+ (qdata_h::rdata)` by ALL_TAC) THEN1 (
ASM_SIMP_TAC std_ss [] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC
) THEN
@@ -552,25 +574,24 @@
`transitive (($<=):num -> num -> bool)` by ALL_TAC THEN1 (
SIMP_TAC arith_ss [transitive_def]
) THEN
- Q.PAT_ASSUM `qdata = X` ASSUME_TAC THEN
FULL_SIMP_TAC list_ss [SORTED_EQ] THEN
REPEAT STRIP_TAC THEN
- `MEM y (pdata_hd::(pdata_tl ++ qdata_tl))` by METIS_TAC[PERM_MEM_EQ] THEN
+ `MEM y (pdata_h::(pdata_t ++ qdata_t))` by METIS_TAC[PERM_MEM_EQ] THEN
POP_ASSUM MP_TAC THEN
ASM_SIMP_TAC list_ss [DISJ_IMP_THM] THEN
REPEAT STRIP_TAC THEN
- `pdata_hd <= y` by RES_TAC THEN
+ `pdata_h <= y` by RES_TAC THEN
DECIDE_TAC,
Q.PAT_ASSUM `PERM X rdata` MP_TAC THEN
REPEAT (POP_ASSUM (K ALL_TAC)) THEN
- Tactical.REVERSE (`PERM (pdata_hd::(pdata_tl ++ qdata_hd::qdata_tl))
- (qdata_hd::pdata_hd::(pdata_tl ++ qdata_tl))` by ALL_TAC) THEN1 (
+ Tactical.REVERSE (`PERM (pdata_h::(pdata_t ++ qdata_h::qdata_t))
+ (qdata_h::pdata_h::(pdata_t ++ qdata_t))` by ALL_TAC) THEN1 (
PROVE_TAC[PERM_TRANS, PERM_MONO]
) THEN
- Tactical.REVERSE (`PERM (pdata_tl ++ qdata_hd::qdata_tl)
- (qdata_hd::(pdata_tl ++ qdata_tl))` by ALL_TAC) THEN1 (
+ Tactical.REVERSE (`PERM (pdata_t ++ qdata_h::qdata_t)
+ (qdata_h::(pdata_t ++ qdata_t))` by ALL_TAC) THEN1 (
PROVE_TAC[PERM_TRANS, PERM_MONO, PERM_SWAP_AT_FRONT, PERM_REFL]
) THEN
PROVE_TAC[CONS_PERM, PERM_REFL, PERM_SYM]
@@ -588,10 +609,10 @@
qdata' := qdata
To prove the precondition of merge,
one needs to infer that pdata' is sorted*)
- Q.EXISTS_TAC `pdata_tl` THEN
- Q.EXISTS_TAC `qdata` THEN
- `SORTED $<= (pdata_tl:num list)` by ALL_TAC THEN1 (
- Cases_on `pdata_tl` THEN
+ QUANT_TAC [("pdata'", `pdata_t`, []),
+ ("qdata'", `qdata_h::qdata_t`, [])] THEN
+ `SORTED $<= (pdata_t:num list)` by ALL_TAC THEN1 (
+ Cases_on `pdata_t` THEN
FULL_SIMP_TAC std_ss [SORTED_DEF]
) THEN
ASM_SIMP_TAC list_ss [] THEN
@@ -605,11 +626,11 @@
data is the sorted content of pdata_tl and qdata.
We then need to show that pdata_hd :: rdata is
sorted and contains the same elements as pdata, qdata.*)
- Q.EXISTS_TAC `pdata_hd::rdata` THEN
+ Q.EXISTS_TAC `pdata_h::rdata` THEN
ASM_SIMP_TAC list_ss [] THEN
- Tactical.REVERSE (`SORTED $<= (pdata_hd::rdata) /\
- PERM (pdata_hd::(pdata_tl ++ qdata_hd::qdata_tl))
- (pdata_hd::rdata)` by ALL_TAC) THEN1 (
+ Tactical.REVERSE (`SORTED $<= (pdata_h::rdata) /\
+ PERM (pdata_h::(pdata_t ++ qdata_h::qdata_t))
+ (pdata_h::rdata)` by ALL_TAC) THEN1 (
ASM_SIMP_TAC std_ss [] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC
) THEN
@@ -617,14 +638,13 @@
`transitive (($<=):num -> num -> bool)` by ALL_TAC THEN1 (
SIMP_TAC arith_ss [transitive_def]
) THEN
- Q.PAT_ASSUM `qdata = X` ASSUME_TAC THEN
FULL_SIMP_TAC list_ss [SORTED_EQ] THEN
REPEAT STRIP_TAC THEN
- `MEM y (pdata_tl ++ qdata_hd::qdata_tl)` by METIS_TAC[PERM_MEM_EQ] THEN
+ `MEM y (pdata_t ++ qdata_h::qdata_t)` by METIS_TAC[PERM_MEM_EQ] THEN
POP_ASSUM MP_TAC THEN
ASM_SIMP_TAC list_ss [DISJ_IMP_THM] THEN
REPEAT STRIP_TAC THEN
- `qdata_hd <= y` by RES_TAC THEN
+ `qdata_h <= y` by RES_TAC THEN
DECIDE_TAC,
@@ -642,10 +662,9 @@
CONJ_TAC THEN1 (
(*case p = NULL, both lists _pdata, _rdata are empty*)
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
- REPEAT STRIP_TAC THEN
- Q.EXISTS_TAC `[]` THEN
- Q.EXISTS_TAC `[]` THEN
- ASM_SIMP_TAC list_ss [PERM_REFL] THEN
+ QUANT_TAC [("rdata", `[]`, []),
+ ("pdata", `[]`, [])] THEN
+ SIMP_TAC list_ss [PERM_REFL] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC
) THEN
SMALLFOOT_STEP_TAC THEN
@@ -655,35 +674,31 @@
(*case t1 = NULL, this means a single element
and everything goes to _pdata*)
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
- REPEAT STRIP_TAC THEN
- Q.PAT_ASSUM `data = X` ASSUME_TAC THEN
- Q.EXISTS_TAC `[]` THEN
- Q.EXISTS_TAC `data` THEN
- ASM_SIMP_TAC list_ss [PERM_REFL] THEN
+ QUANT_TAC [("rdata", `[]`, []),
+ ("pdata", `[data_h]`, [])] THEN
+ SIMP_TAC list_ss [PERM_REFL] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC
) THEN
(* there are at least two elements *)
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
- REPEAT STRIP_TAC THEN
(*the data for the recursive call is the
original data without the first two entries*)
- Q.EXISTS_TAC `data_tl_tl` THEN
+ QUANT_TAC [("data'", `data_t_t`,[])] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
SMALLFOOT_CLEAN_TAC THEN
- REPEAT STRIP_TAC THEN
(*the resulting values for _pdata, _rdata in
the postcondition are the ones returned by
the recursive call with the two first
elements added again. It remains to be shown
that is really a permutation of the orginal data*)
- Q.EXISTS_TAC `data_tl_hd::rdata` THEN
- Q.EXISTS_TAC `data_hd::pdata` THEN
+ Q.EXISTS_TAC `data_t_h::rdata` THEN
+ Q.EXISTS_TAC `data_h::pdata` THEN
Tactical.REVERSE (
- `PERM (data_hd::(pdata ++ data_tl_hd::rdata))
- (data_hd::data_tl_hd::data_tl_tl)` by ALL_TAC) THEN1 (
+ `PERM (data_h::(pdata ++ data_t_h::rdata))
+ (data_h::data_t_h::data_t_t)` by ALL_TAC) THEN1 (
ASM_SIMP_TAC list_ss [] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC
) THEN
@@ -701,49 +716,40 @@
CONJ_TAC THEN1 (
(*case p = NULL*)
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
- REPEAT STRIP_TAC THEN
(*if the input is empty, then _rdata is empty as well*)
- Q.EXISTS_TAC `[]` THEN
+ QUANT_TAC [("rdata", `[]`, [])] THEN
ASM_SIMP_TAC std_ss [PERM_REFL, SORTED_DEF] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC
) THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
- REPEAT STRIP_TAC THEN
+
(*call of split, data passed is the original one*)
- Q.EXISTS_TAC `data` THEN
+ QUANT_TAC [("data'", `data`, [])] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
- SMALLFOOT_CLEAN_TAC THEN
- REPEAT STRIP_TAC THEN
(*first call to mergesort, data is the one
returned by split and stored in q*)
- Q.EXISTS_TAC `rdata` THEN
+ QUANT_TAC [("data'", `rdata`, [])] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
- SMALLFOOT_CLEAN_TAC THEN
- REPEAT STRIP_TAC THEN
(*second call to mergesort, data is the one
returned by split and stored in p*)
- Q.EXISTS_TAC `pdata` THEN
+ QUANT_TAC [("data'", `pdata`, [])] THEN
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
- SMALLFOOT_CLEAN_TAC THEN
- REPEAT STRIP_TAC THEN
(*call to mergesort, data is the sorted data from
before. Notice that it is sorted*)
- Q.EXISTS_TAC `rdata''` THEN
- Q.EXISTS_TAC `rdata'` THEN
- ASM_SIMP_TAC std_ss [] THEN
+ QUANT_TAC [("pdata", `rdata''`, []),
+ ("qdata", `rdata'`, [])] THEN
-
SMALLFOOT_NO_CASE_SPLIT_SOLVE_TAC THEN
SMALLFOOT_CLEAN_TAC THEN
- REPEAT STRIP_TAC THEN
+
(*show that the postcondition holds.
the data there is the one returned by merge*)
- Q.EXISTS_TAC `rdata'''` THEN
+ QUANT_TAC [("rdata'", `rdata'''`, [])] THEN
`PERM data rdata'''` by ALL_TAC THEN1 (
REPEAT (Q.PAT_ASSUM `PERM X Y` MP_TAC) THEN
@@ -764,14 +770,3 @@
-SMALLFOOT_SPECIFICATION_TAC
-
-SMALLFOOT_STEP_TAC THEN
-SMALLFOOT_MINI_STEP_TAC THEN
-REPEAT STRIP_TAC THEN
-
-use_smallfoot_pretty_printer := true
-SMALLFOOT_SOLVE_TAC THEN
-CONJ_TAC
-rotate 1
-
Modified: HOL/examples/separationLogic/src/smallfoot/smallfootLib.sml
===================================================================
--- HOL/examples/separationLogic/src/smallfoot/smallfootLib.sml 2009-01-08 13:56:56 UTC (rev 6466)
+++ HOL/examples/separationLogic/src/smallfoot/smallfootLib.sml 2009-01-08 14:02:20 UTC (rev 6467)
@@ -4,6 +4,7 @@
(*
quietdec := true;
loadPath :=
+ (concat [Globals.HOLDIR, "/src/quantHeuristics"]) ::
(concat [Globals.HOLDIR, "/examples/separationLogic/src"]) ::
(concat [Globals.HOLDIR, "/examples/separationLogic/src/smallfoot"]) ::
!loadPath;
@@ -15,9 +16,11 @@
show_assums := true;
*)
+
+
open HolKernel Parse boolLib bossLib
-open generalHelpersTheory
+open generalHelpersTheory quantHeuristicsLib
open finite_mapTheory relationTheory pred_setTheory congLib sortingTheory
listTheory rich_listTheory arithmeticTheory operatorTheory
optionTheory latticeTheory separationLogicTheory separationLogicLib
@@ -31,7 +34,72 @@
*)
+val time_ref = ref (Time.now());
+fun time_step_init () = time_ref := (Time.now());
+fun time_step m =
+ let
+ val d_time = Time.- (Time.now(), !time_ref);
+ val _ = print m;
+ val _ = print ": ";
+ val _ = print (Time.toString d_time);
+ val _ = print "\n";
+ in
+ ()
+ end;
+
+val time_ref = ref Time.zeroTime;
+
+fun time_start () = Time.now();
+
+fun time_stop t1 = let
+ val t2 = !time_ref
+ val d_time = Time.- (Time.now(), t1);
+ val t2 = Time.+ (d_time, t2);
+ in time_ref := t2 end;
+
+fun time_reset () = time_ref := Time.zeroTime
+
+fun time_print () = let
+ val t2 = !time_ref
+ val _ = print (Time.toString t2);
+ val _ = print " s\n";
+ in () end;
+
+
+
+fun timed_CONV (conv:Abbrev.conv) t = let
+ val c = time_start();
+ val thm = conv t;
+ val _ = time_stop c;
+in
+ thm
+end;
+
+
+fun timed_TAC (tac:Abbrev.tactic) x = let
+ val c = time_start();
+ val y = tac x;
+ val _ = time_stop c;
+in
+ y
+end;
+
+
+fun timed_ABSTRACTION_CONV conv sys xenv penv asm p =
+let
+ val c = time_start();
+ val y = conv sys xenv penv asm p;
+ val _ = time_stop c;
+in
+ y
+end
+
+
+
+
+
+
fun bag_el_conv conv n b =
let
val (insert_term, rest_term) = dest_comb b;
@@ -127,8 +195,6 @@
-
-
val LIST_UNROLL_GIVEN_ELEMENT_NAMES_term = ``LIST_UNROLL_GIVEN_ELEMENT_NAMES``;
fun LIST_UNROLL_GIVEN_ELEMENT_NAMES_CONV t =
@@ -201,9 +267,9 @@
(ISPECL [xenv,penv,t] FASL_PROGRAM_IS_ABSTRACTION___REFL)
fun FASL_PROGRAM_ABSTRACTION_CONV_int [] sys xenv penv asm p =
- ISPECL [xenv,penv,p] FASL_PROGRAM_IS_ABSTRACTION___REFL
+ NONE
| FASL_PROGRAM_ABSTRACTION_CONV_int (c1::L) sys xenv penv asm p =
- (c1 sys xenv penv asm p) handle UNCHANGED => FASL_PROGRAM_ABSTRACTION_CONV_int L sys xenv penv asm p;
+ SOME (c1 sys xenv penv asm p) handle UNCHANGED => FASL_PROGRAM_ABSTRACTION_CONV_int L sys xenv penv asm p;
@@ -612,7 +678,8 @@
val _ = if (is_smallfoot_prog_val_arg p) then () else raise UNCHANGED;
val (v,body,arg) = dest_smallfoot_prog_val_arg p;
- val b_thm = sys xenv penv asm body;
+ val b_thm_opt = sys xenv penv asm body;
+ val b_thm = if (isSome b_thm_opt) then valOf b_thm_opt else raise UNCHANGED;
val b_thm2 = GEN_ASSUM v b_thm;
val thm = ISPECL [xenv, penv, arg] FASL_PROGRAM_IS_ABSTRACTION___smallfoot_prog_val_arg;
@@ -626,7 +693,8 @@
let
val _ = if (is_smallfoot_prog_local_var p) then () else raise UNCHANGED;
val (v,body) = dest_smallfoot_prog_local_var p;
- val b_thm = sys xenv penv asm body;
+ val b_thm_opt = sys xenv penv asm body;
+ val b_thm = if (isSome b_thm_opt) then valOf b_thm_opt else raise UNCHANGED;
val b_thm2 = GEN_ASSUM v b_thm;
val thm = ISPECL [xenv, penv] FASL_PROGRAM_IS_ABSTRACTION___smallfoot_prog_local_var;
@@ -720,10 +788,17 @@
val (h,restBodyL) = listSyntax.dest_cons bodyL handle HOL_ERR _ => raise UNCHANGED;
- val thm_h = sys xenv penv asm h;
- val thm_rest = sys xenv penv asm (mk_fasl_prog_block restBodyL);
+ val thm_h_opt = sys xenv penv asm h;
+ val rest = mk_fasl_prog_block restBodyL;
+ val thm_rest_opt = sys xenv penv asm rest;
+ val _ = if (not (isSome thm_h_opt) andalso not (isSome thm_rest_opt)) then raise UNCHANGED else ();
+ val thm_h = if (isSome thm_h_opt) then valOf thm_h_opt else
+ FASL_PROGRAM_ABSTRACTION_REFL_CONV xenv penv h;
+ val thm_rest = if (isSome thm_rest_opt) then valOf thm_rest_opt else
+ FASL_PROGRAM_ABSTRACTION_REFL_CONV xenv penv rest;
+
val (_, _, _, p1) = dest_FASL_PROGRAM_IS_ABSTRACTION (concl thm_h);
val (_, _, _, p2) = dest_FASL_PROGRAM_IS_ABSTRACTION (concl thm_rest);
@@ -796,9 +871,16 @@
val _ = if (is_fasl_prog_cond p) then () else raise UNCHANGED;
val (c,p1,p2) = dest_fasl_prog_cond p;
- val p1_thm = sys xenv penv asm p1;
- val p2_thm = sys xenv penv asm p2;
+ val p1_thm_opt = sys xenv penv asm p1;
+ val p2_thm_opt = sys xenv penv asm p2;
+ val _ = if (not (isSome p1_thm_opt) andalso not (isSome p2_thm_opt)) then raise UNCHANGED else ();
+ val p1_thm = if (isSome p1_thm_opt) then valOf p1_thm_opt else
+ FASL_PROGRAM_ABSTRACTION_REFL_CONV xenv penv p1;
+ val p2_thm = if (isSome p2_thm_opt) then valOf p2_thm_opt else
+ FASL_PROGRAM_ABSTRACTION_REFL_CONV xenv penv p2;
+
+
val (_,_,_,p1') = dest_FASL_PROGRAM_IS_ABSTRACTION (concl p1_thm);
val (_,_,_,p2') = dest_FASL_PROGRAM_IS_ABSTRACTION (concl p2_thm);
@@ -895,44 +977,27 @@
-fun FASL_PROGRAM_ABSTRACTION_CONV___wrapper rewrite_thms conv sys xenv penv asm p =
- let
- val p' = rhs (concl (REWRITE_CONV rewrite_thms p));
- val thm = conv sys xenv penv asm p'
- val hypL = hyp thm;
- val thm1 = DISCH_ALL thm;
- val thm2 = REWRITE_RULE (map GSYM rewrite_thms) thm1;
- val thm3 = foldr (fn (_,thm) => UNDISCH thm) thm2 hypL;
- val (xenv', penv', p', _) = dest_FASL_PROGRAM_IS_ABSTRACTION (concl thm3);
- val _ = if not (xenv = xenv') orelse not (penv = penv') orelse (p' = p) then () else
- raise UNCHANGED;
- in
- thm3
- end handle UNCHANGED => conv sys xenv penv asm p;
-
-
val smallfoot_program_abstraction_convs = [
SMALLFOOT_PROGRAM_ABSTRACTION_CONV___val_arg,
SMALLFOOT_PROGRAM_ABSTRACTION_CONV___local_var,
SMALLFOOT_PROGRAM_ABSTRACTION_CONV___proc_call,
SMALLFOOT_PROGRAM_ABSTRACTION_CONV___parallel_proc_call,
SMALLFOOT_PROGRAM_ABSTRACTION_CONV___with_resource,
- FASL_PROGRAM_ABSTRACTION_CONV___wrapper [smallfoot_prog_block_def] FASL_PROGRAM_ABSTRACTION_CONV___block_flatten,
- FASL_PROGRAM_ABSTRACTION_CONV___wrapper [smallfoot_prog_block_def] FASL_PROGRAM_ABSTRACTION_CONV___block,
- FASL_PROGRAM_ABSTRACTION_CONV___wrapper [smallfoot_prog_cond_def] FASL_PROGRAM_ABSTRACTION_CONV___cond,
+ FASL_PROGRAM_ABSTRACTION_CONV___block_flatten,
+ FASL_PROGRAM_ABSTRACTION_CONV___block,
+ FASL_PROGRAM_ABSTRACTION_CONV___cond,
SMALLFOOT_PROGRAM_ABSTRACTION_CONV___while];
-
-
-
-fun FASL_PROGRAM_HOARE_TRIPLE___CONSEQ_CONV L asm t =
+fun FASL_PROGRAM_HOARE_TRIPLE___CONSEQ_CONV L asm t =
let
val _ = if (is_FASL_PROGRAM_HOARE_TRIPLE t) then () else raise UNCHANGED;
val (xenv, penv, pre, body, post) = dest_FASL_PROGRAM_HOARE_TRIPLE t;
-
- val thm = FASL_PROGRAM_ABSTRACTION_CONV L xenv penv asm body;
+
+ val thm_opt = FASL_PROGRAM_ABSTRACTION_CONV L xenv penv asm body;
+ val thm = if (isSome thm_opt) then valOf thm_opt else raise UNCHANGED;
+
val thm2 = ISPECL [xenv, penv, pre, body, post] FASL_PROGRAM_HOARE_TRIPLE_ABSTRACTION___INTRO;
val thm3 = MATCH_MP thm2 thm;
in
@@ -1062,7 +1127,7 @@
``(smallfoot_env, (K smallfoot_ap_true :string -> smallfoot_a_proposition))``;
val penv_FEMPTY_term = ``
(FEMPTY :string |->
- (smallfoot_var list # num list -> smallfoot_prog))``
+ (smallfoot_var list # num list -> smallfoot_prog))``;
fun SMALLFOOT_COND_HOARE_TRIPLE___CONSEQ_CONV L asm t =
@@ -1070,7 +1135,8 @@
val (pre, body, post) = (dest_SMALLFOOT_COND_HOARE_TRIPLE t)
handle HOL_ERR _ => raise UNCHANGED;
- val thm = FASL_PROGRAM_ABSTRACTION_CONV L COND_HOARE_TRIPLE___xenv_term penv_FEMPTY_term asm body;
+ val thm_opt = FASL_PROGRAM_ABSTRACTION_CONV L COND_HOARE_TRIPLE___xenv_term penv_FEMPTY_term asm body;
+ val thm = if (isSome thm_opt) then valOf thm_opt else raise UNCHANGED;
val (_,_,p1,p2) = dest_FASL_PROGRAM_IS_ABSTRACTION (concl thm);
val _ = if (p1 = p2) then raise UNCHANGED else ();
val _ = if (p1 = body) then () else raise UNCHANGED;
@@ -1245,8 +1311,8 @@
val SMALLFOOT_PROGRAM_HOARE_TRIPLE___STRONG_COND_EXISTS___CONSEQ_CONV =
THEN_CONSEQ_CONV
- (DEPTH_STRENGTHEN_CONSEQ_CONV SMALLFOOT_PROGRAM_HOARE_TRIPLE___STRONG_COND_EXISTS_PRE___CONSEQ_CONV)
- (DEPTH_STRENGTHEN_CONSEQ_CONV SMALLFOOT_PROGRAM_HOARE_TRIPLE___STRONG_COND_EXISTS_POST___CONSEQ_CONV)
+ (REDEPTH_STRENGTHEN_CONSEQ_CONV SMALLFOOT_PROGRAM_HOARE_TRIPLE___STRONG_COND_EXISTS_PRE___CONSEQ_CONV)
+ (REDEPTH_STRENGTHEN_CONSEQ_CONV SMALLFOOT_PROGRAM_HOARE_TRIPLE___STRONG_COND_EXISTS_POST___CONSEQ_CONV)
@@ -1304,8 +1370,77 @@
*)
+val t = ``(
+ FASL_PROGRAM_HOARE_TRIPLE
+ (smallfoot_env,
+ SMALLFOOT_res_decls_renv
+ [("freelist1",[smallfoot_var "TOP"],
+ smallfoot_ap_data_list (smallfoot_tag "tl")
+ (smallfoot_ae_var (smallfoot_var "TOP")) FEMPTY)]) penv
+ (\s.
+ s IN
+ smallfoot_prop_internal_ap ({status; t},{b}) [status; t; b]
+ [smallfoot_p_equal (smallfoot_p_var status)
+ (smallfoot_p_const 0)]
+ (smallfoot_ap_star
+ (smallfoot_ap_star
+ (smallfoot_ap_equal_cond (smallfoot_ae_var status)
+ smallfoot_ae_null
+ (smallfoot_ap_points_to (smallfoot_ae_var b)
+ FEMPTY))
+ (smallfoot_ap_exp_is_defined
+ (smallfoot_ae_var status)))
+ smallfoot_ap_stack_true) /\ (s = x))
+ (fasl_prog_block
+ [smallfoot_prog_block
+ [smallfoot_prog_aquire_resource_input
+ (smallfoot_p_equal (smallfoot_p_const 0)
+ (smallfoot_p_const 0)) (set [smallfoot_var "TOP"])
+ (smallfoot_ap_data_list (smallfoot_tag "tl")
+ (smallfoot_ae_var (smallfoot_var "TOP")) FEMPTY);
+ fasl_prog_block
+ [smallfoot_prog_assign t
+ (smallfoot_p_var (smallfoot_var "TOP"))];
+ smallfoot_prog_release_resource_input
+ (set [smallfoot_var "TOP"])
+ (smallfoot_ap_data_list (smallfoot_tag "tl")
+ (smallfoot_ae_var (smallfoot_var "TOP")) FEMPTY)];
+ smallfoot_prog_field_assign (smallfoot_p_var b)
+ (smallfoot_tag "tl") (smallfoot_p_var t);
+ smallfoot_prog_block
+ [smallfoot_prog_aquire_resource_input
+ (smallfoot_p_equal (smallfoot_p_const 0)
+ (smallfoot_p_const 0)) (set [smallfoot_var "TOP"])
+ (smallfoot_ap_data_list (smallfoot_tag "tl")
+ (smallfoot_ae_var (smallfoot_var "TOP")) FEMPTY);
+ fasl_prog_block
+ [smallfoot_prog_procedure_call "cas"
+ ([status; smallfoot_var "TOP"],
+ [smallfoot_p_var (smallfoot_var "TOP");
+ smallfoot_p_var t; smallfoot_p_var b])];
+ smallfoot_prog_release_resource_input
+ (set [smallfoot_var "TOP"])
+ (smallfoot_ap_data_list (smallfoot_tag "tl")
+ (smallfoot_ae_var (smallfoot_var "TOP")) FEMPTY)]])
+ (\s.
+ s IN
+ smallfoot_prop_internal_ap ({status; t},{b}) [status; t; b] []
+ (smallfoot_ap_star
+ (smallfoot_ap_star
+ (smallfoot_ap_equal_cond (smallfoot_ae_var status)
+ smallfoot_ae_null
+ (smallfoot_ap_points_to (smallfoot_ae_var b)
+ FEMPTY))
+ (smallfoot_ap_exp_is_defined
+ (smallfoot_ae_var status)))
+ smallfoot_ap_stack_true) /\
+ VAR_RES_STACK___IS_EQUAL_UPTO_VALUES (FST x) (FST s)))``;
+
+
+
+
fun REDEPTH_FASL_PROGRAM_HOARE_TRIPLE___CONSEQ_CONV L asm =
let val hyps = flatten (map hyp asm) in
CONJ_ASSUMPTIONS_CONSEQ_CONV
@@ -1385,6 +1520,7 @@
*)
local
+ val conv0 = REDEPTH_CONV (HO_REWR_CONV smallfoot_prop_internal___EXISTS)
val conv1 = COND_REWRITE_CONV [smallfoot_prop_internal___VARS_TO_BAGS];
val conv2 = COND_REWR_CONV smallfoot_prop_internal___VARS_TO_BAGS___END;
val conv3 = COND_REWRITE_CONV [smallfoot_prop_internal___PROP_TO_BAG];
@@ -1401,7 +1537,9 @@
let
val _ = if (is_smallfoot_prop_internal t) then () else raise UNCHANGED;
- val thm1 = (conv1 t) handle UNCHANGED => REFL t;
+
+ val thm0 = (conv0 t) handle UNCHANGED => REFL t;
+ val thm1 = RHS_CONV_RULE conv1 thm0;
val thm2 = RHS_CONV_RULE conv2 thm1
handle HOL_ERR _ => thm1;
@@ -1654,7 +1792,7 @@
-fun smallfoot_ap_unequal___CONV t =
+fun smallfoot_ap_unequal___CONV t =
let
val (l,r) = dest_smallfoot_ap_unequal t;
in
@@ -1684,15 +1822,21 @@
thm2
end handle UNCHANGED =>
let
- val l_string = term_to_string l;
- val r_string = term_to_string r;
+ val l' = dest_smallfoot_ae_const_null l;
+ val r' = dest_smallfoot_ae_const_null r;
+
+ val swap = (Term.compare (l',r') = GREATER);
in
- if (r_string <= l_string) then ISPECL [l,r] smallfoot_ap_unequal___COMM else raise UNCHANGED
+ if swap then ISPECL [l,r] smallfoot_ap_unequal___COMM else raise UNCHANGED
end
-
else raise UNCHANGED
end;
+
+
+
+
+
(*
val t = ``smallfoot_ap_unequal_cond (smallfoot_ae_const 1) smallfoot_ae_null
(smallfoot_ap_stack_true)``;
@@ -1711,6 +1855,7 @@
let
val l' = dest_smallfoot_ae_const_null l;
val r' = dest_smallfoot_ae_const_null r;
+ val _ = if (l' = r') then raise UNCHANGED else ();
val const_eq = mk_eq (l',r');
val eq_thm = reduceLib.REDUCE_CONV const_eq;
@@ -1721,7 +1866,7 @@
val rc_term = mk_comb (smallfoot_ae_const_term, r');
val l_cond_term = mk_smallfoot_ap_unequal_cond (lc_term, rc_term, P)
in
- REWRITE_CONV [EQT_ELIM eq_thm] l_cond_term
+ ONCE_REWRITE_CONV [EQT_ELIM eq_thm] l_cond_term
end
else if (rhs (concl eq_thm) = F) then
let
@@ -1762,6 +1907,7 @@
let
val l' = dest_smallfoot_ae_const_null l;
val r' = dest_smallfoot_ae_const_null r;
+ val _ = if (l' = r') then raise UNCHANGED else ();
val const_eq = mk_eq (l',r');
val eq_thm = reduceLib.REDUCE_CONV const_eq;
@@ -1772,7 +1918,7 @@
val rc_term = mk_comb (smallfoot_ae_const_term, r');
val l_cond_term = mk_smallfoot_ap_equal_cond (lc_term, rc_term, P)
in
- REWRITE_CONV [EQT_ELIM eq_thm] l_cond_term
+ ONCE_REWRITE_CONV [EQT_ELIM eq_thm] l_cond_term
end
else if (rhs (concl eq_thm) = F) then
let
@@ -1890,16 +2036,17 @@
val (tag1,_) = pairLib.dest_pair p1
val (tag2,_) = pairLib.dest_pair p2
val tag1_string = stringLib.fromHOLstring (dest_smallfoot_tag tag1)
- val tag2_string = stringLib.fromHOLstring (dest_smallfoot_tag tag2)
+ val tag2_string = stringLib.fromHOLstring (dest_smallfoot_tag tag2)
+ val comp = String.compare (tag1_string, tag2_string);
in
- if tag1_string < tag2_string then
+ if comp = LESS then
let
val thm0 = PART_MATCH (lhs o snd o dest_imp) (SPEC_ALL FUPDATE_COMMUTES) t;
val thm1 = smallfoot_precondition_prove_RULE NONE [] thm0;
in
thm1
end
- else if tag1_string = tag1_string then
+ else if comp = EQUAL then
PART_MATCH lhs (SPEC_ALL FUPDATE_EQ) t
else raise UNCHANGED
end;
@@ -1974,15 +2121,28 @@
val _ = computeLib.add_conv (``$=``, 2, stringLib.string_EQ_CONV) FAPPLY_cs;
-fun FAPPLY_TAG_SIMP_CONV t =
- (CHANGED_CONV (computeLib.CBV_CONV FAPPLY_cs)) t
-handle HOL_ERR _ => raise UNCHANGED;
+val FAPPLY_tm = ``$'``;
+val FUPDATE_tm = ``$|+``;
+fun is_FAPPLY_FUPDATE t =
+let
+ val (app,rest) = dest_comb (fst (dest_comb t));
+ val (up,_) = dest_comb (fst (dest_comb rest));
+in
+ (same_const app FAPPLY_tm) andalso
+ (same_const up FUPDATE_tm)
+end handle HOL_ERR _ => false;
+fun CHANGED_UNCHANGED_CONV conv t =
+ (CHANGED_CONV conv) t handle HOL_ERR _ => raise UNCHANGED;
+val FAPPLY_TAG_SIMP_CONV =
+ CHANGED_UNCHANGED_CONV (computeLib.CBV_CONV FAPPLY_cs);
+
+
fun LIST_NOT_NIL___HD_EXISTS_CONV t =
let
val b = dest_neg t;
@@ -2000,12 +2160,14 @@
thm1
end handle HOL_ERR _ => raise UNCHANGED;
-val smallfoot___PROP_SIMPLE_EQ_REWRITES_CONV =
+
+
+val smallfoot___PROP_SIMPLE_EQ_REWRITES_CONV =
DEPTH_CONV (QCHANGED_CONV smallfoot_ap_equal___CONV ORELSEC
QCHANGED_CONV smallfoot_ap_unequal___CONV ORELSEC
QCHANGED_CONV smallfoot_ap_equal_cond___decide_non_eq_const___CONV ORELSEC
QCHANGED_CONV smallfoot_ap_unequal_cond___decide_non_eq_const___CONV ORELSEC
- QCHANGED_CONV FEVERY_EXPAND_CONV) THENC
+ QCHANGED_CONV FEVERY_EXPAND_CONV) THENC
FAPPLY_TAG_SIMP_CONV THENC
REWRITE_CONV [smallfoot_ap_bintree___smallfoot_ae_null,
smallfoot_ap_data_list___smallfoot_ae_null,
@@ -2029,26 +2191,66 @@
GSYM smallfoot_ap_empty_heap_cond___false] THENC
DEPTH_CONV (QCHANGED_CONV smallfoot_prop___smallfoot_ap_stack_true_CONV ORELSEC
QCHANGED_CONV smallfoot_prop___smallfoot_ap_exp_is_defined_CONV) THENC
- REDEPTH_CONV FMAP_TAG_NORMALISE_CONV;
+ REDEPTH_CONV (QCHANGED_CONV FMAP_TAG_NORMALISE_CONV);
+(*
+val t = ``LIST_UNROLL_GIVEN_ELEMENT_NAMES L ["r"; "z"; "x"]``
+val v = ``L:'a list``;
+val fv = [``z:'a``]
+fun QUANT_INSTANTIATE_HEURISTIC___LIST_UNROLL_GIVEN_ELEMENT_NAMES (sys:quant_heuristic) fv v t =
+let
+ val (fun_term, argL) = strip_comb t;
+ val _ = if (same_const fun_term LIST_UNROLL_GIVEN_ELEMENT_NAMES_term) andalso
+ (length argL = 2) then () else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp;
+ val (v', names_term) = (el 1 argL, el 2 argL);
+ val _ = if (v' = v) then () else raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp;
+ val list_ty = listSyntax.dest_list_type (type_of v);
+ val (namesL,_) = listSyntax.dest_list names_term
+ val fvL = map (fn n => mk_var(stringLib.fromHOLstring n, list_ty)) namesL;
+ val i = listSyntax.mk_list (fvL, list_ty);
+ val (i,fvL) = term_variant fv fvL i
+ val g_true_term = valOf(make_guess_thm_term v t (guess_true(i,fvL,NONE)))
+ val g_true_thm = prove (g_true_term, REWRITE_TAC[LIST_UNROLL_GIVEN_ELEMENT_NAMES_REWRITE])
+ val g_true = guess_true(i,fvL,SOME (fn () => g_true_thm));
+ fun do_case_split_tac (asm,p) =
+ let
+ val (_, t2) = dest_imp_only p;
+ val t3 = dest_neg t2;
+ val t4 = rand (rator t3)
+ in
+ STRUCT_CASES_TAC (ISPEC t4 list_CASES) (asm,p)
+ end;
+ val g_others_not_possible___no_argument = guess_others_not_possible(i,fvL,NONE)
+ val g_others_not_possible = make_set_guess_thm_opt v t g_others_not_possible___no_argument
+ (fn t => prove (t,
+ GEN_TAC THEN
+ REPEAT (do_case_split_tac THEN REWRITE_TAC [LIST_UNROLL_GIVEN_ELEMENT_NAMES_REWRITE]) THEN
+ SIMP_TAC list_ss []))
+in
+ {rewrites = [g_true_thm],
+ general = [],
+ true = [g_true],
+ false = [],
+ only_not_possible = [],
+ only_possible = [],
+ others_satisfied = [],
+ others_not_possible = [g_others_not_possible]}:guess_collection
+end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp
+*)
-
-
-
-
val precond_cond_cs = reduceLib.num_compset ();
val _ = listSimps.list_rws precond_cond_cs;
val _ = computeLib.add_thms [SMALLFOOT_HOARE_TRIPLE_def,
@@ -2094,18 +2296,6 @@
-val time_ref = ref (Time.now());
-fun time_step_init () = time_ref := (Time.now());
-fun time_step m =
- let
- val d_time = Time.- (Time.now(), !time_ref);
- val _ = print m;
- val _ = print ": ";
- val _ = print (Time.toString d_time);
- val _ = print "\n";
- in
- ()
- end;
(*
@@ -2113,12 +2303,14 @@
*)
+
fun SMALLFOOT_SPECIFICATION___CONSEQ_CONV t =
let
(*Eliminate Recursion*)
val (res_decls_term, p_specs_term) = dest_SMALLFOOT_SPECIFICATION t;
val thm1 = ISPECL [res_decls_term, p_specs_term] SMALLFOOT_SPECIFICATION___INFERENCE;
+
(*Ensure that all used procedure names are different*)
val thm2 = CONV_RULE ANTE_CONJ_CONV thm1;
val thm3 = smallfoot_precondition_prove_RULE (SOME "SMALLFOOT_SPECIFICATION___CONSEQ_CONV") [] thm2;
@@ -2131,9 +2323,14 @@
val (imp_ante, imp_cons) = dest_imp imp_body;
val imp_ante_thms = map ASSUME (strip_conj imp_ante);
- val imp_cons_thm = REDEPTH_FASL_PROGRAM_HOARE_TRIPLE___CONSEQ_CONV smallfoot_program_abstraction_convs imp_ante_thms imp_cons
- handle UNCHANGED => REFL_CONSEQ_CONV imp_cons;
+ val imp_cons_thm0 = REWRITE_CONV [smallfoot_prog_block_def, smallfoot_prog_cond_def] imp_cons;
+ val imp_cons' = rhs (concl imp_cons_thm0);
+ val imp_cons_thm1 = REDEPTH_FASL_PROGRAM_HOARE_TRIPLE___CONSEQ_CONV smallfoot_program_abstraction_convs imp_ante_thms imp_cons'
+ handle UNCHANGED => REFL_CONSEQ_CONV imp_cons';
+ val imp_cons_thm2 = CONV_RULE (RAND_CONV (REWR_CONV (GSYM imp_cons_thm0))) imp_cons_thm1
+ val imp_cons_thm = CONV_RULE (RATOR_CONV (RAND_CONV (REWRITE_CONV [GSYM smallfoot_prog_block_def, GSYM smallfoot_prog_cond_def]))) imp_cons_thm2
+
val imp_thm_term = let
val org_term = imp_term;
val (new_term_concl,_) = dest_imp (concl imp_cons_thm);
@@ -2159,27 +2356,33 @@
(*Simplify specification terms*)
val thm7 = IMP_CONV_RULE (REWRITE_CONV [GSYM SMALLFOOT_HOARE_TRIPLE_def]) thm6;
val thm7a = IMP_CONV_RULE (DEPTH_CONV SMALLFOOT_COND_HOARE_TRIPLE_INTRO___CONV) thm7;
- val thm7b = IMP_CONV_RULE (SIMP_CONV std_ss [smallfoot_prog_release_resource_input___REWRITE,
- smallfoot_prog_aquire_resource_input___REWRITE,
- LIST_TO_SET_THM]) thm7a;
+ val thm7b = IMP_CONV_RULE (REWRITE_CONV [smallfoot_prog_release_resource_input___REWRITE,
+ smallfoot_prog_aquire_resource_input___REWRITE,
+ LIST_TO_SET_THM]) thm7a;
val thm8 = IMP_CONV_RULE (DEPTH_CONV smallfoot_choose_const_best_local_action___CONV) thm7b;
val thm8a = IMP_CONV_RULE (SIMP_CONV std_ss [smallfoot_prop_internal___EXISTS]) thm8;
val thm9 = IMP_CONV_RULE (DEPTH_CONV smallfoot_prop_internal_CONV) thm8a;
- val thm9a = IMP_CONV_RULE (DEPTH_CONV smallfoot___PROP_SIMPLE_EQ_REWRITES_CONV) thm9;
+ val thm9a = IMP_CONV_RULE smallfoot___PROP_SIMPLE_EQ_REWRITES_CONV thm9;
val thm9b = IMP_CONV_RULE (DEPTH_CONV smallfoot_prog_aquire_resource_internal_CONV) thm9a;
val thm9c = IMP_CONV_RULE (DEPTH_CONV smallfoot_prog_release_resource_internal_CONV) thm9b;
- val thm10= STRENGTHEN_CONSEQ_CONV_RULE (K (
- DEPTH_STRENGTHEN_CONSEQ_CONV (SMALLFOOT_COND_HOARE_TRIPLE___CONSEQ_CONV
- (SMALLFOOT_PROGRAM_ABSTRACTION_CONV___smallfoot_cond_choose_const___smallfoot_cond_star::smallfoot_program_abstraction_convs) []))) thm9c
- handle UNCHANGED => thm9c;
+ val thm10a = REWRITE_RULE [smallfoot_prog_block_def, smallfoot_prog_cond_def] thm9c;
+
+ val thm10b= STRENGTHEN_CONSEQ_CONV_RULE (K (
+ REDEPTH_STRENGTHEN_CONSEQ_CONV (
+SMALLFOOT_COND_HOARE_TRIPLE___CONSEQ_CONV
+(SMALLFOOT_PROGRAM_ABSTRACTION_CONV___smallfoot_cond_choose_const___smallfoot_cond_star::smallfoot_program_abstraction_convs) []))) thm10a
+ handle UNCHANGED => thm10a;
+ val thm10 = REWRITE_RULE [GSYM smallfoot_prog_block_def, GSYM smallfoot_prog_cond_def] thm10b;
+
+
(*Eliminate existantial quantification in PRE- and POST-Conditions of
top level Hoare-Triples*)
val thm11= STRENGTHEN_CONSEQ_CONV_RULE (K (
- DEPTH_STRENGTHEN_CONSEQ_CONV SMALLFOOT_PROGRAM_HOARE_TRIPLE___STRONG_COND_EXISTS_PRE___CONSEQ_CONV
+ REDEPTH_STRENGTHEN_CONSEQ_CONV SMALLFOOT_PROGRAM_HOARE_TRIPLE___STRONG_COND_EXISTS_PRE___CONSEQ_CONV
)) thm10 handle UNCHANGED => thm10;
(*Eliminate local variables and call-by value parameters*)
@@ -2417,6 +2620,8 @@
+
+
(*
val smallfoot_prop___COND_INTRO___EQUIV_CONV v t =
let
@@ -2492,25 +2697,19 @@
end
-fun dummy_conv t = let
- val v = mk_var ("XXX", type_of t);
- val t' = mk_eq (t, v);
-in
- mk_thm ([], t')
-end;
+fun SMALLFOOT_COND_INFERENCE___block_to_seq t =
+ let
+ val (P, prog, Q) = dest_SMALLFOOT_COND_HOARE_TRIPLE t;
+ val progL = dest_smallfoot_prog_block prog;
+ val (c1,cL) = listSyntax.dest_cons progL
+ in
+ (c1, fn () => ISPECL [P,c1,cL,Q] SMALLFOOT_COND_HOARE_TRIPLE___BLOCK_FIRST_SPLIT)
+ end;
-fun SMALLFOOT_COND_INFERENCE___block_to_seq_CONV t =
- if (is_SMALLFOOT_COND_HOARE_TRIPLE t) then
- PART_MATCH lhs SMALLFOOT_COND_HOARE_TRIPLE___BLOCK_FIRST_SPLIT t
- else
- raise UNCHANGED;
-
-
-
val FORALL_SIMP_CONV =
let val thm = SPEC_ALL boolTheory.FORALL_SIMP in
HO_PART_MATCH lhs thm
@@ -2554,10 +2753,10 @@
fun SMALLFOOT_COND_INFERENCE_CONV___assign t =
let
- val thm0 = SMALLFOOT_COND_INFERENCE___block_to_seq_CONV t;
+ val (command,thm0_f) = SMALLFOOT_COND_INFERENCE___block_to_seq t;
+ val (v, e) = dest_smallfoot_prog_assign command;
+ val thm0 = thm0_f ();
val t' = rhs (concl thm0);
- val command = dest_SMALLFOOT_COND_HOARE_TRIPLE___first_command t';
- val (v, e) = dest_smallfoot_prog_assign command;
val (quant, thm1) = SMALLFOOT_COND_HOARE_TRIPLE___CONST_INTRO v NONE t';
@@ -2585,10 +2784,10 @@
fun SMALLFOOT_COND_INFERENCE_CONV___new t =
let
- val thm0 = SMALLFOOT_COND_INFERENCE___block_to_seq_CONV t;
+ val (command,thm0_f) = SMALLFOOT_COND_INFERENCE___block_to_seq t;
+ val v = dest_smallfoot_prog_new command;
+ val thm0 = thm0_f ();
val t' = rhs (concl thm0);
- val command = dest_SMALLFOOT_COND_HOARE_TRIPLE___first_command t';
- val v = dest_smallfoot_prog_new command;
val (quant, thm1) = SMALLFOOT_COND_HOARE_TRIPLE___CONST_INTRO v NONE t';
val thm2 = TRANS thm0 thm1;
@@ -2618,7 +2817,8 @@
fun SMALLFOOT_COND_INFERENCE_CONV___cond t =
let
- val thm0 = SMALLFOOT_COND_INFERENCE___block_to_seq_CONV t;
+ val (_,thm0_f) = SMALLFOOT_COND_INFERENCE___block_to_seq t;
+ val thm0 = thm0_f ();
val t' = rhs (concl thm0);
val thm1 = PART_MATCH (snd o dest_imp o snd o dest_imp)
@@ -2672,7 +2872,9 @@
fun SMALLFOOT_COND_INFERENCE_CONV___prog_aquire_resource t =
let
- val thm0 = SMALLFOOT_COND_INFERENCE___block_to_seq_CONV t;
+ val (_,thm0_f) = SMALLFOOT_COND_INFERENCE___block_to_seq t;
+ val thm0 = thm0_f ();
+
val t' = rhs (concl thm0);
val thm1 = PART_MATCH (snd o dest_imp o snd o dest_imp)
@@ -3228,9 +3430,8 @@
+val QCHANGED_FIRST_CONV = FIRST_CONV o (map QCHANGED_CONV);
-val QCHANGED_FIRST_CONV = FIRST_CONV o (map QCHANGED_CONV)
-
val smallfoot_prop___SIMPLIFY_CONV =
(SMALLFOOT_COND_PROP___REPEATC (SMALLFOOT_COND_PROP___DEPTH_CONV (
(QCHANGED_FIRST_CONV
@@ -3277,6 +3478,15 @@
+fun smallfoot_ae_var___is_equals_var___excluded done t =
+ let
+ val (l,r) = dest_smallfoot_ap_equal t;
+ val vl = dest_smallfoot_ae_var l;
+ val vr = dest_smallfoot_ae_var r;
+ in
+ if (not (mem vl done)) then SOME vl else
+ if (not (mem vr done)) then SOME vr else NONE
+ end handle HOL_ERR _ => NONE;
@@ -3348,10 +3558,14 @@
exists_opt save f L
end
+fun opt_combine _ (SOME true) = SOME true
+ | opt_combine x (SOME false) = x
+ | opt_combine (SOME true) _ = SOME true
+ | opt_combine (SOME false) x = x
+ | opt_combine NONE NONE = NONE;
-
fun LIST_SMALLFOOT_AE_USED_VARS___SAVE_IN save v tL =
exists_opt save (SMALLFOOT_AE_USED_VARS___SAVE_IN v) tL;
@@ -3381,6 +3595,15 @@
in
LIST_SMALLFOOT_AE_USED_VARS___SAVE_IN true v [e1,e2]
end else
+if (is_smallfoot_ap_equal_or_unequal_cond t) then
+ let
+ val (e1,e2,t1) = dest_smallfoot_ap_equal_or_unequal_cond t
+ val res1 = LIST_SMALLFOOT_AE_USED_VARS___SAVE_IN true v [e1,e2]
+ val res2 = if (res1 = SOME true) then res1 else
+ SMALLFOOT_AP_USED_VARS___SAVE_IN v t1;
+ in
+ opt_combine res1 res2
+ end else
if (is_smallfoot_ap_exp_is_defined t) then
let
val e = dest_smallfoot_ap_exp_is_defined t
@@ -3393,14 +3616,100 @@
in
SMALLFOOT_AE_USED_VARS___SAVE_IN v e
end
-else NONE;
+else
+ (say ("Could not determine whether smallfoot-variable ``"^(term_to_string v)^
+ "`` is in term ``"^(term_to_string t)^"``! You should consider extending "^
+ "SMALLFOOT_AP_USED_VARS___SAVE_IN!\n"); NONE);
+
+
fun LIST_SMALLFOOT_AP_USED_VARS___SAVE_IN save v tL =
exists_opt save (SMALLFOOT_AP_USED_VARS___SAVE_IN v) tL;
+
+
+fun SMALLFOOT_AE_USED_VARS___SAVE_LIST t =
+if (is_smallfoot_ae_const_null t) then SOME [] else
+if (is_smallfoot_ae_var t) then
+ SOME [dest_smallfoot_ae_var t]
+else NONE;
+
+
+fun flatten_opt acc f [] = SOME acc
+ | flatten_opt acc f (e::L) =
+ let
+ val opt = f e
+ in
+ if (opt = NONE) then NONE else
+ flatten_opt (append (valOf opt) acc) f L
+ end;
+
+
+
+fun LIST_SMALLFOOT_AE_USED_VARS___SAVE_LIST tL =
+ flatten_opt [] SMALLFOOT_AE_USED_VARS___SAVE_LIST tL;
+
+
+
+fun SMALLFOOT_AP_USED_VARS___SAVE_LIST t =
+if (same_const t smallfoot_ap_false_term) then SOME [] else
+if (same_const t smallfoot_ap_stack_true_term) then SOME [] else
+if (is_smallfoot_ap_empty_heap_cond t) then SOME [] else
+if (is_smallfoot_ap_compare t) then
+ let
+ val (e1,e2) = dest_smallfoot_ap_compare t;
+ in
+ LIST_SMALLFOOT_AE_USED_VARS___SAVE_LIST [e1,e2]
+ end else
+if (is_smallfoot_ap_points_to t) then
+ let
+ val (e1,tag_map) = dest_smallfoot_ap_points_to t;
+ val (tag_expL, rest) = dest_finite_map tag_map;
+ in
+ if (isSome rest) then NONE else
+ LIST_SMALLFOOT_AE_USED_VARS___SAVE_LIST (e1::map snd tag_expL)
+ end else
+if (is_smallfoot_ap_data_list_seg_or_list t) then
+ let
+ val (_,e1,_,e2) = dest_smallfoot_ap_data_list_seg_or_list t
+ in
+ LIST_SMALLFOOT_AE_USED_VARS___SAVE_LIST [e1,e2]
+ end else
+if (is_smallfoot_ap_equal_or_unequal_cond t) then
+ let
+ val (e1,e2,t1) = dest_smallfoot_ap_equal_or_unequal_cond t
+ val res1 = LIST_SMALLFOOT_AE_USED_VARS___SAVE_LIST [e1,e2]
+ val res2 = if (res1 = NONE) then NONE else
+ SMALLFOOT_AP_USED_VARS___SAVE_LIST t1;
+ in
+ if (res2 = NONE) then NONE else SOME (append (valOf res2) (valOf res1))
+ end else
+if (is_smallfoot_ap_exp_is_defined t) then
+ let
+ val e = dest_smallfoot_ap_exp_is_defined t
+ in
+ SMALLFOOT_AE_USED_VARS___SAVE_LIST e
+ end else
+if (is_smallfoot_ap_bintree t) then
+ let
+ val (_,_,e) = dest_smallfoot_ap_bintree t
+ in
+ SMALLFOOT_AE_USED_VARS___SAVE_LIST e
+ end
+else
+ (say ("Could not determine smallfoot-variables "^
+ "in term ``"^(term_to_string t)^"``! You should consider extending "^
+ "SMALLFOOT_AP_USED_VARS___SAVE_LIST!\n"); NONE);
+
+
+fun LIST_SMALLFOOT_AP_USED_VARS___SAVE_LIST tL =
+ flatten_opt [] SMALLFOOT_AP_USED_VARS___SAVE_LIST tL;
+
+
+
fun list_remove_element n [] = []
| list_remove_element n (e::L) =
if n = 0 then L else
@@ -3418,30 +3727,31 @@
let
val _ = if (is_smallfoot_prop t) then () else raise UNCHANGED
- val thm0 = (REWRITE_CONV [smallfoot_ae_null_def] t)
- handle UNCHANGED => REFL t;
- val t' = rhs (concl thm0)
-
- val (wpb,rpb,sfb) = dest_smallfoot_prop t';
+ val (wpb,rpb,sfb) = dest_smallfoot_prop t;
val (sfs, _) = bagSyntax.dest_bag sfb;
val found_opt = find_first_num (K (smallfoot_ae_var___is_equals_const___excluded done)) [] 0 sfs
in
if isSome found_opt then
let
- val (pos,_,(v,c)) = valOf found_opt;
+ val (pos,_,(v,c)) = valOf found_opt;
val needs_rewrite_opt = LIST_SMALLFOOT_AP_USED_VARS___SAVE_IN true v
(list_remove_element pos sfs);
val needs_rewrite = (not (isSome needs_rewrite_opt)) orelse (valOf needs_rewrite_opt);
+
+
in if (not needs_rewrite) then
let
- val thm1 = smallfoot_prop___EQ_PROPAGATE___INTERNAL new_vars_intro all_vars_intro (v::done) t'
- handle UNCHANGED => SMALLFOOT_COND_PROP___IMP___REFL_CONV t'
- val thm2 = SMALLFOOT_COND_PROP___IMP___TRANS_RULE thm0 thm1;
+(* val _ = print ("No rewrite needed for "^(term_to_string v)^" in "^(term_to_string t)^"!\n");*)
+
+ val thm1 = smallfoot_prop___EQ_PROPAGATE___INTERNAL new_vars_intro all_vars_intro (v::done) t
in
- thm2
+ thm1
end
else let
- val thm1 = CONV_RULE (RHS_CONV (smallfoot_prop___COND_RESORT_CONV [pos])) thm0
+ val thm1 =
+ RAND_CONV (BAG_RESORT_CONV [pos] THENC
+ bag_el_conv (REWRITE_CONV [smallfoot_ae_null_def]) 0)
+ t
val (_,_,sfb') = dest_smallfoot_prop (rhs (concl thm1));
val (_, sfb'') = bagSyntax.dest_insert sfb';
@@ -3453,10 +3763,8 @@
val thm5 = SMALLFOOT_COND_PROP___IMP___TRANS_RULE thm3 thm4
val (_, p) = dest_SMALLFOOT_COND_PROP___IMP (concl thm5);
- val thm6 = (SMALLFOOT_COND_PROP___THENC
- smallfoot_prop___SIMPLIFY_CONV
- (SMALLFOOT_COND_PROP___DEPTH_CONV
- (smallfoot_prop___EQ_PROPAGATE___INTERNAL new_vars_intro all_vars_intro (v::done)))) p
+ val thm6 = (SMALLFOOT_COND_PROP___DEPTH_CONV
+ (smallfoot_prop___EQ_PROPAGATE___INTERNAL new_vars_intro all_vars_intro (v::done))) p
handle UNCHANGED => SMALLFOOT_COND_PROP___IMP___REFL_CONV p;
in
SMALLFOOT_COND_PROP___IMP___TRANS_RULE thm5 thm6
@@ -3464,9 +3772,9 @@
else
let
val _ = if new_vars_intro orelse all_vars_intro then () else raise UNCHANGED;
- val found_opt = find_first_num (K (smallfoot_ae_var___is_equals_var)) [] 0 sfs
+ val found_opt = find_first_num (K (smallfoot_ae_var___is_equals_var___excluded done)) [] 0 sfs
val v = if (isSome found_opt) then
- let val (_,_,(v,_)) = valOf found_opt in
+ let val (_,_,v) = valOf found_opt in
v
end
else
@@ -3484,13 +3792,14 @@
val c_name = get_const_name_for_var v;
val thm3 = CONV_RULE ((RAND_CONV o RAND_CONV) (RENAME_VARS_CONV [c_name])) thm2
- val thm4 = SMALLFOOT_COND_PROP___IMP___TRANS_RULE thm0 thm3
+ val thm4 = MAKE___SMALLFOOT_COND_PROP___IMP___RULE thm3;
- val (_,p0) = dest_SMALLFOOT_COND_PROP___IMP (concl thm4)
+ val (_,p0) = dest_SMALLFOOT_COND_PROP___IMP (concl thm4);
val (c,p) = dest_COND_PROP___EXISTS p0;
- val thm_p = smallfoot_prop___EQ_PROPAGATE___INTERNAL new_vars_intro all_vars_intro done p
+ val done' = filter (fn v' => not (v = v')) done;
+ val thm_p = smallfoot_prop___EQ_PROPAGATE___INTERNAL new_vars_intro all_vars_intro done' p
handle UNCHANGED => SMALLFOOT_COND_PROP___IMP___REFL_CONV p
val thm_p' = GEN c thm_p
@@ -3502,15 +3811,127 @@
end;
-fun smallfoot_prop___EQ_PROPAGATE_CONV new_vars_intro all_vars_intro =
- SMALLFOOT_COND_PROP___THENC
- (smallfoot_prop___EQ_PROPAGATE___INTERNAL new_vars_intro all_vars_intro [])
- smallfoot_prop___SIMPLIFY_CONV
+local
+ fun filter_found acc t [] = (acc,false)
+ | filter_found acc t (t1::ts) =
+ if (aconv t t1) then (append acc (filter (fn t' => not (aconv t t')) ts), true) else
+ (filter_found (t1::acc) t ts)
+ fun remove_duplicate_terms acc [] = acc
+ | remove_duplicate_terms acc (t::ts) =
+ let
+ val (fts, dup) = filter_found [] t ts;
+ val acc' = if dup then acc else t::acc;
+ in
+ remove_duplicate_terms acc' fts
+ end;
+ fun get_done_vars only_consts t =
+ let
+ val (wpb,rpb,sfb) = dest_smallfoot_prop t;
+ val (sfs, _) = bagSyntax.dest_bag sfb;
+ val used_vars_list_opt = LIST_SMALLFOOT_AP_USED_VARS___SAVE_LIST sfs;
+ val doneL = if isSome used_vars_list_opt then
+ remove_duplicate_terms [] (valOf used_vars_list_opt)
+ else [];
+ val doneL' = if not only_consts orelse not (isSome used_vars_list_opt) then doneL else
+ let
+ val doneL'' = filter (fn v => exists (fn t => isSome (smallfoot_ae_var___is_equals_const v t)) sfs) doneL;
+ in
+ doneL''
+ end;
+ in
+ doneL'
+ end;
+
+
+in
+
+
+(*
+
+val t = ``
+(smallfoot_prop ({|p1; q1; q; p; r|},{| |})
+ {|smallfoot_ap_equal (smallfoot_ae_var r) (smallfoot_ae_var p);
+ smallfoot_ap_equal (smallfoot_ae_var p) smallfoot_ae_null;
+ smallfoot_ap_equal (smallfoot_ae_var p)
+ (smallfoot_ae_const p_const);
+ smallfoot_ap_data_list (smallfoot_tag "tl")
+ (smallfoot_ae_const p_const) FEMPTY|})``
+
+val t = ``smallfoot_prop ({|t; x|},{| |})
+ {|smallfoot_ap_equal (smallfoot_ae_var t) (smallfoot_ae_var x);
+ smallfoot_ap_unequal (smallfoot_ae_var x) smallfoot_ae_null;
+ smallfoot_ap_data_list (smallfoot_tag "tl") (smallfoot_ae_var x)
+ FEMPTY|}``
+val new_vars_intro = true;
+val all_vars_intro = true;
+
+
+use_smallfoot_pretty_printer := true
+
+use_smallfoot_pretty_printer := false
+
+val t = ``smallfoot_prop ({|z; x; e; y|},{|a|})
+ {|smallfoot_ap_equal (smallfoot_ae_var e) (smallfoot_ae_const n);
+ smallfoot_ap_points_to (smallfoot_ae_var y)
+ (FEMPTY |+
+ (smallfoot_tag "hd",
+ smallfoot_ae_const e_smallfoot_tag__hd__const) |+
+ (smallfoot_tag "tl",smallfoot_ae_const n));
+ smallfoot_ap_unequal (smallfoot_ae_var y) (smallfoot_ae_var x);
+ smallfoot_ap_equal (smallfoot_ae_var a)
+ (smallfoot_ae_const e_smallfoot_tag__hd__const);
+ smallfoot_ap_unequal (smallfoot_ae_var z) (smallfoot_ae_const n);
+ smallfoot_ap_unequal (smallfoot_ae_var z) smallfoot_ae_null;
+ smallfoot_ap_unequal (smallfoot_ae_var y) (smallfoot_ae_var z);
+ smallfoot_ap_unequal (smallfoot_ae_var y) (smallfoot_ae_const n);
+ smallfoot_ap_unequal (smallfoot_ae_var y) smallfoot_ae_null;
+ smallfoot_ap_data_list (smallfoot_tag "tl") (smallfoot_ae_const n)
+ FEMPTY;
+ smallfoot_ap_unequal (smallfoot_ae_var y) (smallfoot_ae_var x);
+ smallfoot_ap_points_to (smallfoot_ae_var z)
+ (FEMPTY |+ (smallfoot_tag "tl",smallfoot_ae_var y));
+ smallfoot_ap_data_list_seg (smallfoot_tag "tl") (smallfoot_ae_var x)
+ FEMPTY (smallfoot_ae_var z)|}``
+
+
+val t = `` (smallfoot_prop ({|smallfoot_var "TOP"; t; status|},{|b|})
+ {|smallfoot_ap_equal (smallfoot_ae_var t)
+ (smallfoot_ae_var (smallfoot_var "TOP"));
+ smallfoot_ap_equal (smallfoot_ae_const 0)
+ (smallfoot_ae_const 0);
+ smallfoot_ap_data_list (smallfoot_tag "tl")
+ (smallfoot_ae_var (smallfoot_var "TOP")) FEMPTY;
+ smallfoot_ap_equal (smallfoot_ae_var status) smallfoot_ae_null;
+ smallfoot_ap_equal_cond (smallfoot_ae_var status)
+ smallfoot_ae_null
+ (smallfoot_ap_points_to (smallfoot_ae_var b) FEMPTY)|})``
+
+*)
+
+fun smallfoot_prop___EQ_PROPAGATE_CONV new_vars_intro all_vars_intro t =
+ let
+ val done = get_done_vars (all_vars_intro orelse new_vars_intro) t handle HOL_ERR _ => raise UNCHANGED;
+(* val _ = print ("Found vars for "^(term_to_string t)^"\n");
+ val _ = print (" - "^(concat (commafy (map term_to_string done)))^"\n");
+*)
+ val thm = (SMALLFOOT_COND_PROP___THENC
+ (smallfoot_prop___EQ_PROPAGATE___INTERNAL new_vars_intro all_vars_intro done)
+ smallfoot_prop___SIMPLIFY_CONV) t ;
+(* val _ = print (" - done\n");*)
+ in
+ thm
+ end
+
+end;
+
+
+
+
fun SMALLFOOT_COND_INFERENCE_CONV___EQ_PROPAGATE_CONV new_vars_intro all_vars_intro =
SMALLFOOT_COND_HOARE_TRIPLE___PRECOND_CONV
(smallfoot_prop___EQ_PROPAGATE_CONV new_vars_intro all_vars_intro)
@@ -3572,6 +3993,7 @@
*)
exception smallfoot_ap_bag_implies_in_heap_or_null___PROVE_FOUND_exn of thm
+
fun smallfoot_ap_bag_implies_in_heap_or_null___SEARCH_PROVE sfb expP =
let
val _ = if (expP smallfoot_ae_null_term) then
@@ -3703,7 +4125,7 @@
val uneqP_opt = NONE
-val sfP = K true
+val sfP = (fn t:term => true)
*)
@@ -3754,8 +4176,8 @@
let
val (uneq_pos, turn_flag) = valOf uneq_opt;
val sfb_thm1 = CONV_RULE (RHS_CONV (BAG_RESORT_CONV [points_to_pos, uneq_pos])) sfb_thm0
- val sfb_thm2 = CONV_RULE (RHS_CONV (bag_el_conv smallfoot_ap_unequal_comm___CONV 1))
- sfb_thm1
+ val sfb_thm2 = if turn_flag then CONV_RULE (RHS_CONV (bag_el_conv smallfoot_ap_unequal_comm___CONV 1)) sfb_thm1 else
+ sfb_thm1
in
sfb_thm2
end;
@@ -4040,9 +4462,18 @@
(smallfoot_ae_const y_const);
smallfoot_ap_unequal (smallfoot_ae_const y_const)
smallfoot_ae_null|})``
+val t = ``
+ (smallfoot_prop ({|t; x|},{| |})
+ {|smallfoot_ap_equal (smallfoot_ae_var t) (smallfoot_ae_var x);
+ smallfoot_ap_unequal (smallfoot_ae_var x) smallfoot_ae_null;
+ smallfoot_ap_data_list (smallfoot_tag "tl") (smallfoot_ae_var x)
+ FEMPTY|})``
+val ee = ``SMALLFOOT_P_EXPRESSION_EVAL (smallfoot_p_var x)``
*)
+
+
fun smallfoot_prop___extract_points_to ee t =
let
val e_thm_opt = SOME (SIMP_CONV arith_ss [SMALLFOOT_P_EXPRESSION_EVAL_def,
@@ -4206,13 +4637,12 @@
end
-
fun SMALLFOOT_COND_INFERENCE_CONV___field_lookup t =
let
- val thm0 = SMALLFOOT_COND_INFERENCE___block_to_seq_CONV t;
+ val (command,thm0_f) = SMALLFOOT_COND_INFERENCE___block_to_seq t;
+ val (v, e, tag) = dest_smallfoot_prog_field_lookup command;
+ val thm0 = thm0_f ();
val t' = rhs (concl thm0);
- val command = dest_SMALLFOOT_COND_HOARE_TRIPLE___first_command t';
- val (v, e, tag) = dest_smallfoot_prog_field_lookup command;
val ee = mk_comb (smallfoot_p_expression_eval_term, e);
val thm1 = MAKE___IMP___RULE (SMALLFOOT_COND_HOARE_TRIPLE___PRECOND_CONV (smallfoot_prop___extract_points_to ee) t');
@@ -4228,15 +4658,12 @@
-
-
-
fun SMALLFOOT_COND_INFERENCE_CONV___field_assign_internal tt =
let
val thm1 = PART...
[truncated message content] |