Merge pull request #1915 from GaloisInc/T1892

Add `ogFromParam` to Cryptol URI when importing Cryptol names

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -72,7 +72,7 @@ import qualified Cryptol.Utils.Ident as C
   ( Ident, PrimIdent(..), mkIdent
   , prelPrim, floatPrim, arrayPrim, suiteBPrim, primeECPrim
   , ModName, modNameToText, identText, interactiveName
-  , ModPath(..), modPathSplit, ogModule, Namespace(NSValue)
+  , ModPath(..), modPathSplit, ogModule, ogFromParam, Namespace(NSValue)
   , modNameChunksText
   )
 import qualified Cryptol.Utils.RecordMap as C
@@ -1375,10 +1375,18 @@ importName cnm =
           let (topMod, nested) = C.modPathSplit (C.ogModule og)
               topChunks = C.modNameChunksText topMod
               modNms    = topChunks ++ map C.identText nested
+              -- If the name came from a module parameter, add the module
+              -- parameter identifier to distinguish between names that have the
+              -- same identifier but come from different module parameters (see
+              -- #1892)
+              ifaceNms  = case C.ogFromParam og of
+                            Just i  -> [C.identText i]
+                            Nothing -> []
               shortNm   = C.identText (C.nameIdent cnm)
-              longNm    = Text.intercalate "::" (modNms ++ [shortNm])
+              nmParts   = modNms ++ ifaceNms ++ [shortNm]
+              longNm    = Text.intercalate "::" nmParts
               aliases   = [shortNm, longNm]
-              uri       = cryptolURI (modNms ++ [shortNm]) Nothing
+              uri       = cryptolURI nmParts Nothing
            in pure (ImportedName uri aliases)
 
 -- | Currently this imports declaration groups by inlining all the

intTests/test1892/A.cry

@@ -0,0 +1,3 @@
+interface module A where
+
+a : [8]

intTests/test1892/F.cry

@@ -0,0 +1,6 @@
+module F where
+
+import interface A as X
+import interface A as Y
+
+f = X::a + Y::a

intTests/test1892/I.cry

@@ -0,0 +1,3 @@
+module I where
+
+a = 1

intTests/test1892/J.cry

@@ -0,0 +1,3 @@
+module J where
+
+a = 2

intTests/test1892/M.cry

@@ -0,0 +1 @@
+module M = F { X = I, Y = J }

intTests/test1892/test.saw

@@ -0,0 +1,2 @@
+import "M.cry";
+prove_print z3 {{ f == X::a + Y::a }};

intTests/test1892/test.sh

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