Add two missing bits to SAWScript's Cryptol import syntax.

- allow the word "submodule" (it is currently ignored, but that will
  likely change soon)

- allow the import name to be qualified (as in "...as M::N")

Add a test for the latter part.

Author: sauclovian-g

intTests/test2605/Foo.cry

@@ -0,0 +1,4 @@
+module Foo where
+
+x : [8]
+x = 3

intTests/test2605/test.saw

@@ -0,0 +1,3 @@
+import "Foo.cry" as Moo::Boo;
+
+let y = {{ Moo::Boo::x }};

intTests/test2605/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

saw-central/src/SAWCentral/AST.hs

@@ -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

saw-script/src/SAWScript/Lexer.x

@@ -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

saw-script/src/SAWScript/Parser.y

@@ -51,6 +51,7 @@ import Control.Exception
 
 %token
   'import'       { TReserved _ "import"         }
+  'submodule'    { TReserved _ "submodule"      }
   'and'          { TReserved _ "and"            }
   'as'           { TReserved _ "as"             }
   'hiding'       { TReserved _ "hiding"         }
@@ -89,6 +90,7 @@ import Control.Exception
   '{'            { TPunct    _ "{"              }
   '}'            { TPunct    _ "}"              }
   ':'            { TPunct    _ ":"              }
+  '::'           { TPunct    _ "::"             }
   ','            { TPunct    _ ","              }
   '.'            { TPunct    _ "."              }
   '\\'           { TPunct    _ "\\"             }
@@ -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) }
@@ -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 }
@@ -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.