Proof Steps

[Negabinary]

Overview

This branch adds new kinds of steps to the stepper

In particular it adds steps for:

• Cases (e.g. case on whether a boolean is true/false)
• Axioms (e.g. x * 0 = 0)
• Rewrites (write your own axiom and check it with a SAT solver)

We are also porting over the coq export from #1193 for basic axiom steps.

TODOS:

• Skel-based selection
• Fix hidden steps
• substitute variables in axioms
• fix closure issues
• add context to proofs
• Fix duplicated ids in substitution
• Prevent variable escape at the end of forall (last_step in forall)
• Put rewrites in a box

TODOs for this pr:

• toggle proof actions button
• fix turn off history
• fix turn off stepper
• Add experimental warning to Algebrite thing
• Replace star button in axioms
• Add back the styling for hidden steps
• print out expression that's going to be replaced in algebrite thing

After this pr:

• inexhaustive error message

• add an error message if cases don't end at the same value

• Coq export for axioms

• Make selection select subtrees

• add inductive hypotheses to cases

• Fix capture in substitution

• Fix capture in evaluation etc

• Add conditions to axioms

• Make evaluate work

• Require filling out under-specified rewrites

• Make the exp substitution more principled

• Cleanup: combine Match Exp and Filter match

• Add a Theorem keyword and put the proofs in splices

• Make the patterns in case actually patterns and run exhaustivity, redundancy, ...

• Pattern unpacking

[codecov]

Codecov Report

Attention: Patch coverage is 6.45161% with 29 lines in your changes missing coverage. Please review.

Project coverage is 49.99%. Comparing base (c080dc1) to head (3449c5d).
Report is 50 commits behind head on dev.

Files with missing lines	Patch %	Lines
src/util/ListUtil.re	0.00%	10 Missing ⚠️
src/haz3lcore/lang/Operators.re	16.66%	5 Missing ⚠️
src/haz3lcore/pretty/ExpToSegment.re	0.00%	4 Missing ⚠️
src/haz3lcore/dynamics/DHExp.re	0.00%	3 Missing ⚠️
src/haz3lcore/dynamics/stepper/FilterMatcher.re	0.00%	3 Missing ⚠️
src/haz3lcore/dynamics/stepper/EvaluatorStep.re	0.00%	2 Missing ⚠️
src/haz3lcore/prog/CoreSettings.re	0.00%	1 Missing ⚠️
src/haz3lcore/statics/Ctx.re	0.00%	1 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##              dev    #1533      +/-   ##
==========================================
- Coverage   50.09%   49.99%   -0.10%     
==========================================
  Files         134      134              
  Lines       14855    14872      +17     
==========================================
- Hits         7441     7435       -6     
- Misses       7414     7437      +23     

Files with missing lines	Coverage Δ
src/haz3lcore/dynamics/transition/Transition.re	67.61% <100.00%> (-0.22%)	⬇️
src/util/Web.re	1.44% <ø> (ø)
src/haz3lcore/prog/CoreSettings.re	0.00% <0.00%> (ø)
src/haz3lcore/statics/Ctx.re	42.59% <0.00%> (-0.40%)	⬇️
src/haz3lcore/dynamics/stepper/EvaluatorStep.re	58.33% <0.00%> (+0.07%)	⬆️
src/haz3lcore/dynamics/DHExp.re	70.42% <0.00%> (-0.17%)	⬇️
src/haz3lcore/dynamics/stepper/FilterMatcher.re	6.91% <0.00%> (-2.81%)	⬇️
src/haz3lcore/pretty/ExpToSegment.re	77.97% <0.00%> (-0.11%)	⬇️
src/haz3lcore/lang/Operators.re	82.45% <16.66%> (-0.23%)	⬇️
src/util/ListUtil.re	32.91% <0.00%> (-1.06%)	⬇️

... and 10 files with indirect coverage changes

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.