diff --git a/compiler/README.md b/compiler/README.md index dfb7cd5d25..f6d898d83b 100644 --- a/compiler/README.md +++ b/compiler/README.md @@ -42,3 +42,6 @@ Correctness proof for the CakeML compiler. [repl](repl): Some definitions and proofs used in the proof of the CakeML and Candle read-eval-print loop (REPL). + +[scheme](scheme): +A compiler from Scheme to CakeML diff --git a/compiler/scheme/Holmakefile b/compiler/scheme/Holmakefile new file mode 100644 index 0000000000..4f9d1adf09 --- /dev/null +++ b/compiler/scheme/Holmakefile @@ -0,0 +1,20 @@ +INCLUDES = $(CAKEMLDIR)/translator \ + $(CAKEMLDIR)/basis \ + $(CAKEMLDIR)/basis/pure \ + $(CAKEMLDIR)/compiler/parsing \ + $(CAKEMLDIR)/semantics \ + $(CAKEMLDIR)/misc \ + $(HOLDIR)/examples/formal-languages/context-free + +all: $(DEFAULT_TARGETS) README.md +.PHONY: all + +README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml) +# Filter out unverified/ (they don't have a readmePrefix) +DIRS = $(patsubst examples/,,$(patsubst unverified/,,$(wildcard */))) +README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix unverified/README.md examples/README.md $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES) + $(CAKEMLDIR)/developers/readme_gen $(README_SOURCES) + +ifdef POLY +HOLHEAP = $(CAKEMLDIR)/misc/cakeml-heap +endif diff --git a/compiler/scheme/README.md b/compiler/scheme/README.md new file mode 100644 index 0000000000..a54bda6550 --- /dev/null +++ b/compiler/scheme/README.md @@ -0,0 +1,34 @@ +A compiler from Scheme to CakeML + +[compilation](compilation): +Compilation scripts for the Scheme-to-CakeML compiler. + +[examples](examples): +Example Scheme programs compiled using the Scheme compiler + +[proofs](proofs): +Proofs for Scheme to CakeML compiler + +[scheme_astScript.sml](scheme_astScript.sml): +AST of Scheme + +[scheme_compilerScript.sml](scheme_compilerScript.sml): +Definition of a compiler from Scheme to CakeML + +[scheme_parsingScript.sml](scheme_parsingScript.sml): +Parser for Scheme + +[scheme_semanticsScript.sml](scheme_semanticsScript.sml): +Semantics of Scheme + +[scheme_to_cakeScript.sml](scheme_to_cakeScript.sml): +Code generator for Scheme to CakeML compiler + +[scheme_valuesScript.sml](scheme_valuesScript.sml): +Definition of Scheme values + +[translation](translation): +CakeML translation of Scheme-to-CakeML compiler + +[unverified](unverified): +An unverified compiler from Scheme to ML written in Haskell diff --git a/compiler/scheme/compilation/Holmakefile b/compiler/scheme/compilation/Holmakefile new file mode 100644 index 0000000000..5496db4357 --- /dev/null +++ b/compiler/scheme/compilation/Holmakefile @@ -0,0 +1,12 @@ +INCLUDES = $(CAKEMLDIR)/compiler/scheme/translation $(CAKEMLDIR)/compiler $(CAKEMLDIR)/cv_translator $(CAKEMLDIR)/developers/bin + +all: $(DEFAULT_TARGETS) README.md +.PHONY: all +README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml) +DIRS = $(wildcard */) +README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES) + $(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES) + +ifdef POLY +HOLHEAP = $(CAKEMLDIR)/cv_translator/cake_compile_heap +endif diff --git a/compiler/scheme/compilation/README.md b/compiler/scheme/compilation/README.md new file mode 100644 index 0000000000..4ca533e13c --- /dev/null +++ b/compiler/scheme/compilation/README.md @@ -0,0 +1,4 @@ +Compilation scripts for the Scheme-to-CakeML compiler. + +[scheme_compilerCompileScript.sml](scheme_compilerCompileScript.sml): +In-logic compilation of the Scheme-to-CakeML compiler diff --git a/compiler/scheme/compilation/readmePrefix b/compiler/scheme/compilation/readmePrefix new file mode 100644 index 0000000000..5ef8d1d6d9 --- /dev/null +++ b/compiler/scheme/compilation/readmePrefix @@ -0,0 +1 @@ +Compilation scripts for the Scheme-to-CakeML compiler. diff --git a/compiler/scheme/compilation/scheme_compilerCompileScript.sml b/compiler/scheme/compilation/scheme_compilerCompileScript.sml new file mode 100644 index 0000000000..d1f46195d5 --- /dev/null +++ b/compiler/scheme/compilation/scheme_compilerCompileScript.sml @@ -0,0 +1,13 @@ +(* + In-logic compilation of the Scheme-to-CakeML compiler +*) + +open preamble scheme_compilerProgTheory eval_cake_compile_x64Lib; + +val _ = new_theory "scheme_compilerCompile"; + +Theorem scheme_compiler_compiled = + eval_cake_compile_x64 "" scheme_compiler_prog_def + "scheme_compiler.S"; + +val _ = export_theory (); diff --git a/compiler/scheme/examples/Makefile b/compiler/scheme/examples/Makefile new file mode 100644 index 0000000000..5fac3c5129 --- /dev/null +++ b/compiler/scheme/examples/Makefile @@ -0,0 +1,58 @@ +.PHONY: all clean + +OS ?= $(shell uname) + +ifeq ($(OS),Windows_NT) + PREF = + SUFF = .exe + EVALFLAG = +else + PREF = ./ + SUFF = + EVALFLAG = -DEVAL +endif + +CAKEOPT = --sexp=true + +ifeq ($(OS),Darwin) + # These options avoid linker warnings on macOS + LDFLAGS += -Wl,-no_pie + EVALFLAG = +endif + +ALL = $(patsubst %.scm,%.cake$(SUFF),$(wildcard *.scm)) + +CFLAGS+=-O2 +LDLIBS+=-lm + +ARCH=x64 +WORD_SIZE=64 + +all: $(ALL) + +%.cake.S: %.scm cake scheme_compiler$(SUFF) + cat $< | $(PREF)scheme_compiler$(SUFF) | $(PREF)cake$(SUFF) $(CAKEOPT) > $@ + +%.cake$(SUFF) : %.cake.S ../../../basis/basis_ffi.c + $(CC) $< ../../../basis/basis_ffi.c $(LOADLIBES) $(LDLIBS) -o $@ $(LDFLAGS) + +scheme_compiler.S: ../compilation/scheme_compiler.S + cp $< $@ + +scheme_compiler$(SUFF): scheme_compiler.S ../../../basis/basis_ffi.c + $(CC) -o $@ scheme_compiler.S ../../../basis/basis_ffi.c $(LDLIBS) + +cake.S: + @if [ ! -f "../../bootstrap/compilation/x64/64/$(@F)" ] ; then $(MAKE) download ; else cp ../../bootstrap/compilation/x64/64/$(@F) $@ ; fi + +download: + @echo "$(red)Could not find \`cake.S\`. Downloading the latest version from CakeML's GitHub releases.$(reset)" + curl -LO https://github.com/CakeML/cakeml/releases/latest/download/cake-$(ARCH)-$(WORD_SIZE).tar.gz + @tar -zxf cake-$(ARCH)-$(WORD_SIZE).tar.gz --strip-components 1 cake-$(ARCH)-$(WORD_SIZE)/cake.S + @rm cake-$(ARCH)-$(WORD_SIZE).tar.gz + +cake$(SUFF): cake.S ../../../basis/basis_ffi.c + $(CC) $(CFLAGS) $< ../../../basis/basis_ffi.c $(LOADLIBES) $(EVALFLAG) -o $@ $(LDFLAGS) $(LDLIBS) + +clean: + rm cake$(SUFF) cake.S scheme_compiler$(SUFF) scheme_compiler.S *.cake.S *.cake$(SUFF) diff --git a/compiler/scheme/examples/README.md b/compiler/scheme/examples/README.md new file mode 100644 index 0000000000..3ca08042a5 --- /dev/null +++ b/compiler/scheme/examples/README.md @@ -0,0 +1 @@ +Example Scheme programs compiled using the Scheme compiler diff --git a/compiler/scheme/examples/facimp.scm b/compiler/scheme/examples/facimp.scm new file mode 100644 index 0000000000..868f28093e --- /dev/null +++ b/compiler/scheme/examples/facimp.scm @@ -0,0 +1,4 @@ +(letrec ((fac (lambda (x) + (letrec ((st 0) (acc 1)) (begin + (call/cc (lambda (k) (set! st k))) + (if (eqv? x 0) acc (st (begin (set! acc ( * acc x)) (set! x (- x 1)))))))))) (fac 6)) diff --git a/compiler/scheme/examples/fib.scm b/compiler/scheme/examples/fib.scm new file mode 100644 index 0000000000..569499e5a6 --- /dev/null +++ b/compiler/scheme/examples/fib.scm @@ -0,0 +1,7 @@ +(letrec + ((fib (lambda (n) + (if (eqv? n 0) n + (if (eqv? n 1) n + (+ (fib (- n 1)) + (fib (- n 2)))))))) + (fib 30)) diff --git a/compiler/scheme/examples/list.scm b/compiler/scheme/examples/list.scm new file mode 100644 index 0000000000..28ee6d5bef --- /dev/null +++ b/compiler/scheme/examples/list.scm @@ -0,0 +1,9 @@ +(letrec ( + (cons (lambda (car cdr) (lambda (b) (if b car cdr)))) + (car (lambda (cons) (cons #t))) + (cdr (lambda (cons) (cons #f))) + (nil 999) + (nil? (lambda (l) (eqv? l nil))) + (length (lambda (l) (if (nil? l) 0 (+ 1 (length (cdr l)))))) + (index (lambda (n l) (if (eqv? n 0) (car l) (index (- n 1) (cdr l))))) +) (index 1 (cons 10 (cons 20 (cons 30 nil))))) diff --git a/compiler/scheme/examples/nondet.scm b/compiler/scheme/examples/nondet.scm new file mode 100644 index 0000000000..50afb3bd6e --- /dev/null +++ b/compiler/scheme/examples/nondet.scm @@ -0,0 +1,35 @@ +(letrec + ((nondet + (lambda (fun) + (call/cc + (lambda (cc) + (letrec ((k cc)) + (fun + (lambda (f n m) + (letrec ((i n) + (last k)) + (begin + (call/cc + (lambda (cc) (set! k (lambda (v) (begin (set! i (+ i 1)) (cc v)))))) + (if (eqv? i m) + (begin (set! k last) (k (- 1))) + (f i))))) + (lambda () (k (- 1))))))))) + + (triangle + (lambda (n) + (if (eqv? n 0) n + (+ n (triangle (- n 1)))))) + (fib + (lambda (n) + (if (eqv? n 0) n + (if (eqv? n 1) n + (+ (fib (- n 1)) + (fib (- n 2)))))))) + + ;(display + (nondet + (lambda (choose fail) + (letrec ((x (choose triangle 3 10)) + (y (choose fib 3 10))) + (if (eqv? x y) x (fail))))));) diff --git a/compiler/scheme/examples/print.scm b/compiler/scheme/examples/print.scm new file mode 100644 index 0000000000..7371dc8d72 --- /dev/null +++ b/compiler/scheme/examples/print.scm @@ -0,0 +1 @@ +(letrec ((touch 0)) (begin (set! touch 1) touch)) diff --git a/compiler/scheme/examples/tailfib.scm b/compiler/scheme/examples/tailfib.scm new file mode 100644 index 0000000000..39a90854ed --- /dev/null +++ b/compiler/scheme/examples/tailfib.scm @@ -0,0 +1,5 @@ +(letrec + ((fib (lambda (n a b) + (if (eqv? n 0) a + (fib (- n 1) (+ a b) a))))) + (fib 35 0 1)) diff --git a/compiler/scheme/proofs/Holmakefile b/compiler/scheme/proofs/Holmakefile new file mode 100644 index 0000000000..366d8e8b5b --- /dev/null +++ b/compiler/scheme/proofs/Holmakefile @@ -0,0 +1,21 @@ +INCLUDES = $(CAKEMLDIR)/translator \ + $(CAKEMLDIR)/basis \ + $(CAKEMLDIR)/basis/pure \ + $(CAKEMLDIR)/compiler/parsing \ + $(CAKEMLDIR)/semantics \ + $(CAKEMLDIR)/misc \ + $(HOLDIR)/examples/formal-languages/context-free \ + $(CAKEMLDIR)/compiler/scheme + +all: $(DEFAULT_TARGETS) README.md +.PHONY: all + +README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml) +# Filter out tests/ (they don't have a readmePrefix) +DIRS = $(patsubst tests/,,$(wildcard */)) +README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES) + $(CAKEMLDIR)/developers/readme_gen $(README_SOURCES) + +ifdef POLY +HOLHEAP = $(CAKEMLDIR)/misc/cakeml-heap +endif diff --git a/compiler/scheme/proofs/README.md b/compiler/scheme/proofs/README.md new file mode 100644 index 0000000000..521f60311e --- /dev/null +++ b/compiler/scheme/proofs/README.md @@ -0,0 +1,7 @@ +Proofs for Scheme to CakeML compiler + +[scheme_semanticsPropsScript.sml](scheme_semanticsPropsScript.sml): +Proofs of Scheme semantics properties + +[scheme_to_cakeProofScript.sml](scheme_to_cakeProofScript.sml): +Proof of semantic preservation from Scheme to CakeML diff --git a/compiler/scheme/proofs/readmePrefix b/compiler/scheme/proofs/readmePrefix new file mode 100644 index 0000000000..07c4426a11 --- /dev/null +++ b/compiler/scheme/proofs/readmePrefix @@ -0,0 +1 @@ +Proofs for Scheme to CakeML compiler diff --git a/compiler/scheme/proofs/scheme_semanticsPropsScript.sml b/compiler/scheme/proofs/scheme_semanticsPropsScript.sml new file mode 100644 index 0000000000..839f272fb3 --- /dev/null +++ b/compiler/scheme/proofs/scheme_semanticsPropsScript.sml @@ -0,0 +1,1087 @@ +(* + Proofs of Scheme semantics properties +*) +open preamble; +open mlstringTheory; +open scheme_astTheory; +open scheme_semanticsTheory; +open finite_mapTheory; + +val _ = new_theory "scheme_semanticsProps"; + +Inductive can_lookup: + FEVERY (λ (x, n). n < LENGTH store) env + ⇒ + can_lookup env store +End + +Inductive valid_val: +[~val_SNum:] + valid_val store (SNum n) +[~val_SBool:] + valid_val store (SBool b) +[~val_Prim:] + valid_val store (Prim p) +[~val_Wrong:] + valid_val store (Wrong w) +[~val_SList:] + EVERY (valid_val store) vs + ⇒ + valid_val store (SList vs) +[~val_Proc_NONE:] + static_scope (FDOM env ∪ set xs) e ∧ + can_lookup env store + ⇒ + valid_val store (Proc env xs NONE e) +[~val_Proc_SOME:] + static_scope (FDOM env ∪ set (x::xs)) e ∧ + can_lookup env store + ⇒ + valid_val store (Proc env xs (SOME x) e) +[~val_Throw:] + valid_cont store ks + ⇒ + valid_val store (Throw ks) + +[~cont_Id:] + valid_cont store [] +[~cont_CondK:] + static_scope (FDOM env) t ∧ + static_scope (FDOM env) f ∧ + valid_cont store ks ∧ + can_lookup env store + ⇒ + valid_cont store ((env, CondK t f)::ks) +[~cont_ApplyK_NONE:] + EVERY (static_scope (FDOM env)) es ∧ + valid_cont store ks ∧ + can_lookup env store + ⇒ + valid_cont store ((env, ApplyK NONE es)::ks) +[~cont_ApplyK_SOME:] + valid_val store fn ∧ + EVERY (valid_val store) vs ∧ + EVERY (static_scope (FDOM env)) es ∧ + valid_cont store ks ∧ + can_lookup env store + ⇒ + valid_cont store ((env, ApplyK (SOME (fn, vs)) es)::ks) +[~cont_BeginK:] + EVERY (static_scope (FDOM env)) es ∧ + static_scope (FDOM env) e ∧ + valid_cont store ks ∧ + can_lookup env store + ⇒ + valid_cont store ((env, BeginK es e)::ks) +[~cont_SetK:] + (FDOM env) x ∧ + valid_cont store ks ∧ + can_lookup env store + ⇒ + valid_cont store ((env, SetK x)::ks) +[~cont_LetinitK:] + EVERY (FDOM env) (MAP FST xvs) ∧ + EVERY (valid_val store) (MAP SND xvs) ∧ + (FDOM env) x ∧ + EVERY (FDOM env) (MAP FST bs) ∧ + EVERY (static_scope (FDOM env)) (MAP SND bs) ∧ + static_scope (FDOM env) e ∧ + valid_cont store ks ∧ + can_lookup env store + ⇒ + valid_cont store ((env, LetinitK xvs x bs e)::ks) +End + +Inductive valid_state: +[~Val:] + valid_val store v ∧ + valid_cont store ks ∧ + can_lookup env store ∧ + EVERY (OPTION_ALL (valid_val store)) store + ⇒ + valid_state store ks env (Val v) +[~Exp:] + static_scope (FDOM env) e ∧ + valid_cont store ks ∧ + can_lookup env store ∧ + EVERY (OPTION_ALL (valid_val store)) store + ⇒ + valid_state store ks env (Exp e) +[~Exception:] + valid_state store ks env (Exception s) +End + +Definition terminating_state_def: + terminating_state (store, ks, env, e) + ⇔ (ks = [] ∧ ∃ v . e = Val v) ∨ (∃ ex . e = Exception ex) +End + +Theorem FEVERY_MONO: + ∀ P Q f . + (∀ x . P x ⇒ Q x) ∧ FEVERY P f + ⇒ + FEVERY Q f +Proof + Induct_on ‘f’ + >> rpt strip_tac >- simp[FEVERY_FEMPTY] + >> last_x_assum $ drule_then assume_tac + >> gvs[FEVERY_FUPDATE] + >> qsuff_tac ‘DRESTRICT f (COMPL {x}) = f’ >- (strip_tac >> gvs[]) + >> simp[EQ_FDOM_SUBMAP, DRESTRICT_DEF, EXTENSION] + >> strip_tac + >> iff_tac + >> rpt strip_tac + >> gvs[] +QED + +Theorem EVERY_OPTION_ALL_MAP_SOME: + ∀ f xs . EVERY f xs ⇒ EVERY (OPTION_ALL f) (MAP SOME xs) +Proof + strip_tac + >> Induct + >> simp[] +QED + +Theorem EVERY_TAKE: + ∀ f n xs . EVERY f xs ⇒ EVERY f (TAKE n xs) +Proof + gen_tac + >> Induct_on ‘xs’ + >> Cases_on ‘n’ + >> simp[] +QED + +Theorem SET_MEM: + ∀ l x . set l x ⇔ MEM x l +Proof + Induct + >> simp[] +QED + +Theorem EVERY_SET: + ∀ l . EVERY (set l) l +Proof + simp[EVERY_MEM, SET_MEM] +QED + +Theorem valid_larger_store: + ∀ (store :'a list) (store' :'a list) . + LENGTH store ≤ LENGTH store' + ⇒ + (∀ v . + valid_val store v + ⇒ + valid_val store' v) ∧ + ∀ ks . + valid_cont store ks + ⇒ + valid_cont store' ks +Proof + rpt gen_tac >> strip_tac + >> ho_match_mp_tac valid_val_ind + >> rpt strip_tac + >> simp[Once valid_val_cases] + >> gvs[can_lookup_cases] + >> gvs[SF ETA_ss] + >> irule FEVERY_MONO + >> pop_assum $ irule_at (Pos last) + >> PairCases + >> rpt strip_tac + >> gvs[] +QED + +Theorem valid_val_larger_store = SRULE [PULL_FORALL, AND_IMP_INTRO] $ + cj 1 valid_larger_store; +Theorem valid_cont_larger_store = SRULE [PULL_FORALL, AND_IMP_INTRO] $ + cj 2 valid_larger_store; + +Theorem letrec_preinit_mono: + ∀ bs store env store' env' . + letrec_preinit store env bs = (store', env') + ⇒ + FDOM env ⊆ FDOM env' +Proof + Induct + >> simp[letrec_preinit_def] + >> rpt strip_tac + >> rpt (pairarg_tac >> gvs[]) + >> last_x_assum drule + >> simp[] +QED + +Theorem letrec_preinit_dom: + ∀ xs store env store' env' . + letrec_preinit store env xs = (store', env') + ⇒ + FDOM env ∪ set xs = FDOM env' ∧ + store ++ GENLIST (λ x. NONE) (LENGTH xs) = store' +Proof + Induct + >> simp[letrec_preinit_def, fresh_loc_def] + >> rpt strip_tac + >> rpt (pairarg_tac >> gvs[]) + >> last_x_assum $ drule_then assume_tac + >> gvs[GENLIST] >- ( + rpt strip_tac + >> qpat_x_assum ‘_ ∪ _ = _’ $ simp o single o GSYM + >> simp[EXTENSION] + >> simp[UNION_DEF, INSERT_DEF, SPECIFICATION, GSYM DISJ_ASSOC] + >> strip_tac + >> iff_tac + >> rw[] >> rw[] + ) + >> rpt $ pop_assum kall_tac + >> ‘∃ n . LENGTH xs = n’ by simp[] + >> simp[] + >> pop_assum kall_tac + >> Induct_on ‘n’ + >> simp[GENLIST] +QED + +Theorem letrec_preinit_lookup: + ∀ xs store env store' env' . + can_lookup env store ∧ + letrec_preinit store env xs = (store', env') + ⇒ + can_lookup env' store' +Proof + Induct + >> simp[letrec_preinit_def, fresh_loc_def] + >> rpt strip_tac + >> rpt (pairarg_tac >> gvs[]) + >> qsuff_tac ‘can_lookup (env |+ (h,LENGTH store)) (SNOC NONE store)’ >- ( + strip_tac + >> last_x_assum drule_all + >> simp[] + ) + >> gvs[can_lookup_cases] + >> qsuff_tac ‘FEVERY (λ(x,n). n < SUC (LENGTH store)) env’ >- ( + strip_tac + >> irule $ cj 2 FEVERY_STRENGTHEN_THM + >> simp[] + ) + >> irule FEVERY_MONO + >> qpat_assum ‘FEVERY _ _’ $ irule_at (Pos last) + >> PairCases + >> simp[] +QED + +Theorem parameterize_NONE_dom: + ∀ xs store env vs store' env' e e' . + LENGTH xs = LENGTH vs ∧ + parameterize store env xs NONE e vs = (store', env', e') + ⇒ + Exp e = e' ∧ + FDOM env ∪ set xs = FDOM env' ∧ + store ++ MAP SOME vs = store' +Proof + Induct + >> simp[parameterize_def] + >> Cases_on ‘vs’ + >> simp[parameterize_def] + >> rpt strip_tac + >> rpt (pairarg_tac >> gvs[]) + >> last_x_assum $ drule_at (Pos $ el 2) + >> rpt strip_tac + >> gvs[] >- ( + pop_assum $ simp o single o GSYM + >> simp[Once INSERT_SING_UNION, EXTENSION] + >> strip_tac + >> iff_tac + >> strip_tac + >> simp[] + ) + >> gvs[fresh_loc_def] +QED + +Theorem parameterize_NONE_lookup: + ∀ xs store env vs store' env' e e' . + LENGTH xs = LENGTH vs ∧ + can_lookup env store ∧ + parameterize store env xs NONE e vs = (store', env', e') + ⇒ + can_lookup env' store' +Proof + Induct + >> simp[parameterize_def] + >> Cases_on ‘vs’ + >> simp[parameterize_def] + >> rpt strip_tac + >> rpt (pairarg_tac >> gvs[]) + >> last_x_assum $ drule_at (Pos $ el 3) + >> rpt strip_tac + >> gvs[] + >> pop_assum irule + >> gvs[can_lookup_cases, fresh_loc_def] + >> irule $ cj 2 FEVERY_STRENGTHEN_THM + >> simp[] + >> irule $ FEVERY_MONO + >> qpat_assum ‘FEVERY _ _’ $ irule_at (Pos last) + >> PairCases + >> simp[] +QED + +Theorem parameterize_NONE_exception: + ∀ xs store env vs store' env' e e' . + LENGTH xs ≠ LENGTH vs ∧ + parameterize store env xs NONE e vs = (store', env', e') + ⇒ + ∃ s . Exception s = e' +Proof + Induct + >> Cases_on ‘vs’ + >> simp[parameterize_def] + >> rpt strip_tac + >> rpt (pairarg_tac >> gvs[]) + >> last_x_assum drule_all + >> simp[] +QED + +Theorem parameterize_SOME_dom: + ∀ xs vs store env x store' env' e e' . + LENGTH xs ≤ LENGTH vs ∧ + parameterize store env xs (SOME x) e vs = (store', env', e') + ⇒ + Exp e = e' ∧ + FDOM env ∪ set (x::xs) = FDOM env' ∧ + store ++ MAP SOME (TAKE (LENGTH xs) vs) + ++ [SOME (SList (REVERSE (TAKE (LENGTH vs - LENGTH xs) (REVERSE vs))))] + = store' +Proof + gen_tac >> gen_tac + >> ‘∃ n . n = LENGTH vs - LENGTH xs’ by simp[] + >> pop_assum mp_tac + >> qid_spec_tac ‘vs’ + >> Induct_on ‘xs’ + >> simp[parameterize_def, fresh_loc_def] >- ( + strip_tac >> strip_tac + >> simp_tac bool_ss [Once $ GSYM LENGTH_REVERSE] + >> simp[TAKE_LENGTH_ID] + >> simp[Once UNION_COMM] + >> simp[Once $ GSYM INSERT_SING_UNION] + ) + >> Cases_on ‘vs’ + >> simp[parameterize_def] + >> rpt strip_tac + >> rpt (pairarg_tac >> gvs[]) + >> last_x_assum $ drule_at (Pos $ el 3) + >> rpt strip_tac + >> gvs[fresh_loc_def] >- ( + pop_assum $ simp o single o GSYM + >> simp[EXTENSION] + >> strip_tac + >> iff_tac + >> strip_tac + >> simp[] + ) + >> simp[TAKE_APPEND1] +QED + +Theorem parameterize_SOME_lookup: + ∀ xs vs store env x store' env' e e' . + LENGTH xs ≤ LENGTH vs ∧ + can_lookup env store ∧ + parameterize store env xs (SOME x) e vs = (store', env', e') + ⇒ + can_lookup env' store' +Proof + gen_tac >> gen_tac + >> ‘∃ n . n = LENGTH vs - LENGTH xs’ by simp[] + >> pop_assum mp_tac + >> qid_spec_tac ‘vs’ + >> Induct_on ‘xs’ + >> simp[parameterize_def, fresh_loc_def] >- ( + simp[can_lookup_cases] + >> rpt strip_tac + >> irule $ cj 2 FEVERY_STRENGTHEN_THM + >> simp[] + >> irule $ FEVERY_MONO + >> qpat_assum ‘FEVERY _ _’ $ irule_at (Pos last) + >> PairCases + >> simp[] + ) + >> Cases_on ‘vs’ + >> simp[parameterize_def] + >> rpt strip_tac + >> rpt (pairarg_tac >> gvs[]) + >> last_x_assum $ drule_at (Pos $ el 4) + >> rpt strip_tac + >> gvs[] + >> pop_assum irule + >> gvs[fresh_loc_def, can_lookup_cases] + >> irule $ cj 2 FEVERY_STRENGTHEN_THM + >> simp[] + >> irule $ FEVERY_MONO + >> qpat_assum ‘FEVERY _ _’ $ irule_at (Pos last) + >> PairCases + >> simp[] +QED + +Theorem parameterize_SOME_exception: + ∀ xs store env x vs store' env' e e' . + LENGTH vs < LENGTH xs ∧ + parameterize store env xs (SOME x) e vs = (store', env', e') + ⇒ + ∃ s . Exception s = e' +Proof + Induct + >> Cases_on ‘vs’ + >> simp[parameterize_def] + >> rpt strip_tac + >> rpt (pairarg_tac >> gvs[]) + >> last_x_assum drule_all + >> simp[] +QED + +Theorem letinit_valid: + ∀ store env xvs ks . + EVERY (OPTION_ALL (valid_val store)) store ∧ + EVERY (FDOM env) (MAP FST xvs) ∧ + EVERY (valid_val store) (MAP SND xvs) ∧ + valid_cont store ks ∧ + can_lookup env store + ⇒ + valid_cont (letinit store env xvs) ks ∧ + can_lookup env (letinit store env xvs) ∧ + EVERY (OPTION_ALL (valid_val (letinit store env xvs))) + (letinit store env xvs) +Proof + Induct_on ‘xvs’ + >> simp[letinit_def] + >> PairCases + >> simp[letinit_def] + >> rpt gen_tac + >> strip_tac + >> last_x_assum irule + >> simp[] + >> irule_at (Pos hd) IMP_EVERY_LUPDATE + >> simp[] + >> irule_at (Pos hd) valid_val_larger_store + >> first_assum $ irule_at (Pos $ el 2) + >> simp[] + >> irule_at (Pos hd) EVERY_MONOTONIC + >> last_assum $ irule_at (Pos $ el 2) + >> strip_tac >- ( + rpt strip_tac + >> irule OPTION_ALL_MONO + >> pop_assum $ irule_at (Pos last) + >> rpt strip_tac + >> irule_at (Pos hd) valid_val_larger_store + >> first_assum $ irule_at (Pos last) + >> simp[] + ) + >> irule_at (Pos hd) EVERY_MONOTONIC + >> last_assum $ irule_at (Pos $ el 2) + >> strip_tac >- ( + rpt strip_tac + >> irule_at (Pos hd) valid_val_larger_store + >> first_assum $ irule_at (Pos last) + >> simp[] + ) + >> gvs[can_lookup_cases] + >> irule valid_cont_larger_store + >> first_assum $ irule_at (Pos last) + >> simp[] +QED + +Theorem sadd_num_or_exception: + ∀ vs n . + (∃ m . sadd vs n = Val (SNum m)) ∨ + (∃ s . sadd vs n = Exception s) +Proof + Induct + >> simp[sadd_def] + >> Cases + >> simp[sadd_def] +QED + +Theorem smul_num_or_exception: + ∀ vs n . + (∃ m . smul vs n = Val (SNum m)) ∨ + (∃ s . smul vs n = Exception s) +Proof + Induct + >> simp[smul_def] + >> Cases + >> simp[smul_def] +QED + +Theorem sminus_num_or_exception: + ∀ vs . + (∃ m . sminus vs = Val (SNum m)) ∨ + (∃ s . sminus vs = Exception s) +Proof + Cases + >> simp[sminus_def] + >> Cases_on ‘h’ + >> simp[sminus_def] + >> qspecl_then [‘t’, ‘0’] assume_tac sadd_num_or_exception + >> EVERY_CASE_TAC + >> gvs[] +QED + +Theorem seqv_bool_or_exception: + ∀ vs . + (∃ b . seqv vs = Val (SBool b)) ∨ + (∃ s . seqv vs = Exception s) +Proof + Cases + >> simp[seqv_def] + >> Cases_on ‘t’ + >> simp[seqv_def] + >> Cases_on ‘t'’ + >> simp[seqv_def] +QED + +Theorem valid_state_progress: + ∀ store ks env state . + valid_state store ks env state + ⇒ + ∃ store' ks' env' state' . + step (store, ks, env, state) = (store', ks', env', state') ∧ + valid_state store' ks' env' state' +Proof + Cases_on ‘state’ + >> rpt strip_tac + >~ [‘Exp e’] >- ( + Cases_on ‘e’ + >~ [‘Lit l’] >- ( + Cases_on ‘l’ + >> simp[step_def, lit_to_val_def] + >> simp[Once valid_state_cases, Once valid_val_cases] + >> gvs[Once valid_state_cases] + ) + >~ [‘Begin es e’] >- ( + Cases_on ‘es’ >- ( + simp[step_def, Once valid_state_cases] + >> gvs[Once valid_state_cases, Once static_scope_def] + ) + >> simp[step_def, Once valid_state_cases] + >> simp[Once valid_val_cases] + >> gvs[Once valid_state_cases, Once static_scope_def] + ) + >~ [‘Ident x’] >- ( + simp[step_def] + >> gvs[Once valid_state_cases, Once static_scope_def, can_lookup_cases] + >> ‘∀ x . FDOM env x ⇒ ∃ a. FLOOKUP env x = SOME a’ + by simp[FLOOKUP_DEF, SPECIFICATION] + >> pop_assum drule >> strip_tac + >> drule_all_then assume_tac FEVERY_FLOOKUP + >> qpat_assum ‘EVERY _ _’ $ assume_tac o SRULE [EVERY_EL] + >> gvs[] + >> pop_assum $ drule_then assume_tac + >> ‘∀ x a . FLOOKUP env x = SOME a ⇒ env ' x = a’ by simp[FLOOKUP_DEF] + >> pop_assum $ drule_then assume_tac + >> simp[] + >> Cases_on ‘EL a store’ >- simp[Once valid_state_cases] + >> gvs[Once valid_state_cases, can_lookup_cases] + ) + >~ [‘Letrec bs e’] >- ( + Cases_on ‘bs’ >- ( + simp[step_def, Once valid_state_cases] + >> gvs[Once valid_state_cases, Once static_scope_def] + ) + >> simp[step_def] + >> PairCases_on ‘h’ + >> rpt (pairarg_tac >> gvs[]) + >> gvs[Once valid_state_cases, Once static_scope_def] + >> simp[Once valid_state_cases] + >> simp[Once valid_val_cases] + >> drule_then assume_tac letrec_preinit_dom + >> drule_all_then assume_tac letrec_preinit_lookup + >> gvs[] + >> irule_at (Pat ‘valid_cont _ _’) valid_cont_larger_store + >> qpat_assum ‘valid_cont _ _’ $ irule_at (Pat ‘valid_cont _ _’) + >> simp[] + >> qpat_x_assum ‘_ = FDOM _’ $ assume_tac o GSYM + >> simp[] + >> irule_at (Pos hd) EVERY_MONOTONIC + >> irule_at (Pos $ el 2) EVERY_SET + >> simp[SET_MEM] + >> simp[EVERY_GENLIST] + >> irule_at (Pos hd) EVERY_MONOTONIC + >> first_assum $ irule_at (Pos $ el 2) + >> rpt strip_tac + >> irule OPTION_ALL_MONO + >> pop_assum $ irule_at (Pos last) + >> rpt strip_tac + >> irule valid_val_larger_store + >> pop_assum $ irule_at (Pos last) + >> simp[] + ) + >~ [‘Letrecstar bs e’] >- ( + simp[step_def] + >> rpt (pairarg_tac >> gvs[]) + >> simp[Once valid_state_cases, Once static_scope_def] + >> gvs[Once valid_state_cases, Once static_scope_def] + >> drule_then assume_tac letrec_preinit_dom + >> drule_all_then assume_tac letrec_preinit_lookup + >> gvs[] + >> irule_at (Pos $ el 2) valid_cont_larger_store + >> qpat_assum ‘valid_cont _ _’ $ irule_at (Pos $ el 2) + >> simp[] + >> irule_at (Pos $ el 2) EVERY_MONOTONIC + >> qpat_assum ‘EVERY (OPTION_ALL _) _’ $ irule_at (Pos $ el 2) + >> strip_tac >- ( + rpt strip_tac + >> irule_at (Pos hd) OPTION_ALL_MONO + >> pop_assum $ irule_at (Pos last) + >> rpt strip_tac + >> irule valid_val_larger_store + >> pop_assum $ irule_at (Pos last) + >> simp[] + ) + >> simp[EVERY_GENLIST] + >> qpat_assum ‘EVERY _ (MAP SND bs)’ mp_tac + >> qpat_assum ‘FDOM _ ∪ _ = FDOM _’ mp_tac + >> rpt (pop_assum kall_tac) + >> qid_spec_tac ‘env’ + >> Induct_on ‘bs’ >- simp[] + >> rpt strip_tac + >> PairCases_on ‘h’ + >> simp[Once static_scope_def] + >> gvs[] + >> last_x_assum $ qspec_then ‘env |+ (h0, 0)’ assume_tac + >> gvs[] + >> qsuff_tac ‘FDOM env ∪ (h0 INSERT set (MAP FST bs)) + = (h0 INSERT FDOM env) ∪ set (MAP FST bs)’ >- ( + strip_tac + >> pop_assum $ gvs o single + >> last_x_assum $ simp o single o GSYM + ) + >> rpt $ pop_assum kall_tac + >> simp[EXTENSION, UNION_DEF] + >> strip_tac + >> iff_tac + >> strip_tac + >> simp[] + ) + >> simp[step_def, Once valid_state_cases] + >> simp[Once valid_val_cases] + >> gvs[Once valid_state_cases, Once static_scope_def, can_lookup_cases] + >> Cases_on ‘o'’ + >> gvs[Once valid_state_cases, Once static_scope_def, can_lookup_cases] + ) + >~ [‘Val v’] >- ( + Cases_on ‘ks’ >- ( + simp[step_def, return_def, Once valid_state_cases, + can_lookup_cases, FEVERY_FEMPTY] + >> gvs[Once valid_state_cases] + ) + >> PairCases_on ‘h’ + >> Cases_on ‘h1’ + >~ [‘CondK t f’] >- ( + simp[step_def, return_def] + >> IF_CASES_TAC >- ( + gvs[Once valid_state_cases, Once valid_val_cases] + >> gvs[Once valid_val_cases] + >> simp[Once valid_state_cases] + ) + >> gvs[Once valid_state_cases] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> rpt strip_tac + >> simp[Once valid_state_cases] + ) + >~ [‘BeginK es e’] >- ( + simp[step_def, return_def] + >> CASE_TAC + >> gvs[Once valid_state_cases] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> rpt strip_tac + >> simp[Once valid_state_cases] + >> simp[Once valid_val_cases] + ) + >~ [‘SetK x’] >- ( + simp[step_def, return_def] + >> gvs[Once valid_state_cases] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> rpt strip_tac + >> simp[Once valid_state_cases] + >> simp[Once valid_val_cases] + >> irule_at (Pos hd) valid_cont_larger_store + >> qpat_assum ‘valid_cont _ _’ $ irule_at (Pos $ el 2) + >> simp[] + >> gvs[can_lookup_cases] + >> irule IMP_EVERY_LUPDATE + >> simp[OPTION_ALL_def] + >> irule_at (Pos hd) valid_val_larger_store + >> last_assum $ irule_at (Pos $ el 2) + >> simp[] + >> irule EVERY_MONOTONIC + >> qpat_assum ‘EVERY _ _’ $ irule_at (Pos last) + >> rpt strip_tac + >> irule OPTION_ALL_MONO + >> pop_assum $ irule_at (Pos last) + >> rpt strip_tac + >> irule_at (Pos hd) valid_val_larger_store + >> pop_assum $ irule_at (Pos last) + >> simp[] + ) + >~ [‘LetinitK xvs x bs e’] >- ( + simp[step_def, return_def] + >> CASE_TAC + >> gvs[Once valid_state_cases] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> rpt strip_tac >- ( + simp[Once valid_state_cases] + >> irule letinit_valid + >> simp[] + ) + >> PairCases_on ‘h’ + >> gvs[] + >> simp[Once valid_state_cases] + >> simp[Once valid_val_cases] + ) + >~ [‘ApplyK fnp es’] >- ( + simp[step_def] + >> Cases_on ‘∃ e es' . es = e::es'’ >-( + gvs[] + >> Cases_on ‘∃ fn vs . fnp = SOME (fn,vs)’ + >> Cases_on ‘fnp = NONE’ + >> gvs[] + >> simp[return_def] + >> simp[Once valid_state_cases] + >> gvs[Once valid_state_cases] + >> simp[Once valid_val_cases] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> rpt strip_tac + >> simp[] + >> Cases_on ‘fnp’ >> gvs[] >> PairCases_on ‘x’ >> gvs[] + ) + >> Cases_on ‘es’ >> gvs[] + >> Cases_on ‘fnp’ >- ( + simp[return_def] + >> Cases_on ‘v’ + >> simp[application_def] + >~ [‘Prim p’] >- ( + CASE_TAC + >> simp[Once valid_state_cases, sadd_def, smul_def, + sminus_def, seqv_def, can_lookup_cases, FEVERY_FEMPTY] + >> simp[Once valid_val_cases] + >> gvs[Once valid_state_cases] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> simp[] + ) + >~ [‘Proc env' xs xp e’] >- ( + Cases_on ‘xp’ + >> Cases_on ‘xs’ + >> simp[parameterize_def] >- ( + simp[Once valid_state_cases] + >> gvs[Once valid_state_cases] + >> gvs[Once valid_val_cases] + >> gvs[Once valid_val_cases] + ) + >- simp[Once valid_state_cases] + >- ( + rpt (pairarg_tac >> gvs[]) + >> simp[Once valid_state_cases] + >> gvs[Once valid_state_cases, fresh_loc_def] + >> gvs[Once valid_val_cases] + >> gvs[Once valid_val_cases] + >> simp[Once INSERT_SING_UNION, Once UNION_COMM] + >> irule_at (Pos hd) valid_cont_larger_store + >> qpat_assum ‘valid_cont _ _’ $ irule_at (Pos $ el 2) + >> simp[Once valid_val_cases] + >> irule_at (Pos $ el 2) $ EVERY_MONOTONIC + >> pop_assum $ irule_at (Pos $ el 2) + >> gvs[can_lookup_cases] + >> irule_at (Pos $ el 2) $ cj 2 FEVERY_STRENGTHEN_THM + >> simp[] + >> irule_at (Pos hd) FEVERY_MONO + >> qpat_assum ‘FEVERY _ env'’ $ irule_at (Pos $ el 2) + >> rpt strip_tac >- (PairCases_on ‘x'’ >> gvs[]) + >> irule OPTION_ALL_MONO + >> pop_assum $ irule_at (Pos last) + >> rpt strip_tac + >> irule valid_val_larger_store + >> pop_assum $ irule_at (Pos last) + >> simp[] + ) + >> simp[Once valid_state_cases] + >> gvs[Once valid_state_cases] + >> gvs[Once valid_val_cases] + >> gvs[Once valid_val_cases] + ) + >> simp[Once valid_state_cases] + >> gvs[Once valid_state_cases] + >> gvs[Once valid_val_cases] + >> gvs[Once valid_val_cases] + ) + >> PairCases_on ‘x’ + >> simp[return_def] + >> Cases_on ‘x0’ + >> simp[application_def] + >~ [‘Prim p’] >- ( + TOP_CASE_TAC >- ( + qspecl_then [‘REVERSE x1 ++ [v]’, ‘0’] assume_tac sadd_num_or_exception + >> simp[Once valid_state_cases] + >> gvs[] + >> simp[Once valid_val_cases, can_lookup_cases, FEVERY_FEMPTY] + >> gvs[Once valid_state_cases] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> simp[] + ) + >- ( + qspecl_then [‘REVERSE x1 ++ [v]’, ‘1’] assume_tac smul_num_or_exception + >> simp[Once valid_state_cases] + >> gvs[] + >> simp[Once valid_val_cases, can_lookup_cases, FEVERY_FEMPTY] + >> gvs[Once valid_state_cases] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> simp[] + ) + >- ( + qspec_then ‘REVERSE x1 ++ [v]’ assume_tac sminus_num_or_exception + >> simp[Once valid_state_cases] + >> gvs[] + >> simp[Once valid_val_cases, can_lookup_cases, FEVERY_FEMPTY] + >> gvs[Once valid_state_cases] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> simp[] + ) + >- ( + qspec_then ‘REVERSE x1 ++ [v]’ assume_tac seqv_bool_or_exception + >> simp[Once valid_state_cases] + >> gvs[] + >> simp[Once valid_val_cases, can_lookup_cases, FEVERY_FEMPTY] + >> gvs[Once valid_state_cases] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> simp[] + ) + >> CASE_TAC + >> gvs[] + >> Cases_on ‘t'’ >- ( + gvs[] + >> simp[Once valid_state_cases] + >> gvs[Once valid_state_cases] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> rpt strip_tac + >> simp[Once valid_val_cases, can_lookup_cases, FEVERY_FEMPTY] + ) + >> gvs[] + >> simp[Once valid_state_cases] + >> gvs[Once valid_state_cases] + >> gvs[Once valid_val_cases] + >> gvs[Once valid_val_cases] + ) + >~ [‘Proc env' xs xp e’] >- ( + rpt (pairarg_tac >> gvs[]) + >> gvs[Once valid_state_cases] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> rpt strip_tac + >> qpat_x_assum ‘valid_val _ (Proc _ _ _ _)’ $ mp_tac o SRULE [Once valid_val_cases] + >> rpt strip_tac + >> gvs[] >- ( + Cases_on ‘LENGTH xs = LENGTH (REVERSE x1 ++ [v])’ >- ( + drule_all_then mp_tac parameterize_NONE_dom + >> drule_all_then mp_tac parameterize_NONE_lookup + >> rpt strip_tac + >> qpat_x_assum ‘Exp _ = _’ $ simp o single o GSYM + >> simp[Once valid_state_cases] + >> qpat_x_assum ‘_ ∪ _ = _’ $ simp o single o GSYM + >> qpat_x_assum ‘_ ++ _ = _’ $ simp o single o GSYM + >> irule_at (Pos hd) $ valid_cont_larger_store + >> qpat_assum ‘valid_cont _ _’ $ irule_at (Pos $ el 2) + >> simp[] + >> irule_at (Pos hd) EVERY_MONOTONIC + >> qpat_assum ‘EVERY _ store’ $ irule_at (Pos $ el 2) + >> strip_tac >- ( + rpt strip_tac + >> irule OPTION_ALL_MONO + >> pop_assum $ irule_at (Pos last) + >> rpt strip_tac + >> irule valid_val_larger_store + >> pop_assum $ irule_at (Pos last) + >> simp[] + ) + >> strip_tac >- ( + irule EVERY_OPTION_ALL_MAP_SOME + >> irule EVERY_MONOTONIC + >> qexists ‘valid_val store’ + >> simp[] + >> rpt strip_tac + >> irule valid_val_larger_store + >> pop_assum $ irule_at (Pos last) + >> simp[] + ) + >> irule valid_val_larger_store + >> last_assum $ irule_at (Pos last) + >> simp[] + ) + >> drule_all_then mp_tac parameterize_NONE_exception + >> rpt strip_tac + >> simp[Once valid_state_cases] + >> gvs[] + ) + >> Cases_on ‘LENGTH xs ≤ LENGTH (REVERSE x1 ++ [v])’ >- ( + drule_all_then mp_tac parameterize_SOME_dom + >> drule_all_then mp_tac parameterize_SOME_lookup + >> rpt strip_tac + >> simp[Once valid_state_cases] + >> gvs[] + >> irule_at (Pos hd) $ valid_cont_larger_store + >> qpat_assum ‘valid_cont _ _’ $ irule_at (Pos $ el 2) + >> simp[] + >> irule_at (Pos hd) EVERY_MONOTONIC + >> qpat_assum ‘EVERY _ store’ $ irule_at (Pos $ el 2) + >> strip_tac >- ( + rpt strip_tac + >> irule OPTION_ALL_MONO + >> pop_assum $ irule_at (Pos last) + >> rpt strip_tac + >> irule valid_val_larger_store + >> pop_assum $ irule_at (Pos last) + >> simp[] + ) + >> strip_tac >- ( + irule EVERY_OPTION_ALL_MAP_SOME + >> irule EVERY_TAKE + >> simp[] + >> strip_tac >- ( + irule EVERY_MONOTONIC + >> qpat_assum ‘EVERY _ x1’ $ irule_at (Pos last) + >> rpt strip_tac + >> irule valid_val_larger_store + >> pop_assum $ irule_at (Pos last) + >> simp[] + ) + >> irule valid_val_larger_store + >> last_assum $ irule_at (Pos last) + >> simp[] + ) + >> simp[Once valid_val_cases] + >> irule EVERY_TAKE + >> simp[] + >> strip_tac >- ( + irule valid_val_larger_store + >> last_assum $ irule_at (Pos last) + >> simp[] + ) + >> irule EVERY_MONOTONIC + >> qpat_assum ‘EVERY _ x1’ $ irule_at (Pos last) + >> rpt strip_tac + >> irule valid_val_larger_store + >> pop_assum $ irule_at (Pos last) + >> simp[] + ) + >> ‘LENGTH (REVERSE x1 ++ [v]) < LENGTH xs’ by gvs[] + >> drule_all_then mp_tac parameterize_SOME_exception + >> rpt strip_tac + >> simp[Once valid_state_cases] + >> gvs[] + ) + >~ [‘Throw ks’] >- ( + CASE_TAC >- simp[Once valid_state_cases] + >> CASE_TAC >- ( + gvs[] + >> simp[Once valid_state_cases, can_lookup_cases, FEVERY_FEMPTY] + >> gvs[Once valid_state_cases] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> rpt strip_tac + >> qpat_x_assum ‘valid_val _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> simp[] + ) + >> simp[Once valid_state_cases] + ) + >> simp[Once valid_state_cases] + >> gvs[Once valid_state_cases] + >> gvs[Once valid_val_cases] + >> gvs[Once valid_val_cases] + ) + ) + >> simp[step_def, Once valid_state_cases] +QED + +Theorem terminating_direction: + ∀ store ks env e store' ks' env' e' . + step (store, ks, env, e) = (store', ks', env', e') ∧ + ¬ terminating_state (store', ks', env', e') + ⇒ + ¬ terminating_state (store, ks, env, e) +Proof + simp[terminating_state_def] + >> rpt strip_tac + >> gvs[step_def, return_def] +QED + +Theorem terminating_direction_n: + ∀ n store ks env e store' ks' env' e' . + FUNPOW step n (store, ks, env, e) = (store', ks', env', e') ∧ + ¬ terminating_state (store', ks', env', e') + ⇒ + ¬ terminating_state (store, ks, env, e) +Proof + Induct + >> simp[FUNPOW_SUC] + >> rpt gen_tac + >> strip_tac + >> last_x_assum irule + >> Cases_on ‘FUNPOW step n (store,ks,env,e)’ + >> PairCases_on ‘r’ + >> drule_all_then assume_tac terminating_direction + >> simp[] +QED + +Theorem scheme_divergence: + ∀ store ks env state store' ks' env' state' . + step (store, ks, env, state) = (store', ks', env', state') ∧ + ¬ terminating_state (store, ks, env, state) + ⇒ + (store, ks, env, state) ≠ (store', ks', env', state') +Proof + Cases_on ‘state’ + >> simp[terminating_state_def] + >~ [‘Exp e’] >- ( + Cases_on ‘e’ + >> simp[step_def] >- ( + rpt strip_tac + >> Cases_on ‘EL (env ' m) store’ + >> gvs[] + ) + >- ( + CASE_TAC + >> simp[] + >> rpt strip_tac + >> ‘∀ e e' . e = e' ⇒ exp_size e = exp_size e'’ by simp[] + >> pop_assum drule + >> simp[exp_size_def] + ) + >- ( + CASE_TAC + >> simp[] + >> rpt strip_tac + >- ( + ‘∀ e e' . e = e' ⇒ exp_size e = exp_size e'’ by simp[] + >> pop_assum drule + >> simp[exp_size_def] + ) + >> rpt (pairarg_tac >> gvs[]) + >> PairCases_on ‘h’ + >> gvs[] + ) + >> rpt strip_tac + >> rpt (pairarg_tac >> gvs[]) + ) + >> Cases_on ‘ks’ + >> simp[step_def] + >> PairCases_on ‘h’ + >> simp[oneline return_def, oneline application_def, AllCaseEqs()] + >> rpt strip_tac + >> rpt (pairarg_tac >> gvs[]) + >> qpat_x_assum ‘_ = Throw _’ mp_tac + >> rpt $ pop_assum kall_tac + >> strip_tac + >> ‘∀ v v' . v = v' ⇒ val_size v = val_size v'’ by simp[] + >> pop_assum drule + >> simp[cont_size_def] +QED + +Theorem statically_scoped_program_valid: + ∀ p . static_scope ∅ p ⇒ valid_state [] [] FEMPTY (Exp p) +Proof + simp[Once valid_state_cases, + can_lookup_cases, FEVERY_FEMPTY] + >> simp[Once valid_val_cases] +QED + +val _ = export_theory(); \ No newline at end of file diff --git a/compiler/scheme/proofs/scheme_to_cakeProofScript.sml b/compiler/scheme/proofs/scheme_to_cakeProofScript.sml new file mode 100644 index 0000000000..bce9f900df --- /dev/null +++ b/compiler/scheme/proofs/scheme_to_cakeProofScript.sml @@ -0,0 +1,2367 @@ +(* + Proof of semantic preservation from Scheme to CakeML +*) +open preamble; +open computeLib; +open scheme_astTheory; +open scheme_semanticsTheory; +open scheme_to_cakeTheory; +open scheme_semanticsPropsTheory; + +open astTheory; +open evaluateTheory; +open evaluatePropsTheory; +open semanticPrimitivesTheory; +open namespaceTheory; +open primTypesTheory; +open namespacePropsTheory; +open integerTheory; + +val _ = new_theory "scheme_to_cakeProof"; + +val _ = (max_print_depth := 30); + +Theorem scheme_env1_def[allow_rebind, compute] = EVAL_RULE $ zDefine ‘ + scheme_env1 = case evaluate_decs + (<|clock:=999;next_type_stamp:=0;next_exn_stamp:=0|> :num state) + <|v:=nsEmpty;c:=nsEmpty|> + (prim_types_program ++ [Dtype unknown_loc [(["'a"],"option", + [("None",[]); ("Some",[Atvar "'a"])])]] ++ [scheme_basis1]) of + | (st', Rval env) => env + | _ => <|v:=nsEmpty;c:=nsEmpty|> +’; + +Definition cconses_def[simp]: + cconses = ["SNum"; "SBool"; "True"; "False"; + "Prim";"SAdd";"SMul";"SMinus";"SEqv";"CallCC"; + "[]"; "::"; "Some"; "None"; "Ex"; "Proc"; "Throw";"SList";"Wrong"] +End + +Theorem scheme_env1_rw[simp] = SRULE [nsLookup_def] $ SIMP_CONV pure_ss [ + SimpRHS, scheme_env1_def, + EVERY_DEF, cconses_def, MAP +] “ + EVERY (λ x . nsLookup scheme_env1.c x = nsLookup scheme_env1.c x) $ + MAP Short cconses +”; + +Theorem scheme_env2_def[allow_rebind, compute] = SRULE [] $ + RESTR_EVAL_RULE [“scheme_env1”] $ zDefine ‘ + scheme_env2 = case evaluate_decs + (<|clock:=999;next_type_stamp:=0;next_exn_stamp:=0|> :num state) + scheme_env1 + [scheme_basis2] of + | (st', Rval env) => <|c:=scheme_env1.c;v:=nsAppend env.v scheme_env1.v|> + | _ => <|v:=nsEmpty;c:=nsEmpty|> +’; + +Theorem scheme_env2_rw[simp] = SRULE [GSYM CONJ_ASSOC] $ +CONJ (SRULE [Once scheme_env2_def] $ SCONV [] “ + EVERY (λ x . nsLookup scheme_env2.c x = nsLookup scheme_env1.c x) $ + MAP Short cconses +”) $ SRULE [GSYM scheme_env1_def] $ EVAL “nsLookup scheme_env2.v (Short "sadd")”; + +Theorem scheme_env3_def[allow_rebind, compute] = SRULE [] $ + RESTR_EVAL_RULE [“scheme_env2”] $ zDefine ‘ + scheme_env3 = case evaluate_decs + (<|clock:=999;next_type_stamp:=0;next_exn_stamp:=0|> :num state) + scheme_env2 + [scheme_basis3] of + | (st', Rval env) => <|c:=scheme_env2.c;v:=nsAppend env.v scheme_env2.v|> + | _ => <|v:=nsEmpty;c:=nsEmpty|> +’; + +Theorem scheme_env3_rw[simp] = SRULE [GSYM CONJ_ASSOC] $ +CONJ (SRULE [Once scheme_env3_def] $ SCONV [] “ + EVERY (λ x . nsLookup scheme_env3.c x = nsLookup scheme_env1.c x) $ + MAP Short cconses +”) $ LIST_CONJ $ map + (SRULE [ + GSYM $ EVAL “scheme_env1”, + GSYM $ EVAL “scheme_env2” + ] o EVAL) [ + “nsLookup scheme_env3.v (Short "sadd")”, + “nsLookup scheme_env3.v (Short "smul")” +]; + +Theorem scheme_env4_def[allow_rebind, compute] = SRULE [] $ + RESTR_EVAL_RULE [“scheme_env3”] $ zDefine ‘ + scheme_env4 = case evaluate_decs + (<|clock:=999;next_type_stamp:=0;next_exn_stamp:=0|> :num state) + scheme_env3 + [scheme_basis4] of + | (st', Rval env) => <|c:=scheme_env3.c;v:=nsAppend env.v scheme_env3.v|> + | _ => <|v:=nsEmpty;c:=nsEmpty|> +’; + +Theorem scheme_env4_rw[simp] = SRULE [GSYM CONJ_ASSOC] $ +CONJ (SRULE [Once scheme_env4_def] $ SCONV [] “ + EVERY (λ x . nsLookup scheme_env4.c x = nsLookup scheme_env1.c x) $ + MAP Short cconses +”) $ LIST_CONJ $ map + (SRULE [ + GSYM $ EVAL “scheme_env1”, + GSYM $ EVAL “scheme_env2”, + GSYM $ EVAL “scheme_env3” + ] o EVAL) [ + “nsLookup scheme_env4.v (Short "sadd")”, + “nsLookup scheme_env4.v (Short "smul")”, + “nsLookup scheme_env4.v (Short "sminus")” +]; + +Theorem scheme_env5_def[allow_rebind, compute] = SRULE [] $ + RESTR_EVAL_RULE [“scheme_env4”] $ zDefine ‘ + scheme_env5 = case evaluate_decs + (<|clock:=999;next_type_stamp:=0;next_exn_stamp:=0|> :num state) + scheme_env4 + [scheme_basis5] of + | (st', Rval env) => <|c:=scheme_env4.c;v:=nsAppend env.v scheme_env4.v|> + | _ => <|v:=nsEmpty;c:=nsEmpty|> +’; + +Theorem scheme_env5_rw[simp] = SRULE [GSYM CONJ_ASSOC] $ +CONJ (SRULE [Once scheme_env5_def] $ SCONV [] “ + EVERY (λ x . nsLookup scheme_env5.c x = nsLookup scheme_env1.c x) $ + MAP Short cconses +”) $ LIST_CONJ $ map + (SRULE [ + GSYM $ EVAL “scheme_env1”, + GSYM $ EVAL “scheme_env2”, + GSYM $ EVAL “scheme_env3”, + GSYM $ EVAL “scheme_env4” + ] o EVAL) [ + “nsLookup scheme_env5.v (Short "sadd")”, + “nsLookup scheme_env5.v (Short "smul")”, + “nsLookup scheme_env5.v (Short "sminus")”, + “nsLookup scheme_env5.v (Short "seqv")” +]; + +Theorem scheme_env6_def[allow_rebind, compute] = SRULE [] $ + RESTR_EVAL_RULE [“scheme_env5”] $ zDefine ‘ + scheme_env6 = case evaluate_decs + (<|clock:=999;next_type_stamp:=0;next_exn_stamp:=0|> :num state) + scheme_env5 + [scheme_basis6] of + | (st', Rval env) => <|c:=scheme_env5.c;v:=nsAppend env.v scheme_env5.v|> + | _ => <|v:=nsEmpty;c:=nsEmpty|> +’; + +Theorem scheme_env6_rw[simp] = SRULE [GSYM CONJ_ASSOC] $ +CONJ (SRULE [Once scheme_env6_def] $ SCONV [] “ + EVERY (λ x . nsLookup scheme_env6.c x = nsLookup scheme_env1.c x) $ + MAP Short cconses +”) $ LIST_CONJ $ map + (SRULE [ + GSYM $ EVAL “scheme_env1”, + GSYM $ EVAL “scheme_env2”, + GSYM $ EVAL “scheme_env3”, + GSYM $ EVAL “scheme_env4”, + GSYM $ EVAL “scheme_env5” + ] o EVAL) [ + “nsLookup scheme_env6.v (Short "sadd")”, + “nsLookup scheme_env6.v (Short "smul")”, + “nsLookup scheme_env6.v (Short "sminus")”, + “nsLookup scheme_env6.v (Short "seqv")”, + “nsLookup scheme_env6.v (Short "throw")” +]; + +Theorem scheme_env7_def[allow_rebind, compute] = SRULE [] $ + RESTR_EVAL_RULE [“scheme_env6”] $ zDefine ‘ + scheme_env7 = case evaluate_decs + (<|clock:=999;next_type_stamp:=0;next_exn_stamp:=0|> :num state) + scheme_env6 + [scheme_basis7] of + | (st', Rval env) => <|c:=scheme_env6.c;v:=nsAppend env.v scheme_env6.v|> + | _ => <|v:=nsEmpty;c:=nsEmpty|> +’; + +Theorem scheme_env7_rw[simp] = SRULE [GSYM CONJ_ASSOC] $ +CONJ (SRULE [Once scheme_env7_def] $ SCONV [] “ + EVERY (λ x . nsLookup scheme_env7.c x = nsLookup scheme_env1.c x) $ + MAP Short cconses +”) $ LIST_CONJ $ map + (SRULE [ + GSYM $ EVAL “scheme_env1”, + GSYM $ EVAL “scheme_env2”, + GSYM $ EVAL “scheme_env3”, + GSYM $ EVAL “scheme_env4”, + GSYM $ EVAL “scheme_env5”, + GSYM $ EVAL “scheme_env6” + ] o EVAL) [ + “nsLookup scheme_env7.v (Short "sadd")”, + “nsLookup scheme_env7.v (Short "smul")”, + “nsLookup scheme_env7.v (Short "sminus")”, + “nsLookup scheme_env7.v (Short "seqv")”, + “nsLookup scheme_env7.v (Short "throw")”, + “nsLookup scheme_env7.v (Short "callcc")”, + “nsLookup scheme_env7.v (Short "app")” +]; + +Theorem scheme_env'_def[allow_rebind, compute] = EVAL_RULE $ zDefine ‘ + scheme_env' = case evaluate_decs (<|clock:=999;next_type_stamp:=0;next_exn_stamp:=0|> :num state) <|v:=nsEmpty;c:=nsEmpty|> (prim_types_program ++ [Dtype unknown_loc [(["'a"],"option", + [("None",[]); ("Some",[Atvar "'a"])])]] ++ scheme_basis) of + | (st', Rval env) => env + | _ => <|v:=nsEmpty;c:=nsEmpty|> +’; + +Definition vconses_def[simp]: + vconses = ["sadd"; "smul"; "sminus"; "seqv"; "throw"; "callcc"; "app"] +End + +Theorem scheme_env_def[allow_rebind, compute] = SRULE [GSYM CONJ_ASSOC] $ zDefine ‘ + scheme_env env + ⇔ + EVERY (λ x . nsLookup env.c x = nsLookup scheme_env7.c x) $ + MAP Short cconses ∧ + EVERY (λ x . nsLookup env.v x = nsLookup scheme_env7.v x) $ + MAP Short vconses +’ + +Theorem basis_scheme_env: + scheme_env scheme_env' +Proof + EVAL_TAC +QED + +(* +Example lambda calculus code of conditional expression, +before and after step in CEK machine + +(\k0 -> (\k1 -> k1 $ SBool T) + (\t0 -> match t0 + | SBool F => (\k2 -> k2 (SNum 1)) k0 + | _ => (\k2 -> k2 (SNum 2)) k0)) +(\t -> t) + +--> + +(\k1 -> k1 $ SBool T) +(\t0 -> match t0 + | SBool F => (\k2 -> k2 (SNum 1)) (\t -> t) + | _ => (\k2 -> k2 (SNum 2)) (\t -> t))) +*) + +Definition scheme_typestamp_def: + scheme_typestamp con = SND $ THE $ nsLookup scheme_env1.c (Short con) +End + +Theorem scheme_typestamp_def[allow_rebind, simp] = SRULE [] $ + SIMP_CONV pure_ss [SimpRHS, scheme_typestamp_def, EVERY_DEF, cconses_def] + “EVERY (λ x . scheme_typestamp x = scheme_typestamp x) cconses”; + +Inductive env_rel: + FEVERY (λ (x, n). + nsLookup env.v (Short ("var" ++ explode x)) = SOME (Loc T n)) se + ⇒ + env_rel se env +End + +Theorem vcons_list_def[allow_rebind] = SRULE [] $ Define ‘ + vcons_list [] = Conv (SOME (scheme_typestamp "[]")) [] ∧ + vcons_list (v::vs) = Conv (SOME (scheme_typestamp "::")) [v; vcons_list vs] +’; + +Definition cps_app_ts_def: + cps_app_ts (v::vs) = (let + (t, ts) = cps_app_ts vs + in + ("t" ++ toString (SUC (LENGTH ts)), t::ts)) ∧ + + cps_app_ts [] = ("t0", []) +End + +Inductive val_cont_rels: +[~SBool_T:] + ml_v_vals' (SBool T) $ + Conv (SOME (scheme_typestamp "SBool")) [Conv (SOME (scheme_typestamp "True")) []] +[~SBool_F:] + ml_v_vals' (SBool F) $ + Conv (SOME (scheme_typestamp "SBool")) [Conv (SOME (scheme_typestamp "False")) []] +[~SNum:] + ml_v_vals' (SNum i) $ + Conv (SOME (scheme_typestamp "SNum")) [Litv (IntLit i)] +[~Prim_SAdd:] + ml_v_vals' (Prim SAdd) $ + Conv (SOME (scheme_typestamp "Prim")) [Conv (SOME (scheme_typestamp "SAdd")) []] +[~Prim_SMul:] + ml_v_vals' (Prim SMul) $ + Conv (SOME (scheme_typestamp "Prim")) [Conv (SOME (scheme_typestamp "SMul")) []] +[~Prim_SMinus:] + ml_v_vals' (Prim SMinus) $ + Conv (SOME (scheme_typestamp "Prim")) [Conv (SOME (scheme_typestamp "SMinus")) []] +[~Prim_SEqv:] + ml_v_vals' (Prim SEqv) $ + Conv (SOME (scheme_typestamp "Prim")) [Conv (SOME (scheme_typestamp "SEqv")) []] +[~Prim_CallCC:] + ml_v_vals' (Prim CallCC) $ + Conv (SOME (scheme_typestamp "Prim")) [Conv (SOME (scheme_typestamp "CallCC")) []] +[~Prim_Wrong:] + ml_v_vals' (Wrong s) $ + Conv (SOME (scheme_typestamp "Wrong")) [Litv (StrLit s)] +[~Proc:] + scheme_env env ∧ + env_rel se env ∧ + ce = cps_transform e ∧ + inner = proc_ml xs xp "k" ce + ⇒ + ml_v_vals' (Proc se xs xp e) $ + Conv (SOME (scheme_typestamp "Proc")) [ + Closure env "k" $ Fun "ts" inner + ] +[~Throw:] + cont_rel ks kv + ⇒ + ml_v_vals' (Throw ks) $ + Conv (SOME (scheme_typestamp "Throw")) [kv] +[~SList:] + LIST_REL ml_v_vals' vs mlvs + ⇒ + ml_v_vals' (SList vs) $ + Conv (SOME (scheme_typestamp "SList")) [vcons_list mlvs] + +[~Id:] + scheme_env env + ⇒ + cont_rel [] + (Closure env "t" (Var (Short "t"))) +[~CondK:] + cont_rel ks kv ∧ + nsLookup env.v (Short "k") = SOME kv ∧ + ct = cps_transform te ∧ + cf = cps_transform fe ∧ + scheme_env env ∧ + env_rel se env + ⇒ + cont_rel ((se, CondK te fe) :: ks) + (Closure env "t" $ Mat (Var (Short "t")) [ + (Pcon (SOME $ Short "SBool") [Pcon (SOME $ Short "False") []], + App Opapp [cf; Var (Short "k")]); + (Pany, App Opapp [ct; Var (Short "k")]) + ]) +[~ApplyK_NONE:] + cont_rel ks kv ∧ + nsLookup env.v (Short "k") = SOME kv ∧ + inner = cps_transform_app (Var (Short "t")) [] es (Var (Short "k")) ∧ + scheme_env env ∧ + env_rel se env + ⇒ + cont_rel ((se, ApplyK NONE es) :: ks) + (Closure env "t" $ inner) +[~ApplyK_SOME:] + cont_rel ks kv ∧ + nsLookup env.v (Short "k") = SOME kv ∧ + (t, ts) = cps_app_ts vs ∧ + inner = cps_transform_app (Var (Short "t")) + (Var (Short t) :: MAP (Var o Short) ts) es (Var (Short "k")) ∧ + ml_v_vals' fn mlfn ∧ + nsLookup env.v (Short "t") = SOME mlfn ∧ + LIST_REL ml_v_vals' vs mlvs ∧ + LIST_REL (λ x mlv . nsLookup env.v (Short x) = SOME mlv) ts mlvs ∧ + scheme_env env ∧ + env_rel se env + ⇒ + cont_rel ((se, ApplyK (SOME (fn, vs)) es) :: ks) + (Closure env t $ inner) +[~BeginK:] + cont_rel ks kv ∧ + nsLookup env.v (Short "k") = SOME kv ∧ + inner = cps_transform_seq (Var (Short "k")) es e ∧ + scheme_env env ∧ + env_rel se env + ⇒ + cont_rel ((se, BeginK es e) :: ks) + (Closure env "_" $ inner) +[~SetK:] + cont_rel ks kv ∧ + nsLookup env.v (Short "k") = SOME kv ∧ + inner = refunc_set (Var (Short "t")) (Var (Short "k")) x ∧ + scheme_env env ∧ + env_rel se env + ⇒ + cont_rel ((se, SetK x) :: ks) + (Closure env "t" $ inner) +[~LetinitK:] + cont_rel ks kv ∧ + nsLookup env.v (Short "k") = SOME kv ∧ + (t, ts) = cps_app_ts xvs ∧ + inner = cps_transform_letinit + ((x,Var (Short t))::ZIP (MAP FST xvs, MAP (Var o Short) ts)) + bs e (Var (Short "k")) ∧ + LIST_REL ml_v_vals' (MAP SND xvs) mlvs ∧ + LIST_REL (λ x mlv . nsLookup env.v (Short x) = SOME mlv) ts mlvs ∧ + scheme_env env ∧ + env_rel se env + ⇒ + cont_rel ((se, LetinitK xvs x bs e) :: ks) + (Closure env t $ inner) +End + +Theorem val_cont_rels_ind[allow_rebind] = SRULE [] $ val_cont_rels_ind; +Theorem ml_v_vals'_cases = SRULE [] $ cj 1 val_cont_rels_cases; +Theorem cont_rel_cases = cj 2 val_cont_rels_cases; + +val (store_entry_rel_rules,store_entry_rel_ind,store_entry_rel_cases) = +(fn (x,y,z) => (SRULE [] x,SRULE [] y, SRULE [] z)) $ Hol_reln ‘ + (ml_v_vals' v mlv + ⇒ + store_entry_rel (SOME v) (Refv (Conv (SOME (scheme_typestamp "Some")) [mlv]))) ∧ + store_entry_rel NONE (Refv (Conv (SOME (scheme_typestamp "None")) [])) +’; + +Inductive e_ce_rel: +[~Val:] + ml_v_vals' v mlv ∧ + nsLookup env.v (Short valv) = SOME (mlv) ∧ + nsLookup env.v (Short var) = SOME kv ∧ + valv ≠ var + ⇒ + e_ce_rel (Val v) var env kv $ App Opapp [Var (Short var); Var (Short valv)] +[~Exp:] + ce = cps_transform e ∧ + nsLookup env.v (Short var) = SOME kv ∧ + scheme_env env + ⇒ + e_ce_rel (Exp e) var env kv $ App Opapp [ce; Var (Short var)] +[~Exception:] + e_ce_rel (Exception s) var env kv $ + Con (SOME $ Short "Ex") [Lit $ StrLit $ explode s] +End + +Theorem compile_in_rel: + ∀ p st env . + scheme_env env + ⇒ + ∃ st' env' var mle k kv . + e_ce_rel (Exp p) var env' kv mle ∧ + cont_rel k kv ∧ + evaluate st env [compile_scheme_prog p] = evaluate st' env' [mle] +Proof + simp[Once e_ce_rel_cases, compile_scheme_prog_def] + >> rpt strip_tac + >> rpt (pairarg_tac >> gvs[]) + >> simp[Ntimes evaluate_def 2, nsOptBind_def] + >> irule_at (Pos last) EQ_REFL + >> simp[] + >> simp[Once cont_rel_cases] + >> gvs[scheme_env_def] + >> metis_tac[] +QED + +(* +open scheme_to_cakeProofTheory; +open scheme_parsingTheory; +*) + +Theorem cps_app_ts_res: + ∀ t ts vs . + (t, ts) = cps_app_ts vs + ⇒ + t = "t" ++ toString (LENGTH ts) ∧ + (∀ n:num . n ≥ LENGTH ts ⇒ ¬ MEM ("t" ++ toString n) ts) ∧ + LENGTH vs = LENGTH ts +Proof + Induct_on ‘vs’ + >> simp[cps_app_ts_def] + >> rpt (pairarg_tac >> gvs[]) +QED + +Theorem str_not_num: + ∀ (n:num) str . ¬ EVERY isDigit str ⇒ toString n ≠ str +Proof + simp[EVERY_isDigit_num_to_dec_string] +QED + +Theorem cps_app_ts_distinct: + ∀ t ts vs . + (t, ts) = cps_app_ts vs + ⇒ + ¬ MEM t ts ∧ + ALL_DISTINCT ts ∧ + t ≠ "t" ∧ + t ≠ "k" ∧ + ¬ MEM "t" ts ∧ + ¬ MEM "k" ts ∧ + ¬ MEM t vconses ∧ + EVERY (λ t. ¬ MEM t vconses) ts ∧ + (∀ x . t ≠ "var" ++ x) ∧ + EVERY (λ t. ∀ x . t ≠ "var" ++ x) ts +Proof + Induct_on ‘vs’ + >> simp[cps_app_ts_def] + >> rpt (pairarg_tac >> gvs[]) + >> drule_then mp_tac $ GSYM cps_app_ts_res + >> strip_tac + >> qpat_x_assum ‘_ = t’ $ assume_tac o GSYM + >> simp[] + >> qpat_assum ‘∀ _ . _ ⇒ _’ $ irule_at (Pos hd) o SRULE [] + >> irule_at (Pos last) str_not_num + >> simp[isDigit_def] +QED + +Theorem cons_list_val: + ∀ st env ts vs . + scheme_env env ∧ + LIST_REL (λ x v . nsLookup env.v (Short x) = SOME v) ts vs + ⇒ + evaluate (st:'ffi state) env [cons_list (MAP (Var o Short) ts)] + = (st, Rval [vcons_list vs]) +Proof + rpt strip_tac + >> pop_assum mp_tac + >> qid_spec_tac ‘vs’ + >> qid_spec_tac ‘ts’ + >> ho_match_mp_tac LIST_REL_ind + >> simp[evaluate_def, cons_list_def, vcons_list_def, + do_con_check_def, build_conv_def] + >> gvs[scheme_env_def] +QED + +Theorem map_reverse[simp]: + ∀ xs f . MAP f (REVERSE xs) = REVERSE (MAP f xs) +Proof + Induct >> simp[] +QED + +Theorem LIST_REL_SNOC_ind: + ∀R LIST_REL'. + LIST_REL' [] [] ∧ + (∀h1 h2 t1 t2. + R h1 h2 ∧ LIST_REL' t1 t2 ⇒ LIST_REL' (SNOC h1 t1) (SNOC h2 t2)) ⇒ + ∀a0 a1. LIST_REL R a0 a1 ⇒ LIST_REL' a0 a1 +Proof + strip_tac >> strip_tac >> strip_tac + >> Induct_on ‘a0’ using SNOC_INDUCT + >> Induct_on ‘a1’ using SNOC_INDUCT + >- simp[] + >- simp[EVERY2_LENGTH] + >- simp[EVERY2_LENGTH] + >> pop_assum kall_tac + >> simp[LIST_REL_SNOC] +QED + +Definition eval_eq_def: + eval_eq st mlenv mle st' mlenv' mle' ck = ∀ start. + evaluate (st with clock := ck + start) mlenv [mle] + = + evaluate (st' with clock := start) mlenv' [mle'] +End + +Theorem eval_eq_trivial: + ∀ st mlenv mle . + eval_eq st mlenv mle st mlenv mle 0 +Proof + simp[eval_eq_def] +QED + +Theorem eval_eq_trans: + ∀ st mlenv mle st' mlenv' mle' st'' mlenv'' mle'' ck ck' . + eval_eq st mlenv mle st' mlenv' mle' ck ∧ + eval_eq st' mlenv' mle' st'' mlenv'' mle'' ck' + ⇒ + eval_eq st mlenv mle st'' mlenv'' mle'' (ck + ck') +Proof + simp[eval_eq_def] +QED + +Theorem preservation_of_sadd_body: + ∀ vs mlvs . + LIST_REL ml_v_vals' vs mlvs + ⇒ + ∀ store st env n k kv . + cont_rel k kv ∧ + LIST_REL store_entry_rel store st.refs ∧ + nsLookup env.v (Short "ts") = SOME (vcons_list mlvs) ∧ + nsLookup env.v (Short "n") = SOME (Litv (IntLit n)) ∧ + nsLookup env.v (Short "k") = SOME kv ∧ + nsLookup env.v (Short "sadd") = nsLookup scheme_env2.v (Short "sadd") ∧ + env.c = scheme_env1.c + ⇒ + ∃ck st' mlenv' var' kv' mle'. + (∀ start . evaluate (st with clock := ck + start) env + [Mat (Var (Short "ts")) + [(Pcon (SOME (Short "[]")) [], + Let (SOME "t") (Con (SOME (Short "SNum")) [Var (Short "n")]) + (App Opapp [Var (Short "k"); Var (Short "t")])); + (Pcon (SOME (Short "::")) [Pvar "t"; Pvar "ts'"], + Mat (Var (Short "t")) + [(Pcon (SOME (Short "SNum")) [Pvar "tn"], + App Opapp + [App Opapp + [App Opapp [Var (Short "sadd"); Var (Short "k")]; + App (Opn Plus) [Var (Short "n"); Var (Short "tn")]]; + Var (Short "ts'")]); + (Pany, + Con (SOME (Short "Ex")) + [Lit (StrLit "Arith-op applied to non-number")])])]] = + evaluate (st' with clock := start) mlenv' [mle']) ∧ + cont_rel k kv' ∧ + e_ce_rel (sadd vs n) var' mlenv' kv' mle' ∧ + env_rel FEMPTY mlenv' ∧ + LIST_REL store_entry_rel store st'.refs ∧ + st.ffi = st'.ffi +Proof + ho_match_mp_tac LIST_REL_ind + >> simp[vcons_list_def, sadd_def] + >> rpt strip_tac >- ( + simp[Ntimes evaluate_def 2] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes evaluate_def 3, do_con_check_def, build_conv_def, + nsOptBind_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> last_assum $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases, sadd_def, Once ml_v_vals'_cases, + env_rel_cases, FEVERY_FEMPTY] + ) + >> gvs[Once ml_v_vals'_cases] + >> gvs[vcons_list_def] + >~ [‘SNum m’] >- ( + simp[sadd_def] + >> simp[evaluate_def, do_opapp_def, do_app_def, + opn_lookup_def, can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def, do_con_check_def, build_conv_def, dec_clock_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> qrefine ‘ck+3’ + >> simp[Ntimes evaluate_def 2] + >> ‘st.ffi = (st with <|refs := st.refs; ffi := st.ffi|>).ffi’ by simp[] + >> first_assum $ once_asm_rewrite_tac o single + >> pop_assum $ simp_tac pure_ss o single o Once o GSYM + >> last_x_assum irule + >> simp[] + >> simp[Once INT_ADD_COMM] + ) + >> simp[Ntimes evaluate_def 10, do_opapp_def, do_app_def, + opn_lookup_def, can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def, do_con_check_def, build_conv_def, dec_clock_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> simp[sadd_def, Once e_ce_rel_cases] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[env_rel_cases, FEVERY_FEMPTY] +QED + +Theorem preservation_of_smul_body: + ∀ vs mlvs . + LIST_REL ml_v_vals' vs mlvs + ⇒ + ∀ store st env n k kv . + cont_rel k kv ∧ + LIST_REL store_entry_rel store st.refs ∧ + nsLookup env.v (Short "ts") = SOME (vcons_list mlvs) ∧ + nsLookup env.v (Short "n") = SOME (Litv (IntLit n)) ∧ + nsLookup env.v (Short "k") = SOME kv ∧ + nsLookup env.v (Short "smul") = nsLookup scheme_env3.v (Short "smul") ∧ + env.c = scheme_env1.c + ⇒ + ∃ck st' mlenv' var' kv' mle'. + (∀ start . evaluate (st with clock := ck + start) env + [Mat (Var (Short "ts")) + [(Pcon (SOME (Short "[]")) [], + Let (SOME "t") (Con (SOME (Short "SNum")) [Var (Short "n")]) + (App Opapp [Var (Short "k"); Var (Short "t")])); + (Pcon (SOME (Short "::")) [Pvar "t"; Pvar "ts'"], + Mat (Var (Short "t")) + [(Pcon (SOME (Short "SNum")) [Pvar "tn"], + App Opapp + [App Opapp + [App Opapp [Var (Short "smul"); Var (Short "k")]; + App (Opn Times) [Var (Short "n"); Var (Short "tn")]]; + Var (Short "ts'")]); + (Pany, + Con (SOME (Short "Ex")) + [Lit (StrLit "Arith-op applied to non-number")])])]] = + evaluate (st' with clock := start) mlenv' [mle']) ∧ + cont_rel k kv' ∧ + e_ce_rel (smul vs n) var' mlenv' kv' mle' ∧ + env_rel FEMPTY mlenv' ∧ + LIST_REL store_entry_rel store st'.refs ∧ + st.ffi = st'.ffi +Proof + ho_match_mp_tac LIST_REL_ind + >> simp[vcons_list_def, smul_def] + >> rpt strip_tac >- ( + simp[Ntimes evaluate_def 2] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes evaluate_def 3, do_con_check_def, build_conv_def, + nsOptBind_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> last_assum $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases, smul_def, Once ml_v_vals'_cases, + env_rel_cases, FEVERY_FEMPTY] + ) + >> gvs[Once ml_v_vals'_cases] + >> gvs[vcons_list_def] + >~ [‘SNum m’] >- ( + simp[smul_def] + >> simp[evaluate_def, do_opapp_def, do_app_def, + opn_lookup_def, can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def, do_con_check_def, build_conv_def, dec_clock_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> qrefine ‘ck+3’ + >> simp[Ntimes evaluate_def 2] + >> ‘st.ffi = (st with <|refs := st.refs; ffi := st.ffi|>).ffi’ by simp[] + >> first_assum $ once_asm_rewrite_tac o single + >> pop_assum $ simp_tac pure_ss o single o Once o GSYM + >> last_x_assum irule + >> simp[] + >> simp[scheme_env2_def, Once INT_MUL_COMM] + ) + >> simp[Ntimes evaluate_def 10, do_opapp_def, do_app_def, + opn_lookup_def, can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def, do_con_check_def, build_conv_def, dec_clock_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> simp[smul_def, Once e_ce_rel_cases] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[env_rel_cases, FEVERY_FEMPTY] +QED + +Theorem preservation_of_sminus_body: + ∀ vs mlvs . + LIST_REL ml_v_vals' vs mlvs + ⇒ + ∀ store (st:'ffi state) env n k kv . + cont_rel k kv ∧ + LIST_REL store_entry_rel store st.refs ∧ + nsLookup env.v (Short "ts") = SOME (vcons_list mlvs) ∧ + nsLookup env.v (Short "k") = SOME kv ∧ + nsLookup env.v (Short "sadd") = nsLookup scheme_env3.v (Short "sadd") ∧ + env.c = scheme_env1.c + ⇒ + ∃ck st' mlenv' var' kv' mle'. + (∀ start . evaluate (st with clock := ck + start) env + [Mat (Var (Short "ts")) + [(Pcon (SOME (Short "[]")) [], + Con (SOME (Short "Ex")) [Lit (StrLit "Arity mismatch")]); + (Pcon (SOME (Short "::")) [Pvar "t"; Pvar "ts'"], + Mat (Var (Short "t")) + [(Pcon (SOME (Short "SNum")) [Pvar "n"], + Mat (Var (Short "ts'")) [ + (Pcon (SOME $ Short "[]") [], + Let (SOME "t") (Con (SOME $ Short "SNum") [ + App (Opn Minus) [Lit $ IntLit 0; Var (Short "n")]]) $ + App Opapp [Var (Short "k"); Var (Short "t")]); + (Pany, App Opapp [App Opapp [App Opapp [Var (Short "sadd"); + Fun "t" $ Mat (Var (Short "t")) [ + (Pcon (SOME $ Short "SNum") [Pvar "m"], + Let (SOME "t") (Con (SOME $ Short "SNum") [ + App (Opn Minus) [Var (Short "n"); Var (Short "m")]]) $ + App Opapp [Var (Short "k"); Var (Short "t")]); + (Pany, + App Opapp [Var (Short "k"); Var (Short "t")]) + ]]; + Lit $ IntLit 0]; Var (Short "ts'")])]); + (Pany, + Con (SOME (Short "Ex")) + [Lit (StrLit "Arith-op applied to non-number")])])]] = + evaluate (st' with clock := start) mlenv' [mle']) ∧ + cont_rel k kv' ∧ + e_ce_rel (sminus vs) var' mlenv' kv' mle' ∧ + env_rel FEMPTY mlenv' ∧ + LIST_REL store_entry_rel store st'.refs ∧ + st.ffi = st'.ffi +Proof + Cases_on ‘vs’ >- ( + simp[vcons_list_def] + >> rpt strip_tac + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> last_assum $ irule_at (Pos hd) + >> simp[sminus_def] + >> simp[Once e_ce_rel_cases, env_rel_cases, FEVERY_FEMPTY] + ) + >> Cases_on ‘mlvs’ + >> simp[vcons_list_def] + >> strip_tac + >> gvs[Once ml_v_vals'_cases] + >~ [‘SNum i’] >- ( + simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> rpt strip_tac + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> Cases_on ‘t=[]’ >- ( + gvs[vcons_list_def] + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes evaluate_def 6, do_app_def, do_con_check_def, + build_conv_def, nsOptBind_def, opn_lookup_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[sminus_def, Once e_ce_rel_cases, Once ml_v_vals'_cases, + env_rel_cases, FEVERY_FEMPTY] + ) + >> qrefine ‘ck+3’ + >> ‘∃ t' ts' . t'::ts'=t’ by (Cases_on ‘t’ >> gvs[]) + >> simp[sminus_def] + >> first_assum $ simp_tac bool_ss o single o GSYM + >> simp[Ntimes evaluate_def 3] + >> ‘∃ y ys . y::ys = t'’ by gvs[] + >> pop_assum $ simp_tac bool_ss o single o (fn x => Ntimes x 2) o GSYM + >> simp[vcons_list_def] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> pop_assum kall_tac + >> pop_assum kall_tac + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes evaluate_def 7, do_opapp_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> simp[Ntimes evaluate_def 2, dec_clock_def] + >> simp[sminus_def] + >> ‘∃ n . 0i = n’ by simp[] + >> pop_assum mp_tac >> strip_tac + >> pop_assum $ simp o single + >> ‘∃ kenv . (env with + v := + nsBind "n" (Litv (IntLit i)) + (nsBind "ts'" (vcons_list t') + (nsBind "t" + (Conv (SOME (TypeStamp "SNum" 4)) + [Litv (IntLit i)]) env.v))) + = kenv’ by simp[] + >> pop_assum mp_tac >> strip_tac + >> ‘nsLookup kenv.v (Short "n") = SOME (Litv (IntLit i))’ by gvs[] + >> ‘nsLookup kenv.v (Short "k") = SOME kv’ by gvs[] + >> ‘kenv.c = scheme_env1.c’ by gvs[] + >> qpat_x_assum ‘_ = kenv’ $ simp o single + >> rpt $ qpat_x_assum ‘nsLookup env.v _ = _’ kall_tac + >> rpt $ pop_assum mp_tac + >> strip_tac + >> qid_spec_tac ‘i''’ + >> qid_spec_tac ‘n’ + >> qid_spec_tac ‘st’ + >> pop_assum mp_tac + >> qid_spec_tac ‘t'’ + >> qid_spec_tac ‘t’ + >> ho_match_mp_tac LIST_REL_ind + >> rpt strip_tac >- ( + simp[vcons_list_def, sadd_def] + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes evaluate_def 7, do_opapp_def, do_con_check_def, + build_conv_def, nsOptBind_def] + >> qrefine ‘ck+1’ + >> simp[Ntimes evaluate_def 3, dec_clock_def] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes evaluate_def 6, do_app_def, do_con_check_def, + build_conv_def, nsOptBind_def, opn_lookup_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[env_rel_cases, FEVERY_FEMPTY] + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases, Once ml_v_vals'_cases] + ) + >> gvs[Once ml_v_vals'_cases] + >~ [‘SNum m’] >- ( + simp[sadd_def, vcons_list_def] + >> simp[evaluate_def, do_opapp_def, do_app_def, + opn_lookup_def, can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def, do_con_check_def, build_conv_def, dec_clock_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> qrefine ‘ck+3’ + >> simp[Ntimes evaluate_def 2] + >> simp[Once INT_ADD_COMM] + >> ‘st.ffi = (st with <|refs := st.refs; ffi := st.ffi|>).ffi’ by simp[] + >> first_assum $ once_asm_rewrite_tac o single + >> pop_assum $ simp_tac pure_ss o single o Once o GSYM + >> last_x_assum irule + >> simp[] + ) + >> simp[sadd_def, vcons_list_def] + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[env_rel_cases, FEVERY_FEMPTY] + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases] + ) + >> simp[sminus_def] + >> rpt strip_tac + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[env_rel_cases, FEVERY_FEMPTY] + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases] +QED + +Theorem preservation_of_proc: +∀ (st:'ffi state) inner n n' m m' env env' mlenv var kv n xs xp e e' ce k args vs mlvs store store' . + valid_val store (Proc env xs xp e) ∧ + LIST_REL ml_v_vals' vs mlvs ∧ + EVERY (valid_val store) vs ∧ + valid_cont store k ∧ + cont_rel k kv ∧ + ce = cps_transform e ∧ + inner = proc_ml xs xp "k" ce ∧ + (store', env',e') = parameterize store env xs xp e vs ∧ + EVERY (OPTION_ALL (valid_val store)) store ∧ + nsLookup mlenv.v (Short "k") = SOME kv ∧ + nsLookup mlenv.v (Short "ts") = SOME (vcons_list mlvs) ∧ + env_rel env mlenv ∧ + scheme_env mlenv ∧ + can_lookup env store ∧ + LIST_REL store_entry_rel store st.refs + ⇒ + ∃ck st' mlenv' var' kv' mle'. + (∀ start . evaluate (st with clock := ck + start) mlenv [inner] + = evaluate (st' with clock := start) mlenv' [mle']) ∧ + cont_rel k kv' ∧ + e_ce_rel e' var' mlenv' kv' mle' ∧ + env_rel env' mlenv' ∧ + LIST_REL store_entry_rel store' st'.refs ∧ + st.ffi = st'.ffi +Proof + Induct_on ‘xs’ + >> rpt strip_tac + >- ( + qpat_assum ‘cont_rel _ _’ $ irule_at (Pat ‘cont_rel _ _’) + >> Cases_on ‘xp’ + >> gvs[proc_ml_def] >- ( + Cases_on ‘vs’ + >> gvs[parameterize_def] >- ( + simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, evaluate_match_def, vcons_list_def, + pmatch_def] + >> qpat_assum ‘scheme_env mlenv’ $ simp o single + o SRULE [scheme_env_def] + >> simp[same_type_def, same_ctor_def, pat_bindings_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases] + ) + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, evaluate_match_def, vcons_list_def, + pmatch_def] + >> qpat_assum ‘scheme_env mlenv’ $ simp o single + o SRULE [scheme_env_def] + >> simp[same_type_def, same_ctor_def, pat_bindings_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases] + >> simp[env_rel_cases, FEVERY_FEMPTY] + ) + >> gvs[parameterize_def] + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, evaluate_match_def, vcons_list_def, + pmatch_def, do_con_check_def, build_conv_def] + >> qpat_assum ‘scheme_env mlenv’ $ simp o single + o SRULE [scheme_env_def] + >> simp[same_type_def, same_ctor_def, pat_bindings_def] + >> simp[Ntimes evaluate_def 2, do_app_def, store_alloc_def] + >> simp[can_pmatch_all_def, evaluate_match_def, vcons_list_def, + pmatch_def, do_con_check_def, build_conv_def, nsOptBind_def] + >> qpat_assum ‘scheme_env mlenv’ $ simp o single + o SRULE [scheme_env_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[] + >> rpt (pairarg_tac >> gvs[]) + >> gvs[fresh_loc_def, store_entry_rel_cases, SNOC_APPEND] + >> simp[Once ml_v_vals'_cases] + >> simp[Once e_ce_rel_cases] + >> irule_at Any EQ_REFL + >> simp[] + >> gvs[scheme_env_def, env_rel_cases] + >> Cases_on ‘x ∈ FDOM env’ >- ( + simp[FEVERY_DEF] + >> strip_tac + >> Cases_on ‘x = x'’ + >> gvs[] >- ( + drule $ cj 1 $ iffLR EVERY2_EVERY + >> simp[] + ) + >> strip_tac + >> gvs[FEVERY_DEF] + >> simp[FAPPLY_FUPDATE_THM] + ) + >> irule $ cj 2 FEVERY_STRENGTHEN_THM + >> simp[] + >> drule_then assume_tac $ cj 1 $ iffLR EVERY2_EVERY + >> simp[FEVERY_DEF] + >> rpt strip_tac + >> ‘x ≠ x'’ by (strip_tac >> gvs[]) + >> gvs[FEVERY_DEF] + ) + >> gvs[proc_ml_def] + >> rpt (pairarg_tac >> gvs[]) + >> Cases_on ‘vs’ + >> gvs[parameterize_def] >- ( + qpat_assum ‘cont_rel _ _’ $ irule_at (Pat ‘cont_rel _ _’) + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, evaluate_match_def, vcons_list_def, + pmatch_def] + >> qpat_assum ‘scheme_env mlenv’ $ simp o single + o SRULE [scheme_env_def] + >> simp[same_type_def, same_ctor_def, pat_bindings_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases] + >> simp[env_rel_cases, FEVERY_FEMPTY] + ) + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, evaluate_match_def, vcons_list_def, + pmatch_def] + >> qpat_assum ‘scheme_env mlenv’ $ simp o single + o SRULE [scheme_env_def] + >> simp[same_type_def, same_ctor_def, pat_bindings_def] + >> simp[Ntimes evaluate_def 4, do_app_def, store_alloc_def] + >> simp[can_pmatch_all_def, evaluate_match_def, vcons_list_def, + pmatch_def, do_con_check_def, build_conv_def, nsOptBind_def] + >> qpat_assum ‘scheme_env mlenv’ $ simp o single + o SRULE [scheme_env_def] + >> simp[same_type_def, same_ctor_def, pat_bindings_def] + >> ‘st.ffi = (st with <|refs := + st.refs ++ [Refv (Conv (SOME (TypeStamp "Some" 2)) [y])]; + ffi := st.ffi|>).ffi’ by simp[] + >> first_assum $ once_asm_rewrite_tac o single + >> pop_assum $ simp_tac pure_ss o single o Once o GSYM + >> last_x_assum irule + >> simp[] + >> rpt (pairarg_tac >> gvs[]) + >> rpt $ irule_at Any EQ_REFL + >> simp[] + >> qpat_assum ‘scheme_env mlenv’ $ simp + o curry ((::) o swap) [scheme_env_def] + o SRULE [scheme_env_def] + >> gvs[fresh_loc_def] + >> simp[SNOC_APPEND, store_entry_rel_cases] + >> irule_at (Pos hd) EVERY_MONOTONIC + >> qpat_assum ‘EVERY _ store’ $ irule_at (Pos $ el 2) + >> strip_tac >- ( + rpt strip_tac + >> irule OPTION_ALL_MONO + >> pop_assum $ irule_at (Pos last) + >> rpt strip_tac + >> irule valid_val_larger_store + >> pop_assum $ irule_at (Pos last) + >> simp[] + ) + >> irule_at (Pos hd) valid_val_larger_store + >> qpat_assum ‘valid_store _ h'’ $ irule_at (Pos $ el 2) + >> simp[] + >> irule_at (Pos hd) EVERY_MONOTONIC + >> qpat_assum ‘EVERY _ t’ $ irule_at (Pos $ el 2) + >> strip_tac >- ( + rpt strip_tac + >> irule valid_val_larger_store + >> pop_assum $ irule_at (Pos last) + >> simp[] + ) + >> irule_at (Pos $ el 3) valid_cont_larger_store + >> qpat_assum ‘valid_cont _ k'’ $ irule_at (Pos $ el 2) + >> simp[Once valid_val_cases] + >> conj_asm1_tac >- ( + gvs[can_lookup_cases] + >> irule $ cj 2 FEVERY_STRENGTHEN_THM + >> irule_at (Pos last) FEVERY_MONO + >> qpat_assum ‘FEVERY _ env’ $ irule_at (Pos $ el 2) + >> simp[] + >> PairCases + >> simp[] + ) + >> simp[] + >> gvs[env_rel_cases] + >> strip_tac >- ( + Cases_on ‘h ∈ FDOM env’ >- ( + simp[FEVERY_DEF] + >> strip_tac + >> Cases_on ‘x = h’ + >> gvs[] >- ( + drule $ cj 1 $ iffLR EVERY2_EVERY + >> simp[] + ) + >> strip_tac + >> gvs[FEVERY_DEF] + >> simp[FAPPLY_FUPDATE_THM] + ) + >> irule $ cj 2 FEVERY_STRENGTHEN_THM + >> simp[] + >> drule_then assume_tac $ cj 1 $ iffLR EVERY2_EVERY + >> simp[FEVERY_DEF] + >> rpt strip_tac + >> ‘x ≠ h’ by (strip_tac >> gvs[]) + >> gvs[FEVERY_DEF] + ) + >> Cases_on ‘xp’ + >> simp[] + >> irule static_scope_mono + >> gvs[Once valid_val_cases] + >> qpat_assum ‘static_scope _ _’ $ irule_at (Pos last) + >> simp[Ntimes INSERT_SING_UNION 2] + >> simp[SUBSET_DEF] +QED + +Theorem preservation_of_letrec: + ∀ xs inner (st:'ffi state) mlenv store env store' env' . + (store', env') = letrec_preinit store env xs ∧ + env_rel env mlenv ∧ + LIST_REL store_entry_rel store st.refs ∧ + scheme_env mlenv + ⇒ + ∃ ck st' mlenv' var' . + (∀ start . evaluate (st with clock:=ck+start) mlenv [letpreinit_ml xs inner] + = evaluate (st' with clock:=start) mlenv' [inner]) ∧ + env_rel env' mlenv' ∧ + LIST_REL store_entry_rel store' st'.refs ∧ + (∀ x v . (∀ x' . x ≠ "var" ++ x') ∧ nsLookup mlenv.v (Short x) = SOME v + ⇒ + nsLookup mlenv'.v (Short x) = SOME v) ∧ + scheme_env mlenv' ∧ + st.ffi = st'.ffi +Proof + Induct + >> simp[letrec_preinit_def, letpreinit_ml_def] + >> rpt strip_tac >- ( + simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[] + ) + >> rpt (pairarg_tac >> gvs[]) + >> simp[Ntimes evaluate_def 3, do_con_check_def, build_conv_def, + do_app_def, store_alloc_def, nsOptBind_def] + >> qpat_assum ‘scheme_env _’ $ simp o single + o SRULE [scheme_env_def] + >> qsuff_tac ‘∀ mlenv' . + (∀x v. + (∀x'. x ≠ STRING #"v" (STRING #"a" (STRING #"r" x'))) ∧ + nsLookup (mlenv with + v := + nsBind (STRING #"v" (STRING #"a" (STRING #"r" (explode h)))) + (Loc T (LENGTH st.refs)) mlenv.v).v (Short x) = SOME v ⇒ + nsLookup mlenv'.v (Short x) = SOME v) + ⇔ + (∀x v. + (∀x'. x ≠ STRING #"v" (STRING #"a" (STRING #"r" x'))) ∧ + nsLookup mlenv.v (Short x) = SOME v ⇒ + nsLookup mlenv'.v (Short x) = SOME v) + ’ >- ( + strip_tac + >> pop_assum $ simp_tac pure_ss o single o GSYM + >> ‘st.ffi = (st with <|refs := + st.refs ++ [Refv (Conv (SOME (TypeStamp "None" 2)) [])]; + ffi := st.ffi|>).ffi’ by simp[] + >> first_assum $ once_asm_rewrite_tac o single + >> pop_assum $ simp_tac pure_ss o single o Once o GSYM + >> last_x_assum $ irule + >> simp[] + >> strip_tac >- gvs[scheme_env_def] + >> irule_at (Pos hd) EQ_REFL + >> gvs[env_rel_cases, fresh_loc_def, store_entry_rel_cases,SNOC_APPEND] + >> Cases_on ‘h ∈ FDOM env’ >- ( + simp[FEVERY_DEF] + >> strip_tac + >> Cases_on ‘x = h’ + >> gvs[] >- ( + drule $ cj 1 $ iffLR EVERY2_EVERY + >> simp[] + ) + >> strip_tac + >> gvs[FEVERY_DEF] + >> simp[FAPPLY_FUPDATE_THM] + ) + >> irule $ cj 2 FEVERY_STRENGTHEN_THM + >> simp[] + >> drule_then assume_tac $ cj 1 $ iffLR EVERY2_EVERY + >> simp[FEVERY_DEF] + >> rpt strip_tac + >> ‘x ≠ h’ by (strip_tac >> gvs[]) + >> gvs[FEVERY_DEF] + ) + >> strip_tac + >> iff_tac + >> rpt strip_tac + >> qpat_assum ‘∀ _ _ . _ ∧ _ ⇒ _’ irule + >> simp[] + >> qpat_assum ‘∀ _ . _ ≠ _’ $ qspec_then ‘explode h’ assume_tac + >> simp[] + >> Cases_on ‘mlenv’ + >> gvs[] +QED + +Theorem preservation_of_letinit: + ∀ (st:'ffi state) mlenv mlvs store env e k kv var xvs ts . + EVERY (FDOM env) (MAP FST xvs) ∧ + EVERY (valid_val store) (MAP SND xvs) ∧ + LIST_REL ml_v_vals' (MAP SND xvs) mlvs ∧ + LIST_REL (λx mlv. nsLookup mlenv.v (Short x) = SOME mlv) ts mlvs ∧ + cont_rel k kv ∧ nsLookup mlenv.v (Short var) = SOME kv ∧ + scheme_env mlenv ∧ + env_rel env mlenv ∧ + can_lookup env store ∧ + LIST_REL store_entry_rel store st.refs + ⇒ + ∃ck st' mlenv' var' kv' mle'. + (∀start. + evaluate (st with clock := ck + start) mlenv + [letinit_ml + (ZIP (MAP FST xvs,MAP (Var ∘ Short) ts)) + (App Opapp [cps_transform e; Var (Short var)])] = + evaluate (st' with clock := start) mlenv' [mle']) ∧ + cont_rel k kv' ∧ e_ce_rel (Exp e) var' mlenv' kv' mle' ∧ + env_rel env mlenv' ∧ + LIST_REL store_entry_rel (letinit store env xvs) st'.refs ∧ + st.ffi = st'.ffi +Proof + Induct_on ‘xvs’ + >> rpt strip_tac + >> gvs[letinit_ml_def, letinit_def] >- ( + simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases] + ) + >> PairCases_on ‘h’ + >> simp[letinit_def] + >> gvs[] + >> simp[Ntimes evaluate_def 6, do_con_check_def, build_conv_def, + nsOptBind_def] + >> qpat_assum ‘scheme_env _’ $ simp o single + o SRULE [scheme_env_def] + >> qpat_assum ‘env_rel env _’ $ drule_then assume_tac + o SRULE [env_rel_cases, FEVERY_DEF, SPECIFICATION] + >> simp[do_app_def, store_assign_def, store_v_same_type_def] + >> qpat_assum ‘can_lookup env _’ $ drule_then assume_tac + o SRULE [can_lookup_cases, FEVERY_DEF, SPECIFICATION] + >> drule_then assume_tac EVERY2_LENGTH + >> drule_all_then assume_tac $ cj 2 $ iffLR LIST_REL_EL_EQN + >> gvs[store_entry_rel_cases] + >> (‘st.ffi = (st with <|refs := LUPDATE (Refv (Conv (SOME (TypeStamp "Some" 2)) [y])) + (env ' h0) st.refs; ffi := st.ffi|>).ffi’ by simp[] + >> first_assum $ once_asm_rewrite_tac o single + >> pop_assum $ simp_tac pure_ss o single o Once o GSYM + >> last_x_assum $ irule + >> first_assum $ irule_at (Pos last) + >> simp[] + >> irule_at (Pos hd) EVERY_MONOTONIC + >> last_assum $ irule_at (Pos $ el 2) + >> strip_tac >- ( + rpt strip_tac + >> irule valid_val_larger_store + >> pop_assum $ irule_at (Pos last) + >> simp[LENGTH_LUPDATE] + ) + >> gvs[can_lookup_cases] + >> irule EVERY2_LUPDATE_same + >> simp[store_entry_rel_cases]) +QED + +Theorem step_preservation: + ∀ store store' env env' e e' k k' (st : 'ffi state) mlenv var kv mle . + step (store, k, env, e) = (store', k', env', e') ∧ + valid_state store k env e ∧ + cont_rel k kv ∧ + e_ce_rel e var mlenv kv mle ∧ + env_rel env mlenv ∧ + LIST_REL store_entry_rel store st.refs + ⇒ + ∃ ck st' mlenv' var' kv' mle' . + (∀ start . evaluate (st with clock := start + ck) mlenv [mle] + = + evaluate (st' with clock := start) mlenv' [mle']) ∧ + cont_rel k' kv' ∧ + e_ce_rel e' var' mlenv' kv' mle' ∧ + env_rel env' mlenv' ∧ + LIST_REL store_entry_rel store' st'.refs ∧ + (¬ terminating_state (store', k', env', e') ⇒ 0 < ck) ∧ + st.ffi = st'.ffi +Proof + Cases_on ‘e’ + >> simp[terminating_state_def] + >~ [‘Exception s’] >- ( + simp[step_def, Once e_ce_rel_cases] + >> rpt strip_tac + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases, Once cont_rel_cases] + >> qexists ‘scheme_env7’ + >> simp[scheme_env_def] + ) + >~ [‘Exp e’] >- ( + Cases_on ‘e’ + >> simp[step_def, Once e_ce_rel_cases] + >~ [‘Lit l’] >- ( + simp[cps_transform_def] + >> rpt strip_tac + >> Cases_on ‘l’ + >> simp[lit_to_val_def, to_ml_vals_def] + >> TRY CASE_TAC (*for Prim cases*) + >> TRY (Cases_on ‘b’) (*for Bool cases*) + >> gvs[lit_to_val_def, to_ml_vals_def] + >> qrefine ‘ck+1’ + >> simp[SimpLHS, Ntimes evaluate_def 7, do_opapp_def, + do_con_check_def, build_conv_def, nsOptBind_def, dec_clock_def] + >> qpat_assum ‘scheme_env mlenv’ $ simp o single + o SRULE [scheme_env_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases, Once ml_v_vals'_cases] + >> gvs[env_rel_cases] + ) + >~ [‘Cond c te fe’] >- ( + simp[cps_transform_def] + >> rpt strip_tac + >> qrefine ‘ck+1’ + >> simp[SimpLHS, Ntimes evaluate_def 6, do_opapp_def, + nsOptBind_def, dec_clock_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases, Once cont_rel_cases] + >> gvs[scheme_env_def, env_rel_cases] + ) + >~ [‘Apply fn es’] >- ( + simp[cps_transform_def] + >> rpt strip_tac + >> qrefine ‘ck+1’ + >> simp[SimpLHS, Ntimes evaluate_def 6, do_opapp_def, + nsOptBind_def, dec_clock_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases, Once cont_rel_cases] + >> gvs[scheme_env_def, env_rel_cases] + ) + >~ [‘Begin es e’] >- ( + Cases_on ‘es’ + >> rpt strip_tac + >> gvs[cps_transform_def] >- ( + qrefine ‘ck+1’ + >> simp[SimpLHS, Ntimes evaluate_def 4, do_opapp_def, + nsOptBind_def, dec_clock_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases] + >> gvs[scheme_env_def, env_rel_cases] + ) + >> qrefine ‘ck+1’ + >> simp[SimpLHS, Ntimes evaluate_def 6, do_opapp_def, + nsOptBind_def, dec_clock_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases, Once cont_rel_cases] + >> gvs[scheme_env_def, env_rel_cases] + ) + >~ [‘Lambda xs xp e’] >- ( + simp[cps_transform_def] + >> rpt strip_tac + >> qrefine ‘ck+1’ + >> simp[Ntimes evaluate_def 7, do_opapp_def, + nsOptBind_def, dec_clock_def, do_con_check_def, + build_conv_def] + >> qpat_assum ‘scheme_env mlenv’ $ simp o single + o SRULE [scheme_env_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> last_assum $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases, Once ml_v_vals'_cases] + >> gvs[scheme_env_def, env_rel_cases] + ) + >~ [‘Ident x’] >- ( + simp[cps_transform_def] + >> rpt strip_tac + >> gvs[Once valid_state_cases] + >> gvs[Once static_scope_def] + >> gvs[Once $ GSYM SPECIFICATION] + >> qpat_assum ‘env_rel _ _’ $ drule_then assume_tac + o SRULE [env_rel_cases, FEVERY_DEF] + >> qpat_assum ‘can_lookup _ _’ $ drule_then assume_tac + o SRULE [can_lookup_cases, FEVERY_DEF] + >> qpat_assum ‘LIST_REL _ _ _’ $ mp_tac + o SRULE [LIST_REL_EL_EQN, store_entry_rel_cases] + >> strip_tac + >> pop_assum $ drule_then assume_tac + >> qrefine ‘ck+1’ + >> simp[SimpLHS, Ntimes evaluate_def 7, do_opapp_def, + nsOptBind_def, dec_clock_def] + >> simp[can_pmatch_all_def, pmatch_def, evaluate_match_def, + do_app_def, store_lookup_def] + >> Cases_on ‘EL (env ' x) store’ + >> gvs[] + >> simp[can_pmatch_all_def, pmatch_def, evaluate_match_def, + do_app_def, store_lookup_def] + >> qpat_assum ‘scheme_env mlenv’ $ simp o single + o SRULE [scheme_env_def] + >> simp[same_type_def, same_ctor_def, pat_bindings_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[] + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases] + >> gvs[env_rel_cases] + ) + >~ [‘Set x e’] >- ( + simp[cps_transform_def] + >> rpt strip_tac + >> qrefine ‘ck+1’ + >> simp[SimpLHS, Ntimes evaluate_def 6, do_opapp_def, + nsOptBind_def, dec_clock_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases, Once cont_rel_cases] + >> gvs[scheme_env_def, env_rel_cases] + ) + >~ [‘Letrec bs e’] >- ( + Cases_on ‘bs’ + >> rpt strip_tac + >> gvs[cps_transform_def] >- ( + qrefine ‘ck+1’ + >> simp[SimpLHS, Ntimes evaluate_def 4, do_opapp_def, + nsOptBind_def, dec_clock_def, letpreinit_ml_def, letinit_ml_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases] + >> gvs[scheme_env_def, env_rel_cases] + ) + >> PairCases_on ‘h’ + >> simp[cps_transform_def] + >> rpt (pairarg_tac >> gvs[]) + >> qrefine ‘ck+1’ + >> simp[SimpLHS, Ntimes evaluate_def 4, do_opapp_def, + nsOptBind_def, dec_clock_def] + >> qpat_x_assum ‘letrec_preinit _ _ _ = _’ $ assume_tac o GSYM + >> drule preservation_of_letrec + >> ‘env_rel env (mlenv with v := nsBind "k" kv mlenv.v)’ + by gvs[env_rel_cases] + >> strip_tac + >> pop_assum $ drule_then drule + >> ‘scheme_env (mlenv with v := nsBind "k" kv mlenv.v)’ + by gvs[scheme_env_def] + >> strip_tac + >> pop_assum $ drule + >> strip_tac + >> pop_assum $ qspec_then + ‘Let (SOME "k'") + (Fun "t0" + (cps_transform_letinit [(h0,Var (Short "t0"))] t e + (Var (Short "k")))) + (App Opapp [cps_transform h1; Var (Short "k'")])’ mp_tac + >> rpt strip_tac + >> gvs[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trans + >> first_assum $ irule_at (Pos hd) + >> simp[eval_eq_def] + >> simp[Ntimes evaluate_def 2, nsOptBind_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once cont_rel_cases] + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pat ‘cont_rel _ _’) + >> simp[cps_app_ts_def] + >> simp[Once e_ce_rel_cases] + >> gvs[scheme_env_def, env_rel_cases] + ) + >~ [‘Letrecstar bs e’] >- ( + simp[Once cps_transform_def] + >> rpt strip_tac + >> rpt (pairarg_tac >> gvs[]) + >> qrefine ‘ck+1’ + >> simp[Ntimes evaluate_def 4, do_opapp_def, dec_clock_def] + >> pop_assum $ assume_tac o GSYM + >> drule preservation_of_letrec + >> ‘env_rel env (mlenv with v := nsBind "k" kv mlenv.v)’ + by gvs[env_rel_cases] + >> strip_tac + >> pop_assum $ drule_then drule + >> ‘scheme_env (mlenv with v := nsBind "k" kv mlenv.v)’ + by gvs[scheme_env_def] + >> strip_tac + >> pop_assum $ drule + >> strip_tac + >> pop_assum $ qspec_then + ‘App Opapp + [cps_transform (Begin (MAP (UNCURRY Set) bs) e); + Var (Short "k")]’ mp_tac + >> rpt strip_tac + >> gvs[GSYM eval_eq_def] + >> first_assum $ irule_at (Pos hd) + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases] + ) + ) + >~ [‘Val v’] >- ( + Cases_on ‘k’ + >- ( + simp[step_def, return_def] + >> rw[] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[env_rel_cases, FEVERY_FEMPTY] + >> metis_tac[] + ) + >> PairCases_on ‘h’ + >> Cases_on ‘∃ te fe . h1 = CondK te fe’ >- ( + gvs[] + >> simp[step_def, return_def] + >> simp[Once e_ce_rel_cases, Once cont_rel_cases] + >> simp[Once ml_v_vals'_cases] + >> rpt strip_tac + >> gvs[] + >> qrefine ‘ck+1’ + >> simp[SimpLHS, Ntimes evaluate_def 6, do_con_check_def, + build_conv_def, scheme_env_def, do_opapp_def, + can_pmatch_all_def, pmatch_def, dec_clock_def] + >> qpat_assum ‘scheme_env env''’ $ simp o curry ((op ::) o swap) [ + same_type_def, same_ctor_def, do_opapp_def, + evaluate_match_def, pmatch_def, pat_bindings_def] + o SRULE [scheme_env_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> gvs[] + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases] + >> gvs[scheme_env_def, env_rel_cases] + ) + >> Cases_on ‘∃ es e . h1 = BeginK es e’ >- ( + gvs[] + >> Cases_on ‘es’ + >> rpt strip_tac + >> gvs[Once cont_rel_cases, Once e_ce_rel_cases] + >> gvs[cps_transform_def, step_def, return_def] + >> qrefine ‘ck+1’ + >> simp[SimpLHS, Ntimes evaluate_def 4, do_opapp_def, + nsOptBind_def, dec_clock_def] >- ( + simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases] + >> gvs[scheme_env_def, env_rel_cases] + ) + >> simp[SimpLHS, Ntimes evaluate_def 2, nsOptBind_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases, Once cont_rel_cases] + >> gvs[scheme_env_def, env_rel_cases] + ) + >> Cases_on ‘∃ x . h1 = SetK x’ >- ( + gvs[] + >> simp[step_def, return_def, Once e_ce_rel_cases, refunc_set_def, + Once cont_rel_cases, cps_transform_def, cps_app_ts_def] + >> rpt strip_tac + >> simp[] + >> gvs[Once valid_state_cases] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac + o SRULE [Once valid_val_cases] + >> strip_tac + >> qpat_assum ‘env_rel h0 _’ $ drule_then assume_tac + o SRULE [env_rel_cases, FEVERY_DEF, SPECIFICATION] + >> qpat_assum ‘can_lookup h0 _’ $ drule_then assume_tac + o SRULE [can_lookup_cases, FEVERY_DEF, SPECIFICATION] + >> drule_then assume_tac EVERY2_LENGTH + >> drule_all_then assume_tac $ cj 2 $ iffLR LIST_REL_EL_EQN + >> gvs[store_entry_rel_cases] + >> qrefine ‘ck+1’ + >> simp[Ntimes evaluate_def 13, do_con_check_def, nsOptBind_def, + build_conv_def, scheme_env_def, do_opapp_def, dec_clock_def, + do_app_def, store_assign_def, store_v_same_type_def] + >> qpat_assum ‘scheme_env _’ $ simp o single + o SRULE [scheme_env_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[] + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases, Once ml_v_vals'_cases] + >> gvs[env_rel_cases] + >> irule EVERY2_LUPDATE_same + >> simp[store_entry_rel_cases] + ) + >> Cases_on ‘∃ xvs x bs e . h1 = LetinitK xvs x bs e’ >- ( + gvs[] + >> Cases_on ‘bs’ + >> rpt strip_tac + >> gvs[Once cont_rel_cases, Once e_ce_rel_cases] + >> gvs[cps_transform_def, step_def, return_def] + >> qrefine ‘ck+1’ + >> simp[SimpLHS, Ntimes evaluate_def 4, do_opapp_def, + nsOptBind_def, dec_clock_def] >- ( + gvs[Once valid_state_cases] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac + o SRULE [Once valid_val_cases] + >> strip_tac + >> ‘∃ xvs' . (x,v)::xvs = xvs'’ by simp[] + >> first_assum $ simp_tac bool_ss o single + >> ‘x::(MAP FST xvs) = MAP FST xvs'’ by gvs[] + >> simp_tac bool_ss [Once $ cj 3 $ GSYM ZIP_def] + >> first_assum $ simp_tac bool_ss o single + >> ‘Var (Short t')::MAP (Var o Short) ts = MAP (Var o Short) (t'::ts)’ by gvs[] + >> first_assum $ simp_tac bool_ss o single + >> irule preservation_of_letinit + >> drule cps_app_ts_distinct + >> strip_tac + >> gvs[] + >> last_assum $ irule_at (Pos last) + >> irule_at (Pos $ el 5) EQ_REFL + >> irule_at Any EQ_REFL + >> simp[] + >> irule_at (Pos last) EVERY2_MEM_MONO + >> qpat_assum ‘LIST_REL _ ts mlvs’ $ irule_at (Pat ‘LIST_REL _ ts mlvs’) + >> strip_tac >- ( + PairCases + >> simp[] + >> rpt strip_tac + >> qpat_assum ‘LIST_REL _ ts mlvs’ $ assume_tac + >> dxrule_then assume_tac EVERY2_LENGTH + >> drule_at_then (Pos $ el 2) assume_tac $ cj 1 MEM_ZIP_MEM_MAP + >> gvs[] + >> Cases_on ‘x'0 = t'’ + >> gvs[] + ) + >> gvs[scheme_env_def, env_rel_cases] + ) + >> PairCases_on ‘h’ + >> gvs[] + >> simp[cps_transform_def] + >> simp[Ntimes evaluate_def 2, nsOptBind_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases, Once cont_rel_cases] + >> simp_tac bool_ss [Once $ GSYM ZIP_def] + >> ‘Var (Short t'')::MAP (Var o Short) ts = MAP (Var o Short) (t''::ts)’ by gvs[] + >> first_assum $ simp_tac bool_ss o single + >> irule_at (Pos hd) EQ_REFL + >> simp[cps_app_ts_def] + >> rpt (pairarg_tac >> gvs[]) + >> qpat_assum ‘LIST_REL _ ts mlvs’ $ assume_tac + >> dxrule_then assume_tac EVERY2_LENGTH + >> qpat_assum ‘LIST_REL ml_v_vals' _ mlvs’ $ assume_tac + >> dxrule_then assume_tac EVERY2_LENGTH + >> gvs[] + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> qpat_assum ‘LIST_REL ml_v_vals' _ _’ $ irule_at (Pos $ el 2) + >> drule $ GSYM cps_app_ts_distinct + >> strip_tac + >> simp[] + >> irule_at (Pos hd) EVERY2_MEM_MONO + >> qpat_assum ‘LIST_REL _ ts mlvs’ $ irule_at (Pat ‘LIST_REL _ ts mlvs’) + >> strip_tac >- ( + PairCases + >> simp[] + >> rpt strip_tac + >> drule_at_then (Pos $ el 2) assume_tac $ cj 1 MEM_ZIP_MEM_MAP + >> gvs[] + >> Cases_on ‘x'0 = t''’ + >> gvs[] + ) + >> gvs[scheme_env_def, env_rel_cases] + ) + >> Cases_on ‘∃ e es . h1 = ApplyK NONE (e::es)’ >- ( + gvs[] + >> simp[step_def, return_def, Once e_ce_rel_cases, + Once cont_rel_cases, cps_transform_def, cps_app_ts_def] + >> rpt strip_tac + >> qrefine ‘ck+1’ + >> simp[Ntimes evaluate_def 6, do_opapp_def, + nsOptBind_def, dec_clock_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases, Once cont_rel_cases] + >> simp[cps_app_ts_def] + >> gvs[scheme_env_def, env_rel_cases] + ) + >> Cases_on ‘∃ fn vs e es . h1 = ApplyK (SOME (fn, vs)) (e::es)’ >- ( + gvs[] + >> simp[step_def, return_def, Once e_ce_rel_cases, + Once cont_rel_cases, cps_transform_def, cps_app_ts_def] + >> rpt strip_tac + >> qrefine ‘ck+1’ + >> simp[Ntimes evaluate_def 6, do_opapp_def, + nsOptBind_def, dec_clock_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases, Once cont_rel_cases] + >> simp[PULL_EXISTS] + >> irule_at (Pos hd) EQ_REFL + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[cps_app_ts_def] + >> rpt (pairarg_tac >> gvs[]) + >> qpat_assum ‘ml_v_vals' _ _’ $ irule_at Any + >> qpat_assum ‘LIST_REL ml_v_vals' _ _’ $ irule_at Any + >> drule $ GSYM cps_app_ts_distinct + >> strip_tac + >> simp[] + >> irule_at (Pos hd) EVERY2_MEM_MONO + >> qpat_assum ‘LIST_REL _ ts _’ $ irule_at Any + >> qpat_x_assum ‘LIST_REL _ ts _’ $ assume_tac + >> drule_then assume_tac EVERY2_LENGTH + >> strip_tac >- ( + PairCases >> simp[] + >> strip_tac + >> drule_at_then (Pos last) assume_tac MEM_ZIP_MEM_MAP + >> gvs[] + >> qsuff_tac ‘x0 ≠ t'’ + >> strip_tac + >> gvs[] + ) + >> gvs[scheme_env_def, env_rel_cases] + ) + >> Cases_on ‘h1 = ApplyK NONE []’ >- ( + gvs[] + >> simp[step_def, return_def, Once e_ce_rel_cases, Once cont_rel_cases] + >> simp[Once ml_v_vals'_cases] + >> rpt strip_tac + >> gvs[application_def, sadd_def, smul_def, sminus_def, + seqv_def, cps_transform_def, cons_list_def] + >> qrefine ‘ck+2’ + >> simp[SimpLHS, evaluate_def, do_con_check_def, + build_conv_def, do_opapp_def, dec_clock_def] + >> qpat_assum ‘scheme_env env''’ $ simp o single + o SRULE [scheme_env_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> qrefine ‘ck+1’ + >> simp[Ntimes evaluate_def 3, dec_clock_def] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >~ [‘Litv (IntLit i)’] >- ( + qrefine ‘ck+1’ + >> simp[Once evaluate_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases] + >> last_assum $ irule_at (Pos hd) + >> simp[env_rel_cases, FEVERY_FEMPTY] + ) + >~ [‘SOME (Conv (SOME (TypeStamp "SBool" _)) [ + Conv (Some (TypeStamp "True" _)) [] + ])’] >- ( + qrefine ‘ck+1’ + >> simp[Once evaluate_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases] + >> last_assum $ irule_at (Pos hd) + >> simp[env_rel_cases, FEVERY_FEMPTY] + ) + >~ [‘SOME (Conv (SOME (TypeStamp "SBool" _)) [ + Conv (Some (TypeStamp "False" _)) [] + ])’] >- ( + qrefine ‘ck+1’ + >> simp[Once evaluate_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases] + >> last_assum $ irule_at (Pos hd) + >> simp[env_rel_cases, FEVERY_FEMPTY] + ) + >~ [‘SOME (Conv (SOME (TypeStamp "SList" _)) [_])’] >- ( + qrefine ‘ck+1’ + >> simp[Once evaluate_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases] + >> last_assum $ irule_at (Pos hd) + >> simp[env_rel_cases, FEVERY_FEMPTY] + ) + >~ [‘SOME (Conv (SOME (TypeStamp "Wrong" _)) [_])’] >- ( + qrefine ‘ck+1’ + >> simp[Once evaluate_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases] + >> last_assum $ irule_at (Pos hd) + >> simp[env_rel_cases, FEVERY_FEMPTY] + ) + >> qrefine ‘ck+2’ + >> simp[evaluate_def] + >> simp[do_opapp_def, + Once find_recfun_def, Once build_rec_env_def] + >> simp[Ntimes evaluate_def 4, dec_clock_def] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >~ [‘"SAdd"’] >- ( + qrefine ‘ck+1’ + >> simp[Ntimes evaluate_def 3, nsOptBind_def, + do_con_check_def, build_conv_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> last_assum $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases, Once ml_v_vals'_cases] + >> simp[env_rel_cases, FEVERY_FEMPTY] + ) + >~ [‘"SMul"’] >- ( + qrefine ‘ck+1’ + >> simp[Ntimes evaluate_def 3, nsOptBind_def, + do_con_check_def, build_conv_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> last_assum $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases, Once ml_v_vals'_cases] + >> simp[env_rel_cases, FEVERY_FEMPTY] + ) + >~ [‘Proc _ _ _ _’] >- ( + rpt (pairarg_tac >> gvs[]) + >> irule preservation_of_proc + >> simp[] + >> qpat_assum ‘scheme_env env'³'’ $ simp + o curry ((op ::) o swap) [scheme_env_def] + o SRULE [scheme_env_def] + >> first_assum $ irule_at Any o GSYM + >> simp[vcons_list_def] + >> last_x_assum $ mp_tac o SRULE [Once valid_state_cases] + >> strip_tac + >> simp[] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> strip_tac + >> simp[] + >> qpat_x_assum ‘valid_val _ (Proc _ _ _ _)’ $ mp_tac o SRULE [Once valid_val_cases] + >> strip_tac + >> gvs[env_rel_cases] + ) + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[Once e_ce_rel_cases] + >> simp[env_rel_cases, FEVERY_FEMPTY] + >> last_assum $ irule_at Any + ) + >> Cases_on ‘∃ fn vs . h1 = ApplyK (SOME (fn, vs)) []’ >- ( + gvs[] + >> simp[step_def, return_def, Once e_ce_rel_cases, + Once cont_rel_cases] + >> rpt strip_tac + >> gvs[cps_transform_def, cons_list_def] + >> qrefine ‘ck+1’ + >> simp[evaluate_def, do_con_check_def, + build_conv_def, do_opapp_def, dec_clock_def] + >> drule $ cps_app_ts_distinct + >> strip_tac + >> ‘scheme_env (env'' with v:= nsBind t' mlv env''.v)’ by gvs[scheme_env_def] + >> qsuff_tac ‘LIST_REL (λx v'. nsLookup (env'' with v:= nsBind t' mlv + env''.v).v (Short x) = SOME v') (REVERSE (t'::ts)) (REVERSE (mlv::mlvs))’ >- ( + strip_tac + >> drule_all_then assume_tac cons_list_val + >> gvs[Once ml_v_vals'_cases] + >> gvs[application_def] + >> qpat_assum ‘scheme_env env''’ $ simp o single o SRULE [scheme_env_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >~ [‘Prim SAdd’] >- ( + qrefine ‘ck+3’ + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes evaluate_def 7, do_opapp_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> qrefine ‘ck+2’ + >> simp[Ntimes evaluate_def 2, dec_clock_def] + >> irule preservation_of_sadd_body + >> simp[] + >> irule_at (Pos hd) EQ_REFL + >> irule $ cj 1 $ iffLR LIST_REL_APPEND + >> simp[] + ) + >~ [‘Prim SMul’] >- ( + qrefine ‘ck+3’ + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes evaluate_def 7, do_opapp_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> qrefine ‘ck+2’ + >> simp[Ntimes evaluate_def 2, dec_clock_def] + >> irule preservation_of_smul_body + >> simp[] + >> simp[scheme_env2_def] + >> irule_at (Pos hd) EQ_REFL + >> irule $ cj 1 $ iffLR LIST_REL_APPEND + >> simp[] + ) + >~ [‘Prim SMinus’] >- ( + qrefine ‘ck+4’ + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes evaluate_def 5, do_opapp_def, dec_clock_def] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> irule preservation_of_sminus_body + >> simp[] + >> simp[scheme_env3_def, scheme_env2_def] + >> irule_at (Pos hd) EQ_REFL + >> irule $ cj 1 $ iffLR LIST_REL_APPEND + >> simp[] + ) + >~ [‘Proc _ _ _ _’] >- ( + qrefine ‘ck+3’ + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> qrefine ‘ck+1’ + >> simp[Ntimes evaluate_def 5, do_opapp_def, dec_clock_def] + >> rpt (pairarg_tac >> gvs[]) + >> irule preservation_of_proc + >> simp[] + >> qpat_assum ‘scheme_env env'³'’ $ simp + o curry ((op ::) o swap) [scheme_env_def] + o SRULE [scheme_env_def] + >> first_assum $ irule_at Any o GSYM + >> rpt $ irule_at Any EQ_REFL + >> simp[] + >> last_x_assum $ mp_tac o SRULE [Once valid_state_cases] + >> strip_tac + >> simp[] + >> qpat_x_assum ‘valid_cont _ _’ $ mp_tac o SRULE [Once valid_val_cases] + >> strip_tac + >> simp[] + >> qpat_x_assum ‘valid_val _ (Proc _ _ _ _)’ $ mp_tac o SRULE [Once valid_val_cases] + >> strip_tac + >> gvs[env_rel_cases] + ) + >~ [‘Prim SEqv’] >- ( + qrefine ‘ck+4’ + >> simp[Ntimes evaluate_def 3] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes evaluate_def 5, do_opapp_def, dec_clock_def] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> Cases_on ‘vs’ using SNOC_CASES + >> gvs[vcons_list_def, seqv_def] >- ( + simp[Ntimes evaluate_def 8] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases, env_rel_cases, FEVERY_FEMPTY] + ) + >> Cases_on ‘mlvs’ using SNOC_CASES + >> gvs[vcons_list_def, LIST_REL_SNOC, REVERSE_SNOC] + >> simp[Ntimes evaluate_def 5] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> Cases_on ‘l’ using SNOC_CASES + >> gvs[vcons_list_def, seqv_def] >- ( + simp[Ntimes evaluate_def 8] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> Cases_on ‘∃ n . x = SNum n’ >- ( + gvs[Once ml_v_vals'_cases] + >> simp[Ntimes evaluate_def 8] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def, do_con_check_def, build_conv_def] + >> Cases_on ‘∃ m . v = SNum m’ >- ( + gvs[Once ml_v_vals'_cases] + >> simp[Ntimes evaluate_def 11, nsOptBind_def, do_app_def] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def, do_con_check_def, build_conv_def, + do_eq_def, lit_same_type_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[env_rel_cases, FEVERY_FEMPTY] + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> Cases_on ‘i=i'’ + >> simp[Once e_ce_rel_cases, Once ml_v_vals'_cases, + Boolv_def, bool_type_num_def] + ) + >> Cases_on ‘v’ + >> gvs[Once ml_v_vals'_cases] + >> simp[Ntimes evaluate_def 8, nsOptBind_def] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def, do_con_check_def, build_conv_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[env_rel_cases, FEVERY_FEMPTY] + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases, Once ml_v_vals'_cases, + Boolv_def, bool_type_num_def] + ) + >> Cases_on ‘∃ b . x = SBool b’ >- ( + gvs[Once ml_v_vals'_cases] + >> simp[Ntimes evaluate_def 8] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def, do_con_check_def, build_conv_def] + >> (Cases_on ‘∃ b' . v = SBool b'’ >- ( + gvs[Once ml_v_vals'_cases] + >> simp[Ntimes evaluate_def 11, nsOptBind_def, do_app_def] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def, do_con_check_def, build_conv_def, + do_eq_def, lit_same_type_def, ctor_same_type_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[env_rel_cases, FEVERY_FEMPTY] + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases, Once ml_v_vals'_cases, + Boolv_def, bool_type_num_def] + )) + >> Cases_on ‘v’ >> gvs[] + >> gvs[Once ml_v_vals'_cases] + >> simp[Ntimes evaluate_def 8, nsOptBind_def] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def, do_con_check_def, build_conv_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[env_rel_cases, FEVERY_FEMPTY] + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases, Once ml_v_vals'_cases, + Boolv_def, bool_type_num_def] + ) + >> Cases_on ‘x’ >> gvs[] + >> gvs[Once ml_v_vals'_cases] + >> simp[Ntimes evaluate_def 9, nsOptBind_def] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def, do_con_check_def, build_conv_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[env_rel_cases, FEVERY_FEMPTY] + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases, Once ml_v_vals'_cases] + ) + >> Cases_on ‘l'’ using SNOC_CASES + >> gvs[vcons_list_def, LIST_REL_SNOC, REVERSE_SNOC] + >> Cases_on ‘l''’ using SNOC_CASES + >> Cases_on ‘l’ using SNOC_CASES + >> gvs[vcons_list_def, seqv_def, LIST_REL_SNOC, REVERSE_SNOC] + >> simp[Ntimes evaluate_def 8] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases, env_rel_cases, FEVERY_FEMPTY] + ) + >~ [‘Prim CallCC’] >- ( + qrefine ‘ck+4’ + >> simp[Ntimes evaluate_def 5] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> simp[Ntimes evaluate_def 4, do_opapp_def] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> simp[Ntimes evaluate_def 1, do_opapp_def, dec_clock_def] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> Cases_on ‘vs’ using SNOC_CASES + >> gvs[vcons_list_def] >- ( + simp[Ntimes evaluate_def 8] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes evaluate_def 5, do_con_check_def, build_conv_def, + nsOptBind_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[env_rel_cases, FEVERY_FEMPTY] + >> simp[Once cont_rel_cases] + >> gvs[cps_transform_def, cps_app_ts_def] + >> irule_at (Pos hd) EQ_REFL + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> qpat_assum ‘ml_v_vals' _ _’ $ irule_at Any + >> simp[Once e_ce_rel_cases] + >> simp[Once ml_v_vals'_cases] + >> simp[cons_list_def] + >> simp[scheme_env_def, env_rel_cases, FEVERY_FEMPTY] + ) + >> Cases_on ‘mlvs’ using SNOC_CASES + >> gvs[vcons_list_def, LIST_REL_SNOC, REVERSE_SNOC] + >> Cases_on ‘l’ using SNOC_CASES + >> Cases_on ‘l'’ using SNOC_CASES + >> gvs[vcons_list_def, LIST_REL_SNOC, REVERSE_SNOC] + >> simp[Ntimes evaluate_def 8] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases, env_rel_cases, FEVERY_FEMPTY] + ) + >~ [‘Throw _’] >- ( + qrefine ‘ck+4’ + >> simp[Ntimes evaluate_def 5] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> simp[Ntimes evaluate_def 5, do_opapp_def, dec_clock_def] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Ntimes find_recfun_def 2, Ntimes build_rec_env_def 2] + >> Cases_on ‘vs’ using SNOC_CASES + >> gvs[vcons_list_def] >- ( + simp[Ntimes evaluate_def 8] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[env_rel_cases, FEVERY_FEMPTY] + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases] + ) + >> Cases_on ‘mlvs’ using SNOC_CASES + >> gvs[vcons_list_def, LIST_REL_SNOC, REVERSE_SNOC] + >> Cases_on ‘l’ using SNOC_CASES + >> Cases_on ‘l'’ using SNOC_CASES + >> gvs[vcons_list_def, LIST_REL_SNOC, REVERSE_SNOC] + >> simp[Ntimes evaluate_def 8] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases, env_rel_cases, FEVERY_FEMPTY] + ) + >> qrefine ‘ck+3’ + >> simp[Ntimes evaluate_def 5] + >> simp[can_pmatch_all_def, pmatch_def, nsLookup_def, + same_type_def, same_ctor_def, evaluate_match_def, + pat_bindings_def] + >> simp[Once evaluate_def, do_opapp_def, dec_clock_def, + do_con_check_def, build_conv_def] + >> simp[GSYM eval_eq_def] + >> irule_at (Pos hd) eval_eq_trivial + >> simp[env_rel_cases, FEVERY_FEMPTY] + >> qpat_assum ‘cont_rel _ _’ $ irule_at (Pos hd) + >> simp[Once e_ce_rel_cases] + ) + >> simp[] + >> irule_at (Pos hd) EVERY2_MEM_MONO + >> qpat_assum ‘LIST_REL _ ts _’ $ irule_at Any + >> qpat_x_assum ‘LIST_REL _ ts _’ $ assume_tac + >> drule_then assume_tac EVERY2_LENGTH + >> PairCases >> simp[] + >> strip_tac + >> drule_at_then (Pos last) assume_tac MEM_ZIP_MEM_MAP + >> gvs[] + >> qsuff_tac ‘x0 ≠ t'’ + >> strip_tac + >> gvs[] + ) + >> Cases_on ‘h1’ >> gvs[] + >> Cases_on ‘l’ >> gvs[] + >> Cases_on ‘o'’ >> gvs[] + >> PairCases_on ‘x’ >> gvs[] + ) +QED + +Theorem steps_preservation: + ∀ n store store' env env' e e' k k' (st : 'ffi state) mlenv var kv mle . + FUNPOW step n (store, k, env, e) = (store', k', env', e') ∧ + valid_state store k env e ∧ + cont_rel k kv ∧ + e_ce_rel e var mlenv kv mle ∧ + env_rel env mlenv ∧ + LIST_REL store_entry_rel store st.refs + ⇒ + ∃ ck st' mlenv' var' kv' mle' . + (∀ start . evaluate (st with clock := start + ck) mlenv [mle] + = + evaluate (st' with clock := start) mlenv' [mle']) ∧ + cont_rel k' kv' ∧ + e_ce_rel e' var' mlenv' kv' mle' ∧ + env_rel env' mlenv' ∧ + LIST_REL store_entry_rel store' st'.refs ∧ + (¬ terminating_state (store', k', env', e') ⇒ n ≤ ck) ∧ + st.ffi = st'.ffi +Proof + Induct >- ( + simp[terminating_state_def] + >> rpt strip_tac + >> rpt $ pop_assum $ irule_at Any + >> qexists ‘0’ + >> simp[] + ) + >> simp[FUNPOW] + >> rpt strip_tac + >> drule valid_state_progress + >> rpt strip_tac + >> gvs[] + >> last_x_assum $ drule_then assume_tac + >> pop_assum $ drule_then assume_tac + >> drule_all step_preservation + >> rpt strip_tac + >> qpat_x_assum ‘∀ _ _ _ _ _ . _ ⇒ _’ drule_all + >> rpt strip_tac + >> qexists ‘ck + ck'’ + >> gvs[SF SFY_ss] + >> rpt $ first_assum $ irule_at Any + >> simp[] + >> strip_tac + >> gvs[] + >> drule_all_then assume_tac terminating_direction_n + >> gvs[] +QED + +Theorem value_terminating: + ∀ n e v mle mlv store store' ks env (st:'ffi state) mlenv var kv . + FUNPOW step n (store, ks, env, e) = (store', [], FEMPTY, Val v) ∧ + valid_state store ks env e ∧ + e_ce_rel e var mlenv kv mle ∧ + cont_rel ks kv ∧ + env_rel env mlenv ∧ + LIST_REL store_entry_rel store st.refs + ⇒ + ∃ ck st' mlv . evaluate (st with clock:=ck) mlenv [mle] + = (st', Rval [mlv]) ∧ + ml_v_vals' v mlv ∧ + st.ffi = st'.ffi +Proof + rpt strip_tac + >> drule_all steps_preservation + >> rpt strip_tac + >> first_x_assum $ qspec_then ‘1’ $ assume_tac + >> qexists ‘1 + ck’ + >> irule_at (Pos hd) EQ_TRANS + >> pop_assum $ irule_at (Pos hd) + >> qpat_x_assum ‘_ (Val v) _ _ _ _’ mp_tac + >> simp[Once e_ce_rel_cases] + >> rpt strip_tac + >> gvs[] + >> qpat_x_assum ‘cont_rel [] _’ mp_tac + >> simp[Once cont_rel_cases] + >> rpt strip_tac + >> gvs[] + >> simp[evaluate_def, do_opapp_def, dec_clock_def] +QED + +Theorem evaluate_timeout_smaller_clock: + ∀ ck ck' st' (st:'ffi state) env e . + evaluate (st with clock := ck) env [e] = (st', Rerr (Rabort Rtimeout_error)) ∧ + ck' ≤ ck + ⇒ + ∃ st'' . evaluate (st with clock := ck') env [e] = (st'', Rerr (Rabort Rtimeout_error)) +Proof + rpt strip_tac + >> ‘∃ i . ck = ck' + i’ by (qexists ‘ck - ck'’ >> simp[]) + >> qpat_x_assum ‘_ ≤ _’ kall_tac + >> gvs[] + >> spose_not_then assume_tac + >> Cases_on ‘evaluate (st with clock := ck') env [e]’ + >> gvs[] + >> drule_all_then assume_tac evaluate_add_to_clock + >> gvs[] +QED + +Theorem cps_val: + ∀ st env e . ∃ mle . + evaluate st env [cps_transform e] = (st, Rval [Closure env "k" mle]) +Proof + Cases_on ‘e’ + >> simp[cps_transform_def, evaluate_def] +QED + +Theorem diverges: + ∀ e v mle mlv store store' ks env (st:'ffi state) mlenv var kv . + (∀ n . ¬ terminating_state (FUNPOW step n (store, ks, env, e))) ∧ + valid_state store ks env e ∧ + e_ce_rel e var mlenv kv mle ∧ + cont_rel ks kv ∧ + env_rel env mlenv ∧ + LIST_REL store_entry_rel store st.refs + ⇒ + ∀ ck . ∃ st' . evaluate (st with clock:=ck) mlenv [mle] + = (st', Rerr (Rabort Rtimeout_error)) ∧ + st.ffi = st'.ffi +Proof + rpt strip_tac + >> last_x_assum $ qspec_then ‘ck’ assume_tac + >> Cases_on ‘FUNPOW step ck (store,ks,env,e)’ + >> PairCases_on ‘r’ + >> drule_all steps_preservation + >> rpt strip_tac + >> gvs[] + >> qpat_x_assum ‘∀ _._=_’ $ qspec_then ‘0’ assume_tac + >> qpat_x_assum ‘e_ce_rel _ _ _ _ mle'’ $ assume_tac o SRULE [Once e_ce_rel_cases] + >> gvs[terminating_state_def] + >> qpat_x_assum ‘cont_rel _ kv'’ $ assume_tac o SRULE [Once cont_rel_cases] + >> qspecl_then [‘st' with clock:=0’,‘mlenv'’,‘e'’] mp_tac cps_val + >> strip_tac + >> gvs[evaluate_def, do_opapp_def] + >> drule_all evaluate_timeout_smaller_clock + >> strip_tac + >> simp[] + >> rpt $ last_assum $ irule_at Any + >> qpat_assum ‘st.ffi = _’ $ simp o single o GSYM o Once + >> irule io_events_mono_antisym + >> drule_then assume_tac $ cj 1 evaluate_io_events_mono_imp + >> gvs[] + >> rev_drule_then assume_tac ( + cj 4 $ SRULE [PULL_FORALL] $ cj 6 $ + SRULE [is_clock_io_mono_def, pair_CASE_eq_forall] $ + cj 1 is_clock_io_mono_evaluate + ) + >> gvs[] + >> pop_assum $ drule_then assume_tac + >> gvs[] +QED + +val _ = export_theory(); diff --git a/compiler/scheme/readmePrefix b/compiler/scheme/readmePrefix new file mode 100644 index 0000000000..c0bfb8520e --- /dev/null +++ b/compiler/scheme/readmePrefix @@ -0,0 +1 @@ +A compiler from Scheme to CakeML diff --git a/compiler/scheme/scheme_astScript.sml b/compiler/scheme/scheme_astScript.sml new file mode 100644 index 0000000000..c229b8150a --- /dev/null +++ b/compiler/scheme/scheme_astScript.sml @@ -0,0 +1,134 @@ +(* + AST of Scheme +*) +open preamble; +open mlstringTheory; + +val _ = new_theory "scheme_ast"; + +Type senv = “:(mlstring |-> num)” + +(* This needs completing: Var, Lit, ... *) +Datatype: + prim = SAdd | SMul | SMinus | SEqv | CallCC +End + +Datatype: + lit = LitPrim prim | LitNum int | LitBool bool +End + +Datatype: + exp = (*Print mlstring + |*) Apply exp (exp list) + | Lit lit + | Cond exp exp exp + | Ident mlstring + | Lambda (mlstring list) (mlstring option) exp + | Begin (exp list) exp + | Set mlstring exp + | Letrec ((mlstring # exp) list) exp + | Letrecstar ((mlstring # exp) list) exp +End + +Datatype: + (*Contexts for small-step operational semantics*) + cont = ApplyK ((val # val list) option) (exp list) + | CondK exp exp + | BeginK (exp list) exp + | SetK mlstring + | LetinitK ((mlstring # val) list) mlstring ((mlstring # exp) list) exp +; + val = Prim prim | SNum int | Wrong string | SBool bool + | SList (val list) + | Proc senv (mlstring list) (mlstring option) exp + (*requires HOL 94eb753a85c5628f4fd0401deb4b7e2972a8eb25*) + | Throw ((senv # cont) list) +End + +Definition lit_to_val_def: + lit_to_val (LitPrim p) = Prim p ∧ + lit_to_val (LitNum n) = SNum n ∧ + lit_to_val (LitBool b) = SBool b +End + +Definition static_scope_def: + static_scope env (Lit lit) = T ∧ + + static_scope env (Cond c t f) = ( + static_scope env c ∧ + static_scope env t ∧ + static_scope env f) ∧ + + static_scope env (Apply fn es) = ( + static_scope env fn ∧ + static_scope_list env es) ∧ + + static_scope env (Begin es e) = ( + static_scope_list env es ∧ + static_scope env e) ∧ + + static_scope env (Lambda xs NONE e) = ( + ALL_DISTINCT xs ∧ + static_scope (env ∪ set xs) e) ∧ + + static_scope env (Lambda xs (SOME x) e) = ( + ALL_DISTINCT (x::xs) ∧ + static_scope (env ∪ set (x::xs)) e) ∧ + + static_scope env (Letrec bs e) = ( + ALL_DISTINCT (MAP FST bs) ∧ + static_scope_list (env ∪ set (MAP FST bs)) (MAP SND bs) ∧ + static_scope (env ∪ set (MAP FST bs)) e) ∧ + + static_scope env (Letrecstar bs e) = ( + ALL_DISTINCT (MAP FST bs) ∧ + static_scope_list (env ∪ set (MAP FST bs)) (MAP SND bs) ∧ + static_scope (env ∪ set (MAP FST bs)) e) ∧ + + static_scope env (Ident x) = env x ∧ + + static_scope env (Set x e) = ( + env x ∧ + static_scope env e) ∧ + + (static_scope_list env [] = T) ∧ + static_scope_list env (e::es) = (static_scope env e ∧ static_scope_list env es) +Termination + WF_REL_TAC ‘measure (λ x . case x of + | INL(_,e) => exp_size e + | INR(_,es) => list_size exp_size es)’ + >> conj_tac + >> Induct_on ‘bs’ + >> gvs[list_size_def, fetch "-" "exp_size_def"] + >> PairCases + >> strip_tac + >> gvs[list_size_def, fetch "-" "exp_size_def"] + >> pop_assum $ qspec_then ‘e’ assume_tac + >> gvs[list_size_def, fetch "-" "exp_size_def"] +End + +Theorem static_scope_mono_all: + (∀ env' e env . env ⊆ env' ∧ static_scope env e ⇒ static_scope env' e) ∧ + (∀ env' es env . env ⊆ env' ∧ static_scope_list env es ⇒ static_scope_list env' es) +Proof + ho_match_mp_tac static_scope_ind + >> rpt strip_tac + >> simp[Once static_scope_def] + >> gvs[Once static_scope_def] + >> rpt (last_x_assum $ drule_at_then (Pos last) assume_tac) + >> simp[] + >> gvs[SUBSET_DEF, SPECIFICATION] +QED + +Theorem static_scope_mono = cj 1 static_scope_mono_all; + +Theorem every_static_scope[simp]: + ∀ env . static_scope_list env = EVERY (static_scope env) +Proof + gen_tac + >> irule EQ_EXT + >> Induct + >> simp[static_scope_def] +QED + +val _ = export_theory(); diff --git a/compiler/scheme/scheme_compilerScript.sml b/compiler/scheme/scheme_compilerScript.sml new file mode 100644 index 0000000000..03cbf1d43f --- /dev/null +++ b/compiler/scheme/scheme_compilerScript.sml @@ -0,0 +1,41 @@ +(* + Definition of a compiler from Scheme to CakeML +*) +open preamble; +open fromSexpTheory simpleSexpParseTheory; +open scheme_astTheory + scheme_parsingTheory + scheme_to_cakeTheory; + +val _ = new_theory "scheme_compiler"; + +Definition cake_prog_to_string_def: + cake_prog_to_string ast = + print_sexp (listsexp (MAP decsexp ast)) +End + +Definition cake_for_err_def: + cake_for_err err_msg = + let err_str_ast = Lit (StrLit err_msg) in + cake_prog_to_string (cake_print (err_str_ast)) +End + +Definition compile_def: + compile (s:string) = + case parse_to_ast s of + | INL err_str => cake_for_err ("PARSE ERROR: " ++ err_str ++ "\n") + | INR ast => + (case codegen ast of + | INL err_str => cake_for_err ("CODEGEN ERROR: " ++ err_str ++ "\n") + | INR cake_prog => cake_prog_to_string cake_prog) +End + +(* +EVAL “compile "(print hi)"” +*) + +Definition main_function_def: + main_function s = implode (compile (explode s)) +End + +val _ = export_theory(); diff --git a/compiler/scheme/scheme_parsingScript.sml b/compiler/scheme/scheme_parsingScript.sml new file mode 100644 index 0000000000..a0e0c48f9d --- /dev/null +++ b/compiler/scheme/scheme_parsingScript.sml @@ -0,0 +1,331 @@ +(* + Parser for Scheme +*) +open preamble; +open mlstringTheory; +open scheme_valuesTheory; +open scheme_astTheory; + +val _ = new_theory "scheme_parsing"; + +val _ = monadsyntax.declare_monad("sum", { + unit = “INR”, + bind = “λ s f . case s of + | INL l => INL l + | INR r => f r”, + ignorebind = NONE, + fail = NONE, + guard = NONE, + choice = SOME “λ x y . case x of + | INL l => y + | INR r => INR r” +}); + +val _ = monadsyntax.enable_monadsyntax(); +val _ = monadsyntax.enable_monad "sum"; + +Definition mapM_def: + mapM f [] = return [] ∧ + mapM f (x::xs) = do + e <- f x; + es <- mapM f xs; + return (e::es) + od +End + +(* lexing *) + +Datatype: + token = OPEN | CLOSE | DOT | NUM num | QUOTE num + | PLUS | MINUS | TIMES | BOOL bool | WORD string +End + +Definition delimits_next_def: + delimits_next [] = T ∧ + delimits_next (c::cs) = MEM c " \t\n()#;" +End + +Definition read_bool_def: + read_bool (#"#"::c::cs) = ( + if delimits_next cs then + if MEM c "tT" then SOME (T, cs) else + if MEM c "fF" then SOME (F, cs) else + NONE + else NONE) ∧ + read_bool _ = NONE +End + +Theorem read_bool_length: + ∀ b c cs ys . + read_bool (c::cs) = SOME (b,ys) ⇒ + LENGTH ys ≤ LENGTH cs +Proof + Cases_on ‘cs’ >> rw [read_bool_def, delimits_next_def] +QED + +Definition read_num_def: + read_num l h f x acc (c::cs) = + if ORD l ≤ ORD c ∧ ORD c ≤ ORD h then + let newacc = (f * acc + (ORD c - x)) in + if delimits_next cs then SOME (newacc, cs) else + read_num l h f x newacc cs + else NONE +End + +Theorem read_num_length: + ∀l h c cs n ys f acc x. + read_num l h f x acc (c::cs) = SOME (n,ys) ⇒ + LENGTH ys ≤ LENGTH cs +Proof + Induct_on ‘cs’ >> rw [Once read_num_def, delimits_next_def] >> rw[] + >> last_assum $ drule >> rw[] +QED + +Definition read_word_def: + read_word (c::cs) = if delimits_next cs then SOME ([c], cs) else + case read_word cs of + | NONE => NONE + | SOME (ws, cs') => SOME (c::ws, cs') +End + +Theorem read_word_length: + ∀ w c cs ys . + read_word (c::cs) = SOME (w,ys) ⇒ + LENGTH ys ≤ LENGTH cs +Proof + Induct_on ‘cs’ >> rw [Once read_word_def, delimits_next_def] >> gvs[] + >> Cases_on ‘read_word (STRING h cs)’ >> gvs[] + >> PairCases_on ‘x’ >> gvs[] + >> last_assum $ drule >> rw[] +QED + +Definition end_line_def: + end_line [] = [] ∧ + end_line (c::cs) = if c = #"\n" then cs else end_line cs +End + +Theorem end_line_length: + ∀cs. STRLEN (end_line cs) < SUC (STRLEN cs) +Proof + Induct \\ rw [end_line_def] +QED + +Definition lex_def: + lex [] acc = INR acc ∧ + lex (c::cs) acc = + if MEM c " \t\n" then lex cs acc else + if c = #";" then lex (end_line cs) acc else + if c = #"." then lex cs (DOT::acc) else + if c = #"(" then lex cs (OPEN::acc) else + if c = #")" then lex cs (CLOSE::acc) else + if c = #"+" then lex cs (PLUS::acc) else + if c = #"-" then lex cs (MINUS::acc) else + if c = #"*" then lex cs (TIMES::acc) else + (*if c = #"'" then lex QUOTE cs acc else*) + case read_bool (c::cs) of + | SOME (b, rest) => lex rest (BOOL b::acc) + | NONE => case read_num #"0" #"9" 10 (ORD #"0") 0 (c::cs) of + | SOME (n, rest) => lex rest (NUM n::acc) + | NONE => case read_word (c::cs) of + | SOME (w, rest) => lex rest (WORD w::acc) + | NONE => INL ("Failed to parse at character " ++ [c]) +Termination + WF_REL_TAC ‘measure (LENGTH o FST)’ >> rw [] + >- (dxrule read_bool_length >> rw[]) + >- (dxrule read_word_length >> rw[]) + >- (dxrule read_num_length >> rw[]) + >> simp [end_line_length] +End + +Definition lexer_def: + lexer input = lex input [] +End + + +(* parsing *) + +(*Definition quote_def: + quote n = list [Num (name "'"); Num n] +End*) + +Definition parse_def: + parse [] x [] = INR x ∧ + parse [] x s = INL "Too many close brackets" ∧ + parse (CLOSE :: rest) x s = parse rest Nil (x::s) ∧ + parse (OPEN :: rest) x s = + (case s of [] => INL "Too many open brackets" + | (y::ys) => parse rest (Pair x y) ys) ∧ + parse (NUM n :: rest) x s = parse rest (Pair (Num &n) x) s ∧ + parse (BOOL b :: rest) x s = parse rest (Pair (Bool b) x) s ∧ + parse (WORD w :: rest) x s = parse rest (Pair (Word w) x) s ∧ + parse (PLUS :: rest) x s = parse rest (Pair (Word "+") x) s ∧ + parse (MINUS :: rest) x s = parse rest (Pair (Word "-") x) s ∧ + parse (TIMES :: rest) x s = parse rest (Pair (Word "*") x) s ∧ + (*parse (QUOTE n :: rest) x s = parse rest (Pair (quote n) x) s ∧*) + parse (DOT :: rest) x s = parse rest (head x) s +End + +(* +EVAL “case lexer "(print hi)" of +| INL x => INL x +| INR y => case parse y Nil [] of + | INL x => INL x + | INR y => INR (head y)” +*) + + +(* conversion to AST *) + +Definition pair_to_list_def: + pair_to_list Nil = SOME [] ∧ + pair_to_list (Pair x y) = (case pair_to_list y of + | NONE => NONE + | SOME xs => SOME (x::xs)) ∧ + pair_to_list v = NONE +End + +Theorem pair_to_list_size: + ∀ p ls . pair_to_list p = SOME ls ⇒ v_size p = list_size v_size ls +Proof + ho_match_mp_tac pair_to_list_ind + >> simp[pair_to_list_def, list_size_def] + >> rpt strip_tac + >> Cases_on ‘pair_to_list p’ >> gvs[list_size_def] +QED + +Theorem list_size_snoc[simp]: + ∀ f x xs . + list_size f (SNOC x xs) = 1 + (f x + list_size f xs) +Proof + Induct_on ‘xs’ + >> simp[list_size_def] +QED + +Definition cons_formals_def: + cons_formals ps Nil = INR (REVERSE ps, NONE) ∧ + cons_formals ps (Word w) = INR (REVERSE ps, SOME (implode w)) ∧ + cons_formals ps (Pair (Word x) y) = cons_formals (implode x::ps) y ∧ + cons_formals ps _ = INL "Invalid lambda formals" +End + +Definition cons_ast_def: + cons_ast (Num n) = INR (Lit (LitNum n)) ∧ + cons_ast (Bool b) = INR (Lit (LitBool b)) ∧ + cons_ast (Word w) = ( + if w = "+" then INR (Lit (LitPrim SAdd)) else + if w = "-" then INR (Lit (LitPrim SMinus)) else + if w = "*" then INR (Lit (LitPrim SMul)) else + if w = "eqv?" then INR (Lit (LitPrim SEqv)) else + if w = "call/cc" then INR (Lit (LitPrim CallCC)) else + INR (Ident (implode w))) ∧ + cons_ast Nil = INL "Empty S expression" ∧ + cons_ast (Pair x y) = (case pair_to_list y of + | NONE => INL "Invalid S expression" + | SOME ys => (case x of + | Word "if" => (case ys of + | [c;t;f] => do + ce <- cons_ast c; + te <- cons_ast t; + fe <- cons_ast f; + return (Cond ce te fe) + od + | _ => INL "Wrong number of expressions in if statement") + | Word "begin" => (if NULL ys + then INL "Wrong number of expressions to begin" + else do + es <- cons_ast_list (FRONT ys); + e <- cons_ast (LAST ys); + return (Begin es e) + od) + | Word "lambda" => (case ys of + | [xs;y'] => do + (ps,lp) <- cons_formals [] xs; + e <- cons_ast y'; + return (Lambda ps lp e) + od + | _ => INL "Wrong number of expressions in lambda statement") + | Word "letrec" => (case ys of + | [xs;y'] => (case pair_to_list xs of + | NONE => INL "Invalid S expression" + | SOME xs' => do + bs <- cons_ast_bindings xs'; + e <- cons_ast y'; + return (Letrec bs e) + od) + | _ => INL "Wrong number of expressions in letrec statement") + | Word "letrec*" => (case ys of + | [xs;y'] => (case pair_to_list xs of + | NONE => INL "Invalid S expression" + | SOME xs' => do + bs <- cons_ast_bindings xs'; + e <- cons_ast y'; + return (Letrecstar bs e) + od) + | _ => INL "Wrong number of expressions in letrec statement") + | Word "set!" => (case ys of + | [Word w;y'] => do + e <- cons_ast y'; + return (Set (implode w) e) + od + | _ => INL "Invalid set expression") + | fn => do + e <- cons_ast fn; + es <- cons_ast_list ys; + return (Apply e es) + od)) ∧ + + cons_ast_list [] = INR [] ∧ + cons_ast_list (x::xs) = (do + e <- cons_ast x; + es <- cons_ast_list xs; + return (e::es) + od) ∧ + + cons_ast_bindings [] = INR [] ∧ + cons_ast_bindings (x::xs) = (case pair_to_list x of + | NONE => INL "Invalid S expression" + | SOME ys => (case ys of + | [Word w;b] => do + e <- cons_ast b; + es <- cons_ast_bindings xs; + return ((implode w, e)::es) + od + | _ => INL "Invalid letrec binding")) +Termination + WF_REL_TAC ‘measure $ λ x . case x of + | INL v => v_size v + | INR (INL vs) => list_size v_size vs + | INR (INR vs') => list_size v_size vs'’ + >> rpt strip_tac + >> rpt ( + dxrule_then (assume_tac o GSYM) pair_to_list_size + >> gvs[list_size_def] + ) + >> Cases_on ‘ys’ using SNOC_CASES + >> gvs[] +End + +Definition static_scope_check_def: + static_scope_check p = if static_scope ∅ p + then INR p + else INL "Not statically scoped or duplicate parameter in lambda or letrec" +End + +Definition parse_to_ast_def: + parse_to_ast s = do + lxs <- lexer s; + e <- parse lxs Nil []; + p <- cons_ast (head e); + static_scope_check p + od +End + +(* +EVAL “cons_ast (Pair (Word "print") (Pair (Word "hi") Nil))” +EVAL “do e <- do es' <- mapM cons_ast [Word "t"; Word "h"]; return (Apply (Val (SNum 0)) es') od; es <- mapM cons_ast [Pair (Word "+") Nil; Word "-"]; return (Apply e es) od” +EVAL “parse_to_ast "((if #t + * ) 2 3)"” +EVAL “parse_to_ast "(lambda (x y . l) 2)"” +EVAL “parse_to_ast "(letrec ((x 3) (y x)) 2)"” +*) + +val _ = export_theory(); diff --git a/compiler/scheme/scheme_semanticsScript.sml b/compiler/scheme/scheme_semanticsScript.sml new file mode 100644 index 0000000000..790029513c --- /dev/null +++ b/compiler/scheme/scheme_semanticsScript.sml @@ -0,0 +1,323 @@ +(* + Semantics of Scheme +*) +open preamble; +open mlstringTheory; +open scheme_astTheory; +open finite_mapTheory; + +val _ = new_theory "scheme_semantics"; + +Datatype: + e_or_v = Exp exp | Val val | Exception mlstring +End + +Definition sadd_def: + sadd [] n = Val $ SNum n ∧ + sadd (SNum m :: xs) n = sadd xs (m + n) ∧ + sadd (_ :: xs) _ = Exception $ strlit "Arith-op applied to non-number" +End + +Definition smul_def: + smul [] n = Val $ SNum n ∧ + smul (SNum m :: xs) n = smul xs (m * n) ∧ + smul (_ :: xs) _ = Exception $ strlit "Arith-op applied to non-number" +End + +Definition sminus_def: + sminus [] = Exception $ strlit "Arity mismatch" ∧ + sminus (SNum n :: xs) = (case xs of + | [] => Val (SNum (-n)) + | _::_ => (case sadd xs 0 of + | Val (SNum m) => Val (SNum (n - m)) + | e => e)) ∧ + sminus _ = Exception $ strlit "Arith-op applied to non-number" +End + +Definition seqv_def: + seqv [v1; v2] = (Val $ SBool $ case v1 of + | SNum n => (case v2 of + | SNum m => n = m + | _ => F) + | SBool b => (case v2 of + | SBool b' => b = b' + | _ => F) + | _ => F) ∧ + seqv _ = Exception $ strlit "Arity mismatch" +End + +(* +Definition strict_def: + strict (Prim SAdd) xs = sadd xs 0 ∧ + strict (Prim SMul) xs = smul xs 1 +End + +Definition semantics_def: + semantics (Val v) = v ∧ + semantics (Apply fn args) = strict (semantics fn) (MAP semantics args) +Termination + WF_REL_TAC ‘measure exp_size’ +End +*) + +Definition fresh_loc_def: + fresh_loc store ov = (LENGTH store, SNOC ov store) +End + +Definition parameterize_def: + parameterize store env [] NONE e [] = (store, env, Exp e) ∧ + parameterize store env [] (SOME (l:mlstring)) e xs = (let (n, store') = fresh_loc store (SOME $ SList xs) + in (store', (env |+ (l, n)), Exp e)) ∧ + parameterize store env (p::ps) lp e (x::xs) = (let (n, store') = fresh_loc store (SOME x) + in parameterize store' (env |+ (p, n)) ps lp e xs) ∧ + parameterize store _ _ _ _ _ = (store, FEMPTY, Exception $ strlit "Wrong number of arguments") +End + +Definition application_def: + application store ks (Prim p) xs = (case p of + | SAdd => (store, ks, FEMPTY, sadd xs 0) + | SMul => (store, ks, FEMPTY, smul xs 1) + | SMinus => (store, ks, FEMPTY, sminus xs) + | SEqv => (store, ks, FEMPTY, seqv xs) + | CallCC => case xs of + | [v] => (store, (FEMPTY, ApplyK (SOME (v, [])) []) :: ks, FEMPTY, Val $ Throw ks) + | _ => (store, ks, FEMPTY, Exception $ strlit "Arity mismatch")) ∧ + application store ks (Proc env ps lp e) xs = (let (store', env', e') = + parameterize store env ps lp e xs in (store', ks, env', e')) ∧ + application store ks (Throw ks') xs = (case xs of + | [v] => (store, ks', FEMPTY, Val v) + | _ => (store, ks, FEMPTY, Exception $ strlit "Arity mismatch")) ∧ + application store ks _ _ = (store, ks, FEMPTY, Exception $ strlit "Not a procedure") +End + +Definition letinit_def: + letinit store (env : mlstring |-> num) [] = store ∧ + letinit store env ((x,v)::xvs) = + letinit (LUPDATE (SOME v) (env ' x) store) env xvs +End + +Definition return_def: + return store [] v = (store, [], FEMPTY, Val v) ∧ + + return store ((env, ApplyK NONE eargs) :: ks) v = (case eargs of + | [] => application store ks v [] + | e::es => (store, (env, ApplyK (SOME (v, [])) es) :: ks, env, Exp e)) ∧ + return store ((env, ApplyK (SOME (vfn, vargs)) eargs) :: ks) v = (case eargs of + | [] => application store ks vfn (REVERSE $ v::vargs) + | e::es => (store, (env, ApplyK (SOME (vfn, v::vargs)) es) :: ks, env, Exp e)) ∧ + + return store ((env, LetinitK xvs x bs e) :: ks) v = (case bs of + | [] => (letinit store env ((x,v)::xvs), ks, env, Exp e) + | (x',e')::bs' => (store, (env, LetinitK ((x,v)::xvs) x' bs' e) :: ks, env, Exp e')) ∧ + + return store ((env, CondK t f) :: ks) v = (if v = (SBool F) + then (store, ks, env, Exp f) else (store, ks, env, Exp t)) ∧ + + return store ((env, BeginK es e) :: ks) v = (case es of + | [] => (store, ks, env, Exp e) + | e'::es' => (store, (env, BeginK es' e) :: ks, env, Exp e')) ∧ + return store ((env, SetK x) :: ks) v = (LUPDATE (SOME v) (env ' x) store, ks, env, Val $ Wrong "Unspecified") +End + +Definition letrec_preinit_def: + letrec_preinit store env [] = (store, env) ∧ + letrec_preinit store env (x::xs) = (let (n, store') = fresh_loc store NONE + in letrec_preinit store' (env |+ (x, n)) xs) +End + +Definition step_def: + step (store, ks, env, Val v) = return store ks v ∧ + step (store, ks, env, Exp $ Lit lit) = (store, ks, env, Val $ lit_to_val lit) ∧ + step (store, ks, env, Exp $ Apply fn args) = (store, (env, ApplyK NONE args) :: ks, env, Exp fn) ∧ + step (store, ks, env, Exp $ Cond c t f) = (store, (env, CondK t f) :: ks, env, Exp c) ∧ + (*This is undefined if the program doesn't typecheck*) + step (store, ks, env, Exp $ Ident s) = (let ev = case EL (env ' s) store of + | NONE => Exception $ strlit "Letrec variable touched" + | SOME v => Val v + in (store, ks, env, ev)) ∧ + step (store, ks, env, Exp $ Lambda ps lp e) = (store, ks, env, Val $ Proc env ps lp e) ∧ + step (store, ks, env, Exp $ Begin es e) = (case es of + | [] => (store, ks, env, Exp e) + | e'::es' => (store, (env, BeginK es' e) :: ks, env, Exp e')) ∧ + step (store, ks, env, Exp $ Set x e) = (store, (env, SetK x) :: ks, env, Exp e) ∧ + (*There is a missing reinit check, though the spec says it is optional*) + step (store, ks, env, Exp $ Letrec bs e) = (case bs of + | [] => (store, ks, env, Exp e) + | (x,e')::bs' => let (store', env') = letrec_preinit store env (MAP FST bs) + in (store', (env', LetinitK [] x bs' e) :: ks, env', Exp e')) ∧ + step (store, ks, env, Exp $ Letrecstar bs e) = (let + (store', env') = letrec_preinit store env (MAP FST bs) + in (store', ks, env', Exp $ Begin (MAP (UNCURRY Set) bs) e)) ∧ + + step (store, ks, env, Exception ex) = (store, [], env, Exception ex) +End + +Definition steps_def: + steps (n:num) t = if n = 0 then t + else steps (n - 1) $ step t +End + +(* + open scheme_semanticsTheory; + + EVAL “steps 100 ([], [], FEMPTY, Exp $ Letrec [(strlit "x",Lit $ LitNum 2);(strlit "y",Ident $ strlit "x")] (Ident $ strlit "y"))” + EVAL “steps 10 ([], [], FEMPTY, Exp $ Apply (Lit (LitPrim SMinus)) [Lit (LitNum 4); Lit (LitNum 2)])” + EVAL “steps 4 ([], [], Apply (Val (SNum 7)) [Val (SNum 2); Val (SNum 4)])” + EVAL “steps 6 ([], [InLetK []], Apply (Val (Prim SMul)) [Val (SNum 2); Val (Prim SAdd)])” + EVAL “steps 2 ([], [], Cond (Val (SBool F)) (Val (SNum 2)) (Val (SNum 4)))” + EVAL “steps 4 ([], [], SLet [(strlit "x", Val $ SNum 42)] (Ident $ strlit "x"))” + EVAL “steps 6 ([], [], Apply (Lambda [] (SOME $ strlit "x") (Ident $ strlit "y")) [Val $ SNum 4])” + EVAL “steps 3 ([], [], Begin (Val $ SNum 1) [Val $ SNum 2])” + + EVAL “steps 16 ([], [], FEMPTY, + Apply ( + Lambda [strlit "f"; strlit "x"] NONE ( + Apply (Ident $ strlit "f") [Val $ SNum 1] + ) + ) [ + Lambda [strlit "y"] NONE ( + Apply (Val $ Prim SAdd) [ + Ident $ strlit "y"; + Ident $ strlit "x" + ] + ); + Val $ SNum 4 + ] + )” + + EVAL “steps 99 ([], [], FEMPTY,Exp $ + Apply ( + Lambda [strlit "x"] NONE ( + Apply ( + Lambda [strlit "y"] NONE ( + Apply (Lit $ LitPrim SAdd) [ + Ident $ strlit "y"; + Ident $ strlit "x" + ] + ) + ) [Lit $ LitNum 1] + ) + ) [Lit $ LitNum 4] + )” + + EVAL “steps 16 ([], [], FEMPTY, + Apply ( + Lambda [strlit "x"] NONE ( + Apply ( + Lambda [strlit "x"] NONE ( + Apply (Val $ Prim SAdd) [ + Ident $ strlit "x" + ] + ) + ) [Val $ SNum 1] + ) + ) [Val $ SNum 4] + )” + + EVAL “steps 22 ([], [], FEMPTY, + Apply ( + Lambda [strlit "x"] NONE (Begin ( + Apply ( + Lambda [strlit "y"] NONE (Begin ( + Set (strlit "x") (Val $ SNum 5) + ) [ + Apply (Val $ Prim SAdd) [ + Ident $ strlit "y"; + Ident $ strlit "x" + ] + ]) + ) [Val $ SNum 1] + ) [ + Ident $ strlit "x" + ]) + ) [Val $ SNum 4] + )” + + EVAL “steps 100 ([], [], FEMPTY, + Letrecstar [ + (strlit $ "to", Lambda [strlit "x"] NONE ( + Apply (Ident $ strlit "fro") [ + Apply (Val $ Prim SAdd) [Val $ SNum 1; Ident $ strlit "x"] + ] + )); + (strlit $ "fro", Lambda [strlit "x"] NONE ( + Apply (Ident $ strlit "to") [ + Apply (Val $ Prim SMul) [Val $ SNum 2; Ident $ strlit "x"] + ] + )) + ] (Apply (Ident $ strlit "to") [Val $ SNum 0]) + )” + + EVAL “steps 3 ([], [], FEMPTY, + Letrecstar [(strlit $ "fail", Ident $ strlit "fail")] (Val $ SBool F) + )” + + EVAL “steps 20 ([], [], FEMPTY, + Apply (Val $ Prim SMul) [ + Val $ SNum 2; + Apply (Val $ Prim CallCC) [ Lambda [strlit "x"] NONE ( + Apply (Val $ Prim SAdd) [ + Val $ SNum 4; + Cond (Val $ SBool F) ( + Val $ SNum 3 + ) ( + Apply (Ident $ strlit "x") [Val $ SNum 5] + ) + ] + )] + ] + )” + + EVAL “steps 102 ([], [], FEMPTY, + Letrecstar [ + (strlit $ "double", Val $ SNum 0); + (strlit $ "x", Val $ SNum 1) + ] (Begin ( + Apply (Val $ Prim CallCC) [ Lambda [strlit "x"] NONE ( + Set (strlit "double") (Ident $ strlit "x") + )] + ) [ + Set (strlit "x") (Apply (Val $ Prim SMul) [ + Val $ SNum 2; + Ident $ strlit "x" + ]); + Apply (Ident $ strlit "double") [Val $ SNum 0] + ]) + )” + + EVAL “steps 10 ([], [], FEMPTY, Apply (Val $ Prim SMinus) [Val $ SNum 3; Val $ SNum 2])” + + EVAL “steps 1000 ([], [], FEMPTY, Letrecstar [(strlit "fac", Lambda [strlit "x"] NONE ( + Cond (Apply (Val $ Prim SEqv) [Ident $ strlit "x"; Val $ SNum 0]) ( + Val $ SNum 1 + ) ( + Apply (Val $ Prim SMul) [Ident $ strlit "x"; Apply (Ident $ strlit "fac") [ + Apply (Val $ Prim SMinus) [Ident $ strlit "x"; Val $ SNum 1] + ]] + ) + ))] (Apply (Ident $ strlit "fac") [Val $ SNum 6]))” + + EVAL “steps 500 ([], [], FEMPTY, Exp $ Letrecstar [(strlit "fac", Lambda [strlit "x"] NONE ( + Letrecstar [(strlit "st", Lit $ LitNum 0); (strlit "acc", Lit $ LitNum 1)] ( + Begin [ Apply (Lit $ LitPrim CallCC) [ Lambda [strlit "k"] NONE ( + Set (strlit "st") (Ident $ strlit "k") + )]] ( + Cond (Apply (Lit $ LitPrim SEqv) [Ident $ strlit "x"; Lit $ LitNum 0]) + (Ident $ strlit "acc") + (Apply (Ident $ strlit "st") [ Begin [ + Set (strlit "acc") (Apply (Lit $ LitPrim SMul) [ + Ident $ strlit "acc"; + Ident $ strlit "x" + ]) + ] ( + Set (strlit "x") (Apply (Lit $ LitPrim SMinus) [ + Ident $ strlit "x"; + Lit $ LitNum 1 + ]) + )]) + ) + ) + ))] (Apply (Ident $ strlit "fac") [Lit $ LitNum 6]))” +*) + +val _ = export_theory(); \ No newline at end of file diff --git a/compiler/scheme/scheme_to_cakeScript.sml b/compiler/scheme/scheme_to_cakeScript.sml new file mode 100644 index 0000000000..e866a3b6b1 --- /dev/null +++ b/compiler/scheme/scheme_to_cakeScript.sml @@ -0,0 +1,439 @@ +(* + Code generator for Scheme to CakeML compiler +*) +open preamble; +open astTheory; +open scheme_astTheory; + +open semanticPrimitivesTheory; +open namespaceTheory; + +val _ = new_theory "scheme_to_cake"; + +Definition to_ml_vals_def: + to_ml_vals (Prim p) = Con (SOME $ Short "Prim") [case p of + | SAdd => Con (SOME $ Short "SAdd") [] + | SMul => Con (SOME $ Short "SMul") [] + | SMinus => Con (SOME $ Short "SMinus") [] + | SEqv => Con (SOME $ Short "SEqv") [] + | CallCC => Con (SOME $ Short "CallCC") []] ∧ + to_ml_vals (SNum n) = Con (SOME $ Short "SNum") [Lit $ IntLit n] ∧ + to_ml_vals (SBool b) = Con (SOME $ Short "SBool") [Con (SOME $ Short + if b then "True" else "False") []] ∧ + (*following temporary, needed for proofs*) + to_ml_vals _ = Con (SOME $ Short "Ex") [Lit $ StrLit "Not supported"] +End + +Definition cons_list_def: + cons_list [] = Con (SOME $ Short "[]") [] ∧ + cons_list (x::xs) = Con (SOME $ Short "::") [x; cons_list xs] +End + +Definition proc_ml_def: + proc_ml [] NONE k ce = Mat (Var (Short "ts")) [ + (Pcon (SOME $ Short "[]") [], + App Opapp [ce; Var (Short k)]); + (Pany, + Con (SOME $ Short "Ex") [Lit $ StrLit "Wrong number of arguments"]) + ] ∧ + proc_ml [] (SOME x) k ce = Let (SOME $ "var" ++ explode x) + (App Opref [Con (SOME $ Short "Some") [ + Con (SOME $ Short "SList") [Var (Short "ts")]]]) + (App Opapp [ce; Var (Short k)]) ∧ + proc_ml (x::xs) xp k ce = (let + inner = proc_ml xs xp k ce + in + Mat (Var (Short "ts")) [ + (Pcon (SOME $ Short "[]") [], + Con (SOME $ Short "Ex") [Lit $ StrLit "Wrong number of arguments"]); + (Pcon (SOME $ Short "::") [Pvar "t"; Pvar "ts"], + Let (SOME $ "var" ++ explode x) + (App Opref [Con (SOME $ Short "Some") [Var (Short "t")]]) + inner) + ]) +End + +Definition letpreinit_ml_def: + letpreinit_ml [] inner = inner ∧ + letpreinit_ml (x::xs) inner = Let (SOME $ "var" ++ explode x) + (App Opref [Con (SOME $ Short "None") []]) (letpreinit_ml xs inner) +End + +Definition refunc_set_def: + refunc_set t k x = Let NONE (App Opassign [Var (Short $ "var" ++ explode x); + Con (SOME $ Short "Some") [t]]) $ + Let (SOME "t") (Con (SOME $ Short "Wrong") [Lit $ StrLit "Unspecified"]) + (App Opapp [k; Var (Short "t")]) +End + +Definition letinit_ml_def: + letinit_ml [] inner = inner ∧ + letinit_ml ((x,t)::xts) inner = Let NONE + (App Opassign [Var (Short $ "var" ++ explode x); + Con (SOME $ Short "Some") [t]]) $ + letinit_ml xts inner +End + +Definition cps_transform_def: + cps_transform (Lit v) = (let + mlv = to_ml_vals $ lit_to_val v + in + Fun "k" $ Let (SOME "t") mlv $ + App Opapp [Var (Short "k"); Var (Short "t")]) ∧ + + cps_transform (Cond c t f) = (let + cc = cps_transform c; + ct = cps_transform t; + cf = cps_transform f; + in + Fun "k" $ Let (SOME "k'") (Fun "t" $ Mat (Var (Short "t")) [ + (Pcon (SOME $ Short "SBool") [Pcon (SOME $ Short "False") []], + App Opapp [cf; Var (Short "k")]); + (Pany, + App Opapp [ct; Var (Short "k")]) + ]) $ App Opapp [cc; Var (Short "k'")]) ∧ + + cps_transform (Apply fn args) = (let + cfn = cps_transform fn; + capp = cps_transform_app (Var (Short "t")) [] args (Var (Short "k")) + in + Fun "k" $ Let (SOME "k'") (Fun "t" capp) $ App Opapp [cfn; Var (Short "k'")]) ∧ + + cps_transform (Ident x) = Fun "k" $ Mat (App Opderef [Var (Short $ "var" ++ explode x)]) [ + (Pcon (SOME $ Short "None") [], + Con (SOME $ Short "Ex") [Lit $ StrLit "Letrec variable touched"]); + (Pcon (SOME $ Short "Some") [Pvar "t"], + App Opapp [Var (Short "k"); Var (Short "t")])] ∧ + + cps_transform (Lambda xs xp e) = (let + ce = cps_transform e; + inner = proc_ml xs xp "k" ce; + in + Fun "k" $ Let (SOME "t") + (Con (SOME $ Short "Proc") [Fun "k" $ Fun "ts" inner]) $ + App Opapp [Var (Short "k"); Var (Short "t")]) ∧ + + cps_transform (Begin es e) = (let + inner = cps_transform_seq (Var (Short "k")) es e + in + Fun "k" inner) ∧ + + cps_transform (Set x e) = (let + ce = cps_transform e; + inner = refunc_set (Var (Short "t")) (Var (Short "k")) x; + in + Fun "k" $ Let (SOME "k'") (Fun "t" inner) $ App Opapp [ce; Var (Short "k'")]) ∧ + + cps_transform (Letrec bs e) = (let + inner = cps_transform_letinit [] bs e (Var (Short "k")); + in + Fun "k" $ letpreinit_ml (MAP FST bs) $ inner) ∧ + + cps_transform (Letrecstar bs e) = (let + ce = cps_transform (Begin (MAP (UNCURRY Set) bs) e); + in + Fun "k" $ letpreinit_ml (MAP FST bs) $ App Opapp [ce; Var (Short "k")]) ∧ + + + cps_transform_app tfn ts (e::es) k = (let + ce = cps_transform e; + t = "t" ++ toString (LENGTH ts); + inner = cps_transform_app tfn (Var (Short t)::ts) es k + in + Let (SOME "k'") (Fun t inner) $ App Opapp [ce; Var (Short "k'")]) ∧ + + cps_transform_app tfn ts [] k = App Opapp [ + App Opapp [App Opapp [Var (Short "app"); k]; tfn]; + cons_list (REVERSE ts)] ∧ + + + cps_transform_letinit xts [] e k = (let + ce = cps_transform e + in + letinit_ml xts $ App Opapp [ce; k]) ∧ + + cps_transform_letinit xts ((x, e')::bs) e k = (let + ce = cps_transform e'; + t = "t" ++ toString (LENGTH xts); + inner = cps_transform_letinit ((x, Var (Short t))::xts) bs e k + in + Let (SOME "k'") (Fun t inner) $ App Opapp [ce; Var (Short "k'")]) ∧ + + + cps_transform_seq k [] e = (let + ce = cps_transform e + in + App Opapp [ce; k]) ∧ + + cps_transform_seq k (e'::es) e = (let + ce = cps_transform e'; + inner = cps_transform_seq k es e + in + Let (SOME "k'") (Fun "_" inner) $ App Opapp [ce; Var (Short "k'")]) +Termination + WF_REL_TAC ‘inv_image ($< LEX $<) (λ x . case x of + | INL(e) => (exp_size e, case e of Letrecstar _ _ => 1 | _ => 0) + | INR(INL(_,_,es,_)) => (list_size exp_size es, 2n) + | INR(INR(INL(_,bs,e,_))) => (exp1_size bs + exp_size e, 2) + | INR(INR(INR(_,es,e))) => (list_size exp_size es + exp_size e, 2))’ + >> rpt conj_tac + >> simp[exp_size_def] + >> rpt (Cases >> simp[] >> NO_TAC) + >> Induct + >> simp[exp_size_def] + >> PairCases + >> simp[exp_size_def] +End + +Definition compile_scheme_prog_def: + compile_scheme_prog p = let + cp = cps_transform p + in + Let (SOME $ "k") (Fun "t" $ Var (Short "t")) $ + App Opapp [cp; Var (Short "k")] +End + +Definition cake_print_def: + cake_print e = + (* val _ = print e; *) + [Dlet unknown_loc Pany (App Opapp [Var (Short "print"); e])] +End + +Definition scheme_basis1_def: + scheme_basis1 = Dtype unknown_loc [ + ([], "sprim", [ + ("SAdd", []); + ("SMul", []); + ("SMinus", []); + ("SEqv", []); + ("CallCC", []) + ]); + ([], "sval", [ + ("SNum", [Atapp [] (Short "int")]); + ("SBool", [Atapp [] (Short "bool")]); + ("Prim", [Atapp [] (Short "sprim")]); + ("SList", [Atapp [Atapp [] (Short "sval")] (Short "list")]); + ("Wrong", [Atapp [] (Short "string")]); + ("Ex", [Atapp [] (Short "string")]); + ("Proc", [Atfun + (Atfun + (Atapp [] (Short "sval")) + (Atapp [] (Short "sval"))) + (Atfun + (Atapp [Atapp [] (Short "sval")] (Short "list")) + (Atapp [] (Short "sval")))]); + ("Throw", [Atfun + (Atapp [] (Short "sval")) + (Atapp [] (Short "sval"))]); + ]) + ] +End + +Definition scheme_basis2_def: + scheme_basis2 = Dletrec unknown_loc [ + ("sadd", "k", Fun "n" $ Fun "ts" $ Mat (Var (Short "ts")) [ + (Pcon (SOME $ Short "[]") [], + Let (SOME "t") (Con (SOME $ Short "SNum") [Var (Short "n")]) $ + App Opapp [Var (Short "k"); Var (Short "t")]); + (Pcon (SOME $ Short "::") [Pvar "t"; Pvar "ts'"], + Mat (Var (Short "t")) [ + (Pcon (SOME $ Short "SNum") [Pvar "tn"], + App Opapp [ + App Opapp [ + App Opapp [Var (Short "sadd"); Var (Short "k")]; + App (Opn Plus) [Var (Short "n"); Var (Short "tn")] + ]; + Var (Short "ts'") + ]); + (Pany, + Con (SOME $ Short "Ex") [Lit $ StrLit "Arith-op applied to non-number"]) + ]) + ]) + ] +End + +Definition scheme_basis3_def: + scheme_basis3 = Dletrec unknown_loc [ + ("smul", "k", Fun "n" $ Fun "ts" $ Mat (Var (Short "ts")) [ + (Pcon (SOME $ Short "[]") [], + Let (SOME "t") (Con (SOME $ Short "SNum") [Var (Short "n")]) $ + App Opapp [Var (Short "k"); Var (Short "t")]); + (Pcon (SOME $ Short "::") [Pvar "t"; Pvar "ts'"], + Mat (Var (Short "t")) [ + (Pcon (SOME $ Short "SNum") [Pvar "tn"], + App Opapp [ + App Opapp [ + App Opapp [Var (Short "smul"); Var (Short "k")]; + App (Opn Times) [Var (Short "n"); Var (Short "tn")] + ]; + Var (Short "ts'") + ]); + (Pany, + Con (SOME $ Short "Ex") [Lit $ StrLit "Arith-op applied to non-number"]) + ]) + ]) + ] +End + +Definition scheme_basis4_def: + scheme_basis4 = Dlet unknown_loc (Pvar "sminus") $ Fun "k" $ Fun "ts" $ + Mat (Var (Short "ts")) [ + (Pcon (SOME $ Short "[]") [], + Con (SOME $ Short "Ex") [Lit $ StrLit "Arity mismatch"]); + (Pcon (SOME $ Short "::") [Pvar "t"; Pvar "ts'"], + Mat (Var (Short "t")) [ + (Pcon (SOME $ Short "SNum") [Pvar "n"], + Mat (Var (Short "ts'")) [ + (Pcon (SOME $ Short "[]") [], + Let (SOME "t") (Con (SOME $ Short "SNum") [ + App (Opn Minus) [Lit $ IntLit 0; Var (Short "n")]]) $ + App Opapp [Var (Short "k"); Var (Short "t")]); + (Pany, App Opapp [App Opapp [App Opapp [Var (Short "sadd"); + Fun "t" $ Mat (Var (Short "t")) [ + (Pcon (SOME $ Short "SNum") [Pvar "m"], + Let (SOME "t") (Con (SOME $ Short "SNum") [ + App (Opn Minus) [Var (Short "n"); Var (Short "m")]]) $ + App Opapp [Var (Short "k"); Var (Short "t")]); + (Pany, + App Opapp [Var (Short "k"); Var (Short "t")]) + ]]; + Lit $ IntLit 0]; Var (Short "ts'")]) + ]); + (Pany, + Con (SOME $ Short "Ex") [Lit $ StrLit "Arith-op applied to non-number"]) + ]) + ] +End + +Definition scheme_basis5_def: + scheme_basis5 = Dlet unknown_loc (Pvar "seqv") $ Fun "k" $ Fun "ts" $ + Mat (Var (Short "ts")) [ + (Pcon (SOME $ Short "[]") [], + Con (SOME $ Short "Ex") [Lit $ StrLit "Arity mismatch"]); + (Pcon (SOME $ Short "::") [Pvar "t1"; Pvar "ts'"], + Mat (Var (Short "ts'")) [ + (Pcon (SOME $ Short "[]") [], + Con (SOME $ Short "Ex") [Lit $ StrLit "Arity mismatch"]); + (Pcon (SOME $ Short "::") [Pvar "t2"; Pvar "ts''"], + Mat (Var (Short "ts''")) [ + (Pcon (SOME $ Short "[]") [], + (Let (SOME "t") (Con (SOME $ Short "SBool") [ + Mat (Var (Short "t1")) [ + (Pcon (SOME $ Short "SNum") [Pvar "n"], + Mat (Var (Short "t2")) [ + (Pcon (SOME $ Short "SNum") [Pvar "m"], + App Equality [Var (Short "n"); Var (Short "m")]); + (Pany, + Con (SOME $ Short "False") []) + ]); + (Pcon (SOME $ Short "SBool") [Pvar "b"], + Mat (Var (Short "t2")) [ + (Pcon (SOME $ Short "SBool") [Pvar "b'"], + App Equality [Var (Short "b"); Var (Short "b'")]); + (Pany, + Con (SOME $ Short "False") []) + ]); + (Pany, + Con (SOME $ Short "False") []) + ]]) $ App Opapp [Var (Short "k"); Var (Short "t")])); + (Pany, + Con (SOME $ Short "Ex") [Lit $ StrLit "Arity mismatch"]) + ]) + ]) + ] +End + +Definition scheme_basis6_def: + scheme_basis6 = Dlet unknown_loc (Pvar "throw") $ Fun "k" $ Fun "ts" $ + Mat (Var (Short "ts")) [ + (Pcon (SOME $ Short "[]") [], + Con (SOME $ Short "Ex") [Lit $ StrLit "Arity mismatch"]); + (Pcon (SOME $ Short "::") [Pvar "t"; Pvar "ts'"], + Mat (Var (Short "ts'")) [ + (Pcon (SOME $ Short "[]") [], + App Opapp [Var (Short "k"); Var (Short "t")]); + (Pany, + Con (SOME $ Short "Ex") [Lit $ StrLit "Arity mismatch"]); + ]) + ] +End + +Definition scheme_basis7_def: + scheme_basis7 = Dletrec unknown_loc [ + ("callcc", "k", Fun "ts" $ Mat (Var (Short "ts")) [ + (Pcon (SOME $ Short "[]") [], + Con (SOME $ Short "Ex") [Lit $ StrLit "Arity mismatch"]); + (Pcon (SOME $ Short "::") [Pvar "t"; Pvar "ts"], + Mat (Var (Short "ts")) [ + (Pcon (SOME $ Short "[]") [], + Let (SOME "k'") ( + Fun "t0" $ App Opapp [ + App Opapp [ + App Opapp [Var (Short "app");Var (Short "k")]; + Var (Short "t")]; + cons_list [Var (Short "t0")]] + ) $ Let (SOME "t") (Con (SOME $ Short "Throw") [Var (Short "k")]) $ + App Opapp [Var (Short "k'"); Var (Short "t")]); + (Pany, + Con (SOME $ Short "Ex") [Lit $ StrLit "Arity mismatch"]) + ]) + ]); + ("app", "k", Fun "fn" $ Mat (Var (Short "fn")) [ + (Pcon (SOME $ Short "Prim") [Pcon (SOME $ Short "SAdd") []], + App Opapp [App Opapp [Var (Short "sadd"); Var (Short "k")]; Lit $ IntLit 0]); + (Pcon (SOME $ Short "Prim") [Pcon (SOME $ Short "SMul") []], + App Opapp [App Opapp [Var (Short "smul"); Var (Short "k")]; Lit $ IntLit 1]); + (Pcon (SOME $ Short "Prim") [Pcon (SOME $ Short "SMinus") []], + App Opapp [Var (Short "sminus"); Var (Short "k")]); + (Pcon (SOME $ Short "Prim") [Pcon (SOME $ Short "SEqv") []], + App Opapp [Var (Short "seqv"); Var (Short "k")]); + (Pcon (SOME $ Short "Prim") [Pcon (SOME $ Short "CallCC") []], + App Opapp [Var (Short "callcc"); Var (Short "k")]); + (Pcon (SOME $ Short "Proc") [Pvar "e"], + App Opapp [Var (Short "e"); Var (Short "k")]); + (Pcon (SOME $ Short "Throw") [Pvar "k'"], + App Opapp [Var (Short "throw"); Var (Short "k'")]); + (Pany, Fun "_" $ Con (SOME $ Short "Ex") [Lit $ StrLit"Not a procedure"]) + ]) + ] +End + +Definition scheme_basis_def: + scheme_basis = [ + scheme_basis1; + scheme_basis2; + scheme_basis3; + scheme_basis4; + scheme_basis5; + scheme_basis6; + scheme_basis7 + ] +End + +Definition codegen_def: + codegen p = INR $ scheme_basis ++ [ + Dlet unknown_loc (Pvar "res") $ compile_scheme_prog p; + Dlet unknown_loc Pany $ Mat (Var (Short "res")) [ + (Pcon (SOME $ Short "SNum") [Pvar "n"], + App Opapp [Var (Short "print_int"); Var (Short "n")]); + (Pcon (SOME $ Short "SBool") [Pcon (SOME $ Short "True") []], + App Opapp [Var (Short "print"); Lit $ StrLit "#t"]); + (Pcon (SOME $ Short "SBool") [Pcon (SOME $ Short "False") []], + App Opapp [Var (Short "print"); Lit $ StrLit "#f"]); + (Pcon (SOME $ Short "Ex") [Pvar "ex"], + App Opapp [Var (Short "print"); Var (Short "ex")]); + (Pcon (SOME $ Short "Wrong") [Pany], + App Opapp [Var (Short "print"); Lit $ StrLit "unspecified"]); + (Pany, App Opapp [Var (Short "print"); Lit $ StrLit "proc"]) + ] + ] +End + +(* +open scheme_parsingTheory; +open scheme_to_cakeTheory; +EVAL “cps_transform 0 $ OUTR $ parse_to_ast +"(begin 1 2 3)"” +*) + +val _ = export_theory(); diff --git a/compiler/scheme/scheme_valuesScript.sml b/compiler/scheme/scheme_valuesScript.sml new file mode 100644 index 0000000000..91ae996820 --- /dev/null +++ b/compiler/scheme/scheme_valuesScript.sml @@ -0,0 +1,138 @@ +(* + Definition of Scheme values +*) +open preamble; +open arithmeticTheory listTheory stringTheory; + +val _ = new_theory "scheme_values"; + +(* Values in the source semantics are binary trees *) +Datatype: + v = Pair v v | Num int | Bool bool | Word string | Nil +End +(* +(* Since strings are not in the representation, we have a function that + coverts strings into numbers. Note that parsing and pretty printing + is set up so that printing reproduces these strings when possible. *) +Definition name_def: + name [] = 0 ∧ + name (c::cs) = ORD c * 256 ** (LENGTH cs) + name cs +End + +Overload Name = “λn. Num (name n)” + +(* Lists are terminated with Num 0 *) +Definition list_def[simp]: + list [] = Num 0 ∧ + list (x::xs) = Pair x (list xs) +End + +(* various convenience functions below, most are automatic rewrites [simp] *) + +Definition less_def[simp]: + less (Num n) (Num m) <=> n < m +End + +Definition plus_def[simp]: + plus (Num n) (Num m) = Num (n + m) +End + +Definition minus_def[simp]: + minus (Num n) (Num m) = Num (n - m) +End + +Definition div_def[simp]: + div (Num n) (Num m) = Num (n DIV m) +End +*) + +Definition head_def[simp]: + head (Pair x y) = x ∧ + head v = v +End + +Definition tail_def[simp]: + tail (Pair x y) = y ∧ + tail v = v +End + +Definition cons_def[simp]: + cons x y = Pair x y +End + +(* +Definition bool_def[simp]: + bool T = Num 1 ∧ + bool F = Num 0 +End + +Definition map_def[simp]: + map f xs = list (MAP f xs) +End + +Overload "list" = “map”; + +Definition pair_def[simp]: + pair f g (x,y) = Pair (f x) (g y) +End + +Definition option_def[simp]: + option f NONE = list [] ∧ + option f (SOME x) = list [f x] +End + +Definition char_def[simp]: + char c = Num (ORD c) +End + +Definition isNum_def[simp]: + isNum (Num n) = T ∧ isNum _ = F +End + +Definition getNum_def[simp]: + getNum (Num n) = n ∧ + getNum _ = 0 +End + +Definition el1_def[simp]: + el1 v = head (tail v) +End + +Definition el2_def[simp]: + el2 v = el1 (tail v) +End + +Definition el3_def[simp]: + el3 v = el2 (tail v) +End + +Overload isNil[inferior] = “isNum”; +Overload el0[inferior] = “head”; + +Theorem isNum_bool[simp]: + isNum (bool b) +Proof + Cases_on ‘b’ \\ EVAL_TAC +QED +*) + +Theorem v_size_def[simp,allow_rebind] = fetch "-" "v_size_def"; + +(*Theorem all_macro_defs = LIST_CONJ [list_def, cons_def, bool_def, + map_def, pair_def, option_def]; + +Definition is_upper_def: + (* checks whether string (represented as num) starts with uppercase letter *) + is_upper n = + if n < 256:num then + if n < 65 (* ord A = 65 *) then F else + if n < 91 (* ord Z = 90 *) then T else F + else is_upper (n DIV 256) +End + +Definition otherwise_def[simp]: + otherwise x = x +End +*) + +val _ = export_theory(); diff --git a/compiler/scheme/translation/Holmakefile b/compiler/scheme/translation/Holmakefile new file mode 100644 index 0000000000..c7b38b26e9 --- /dev/null +++ b/compiler/scheme/translation/Holmakefile @@ -0,0 +1,13 @@ +INCLUDES = $(CAKEMLDIR)/compiler/scheme $(CAKEMLDIR)/translator $(CAKEMLDIR)/basis + +all: $(DEFAULT_TARGETS) README.md +.PHONY: all + +README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml) +DIRS = $(wildcard */) +README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES) + $(CAKEMLDIR)/developers/readme_gen $(README_SOURCES) + +ifdef POLY +HOLHEAP = $(CAKEMLDIR)/basis/basis-heap +endif diff --git a/compiler/scheme/translation/README.md b/compiler/scheme/translation/README.md new file mode 100644 index 0000000000..180d1fda50 --- /dev/null +++ b/compiler/scheme/translation/README.md @@ -0,0 +1,7 @@ +CakeML translation of Scheme-to-CakeML compiler + +[scheme_compilerProgScript.sml](scheme_compilerProgScript.sml): +Build a CakeML program implementing Scheme-to-Cake compiler + +[to_sexpProgScript.sml](to_sexpProgScript.sml): +Translation of printing to CakeML sexp diff --git a/compiler/scheme/translation/readmePrefix b/compiler/scheme/translation/readmePrefix new file mode 100644 index 0000000000..c191104d69 --- /dev/null +++ b/compiler/scheme/translation/readmePrefix @@ -0,0 +1 @@ +CakeML translation of Scheme-to-CakeML compiler diff --git a/compiler/scheme/translation/scheme_compilerProgScript.sml b/compiler/scheme/translation/scheme_compilerProgScript.sml new file mode 100644 index 0000000000..71321aa461 --- /dev/null +++ b/compiler/scheme/translation/scheme_compilerProgScript.sml @@ -0,0 +1,91 @@ +(* + Build a CakeML program implementing Scheme-to-Cake compiler +*) +open preamble basis; +open to_sexpProgTheory; +open scheme_astTheory; +open scheme_parsingTheory; +open scheme_to_cakeTheory; +open scheme_compilerTheory; + +val _ = new_theory "scheme_compilerProg"; + +val _ = translation_extends "to_sexpProg"; + +(* parsing *) + +val r = translate (delimits_next_def |> SRULE [MEMBER_INTRO]); +val r = translate (read_bool_def |> SRULE [MEMBER_INTRO]); +val r = translate read_num_def; +val r = translate read_word_def; +val r = translate end_line_def; +val r = translate (lex_def |> SRULE [MEMBER_INTRO]); +val r = translate lexer_def; +(*val r = translate scheme_valuesTheory.list_def;*) +(*val r = translate scheme_valuesTheory.name_def;*) +val r = translate scheme_valuesTheory.head_def; +(*val r = translate quote_def;*) +val r = translate (IN_UNION |> SIMP_RULE bool_ss [SPECIFICATION]); +val r = translate LIST_TO_SET_DEF; +val r = translate static_scope_def; +val r = translate parse_def; +val r = translate pair_to_list_def; +val r = translate cons_formals_def; +val r = translate cons_ast_def; +val r = translate EMPTY_DEF; +val r = translate static_scope_check_def; +val r = translate parse_to_ast_def; + +(* codegen *) + +val r = translate locationTheory.unknown_loc_def; +val r = translate lit_to_val_def; +val r = translate cake_print_def; +val r = translate to_ml_vals_def; +val r = translate cons_list_def; +val r = translate proc_ml_def; +val r = translate letpreinit_ml_def; +val r = translate refunc_set_def; +val r = translate letinit_ml_def; +val r = translate cps_transform_def; +val r = translate compile_scheme_prog_def; +val r = translate scheme_basis1_def; +val r = translate scheme_basis2_def; +val r = translate scheme_basis3_def; +val r = translate scheme_basis4_def; +val r = translate scheme_basis5_def; +val r = translate scheme_basis6_def; +val r = translate scheme_basis7_def; +val r = translate scheme_basis_def; +val r = translate codegen_def; + +(* top-level compiler *) + +val r = translate cake_prog_to_string_def; +val r = translate cake_for_err_def; +val r = translate compile_def; +val r = translate main_function_def; + +(* main function *) + +val _ = type_of “main_function” = “:mlstring -> mlstring” + orelse failwith "The main_function has the wrong type."; + +val main = process_topdecs + `print (main_function (TextIO.inputAll TextIO.stdIn));`; + +val prog = + get_ml_prog_state () + |> ml_progLib.clean_state + |> ml_progLib.remove_snocs + |> ml_progLib.get_thm + |> REWRITE_RULE [ml_progTheory.ML_code_def] + |> concl |> rator |> rator |> rand + |> (fn tm => “^tm ++ ^main”) + |> EVAL |> concl |> rand; + +Definition scheme_compiler_prog_def: + scheme_compiler_prog = ^prog +End + +val _ = export_theory (); diff --git a/compiler/scheme/translation/to_sexpProgScript.sml b/compiler/scheme/translation/to_sexpProgScript.sml new file mode 100644 index 0000000000..af58535bcc --- /dev/null +++ b/compiler/scheme/translation/to_sexpProgScript.sml @@ -0,0 +1,43 @@ +(* + Translation of printing to CakeML sexp +*) +open preamble basis; +open astTheory fromSexpTheory simpleSexpParseTheory; + +val _ = new_theory "to_sexpProg"; + +val _ = translation_extends "basisProg"; + +val _ = register_type “:ast$dec”; + +(* TODO: remove all preconditions *) + +val r = translate numposrepTheory.n2l_def; +val r = translate ASCIInumbersTheory.n2s_def; +val r = translate ASCIInumbersTheory.HEX_def; +val r = translate ASCIInumbersTheory.num_to_dec_string_def; +val r = translate simpleSexpParseTheory.print_space_separated_def; +val r = translate simpleSexpParseTheory.strip_dot_def; +val r = translate simpleSexpParseTheory.escape_string_def; +val r = translate listTheory.EL; +val r = translate simpleSexpParseTheory.print_sexp_def; +val r = translate fromSexpTheory.listsexp_def; +val r = translate fromSexpTheory.locnsexp_def; +val r = translate fromSexpTheory.locssexp_def; +val r = translate stringTheory.isPrint_def; +val r = translate ASCIInumbersTheory.num_to_hex_string_def; +val r = translate fromSexpTheory.encode_control_def; +val r = translate fromSexpTheory.SEXSTR_def; +val r = translate fromSexpTheory.litsexp_def; +val r = translate fromSexpTheory.optsexp_def; +val r = translate fromSexpTheory.idsexp_def; +val r = translate fromSexpTheory.typesexp_def; +val r = translate fromSexpTheory.patsexp_def; +val r = translate fromSexpTheory.opsexp_def; +val r = translate fromSexpTheory.lopsexp_def; +val r = translate fromSexpTheory.scsexp_def; +val r = translate fromSexpTheory.expsexp_def; +val r = translate fromSexpTheory.type_defsexp_def; +val r = translate fromSexpTheory.decsexp_def; + +val _ = export_theory (); diff --git a/compiler/scheme/unverified/Compiler.hs b/compiler/scheme/unverified/Compiler.hs new file mode 100644 index 0000000000..c194dfd246 --- /dev/null +++ b/compiler/scheme/unverified/Compiler.hs @@ -0,0 +1,47 @@ +module Compiler where +import Scheme +import Prettyprinter (Pretty(pretty), (<+>), lparen, rparen, parens, line, nest, dquotes, vsep) +import System.IO (hPutStrLn, stderr) +import Control.Monad ((<=<), foldM) + +compile (ConstExp (SNum x)) = Right $ parens $ pretty "SInt" <+> pretty x +compile (ConstExp (SBool False)) = Right $ parens $ pretty "SBool" <+> pretty "False" +compile (ConstExp (SBool True)) = Right $ parens $ pretty "SBool" <+> pretty "True" + +compile (Apply (PrimExp Plus) xs) = foldM add (pretty "(SInt 0)") xs where + add p x = parens . ((pretty "sadd" <+> p) <+>) <$> compile x + +compile (Apply (PrimExp Multiply) xs) = foldM multiply (pretty "(SInt 1)") xs where + multiply p x = parens . ((pretty "smul" <+> p) <+>) <$> compile x + +compile (Cond c x y) = do + cond <- compile c + ifTrue <- compile x + ifFalse <- compile y + return $ parens $ pretty "if" <+> cond <+> pretty "then" <+> ifTrue <+> pretty "else" <+> ifFalse + +compile (Equiv x y) = do + left <- compile x + right <- compile y + return $ parens $ left <+> pretty "=" <+> right + +compile (Display x) = parens . (pretty "print_sval" <+>) <$> compile x +compile (Begin (x:xs)) = parens <$> foldl state (compile x) xs where + state p y = (<>) . (<> pretty ";") <$> p <*> compile y + +inContext x = vsep [pretty "datatype sval = SInt int | SBool bool;", + line <> nest 4 (vsep [pretty "fun print_sval v = case v of", + pretty "SInt i => print_int i", + pretty "| SBool b => print_pp (pp_bool b);"]), + line <> pretty "exception SchemeArith string;", + line <> nest 4 (vsep [pretty "fun sadd x y = case (x, y) of", + pretty "(SInt a, SInt b) => SInt (a + b)", + pretty "| (_, _) => raise SchemeArith" <+> dquotes (pretty "Argument to + must be a number") <> pretty ';']), + line <> nest 4 (vsep [pretty "fun smul x y = case (x, y) of", + pretty "(SInt a, SInt b) => SInt (a * b)", + pretty "| (_, _) => raise SchemeArith" <+> dquotes (pretty "Argument to * must be a number") <> pretty ';']), + line <> pretty "val _ =" <+> parens x <+> pretty "handle SchemeArith msg => TextIO.print_err msg;" + ] + +main = either (hPutStrLn stderr) (print . inContext . head) + . (mapM compile <=< mapM toAst <=< parse [] [] <=< schlex []) =<< getContents diff --git a/compiler/scheme/unverified/Interpreter.hs b/compiler/scheme/unverified/Interpreter.hs new file mode 100644 index 0000000000..910179071e --- /dev/null +++ b/compiler/scheme/unverified/Interpreter.hs @@ -0,0 +1,29 @@ +module Interpreter where +import Scheme +import Control.Monad (liftM2, (<=<), foldM, liftM3) +import System.IO (hPutStrLn, stderr) +import Data.Bool (bool) +import Data.Map.Strict (Map, empty, (!?), singleton, union, fromList) + +strict :: Map String SValue -> SValue -> [SValue] -> IO SValue +strict store (Proc params exps) xs = if length params == length xs + then last <$> mapM (evaluate $ union (fromList $ zip params xs) store) exps + else fail "Wrong number of arguments" +strict _ (SPrim Plus) xs = SNum <$> foldM add 0 xs where + add n (SNum x) = return $ n + x + add _ _ = fail "Argument to + must be a number" +strict _ (SPrim Multiply) xs = SNum <$> foldM multiply 1 xs where + multiply n (SNum x) = return $ n * x + multiply _ _ = fail "Argument to * must be a number" + +evaluate :: Map String SValue -> Exp -> IO SValue +evaluate store (Apply fn xs) = (mapM (evaluate store) xs >>=) . strict store =<< evaluate store fn +evaluate store (Cond c x y) = evaluate store . bool y x . (SBool False /=) =<< evaluate store c +evaluate store (Equiv x y) = SBool <$> ((==) <$> evaluate store x <*> evaluate store y) +evaluate store (Begin xs) = foldM (const $ evaluate store) Unit xs +evaluate store (Display x) = (print =<< evaluate store x) >> return Unit +evaluate store (SIdentifier i) = maybe (fail $ "Symbol " <> i <> " has no definition") return $ store !? i +evaluate store (Lambda params xs) = return $ Proc params xs +evaluate store (Val v) = return v + +main = (either fail (mapM $ evaluate $ singleton "x" $ Proc ["y"] [Apply (Val (SPrim Multiply)) [Val (SNum 2), SIdentifier "y"]]) . (mapM toAst <=< parse [] [] <=< schlex [])) =<< getContents diff --git a/compiler/scheme/unverified/Makefile b/compiler/scheme/unverified/Makefile new file mode 100644 index 0000000000..96c0645e77 --- /dev/null +++ b/compiler/scheme/unverified/Makefile @@ -0,0 +1,37 @@ +all: lib/scheme_interpreter lib/unverified_scheme_compiler +.PHONY: all clean + +%.cake.S: %.scm lib/cake lib/unverified_scheme_compiler + cat $< | ./lib/unverified_scheme_compiler | ./lib/cake $(CAKEOPT) > $@ + +%.cake: %.cake.S ../../../basis/basis_ffi.c + $(CC) $^ $(LOADLIBES) $(LDLIBS) -o $@ $(LDFLAGS) + +lib/scheme_interpreter: Interpreter.hs Scheme.hs +lib/unverified_scheme_compiler: Compiler.hs Scheme.hs +lib/scheme_interpreter lib/unverified_scheme_compiler: + @mkdir -p $(@D) + ghc $^ -main-is $(basename $<) -outputdir lib -o $@ + +CFLAGS+=-O2 +LDLIBS+=-lm + +ARCH=x64 +WORD_SIZE=64 + +lib/cake.S: + @mkdir -p $(@D) + @if [ ! -f "../../bootstrap/compilation/x64/64/$(@F)" ] ; then $(MAKE) download ; else cp ../../bootstrap/compilation/x64/64/$(@F) $@ ; fi + +download: + @echo "$(red)Could not find \`cake.S\`. Downloading the latest version from CakeML's GitHub releases.$(reset)" + curl -LO https://github.com/CakeML/cakeml/releases/latest/download/cake-$(ARCH)-$(WORD_SIZE).tar.gz + @tar -zxf cake-$(ARCH)-$(WORD_SIZE).tar.gz -C lib --strip-components 1 cake-$(ARCH)-$(WORD_SIZE)/cake.S + @rm cake-$(ARCH)-$(WORD_SIZE).tar.gz + +lib/cake: lib/cake.S ../../../basis/basis_ffi.c + @mkdir -p $(@D) + $(CC) $(CFLAGS) $^ $(LOADLIBES) $(EVALFLAG) -o $@ $(LDFLAGS) $(LDLIBS) + +clean: + rm -rf lib *.cake.S *.cake diff --git a/compiler/scheme/unverified/README.md b/compiler/scheme/unverified/README.md new file mode 100644 index 0000000000..76a54b1ed3 --- /dev/null +++ b/compiler/scheme/unverified/README.md @@ -0,0 +1 @@ +An unverified compiler from Scheme to ML written in Haskell diff --git a/compiler/scheme/unverified/Scheme.hs b/compiler/scheme/unverified/Scheme.hs new file mode 100644 index 0000000000..6286081968 --- /dev/null +++ b/compiler/scheme/unverified/Scheme.hs @@ -0,0 +1,80 @@ +module Scheme where +import Data.Typeable (cast) +import Data.Char (ord, isSpace, toLower) +import Data.Maybe (fromMaybe) +import Control.Monad (liftM2, guard) +import Control.Applicative ((<|>)) +import Data.Either.Extra (maybeToEither) +import Data.Tuple (swap) + +data ArithOp = Plus | Minus | Multiply + deriving (Show, Eq) +data Token = Open | Close | Value SValue | Identifier String + deriving Show + +data Datum = ExpList [Datum] | Const SValue | Symbol String + deriving Show +data SValue = SNum Int | SBool Bool | SPrim ArithOp | Unit | Proc [String] [Exp] + deriving (Show, Eq) + +data Exp = Apply Exp [Exp] | Cond Exp Exp Exp | Equiv Exp Exp | Begin [Exp] + | Val SValue | Display Exp | SIdentifier String | Lambda [String] [Exp] + deriving (Show, Eq) + +delimitsNext [] = True +delimitsNext (x:_) = elem x ['(', ')', '[', ']', '"', ';', '#'] || isSpace x + +lexSymb ('(':xs) = Just (xs, Open) +lexSymb (')':xs) = Just (xs, Close) +lexSymb ('[':xs) = Nothing +lexSymb (']':xs) = Nothing +lexSymb ('"':xs) = Nothing +lexSymb ('#':xs) = Nothing +lexSymb (';':xs) = Nothing +lexSymb ('+':xs) = Just (xs, Value $ SPrim Plus) +lexSymb ('-':xs) = Just (xs, Value $ SPrim Minus) +lexSymb ('*':xs) = Just (xs, Value $ SPrim Multiply) +lexSymb _ = Nothing + +lexBool ('#':x:xs) + | toLower x == 'f' && delimitsNext xs = Just (xs, Value $ SBool False) + | toLower x == 't' && delimitsNext xs = Just (xs, Value $ SBool True) + | otherwise = Nothing +lexBool _ = Nothing + +lexIdentifier (x:xs) = if delimitsNext xs then Just (xs, [x]) + else ((x:) <$>) <$> lexIdentifier xs + +lexNum acc (x:xs) = if ord '0' <= ord x && ord x <= ord '9' + then (if delimitsNext xs then Just . (xs,) . Value . SNum else flip lexNum xs) $ acc * 10 + (ord x - ord '0') + else Nothing +lexNum _ _ = Nothing + +schlex acc [] = Right acc +schlex acc ls@(x:xs) = if isSpace x then schlex acc xs + else uncurry (schlex . (:acc)) . swap =<< maybeToEither ("Failed to parse at character " <> [x]) (foldl (<|>) Nothing $ map ($ ls) [ + lexSymb, + lexBool, + lexNum 0, + ((Identifier <$>) <$>) . lexIdentifier + ]) + +parse [] p [] = Right p +parse _ _ [] = Left "Too many close brackets" +parse q p (Close:xs) = parse (ExpList p:q) [] xs +parse (ExpList q':q) p (Open:xs) = parse q (ExpList p:q') xs +parse _ _ (Open:_) = Left "Too many open brackets" +parse q p (Value v:xs) = parse q (Const v:p) xs +parse q p (Identifier i:xs) = parse q (Symbol i:p) xs + +toAst (Const v) = Right $ Val v +toAst (Symbol x) = Right $ SIdentifier x +toAst (ExpList []) = Left "Empty S expression" +toAst (ExpList [Symbol "if", c, x, y]) = Cond <$> toAst c <*> toAst x <*> toAst y +toAst (ExpList (Symbol "if":_)) = Left "Wrong number of arguments to if" +toAst (ExpList [Symbol "eq?", x, y]) = Equiv <$> toAst x <*> toAst y +toAst (ExpList [Symbol "begin"]) = Left "Wrong number of arguments to begin" +toAst (ExpList (Symbol "begin":xs)) = Begin <$> mapM toAst xs +toAst (ExpList [Symbol "display", x]) = Display <$> toAst x +toAst (ExpList (Symbol "display":_)) = Left "Wrong number of arguments to display" +toAst (ExpList xs) = liftM2 Apply head tail <$> mapM toAst xs diff --git a/developers/build-sequence b/developers/build-sequence index db62dd7e3e..1d7fb7c516 100644 --- a/developers/build-sequence +++ b/developers/build-sequence @@ -114,6 +114,12 @@ compiler/dafny/translation compiler/dafny/compilation compiler/dafny/semantics +# Scheme compiler +compiler/scheme +compiler/scheme/translation +compiler/scheme/compilation +compiler/scheme/proofs + # examples and tests characteristic/examples tutorial/solutions