Rationalize the SAWScript REPL #2753

sauclovian-g · 2025-10-28T03:40:03Z

This is not done yet; I just want a full CI run as a precaution...

(note for when it is done: there's a lot here and you'll almost certainly want to review one commit at a time)

sauclovian-g · 2025-10-31T08:05:39Z

Provided it doesn't break, I think it's about time to merge this one.

RyanGlScott · 2025-10-31T11:40:34Z

saw-script/src/SAWScript/REPL/Trie.hs

+module SAWScript.REPL.Trie (
+    Trie,
+    empty,
+    insert,
+    lookup,
+    lookupWithExact,
+    leaves
+ ) where


It might be worth adding some module Haddocks where saying that SAWScript.REPL.Trie is intended to be imported qualified, given that it exports some commonly-used function names like empty, insert, and lookup.

RyanGlScott · 2025-10-31T11:41:47Z

saw-script/src/SAWScript/REPL/Command.hs

+searchCmd :: Text -> REPL ()
 searchCmd str
-  | null str = do io $ putStrLn $ "[error] :search requires at least one argument"
+  | Text.null str = io $ putStrLn $ "[error] :search requires at least one argument"


Redundant $:

- | Text.null str = io $ putStrLn $ "[error] :search requires at least one argument" + | Text.null str = io $ putStrLn "[error] :search requires at least one argument"

Similarly for cdCmd.

Fixed. The one disappeared, but apparently not the other.

RyanGlScott · 2025-10-31T11:55:09Z

saw-script/src/SAWScript/REPL/Trie.hs

+          let subnode = case Map.lookup c tbl of
+                Nothing -> empty
+                Just n -> n
+              subnode' = insert' key' subnode
+          in
+          Node (Map.insert c subnode' tbl) mbValue


This uses Map.lookup/Map.insert to replace Map.alter, the latter of which is a single, fused O(log n) operation that will likely be more efficient than the former, which use two separate O(log n) operations. I would prefer using Map.alter unless you have a compelling reason not to.

To me it's clearer this way, or at least not as messy, and since there are about half a dozen REPL commands that's all the thing is used for, it can't possibly matter...

RyanGlScott · 2025-10-31T11:57:13Z

saw-script/src/SAWScript/Interpreter.hs

 import qualified Lang.Crucible.FunctionHandle as Crucible


+deriving instance Typeable AIG.Proxy


FYI: Typeable instances are automatically derived for all data types since GHC 7.10, since there's no need to keep this explicit Typeable instance around. (In fact, recent versions of GHC will warn if you try to do this.)

Removed, along with a few others that are floating about.

RyanGlScott · 2025-10-31T12:03:33Z

saw-script/src/SAWScript/REPL/Command.hs

 Stability   : provisional
 -}
 {-# LANGUAGE OverloadedStrings #-}
-- TODO RGS: Do better (or at least comment why we do this)


Thank you for fixing this! I'm embarrassed that I accidentally checked this comment in :)

RyanGlScott · 2025-10-31T12:08:42Z

saw-script/src/SAWScript/REPL/Monad.hs

-  , rTopLevelRW :: IORef TopLevelRW
-  , rProofState :: Maybe (IORef ProofState)
+  , rTopLevelRW :: TopLevelRW
+  , rProofState :: Maybe ProofState


It might be worth documenting under what conditions one can expect this field to be Just. Some of the panics introduced elsewhere in this comment talk about a "ProofScript mode", which seems relevant here.

Good thought. Done

RyanGlScott · 2025-10-31T12:20:23Z

saw-script/src/SAWScript/Import.hs

 -- found, load it. If not, raise an error.
-findAndLoadFile :: Options -> FilePath -> IO [Stmt]
+findAndLoadFile :: Options -> FilePath -> IO (Either [Text] [Stmt])


A minor thing, but after these changes, this function no longer raises an error (as claimed in the Haddocks), but instead returns an error (via Left).

RyanGlScott · 2025-10-31T12:25:45Z

saw-script/src/SAWScript/Import.hs


 -- | Load the 'Stmt's in a @.saw@ file.
-loadFile :: Options -> FilePath -> IO (Either [Text] [Stmt])
+loadFile :: Options.Options -> FilePath -> IO (Either [Text] [Stmt])


It might be worth having a separate import SAWCentral.Options (Options) statement so that we don't have to repeat ourselves in writing Options.Options.

Fixed

It looks like if GH thinks a file is deleted (even if it was actually renamed and the rename matching can't figure it out across the whole patch set) that it doesn't display the comments on it in the diff view. Sigh

RyanGlScott · 2025-10-31T12:31:22Z

saw-script/src/SAWScript/Interpreter.hs

    -- A few more misc commands

-  , prim "sharpSAT"  "Term -> TopLevel Integer"
+  , prim "sharpSAT"  "Term -> TopLevel Int"


FYI, some of the test cases' expected output needs to be updated as a result of this change.

sauclovian-g · 2025-10-31T19:01:37Z

force-push: fix routine test failures and rebase on master.

The test2314 failure is a real bug and needs further analysis.

sauclovian-g · 2025-10-31T19:50:08Z

force-push: fix the problem with test2314 (misplaced catch) and also apply one of the cosmetic review comments.

sauclovian-g · 2025-10-31T19:51:55Z

Also, the last three of the changes listed before the force-push aren't actually part of it. (Thanks, GH...)

They address the rest of the review comments so far.

sauclovian-g · 2025-11-01T06:31:47Z

ok, that's strange, a message got an extra space in it? and broke test_search... ah I see why, mistake in the 80-columns patch, I'll fix it Monday

Should have been part of #2752. (Oops.)

NFCI

Also add an export list. There should always be an export list. NFCI.

No functional change intended, except: - I fixed a typo in a string constant - use the correct panic module in Trie.hs

NFCI

For git safety this commit contains only the rename; build changes are next.

The only AIGProxy ever passed to this is compactProxy, so don't waste brain cycles on threading that through the REPL logic. Also, nothing uses the returned BuiltinContext so don't bother returning it. NFCI

NFCI

Much less guff this way... NFCI

It's not obvious if they're the same (they are) or which one should be used when. Just use "liftIO" as it's standard, even though it costs a bit more to type. NFCI

It contains some IORefs, but it's not at all clear why it does when it's already a state monad of its own, and I think I'm going to remove them. NFCI

It's already a state monad; the refs are pointless.

NFCI

Boot the rest out, mostly into a new file SAWScript.REPL.Data, so named because it provides code that inspects the data in the REPL state. NFCI

No actual changes, just move text around.

No real changes

Split the data extraction part (move to Data.hs) from the printing part.

No real changes

For now, shift the throws to the callers. This might get rearranged later, but for the moment I'm about to add more stuff to this module that has different caller requirements and I'd like it to all be uniform. The state of the chewing gum currently serving as SAW's exception handling is such that this changes the way parse errors print. (The whitespace is different and there's now a vacuous stack trace like type errors generate.) Accept this for now and update all the affected test reference outputs.

Now it's the only place that calls directly into the lexer and parser. There wasn't any code that was doing anything inappropriate with the lexer output, or anything besides feeding it directly to the parser; but on the other hand there's no reason to have five copies of that logic across three modules. NFCI

Rename readSchema to readSchemaPure because unlike all the other entry points it doesn't need IO. (It panics on any errors because it's used to handle types in the builtins table.)

Move that check out of the caller. This is somewhat ugly on the Import side for various reasons. Condensing it will happen later.

Move that check out of the caller. This is also somewhat ugly on the Import side for various reasons. Condensing it will happen later.

It was "Term -> TopLevel Integer" rather than "Term -> TopLevel Int". There is no type "Integer"; we weren't checking that the types of builtins are well formed. That's about to change. Update the affected test reference outputs.

There was no check in the caller; we were assuming all of the types of builtins were valid, and as noted in the previous commit one of them wasn't. "Oops" Beware: the check is only evaluated if something actually looks at the type. Running :search or :env is sufficient (and we have tests that do that) but just starting SAW with a bad type in the builtins table will not panic. (I tried adding some strictness notations and that didn't help; but I think detecting problems on any :search or :env run is probably acceptable so didn't try that hard.)

Instead of calling out the functions that call the typechecker as "checked", call out the ones that don't as "unchecked". NFCI. Currently the only uses that do not call the typechecker are the ones that lead into the interpreter's statement-at-a-time execution, and that's going to require other more involved cleanup before it can be made to go away.

"import" is the wrong terminology, as in SAWScript "import" means importing Cryptol. "Loader" seems like a good alternative. For git safety this commit is just the rename. Accompanying build changes are next.

The execution changes just move some of the bits to Command.hs; the completion rework is pretty much total. It should be at least marginally better than it was before, e.g. if you type "let x : <tab>" it'll offer names of types rather than values. If you spot any regressions please file issues.

Source files should have - directives - the Haddock header - the module name and export list - imports in a rational order It looks nicer to have the Haddock header first and then the directives list, but it turns out that any whole-file documentation or description has to go in the Haddock header or Haddock throws it away, and putting the directives after then makes them too far down in modules with lots of things to say.

sauclovian-g · 2025-11-03T20:14:50Z

That force-push was the fix, the one I'm about to push rebases over #2766.

sauclovian-g force-pushed the rationalize-repl branch 2 times, most recently from 108e6b2 to c249a64 Compare October 31, 2025 07:14

sauclovian-g marked this pull request as ready for review October 31, 2025 08:05

sauclovian-g requested review from RyanGlScott and brianhuffman October 31, 2025 08:05

RyanGlScott reviewed Oct 31, 2025

View reviewed changes

sauclovian-g force-pushed the rationalize-repl branch from 1d89206 to 839e07c Compare October 31, 2025 19:00

sauclovian-g force-pushed the rationalize-repl branch from 839e07c to ece1b22 Compare October 31, 2025 19:48

sauclovian-g force-pushed the rationalize-repl branch from a630f06 to e1e487a Compare November 1, 2025 18:53

sauclovian-g added 16 commits November 3, 2025 15:14

intTests/test2242_2243: Update README.

97b8a34

Should have been part of #2752. (Oops.)

Interpreter: interpretFile is internal; don't export it.

a5d3041

NFCI

REPL: SAWScript.REPL.Trie is a data type; normalize imports and naming.

db5f068

Also add an export list. There should always be an export list. NFCI.

REPL: Textify.

3025a36

No functional change intended, except: - I fixed a typo in a string constant - use the correct panic module in Trie.hs

Trie: tidy, simplify, improve naming, add comments.

2780ebc

NFCI

Trie: move to saw-support.

4598489

For git safety this commit contains only the rename; build changes are next.

Trie: build changes for the move.

43448ee

Interpreter: Simplify buildTopLevelEnv signature.

8f6b432

The only AIGProxy ever passed to this is compactProxy, so don't waste brain cycles on threading that through the REPL logic. Also, nothing uses the returned BuiltinContext so don't bother returning it. NFCI

REPL: Add missing export list to Logo.hs and remove unused type.

f537158

NFCI

REPL: Don't export stuff not used downstream and prune dead code.

a1b8e95

NFCI

REPL: Use StateT for the REPL monad, instead of handrolled.

c32e4df

Much less guff this way... NFCI

REPL: Don't disable easily fixed compiler warnings.

73196a8

REPL: It's confusing to have both "io" and "liftIO".

6291a70

It's not obvious if they're the same (they are) or which one should be used when. Just use "liftIO" as it's standard, even though it costs a bit more to type. NFCI

REPL: call the REPL state "REPLState" rather than "Refs".

cdd4ab1

It contains some IORefs, but it's not at all clear why it does when it's already a state monad of its own, and I think I'm going to remove them. NFCI

REPL: Remove the IORefs from the REPL state.

9ca8b73

It's already a state monad; the refs are pointless.

REPL: Simplify the interface for Main to start and enter the REPL.

8da71fc

NFCI

sauclovian-g added 25 commits November 3, 2025 15:14

REPL: Keep only monad widgetry in SAWScript.REPL.Monad.

0662ae1

Boot the rest out, mostly into a new file SAWScript.REPL.Data, so named because it provides code that inspects the data in the REPL state. NFCI

SAWScript.REPL.Monad: sort contents of file.

5388b63

No actual changes, just move text around.

SAWScript.REPL.Monad: fix up section dividers.

dd1c24c

No real changes

SAWScript.REPL.Command: Move code around.

1e4b446

No real changes

REPL: Tidy the :env and :tenv commands.

23bf22b

Split the data extraction part (move to Data.hs) from the printing part.

SAWScript.Import: tsort contents of file.

33fc49f

No real changes

SAWScript.Import: Simplify, unify logic.

b662b61

Rename readSchema to readSchemaPure because unlike all the other entry points it doesn't need IO. (It panics on any errors because it's used to handle types in the builtins table.)

SAWScript.Import: Typecheck after parsing schema patterns.

8289189

Move that check out of the caller. This is somewhat ugly on the Import side for various reasons. Condensing it will happen later.

SAWScript.Import: Typecheck after parsing expressions.

947d123

Move that check out of the caller. This is also somewhat ugly on the Import side for various reasons. Condensing it will happen later.

SAWScript: Correct the type of "sharpSAT".

7d57089

It was "Term -> TopLevel Integer" rather than "Term -> TopLevel Int". There is no type "Integer"; we weren't checking that the types of builtins are well formed. That's about to change. Update the affected test reference outputs.

SAWScript.Import: Rename to SAWScript.Loader.

8f63729

"import" is the wrong terminology, as in SAWScript "import" means importing Cryptol. "Loader" seems like a good alternative. For git safety this commit is just the rename. Accompanying build changes are next.

Build changes for renaming SAWScript.Import -> SAWScript.Loader.

8ab6191

REPL: Simplify and clarify code more.

90bf20a

REPL: Now rework the way things execute in Command.hs.

c5794c4

REPL: a few more minor cleanups

0fe9e5a

REPL: Edit width should be 80. NFCI

8b6c2c2

More haddocks (review comments + other adjacent bits)

8f1c9fb

Remove obsolete explicit Typeable references.

4db4a29

SAWScript.Loader: Avoid writing "Options.Options"

1087bb5

sauclovian-g force-pushed the rationalize-repl branch from e1e487a to 1087bb5 Compare November 3, 2025 20:15

RyanGlScott approved these changes Nov 3, 2025

View reviewed changes

sauclovian-g merged commit 1c52684 into master Nov 3, 2025
37 checks passed

sauclovian-g deleted the rationalize-repl branch November 3, 2025 21:43

		import qualified Lang.Crucible.FunctionHandle as Crucible


		deriving instance Typeable AIG.Proxy

Rationalize the SAWScript REPL #2753

Rationalize the SAWScript REPL #2753

Conversation

sauclovian-g commented Oct 28, 2025

Uh oh!

sauclovian-g commented Oct 31, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sauclovian-g commented Oct 31, 2025

Uh oh!

sauclovian-g commented Oct 31, 2025

Uh oh!

sauclovian-g commented Oct 31, 2025

Uh oh!

sauclovian-g commented Nov 1, 2025

Uh oh!

sauclovian-g commented Nov 3, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants