Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Constant folding and propagation in word_simp #176

Merged
merged 23 commits into from
Nov 26, 2016
Merged

Constant folding and propagation in word_simp #176

Changes from 1 commit
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
19a530f
Move word_sh to wordLang
AndreasLoow Nov 8, 2016
05e286d
Move PERM_list_rearrange to wordProps
AndreasLoow Oct 27, 2016
a00e383
Eval does not affect gc_fun (same proof as code)
AndreasLoow Oct 18, 2016
06d9284
Generalize some const thms for wordLang
AndreasLoow Nov 13, 2016
da42730
Constant folding and propagation optimization for wordLang
AndreasLoow Nov 13, 2016
fbb303c
Ops, store_thm -> Q.store_thm fix mistake.
AndreasLoow Nov 14, 2016
1384d4a
Proof for if case, and remove pair_option.
AndreasLoow Nov 14, 2016
1b1d3f6
Uncomment use of constant folding in wordLang (word_simp)
myreen Nov 15, 2016
e82874b
Update compset with const prop+folding (word_simp)
myreen Nov 15, 2016
2c27f0c
Update word_simp for Div; fix metis call
myreen Nov 19, 2016
e281a55
Prove extract_labels for word_const_fp (word_simp)
myreen Nov 19, 2016
9f68b18
Remove last cheat from word_simpProof
myreen Nov 19, 2016
259577e
Merge remote-tracking branch 'origin/master' into const_fp
tanyongkiam Nov 20, 2016
9b3543e
Remove cheats due to const_fp
tanyongkiam Nov 20, 2016
08fda6e
Merge remote-tracking branch 'origin/data_to_word' into const_fp
myreen Nov 21, 2016
6fd2b5a
Adjust const_fp for updated MustTerminate
myreen Nov 21, 2016
6ea57e5
Merge branch 'const_fp' of github.com:CakeML/cakeml into const_fp
myreen Nov 21, 2016
999ba25
Add a arith_shift_right_rwt theorem.
acjf3 Nov 21, 2016
78b4269
Merge remote-tracking branch 'origin/data_to_word' into const_fp
myreen Nov 21, 2016
4e24823
Correct a reference to word_sh_def (it has moved)
xrchz Nov 23, 2016
b94a137
Merge remote-tracking branch 'origin/master' into const_fp
xrchz Nov 24, 2016
49fea6f
Fix translation of word_simp
xrchz Nov 24, 2016
f1e274c
Move word_cmp from asmSem to asm
AndreasLoow Nov 25, 2016
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Merge remote-tracking branch 'origin/data_to_word' into const_fp
  • Loading branch information
@myreen
myreen committed Nov 21, 2016
commit 78b426936803e286d3b81cdeda22a1e48f413e57

This merge commit was added into this branch cleanly.

There are no new changes to show, but you can still view the diff.