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.

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

let inlining in goal printing #1832

Merged
merged 15 commits into from
May 17, 2023
Merged

let inlining in goal printing #1832

merged 15 commits into from
May 17, 2023

Conversation

samcowger
Copy link
Contributor

This implements a new primitive, print_goal_inline :: [Int] -> ProofScript (). print_goal_inline, provided a list of numbers, prints the current goal while inlining the memoization variables that would otherwise be assigned a number in the provided list.

@samcowger samcowger changed the title let inlining let inlining in goal printing Mar 3, 2023
Copy link
Contributor

@eddywestbrook eddywestbrook left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please add a haddock for print_goal_inline. You can just copy the doc string for it in the interpreter. Also, it would be good to think about how to test this functionality, though testing printing is always a bear. Otherwise, these changes look good to me!

KarmaHaze

This comment was marked as spam.

@samcowger samcowger requested a review from eddywestbrook April 13, 2023 20:20
@samcowger samcowger requested a review from RyanGlScott May 4, 2023 20:08
src/SAWScript/Interpreter.hs Outdated Show resolved Hide resolved
saw-core/src/Verifier/SAW/Term/Pretty.hs Outdated Show resolved Hide resolved
saw-core/src/Verifier/SAW/Term/Pretty.hs Outdated Show resolved Hide resolved
saw-core/src/Verifier/SAW/Term/Pretty.hs Outdated Show resolved Hide resolved
@samcowger samcowger added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label May 16, 2023
@mergify mergify bot merged commit fc9378a into master May 17, 2023
@mergify mergify bot deleted the feature/let-inlining branch May 17, 2023 21:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants