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

Jump to bottom

Candle REPL fixes #903

Closed
wants to merge 149 commits into from
Closed

Candle REPL fixes #903

wants to merge 149 commits into from

Conversation

oskarabrahamsson
Copy link
Contributor

@oskarabrahamsson oskarabrahamsson commented Aug 16, 2022 •
edited

See #904.

@oskarabrahamsson
Give names to rules in proves relation
b0aa65e
@oskarabrahamsson
Add first version of compute syntax (with cheats)
7133ed3
@oskarabrahamsson
Prove all theorems in computeSyntax
31b7328
@oskarabrahamsson
Move candle_kernel and computeSyntax
701e62c
@oskarabrahamsson
Update READMEs
17ff675
@oskarabrahamsson
Add lists+overloads to compute syntax
ab76610
@oskarabrahamsson
Add functions for inserting :thm checks
8826164
@oskarabrahamsson
Comment about term_ok
e2bbfe3
@oskarabrahamsson
Add some boolean syntax
ef52b57
@oskarabrahamsson
Use the BIT1 equation with addition
761b96c
@oskarabrahamsson
Un-local a few theorems
d88c827
@oskarabrahamsson
Sketch compute_add and its correctness
d87d926
@oskarabrahamsson
Derive term_ok from proves
aa3aecd
@oskarabrahamsson
Move overloads to top
e39717b
@oskarabrahamsson
Use quantifier-free theorems (and the real BIT1)
96d93ba
@oskarabrahamsson
Derive term_ok for bool_thy_ok
93c15cf
@oskarabrahamsson
Update num2bit _0-case
4b9906c
@oskarabrahamsson
Set up the necessary cheats for compute_add_thm
28377fb
@oskarabrahamsson
Un-local theorems and prove BIT0 equation
69f2343
@oskarabrahamsson
Prove compute_add correctness
e3b6b31
@oskarabrahamsson
Rename num_ths
3a329ec
@oskarabrahamsson
Update README
084be7c
@oskarabrahamsson
Translate compute_add
d883b53
@oskarabrahamsson
Make sure candle_kernelProg builds
48d24d2
@oskarabrahamsson
Lift runtime typechecking code into its own lib/thy
3332755
@oskarabrahamsson
Add PMATCH definitions for compute functions
ee572d1
@oskarabrahamsson
Add thm list check
3a8825b
@oskarabrahamsson
Add checks to compute_add translation
52b9bf6
@oskarabrahamsson
Update kernel_vals with compute_add and check_thm{_list}
2d56371
@oskarabrahamsson
Prove perms theorems for new functions
4c3b33a
oskarabrahamsson and others added 28 commits June 3, 2022 20:34
@oskarabrahamsson
Updates to compute permissions
5efea5a
@oskarabrahamsson
Update kernel_vals_ok proof
ed5e154
@oskarabrahamsson
Hide some overloads in prover_evaluate
f647fe2
@oskarabrahamsson
Hide some overloads in basis_evaluate
fc3e665
@oskarabrahamsson
Fix prover_semantics
b67a3a7
@oskarabrahamsson
Prove compute_eval always succeeds or diverges
e2b5bf7 
compute_eval will either succeed or raise a <<timeout>> exception.
Unfortunately the type checks in compute raises all sorts of exceptions
if the type check fails, so this fact is not visible in the top-level
theorem.
@oskarabrahamsson
Qualify :asm$binop to avoid translation issues
06f0fa9
@oskarabrahamsson
Implement equality for :compute_exp
3f2a93b
@oskarabrahamsson
Gather all compute files under the same directory
dcfd05c
@oskarabrahamsson
Update generated READMEs
fb4a1d9
@oskarabrahamsson
Collect 1-ary ops in one datatype
a9ce89a
@myreen
Merge remote-tracking branch 'origin/master' into candle-compute-v4
18d4960
@myreen
Merge remote-tracking branch 'origin/master' into candle-compute-v4
e6644ca
@oskarabrahamsson
Add LET to compute_syntax
c92d5fd
@oskarabrahamsson
Update compute_syntaxProof with LET
aaf0500
@oskarabrahamsson
Update compute_evalScript
5668ba7
@oskarabrahamsson
Fix main eval theorem but cheat two lemmas
3d1a916
@oskarabrahamsson
Add the LET equation to the init thms
71d1c3c
@oskarabrahamsson
Update const_list and var_list
ae34144
@oskarabrahamsson
Update check_cexp_closed
1c9c588
@oskarabrahamsson
Update translation
166f04c
@oskarabrahamsson
Fix how candle_kernel_vals finds v_defs
c7735b9
@oskarabrahamsson
Hide compute_exp "Let" constructor
bb348b2
@oskarabrahamsson
Remove VFREE_IN cheat
47ee756
@oskarabrahamsson
Remove the last cheat in compute_evalProof
1fe70b1
@oskarabrahamsson
Treat type variables more robustly in REPL
ac36a04
@oskarabrahamsson
Various fixes to Candle REPL
8ba7d44 
- Pointer equality definition (==) defaulting to false
- Define rat_minus
- Define a printer for rationals
- Set userInput when recovering from error
- Add comment about exception printer
@oskarabrahamsson
Use loads/needs instead of #load/#need in REPL
e6dce39 
This makes the REPL pick up on the words 'needs' and 'loads' when
they sit at the top level. If they are followed by a string literal
and a double semicolon token, the REPL loads a file (like previously
with #load and #need).

The motivation behind this change is to make sure Candle accepts HOL
Light source files with as minor changes as possible.
@oskarabrahamsson
Copy link
Contributor Author

Err, looks like these commits got tacked onto the candle-compute-v3 branch. Please ignore.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@oskarabrahamsson @myreen