Skip to content

Add missing bits to SAWScript's Cryptol import syntax #2607

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

Merged
merged 2 commits into from
Sep 18, 2025
Merged

Add missing bits to SAWScript's Cryptol import syntax #2607

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f04b00b
Add two missing bits to SAWScript's Cryptol import syntax.
sauclovian-g Sep 17, 2025
c3f765d
Bump CABAL_CACHE_VERSION to 12.
sauclovian-g Sep 18, 2025
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
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ env:
# version is changed but older .so files are cached, which can have various
# effects (e.g. cabal complains it can't find a valid version of the "happy"
# tool).
CABAL_CACHE_VERSION: 10
CABAL_CACHE_VERSION: 12
CARGO_CACHE_VERSION: 1
SOLVER_CACHE_VERSION: 1

Expand Down
4 changes: 4 additions & 0 deletions intTests/test2605/Foo.cry
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
module Foo where

x : [8]
x = 3
3 changes: 3 additions & 0 deletions intTests/test2605/test.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
import "Foo.cry" as Moo::Boo;

let y = {{ Moo::Boo::x }};
3 changes: 3 additions & 0 deletions intTests/test2605/test.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
set -e

$SAW test.saw
4 changes: 2 additions & 2 deletions intTests/test_sawscript_builtins/files.log.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@
[104, 101, 108, 108, 111, 10]
dump_file_AST:
Loading file "include/syntax.saw"
StmtImport include/syntax.saw:5:1-5:30 (Import {iModule = Left "Foo.cry", iAs = Just (ModName "Foo" NormalName), iSpec = Just (Only [Ident False NormalName "foo"]), iPos = include/syntax.saw:5:8-5:30})
StmtImport include/syntax.saw:6:1-6:30 (Import {iModule = Left "Bar.cry", iAs = Nothing, iSpec = Just (Hiding [Ident False NormalName "bar"]), iPos = include/syntax.saw:6:8-6:30})
StmtImport include/syntax.saw:5:1-5:30 (Import {iIsSubmodule = False, iModule = Left "Foo.cry", iAs = Just (ModName "Foo" NormalName), iSpec = Just (Only [Ident False NormalName "foo"]), iPos = include/syntax.saw:5:8-5:30})
StmtImport include/syntax.saw:6:1-6:30 (Import {iIsSubmodule = False, iModule = Left "Bar.cry", iAs = Nothing, iSpec = Just (Hiding [Ident False NormalName "bar"]), iPos = include/syntax.saw:6:8-6:30})
StmtBind include/syntax.saw:8:1-8:4 (PWild include/syntax.saw:8:1-8:1 Nothing) (Int include/syntax.saw:8:1-8:4 123)
StmtBind include/syntax.saw:9:1-9:16 (PVar include/syntax.saw:9:1-9:2 "a" (include/syntax.saw:9:1-9:2) Nothing) (Application include/syntax.saw:9:6-9:16 (Var "return" (include/syntax.saw:9:6-9:12)) (Int include/syntax.saw:9:13-9:16 456))
StmtLet include/syntax.saw:11:1-11:12 (NonRecursive (Decl {dPos = include/syntax.saw:11:5-11:12, dPat = PVar include/syntax.saw:11:5-11:6 "f" (include/syntax.saw:11:5-11:6) Nothing, dType = Nothing, dDef = Lambda include/syntax.saw:11:7-11:12 (Just "f") (PVar include/syntax.saw:11:7-11:8 "x" (include/syntax.saw:11:7-11:8) Nothing) (Var "x" (include/syntax.saw:11:11-11:12))}))
Expand Down
3 changes: 2 additions & 1 deletion saw-central/src/SAWCentral/AST.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,8 @@ type LName = Located Name
-- Expr Level {{{

data Import = Import
{ iModule :: Either FilePath P.ModName
{ iIsSubmodule :: Bool
, iModule :: Either FilePath P.ModName
, iAs :: Maybe P.ModName
, iSpec :: Maybe P.ImportSpec
, iPos :: Pos
Expand Down
2 changes: 1 addition & 1 deletion saw-script/src/SAWScript/Lexer.x
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ $idfirst = [$alpha \_]
$idchar = [$alpha $digit $unidigit $unitick \' \_]
$codechar = [$graphic $whitechar \n]

@reservedid = import|and|let|rec|in|do|if|then|else|as|hiding|typedef
@reservedid = import|submodule|and|let|rec|in|do|if|then|else|as|hiding|typedef
|JavaSetup|LLVMSetup|MIRSetup|ProofScript|TopLevel|CrucibleSetup
|Int|String|Term|Type|Bool|AIG|CFG
|CrucibleMethodSpec|LLVMSpec|JVMMethodSpec|JVMSpec|MIRSpec
Expand Down
26 changes: 24 additions & 2 deletions saw-script/src/SAWScript/Parser.y
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,7 @@ import Control.Exception

%token
'import' { TReserved _ "import" }
'submodule' { TReserved _ "submodule" }
Copy link
Contributor

Choose a reason for hiding this comment

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

Surely we should have a test case that exercises this new bit of the parser?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

We should, but I left it off for now because it's going to interact with Mark's branches. There's basically three options:

  1. Merge this now, rebase all of Mark's code on it, add code there to recognize the submodule tag when processing the import, add a test there.

  2. Merge Mark's code first, rebase this on it, add code here to recognize the submodule tag when processing the import, add a test here.

  3. Merge both independently, then do another branch that adds the code to recognize the submodule tag when processing the import along with a test.

For various reasons (3) seems preferable...

Copy link
Contributor Author

Choose a reason for hiding this comment

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

(Contributing factor: nothing new should be needed on Mark's side to be able to handle the qualified names; that was purely a parser limitation)

Copy link
Contributor

Choose a reason for hiding this comment

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

Ah, I see. Should I understand that this just makes the parser recognize the submodule syntax, but doesn't actually do anything semantically meaningful with it?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes.

'and' { TReserved _ "and" }
'as' { TReserved _ "as" }
'hiding' { TReserved _ "hiding" }
Expand Down Expand Up @@ -89,6 +90,7 @@ import Control.Exception
'{' { TPunct _ "{" }
'}' { TPunct _ "}" }
':' { TPunct _ ":" }
'::' { TPunct _ "::" }
',' { TPunct _ "," }
'.' { TPunct _ "." }
'\\' { TPunct _ "\\" }
Expand Down Expand Up @@ -134,11 +136,12 @@ StmtSemi :: { Stmt }
: fst(Stmt, opt(';')) { $1 }

Import :: { Import }
: string mbAs mbImportSpec { Import (Left (unpack $ tokStr $1)) (fst $2) (fst $3) (maxSpan [tokPos $1, snd $2, snd $3])}
: string mbAs mbImportSpec { buildImport False $1 $2 $3 }
| 'submodule' string mbAs mbImportSpec { buildImport True $2 $3 $4 }
-- TODO: allow imports by module name instead of path

mbAs :: { (Maybe P.ModName, Pos) }
: 'as' name { (Just (P.packModName [tokStr $2]), maxSpan [$1, $2]) }
: 'as' QName { (Just (P.packModName (fst $2)), maxSpan' $1 (snd $2)) }
| {- empty -} { (Nothing, Unknown) }

mbImportSpec :: { (Maybe P.ImportSpec, Pos) }
Expand Down Expand Up @@ -271,6 +274,9 @@ Context :: { Type }
FieldType :: { (Name, Type) }
: name ':' Type { (tokStr $1, $3) }

QName :: { ([Text], Pos) }
: sepBy1(name, '::') { (map tokStr $1, maxSpan (map tokPos $1)) }

-- Parameterized productions, most come directly from the Happy manual.
fst(p, q) : p q { $1 }
snd(p, q) : p q { $2 }
Expand Down Expand Up @@ -356,6 +362,22 @@ parseError toks = case toks of
[] -> Left UnexpectedEOF
t : _ -> Left (UnexpectedToken t)

-- | Cons up an import.
buildImport ::
Bool ->
Token Pos ->
(Maybe P.ModName, Pos) ->
(Maybe P.ImportSpec, Pos) ->
Import
buildImport issub modName (mbAsName, asPos) (mbSpec, specPos) =
Import {
iIsSubmodule = issub,
iModule = Left (unpack $ tokStr modName),
iAs = mbAsName,
iSpec = mbSpec,
iPos = maxSpan [tokPos modName, asPos, specPos]
}

-- | As seen by the parser, a "function name" is an arbitrary pattern.
-- This is because we use the same syntax for function and value bindings:
-- in "let (a, b) = e" the "(a, b)" can and should be an arbitrary pattern.
Expand Down
Loading