Implement insantiating imports with { }

src/Cryptol/ModuleSystem/Base.hs

@@ -333,10 +333,10 @@ addPrelude m
   prel = P.Located
     { P.srcRange = emptyRange
     , P.thing    = P.Import
-      { iModule    = P.ImpTop preludeName
-      , iAs        = Nothing
-      , iSpec      = Nothing
-      , iWhere     = Nothing
+      { iModule  = P.ImpTop preludeName
+      , iAs      = Nothing
+      , iSpec    = Nothing
+      , iInst    = Nothing
       }
     }
 

src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs

@@ -106,7 +106,7 @@ mkImp loc xs =
                      { iModule = ImpNested (isToName xs)
                      , iAs     = Just (isToQual xs)
                      , iSpec   = Nothing
-                     , iWhere  = Nothing
+                     , iInst   = Nothing
                      }
       }
 

src/Cryptol/Parser.y

@@ -207,25 +207,18 @@ imports1                  :: { [ Located (ImportG (ImpName PName)) ] }
   | imports1 ';'  import     { $3 : $1 }
   | import                   { [$1] }
 
--- XXX replace rComb with uses of at
+
 import                          :: { Located (ImportG (ImpName PName)) }
-  : 'import' impName mbAs mbImportSpec optImportWhere
-                              { Located { srcRange = rComb $1
-                                                   $ fromMaybe (srcRange $2)
-                                                   $ msum [ fmap srcRange $4
-                                                          , fmap srcRange $3
-                                                          ]
-                                        , thing    = Import
-                                          { iModule    = thing $2
-                                          , iAs        = fmap thing $3
-                                          , iSpec      = fmap thing $4
-                                          , iWhere     = $5
-                                          }
-                                        } }
+  : 'import' impName optInst mbAs mbImportSpec optImportWhere
+                              {% mkImport $1 $2 $3 $4 $5 $6 }
 
 optImportWhere             :: { Maybe (Located [Decl PName]) }
   : 'where' whereClause       { Just $2 }
-  |                           { Nothing }
+  | {- empty -}               { Nothing }
+
+optInst                    :: { Maybe (ModuleInstanceArgs PName) }
+  : '{' modInstParams '}'     { Just $2 }
+  | {- empty -}               { Nothing }
 
 impName                    :: { Located (ImpName PName) }
   : 'submodule' qname         { ImpNested `fmap` $2 }

src/Cryptol/Parser/AST.hs

@@ -324,7 +324,7 @@ data Signature name = Signature
   , sigTypeParams   :: [ParameterType name]     -- ^ Type parameters
   , sigConstraints  :: [Located (Prop name)]    -- ^ Constraints on type params
   , sigFunParams    :: [ParameterFun name]      -- ^ Value parameters
-  } deriving (Eq,Show,Generic,NFData)
+  } deriving (Show,Generic,NFData)
 
 {- | A module parameter declaration.
 
@@ -358,9 +358,9 @@ data ImportG mname = Import
   { iModule    :: !mname
   , iAs        :: Maybe ModName
   , iSpec      :: Maybe ImportSpec
-  , iWhere     :: !(Maybe (Located [Decl PName]))
-    -- ^ `iWhere' exists only during parsing
-  } deriving (Eq, Show, Generic, NFData)
+  , iInst      :: !(Maybe (ModuleInstanceArgs PName))
+    -- ^ `iInst' exists only during parsing
+  } deriving (Show, Generic, NFData)
 
 type Import = ImportG ModName
 
@@ -883,15 +883,22 @@ instance PPName name => PP (Newtype name) where
     ]
 
 instance (PP mname) => PP (ImportG mname) where
-  ppPrec _ d = vcat [ text "import" <+> sep ([pp (iModule d)] ++ mbAs ++ mbSpec)
+  ppPrec _ d = vcat [ text "import" <+> sep ([pp (iModule d)] ++ mbInst ++
+                                                      mbAs ++ mbSpec)
                     , indent 2 mbWhere
                     ]
     where
     mbAs   = maybe [] (\ name -> [text "as" <+> pp name]) (iAs d)
     mbSpec = maybe [] (\x -> [pp x]) (iSpec d)
-    mbWhere = case iWhere d of
-                Nothing -> mempty
-                Just ds -> "where" $$ vcat (map pp (thing ds))
+    mbInst = case iInst d of
+                Just (DefaultInstArg x) -> [ braces (pp (thing x)) ]
+                Just (NamedInstArgs xs) -> [ braces (commaSep (map pp xs)) ]
+                _ -> []
+    mbWhere = case iInst d of
+                Just (DefaultInstAnonArg ds) ->
+                  "where" $$ vcat (map pp ds)
+                _ -> mempty
+ 
 
 instance PP name => PP (ImpName name) where
   ppPrec _ nm =

src/Cryptol/Parser/ParserUtils.hs

@@ -25,7 +25,7 @@ import Data.Maybe(mapMaybe)
 import Data.List(foldl')
 import Data.List.NonEmpty ( NonEmpty(..) )
 import qualified Data.List.NonEmpty as NE
-import Control.Monad(liftM,ap,unless,guard)
+import Control.Monad(liftM,ap,unless,guard,msum)
 import qualified Control.Monad.Fail as Fail
 import           Data.Text(Text)
 import qualified Data.Text as T
@@ -952,6 +952,55 @@ mkSelector tok =
     _ -> panic "mkSelector" [ "Unexpected selector token", show tok ]
 
 
+mkImport ::
+  Range ->
+  Located (ImpName PName) ->
+  Maybe (ModuleInstanceArgs PName) ->
+  Maybe (Located ModName) ->
+  Maybe (Located ImportSpec) ->
+  Maybe (Located [Decl PName]) ->
+  ParseM (Located (ImportG (ImpName PName)))
+
+mkImport loc impName optInst mbAs mbImportSpec optImportWhere =
+  do i <- getInst
+     let end = fromMaybe (srcRange impName)
+             $ msum [ srcRange <$> optImportWhere
+                    , srcRange <$> mbImportSpec
+                    , srcRange <$> mbAs
+                    ]
+
+     pure Located { srcRange = rComb loc end
+                  , thing    = Import
+                                 { iModule    = thing impName
+                                 , iAs        = thing <$> mbAs
+                                 , iSpec      = thing <$> mbImportSpec
+                                 , iInst      = i
+                                 }
+                  }
+  where
+  getInst =
+    case (optInst,optImportWhere) of
+      (Just _, Just _) ->
+         errorMessage loc [ "Invalid instantiating import."
+                          , "Import should have at most one of:"
+                          , "  * { } instantiation, or"
+                          , "  * where instantiation"
+                          ]
+      (Just a, Nothing)  -> pure (Just a)
+      (Nothing, Just a)  ->
+        pure (Just (DefaultInstAnonArg (map instTop (thing a))))
+         where
+         instTop d = Decl TopLevel
+                            { tlExport = Public
+                            , tlDoc    = Nothing
+                            , tlValue  = d
+                            }
+      (Nothing, Nothing) -> pure Nothing
+
+
+
+
+
 mkTopMods :: Module PName -> ParseM [Module PName]
 mkTopMods = desugarMod
 
@@ -1074,11 +1123,11 @@ desugarTopDs ownerName = go 1 emptySig
         case d of
 
           DImport i | ImpTop _ <- iModule (thing i)
-                    , Nothing  <- iWhere (thing i) ->
+                    , Nothing  <- iInst (thing i) ->
             cont [d] (addI i sig)
 
-          DImport i | Just lds <- iWhere (thing i) ->
-            do newDs <- desugarWhereImport st i (thing lds)
+          DImport i | Just inst <- iInst (thing i) ->
+            do newDs <- desugarInstImport st i inst
                cont' newDs (st + 1) sig
 
           DParamDecl _ ds' -> cont [] (jnSig ds' sig)
@@ -1089,18 +1138,16 @@ desugarTopDs ownerName = go 1 emptySig
 
           _ -> cont [d] sig
 
-desugarWhereImport ::
+desugarInstImport ::
   Int                               {- ^ Used to generate a fresh name -} ->
   Located (ImportG (ImpName PName)) {- ^ The import -} ->
-  [Decl PName]                      {- ^ The `where` clause -} ->
+  ModuleInstanceArgs PName          {- ^ The insantiation -} ->
   ParseM [TopDecl PName]
-desugarWhereImport st i ds =
+desugarInstImport st i inst =
   do ms <- desugarMod
            Module { mName = i { thing = iname }
                   , mDef  = FunctorInstance
-                              (iModule <$> i)
-                              (DefaultInstAnonArg (map instTop ds))
-                              emptyModuleInstance
+                              (iModule <$> i) inst emptyModuleInstance
                   }
      pure (DImport (newImp <$> i) : map modTop ms)
 
@@ -1113,7 +1160,7 @@ desugarWhereImport st i ds =
             ImpNested n -> Text.pack (show (pp n))
 
   newImp d = d { iModule = ImpNested iname
-               , iWhere  = Nothing
+               , iInst   = Nothing
                }
 
   modTop m = DModule TopLevel
@@ -1124,11 +1171,3 @@ desugarWhereImport st i ds =
 
 
 
-  instTop d = Decl TopLevel
-                     { tlExport = Public
-                     , tlDoc    = Nothing
-                     , tlValue  = d
-                     }
-
-
-

tests/modsys/functors/T023.cry

@@ -0,0 +1,13 @@
+module T023 where
+
+submodule F where
+  parameter
+    x : [8]
+
+  y = x + 1
+
+submodule G where
+  x = 2
+
+import submodule F { submodule G }
+

tests/modsys/functors/T023.icry

@@ -0,0 +1,2 @@
+:load T023.cry
+y

tests/modsys/functors/T023.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T023
+0x03

tests/modsys/functors/T024.cry

@@ -0,0 +1,14 @@
+module T023 where
+
+submodule F where
+  parameter
+    x : [8]
+
+  y = x + 1
+
+submodule G where
+  x = 2
+
+import submodule F { submodule G }
+  where z = 2
+

tests/modsys/functors/T024.icry

@@ -0,0 +1 @@
+:load T024.cry

tests/modsys/functors/T024.icry.stdout

@@ -0,0 +1,7 @@
+Loading module Cryptol
+
+Parse error at T024.cry:12:1--12:7
+  Invalid instantiating import.
+  Import should have at most one of:
+    * { } instantiation, or
+    * where instantiation