Skip to content

Commit

Permalink
Attempt fixes after 45a84e0
Browse files Browse the repository at this point in the history
  • Loading branch information
@xrchz
xrchz committed May 8, 2019
1 parent f3af758 commit 3b2a4f4
Show file tree
Hide file tree
Showing 3 changed files with 23 additions and 23 deletions.
20 changes: 10 additions & 10 deletions basis/TextIOProofScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2394,28 +2394,28 @@ Theorem copy_spec
NTAC 2 (first_x_assum (fn x => fs [x])) >>
qmatch_goalsub_abbrev_tac`IOx _ fs'` >>
`get_file_content fs' out = SOME(content2,LENGTH content2)`
by (fs[get_file_content_def,Abbr`fs'`,bumpFD_def,ALIST_FUPDKEY_ALOOKUP]) >>
by (fs[get_file_content_def,Abbr`fs'`,bumpFD_def,AFUPDKEY_ALOOKUP]) >>
xlet_auto
>-(fs[FD_def,iobuff_loc_def,Abbr`fs'`,liveFS_bumpFD,liveFS_def,validFD_bumpFD,
validFD_numchars,ALOOKUP_validFD,get_mode_def] >> xsimpl) >>
fs[MAP_MAP_o, CHR_w2n_n2w_ORD,TAKE_APPEND1,TAKE_TAKE,insert_atI_end] >>
qmatch_goalsub_abbrev_tac`IOFS fs''` >>
xapp >> fs[IOFS_def,IOFS_iobuff_def] >> xsimpl >>
fs[ALIST_FUPDKEY_ALOOKUP,insert_atI_def] >>
fs[AFUPDKEY_ALOOKUP,insert_atI_def] >>
map_every qexists_tac [`emp`, `pos + nr`,`fs''`,`content2 ++ TAKE nr (DROP pos content1)`] >>
xsimpl >> rw[Abbr`fs''`, Abbr`fs'`]
>-(fs[fsupdate_def,ALIST_FUPDKEY_ALOOKUP,bumpFD_def])
>-(fs[fsupdate_def,ALIST_FUPDKEY_ALOOKUP,bumpFD_def])
>-(fs[fsupdate_def,ALIST_FUPDKEY_ALOOKUP,bumpFD_def])
>-(fs[fsupdate_def,ALIST_FUPDKEY_ALOOKUP,bumpFD_def])
>-(fs[fsupdate_def,AFUPDKEY_ALOOKUP,bumpFD_def])
>-(fs[fsupdate_def,AFUPDKEY_ALOOKUP,bumpFD_def])
>-(fs[fsupdate_def,AFUPDKEY_ALOOKUP,bumpFD_def])
>-(fs[fsupdate_def,AFUPDKEY_ALOOKUP,bumpFD_def])
>-(qexists_tac`THE (LDROP k (THE (LTL ll)))` >> rw[]
>-(fs[fsupdate_numchars] >> irule wfFS_fsupdate >> conj_tac
>-(
`(bumpFD inp (fs with numchars := ll) nr).numchars = THE (LTL ll)`
by fs[bumpFD_numchars] >>
first_x_assum (fn x => rw[GSYM x]) >>
fs[wfFS_bumpFD,wfFS_LDROP ])
>-(fs[bumpFD_def,MAP_FST_ALIST_FUPDKEY] >> simp[MEM_MAP] >>
>-(fs[bumpFD_def,MAP_FST_AFUPDKEY] >> simp[MEM_MAP] >>
imp_res_tac ALOOKUP_MEM >>
qexists_tac`(out,ino2,WriteMode,STRLEN content2)` >> fs[]))
>-(irule STD_streams_fsupdate >> rw[] >>
Expand All @@ -2427,8 +2427,8 @@ Theorem copy_spec
fs[GEN_ALL STD_streams_bumpFD,GSYM STD_streams_numchars])
>-(qmatch_abbrev_tac`IOx fs_ffi_part fs1 ==>> IOx fs_ffi_part fs2` >>
`fs2 = fs1` suffices_by xsimpl >> unabbrev_all_tac >>
fs[ALIST_FUPDKEY_ALOOKUP,insert_atI_end,TAKE_APPEND,TAKE_TAKE, fsupdate_def,
bumpFD_def,ALIST_FUPDKEY_unchanged] >> rw[IO_fs_component_equality]))
fs[AFUPDKEY_ALOOKUP,insert_atI_end,TAKE_APPEND,TAKE_TAKE, fsupdate_def,
bumpFD_def,AFUPDKEY_unchanged] >> rw[IO_fs_component_equality]))
>-(qexists_tac`x` >>
qmatch_goalsub_abbrev_tac`IOx fs_ffi_part (fs1 with numchars := x)
==>> IOx fs_ffi_part (fs2 with numchars := x) * GC` >>
Expand All @@ -2440,7 +2440,7 @@ Theorem copy_spec
ALOOKUP fs'.infds out = SOME (ino2,WriteMode,STRLEN content2) ∧
ALOOKUP fs'.inode_tbl ino1 = SOME content1 ∧
ALOOKUP fs'.inode_tbl ino2 = SOME content2`
by fs[Abbr`fs'`,forwardFD_def,ALIST_FUPDKEY_ALOOKUP] >>
by fs[Abbr`fs'`,forwardFD_def,AFUPDKEY_ALOOKUP] >>
fs[GSYM fsupdate_fastForwardFD_comm,fsupdate_numchars] >>
fs[Abbr`fs'`,fastForwardFD_with_numchars,fastForwardFD_forwardFD] >>
fs[GSYM DROP_DROP] >>
Expand Down
6 changes: 3 additions & 3 deletions basis/fsFFIPropsScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -440,7 +440,7 @@ Theorem wfFS_fastForwardFD[simp]
\\ pairarg_tac \\ fs[]
\\ Cases_on`ALOOKUP fs.inode_tbl ino` \\ fs[libTheory.the_def]
\\ rw[]
>-(res_tac \\ simp[ALIST_FUPDKEY_ALOOKUP] \\ CASE_TAC \\ fs[])
>-(res_tac \\ simp[AFUPDKEY_ALOOKUP] \\ CASE_TAC \\ fs[])
>-(fs[consistentFS_def] \\ rw[] \\ res_tac)
>-(fs[liveFS_def]))

Expand All @@ -453,8 +453,8 @@ Theorem fsupdate_fastForwardFD_comm
ino1 ≠ ino2 ⇒
fsupdate (fastForwardFD fs fd1) fd2 k p c =
fastForwardFD (fsupdate fs fd2 k p c) fd1`
(rw[fsupdate_def,fastForwardFD_def,ALIST_FUPDKEY_ALOOKUP] >> EVAL_TAC >>
fs[ALIST_FUPDKEY_ALOOKUP,IO_fs_component_equality,ALIST_FUPDKEY_comm]);
(rw[fsupdate_def,fastForwardFD_def,AFUPDKEY_ALOOKUP] >> EVAL_TAC >>
fs[AFUPDKEY_ALOOKUP,IO_fs_component_equality,AFUPDKEY_comm]);

(* fsupdate *)

Expand Down
20 changes: 10 additions & 10 deletions examples/iocatProgScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -90,10 +90,10 @@ val cat_spec0 = Q.prove(
>- res_tac
>-(fs[MEM_FST_ALOOKUP_SOME])
>- res_tac) >> fs[] >> rw[]
>- fs[fsupdate_def,ALIST_FUPDKEY_ALOOKUP,openFileFS_files,A_DELKEY_nextFD_openFileFS,
A_DELKEY_ALIST_FUPDKEY_comm,ALOOKUP_inFS_fname_openFileFS_nextFD,A_DELKEY_fastForwardFD_elim]
>- fs[fsupdate_def,ALIST_FUPDKEY_ALOOKUP,openFileFS_files,A_DELKEY_nextFD_openFileFS,
A_DELKEY_ALIST_FUPDKEY_comm,ALOOKUP_inFS_fname_openFileFS_nextFD,A_DELKEY_fastForwardFD_elim]
>- fs[fsupdate_def,AFUPDKEY_ALOOKUP,openFileFS_files,ADELKEY_nextFD_openFileFS,
ADELKEY_AFUPDKEY_comm,ALOOKUP_inFS_fname_openFileFS_nextFD,ADELKEY_fastForwardFD_elim]
>- fs[fsupdate_def,AFUPDKEY_ALOOKUP,openFileFS_files,ADELKEY_nextFD_openFileFS,
ADELKEY_AFUPDKEY_comm,ALOOKUP_inFS_fname_openFileFS_nextFD,ADELKEY_fastForwardFD_elim]
>-(qmatch_goalsub_abbrev_tac`inFS_fname fs1` >>
`consistentFS fs1`
by (unabbrev_all_tac >> fs[consistentFS_def,fsupdate_def,openFileFS_def] >>
Expand All @@ -103,16 +103,16 @@ val cat_spec0 = Q.prove(
\\ `fs' = up_stdout fs (implode (out ++ content))`
by (
fs[Abbr`fs'`,up_stdo_def,IO_fs_component_equality,fsupdate_def,
openFileFS_numchars,openFileFS_inode_tbl,ALIST_FUPDKEY_ALOOKUP,openFileFS_files,
ALOOKUP_inFS_fname_openFileFS_nextFD,A_DELKEY_ALIST_FUPDKEY_comm,
A_DELKEY_nextFD_openFileFS,ALIST_FUPDKEY_unchanged] ) \\
openFileFS_numchars,openFileFS_inode_tbl,AFUPDKEY_ALOOKUP,openFileFS_files,
ALOOKUP_inFS_fname_openFileFS_nextFD,ADELKEY_AFUPDKEY_comm,
ADELKEY_nextFD_openFileFS,AFUPDKEY_unchanged] ) \\
qunabbrev_tac`fs'` \\ pop_assum SUBST_ALL_TAC \\
qmatch_goalsub_abbrev_tac`ALOOKUP fs'.inode_tbl _` \\
`fs'.inode_tbl = ALIST_FUPDKEY (UStream (strlit "stdout")) (λ_. out++content) fs.inode_tbl` by (
`fs'.inode_tbl = AFUPDKEY (UStream (strlit "stdout")) (λ_. out++content) fs.inode_tbl` by (
fs[Abbr`fs'`,up_stdo_def,fsupdate_def,ALOOKUP_inFS_fname_openFileFS_nextFD,
ALIST_FUPDKEY_ALOOKUP,K_DEF,ALIST_FUPDKEY_unchanged]) \\
AFUPDKEY_ALOOKUP,K_DEF,AFUPDKEY_unchanged]) \\
qunabbrev_tac`fs'` \\ pop_assum SUBST_ALL_TAC \\
simp[ALIST_FUPDKEY_ALOOKUP] \\
simp[AFUPDKEY_ALOOKUP] \\
qmatch_goalsub_abbrev_tac`MAP f` \\
qmatch_goalsub_abbrev_tac`_::(MAP f' _)` \\
`f = f'` by (
Expand Down

0 comments on commit 3b2a4f4

Please sign in to comment.