Skip to content

Commit

Permalink
Merge pull request #703 from CakeML/cfletautolib-fix
Browse files Browse the repository at this point in the history 
Make cfLetAutoLib robust against load order
  • Loading branch information
@myreen
myreen committed Nov 15, 2019
2 parents da2db1b + d61723d commit 140e323
Show file tree
Hide file tree
Showing 4 changed files with 76 additions and 75 deletions.
130 changes: 63 additions & 67 deletions basis/HashtableProofScript.sml
View file
Expand Up @@ -1315,88 +1315,84 @@ Theorem hashtable_delete_spec:
(POSTv uv. &(UNIT_TYPE () uv) * HASHTABLE a b hf cmp (h \\ k) htv)
Proof
xcf_with_def "Hashtable.delete" Hashtable_delete_v_def
\\ fs[HASHTABLE_def, REF_ARRAY_def, hashtable_inv_def]
\\ fs [HASHTABLE_def, REF_ARRAY_def, hashtable_inv_def]
\\ xpull
\\ xmatch
\\ xlet_auto
>-(CONV_TAC(RESORT_EXISTS_CONV List.rev)
\\ qexists_tac `arr` \\ xsimpl)
\\ xlet_auto >- xsimpl
\\ xlet `POSTv bv. &(NUM (LENGTH vlv) bv) *
REF_ARRAY ar arr vlv *
REF_NUM ur heuristic_size`
>-( fs[REF_ARRAY_def] \\ xapp
\\ CONV_TAC(RESORT_EXISTS_CONV List.rev)
\\ qexists_tac `vlv` \\ xsimpl)
ar ~~> arr *
ARRAY arr vlv *
REF_NUM ur heuristic_size`
>- (xapp \\ xsimpl)
\\ xlet_auto >- xsimpl
\\ xlet_auto >- xsimpl
\\ fs[REF_ARRAY_def]
\\ xlet_auto >-( xsimpl \\ fs[LENGTH_NIL,NOT_NIL_EQ_LENGTH_NOT_0, MOD_LESS])
\\ `LENGTH buckets = LENGTH vlv` by (imp_res_tac LIST_REL_LENGTH)
\\ imp_res_tac LIST_REL_LENGTH
\\ `hf k MOD LENGTH vlv < LENGTH buckets`
by fs[LENGTH_NIL,NOT_NIL_EQ_LENGTH_NOT_0, MOD_LESS]
by fs [LENGTH_NIL,NOT_NIL_EQ_LENGTH_NOT_0, MOD_LESS]
\\ `MAP_TYPE a b (EL (hf k MOD LENGTH vlv) buckets)
(EL (hf k MOD LENGTH vlv) vlv)`
by fs[LIST_REL_EL_EQN]
(EL (hf k MOD LENGTH vlv) vlv)`
by fs[LIST_REL_EL_EQN]
\\ xlet_auto >- xsimpl
\\ xlet_auto >- xsimpl
\\ xlet_auto >- xsimpl
\\ xlet_auto >- xsimpl
\\ xlet_auto >- xsimpl
\\ xlet `POSTv fv.
&(BOOL (¬(mlmap$null (EL (hf k MOD LENGTH vlv) buckets)) /\ mlmap$null
(mlmap$delete (EL (hf k MOD LENGTH vlv) buckets) k)) fv) *
ARRAY yv (LUPDATE v' (hf k MOD LENGTH vlv) vlv) * ar ~~> yv *
REF_NUM ur heuristic_size`
>-(xlog
\\CASE_TAC
>-(xapp \\ fs[PULL_EXISTS]
\\ CONV_TAC(RESORT_EXISTS_CONV List.rev)
\\ MAP_EVERY qexists_tac [`b`, `a`,
`(delete (EL (hf k MOD LENGTH vlv) buckets) k)`]
\\xsimpl)
>-(xsimpl))
\\xlet `POSTv jv.
&(BOOL (¬(mlmap$null (EL (hf k MOD LENGTH vlv) buckets)) /\
mlmap$null (mlmap$delete (EL (hf k MOD LENGTH vlv)
buckets) k) /\
0 < heuristic_size) jv) *
mlmap$null
(mlmap$delete (EL (hf k MOD LENGTH vlv) buckets) k)) fv) *
ARRAY yv (LUPDATE v' (hf k MOD LENGTH vlv) vlv) * ar ~~> yv *
REF_NUM ur heuristic_size`
>-(xlog
\\ CASE_TAC
>-(fs[REF_NUM_def] \\ xpull \\ xlet_auto >-(xsimpl)
>-(xapp \\ fs[PULL_EXISTS]
\\ CONV_TAC(RESORT_EXISTS_CONV List.rev)
\\qexists_tac `&heuristic_size`
\\xsimpl \\ fs[NUM_def]))
>-(xsimpl \\ fs[NUM_def]))
>-(xif
>-(fs[REF_NUM_def] \\ xpull \\ xlet_auto >- xsimpl
>-(fs[NUM_def] \\ xlet_auto >- xsimpl
>-(xapp \\ CONV_TAC(RESORT_EXISTS_CONV List.rev)
\\qexists_tac `yv'` \\ xsimpl
\\ ntac 2 strip_tac
\\ MAP_EVERY qexists_tac
[`ur`, `ar`, `hfv`, `(LUPDATE v' (hf k MOD LENGTH vlv) vlv)`,
`yv`, `cmpv`, `heuristic_size - 1`, `iv`] \\ xsimpl
\\ qexists_tac `(LUPDATE (mlmap$delete (EL (hf k MOD LENGTH vlv) buckets) k)
(hf k MOD LENGTH vlv) buckets)`
\\ `buckets <> []` by (imp_res_tac LIST_REL_LENGTH
\\ fs[NOT_NIL_EQ_LENGTH_NOT_0])
\\imp_res_tac list_union_lupdate_delete \\ rfs[]
\\fs[buckets_ok_delete, every_map_ok_delete,
every_cmp_of_delete, list_rel_delete]
\\ fs[INT_def] \\ fs[int_arithTheory.INT_NUM_SUB])))
\\ xcon \\ xsimpl
\\ MAP_EVERY qexists_tac
[`ur`, `ar`, `hfv`, `(LUPDATE v' (hf k MOD LENGTH vlv) vlv)`,
`yv`, `cmpv`, `heuristic_size `] \\ xsimpl
\\qexists_tac `(LUPDATE (mlmap$delete (EL (hf k MOD LENGTH vlv) buckets) k)
(hf k MOD LENGTH vlv) buckets)`
\\ `buckets <> []` by (imp_res_tac LIST_REL_LENGTH
\\ fs[NOT_NIL_EQ_LENGTH_NOT_0])
\\imp_res_tac list_union_lupdate_delete \\ rfs[]
\\fs[buckets_ok_delete, every_map_ok_delete,
every_cmp_of_delete, list_rel_delete])
>-
(xlog
\\ CASE_TAC \\ xsimpl
\\ xapp
\\ xsimpl
\\ goal_assum (first_assum o mp_then Any mp_tac)
\\ rw [])
\\ xlet `POSTv jv.
&(BOOL (¬(mlmap$null (EL (hf k MOD LENGTH vlv) buckets)) /\
mlmap$null (mlmap$delete (EL (hf k MOD LENGTH vlv)
buckets) k) /\
0 < heuristic_size) jv) *
ARRAY yv (LUPDATE v' (hf k MOD LENGTH vlv) vlv) * ar ~~> yv *
REF_NUM ur heuristic_size`
>-
(xlog
\\ fs [REF_NUM_def, NUM_def]
\\ CASE_TAC \\ xsimpl \\ fs []
\\ xpull
\\ xlet_auto >- xsimpl
\\ xapp
\\ xsimpl \\ fs []
\\ asm_exists_tac \\ rw [])
\\ fs [REF_NUM_def, NUM_def]
\\ xpull
\\ xif
>-
(xlet_auto >- xsimpl
\\ fs []
\\ xlet_auto >- xsimpl
\\ xapp
\\ xsimpl \\ rw []
\\ MAP_EVERY qexists_tac
[`ur`, `ar`, `hfv`, `(LUPDATE v' (hf k MOD LENGTH vlv) vlv)`,
`arr`, `cmpv`, `heuristic_size - 1`, `nv2`] \\ xsimpl
\\ qexists_tac `LUPDATE (mlmap$delete (EL (hf k MOD LENGTH vlv) buckets) k)
(hf k MOD LENGTH vlv) buckets`
\\ imp_res_tac list_union_lupdate_delete \\ rfs[]
\\ fs [buckets_ok_delete, every_map_ok_delete,
every_cmp_of_delete, list_rel_delete, NOT_NIL_EQ_LENGTH_NOT_0,
NUM_def, INT_def, int_arithTheory.INT_NUM_SUB])
\\ xcon
\\ xsimpl
\\ xsimpl
\\ goal_assum (first_assum o mp_then Any mp_tac)
\\ qexists_tac `LUPDATE (mlmap$delete (EL (hf k MOD LENGTH vlv) buckets) k)
(hf k MOD LENGTH vlv) buckets`
\\ imp_res_tac list_union_lupdate_delete \\ rfs []
\\ fs [buckets_ok_delete, every_map_ok_delete, every_cmp_of_delete,
list_rel_delete, NOT_NIL_EQ_LENGTH_NOT_0]
QED

Theorem hashtable_clear_spec:
Expand Down
2 changes: 1 addition & 1 deletion basis/TextIOProofScript.sml
View file
Expand Up @@ -2493,7 +2493,7 @@ Proof
\\ `i ≤ LENGTH content` by rw[Abbr`i`]
\\ `j + pos < i` by rw[Abbr`i`]
\\ `i ≤ pos + LENGTH arr` by rw[Abbr`i`]
\\ `NUM (i-pos) nv2` by ( rw[Abbr`i`] \\ fs[] )
\\ `NUM (i-pos) nv3` by ( rw[Abbr`i`] \\ fs[] )
\\ qexists_tac`i - pos`
\\ simp[]
\\ `fs2 = forwardFD fs' fd (i - pos - j)`
Expand Down
17 changes: 11 additions & 6 deletions characteristic/cfLetAutoLib.sml
View file
Expand Up @@ -86,9 +86,9 @@ fun add_expand_retract_thms expandThms retractThms =
fun get_expand_thms () = !RI_EXPAND_THMSL;
fun get_retract_thms () = !RI_RETRACT_THMSL;

val EXPAND_TAC = FULL_SIMP_TAC (srw_ss()) (get_expand_thms());
val RETRACT_TAC = FULL_SIMP_TAC (srw_ss()) (get_retract_thms());
val REWRITE_RI_TAC = EXPAND_TAC THEN RETRACT_TAC;
fun EXPAND_TAC g = FULL_SIMP_TAC (srw_ss()) (get_expand_thms()) g;
fun RETRACT_TAC g = FULL_SIMP_TAC (srw_ss()) (get_retract_thms()) g;
fun REWRITE_RI_TAC g = (EXPAND_TAC THEN RETRACT_TAC) g;

(* List of equality types *)
val EQUALITY_TYPE_THMS = ref ([] : thm list);
Expand Down Expand Up @@ -216,13 +216,18 @@ fun add_rewrite_thms thms = (RW_THMS := thms @ !RW_THMS);
fun get_rewrite_thms () = !RW_THMS;

(* Default simpset *)
val DEF_SIMPSET = ref pure_ss;
val _ = (DEF_SIMPSET := srw_ss());
val DEF_SIMPSET = ref list_ss;

(* TODO: Find a way to export that - like with ThmSetData.new_exporter *)
fun add_simp_frag sf = (DEF_SIMPSET := ((!DEF_SIMPSET) ++ sf));
fun get_default_simpset () = !DEF_SIMPSET;

val _ = List.app (add_simp_frag o BasicProvers.thy_ssfrag)
["cfTactics",
"cfHeapsBase",
"cf",
"integer"
];

fun add_refinement_invariants ri_defs =
let
val (expandThms, retractThms) = generate_expand_retract_thms ri_defs
Expand Down
2 changes: 1 addition & 1 deletion examples/divScript.sml
View file
Expand Up @@ -65,7 +65,7 @@ Proof
\\ xlet_auto THEN1 xsimpl
\\ xapp
\\ MAP_EVERY qexists_tac [`emp`, `u`, `s`, `ns`]
\\ xsimpl \\ fs [INT_def] \\ intLib.COOPER_TAC)
\\ xsimpl \\ fs [INT_def, NUM_def])
THEN1 (
fs [SEP_CLAUSES] \\ fs [SEP_F_to_cond, POSTvd_def, GSYM POSTd_def]
\\ xcf_div "condLoop" st
Expand Down

0 comments on commit 140e323

Please sign in to comment.