Merge pull request #104 from GaloisInc/tc-errors

Adapt to GaloisInc/cryptol#964 tc-errors.
GaloisInc · Nov 20, 2020 · d3cb3e3 · d3cb3e3
2 parents 94c8e51 + efd7592
commit d3cb3e3
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -265,7 +265,7 @@ importType sc env ty =
           do tf' <- importTFun sc tf
              tyargs' <- traverse go tyargs
              scApplyAll sc tf' tyargs'
-        C.TError _k _msg ->
+        C.TError _k ->
           panic "importType TError" []
   where
     go = importType sc env

diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
@@ -250,15 +250,15 @@ runInferOutput :: TM.InferOutput a -> MM.ModuleM a
 runInferOutput out =
   case out of
 
-    TM.InferOK warns seeds supply o ->
+    TM.InferOK nm warns seeds supply o ->
       do MM.setNameSeeds seeds
          MM.setSupply supply
-         MM.typeCheckWarnings warns
+         MM.typeCheckWarnings nm warns
          return o
 
-    TM.InferFailed warns errs ->
-      do MM.typeCheckWarnings warns
-         MM.typeCheckingFailed errs
+    TM.InferFailed nm warns errs ->
+      do MM.typeCheckWarnings nm warns
+         MM.typeCheckingFailed nm errs
 
 -- Translate -------------------------------------------------------------------
 
@@ -642,7 +642,7 @@ moduleCmdResult (res, ws) = do
     suppressDefaulting :: MM.ModuleWarning -> MM.ModuleWarning
     suppressDefaulting w =
       case w of
-        MM.TypeCheckWarnings xs -> MM.TypeCheckWarnings (filter (notDefaulting . snd) xs)
+        MM.TypeCheckWarnings nm xs -> MM.TypeCheckWarnings nm (filter (notDefaulting . snd) xs)
         MM.RenamerWarnings xs -> MM.RenamerWarnings xs
 
     notDefaulting :: TE.Warning -> Bool